Repository navigation

chore: add bmt formal verification - #2030

Draft

ananas-block wants to merge 28 commits into

mainfrom

jorrit/refactor-tests

Draft

chore: add bmt formal verification#2030
ananas-block wants to merge 28 commits into
mainfrom
jorrit/refactor-tests

Commits on Oct 29, 2025
- refactor: batched merkle tree unit test
  ananas-block
  committed
  8a46fcc
- refactor: batched merkle tree integration tests
  ananas-block
  committed
  bca3c71
- cleanup test import warnings
  ananas-block
  committed
  a484485
- fix: address queue e2e test
  ananas-block
  committed
  3fa2582
- test: add better address root asserts
  ananas-block
  committed
  624a013
- more address tree asserts
  ananas-block
  committed
  a64d43a
- stash docs
  ananas-block
  committed
  128eec5
- add init state tree docs
  ananas-block
  committed
  dd387df
- add init address tree docs
  ananas-block
  committed
  14ddd81
- add insert into output queue doc
  ananas-block
  committed
  d33b7c9
- add insert into input queue doc
  ananas-block
  committed
  0549429
- add insert into address queue doc
  ananas-block
  committed
  4f2b456
- add update from output queue doc
  ananas-block
  committed
  290d8ba
- add update from input queue doc
  ananas-block
  committed
  11fd44c
Commits on Oct 30, 2025
- add kani for batch
  ananas-block
  committed
  4aff74c
- zero out root one kani check works
  ananas-block
  committed
  c5ae8b9
Commits on Oct 31, 2025
- batched merkle tree integration tests work, simulate no advanced root checks yet
  ananas-block
  committed
  0240adf
Commits on Nov 2, 2025
- simulate works with extended asserts
  ananas-block
  committed
  3f21a74
- fix lint
  ananas-block
  committed
  112e406
- cleanup
  ananas-block
  committed
  3bad7a1
- feat: kani versions for cyclic and zero copy vec
  ananas-block
  committed
  0b80971
Commits on Nov 3, 2025
- stash more kani conditions
  ananas-block
  committed
  8a589fb
- stash state tree update from input queue
  ananas-block
  committed
  04cae12
- add verify_state_tree_append_minimal, verify_state_tree_append_one_by_one
  ananas-block
  committed
  2751e49
- add verify_state_tree_mixed_random, verify_state_tree_mixed_one_by_one
  ananas-block
  committed
  e9a637b
- fmt and fix lint
  ananas-block
  committed
  746ea8a
Commits on Nov 4, 2025
- refactor: verify_state_tree_mixed_random
  ananas-block
  committed
  77e0155
Commits on Nov 10, 2025
- fix fv
  ananas-block
  committed
  2dd0da7

Commits

Commits on Oct 29, 2025

Commits on Oct 30, 2025

Commits on Oct 31, 2025

Commits on Nov 2, 2025

Commits on Nov 3, 2025

Commits on Nov 4, 2025

Commits on Nov 10, 2025