This document is the single source of truth (SSOT) for how we treat the machine, the ahead-of-time (AOT) binary, and missing features. It does not store host inventory.
Related: VISION.md (roadmap), LIMITS.md (IO honesty), BENCHMARKS.md (measure), PROOFS.md (proof inventory).
| Claim | Status |
|---|---|
| Product logic is written and proved in Lean 4 | True - product modules under beastdb/ |
Shipped runtime is the Lean C-backend AOT binary from nix build |
True - not a separate hand-written C engine |
| Generated C is source of truth for the product | False - generated C is compiler output; never hand-edited or committed as product source |
| "Works in Lean interpreter ⇒ product" | False - gates are nix build / nix flake check / demo / bench on the extracted binary |
Workflow (non-negotiable):
- Specify + implement + prove in Lean (or explicitly scope out in LIMITS/GAPS).
- Test via flake checks and CLI on the AOT binary.
- Measure when performance claims are made (BENCHMARKS); model costs in Lean are not wall-clock.
- Only then treat the extracted binary as the database product for a given feature.
Thin Nix-generated helpers (e.g. beastdb-fsync, LMDB microbench harness) are allowed at the OS boundary. They are not the KV engine and must not reimplement product logic.
If a capability is not present, the product must not pretend it is.
Prefer fail closed (Error.validation / Error.corrupt / Error.concurrent /
process exit non-zero) or a documented soft degrade - never silent wrong answers.
| Situation | Required behavior |
|---|---|
Optional helper missing (beastdb-fsync) |
Soft degrade to flush-only unless requireFsync := true -> then throw |
Auth/enc key missing for v4/v5/beastdbE load |
Fail closed (none / Error.corrupt) |
| Empty string crypto config | Layer disabled (documented); some [] at PersistIO refused |
| Second concurrent writer (today) | Error.concurrent - not silent multi-writer |
| Multi-process MWMR put (G22 shipped) | Disjoint leaves: two processes may both put; same leaf or global LOCK held -> Error.concurrent |
| Multi-process structural (Track 3 / J) | Generation-fenced splitAndReconcile race: one wins, loser -> Error.concurrent; short cooperative LOCK still serializes publish critical section |
| SIMD / vector path unavailable | Use portable scalar path (current product: always scalar Bulk); never claim single instruction multiple data (SIMD) speedups without a real measured vector path |
| Resource bound exceeded | Error.validation (G10) |
| Corrupt checksum/MAC | Fail closed load - no "best effort" partial store |
Product rule: capability flags and docs must stay aligned. A feature behind a
gap ID that is open is unavailable; APIs that would need it either do not
exist yet or fail closed.
Assumptions must be checked against code, measure, or upstream docs. Update this table when evidence changes.
| ID | Assumption | Evidence / validation | If false -> |
|---|---|---|---|
| A1 | Prefix trie partitions keys so each key maps to exactly one leaf | Proved routing / LRR paths in Engine | Stop MWMR design until fixed |
| A2 | Latest-value compact preserves gets | Theorems get_compact family |
Do not claim compact safety |
| A3 | Cooperative LOCK excludes second writer among honoring processes |
Demo + O_EXCL; not kernel vs foreign processes | Document LIMITS + §4 C2 trust model; never claim kernel leases (deferred) |
| A4 | Temp+rename publish is atomic for one file | POSIX rename; multi-file still multi-step | Crash suite (G13); LIMITS windows |
| A5 | AOT extract preserves pure-function semantics for pure core | Trusted TCB (Lean+C+kernel); demo gates | Keep no-sorry; expand tests |
| A6 | Unique residual: TreeMap uniqueIndex when keysUnique (Next-1; after compact / Tier B cold-open re-detect / R1 put-maintain on fresh-key put); overwrite / non-unique: latestRev (≡ fold-latest; reverse charges full reverse in Cost) |
Code + beastdb.Cost (treeLookupCost / productLookupCost_*) + BENCHMARKS Step 2 grid + Step 3 decision |
Plan Step 3: distinct-key multi-put get closed measured win (~O(N log N); no further redesign); overwrite accepted residual / compact discipline ~O(N²) until compact; not O(1); no mmap B+tree claim |
| A7 | Disjoint leaf shards enable concurrent writers without clobbering each other's keys | Routing disjointness proved; pure beastdb.Mwmr (G16); G22 product put = per-leaf lock + per-leaf WAL; AOT mwmr-smoke; Track 3 structural generation fence + struct-smoke |
Lock-free dual MANIFEST publishers residual (Tier C design preconditions §4); short cooperative LOCK required; not kernel leases; not linearizability |
| A11 | Experimental EtM export composition over G9 models, not NIST AEAD / not core put path | G19: requireAuth / productAead; EtM theorems + AOT horizon5 |
Never claim AES-GCM/NIST; multi-file unencrypted default; production crypto deferred |
| A8 | Breccia mark-word design is mmap-friendly blob storage | ref/breccia/DESIGN.md |
Study only; do not copy format without design |
| A9 | FNV trailer is integrity not authentication | LIMITS/G9 honesty | Use keyed MAC model or real crypto for auth claims |
| A10 | Host has useful multi-core for C1 | Local probe only (see §5); not committed | Parallel work still correct if 1 core |
A7 is critical: sharding is the enabler of MWMR. Pure model closed (G16).
G22 ships multi-process product put on disjoint leaves (per-leaf lock + WAL).
Track 3 / Workstream J product slice ships generation-fenced multi-process
structural publish (lifecycle epoch id CAS + short cooperative LOCK).
Checkpoint / compact / session beginWrite still use global LOCK. Cooperative
only - not kernel leases.
| Mode | Meaning | Status |
|---|---|---|
| SWMR (session / structural critical section) | One exclusive global LOCK for beginWrite, checkpoint, compact, split publish section; many readers with pure snapshots |
Shipped Wave 6 |
| MWMR put (G22) | Multiple writers may durable-put on disjoint leaf shards concurrently; same-shard conflicts fail closed; readers snapshot-isolated | Shipped - per-leaf lock + per-leaf WAL; AOT mwmr-smoke |
| Structural CAS (Track 3) | Generation-fenced structural publish (lifecycle epoch id); race loser / stale free-copy -> Error.concurrent; store coherent |
Shipped - short LOCK + fence; AOT struct-smoke |
Goal interpretation of full use of system resources but no more: product and pure models grant exclusive resources only where the concurrency contract requires them; residual serialization is documented, not grepped as free multi-core or lock-free.
| Product path | Exclusive resource held | Why needed | Evidence |
|---|---|---|---|
openStore / get |
None (pure snapshot) | Snapshot isolation without reader lock thrash | Pure Concurrency.step_read; AOT SWMR smoke |
Default put (empty lease) |
Per-leaf shard-<id>.lock only |
Disjoint leaves may write concurrently (G22); same leaf fail closed | Pure Mwmr.tryAcquire_disjoint_*; mwmr-smoke |
beginWrite session |
Global LOCK + lease token |
Multi-op exclusive writer section | Pure wellFormed_session; Wave 6 demo |
| Checkpoint / compact / structural publish | Short global LOCK (+ wait for leaf locks when needed) |
Multi-file MANIFEST/LIFECYCLE multi-step atomicity |
Next-4 residual: not lock-free; struct-smoke |
Atomic pure put/compact (no session) |
Virtual exclusive for the step only | Pure SWMR automaton does not leave exclusive held after free-path put/compact | step_put_from_free_no_excess_hold |
| Task multi-core compact | Not shipped | Disk/metadata dominate; sequential on purpose after measure | F2 closed measured residual; BENCHMARKS 1-vs-N |
Not claimed: kernel leases against foreign processes; linearizability; lock-free dual MANIFEST publishers; product SIMD; absolute global maximality theorems beyond pure cost/ordering + measure-gated residual honesty.
Pure modules in Engine.lean prove lock histories and lease maps, not
multi-process file IO. Full mismatch table: PROOFS.md § pure model
vs product concurrency.
| Pure surface | Product exclusive resource | Misread to avoid |
|---|---|---|
Concurrency free-path put exclusive for one automaton step |
Per-leaf shard-<id>.lock only (G22); global LOCK is not held by default put |
Pure SWMR put exclusive ⇒ product forbids concurrent puts on disjoint leaves |
Mwmr disjoint leaf leases |
Same per-leaf lock files + WAL | Pure lease theorems ⇒ kernel leases / linearizability |
Structural generation-fenced CAS on free-copy State |
Short global LOCK + durable lifecycle epoch (struct-smoke) |
Pure CAS race loser ⇒ lock-free dual MANIFEST publishers shipped |
ForkJoin.multiGet_parallel_eq (definitional) |
Sequential product evaluation; compact schedule F1 under SWMR | "Parallel" ⇒ Task multi-core wall-clock (F2 closed residual) |
Operator footguns that proofs do not refine (handle free-copy, single-file put vs sync, mid-schedule compact lag, WAL soft fsync): LIMITS.md § operator safety.
Horizon 2 + Horizon 5 + G22 + Track 3 status (honest):
| Layer | Status |
|---|---|
| Pure per-shard lease + disjoint put model | Shipped (beastdb.Mwmr; AOT horizon2) |
| Sequential ≡ schedule compact / multi-get | Shipped (beastdb.ForkJoin; product uses leafSchedule via F1) |
| Per-shard cooperative lock files | Shipped - shards/shard-<id>.lock; wired into product put |
| Per-leaf write-ahead log | Shipped - wal/shard-<id>.log (+ legacy wal/wal.log replay) |
| Product multi-process put on disjoint leaves | Shipped (G22) - checks.mwmr-smoke |
| Pure concurrent structural publish model (Workstream J) | Shipped - beastdb.Structural generation fence + unique publisher; AOT via horizon2 |
| Product multi-process generation-fenced structural | Shipped (Track 3) - loadStructuralBase / trySplitAndReconcileDir; AOT struct-smoke |
Lock-free dual MANIFEST publishers (no cooperative LOCK) |
Not shipped - short exclusive section required (Next-4 / R3 honesty residual; north-star deferred pending P1-P6 below; not abandoned) |
| Kernel multi-writer leases | Deferred - cooperative trust only (C2) |
| Linearizability of concurrent IO | Deferred - snapshot isolation honesty (C3) |
This section is the product design note for directory metadata publish
(MANIFEST directory control plane + LIFECYCLE epoch file) and for the
north-star residual of dual publishers without a process-held exclusive
LOCK. Expand short names on first use: MANIFEST, LIFECYCLE, compare-and-swap
(CAS), multi-writer multi-reader (MWMR).
Who wins a race: two processes open the same multi-file store at lifecycle
epoch id G and both call atomic splitAndReconcile (CLI split-reconcile).
Cooperative O_EXCL on dbDir/LOCK serializes the critical section. The first
publisher to hold LOCK reloads durable managed + MANIFEST, checks
expectedGen = G, applies pure Lifecycle.splitAndReconcile, publishes shards +
MANIFEST + LIFECYCLE at generation G+1, then releases. The second process
either fails while LOCK is held (lock held -> Error.concurrent) or, after
the first finishes, fails the generation fence (stale structural generation ->
Error.concurrent). Exactly one structural transform is durable. Evidence:
AOT struct-smoke (one wins, one concurrent; stale free-copy concurrent; reopen
coherent).
Critical-section scope (honest, not reduced without measure): under LOCK
the product already (1) reloads durable base, (2) waits for relevant per-leaf
shard locks, (3) rewrites shard epoch files + MANIFEST + LIFECYCLE + WAL
truncate via publishCheckpointCore. Session beginWrite, checkpoint, and
compact also take global LOCK. Tier C does not claim a smaller exclusive
window was measured or shipped; the generation fence alone is not sufficient
to remove exclusivity while multi-file publish remains multi-step.
What readers see: readers take no exclusive lock. They materialize a pure
snapshot of MANIFEST + shards + write-ahead log (WAL) + LIFECYCLE. During a
race they may observe either generation G or G+1 (snapshot isolation -
not linearizability). After reopen they see a coherent post-publish store
(gets preserved for keys not rewritten by the pure transform).
Crash windows: publish remains multi-step (shard files, then MANIFEST, then
LIFECYCLE, then WAL truncate) under lock - same multi-file honesty as G13.
Half-published state is never reported as API success (throw before return).
Orphan production temps are ignored on open (image .beastdb-tmp, multi-file
MANIFEST.tmp / LIFECYCLE.tmp / per-leaf WAL *.log.tmp); incomplete or
corrupt control-plane files fail closed (e.g. corrupt LIFECYCLE, missing
MANIFEST-named shard, torn image - crash-suite / Track 4). Stale free-copy
handles after generation advance fail closed on mutate - they must not clobber a
newer durable tree. Returned close / closeImage handles set closed := true
(mutate -> Error.validation); free-copy pre-close values are not
disk-invalidated (Tier A residual - single-owner operator rule, not linear types).
Relationship to pure beastdb.Structural: the pure model encodes a single
shared-state lineage with generation fence (tryCasPublish_*, unique structural
session on one value). Product maps lifecycle epoch id ↔ pure gen and uses
loadStructuralBase under cooperative exclusive. Pure free-copied multi-world
"two winners" is not the product story; product uniqueness is exclusive
LOCK + durable epoch fence along one on-disk lineage. Race-loser theorems are
single-lineage, not free-copy multi-world re-check.
Decision (Next-4 / R3 reaffirmation): full lock-free dual directory
publishers (two processes publish MANIFEST / LIFECYCLE without a process-held
exclusive critical section) is not shipped. Short cooperative exclusive
LOCK is required today. Dual-publisher is a north star deferred (not
abandoned forever) - soft-reopen only after all of P1-P6 below. Do not
invent a greppable "lock-free dual publishers shipped" claim without a product
path + smoke evidence.
Reasons (fail-closed preference over aspirational concurrency):
- Multi-file publish is multi-step. Shard epoch files, MANIFEST,
LIFECYCLE, and WAL truncate are separate durable steps. Without mutual exclusion, two publishers can interleave renames and leave a control plane that no open path can treat as a single coherent generation. - Generation CAS is necessary but not sufficient. Comparing lifecycle epoch id at the start of a publish detects stale plans; it does not serialize the multi-rename publish window. A pure CAS on one file does not make a multi-file directory atomic.
- Crash reopen must fail closed. Corrupt or mismatched MANIFEST/
LIFECYCLEalready returnsnone/Error.corrupt. Dual concurrent publishers without exclusivity widen torn-control-plane windows beyond what crash-suite models. - G22 puts still need a quiet publish window. Structural publish waits for
per-leaf shard locks so concurrent puts cannot append mid-rewrite. Global
LOCKalso makes ordinary puts fail closed during the section so checkpoint cannot race put-side durable appends.
Product multi-file steps under LOCK today (trySplitAndReconcileDir /
publishCheckpointCore - unchanged multi-step shape since Track 3 / Tier C):
| Step | Product action | Atomic alone? |
|---|---|---|
| 1 | loadStructuralBase - open managed + lifecycle epoch id fence + load MANIFEST |
No (read fence only) |
| 2 | Pure Lifecycle.Managed.splitAndReconcile on disk store |
Memory only |
| 3 | Wait for leaf / prior per-leaf shard locks | Quiet put window |
| 4 | Per-shard writeShardFile at new epoch names |
Each file may temp+rename; many files |
| 5 | writeManifest (temp+rename) |
One control-plane file |
| 6 | writeLifecycle at generation G+1 (temp+rename) |
One control-plane file |
| 7 | Truncate per-leaf WALs; best-effort remove superseded shard epochs | After publish |
Readers that open between steps 4-6 can still see a coherent pre- or post-
publish snapshot only because cooperative LOCK excludes a second
publisher. Without LOCK, two racers can interleave steps 4-6 and violate P1.
A correct product path may remove process-held exclusive LOCK for structural
publish only if all of the following hold. Until then residual language must
say the exclusive critical section is required.
| # | Precondition | Rationale | Status vs product today (Next-4) |
|---|---|---|---|
| P1 | Single atomic visibility unit for generation. Readers that open mid-publish must see either full generation G or full G+1 - never MANIFEST naming shards that do not exist, or LIFECYCLE epoch id that disagrees with the published tree. Options include dual-meta generations (two MANIFEST candidates + generation pointer), or a single rename that switches a complete prepared tree. Partial multi-rename without a generation fence on the last visibility flip is forbidden. |
Without a last visibility flip, multi-file steps 4-6 above are not one generation. | Unmet - no dual-meta pointer / single rename of a prepared tree; multi-step under LOCK |
| P2 | Prepare-then-CAS publish order. (1) Write new shard epoch files under unused names; (2) stage new MANIFEST body (temp); (3) stage new LIFECYCLE at G+1 (temp); (4) CAS-publish only if on-disk generation is still G (loser abandons temps, does not delete winner files); (5) best-effort GC of superseded epochs. Race loser -> Error.concurrent; never report success after observing generation advance. |
Separates prepare from visibility so racers do not clobber each other. | Partial under LOCK only - epoch files + temp+rename + gen fence exist, but publish visibility is not a single lock-free CAS of a generation pointer |
| P3 | Reader open rules. Open must resolve the durable generation first, then load only MANIFEST/shards/LIFECYCLE that agree with that generation (epochOkForOpen / agreesWithTree style). Mismatch or corrupt control plane -> fail closed (none / Error.corrupt), never "best effort" merge of two racers' files. |
Dual racers must not produce a "merged" open that is neither G nor G+1. | Met for shipped LOCK path - open fails closed on mismatch; not re-proved for dual-meta candidates (none exist) |
| P4 | Crash windows documented + crash-suite fixtures. Orphan temps remain ignored; half-published dual-meta candidates must not become the open winner; corrupt pointer / trailer still fail closed. Extend crash-suite / struct-smoke before claiming ship. |
New windows appear only with dual-meta / prepare-CAS; cooperative fixtures today assume exclusive publish. | Unmet for dual-publisher - crash-suite covers cooperative LOCK-era windows only |
| P5 | Put interaction. Concurrent G22 puts on leaves being rewritten must still fail closed or wait; publish must not drop durable WAL records that won their leaf lock before the generation flip. Keep pure Structural / product fence alignment (lifecycle epoch id = CAS generation). |
Structural rewrite must not race leaf WAL appends. | Met under LOCK (puts fail closed while held; shard locks waited); lock-free design must re-specify this |
| P6 | Evidence bar. Two-process race smoke (one wins, one concurrent), stale free-copy concurrent, reopen coherent gets, and pure-model alignment before any "lock-free dual publishers" status flip. No linearizability claim as a substitute for smoke. | Greppable product proof, not aspirational docs. | Met for LOCK+fence path (struct-smoke); not evidence for lock-free dual publishers |
Soft reopen criteria (explicit): re-open product work to remove structural
LOCK only when a design implements all of P1-P6 with:
- Product code path that does not hold process exclusive
LOCKfor the MANIFEST /LIFECYCLEpublish critical section. - Extended
crash-suitefixtures for dual-meta / prepare-CAS crash windows (orphan temps ignored; half-published candidates never win open; corrupt pointer / trailer fail closed). - Extended
struct-smoke(or successor) grepping lock-free race honesty only after the path exists - never flip residual status on docs alone. - No silent dual success; no greppable "lock-free dual publishers shipped" string until the above evidence is in tree.
Until then residual board language: short cooperative LOCK required;
lock-free dual MANIFEST publishers = honesty residual / north star deferred
(not abandoned; not shipped).
Out of scope for that land (still deferred): kernel multi-writer leases (C2); linearizability of concurrent IO (C3).
Trust model (cooperative only): LOCK and per-leaf shard-*.lock use
O_CREAT|O_EXCL create. Processes that honor the beastdb protocol exclude
each other. Foreign processes (or operators) that ignore the protocol, delete
lock files, or write MANIFEST/shards/WAL out of band are not excluded by the
kernel - there is no mandatory file lease, flock product path, or OS mandatory
locking in the extracted binary.
Deferred with reason: kernel leases are not implemented. Lean/Nix product boundaries do not expose a portable, proved, multi-OS mandatory lock API in this tree; even if added later, tests would need multi-process foreign-writer fixtures proving exclusion - not present today. Do not claim kernel leases.
Not claimed. Concurrent readers may observe generation G or G+1 during a publish race (snapshot isolation on pure snapshots after open). The product does not provide a single linearization point for all multi-process puts + structural publishes. Pure models prove generation-fence and routing properties, not an interleaving refinement of concurrent IO. Leave deferred; not the next fitness milestone after Tier C residual honesty.
| Item | Status |
|---|---|
Generation-fenced multi-process structural + struct-smoke |
Shipped (Track 3 / J product slice) |
Short cooperative exclusive LOCK on MANIFEST/LIFECYCLE critical section |
Required today (Next-4 / R3 reaffirmation - not lock-free dual publishers) |
| Lock-free dual MANIFEST / structural publishers | Honesty residual / north star deferred (Next-4 settled: P1-P6 above; soft reopen only after all preconditions + smoke; not abandoned; no product path) |
| Kernel multi-writer leases | Deferred (cooperative trust only; no OS lease API + tests) |
| Linearizability of concurrent IO | Deferred (snapshot isolation honesty) |
| Free-copy pre-close global invalidation | Honesty residual (Tier A; not linear types) |
| Kill-mid-write under CI (R9) | Not claimed / closed residual as cooperative-only (Tier D1; crash-suite + human offline recipe in TESTING; never flake check). Soft reopen only with hermetic stable CI story + fixtures; never a flaky kill-9 gate without design |
| Hardware power-fail (R10) | Not claimed (Tier D2; lab-only if ever). Soft reopen only with lab instrumentation + honesty; never marketing without product |
| NIST / standards-grade encryption at rest (R11) | Deferred product decision (Tier D3; G9/G19 models; multi-file unencrypted default). Soft reopen only after explicit product decision + real algorithms + key management + fail-closed defaults |
| Compression ratio / libzstd (R12) | Deferred (Tier D4; framing + demo RLE only). Soft reopen only if storage size is real operator pain and a stack-legal boundary exists |
| Product SIMD (R13 / I) | Closed measured residual (scalar Bulk only; not open work). Soft reopen only if Bulk is a measured hotspot and a legal path exists without forbidden product C |
| L3 multi-process worker pool (R18 / F3) | Deferred (pure Msg only). Soft reopen only after explicit architecture decision for multi-process workers; no distributed-DB claim |
Pure / product modules that form the systems-facing corpus. Add new kernels by following the SOP in §6; wire an AOT horizon check when the kernel is product-facing.
| Module | Home | Role | Horizon / gap |
|---|---|---|---|
beastdb.Bulk |
Persist.lean |
L1 portable scalar kernels (FNV, cmp, merge, align) | G17 / H3 |
beastdb.Cost |
Compact.lean |
Nat step cost model for get/scan/unique | G14 / H1 |
beastdb.Msg |
Engine.lean |
L3 mailbox protocol (fail closed when off) | G15 / H2 |
beastdb.ForkJoin |
Engine.lean |
L2 compact schedule + multi-get; product leaf schedule (F1) | G16 / H2 / F1 |
beastdb.Mwmr |
Engine.lean |
Pure per-shard leases (not multi-process put) | G16 / H2 |
beastdb.Structural |
Engine.lean |
Pure generation-fenced concurrent structural publish (product path is Track 3) | Workstream J / Track 3 |
beastdb.Resource |
Engine.lean |
Encoded linear/affine exclusive write / snapshot / buffer | G18 / H4 |
beastdb.Crypto / Compress |
Persist.lean |
G9 models; G19 product EtM composition | G9 / G19 / H5 |
beastdb.Concurrency |
Engine.lean |
Pure SWMR lock histories | G6 |
| Product AOT CLI | Main.lean |
horizon2...horizon5, bench, crash-suite, swmr-smoke, mwmr-smoke, struct-smoke, layout-smoke |
gates |
- Portable scalar kernels first (checksum, compare, merge) as Lean specs.
- Landed (G17 / Horizon 3):
beastdb.Bulk- byte FNV (sharesfnv1a32Stepwith product char path), byte/key compare, sorted merge helpers, alignment predicates; AOThorizon3/checks.horizon3. - Optional faster paths: local measure is necessary but not sufficient. Workstream I re-measured the extracted product and kept scalar (Bulk not primary hotspot; pure Lean cannot ship true Advanced Vector Extensions (AVX2) / NEON without handwritten product C, which AGENTS.md forbids). Any future path must be fail-closed, scalar-equivalent, and within stack policy - not "probe flags present ⇒ ship SIMD."
- SIMD status (Workstream I closed - measured residual): product path remains scalar only. Local
host-probemay report vector flags (anonymous class only - e.g. multi-core + AVX2 present on a measured host);profile-cpuon the extracted ahead-of-time (AOT) product bench does not show Bulk compare/hash as the primary hotspot (get fold / compact / checkpoint dominate). No product "uses AVX2" claim; probe flags != vector runtime. - Docs that record methodology, not your laptop's serial number.
Agents and humans may run local probes to prioritize work:
nix run .#host-probe # preferred: short report, no machine identity fields
# or ad-hoc: lscpu, garuda-inxi - still never commit dumpsNever commit:
- Full
inxi/garuda-inxidumps - Hostnames, usernames, serial numbers, hardware UUIDs, disk/LUKS UUIDs, MAC addresses
- Exact firmware strings that identify a single machine
Allowed in docs (anonymous class only): e.g. "8 cores, AVX2 available."
Do not assume advanced vector extensions (AVX-512, NEON, SVE). Prefer portable
byte kernels first. Workstream I re-measured: keep scalar beastdb.Bulk;
do not invent a "vector-shaped" pure API that claims single instruction multiple
data (SIMD) speedup without a real vectorized product path. Optional future
vector helpers only after a local measure, a path that cannot disagree with
scalar, and stack policy that still forbids handwritten product C. See
BENCHMARKS.md for profiling the extracted binary with Linux
tools packaged in the flake.
The product is the ahead-of-time (AOT) binary from nix build. Profile that
binary, not lean --run. Workstream B / G21 packages this workflow.
| Command | Role |
|---|---|
nix run .#host-probe |
Logical CPUs + optional vector flags (terminal only; ephemeral) |
nix run .#bench -- 1000 |
Wall-clock put/get vs LMDB microbench |
nix run .#profile-cpu -- 500 |
CPU sample (perf when available) of a short bench; else wall-clock |
nix run .#profile-mem |
Memory check (valgrind when available) of short init/put/get; else plain put/get |
nix run .#deep-cpu |
Deep call-graph (perf record ± optional flamegraph) on non-stripped AOT binary; soft-degrade to bare same workload; G24 closed (Workstream L) - not CI |
nix run .#deep-mem |
Deep heap timeline (valgrind Massif) on non-stripped AOT binary; default short-putget + --trace-children; soft-degrade to bare same workload; G24 closed - not CI |
nix run .#deep-rr |
Deep reverse-debug (rr record + replay recipe) on non-stripped AOT binary; removes prior rr-trace then lets rr create the pack; soft-degrade to bare same workload; G24 closed - not CI |
nix run .#value-assess |
Fixed value-assessment scenario matrix (AOT + C application binary interface / ABI); allowlisted results.tsv; fail-closed on product/ABI (no soft-degrade); G24 closed - not CI; not LMDB parity / not an SLA |
nix run .#asan-smoke |
ASan/UBSan Phase A smoke on C demo + unsanitized libbeastdb.so (mixed-link); fail-closed on sanitizer fire; not product ASan clean; G24 closed - not CI |
nix run .#ycsbc |
Linked Yahoo! Cloud Serving Benchmark in C++ (YCSB-C) with -db beastdb (measure-only ref/ link + bench/ycsb driver); workloads A-F; prefer -threads 1; not CI / not LMDB parity |
nix run .#ycsb-bench |
Lightweight first-party proportion harness (not full YCSB-C client) |
nix run .#suite-report |
Comprehensive power-labeled suite (compare-lmdb + ycsb A + optional ycsbc-A / fair ycsbc-compare + thr + value-assess -> metrics.tsv + charts/*.svg); TMPDIR; optional --archive -> $XDG_DATA_HOME/beastdb-bench-history/<profile>/<stamp>/; see BENCHMARKS.md § Comprehensive measure suite |
nix run .#test-suite |
Continuous-integration-safe gates (includes host-probe; not long profiles / deep measure) |
Deep perf record / rr may need kernel permissions (performance monitoring
unit / ptrace) and are not CI gates; wall-clock bench always works without
root. Profile wrappers soft-degrade (exit 0) when tools are missing or
unusable if the product path still succeeds. value-assess does not
soft-degrade product/ABI failures. asan-smoke fails closed on sanitizer
fire (demo instrumentation only - do not claim product ASan clean). Full test
map: TESTING.md. Methodology, daily deep-measure workflow, and
hyperfine notes: BENCHMARKS.md. G24 deep measure suite
is closed (deep-cpu + deep-mem + deep-rr + value-assess + sanitizer
Phase A (+ optional Phase B CLI package); not in test-suite / default
flake checks; soft-degrade tools vs fail-closed product/sanitizer; not
product ASan clean; not LMDB parity; do not reopen G21).
| Layer | Role | Doc / gate |
|---|---|---|
| Cost model (Lean) | Nat steps / sizes: "more efficient / less efficient" relative to another algorithm | PROOFS.md beastdb.Cost / Bulk.byteFoldCost |
| AOT bench | Wall ms, ops/s on the extracted binary | BENCHMARKS.md; checks.bench |
| Alternatives | LMDB microbench, optional Nix-generated C kernels on same synthetic load | nix run .#bench |
| Mismatch | Document extraction, allocation, cache - refine model or code; never "proved fast" without measure | release notes + BENCHMARKS notes |
- Specify pure Lean API + honesty docstring (what is not claimed).
- Prove round-trip / fail-closed / cost inequalities (no
sorry). - Wire product surface only if needed (
Api.*); else keep pure. - AOT demo CLI string + flake
checks.horizonNgreps (or extend existing). - Measure only if making a wall-clock claim - record method in BENCHMARKS; never commit host dumps.
- Update GAPS status, PROOFS inventory row, SYSTEMS corpus index.
Cost model (Horizon 1 / G14 + Workstream E + Next-1 / R1): pure namespace
beastdb.Cost (co-located in Compact.lean) - Nat step counts only
(foldLookupCost, scanLookupCost, treeLookupCost, uniqueLookupCost_le_fold,
productLookupCost / productLookupCost_compact_le_rev). The last theorem is
same residual list only (does not bound pre-compact wall vs post-compact wall;
reverse-path residual is overwrite / non-unique only - distinct-key pre-compact
is TreeMap after R1 put-maintain).
treeLookupCost is a coarse order-of-log model (log2 n + 1; not exact
Std.TreeMap probe count, not wall-clock, not O(1)). Product get uses TreeMap
uniqueIndex.get? when tagged keysUnique (after compact / single-file sync /
multi-file checkpoint compact-on-publish / Tier B cold open when residual
keys are Nodup - re-detect builds the index), else latestRev (≡ fold-latest).
Wire decode does not persist the flag; ofEntries / normalizeStore
re-detect uniqueness from residual keys (Tier B). R1 put-maintain (Plan Step
3): put of a fresh key on a unique residual keeps the TreeMap - distinct-key
multi-put get is a closed measured win (no further redesign that path);
overwrite / non-unique residuals stay on reverse get (accepted residual /
compact discipline ~O(N²) get-all until compact). Wall-clock remains
BENCHMARKS.md; model-measure mismatches are insight, not
proof failures.
| Layer | Intent | Gate before claiming |
|---|---|---|
| L3 message passing | Workers for shard IO / compact | G15 closed (pure): beastdb.Msg protocol + fail closed when disabled; F3 deferred - no multi-process worker pool; no distributed DB claim |
| L2 fork-join | Multi-core map over shards/runs | G16 + F1 closed (pure + product schedule): ForkJoin.leafSchedule / compactSchedule join ≡ sequential gets; product Api.compactBySchedule sequential durable IO on purpose (Track 2 / Tier B2 + Next-2); F2 closed measured residual - no Task multi-core compact |
| L1 data parallel | Bulk kernels | G17 closed (scalar) + Workstream I measured residual: beastdb.Bulk portable FNV/compare/merge/align; product never claims SIMD; no assumed ISA |
| Resource discipline | Exclusive write / affine snapshot / unique buffers | G18 closed (Horizon 4 + Tier A): pure encodings in beastdb.Resource; product leaseToken free-copy + re-verify; returned closed refuse mutate; pre-close free-copy residual |
| Experimental EtM export composition | Whole-file export/import only | G19 closed (Horizon 5): G9 models + requireAuth; not NIST AEAD; production crypto deferred; not a peer of put/get/sync |
Details: VISION.md.
| ID | Topic |
|---|---|
| G13 | Crash + multi-process evidence - closed in tree (Workstream G + Track 4 depth: cooperative simulated multi-file + per-leaf WAL + image/migrate + production temps + compact-on-publish windows; orphan temps ignored vs corrupt control plane fail closed - do not conflate). Next-6: not power-fail HW - Tier D2 / R10 not claimed (soft reopen: lab instrumentation + honesty); not kill-9 mid-put / mid-sync under CI - Track 4 + Tier D1 / R9 not claimed / cooperative-only (soft reopen: hermetic stable CI + fixtures; never flaky kill-9 gate); human offline recipe in TESTING |
| G14 | Get-path / cost proofs - closed in tree (Workstream E + Tier B cold-open re-detect + Next-1 TreeMap unique index + R1 put-maintain fresh-key keeps unique); residual honesty (Plan Step 3): distinct-key multi-put get closed measured win (no further redesign that path; ~O(N log N) not O(1)); overwrite multi-put accepted residual / compact discipline ~O(N²) until compact; on-disk single-file store product path is G23 closed |
| G15 | L3 message protocol - closed (pure + AOT demo; no worker pool product) |
| G16 | L2 fork-join + pure MWMR - closed (product multi-process put is G22; F1 product schedule wiring) |
| F1 | Product multi-shard compact schedule ≡ pure leaf schedule - closed (sequential IO) |
| F2 | Task / multi-process disjoint compact IO - closed (measured residual - sequential on purpose) after Track 2 + Next-2 / R2 1-vs-N (~1.0); recipe in BENCHMARKS; no greppable parallel path; soft reopen only after measured fail-closed win; never silent half-compact |
| F3 | L3 multi-process Msg worker pool - deferred (Tier B3 / R18: pure protocol only; no product worker pool; no distributed DB claim). Soft reopen only after explicit architecture decision for multi-process workers |
| G17 | L1 kernels - closed (scalar) |
| I | Optional ISA / SIMD (R13) - closed (measured residual): keep scalar Bulk; probe may show flags; no product vector path. Soft reopen only if Bulk is measured hotspot + legal path without forbidden product C |
| J | Concurrent structural publish - closed (pure + Track 3 product slice): beastdb.Structural generation fence; product multi-process generation-fenced structural + struct-smoke; short cooperative LOCK required (Next-4 / R3 residual - not lock-free dual publishers; P1-P6 + soft reopen in §4) |
| G18 | Full linear/affine encodings - closed (Horizon 4) with honesty: API + ghost world + proofs; not language linear types |
| G19 | Experimental EtM export composition - closed (Horizon 5); algorithms remain G9 models; not NIST; production crypto deferred |
| G20 | Systems corpus + proof↔measure methodology - closed (Horizon 5) |
| G22 | Multi-process MWMR product put on disjoint leaves - closed (mwmr-smoke) |
| G23 | Single-file store product path + migrate - closed (layout-smoke) |
| Lock-efficiency | Needed exclusivity only - shipped (pure Concurrency / Mwmr theorems; § lock resource budget; AOT lock efficiency: ... greps). Not lock-free dual publishers |
| Foreign C ABI | Dual-backend deeper partial (P6-EXPORT PR2 + P6-CURSOR + P6-ACID + P6-RANGE + D1 + D2 + D3/M2 measure + R7-BYTES + R7-SCAN) - beastdb-lib / ffi-smoke shipped; UTF-8 + length-prefixed binary put/get + multi/contains/delete/cursor/atomic-batch/range/len/clear API v9; package default = export; CLI emergency BEASTDB_USE_CLI=1; M2 + R7-BYTES (bulk export get; still ~linear large-value) + R7-SCAN (lazy external pairs; open still freezes live index); not lmdb.h / LMDB wire / LMDB page ACID; R7 deeper partial (not closed) |
| Heed-inspired Rust crate (R17) | Closed Phases 3-5 + D2 - ffi/rust/beastdb/ thin v0 + selective T0 8 / T1 26 / T2 8; heed3 tests zero; not full heed; does not close R7 (HEED-MAP.md, PLAN.md) |
Summary: The database product is the proved-then-extracted AOT binary.
Missing features fail closed or degrade only when documented. Assumptions
are listed and checked. Multi-writer multi-reader (MWMR) put on disjoint
leaves is shipped (G22). Generation-fenced multi-process structural
is shipped (Track 3 / Workstream J product slice + struct-smoke); short
cooperative global LOCK still serializes the MANIFEST / LIFECYCLE
critical section (required today). Lock-efficiency (exclusive resources only
where the concurrency contract needs them) is shipped as pure theorems +
the lock resource budget above + AOT honesty greps - still not lock-free dual
MANIFEST publishers. Session beginWrite / checkpoint / compact remain
single-writer multi-reader (SWMR) under global LOCK. Tier C + Next-4 / R3
residual honesty: lock-free dual MANIFEST publishers not shipped (LOCK
required; dual-publisher north-star deferred pending P1-P6 + soft reopen in
§4; not abandoned); kernel multi-writer leases deferred (cooperative trust
only); linearizability deferred (snapshot isolation). Single-file store path
Foreign C ABI is deeper partial dual-backend (beastdb-lib / ffi-smoke;
length-prefixed binary put/get + multi/contains/delete/cursor/atomic-batch/range/len/clear API v9;
export package default; CLI emergency BEASTDB_USE_CLI=1) - not LMDB wire, not
full lmdb.h, not free-page reclaim, not LMDB page ACID. R7 is deeper partial
(not closed; D3/M2 measured; R7-BYTES bulk-copy + R7-SCAN lazy pairs do not close R7).
R17 closed separately (heed-inspired thin v0 crate + T0/T1/T2; Phase 6 advanced
partial with P6-EXPORT PR2 export package default). Hardware probes guide work without polluting
the repo.