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

S16: ratification round 4 -- "the resulting value" is not a value when there are two reductions 

Whole-artifact review of 3e0a4d3 returned one blocking finding in round 3's own
harness.

Pin 7a collapsed two fixtures into one binding. t8b runs TWO authoring orders
(§0.5) -- two reductions over two different groups -- but pin 7a bound "the
resulting StaffGroup.members" and one filtered invariant result. A single
members local satisfies the harness as written while leaving either mutation's
required observation absent, depending on which order it came from; and the
invariant result filtered from the wrong reduction is the wrong verdict, not a
missing one.

Pin 7a now binds four, before any assertion:

  1. spurious-order OperationEffect  (M1: becomes an applied effect)
  2. spurious-order members          (M1: the spurious membership in the graph)
  3. missing-order members           (M2: stays empty)
  4. missing-order invariant-21 violations (M2: the disagreement left behind)

Every assertion formats all four, so whichever assertion a mutation trips
carries both of that mutation's observations. Gate 14 must now establish WHICH
ORDER each binding came from rather than counting bindings. M1 and M2 name
their own order at every mention.

Round 3 fixed the channel and left the fixtures conflated. It correctly
established that a failing test has one output channel and that state must be
bound before the assertion a mutation trips, then described the state as though
t8b had one reduction. The ordering rule was right and the inventory was wrong,
which is why the harness looked complete: three plausible bindings, none wrong
on its face, and nothing in the pin revealing that two of them are per-order.

The generalisable form: a definite article asserts uniqueness exactly as
silently as a number asserts a total. "The resulting value" reads as precise
and hides the question of which one -- the singular-noun cousin of the count
defects this contract has been removing since revision A.

And gate 14 inherited gate 12's defect before gate 12's fix could reach it.
Gate 12 was rewritten in revision H because a four-line aggregate proved a
population and not a pairing; gate 14 was written in round 3 requiring "three
bindings" -- the same shape, one section over, three rounds later. Ratification
round 1 recorded a fix failing to reach a declared peer; this is a fix failing
to reach a gate written after it.

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:57:18 +02:00
parent 3e0a4d38c1
commit e48bb8d0b4
No known key found for this signature in database
1 changed files with 79 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

106
spec/CONTRACT_P13S16_PROJECTION.md
View File

