Skip to content

API.md

Latest commit

 

History

History
666 lines (553 loc) · 46.1 KB

API.md

File metadata and controls

666 lines (553 loc) · 46.1 KB
Raw

beastdb - product API

Versioned library and CLI surface for the multi-file directory store (default) and an optional single-file store (G23; one DB file on disk - not photos/media). Pure engine modules stay pure; this layer wraps StoreDir + Lifecycle.Managed (and Layout / LayoutIO for the single-file path) with external key/value bytes and typed errors.

Naming debt: API/CLI still use Image* / image-* symbols for the single-file store (historical). Prefer "single-file store" in operator prose; rename is a separate product pass.

Library version string: beastdb.Api.version (0.1.0-core).

Getting started (operator defaults)

Default for new stores: multi-file directory (init / openStore / put / get / sync / close). That is the durable WAL put path and multi-process multi-writer multi-reader (MWMR) put path (G22). Single-file store (beastdbI magic) is opt-in - never silent-guessed as multi-file; use explicit image-* CLI or ImageHandle library ops + migrate-*.

Optional experimental snapshot compress/crypto on export/import is deferred for real use; multi-file stays unencrypted by default. Focus: put/get/sync locks.

Multi-file CLI (durable put on write-ahead log append)

nix build .#beastdb
./result/bin/beastdb init /tmp/db
./result/bin/beastdb put /tmp/db hello world   # WAL append is durability point
./result/bin/beastdb get /tmp/db hello           # prints world
./result/bin/beastdb sync /tmp/db                # checkpoint MANIFEST+shards; truncate WAL

Single-file CLI (API still says image-*; library put is in-memory)

./result/bin/beastdb image-init /tmp/db.beastdbI
./result/bin/beastdb image-put /tmp/db.beastdbI hello world  # put + checkpoint (durable)
./result/bin/beastdb image-get /tmp/db.beastdbI hello
# Library: putImage alone is NOT durable - call syncImage (or closeImage flush)

Durability asymmetry (do not conflate)

Path Put durability Multi-process MWMR put
Multi-file put / CLI put Per-leaf write-ahead log (WAL) append after leaf lock Yes (disjoint leaves)
Single-file library putImage In-memory only until syncImage No (cooperative file lock only)
Single-file CLI image-put Forces put + syncImage (durable) No

Errors (pointer)

Typed sum: io / corrupt / validation / concurrent. Thrown IO paths use substring classifyIO (order matters) - see Errors below. Fail closed: missing features and corrupt control plane refuse; orphan production temps are ignored on open (do not conflate with corrupt fail-closed).

Honest crash windows and residuals: LIMITS.md. Full gap inventory: GAPS.md.

Historical error token (G19): the greppable validation substring product AEAD (and demo expectClass / AOT greps) remains for R16 classifyIO / checks.demo stability. Operator meaning is experimental EtM export composition (requireAuth / productAead) - not NIST AEAD and not a core put path. Prefer that prose; do not half-rename the wire string without updating Main expectClass + greps together.

Module placement (flake discovery): namespaces live in existing Lean files because untracked sibling modules are invisible to pure flake builds:

Namespace File
beastdb.Types beastdb/KV.lean
beastdb.Api beastdb/StoreDir.lean
beastdb.Concurrency beastdb/Engine.lean (pure single-writer multi-reader / SWMR model; Wave 6)
beastdb.Msg beastdb/Engine.lean (L3 message protocol; Horizon 2 / G15)
beastdb.ForkJoin beastdb/Engine.lean (L2 compact/multi-get schedules; Horizon 2 / G16 + Workstream F1 leaf schedule)
beastdb.Mwmr beastdb/Engine.lean (pure disjoint-shard leases; Horizon 2 / G16)
beastdb.Structural beastdb/Engine.lean (Workstream J pure generation-fenced concurrent structural publish; product Track 3 path is StoreDir.loadStructuralBase / Api.splitAndReconcile + AOT struct-smoke)
beastdb.Resource beastdb/Engine.lean (Horizon 2 / H2.4 + Horizon 4 / G18: exclusive write ghost world, affine snapshots, unique buffers; encoded linear/affine - not language linear types)
beastdb.Bounds beastdb/Persist.lean (resource caps; Wave 7 / G10)
beastdb.Compress / beastdb.Crypto beastdb/Persist.lean (Wave 8 / G9 experimental models; co-located for flake discovery)
beastdb.Cost beastdb/Compact.lean (Horizon 1 / G14 Nat step costs; bulkByteFoldCost -> G17)
beastdb.Bulk beastdb/Persist.lean (Horizon 3 / G17 L1 portable scalar kernels; Workstream I: no product SIMD)
beastdb.Layout beastdb/Persist.lean (G23 pure single-file store codec)
beastdb.LayoutIO beastdb/PersistIO.lean (G23 single-file save/load publish protocol)
beastdb.Api single-file beastdb/StoreDir.lean (ImageHandle historical name, migrate)
CLI + demo beastdb/Main.lean (crash-suite, swmr-smoke, mwmr-smoke, struct-smoke, layout-smoke, horizon2...horizon5)

Public types (beastdb.Types)

Bytes

abbrev Bytes := List UInt8

Opaque external key/value payload (API byte sequence).

Key embedding (G8.5)

Terminology (project preference): external key = API Bytes payload; internal key = KV.Key (List Bool) after bytesToKey. Prefer those terms over "public key" / "routing key" for this distinction (see AGENTS.md § Terminology). Scan/range order is internal-key order (LSB-first bit expansion per external byte) - not always unsigned external-byte / memcmp order.

Internal keys remain KV.Key (List Bool). External key bytes expand to bits least-significant bit first, eight bits per byte:

Function Role
byteToBits / bitsToByte One-byte pack/unpack
bytesToKey Bytes -> KV.Key (external -> internal)
keyToBytes Inverse when bit length is a multiple of 8
stringToKey UTF-8 string -> internal key (CLI convenience)

Proved:

  • keyToBytes_bytesToKey - round-trip on the image of bytesToKey
  • bytesToKey_injective - distinct external keys never collide under embedding
  • length_bytesToKey - bit length is 8 * bytes.length
  • bitsToByte_byteToBits / byteToBits_injective

Docstrings do not claim cryptographic uniqueness or hash-table properties - only injectivity of the bit expansion.

Value embedding

Engine values remain KV.Value (String). At the library boundary:

Function Role
bytesToValue Each byte -> Char.ofNat (codepoint 0-255)
valueToBytes Inverse (wraps via UInt8.ofNat outside 0-255)
utf8Bytes / utf8String? CLI UTF-8 helpers

Proved: valueToBytes_bytesToValue (round-trip on the image of bytesToValue).

This is not UTF-8 for engine storage; UTF-8 is only for CLI string args.

L1 bulk helpers (beastdb.Bulk / beastdb.Api)

Horizon 3 / G17 portable scalar kernels (Workstream I measured residual: no product SIMD):

Function Role
Bulk.checksumFnv1a32Bytes FNV-1a over Types.Bytes (shares Persist.fnv1a32Step)
Bulk.bytesEq / keyEq Lex equality for bytes / bit keys
Bulk.mergeSortedKeys Sorted key-list merge helper (not product compact path)
Bulk.requireAligned / padToAlign / truncateToAlign Layout-aligned buffer views (fail closed / pad / truncate)
Api.keysEqual External key equality via Bulk.publicKeysEqual
Api.fingerprintBytes External-byte FNV fingerprint (not a MAC)

Persist whole-file codec remains char-stream; bulk is a parallel byte path with proved latin-1 FNV bridge (checksumFnv1a32Bytes_eq_chars).

Errors (beastdb.Api.Error)

inductive Error where
  | io (msg : String)
  | corrupt (msg : String)
  | validation (msg : String)
  | concurrent (msg : String)
Constructor Typical causes
io Filesystem / unexpected IO failures
corrupt Decode/checksum/MAC/decrypt failure, fail-closed open (LRR, epoch/tree mismatch); thrown messages containing corrupt / checksum / mac / wrong-key authKey/encKey / decrypt
validation Structural API refusal (existing store on init, non-leaf compact id, mid-window splitAndReconcile, bad split ids, resource bounds, closed handle (store handle closed / image handle closed), G19 requireAuth / productAead missing keys or enc-without-MAC, empty secrets when a layer was requested, ...)
concurrent Global writer LOCK held ("lock held" / "writer lock" / "stale lease"; session/structural); or per-leaf product put lock (shard lock - G22); or stale image handle sync ("stale image" - G23 free-copy when disk generation ahead); or stale structural generation fence ("stale structural" / "structural generation" - Track 3 free-copy / race loser)

Library ops return IO (Except Error α). Mapping of thrown IO.userErrors is best-effort string classification via classifyIO (order matters; Next-5 / R16 residual - not a fully typed StoreDir error algebra). Order: lock / shard lock / stale leasegenimage*structural -> concurrent; resource bounds / closed handle / requireAuth / empty-secret refuse -> validation; corrupt / checksum / mac / wrong-key crypto -> corrupt; else io. Empty-secret and resource-bound messages are classified as validation before the corrupt branch (which also matches authKey / encKey words). AOT demo greps lock the taxonomy (classifyIO taxonomy: ...). Many mutate paths return typed Error.validation / Error.concurrent directly (closed handle, G10 put gate) without going through classifyIO.

Handle

structure Handle where
  path : System.FilePath
  managed : Lifecycle.Managed
  manifest : Manifest.Manifest
  strict : Bool
  requireFsync : Bool
  leaseToken : String := ""
  closed : Bool := false   -- set on the handle **returned** by `close`

Operator rule (Tier A): treat handles as single-owner. Prefer the handle returned by every mutate / lease / sync / close. Lean values free-copy; the product does not implement language linear types.

  • Readers (openStore / get) take no exclusive lock. get remains readable after close on the same value (snapshot read).
  • Default product put (G22): per-leaf shard-<id>.lock + per-leaf WAL (not global LOCK). Session leaseToken / structural ops (sync, compact, split) use global LOCK when the token is empty or verified.
  • sync: publishes from durable disk truth (openDir under locks when trees match) and refreshes managed.store so long-lived handles do not later wipe sibling multi-process puts.
  • Closed flag: mutate paths (put, beginWrite, endWrite, compact, structural begin/finish/split, sync, exportSnapshot) call handleEnsureOpen and refuse with Error.validation (store handle closed) when the returned close handle is reused. AOT demo greps cover closed put / endWrite / compact / exportSnapshot / sync / beginWrite. Free copies of a pre-close handle are not disk-invalidated - only the returned close handle has closed := true (R6 honesty residual; discard free copies; not language linear types).
  • Stale generation / lease: free-copy after peer gen advance or endWrite fails closed on mutate via disk re-check (Error.concurrent - not validation).
  • Mid-window puts use durable putManaged (per-leaf WAL), not pure Managed.put.
  • Reads use product dual-read policy (getPolicy) on the pure snapshot in the handle (re-open or sync for a newer durable snapshot).

