docs: settle the storage engine and proof retention window

ARCHITECTURE.md

@@ -164,9 +164,12 @@ upstream Lean library name per Rust's `-sys` convention.
 **Thin glue over existing libraries**
 
 - `verity-p2p` — gossip and req/resp over libp2p.
-- `verity-crypto` — adapter over leanMultisig (XMSS verify / sign / aggregate).
-- `verity-db` — persistence (Repository): blocks, states, and the finalized anchor, over an
-  embedded key-value store. Keeps the storage concern out of the single-writer aggregate coordinator.
+- `verity-crypto` — adapter over the two upstream signature libraries: [`leansig`](https://github.com/leanEthereum/leanSig)
+  for per-validator XMSS sign / verify, and [`leanMultisig`](https://github.com/leanEthereum/leanMultisig)
+  for aggregation and aggregate-proof verification. One capability contract, two suppliers behind it.
+- `verity-db` — persistence (Repository): blocks, states, aggregate proofs, and the finalized anchor.
+  Keeps the storage concern out of the single-writer aggregate coordinator. See
+  [Storage engine and retention](#storage-engine-and-retention).
 - `verity-rpc` — HTTP API surface.
 - `verity-metrics` — implementation of the leanMetrics contract.
 
@@ -211,6 +214,42 @@ flowchart TB
     DB --> TYPES
 ```
 
+### Storage engine and retention
+
+`verity-db` stores two workloads with opposite shapes, and the split drives every decision below.
+Sizes are measured from leanSpec's `fixtures-prod-scheme.tar.gz` release asset; at
+`SECONDS_PER_SLOT = 4` a day is 21,600 slots.
+
+| Workload | Value size | Volume | Lifetime |
+|---|---|---|---|
+| Blocks, states, indices, finalized anchor | ~100 B – 800 B | ~5 MB/day | permanent |
+| Aggregate proofs (`MultiMessageAggregate`) | 155–236 KB, median 190 KB | ~4.1 GB/day | pruned after ~1 day |
+
+**Engine: RocksDB.** The proof workload — six-figure-byte values written continuously and dropped
+en masse a day later — is what an LSM tree with range tombstones is built for, and the same choice
+is what ethlambda, zeam, and qlean-mini run (gean uses Pebble, the same family). The cost is a C++
+dependency in the runtime's build and trust surface; that cost is accepted for Runtime Shell, where
+the bar is memory-safe, panic-free Rust around a well-exercised store, not proof. It buys nothing in
+Verified Core and reaches nothing there.
+
+**Backend trait.** Storage sits behind a backend trait with an in-memory implementation alongside
+the RocksDB one, following ethlambda's `StorageBackend` split. Tests and ephemeral nodes run
+in-memory; the engine stays replaceable if the proof workload later moves out of the database.
+Anything that leaks one engine's semantics into the trait — range deletes above all — is documented
+at the trait, not assumed.
+
+**Proof retention: 21,600 slots (~1 day).** Proofs live in their own table keyed `slot ‖ root`, so
+pruning is a slot-ordered range delete rather than a scan. They are dropped only below
+`tip_slot − 21,600` and only when that cutoff is already finalized; non-finalized proofs are never
+touched. Blocks and states are never pruned by this path.
+
+The floor is not ours to choose: leanSpec sets `MIN_SLOTS_FOR_BLOCK_REQUESTS = 3600` (4 hours) and
+a responder **MUST** serve `BlocksByRange` over that window. Everything above it is an operational
+choice about how far behind a peer can fall and still catch up over P2P instead of needing a
+checkpoint. One day is that horizon — a node down overnight rejoins by range sync — at 6× the
+mandated floor. Note that leanSpec's own reference node satisfies the requirement in memory and
+persists no proofs at all; Verity persists them so the guarantee survives a restart.
+
 ### Capability contracts
 
 The Verified Core ↔ Runtime Shell boundary is expressed not as a fixed list of FFI functions but as a small set of **capability

CLAUDE.md

@@ -18,9 +18,14 @@ Owner-ratified ground rules for the first Rust code. Do not re-open these withou
 - **Goal**: a full node from the start (networking included), not a fixtures-passing library. leanSpec fixture conformance is still the CI backbone.
 - **Crates**: start with a single `verity-consensus` crate (no chain/validator split). Proposer selection lives chain-side as a pure function next to STF/fork choice. Shared types stay a module until a second crate exists.
 - **Dependencies**:
-  - XMSS: [`leansig`](https://github.com/leanEthereum/leanSig) as a git dependency, **rev-pinned** (not branch-tracked).
+  - XMSS: [`leansig`](https://github.com/leanEthereum/leanSig) as a git dependency, **rev-pinned** (not branch-tracked), for per-validator sign / verify. Aggregation and aggregate-proof verification come from [`leanMultisig`](https://github.com/leanEthereum/leanMultisig) — both sit behind `verity-crypto`'s one capability contract, so a doc naming only one of them is incomplete, not contradictory.
   - SSZ: `libssz` 0.2.2 (lambdaclass). [NyxFoundation/leanSSZ](https://github.com/NyxFoundation/leanSSZ) (proven Lean SSZ, C ABI PoC complete) is deliberately NOT adopted initially — it is the future Lean-adoption candidate for SSZ.
   - Networking: upstream `rust-libp2p` (QUIC, gossipsub, reqresp). Fork only if a concrete need materializes, as lambdaclass did for ethlambda.
+  - Storage: **RocksDB** behind a backend trait with an in-memory sibling implementation (ethlambda's `StorageBackend` split). Decided 2026-08-10 — see **Storage** below.
+- **Storage** (2026-08-10): aggregate proofs are persisted and pruned on a **21,600-slot (~1 day)** window, in their own table keyed `slot ‖ root` so pruning is a slot-ordered range delete. Two facts fix this:
+  - Measured from leanSpec's `fixtures-prod-scheme.tar.gz`: an aggregate block proof is 155–236 KB (median 190 KB) against ~100–800 B for everything else. At 4 s slots that is ~4.1 GB/day of proofs vs ~5 MB/day of blocks and states — the large-value, bulk-delete workload is what selects an LSM engine.
+  - leanSpec sets `MIN_SLOTS_FOR_BLOCK_REQUESTS = 3600` (4 hours) and a `BlocksByRange` responder MUST serve that window. One day is an operational choice 6× above that floor: it is how far a peer can fall behind and still catch up over P2P instead of needing a checkpoint. leanSpec's reference node meets the requirement in memory and persists no proofs at all; we persist so the guarantee survives a restart.
+  - Do not re-derive these numbers from the devnet-scheme fixtures in the leanSpec source tree — those are much smaller (XMSS signature 424 B there vs 2,536 B in the production scheme) and will mislead.
 - **Differential testing**: consume leanSpec's release asset `fixtures-prod-scheme.tar.gz` in CI, pinned to a commit and bumped manually. Use [leansig-test-keys](https://github.com/leanEthereum/leansig-test-keys) pre-generated keys for fast tests.
 - **Toolchain**: Rust edition 2024, resolver 3, latest stable pinned via `rust-toolchain.toml` (external floor: leanSig requires ≥1.87; no nightly needed).
 - **License**: MIT (Nyx Foundation copyright).

DOMAIN_MODEL.md

@@ -34,11 +34,11 @@ below; this section is the *strategic* frame above it.
 |---|---|---|---|---|
 | **State Transition** | Consensus-critical | `State` aggregate + `SignedBlock` processing; justification / finalization invariants | Verified Core (pure fns) | Verity Consensus (separate Lean repo) |
 | **Fork Choice** | Consensus-critical | `Store` aggregate, LMD GHOST, head / safe_target, payload `new → known` | Verified Core pure decision fns **+** Runtime Shell single-writer store | Verity Consensus + `verity-chain` |
-| **Signature & Aggregation** | Supporting | signatures, Type-1 / Type-2 proofs, verify / aggregate | Runtime Shell | `verity-crypto` (ACL → leanMultisig) |
+| **Signature & Aggregation** | Supporting | signatures, Type-1 / Type-2 proofs, verify / aggregate | Runtime Shell | `verity-crypto` (ACL → leanSig, leanMultisig) |
 | **Serialization** | Supporting | SSZ encode / decode, `hash_tree_root`, merkleization | Runtime Shell | `verity-types` (+ external SSZ lib) |
 | **Validator Duties** | Supporting | proposer / attester duties, production, signing, aggregation scheduling | I/O Edge | `verity-validator` |
 | **Networking** | Generic | gossip topics, req / resp, peers | I/O Edge | `verity-p2p` |
-| **Persistence** | Generic | block / state store, finalized anchor; Repository over an embedded KV store | Runtime Shell | `verity-db` |
+| **Persistence** | Generic | block / state store, aggregate-proof store with a bounded retention window, finalized anchor; Repository over RocksDB behind a backend trait | Runtime Shell | `verity-db` |
 | **Node Orchestration** | Generic | lifecycle, slot clock, backpressure | I/O Edge | `verity` (bin) |
 | **API** | Generic | HTTP / RPC surface | I/O Edge | `verity-rpc` |
 | **Telemetry** | Generic | metric contract | I/O Edge | `verity-metrics` (Conformist → leanMetrics) |
@@ -61,7 +61,8 @@ pattern names *how* each relationship is governed.
 | Upstream (external) | Verity context | Pattern |
 |---|---|---|
 | **leanSpec** | State Transition / Fork Choice | **Conformist** on container shapes; **Partnership** on correctness (proofs find spec bugs; fixes flow back upstream) |
-| **leanMultisig** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) |
+| **leanSig** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) — per-validator XMSS sign / verify |
+| **leanMultisig** | Signature & Aggregation | **ACL / Anti-Corruption Layer** (adapter) — aggregation and aggregate-proof verification |
 | **leanMetrics** | Telemetry | **Conformist** (exact metric contract) |
 | **external SSZ library** | Serialization | **ACL / adapter** |
 
@@ -84,6 +85,7 @@ invariant (calls flow toward higher assurance; Verified Core never calls outward
 flowchart LR
     subgraph ext["External upstream contexts"]
         SPEC["leanSpec"]
+        SIGLIB["leanSig"]
         MULTI["leanMultisig"]
         METR["leanMetrics"]
         SSZ["SSZ library"]
@@ -100,6 +102,7 @@ flowchart LR
     TEL["Telemetry · I/O Edge"]
     SPEC -->|"Conformist (shape) / Partnership (correctness)"| ST
     SPEC --> FC
+    SIGLIB -->|ACL| SIG
     MULTI -->|ACL| SIG
     METR -->|Conformist| TEL
     SSZ -->|ACL| SER

docs/src/reference/architecture.md

@@ -1,10 +1,11 @@
 ---
 title: Verity Architecture
-last_updated: 2026-07-22
+last_updated: 2026-08-10
 tags:
   - architecture
   - verification-boundary
   - crate-layout
+  - storage
 ---
 
 <!--
@@ -180,9 +181,12 @@ upstream Lean library name per Rust's `-sys` convention.
 **Thin glue over existing libraries**
 
 - `verity-p2p` — gossip and req/resp over libp2p.
-- `verity-crypto` — adapter over leanMultisig (XMSS verify / sign / aggregate).
-- `verity-db` — persistence (Repository): blocks, states, and the finalized anchor, over an
-  embedded key-value store. Keeps the storage concern out of the single-writer aggregate coordinator.
+- `verity-crypto` — adapter over the two upstream signature libraries: [`leansig`](https://github.com/leanEthereum/leanSig)
+  for per-validator XMSS sign / verify, and [`leanMultisig`](https://github.com/leanEthereum/leanMultisig)
+  for aggregation and aggregate-proof verification. One capability contract, two suppliers behind it.
+- `verity-db` — persistence (Repository): blocks, states, aggregate proofs, and the finalized anchor.
+  Keeps the storage concern out of the single-writer aggregate coordinator. See
+  [Storage engine and retention](#storage-engine-and-retention).
 - `verity-rpc` — HTTP API surface.
 - `verity-metrics` — implementation of the leanMetrics contract.
 
@@ -227,6 +231,42 @@ flowchart TB
     DB --> TYPES
 ```
 
+### Storage engine and retention
+
+`verity-db` stores two workloads with opposite shapes, and the split drives every decision below.
+Sizes are measured from leanSpec's `fixtures-prod-scheme.tar.gz` release asset; at
+`SECONDS_PER_SLOT = 4` a day is 21,600 slots.
+
+| Workload | Value size | Volume | Lifetime |
+|---|---|---|---|
+| Blocks, states, indices, finalized anchor | ~100 B – 800 B | ~5 MB/day | permanent |
+| Aggregate proofs (`MultiMessageAggregate`) | 155–236 KB, median 190 KB | ~4.1 GB/day | pruned after ~1 day |
+
+**Engine: RocksDB.** The proof workload — six-figure-byte values written continuously and dropped
+en masse a day later — is what an LSM tree with range tombstones is built for, and the same choice
+is what ethlambda, zeam, and qlean-mini run (gean uses Pebble, the same family). The cost is a C++
+dependency in the runtime's build and trust surface; that cost is accepted for Runtime Shell, where
+the bar is memory-safe, panic-free Rust around a well-exercised store, not proof. It buys nothing in
+Verified Core and reaches nothing there.
+
+**Backend trait.** Storage sits behind a backend trait with an in-memory implementation alongside
+the RocksDB one, following ethlambda's `StorageBackend` split. Tests and ephemeral nodes run
+in-memory; the engine stays replaceable if the proof workload later moves out of the database.
+Anything that leaks one engine's semantics into the trait — range deletes above all — is documented
+at the trait, not assumed.
+
+**Proof retention: 21,600 slots (~1 day).** Proofs live in their own table keyed `slot ‖ root`, so
+pruning is a slot-ordered range delete rather than a scan. They are dropped only below
+`tip_slot − 21,600` and only when that cutoff is already finalized; non-finalized proofs are never
+touched. Blocks and states are never pruned by this path.
+
+The floor is not ours to choose: leanSpec sets `MIN_SLOTS_FOR_BLOCK_REQUESTS = 3600` (4 hours) and
+a responder **MUST** serve `BlocksByRange` over that window. Everything above it is an operational
+choice about how far behind a peer can fall and still catch up over P2P instead of needing a
+checkpoint. One day is that horizon — a node down overnight rejoins by range sync — at 6× the
+mandated floor. Note that leanSpec's own reference node satisfies the requirement in memory and
+persists no proofs at all; Verity persists them so the guarantee survives a restart.
+
 ### Capability contracts
 
 The Verified Core ↔ Runtime Shell boundary is expressed not as a fixed list of FFI functions but as a small set of **capability