Skip to content

VISION.md

Latest commit

 

History

History
249 lines (190 loc) · 34.6 KB

VISION.md

File metadata and controls

249 lines (190 loc) · 34.6 KB
Raw

beastdb - architecture & roadmap

Production-oriented, high-assurance embedded key-value store. Implementation and proofs: Lean 4 only. Build, packaging, and repo tooling: Nix flakes only.

Date: July 12, 2026 Vision Owner: Hunter Beast Core principle: Reliability and correctness first. Everything that can be expressed in Lean 4 will be. All orchestration, building, proving, extraction, and packaging happens through Nix flakes. Product engine Lean-only - no Rust product engine, no handwritten product C, no Bash/Python product scripts, no impure Lake-driven releases. Foreign language bindings under ffi/<lang>/ are an AGENTS exception (not product engine).

Open work is tracked as gap IDs in docs/GAPS.md. Waves W0-W9, Horizon 1-5 (G13-G20), measure tooling G21, multi-process multi-writer multi-reader put on disjoint leaves G22, single-file layout G23, and deep measure suite G24 / Workstream L are closed in tree with honesty notes (G24: Slices 1-6 - deep-cpu / deep-mem / deep-rr / value-assess / asan-smoke + optional Phase B CLI; not continuous-integration / not in test-suite; soft-degrade tools vs fail-closed product/sanitizer; not product ASan clean; not LMDB parity; do not reopen G21). Workstream E + Tier B + Next-1 / R1 put-maintain ship unique-residual get via a sorted Std.TreeMap index (uniqueIndex; ~O(N log N) get-all measured) - not O(1) / not mmap B+tree; Plan Step 3: distinct-key multi-put get is a closed measured win (keeps TreeMap; no further redesign that path); overwrite multi-put remains accepted residual / compact discipline (~O(N²) get-all until compact). Workstream F1 wires product multi-shard compact to the pure L2 leaf schedule; durable IO is sequential on purpose after Track 2 + Next-2 1-vs-N measure (no free multi-core win on the current path; F2 closed measured residual - no greppable Task multi-core compact; soft reopen only after fail-closed path + measured win). Workstream I closed as measured residual: product keeps portable scalar L1 Bulk (host may show vector flags; no product single instruction multiple data / SIMD claim). Workstream J + Track 3 closed: pure beastdb.Structural generation-fenced concurrent structural publish and product multi-process generation-fenced structural with short cooperative LOCK (AOT struct-smoke). Tier C + Next-4 / R3 residual honesty: lock-free dual MANIFEST publishers not shipped (exclusive critical section required today; dual-publisher north-star deferred not abandoned - soft reopen only after all P1-P6 in SYSTEMS.md §4); kernel multi-writer leases deferred (cooperative trust only); linearizability deferred (snapshot isolation). Tier D residual honesty (Next-6 / R9-R13 settled - assurance + polish only; no product land): cooperative crash-suite only - not CI kill -9 mid-write (D1 / R9 not claimed / cooperative-only; soft reopen only with hermetic stable CI story + fixtures; never a flaky kill-9 gate; optional human offline recipe in TESTING.md); hardware power-fail not claimed (D2 / R10 - soft reopen only with lab instrumentation + honesty; never marketing without product); NIST AES-GCM / standards-grade encryption at rest deferred product decision (D3 / R11 - soft reopen only after explicit product decision + real algorithms + key management + fail-closed defaults; multi-file unencrypted default); compression ratio / libzstd deferred (D4 / R12 - soft reopen only if storage size is real operator pain + stack-legal boundary); multi-file is the default new-store multi-process path with clear multi-file put vs single-file library putImage / CLI image-put durability (D5). R13 / I product SIMD is a closed measured residual (not open work; soft reopen only if Bulk is measured hotspot + legal path without forbidden product C). F3 / R18 L3 worker pool stays deferred (pure Msg only; soft reopen only after architecture decision for multi-process workers; no distributed-DB claim). Forward scale residual is overwrite multi-put large-N get (~O(N²) until compact) + optional denser on-disk/mmap index if measured need appears - not re-open F2 as default work (F2 closed sequential-on-purpose). Lock-efficiency pure theorems + SYSTEMS lock resource budget are shipped (needed exclusivity only - not lock-free dual publishers). Foreign C ABI is deeper partial dual-backend (beastdb-lib / ffi-smoke - export package default + CLI emergency BEASTDB_USE_CLI=1 full v9 same-process compiled @[export] (cursor + multi-key atomic batch + reverse/range/first-last/neighbor + len/clear/delete_range); not lmdb.h / LMDB wire / LMDB page ACID; R7 deeper partial, not closed). Human G1 publish residual remains. Docs status flags are kept aligned by standing Workstream K / R14-R15 residual hygiene (not a product gap). This document is the architecture and roadmap single source of truth (SSOT); GAPS is the closure inventory. Prior art: PRIOR-ART.md / ref/. Systems honesty: SYSTEMS.md.

