Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/formats/segment-store-v1/requirements.md
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ below.
| `KEEP-CATALOG-007` | Retained kernel locks on the pinned store root and persistent writer file exclude a second cooperative writer even if the directory entry is replaced; neither lock is deleted on release, and lock ownership alone cannot construct a publisher without platform admission | Multi-handle lock model, replacement fixture, and public unsupported-platform refusal | `tests/catalog_writer_lock.rs`, `tests/catalog_platform_admission.rs`; [admission evidence](../../testing-evidence/catalog-platform-admission.md) | Implemented in #16; replacement-hardened in #17; repository-task admission corrected for #150 |
| `KEEP-CATALOG-008` | Segment, catalog, and head publication follows the documented synchronization order; retained fixed-name recovery state refuses before mutation; an absent head requires empty immutable pools; retry of an already-current candidate performs no publication mutation and re-synchronizes the root | Fault-recording port and filesystem fixtures | `tests/catalog_publication.rs`, `src/adapters/filesystem_catalog_publisher_tests.rs` | Implemented in #16 |
| `KEEP-CATALOG-009` | Restart loading refuses corrupt, unsupported, noncanonical, dangling, and conflicting catalog state | Corruption matrix | `tests/catalog_restart.rs` | Implemented in #16 |
| `KEEP-CATALOG-010` | Model-based transitions and lookups agree with a deterministic `BTreeMap` catalog | Boring reference catalog | `tests/catalog_model.rs` | Implemented in #16 |
| `KEEP-CATALOG-010` | Model-based transitions and lookups agree with a deterministic `BTreeMap` catalog | Boring reference catalog | `tests/catalog_model.rs`, `tests/catalog_model/generated_histories.rs`, `tests/catalog_model/transition_refusals.rs`; bounded oracle and calibration in [model evidence](../../testing-evidence/catalog-model-histories.md) | Implemented in #16; generated model evidence in #166 |
| `KEEP-CATALOG-011` | Every public catalog and publication-head parser boundary is fuzzed from canonical deterministic seeds | Canonical generation-1, generation-2, and bundle artifacts | `fuzz/fuzz_targets/catalog_format.rs`, `xtask/src/fuzz_seed_corpus/catalog_seeds.rs` | Implemented in #16 |

<!-- markdownlint-enable MD013 -->
Expand Down
48 changes: 48 additions & 0 deletions docs/testing-evidence/catalog-model-histories.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
# Generated catalog model evidence

Change kind: test-evidence enhancement for #166, found by the T-12.3 audit under #131. Owner: `@flyingrobots`. The subject is Keep's public catalog construction, admission, snapshot lookup and successor refusal behavior. Production code and durable formats are unchanged.

## Oracle and bounded claim

The new model chooses membership before encoding. Chunk expectations use explicit source bytes and `ChunkId::hash_bytes`; layout expectations use the frozen `empty` and `one-zero` identities from `conformance/layout/v1/layouts.tsv` and their literal record fixtures. It never derives expected membership or payloads from segment iteration, catalog enumeration or returned records. Chunk hashing is still shared with production; this suite does not independently establish hash correctness. The existing independent format and identity corpus remains necessary.

All subsets of those four records form the generation states. The generator visits all three-generation histories in lexicographic mask order, with bundled segments and with reversed, separately packed records. Assertions compare exact returned bytes, absence, logical record count and each pinned generation after every snapshot has been created. Valid successor results are compared with input-derived generation arithmetic. Layout inclusion here is catalog membership, not a claim of retained closure or natural chunk boundaries.

Separate generated laws reject stale and skipped successor generations, a wrong predecessor digest, and a head/catalog generation mismatch with exact typed coordinates. These supplement existing named examples; they do not replace the format, restart, concurrency or crash suites.

## Replay and reduction

Run `cargo test --locked --test catalog_model generated_histories` in the copied Docker source, adding `--release` for optimized execution. The external runner records this command and source commit before launch. Enumeration has no random seed or environment-controlled input. Every assertion identifies its history or mask and relevant packing/generation coordinates; the complete finite input space is reconstructible even if the child crashes.

The deterministic reducer is exhaustive replay in the same ascending mask-tuple order, stopping on the first failure. This identifies the least failing tuple in that bounded order without relying on a random seed or a large opaque counterexample. It does not minimize arbitrary-length histories or prove behavior outside the fixed record universe and three-generation bound. Newly discovered production failures must additionally become named permanent regression cases; none was found in the unmutated implementation during this change.

## Calibration

