From 2818ced2299aeee1555ab5ea5547c4014423a2bc Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 9 Aug 2026 17:51:21 +0200 Subject: [PATCH] S16 draft amendment 1 rev F: a transformation's output needs its input's guarantees MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Independent review of abe2c35 returned one blocking finding, and it is both prior revisions' lessons colliding. The shrink leg had no observable direction or exactness guarantee. Row 8 requires the S->G fixture to survive shrinking, but: - the named generator test asserted only on the raw violating_score(...); - the shrunk score was checked solely by every_invariant_shrinks_to_a_small_witness (generators.rs:1003), whose !check_invariant(&small, inv).is_empty() is membership in ONE GraphInvariant variant -- and both directions of invariant 21 are the same variant, so a shrunk witness that flipped to G->S-only passes it. Because it calls check_invariant (singular) rather than check_invariants, a shrunk witness that gained an unrelated second defect passes too; - §6 item 2d still said "quote the shrunk witness," which a passing test cannot emit. So a shrunk witness that changed direction, or acquired a second defect while retaining invariant 21, satisfied every assertion and every gate. Fixed: the named test now asserts the same three properties TWICE -- on the raw fixture and again on shrink(&that, StaffGroupMembershipAgreement): exactly one violation and it is StaffGroupMembershipAgreement, the witness naming the S->G ids, and G->S asserted satisfied. Gate 6 requires both legs. Item 2d rewritten to revision E's source-assertion-plus-pass-verdict model. Item 2e extended to both legs. Row 8's description of the existing shrink tests now says plainly that they establish only that SOMETHING still fires, and that direction and exactness after shrinking come solely from the named test's shrunk leg. Two lessons collided here. Revision E established that a gate must name evidence its artifact produces and fixed gate 6 -- stopping one hop short of item 2d, which is the fix-propagation failure revisions A-D kept recording. And the underlying gap is revision D's: a requirement, "survives shrinking," with nothing able to fail it. The generalisable rule now recorded: shrink is a TRANSFORMATION, and a transformation's output needs the same guarantees asserted of its input. Requiring a fixture to "survive" a transformation establishes only that something survived. Every property the input was pinned for must be re-asserted on the output, or the transformation is free to change what the fixture proves. 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 | 79 ++++++++++++++++++++++++------ 1 file changed, 64 insertions(+), 15 deletions(-) diff --git a/spec/CONTRACT_P13S16_PROJECTION.md b/spec/CONTRACT_P13S16_PROJECTION.md index 54c454e..a3f602d 100644 --- a/spec/CONTRACT_P13S16_PROJECTION.md +++ b/spec/CONTRACT_P13S16_PROJECTION.md @@ -162,7 +162,27 @@ applied to a unit test that emits nothing on success. **A gate must name evidenc 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 +### Draft amendment 1, revision F — independent review of `abe2c35` + +**One blocking finding, and it is both prior lessons at once.** + +| # | Finding | Disposition | +|---|---|---| +| **1** | **The shrink leg had no observable direction or exactness guarantee.** Row 8 requires the S→G fixture to *survive* shrinking, but the named test asserted only on the **raw** `violating_score(...)`; the shrunk score was checked solely by `every_invariant_shrinks_to_a_small_witness` (`:1003`), whose `!check_invariant(&small, inv).is_empty()` is **membership in one variant** — and **both directions are the same variant**, so a shrunk witness that flipped to **G→S-only** passes it. Because it calls `check_invariant` (singular), a shrunk witness that **gained an unrelated second defect** passes too. And §6 item 2d still said *"quote the shrunk witness"* — the unproduced-runtime-evidence defect revision E fixed in gate 6 **and did not carry one hop to item 2d** | The named test now asserts **the same three properties twice — raw and shrunk**. Gate 6 requires **both legs**; item 2d rewritten to revision E's source-assertion-plus-verdict model; §6 item 2e extended to both legs | + +**This finding is the two prior lessons colliding.** Revision E established that *a gate +must name evidence its artifact produces* and fixed gate 6 — **stopping one hop short of +item 2d**, which is the fix-propagation failure revisions A–D kept recording. And the +underlying gap is revision D's: **a requirement — "survives shrinking" — with nothing +able to fail it.** + +**The generalisable rule: `shrink` is a TRANSFORMATION, and a transformation's output +needs the same guarantees asserted of its input.** Requiring a fixture to "survive" a +transformation establishes only that *something* survived. Every property the input was +pinned for must be re-asserted on the output, or the transformation is free to change +what the fixture proves. + +**The pattern across revisions A–F 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 @@ -920,11 +940,27 @@ mechanism can detect a semantics change. They must be **updated, not deleted or invariant_21_negative_generator_breaks_staff_to_group_only ``` - It MUST assert, on `violating_score(StaffGroupMembershipAgreement, seed)`: + It MUST assert **the same three properties twice — before and after shrinking. THE + SHRUNK LEG IS ADDED IN REVISION F.** On `violating_score(StaffGroupMembershipAgreement, + seed)` **and again on `shrink(&that, StaffGroupMembershipAgreement)`**: + **(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. + > **The shrink leg was required by row 8 and observed by nothing.** The raw fixture was + > checked by this test; the shrunk one only by + > `every_invariant_shrinks_to_a_small_witness` (`:1003`), which asserts + > `!check_invariant(&small, inv).is_empty()`. **That is membership in a single + > `GraphInvariant` variant**, so a shrunk witness that flipped to **G→S-only** passes + > it — both directions are the same variant — and because it calls `check_invariant` + > (singular) rather than `check_invariants`, **a shrunk witness that gained an + > unrelated second defect passes too.** + > + > **`shrink` is a transformation, so its output needs the same guarantees as its + > input.** Requiring a fixture to "survive shrinking" without asserting *what survives* + > only establishes that something still fires. + > **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 @@ -955,12 +991,15 @@ mechanism can detect a semantics change. They must be **updated, not deleted or at execution", deferring a **static fact readable from the function body**. Corrected on review: a draft that can decide something must decide it, or it exports its own unfinished reading as execution work.)* -- **What `shrink` does impose is a fixture obligation**: `generators.rs:1025`–`:1026` - runs `shrink(&violating_score(inv, 7), inv)` for **every** variant, and `shrink` - asserts on entry that its input violates the target. **So invariant 21's fixture must - still violate 21 after greedy shrinking** — a fixture whose violation depends on - incidental structure that `shrink_candidates` removes will fail there, not in the - generator. +- **What the EXISTING `shrink` tests impose is weak, and revision F is why the named test + carries a shrunk leg.** `generators.rs:1025`–`:1026` runs + `shrink(&violating_score(inv, 7), inv)` for every variant, and `shrink` asserts on + entry that its input violates the target; `:1003` then checks the shrunk score with + `!check_invariant(&small, inv).is_empty()`. **Together these establish only that + *something* still fires** — a fixture whose violation depends on incidental structure + `shrink_candidates` removes fails there, which is real but is the *weakest* of the + three properties. **Direction and exactness after shrinking are guaranteed only by the + named test's shrunk leg.** **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 @@ -1122,6 +1161,10 @@ weakening is invisible. 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. + **The generator test's evidence covers BOTH its legs — revision F:** the raw fixture + **and the shrunk one**, each with the exact-set, witness-direction and + opposite-direction assertions. **A gate that accepts only the raw leg leaves `shrink` + free to change what the fixture proves.** **EVIDENCE MODEL — CHOSEN EXPLICITLY IN REVISION E. Quote the SOURCE assertions plus the pass verdict; do NOT claim a runtime return.** @@ -1270,15 +1313,21 @@ its evidence at `invariants.rs:69`–`:71` must stay intact. *(This item read "decide and report" and, before that, "all three counters and their new values" — the rule pin 10a had just corrected, surviving in its own report consumer. **Third site of one false claim**: the pin, touch row 11, and here.)* -2d. **Invariant 21's negative fixture survives `shrink`** — quote the shrunk witness and - confirm it still violates 21. **REWRITTEN on review:** this item asked whether - `shrink` matches `GraphInvariant` exhaustively, which is a **static fact the draft - 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. +2d. **Invariant 21's negative fixture survives `shrink` with its properties intact** — + evidenced by `invariant_21_negative_generator_breaks_staff_to_group_only`'s **shrunk + leg**, per gate 6's model: **the shrunk-leg assertions quoted from source, plus the + test's pass verdict.** + **REWRITTEN IN REVISION F — it said "quote the shrunk witness", which the test cannot + emit.** That is the same unproduced-runtime-evidence defect revision E fixed in gate 6 + **and did not carry one hop to this item**; and "still violates 21" was the weak + membership check that let a shrunk witness flip direction or gain a second defect. + *(Earlier still, this item asked whether `shrink` matches `GraphInvariant` + exhaustively — a **static fact the draft could read**: it does not, it calls + `check_invariant(score, inv)`.)* 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. + exact-set and direction assertions quoted from source**, per gate 6's evidence model, + **and for the generator test BOTH legs, raw and shrunk (revision F).** **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.