Machine-checked theorems live in product Lean modules under beastdb/.
This document is a living stub: counts are regenerated from the tree;
they are not a substitute for reading the modules.
Policy (G12.1): product Lean under beastdb/ must contain no sorry.
Enforced by flake check checks.no-sorry (nix build .#checks.x86_64-linux.no-sorry
or nix flake check). Default-build modules must not land sorry.
Stack: Lean 4 only (no mathlib). Proofs use core Lean tactics and module-local lemmas.
Counted on 2026-07-09 (Workstream J + post-Horizon inventory) from line-start
declarations matching ^\s*(private\s+|protected\s+)?theorem\s (and the same
optional modifiers for def / structure / inductive / abbrev) in
beastdb/*.lean.
Private and protected theorems are included (public-only would under-count
helper proofs). Attributes on the preceding line (@[...]) are not
folded into the count; multi-line attributes may appear later.
Refresh after material proof work (commands below). Horizon 5 added G19 EtM /
product AEAD theorems in Persist.lean (requireAuth gate, concrete wrong-key
demos, MAC trailer demos). Workstream J added pure Structural CAS / session
theorems in Engine.lean.
Wave 8: beastdb.Compress / beastdb.Crypto co-located in Persist.lean.
Horizon 1: beastdb.Cost co-located in Compact.lean.
Horizon 2: Msg / ForkJoin / Mwmr / Resource co-located in Engine.lean.
Horizon 3: Bulk co-located in Persist.lean.
Horizon 4: Resource linear/affine encodings in Engine.lean.
Horizon 5: product AEAD EtM composition theorems in Persist.lean.
Workstream J: beastdb.Structural co-located in Engine.lean. No sorry.
Refresh snapshot (2026-07-09): 506 theorems total; Engine.lean 218
(includes Msg / ForkJoin / Mwmr / Resource H4 / Structural J). Persist.lean
135 (G19 EtM + empty-key gates + Layout frame proofs + Bulk). No sorry.
These counts are inventory only - they do not claim end-to-end IO proofs.
Notes:
Main.lean/PersistIO.lean/StoreDir.leanare mostly executable / IO surface (few or no theorems).- Nested
theoreminsidesection/namespacestill match the line pattern. - Counts are intentionally coarse (proof-stats for operators/reviewers, not a formal metric).
rg (ripgrep) is on PATH in nix develop (pkgs.ripgrep). You can also use
a host rg or nix-shell -p ripgrep. From the repository root:
# Pattern: optional private/protected before theorem/def/...
TH='^\s*(private\s+|protected\s+)?theorem\s'
DF='^\s*(private\s+|protected\s+)?def\s'
# Per-module theorem counts
for f in beastdb/*.lean; do
printf '%s\t' "$f"
rg -c "$TH" "$f" || echo 0
done
# Totals
rg -c "$TH" beastdb/*.lean | awk -F: '{s+=$2} END {print "theorems", s+0}'
rg -c "$DF" beastdb/*.lean | awk -F: '{s+=$2} END {print "defs", s+0}'
# No-sorry gate (same idea as checks.no-sorry; that check uses grep)
rg -n --glob '*.lean' '(^|[^a-zA-Z_])sorry([^a-zA-Z_]|$)' beastdb/ && echo FAIL || echo okAfter material proof work, update the table above and the date line, and note
the change in release notes.
| Area | Status |
|---|---|
Append-only log (Basic) |
Length / prefix / last-element lemmas |
Latest-value KV (KV) |
get/put equations |
Prefix routing (Routing) |
Coverage, split well-formedness, route uniqueness |
Multi-shard engine (Engine) |
ShardsCover, LRR preservation, compact/split/reconcile get equations; compactOne; get_compactOne_comm (G6.4) |
Split lifecycle (Lifecycle in Engine) |
Epoch model; dual-read getPolicy; splitAndReconcile_get / begin_finish_get / SC restore |
SWMR concurrency (Concurrency in Engine) |
Well-formed lock histories; idempotent nested beginWrite / bare endWrite (product-aligned); reader-during-write; immutability note reader_snapshot_vs_writer_put (not interleaving); lock-efficiency: step_put_from_free_no_excess_hold / run_serial_puts_leave_free / get_not_exclusive / step_get_during_session_preserves_exclusive (needed exclusivity only in pure automaton). Pure!=product put lock: pure Op.put steps under the global exclusive automaton; product default put holds per-leaf shard-<id>.lock only (G22). Do not read pure SWMR put exclusivity as "two concurrent product puts impossible" - disjoint leaves may put multi-process |
MWMR leaf leases (Mwmr in Engine) |
Disjoint acquire + conflict fail closed; tryAcquire_disjoint_both_held (two leaf leases concurrent); tryPut lease soundness. Pure lease world is not multi-process file locks; product G22 maps to per-leaf shard-*.lock + WAL (mwmr-smoke) |
L3 messages (Msg in Engine) |
deliver_off_store / deliver_off_rejected / deliverAll_off_store / drain_off_store; deliver_acquire_rejected / deliver_release_rejected (Mwmr-only leases); enabled compact/put get equations; empty step |
L2 fork-join (ForkJoin in Engine) |
get_compactSchedule / get_compactSchedule_any / pair / get_compactSchedule_rev; leafSchedule / compactLeaves / get_compactLeaves / get_compactLeaves_rev / get_compactLeaves_any; multiGet_parallel_eq (definitional rfl - same pure fold both sides; not Lean Task / multi-core evaluation) / multiGet_compactSchedule; keysForShard_sound. Product multi-shard compact uses same leaf schedule (F1; durable IO sequential under SWMR; F2 closed measured residual - no multi-core compact claim) |
Pure MWMR (Mwmr in Engine) |
tryPut_get_eq / tryPut_no_lease / tryPut_wrong_holder; tryAcquire_init / tryAcquire_nonleaf / tryAcquire_conflict_fresh; holder_clear / tryPut_after_matching_release (general); concrete tryPut_after_release Bool; disjoint put Bool histories (not multi-process IO refinement; product multi-process put is G22 + smokes) |
Pure concurrent structural (Structural in Engine, Workstream J) |
Generation-fenced CAS publish: tryCasPublish_stale / tryCasPublish_success / tryCasPublish_race_loser / tryCasPublish_get (via splitAndReconcile_get); session path: trySessionPublish_stale / trySessionPublish_race_loser / trySessionPublish_no_holder / trySessionPublish_wrong_holder / trySessionPublish_success; unique structural session: tryAcquireStructural_init / tryAcquireStructural_conflict (general) / tryAcquireStructural_nested_eq / structuralAuthorize_unique / releaseStructural_matching; put path: tryPut_no_lease / tryPut_get_eq. Honesty: race loser = single shared-state lineage on free-copy State values (not free-copied pre-publish multi-world re-check); leases preserved across publish (orphaned-leaf residual; puts fail closed via route re-check). Concrete Bool demos (casRaceOneWins?, dualStructuralConflict?, sessionPublishFence?, disjointPutAfterPublish?, sessionAfterReleaseFail?) are demos, not multi-process IO. Product (Track 3, not pure theorems): multi-process uniqueness = short cooperative LOCK + durable lifecycle epoch fence (struct-smoke). Pure CAS theorems do not prove lock-free dual MANIFEST publishers; short exclusive remains required (Next-4 / R3; SYSTEMS.md §4). Not linearizability / kernel leases |
Resource handles (Resource in Engine, G18/H4) |
Exclusive write: authorize_unique (at most one exclusive token); authorize_endWrite_returned / authorize_stale_after_matching_end / endWrite_matching_frees; dual begin = nested beginWrite_nested_eq idempotent, busy empty beginWrite_busy_empty_none + busy mismatch beginWrite_busy_mismatch_none fail closed. Affine snapshots: get-only; write paths fail closed; free-copy residual (flag on value, not language-affine). Buffers: consume double-use Prop from init; consumeAligned_eq_consume_of_require + consumeAligned_then_consume_none_init / bufferDiscipline? for aligned path; no full WF on arbitrary live lists. Not language linear types; product leaseToken free-copy + runtime re-verify |
Compaction (Compact / Levels) |
Latest-value semantics, key uniqueness; length_mergeRuns_le / length_mergeRuns_lt; lookup_flush / lookup_mergeTop / lookup_compactAll / get_toCompactStore |
| Get path (G14 + Workstream E + Tier B + Next-1 / R1 put-maintain) | latestRev_eq_latest / get?_eq_latest (unique flag + inv ⇒ TreeMap index or reverse ≡ fold-latest); buildUniqueIndex_get?_eq_latest (index ≡ fold-latest under Nodup); latestUnique_eq_latest_of_nodup / latestUnique_compactList / get_compact_eq_latestUnique; keysUnique_ofEntries_of_nodup / keysUnique_ofEntries_iff (wire ofEntries re-detects unique residual + builds index); put-maintain: entries_put / keysUnique_put_fresh (fresh key on unique residual keeps TreeMap + insert) / keysUnique_put_dup (overwrite clears unique) / keysUnique_put_multi; Plan Step 3: distinct-key multi-put get closed measured win; overwrite accepted residual / compact discipline; not O(1) |
Cost model (beastdb.Cost in Compact.lean) |
Nat steps: treeLookupCost / treeLookupCost_le_len, uniqueLookupCost_le_fold, unique_le_fold_on_compactList, revLookupCost_ge_len, rev_scan_hit_last, productLookupCost / productLookupCost_compact_le_rev (same residual only - not pre- vs post-compact wall; reverse residual is overwrite/non-unique after R1), bulkByteFoldCost_eq - not wall-clock |
| Wire normalize (Workstream E + Tier B) | decode_encode_store / string round-trips recover normalizeStore (entries; keysUnique not on wire - re-detected from residual via ofEntries) |
L1 bulk (Bulk in Persist) |
charsToBytes_bytesToChars + bytesToChars_of_charsToBytes?; injectivity; charToByte?_none_of_ge / charsToBytes?_none_of_head / charToByte?_gamma_none; checksumFnv1a32Bytes_eq_chars / checksumFnv1a32Bytes_foldl; bytesEq_iff / keyEq_iff; length_mergeSortedKeys / length_mergeSortedBytes; pad/truncate alignment - scalar only; Workstream I: not product SIMD (measured residual keeps scalar) |
Snapshot codec (Persist) |
Encode/decode round-trips (v1 + v2); validated/strict soundness; Bool↔Prop LRR; shared fnv1a32Step |
| Product AEAD / EtM (G19) | Gate: productAeadOk?_requireAuth_enc_only / productAeadOk?_requireAuth_empty_keys / productAeadOk?_productAead_empty_lists / encodeStoreOpts_requireAuth_enc_only_empty / productAead_ok; concrete demos: round-trip, wrong MAC/enc none, enc-only refuse + envelope refuse; MAC trailer demos; decrypt_encrypt / macVerify_*. productAead_is_etm is opts shape only (both keys set isEncryptThenMac?) - not AEAD security. Not NIST AEAD |
Resource bounds (Bounds in Persist) |
totalEntries_compact_le; resourceOk_compact; resourceOk_empty_binary - not a proved encode-size formula (computable check only) |
| MANIFEST / shard blobs | v1 shard + MANIFEST round-trips; v2 multi-level decode_encode_levels_blob (store = Levels.toStore); assemble soundness |
WAL recovery (Wal) |
Put apply = sequential Engine.put; get_applyWal / recover_puts |
Disk IO (PersistIO, StoreDir) |
Not proved end-to-end (IO effects); protocols documented |
Benchmarks (Main bench / LMDB) |
Not proved; environment-dependent samples in BENCHMARKS.md |
Trusted computing base for the extracted binary includes the Lean compiler, generated C, and the host C toolchain under Nix - not re-proved here.
| Check | Command |
|---|---|
| Name | nix build .#namecheck |
| Product + proofs | nix build .#beastdb |
No sorry |
nix build .#checks.x86_64-linux.no-sorry (or nix flake check) |
| Demo (incl. corrupt reject) | nix build .#checks.x86_64-linux.demo |
| Crash suite (G13 + Workstream G + Track 4 + Tier D honesty: cooperative simulated multi-file, per-leaf WAL, image mid-body/junk, mid-migrate residual, production temps, compact-on-publish, mid-checkpoint WAL re-apply; not power-fail / not kill-9 mid-write under CI) | nix build .#checks.x86_64-linux.crash-suite |
| Multi-process SWMR smoke (G13) | nix build .#checks.x86_64-linux.swmr-smoke |
| Multi-process MWMR put smoke (G22) | nix build .#checks.x86_64-linux.mwmr-smoke |
| Multi-process generation-fenced structural smoke (Track 3) | nix build .#checks.x86_64-linux.struct-smoke |
| Single-file image layout smoke (G23) | nix build .#checks.x86_64-linux.layout-smoke |
| Horizon 2 pure L2/L3/MWMR + Workstream J Structural (G15-G16 / J) | nix build .#checks.x86_64-linux.horizon2 |
| Horizon 3 L1 bulk kernels (G17; scalar / Workstream I residual) | nix build .#checks.x86_64-linux.horizon3 |
| Horizon 4 linear/affine resources (G18) | nix build .#checks.x86_64-linux.horizon4 |
| Horizon 5 product AEAD + shard locks (G19-G20) | nix build .#checks.x86_64-linux.horizon5 |
| Small-N bench | nix build .#checks.x86_64-linux.bench |
| Full suite | nix flake check |
| Layer | Where | Claim type |
|---|---|---|
| Nat step costs | beastdb.Cost, Bulk.byteFoldCost |
Relative efficiency theorems only |
| Wall-clock | BENCHMARKS.md, beastdb bench |
Environment-dependent samples |
| Methodology SOP | SYSTEMS.md §6 | Proof↔measure loop; never "proved fast" without measure |
| Concern | Machine-checked (pure) | Runtime / product IO |
|---|---|---|
| Exclusive writer uniqueness | authorize_unique (same token when both authorize); ghost LeaseWorld.currentToken |
Global file LOCK + leaseToken re-verify (Wave 6 SWMR) |
Use after endWrite |
Returned + stale free-copy authorize = false | Stale handle -> Error.concurrent via verifyLease |
| Dual / nested begin | Nested matching idempotent; busy empty and busy non-matching token -> none |
Nested beginWrite reuses session; second process -> concurrent |
| Snapshot not write | snapshotWriteLease / authorizeWriteFromSnapshot always fail closed |
Readers openStore without exclusive lock; no write lease from snapshot |
| Snapshot free-copy | Flag-based on the value; release does not kill other free-copies that still have live = true |
Same class as lease free-copy - API re-check, not language affine |
| Buffer double-consume | consume Prop from init; consumeAligned = consume when align-gate passes + consumeAligned_then_consume_none_init / Bool AOT; init-chain only (no full WF) |
No product buffer-token IO yet; Bulk kernels are pure byte ops |
| Per-shard exclusive | tryPut_after_matching_release (general) + concrete tryPut_after_release + acquire conflict |
Product G22: per-leaf lock + WAL; AOT mwmr-smoke (not pure theorem) |
| Language linear types | Not claimed - Lean encodes affine/linear via API + world + proofs | Free-copy values remain; discipline is re-check fail-closed |
High reading risk: inventory rows above name pure modules that are easy to over-read as multi-process or lock-free product guarantees. This table is the explicit mismatch map. Lock resource budget (product exclusive resources): SYSTEMS.md § lock resource budget.
| Pure claim surface | What the pure model actually is | What product does | Do not conclude |
|---|---|---|---|
Concurrency put exclusive |
Sequential global lock automaton: free-path Op.put takes virtual exclusive for the step only (step_put_from_free_no_excess_hold) |
Default product put: per-leaf shards/shard-<id>.lock + per-leaf WAL; global LOCK only for session / checkpoint / compact / structural publish |
"Two concurrent product puts are impossible" - false for disjoint leaves (G22 mwmr-smoke) |
Mwmr leaf leases |
Pure lease map on one store value; conflict / disjoint acquire theorems | Cooperative per-leaf lock files + WAL append; not kernel leases | Multi-process linearizability or OS-enforced exclusivity against foreign processes |
Structural CAS / race loser |
Single-lineage free-copy State + generation fence; race theorems on that lineage |
Multi-process: hold short global LOCK, reload durable base, check lifecycle epoch, publish under exclusive (struct-smoke) |
Pure race theorems prove lock-free dual MANIFEST publishers - they do not; short LOCK required today |
ForkJoin.multiGet_parallel_eq |
Definitional equality (rfl) of two pure folds with the same schedule |
Product multi-get / multi-shard compact evaluate sequentially (F1 schedule wiring; F2 closed measured residual) | Inventory "parallel" means Lean Task multi-core wall-clock speedup |
Resource.authorize_* |
Ghost exclusive token uniqueness on pure world | Product free-copies leaseToken / handles; runtime re-verify -> concurrent / closed -> validation |
Language linear types or disk-invalidation of free-copy pre-close values |
Bool / native_decide demos |
Concrete finite histories machine-checked | Same - demos only | Universal multi-process safety from demo count or theorem inventory size |
Still not proved end-to-end (Track P-B): disk IO open/put/sync/crash paths;
multi-file multi-step publish windows; mid-schedule compact handle lag after a
prefix of leaves; optional WAL fsync failure leaving memory committed; FFI
fork/exec bridge. Operator packaging: LIMITS.md § operator safety.
Evidence for product concurrency is AOT smokes (swmr-smoke, mwmr-smoke,
struct-smoke) + crash-suite fixtures - not pure refinement of IO.
Correctness obligations pure theorems help gate when code changes (P-F):
- Product
putuniqueness (R1 put-maintain - do not clear on every put):- Fresh key on a unique residual (
get? k = none): must keepkeysUniqueandTreeMap.insertintouniqueIndex(theoremskeysUnique_put_fresh/entries_put; preservesinv/get?_eq_latest). - Overwrite / already-present key on a unique residual: must clear
keysUniqueand dropuniqueIndex(log now has dups; theoremkeysUnique_put_dup- else TreeMap get can disagree with fold-latest). - Non-unique residual: put stays non-unique (no TreeMap path until compact / re-detect). Plan Step 3 residual honesty: distinct-key path is closed measured win; overwrite is accepted residual / compact discipline.
- Fresh key on a unique residual (
ofUnique/ compact mustbuildUniqueIndexfrom the same residual entries (inv).ofEntriesNodup re-detect after WAL apply must match residual reality.- Structural product must re-load expected generation under
LOCK(pure CAS alone is insufficient for multi-file publish). classifyIO: validation before corrupt for overlapping substrings (authKey/encKey).- FFI field max vs capture max stay consistent.
See also: GAPS.md (G12), LIMITS.md, SYSTEMS.md, VISION.md.