Concurrency (beastdb.Api + beastdb.Concurrency)

Rule Behavior
Multi-reader Concurrent openStore/get without exclusive lock
Default product put (G22) Per-leaf shard-<id>.lock + per-leaf wal/shard-<id>.log; disjoint leaves may put multi-process; same leaf -> Error.concurrent
Session / structural exclusive Global LOCK for beginWrite, checkpoint, compact, split publish section; puts fail closed while held
Structural generation fence (Track 3) Lifecycle epoch id CAS on split/reconcile; race loser or free-copy after gen advance -> Error.concurrent; AOT struct-smoke
Session lease beginWrite acquires token into LOCK (monotonic .beastdb-lease-seq under exclusive create); nested begin is no-op while token valid; endWrite / close release (close always releases even if flush fails); bare endWrite (empty token, open handle) is no-op; returned closed handle -> Error.validation on endWrite and other mutates (store handle closed)
Stale handle Pre-release handle with old token -> Error.concurrent on mutate (tokens unique across sequential acquires, not wall-clock alone)
Visibility Snapshot isolation on pure managed after open - not linearizability
Multi-shard compact (F1) Api.compactScheduleIds / compactBySchedule over pure ForkJoin.leafSchedule; sequential durable IO; pure get_compactSchedule_any / get_compactLeaves_rev (any order ≡ same gets); non-leaf ids -> validation (before durable work). Mid-schedule .error: disk may have compacted a prefix while the call-site handle is unchanged - reopen/refresh
Pure MWMR (G16) beastdb.Mwmr per-shard leases - model; product multi-process put is G22
L3 messages (G15) beastdb.Msg - mailbox + deliver; disabled -> fail closed; lease work units reject (Mwmr only); workers stub

Pure SWMR theorems live in beastdb.Concurrency (sequential lock automaton; idempotent nested beginWrite aligned with product). Concurrent same-leaf / session rejection is an IO O_EXCL fact. Cooperative only - not a kernel lease against foreign processes. AOT gate: beastdb mwmr-smoke / checks.mwmr-smoke.

Library operations (beastdb.Api)

Op Signature (conceptual) Notes
init path -> Except Error Handle Empty binary tree (shards 0|1), strict save. Refuses if MANIFEST already present unless force := true (destructive overwrite).
openStore path -> Except Error Handle Reader path (no exclusive lock except pending wal/atomic-commit recovery, which briefly takes global LOCK). Named openStore because open is a Lean keyword. Default strict := true (LRR).
get Handle -> Bytes -> Except Error (Option Bytes) Reader - getPolicy + value embedding; missing key is ok none
beginWrite Handle -> Except Error Handle Acquire session writer lease (LOCK)
endWrite Handle -> Except Error Handle Release session lease
put Handle -> Bytes -> Bytes -> Except Error Handle putManaged (per-leaf WAL; epoch preserved); leaf shard lock (or session lease); G10 refuses when maxEntries would be exceeded
compactScheduleIds Handle -> List Nat Current leaf ids (ForkJoin.leafSchedule)
compactBySchedule Handle -> List Nat -> Except Error Handle Sequential durable fold over schedule; non-leaf -> validation (F1)
compact Handle -> Option Nat -> Except Error Handle One leaf or all leaves via compactBySchedule + leaf schedule; sequential IO
beginSplit Handle -> target -> id0 -> id1 -> Except Error Handle Durable split window; gen-id fence; mid-window dual begin -> validation (id not bumped); lock held / post-finish stale gen -> concurrent
finishReconcile Handle -> Except Error Handle Close window + SC restore
splitAndReconcile Handle -> target -> id0 -> id1 -> Except Error Handle Atomic pure path + generation-fenced durable publish (Track 3); stable-only; race/stale -> concurrent
sync Handle -> Except Error Handle Checkpoint (preserve on-disk LIFECYCLE by default); closed -> validation
close Handle -> flush? -> Except Error Handle Optional checkpoint; always releases session lease if held (even when flush fails). Success: returns handle with closed := true (mutate refuse). Flush failure: returns .error only - lease is still released, but no closed handle is returned (caller must discard free-copies / reopen; residual free-copy may still show closed = false and old token -> later mutate concurrent via stale lease). Prefer returned handle on success
exportSnapshot Handle -> path -> CryptoConfig -> Except Error Unit Whole-file snapshot with optional compress/MAC/encrypt (Wave 8); closed -> validation
importSnapshot dir -> path -> CryptoConfig -> Except Error Handle Decode snapshot into multi-file dir; wrong MAC/key -> corrupt
scanOpen Handle -> Bytes -> Except Error ScanCursor P6-CURSOR + R7-SCAN: open ordered live-key scan; empty keyPrefix -> full store; external-byte prefix filter; snapshot at open; tombstones hidden; freezes internal KeyxValue pairs (not full external Bytes list); internal-key order; not B+tree
scanOpenWith Handle -> ScanOpts -> Except Error ScanCursor P6-RANGE + R7-SCAN: reverse + lower/upper inclusive/exclusive bounds (internal-key order) + prefix; same internal-pair freeze at open
scanFirst / scanLast Handle -> Bytes -> Except Error (Option (Bytes x Bytes)) P6-RANGE: first/last live pair (optional prefix); empty -> none; uses R7-SCAN open+next
getNeighbor Handle -> Bytes -> NeighborDir -> Except Error (Option (Bytes x Bytes)) P6-RANGE: LT/LE/GT/GE neighbor (internal-key order); missing -> none
len Handle -> Except Error Nat D1: live key count (tombs not counted; current managed live index - same class as get/contains; not cursor snapshot-at-open)
isEmpty Handle -> Except Error Bool D1: live count == 0 (same live class as len)
clear Handle -> Except Error Handle D1: tombstone all live keys in one multi-key atomic batch; empty OK; not hard wipe; fail closed on bad internal key bit length
deleteRange Handle -> ScanBound -> ScanBound -> Except Error Handle D1: tombstone live keys in internal-key bounds (not memcmp); one atomic batch; fail closed on key conversion (same class as clear)
scanNext ScanCursor -> Except Error (Option (Bytes x Bytes) x ScanCursor) R7-SCAN: next live pair as external Bytes on demand, or none at end; fail closed (not DONE) if internal key cannot convert - unreachable for product-opened cursors
scanClose ScanCursor -> Unit Drop cursor (GC; no IO)