@ -368,6 +368,31 @@ observation is a single value under `assert_eq!`, the default diagnostic carries
`assert!(matches!(…))`, which prints nothing, and the report must say which form each
uses. Where it is composite or behind an unreachable assertion, a harness is required.
### RATIFICATION ROUND 4 — independent, whole-artifact, against `3e0a4d3`. One blocking finding.
| # | Finding | Disposition |
|---|---|---|
| **1** | **Pin 7a collapsed two fixtures into one binding.** `t8b` runs **two authoring orders** (§0.5) — two reductions over two different groups — but pin 7a bound *"the resulting `StaffGroup.members`"* and one filtered invariant result. **A single `members` local satisfies the harness while leaving either mutation's observation absent**, depending on which order it was taken from; the invariant result filtered from the wrong reduction is the *wrong verdict*, not a missing one | Pin 7a now binds **four**: spurious-order effect, spurious-order members, missing-order members, missing-order invariant-21 violations — **every** assertion formatting all four. **Gate 14** must establish **which order each binding came from**, not count bindings. **M1 and M2 name their own order** at every mention |
**Round 3 fixed the channel and left the fixtures conflated.** It correctly established
that a failing test has one output channel and that state must be bound before the
assertion a mutation trips — then described the state as though `t8b` had one reduction.
**The ordering rule was right and the inventory was wrong**, which is why the harness
looked complete: three plausible bindings, none of them wrong on its face, and no way to
tell from the pin that two of them are per-order.
**"The resulting value" is not a value when there are two reductions.** That is the
generalisable form, and it is the singular-noun cousin of the count defects: *a
definite article asserts uniqueness exactly as silently as a number asserts a total.*
Both read as precise and both hide the question of which one.
**And gate 14 inherited gate 12's defect before gate 12's fix could reach it.** Gate 12
was rewritten in revision H because a four-line aggregate proved a population and not a
pairing; gate 14 was written in round 3 requiring *"three bindings"* — **the same shape,
one section over, three rounds later.** It now requires the mapping. *(A fix reaching a
peer is what ratification round 1 recorded; this is a fix failing to reach a gate written
after it.)*
**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
caught row 11 and stopped before §6's consumer; rev D found pin 10a's *decision* still
@ -945,21 +970,33 @@ emits nothing but its assertion diagnostics**, so unless the state is in those
diagnostics it is unobtainable, and revision E already ruled out adding print
instrumentation for a report.
So `t8b` MUST:
**`t8b` exercises TWO authoring orders (§0.5), which are two reductions over two
different groups — so there are FOUR observations, not three. CORRECTED IN RATIFICATION
ROUND 4.** Bind all four to locals **before any assertion**:
1. **Bind all three observations to locals BEFORE the first assertion** — the
`OperationEffect` for the spurious-order `CreateStaffGroup`, the resulting
`StaffGroup.members`, and `check_invariants` filtered to
`StaffGroupMembershipAgreement`;
2. **format all three into EVERY assertion's failure message**, not just the assertion
they most obviously belong to.
| # | Binding | The mutation that needs it |
|---|---|---|
| 1 | **spurious-order `OperationEffect`** — `ContainerNotEmpty` when pin 1 holds | **M1**: becomes an applied effect |
| 2 | **spurious-order `StaffGroup.members`** | **M1**: carries the spurious membership that reached the graph |
| 3 | **missing-order `StaffGroup.members`** — `[s]` when pin 2 holds | **M2**: stays empty |
| 4 | **missing-order `check_invariants`, filtered to `StaffGroupMembershipAgreement`** | **M2**: the disagreement the empty projection leaves |
> **Requirement 2 is the load-bearing half, and ordering is why.** A failing test stops
> at its **first** failed assertion, so state carried only in a later assertion's message
> is never printed. Under M1 the spurious-order assertion fires; under M2 the
> missing-order one does — **different assertions, and each must carry the whole state**,
> or the mutation that trips the other one observes nothing. **Putting each value in
> "its own" assertion is exactly the arrangement that fails.**
**Then format ALL FOUR into EVERY assertion's failure message.**
> **Bindings 2 and 3 are different groups in different reductions, and an earlier draft
> of this pin collapsed them into one "resulting `StaffGroup.members`".** A single
> `members` local satisfies the harness as written **while leaving either mutation's
> required observation absent** — whichever order it was taken from. The invariant result
> has the same problem: filtered from the wrong reduction it is the wrong verdict, not a
> missing one. **A harness for two fixtures needs two sets of bindings; "the resulting
> value" is not a value when there are two reductions.**
>
> **The ordering rule is unchanged and still load-bearing.** A failing test stops at its
> **first** failed assertion, so state carried only in a later assertion's message is
> never printed. **Under M1 the spurious-order assertion fires; under M2 the
> missing-order one does** — different assertions, so each must carry the **whole** set.
> **Putting each value in "its own" assertion is exactly the arrangement that fails**,
> and splitting the set per order would reintroduce it one level down.
**Pin 8 — the four G3a undo-repair tests are re-verified, not assumed. NAMED by draft
amendment 1.** All four are in `crates/epiphany-ops/src/reduce.rs`:
@ -1338,18 +1375,22 @@ Applied, **run**, output recorded verbatim, restored **by hand-editing back**.
**M1 — the refusal fires. OBSERVATION TIGHTENED, draft amendment 1; CHANNEL PINNED IN
RATIFICATION ROUND 3.** Remove pin 1's emptiness check. **Required observation:** a
`CreateStaffGroup` carrying a **non-empty `members`** is now **applied instead of
refused** — the resulting `OperationEffect` and the minted `StaffGroup.members`, showing
the spurious membership that reached the graph. **Obtain them by quoting `t8b`'s
spurious-order assertion failure verbatim**, which pin 7a's harness requires to carry
all three observations. The assertion failing is the *symptom*; the applied mint is the
observation.
refused** — the **spurious-order** `OperationEffect` and the **spurious-order**
`StaffGroup.members`, showing the spurious membership that reached the graph. **Obtain
them by quoting `t8b`'s spurious-order assertion failure verbatim**, which pin 7a's
harness requires to carry **all four** of its bindings — so this mutation's two are
present whichever assertion fires. *(Read "all three observations" until round 4, when
pin 7a's collapsed `members` binding was split per authoring order.)* The assertion
failing is the *symptom*; the applied mint is the observation.
**M2 — the maintenance fires. OBSERVATION TIGHTENED, draft amendment 1; CHANNEL PINNED
IN RATIFICATION ROUND 3.** Remove pin 2's append. **Required observation:** after a
`CreateStaff` naming a live group, `StaffGroup.members` is **still empty**, and invariant
21's verdict on that state. **Obtain both by quoting `t8b`'s missing-order assertion
failure verbatim** — the same harness, a different assertion, which is why pin 7a
requires every assertion to carry the whole state.
`CreateStaff` naming a live group, the **missing-order** `StaffGroup.members` is **still
empty**, and the **missing-order** invariant-21 verdict on that state. **Obtain both by
quoting `t8b`'s missing-order assertion failure verbatim** — the same harness, a
different assertion and **a different reduction from M1's**, which is why pin 7a binds
`members` and the invariant result **per authoring order** and requires every assertion
to carry all four.
**M3 — the re-carry stays idempotent.** Make pin 3 write maintained members into
`staff_group_values`; a byte-identical re-carry must degrade from
@ -1651,11 +1692,22 @@ weakening is invisible.
formatted in. **M5 can only report what these messages print**, so a harness this
gate does not check is a mutation that observes nothing.
14. **Pin 7a's observation harness in `t8b` — ADDED IN RATIFICATION ROUND 3.** Quote from
source: the three bindings above `t8b`'s first assertion, and **every** assertion's
failure message showing all three formatted in. **Both M1 and M2 draw their required
observations from these messages, via different assertions** — so a message carrying
only "its own" value silently disarms whichever mutation trips the other one.
14. **Pin 7a's observation harness in `t8b` — ADDED IN RATIFICATION ROUND 3, CORRECTED IN
ROUND 4.** Quote from source, above `t8b`'s first assertion, **all four** bindings —
**spurious-order effect, spurious-order members, missing-order members, missing-order
invariant-21 violations** — and **every** assertion's failure message showing **all
four** formatted in.
**Confirm bindings 2 and 3 come from the two different reductions**, not one value
reused: they are different groups, and a single `members` local satisfies a
four-line-shaped check while leaving one mutation's observation absent. **Name which
order each binding was taken from.**
> **Both M1 and M2 draw their observations from these messages, via different
> assertions** — so a message carrying only "its own" values silently disarms
> whichever mutation trips the other one. **This gate must establish a mapping from
> each binding to its order, not a count of bindings** — gate 12's lesson, one
> section over.
---