Code

Amortized hash non resizing#18

Code

Merged

hei411 merged 21 commits intomainlogsem/clutch:mainfrom constant_hashlogsem/clutch:constant_hashCopy head branch name to clipboardFeb 6, 2024

+1,259-11

Commits

Commits on Jan 29, 2024

• Amortized hash non resizing

  hei411

  committed
  4b05c4e

  Copy full SHA for 4b05c4e

Commits on Jan 30, 2024

• amortized hash spec now uses spec of non-amortized

  hei411

  committed
  25bdb1e

  Copy full SHA for 25bdb1e

• Second try, not sure why check failed

  hei411

  committed
  9f3b3d4

  Copy full SHA for 9f3b3d4

• progress with merkel tree

  hei411

  committed
  6491bf3

  Copy full SHA for 6491bf3

• Change merkel to merkle. Also change many proposition to inductive

  hei411

  committed
  8e7cc92

  Copy full SHA for 8e7cc92

Commits on Feb 1, 2024

• merkle tree example when hash is correct

  hei411

  committed
  d7e2672

  Copy full SHA for d7e2672

• merkle tree done, but wrong implementation :)

  hei411

  committed
  bb51d1e

  Copy full SHA for bb51d1e

• Start writing 2nd version of the code

  hei411

  committed
  e9815b8

  Copy full SHA for e9815b8

Commits on Feb 2, 2024

• merkle tree done

  hei411

  committed
  17c0c8c

  Copy full SHA for 17c0c8c

• Added a helper function

  hei411

  committed
  3a452ca

  Copy full SHA for 3a452ca

• add lemma for incorrect proof

  hei411

  committed
  39cd2dc

  Copy full SHA for 39cd2dc

• Prove 2 out of four cases of the incorrect proof lemma

  hei411

  committed
  c57e605

  Copy full SHA for c57e605

• Add lemma for incorrect proof but correct leaf

  hei411

  committed
  306d848

  Copy full SHA for 306d848

Commits on Feb 5, 2024

• Improve spec of wp lemmas + prove converse of incorrect correct proof proposition

  hei411

  committed
  7c8e2b4

  Copy full SHA for 7c8e2b4

• small fix

  hei411

  committed
  35ad507

  Copy full SHA for 35ad507

• General spec

  hei411

  committed
  1f1696c

  Copy full SHA for 1f1696c

• added comments

  hei411

  committed
  2d47515

  Copy full SHA for 2d47515

• Wrote program for unreliable storage

  hei411

  committed
  b3be3ba

  Copy full SHA for b3be3ba

• small fix, using unreliable alloc

  hei411

  committed
  fd5bdf8

  Copy full SHA for fd5bdf8

• Using new axioms to implement program

  hei411

  committed
  ecf0a28

  Copy full SHA for ecf0a28

Commits on Feb 6, 2024

• update ltac of total

  hei411

  committed
  8bbe5ea

  Copy full SHA for 8bbe5ea