Skip to content

RELEASE.md

Latest commit

 

History

History
858 lines (691 loc) · 46.5 KB

RELEASE.md

File metadata and controls

858 lines (691 loc) · 46.5 KB
Raw

beastdb: release and land checklist (v0.1.0-core)

This document is for humans only. Agents may prepare the tree and docs; they must never run git commit, git tag, or git push (AGENTS.md).

What you are publishing (plain language)

A production-oriented embedded key-value store written in Lean 4, built with Nix, with:

  • Multi-file durable store (init/put/get/sync, compaction, crash windows that are cooperative only - not power-fail claims)
  • Freestanding library package packages.libbeastdb (Systems Lean spine; no Lean managed runtime in the consumer) - product direction
  • Temporary full C ABI library packages.beastdb-lib (export + managed runtime) for demos / YCSB / Rust - not freestanding; not an alias
  • Foreign bindings under ffi/ (C header + bridge + Rust crate)
  • Machine-checked core + AOT host CLI; flake checks green before you tag

Still open (do not claim closed on the tag): deeper freestanding embed (multi-file freestanding product, full freestanding C surface, YCSB against freestanding); not LMDB wire/page compatible; human G1 publish steps below.

Inventory IDs (Horizons, waves, gap codes) live in GAPS.md for maintainers. They are not the public product story. Historical CLI names like beastdb horizon3 are internal CI demos only.

Use this checklist for the first published core line, tag v0.1.0-core.

G1.4 (continuous integration / CI) is already closed in GAPS.md: the in-tree workflow .github/workflows/ci.yml runs nix flake check. Confirming the first remote green build is a post-push smoke check under G1.2, not a separate open gap.

Human residual (leave open in GAPS until done): G1.1, G1.2, G1.3, G1.5, G1.6. Do not mark those closed until the corresponding step below is complete. Do not mark G1 as a whole closed while any of those rows remain open.

Open product residuals after land (not human G1): L3 worker pool (F3 / R18 deferred - pure Msg only; soft reopen only after architecture decision for multi-process workers; no distributed-DB claim); large-N get partial win (Next-1 + R1 put-maintain; Plan Step 3 settled): distinct-key multi-put get closed measured win (TreeMap; ~O(N log N); get_pre ~= post-compact; no further redesign that path - not O(1)/mmap); overwrite multi-put accepted residual / compact discipline (~O(N²) until compact; Workstream E + Tier B cold-open re-detect; no O(1) / mmap B+tree). F2 closed measured residual: sequential durable IO on purpose after Track 2 + Next-2 / R2 1-vs-N (~1.0; F1 schedule closed; no greppable Task multi-core compact). Free-copy pre-close handle residual (returned close handle only; not language linear types - Tier A / Next-5 / R6; mutate refuse grepped). Single-file store put durability partial (Next-5 / R8: library putImage in-memory; CLI image-put durable; not photos). classifyIO audited residual (Next-5 / R16). Workstream J / Track 3 generation-fenced multi-process structural is closed (product slice + pure model; short cooperative LOCK required - Next-4 / R3 residual honesty: not lock-free dual publishers; dual-publisher north-star deferred pending P1-P6 + soft reopen in SYSTEMS.md §4; struct-smoke). Workstream I / R13 (optional single instruction multiple data / SIMD) is closed as measured residual - product keeps scalar Bulk; host-probe flags != product SIMD (soft reopen only if Bulk is measured hotspot + legal path without forbidden product C). G22 multi-process multi-writer multi-reader put and G23 single-file layout are closed (mwmr-smoke / layout-smoke; see LAYOUT.md). 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 (ffi/ + beastdb-lib / checks.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 + D1 len/clear/delete_range); not lmdb.h / LMDB wire / LMDB page ACID; R7 deeper partial; land set must include ffi/).

