- tests/conformance/README.md: the convention doc — row naming (property- stated names, engine dimension is the column), the Contract stamp: format (the alkstore ADR-017 §4.2 convention adapted), the one- normative-owner-per-property rule, the factory contract (fresh isolated instance per open, idempotent teardown, safe over an abandoned instance), the SKIP posture (SQL-attached columns skip cleanly server-less; acceptance requires green against the server), the invariant backlog (the seven store-api.md §Invariants registered as the rows-to-grow table with pinning citations), and the mem-first column plan (mem is the contract-reference engine, ADR-011 §2) - harness skeleton, compile-able with zero rows: StoreFactory (fresh + isolated + idempotent-teardown contract; the Store associated type is wave 2's binding point for the facade type), stamp.rs (the marker + convention anchor), backlog.rs (in-code registry with a traceability gate asserting INV-1..7 mirror §Invariants in order) - no engine-specific code; no dependencies added Verification: cargo test (33 passed across lib + 3 targets), cargo clippy --all-targets -- -D warnings, cargo fmt --check
158 lines
6.8 KiB
Rust
158 lines
6.8 KiB
Rust
//! 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-<n>` — 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)
|
||
}
|