diff --git a/spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md b/spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md index e3f4505..219ae40 100644 --- a/spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md +++ b/spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md @@ -1,11 +1,19 @@ # Contract — P13-S27: the reduction version gets an outside witness -**Status:** **RATIFIED 2026-08-07** after **review round 1**, which returned nine -findings — four of them blocking — all now carried in the document; **AMENDED -2026-08-07** twice, both before dispatch: **pin 10** (the unsatisfiable escape -clause) and **round 1's nine**. **Not yet implemented. The pins are now frozen — -they may be executed, not edited.** A defect found during execution is -**reported, not patched in place**. +**Status:** **RATIFIED 2026-08-07** after **two adversarial review rounds** +(nine findings then six, eight blocking in total), all now carried in the +document; **AMENDED 2026-08-07** three times, all before dispatch: **pin 10** (the +unsatisfiable escape clause), **round 1's nine**, and **round 2's six**. **Not yet +implemented. The pins are frozen — they may be executed, not edited.** A defect +found during execution is **reported, not patched in place**. + +> **Round 2 was run against the frozen contract and found four more blocking +> defects, two of them created by round 1's own amendments.** Ratifying after a +> single round was premature. A third round is warranted before dispatch by the +> same reasoning that justified the second — the format-epoch rung took four, and +> **the defect rate here has not yet fallen**: round 1 found nine, round 2 found +> six. Treat "dispatchable" as a claim requiring evidence of convergence, not a +> status reached by running out of findings. (Was: DRAFT, BLOCKED on the format-epoch rung, `spec/CONTRACT_FORMAT_EPOCH_MAJOR1.md`, which at the time was ratified and in @@ -30,6 +38,29 @@ round 1 returned: | 8 | Gate 6a checked `textproj` only, while touch row 7 gives `testkit` the real authority | Scope widened to both | | 9 | No **commit-side positive** test, though obligation 1 warns that converting one branch leaves a hole | **Test 8** added | +**Review round 2 — 2026-08-07, at `39287f8`.** Run against the *ratified and +frozen* contract, and it returned **six more findings, four of them blocking**. +Round 1's ratification was premature; this is the round that should have followed +it before dispatch. + +| # | Finding | Disposition | +|---|---|---| +| 1 | The call-site count was corrected in §0.4 only. The "Rung type" paragraph still said **57**, and touch row 2 still said `bundle.rs` has **35** opens — a figure that was never `bundle.rs` alone (it was `bundle.rs` + `fuzz.rs`, which has its own row) and is now stale on top of that. Reconciliation was impossible | Both corrected to **60** / **23**; row 5 now states `fuzz.rs`'s 15 + 1 explicitly | +| 2 | §0.4 called `project.rs:936` a **production** bundle writer. `#[cfg(test)]` starts at `:630`; every `Bundle` call in the file is below it | Struck. §0.4's correction stands on `serialize.rs` alone. Recorded as the **fourth** instrument failure in that section | +| 3 | **M5 unexecutable.** `serialize_document` refuses bases at `serialize.rs:151`, so its output is base-free, and pin 5 + test 4 require base-free bundles to open at *any* authority — the mutation cannot fail | Split into **M5a** (production wires the constant) and **M5b** (the authority is load-bearing where a base exists) | +| 4 | **M6's second half unexecutable.** `open` rejects a stale base, `create` rejects a base-bearing manifest (`bundle.rs:234`), `commit` validates what it emits — no caller can hold an open `Bundle` with a stale *inherited* base | Replaced: **broaden** pin 3a rather than narrow it. The unreachability is itself reported | +| 5 | Pin 3a's justification — *"production code mints a self-consistent stale document"* — is false in-tree. **Zero** production paths stage a base | Restated: pin 3a guards the **public `commit_versioned` API**, not an in-tree path | +| 6 | `serialize.rs:157` is dead code, orphaned by the `:151` guard | Recorded as a finding; explicitly **not** this rung's to repair | + +**Two of round 2's findings were introduced by round 1, and that is the lesson +worth carrying.** Ruling M7's refusal permanent is what made M5 unexecutable, and +adding test 8 on the write side did not come with a re-derivation of M6 against +the same reachability. **An amendment is a change to the system, not a patch to a +line**; the next round must re-derive every mutation against every ruling the +previous round made, not only inspect the text it edited. Round 1's own §0.4 +correction has the same shape: it verified one claim in a list and inherited its +neighbours. + **Pins 1 and 3–10 are settled and internally consistent.** Pin 2a is resolved from outside (below); pin 2 is unchanged. @@ -57,8 +88,10 @@ prohibition required. **Rung type:** **capability + API change.** No wire bytes move and no schema major or minor changes — `BundleError` has no discriminant and no encoder (`bundle/src/error.rs`), so a new variant is a pure Rust API change. What does -change is `Bundle::open`'s **and `Bundle::create`'s** signatures, at 57 and 32 -call sites. +change is `Bundle::open`'s **and `Bundle::create`'s** signatures, at **60** and 32 +call sites. *(Was "57 and 32". Corrected in review round 2 — round 1 corrected +§0.4's table and left this spelling and touch row 2's untouched, which is the +same one-path-of-several defect §1.7 of the handoff names.)* **Now DOES unblock P13-S16, once it lands.** This rung installs the authority and validates both read and write paths; S16's remaining precondition was pin 2a's @@ -158,12 +191,46 @@ code: `serialize_document` (`serialize.rs:119`) creates a bundle and commits a manifest built by `build_manifest` (`serialize.rs:212`), which **copies `base.reduction_algorithm_version` verbatim** into a fresh `SnapshotRef` (`:219`–`:222`). `commit_versioned` then stamps the superblock from that same -carried value via `reduction_version_for` (`bundle.rs:798`). `project.rs:936` is -a **second** production write path of the same shape. +carried value via `reduction_version_for` (`bundle.rs:798`). ~~`project.rs:936` is +a **second** production write path of the same shape.~~ -**So production code mints a self-consistent stale document without ever calling -`open`.** An authority enforced only at read time would leave that entirely -open, which is the gap this revision closes (pin 3a, pin 4a). +> **CORRECTED 2026-08-07 in review round 2 — `project.rs` is NOT a production +> write path, and never was.** `#[cfg(test)]` begins at `project.rs:630`. Every +> `Bundle` call in the file sits below it: `Bundle::create` at `:983` and +> `:1122`, `Bundle::open` at `:1147`. `:936` is an assertion inside a test. The +> `serialize.rs` half of this paragraph **is** correct — its `Bundle::create` +> (`:155`) and `commit_versioned` (`:183`) are above that file's `#[cfg(test)]` +> at `:284` — so §0.4's correction stands on **one** example, not two. +> +> **The same slip reaches the open table below:** both textproj entries there +> (`serialize.rs:383`, `project.rs:1147`) are also below their files' +> `#[cfg(test)]`, so **`epiphany-textproj` has zero production `Bundle::open` +> sites.** The crate still counts 2 for signature-change purposes; it counts 0 +> for any argument about what production does. +> +> **Fourth instrument failure in this section.** Round 1 checked the +> `epiphany-editor-core` claim in this paragraph and did not check its +> neighbours — verifying one claim in a list and inheriting the rest. + +**Pin 3a's justification, restated in review round 2.** This paragraph used to +conclude *"production code mints a self-consistent stale document without ever +calling `open`."* **That is no longer true in-tree.** Checking every +`canonical_base:` assignment above the `#[cfg(test)]` boundary in `serialize.rs`, +`project.rs` and `bundle.rs` returns **zero**: the format rung's pin 3b closed +the only in-tree path when it made `serialize_document` refuse a base-bearing +document (`serialize.rs:151`), and `create` already rejected a base-bearing +manifest (`bundle.rs:234`). + +**Pin 3a survives on a different and narrower footing, which it must now state:** +`commit`/`commit_versioned` are **public API**, and an out-of-tree caller can +stage a canonical base directly without going through `epiphany-textproj` at all. +The writer check guards that surface. It is no longer guarding an in-tree +production path, because there is not one. + +> **Consequence for M5, which round 1 did not follow through.** If no production +> path stages a base, no production path is authority-load-bearing, and a +> mutation of the authority cannot break a production round trip. M5 was written +> against the old reading and is corrected in §4. > **Method note, recorded because it is this rung's own subject matter.** The > false claim came from `grep … canonical_base | head -14`. The `textproj` hits @@ -596,10 +663,10 @@ row may not record S16 as open until those land with this rung**; ratification o | # | File | Change | |---|---|---| | 1 | `crates/epiphany-ops/src/lib.rs` (or a new `reduction.rs`) | pins 1, 2 | -| 2 | `crates/epiphany-bundle/src/bundle.rs` | pins 3, 3a, 3b, 5, 6, 7 + 35 in-crate `open` sites + 11 in-crate `create` sites | +| 2 | `crates/epiphany-bundle/src/bundle.rs` | pins 3, 3a, 3b, 5, 6, 7 + **23** in-crate `open` sites + 11 in-crate `create` sites. *(Was "35 opens" — corrected in review round 2. The 35 was never `bundle.rs` alone: it was `bundle.rs` 20 + `fuzz.rs` 15 at `381c498`, and `fuzz.rs` has its own row 5. Now 23 after the format rung added 3.)* | | 3 | `crates/epiphany-bundle/src/error.rs` | pin 4 | | 4 | `crates/epiphany-bundle/src/ids.rs` | pin 8 | -| 5 | `crates/epiphany-bundle/src/fuzz.rs` | call sites | +| 5 | `crates/epiphany-bundle/src/fuzz.rs` | **15** `open` sites + **1** `create` site. *(Figures stated in review round 2; row 2's old "35" silently included these, so the two rows together could not be reconciled against §0.4.)* | | 6 | `crates/epiphany-bundle/tests/{crash_recovery,manifest_selection}.rs` | call sites | | 7 | `crates/epiphany-testkit/src/{bundle_harness,roundtrip,generators}.rs` | call sites, real authority | | 8 | `crates/epiphany-testkit/tests/bundle_reopen.rs`, `benches/bundle.rs` | call sites | @@ -726,18 +793,67 @@ compile**, then reverted — it demonstrates what pin 3 forbids and why the prohibition needs to be a review rule, since no test can catch a `Default` that callers then use. Report it as a *prohibition recorded*, not a guard. -**M5 — the authority is the one consulted, and by a production path.** Change -`CURRENT_REDUCTION_ALGORITHM_VERSION` to a different value. The failing test -MUST be one exercising a **production composition path** — `textproj`'s -`serialize_document` / `project` round trip — **not** a fixture using -`synthetic_for_fixture`, which by design would not move. Report which test -failed; if only fixture tests fail, pin 3b has been applied backwards and that -is a finding. +**M5 — SPLIT IN REVIEW ROUND 2. It was unexecutable as written.** + +> **Why.** It required changing `CURRENT_REDUCTION_ALGORITHM_VERSION` and +> observing a **production composition path** test fail — naming `textproj`'s +> round trip. But `serialize_document` refuses base-bearing documents at +> `serialize.rs:151`, *before* `Bundle::create`, so its output is **necessarily +> base-free**; and pin 5 with test 4 require a base-free bundle to open at **any** +> authority. The mutation therefore cannot make that test fail — not because the +> wiring is absent, but because the path carries nothing for the authority to +> check. Round 1 introduced this by ruling M7's refusal permanent and not +> re-deriving M5 against it. + +The original intent had two halves. They are now separate mutations, because no +single path carries both any more. + +**M5a — the constant is wired into production.** Change +`CURRENT_REDUCTION_ALGORITHM_VERSION`. Observe that the `BundleCapabilities` +`serialize_document` constructs changes with it — the production path really does +source the authority rather than a literal. Assert on the constructed capability, +**not** on an open or commit outcome; there is no base, so no check fires and +none should. **A test that fails here would mean the production path is doing +something the contract does not authorize.** + +**M5b — the authority is load-bearing where a base exists.** Same mutation, but +the failing test MUST be one combining the **real** authority with a +**base-bearing** bundle. After obligation 3, that is +`assert_reduction_serialization_stable` (`testkit/src/roundtrip.rs:255`), whose +base coverage this rung restores and which touch row 7 gives the real authority. +Report which test failed. **If only `synthetic_for_fixture` tests move, pin 3b +has been applied backwards** — that was the original M5's finding condition and +it is preserved here. + +**Both halves are required.** M5a alone shows the constant is read but never that +it matters; M5b alone shows it matters but never that production reads it. The +original mutation conflated the two because, at `381c498`, one path did both. **M6 — the writer check fires.** Remove pin 3a's commit-side validation; test 5 -must fail. Then narrow it to refuse *any* stale inherited base rather than only a -newly emitted or replaced one, and confirm an unrelated commit on an -already-open bundle starts failing — signing that pin 3a's scope is deliberate. +must fail. + +**Second half REPLACED IN REVIEW ROUND 2. It was unexecutable as written.** + +> **Why.** It asked for pin 3a to be narrowed to refuse *any* stale **inherited** +> base, then for an unrelated commit on an already-open bundle to start failing. +> That state cannot be constructed: `open` rejects a stale base (pin 5, test 2), +> `create` rejects a base-bearing manifest outright (`bundle.rs:234`), and a +> successful `commit` validates the base it emits. **No caller can hold an open +> `Bundle` whose inherited base is stale**, so the mutation has nothing to +> observe. Round 1 added test 8 on the write side without re-deriving M6 against +> the same reachability. + +**As replaced — broaden rather than narrow.** Widen pin 3a to refuse a commit on +a **base-bearing bundle regardless of whether the version matches**, then confirm +that an unrelated commit — one that does not touch `canonical_base` — starts +failing on a bundle opened with a matching base. That state **is** reachable +(test 6 opens exactly it), so the mutation runs, and it signs the same thing the +original was reaching for: that *"newly emitted or replaced"* is a deliberate +scope and not an accident of where the check was placed. + +**Record alongside it** that the original formulation was unreachable. That pin +3a's scope is *forced* rather than *chosen* is a stronger result than the +mutation was written to obtain, and it belongs in the report. **M7 — the laundering the text refusal prevents, finally observed. ADDED 2026-08-07 in review round 1; this discharges inherited obligation 2.** @@ -766,6 +882,15 @@ argument for the refusal, and it has never been run. result as a **demonstration**, not a guard: nothing in the shipped tree changes, and the refusal is permanent (see the ruling under inherited obligation 2). +> **You will meet dead code here. Do NOT fix it — report it.** Found in review +> round 2: `serialize.rs:157`'s `if let Some(base) = &document.canonical_base` +> is **unreachable**, orphaned by the `:151` guard that returns +> `CanonicalBaseUnsupported` before it. Removing the guard for M7 makes it live +> again, which is what lets the demonstration run at all — and restoring the +> guard makes it dead again. It is a pre-existing defect from the format-epoch +> rung, **not this rung's to repair**, and touching it would put an unpinned +> change in a staged file. Record it in the report; it is a Pass-13 candidate. + **This is a mutation whose expected outcome is SUCCESS, not failure.** Every other mutation here breaks a test; this one makes a refused path succeed, and the finding is that it succeeds *silently*. Do not report it as a passing gate. @@ -842,9 +967,10 @@ figure the document had outgrown. This is the same drift as §3's header and gat 1: **three independent stale counts of the same three lists.** Prefer "every item in §N" to a number.* -1. **Every mutation in §4** — currently **seven** (M1–M7), each with verbatim - output. **M4 is a recorded prohibition** (observed to compile, then reverted) - and **M7 is a demonstration whose expected outcome is success**. Neither is a +1. **Every mutation in §4** — currently **eight** (M1, M2, M3, M4, **M5a**, + **M5b**, M6, M7), each with verbatim output. *(M5 split in review round 2.)* + **M4 is a recorded prohibition** (observed to compile, then reverted) and + **M7 is a demonstration whose expected outcome is success**. Neither is a passing guard; do not report them as one. 2. **Every gate item in §5** — currently **eight** (1, 2, 3, 4, 5, 6, 6a, 7), each with the command that produced it. @@ -863,4 +989,9 @@ in §N" to a number.* 8. **Confirmation that the pin-3c suspension marker naming this contract is gone from `testkit/src/roundtrip.rs`.** If it is still in the tree, obligation 3's restoration did not happen, whatever the prose says. -9. Anything contradicting this contract. +9. **The `serialize.rs:157` dead branch**, recorded as a finding and **not + repaired** — see the note under M7. +10. **M6's replaced second half**, with the reachability result stated: that no + caller can hold an open `Bundle` with a stale *inherited* base, so pin 3a's + scope is forced rather than chosen. +11. Anything contradicting this contract. diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index 675e0bc..4f1adde 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -122,5 +122,5 @@ evidence in isolation. | P13-S23 | **No filed candidate owns "place any anchor pair on a common timeline and measure musical distance along it" — P13-S18 previously mis-cited a narrower capability as its gate.** Two disjoint deficiencies, both owned by this candidate. (1) **No ordering.** The pair is not comparable under any of `measure20_comparable_order`'s five shapes c1-c5 (`invariants.rs:2457`) at all — whether the failure is in the **referent** (distinct `Event` ids; distinct `Measure` ids outside c3's `Start`+`Zero` restriction), the **variant or selector** (`Event` against `Measure`, `Measure` against `Region`, differing `pos`/`edge`), or the **clock** (`Musical` against `WallClock`, including inside `measure20_offset_order`, `:2419`) — this is what invariant 20's A4 and B4 are made of. (2) **Ordering without a usable delta.** The pair IS comparable and still yields no musical distance: c3 supplies a vector index (an order, never a distance), and c5 compares two `WallClock`s, and `measure20_musical_delta` (`:2522`) never returns a `WallClock` delta (`:2527`) — this is what invariant 20's B5 is made of. Scoping this as merely "anchors of differing shapes" or "not directly comparable under c1-c5" would exclude B5 entirely — S5 (distinct-id `Measure` `Start`/`Zero`) is c3-comparable and S1 (`WallClock` measures, `WallClock` meter changes) is c5-comparable, and both still reach B5 — an earlier draft of this filing made exactly that narrower mistake. **Explicitly broader than P11-C5**: P11-C5 (`PASS11_WORKLIST.md:159`) is a re-anchoring proximity metric that resolves "when the graph-mutation phase tracks resolved positions", and covers narrowly the two-distinct-`Event`s case (`CONTRACT_GENESIS_G3B_MEASURE.md:223`, `effect.rs:139`-`:142`'s `PositionOutsideRegion` Reserved note); P13-S23 is the timeline itself, whatever positions get placed on it. Names its dependents: invariant 20's A4, B4 and B5, and `PositionOutsideRegion`'s Reserved status | `spec/CONTRACT_P13S18_MATRIX.md` pin 10 (filed 2026-07-31 during the same rung that corrected P13-S18's over-narrow P11-C5 citation) | **open.** No code owed by this rung. Closing it needs the deferred common-timeline/duration machinery — once a `Measure` end, a distinct-id `Measure`/`Event` referent, or an `Event` position on a wall-clock-placed region can be placed on a common timeline with a musical distance, invariant 20's A4/B4/B5 residue and `PositionOutsideRegion`'s Reserved status shrink together | | P13-S25 | **The committed decode corpus's numbered tag rows lock byte→byte, not variant→byte — one row already has the property the other thirty-nine lack.** `ops/src/vectors.rs:206`–`:209` emits one row per tag as `format!("tag_{:02}", tag.discriminant())` carrying `[discriminant]`: **both the name and the payload derive from the value alone**, so `tag_32` asserts that `0x20` round-trips and never that `SetCanvasLayoutDefaults` is 32. The `Registered` row (`:210`–`:217`) is different — its name is the hard-coded string `"registered"` while its bytes are computed from the variant, so the frozen literal at `spec/vectors/decode_vectors.txt:80` binds the association. **Disposition B of P13-S22:** give the numbered rows the same property. It **does** catch the coordinated permutation — by exactly the `Registered` mechanism, with the committed text serving as the independent statement — and it propagates the property to every implementation that reads the cross-impl corpus, which an in-crate Rust test cannot do | `spec/CONTRACT_P13S22_TAGLOCK.md` (disposition B, considered and deferred during the 2026-07-31 ruling; filed rather than left as a closing remark, per the same discipline that moved P13-S22 out of P13-S15's resolved row) | **open. Complementary to P13-S22, not a replacement for it, and not a re-litigation of it.** P13-S22 landed disposition A (`tag_wire_discriminants_are_golden`, `payload.rs:2730`), which fails **by variant name inside the crate**. B cannot supply that: its failure is still *"spec/vectors/decode_vectors.txt is stale. Regenerate: …"* (`testkit/src/vectors.rs:224`) — the misleading diagnosis P13-S22 was filed about — even though the diff text would now name variants. **What B buys is cross-implementation reach; what it costs is churn in a committed artifact other implementations pin.** Both are wanted; neither substitutes for the other. Sequencing note: run B's own signing mutation as the coordinated permutation (literals *and* declaration lines), since the literal-only form is caught today by row ordering and proves nothing | | P13-S26 | **A doc comment in shipped code claims a specification repair that never landed, and the claim is guarded on the code side and nowhere on the specification side.** `crates/epiphany-core/src/invariants.rs:69`–`:71` enumerates invariant 10's four reference classes and states that *“genesis tranche G3a repairs this prose to name what the check body already enforced”*. **It did not.** `core_spec.tex:6570`–`:6572`, the normative enumeration item 10, still reads only *“Every cross-cutting structure's references resolve to extant objects in the graph, except where explicit re-anchoring rules permit transient dangling states during edits”* — naming neither a staff's declared instrument, a staff's group, a staff group's members, a part's staves, a view's active layers, nor any of the meter/time-signature references the Rust doc lists and the check body enforces. The repair landed in the Rust doc comment only. **The asymmetry is the defect's sharp edge:** the Rust doc block is protected by a grep-assert, `t12_invariant_10_doc_comment_names_the_four_reference_classes` (`invariants.rs:4554`, needles at `:4562`–`:4566`), so the side that is *wrong about the other* is the side that is **locked**, while the side that is actually stale is unguarded | this file (found 2026-07-31 during P13-S16 reconnaissance, while verifying that row's invariant-10 citations; no ledger entry covered it) | **open.** **Not a live incorrectness** — the check body is correct and enforces every class; only the normative prose under-describes it, and only the doc comment lies about that. **A P13-S9 instance**, and filed deliberately as one: the loud form (a dangling citation) is caught by `requirement_labels.rs`, and this quiet form — a *true-sounding claim about another document's state* — is caught by nothing. **`invariants.rs:69`–`:71` MUST NOT be “corrected” on its own.** It is currently the only artifact in the tree pointing at the `core_spec.tex` gap; softening the Rust claim in isolation would make the specification defect invisible and convert a caught defect into an uncaught one — which is P13-S9's stated failure mode verbatim. **Repair both sides in one rung**, and consider whether the LaTeX enumeration deserves the grep-assert its Rust mirror already has | -| P13-S27 | **The reduction-algorithm-version machinery is self-referential, so the one check that would detect a canonical-semantics change necessarily passes.** `core_spec.tex:11614`–`:11617` is normative — *"Snapshots produced under an earlier algorithm version cannot be used as canonical bases under a later one without rebuilding"* — and `:14369`–`:14372` states that replicas at differing versions *"may produce different canonical states from the same operation set."* The machinery to enforce it appears to exist: `ReductionAlgorithmVersion` (`bundle/src/ids.rs:291`) is a superblock wire field (bytes `68..72`, `superblock.rs:20`); `reduction_version_for` (`bundle.rs:989`) sets a new superblock's value; and `open` (`bundle.rs:396`–`:399`) rejects a mismatch. **But the writer sources the value from the canonical base's own self-report** (mapping the base's `reduction_algorithm_version` through `unwrap_or_default()`), **and the reader compares it only against the superblock that value seeded.** Nothing compares either against the semantics the running implementation actually implements. **The check is not vacuous** — it catches a corrupt or tampered base whose version disagrees with its superblock — but it **necessarily passes for a conformingly propagated stale base**, which is precisely the case the requirement exists to prevent. Supporting: **no constant or accessor anywhere names the implementation's current reduction semantics**, and `ids.rs:288`–`:289` states that *"the algorithm catalog itself lives in `epiphany-ops`"* while nothing of the kind exists in that crate — **a second instance of P13-S26's pattern**, a doc comment asserting a false fact about another module | `spec/CONTRACT_P13S16_PROJECTION.md` pin 0 (found 2026-07-31 while scoping P13-S16, which is a canonical reduction-semantics change and therefore the first rung to need this guarantee; filed in the same ledger edit as the row it blocks) | **UNBLOCKED 2026-08-07 — the format-epoch rung landed; dispatchable, and still blocking P13-S16.** (Was: open, BLOCKED on P13-S28.) **Scoped 2026-07-31 as `spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md` (DRAFT, not dispatchable).** Rulings taken: a typed `BundleCapabilities` required at both `Bundle::open` and `Bundle::create` and carried on the `Bundle` — no default, so every caller states the semantics it implements — and outright rejection on mismatch via a new `CanonicalBaseRequiresRebuild` error, not read-only and not an integrity anomaly. Storing the capability keeps all 57 `commit` sites unchanged; only `open` (57 sites) and `create` (32) move. **The scoping also falsified this row's first reading that the writer path was test-only:** `epiphany-textproj`'s `serialize_document` (`serialize.rs:119`) and `project.rs:936` are production paths that copy a base's `reduction_algorithm_version` verbatim into a fresh `SnapshotRef`, which `commit_versioned` then stamps into the superblock (`bundle.rs:798`) — so production mints self-consistent stale documents **without ever calling `open`**, and the capability must govern writers too. **What blocks it:** contract pin 2a. Baseline authority `0` does not preserve the corpus (`serialize.rs:327` stamps `1` and round-trips it; `vectors.rs:353`/`:363` likewise), and once P13-S16 moves the authority to `1`, a pre-S27 base that happens to carry `1` is **indistinguishable from a legitimately rebuilt one** — a raw `u32` carries no provenance. Four dispositions are recorded there; `FORMAT_MINOR` as a provenance carrier was proposed and **rejected** (the header never changes after creation, `core_spec.tex:10799`, so a legacy bundle committing a freshly validated base keeps its old minor forever; and a minor change may only append append-safe discriminants, `:12258`, not alter acceptance semantics). The surviving requirement — provenance must ride a container property **old readers cannot silently accept** and **a later commit cannot inherit unchanged** — is a format-epoch design, filed as **P13-S28**. **Scope of the claim, deliberately narrow:** this establishes that the **current implementation** has no detection mechanism. It does **not** establish that no reduction-semantics change in the project's history was ever detectable — that needs a history audit not yet done, and the stronger sentence is deliberately not written here. **What closing it requires:** an authority naming the semantics this build implements, and a rejection-or-rebuild path when a base disagrees with it. Until then any rung changing canonical reduction semantics can record its break in prose but cannot make stale bases unusable — which is why P13-S16's contract is complete, ratifiable as a plan, and **not dispatchable**. **Method note:** an earlier draft of S16's pin 0 claimed no writer path existed at all. That was false, and the way it was false is the point — the search behind it looked for `ReductionAlgorithmVersion(` constructor calls, which cannot find a path that propagates an existing value without constructing one. The instrument could not observe the thing it was used to rule out. **UNBLOCKED 2026-08-07:** the format-epoch rung landed and its pin 8 **resolves pin 2a** — reduction-version authority is meaningful only in major-1 containers, so legacy bases are refused by container epoch and never by version arithmetic. The collision pin 2a identified never has to be adjudicated: a pre-S27 base carrying `1` and a rebuilt S16 base carrying `1` are indistinguishable as numbers but can never meet, because the former exists only in a major-0 container, refused at the epoch boundary before any version is compared. The `u32` never has to carry provenance because the container does. **S27 now additionally owes three inherited items** (both interim refusals converted to validation, M8's deferred laundering demonstration, pin 3c's two suspended conformance assertions), recorded in its contract as required tests. **RATIFIED 2026-08-07 after review round 1** — run because this contract had reached "dispatchable" with **zero** ratification rounds on record, against the standing rule that contracts go through adversarial review before dispatch. Round 1 returned **nine findings, four blocking**, all now carried in the contract. **Correcting this row's own preceding clause:** the three inherited items were *not* all "recorded as required tests" — obligation 2, M8's laundering demonstration, appeared in **neither** the contract's test section nor its mutation plan, while that section's preamble claimed all of them were tests. It is now **M7**, and ruled a **mutation** rather than a capability restoration: the format rung's text refusal is permanent, `COMPANION_VERSION` stays 0.14.0, and the text-projection corpus keeps `canonical_bases` reach 0. The other blocking three: §0.4's `commit`-site count counted a same-named method in `epiphany-editor-core`, **a crate with no `epiphany-bundle` dependency at all** — the third instrument failure recorded in that one section; three independent stale list-counts (the test-section header, gate 1, and three report items) all naming figures the document had outgrown; and `testkit/tests/requirement_labels.rs` missing from the touch table while pin 9 may move `CORE_REQUIREMENT_COUNT` 213 → 214 — **the escapee `CLAUDE.md` names by name**, which also escaped the format-epoch rung. Non-blocking: locator drift since `381c498` (`bc06706` grew `bundle.rs` by 338 lines; pin 5's own `:396`–`:399` confirmed unmoved), pin 2a's corpus evidence superseded by the 2 → 0 rebuild, `Bundle::open(` 57 → **60**, gate 6a's scope widened to `epiphany-testkit`, and a missing **commit-side positive** test now added as test 8. **Pins are frozen; dispatchable** | +| P13-S27 | **The reduction-algorithm-version machinery is self-referential, so the one check that would detect a canonical-semantics change necessarily passes.** `core_spec.tex:11614`–`:11617` is normative — *"Snapshots produced under an earlier algorithm version cannot be used as canonical bases under a later one without rebuilding"* — and `:14369`–`:14372` states that replicas at differing versions *"may produce different canonical states from the same operation set."* The machinery to enforce it appears to exist: `ReductionAlgorithmVersion` (`bundle/src/ids.rs:291`) is a superblock wire field (bytes `68..72`, `superblock.rs:20`); `reduction_version_for` (`bundle.rs:989`) sets a new superblock's value; and `open` (`bundle.rs:396`–`:399`) rejects a mismatch. **But the writer sources the value from the canonical base's own self-report** (mapping the base's `reduction_algorithm_version` through `unwrap_or_default()`), **and the reader compares it only against the superblock that value seeded.** Nothing compares either against the semantics the running implementation actually implements. **The check is not vacuous** — it catches a corrupt or tampered base whose version disagrees with its superblock — but it **necessarily passes for a conformingly propagated stale base**, which is precisely the case the requirement exists to prevent. Supporting: **no constant or accessor anywhere names the implementation's current reduction semantics**, and `ids.rs:288`–`:289` states that *"the algorithm catalog itself lives in `epiphany-ops`"* while nothing of the kind exists in that crate — **a second instance of P13-S26's pattern**, a doc comment asserting a false fact about another module | `spec/CONTRACT_P13S16_PROJECTION.md` pin 0 (found 2026-07-31 while scoping P13-S16, which is a canonical reduction-semantics change and therefore the first rung to need this guarantee; filed in the same ledger edit as the row it blocks) | **UNBLOCKED 2026-08-07 — the format-epoch rung landed; dispatchable, and still blocking P13-S16.** (Was: open, BLOCKED on P13-S28.) **Scoped 2026-07-31 as `spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md` (DRAFT, not dispatchable).** Rulings taken: a typed `BundleCapabilities` required at both `Bundle::open` and `Bundle::create` and carried on the `Bundle` — no default, so every caller states the semantics it implements — and outright rejection on mismatch via a new `CanonicalBaseRequiresRebuild` error, not read-only and not an integrity anomaly. Storing the capability keeps all 57 `commit` sites unchanged; only `open` (57 sites) and `create` (32) move. **The scoping also falsified this row's first reading that the writer path was test-only:** `epiphany-textproj`'s `serialize_document` (`serialize.rs:119`) and `project.rs:936` are production paths that copy a base's `reduction_algorithm_version` verbatim into a fresh `SnapshotRef`, which `commit_versioned` then stamps into the superblock (`bundle.rs:798`) — so production mints self-consistent stale documents **without ever calling `open`**, and the capability must govern writers too. **What blocks it:** contract pin 2a. Baseline authority `0` does not preserve the corpus (`serialize.rs:327` stamps `1` and round-trips it; `vectors.rs:353`/`:363` likewise), and once P13-S16 moves the authority to `1`, a pre-S27 base that happens to carry `1` is **indistinguishable from a legitimately rebuilt one** — a raw `u32` carries no provenance. Four dispositions are recorded there; `FORMAT_MINOR` as a provenance carrier was proposed and **rejected** (the header never changes after creation, `core_spec.tex:10799`, so a legacy bundle committing a freshly validated base keeps its old minor forever; and a minor change may only append append-safe discriminants, `:12258`, not alter acceptance semantics). The surviving requirement — provenance must ride a container property **old readers cannot silently accept** and **a later commit cannot inherit unchanged** — is a format-epoch design, filed as **P13-S28**. **Scope of the claim, deliberately narrow:** this establishes that the **current implementation** has no detection mechanism. It does **not** establish that no reduction-semantics change in the project's history was ever detectable — that needs a history audit not yet done, and the stronger sentence is deliberately not written here. **What closing it requires:** an authority naming the semantics this build implements, and a rejection-or-rebuild path when a base disagrees with it. Until then any rung changing canonical reduction semantics can record its break in prose but cannot make stale bases unusable — which is why P13-S16's contract is complete, ratifiable as a plan, and **not dispatchable**. **Method note:** an earlier draft of S16's pin 0 claimed no writer path existed at all. That was false, and the way it was false is the point — the search behind it looked for `ReductionAlgorithmVersion(` constructor calls, which cannot find a path that propagates an existing value without constructing one. The instrument could not observe the thing it was used to rule out. **UNBLOCKED 2026-08-07:** the format-epoch rung landed and its pin 8 **resolves pin 2a** — reduction-version authority is meaningful only in major-1 containers, so legacy bases are refused by container epoch and never by version arithmetic. The collision pin 2a identified never has to be adjudicated: a pre-S27 base carrying `1` and a rebuilt S16 base carrying `1` are indistinguishable as numbers but can never meet, because the former exists only in a major-0 container, refused at the epoch boundary before any version is compared. The `u32` never has to carry provenance because the container does. **S27 now additionally owes three inherited items** (both interim refusals converted to validation, M8's deferred laundering demonstration, pin 3c's two suspended conformance assertions), recorded in its contract as required tests. **RATIFIED 2026-08-07 after review round 1** — run because this contract had reached "dispatchable" with **zero** ratification rounds on record, against the standing rule that contracts go through adversarial review before dispatch. Round 1 returned **nine findings, four blocking**, all now carried in the contract. **Correcting this row's own preceding clause:** the three inherited items were *not* all "recorded as required tests" — obligation 2, M8's laundering demonstration, appeared in **neither** the contract's test section nor its mutation plan, while that section's preamble claimed all of them were tests. It is now **M7**, and ruled a **mutation** rather than a capability restoration: the format rung's text refusal is permanent, `COMPANION_VERSION` stays 0.14.0, and the text-projection corpus keeps `canonical_bases` reach 0. The other blocking three: §0.4's `commit`-site count counted a same-named method in `epiphany-editor-core`, **a crate with no `epiphany-bundle` dependency at all** — the third instrument failure recorded in that one section; three independent stale list-counts (the test-section header, gate 1, and three report items) all naming figures the document had outgrown; and `testkit/tests/requirement_labels.rs` missing from the touch table while pin 9 may move `CORE_REQUIREMENT_COUNT` 213 → 214 — **the escapee `CLAUDE.md` names by name**, which also escaped the format-epoch rung. Non-blocking: locator drift since `381c498` (`bc06706` grew `bundle.rs` by 338 lines; pin 5's own `:396`–`:399` confirmed unmoved), pin 2a's corpus evidence superseded by the 2 → 0 rebuild, `Bundle::open(` 57 → **60**, gate 6a's scope widened to `epiphany-testkit`, and a missing **commit-side positive** test now added as test 8. **REVIEW ROUND 2, 2026-08-07, against the frozen contract: six further findings, four blocking — and round 1's ratification was therefore premature.** (1) The call-site correction had been applied to §0.4 only, leaving the "Rung type" paragraph at **57** and touch row 2 claiming `bundle.rs` has **35** opens — a figure that was never `bundle.rs` alone and is stale besides — which made the required reconciliation impossible. (2) §0.4 called `project.rs:936` a **production** bundle writer; `#[cfg(test)]` starts at `:630` and every `Bundle` call in that file is below it, so the writer-path correction stands on `serialize.rs` alone. (3) **M5 was unexecutable**: `serialize_document` refuses bases at `serialize.rs:151`, so its output is base-free, and pin 5 with test 4 require base-free bundles to open at *any* authority — split into **M5a**/**M5b**. (4) **M6's second half was unexecutable**: `open` rejects a stale base, `create` rejects a base-bearing manifest (`bundle.rs:234`), and `commit` validates what it emits, so no caller can hold an open `Bundle` with a stale *inherited* base — replaced by broadening rather than narrowing, with the unreachability itself reported as the stronger result. Non-blocking: pin 3a's justification (*"production code mints a self-consistent stale document"*) is **false in-tree** — zero production paths stage a base — so it now rests on guarding the public `commit_versioned` API; and `serialize.rs:157` is dead code orphaned by the `:151` guard, recorded and explicitly **not** repaired here. **Two of round 2's findings were introduced by round 1** — ruling M7's refusal permanent is what made M5 unexecutable, and test 8 was added without re-deriving M6 against the same reachability. **Method note: an amendment is a change to the system, not a patch to a line**; a round must re-derive every mutation against every ruling the previous round made. **Round 3 is warranted before dispatch — the defect rate has not fallen (9, then 6), and "dispatchable" is a claim requiring evidence of convergence rather than a status reached by running out of findings** | | P13-S28 | **No container property distinguishes a document produced under a validated reduction authority from one produced before any authority existed — and the two candidates that look like they would, cannot.** P13-S27 installs an authority and validates it at read and write time, but cannot state what to do with a canonical base that predates the authority: a raw `ReductionAlgorithmVersion` is a bare `u32` (`bundle/src/ids.rs:291`) carrying no provenance, and the text-projection parser accepts an unbounded one from a document (`textproj/src/parse.rs:591`), so no numeric convention — including a deliberately high epoch — is safe from a hand-authored or third-party document declaring it. **`FORMAT_MINOR` does not work either, for two independent reasons:** the header *"never changes after the file is created"* (`core_spec.tex:10799`–`:10800`) and `commit_versioned` publishes only a superblock (`bundle.rs:791`), so a legacy bundle that commits a base S27 just validated keeps its old minor **permanently** — rejecting minor-≤1 bases would then reject a base the authority itself accepted, and accepting them leaves S16's `1` ambiguous; and `core_spec.tex:12258`–`:12262` limits a minor change to appending append-safe discriminants and calls it backward-compatible, whereas making a previously-valid base newly rejectable is a **semantic acceptance change**, with current readers ignoring minor entirely (`header.rs:119` gates on major alone) so the boundary would bind only readers that already comply. **The requirement that survives:** provenance MUST ride a container property that **old readers cannot silently accept** and that **a later commit cannot inherit unchanged** | `spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md` pin 2a (filed 2026-07-31; the disposition S27 cannot make from inside itself) | **IMPLEMENTED 2026-08-07 (`bc06706`, fix `be244df`). Was the critical path; both P13-S27 and P13-S16 were blocked on it.** **This rung must own all five, and none may be deferred into S27:** (1) an **old-reader rejection boundary** — pre-boundary readers must fail closed rather than silently open a document whose safety check they do not run; (2) **provenance that survives commits correctly**, i.e. is not inherited unchanged by a later generation and is not lost by one; (3) **legacy-base rebuild/repack behaviour**, stated for real artifacts rather than assumed away; (4) **every writer path, including text projection** — `serialize_document`, `project.rs`, and the committed `.txt` vectors, since a text document can declare any version; (5) **the exact format-version and compatibility consequences**, most plausibly a **major**-version boundary or a generation-scoped attestation paired with an incompatibility boundary. **Not a sub-pin of S27 and must not drift into it** — S27's pin 2a carries an explicit prohibition against being amended into a disposition without its own ratification round. **Scoped and RATIFIED 2026-07-31 as `spec/CONTRACT_FORMAT_EPOCH_MAJOR1.md`** after four adversarial review rounds — 11 pins, 11 tests, 11 mutations, 15 touch rows, 7 gate items. **This row is now a dependency record only; the work lives there and P13-S28 does not execute as a Pass 13 rung.** Rulings taken: the carrier is the **format major** (`FORMAT_MAJOR` 0 → 1, `FORMAT_MINOR` 1 → 0), decoded three ways through a named `FormatEpoch` rather than a bool, with **no** generation-scoped attestation in this epoch; legacy resolves to **hard rejection, not read-only**; and an eight-row epoch matrix in which a major-0 bundle with no base may open, one carrying a base is rejected, and one attempting to *add* a base is rejected and told to repack — **the non-inheritance rule that `FORMAT_MINOR` could not express**. All five things this row required the rung to own are pinned: old-reader boundary (pin 2), commit-surviving provenance (pin 3), legacy repack (pins 4, 5), every writer path including text projection (pins 3b, 6), and the exact format/compatibility consequences (pins 1, 7). **Three findings from the review rounds that changed the rung's shape**, none of them visible at filing: (1) **it cannot stamp major 1 before S27's writer enforcement exists**, so pin 3a temporarily refuses *both* boundaries — opening a major-1 bundle already carrying a base, and committing one into it — through a third, temporary `ReductionAuthorityUnavailable` error that must name P13-S27 and must **not** name repack; (2) **text projection launders provenance straight through the boundary** (`serialize_document` stages a carried base into a fresh bundle and `build_manifest` writes it), resolved as **symmetric document-level refusal** — projection, parsing and a new dedicated `SerializeError` variant, none of which existed to be "retained" — which forces `COMPANION_VERSION` 0.13.0 → **0.14.0** and rebuilds the committed corpus to **20 vectors, ten rejection classes, `canonical_bases` reach 2 → 0**, a real and stated capability loss; (3) **corruption precedence binds in both epochs** — a corrupt major-1 base must still fail as malformed, never as the *temporary* authority error a user would reasonably retry. **IMPLEMENTED 2026-08-07** — amended once before dispatch (pin 3c, touch rows 10/11, gate 8) after reconnaissance found pin 3a's refusals reaching a conformance criterion through a file the touch table did not carry. All 11 tests landed under their contract names, all 11 mutations run and observed, workspace green at 1569. **P13-S27 is unblocked and P13-S16 remains blocked on S27** — pin 8 resolved S27's open pin 2a (legacy bases are refused by container epoch, never by version arithmetic), and S27 additionally inherits three obligations recorded in its own contract: converting **both** interim refusals to validation, M8's deferred laundering demonstration, and pin 3c's two suspended conformance assertions. **Two touch-table gaps found during execution, both of the same shape** — a `.tex` requirement addition moves hardcoded counts in `testkit/tests/requirement_labels.rs`, and a companion-version bump moves a second normative version literal spelled `version~0.13.0` rather than `(0 13 0)`; neither file was in any touch table, and the second was caught only because `requirements_name_only_this_companion_version` exists. **A third gap was caught in review, after the rung was committed:** pin 3b's projection refusal had been implemented only on the **bundle** side (`document_from_bundle`), leaving the public `project_text_document` free to emit a `(canonical-base ...)` line for a directly constructed `TextDocument` — text the parser then rejects. A projector that can produce what the parser refuses is exactly the asymmetry pin 3b exists to close, and the refusal is unreachable through a `Bundle` during the interval anyway, so the *only* reachable half was the unguarded one. The public projector now returns `Result` and refuses; a crate-private `render_text_document` retains the base spelling for the one legitimate caller, the `canonical_base_present` negative vector. **The lesson is the rung's own recurring one:** a guard placed on the path that happened to be named, rather than on every path a caller can reach |