Code

Fisher-Yates: Equivalence proof#142

Code

Merged

stefan-aws merged 36 commits intomaindafny-lang/Dafny-VMC:mainfrom equivalencedafny-lang/Dafny-VMC:equivalenceCopy head branch name to clipboardFeb 5, 2024

+72-24

Commits

Commits on Jan 29, 2024

• skeleton

  stefan-aws

  committed
  011f865

  Copy full SHA for 011f865

• fix tests.dfy

  stefan-aws

  committed
  6920653

  Copy full SHA for 6920653

• proof fixes

  stefan-aws

  committed
  d8e86dd

  Copy full SHA for d8e86dd

• Remove axioms

  stefan-aws

  committed
  25e8b64

  Copy full SHA for 25e8b64

• types

  stefan-aws

  committed
  395aa1e

  Copy full SHA for 395aa1e

• audit and brackets

  stefan-aws

  committed
  d77e30f

  Copy full SHA for d77e30f

Commits on Jan 30, 2024

• factorialtraditional

  stefan-aws

  committed
  5513c9b

  Copy full SHA for 5513c9b

• audit etc

  stefan-aws

  committed
  29a831d

  Copy full SHA for 29a831d

• inductionhypothesis

  stefan-aws

  committed
  ccb5641

  Copy full SHA for ccb5641

• progress for induction hypthesis precondition

  stefan-aws

  committed
  addb406

  Copy full SHA for addb406

• ih progress

  stefan-aws

  committed
  4f98c5a

  Copy full SHA for 4f98c5a

• towards ih precondition

  stefan-aws

  committed
  f8d60c8

  Copy full SHA for f8d60c8

• towards ih precondition

  stefan-aws

  committed
  c282170

  Copy full SHA for c282170

• remove remaining axioms in one part of ih precond

  stefan-aws

  committed
  9bb2127

  Copy full SHA for 9bb2127

• rlimit, split, etc

  stefan-aws

  committed
  41ee247

  Copy full SHA for 41ee247

• one line fix

  stefan-aws

  committed
  b5df12b

  Copy full SHA for b5df12b

• progress main proof

  stefan-aws

  committed
  6408fc8

  Copy full SHA for 6408fc8

• probabilityofe separate lemma

  stefan-aws

  committed
  f7ece57

  Copy full SHA for f7ece57

• InductionHypothesisPrecondition1

  stefan-aws

  committed
  453c6b9

  Copy full SHA for 453c6b9

• EInEventSpace

  stefan-aws

  committed
  470099e

  Copy full SHA for 470099e

• format and audit

  stefan-aws

  committed
  06641dd

  Copy full SHA for 06641dd

• InductionHypothesisPrecondition2 proof

  stefan-aws

  committed
  34b84d9

  Copy full SHA for 34b84d9

Commits on Jan 31, 2024

• DecomposeE Proof

  stefan-aws

  committed
  64f63ab

  Copy full SHA for 64f63ab

• BitStreamsInA Proof

  stefan-aws

  committed
  4874ac1

  Copy full SHA for 4874ac1

• full proof minus one axiom

  stefan-aws

  committed
  40fae99

  Copy full SHA for 40fae99

• model

  stefan-aws

  committed
  d84f88d

  Copy full SHA for d84f88d

• remove last axiom

  stefan-aws

  committed
  9f44e6c

  Copy full SHA for 9f44e6c

• Merge branch 'main' into fisher-yates-model-correctness-unique-elements

  stefan-aws

  authored
  4f58d17

  Copy full SHA for 4f58d17

Commits on Feb 1, 2024

• factorial traditional in tests

  stefan-aws

  committed
  2b79acf

  Copy full SHA for 2b79acf

• Merge branch 'fisher-yates-model-correctness-unique-elements' of https://github.com/dafny-lang/dafny-vmc into fisher-yates-model-correctness-unique-elements

  stefan-aws

  committed
  fe5a8fd

  Copy full SHA for fe5a8fd

• equivalence proof prior cleanup

  stefan-aws

  committed
  0d969dc

  Copy full SHA for 0d969dc

• shorten equivalence proof

  stefan-aws

  committed
  d251afe

  Copy full SHA for d251afe

• swap interop

  stefan-aws

  committed
  5a66a14

  Copy full SHA for 5a66a14

• remove simplification to fix correctness proof

  stefan-aws

  committed
  3b40ceb

  Copy full SHA for 3b40ceb

• naming issue, interface

  stefan-aws

  committed
  79dad82

  Copy full SHA for 79dad82

Commits on Feb 5, 2024

• Merge branch 'main' into equivalence

  stefan-aws

  authored
  e114353

  Copy full SHA for e114353