The test source was committed as `c9b41e99fb7e89217afbd896732dbea09a0c97ab`, on production base `6051abb25a9fd33ae7ee0de5614514b709a4d82a`. Subsequent formatting changes do not change the calibrated assertions. Each mutation below changed only a production file in an isolated Docker copy; the normal working tree retained the correct implementation.

| Violated behavior | Production mutation | Observed runtime RED |
| --- | --- | --- |
| Present records remain retrievable | Filter every admitted catalog lookup result away | Exact payload/absence assertion |
| Absent records remain absent | Failed binary search falls back to the first binding | Exact payload/absence assertion |
| Logical record count describes the selected catalog | Return zero from admitted catalog count | Membership count assertion |
| Snapshot reports its pinned generation | Return generation one from snapshot generation | Pinned generation assertion |
| Successor proof reports its admitted candidate | Return generation one from successor generation | Successor assertion |
| Stale/skipped candidate reports the specified generation refusal | Invert the generation mismatch guard | Refused-operation check |
| Wrong predecessor reports the specified digest refusal | Invert the predecessor mismatch guard | Refused-operation check |
| Stale/skipped refusal retains its expected/observed coordinates | Swap generation coordinates while preserving refusal | Exact typed generation assertion |
| Predecessor refusal retains its expected/observed coordinates | Swap predecessor coordinates while preserving refusal | Exact typed predecessor assertion |
| Head and catalog generation mismatch remains precise | Invert the head generation mismatch guard | Exact typed generation assertion |

Independent review of `343a6f9ac91056bad67134f2dad377f67a5783da` identified that the guard inversions only calibrated refusal existence. The two diagnostic-only mutations above preserve refusal and reach the existing exact-coordinate assertions; both fail at runtime. The reviewed test source is unchanged, and restored-production debug/release execution passes. No production fix or new expectation was needed.

The original handwritten model passes the absent-record mutant: it checks present records but never queries an absent identity. The generated law fails against the same mutated production lookup. This is direct evidence that the additional runtime oracle catches a defect the original model missed; it is not a claim that main contained that production defect.

The first missing-record mutant failed compilation because it made a private method unused; that result is excluded. The corrected mutant retained the call and filtered its result, producing the recorded assertion failure. An initial GREEN attempt reused a cached mutant binary after timestamp-preserving restoration; that result is also excluded. The isolated Keep package artifacts were then invalidated and the unmutated source rebuilt before successful debug/release execution. A source-policy invocation without Git metadata failed setup and required a correctly initialized copied repository.

## Execution and limits

The laws execute in memory with the pinned Rust 1.96.0 toolchain on Linux Docker. The serialization sink supplies owned bytes and makes no filesystem durability claim. No clock, random source, sleep, scheduling dependency or network is consulted by the test. The proposed size is small; ordinary Cargo execution does not enforce the repository's desired per-test filesystem/network/time/memory ceilings, as documented in `docs/testing/enforcement.md`. This record does not claim those enforcement gaps are closed or waived.

Focused debug/release execution and Clippy pass. Formatting, source policy and final hosted checks are recorded on the PR's exact head before readiness. Broad checks from another SHA are not transferred. Raw calibration and setup receipts remain with the review evidence; the mutation descriptions and commands above permit reproduction without machine-local source paths.

Delete these tests only if the catalog contract is removed or a stronger, cheaper independently calibrated model subsumes their claims. A production bug found by generation keeps its minimized named counterexample even if the exploratory generator is later replaced.
3 changes: 3 additions & 0 deletions tests/catalog_model.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
//! Deterministic catalog transition and lookup model laws.

#[path = "catalog_model/generated_histories.rs"]
mod generated_histories;

mod support;

use std::collections::BTreeMap;
Expand Down
158 changes: 158 additions & 0 deletions tests/catalog_model/generated_histories.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
//! Generated finite catalog histories checked against pre-encoding input maps.

#[path = "record_inputs.rs"]
mod record_inputs;
#[path = "transition_refusals.rs"]
mod transition_refusals;

use keep::{
AdmittedSegment, CanonicalCatalog, CanonicalPublicationHead, CatalogGeneration,
CatalogSnapshot, ChecksummedPublicationHead, LayoutEntryLimit, SegmentReadPolicy,
SegmentRecordLimit,
};
use record_inputs::{Packing, RecordMap};
use std::error::Error;

type ResultOf<T> = Result<T, Box<dyn Error>>;

// Size: small (memory only). Oracle: the input maps, chosen before any writer,
// decoder or catalog executes. Exhaustive bounded generator, no ambient seed.
#[test]
fn generated_histories_preserve_exact_membership_in_pinned_snapshots() -> ResultOf<()> {
let inputs = record_inputs::inputs()?;
for packing in [Packing::Bundled, Packing::SeparateReversed] {
check_packing(&inputs, packing)?;
}
Ok(())
}

fn check_packing(inputs: &RecordMap, packing: Packing) -> ResultOf<()> {
for first in 0..16_u8 {
for second in 0..16_u8 {
for third in 0..16_u8 {
check_history(inputs, [first, second, third], packing)?;
}
}
}
Ok(())
}

fn check_history(inputs: &RecordMap, history: [u8; 3], packing: Packing) -> ResultOf<()> {
let models = history
.map(|mask| record_inputs::select(inputs, mask))
.into_iter()
.collect::<ResultOf<Vec<_>>>()?;
let encoded = models
.iter()
.map(|model| record_inputs::encode(model, packing))
.collect::<ResultOf<Vec<_>>>()?;
let segments = encoded
.iter()
.map(|generation| {
generation
.iter()
.map(|bytes| AdmittedSegment::decode(bytes, policy()))
.collect::<Result<Vec<_>, _>>()
})
.collect::<Result<Vec<_>, _>>()?;
let catalogs = build_catalogs(&segments)?;
let heads: Vec<_> = catalogs
.iter()
.map(|catalog| CanonicalPublicationHead::for_catalog(catalog.checksummed()))
.collect();
let snapshots = catalogs
.iter()
.zip(&segments)
.zip(&heads)
.map(|((catalog, records), head)| {
ChecksummedPublicationHead::decode(head.encoded())?
.admit(catalog.checksummed().admit(records)?)
.map_err(Into::into)
})
.collect::<ResultOf<Vec<_>>>()?;
for (index, (snapshot, model)) in snapshots.iter().zip(&models).enumerate() {
assert_eq!(
snapshot.generation().get(),
u64::try_from(index)?
.checked_add(1)
.ok_or("generation overflow")?,
"pinned generation history={history:?} packing={packing:?}"
);
check_membership(snapshot, model, inputs, history, packing)?;
}
check_successors(&catalogs, &segments, history, packing)
}

