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
|
peer is what ratification round 1 recorded; this is a fix failing to reach a gate written
|
||||||
after it.)*
|
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
|
**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
|
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
|
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
|
> imports its blind spots along with its virtue**, and m40 never needed exactness because
|
||||||
> nothing about invariant 20 turned on it.
|
> 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 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
|
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
|
> - Where the observation is **composite**, or lives behind an assertion the mutation
|
||||||
> makes unreachable, the test needs a **pinned observation harness** — bind the values
|
> 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
|
> 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
|
> **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
|
> 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,
|
→ `m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff` must fail,
|
||||||
**and `m41` must still pass.**
|
**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
|
**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
|
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
|
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:
|
So for each of the three tests, the report gives:
|
||||||
1. **The exact-set assertion, quoted verbatim from source** — the `len() == 1` and
|
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`.
|
2. **The test's pass verdict** from `cargo test`.
|
||||||
|
|
||||||
**A passing exact-set assertion IS the observation**; the assertion text says what was
|
**A passing exact-set assertion IS the observation**; the assertion text says what was
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue