P13-S29 RATIFIED; pins frozen, dispatched
Graph invariant 10 reported Chapter 3 and Chapter 4 failures under its own number, through a public API: check_invariant is pub and re-exported, and Display rendered a tempo rule as "invariant 10 (CrossCuttingRefsResolve) violated". Disposition (b), type-neutral: InvariantViolation becomes WellFormednessViolation carrying a two-armed ViolationKind. check_invariants stays comprehensive, so every broad caller keeps its rule coverage; the deliberate behaviour change is that check_invariant narrows to the invariant arm, with a symmetric check_requirement added. GraphInvariant does not move -- 21 variants, unchanged, and no new negative generator or shrink obligation. req:time:tempo-segment-shape is minted for the one rider that had no label, stating the enforced shape/end_tempo compatibility without resolving P13-S8's canonical-form question, so the label survives whichever spelling S8 ratifies. Eighteen review rounds. Four mutation radii were measured against disposable implementations rather than derived, and every one of the four differed from what static reading predicted: M2a by ten false positives and seventeen omissions, M17-C1 by naming seven where eighteen fail and including a test that belongs to C2, M17-C2 and C3 by predicting observers that measurement put at one and zero. Two of those measurements first produced a compile error reporting zero failures -- a compile error observes nothing -- and one misread cargo test's "error: test failed" as a compilation signal; only the third method is pinned. Several defects were structural rather than arithmetic. Both selectors could have matched their arm while ignoring their payload, satisfied by every fixture presenting a single variant or label. A complete third ViolationKind arm, or a fully implemented 22nd GraphInvariant omitted from all(), compiles and leaves every gate green -- a variant nothing enumerates is a variant nothing observes. The accidental tests identified their rule by a witness suffix this rung deletes, so a selector-only migration would have left two negatives green and vacuous. And invariants.rs:8 carries the old type name in retained header prose, which would have made gate 6 unsatisfiable. Prerequisite review scaffolding, applied earlier under a narrow authorization and committed here because ratification is what changes its staging state: one temporary DISCUSSED_NOT_CITED row for req:time:tempo-segment-shape, deleted by pin 3 when the requirement lands, with landing gates for its absence and for the baseline being green because the label is defined rather than still allowlisted. Baseline unchanged at 43 suites, 1586 passing; no implementation target has been modified. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
This commit is contained in:
parent
3fda93bc6b
commit
cea21cd8f9
|
|
@ -397,6 +397,16 @@ const DISCUSSED_NOT_CITED: &[(&str, &str)] = &[
|
|||
spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md and recorded in \
|
||||
spec/EVIDENCE_P13S26_EXECUTION.md as M6's verbatim diagnostic. PERMANENT.",
|
||||
),
|
||||
(
|
||||
"req:time:tempo-segment-shape",
|
||||
"proposed by spec/CONTRACT_P13S29_VIOLATION_KIND.md; the requirement does not \
|
||||
exist until that contract's pin 3 lands. TEMPORARY -- pin 3 REMOVES this row \
|
||||
when it mints the requirement, because this row's own claim (discussed, never \
|
||||
cited) becomes false at that moment. A stale row is inert, so nothing else \
|
||||
will catch it; that contract's landing gate does. Remove by hand if S29 is \
|
||||
abandoned or the label changes. Prerequisite review scaffolding, NOT dispatch: \
|
||||
it licenses no other pin work.",
|
||||
),
|
||||
];
|
||||
|
||||
fn requirement_strings(text: &str) -> BTreeSet<String> {
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue