S16: ratification round 5 -- the assert macro is part of the channel
Whole-artifact review of e48bb8d returned one blocking finding: M6 was not
covered by round 3's own channel rule.
Pin 6a requires an exact violation set without saying how, so a conforming
assert!(violations.len() == 1 && ...) satisfies it and prints nothing on
failure -- and that assertion is precisely what M6 trips. Gate 6 and §6 item 2e
use the passing-test model, source assertions plus ok. So M6 reverted to "the
named test failed", the signature this contract rejects.
Pin 6a gains a harness for m41, m41b and the generator test: bind
check_invariants to a local before any assertion; make the cardinality check an
assert_eq! on that local with the full violations vector in its diagnostic; and
make it the first assertion after the bindings, since it is the one M6 trips.
Gate 6 now confirms the macro. M6a/M6b quote the failing output plus the
sibling's pass verdict.
Round 3 wrote the channel rule and applied it to M1, M2 and M5 -- the
mutations named in that round's finding -- and not to M6, which has the
identical need. Round 3's text even carved M6 out, listing it among mutations
that "already met the standard": true of its behavioural observation, which
names the state, and false of its channel, which had none.
The macro is part of the channel, not a style choice. assert_eq! prints
left/right; assert! prints only its message. Under M6a the S->G arm is gone,
check_invariants returns empty for m41's fixture, and assert_eq! prints 0
against 1 with an empty vector -- that is "the violation went unreported",
quoted rather than inferred. With assert! the same requirement is met with no
evidence. Where a mutation's observation IS the compared value, the pin must
name the macro; the rule is now at the head of §3 rather than left to each
mutation.
A second gap closed with it. M6a also breaks the generator test, since that
fixture is S->G. Unstated, an executor either reports a defect that is not one
or ignores a failure it cannot classify. M6b leaving the generator green is now
recorded as positive evidence that touch row 8's pinned direction holds. A
mutation must state every test it is expected to break, or its blast radius is
discovered instead of specified.
Still DRAFT, still unratified. No implementation work has begun.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
This commit is contained in:
parent
e48bb8d0b4
commit
85429d6243
|
|
@ -393,6 +393,32 @@ one section over, three rounds later.** It now requires the mapping. *(A fix rea
|
|||
peer is what ratification round 1 recorded; this is a fix failing to reach a gate written
|
||||
after it.)*
|
||||
|
||||
### RATIFICATION ROUND 5 — independent, whole-artifact, against `e48bb8d`. One blocking finding.
|
||||
|
||||
| # | Finding | Disposition |
|
||||
|---|---|---|
|
||||
| **1** | **M6 was not covered by round 3's own channel rule.** Pin 6a requires an *exact violation set* without saying **how**, so a conforming `assert!(violations.len() == 1 && …)` satisfies it and **prints nothing on failure** — and that assertion is precisely what M6 trips. Gate 6 and §6 2e use the **passing**-test model. **So M6 reverts to "the named test failed"**, the signature this contract rejects | **Pin 6a gains a harness** for `m41`, `m41b` **and** the generator test: bind `check_invariants` before any assertion; make the cardinality check an **`assert_eq!`** on that local **with the violations vector in its diagnostic**; make it the **first** assertion. **Gate 6 confirms the macro.** M6a/M6b quote the failing output, the sibling's pass verdict, **and the generator test's outcome** |
|
||||
|
||||
**Round 3 wrote the channel rule and applied it to M1, M2 and M5 — the mutations named in
|
||||
that round's finding — and not to M6**, which has the identical need. Round 3's own text
|
||||
even carved M6 out, listing it among the mutations that *"already met the standard"*: true
|
||||
of its **behavioural** observation, which names the state, and false of its **channel**,
|
||||
which had none.
|
||||
|
||||
**The macro is part of the channel.** `assert_eq!` prints `left`/`right`; `assert!` prints
|
||||
only its message. Under M6a the S→G arm is gone, `check_invariants` returns **empty** for
|
||||
`m41`'s fixture, and `assert_eq!` prints `0` against `1` with an empty vector — **that is
|
||||
"the violation went unreported", quoted rather than inferred.** With `assert!` the same
|
||||
requirement is met with no evidence. **Where a mutation's observation *is* the compared
|
||||
value, the pin must name the macro** — a rule now recorded at the head of §3 rather than
|
||||
left to each mutation.
|
||||
|
||||
**A second gap closed with it: M6a breaks the generator test too**, since that fixture is
|
||||
S→G. Unstated, an executor either reports a defect that is not one or ignores a failure it
|
||||
cannot classify. **M6b leaving the generator green is now positive evidence** that touch
|
||||
row 8's pinned direction holds. **A mutation must state every test it is expected to
|
||||
break** — otherwise its blast radius is discovered instead of specified.
|
||||
|
||||
**The pattern across revisions A–J 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
|
||||
|
|
@ -913,6 +939,34 @@ So each of `m41` / `m41b` MUST assert:
|
|||
> imports its blind spots along with its virtue**, and m40 never needed exactness because
|
||||
> nothing about invariant 20 turned on it.
|
||||
|
||||
**OBSERVATION HARNESS — ADDED IN RATIFICATION ROUND 5. M6 was not covered by the
|
||||
round-3 channel rule.**
|
||||
|
||||
Requirement 1 says *exact set* and does not say **how**, so a conforming
|
||||
`assert!(violations.len() == 1 && violations[0].invariant == …)` satisfies it **and prints
|
||||
nothing on failure**. Under M6 that assertion is exactly what fails — and M6's required
|
||||
observation is that the mutated fixture went **unreported**, which the diagnostic would
|
||||
not show. **M6 would fall back to "the named test failed", the signature this contract
|
||||
rejects.**
|
||||
|
||||
So in **each** of `m41`, `m41b` **and**
|
||||
`invariant_21_negative_generator_breaks_staff_to_group_only`:
|
||||
|
||||
1. **Bind `check_invariants(&s)` to a local before any assertion.**
|
||||
2. **Requirement 1's cardinality check MUST be an `assert_eq!` on that local's length,
|
||||
with the full violations vector formatted into its diagnostic**, e.g.
|
||||
`assert_eq!(violations.len(), 1, "expected exactly the invariant-21 violation, got {violations:?}")`.
|
||||
3. **It MUST be the first assertion after the bindings** — it is the one M6 trips, and
|
||||
the round-3 ordering rule applies: state behind a later assertion is unreachable.
|
||||
|
||||
> **`assert_eq!` is required rather than suggested because its default `left`/`right`
|
||||
> diagnostic is the observation.** Under M6a the S→G arm is gone, `check_invariants`
|
||||
> returns an **empty** set for `m41`'s fixture, and the diagnostic prints `0` against `1`
|
||||
> with an empty vector — **that is "the violation went unreported", quoted rather than
|
||||
> inferred.** `assert!` on the same condition prints only the message, so the identical
|
||||
> requirement is met with and without evidence depending on a macro choice the pin had
|
||||
> left open.
|
||||
|
||||
**Pin 6b — the MUTATION SURFACE is pinned, not just the behaviour. ADDED IN REVISION G.**
|
||||
|
||||
Pin 6 and pin 6a specify **behaviour only**, and **a conforming implementation can
|
||||
|
|
@ -1366,7 +1420,12 @@ Applied, **run**, output recorded verbatim, restored **by hand-editing back**.
|
|||
> - Where the observation is **composite**, or lives behind an assertion the mutation
|
||||
> makes unreachable, the test needs a **pinned observation harness** — bind the values
|
||||
> before the assertions and format them into every relevant message. **That is pins 7a
|
||||
> (`t8b`, for M1/M2) and 5a (`u5`, for M5).**
|
||||
> (`t8b`, for M1/M2), 5a (`u5`, for M5) and 6a (`m41`/`m41b` and the generator test, for
|
||||
> M6 — added in ratification round 5).**
|
||||
> - **The macro is part of the channel, not a style choice.** `assert_eq!` prints
|
||||
> `left`/`right`; `assert!` prints only its message. **Where a mutation's observation
|
||||
> *is* the compared value, the pin must require `assert_eq!`** — otherwise the same
|
||||
> requirement is satisfiable with and without evidence.
|
||||
>
|
||||
> **Revision E chose "quote the source assertion plus the pass verdict" for gates, which
|
||||
> is right for a PASSING test. Mutations need the failing case, and the failing case has
|
||||
|
|
@ -1450,6 +1509,24 @@ bound in revision C, surface pinned in REVISION G:**
|
|||
→ `m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff` must fail,
|
||||
**and `m41` must still pass.**
|
||||
|
||||
**Each half reports, per ratification round 5:**
|
||||
|
||||
1. **The failing test's `assert_eq!` output verbatim** — pin 6a's harness makes it print
|
||||
the cardinality it got against `1`, with the violations vector, so the observation is
|
||||
*"the mutated fixture went unreported"* rather than *"a test failed"*;
|
||||
2. **the sibling test's pass verdict**, which is what shows the two arms independent;
|
||||
3. **the generator test's outcome**, which differs between the halves and is itself
|
||||
evidence: **M6a must also fail `invariant_21_negative_generator_breaks_staff_to_group_only`**
|
||||
— its fixture is S→G, so deleting that arm silences it too — **while M6b must leave it
|
||||
passing**, because the generator violates S→G only. **M6b leaving it green is
|
||||
independent confirmation of the direction pinned in touch row 8**, and M6a's extra
|
||||
failure is **expected, not a finding**.
|
||||
|
||||
> **Point 3 exists because an unannounced third failure reads as a finding.** M6a breaks
|
||||
> two tests by design; without saying so, an executor either reports a defect that is not
|
||||
> one or quietly ignores a failure it cannot classify. **A mutation must state every test
|
||||
> it is expected to break**, or its blast radius is discovered instead of specified.
|
||||
|
||||
**Each deletion is a single named call site**, which is what makes the two independently
|
||||
removable. *(M6 previously said "delete each arm in turn" while pin 6 required only
|
||||
behaviour — so against a single-shared-check implementation there were no two arms and
|
||||
|
|
@ -1560,7 +1637,12 @@ weakening is invisible.
|
|||
|
||||
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.
|
||||
invariant-identity assertions, and the witness-id assertion. **It MUST be an
|
||||
`assert_eq!` on a `check_invariants` local bound above it, with the violations
|
||||
vector in its diagnostic, and MUST be the first assertion after the bindings —
|
||||
pin 6a's harness, ratification round 5. Confirm the macro is `assert_eq!` and not
|
||||
`assert!`**: M6 draws its whole observation from that macro's `left`/`right` output,
|
||||
so an `assert!` satisfies pin 6a and disarms M6.
|
||||
2. **The test's pass verdict** from `cargo test`.
|
||||
|
||||
**A passing exact-set assertion IS the observation**; the assertion text says what was
|
||||
|
|
|
|||
Loading…
Reference in New Issue