S16 draft amendment 1: fourteen findings from ratification reconnaissance
Fourteen findings, thirteen blocking, against the draft BEFORE its first ratification round. Nine from the recon pass, five from a second sweep of the same defect classes. The contract is a DRAFT, so these are edits to an unratified plan, not amendments to frozen pins. Root cause, and the one that changes the rung's shape: invariant 21 is a TWO-crate change. violating_score (epiphany-core/src/generators.rs:498) matches GraphInvariant exhaustively, so the new variant does not compile without an arm, and four all()-driven tests (:991, :1004, :1025, :1042) then require a real generator rather than a stub. The contract had treated the enum extension as local to invariants.rs. Nothing in its §0 inspection would have surfaced this -- it appears at compile time, after execution begins. Touch table gained five rows: - epiphany-ops/src/lib.rs -- the bump and its Bumps entry. The rung's defining act had no pin, no touch row, no gate and no report item; it existed only as a note inside pin 0's discharge. Now pin 12, touch row 7, gate 10, item 2b. - epiphany-core/src/generators.rs -- the root cause above. - epiphany-testkit/src/roundtrip.rs and epiphany-textproj/src/serialize.rs -- S27's two tripwires. Test 10b panics by design once the authority moves; test 10a asserts the literal 0 and its own doc says it is expected to fail when S16 bumps. Both fail gate 1 with no row to fix them in -- the same shape as S27's own gminor.rs failure. Gate 11 requires they be updated, not silenced: a tripwire accepting both values rebuilds the tautology S27 existed to remove. - requirement_labels.rs -- conditional, the escapee CLAUDE.md names by name. Pin 10a now forces an explicit decision on whether pin 6 or pin 10 mints a label; this rung touches both counted documents, and all three counters move if either does. Gates: 2 and 3 now pin +1.95.0 (CI gates on it; this machine defaults to 1.97.1). Gate 3 formatted two crates of four and would have reported clean over the two the new rows added. Gate 1 gained the 1577/0/0 baseline, three delta buckets, and a 0-ignored requirement. Gate 4's "exactly §2" was the formulation S27's round 17 found unsatisfiable with a conditional row. Mutations: M1, M2 and M4 accepted "the named test fails" as their whole signature; each now names the behaviour the mutated build produces -- the applied spurious mint, the still-empty members, the re-carry misverdict. M3, M5, M6 and M9 already met the standard. M7 covered two independently guarded doc blocks while reverting one, so it could pass with the other guard still weak; split into M7a and M7b, each quoting its own needle's non-match. Locators: pin 8's four tests were identified by INTERIOR line numbers, a dozen lines into each body, anchored to nothing searchable -- now named. t6/t7/t9 re-derived to :16158/:16231/:16461, with the trap recorded that reduce.rs has two t6/t7 families and grepping "fn t6" lands on the wrong one. New §4a, landing obligation: the bump falsifies live statements in CLAUDE.md:106 and the handoff's POST-S27 block. Both are explicitly NOT staged during execution -- staging them would assert the rung had landed while it awaited acceptance -- and are required as post-acceptance reconciliation the report must list as outstanding. Pin 11's ledger row is different and is staged: a ledger records what a rung did; those two state what is true now. Report item 2d requires execution to determine whether shrink() also matches GraphInvariant exhaustively. Deliberately not guessed -- guessing about an exhaustive match is what produced the root-cause finding. Findings 5-8 are all defects S27 had already found and fixed in its own gate set; this contract predates those corrections and inherited none of them. The next contract drafted here should start from S27's §5. No implementation work has begun. Still DRAFT, still unratified. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
This commit is contained in:
parent
d2e43b4204
commit
d06e2f7266
|
|
@ -15,9 +15,45 @@ ratifiable as a *plan* and has **not been through adversarial review rounds**.
|
|||
contract came to be ratified after a single round and then have that ratification
|
||||
withdrawn — see its status block.
|
||||
|
||||
**This rung's first act is bumping the authority to `1`**, because it changes
|
||||
`CreateStaffGroup`'s reduction verdict. That bump is the discipline S27 installed: no
|
||||
mechanism can detect a semantics change, so the bump is the entire guarantee.
|
||||
**This rung's first act is bumping the authority to `1`** (**pin 12**), because it
|
||||
changes `CreateStaffGroup`'s reduction verdict. That bump is the discipline S27
|
||||
installed: no mechanism can detect a semantics change, so the bump is the entire
|
||||
guarantee.
|
||||
|
||||
### Draft amendment 1 — 2026-08-09, on ratification reconnaissance. NOT a review round.
|
||||
|
||||
**Fourteen findings, thirteen blocking**, against the draft **before** its first
|
||||
ratification round. Nine came from the reconnaissance pass, five from a second sweep of
|
||||
the same defect classes. **The contract is a DRAFT, so these are edits, not amendments to
|
||||
frozen pins** — the distinction S27's status block draws, applied here.
|
||||
|
||||
| # | Finding | Disposition |
|
||||
|---|---|---|
|
||||
| **1** | **§2 omitted `epiphany-ops/src/lib.rs`**, though the rung's defining act is bumping the authority there. The bump had **no pin, no touch row, no gate and no report item** — it lived only in pin 0's discharge note | **Pin 12** added, with **touch row 7**, **gate 10**, **report item 2b** |
|
||||
| **2** | **Invariant 21 is a TWO-crate change, not one.** `violating_score` (`generators.rs:498`) matches `GraphInvariant` **exhaustively** — invariant 21 does not compile without an arm — and four `all()`-driven tests then require a **real** generator | **Touch row 8** added, with the consumer surface enumerated. **This is the amendment's root cause**; everything else is bookkeeping by comparison |
|
||||
| **3** | **S27's two tripwires fail at gate 1 with no touch row.** `roundtrip.rs` test 10b `panic!`s by design once the authority moves; `serialize.rs` test 10a asserts the literal `0` and its own doc says it *is expected to fail when S16 bumps* | **Touch rows 9 and 10**, plus **gate 11** requiring they be updated and not silenced |
|
||||
| **4** | **`requirement_labels.rs` — the escapee `CLAUDE.md` names by name — was absent**, and the contract never decided whether pin 6 or pin 10 mints a label. It touches **both** counted documents | **Pin 10a** forces the decision; **touch row 11** conditional; **report item 2c**. All three counters named, per S27's finding |
|
||||
| **5** | **Gates 2–3 pinned no toolchain**, in a repo whose CI gates on **1.95.0** while this machine's default is **1.97.1** | Both pinned |
|
||||
| **6** | **Gate 3 formatted two crates of four** — and rows 9–10 added the other two, so it would have reported clean over unformatted code | Expanded to ops, core, textproj, testkit |
|
||||
| **7** | **Gate 1 had no baseline and no ignored requirement** | Baseline **1577 / 0 / 0**, three delta buckets, ignored MUST be 0 |
|
||||
| **8** | **Gate 4 said "exactly §2"** — the formulation S27's round 17 found **unsatisfiable** with a conditional row, and row 11 is now conditional | Subset both ways, with the unused row named in the report |
|
||||
| **9** | **M1, M2, M4 accepted "the test failed"** as their whole signature | Each now names the **behaviour** the mutation produces. M3, M5, M6, M9 already met the standard |
|
||||
| **10** | **M7 covered two independently guarded doc blocks but reverted "one doc comment"** — it could pass while the other guard stayed weak | Split into **M7a** and **M7b**, each quoting its own needle's non-match |
|
||||
| **11** | **Pin 8 identified four tests by INTERIOR line numbers** (`:16838` etc.), roughly a dozen lines into each body — anchored to nothing searchable | All four **named**, with `fn` lines given second |
|
||||
| **12** | **`t6`/`t7`/`t9` locators stale** | Re-derived to `:16158`, `:16231`, `:16461`, with the **two-`t6`-families trap** recorded |
|
||||
| **13** | **The bump falsifies live statements in `CLAUDE.md` and the handoff** | **§4a** added: explicitly **not staged** during execution — staging them would assert the rung had landed while it awaited acceptance — and required as a post-acceptance reconciliation the report must list as outstanding |
|
||||
| 14 | **`shrink` also takes `GraphInvariant`; whether it matches exhaustively was not established** | **Report item 2d** requires execution to determine it. **Deliberately not guessed** — guessing about an exhaustive match is what produced finding 2 |
|
||||
|
||||
**Finding 2 is the one that changes the rung's shape.** The others make an existing plan
|
||||
checkable; this one says the plan was scoped to the wrong number of files. **An enum
|
||||
extension in a crate with a generated exhaustive consumer is never local**, and nothing
|
||||
in the contract's own §0 inspection would have surfaced it — it appears at compile time,
|
||||
after execution begins.
|
||||
|
||||
**Findings 5–8 are all defects S27 had already found and fixed in its own gate set.**
|
||||
This contract predates those corrections and inherited none of them. **A ratified
|
||||
contract's gate section is reusable knowledge**, and the next contract drafted here
|
||||
should start from S27's §5 rather than from an older template.
|
||||
|
||||
> **The original status, retained:** *DRAFT — BLOCKED on P13-S27. Not executable as
|
||||
> written. Pin 0 exposes that no authority defines the implementation's current
|
||||
|
|
@ -312,11 +348,21 @@ written into the ledger.
|
|||
entire guarantee — so the bump is this rung's obligation and nothing will catch its
|
||||
absence.
|
||||
|
||||
> **Line-number citations in this contract predate S27 and have NOT been re-derived.**
|
||||
> S27 changed `bundle.rs` by 795 lines, so `bundle.rs:989`, `:396` and `ids.rs:288`
|
||||
> above — and every other `bundle.rs` reference in this document — are stale as
|
||||
> locators even where the claim about them is historical. **Re-deriving them is part of
|
||||
> ratification**, not something this supersession did.
|
||||
> **Line-number citations in this contract predate S27 and are only PARTLY
|
||||
> re-derived.** S27 changed `bundle.rs` by 795 lines, so `bundle.rs:989`, `:396` and
|
||||
> `ids.rs:288` above — and every other `bundle.rs` reference in this document — remain
|
||||
> stale as locators even where the claim about them is historical.
|
||||
>
|
||||
> **Draft amendment 1 re-derived the ones that name executable targets:** `t6`
|
||||
> `:16154`→**`:16158`**, `t7` `:16229`→**`:16231`**, `t9` `:16454`→**`:16461`**, and
|
||||
> pin 8's four interior line numbers replaced by test **names**. **The rest are not
|
||||
> done** and finishing them is ratification work.
|
||||
>
|
||||
> **A trap the re-derivation found, recorded so the next pass does not fall into it:**
|
||||
> `reduce.rs` contains **two `t6`/`t7` families** — `t6_undo_restores_the_chain_...`
|
||||
> (`:15577`) and `t6_g3a_referential_loops_...` (`:16158`). **A re-derivation that greps
|
||||
> `fn t6` and takes the first hit lands on the wrong test**, and both hits are plausible
|
||||
> in context. Match on the full `_g3a_` name, never the prefix.
|
||||
|
||||
**Pin 1 — refuse a non-empty carried `members`, using the existing helper.**
|
||||
In `create_staff_group` (`reduce.rs:4458`), before the liveness loop, refuse a
|
||||
|
|
@ -343,9 +389,9 @@ revised.** Each currently *passes* by asserting the outgoing rule:
|
|||
|
||||
| Test | Line | Currently asserts | Under pin 1 |
|
||||
|---|---|---|---|
|
||||
| `t6` | `reduce.rs:16154` | `CreateStaffGroup.members` naming a non-live target is `TargetMissing`, one of three referential loops asserted separately | that arm becomes `ContainerNotEmpty` and stops testing a *referential* loop at all; the `CreatePartDefinition.staves` and `CreateView.active_layers` arms are untouched and must stay |
|
||||
| `t7` | `reduce.rs:16229` | those same preconditions are **not** enforced base-free | pin 1's refusal is **not** graph-gated — it is a property of the carried value — so this arm now refuses base-free too, inverting the claim for that arm only |
|
||||
| `t9` | `reduce.rs:16454` | a from-empty score passes `check_invariants`, and **each skipped reducer check independently makes invariant 10 fire**, on a fixture that already attempts a dangling reference in each of the four ops | the dangling-member fixture can no longer enter the graph, so both the fixture and t9's own mutation set change |
|
||||
| `t6` | `reduce.rs:16158` | `CreateStaffGroup.members` naming a non-live target is `TargetMissing`, one of three referential loops asserted separately | that arm becomes `ContainerNotEmpty` and stops testing a *referential* loop at all; the `CreatePartDefinition.staves` and `CreateView.active_layers` arms are untouched and must stay |
|
||||
| `t7` | `reduce.rs:16231` | those same preconditions are **not** enforced base-free | pin 1's refusal is **not** graph-gated — it is a property of the carried value — so this arm now refuses base-free too, inverting the claim for that arm only |
|
||||
| `t9` | `reduce.rs:16461` | a from-empty score passes `check_invariants`, and **each skipped reducer check independently makes invariant 10 fire**, on a fixture that already attempts a dangling reference in each of the four ops | the dangling-member fixture can no longer enter the graph, so both the fixture and t9's own mutation set change |
|
||||
|
||||
**`t7`'s inversion is the subtle one and must be stated in its doc block:** a
|
||||
graph-aware precondition asks about the *universe* and cannot run base-free; an
|
||||
|
|
@ -439,12 +485,67 @@ previously pinned the opposite, and why the change is the ratified disposition
|
|||
rather than a regression. **Deleting it is forbidden** — the pairing of the two
|
||||
orders is the coverage.
|
||||
|
||||
**Pin 8 — the four G3a undo-repair tests are re-verified, not assumed.**
|
||||
`:16838`, `:16992`, `:17138`, `:17345` each construct the missing-member form,
|
||||
**Pin 8 — the four G3a undo-repair tests are re-verified, not assumed. NAMED by draft
|
||||
amendment 1.** All four are in `crates/epiphany-ops/src/reduce.rs`:
|
||||
|
||||
| Test | `fn` at |
|
||||
|---|---|
|
||||
| `u2a_a_live_staff_naming_the_group_blocks_its_undo` | `:16826` |
|
||||
| `u2bf_a_the_staff_group_guard_holds_base_free` | `:16983` |
|
||||
| `u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo` | `:17125` |
|
||||
| `u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole` | `:17333` |
|
||||
|
||||
> **This pin previously identified them ONLY as `:16838`, `:16992`, `:17138`,
|
||||
> `:17345`** — and those are **interior** line numbers, roughly a dozen lines into each
|
||||
> body, not the `fn` lines. An interior line number is worse than a stale one: it
|
||||
> anchors to nothing a reader can search for, and it silently drifts with every edit to
|
||||
> the function above it. **Names are stable; line numbers are a convenience.** The `fn`
|
||||
> line numbers above are given second and are already subject to the locator warning
|
||||
> under pin 0.
|
||||
|
||||
They each construct the missing-member form,
|
||||
which pin 2 now makes an agreeing form. They assert on undo effects rather than
|
||||
on `members`, so they are expected to survive — **expected, not known.** Each
|
||||
must be run and its verdict reported; any that changes is a finding.
|
||||
|
||||
**Pin 12 — the authority bump. ADDED BY DRAFT AMENDMENT 1; it had no pin, no touch row
|
||||
and no gate.**
|
||||
|
||||
Bump `epiphany_ops::CURRENT_REDUCTION_ALGORITHM_VERSION` **`0` → `1`** (touch row 7),
|
||||
**and add this rung's entry to the constant's own `Bumps` list** in the same doc
|
||||
comment. The list is the only record of *why* a version exists; a bump without its
|
||||
entry leaves a number nobody can account for.
|
||||
|
||||
**This is not optional and not a consequence — it is the obligation.** This rung changes
|
||||
`CreateStaffGroup`'s reduction verdict, and `core_spec.tex` §"Canonical Document
|
||||
Identity" makes such a change require a new version. **No mechanism can detect a missed
|
||||
bump** (see *Enforcement is not detection* under pin 0), so nothing in the gate set will
|
||||
catch its absence except the two tripwires in rows 9 and 10 — which is exactly why they
|
||||
must be updated rather than silenced.
|
||||
|
||||
> **The bump is stated in pin 0's discharge as requirement 3, which is a discharge note
|
||||
> and not a pin.** So it had no numbered pin to execute, no touch row to stage, no gate
|
||||
> to check and no report item to confirm — **the four places this repo's discipline
|
||||
> requires a mandated change to appear.** It now has all four: pin 12, touch row 7,
|
||||
> gate 10, report item 2b.
|
||||
|
||||
**Pin 10a — whether pin 6 or pin 10 mints a `\label{req:...}` MUST be decided
|
||||
explicitly, and stated in the report. ADDED BY DRAFT AMENDMENT 1.**
|
||||
|
||||
This rung edits **`core_spec.tex`** (row 5, invariant 21's enumeration) and
|
||||
**`operation_catalog.tex`** (row 4), and `crates/epiphany-testkit/tests/requirement_labels.rs`
|
||||
counts requirements and labels in **both**. The two readings have different touch tables:
|
||||
|
||||
- **If either mints a label**, touch row 11 is used and **all three counters move** —
|
||||
`CORE_REQUIREMENT_COUNT`, `SUITE_REQUIREMENT_COUNT`, `SUITE_LABEL_COUNT`. S27 found the
|
||||
hard way that naming only the first leaves two failing tests.
|
||||
- **If neither does**, row 11 is unused and **the report says so.**
|
||||
|
||||
> **`CLAUDE.md` names this file by name as a recurring escapee**, it escaped the
|
||||
> format-epoch rung's table, and S27 had to add it mid-execution. **A file that must
|
||||
> change but is not listed silently drops out of the commit**, and the failure surfaces
|
||||
> on someone else's branch. Carrying it conditionally costs nothing if unused.
|
||||
|
||||
**Pin 9 — no byte artifact moves.**
|
||||
`spec/vectors/decode_vectors.txt`, `ops/src/vectors.rs:829`'s literal-byte
|
||||
vector, and `textproj/src/vectors.rs:198`'s golden are all **unchanged**,
|
||||
|
|
@ -553,29 +654,87 @@ unblocked, dispatchable and resolved are three different states.
|
|||
| 4 | `spec/operation_catalog.tex` (+ `.pdf`) | pin 10 |
|
||||
| 5 | `spec/core_spec.tex` (+ `.pdf`) | pins 6, 10 |
|
||||
| 6 | `spec/PASS13_CANDIDATES.md` | pin 11 |
|
||||
| **7** | `crates/epiphany-ops/src/lib.rs` | **ADDED by draft amendment 1.** **Pin 12** — bump `CURRENT_REDUCTION_ALGORITHM_VERSION` `0 → 1` **and add its entry to the constant's own `Bumps` list**, which is in the same doc comment. The rung mandated by pin 0's discharge had no touch row, no pin and no gate |
|
||||
| **8** | `crates/epiphany-core/src/generators.rs` | **ADDED by draft amendment 1 — the root cause below.** `violating_score` (`:498`) matches `GraphInvariant` **exhaustively**, so invariant 21 **does not compile** without a new arm. Four `all()`-driven tests (`:991`, `:1004`, `:1025`, `:1042`) then consume it, so the arm must be a **real generator**, not a stub |
|
||||
| **9** | `crates/epiphany-testkit/src/roundtrip.rs` | **ADDED by draft amendment 1.** S27 test 10b (`:894`) reopens a literal-`0` base under `production_caps()`; pin 12's bump makes that path return `Err` and hit an arm that **`panic!`s by design** |
|
||||
| **10** | `crates/epiphany-textproj/src/serialize.rs` | **ADDED by draft amendment 1.** S27 test 10a (`:659`) asserts the production writer supplies `ReductionAlgorithmVersion(0)`. Its own doc (`:655`) says it **is expected to fail when S16 bumps** and that updating it *is* S16 stating the authority moved |
|
||||
| **11** | `crates/epiphany-testkit/tests/requirement_labels.rs` | **ADDED by draft amendment 1 — CONDITIONAL**, exactly as S27's row 12. Only if pin 6 or pin 10 mints a `\label{req:...}`. **That decision MUST be made explicitly and stated in the report** — see pin 10a. If it mints one, **all three counters move**, not one: `CORE_REQUIREMENT_COUNT` (`:15`), `SUITE_REQUIREMENT_COUNT` (`:18`), `SUITE_LABEL_COUNT` (`:19`). This file counts **both** `core_spec.tex` and `operation_catalog.tex`, and this rung touches both. If no label is minted, leave unmodified and say so |
|
||||
|
||||
Regenerate the two PDFs **only after** their sources reach final form.
|
||||
|
||||
### Rows 9 and 10 are S27's tripwires firing as designed, not collateral damage
|
||||
|
||||
S27 wrote two assertions against the **literal** `0` precisely so they would move when
|
||||
the authority moved, and `serialize.rs:655` says so in as many words. **Their failure is
|
||||
this rung's signal that the bump took effect** — the only signal it gets, since no
|
||||
mechanism can detect a semantics change. They must be **updated, not deleted or
|
||||
`#[ignore]`d**, and the report must quote both before and after.
|
||||
|
||||
> **Neither file was in any touch row, and both fail at gate 1.** That is the exact
|
||||
> shape of S27's own `gminor.rs` failure: a file the rung must change that no surface
|
||||
> count reached, found by a gate rather than by the table. **The allowlist catching it
|
||||
> is the allowlist working** — but only if the row exists before execution starts.
|
||||
|
||||
### Row 8 is the rung's real shape change: an enum extension is a TWO-crate change
|
||||
|
||||
**This contract treated invariant 21 as local to `invariants.rs`.** It is not.
|
||||
`GraphInvariant` has an **exhaustive generated-consumer surface in `epiphany-core`**:
|
||||
|
||||
- `violating_score` (`generators.rs:498`) matches every variant — **adding one is a
|
||||
compile error until its arm exists.**
|
||||
- Four `all()`-driven tests then call it and `shrink` (`:991`, `:1004`, `:1025`,
|
||||
`:1042`), so **a `todo!()` or trivial arm fails them.** Invariant 21 needs a fixture
|
||||
that genuinely violates it in both directions and survives shrinking.
|
||||
- **`shrink` (`:932`) takes `GraphInvariant` too. Whether it also matches exhaustively
|
||||
MUST be checked at execution and reported** — this amendment did not establish it
|
||||
either way, and guessing is what produced this finding.
|
||||
|
||||
**Consequence for the mutation plan and gate 6:** invariant 21's generator is itself
|
||||
load-bearing, so M6 (deleting each arm) now has a second signature — the negative
|
||||
generator must still produce a violating score for the arm under test.
|
||||
|
||||
---
|
||||
|
||||
## §3. Mutation plan
|
||||
|
||||
Applied, **run**, output recorded verbatim, restored **by hand-editing back**.
|
||||
|
||||
**M1 — the refusal fires.** Remove pin 1's emptiness check; the rewritten `t8b`
|
||||
spurious-order assertion must fail.
|
||||
> ### A FAILING TEST IS NOT AN OBSERVATION — draft amendment 1
|
||||
>
|
||||
> **M1, M2 and M4 accepted "the named test fails" as their whole signature.** That
|
||||
> signs nothing: a test fails for the mutation, for a typo, for an unrelated panic, or
|
||||
> because the harness changed — and a **compile error is not a test failure at all.**
|
||||
> **The evidence a mutation owes is the BEHAVIOUR it changed, not the assertion it
|
||||
> broke.** Each mutation below must now name the wrong verdict, value or state the
|
||||
> mutated build produces, and the report must quote it. *(This is S27's round-15/16
|
||||
> lesson, which cost four defects there; M3, M5, M6 and M9 in this contract already
|
||||
> met the standard, so the fix is uneven-by-design rather than uniform.)*
|
||||
|
||||
**M2 — the maintenance fires.** Remove pin 2's append; the rewritten `t8b`
|
||||
missing-order assertion must fail.
|
||||
**M1 — the refusal fires. OBSERVATION TIGHTENED, draft amendment 1.** Remove pin 1's
|
||||
emptiness check. **Required observation:** a `CreateStaffGroup` carrying a **non-empty
|
||||
`members`** is now **applied instead of refused** — report the resulting
|
||||
`OperationEffect` and the minted `StaffGroup.members` value, showing the spurious
|
||||
membership that reached the graph. The rewritten `t8b` spurious-order assertion failing
|
||||
is the *symptom*; the applied mint is the observation.
|
||||
|
||||
**M2 — the maintenance fires. OBSERVATION TIGHTENED, draft amendment 1.** Remove pin 2's
|
||||
append. **Required observation:** after a `CreateStaff` naming a live group,
|
||||
`StaffGroup.members` is **still empty** — quote it, and quote invariant 21's verdict on
|
||||
that state. The rewritten `t8b` missing-order assertion failing is the symptom.
|
||||
|
||||
**M3 — the re-carry stays idempotent.** Make pin 3 write maintained members into
|
||||
`staff_group_values`; a byte-identical re-carry must degrade from
|
||||
`AlreadyApplied` to `RecreateContentMismatch`. **This mutation must be observed,
|
||||
not reasoned about** — it is the sub-pin disposition A named.
|
||||
|
||||
**M4 — the base-ingest hazard is real.** Restore `:1619` to `group.clone()`;
|
||||
pin 4a's test must fail. **If it does NOT fail, pin 4 is unmotivated and that is
|
||||
a finding** — report it rather than keeping a guard nothing needs.
|
||||
**M4 — the base-ingest hazard is real. OBSERVATION TIGHTENED, draft amendment 1.**
|
||||
Restore `:1619` to `group.clone()`. **Required observation: the re-carry misverdict
|
||||
itself** — name what an ingested base's `CreateStaffGroup` re-carry now returns and what
|
||||
it should have returned, in the shape M3 already uses (`AlreadyApplied` →
|
||||
`RecreateContentMismatch`). "Pin 4a's test must fail" was the entire signature and does
|
||||
not distinguish the hazard from any other breakage.
|
||||
**If the misverdict does NOT appear, pin 4 is unmotivated and that is a finding** —
|
||||
report it rather than keeping a guard nothing needs.
|
||||
|
||||
**M3 and M4 are signed by pins 3a and 4a, not by manual demonstration.** Run each
|
||||
mutation against its named test so the guard, not the transcript, is what
|
||||
|
|
@ -599,21 +758,56 @@ must leave a disagreeing pair that invariant 21 flags.
|
|||
**M6 — invariant 21 sees both directions.** Delete each arm in turn; each
|
||||
deletion must leave a distinct disagreeing fixture unreported.
|
||||
|
||||
**M7 — the doc guards discriminate.** With pin 10's needles updated, revert one
|
||||
doc comment to its disposition-B wording; the guard must fail. A guard that
|
||||
passes against both wordings is weakened, not updated.
|
||||
**M7 — the doc guards discriminate. SPLIT IN TWO by draft amendment 1.** Pin 10 covers
|
||||
**two independently guarded doc blocks** — `Staff.group` and `StaffGroup.members`, each
|
||||
with its own grep guard (touch row 3). Reverting *"one doc comment"* leaves the other
|
||||
guard untested, and a run that reverts the stronger one **passes while the weaker guard
|
||||
is still weak.** So:
|
||||
|
||||
- **M7a — `Staff.group`.** Revert that block to its disposition-B wording. **Required
|
||||
observation:** quote the guard's own output showing **its specific needle no longer
|
||||
matches**, not merely that a test failed.
|
||||
- **M7b — `StaffGroup.members`.** The same, independently, with its own output.
|
||||
|
||||
**Both must be run and both outputs reported.** A guard that passes against both
|
||||
wordings is weakened, not updated — and with one mutation covering two guards, that
|
||||
weakening is invisible.
|
||||
|
||||
---
|
||||
|
||||
## §4. Gate
|
||||
|
||||
1. `cargo test --workspace` — full pass. **The count will move** (t8b renamed,
|
||||
new invariant tests). Report the new total and the delta with its cause.
|
||||
2. `cargo clippy --workspace --all-targets -- -D warnings` → clean.
|
||||
3. `cargo fmt -p epiphany-ops -p epiphany-core --check` → clean.
|
||||
**`cargo fmt --all` is forbidden.**
|
||||
4. `git diff --cached --check` → clean, after staging; confirm the staged list
|
||||
is exactly §2.
|
||||
1. `cargo test --workspace` — full pass. **Baseline is 1577 passed / 0 failed / 0
|
||||
ignored across 42 suites** *(the post-S27 figure; `CLAUDE.md`'s Green baseline is the
|
||||
single origin — if it disagrees with this line, `CLAUDE.md` wins and that is a
|
||||
finding)*. **The count will move** (t8b renamed, new invariant tests, and rows 9–10's
|
||||
tripwire updates). Give the delta in buckets — net-new, converted-from-existing,
|
||||
tripwire-updated — and **if they do not sum to the observed delta, that is a finding,
|
||||
not an arithmetic error to be papered over.**
|
||||
**Report the ignored count, which MUST be 0** — a "full pass" is satisfied by an
|
||||
`#[ignore]`d test that never runs.
|
||||
2. `cargo +1.95.0 clippy --workspace --all-targets -- -D warnings` → clean.
|
||||
**The toolchain is part of the gate**: CI pins **1.95.0**, this machine's default
|
||||
`stable` is **1.97.1**, and the repo's CI comment records that *1.97 rejects a bare
|
||||
`2.0` that 1.95 accepts*. **A clippy result that does not say which toolchain
|
||||
produced it says nothing.** Report the toolchain with the result.
|
||||
3. `cargo +1.95.0 fmt -p epiphany-ops -p epiphany-core -p epiphany-textproj -p
|
||||
epiphany-testkit --check` → clean, on the same pinned toolchain.
|
||||
**All four changed crates — corrected by draft amendment 1**, which added rows 9 and
|
||||
10 in `epiphany-testkit` and `epiphany-textproj`; the command named only two and
|
||||
would have left both unformatted while reporting clean.
|
||||
**`cargo fmt --all` is forbidden** — it reaches `spikes/` through path dependencies.
|
||||
4. `git diff --cached --check` → clean after staging. **The staged list is a SUBSET of
|
||||
§2, not an equality — corrected by draft amendment 1.** "Exactly §2" is
|
||||
**unsatisfiable** here because row 11 is conditional: read literally it fails whenever
|
||||
a conditional row is correctly unused, or invites staging an unchanged file to satisfy
|
||||
it. **Instead:** every staged path must appear in §2, **and** every §2 row must be
|
||||
either staged or **named in the report as unused, with its reason.** Neither
|
||||
direction may be silent. *(This is S27's round-17 correction; S16 carried the
|
||||
formulation S27 had already found unsatisfiable.)*
|
||||
4a. **§2 carries no prohibitions**, unlike S27's §2 — so gate 4 is the whole staging
|
||||
check here. **If a later amendment adds an absence rule, this gate does not cover
|
||||
it**: "appears in §2" and "is not forbidden by §2" are different questions.
|
||||
5. `spec/vectors/decode_vectors.txt` **unmodified** (pin 9). Confirm by `git
|
||||
status`, not by inspection.
|
||||
6. Invariant 21 is reached **through `check_invariants`** on a score violating
|
||||
|
|
@ -624,6 +818,47 @@ passes against both wordings is weakened, not updated.
|
|||
8. The pin-1 structural gate: `create_staff_group`'s production body contains
|
||||
the empty-members refusal and no member-liveness/`TargetMissing` path.
|
||||
9. `t8c` (pin 3a) and `t8d` (pin 4a) both present and passing, by name.
|
||||
10. **Pin 12's bump landed, by value comparison — ADDED BY DRAFT AMENDMENT 1.**
|
||||
```
|
||||
grep -n "pub const CURRENT_REDUCTION_ALGORITHM_VERSION" crates/epiphany-ops/src/lib.rs
|
||||
git show HEAD:crates/epiphany-ops/src/lib.rs | grep -n "pub const CURRENT_REDUCTION_ALGORITHM_VERSION"
|
||||
```
|
||||
→ working tree **`= 1`**, `HEAD` **`= 0`**. **Report both outputs, not the
|
||||
conclusion**, and **quote the new `Bumps` list entry verbatim.** A bump without its
|
||||
entry fails this gate.
|
||||
11. **Rows 9 and 10's tripwires were UPDATED, not silenced.** Quote both assertions
|
||||
before and after. **Neither may be deleted, `#[ignore]`d, or weakened to accept any
|
||||
version** — a tripwire that accepts both values is the tautology S27 existed to
|
||||
remove, rebuilt.
|
||||
|
||||
---
|
||||
|
||||
## §4a. Landing obligation — files that must NOT be staged, and must be fixed after
|
||||
|
||||
**ADDED BY DRAFT AMENDMENT 1.** Pin 12's bump makes two live statements false, and both
|
||||
are in documents **outside this rung's touch table on purpose**:
|
||||
|
||||
| File | Statement the bump falsifies |
|
||||
|---|---|
|
||||
| `CLAUDE.md:106` | *"`CURRENT_REDUCTION_ALGORITHM_VERSION` — **currently `0`**"*, and *"P13-S16 is the first rung that must move it to `1`"* |
|
||||
| `spec/HANDOFF_2026-08-07.md:25` | the POST-S27 block's *"currently `0`"* and the same "first rung" sentence |
|
||||
|
||||
**DO NOT STAGE EITHER DURING EXECUTION.** Both describe the state of the repository
|
||||
**after a rung has landed**, and this rung is not landed while it is staged and awaiting
|
||||
acceptance. Staging them would have the contract assert S16 had landed at the moment it
|
||||
was submitted for review — **a claim about the future written as present fact**, which is
|
||||
the defect class S27's amendments 4 through 7 were spent removing.
|
||||
|
||||
**They are a POST-ACCEPTANCE obligation.** Once the owner accepts and commits this rung,
|
||||
reconcile both in a separate commit, together with anything else the bump falsifies.
|
||||
**The report MUST list them as outstanding**, so acceptance is not mistaken for
|
||||
completion.
|
||||
|
||||
> **Pin 11 already covers `spec/PASS13_CANDIDATES.md`, which is different** and *is*
|
||||
> staged: a ledger row records what a rung *did*, and is written by the rung. `CLAUDE.md`
|
||||
> and the handoff state what is *true now*, and only become true at acceptance. **The
|
||||
> distinction is whether the file's claim is dated or live** — the rule amendment 6
|
||||
> settled for S27, applied here to decide staging rather than wording.
|
||||
|
||||
---
|
||||
|
||||
|
|
@ -657,6 +892,15 @@ its evidence at `invariants.rs:69`–`:71` must stay intact.
|
|||
|
||||
1. The nine mutations (M1–M9), each with verbatim failure output.
|
||||
2. The nine gate results, each with its command.
|
||||
2b. **Pin 12's bump and its `Bumps` entry**, with gate 10's two outputs; **and rows 9
|
||||
and 10's tripwire updates**, each quoted before and after, with gate 11's confirmation
|
||||
that neither was silenced. **ADDED BY DRAFT AMENDMENT 1.**
|
||||
2c. **Whether pin 6 or pin 10 minted a `\label{req:...}`** (pin 10a), and therefore
|
||||
whether touch row 11 was used. **If used, all three counters and their new values;
|
||||
if not, say so explicitly.** **ADDED BY DRAFT AMENDMENT 1.**
|
||||
2d. **Whether `shrink` (`generators.rs:932`) matches `GraphInvariant` exhaustively**, and
|
||||
if so what its invariant-21 arm does. **Draft amendment 1 did not establish this
|
||||
either way and deliberately did not guess.** **ADDED BY DRAFT AMENDMENT 1.**
|
||||
2a. **REWRITTEN 2026-08-09 — it required the opposite of what is now correct.** It read:
|
||||
*"For pin 0: confirmation that **nothing** was added claiming to reject or detect
|
||||
stale canonical bases, and that the break is recorded only in prose."* That was right
|
||||
|
|
|
|||
Loading…
Reference in New Issue