1. Executive summary

beastdb is a production-grade embedded key-value (KV) store whose critical algorithms and invariants are machine-checked in Lean 4 and shipped as a reproducible ahead-of-time (AOT) binary (Lean C backend via Nix). Formal methods are the engineering strategy - not a research side project bolted onto an unverified core.

Product (what ships): the extracted native binary from nix build. Logic is proved and tested in Lean first; generated C is compiler output, never hand-edited. See SYSTEMS.md §1.

Non-negotiable constraints:

  • 100% of product implementation logic, data structures, algorithms, and proofs in Lean 4.
  • Properties we ship claims for are proved in Lean or explicitly scoped out in LIMITS.md / GAPS.md.
  • AOT compilation via Lean's C backend - the C image is the runtime product, still owned by the Lean source + proofs.
  • Missing features fail closed (or documented soft degrade only) - never silent wrong answers (SYSTEMS.md §2).
  • Build and tooling: sole entrypoint flake.nix. CI invokes Nix only.
  • No mathlib unless a real dependency appears; proofs stay in core Lean 4.

Product shape: a better-proven working alternative in the LMDB problem class - embedded local KV - using dynamic prefix-trie sharding, append-only logs, and compaction. Not a drop-in LMDB/RocksDB clone. Comparisons: PRIOR-ART.md.

Freestanding libbeastdb goal (standing directive - R7-RT open; Option E locked): systems-class in-process libbeastdb in Lean without managed runtime / automatic memory management in the consumer; linear/affine systems discipline; small static .a with a real engine. This is a primary long-term product architecture goal, not optional polish. Hard reqs + evidence table: LIMITS.md Embed TCB. Compiler design (fork seed): LEAN4.md. Agent rules: AGENTS.md freestanding directive. Plan: .agents/plans/plan-systems-embed-gap.md. Measure suite (G24, YCSB-C, LMDB compare, value-assess, freestanding thr) exists to quantify managed-runtime residual vs freestanding progress - not as a substitute for closing R7-RT.