Single-file store (Api.ImageHandle, G23)

Opt-in one-file database layout (not photos). Magic beastdbI; never silent-guessed as multi-file. Symbols still say Image* until a rename pass.

structure ImageHandle where
  path : System.FilePath
  image : Layout.Image
  store : Engine.Store
  requireFsync : Bool
  dirty : Bool := false
  closed : Bool := false
Op Notes
initImage Empty single-file store (binary 0|1); exists-check+write under one lock; refuse unless force
openImage Reader path; corrupt magic/frames/trailer -> Error.corrupt; G10 bounds -> validation
getImage Engine get on handle store; missing -> ok none (readable after close)
putImage In-memory only - does not touch disk; durable only after successful syncImage (or closeImage with flush := true when dirty). Closed -> validation
syncImage Checkpoint publish (temp+rename+fsync under cooperative lock); refuses if disk generation ahead (concurrent); closed -> validation
compactImage In-memory run rewrite; durable on next sync; closed -> validation
closeImage Optional flush when dirty. Success: closed := true. Flush failure: .error only (no closed handle - discard free-copies / reopen)
migrateDirToImage Explicit multi-file -> single-file; leaves multi-file intact
migrateImageToDir Explicit single-file -> multi-file; refuse existing MANIFEST unless force; mid-saveDir can leave a partial multi-file destination (source file intact)

CLI vs library (no silent durability surprise):

Entry Durability
Library putImage In-memory until syncImage / flush-on-close when dirty
CLI image-put Forces putImage + syncImage (durable)
Multi-file put / CLI put Per-leaf WAL append is the durability point

Smoke: beastdb layout-smoke. Primary multi-process path remains multi-file (G22). Single-file publish uses cooperative path.beastdb-lock only - no multi-process MWMR put on this layout. Free-copy pre-close residual same as multi-file.

Defaults: requireFsync := true on init / openStore / initImage / openImage (hard-fail path when beastdb-fsync is on PATH).

Wave 8 crypto config (Api.CryptoConfig / Persist.PersistOpts)

Field Default Role
compress false Alone -> format v3; with auth (no enc) -> v5
authKey "" / none Alone -> v4; with compress -> v5; with enc -> outer encrypt-then-MAC
encKey "" / none -> beastdbE envelope over inner v2 or v3 (auth stripped from inner)
encNonce 0 Stream-cipher nonce (caller must vary per plaintext under a key)
requireAuth false G19: when true, both non-empty authKey and encKey required (EtM only; validation / pure empty encode if either missing)

G19 experimental EtM export helpers (not a peer of multi-file put/get/sync; production crypto deferred):

Helper Role
CryptoConfig.productAead auth enc nonce compress? Both keys + requireAuth := true (experimental export path)
CryptoConfig.validate Fail closed if requireAuth and either key empty (no silent plaintext)
PersistOpts.productAead / productAeadOk? Pure dual: both keys required under requireAuth

Format matrix (no envelope unless encKey set):

compress authKey encKey Result
false empty empty v2 (default)
true empty empty v3 framed compress + FNV
false set empty v4 + keyed MAC
true set empty v5 framed compress + keyed MAC
* set set beastdbE EtM (experimental export composition)
* empty set enc-only outer FNV (experimental; only when requireAuth = false)

Default multi-file writes stay unencrypted v2-style shards. Wave 8 / G19 layers are opt-in on whole-file export/import only. Empty key strings disable layers when requireAuth = false. With requireAuth / productAead, both keys must be non-empty (validation refuse - no silent plaintext). CLI snapshot-export with auth+enc uses productAead. Keys are caller-supplied only. Do not reuse (encKey, encNonce). Not NIST AES-GCM / AEAD - algorithms remain G9 keyed FNV + stream-XOR.

CLI (beastdb binary)

Lean passes process argv to main (args : List String) (program name excluded).

