neuwirth
/
epiphany
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

S16: ratification round 11 -- rederive m40 locators

This commit is contained in:
Levi Neuwirth 2026-08-09 20:47:46 +02:00
parent 63a2dc8ce7
commit 25b492575e
No known key found for this signature in database
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
spec/CONTRACT_P13S16_PROJECTION.md
View File

@ -986,7 +986,7 @@ here; that is S26's rung).
**The count is not the test.** `all().len() == 21` passes with the dispatch arm
deleted — the project already knows this, which is why
`m40_check_invariants_dispatches_invariant_20` exists
(`invariants.rs:6045`–`:6066`, whose own doc says *"`all().len() == 20` passes
(`invariants.rs:6060`–`:6135`, whose own doc says *"`all().len() == 20` passes
even with the dispatch arm deleted, so this row must instead show a score
violating ONLY invariant 20 is actually flagged by the top-level
`check_invariants` entry point"*). Pin 6 requires the **same behavioural shape**:
@ -1839,7 +1839,7 @@ weakening is invisible.
status`, not by inspection.
6. Invariant 21 is reached **through `check_invariants`** on a score violating
only it, in the shape of `m40_check_invariants_dispatches_invariant_20`
(`invariants.rs:6045`) — **for BOTH directions, by pin 6a's two named tests**:
(`invariants.rs:6063`) — **for BOTH directions, by pin 6a's two named tests**:
`m41_check_invariants_dispatches_invariant_21_staff_names_absent_group` **and**
`m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff`. **Both run,
both verdicts reported, and each confirmed to satisfy the direction it does not