This note records what pure Lean 4 + Nix can and cannot do yet for persistence and systems-facing behavior. It is intentionally conservative: prefer measured or API-level facts over marketing claims.
Standing project directive (AGENTS.md): freestanding beastdb is a
primary long-term architecture goal. Goal: systems-class in-process embed, engine
developed in Lean, without a managed Lean runtime in the consumer. Plan:
.agents/plans/plan-systems-embed-gap.md.
Compiler feature set (fork seed): LEAN4.md. Measure evidence pipeline:
BENCHMARKS.md (G24 / YCSB / LMDB / freestanding thr) - quantifies
ship vs freestanding; does not close R7-RT by itself.
| Flake package | Role |
|---|---|
nix build .#libbeastdb |
Default freestanding product library - Systems Lean best-effort spine libbeastdb.a (put/get/delete/sync + index + read-side mmap get + dir/DATA); no libleanshared. Gate: nix run .#freestanding-gate. Product direction. Original thr exact fields vs export residual: BENCHMARKS.md § Original baseline figures (N=10000 stamp 20260715T0452Z - compare future Systems Lean to those prints, not rounded factors). Better Systems Lean still TODO - R7-RT open. |
nix build .#beastdb-lib |
Decommissioned ship path - export+runtime residual (full C ABI v9 + managed runtime). May still build for history/gates; do not expand. thr baseline: BENCHMARKS.md § Original baseline figures. Not an alias of .#libbeastdb. |
nix build .#beastdb |
Product AOT CLI / proofs - lean4-nix pin (host tools). |
Phase 5 did: promote freestanding packages.libbeastdb as the freestanding
library package story + dual-path docs honesty. Phase 5 did not: close R7-RT
(Embed TCB hard requirements below are not all met).
| # | Hard requirement | Status | Evidence / residual |
|---|---|---|---|
| 1 | In-process library with a real engine (not spawn-only) | Partial | Freestanding: append-log engine in store_env.c - put/get/delete/sync, live key index, optional dir -> DATA log layout (beastdb_env_* size_t API). Not multi-file product v9 (MANIFEST/shards/WAL/cursor/batch/MWMR). Export residual: real multi-file engine plus runtime. |
| 2 | No Lean managed runtime in the consumer | Met on freestanding path only | freestanding-gate / readelf -d: no libleanshared on beastdb-smoke. Full v9 consumers still load runtime via beastdb-lib. |
| 3 | No automatic memory management in the embed TCB | Partial | Freestanding extract aims unboxed/affine handles; C ABI is consumer-trust for close/UAF. Not full product lifecycle under language-enforced no-auto-MM. G18 remains encoded models only on host pin. |
| 4 | mmap / page-cache-class IO + tight deps | Partial | Freestanding: read-side mmap(MAP_SHARED, PROT_READ) of the append log for rebuild scan + value get; puts still write(2) + fsync. Not LMDB page-cache B+tree / write-through map durability class. Export path still snapshot / TreeMap materialize class. |
| 5 | Small static .a with the real engine |
Partial | Freestanding packages.libbeastdb libbeastdb.a = real freestanding engine spine (index/delete/mmap get/dir DATA) - not CLI-only; no libleanshared. Residual beastdb-lib static .a = CLI fork/exec only (no engine). Dual-backend full v9 path = residual shared .so + runtime. Static Lean export still has managed runtime -> does not close R7-RT (R7-STATIC honesty; PLAN-REMAINING.md Track C). |
| 6 | Linear/affine systems discipline (beyond G18 ghosts) | Not met | Substrate affine Fd/Arena conventions; C-ABI env/fd ownership is consumer-trust (documented in freestanding README A6). Not full type-system enforcement of product embed resources. |
Blocking close (honest residual list): full multi-file MANIFEST/shard product
depth on freestanding extract; LMDB-class page-cache write path; full beastdb.h v9
(or documented freestanding ABI parity + adapter); language-enforced affine product
resources beyond consumer-trust C ABI; optional bridge freestanding backend; measure
re-run when multi-file depth lands. Get-index thr and delete/mmap/dir steps landed
(2026-07-14 Track A).
Depth deferred (2026-07-14): further freestanding multi-file / write-path page-cache /
full freestanding ABI / affine close / conversion C5 is on hold until Systems Lean
is stable enough. Full four-part reopen criteria (SSOT):
PLAN-REMAINING.md § Recommended order. Parked spine + packages +
measure A/B kept. Deferral is not abandonment and does not invent R7-RT
closed. Primary near-term board next is human G1 publish; full C ABI consumers stay
on residual beastdb-lib.
Ship paths (honest dual track):
- Freestanding library (promoted package story; depth parked):
.#libbeastdb- spine; gate/thr/demo. - Full C ABI / Rust (temporary residual; active ship path):
.#beastdb-lib- export.so+libleanshared; static residual.a= CLI only. - Host CLI/proofs: lean4-nix
.#beastdb.
Default Lean 4 AOT on the product pin fails hard reqs 2-3 for full embed -> fix Lean (freestanding extract / backend). Not closed by R7-BYTES/SCAN/STATIC/SNAP or by Phase 5 packaging docs alone. Product pin stays lean4-nix for CLI/proofs until a deliberate freestanding pin promote is justified by Embed TCB evidence.
Legend: Done = shipped product capability. Done (experimental model only)
= closed gap in GAPS.md with models in tree, not a peer of
durable multi-file put/get/sync; production crypto/compression remains deferred.
GAPS closed for G9/G19 means those experimental models landed - not that
production encryption is claimed.
| Capability | Status |
|---|---|
Pure engine encode/decode (beastdb.Persist) |
Done - format v2 (Fowler-Noll-Vo / FNV-1a trailer) default write; v1 still loads; optional experimental v3 compress+FNV / v4/v5 keyed message authentication code (MAC) / beastdbE encrypt envelope (G9 - not core durable-KV path) |
Compression model (beastdb.Compress) |
Done (experimental model only) / production deferred - pure framing + RLE model; proved round-trip; not libzstd / not ratio-optimal; not a peer of put/get/sync |
Keyed MAC + encrypt model (beastdb.Crypto) |
Done (experimental model only) / production deferred - keyed FNV MAC (not NIST); stream-XOR cipher (not AES / authenticated encryption with associated data (AEAD) / post-quantum); encrypt-then-MAC (EtM); export/snapshot only |
| Product EtM export composition (G19) | Done (experimental model only) / production deferred - EtM + requireAuth (both non-empty auth+enc; empty fail closed); not NIST AEAD; multi-file unencrypted default; not production encryption at rest |
| Per-shard lock files (G22) | Done - shards/shard-<id>.lock on product put path; multi-process same-leaf fail / disjoint ok |
File save/load via Lean IO (beastdb.PersistIO) |
Done - lock + temp write + flush + optional fsync + rename + dir fsync |
Multi-file directory store (beastdb.StoreDir) |
Done - MANIFEST (directory control plane) + shards/shard-<id>-e<epoch>.dat + per-leaf wal/shard-<id>.log (+ legacy wal/wal.log) + LOCK |
Write-ahead log (WAL) puts + deletes + recovery (beastdb.Wal) |
Done - append-only put ('P') and delete ('D' tombstone) records; openDir replays legacy + per-leaf WALs onto checkpoint (G3.2 + G22 + P6-DEL) |
| Per-shard on-disk compact (G4.4) | Done - compactShard rewrites only that shard file + MANIFEST epoch |
| Multi-level compaction (G4.1-G4.3) | Done - Levels pure model; shard blob v2 multi-run; compactShardLevels |
| Split lifecycle & hybrid consistency (G5) | Done - Lifecycle.Managed epoch model; dual-read getPolicy; first-class API; durable LIFECYCLE side file + openManaged / putManaged |
| Product library + CLI (G8) | Done - beastdb.Api + Types.Bytes embedding; CLI subcommands; see API.md |
| Single-writer multi-reader (SWMR) concurrency (G6) | Done - exclusive writer LOCK (per-op + session lease); readers open without lock; pure Concurrency model; sequential multi-shard compact |
| Bench harness + LMDB baseline (G7) | Done - beastdb bench; Nix LMDB microbench; BENCHMARKS.md |
| Measure-and-real shallow (G21) | Done - host-probe, profile-cpu / profile-mem, side-by-side bench; soft-degrade tools; not long profiles in test-suite |
| Deep measure suite (G24 / Workstream L) | Done (local only) - deep-cpu / deep-mem / deep-rr / value-assess / asan-smoke (+ optional Phase B CLI asan); soft-degrade tools vs fail-closed product/sanitizer; artifacts under TMPDIR; not CI / not in test-suite; not product ASan clean; not LMDB parity; does not reopen G21 |
| Prior-art study (G11.1-G11.4) | Done - ref/lmdb + ref/leveldb + ref/breccia; PRIOR-ART.md (docs only - not a new runtime codec) |
| Ahead-of-time (AOT) product + fail-closed rules | Documented - SYSTEMS.md; missing features must not silent-succeed |
| L3 / L2 pure models (G15-G16) | Done (Horizon 2) - beastdb.Msg / ForkJoin |
| Product multi-shard compact schedule (Workstream F1) | Done - ForkJoin.leafSchedule + Api.compactBySchedule; durable IO sequential under SWMR on purpose (Track 2 + Next-2); no Task multi-core compact (F2 closed measured residual) |
| Pure multi-writer multi-reader (MWMR) disjoint leaves (G16) | Done (model) - beastdb.Mwmr; AOT horizon2 |
| Pure concurrent structural publish (Workstream J) | Done (pure model) - beastdb.Structural generation fence; AOT horizon2 |
| Product multi-process generation-fenced structural (Track 3) | Done (product slice) - lifecycle epoch id CAS + short cooperative LOCK required; AOT struct-smoke; Next-4 / R3: not lock-free dual publishers (north-star deferred pending P1-P6 in SYSTEMS.md §4) |
| L1 portable bulk kernels (G17) | Done (scalar) - beastdb.Bulk; AOT horizon3; Workstream I measured residual: no product single instruction multiple data (SIMD) |
| Linear/affine resource encodings (G18) | Done (model) - beastdb.Resource H4; AOT horizon4; not language linear types |
| Multi-process MWMR put via trie sharding (G22) | Done - per-leaf lock + per-leaf WAL; AOT mwmr-smoke; structural publish uses short global LOCK + generation fence (Track 3) |
Single-file store (G23; API still *Image*) |
Done (opt-in) - pure beastdb.Layout + product LayoutIO / Api.ImageHandle (init/open/put/get/sync) + explicit migrate both ways + layout-smoke / crash-suite single-file windows. Not photos/media. Honesty: library puts durable only on syncImage; no multi-process MWMR put on single-file path; multi-file remains the default |
| Resource bounds (G10) | Done - beastdb.Bounds fail-closed put/save/open; compact total-entries non-growth theorem |
| Snapshot -> multi-file migrate | Done - migrateSnapshot / migrateSnapshotStrict (G3.5 path) |
| Structural load fail-closed | Done - parse + validSnapshot? (WF+SC); checksum on v2 / MANIFEST / shards |
| Strict load (LRR) | Done - loadStoreStrict / openDirStrict (G3.3-G3.4) |
AOT binary via nix build .#beastdb |
Done - demo exercises Waves 1-8 + Horizon 2-5 under IO.FS.withTempDir; CLI for Wave 5+ / horizon2...horizon5 |
| Foreign C ABI + C/C++/Rust consumers (FFI) | Done (dual-backend / R7 deeper partial; R7-RT open) - nix build .#beastdb-lib installs libbeastdb.so + beastdb.h; demos beastdb-ffi-c / -cpp / -rust; gate checks.ffi-smoke. PR2 package default = export (same-process compiled @[export] full C ABI v9 in beastdb/FfiExport.lean plus Lean runtime libleanshared in the consumer process - not a second engine, not a no-runtime C embed). Force CLI: BEASTDB_USE_CLI=1 at open. Force export: BEASTDB_USE_EXPORT=1. Not OpenLDAP LMDB wire/page format; not full lmdb.h. UTF-8 put/get + length-prefixed binary + bulk multi-put + contains + product tombstone delete + ordered cursor + multi-key atomic batch + reverse/range/first-last/neighbor + D1 len/clear/delete_range (BEASTDB_API_VERSION 9; end -> BEASTDB_ERR_DONE). Delete / clear are not LMDB free-page reclaim (clear = tombstone-all live keys; delete_range = internal-key bounds). Atomic batch is product multi-key atomic batch (temp+rename), not LMDB page-level ACID. Cursor is product snapshot scan (internal-key order; freezes live unique index + internal pairs at open; external Bytes on scanNext - R7-SCAN; not LMDB B+tree). Export env = long-lived Api.Handle snapshot (R7-SNAP docs: idle gets do not auto-follow peer multi-process puts; reopen = close+open or successful sync / beastdb_sync refreshes handle from disk; CLI emergency reopens per call; not LMDB multi-version concurrency control (MVCC) / reader table; no beastdb_env_refresh in v9). Export open uses requireFsync := true (needs beastdb-fsync on PATH). R7-BYTES: export two-phase get densifies to ByteArray + bulk memcpy (ABI unchanged; M2b ~2x at 64 KiB; still ~linear / not mmap O(1)). R7 depth residual is deeper partial (not closed) - export is production package default; CLI emergency remains; static .a is CLI-only; D3/M2 + R7-BYTES + R7-SCAN measure evidence in BENCHMARKS.md; R7-SNAP docs honesty in API.md / CONSUME-RUST.md / beastdb.h / PLAN boards. Separate: heed-inspired Rust crate ffi/rust/beastdb/ is R17 closed (thin v0 + T0 8 / T1 26 / T2 8 + Phase 6 growth + D1 + D2 RoTxn/MIGRATE-HEED - not full heed; heed3 tests zero; gates beastdb-rust-smoke / t0 / t1 / t2). See GAPS.md, EXPORT-LINK.md, PLAN.md, HEED-MAP.md, TESTING.md |
| Lock-efficiency (needed exclusivity only) | Done (pure + product honesty) - pure Concurrency / Mwmr theorems; SYSTEMS.md lock resource budget; AOT greps lock efficiency: .... Short cooperative LOCK still required for structural publish - not lock-free dual MANIFEST publishers |
| Release binary | Done - nix build .#beastdb-release (requires strip success + fsync wrap; same -O3 objects; Nix closure still includes Lean runtime) |
| Buffer flush after write | Done - IO.FS.Handle.flush after putStr |
| File + parent dir fsync helper | Done - Nix-built beastdb-fsync (G2.1-G2.2); optional hard-fail |
| Cooperative single-writer lock | Done - whole-file *.beastdb-lock; multi-file dbDir/LOCK via O_CREAT|O_EXCL (G2.5); product Error.concurrent |
- Public surface: library
beastdb.Api+ CLI; external key bytes embed to internal keys via injectivebytesToKey(not a crypto hash; internal-key order is not always unsigned external-byte / memcmp order - see API.md and AGENTS.md § Terminology); UTF-8 CLI strings are a convenience embedding only. - Errors: typed sum, but thrown IO paths are classified by substring
matching via
classifyIO(order matters; Next-5 / R16 audited residual): lock / stale leasegenimage -> concurrent; resource bounds / closed handle / empty-secret refuse -> validation;corrupt/checksum/wrong-key crypto -> corrupt; else io - not a fully typed StoreDir error algebra. AOT demo greps lock the taxonomy. Closed-handle and G10 put gates often return typedError.validationdirectly (no substring map). - Locks (Wave 6 SWMR + G22 MWMR put + Track 3 structural fence): default product
puttakes the routed leafshards/shard-<id>.lockand appendswal/shard-<id>.log(no globalLOCK). Session lease viaApi.beginWrite/endWriteholds globalLOCK(excludes other puts). Structural ops (checkpoint / compact / split) take a short globalLOCKthen wait for relevant shard locks; split/reconcile also compare-and-swap the lifecycle epoch id (stale free-copy / race loser ->Error.concurrent). Tokens use a per-store monotonic counter (.beastdb-lease-seq) under exclusiveLOCK. Readers (openStore/get) take no exclusive lock except pendingwal/atomic-commitrecovery on open (brief globalLOCK). Stale free-copy handles after release or generation advance fail closed on mutate (concurrent). Returnedclosehandle hasclosed := true(mutate ->validation); free-copy pre-close handles are not disk-invalidated (Tier A / Next-5 / R6 honesty residual - treat handles as single-owner; not language linear types). Mutate refuse: all product mutate paths callhandleEnsureOpen/imageEnsureOpen(including multi-file structural begin/finish/split + put / beginWrite / endWrite / compact / sync / export; single-file put/sync/compact). AOT greps cover multi-file closed put / endWrite / compact / export / sync / beginWrite and single-file closed put / sync / compact - not structural closed-handle greps (code-gated only; same class as API/GAPS inventories).closealways releases a held lease (even when flush/sync fails). Flush-failure honesty: ifflush := trueand checkpoint fails, the API returns.erroronly - lease is released on disk, but no closed handle is returned; discard free-copies and reopen (do not expectclosed := trueon the caller's pre-close value). Same flush-failure class forcloseImage. - Init: refuses existing
MANIFESTunlessforce; does not claim exclusive ownership of an arbitrary directory tree. - Compact / splitAndReconcile: product API validates leaf ids and stable-only
atomic split; lower-level
StoreDir.compactShardstill allows raw id misuse if called directly.
Short packaging of the highest-risk operator mental-model mismatches. Details remain in durability / concurrency sections below and in PROOFS.md (pure!=product) / SYSTEMS.md (lock budget). Residual IDs: GAPS.md.
| Footgun | What actually happens | Safe operator rule |
|---|---|---|
| Free-copy pre-close handles (R6) | Lean values free-copy. Only the handle returned by close / closeImage has closed := true (mutate -> Error.validation). Free-copies taken before close keep closed = false and are not disk-invalidated. Flush-failure close: lease may be released on disk, but API returns .error only - no closed handle; discard free-copies and reopen. Stale lease/gen after peer advance -> Error.concurrent on mutate. |
Treat handles as single-owner. Prefer the returned close handle. After failed flush/close, reopen - do not keep using pre-close free-copies. Not language linear types. |
| Single-file put durability (R8) | Optional one-file DB layout (API still says *Image*; not photos). Library putImage is in-memory only until syncImage (or flush-on-close when dirty). CLI image-put always put+sync (durable). Multi-file put appends WAL (durable on append). No multi-process MWMR on single-file path. |
Prefer multi-file for real multi-process use. For single-file durability: syncImage or CLI image-put - do not assume library put alone survives crash. |
| Mid-schedule compact handle lag (P-B) | Pure ForkJoin schedule is a total fold (any order agrees on get). Product multi-shard compact is sequential under global LOCK: each leaf compactShard may rewrite disk. If a later leaf fails mid-schedule, earlier leaves may already be durable-compacted while the caller's pure handle can lag the on-disk base until a successful refresh / reopen / sync path that reloads. |
After compact error, do not trust the pre-call handle as disk truth - reopen or sync/reload before further mutate. Greppable full multi-leaf compact success still leaves residual free-copy of the old handle if you kept a free-copy. |
| WAL soft fsync (P-B) | Product put: per-leaf lock -> append/flush WAL -> update memory. Optional beastdb-fsync after flush is best-effort unless requireFsync. A failed optional fsync does not roll back the in-memory put (avoids desync with recovery if the record is on disk). Crash after flush but before fsync: record may still be durable; recovery applies complete WAL prefix. |
Treat successful put as memory-consistent with recovery if the WAL record is present. For hard durability barriers, run with fsync helper + requireFsync where the path supports it - still not a proved power-fail model (R10 not claimed). |
| Pure concurrency theorems != product locks | Pure SWMR put exclusivity / Structural CAS / multiGet_parallel_eq are not multi-process lock-free or Task guarantees. Product: G22 leaf locks; structural short LOCK + epoch; sequential compact. |
Read PROOFS.md § pure model vs product concurrency before claiming lock-free or multi-core product behavior. |
- Available:
Handle.flush+ optionalbeastdb-fsynchelper (Nix-built POSIXfsyncon file and parent directory after rename). Helper absence degrades to flush-only unlessrequireFsync := true(then save throws). - Publish protocol (G2.4):
- Acquire cooperative lock
path.beastdb-lockwithwriteNew/O_EXCL(G2.5) - Write sibling
*.beastdb-tmp+ flush beastdb-fsynctemp (G2.1) if helper onPATH(hard-fail ifrequireFsync)IO.FS.renametemp -> targetbeastdb-fsync --dirparent (G2.2) if helper onPATH(hard-fail ifrequireFsync)- Release lock (delete lock file in
finally)
- Acquire cooperative lock
- Checksum (G2.3): format v2 appends FNV-1a 32-bit trailer over the
raw body prefix (full
Char.toNatscalars, no low-byte truncation). Load verifies the trailer against that same on-stream prefix (not a re-encode of the parsed store). Pure round-tripdecode_encode_storeplus reject lemmasdecodeStore_bad_checksum_reject/decodeStore_trailing_junk_reject. Detects wrong trailer, truncation after the body, and many in-place corruptions of the body image (including Unicode scalar flips that share a low 8-bit). Not a MAC/authenticator; non-canonical digit padding that keeps a matching raw trailer still loads to the same logical store. - Wave 8 compression / MAC / encryption (G9 - experimental models, not production crypto):
- v3: single length-prefixed
Compress.compressof tree+shards payload + FNV over raw body prefix (same raw-trailer discipline as v2). This is framing, not RLE;rleEncodeis demo-only and never written by Persist. - v4/v5: keyed
Crypto.macFnv1a32trailer (key ‖ body ‖ key). Integrity under key secrecy only - not NIST MAC strength, not HMAC-SHA. - Encrypt envelope (
beastdbE): stream-XOR over codepoint Nats with keystream from key+nonce+index FNV; not AES, not AEAD, not PQ. - G9 + G19: multi-file MANIFEST/shards/WAL remain unencrypted by default;
whole-file crypto is opt-in export/import only. G19 is experimental EtM
composition +
requireAuth(both non-empty auth+enc keys required; empty fail closed; not NIST AEAD). Historical greppable token: validation / demo strings may still sayproduct AEADforclassifyIO/ AOT stability - meaning remains experimental EtM export, not standards AEAD / not core put. Ciphertext uses decimalencodeNatof each XOR'd codepoint - large expansion vs plaintext;maxEncodedBytesis checked post-encode and may refuse stores that fit unencrypted. Nonce discipline: reusing the same(encKey, encNonce)across distinct plaintexts enables keystream reuse (XOR of ciphertexts leaks XOR of plaintexts). Nonce is stored in the envelope; default libraryencNonce := 0is a footgun if left unchanged. - When both
encKeyandauthKeyare set: encrypt-then-MAC on the outer envelope (inner snapshot uses FNV only). Enc-only (no authKey) uses outer unkeyed FNV over ciphertext - integrity is not authentication; prefer MAC for authenticity. - Default product write remains v2 (opt-in via
PersistOpts/Api.CryptoConfig/exportSnapshot). Multi-file MANIFEST/shards/WAL are not auto-encrypted. - Wrong MAC / wrong enc key / missing key for v4/v5/envelope -> fail closed
(
none/Error.corrupt). Unencrypted legacy still loads without keys. - Keys are always caller-supplied - no hardcoded product secrets.
- Pure
PersistOpts:some []keys are treated as absent (empty ≡ disable). PersistIO refusessome []if a layer was requested with an empty list.
- v3: single length-prefixed
- Strict load (G3.3-G3.4):
loadStoreStrictrequireslogsRespectRouting?. Bool gate is linked toEngine.LogsRespectRoutingbyof_logsRespectRouting?_true/logsRespectRouting?_true_of(latter needs unique shard keys). Mis-routed leaf entries fail closed (no silent emptyget?). - v1 migration (G3.5): snapshots without a trailer still decode; current
writers emit v2 only (
encodeStore/saveStore*). - Wave 2 multi-file + WAL (G3.1, G3.2, G4.4):
- Directory layout is the product path for incremental storage; whole-file snapshots remain for compatibility and migration source.
- Puts (
StoreDir.put, G22): per-leaf lock + append/flush towal/shard-<id>.log, then update memory (one-way: append ⇒ recovery may include the put). Optional WAL fsync is best-effort after flush; a failed fsync does not roll back the in-memory put (avoids desync with recovery). - Checkpoint / sync (G22 + Workstream E): under global + shard locks, choose
publish base carefully - normal
sync(lifecycle := none) with matching trees usesopenDirdisk truth (not a stale pure handle); structural lifecycle publish keeps the caller transform and absorbs keys present only on disk, then merges remaining WAL. The publish base is then compacted (eBase.compact) before shard rewrite so residual is unique-key and the returned handle iskeysUnique-tagged. Rewrite shards + MANIFEST (temp+rename+optional fsync), then truncate all known WALs via temp+rename empty header.Api.syncrefreshesmanaged.storeto that published compacted engine. - Recovery: load MANIFEST + shard blobs (checksummed; missing blob ids fail
closed in pure
assemble), thenapplyWalover legacy + per-leaf WALs. Missing WAL -> empty; corrupt WAL header -> open fails. Truncated last record dropped (complete prefix only). Wire decode materializesofEntries(flag not on wire); Tier B:ofEntriesre-detects uniqueness from residual keys so a unique-shaped residual (e.g. after compact-on-publish) cold-opens on the TreeMap unique-index path (Next-1). Multi-put residuals with duplicate keys stay onlatestRev. WAL replay usesput(R1: fresh key on unique residual keeps TreeMap; overwrite clears unique until compact/sync/ re-materialize). - Compaction on disk (Workstream E):
compactShard/compactShardLevelsbump one epoch, rewrite oneshard-*-e*.dat+ MANIFEST, then truncate that leaf's WAL so reopen does not re-apply superseded puts onto the compacted residual (get? preserved; log stays compacted). Other shard epochs untouched. Cold open re-detectskeysUniquefrom residual (Tier B); the flag is still not a wire field. - Epoch GC: superseded
shard-*-e<old>.datbest-effort deleted after successful publish; MANIFEST remains authority. Residual orphans possible if delete fails. - Multi-level (Wave 3): pure
Levels+ shard v2 encode L0 + runs; load flattens toKV.Storefor the engine (lookup-preserving). DefaultsaveDirstill writes v1 flat blobs;compactShardLevelsemits v2. - Not a page/WAL log with group commit or torn-write bitmaps. WAL has no whole-file checksum (append-friendly).
| Window | Effect |
|---|---|
| WAL append after flush, fsync fails / crash | Record may be durable; put keeps memory in sync; get? OK on recovery if record present |
| Checkpoint after new MANIFEST, before WAL truncate | Reopen may re-apply WAL puts (get? equal for put-only latest-value; logs re-inflate) |
compactShard then reopen |
Leaf WAL truncated with compact (Workstream E); residual stays compacted; cold open re-detects unique residual (Tier B) |
Checkpoint / sync complete |
Publish base is compacted before write; returned handle has keysUnique; WAL truncated; cold reopen re-detects unique |
| Post-rename dir fsync fail (MANIFEST/shards/empty WAL) | Target may already be visible; error says so |
| Corrupt WAL with good MANIFEST+shards | openDir -> none (fail closed; not treated as empty) |
| Window | Effect |
|---|---|
After beginSplitDir (shards+MANIFEST+LIFECYCLE+WAL truncate) |
openManaged restores splitWindow epoch; product getPolicy dual-reads orphan. Plain openDir/get? still sees empty children (leaf-only) - callers must use Managed / getPolicy during the window |
MANIFEST published, LIFECYCLE not yet rewritten (same lock, multi-file non-atomic) |
Open can pair new tree with old epoch. openManaged fail-closed: stable + hybrid (¬SC) -> none; window + ¬agreesWithTree -> none. Retry / repair after full publish |
Mid-window pure Managed.put (no WAL) |
Not durable - lost on crash. Use StoreDir.putManaged (WAL) for crash-safe mid-window writes |
Mid-window after putManaged, before finish |
WAL put + prior split checkpoint; openManaged recovers epoch from LIFECYCLE and put via WAL replay |
Wave-2 checkpoint dbDir e prev mid-window |
Default preserves on-disk LIFECYCLE (lifecycle := none); does not clobber to stable 0. Pass some ep only when intentionally changing epoch |
Corrupt / bad-checksum LIFECYCLE |
loadLifecycle -> none; checkpoint with preserve throws (refuses clobber). Missing file -> legacy stable 0 |
Mismatched LIFECYCLE vs tree (hand-edit / stale) |
openManaged -> none (epochOkForOpen / agreesWithTree) |
After finishReconcileDir |
Stable LIFECYCLE; orphan empty under SC; plain get? and policy agree |
- Remaining open (see
docs/GAPS.mdresidual list SSOT): human publish G1; scale residuals (large-N partial win Next-1 + R1 put-maintain; Plan Step 3: distinct-key multi-put get closed measured win - no further redesign; overwrite accepted residual / compact discipline ~O(N²) until compact; F3 deferred); free-copy pre-close handle residual (Tier A / Next-5 / R6 - returnedcloseonly; mutate refuse grepped); single-file put durability / no single-file MWMR / full codec theorem partial (Next-5 / R8 / G23 - CLIimage-putdurable; libraryputImagein-memory; migrate partial dest residual); foreign C ABI depth deeper partial (P6-EXPORT PR2 dual-backend: package default export same-process compiled@[export]; CLI emergencyBEASTDB_USE_CLI=1; full C ABI v9 (binary put/get + multi-put + contains + product tombstone delete + ordered cursor + reverse/range- multi-key atomic batch + D1 len/clear/delete_range) +
ffi-smokeshipped; D3/M2 + R7-BYTES (export get densify + bulk memcpy; still ~linear large-value) + R7-SCAN (lazy external pairs; open still freezes live index) + static.aCLI-only; notlmdb.h/ LMDB wire / free-page reclaim / LMDB page ACID - R7 deeper partial, not closed); typed StoreDir error algebra residual (Next-5 / R16 -classifyIOsubstring map audited + taxonomy greps; not fully typed algebra); Tier C dual-publisher / kernel-lease / linearizability honesty. Assurance residuals (Tier D / Next-6 settled - not marketed): crash-suite is cooperative simulated only (G13 + Workstream G + Track 4 closed in tree; orphan production temps ignored on open; corrupt control plane fail closed - do not conflate); not hardware power-fail (D2 / R10 - not claimed; soft reopen only with lab instrumentation + honesty; never marketing without product); not CIkill -9mid-put / mid-sync (D1 / R9 - not claimed / cooperative-only; soft reopen only with hermetic stable CI story + fixtures; never a flaky kill-9 gate without design; optional human-only offline recipe in TESTING.md - never a flake check). G9/G19 crypto remains experimental models - not NIST AES-GCM product crypto (D3 / R11 - deferred product decision; soft reopen only after explicit product decision - real algorithms + key management + fail-closed defaults); multi-file
unencrypted by default. Compression ratio / libzstd deferred (D4 / R12;
soft reopen only if storage size is real operator pain + stack-legal boundary).
G22-G23 closed in tree with honesty (MWMR put multi-file; optional single-file
store + migrate). G17 scalar + Workstream I / R13 closed measured residual
(no product SIMD; soft reopen only if Bulk is measured hotspot + legal path
without forbidden product C).
Lock-efficiency pure + SYSTEMS budget shipped (not open work). Prior-art
G11.1-G11.4 closed - see PRIOR-ART.md. Dual-read /
snapshot isolation is not linearizability (C3 deferred). Lock-free dual
MANIFEST publishers not shipped (Next-4 / R3 settled) - short cooperative
exclusive
LOCKstill required; dual-publisher is a north star deferred (not abandoned) pending preconditions P1-P6 + soft reopen in SYSTEMS.md §4.
- multi-key atomic batch + D1 len/clear/delete_range) +
- Single-file store durability (G23): one DB file (
beastdbI; API*Image*names are historical). LibraryputImageis in-memory only vs multi-file WAL put. OnlysyncImage(or flush-on-close when dirty) publishes via temp+rename. CLIimage-putalways syncs. Stale free-copy sync when disk gen ahead ->Error.concurrent. Corrupt/torn file ->Error.corrupt. Multi-fileputremains the durable multi-process path. No single-file append log. - Single-file -> multi-file migrate residual:
migrateImageToDirmulti-stepsaveDir; mid-write can leave a partial multi-file destination (source file intact). - Concurrent readers (Wave 6): may open without
LOCKand see a pure snapshot of MANIFEST+shards+WAL (+LIFECYCLE). Temp+rename publish avoids torn single-file images; WAL append is in-place (truncated last record dropped). Not a kernel shared-lock reader count.
| Concern | beastdb today | Typical LMDB / RocksDB class |
|---|---|---|
| Persistence unit | Whole-file snapshot, MANIFEST+shards+WAL, or single-file beastdbI store |
Pages / WAL / mmap regions |
| Random access | Reload whole snapshot/single-file into pure store | mmap / block cache |
| Concurrent multi-writer | G22: disjoint leaf puts multi-process; same leaf / structural global LOCK fail closed; cooperative only |
Single-writer (LMDB) or controlled multi-writer |
| mmap | Split path: freestanding store_env.c uses read-side mmap(MAP_SHARED, PROT_READ) of the append log for rebuild + value get only (puts still write(2)+fsync; not LMDB page-cache B+tree). Host product AOT / multi-file export (beastdb-lib) still no product mmap. R7-RT #4 remains Partial. |
Core of LMDB |
| Throughput | Microbench only (see BENCHMARKS.md); not multi-GB | Engineered for high ops/s |
| Space amplification | Snapshots encode full logs; multi-file leaves old epoch files until best-effort GC | Compaction / freelist / copy-on-write pages |
| Resource caps | maxEntries 1e6 / maxShards 4096 / maxEncodedBytes 256 MiB fail-closed |
Often configurable map size / freelist |
Full architecture comparison (LMDB B+tree, LevelDB LSM, Breccia blob store,
lessons adopted / not adopted, explicit non-claims): PRIOR-ART.md.
Study trees: ref/lmdb, ref/leveldb, ref/breccia (never product source).
Performance vs LMDB: small-N microbenches are in BENCHMARKS.md.
No multi-GB parity is claimed. Per-key get on a unique residual is
TreeMap search (~log in residual size - not O(1)). R1 put-maintain:
put of a fresh key on a unique residual keeps keysUnique + TreeMap insert.
Overwrite (or any residual that is not unique-tagged) uses latestRev
(linear in the routed shard log). Get-all of N keys: ~O(N log N) for
distinct-key multi-put / unique-tagged residuals; ~O(N²) on overwrite /
non-unique residuals until compact.
| Path | Product get algorithm | Notes |
|---|---|---|
| Multi-file after put of fresh key on unique residual | uniqueIndex.get? (TreeMap) |
R1 put-maintain keeps keysUnique + insert |
| Multi-file after overwrite put (or non-unique residual) | latestRev (reverse + early-exit) |
Overwrite clears keysUnique and drops index |
Multi-file after compact (same handle, pre-sync) |
uniqueIndex.get? (TreeMap) |
compactShard / ofUnique builds index; leaf WAL truncated |
Multi-file after sync / checkpoint |
TreeMap unique index | Publish compacts base before write; returned handle tagged unique |
Multi-file after cold reopen (openDir) |
TreeMap when residual keys are Nodup; else latestRev |
Tier B + Next-1: ofEntries re-detects uniqueness and builds index (flag not on wire) |
| Single-file store after put of fresh key (dirty) | TreeMap when residual unique (R1) | Same put-maintain as multi-file engine |
| Single-file after overwrite put (dirty) | latestRev on mutated shards |
Overwrite clears unique until sync/compact |
Single-file after syncImage / compactImage |
TreeMap unique index (engineAfterOfStore compact) |
Keeps unique tag without re-toStore |
Single-file after openImage |
run-on-empty-shard installs compacted unique logs + index | applyFrame |
Not claimed: O(1) get, mmap B+tree, LMDB parity. Shipped (Next-1 + R1 put-maintain; Plan Step 3 closed measured win for distinct-key multi-put get): proved TreeMap unique residual get + fresh-key put keeps the index - measured multi-file get-all post-compact (and distinct-key get_pre) wall_ms drops from ~0.5-7 s @ N=2k historical reverse path to tens of ms / single-digit ms on one host (ephemeral; see BENCHMARKS.md). No further product redesign for that path without new measured pain. Accepted residual / compact discipline: overwrite multi-put get-all still ~O(N²) until compact; index build cost at compact/open; no O(1)/mmap. LMDB mmap B+trees can still be faster on the same synthetic shape (and LMDB microbench uses one batched write txn vs N WAL appends). Priority remains correctness boundary + round-trip proofs, not QPS.
| Gate | What is checked | What is not proved |
|---|---|---|
maxEntries |
Sum of shard log lengths before put/save/open / multi-key atomic batch | Bound on unique keys after compact; D1 note: clear / delete_range stage one tomb per matched live key via applyAtomicBatch, so they need headroom totalEntries + liveMatched <= maxEntries (historical tombs still count toward totalEntries - a store can accept single puts yet refuse clear/range-delete until compact) |
maxShards |
e.shards.length before split/save/open |
Tree height / key bit length |
maxEncodedBytes |
Pre-stat (metadata.byteSize) before readBinFile on whole-file, MANIFEST, per-shard, and WAL paths. Multi-file open also tracks a running aggregate of on-disk component sizes and aborts early. Encode-length proxy still checked after recover on checkpoint/saveDir/openDir. |
Closed-form worst-case encode size; TOCTOU if file grows between stat and read; peak RSS can still include already-loaded smaller components before an aggregate throw |
Defaults are conservative for the pure-list engine. Operators must not assume multi-GB capacity.
Product open error classes (G10):
| Failure | Surface |
|---|---|
Per-component or aggregate oversize; post-recover resourceOk? / encode proxy |
Throws resource bound -> product Error.validation |
| Missing/corrupt codecs (bad decode, LRR, epoch/tree) | none -> product Error.corrupt |
Whole-file loadStore / loadStoreStrict oversize (pre-stat) |
Option none (not a product Error; library callers must map) |
| Attr | Optimization | Strip | Notes |
|---|---|---|---|
packages.beastdb (default) |
lean4-nix -O3 -DNDEBUG (debug = false) |
no | Dev/CI default |
packages.beastdb-release |
same objects | yes (strip) |
Smaller on-disk binary; still wraps beastdb-fsync |
Optional LTO (-flto via leancFlags / linkFlags) is not enabled by
default - Lean runtime + shared libs make LTO environment-specific; experiment
locally if needed, do not claim default LTO.
- Engine state is an immutable pure value; "mutation" is constructing a new
Engine.Store. - The demo is single-threaded
IO(cooperative interleaving, not OS threads). - Product contract:
- Default put writers (G22): exclusive per-leaf
shards/shard-<id>.lock+ append towal/shard-<id>.log. Disjoint leaves may put multi-process. Same leaf ->Error.concurrent. Puts also fail closed while globalLOCKis held (session/structural exclusive). - Session / structural writers: exclusive
dbDir/LOCKviaO_CREAT|O_EXCLforbeginWrite, checkpoint/sync, compact, split/reconcile (or multi-op session lease). Checkpoint reloads durable state under locks and refreshes the caller's published engine. Structural ops (Track 3) reload durable managed under lock vialoadStructuralBase(WAL-replayed disk base) and re-merge write-ahead log records on publish; same-tree finish/sync-style paths also absorb keys present only on disk. Tree-changing split does not absorb across mismatched routing trees (disk base + WAL merge instead). - Readers:
openDir/openStore/gettake no exclusive lock except pending P6-ACIDwal/atomic-commitrecovery on open (brief globalLOCK, same class asapplyAtomicRecords; concurrent puts fail closed while recovery re-appends + clears). Open materializes a pure snapshot. - Cooperative trust model (Tier C / C2): locks exclude only processes that
honor the beastdb protocol (
O_EXCLcreate ofLOCK/ per-leafshard-*.lock). Foreign processes, operators who delete lock files, or out-of-band writers are not excluded by the kernel. Kernel multi-writer leases remain deferred (no portable OS lease product path + tests in this tree). - Shard lock wait (structural): checkpoint/compact busy-wait up to ~2s
(
acquireShardLockWait, 2000 x 1 ms) then fail closed if a put still holds the leaf lock. - G10 multi-process:
putWouldExceed?is per-handle; two processes may each pass local bounds and together exceed caps until open/checkpoint fails closed (not a global multi-process quota).
- Default put writers (G22): exclusive per-leaf
- Pure model (G6.3):
beastdb.Concurrencysequential lock automaton; well-formed ⇒ one exclusive session; nestedbeginWriteand bareendWriteare product-aligned no-ops; reader-during-write allowed. Concurrent second writer is IOO_EXCL. Snapshot story restates engine immutability (reader_snapshot_vs_writer_put≡get_put_other) - not an interleaving refinement. Not linearizability of concurrent IO (C3 deferred - snapshot isolation honesty only; not the next fitness milestone). - Shard compact (G6.4 / G16 / Workstream F1): product multi-shard compact
uses the pure L2 leaf schedule (
ForkJoin.leafSchedule/Api.compactScheduleIds) and folds durablecompactShardviaApi.compactBySchedule. Pureget_compactSchedule_any/get_compactLeaves_revshow any order (including reverse) agrees on lookup. IO honesty: each leaf is still compacted sequentially under global SWMRLOCK+ per-leaf shard lock; MANIFEST epoch publish is single-threaded. No LeanTask/ multi-process parallel compact in the extracted binary (F2 closed measured residual: sequential on purpose after Track 2 + Next-2 1-vs-N measure - do not claim multi-core compact speedup). Non-leaf schedule ids ->Error.validation(fail closed). - Horizon 2 pure MWMR + G22 product put:
beastdb.Mwmrmodels per-shard leases; product multi-process put uses per-leaf locks + per-leaf WALs (AOTmwmr-smoke). GlobalLOCKremains for session/structural sections only. - Writer lock (G2.5 + G6):
withWriterLock/withLockexclusive-create then always release infinallyfor per-op sections. Session lease can leave a staleLOCKon crash until removed. requireFsync: defaultfalse(best-effort; silent degrade if helper missing). Whentrue: pre-rename file-fsync failure removes temp and leaves the target unchanged; post-rename parent-dir fsync failure throws even though the snapshot may already be visible atpath(directory durability unknown). Bare paths withparent = nonefsync".".- No shared-memory multi-writer. Proving OS-level data-race freedom for concurrent IO remains outside the pure model.
- Format is a versioned char stream (magic
beastdb, version nat +;), not a page format. See header comment inbeastdb/Persist.lean.- v1: body only (legacy load path)
- v2 (current write): body + FNV-1a 32 checksum trailer
- Values are length-prefixed character payloads from
String.toList(no compression, no encryption). UTF-8 multi-byte values are supported on the file path viaputStr/readBinFile+String.fromUTF8?. - Load returns
none(uniform Option channel) for:- invalid UTF-8 file bytes
- bad magic / version / parse errors / trailing junk
- bad v2 checksum trailer
- duplicate leaf ids (
wellFormed?) - non-unique shard keys or missing leaf coverage (
keysNodup?/coversLeaves?) - strict only:
logsRespectRouting? = false(mis-routed leaf entries)
- Load throws for ordinary OS failures such as missing path (not folded
into
none). - Structural acceptance (
decodeStoreValidated/loadStore) means parse + WF+SC only (proved:decodeStoreValidated_sound). It does not require LRR. - Strict acceptance (
decodeStoreStrict/loadStoreStrict) adds LRR (proved:decodeStoreStrict_sound⇒ WF ∧ SC ∧ LRR Bool ∧LogsRespectRouting). saveStorewill encode ill-formed stores;saveStoreValidated/saveStoreStrictrefuse them. "Saved with rawsaveStore" does not imply "reloadable."
Trusted computing base for the binary still includes:
- Lean 4 compiler + C backend
- host C toolchain (via Nix stdenv)
- OS filesystem and process runtime (including rename atomicity assumptions)
- Nix-generated
beastdb-fsynchelper (tiny C, not hand-maintained product source) - Nix evaluation for reproducibility of the build, not of runtime disk
Machine-checked properties cover the pure codec and engine; IO is an unverified monadic boundary that calls into those pure functions.
Closed in Wave 7: bench harness + LMDB microbench (G7); resource bounds (G10); release strip package. See BENCHMARKS.md.
Closed in Wave 8 (experimental models only - not core durable-KV peers): pure
compress + keyed MAC + encrypt-at-rest models (G9); opt-in formats v3-v5 /
beastdbE; checksum remains distinct from MAC. Production crypto/compression
deferred (multi-file unencrypted by default).
Still open (aligned with GAPS.md residual open list after Tier A-D + lock-efficiency ship + foreign C ABI partial - GAPS remains SSOT):
- Human publish / forge hygiene (G1.1-G1.3, G1.5, G1.6) - see RELEASE.md. Do not mark G1 closed while any of those rows remain open.
- Large-N get partial win (Next-1 + R1 put-maintain; Plan Step 3 settled):
unique residual TreeMap; distinct-key multi-put get - closed measured win
(tree get ~O(N log N); no further redesign that path); overwrite multi-put -
accepted residual / compact discipline (~O(N²) until compact; Workstream E +
Tier B + Track 2 / R1 measure; not asymptotic O(1); no mmap B+tree claim); L3
worker pool deferred (F3). F2 closed measured
residual: sequential multi-shard compact on purpose after Track 2 +
Next-2 1-vs-N (~1.0 ratio; no free multi-core win) - see BENCHMARKS recipe;
no greppable Task multi-core path; soft reopen only after measured fail-closed
win. Workstream J / Track 3 generation-fenced multi-process structural
closed (product slice + pure model; short cooperative
LOCKhonesty residual- not lock-free dual publishers). Workstream I closed as measured residual: product keeps scalar L1 Bulk (host may show vector flags; no product SIMD claim - SYSTEMS.md §5). Kernel leases / linearizability unclaimed (Tier C). Lock-efficiency pure theorems + SYSTEMS budget are shipped (not open work).
- Free-copy pre-close handles (A1 / Next-5 / R6): returned
close/closeImagehandle refuses mutate (AOT greps); free-copy pre-close values are not disk-invalidated (not language linear types). Single-file store partial (Next-5 / R8 / G23): libraryputImagein-memory untilsyncImage; CLIimage-putforces put+sync; no single-file MWMR; migrate partial dest residual; fulldecode_encode_imagetheorem deferred. Typed StoreDir error algebra (Next-5 / R16):classifyIOsubstring map audited residual (taxonomy greps; not fully typed algebra). - Foreign C ABI depth (deeper partial / R7):
beastdb-lib+ C/C++/Rust demos +checks.ffi-smokedual-backend. Length-prefixed binary put/get, bulk multi-put, contains, product tombstone delete, ordered cursor, multi-key atomic batch, and D1 len/clear/delete_range shipped (API v9; delete missing key idempotent; cursor end ->BEASTDB_ERR_DONE; atomic batch = product temp+rename, not LMDB page-level ACID; not LMDB free-page reclaim; clear = tombstone-all; range delete = internal-key bounds). Mode B flush policy (BatchFlushPolicy) auto-flushes without sync when thresholds hit (each chunk product-atomic; not rolled back by later abort). P6-EXPORT PR2 + P6-CURSOR + P6-ACID + P6-RANGE + D1 landed: full C ABI v9@[export]inbeastdb/FfiExport.leanlinked intolibbeastdb.so(EXPORT-LINK.md); package default = export; CLI emergencyBEASTDB_USE_CLI=1at open; M1 measured. Residual: not fulllmdb.h; long-lived snapshot visibility; R7-BYTES densified export get (ByteArray+ bulk memcpy; M2b ~2x at 64 KiB; still ~linear / not mmap O(1); remaining densify-from-engine-Valuecost); static.aCLI-only; cursor is not streaming B+tree (R7-SCAN lazy external pairs; open still freezes live index and dominates iterate - M2c). R17 closed separately. D3 measure + R7-BYTES + R7-SCAN landed (R7 still deeper partial). Do not invent R7 closed. - Tier D assurance residuals (Next-6 settled - not product features to ship next; soft reopen only as listed): kill-mid-write under CI (D1 / R9 - not claimed / closed residual as cooperative-only; soft reopen only with hermetic stable CI story + fixtures; never a flaky kill-9 gate without design); hardware power-fail (D2 / R10 - not claimed; soft reopen only with lab instrumentation + honesty; never marketing without product); NIST AES-GCM / standards product crypto (D3 / R11 - deferred product decision - G9/G19 models; multi-file unencrypted default; soft reopen only after explicit product decision + real algorithms + key management + fail-closed defaults); compression ratio / libzstd (D4 / R12 - deferred; soft reopen only if storage size is real operator pain and a stack-legal boundary exists). R13 product SIMD is a closed measured residual (scalar Bulk; soft reopen only if Bulk is a measured hotspot + legal path without forbidden product C). F3 / R18 L3 worker pool remains deferred (soft reopen only after architecture decision; no distributed-DB claim).
- Full residual board: GAPS.md. Systems honesty: SYSTEMS.md.
Closed in Horizon 1: G13 simulated crash suite + multi-process SWMR smoke
(beastdb crash-suite / swmr-smoke; flake checks.crash-suite /
checks.swmr-smoke). Not hardware power-fail coverage. G14 get-path
(latestRev ≡ latest), beastdb.Cost; Workstream E + Tier B + Next-1
prefer TreeMap uniqueIndex when keysUnique (after compact / single-file sync /
cold-open re-detect on unique residual). latestUnique remains a proved list
helper / cost bridge - not the product unique hot path.
Closed in Horizon 2: G15 pure L3 beastdb.Msg; G16 L2 ForkJoin + pure
Mwmr (AOT horizon2 / checks.horizon2). H2.4 Resource affine start.
Closed in Workstream F1: product multi-shard compact schedule matches pure
ForkJoin.leafSchedule (Api.compactBySchedule); AOT product schedule of the
same pre-state ≡ pure gets. F2 closed (measured residual): no greppable Task
multi-core compact path; product compact is sequential on purpose (Track 2 +
Next-2 / R2 taskset 1-vs-N probe: ratio ~1.0 on sequential binary; end-to-end
fold + disk + LOCK/MANIFEST dominate). Soft reopen only after a fail-closed path
shows a measured win. F3 deferred: L3 multi-process worker pool.
Closed in Horizon 3 + Workstream I: G17 portable scalar L1 beastdb.Bulk
(AOT horizon3 / checks.horizon3); product Api.fingerprintBytes / keysEqual.
Workstream I measured residual: keep scalar; probe may report vector flags;
product does not select a vector path and does not claim "uses AVX2."
Single-file store path closed as G23 (LAYOUT.md).
Closed in Horizon 4: G18 pure linear/affine encodings in beastdb.Resource
(exclusive write ghost world, affine snapshots, unique buffers; AOT horizon4 /
checks.horizon4). Not language linear types; product leaseToken still
free-copy + re-verify.
Closed in Horizon 5 (experimental export path - not core durable-KV): G19
product EtM composition (requireAuth; AOT horizon5 / checks.horizon5) -
algorithms remain G9 models, not NIST AEAD; multi-file unencrypted by default;
production crypto deferred. G20 systems corpus + proof↔measure SOP in
SYSTEMS.md. H5.2 per-shard lock multi-process smoke.
Closed in Workstream C / G22: multi-process multi-writer multi-reader product
put on disjoint leaves (beastdb mwmr-smoke / checks.mwmr-smoke); per-leaf WAL
- shard lock; structural/session sections still global
LOCK.
Closed in Workstream D / G23: single-file store pure codec + product
open/put/sync + explicit multi-file↔single-file migrate (layout-smoke, crash-suite
single-file windows). Multi-file remains the default. Single-file library puts
durable only on sync.
Closed in Workstream J + Track 3: pure beastdb.Structural generation-fenced
concurrent structural publish + unique publisher session (AOT horizon2); product
multi-process generation-fenced structural publish (lifecycle epoch id CAS + short
cooperative LOCK; AOT struct-smoke). Honesty residual (Next-4 / R3): not
lock-free dual MANIFEST publishers (LOCK required; dual-publisher north-star
deferred pending SYSTEMS §4 P1-P6); not kernel leases; not linearizability.
Closed: Wave 9 prior art (G11.1-G11.3) + G11.4 Breccia pin; see PRIOR-ART.md.
| Claim | Status |
|---|---|
| AOT exercises documented multi-file windows (trunc WAL, bad header, missing shard, stale LIFECYCLE, orphan temp) + single-file corrupt/torn fail closed | Yes - crash-suite |
| Per-leaf WAL multi-put longest complete-prefix recover; corrupt per-leaf WAL header fail closed | Yes - crash-suite (Workstream G) |
| Foreign put + compact/sync keeps sibling leaf data | Yes - crash-suite (cooperative + child process put) |
Single-file mid-body / torn last frame region + trailing junk -> Error.corrupt |
Yes - crash-suite |
Real migrateImageToDir leaves source single-file store intact; residual-state partial dest (corrupt MANIFEST + orphan shard) -> openDir none |
Yes - crash-suite (product migrate path + residual-state sim; not mid-saveDir IO interrupt) |
Orphan production temps ignored: single-file .beastdb-tmp, multi-file LIFECYCLE.tmp, per-leaf WAL *.log.tmp |
Yes - crash-suite (Track 4; production naming) |
Corrupt LIFECYCLE body -> openManaged none (fail closed; not invent stable 0) |
Yes - crash-suite (Track 4) |
Compact-on-publish sync after multi-put same key truncates per-leaf WAL to empty header; cold reopen latest get preserved |
Yes - crash-suite (Track 4) |
| Mid-checkpoint residual: complete WAL records still present after published residual -> reopen get equal (idempotent put re-apply) | Yes - crash-suite (Track 4; cooperative sim of LIMITS Wave 2 window) |
| Orphan future shard epoch blob (MANIFEST still names prior epoch) ignored | Yes - crash-suite (Track 4 mid-publish residual) |
| Multi-process second writer -> concurrent; reader get without exclusive lock | Yes - swmr-smoke |
| Full power-fail / disk pull / kernel crash injection | No - not claimed (Tier D2 / R10; Next-6 settled). Lab-only if ever instrumented; do not market power-fail safety. Out of default product / CI scope. Soft reopen only with lab instrumentation + honesty; never marketing without product. |
Subprocess kill -9 mid-put / mid-sync then recover |
No - not claimed / closed residual as cooperative-only (Track 4 + Tier D1 / R9; Next-6 settled). Racey under hermetic Nix continuous integration; Lean Child.kill exists but is not a flake check / not CI-stable. Prefer cooperative file-window simulation (temp + rename, torn/corrupt fixtures matching production names). Optional human-only offline recipe in TESTING.md (never claim CI coverage). Soft reopen only with hermetic stable CI story + fixtures; never a flaky kill-9 gate without design. |
| Single-fsync multi-file atomicity | No - multi-step publish remains |
| Standards-grade / NIST product crypto on multi-file path | No - Tier D3 / R11 deferred product decision (Next-6 settled). G9/G19 are experimental models (keyed FNV MAC + stream-XOR + EtM composition), not NIST AES-GCM / AEAD / PQ. Multi-file MANIFEST/shards/WAL remain unencrypted by default. Soft reopen only after explicit product decision + real algorithms + key management + fail-closed defaults. |
| Compression ratio optimality / libzstd wire | No - Tier D4 / R12 deferred (Next-6 settled). Pure framing + demo RLE model only; not libzstd; ratio optimality not claimed. Soft reopen only if storage size is real operator pain and a stack-legal boundary exists. |
beastdb delivers a verified pure engine + Lean IO persistence with whole-file
snapshots and a multi-file directory layout (MANIFEST + per-shard files +
per-leaf WAL), machine-checked codecs/recovery get-semantics, structural and
strict LRR validation, SWMR session/structural exclusive locking plus
MWMR product put on disjoint leaves (G22: per-leaf lock + per-leaf WAL),
optional fsync-class barriers via a Nix helper, and a product library/CLI
surface (beastdb.Api + byte-key embedding).
It includes microbenches and fail-closed resource bounds (Wave 7). The shipped
product is the Lean AOT binary (SYSTEMS.md). Default durable
path for new multi-process stores is the multi-file directory layout
(init / put / get / sync); single-file store is opt-in (G23; API still
*Image*; library puts durable only on syncImage / CLI image-put). The shipped multi-file AOT / export product does not provide LMDB-class
mmap page cache. Freestanding libbeastdb has a read-side log map only
(Embed TCB #4 Partial - not page-cache parity). Neither path provides
lock-free dual MANIFEST publishers without cooperative
LOCK (Next-4: north-star deferred, not abandoned), kernel leases against foreign
processes, linearizability, multi-GB LMDB parity, NIST-grade on-disk crypto,
libzstd / ratio-optimal compression, CI-proven kill -9 mid-write recovery, or
hardware power-fail safety.
Pure beastdb.Structural (Workstream J) and product Track 3 generation-fenced
structural publish fail closed on race / stale free-copy; short cooperative LOCK
still serializes the publish critical section (required today). Missing capabilities must fail closed or use a
documented soft degrade - never silent success. See GAPS.md
(G13-G24 closed in tree with honesty; G24 deep measure / Workstream L local-only -
not CI / not product ASan clean / not LMDB parity; do not reopen G21; Tier A-D fitness residuals; G17 scalar +
Workstream I measured residual; Workstream J / Track 3 short-LOCK honesty;
lock-efficiency pure + budget shipped; foreign C ABI dual-backend deeper partial
(export package default + CLI emergency; R7 not closed) - not LMDB wire / not
full lmdb.h; heed-inspired Rust crate R17 closed thin v0 + selective
T0/T1/T2 - not full heed / heed3 tests zero; Phase 6 advanced (partial) -
P6-ACID + P6-RANGE + D1 + D2 + D3 measure + R7-BYTES + R7-SCAN done (Tier 0 multi-key
atomic batch + reverse/range/first-last + len/clear/delete_range + RoTxn/T2 +
M2 embed measure + export get densify/bulk memcpy + lazy scan external pairs; R7 still deeper partial);
R7 stays deeper partial (not closed);
remaining bindings-plan open = G1 human + optional P6-WAL / optional further
R7 product depth (SCAN/STATIC/SNAP; not default next) - see
PLAN.md / PLAN-REMAINING.md / GAPS.md).