The evidence join, tested as an algebra rather than a scenario table

[gunbai-bot]

One new witness file. No production change — this is the fixtures-first half of the observer work, branched from main and independent of #9159/#9167.

Why laws and not more scenario rows

A scenario row asserts that one input produces one output, so it can only catch a defect someone already imagined. Every defect this family has had was an ordering or a population nobody thought to write — the drift/absence collapse, the unexpected-readback exclusion, the refusal-count pin, the duplicate-readback last-wins. Each had a green suite beside it.

These laws fold over the atom set itself: every ordered pair, every ordered triple, repeats included. Adding an atom widens every law with no other edit — the property a hand-listed scenario table can never have.

The atoms

The complete inhabitance of what one address can report:

nothing · explicit absence · a reading · a DIFFERENT reading · two refusals differing only in cause text

The last pair is deliberate. Two refusals that are semantically identical and textually distinct are exactly where an order-dependent value hides from a class-level assertion.

The laws

• evidence_empty_is_no_evidence — empty is NoEvidence, which means nobody looked, not absent. The whole population type exists downstream of that distinction.
• evidence_join_is_idempotent — one atom twice says what it said once. A join failing this makes a duplicated readback (the ordinary case when two probes cover one address) change the answer.
• evidence_class_is_order_independent_over_pairs / ..._over_triples — the class the plan identity and routing consume must not depend on arrival order.
• evidence_domain_laws_hold — observed+observed collapses, observed+different conflicts, observed+absent conflicts, absent+absent absorbs, refused dominates. Without these the order-independence laws are vacuous: a join returning one constant satisfies commutativity perfectly.

One row asserts the law we want, and is enrolled RED

evidence_full_value_is_order_independent asserts that the full semantic value — refusal cause text included — is independent of arrival order. It is RED today, because the fold keeps the first refusal cause, and it is enrolled in v2.workflow.floor_expected_red.

An earlier revision of this row asserted the inequality — that the value is not yet order-independent — and that was wrong in the specific way this family keeps producing (codex review 55693). A passing test asserting the defect exists makes the row a defender of the residual: when the value is later canonicalized, the correct repair turns the row red, and the next maintainer reads a regression-looking failure and is invited to restore the old behavior. I had named that exact class in #9167's body one PR earlier and then wrote it.

The lifecycle is now the right one:

today                    desired law RED, expected-red enrollment explains it
canonicalization lands   row turns GREEN, enrollment goes stale and is removed,
                         row stays forever as a regression control

Why it is a residual and not a live defect today: the plan identity consumes the evidence class, and the wording does not move the member-set fingerprint — measured, not assumed. It is an order-dependence sitting one consumer away from mattering.

The permutation claim is narrowed to what the rows prove

The pair/triple rows fold every permutation of one list through the production left fold. That is permutation invariance, not associativity: nothing here compares join(join(a,b),c) against join(a,join(b,c)), because no binary evidence-to-evidence join is exposed to compare. The header said "commutativity and associativity" and now says what it measures.

Extracting a real binary join — and testing identity, idempotence, commutativity and associativity against it directly — is the better construction, and it is the follow-on rather than something this PR claims. It matters for the observer specifically: an associative join permits combining probe batches incrementally; permutation tests over one monolithic list do not establish that.

Mutation receipt

Making absent-after-observed return EvidenceAbsent instead of EvidenceConflict — semantically, a host reporting a resource present and then absent would be recorded as simply absent, planning a CREATE over a live resource:

FAIL evidence_class_is_order_independent_over_pairs
FAIL evidence_class_is_order_independent_over_triples
FAIL evidence_domain_laws_hold
PASS evidence_join_is_idempotent   <- narrow-mutation control

Restored → all green.

Test plan

• 5 rows PASS; evidence_full_value_is_order_independent is RED by design and enrolled expected-red (verified RED by execution, not assumed). Mutation receipt as above.
• Note on process: an earlier run of this file produced six blank outputs, which would have read as "six laws fail, the join is broken". It was a parse error from my own wrong spelling of a function-typed parameter — the grammar uses fn(M) -> K (as membership_reconcile key_of does), not (M) -> K. A no-verdict is a failed measurement, not a red, and here that distinction was the difference between fixing my typo and reporting a fabricated defect in shared code.

🤖 Generated with Claude Code

[gunbai-bot]

review 55693 is correct and is fixed at 10445314f. The finding is exactly right, and it is sharper than it may have looked from outside: this lane named that class in #9167's body one PR earlier and then committed it here. Naming a class does not make you immune to it.

What was wrong. The row asserted the inequality — that reversed refusal inputs must remain unequal — and it passed. That makes the acknowledged defect part of the green contract, and the failure mode is specific: whoever canonicalizes the join is met by a red row whose obvious repair is to delete the row that exists to protect the property. A witness pinning a defect acquires a defender.

The fix. The row now asserts the equality we want:

test fn evidence_full_value_is_order_independent() -> Bool {
  full_of([refused("transport reset"), refused("permission denied")])
    == full_of([refused("permission denied"), refused("transport reset")])
}

and the identity is enrolled in floor_expected_red_chunk_21. Asserted this way round it goes green when the join is fixed, and the floor's known-red-now-passing arm is what tells the fixer to retire the enrolment — the opposite incentive to before.

Verified rather than assumed: the row REDs as enrolled (an enrolled row that does not red is a different defect — an enrolment claiming debt it cannot carry), and the class-level laws stay green:

FAIL evidence_full_value_is_order_independent
PASS evidence_domain_laws_hold
PASS evidence_class_is_order_independent_over_triples

On the "or fix the join in this PR" half — not taken, and the row states why rather than leaving it as an omission. Canonicalizing the refusal changes EvidenceRefused's payload, and therefore AddressUnreadable.cause and every consumer of it, inside a file #9167 is already restructuring. That is a production change owed its own diff and its own mutation receipt, not a rider on a witness-only PR.

What I did not do is call it harmless. The plan identity consumes the stable class, so the wording does not move the member-set fingerprint today — measured, not assumed — but it sits one consumer away: whoever routes on cause, or renders it into anything content-addressed, reopens the CAS defect this family already fixed once.

— sent from silent-bear-842