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

S16 draft amendment 1 rev H: where a gate must establish a mapping, it cannot count 

Independent review of 09d8439 returned one blocking finding. A sweep found a
second of the same family.

1. Gate 12's four-line aggregate could pass with one surface missing. Both
   definitions can exist (2 lines) while check_invariants calls
   check_staff_names_absent_group TWICE and check_group_lists_unowned_staff
   NEVER (2 lines). Four lines total, the stated "fewer than four fails" rule
   reports success, and M6b has no call site to delete.

   Replaced by four independent grep -c checks, each required to be exactly 1
   -- so a count ABOVE 1 now fails too, catching the doubled dispatch
   directly. Plus quoted context, because a count is not a mapping: each
   definition with its enclosing impl GraphIndex<'_> header, proving it is a
   method on the type check_invariants builds; each dispatch with the pub fn
   check_invariants header, proving the call is in the dispatcher M6 edits and
   not in a test or a second dispatcher.

   This is the contract's oldest defect class in new clothes. Revisions A-C
   removed counts that had gone stale; this one was never right -- an
   aggregate can be satisfied by the wrong distribution of the same total.
   Where a gate must establish a mapping, it cannot count. It has to check
   each element on its own, which is the structural sibling of the rule this
   document already carries: where a claim requires completeness, do not
   enumerate, derive.

2. Sweep: gate 8 asserted an absence with no method. "contains the
   empty-members refusal and no member-liveness/TargetMissing path" named no
   command, and a TargetMissing path can be spelled without either literal, so
   any grep would prove only that a chosen string is gone. Method pinned:
   quote create_staff_group's production body in full to the #[cfg(test)]
   boundary and read it, explicitly not a grep -- S27's gate-6a lesson and the
   reason its gate 6c quotes a definition rather than searching for it. M8
   signs exactly this gate, so a vacuous gate 8 leaves M8's deletion
   unobserved.

Both findings are gates that report success without observing what they
claim. One counted instead of pairing; the other asserted an absence with
nothing able to establish it. A structural gate needs a method, and the method
must distinguish the passing case from every failing one -- not merely from
the most obvious failing one.

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:
Levi Neuwirth 2026-08-09 18:09:08 +02:00
parent 09d8439c93
commit 5d2db937e9
No known key found for this signature in database
1 changed files with 59 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

67
spec/CONTRACT_P13S16_PROJECTION.md
View File

