Independent review of d06e2f7 returned six findings, five blocking, all in
draft amendment 1's own text. A sweep found a seventh: the same false claim at
a second site.
1. Report item 2d asked execution to decide a static fact the draft could
read. shrink (generators.rs:932) does NOT match GraphInvariant -- it calls
check_invariant(score, inv). The unverified claim was made twice, in item
2d and in touch row 8. Both corrected. Item 2d replaced with the real
obligation: invariant 21's fixture must survive shrinking (:1025), since
shrink asserts on entry that its input still violates the target.
2. Pin 10a's "all three counters move if either document mints a label" is
false. CORE_REQUIREMENT_COUNT is asserted only against core_spec.tex
(requirement_labels.rs:259); a label in operation_catalog.tex moves the two
suite counters only. Replaced with a per-document table.
Sweep finding: touch row 11 carried the same false sentence and was left
standing while pin 10a was fixed -- the fix-one-site defect, committed
inside the edit that fixed the other site. Row 11 now points at pin 10a
rather than restating it.
3. Gate 11 permitted the exact tautology it exists to prevent. "Updated, not
silenced" does not forbid replacing the literals with
CURRENT_REDUCTION_ALGORITHM_VERSION -- the tidiest-looking update, after
which both operands move together and M5a/M5b are vacuous. Rewritten as
11a-e requiring independent literal 1 values, never the constant, each
quoted. S27 round 3 caught this substitution and roundtrip.rs:882 forbids
it by name.
4. Gate 11 omitted roundtrip.rs:947, test 10b's mutation-only Err arm. Left at
0, M5b aborts on the base comparison before reaching the two-field panic
that is its required observation -- failing at the wrong assertion while
observing nothing. Added as 11d, with 11e for the literal-preservation
comments whose reasoning is what stops the next rung making substitution 3.
5. §6 demanded "the nine mutations (M1-M9)" while M7's split makes ten
executions. Count removed; §3 is the single origin.
6. Pin 12 said no gate catches a missed bump except the tripwires, written in
the same amendment that added gate 10, which compares the value against
HEAD directly. Split: gate 10 guards this bump, 11a-e guard the wiring,
only the general future case stays undetectable.
Tightening folded in with finding 1: M6's two fixtures must each violate ONE
direction only. A fixture disagreeing in both is still reported after either
arm is deleted, so the mutation appears to fail correctly while signing
nothing. The same trap applies to touch row 8's generator, whose all()-driven
consumers only ask whether 21 is reported.
Findings 1, 2, 3 and 6 share one root cause: an S27 conclusion applied without
re-derivation. S27's "name all three counters," its "no mechanism can detect a
semantics change," and its literal-independence rule are true statements about
S27; two are false or incomplete here and one was dropped where it was needed.
A ratified contract is reusable as a source of questions, not of answers.
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
Levi Neuwirth
3096c54d09