Freestanding dual-package honesty (land set must include freestanding work):

  • packages.libbeastdb (nix build .#libbeastdb) - freestanding product library (Systems Lean spine; no libleanshared). Paths: freestanding/, nix/libbeastdb.nix, thr measure nix/libbeastdb-thr.nix, design LEAN4.md, flake input systems-lean in flake.lock.
  • packages.beastdb-lib (nix build .#beastdb-lib) - temporary export+runtime residual for full C ABI v9 / demos / YCSB / Rust. Not an alias of packages.libbeastdb.
  • Same on-disk library name libbeastdb; two package attrs; R7-RT remains open (Phase 5 packaging/docs promote != C5 Embed TCB close). Do not invent R7-RT closed at tag time. Gate: nix run .#freestanding-gate.

Kernel leases and linearizability remain deferred (C2 cooperative trust / C3 snapshot isolation - not claimed). Tier D / Next-6 assurance residuals (not product features to ship next): R9 kill-mid-write under CI not claimed / cooperative-only; R10 power-fail not claimed; R11 NIST crypto deferred product decision; R12 libzstd/ratio deferred - soft reopen criteria in GAPS.md. Full residual inventory: GAPS.md.

Index hazard (common failure mode): agents update the working tree but do not git add. The index may still hold pre-Horizon blobs (early wave-only land scope, Wave 9-only staging, no G11.4 / SYSTEMS / Horizon 1 / G21). Never git commit on a stale index. Re-run the full Required paths git add block, then pass the Index must match working tree gates below. If git status shows MM / AM / ?? on any LAND_PATHS entry, do not commit until those paths are re-staged and the pre-commit checks pass.

Scratch / do not stage: _u8.lean was a throwaway Lean #check scratch at repo root. Agents deleted it; if it still appears in the index (AD / A), drop it before commit:

git reset HEAD -- _u8.lean 2>/dev/null || true
rm -f _u8.lean
# must not appear in staged set:
git status --porcelain | rg '_u8' || true   # empty expected

Do not stage result*, .lake, host-identity dumps (garuda-inxi, full inxi, serials, UUIDs, hostnames), or probe output from nix run .#host-probe.

Prerequisites

  • user.signingkey and a working gpg-agent configured
  • nix run .#install-hooks already run in this clone (local commit.gpgsign / tag.gpgsign, pre-commit, pre-push)
  • Tree reviewed; no accidental secrets; product name remains lowercase beastdb
  • No host-identity dumps (garuda-inxi, etc.) staged - SYSTEMS.md privacy rule
  • _u8.lean absent from working tree and index (see above)
  • Local gates green (run before staging/commit):

Product / smoke gates (required - same continuous-integration-safe core as nix run .#test-suite, minus optional bench):

nix build .#namecheck --no-link
nix build .#beastdb --no-link
nix build .#checks.x86_64-linux.no-sorry --no-link
nix build .#checks.x86_64-linux.demo --no-link
nix build .#checks.x86_64-linux.crash-suite --no-link
nix build .#checks.x86_64-linux.swmr-smoke --no-link
nix build .#checks.x86_64-linux.mwmr-smoke --no-link
nix build .#checks.x86_64-linux.struct-smoke --no-link
nix build .#checks.x86_64-linux.layout-smoke --no-link
nix build .#checks.x86_64-linux.horizon2 --no-link
nix build .#checks.x86_64-linux.horizon3 --no-link
nix build .#checks.x86_64-linux.horizon4 --no-link
nix build .#checks.x86_64-linux.horizon5 --no-link
nix build .#checks.x86_64-linux.host-probe --no-link
# Foreign C ABI dual-backend (deeper partial ship; R7 deeper partial) - in full flake check / land prep;
# **not** part of `nix run .#test-suite`:
nix build .#checks.x86_64-linux.ffi-smoke --no-link
# Heed-inspired Rust crate selective suite (R17; not full heed; heed3 tests zero):
nix build .#checks.x86_64-linux.beastdb-rust-smoke --no-link
nix build .#checks.x86_64-linux.beastdb-rust-t0 --no-link
nix build .#checks.x86_64-linux.beastdb-rust-t1 --no-link
nix build .#checks.x86_64-linux.beastdb-rust-t2 --no-link
# Freestanding product library (not in default test-suite; dual-path vs beastdb-lib):
nix build .#libbeastdb --no-link
nix run .#freestanding-gate
# optional freestanding thr measure package (TMPDIR only - never commit thr dumps):
# nix build .#libbeastdb-thr --no-link
# optional if time:
# nix build .#checks.x86_64-linux.bench --no-link
# or product subset wrapper (still omits ffi-smoke / rust gates / freestanding / release / hooks):
# nix run .#test-suite

Recommended before G1.1 (catches packages remote continuous integration / CI builds that test-suite omits - ffi-smoke, release strip + git-policy hooks). Prefer one of:

# Best: same surface as remote CI (G1.2 smoke) - includes ffi-smoke + release + hooks
nix flake check

# Or the extras only (if product smokes already green):
nix build .#checks.x86_64-linux.ffi-smoke --no-link
nix build .#checks.x86_64-linux.beastdb-rust-smoke --no-link
nix build .#checks.x86_64-linux.beastdb-rust-t0 --no-link
nix build .#checks.x86_64-linux.beastdb-rust-t1 --no-link
nix build .#checks.x86_64-linux.beastdb-rust-t2 --no-link
nix build .#libbeastdb --no-link
nix run .#freestanding-gate
nix build .#beastdb-release --no-link
nix build .#checks.x86_64-linux.pre-commit --no-link
nix build .#checks.x86_64-linux.pre-push --no-link
nix build .#checks.x86_64-linux.verify-signatures --no-link

test-suite is intentionally a subset of full land prep; see TESTING.md. Running only product smokes can leave a beastdb-release, ffi-smoke, or hook-package break for the first remote green run.

On other systems, replace x86_64-linux with your flake system (for example aarch64-darwin). Gate map: TESTING.md.

Full-tree staging checklist (G1.1)

Agents must not stage or commit. Before the signed land commit, the human must include all intentional product/docs/tooling so the index cannot ship a partial tree (e.g. submodules without PRIOR-ART, or Lean without docs/G21).

Required paths

# Product Lean (Phases 0-3 + Waves 1-8 + Horizon 1-5 runtime)
git add beastdb/*.lean
# typically: Basic.lean Compact.lean Engine.lean KV.lean Main.lean Manifest.lean
#            Persist.lean PersistIO.lean Routing.lean ShardFile.lean StoreDir.lean Wal.lean

# Foreign C ABI dual-backend (partial ship - export package default + CLI emergency;
# not lmdb.h / LMDB wire; R7 deeper partial). Required for beastdb-lib / ffi-smoke.
git add ffi/include/beastdb.h ffi/src/beastdb_bridge.c
git add ffi/demos/c/main.c ffi/demos/cpp/main.cpp ffi/demos/rust/main.rs
# First-class Rust crate (heed-inspired; links temporary beastdb-lib, not freestanding spine):
# git add ffi/rust/beastdb/   # when residual crate paths are dirty

# Freestanding product library (Systems Lean / packages.libbeastdb - no libleanshared).
# Dual-path honesty: libbeastdb != beastdb-lib. Includes store_env spine, smoke, S0 study tree.
git add freestanding/
# Nix freestanding packages (also covered by nix/ below - listed for visibility):
#   nix/libbeastdb.nix  nix/libbeastdb-thr.nix  nix/freestanding-s0.nix (unwired study)

# Flake / Nix / continuous-integration workflow / toolchain
# (includes G21 host-probe + profile/test apps + G24 deep-measure + beastdb-lib /
#  ffi-smoke + freestanding libbeastdb / thr; flake.lock must pin systems-lean input)
git add flake.nix flake.lock lean-toolchain nix/
git add .github/workflows/ci.yml

# Prior-art submodules + registry + inventory (LMDB, LevelDB, Breccia)
git add .gitmodules ref/lmdb ref/leveldb ref/breccia ref/README.md

# Docs (full set - include TESTING for G21 + LEAN4 freestanding design + MIGRATE-HEED)
git add docs/API.md docs/BENCHMARKS.md docs/PRIOR-ART.md docs/PROOFS.md
git add docs/LIMITS.md docs/VISION.md docs/GAPS.md docs/RELEASE.md
git add docs/SYSTEMS.md docs/LAYOUT.md docs/TESTING.md
git add docs/CONSUME-RUST.md docs/EXPORT-LINK.md
git add docs/HEED-MAP.md docs/PLAN-COMPLETED.md docs/PLAN-REMAINING.md
git add docs/LEAN4.md docs/MIGRATE-HEED.md
# SYSTEMS, G23 layout product path, testing map, host-probe/profiling docs
# Stage intentional untracked deliverables; do NOT add dead/scratch paths
# (e.g. stale ffi/rust/beastdb/src/iter.rs if reintroduced - live RoIter is database.rs).

# Product-facing entry + decisions + rules (AGENTS language rule is G21)
git add README.md release notes (forge / tag) AGENTS.md PLAN.md
# Optional plans (if dirty and intentional): .agents/plans/
# Optional measure drivers (if dirty): bench/

If other intentional first-party files appear in git status, review and add them; do not add host dumps, result*, .lake artifacts, thr dumps under $TMPDIR, host-probe output, or _u8.lean.

Pre-commit checks (human) - index must match working tree

Do not skip this section. Passing only test -f on the working tree is insufficient when paths are MM / AM / ??.

# --- Land-set paths (must be clean: no unstaged diff, no untracked land docs) ---
LAND_PATHS=(
  beastdb
  ffi
  freestanding
  flake.nix flake.lock lean-toolchain nix
  .github/workflows/ci.yml
  .gitmodules ref/lmdb ref/leveldb ref/breccia ref/README.md
  docs/API.md docs/BENCHMARKS.md docs/PRIOR-ART.md docs/PROOFS.md
  docs/LIMITS.md docs/VISION.md docs/GAPS.md docs/RELEASE.md
  docs/SYSTEMS.md docs/LAYOUT.md docs/TESTING.md
  docs/CONSUME-RUST.md docs/EXPORT-LINK.md
  docs/HEED-MAP.md docs/PLAN-COMPLETED.md docs/PLAN-REMAINING.md
  docs/LEAN4.md docs/MIGRATE-HEED.md
  README.md release notes (forge / tag) AGENTS.md PLAN.md
)

# 0) Scratch must not be staged
! git ls-files --error-unmatch _u8.lean 2>/dev/null
test ! -f _u8.lean

# 1) SYSTEMS + TESTING + freestanding design docs must be tracked (not ??)
test -f docs/SYSTEMS.md && test -f docs/TESTING.md && test -f docs/LEAN4.md
git ls-files --error-unmatch docs/SYSTEMS.md
git ls-files --error-unmatch docs/TESTING.md
git ls-files --error-unmatch docs/LEAN4.md
git ls-files --error-unmatch freestanding/README.md
git ls-files --error-unmatch nix/libbeastdb.nix
git ls-files --error-unmatch nix/libbeastdb-thr.nix

# 2) No unstaged working-tree changes on land-set paths (MM / unstaged half of AM)
#    Empty output required. If non-empty: re-run the Required paths git add block.
#    Classic freestanding hazard: MM on freestanding/* / nix/libbeastdb*.nix
#    or AM on freestanding/store_env.c - restage before commit.
git diff --name-only -- "${LAND_PATHS[@]}"
test -z "$(git diff --name-only -- "${LAND_PATHS[@]}")"

# 3) No untracked files that belong in the land set
#    Empty output required for SYSTEMS/TESTING/freestanding and other docs listed above.
git status --porcelain -- "${LAND_PATHS[@]}"
# Expect: only lines starting with A / M / R in the index column, no "??" lines.
# If any line is "?? ..." or " M ..." / "MM ..." / "AM ...": re-add those paths before commit.

# 4) Staged GAPS/RELEASE must describe the full core land (not an early-wave-only slice)
#    Positive checks (must match):
git show :docs/GAPS.md | rg -n 'Phases 0-3 \+ Waves 0-9 \+ G11\.4'
git show :docs/GAPS.md | rg -n 'G11\.4'
git show :docs/GAPS.md | rg -n 'G13|G20|G21|G24'
git show :docs/GAPS.md | rg -n 'G1\.1 \| open'
git show :docs/GAPS.md | rg -n 'G21 \| closed'
git show :docs/GAPS.md | rg -n 'G22 \| closed'
git show :docs/GAPS.md | rg -n 'G23 \| closed'
git show :docs/GAPS.md | rg -n 'G24 \| closed'
git show :docs/GAPS.md | rg -n 'R7-RT|freestanding|libbeastdb'
git show :docs/RELEASE.md | rg -n 'Phases 0-3 \+ Waves 0-9'
git show :docs/RELEASE.md | rg -n 'ref/breccia'
git show :docs/RELEASE.md | rg -n 'SYSTEMS'
git show :docs/RELEASE.md | rg -n 'host-probe|G21'
git show :docs/RELEASE.md | rg -n 'mwmr-smoke|layout-smoke'
git show :docs/RELEASE.md | rg -n 'deep-cpu|G24'
git show :docs/RELEASE.md | rg -n 'docs/TESTING\.md'
git show :docs/RELEASE.md | rg -n 'Index must match working tree|index must match'
git show :docs/RELEASE.md | rg -n 'freestanding|libbeastdb'
git show :docs/RELEASE.md | rg -n 'packages\.libbeastdb|packages\.beastdb-lib'
# Dual-package honesty on staged docs (not aliases) - hard-require LIMITS Embed TCB:
git show :docs/LIMITS.md | rg -n 'libbeastdb|Embed TCB|R7-RT'
git show :flake.lock | rg -n 'systems-lean'
# Negative checks (must be empty - stale early-wave land targets must not remain).
# Do not embed the forbidden literals in comments in this file: the gate greps the
# whole staged blob. Forbidden as a land target (not as prose about avoiding it):
#   early-wave-only tree phrasing; land-core hygiene tag subjects from that slice.
! git show :docs/GAPS.md | rg -n 'Waves 0-1 tree|Phases 0-3 \+ Waves 0-1'
! git show :docs/RELEASE.md | rg -n 'Phases 0-3 \+ Waves 0-1|Waves 0-1 \(land-core'
# Staged PRIOR-ART must include Breccia; staged GAPS must not lack G11.4
git show :docs/PRIOR-ART.md | rg -n -i 'Breccia'
git show :docs/GAPS.md | rg -n 'G11\.4'
# Staged TESTING present (G21)
git show :docs/TESTING.md | rg -n 'host-probe|flake check'

# 5) Existence + submodule pins + freestanding tree
test -f docs/PRIOR-ART.md && test -f docs/SYSTEMS.md && test -f docs/TESTING.md
test -f docs/LEAN4.md && test -f freestanding/README.md
test -f nix/libbeastdb.nix && test -f nix/libbeastdb-thr.nix
test -f .gitmodules
test -f ref/breccia/DESIGN.md
git submodule status
# expect:
#   1845f81e... ref/breccia
#   7ee830d0... ref/leveldb
#   704dc702... ref/lmdb

# 6) Review staged surface
git status
git diff --cached --stat
git diff --cached -- docs/GAPS.md docs/RELEASE.md freestanding/ nix/libbeastdb.nix | head -160

# 7) productSrc / namecheck still exclude ref/ (no Lean import of ref/)
rg -n 'import .*ref' beastdb/ || true   # should be empty of ref paths

Stop and re-stage if any of (0)-(4) fails. Classic failure: ref/breccia gitlink staged while staged docs/GAPS.md / docs/PRIOR-ART.md still lack G11.4 / Breccia prose, or docs/SYSTEMS.md / docs/TESTING.md still ??, or _u8.lean still staged.

Do not commit only .gitmodules + ref/* without docs/PRIOR-ART.md, docs/SYSTEMS.md, docs/TESTING.md, closed G11/G13-G21 rows, and the product Lean tree. Review the full index before signing.

Workstream H - agent vs human (publish residual)

Track 1 / Track B (publish) is human-owned end-to-end. Agents may refresh this checklist, re-run local gates, inventory readiness, and draft the handoff; they must not git add (unless the human already asked), git commit, git tag, or git push. Leave G1.1, G1.2, G1.3, G1.5, G1.6 open in GAPS until each human step below is actually done.

Step Owner Maps to Done when
Agent land prep agent - Tree green; RELEASE/GAPS accurate; freestanding in LAND_PATHS; G1 rows still open; handoff drafted (this section + gates above)
H1 human G1.1 Signed commit covers full land set (incl. ffi/ + freestanding/ dual package); index ≡ working tree
H2 human G1.3 Signed tag v0.1.0-core (subject G21-G24 + freestanding dual-path honesty); git verify-tag
H3 human G1.2 Push commit then tag with hooks; remote continuous integration (CI) green
H4 human G1.5 Forge: require signed commits on default branch
(with H2 or after) human G1.6 forge release notes for v0.1.0-core cut + forge release notes

Authoritative order for land is Ordered human steps 4-8 below (commit -> tag -> push -> forge -> forge release notes). H1-H4 map to ordered steps 4-7 (G1.1, G1.3, G1.2, G1.5). G1.6 is ordered step 8 (may run with the tag / H2 or after forge). Together, H1-H4 + G1.6 = steps 4-8.

Agents stop before the signed commit. Agents never run git commit, git tag, or git push. Prefer not staging; use the Required paths git add block in Full-tree staging checklist above when the human stages.

Ordered human steps after gates are green

Do these in order when the full product land is not yet on HEAD. Agents stop before the human G1.1 signed commit (Ordered step 4). They must not git commit, git tag, or git push, and should prefer not to git add unless the human already asked.

Mandatory: If git status shows MM / AM / ?? on any LAND_PATHS path, do not commit. Re-run the Required paths git add block first. Agents never stage; a correct working tree with a stale index ships a wrong land. Freestanding residual often shows MM / AM on freestanding/* and nix/libbeastdb*.nix - restage those before signing.

  1. Review working tree - git status / git diff; confirm no secrets, no host dumps, no thr/host-probe dumps, no _u8.lean, product name lowercase; dual-package names remain libbeastdb vs beastdb-lib (not aliases).
  2. Stage full land set - Required paths block above (not a partial wave; include freestanding/ + nix/libbeastdb*.nix + docs/LEAN4.md when dirty).
  3. Index ≡ working tree - every pre-commit check (0)-(7) passes.
  4. G1.1 - Signed commit - message below (or residual follow-up draft if core already on HEAD); git verify-commit HEAD; nix run .#verify-signatures.
  5. G1.3 - Signed tag v0.1.0-core - annotation below; git verify-tag.
  6. G1.2 - Push - ensure a forge remote is configured (see G1.2), then git push origin HEAD and git push origin v0.1.0-core; confirm remote continuous-integration (CI) / nix flake check green (smoke).
  7. G1.5 - Forge - default branch Require signed commits.
  8. G1.6 - forge release notes - move [Unreleased] land body under [0.1.0-core] - YYYY-MM-DD; publish forge release notes; then close G1 inventory rows with a follow-up signed commit (see Post-publish inventory recipe below).

Until 4-8 are done and inventory rows are flipped in a signed follow-up, G1.1-G1.3 / G1.5 / G1.6 stay open in GAPS. The land commit itself must still contain G1.1 | open (pre-commit greps require that honesty). Do not mark R7-RT closed when tagging - freestanding land != Embed TCB close.

When core product land is already on HEAD (do not re-land Lean core)

If a human GPG-signed commit already contains the bulk product + ffi/ + early freestanding path set (example: tip with product Lean, flake, CI, prior-art pins, ffi/, and freestanding Phase 1-3 packaging - check with git ls-tree), do not re-stage every Lean module or re-apply the full v0.1.0-core product land commit message as if the core tree were still uncommitted.

Important (R15 land-set honesty): today's Required paths / LAND_PATHS include ffi/ and freestanding/. A tip without either is not the full land set and does not close G1.1 by itself. Confirm:

git ls-tree -r HEAD --name-only | rg '^ffi/'          # empty ⇒ ffi residual required
git ls-tree -r HEAD --name-only | rg '^freestanding/' # empty ⇒ freestanding residual required
git ls-tree -r HEAD --name-only | rg 'nix/libbeastdb' # empty ⇒ freestanding nix residual
rg -n 'systems-lean' flake.lock                       # missing ⇒ freestanding toolchain residual

Residual path instead (typical when freestanding Track A / docs are dirty):

  1. Confirm: git verify-commit HEAD; nix run .#verify-signatures; G1 human rows still open on that tip.
  2. Stage remaining intentional residual paths - at minimum dirty freestanding/** (incl. store_env.c, smoke, README, Extract), nix/libbeastdb.nix, nix/libbeastdb-thr.nix, freestanding docs honesty (docs/LIMITS.md, docs/LEAN4.md, docs/GAPS.md, docs/BENCHMARKS.md, docs/PLAN-REMAINING.md, docs/RELEASE.md, release notes (forge / tag)) when dirty; plus any still-dirty ffi/** / product Lean. Signed follow-up commit(s) - keep G1 rows open. Prefer the freestanding residual commit message draft below over replaying the full first-core message.
  3. Re-check index ≡ working tree for full Required paths / LAND_PATHS (including ffi + freestanding); prefer nix flake check + nix run .#freestanding-gate before tag.
  4. Continue from ordered steps 5-8 (tag -> push with remote configured -> forge -> forge release notes + inventory follow-up).
  5. Flip G1.1 -> closed only after the human accepts the signed land tip as meeting G1.1 including foreign C ABI dual-backend and freestanding dual package (post-publish inventory recipe) - agents never flip it.

See GAPS.md Workstream H for the current clone's residual list.

G1.1 - Signed commit(s) of the landed tree

  1. Review git status / git diff (agent work is uncommitted until you act).
  2. Stage intentional paths only (git add ...) using the Full-tree staging checklist above.
  3. Pass every pre-commit check in the section above (index ≡ working tree for land set).
  4. Create a GPG-signed commit (hooks set commit.gpgsign=true after install-hooks).

Agents stop here. Do not create the commit for the human.

Suggested commit message (full first core land)

Use this when the entire v0.1.0-core tree is still uncommitted. If core + ffi/ + early freestanding are already on a signed tip and only freestanding Track A / docs residual is dirty, prefer the residual follow-up draft below.

Prefer this plain public message (inventory detail stays in GAPS / below if needed):

beastdb v0.1.0-core: durable store, freestanding libbeastdb, foreign bindings

First publishable core line:

- Multi-file durable key-value store (Lean 4 + Nix): put/get/sync, compaction,
  single-writer multi-reader sessions, multi-writer puts on disjoint leaves,
  generation-fenced structural ops, optional single-file layout
- Freestanding product library: packages.libbeastdb (no Lean managed runtime);
  temporary packages.beastdb-lib for full C ABI demos/YCSB/Rust (not freestanding)
- Foreign C/Rust bindings under ffi/; flake checks and measure suite
- Honest limits: not LMDB wire; freestanding multi-file depth still open;
  cooperative crash tests only (not power-fail); production crypto deferred

Human residual after this commit: push/smoke, signed tag, forge signed-commits
policy, forge release notes (see G1 steps in this file / GAPS).

Maintainer inventory dump (optional; do not put this wall on the GitHub release title). Gap IDs map to GAPS.md:

beastdb v0.1.0-core (maintainer inventory cross-links)

Phases 0-3, waves 0-9, horizons 1-5 closed with honesty; G21-G24; freestanding
dual-path; R7 deeper partial; R7-RT open; mwmr-smoke; layout-smoke; ffi dual-backend
export default. Full residual board: docs/GAPS.md.

git commit -m "$(cat <<'EOF'
beastdb v0.1.0-core: durable store, freestanding libbeastdb, foreign bindings

First publishable core line:

- Multi-file durable key-value store (Lean 4 + Nix): put/get/sync, compaction,
  single-writer multi-reader sessions, multi-writer puts on disjoint leaves,
  generation-fenced structural ops, optional single-file layout
- Freestanding product library: packages.libbeastdb (no Lean managed runtime);
  temporary packages.beastdb-lib for full C ABI demos/YCSB/Rust (not freestanding)
- Foreign C/Rust bindings under ffi/; flake checks and measure suite
- Honest limits: not LMDB wire; freestanding multi-file depth still open;
  cooperative crash tests only (not power-fail); production crypto deferred

Human residual after this commit: push/smoke, signed tag, forge signed-commits
policy, forge release notes (G1 steps in docs/RELEASE.md / docs/GAPS.md).
EOF
)"
# Prefer an explicit signed commit if unsure:
# git commit -S -m "..."

Suggested residual follow-up commit (when core already on HEAD)

Typical current residual: freestanding Track A depth + docs honesty + G1 readiness package (RELEASE/PLAN-REMAINING). Do not invent R7-RT closed. Keep G1 rows open. Agents stop before this commit.

beastdb: freestanding Track A depth + G1 land readiness (R7-RT open)

Land freestanding residual for packages.libbeastdb (Systems Lean; no
libleanshared): store_env append-log spine with live get index (S-A1), delete
tombstone (S-A2), read-side mmap get (S-A3), dir/DATA layout (S-A4a); smoke and
nix/libbeastdb.nix + libbeastdb-thr wiring; docs honesty (LIMITS Embed TCB,
LEAN4, GAPS R7-RT, BENCHMARKS, PLAN-REMAINING, RELEASE LAND_PATHS).

Dual-package honesty: packages.libbeastdb = freestanding product library;
packages.beastdb-lib = temporary export+runtime residual for full C ABI v9 /
demos / YCSB / Rust - not an alias. Host CLI/proofs stay lean4-nix packages.beastdb.

Does not close R7-RT (not multi-file MANIFEST/MWMR v9; not C5 Embed TCB close).
Does not flip GAPS G1.1-G1.3 / G1.5 / G1.6 closed (post-publish inventory recipe
only - leave rows open in this land commit). This residual signed commit *is*
the G1.1 land action when core is already on HEAD; inventory flip is later only.

Human residual after this commit: G1.3 tag v0.1.0-core, G1.2 push/CI smoke,
G1.5 forge require-signed-commits, G1.6 forge release notes (then inventory follow-up).

# After Required paths restage so no MM/AM/?? on LAND_PATHS:
git commit -m "$(cat <<'EOF'
beastdb: freestanding Track A depth + G1 land readiness (R7-RT open)

Land freestanding residual for packages.libbeastdb (Systems Lean; no
libleanshared): store_env append-log spine with live get index (S-A1), delete
tombstone (S-A2), read-side mmap get (S-A3), dir/DATA layout (S-A4a); smoke and
nix/libbeastdb.nix + libbeastdb-thr wiring; docs honesty (LIMITS Embed TCB,
LEAN4, GAPS R7-RT, BENCHMARKS, PLAN-REMAINING, RELEASE LAND_PATHS).

Dual-package honesty: packages.libbeastdb = freestanding product library;
packages.beastdb-lib = temporary export+runtime residual for full C ABI v9 /
demos / YCSB / Rust - not an alias. Host CLI/proofs stay lean4-nix packages.beastdb.

Does not close R7-RT (not multi-file MANIFEST/MWMR v9; not C5 Embed TCB close).
Does not flip GAPS G1.1-G1.3 / G1.5 / G1.6 closed (post-publish inventory recipe
only - leave rows open in this land commit). This residual signed commit *is*
the G1.1 land action when core is already on HEAD; inventory flip is later only.

Human residual after this commit: G1.3 tag v0.1.0-core, G1.2 push/CI smoke,
G1.5 forge require-signed-commits, G1.6 forge release notes (then inventory follow-up).
EOF
)"
# Immediate post-commit verify (not a separate "G1.1 residual" commit):
git verify-commit HEAD
nix run .#verify-signatures
  1. Verify:
nix run .#verify-signatures
git verify-commit HEAD

Do not use --no-gpg-sign or push unsigned history.

G1.3 - Version tag

Suggested first core tag: v0.1.0-core (annotated + signed). Do not invent the tag as done until the human creates it.

Suggested tag annotation

Public subject (use this on the tag and forge release title):

beastdb v0.1.0-core: durable store, freestanding libbeastdb, foreign bindings

beastdb v0.1.0-core: durable store, freestanding libbeastdb, foreign bindings

Multi-file durable key-value store (Lean 4 + Nix): put/get/sync, compaction,
single-writer multi-reader sessions, multi-writer puts on disjoint leaves,
generation-fenced structural ops, optional single-file layout.

Freestanding product library packages.libbeastdb (no Lean managed runtime).
Temporary packages.beastdb-lib for full C ABI demos/YCSB/Rust (not freestanding;
not an alias). Foreign bindings under ffi/. Flake checks + measure suite.

Honesty: not LMDB wire; freestanding multi-file depth still open; cooperative
crash tests only (not power-fail); production crypto deferred; checksum is not
authentication. See docs/LIMITS.md and docs/GAPS.md.

git tag -s v0.1.0-core -m "beastdb v0.1.0-core: durable store, freestanding libbeastdb, foreign bindings

Multi-file durable key-value store (Lean 4 + Nix): put/get/sync, compaction,
single-writer multi-reader sessions, multi-writer puts on disjoint leaves,
generation-fenced structural ops, optional single-file layout.

Freestanding product library packages.libbeastdb (no Lean managed runtime).
Temporary packages.beastdb-lib for full C ABI demos/YCSB/Rust (not freestanding;
not an alias). Foreign bindings under ffi/. Flake checks + measure suite.

Honesty: not LMDB wire; freestanding multi-file depth still open; cooperative
crash tests only (not power-fail); production crypto deferred; checksum is not
authentication. See docs/LIMITS.md and docs/GAPS.md."
git verify-tag v0.1.0-core

Local config after install-hooks includes tag.gpgsign=true; -s is still explicit and preferred.

G1.2 - Push

Remote required. Some clones (including local-only agent worktrees) have no git remote yet. Before push:

git remote -v
# If empty, add the forge remote (name is usually origin):
# git remote add origin <your-forge-url>
# Or substitute your remote name for origin in the push commands below.
git push origin HEAD
git push origin v0.1.0-core
  • Pre-push runs git verify-commit on every commit in the push range and aborts if any signature is missing or invalid.
  • Forbidden as normal workflow: git push --no-verify.
  • Post-push smoke (still G1.2, not a reopened G1.4): confirm the remote ci / nix flake check job is green on the pushed tip. G1.4 already closed when the workflow landed in-tree.

G1.5 - Require signed commits on the default branch

On the hosting forge (e.g. GitHub), for the default branch protection rule:

  1. Open the repository Settings -> Branches (or Rulesets).
  2. Add or edit protection for main (or your default branch).
  3. Enable Require signed commits (or the forge's equivalent).
  4. Prefer also: require status checks to pass - select the ci / nix flake check job once it has run at least once.
  5. Optionally enable server-side "require linear history" / "no force push" for defense in depth.

Exact UI labels vary by host; the invariant is: unsigned commits must not land on the default branch.

Agents cannot enable forge settings; a human with admin rights must.

G1.6 - Publish forge release notes

  1. In [release notes (forge / tag)](../release notes (forge / tag)), move the landed material under a new section:

    ## [0.1.0-core] - YYYY-MM-DD

    Keep ## [Unreleased] for subsequent work (empty or with post-tag deltas only).

    Guidance: fold the entire pre-tag [Unreleased] body (Waves 0-9 + Horizons + G21 + post-wave foundation bullets) under [0.1.0-core]. Do not invent a shipped date before the tag exists; fill YYYY-MM-DD at tag time only.

  2. Align the GitHub (or forge) Release body with that section (copy bullets; link the tag).

  3. Mention durability limits honestly (LIMITS.md) - checksum != auth; fsync helper optional; cooperative locks not kernel leases; multi-writer multi-reader put on disjoint leaves only (G22); structural publish generation-fenced with short cooperative exclusive (Track 3).

  4. Point at gap inventory: GAPS.md (G13-G24 closed in tree with honesty; G24 deep measure / Workstream L local-only - not CI / not product ASan clean / not LMDB parity; do not reopen G21; G17 scalar + Workstream I measured residual; F2 closed sequential on purpose / F3 deferred; Workstream J / Track 3 structural closed with short-LOCK honesty; R7-RT open freestanding dual-path; flip human G1.x to closed only after the matching publish action, via the Post-publish inventory recipe).

  5. Freestanding dual-package bullets (required in forge notes):

    • packages.libbeastdb - freestanding Systems Lean library (no libleanshared)
    • packages.beastdb-lib - temporary export+runtime residual (full C ABI v9) - not an alias
    • R7-RT still open - land does not close Embed TCB
    • Summarize freestanding land (Phase 1-5 + Track A) in release notes into [0.1.0-core] at tag time; keep post-tag deltas only under new Unreleased

Draft forge release-notes skeleton (human fills date at tag)

## beastdb v0.1.0-core

First publishable **core** line: durable multi-file store + freestanding libbeastdb + foreign bindings (maintainer inventory: Phases 0-3, waves 0-9, horizons 1-5, G21-G24)
+ foreign C ABI dual-backend (deeper partial) + freestanding dual-path library.

### Highlights
- Verified multi-shard engine, multi-file MANIFEST/WAL, SWMR + MWMR put on
  disjoint leaves, structural generation fence, crash-suite cooperative depth
- Foreign bindings: `ffi/` + `packages.beastdb-lib` (export+runtime; C ABI v9)
- Freestanding: `packages.libbeastdb` (Systems Lean spine; no libleanshared)
- Measure: G24 deep suite, thr A/B, YCSB-C on temporary export path

### Honesty / non-claims
- Not LMDB wire / `lmdb.h` / page ACID
- Cooperative crash only - not hardware power-fail; kill-mid-write not CI
- **R7-RT open** - freestanding spine != multi-file product v9 Embed TCB close
- Dual package: `libbeastdb` != `beastdb-lib`

See forge release notes for v0.1.0-core, docs/LIMITS.md, docs/GAPS.md.

Post-publish inventory recipe (close G1 rows; signed follow-up)

The land commit (G1.1) must still show human G1 rows as open so pre-commit land greps stay honest. After each publish action exists (or once at the end), record closures with a separate GPG-signed commit - do not reopen product land scope or restage the full tree unless those files also changed.

When to flip which row

After this action exists Set in docs/GAPS.md
Signed land commit on the full tree G1.1 | closed
Signed tag v0.1.0-core G1.3 | closed
Push + remote CI smoke green G1.2 | closed
Forge require-signed-commits on default branch G1.5 | closed
forge release notes for v0.1.0-core cut + forge release notes G1.6 | closed

Recipe (batch at end is fine; one commit per step is also fine):

# 1) Edit docs only - GAPS status table (G1.6).
#    Keep product Lean / flake out of this follow-up unless they truly changed.

# 2) Stage inventory + notes only
git add docs/GAPS.md release notes (forge / tag)
# if RELEASE/README/VISION mention G1 open/closed language, include those too:
# git add docs/RELEASE.md docs/VISION.md README.md

# 3) Index clean for those paths
git diff --name-only -- docs/GAPS.md release notes (forge / tag)
test -z "$(git diff --name-only -- docs/GAPS.md release notes (forge / tag))"

# 4) GPG-signed follow-up (hooks: commit.gpgsign)
git commit -m "$(cat <<'EOF'
docs: close human G1 publish residuals for v0.1.0-core

Record G1.1-G1.3 / G1.5 / G1.6 closed after signed land, tag, push/CI smoke,
forge require-signed-commits, and forge release notes for v0.1.0-core cut. No product
algorithm change.
EOF
)"

git verify-commit HEAD
nix run .#verify-signatures

# 5) Push the follow-up (same remote rules as G1.2)
git push origin HEAD

Do not mark any G1 human row closed until the corresponding action is real. Agents never perform this recipe.

Post-release verification

nix run .#verify-signatures          # full HEAD history
git verify-tag v0.1.0-core
# After push: confirm green "ci / nix flake check" (G1.2 smoke; G1.4 already closed)

What this tag covers (scope)

Area In v0.1.0-core tree
Phases 0-3 Bootstrap, sharding core, compact/reconcile, persistence + extract
Wave 0 Continuous integration (CI), PROOFS, RELEASE, VISION production framing (G1.4, G11.3, G12.2)
Wave 1 Disk trust: fsync helper, Fowler-Noll-Vo (FNV) v2, strict logs-respect-routing (LRR), lock (G2, G3.3-G3.5)
Wave 2 Multi-file MANIFEST/shards/write-ahead log (WAL) (G3.1-G3.2, G4.4)
Wave 3 Multi-level compaction (G4.1-G4.3)
Wave 4 Split lifecycle / hybrid consistency (G5)
Wave 5 Product API & CLI (G8)
Wave 6 Single-writer multi-reader (SWMR) concurrency (G6); not multi-writer multi-reader (MWMR)
Wave 7 Bench + resource bounds (G7, G10)
Wave 8 Experimental compress/MAC/encrypt models (G9) - deferred for production
Wave 9 Prior art LMDB + LevelDB (G11.1-G11.3)
G11.4 ref/breccia + PRIOR-ART Breccia section
SYSTEMS Ahead-of-time (AOT) product rule, fail closed, assumptions register
Horizon 1 G13 crash-suite + swmr-smoke; G14 get-path/cost (closed in tree; LAYOUT design history only - product single-file path is G23). Track 4 + Tier D: deeper cooperative simulated windows (production temps, compact-on-publish, mid-checkpoint residual); not CI kill -9 mid-write (D1) / power-fail (D2) - residual in LIMITS.md + human offline recipe TESTING.md
Horizon 2 G15 pure L3 Msg; G16 L2 ForkJoin + pure Mwmr; Resource affine start (closed)
Horizon 3 G17 L1 portable scalar Bulk (closed)
Workstream I Optional ISA / single instruction multiple data (SIMD) measure (closed measured residual: keep scalar; no product vector path)
Horizon 4 G18 linear/affine resource encodings (closed with honesty; not language linear types)
Horizon 5 G19 experimental EtM export composition + G20 systems methodology (closed G19/G20; production crypto deferred)
G21 measure-and-real host-probe package/check; profile-cpu / profile-mem; test-suite app; TESTING.md; BENCHMARKS/SYSTEMS profiling; AGENTS language rule (closed in tree)
G22 MWMR put multi-process multi-writer product put on disjoint leaves; per-leaf WAL + lock; mwmr-smoke (closed)
G23 layout single-file beastdbI pure codec + product single-file path + migrate; layout-smoke (closed)
G24 deep measure / Workstream L deep-cpu / deep-mem / deep-rr / value-assess / asan-smoke (+ optional Phase B CLI asan); soft-degrade tools vs fail-closed product/sanitizer; artifacts under TMPDIR; local only - not in test-suite / default flake checks; not product ASan clean; not LMDB parity; does not reopen G21 (closed)
Freestanding dual package (R7-RT open) packages.libbeastdb: Systems Lean freestanding spine (freestanding/, nix/libbeastdb.nix, thr nix/libbeastdb-thr.nix, systems-lean in flake.lock, freestanding-gate) - no libleanshared. Track A depth: live get index / delete tombstone / read-side mmap get / dir DATA. packages.beastdb-lib: temporary export+runtime residual for full C ABI v9 / demos / YCSB / Rust - not an alias. Phase 5 packaging/docs promote != C5 Embed TCB close; R7-RT remains open
Workstream F1 Product multi-shard compact schedule ≡ pure ForkJoin.leafSchedule; sequential durable IO (closed)
Workstream F2 Multi-shard compact wall - closed (measured residual - sequential on purpose) after Track 2 + Next-2 / R2 1-vs-N (~1.0); no greppable Task multi-core path; BENCHMARKS recipe
Workstream J / Track 3 Pure beastdb.Structural + product generation-fenced multi-process structural (struct-smoke) (closed product slice + pure model; short cooperative LOCK required - Next-4 / R3 residual honesty)
Open residual L3 worker pool (F3 / R18 deferred - soft reopen only after architecture decision; no distributed-DB claim); large-N get residual: partial win Next-1 + R1 put-maintain (Plan Step 3: distinct-key multi-put get closed measured win - no further redesign; overwrite accepted residual / compact discipline ~O(N²) until compact; no O(1)/mmap); free-copy pre-close residual (Tier A / Next-5 / R6 honesty); single-file put durability / no single-file MWMR partial (Next-5 / R8); classifyIO substring algebra audited residual (Next-5 / R16); lock-free dual MANIFEST publishers (Next-4 / R3 settled: short LOCK required; dual-publisher north-star deferred pending SYSTEMS §4 P1-P6 + soft reopen - not shipped; not abandoned); foreign C ABI depth deeper partial (ffi/ + beastdb-lib / ffi-smoke dual-backend: export package default; CLI emergency BEASTDB_USE_CLI=1 full v9 same-process export (cursor + multi-key atomic batch + reverse/range/first-last/neighbor + D1 len/clear/delete_range); not lmdb.h / LMDB wire / LMDB page ACID; R7 deeper partial); R7-RT systems embed open (freestanding packages.libbeastdb spine + Track A partial depth landed; multi-file freestanding / full Embed TCB hard reqs not met - Phase 5 packaging != C5 close); kernel multi-writer leases deferred (C2 cooperative trust); linearizability deferred (C3); Tier D / Next-6 assurance residuals: kill-mid-write under CI (R9 not claimed / cooperative-only; soft reopen only with hermetic stable CI + fixtures; never flaky kill-9 gate; human offline recipe in TESTING.md); hardware power-fail (R10 not claimed; soft reopen only with lab instrumentation + honesty; never marketing); NIST crypto (R11 deferred product decision - soft reopen only after product decision + real algorithms + key management + fail-closed defaults); libzstd/ratio (R12 deferred - soft reopen only if storage size is real operator pain + stack-legal boundary); human G1.1-G1.3 / G1.5 / G1.6. Shipped closed (not residual): F2 sequential-on-purpose measured residual; Workstream I / R13 product SIMD closed measured residual (scalar Bulk; soft reopen only if Bulk hotspot + legal path without forbidden product C); G24 deep measure / Workstream L (local-only suite; not CI; not product ASan clean; not LMDB parity; do not reopen G21); lock-efficiency pure + SYSTEMS budget. Full list: GAPS.md

Status after human completes this doc

Gap When closed Who
G1.1 Signed commit(s) of the full Phases 0-3 + Waves 0-9 + G11.4 + SYSTEMS + Horizon 1-5 + G21-G24 + Workstreams D-G / F1 / I / J pure-model residual tree + foreign C ABI dual-backend (ffi/ + checks.ffi-smoke; R7 deeper partial) + freestanding dual package (freestanding/ + nix/libbeastdb*.nix + systems-lean lock; packages.libbeastdb != packages.beastdb-lib; R7-RT still open) exist (pre-ffi/ or pre-freestanding tip alone is not enough) human
G1.2 Push succeeded with hooks; signatures verify; remote CI smoke green human
G1.3 Tag v0.1.0-core (or chosen name) exists and is signed human
G1.4 Already closed: in-tree .github/workflows/ci.yml runs nix flake check agent (Wave 0)
G1.5 Default branch requires signed commits human
G1.6 Forge release notes published human

Until G1.1-G1.3, G1.5, and G1.6 are done, leave those rows open in GAPS.md. Do not reopen G1.4 for the first remote green run - that verify lives under G1.2. Do not claim "G1 closed" while any of those human rows remain open.