fn build_catalogs(segments: &[Vec<AdmittedSegment<'_>>]) -> ResultOf<Vec<CanonicalCatalog>> {
let mut catalogs = Vec::new();
let mut predecessor = None;
for (index, records) in segments.iter().enumerate() {
let generation = CatalogGeneration::new(
u64::try_from(index)?
.checked_add(1)
.ok_or("generation overflow")?,
)?;
let catalog = CanonicalCatalog::from_segments(generation, predecessor, records)?;
predecessor = Some(catalog.checksummed().digest());
catalogs.push(catalog);
}
Ok(catalogs)
}

fn check_successors(
catalogs: &[CanonicalCatalog],
segments: &[Vec<AdmittedSegment<'_>>],
history: [u8; 3],
packing: Packing,
) -> ResultOf<()> {
for (index, (current, next)) in catalogs.windows(2).zip(segments.windows(2)).enumerate() {
let [before, after] = current else {
return Err("missing catalog pair".into());
};
let [old_records, new_records] = next else {
return Err("missing segment pair".into());
};
let successor = before
.checksummed()
.admit(old_records)?
.validate_successor(after.checksummed().admit(new_records)?)?;
assert_eq!(
successor.generation(),
CatalogGeneration::new(
u64::try_from(index)?
.checked_add(2)
.ok_or("generation overflow")?
)?,
"successor history={history:?} packing={packing:?}"
);
}
Ok(())
}

fn check_membership(
snapshot: &CatalogSnapshot<'_, '_, '_>,
model: &RecordMap,
inputs: &RecordMap,
history: [u8; 3],
packing: Packing,
) -> ResultOf<()> {
assert_eq!(
snapshot.record_count(),
u64::try_from(model.len())?,
"membership count history={history:?} packing={packing:?}"
);
for identity in inputs.keys() {
let observed = snapshot.record(*identity);
assert_eq!(
observed.map(keep::AdmittedSegmentRecord::payload),
model.get(identity).map(Vec::as_slice),
"exact payload/absence history={history:?} packing={packing:?} generation={} identity={identity:?}",
snapshot.generation().get()
);
}
Ok(())
}

const fn policy() -> SegmentReadPolicy {
SegmentReadPolicy::new(SegmentRecordLimit::MAXIMUM, LayoutEntryLimit::MAXIMUM)
}
118 changes: 118 additions & 0 deletions tests/catalog_model/record_inputs.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,118 @@
//! Specified record inputs and an in-memory serialization sink; no durability claim.

use std::cell::RefCell;
use std::collections::BTreeMap;
use std::error::Error;
use std::io::{self, Write};
use std::rc::Rc;

use crate::support::decode_hex;
use keep::{
AdmittedLayout, AdmittedSegmentRecord, ChunkId, LayoutDecodePolicy, LayoutEntryLimit, LayoutId,
SegmentRecordIdentity, SegmentRecordLimit, SegmentStage, StagedSegment,
};

type ResultOf<T> = Result<T, Box<dyn Error>>;
pub(super) type RecordMap = BTreeMap<SegmentRecordIdentity, Vec<u8>>;

pub(super) fn inputs() -> ResultOf<RecordMap> {
let mut records = RecordMap::new();
for bytes in [vec![0], vec![1, 2, 3]] {
records.insert(
SegmentRecordIdentity::Chunk(ChunkId::hash_bytes(&bytes)?),
bytes,
);
}
// Oracle: independently frozen layouts.tsv identities and literal fixture bytes,
// never decoded segment records or catalog enumeration.
for (id, hex) in [
(
"keep:layout:v1:flat-chunks-v1:blake3-256:176:539516cc52fe7433e3a984a4e2a4877676673bb62d6203a88dfe1ce253c2c0f8",
include_str!("../../conformance/layout/v1/empty.layout.hex"),
),
(
"keep:layout:v1:flat-chunks-v1:blake3-256:220:887da23f1a7483359a78fc9a7fde80030ec2c4690603803f0ab7d0edb56575b8",
include_str!("../../conformance/layout/v1/one-zero.layout.hex"),
),
] {
records.insert(
SegmentRecordIdentity::Layout(id.parse::<LayoutId>()?),
decode_hex(hex.trim_end())?,
);
}
Ok(records)
}

pub(super) fn select(inputs: &RecordMap, mask: u8) -> ResultOf<RecordMap> {
let mut selected = RecordMap::new();
for (index, (identity, bytes)) in inputs.iter().enumerate() {
let bit = 1_u8
.checked_shl(u32::try_from(index)?)
.ok_or("input mask overflow")?;
if mask & bit != 0 {
selected.insert(*identity, bytes.clone());
}
}
Ok(selected)
}

#[derive(Clone, Copy, Debug)]
pub(super) enum Packing {
Bundled,
SeparateReversed,
}

pub(super) fn encode(records: &RecordMap, packing: Packing) -> ResultOf<Vec<Vec<u8>>> {
let entries: Vec<_> = records.iter().collect();
match packing {
Packing::Bundled if entries.is_empty() => Ok(Vec::new()),
Packing::Bundled => Ok(vec![segment(&entries)?]),
Packing::SeparateReversed => entries
.iter()
.rev()
.map(|entry| segment(&[*entry]))
.collect(),
}
}

fn segment(records: &[(&SegmentRecordIdentity, &Vec<u8>)]) -> ResultOf<Vec<u8>> {
let output = Rc::new(RefCell::new(Vec::new()));
let mut staged =
StagedSegment::begin(MemoryStage(Rc::clone(&output)), SegmentRecordLimit::MAXIMUM)?;
for (identity, bytes) in records {
staged = match identity {
SegmentRecordIdentity::Chunk(_) => {
staged.append(AdmittedSegmentRecord::for_chunk(bytes)?)?
}
SegmentRecordIdentity::Layout(_) => {
let layout = AdmittedLayout::decode_record(
bytes,
LayoutDecodePolicy::new(LayoutEntryLimit::MAXIMUM),
)?
.encode_record()?;
staged.append(AdmittedSegmentRecord::for_layout(&layout)?)?
}
};
}
let _sealed = staged.seal()?;
let bytes = output.borrow().clone();
Ok(bytes)
}

struct MemoryStage(Rc<RefCell<Vec<u8>>>);

impl Write for MemoryStage {
fn write(&mut self, bytes: &[u8]) -> io::Result<usize> {
self.0.borrow_mut().extend_from_slice(bytes);
Ok(bytes.len())
}
fn flush(&mut self) -> io::Result<()> {
Ok(())
}
}

impl SegmentStage for MemoryStage {
fn synchronize(&mut self) -> io::Result<()> {
Ok(())
}
}
Loading
Loading