beastdb

beastdb is a production-oriented, high-assurance embedded key-value store.

License: Unlicense (public domain dedication).

Store logic and proofs are Lean 4. Build, packaging, and repo tooling are Nix flakes only. Foreign language bindings live under ffi/ (shared C ABI, demos, and a heed-inspired Rust crate at ffi/rust/beastdb/). Lean remains the single source of truth for store semantics. The product name is always lowercase beastdb.

What ships

Package	Role
nix build .#libbeastdb	Freestanding product library: libbeastdb.a, no Lean managed runtime in the consumer. Systems Lean spine (put/get/delete/sync). Product direction.
nix build / .#beastdb	Host CLI + proofs (lean4-nix pin). Multi-file durable store.
nix build .#beastdb-lib	Older export+runtime residual library (full C ABI for demos/YCSB/Rust). Not freestanding; not an alias of libbeastdb. Do not expand.

Embed goals and honesty bounds: docs/LIMITS.md. Freestanding measure baseline: docs/BENCHMARKS.md § Original baseline figures. Design notes: docs/LEAN4.md. Project rules: AGENTS.md.

just                 # default: flake check + full measure suite (thr / LMDB / YCSB-C / charts)
just check           # gates only (no long measure)
just bench           # measure suite only

Or piece by piece:

nix build .#libbeastdb
./result/bin/beastdb-demo
nix run .#freestanding-gate
nix run .#libbeastdb-thr -- 10000   # freestanding vs residual thr (TMPDIR)
nix run .#suite-report -- --archive # thr + LMDB micro + YCSB-C + charts

Standing measure goal: real YCSB-C against freestanding libbeastdb (today YCSB still uses the residual export library until freestanding depth is ready).

Quick start (CLI)

nix develop
nix build
./result/bin/beastdb

Multi-file directory (default durable path)

./result/bin/beastdb init /tmp/db
./result/bin/beastdb put /tmp/db hello world
./result/bin/beastdb get /tmp/db hello
./result/bin/beastdb sync /tmp/db

Optional single-file store

One file on disk (image-* CLI names mean single-file store layout, not photos).

./result/bin/beastdb image-init /tmp/db.beastdbI
./result/bin/beastdb image-put /tmp/db.beastdbI hello world
./result/bin/beastdb image-get /tmp/db.beastdbI hello

Build, measure, gates

./result/bin/beastdb bench /tmp/db-bench 1000
nix run .#bench
nix run .#test-suite
nix flake check
nix run .#install-hooks   # namecheck + whitespace pre-commit; GPG pre-push
nix run .#whitespace-check
nix run .#whitespace-fix
# Prove thr + suite still emit the same machine-readable format (not a perf SLA):
nix run .#measure-format-smoke

API surface: docs/API.md. Limits (what we do not claim): docs/LIMITS.md. How to measure: docs/BENCHMARKS.md. How to test: docs/TESTING.md.

Prior-art trees under ref/ are git submodules (study only, not required for nix build). Clone with --recurse-submodules or git submodule update --init --recursive.

Human-only: commit and push (GPG required)

Agents never create commits or push.

git commit -m "your message"   # signed after install-hooks
nix run .#verify-signatures
git push                       # pre-push refuses unsigned history

Documentation

File	Purpose
AGENTS.md	Project rules (languages, naming, git/GPG)
docs/VISION.md	Architecture and roadmap
docs/GAPS.md	Open/closed residual inventory
docs/LIMITS.md	Honest durability and embed bounds
docs/API.md	Library and CLI surface
docs/BENCHMARKS.md	Measure methodology and baseline figures
docs/TESTING.md	Flake checks and how to run tests
docs/RELEASE.md	Human land / tag / push checklist
docs/PROOFS.md	Proof inventory honesty
docs/PRIOR-ART.md	Prior art (LMDB, LevelDB, Breccia, heed, ...)
docs/CONSUME-RUST.md	Using the Rust crate from another app
PLAN.md	Bindings / heed migration plan
docs/PLAN-COMPLETED.md	Completed plan items
docs/PLAN-REMAINING.md	Remaining plan work
ref/README.md	Reference submodules

Status (plain language)

Shipped: multi-file durable store; single-writer multi-reader sessions; multi-writer puts on disjoint leaves; generation-fenced multi-process structural ops; optional single-file layout; machine-checked Lean core + AOT CLI via Nix; freestanding libbeastdb spine (no managed runtime) with measure suite; foreign C/Rust bindings (export residual path still used for full ABI demos and YCSB).

Open / do not invent closed: freestanding embed depth (multi-file freestanding, full freestanding C surface, YCSB against freestanding library); not LMDB wire or page-format compatible; cooperative crash testing only (not CI kill-9 / not power-fail claims); human signed publish steps (docs/RELEASE.md).

Full residual board: docs/GAPS.md.

Constraints (summary)

• Product engine: Lean 4 only
• Foreign bindings: ffi/<lang>/ only (not product engine)
• Build/tooling: Nix flakes only
• Name: only beastdb (nix build .#namecheck)
• Agents never commit or push
• Every pushed commit must be GPG-signed

Full rules: AGENTS.md.