@ -203,7 +203,28 @@ method per invariant is the crate's existing shape. And a shared helper the two
both call is explicitly permitted — **the deletable call site is what M6 needs, not a both call is explicitly permitted — **the deletable call site is what M6 needs, not a
duplicated walk.** duplicated walk.**
**The pattern across revisions A–G is sharper than any individual finding: a correction ### Draft amendment 1, revision H — independent review of `09d8439`
**One blocking finding, and one of the same family found by sweeping.**
| # | Finding | Disposition |
|---|---|---|
| **1** | **Gate 12's four-line aggregate could pass with one surface missing.** Both definitions can exist (2 lines) while `check_invariants` calls `check_staff_names_absent_group` **twice** and `check_group_lists_unowned_staff` **never** (2 lines) — **four lines, gate passes, and M6b has no call site to delete.** The count proved a population, never a pairing | Replaced by **four independent `grep -c` checks, each required to be exactly `1`** — a count **above** 1 now also fails — plus **quoted context**: each definition with its enclosing `impl GraphIndex<'_>` header, each dispatch with the `pub fn check_invariants` header |
| 2 | *(sweep)* **Gate 8 asserted an absence with no method.** *"contains the empty-members refusal and no member-liveness/`TargetMissing` path"* named no command, and a `TargetMissing` path can be spelled without either literal | **Method pinned: quote the production body in full and read it**, explicitly not a grep. S27's gate-6a lesson; **M8 signs exactly this**, so a vacuous gate 8 leaves M8's deletion unobserved |
**Finding 1 is the count-versus-mapping failure, and it is this contract's oldest defect
class wearing new clothes.** Revisions A–C removed counts that had gone *stale*; this one
was **never right** — an aggregate can be satisfied by the wrong distribution of the
same total. **Where a gate must establish a mapping, it cannot count.** It has to check
each element on its own, which is the structural sibling of the rule this document
already carries: *where a claim requires completeness, do not enumerate — derive.*
**Both findings are gates that report success without observing what they claim.** One
counted instead of pairing; the other asserted an absence with nothing able to establish
it. **A structural gate needs a method, and the method must distinguish the passing case
from every failing one** — not merely from the most obvious failing one.
**The pattern across revisions A–H 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
deferred after two reworders. Rev A removed item 1's mutation tally and left item 2's deferred after two reworders. Rev A removed item 1's mutation tally and left item 2's
@ -1263,6 +1284,14 @@ weakening is invisible.
gate tallies beside it were removed. Pin 8's table is the origin.)* gate tallies beside it were removed. Pin 8's table is the origin.)*
8. The pin-1 structural gate: `create_staff_group`'s production body contains 8. The pin-1 structural gate: `create_staff_group`'s production body contains
the empty-members refusal and no member-liveness/`TargetMissing` path. the empty-members refusal and no member-liveness/`TargetMissing` path.
**METHOD PINNED IN REVISION H — it named none.** **Quote `create_staff_group`'s
production body in full** (to the `#[cfg(test)]` boundary) and read it; report the
refusal's lines and state that no member-liveness or `TargetMissing` path remains.
**Do not establish the absence by grep**: a `TargetMissing` path can be spelled
without either literal, so **a grep for absence proves only that a chosen string is
gone** — S27's gate-6a lesson, and the reason its gate 6c quotes a definition rather
than searching for it. **This is also what M8 signs**, so a vacuous gate 8 makes M8's
deletion unobserved.
9. `t8c` (pin 3a) and `t8d` (pin 4a) both present and passing, by name. 9. `t8c` (pin 3a) and `t8d` (pin 4a) both present and passing, by name.
10. **Pin 12's bump landed, by value comparison — ADDED BY DRAFT AMENDMENT 1.** 10. **Pin 12's bump landed, by value comparison — ADDED BY DRAFT AMENDMENT 1.**
``` ```
@ -1300,17 +1329,39 @@ weakening is invisible.
mutation surface exists **before** M6 is attempted rather than discovering its mutation surface exists **before** M6 is attempted rather than discovering its
absence mid-run. absence mid-run.
**FOUR INDEPENDENT CHECKS, each required to be EXACTLY ONE. REWRITTEN IN REVISION H
— the aggregate count it replaced could pass with one surface missing.**
``` ```
grep -n "fn check_staff_names_absent_group\|fn check_group_lists_unowned_staff" crates/epiphany-core/src/invariants.rs grep -c "fn check_staff_names_absent_group" crates/epiphany-core/src/invariants.rs # a → 1
grep -n "idx.check_staff_names_absent_group\|idx.check_group_lists_unowned_staff" crates/epiphany-core/src/invariants.rs grep -c "fn check_group_lists_unowned_staff" crates/epiphany-core/src/invariants.rs # b → 1
grep -c "idx.check_staff_names_absent_group(&mut v)" crates/epiphany-core/src/invariants.rs # c → 1
grep -c "idx.check_group_lists_unowned_staff(&mut v)" crates/epiphany-core/src/invariants.rs # d → 1
``` ```
→ **two definitions and two call sites, four lines total.** **Quote all four**, per **Report all four counts separately. Any count other than exactly `1` is a pin 6b
gate 6's evidence model. **Fewer than four is a pin 6b violation and a finding**, not violation and a finding** — including a count **greater** than 1, which means a
a gate to be worked around: one definition with a direction parameter, or one call duplicated definition or a doubled dispatch.
site handling both, means M6 has no independently deletable surface.
> **A grep for presence is defeated by a rename**, so the names in pin 6b are pinned **And quote the context, because a count is not a mapping:**
- **each definition with its enclosing `impl GraphIndex<'_>` header**, proving the
method belongs to the type `check_invariants` builds — not a free function, not a
method on some other type that merely shares the name;
- **each dispatch with the `pub fn check_invariants` header above it**, proving the
call is in the dispatcher M6 will edit — not in a test, a helper, or a second
dispatcher.
> **What the previous version permitted, stated so it is not reintroduced.** It ran
> two alternation greps and required *"four lines total"*. **Both definitions can
> exist (2 lines) while `check_invariants` calls `check_staff_names_absent_group`
> **twice** and `check_group_lists_unowned_staff` **never** (2 lines) — four lines,
> gate passes, and M6b has no call site to delete.** The aggregate proved a
> population, never a pairing. **Where a gate must establish a MAPPING, it cannot
> count** — it has to check each element on its own, which is the same shape as this
> contract's rule against enumerating where completeness is required.
>
> **A grep for presence is also defeated by a rename**, so pin 6b's names are pinned
> and this gate and M6 both use them. If the implementation chose other names, **that > and this gate and M6 both use them. If the implementation chose other names, **that
> is the finding** — the gate has not "passed with zero matches", it has failed. > is the finding** — the gate has not "passed with zero matches", it has failed.