Args Behavior
(empty) or demo Built-in Waves 1-8 + Horizon 2-5 demo (checks.demo greps)
version Print beastdb 0.1.0-core
init <dir> Create empty multi-file store (fails if MANIFEST exists)
put <dir> <key> <value> UTF-8 key/value put
get <dir> <key> Print UTF-8 value (exit 2 if missing)
compact <dir> [shardId] Compact all leaves or one leaf shard (unknown id -> validation)
split <dir> <target> <id0> <id1> beginSplit
reconcile <dir> finishReconcile
sync <dir> Checkpoint
bench <dir> [n] Multi-file microbench: N puts, get-all pre-compact, multi-shard compact (compact_schedule / mode=sequential), get-all post-compact (TreeMap unique), checkpoint, get-all post-sync, cold reopen get-all post-reopen (Tier B re-detect + index); ops/s + disk (default n=1000; large N human; R1 Plan Step 3: distinct-key multi-put get closed measured win ~O(N log N); overwrite accepted residual / compact discipline ~O(N²) until compact - not O(1)/mmap)
bench-image <file> [n] Single-file store microbench (CLI name historical): N puts, get pre-sync, sync, get post-sync; compare with multi-file (Workstream E)
crash-suite Horizon 1 / G13 + G23 + Workstream G + Track 4 + Tier D: cooperative simulated multi-file + per-leaf WAL + single-file/migrate + compact-on-publish / production-temp crash windows (not hardware power-fail; not CI kill -9 mid-put / mid-sync - residual; human offline recipe in TESTING.md); checks.crash-suite
swmr-smoke Horizon 1 / G13: multi-process SWMR (second writer fail closed; reader get ok); checks.swmr-smoke
mwmr-smoke G22: multi-process MWMR product put on disjoint leaves (both succeed; same-leaf fail closed); checks.mwmr-smoke
layout-smoke G23: pure single-file codec + product init/put/sync/open/get + stale free-copy sync refuse + migrate both ways; checks.layout-smoke
image-init <file> Create empty single-file store (beastdbI; not photos)
image-put <file> <key> <value> Put + syncImage (durable)
image-get <file> <key> Get from single-file store (exit 2 if missing)
image-sync <file> Checkpoint rewrite + publish
migrate-to-image <dir> <file> Explicit multi-file -> single-file store
migrate-to-dir <file> <dir> Explicit single-file -> multi-file
horizon2 Horizon 2 / G15-G16 + F1 + Workstream J: L3 fail closed, L2 schedule, product multi-shard compact ≡ pure gets, pure MWMR, pure Structural concurrent publish model, resources; checks.horizon2
struct-smoke Track 3 multi-process generation-fenced structural (race one-wins; stale free-copy concurrent; reopen coherent); checks.struct-smoke
split-reconcile CLI atomic Api.splitAndReconcile (used by struct-smoke children)
horizon3 Horizon 3 / G17: L1 bulk FNV/compare/merge/align (scalar; Workstream I measured residual - no product SIMD); checks.horizon3
horizon4 Horizon 4 / G18: exclusive write + affine snapshot + buffer uniqueness; checks.horizon4
horizon5 Horizon 5 / G19-G20: experimental EtM export composition + requireAuth fail closed + shard locks; checks.horizon5
shard-lock-try <dir> <shardId> Multi-process helper: acquire/release one shard lock (exit 0/1)
snapshot-export <dir> <file> [authKey] [encKey] [encNonce] Compress default; auth alone -> MAC; auth+enc -> G19 productAead (both non-empty required; empty either -> Error.validation); default nonce = monoMs
snapshot-import <dir> <file> [authKey] [encKey] Import; nonce from envelope; auth alone -> MAC; auth+enc -> productAead (not enc-only; empty either -> validation)

CLI put / get keys/values are UTF-8 strings mapped through Types.utf8Bytes and the external-key embedding (bytesToKey). This is a convenience over the byte API, not a separate key space.

Subcommand Notes
put-bytes <dir> Binary-safe: stdin u32be keyLen | key | u32be valLen | val -> product Api.put with raw Types.Bytes (fail closed on truncate/oversize; max field 16 MiB)
put-bytes-multi <dir> Bulk binary: stdin u32be count | (u32be keyLen | key | u32be valLen | val)* - one open session applies N pairs (foreign multi-put path; max count 1_000_000; fail closed on truncate/oversize/bad count). Not multi-key ACID if mid-batch fails
get-bytes <dir> Binary-safe: stdin u32be keyLen | key; stdout u32be valLen | val (exit 2 if missing; no println framing)
contains-bytes <dir> Existence only: stdin u32be keyLen | key; exit 0 present, exit 2 missing; no value on stdout (still product Api.get under the hood)
delete-bytes <dir> Product tombstone delete: stdin u32be keyLen | key; exit 0 success including missing key (idempotent); no stdout payload (P6-DEL)
scan-bytes <dir> Ordered live-key scan (P6-CURSOR): stdin u32be keyPrefixLen | keyPrefix (len=0 -> full store); stdout u32be count | (u32be kLen|key|u32be vLen|val)*; tombstones hidden; internal-key order
scan-bytes-ex <dir> P6-RANGE extended scan: stdin prefix + flags + lower/upper bound frames; reverse/range (internal-key order)
first-bytes / last-bytes P6-RANGE first/last live pair; stdout framed pair; exit 2 if empty
neighbor-bytes <dir> P6-RANGE neighbor: stdin u32be keyLen|key|u8 kind (0=LT 1=LE 2=GT 3=GE); exit 2 if none
atomic-batch-bytes <dir> P6-ACID multi-key atomic batch: stdin u32be count | (u8 tag | frames)* - tag 0 put (u32be kLen|key|u32be vLen|val), tag 1 del (u32be kLen|key); all ops apply or none (product temp+rename); not LMDB page-level ACID
len-bytes <dir> D1: stdout u32be live count (tombs not counted)
clear <dir> D1: tombstone all live keys (multi-key atomic batch; empty OK)
delete-range-bytes <dir> D1: stdin bound frame (kinds 0/1/2); internal-key range delete batch

