//! The invariant backlog — store-api.md §Invariants' seven entries //! registered as the rows-to-grow table (README §The invariant //! backlog is the normative statement; this module is its in-code //! registry, which waves 2–6 grow rows against). //! //! Each entry traces to the store-api.md invariant numbering (INV-1 //! through INV-7 mirror §Invariants 1–7) and carries the pinning text //! the row stamps will cite. A suite row that does not trace to an //! entry here is not a conformance row; a new property needs a backlog //! entry and its stamp first. //! //! The column plan: mem is the contract-reference engine (ADR-011 §2) //! — wave 2 lands its column first, every other engine's rows mirror //! it, and additions to mem's column propagate to all others (INV-7). #![allow(dead_code)] /// One backlog entry: an invariant of store-api.md §Invariants, its /// planned row family, the pinning texts its row stamps cite, and the /// first column to land it. pub struct Invariant { /// `INV-` — mirrors the n-th item of store-api.md §Invariants. pub id: &'static str, /// One-line restatement of the invariant as specced. pub invariant: &'static str, /// The planned row family — what wave-grown rows assert (README /// table's "Row family" column). pub row_family: &'static str, /// The pinning texts the rows' stamps cite (spec §/ADR §; the /// README table's "Pinning text" column, split by citation). pub pins: &'static [&'static str], /// The first column and wave to land the family (README table's /// last column). pub first_column: &'static str, } /// The backlog, in store-api.md §Invariants order. pub const BACKLOG: [Invariant; 7] = [ Invariant { id: "INV-1", invariant: "whole-blob put/get round-trips byte-identical under the canonical \ derivation — both tiers, both put paths, every shipped engine", row_family: "one round-trip family over the content matrix (put paths and tiers \ loop in-body; the git-interop test remains the derivation's source \ of truth)", pins: &[ "store-api.md §Invariants 1", "ADR-002 (canonical derivation)", "ADR-003 (both put paths, dispatch)", "ADR-007/008/009/011 (the shipped engines)", ], first_column: "wave 2 — mem (kv tier), then local (large tier)", }, Invariant { id: "INV-2", invariant: "dedup: putting identical content twice (same or different path) is \ one pool entry", row_family: "one dedup row, same-path and different-path legs", pins: &[ "store-api.md §Invariants 2", "ADR-003 (whole-value put is CAS first-writer-wins)", "ADR-005 (re-put refcounts the existing entry)", ], first_column: "wave 2 — mem", }, Invariant { id: "INV-3", invariant: "stage hygiene: any failure mid-put leaves zero stage files; any \ success leaves exactly one committed entry", row_family: "one exact-count hygiene family over both put paths and both failure \ modes (explicit discard, failed commit)", pins: &[ "store-api.md §Invariants 3", "ADR-010 §1 (the staged-put contract: commit publishes, every failure path \ discards)", "ADR-003 (stage-then-commit-rename)", ], first_column: "wave 2 — mem (degenerate kv stage) and local (the stage form)", }, Invariant { id: "INV-4", invariant: "sweep safety: with correct liveness registered sweep counts are \ exact; with aborting sources sweep deletes nothing", row_family: "one single-node exact-count family (happy + abort shapes); the fleet \ form is its own engine-gated row family running under \ `--all-features`", pins: &[ "store-api.md §Invariants 4", "ADR-005 (delete windows, abort-as-data)", "ADR-008 (the engine-gated fleet form)", "ADR-012 §1/§4/§6.7 (sweep shape, GC-state host, executor-of-window ruling)", "ADR-013 §2 (the sweep lease's semantics)", ], first_column: "wave 2 — mem (in-process protocol); the fleet form first runs in \ wave 6", }, Invariant { id: "INV-5", invariant: "`list()` correctness is observable only through GC", row_family: "list-correctness rows assert through sweep outcomes (exact counts), \ never by comparing enumerated lists directly", pins: &[ "store-api.md §Invariants 5", "ADR-003 (`list()` complete and well-formed by contract)", "ADR-005 (GC's live-set diff rides `list()`)", ], first_column: "wave 2 — mem", }, Invariant { id: "INV-6", invariant: "`stat`/`size` on any engine returns the entry length without fetching \ content", row_family: "one stat-discipline family per engine column", pins: &[ "store-api.md §Invariants 6", "ADR-008 (the trait `size` probe discipline)", "ADR-009 (pg-lo's companion-row probe)", ], first_column: "wave 2 — mem", }, Invariant { id: "INV-7", invariant: "engine-conformance uniformity: every engine's bodies pass the same \ contract suite mem (the reference engine) passes", row_family: "the meta-gate — a column's green run against mem's rows is the \ assertion; no separate uniformity test exists", pins: &[ "store-api.md §Invariants 7", "ADR-010 §1 (one trait, every engine, same suite)", "ADR-011 §2 (mem's contract-reference role)", ], first_column: "wave 2 — mem (its column defines the required set)", }, ]; /// The backlog's traceability gate: entries mirror store-api.md /// §Invariants' numbering in order, and every entry's fields are /// populated. The harness's tests call this; a violation is a /// registry-editing mistake, not a runtime event. pub fn assert_traceable() { for (position, entry) in BACKLOG.iter().enumerate() { assert_eq!( entry.id, format!("INV-{}", position + 1), "backlog order mirrors store-api.md §Invariants" ); assert!(!entry.invariant.is_empty()); assert!(!entry.row_family.is_empty()); assert!(!entry.pins.is_empty(), "{} must pin its behavior", entry.id); assert!(!entry.first_column.is_empty()); } } /// Look a backlog entry up by its `INV-n` id. pub fn invariant_by_id(id: &str) -> Option<&'static Invariant> { BACKLOG.iter().find(|entry| entry.id == id) }