From abe2c359f7485959b0bd7025ea32952339c2a169 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 9 Aug 2026 17:42:22 +0200 Subject: [PATCH] S16 draft amendment 1 rev E: a gate must name evidence its artifact produces MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Independent review of cae1d32 returned two blocking findings and one stale rationale. Both blocking findings are in requirements revision D itself wrote, and both are revision D's own closing lesson turned back on it. 1. Row 8's new generator test had no name, so nothing consumed it. Gate 6 named only m41 and m41b; §6 item 2d asks for shrink evidence. Omitting the test entirely would still compile, satisfy all four all() loops, and pass every named gate. Named invariant_21_negative_generator_breaks_staff_to_group_only, with its three assertions spelled out: exactly one violation and it is StaffGroupMembershipAgreement, the witness naming the S->G ids, and the G->S direction asserted satisfied. Added to gate 6 and to new §6 item 2e. This is revision D's own lesson unapplied to itself: it closed by distinguishing a rule with no consumer from a rule with no observer, then wrote a requirement with neither. An unnamed artifact cannot be gated, because every gate here names what it checks. 2. Gate 6 demanded runtime evidence the prescribed tests cannot emit. It said to quote check_invariants' full return and witness ids, but these are assert!-style tests in m40's shape and cargo test prints ok, not local values. Obeying it literally would need unpinned --nocapture instrumentation added purely to produce a report, or source inference presented as observation. Evidence model now chosen explicitly: quote the SOURCE assertions plus the pass verdict. A passing exact-set assertion IS the observation -- the assertion text says what was checked, the verdict says it held. This follows S27's gate 6c, which quotes a struct definition rather than grepping for it: a quoted source construct is read, not inferred. It also adds no code to epiphany-core written solely for a report. The requirement was right and the mechanism was borrowed from gates that run commands and read stdout. A gate must name evidence the prescribed artifact actually produces; otherwise execution improvises, and improvised instrumentation is unpinned scope arriving through the report. 3. Gate 4's rationale still said row 11 is "conditional," which revision D changed to decided-unused. A fourth site under pin 10a said "carrying it conditionally costs nothing" -- found by sweep. Both updated. The subset rule itself is unaffected; only its rationale needed the current term. Still DRAFT, still unratified. No implementation work has begun. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x --- spec/CONTRACT_P13S16_PROJECTION.md | 111 ++++++++++++++++++++++++----- 1 file changed, 93 insertions(+), 18 deletions(-) diff --git a/spec/CONTRACT_P13S16_PROJECTION.md b/spec/CONTRACT_P13S16_PROJECTION.md index e08e2d6..54c454e 100644 --- a/spec/CONTRACT_P13S16_PROJECTION.md +++ b/spec/CONTRACT_P13S16_PROJECTION.md @@ -138,7 +138,31 @@ depend on a choice made at the keyboard, so **the touch table can be wrong in ei direction and the report will agree with whatever happened.** Where the facts are readable — and these were, in the `.tex` source — the contract decides. -**The pattern across revisions A–D is sharper than any individual finding: a correction +### Draft amendment 1, revision E — independent review of `cae1d32` + +**Two blocking findings and one stale rationale. Both blocking findings are in +requirements revision D itself wrote**, and both are its own closing lesson turned back +on it. + +| # | Finding | Disposition | +|---|---|---| +| **1** | **Row 8's new generator test had no name, so nothing consumed it.** Gate 6 named only `m41`/`m41b`; §6 item 2d asks for shrink evidence. **Omitting the test entirely would still compile, satisfy all four `all()` loops, and pass every named gate** | Named **`invariant_21_negative_generator_breaks_staff_to_group_only`**, with its three required assertions spelled out; **added to gate 6** and to **§6 item 2e** | +| **2** | **Gate 6 demanded runtime evidence the prescribed tests cannot emit.** It said to quote `check_invariants`' full return and witness ids — but these are `assert!` tests in `m40`'s shape, and `cargo test` prints `ok`, not local values. Satisfying it literally would need **unpinned `--nocapture` instrumentation** or source inference presented as observation | **Evidence model chosen explicitly: quote the SOURCE assertions plus the pass verdict.** A passing exact-set assertion *is* the observation. Follows S27's gate 6c — a quoted source construct is read, not inferred — and adds no code to `epiphany-core` written solely for a report | +| 3 | **Gate 4's rationale still said row 11 is "conditional"**, which revision D changed to decided-unused. *(A fourth site under pin 10a said "carrying it conditionally costs nothing" — found by sweep)* | Both updated. **The subset rule itself is unaffected**; only its rationale needed the current term | + +**Finding 1 is revision D's own lesson, unapplied to revision D.** It closed by +distinguishing a rule with no *consumer* from a rule with no *observer* — and then wrote +a requirement with neither. **An unnamed artifact cannot be gated**, because every gate +in this contract names what it checks. + +**Finding 2 is the more interesting failure: a gate that specified the right thing to +know and the wrong way to know it.** Exactness is the correct requirement; *"quote the +runtime return"* was a mechanism borrowed from gates that run commands and read stdout, +applied to a unit test that emits nothing on success. **A gate must name evidence the +prescribed artifact actually produces** — otherwise execution improvises, and improvised +instrumentation is unpinned scope arriving through the report. + +**The pattern across revisions A–E is sharper than any individual finding: a correction propagates one hop and stops.** Rev A fixed pin 10a and left touch row 11; the sweep caught row 11 and stopped before §6's consumer; rev D found pin 10a's *decision* still deferred after two reworders. Rev A removed item 1's mutation tally and left item 2's @@ -737,7 +761,9 @@ table below, which is retained for that case and for the next rung. > **`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. +> on someone else's branch. **Carrying it as a decided-unused row costs nothing and +> documents the decision** — revision E; it read "carrying it conditionally costs nothing +> if unused" until revision D removed the conditionality. **Pin 9 — no byte artifact moves.** `spec/vectors/decode_vectors.txt`, `ops/src/vectors.rs:829`'s literal-byte @@ -880,14 +906,30 @@ mechanism can detect a semantics change. They must be **updated, not deleted or that violates the **S→G direction — a staff whose `group` names a group whose `members` omit it — and NOT the G→S direction**, and survives shrinking. **The direction is PINNED here, in revision C.** -- **The direction needs its own permanent assertion — REVISION D.** **No existing - `all()`-driven test can observe it.** `negative_generators_are_reasonably_targeted` - (`:1037`) collects `kinds: BTreeSet` and allows `kinds.len() <= 3`, but - **both directions of invariant 21 are the same `GraphInvariant` variant**, so they - collapse to one element and the bound is blind to the distinction; the other three - loops assert only `!is_empty()`. Add a dedicated test in `generators.rs`'s test module - asserting `violating_score(StaffGroupMembershipAgreement, seed)` violates **S→G and - not G→S**, with the witness ids quoted in the report. +- **The direction needs its own permanent, NAMED test — REVISION D, name pinned in + REVISION E.** **No existing `all()`-driven test can observe direction.** + `negative_generators_are_reasonably_targeted` (`:1037`) collects + `kinds: BTreeSet` and allows `kinds.len() <= 3`, but **both directions + of invariant 21 are the same `GraphInvariant` variant**, so they collapse to one + element and the bound is blind to the distinction; the other three loops assert only + `!is_empty()`. + + Add to `generators.rs`'s test module, named **exactly**: + + ``` + invariant_21_negative_generator_breaks_staff_to_group_only + ``` + + It MUST assert, on `violating_score(StaffGroupMembershipAgreement, seed)`: + **(i)** `check_invariants` returns **exactly one** violation and it is + `StaffGroupMembershipAgreement`; **(ii)** that violation's witness names the **S→G** + staff and group ids; **(iii)** the **G→S** direction is satisfied, asserted directly. + + > **Revision D required this test and gave it no name — so nothing consumed it.** + > Gate 6 named only `m41`/`m41b`, and §6 item 2d asks for shrink evidence. **Omitting + > the test entirely would still compile, satisfy all four `all()` loops, and pass every + > named gate.** An unnamed obligation has no consumer, which is revision D's own + > closing lesson applied to the requirement revision D wrote. > **"Both directions" was wrong here and incompatible with M6 — corrected in revision > B.** `violating_score` returns **one** `Score` per variant, so it cannot carry two @@ -1050,9 +1092,12 @@ weakening is invisible. **`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 + **unsatisfiable** here because **row 11 is deliberately unused** (pin 10a decided in + revision D that no label is minted): read literally, "exactly §2" fails whenever a row + is correctly unstaged, or invites staging an unchanged file to satisfy it. + *(This said "row 11 is conditional" until revision E — true when written, and revision + D made the row **decided-unused** rather than conditional. **The subset rule is + unaffected**; only its rationale needed the current term.)* **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.)* @@ -1073,11 +1118,35 @@ weakening is invisible. both verdicts reported, and each confirmed to satisfy the direction it does not break.** *(Revision C: this asked for one score, which left one branch with no durable coverage once M6 was reverted.)* - **Report the EXACT violation set each fixture produces — revision D.** Quote - `check_invariants`' full return for both, showing **one** violation each and its - witness ids. *(This gate asked for the target verdict and the opposite direction's - absence, but **not the absence of invariants 1–20**, so a fixture carrying an - unrelated second defect passed every stated check.)* + **And `invariant_21_negative_generator_breaks_staff_to_group_only`** (touch row 8), + which is the only consumer of the generator's pinned direction. **Three tests, all + run, all verdicts reported — revision E**; revision D named two and left the third + with no gate. + + **EVIDENCE MODEL — CHOSEN EXPLICITLY IN REVISION E. Quote the SOURCE assertions plus + the pass verdict; do NOT claim a runtime return.** + + Revision D said *"quote `check_invariants`' full return … and its witness ids"*, which + **the prescribed tests cannot emit**: they are `assert!`-style tests in `m40`'s shape, + and `cargo test` prints `ok` for a passing test, not local values. A report obeying + that literally would need either **unpinned `--nocapture` instrumentation added purely + to produce it**, or inference from source dressed up as observed output. **Neither is + evidence.** + + So for each of the three tests, the report gives: + 1. **The exact-set assertion, quoted verbatim from source** — the `len() == 1` and + invariant-identity assertions, and the witness-id assertion. + 2. **The test's pass verdict** from `cargo test`. + + **A passing exact-set assertion IS the observation**; the assertion text says what was + checked and the verdict says it held. *(This follows S27's gate 6c, which quotes a + struct definition rather than grepping for it: **a quoted source construct is read, + not inferred**. Adding print instrumentation to satisfy a report would be new, + unpinned code in `epiphany-core` written for no other purpose.)* + + *(Revision D added the exactness requirement because this gate checked the target + verdict and the opposite direction but **not the absence of invariants 1–20**, so a + fixture carrying an unrelated second defect passed every stated check.)* `all().len() == 21` and the `core_spec.tex` enumeration ending at 21 are checked **in addition**, never instead. 7. **Every test named in pin 8** runs, each verdict reported. *(Read "the four pin-8 @@ -1207,6 +1276,12 @@ its evidence at `invariants.rs:69`–`:71` must stay intact. could read** (it does not — it calls `check_invariant(score, inv)`). Deferring a readable fact to execution is not caution; it is unfinished drafting handed downstream as an obligation. +2e. **The three invariant-21 tests' verdicts** — `m41`, `m41b`, and + `invariant_21_negative_generator_breaks_staff_to_group_only` — **each with its + exact-set and direction assertions quoted from source**, per gate 6's evidence model. + **No runtime return or witness dump is claimed**; a passing exact-set assertion is the + observation. **ADDED IN REVISION E**, which found the generator test required by + revision D but consumed by nothing. 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