Foreign C ABI (ffi/include/beastdb.h, BEASTDB_API_VERSION 9): UTF-8 beastdb_put / beastdb_get; length-prefixed beastdb_put_bytes / beastdb_get_bytes (malloc'd value + length; caller free); bulk beastdb_put_bytes_multi (not multi-key ACID); multi-key atomic beastdb_atomic_batch_bytes (P6-ACID; tags 0=put / 1=del); existence beastdb_contains / beastdb_contains_bytes (missing -> BEASTDB_ERR_VALIDATION); product tombstone beastdb_delete / beastdb_delete_bytes (missing -> BEASTDB_OK idempotent; not LMDB free-page reclaim); ordered cursor beastdb_cursor_open / beastdb_cursor_next / beastdb_cursor_close (end -> BEASTDB_ERR_DONE, not missing-key); reverse/range beastdb_cursor_open_ex + first/last/neighbor (API v8 / P6-RANGE; internal-key order); D1 beastdb_len / beastdb_clear / beastdb_delete_range_bytes (API v9; live count; tombstone-all; internal-key range). Dual-backend (P6-EXPORT PR2 + P6-CURSOR + P6-ACID + P6-RANGE + D1): package default is export (same-process compiled @[export] full v9; no mid-env flip; no per-symbol CLI fallback on an EXPORT env). CLI emergency at open via BEASTDB_USE_CLI=1 (one spawn per call / per multi or atomic batch / one scan per cursor open). R7 is deeper partial (not closed). See Foreign bindings / Rust crate below.

EXPORT long-lived handle visibility (R7-SNAP docs): an open EXPORT env holds a long-lived product Api.Handle snapshot. Idle point reads do not auto-follow peer multi-process puts on every get. To load a newer durable snapshot into that env:

  1. Reopen the env (close + open), or
  2. Successful sync - product Api.sync / C beastdb_sync / Rust Env::sync refreshes managed.store from durable disk truth (G22 publish base when routing trees match; EXPORT replaces the in-process handle via leanEnvSync). After a successful sync, subsequent point reads on that same env can see peer durable puts without close+open.

There is no dedicated beastdb_env_refresh in C ABI v9 (optional future Wave B2 only if embed need). CLI contrast: the CLI emergency backend reopens the store per call (fork/exec), so the next op sees durable peer puts without a long-lived in-process snapshot. Not LMDB multi-version concurrency control (MVCC) / reader-table auto-follow - sync is an explicit durable checkpoint that also refreshes the handle, not silent per-get follow. R7-SNAP is docs honesty only and does not close R7.

Resource bounds (beastdb.Bounds)

Constant Default Applied at
maxEntries 1_000_000 Api.put / StoreDir.put / open / save / checkpoint
maxShards 4_096 open / save / beginSplitDir (+2 children)
maxEncodedBytes 256 MiB whole-file save/load; multi-file saveDir/checkpoint/openDir via encode-length proxy; per-shard + WAL file size on multi-file load

Exceeding bounds:

Path Result
Api.put / save / checkpoint / multi-file open (per-file, aggregate, post-recover) Error.validation (resource bound via throw + classifyIO)
Image openImage / loadImage oversize or engine resource bounds Error.validation (throw resource bound...)
Whole-file loadStore / loadStoreStrict oversize Option none (pre-stat; no product Error until mapped)
Missing/corrupt multi-file component or image decode Error.corrupt

Loads pre-stat file size before readBinFile (no multi-GB materialise-then-reject on a single component). Multi-file open tracks aggregate on-disk bytes and aborts before loading further components when the running sum exceeds the cap. See BENCHMARKS.md and LIMITS.md.

Lifecycle notes

  1. Stable epoch: get ≡ leaf get under the routing tree.
  2. Split window: get uses dual-read on the raw leaf binding first (live put or delete tombstone), then dual-reads the orphan only when the leaf has no raw binding for that key. Empty child leaves do not hide orphan data for keys that were never written post-split. A mid-window delete installs a leaf tombstone that wins over orphan history (product get stays missing; finishReconcile / putIfAbsent gap-fill does not resurrect the pre-split value).
  3. Durable window recovery: LIFECYCLE side file + openManaged / openStore. Mid-window writers must go through put -> putManaged (and delete -> deleteManaged for tombstones).
  4. Fail closed: corrupt codecs, LRR (strict), epoch/tree mismatch -> Error.corrupt.
  5. Concurrency (Wave 6 SWMR + G22 MWMR put): multi-reader snapshots; disjoint leaf multi-process puts; same-leaf or global session/structural LOCK -> Error.concurrent. Cooperative protocol, not kernel leases. Not linearizability.
  6. splitAndReconcile is stable-only: does not run mid-window (would publish a stable LIFECYCLE and clobber the open orphan). Call finishReconcile first.
  7. init does not clobber an existing multi-file store unless force.
  8. Handle free-copy (Tier A): mutate refuses closed returned handles (Error.validation) and stale gen/lease free-copies (Error.concurrent). Pre-close free copies are not globally invalidated - single-owner discipline is an operator rule, not a language linear type.

Honest IO / crash windows: LIMITS.md.

Foreign bindings / Rust crate

First-party language bindings live under ffi/<lang>/ (not product engine logic; Lean remains the single source of truth for store semantics). Residual R17 closed (Phases 3-5): heed-inspired Rust crate + selective T0/T1/T2 flake suite + docs honesty. Phase 6 advanced (partial): bulk multi-put + contains

  • product delete (P6-DEL) + Mode B flush policy (size/count/max_delay) + P6-EXPORT PR2 dual-backend + P6-CURSOR + P6-ACID + P6-RANGE + D1 (API v9 len/clear/delete_range + reverse/range + atomic batch; Rust Mode B unlimited multi-key commit/abort; export package default) + D2 done (RoTxn / read_txn; selective T2 8; MIGRATE-HEED.md) + D3 measure done (M2) + R7-BYTES done (export get ByteArray + bulk memcpy; ABI unchanged) + R7-SCAN done (lazy external-pair cursor; snapshot-at-open; ABI unchanged) + R7-SNAP done (docs-only: EXPORT idle gets do not auto-follow peers; reopen or successful sync refreshes; not LMDB MVCC). R7 deeper partial (not closed). Board: PLAN.md; completed: PLAN-COMPLETED.md; remaining: PLAN-REMAINING.md (default next G1 human; P6-WAL optional/deprioritized).
Path / package Role
ffi/rust/beastdb/ First-class Rust crate (heed-shaped ergonomics; thin v0)
beastdb-rust Nix package for the crate
checks.beastdb-rust-smoke / beastdb-rust-t0 / beastdb-rust-t1 / beastdb-rust-t2 Flake gates (full nix flake check; not in test-suite subset)
ffi/include/beastdb.h + beastdb-lib Shared C application binary interface (ABI); dual-backend - export package default + CLI emergency (BEASTDB_USE_CLI=1); force export (BEASTDB_USE_EXPORT=1); R7 deeper partial

Getting started shape (Rust)

Open a multi-file env, put, commit (durable publish), get - with both write modes available:

  1. Mode A (immediate): each put hits the C ABI / CLI bridge; commit() -> durable publish (sync / checkpoint).
  2. Mode B (batch / P6-ACID): buffer puts and deletes in the crate; optional BatchFlushPolicy (max_pairs / max_bytes / max_delay) auto-flushes via product multi-key atomic batch (beastdb_atomic_batch_bytes) without durable sync when thresholds hit (lazy time check on put/delete or WriteTxn::poll_flush); commit() flushes remaining ops via one atomic batch then durable publish. Drop/abort discards only the unflushed buffer - already auto-flushed chunks stay applied (not rolled back). With BatchFlushPolicy::unlimited, whole-txn multi-key abort is product-atomic for that buffer. This is beastdb multi-key atomic batch, not LMDB page-level ACID. (put_bytes_multi remains a separate non-ACID bulk path.)
  3. Contains: Database::contains -> Result<bool> (missing is false, not error).
  4. Delete: Database::delete -> product tombstone (missing is Ok(()) idempotent). Not LMDB free-page reclaim. Mode A applies delete immediately; Mode B buffers deletes with puts for one atomic batch on commit (unflushed ops invisible to get/contains).
  5. Iterate (P6-CURSOR + P6-RANGE): Database::iter / prefix_iter / rev_iter / range / rev_range / first / last / neighbors -> RoIter over product ordered scan (C ABI v6/v8). Snapshot at open; tombstones hidden; internal-key order (not always unsigned external-byte). Freezes live unique index + internal pairs at open; external Bytes on next (R7-SCAN; not LMDB B+tree cursor).
  6. Count / clear / range-delete (D1): Database::len / is_empty / clear / delete_range (C ABI v9). Live keys only; clear = tombstone-all atomic batch; range bounds are internal-key (not memcmp).
  7. Read view (D2): Env::read_txn -> RoTxn (heed-shaped; point reads = product path; cursors snapshot at open; not LMDB MVCC reader table). db.get(&rtxn, key) works alongside db.get(&env, key). Migration: MIGRATE-HEED.md.

Typical path: open -> put -> commit -> get/contains/delete/iter/len/clear (and reopen to confirm durability). Codecs shipped: Bytes + Str. Corrupt / missing control plane at open fails closed (not empty success).

Thin v0 completeness (one-liner)

Enough for open -> put/get/contains/delete/iter/len/clear -> commit/sync -> reopen, dual write paths (+ flush policy + Mode B multi-key atomic batch + D1 range-delete), Bytes/Str, and fail-closed corrupt open - a small core slice of heed's public surface, not "most of heed." Missing (non-exhaustive): mut cursors, multi-DB, nested txns, map_size, serde, full MdbError. Port/Adapt/Skip + completeness table: HEED-MAP.md §6-§8.1.

Cross-links and honesty bounds

  • Residual R17 closed in GAPS.md (crate + selective T0/T1/T2); does not close R7 (PR2 dual-backend is deeper partial - export package default; CLI emergency; not lmdb.h / free-page reclaim; long-lived snapshot visibility delta on EXPORT envs).
  • Workstream plan: PLAN.md. Prior art: PRIOR-ART.md (heed family). Test map: TESTING.md.
  • Bindings durability story is local embedded durability (uninterruptible power supply (UPS) / laptop battery assumed) with explicit commit/sync - see LIMITS.md for product IO honesty. This is not a durability-"C1" class and is not fitness C1 / R3 (lock-free dual MANIFEST publishers).

Non-claims (bindings)

  • Not lmdb.h / LMDB on-disk wire or page format.
  • Not full heed suite green; suite is selective heed-shaped beastdb tests (T0+T1+T2). heed3 tests: zero (encryption-at-rest contrast only).
  • Not heed3 encryption-at-rest product.
  • Not power-fail / kill -9 mid-write claims (R9/R10 unchanged).
  • C ABI package default is export (PR2); CLI emergency via open-time BEASTDB_USE_CLI=1. Export handles are long-lived snapshots (not CLI per-call reopen). R7-SNAP: peer multi-process puts are not auto-visible on idle gets - reopen or successful sync refreshes the handle from disk (not LMDB MVCC; no beastdb_env_refresh in v9; docs-only; does not close R7). R7 deeper partial (large get ~linear; scan open freezes index; static .a CLI-only). R7-RT open; goal = E (fix Lean) - ship still loads libleanshared on export; see LIMITS.md Embed TCB.

What this API does not claim

  • Same-leaf multi-writer or put during global session/structural LOCK (-> Error.concurrent)
  • Lock-free dual MANIFEST / structural publishers without cooperative LOCK (Track 3 ships generation-fenced multi-process structural with short exclusive section required + AOT struct-smoke; pure model is beastdb.Structural; Next-4 / R3 residual - dual-publisher north-star deferred pending P1-P6 + soft reopen in SYSTEMS.md §4; not shipped; not abandoned)
  • Linearizability of concurrent IO (C3 deferred - snapshot isolation only)
  • Kernel leases against foreign processes (C2 deferred - cooperative trust among honoring beastdb processes only; foreign/bypassers not excluded)
  • NIST-grade MAC / AEAD / AES / post-quantum crypto (Wave 8 / G19 are pure models under key secrecy only - Tier D3 / R11 deferred product decision; multi-file unencrypted by default; Next-6 soft reopen only after explicit product decision + real algorithms + key management + fail-closed defaults)
  • Automatic encryption of multi-file MANIFEST/shards/WAL (export/import opt-in only)
  • zstd / libzstd wire compatibility or proved optimal compression ratio (Tier D4 / R12 deferred; soft reopen only if storage size is real operator pain + stack-legal boundary)
  • Power-fail integration tests beyond the cooperative protocol (Tier D2 / R10 - not claimed; lab-only if ever; soft reopen only with lab instrumentation + honesty; never marketing without product)
  • Process kill -9 mid-put / mid-sync under continuous integration (Tier D1 / R9 not claimed / cooperative-only; crash-suite file windows only; optional human offline recipe - never CI; soft reopen only with hermetic stable CI story + fixtures; never flaky kill-9 gate without design)
  • Stable wire ABI versioning beyond Api.version string
  • Task-parallel / multi-core wall-clock shard compaction in the extracted binary (F1 schedule wiring closed; sequential durable IO under SWMR on purpose after Track 2 + Next-2 measure; F2 closed measured residual - no multi-core speedup claim)
  • Multi-GB throughput parity with LMDB (microbench only; BENCHMARKS.md)
  • Drop-in wire/page replacement for LMDB / LevelDB / RocksDB (see PRIOR-ART.md). Foreign C ABI (ffi/include/beastdb.h, package beastdb-lib) is an LMDB-class embeddable open/put/get/contains/delete/cursor/atomic-batch/range/len/clear/sync surface for C/C++/Rust - dual-backend (export package default + CLI emergency); UTF-8 + length-prefixed binary keys/values + bulk multi-put + contains + product tombstone delete + ordered cursor + multi-key atomic batch + reverse/range/first-last/neighbor + D1 len/clear/delete_range (API v9); not lmdb.h clone / not LMDB on-disk format / not LMDB free-page reclaim / not LMDB page-level ACID (GAPS R7 depth residual is deeper partial, not closed)

Related docs

  • VISION.md - architecture / roadmap
  • GAPS.md - gap inventory SSOT (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; F2 closed measured residual sequential on purpose; F3 / R18 deferred; large-N get partial win (Next-1 + R1 put-maintain; Plan Step 3 settled): distinct-key multi-put get closed measured win (no further redesign); overwrite multi-put accepted residual / compact discipline ~O(N²) until compact; no O(1)/mmap; Workstream J / Track 3 generation-fenced structural closed with short-LOCK required residual; Next-4 / R3 dual-publisher north-star deferred (LOCK required; not shipped); lock-efficiency pure + SYSTEMS budget shipped (not lock-free dual publishers); foreign C ABI CLI bridge partial; Tier C dual-publisher / kernel-lease / linearizability honesty; Next-6 Tier D R9-R12 assurance residuals settled (not claimed / deferred + soft reopen; not product land); Workstream I / R13 SIMD closed measured residual; human G1.x open)
  • TESTING.md - flake gates + crash residual honesty (Tier D1 human offline kill recipe); ffi-smoke under full nix flake check
  • LIMITS.md - durability honesty + lock budget / FFI bridge honesty
  • BENCHMARKS.md - bench methodology + sample numbers (no O(1) get claim)
  • PRIOR-ART.md - LMDB / LevelDB / Breccia + heed family (Wave 9 + G11.4 + R17)
  • HEED-MAP.md - Port/Adapt/Skip; suite provenance; thin v0 completeness
  • PLAN.md - bindings Phases 0-5 done; Phase 6 advanced (partial); P6-ACID + P6-RANGE done; P6-WAL remaining optional; PLAN-REMAINING.md
  • Foreign ABI: ffi/include/beastdb.h (API v9); packages beastdb-lib, beastdb-ffi-c, beastdb-ffi-cpp, beastdb-ffi-rust; check ffi-smoke (dual-backend export default + CLI emergency + atomic batch + range + D1; R7 deeper partial)
  • First-party Rust crate: ffi/rust/beastdb/; checks beastdb-rust-smoke / beastdb-rust-t0 / beastdb-rust-t1 / beastdb-rust-t2 (R17 closed Phases 3-5; T0 8 / T1 26 / T2 8; heed3 tests zero; thin v0 + D1 + D2)
  • PROOFS.md - theorem inventory (includes lock-efficiency Concurrency/Mwmr theorems)