M9 finish follow-up 3: §14.12/§14.13 DoD reconciliation audit#37
Merged
Conversation
…nly) The closing M9 truthfulness pass. New §14.12.1 subsection reconciles the traceability matrix against the actual tree, with every covering test grep-verified to exist and each D1–D12 row marked passing (a currently-existing software test) vs contingent (a named physical-layer gate). Verified (all 13 cited symbols confirmed present): - D5 traces to the sentinel-fix tests (rec_type_zeroed_interior_is_fatal_tornmidlog + tail companion) AND the §14.9 differential — not anything stale. - D4/D10/D11 cite the §14.9 differential; those PR #35 edits landed on main and name real differential_* symbols. - loom is absent from the matrix, the DoD, and the code (grep -i loom over src/ tests/ .github/ Cargo.toml finds only the docs "why not" note). - §14.9 differential present and implemented. - Each contingent gate names its unmet condition: fuzz ≥24 CPU-h/target since 2b198e7 (dedicated runner), soak multi-hour run, H1 owner hardware, LazyFS FUSE runner, §14.4d documented negative result. - Structural-vs-substantive caveat flagged: the D11 bounded-scan counter is a drift guard (the loop window IS scan_bound), not an input-bug finder; the substantive D11 proof is F1–F4's crash-free surface + the differential. §14.13's "every row has a passing test" bullet now points at §14.12.1. Docs-only (docs/wal_design_v6.md + CLAUDE.md); no src/, no test, no workflow. After this, M9 is software-complete; the only remaining §14.13 gates are passive runner time (fuzz 24-CPU-h/target, multi-hour soak), accruing off the critical path alongside H1. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Rpbwt9JT56hQvVXiqTS131
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
M9 close-out follow-up 3 — the DoD reconciliation audit (its own PR, docs-only)
The closing M9 truthfulness pass. Adds §14.12.1 — an explicit invariant→test→status table reconciled against the actual tree, with every covering test grep-verified to exist. This is an audit for truthfulness, not a checkbox sweep: the correct output is "every invariant has a currently-passing software test, and the physical-durability layer is honestly contingent," which is what it found.
Grep-verified (13/13 cited symbols exist)
rec_type_zeroed_interior_is_fatal_tornmidlog,rec_type_zeroed_at_tail_is_torn_tail_and_zeroed,corrupt_last_record_is_a_torn_tail_and_is_zeroed,corrupt_middle_acked_record_is_fatal_tornmidlog,zeroing_prevents_resurrection_of_stale_valid_record,truncated_file_below_segment_size_recovers_without_panic,arbitrary_bytes_never_panic_and_terminate,differential_scenario_matrix/differential_over_fuzz_corpora,sealed_segments_are_immutable_across_activity_and_recovery,deletable_prefix_len_boundary_math,single_segment::{p1_fidelity,p2_density,p6_idempotent_recovery},checkpoint_preserves_records_above_up_to,split_and_roll_roundtrip_is_dense,sigkill_at_varied_points_recovers_dense_suffix,sigkill_during_checkpoint_recovers_contiguous_suffix— all confirmed insrc/ortests/.Rows changed this milestone — reconciled
rec_type_zeroed_interior_is_fatal_tornmidlog+ the tail companion) and the §14.9 differential; not anything stale.mainand name realdifferential_*symbols (grep-confirmed).grep -i loomoversrc/ tests/ .github/ Cargo.tomlfinds only the docs "why not" note) — removed, not marked done.Contingent gates each name their unmet condition
fuzz — ≥24 CPU-h/target since
2b198e7(dedicated runner); soak — a multi-hour run; §14.8 H1 — owner power-pull hardware; §14.4b/c/g LazyFS — a FUSE runner (#[ignore]); §14.4d behavioral — closed as a documented negative result (Tier-1 strace carries the DoD).Structural-vs-substantive caveat (flagged, not implied)
The D11 "bounded-scan counter never exceeded" clause is satisfied structurally — the production loop's window is
scan_bound(max_record_size), so it's a drift guard, not an input-bug finder. The substantive D11 proof is F1–F4's crash-free / no-OOB / termination surface + the §14.9 differential's exact-match classification.Scope
Docs-only (
docs/wal_design_v6.md+CLAUDE.md) — nosrc/, no test, no workflow.cargo fmt --checkclean.After this
M9 is software-complete. The only remaining §14.13 gates are passive runner time — the F1–F4 24-CPU-h/target fuzz run and the multi-hour soak run — which accrue off the critical path on owner/dedicated hardware, alongside the H1 power-pull.
🤖 Generated with Claude Code
Generated by Claude Code