Benchmark/vendor examples specs - #131

Draft

lemmy wants to merge 37 commits into

mainfrom

benchmark/vendor-examples-specs

Commits on Aug 20, 2026

fix(dataset): rewrite an EXTENDS clause whose keyword stands alone
lemmy
committed
88369ec
fix(dataset): drop a RECURSIVE declaration whose definition was stripped
lemmy
committed
18d1e89
benchmark: vendor bosco with its TLC-checked invariants as theorems
lemmy
committed
7ebf58e
benchmark: vendor the Disruptor ring buffer with its TLC-checked invariants
lemmy
committed
fe67ec6
benchmark: vendor braf verbatim
lemmy
committed
cf211c7
refactor(braf): one module per file
lemmy
committed
23acc89
braf: assume the constants are what their comments describe
lemmy
committed
ae6b677
benchmark: state braf's TLC-checked invariants and properties as theorems
lemmy
committed
ae09ac9
benchmark: vendor btree verbatim
lemmy
committed
526da98
refactor(btree): define FindLeafNode as a recursive function
lemmy
committed
14a997b
btree: assume the size constants are naturals
lemmy
committed
83d8a42
benchmark: state btree's TLC-checked invariants as theorems
lemmy
committed
c387da0
benchmark: vendor Nano verbatim
lemmy
committed
5d52da3
refactor(Nano): define PublicKeyOf as a recursive function
lemmy
committed
779145b
refactor(Nano): inline ValueOfSendBlock into a recursive BalanceAt
lemmy
committed
5d8584e
refactor(Nano): define SumBag as a recursive function over the bag's support
lemmy
committed
fbb994e
benchmark: take Nano's Safety theorem as a proof-from-scratch task
lemmy
committed
c76caf4
benchmark: vendor Sailfish verbatim
lemmy
committed
9bf20b8
refactor(Digraph): define Descendants as a recursive function
lemmy
committed
29139bb
refactor(BlockDag): define OrderSet as a recursive function
lemmy
committed
c716c0d
refactor(BlockDag): define Linearize as a recursive function over sub-dags
lemmy
committed
19d68e8
Sailfish: assume the quorum system's intersection properties
lemmy
committed
90c5b64
benchmark: state Sailfish's TLC-checked invariants as theorems
lemmy
committed
c563ae5

Commits on Aug 21, 2026

benchmark: name the module-level assumptions of the vendored specs
lemmy
committed
ac43921
benchmark: name Nano's assumption too
lemmy
committed
6cf37df
fix(dataset): satisfy ruff in the RECURSIVE pruning helper
lemmy
committed
e5a66ca
NOTICE: record how Sailfish's assumptions were checked
lemmy
committed
4e5bd6e
NOTICE: correct why the assumptions carry names
lemmy
committed
1dd5711

Commits on Aug 23, 2026

Commits on Aug 24, 2026

Commits on Aug 27, 2026

Merge branch 'main' into benchmark/vendor-examples-specs
lemmy
committed
605afa2