Phase 5 packaging/docs promote (2026-07-14): freestanding product library package = packages.libbeastdb (nix build .#libbeastdb). Temporary full C ABI v9 residual = beastdb-lib. R7-RT still open (spine != multi-file product; Embed TCB hard reqs not all met). Phase 5 docs promote does not close R7-RT.

Goal (E) Landed / ship (honest)
Freestanding library package Default embed library packages.libbeastdb Systems Lean best-effort spine (no libleanshared); original thr exact fields vs export residual enshrined (BENCHMARKS.md § Original baseline figures - compare future Systems Lean to those prints); depth + polished Systems Lean still TODO (R7-RT open; G1 primary near-term)
Full C ABI v9 / Rust Same freestanding path Temporary residual beastdb-lib + libleanshared
Memory Explicit lifetimes Freestanding partial; export residual managed RC
Static .a Real multi-file engine Freestanding spine engine; residual export .a = CLI only
IO mmap / page-cache-class Append-log Fd spine / export TreeMap class - not mmap parity

Default AOT on the product pin fails full Embed TCB -> fix Lean. R7 product polish (BYTES / SCAN / STATIC / SNAP) and Phase 5 packaging docs do not close R7-RT. Host pin stays lean4-nix for CLI/proofs.

Concurrency target:

  • Today (shipped): cooperative single-writer multi-reader (SWMR) for session/beginWrite and the short structural publish critical section (global LOCK); multi-writer multi-reader (MWMR) product put on disjoint leaf shards (G22: per-leaf lock + per-leaf write-ahead log); generation-fenced multi-process structural (Track 3 / Workstream J product slice: lifecycle epoch id CAS + AOT struct-smoke); same-shard conflicts and structural race losers fail closed; readers remain snapshot-isolated.
  • North star residual (Tier C + Next-4 / R3 honesty): lock-free dual MANIFEST publishers (no cooperative exclusive - not shipped; short LOCK required today; dual-publisher deferred not abandoned - soft reopen only after all P1-P6 in SYSTEMS.md §4); kernel leases deferred (C2 cooperative trust); linearizability deferred (C3). Pure models: beastdb.Mwmr / ForkJoin / Msg (Horizon 2) plus pure beastdb.Structural (generation fence; product path shipped as Track 3 with short LOCK honesty). Optional single-file store shipped (G23; API still *Image*); multi-process MWMR put remains multi-file only.

Target fitness: C1 (one client process saturating the machine - cores, memory hierarchy, optional data-parallel kernels) first; expand machine classes later. Not a C10K/C10M network service plan.

Parallelism (Three Layer Cake): L1 data-parallel kernels * L2 fork-join * L3 message-passing workers - with typed contracts and fail closed when a layer is unavailable (SYSTEMS.md).

2. Core architecture (Lean 4)

2.1 Dynamic prefix sharding with auto-bifurcation

  • Verified prefix routing (binary trie) partitioning the key space.
  • Proved invariants: every key maps to a leaf shard; splits preserve coverage and disjointness; routing is total.
  • Bifurcation installs fresh child leaf ids; engine guards empty child slots so unreconciled orphans are not silently dropped.
  • New data appends to the routed shard log without global rebalancing of unrelated shards.

2.2 Append-only logs + Breccia-inspired compaction

  • Mutations are immutable appends to per-shard logs.
  • Compaction: latest-value fold (compactList) plus multi-level runs (Levels: L0 + newest-first unique runs, mergeRuns newer-wins).
  • Obligations: preserve latest visible value per key; weak non-growth size bound (length_mergeRuns_le / length_compactList_le); unique keys after compact; merge order confluent on latest maps (latest_mergeRuns_assoc).
  • On-disk multi-level shard blobs (v2) flatten on load for the engine.

2.3 Hybrid consistency with reconciliation

  • Strong structural consistency when there are no non-empty non-leaf logs (StronglyConsistent / NoNonEmptyOrphans).
  • During split, data may remain under an orphan id until reconcile (compact orphan + putIfAbsent merge: visible wins).
  • LogsRespectRouting (LRR): leaf entries must match the routing tree; strict load enforces LRR on durable snapshots.
  • Epoch / first-class split lifecycle API (Lifecycle.Managed, dual-read policy, durable LIFECYCLE + openManaged/putManaged): closed Wave 4 (G5).

2.4 Compression & encryption (experimental / deferred - not core durable-KV)

  • Not a peer of put/get/sync. Production crypto and compression are deferred; multi-file stays unencrypted by default.
  • Pure Lean beastdb.Compress (experimental): wire uses length-prefix framing (compress / proved decompress_compress); RLE (rleEncode) is demo-only off-wire; optional dict envelope stores dict bytes without substitution coding; not libzstd; ratio optimality deferred.
  • Optional snapshot formats: v3 framed-compress+FNV, v4/v5 keyed MAC, outer beastdbE encrypt envelope with encrypt-then-MAC (EtM) when both keys set.
  • Encryption model is pure stream-XOR over whole-file export/import only - not production encryption at rest on the multi-file path.
  • G19 (Horizon 5): experimental product EtM composition + requireAuth fail-closed API; algorithms remain G9 models - not NIST AES-GCM / authenticated encryption with associated data (AEAD) / post-quantum. Fail closed on wrong/missing keys remains intact.
  • Honesty: MAC is keyed integrity under key secrecy only; cipher is not AES/AEAD/PQ; reuse of (encKey, nonce) risks keystream reuse.

2.5 Effects, I/O, concurrency & memory safety

  • Pure core for encode/decode and engine transitions; Lean IO only at the persistence boundary (PersistIO).
  • Memory safety via dependent types and Lean's runtime - no manual product-side allocators.
  • Concurrency today: multi-reader pure snapshots; MWMR product put on disjoint leaves (G22 - per-leaf lock + per-leaf WAL; AOT mwmr-smoke); generation-fenced multi-process structural (Track 3 - lifecycle epoch id CAS + short cooperative LOCK; AOT struct-smoke); session exclusive global LOCK (Wave 6). Cooperative among honoring processes (not kernel multi-writer leases).
  • Concurrency residual (Tier C + Next-4 / R3): lock-free dual MANIFEST publishers without cooperative LOCK (not shipped - exclusive section required today; dual-publisher north-star deferred pending SYSTEMS §4 P1-P6; not abandoned); kernel leases deferred (C2); linearizability deferred (C3). Same-leaf second writer or structural race loser / stale free-copy -> Error.concurrent (fail closed).
  • Durability: format v2 FNV-1a trailer (default write); optional v3 compress, v4/v5 MAC, encrypt envelope (Wave 8 - experimental models). Temp + rename publish; optional Nix-built beastdb-fsync. Checksum != MAC. See LIMITS.md.
  • Linear/affine encodings (handles, buffers, leases): G18 closed (Horizon 4) - encoded in API/world/proofs, not "Rust ownership for free" / not language linear types.

2.6 Three Layer Cake of Parallelism (forward)

  • L3 message passing (G15 closed pure): typed mailboxes (beastdb.Msg); fail closed when disabled; no multi-process worker pool yet.
  • L2 fork-join (G16 + F1): pure compactSchedule / leafSchedule / multi-get; join ≡ sequential gets; product Api.compactBySchedule uses the same leaf schedule with sequential durable IO under SWMR on purpose after Track 2 + Next-2 measure (no Task multi-core compact - F2 closed measured residual).
  • L1 data parallel: portable scalar bulk kernels landed (beastdb.Bulk, G17); Workstream I measured residual keeps scalar - no product SIMD / no assumed ISA (SYSTEMS.md §5).
  • Proof ↔ measure: cost-model theorems (more/less efficient) + AOT benches; mismatches are insight (G14/G20).

3. Technology stack

Layer Technology Notes
Product logic & proofs Lean 4 All algorithms and machine-checked invariants (product engine Lean-only)
Verification Core Lean 4 (no mathlib by default) Sharding, compaction, reconcile, codec soundness
Build & packaging Nix flakes Hermetic toolchain, proofs-as-build, AOT binary
Dev environment nix develop Lean, git, gnupg; no global toolchain requirement
AOT Lean C backend + Nix stdenv Generated C never hand-edited
Foreign language bindings (not product engine) ffi/<lang>/ (AGENTS exception) First-party crates/demos over the C ABI; Lean remains store single source of truth (SSOT). Start: heed-inspired Rust crate ffi/rust/beastdb/ (R17 closed - selective suite, not product engine Rust)
CI GitHub Actions -> nix flake check Namecheck, no-sorry, product, demo, crash/swmr/mwmr/struct/layout smokes, ffi-smoke (foreign C ABI thin bridge - not in test-suite), beastdb-rust-smoke / beastdb-rust-t0 / beastdb-rust-t1 / beastdb-rust-t2 (Rust bindings gates - not in test-suite; see TESTING.md), horizons, host-probe, hook packages
Forbidden as product engine / repo-tooling source Rust, Bash/Python in-tree, Make, handwritten C as product or Nix-policy source Exception: foreign bindings under ffi/<lang>/ (not Lean product engine). ref/ submodules exempt (study only). See AGENTS.md.

Why this stack for production assurance:

  • Dependent types encode sharding and merge invariants that type systems without proofs cannot state.
  • Nix gives reproducible artifacts and a single gate (nix flake check) for humans and CI.
  • Limits are documented honestly so operators know what is proved vs. operational remaining risk.

4. Verification strategy

The Lean code is specification + implementation + proof for the pure core.

Key properties (incremental, many already landed):

  • Routing partitions the key space; splits preserve well-formedness and coverage.
  • Append-only logs; latest-value get/put equations.
  • Compaction preserves latest values; weak size bound; key uniqueness after compact.
  • Reconciliation restores structural strong consistency without clobbering visible keys.
  • Snapshot codec round-trips; validated/strict decode soundness for WF+SC (+ LRR when strict).
  • Extracted binary is exercised by checks.demo; end-to-end IO is not fully proved (TCB: Lean extractor + C compiler + kernel).

Proof inventory and refresh commands: docs/PROOFS.md. No-sorry policy: flake checks.no-sorry (G12.1).

5. Production readiness & measurement

Phases 0-3 + Waves 0-9 + Horizon 1-5 (G13-G20) + G21-G24 + Workstream F1 + Workstream I (scalar L1 residual) + Workstream J / Track 3 (generation-fenced structural) + lock-efficiency slice + foreign C ABI thin bridge delivered a verified pure engine + durable multi-file store (default) + optional single-file store + product API + SWMR sessions + multi-process MWMR put on disjoint leaves + generation-fenced multi-process structural + pure L2/L3 models + product multi-shard compact schedule wiring + portable L1 bulk kernels + encoded resource discipline + systems methodology + benches + prior-art study + needed-exclusivity lock budget + LMDB-class C/C++/Rust dual-backend ABI (deeper partial; export default). Experimental EtM export composition (G9/G19) exists in tree but is deferred for real use - not a peer of put/get/sync. F2 closed measured residual - sequential multi-shard compact on purpose (Next-2; not open work). Residual open work is human G1, scale paths (large-N get / F3 deferred), lock-free dual MANIFEST publishers (Next-4 / R3 settled: short cooperative LOCK required today; dual-publisher north-star deferred pending SYSTEMS §4 P1-P6 - not abandoned; not shipped), foreign C ABI depth (R7 deeper partial - export package default; CLI emergency; not closed), free-copy pre-close honesty residual (Next-5 / R6 audited greps; not linear types), single-file put durability partial (Next-5 / R8), classifyIO substring algebra residual (Next-5 / R16 audited), and Tier D assurance residuals (kill-mid-write under CI / hardware power-fail / NIST product crypto / libzstd compression - not claimed or deferred; not marketed) - not implied "done." Full residual inventory: GAPS.md residual open list (free-copy pre-close, kernel leases, linearizability, Tier D R9-R12, F3/R18, etc.). R13 product SIMD, F2 sequential compact, and G24 deep measure are closed measured residuals - shipped-closed slices, not open work. G21 shallow measure stays closed (do not reopen). Also SYSTEMS.md.

Strengths already in tree:

  • Machine-checked routing, compaction, and reconcile core (sharding enables MWMR put).
  • Fail-closed load on structure (+ strict LRR path); missing optional features fail closed or documented soft degrade.
  • Whole-file snapshots, multi-file MANIFEST/shards/per-leaf WAL, and optional single-file beastdbI store with explicit migrate.
  • SWMR session exclusive + G22 multi-process MWMR put on disjoint leaves + Track 3 generation-fenced multi-process structural (not linearizability; short cooperative LOCK remains - not lock-free dual publishers).
  • L3 pure message protocol + L2 fork-join schedule equivalence theorems.
  • Reproducible Nix AOT binary, bench harness, and CI entrypoint.
  • Resource bounds fail-closed (beastdb.Bounds) with compact non-growth theorem on total entries.
  • Prior-art trees ref/lmdb, ref/leveldb, ref/breccia and PRIOR-ART.md.
  • G23 single-file store (beastdb.Layout + LayoutIO / ImageHandle + layout-smoke; not photos).

Closed with honesty (not open - see GAPS / LIMITS):

  • Horizon 1-5 (G13-G20) in tree: H1 simulated crash; H2 pure MWMR/L2/L3; H3 scalar L1 bulk + Workstream I measured residual (no product SIMD); H4 encoded linear/affine resources (not language linear types); H5 experimental EtM export composition + systems methodology (crypto deferred for production).
  • Workstream G crash depth: expanded crash-suite (per-leaf WAL prefix / corrupt header, foreign put + compact, single-file mid-body/trailing junk, mid-migrate residual). Cooperative simulation only - not hardware power-fail; not kill -9 mid-put under hermetic Nix (LIMITS.md).
  • Track 4 + Tier D + Next-6 deeper crash assurance + residual honesty: production-named orphan temps (single-file .beastdb-tmp, LIFECYCLE.tmp, per-leaf WAL .tmp - ignored on open), corrupt LIFECYCLE (fail closed - do not conflate), compact-on-publish empty WAL, mid-checkpoint WAL re-apply get-equal, orphan future shard epoch. Decision (Next-6 settled): no CI kill -9 mid-write (D1 / R9 not claimed / cooperative-only; soft reopen only with hermetic stable CI + fixtures; human offline recipe only); no hardware power-fail claim (D2 / R10; soft reopen only with lab instrumentation + honesty); no NIST crypto product land (D3 / R11 deferred product decision - G9/G19 models; soft reopen only after product decision + real algorithms + key management + fail-closed defaults); no libzstd / ratio product land (D4 / R12 deferred).
  • G22 multi-process MWMR product put on disjoint leaves (AOT mwmr-smoke).
  • G23 single-file store product path + migrate (AOT layout-smoke; library puts durable on sync only).
  • Workstream J / Track 3 generation-fenced multi-process structural (AOT struct-smoke; short cooperative LOCK required - Next-4 / R3: dual-publisher north-star deferred, not lock-free dual publishers shipped).
  • Lock-efficiency slice - pure Concurrency / Mwmr theorems; SYSTEMS lock resource budget; AOT lock efficiency: ... greps (needed exclusivity only; not lock-free dual publishers).
  • Foreign C ABI dual-backend (P6-EXPORT PR2 + P6-CURSOR + P6-ACID + P6-RANGE + D1) - beastdb-lib + C/C++/Rust demos + checks.ffi-smoke (UTF-8 + length-prefixed binary put/get + multi/contains/delete + ordered cursor + multi-key atomic batch + reverse/range/first-last/neighbor + len/clear/delete_range API v9; package default = export; CLI emergency BEASTDB_USE_CLI=1; multi-key atomic batch not LMDB page-level ACID; not lmdb.h / LMDB wire / free-page reclaim - R7 is deeper partial, not closed).
  • Bindings residual R17 closed (Phases 3-5) - heed-inspired Rust crate ffi/rust/beastdb/ + selective T0 8 / T1 26 / T2 8 flake suite (checks.beastdb-rust-smoke / beastdb-rust-t0 / beastdb-rust-t1 / beastdb-rust-t2; not full heed suite; heed3 tests zero / encryption contrast only; thin v0 + D1 + D2 - not "most of heed"). Soft reopen / measure + embed need applies to remaining Phase 6 growth (optional WAL) and optional further R7 product depth (STATIC / optional SNAP B2 refresh). Phase 6 advanced / partial - bulk multi-put + contains + product delete + Mode B flush policy + P6-EXPORT PR2 export default + P6-CURSOR + P6-ACID multi-key atomic batch + P6-RANGE reverse/range/first-last + D1 len/clear/delete_range + D2 (RoTxn / read_txn + selective T2 + MIGRATE-HEED.md) + D3 measure (M2) + R7-BYTES (export get densify + bulk memcpy; still ~linear / not mmap O(1)) + R7-SCAN (lazy external pairs) + R7-SNAP docs (EXPORT idle gets do not auto-follow peers; reopen or successful sync refreshes; not LMDB MVCC) shipped. Tier 0 master decision locked 2026-07-13: priority track = heed / heed3 non-encrypted drop-in migration; P6-ACID done; P6-RANGE done; D1 done; D2 done; D3 measure done; R7-BYTES done; R7-SCAN done; R7-SNAP docs done; P6-WAL optional / deprioritized. Open rows actionable in PLAN-REMAINING.md - default next G1 human; R7 deeper partial. Closing R17 / PR2 / P6-CURSOR / P6-ACID / P6-RANGE / D1 / D2 / D3 measure / R7-BYTES / R7-SCAN / R7-SNAP docs does not close R7 (deeper partial only; remaining densify-from-engine-Value + live-index freeze + static .a CLI-only + idle long-lived handle still does not auto-follow without reopen/sync). Map + gates + board: GAPS.md R17, PLAN.md, PLAN-COMPLETED.md, PLAN-REMAINING.md, HEED-MAP.md, TESTING.md rust gates.
  • G19 is experimental EtM composition over G9 models - not NIST AEAD; multi-file unencrypted by default; production crypto deferred.

Closed measured residuals (not open work): F2 sequential multi-shard compact on purpose after Track 2 + Next-2 / R2 1-vs-N (no free multi-core win; no greppable Task multi-core path; soft reopen only after fail-closed path + measured win). Workstream I / R13 (optional SIMD) closed as measured residual - scalar Bulk retained (soft reopen only if Bulk is measured hotspot + legal path without forbidden product C). R17 heed-inspired crate + selective T0/T1/T2 suite closed (not open work; not full heed / not heed3 encryption). G24 / Workstream L deep measure suite closed (deep-cpu / deep-mem / deep-rr / value-assess / asan-smoke; not CI; not product ASan clean; not LMDB parity; do not reopen G21).

Open production work (see GAPS residual list - fitness A-D cross-links):

  • Human publish / forge (G1.1-G1.3, G1.5, G1.6).
  • 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 for that path (keeps TreeMap; ~O(N log N); Step 2 grid; no further product redesign - not O(1)/mmap); overwrite multi-put - accepted residual / compact discipline (~O(N²) until compact); Tier B cold-open uniqueness re-detect shipped. L3 worker pool (F3 / R18 deferred - pure Msg only; soft reopen only after architecture decision; no distributed-DB claim). Lock-free dual MANIFEST publishers residual (Next-4 settled: short cooperative LOCK still required; dual-publisher north-star deferred pending SYSTEMS §4 P1-P6; kernel leases / linearizability deferred). Foreign C ABI depth (R7) is deeper partial (not closed) (P6-EXPORT PR2 + P6-CURSOR + P6-ACID + P6-RANGE + D1 + D2 + D3/M2 measure + R7-BYTES + R7-SCAN + R7-SNAP docs: package default export same-process compiled @[export] full v9; CLI emergency BEASTDB_USE_CLI=1; multi-key atomic batch + reverse/range + len/clear/delete_range shipped but not LMDB page ACID; not lmdb.h / free-page reclaim; long-lived EXPORT idle gets do not auto-follow peers - reopen or successful sync refreshes (docs honesty; not LMDB MVCC); R7-BYTES bulk export get (~2x at 64 KiB; still ~linear / not mmap O(1); remaining densify-from-engine-Value); scan open still freezes live index (R7-SCAN; M2); static .a CLI-only). R17 (heed-inspired crate + selective suite) is closed separately - see closed-with-honesty above; not re-listed as open work.
  • Tier D assurance residuals (Next-6 settled - not marketed; not product work to ship next): kill-mid-write under CI (R9 not claimed / cooperative-only); hardware power-fail safety (R10 not claimed); NIST AES-GCM product crypto (R11 deferred product decision); libzstd / ratio-optimal compression (R12 deferred). Soft reopen criteria in GAPS.md. R13 SIMD is closed measured residual - not open work.

Success for a production core line (e.g. v0.1.0-core): signed history, green nix flake check on CI, documented limits, no sorry, demo green - with Horizons 1-5 + G22 MWMR put + G23 layout + Track 3 generation-fenced structural + lock-efficiency slice + foreign C ABI dual-backend already in tree. Residual after publish: human G1 steps (close only when each action is done), LMDB-class C1 scale honesty (multi-put large-N get residual; F2 is closed sequential-on-purpose measured residual - not open work; R13 SIMD closed measured residual - not open work), lock-free dual MANIFEST publishers (Next-4: short LOCK required; dual-publisher north-star deferred - not claimed shipped), foreign C ABI depth (R7 deeper partial - export package default; CLI emergency; not closed), and standing Tier D honesty residuals in GAPS.md (R9-R12 - not marketed; soft reopen only per Next-6 criteria; do not close on publish alone).

6. Phased roadmap

Phase 0: Bootstrap - complete

  • Flake pins Lean 4; nix develop / nix build; namecheck; GPG hooks; append-only log proofs.

Phase 1: Verified sharding & append-only core - complete

  • Routing tree, KV get/put, multi-shard engine, structural split, ShardsCover.

Phase 2: Compaction, reconciliation & hybrid consistency - core complete

  • Latest-value compact; reconcile with visible-wins merge; LRR preservation; hybrid SC model.
  • Dictionary/RLE model closed in Wave 8 (G9.1); multi-level compact closed in Wave 3.

Phase 3: Persistence & extraction - core complete

  • Pure codec + Lean IO snapshots; temp+rename publish; structural validation on load.
  • Wave 1 upgrades: v2 checksum, strict LRR load, fsync helper, cooperative lock.
  • Wave 2 upgrades: multi-file MANIFEST + per-shard blobs + WAL recovery (G3.1, G3.2, G4.4).
  • Deferred: mmap.

Wave 0: Land-the-core hygiene - agent docs/CI done; human publish open

  • CI workflow, proof stats, release checklist, production framing in this document.
  • Human: signed commit, tag, push, require-signed-commits (see RELEASE.md).

Waves 1-9: Gap closure

  • W1 disk trust - closed in tree (G2, G3.3-G3.5, G12.1/G12.3).
  • W2 incremental storage - closed in tree (G3.1, G3.2, G4.4).
  • W3 multi-level compaction - closed in tree (G4.1-G4.3).
  • W4 split lifecycle & hybrid consistency - closed in tree (G5.1-G5.4).
  • W5 product API & types - closed in tree (G8.1-G8.5); see API.md.
  • W6 concurrency SWMR - closed in tree (G6.1-G6.4); pure MWMR model is G16, product multi-process put is G22 (neither is W6).
  • W7 measure & optimize + resource bounds - closed in tree (G7.1-G7.5, G10.1-G10.2); see BENCHMARKS.md.
  • W8 compression & encryption - closed in tree (G9.1-G9.4; experimental models).
  • W9 prior art - closed (G11.1-G11.3); G11.4 Breccia pin closed separately.

7. Risks & mitigations

Risk Likelihood Impact Mitigation
Proof burden slows features Medium High Small modules; no-sorry gate; prove invariants that operators rely on
Extracted binary slower than C engines Medium Medium Profile under Nix; optimize Lean first; measure before FFI expansion
I/O / durability gaps Medium High Explicit LIMITS + GAPS; Waves 1-2 closed checksum/strict/fsync + multi-file/WAL; crash integration tests remain
Scope creep High High Wave + gap IDs; no silent "research stretch" as shipped claims
Supply-chain / history trust Medium High Mandatory GPG on every pushed commit; pre-push + verify-signatures; forge require-signed-commits

8. Immediate next steps

Done in tree (not next work): Horizon 1-5 (G13-G20) with honesty notes as above.

  1. Human publish residual - docs/RELEASE.md: verify signed land tip (core product may already be on HEAD; ffi/ may still be residual - full land set includes foreign C ABI thin bridge) + residual Track 3-5 product/docs/ffi/ follow-up if dirty; tag v0.1.0-core, push, require-signed-commits, release notes cut (G1.1-G1.3, G1.5, G1.6 stay open until each human step is done).
  2. Post-push smoke (G1.2): remote nix flake check green (includes crash-suite / swmr-smoke / mwmr-smoke / struct-smoke / layout-smoke / ffi-smoke / horizon2...horizon5 when full check runs; ffi-smoke is not in test-suite).
  3. Large-N get residual: Next-1 + R1 put-maintain - Plan Step 3: distinct-key multi-put get is a closed measured win (no further redesign that path; not O(1)/mmap); overwrite multi-put accepted residual / compact discipline (~O(N²) until compact). Optional denser on-disk / mmap index only if new measured need appears. F2 closed sequential-on-purpose after Next-2 1-vs-N (~1.0; no free multi-core win on current path). Workstream I: SIMD measured residual closed (scalar Bulk). Workstream E + Next-1: unique residual tree get landed. Lock-free dual MANIFEST publishers remain a north-star residual (Next-4 settled: short cooperative LOCK required; soft reopen only after SYSTEMS §4 P1-P6). Foreign C ABI depth residual is deeper partial (P6-EXPORT PR2: package default export; CLI emergency BEASTDB_USE_CLI=1; M1 measured; not lmdb.h; do not invent R7 closed).
  4. Follow SYSTEMS.md and standing Workstream K / Track 5 / R14-R15 residual hygiene - never claim missing features; open / closed / partial only when true.

Production reliability is the goal. Lean 4 proves it; the AOT binary ships it; missing pieces fail closed. Remaining work is inventory in GAPS.md.