Libmdbx spike

Cargo.toml

@@ -11,6 +11,7 @@ members = [
     "crates/hotblocks",
     "crates/hotblocks-harness",
     "crates/hotblocks-retain",
+    "crates/mdbx-spike",
     "crates/polars",
     "crates/primitives",
     "crates/query",

Dockerfile

@@ -1,5 +1,7 @@
 # syntax=docker/dockerfile:1
-FROM rust:1.89-bookworm AS rust
+# rust-toolchain.toml is not copied into the build context, so this base image
+# version IS the container toolchain — keep it in lockstep with the pin there.
+FROM rust:1.94-bookworm AS rust
 
 
 FROM rust AS builder
@@ -81,6 +83,23 @@ COPY --from=flush-bench-builder /out/flush_spill .
 ENTRYPOINT ["/app/flush_spill"]
 
 
+FROM builder AS mdbx-spike-builder
+ARG TARGETARCH
+RUN --mount=type=cache,target=/usr/local/cargo/registry,sharing=locked \
+    --mount=type=cache,target=/usr/local/cargo/git,sharing=locked \
+    --mount=type=cache,target=/app/target,id=cargo-target-${TARGETARCH},sharing=locked \
+    cargo build -p mdbx-spike --release \
+    && mkdir -p /out \
+    && cp target/release/mdbx-spike /out/
+
+
+# ADR 0002 churn bench; run matrix in crates/mdbx-spike/README.md
+FROM debian:bookworm-slim AS mdbx-spike
+WORKDIR /app
+COPY --from=mdbx-spike-builder /out/mdbx-spike .
+ENTRYPOINT ["/app/mdbx-spike"]
+
+
 FROM builder AS archive-builder
 ARG TARGETARCH
 RUN --mount=type=cache,target=/usr/local/cargo/registry,sharing=locked \

crates/hotblocks/spec/02-data-model.md

@@ -121,6 +121,11 @@ prefix**; blocks above it are the **volatile suffix**, subject to replacement by
 | `External` | The lower bound is set at runtime by the retention controller via the SET-RETENTION operation. Until first set: unbounded, and a dataset that is *empty* at activation defers ingestion until the first instruction (WP-5). |
 | `Unbounded` | Never trim. |
 
+All four policies are additionally subject to the space bounds of RS-13 (09 §1):
+self-healing policies (`Window`, `External`) may be trimmed past their bound under
+space pressure — observably; promise policies (`Pinned`, `Unbounded`) are never
+trimmed by space and pause at their quota instead (FM-STOR-6).
+
 **DEF-10 (Version order).** For one dataset, committed states are totally ordered by
 `ver`. "Later state" always means greater `ver`, never a comparison of head numbers (a
 fork can lower the head number while increasing `ver`).

crates/hotblocks/spec/03-write-path.md

@@ -179,6 +179,11 @@ history cannot be re-acquired through RETAIN.
   re-acquired in place (there is no downward backfill), so in self-healing modes
   (`Window`, `External` runtime application) the instruction MUST be executed as
   `RESET(⟨from − 1, h?⟩)`: the window is discarded and re-ingested from `from` upward.
+  Exception (RS-13): while a space bound governs the dataset (gap-mode) — and, where a
+  position cap is configured, unconditionally — the instruction is clamped to `first(D)`
+  instead — observable, never silent — because the RESET would re-bootstrap in a loop
+  against the very consumer lag that opened the gap (on a capped dataset a downward
+  instruction signals that lag even when the cap is not the governing bound).
   Like every RESET this MUST be observable (OB-9) — a downward `SET-RETENTION` is a
   destructive re-bootstrap, not a widening, and controllers MUST treat it as such
   (FM-OP-4). During boot validation of a `Pinned` policy whose `from` lies below the
@@ -206,14 +211,18 @@ history cannot be re-acquired through RETAIN.
   the availability floor RS-3
   (at least the last `k` blocks) always holds and the excess bound RS-4
   (`first(D) ≥ next(D) − k − P-RETENTION-SLACK`, eventually) is met. Trimming MAY be
-  batch-granular.
+  batch-granular. RS-13's effective bound MAY trim beyond `k`'s floor under space
+  pressure — the sanctioned, alarmed RS-3 exception.
 - **WP-11 (External application).** A SET-RETENTION instruction accepted through the API
   MUST be applied (the corresponding RETAIN committed) within `P-RETENTION-APPLY`, and be
   observable via the retention read afterwards. Acceptance and application are distinct
   points: the acknowledgement means the instruction is recorded and scheduled, not that
   the trim has happened. Between the two, GET-RETENTION reports the *instructed* bound —
   an acknowledged instruction is never silently forgotten (CN-9; violated today, GAP-28) —
-  and `ver` advances with the RETAIN/RESET commit itself, not at acceptance. What
+  and `ver` advances with the RETAIN/RESET commit itself, not at acceptance. Application
+  is subject to RS-13: while a space bound governs — or whenever a position cap is
+  configured — a downward instruction is clamped: recorded and observable, applied as
+  `first(D)` (§2.5 exception). What
   instruction payloads other than a block bound mean for an External dataset (policy-mode
   changes, e.g. the binding's `"None"`) is unspecified, and the current behavior diverges
   from the binding's reading (GAP-35).

crates/hotblocks/spec/06-invariants.md

@@ -243,7 +243,8 @@ paths).
 *Check:* CT-5 boot matrix (config × pre-state).
 
 **INV-44 — Destructive operations are explicit.** [transition]
-Data leaves the store only through: RETAIN per policy, REPLACE of the volatile suffix,
+Data leaves the store only through: RETAIN per policy (the policy bound composed with
+RS-13's space bound), REPLACE of the volatile suffix,
 RESET under its defined triggers (WP-6b / WP-9 / downward retention bound, WP §2.5 /
 operator), or DROP of datasets removed from configuration. Each destructive path is deliberate, documented, and observable (OB-9).
 There is no other code path by which committed blocks disappear. One non-transition

crates/hotblocks/spec/07-liveness.md

@@ -29,7 +29,9 @@ service catches up at a rate ≥ `P-CATCHUP-RATE` until steady lag is reached.
 Under the LIV-1 preconditions, the interval during which a dataset makes **zero** commit
 progress while its sources offer new data never exceeds `P-STALL-BUDGET`. This bound
 covers all internal causes: storage backpressure, maintenance debt, shared-pool
-contention, deferred-deletion churn.
+contention, deferred-deletion churn. One documented exemption: a dataset paused at its
+own disk quota (FM-STOR-6) — alarmed, per-dataset, and excluded from this budget for
+that dataset only.
 *Why this exists:* multi-minute all-dataset freezes have been observed post-deploy; this
 property is the formal target the stall harness must enforce (GAP-1).
 *Witness:* OB-3 stall detector. *Tests:* CT-7 soak + CT-6 stress.
@@ -62,8 +64,11 @@ alarm (CN-10) without blocking the rest.
 
 **LIV-7 — Reclamation liveness.**
 After logical deletions (retention, forks, drops), physical space converges: within
-`P-RECLAIM-LAG`, disk usage returns to within the amplification bound RS-6. Deletion debt
-(logically deleted but physically present data) is eventually zero in a quiescent system.
+`P-RECLAIM-LAG`, disk usage returns to within the amplification bound RS-6 — in its
+ratchet reading (RS-6b): deletion debt converges; a high-water file does not shrink on
+its own and is excluded, its return path being the dataset storage reset (RS-14).
+Deletion debt (logically deleted but physically present data) is eventually zero in a
+quiescent system.
 *Witness:* OB-6 space accounting. *Tests:* CT-7 (GAP-6).
 
 **LIV-8 — No cross-dataset starvation.**

crates/hotblocks/spec/08-failure-model.md

@@ -42,10 +42,11 @@ each. "Required response" uses four verbs:
 | # | Fault | Required response |
 |---|---|---|
 | FM-STOR-1 | Slow storage (I/O saturation, maintenance debt) | degrade: writes throttle; bounded by LIV-2 stall budget; reads keep serving; OB-3 signals pressure |
-| FM-STOR-2 | Disk approaching full | alarm at `P-DISK-FLOOR`; degrade per documented policy: reads MUST keep working; writes MAY pause (counts toward stall accounting, exempt from LIV-2 only while below floor); the system MUST NOT corrupt state and MUST provide a documented, bounded recovery path (RS-8 boot maintenance) that does not require scratch space proportional to reclaimable data |
+| FM-STOR-2 | Disk approaching full (node level) | alarm at `P-DISK-FLOOR`; degrade per RS-13: self-healing datasets ring past their floors (gap-mode), promise datasets keep data and MAY pause writes; reads MUST keep working; the system MUST NOT corrupt state and MUST provide a documented, bounded recovery path (RS-14 dataset reset; RS-8 at boot) that does not require scratch space proportional to reclaimable data |
 | FM-STOR-3 | Disk full (hard) | fail-safe: no committed-state corruption (INV-40 holds for the pre-full history); recovery path documented; startup after freeing space restores service |
 | FM-STOR-4 | Detected corruption of stored state (checksum/decode failure) | fail-safe + alarm per dataset (CN-10): the damaged dataset stops, others serve; corruption MUST be detected (never returned as data), and MUST NOT silently disable global functions (e.g. reclamation for everyone) without alarm (GAP-6 adjacent) |
 | FM-STOR-5 | Partial write persisted at crash (torn build) | mask: invisible by CN-2/INV-40; residue collected (RS-10) |
+| FM-STOR-6 | Per-dataset quota exhausted (`P-DISK-QUOTA`) | degrade per RS-13: self-healing policies trim to the effective bound (gap-mode, alarmed); promise policies — or any dataset at the `P-REORG-KEEP` ring floor, or one whose emergency trim itself cannot commit (deletes need COW pages at a full map) — pause writes (alarmed, LIV-2-exempt for that dataset), reads keep serving, other datasets unaffected (FM-3, INV-35/36); recovery: operator action or RS-14 reset |
 
 ## 3. Process faults (FM-PROC)
 
@@ -82,5 +83,5 @@ each. "Required response" uses four verbs:
 - Crash matrix: FM-PROC-* ⇢ INV-40/42, LIV-5/6, CT-2.
 - Source misbehavior corpus: FM-SRC-* ⇢ INV-7/12/13/14/23, LIV-1/9, CT-4.
 - Overload & client abuse: FM-CLI-* ⇢ RP-3/17/18, LIV-3/4/10, CT-6/CT-9.
-- Storage pressure: FM-STOR-* ⇢ INV-41, LIV-2/7, RS-6/8, CT-7.
+- Storage pressure: FM-STOR-* ⇢ INV-41, LIV-2/7, RS-6/8/13/14, CT-7/CT-8.
 - Operator: FM-OP-* ⇢ INV-43/44, CT-5 boot matrix.