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

dag/test/claim/fabric_cell_evidence_algebra_witness_test.dag

@@ -0,0 +1,224 @@
+module test.claim.fabric_cell_evidence_algebra_witness
+
+import std.types { Bool, String, Int, NonEmptyStr, list_length }
+import gunbc.build_cache_instance { RunnerSlotIdentity }
+import gunbc.fleet_intent_network { operator_host_srv3 }
+import gunbc.fabric_cell_converge {
+  FabricCellMember,
+  FabricCellAddressObservation,
+  AddressObserved,
+  AddressAbsent,
+  AddressObservationRefused,
+  FabricCellAddressEvidence,
+  NoEvidence,
+  EvidenceRefused,
+  EvidenceAbsent,
+  EvidenceObserved,
+  EvidenceConflict,
+  fabric_cell_address_evidence,
+  FabricCellResourceBoundaryAddress,
+}
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+// THE JOIN IS TESTED AS AN ALGEBRA, NOT AS A LIST OF SCENARIOS, AND THE DIFFERENCE IS WHAT THIS
+// FAMILY KEEPS PAYING FOR. A scenario row asserts that one input produces one output; it can only
+// catch a defect someone already imagined. A law quantifies over EVERY ordering of an atom set, so
+// it catches the orderings nobody thought to write -- and every defect this family has had was an
+// ordering or a population nobody thought to write.
+//
+// The atoms below are the complete inhabitance of what one address can report: nothing, an explicit
+// absence, a positive reading, a DIFFERENT positive reading, and two refusals that differ only in
+// their cause text. The last pair is deliberate: it is the only pair whose two members are
+// semantically identical and textually distinct, which is exactly where an order-dependent value
+// hides from a class-level assertion.
+
+fn algebra_slot() -> RunnerSlotIdentity {
+  RunnerSlotIdentity { host: operator_host_srv3, slot_index: 6 }
+}
+
+fn algebra_member(digest: String) -> FabricCellMember {
+  FabricCellMember {
+    slot: algebra_slot(),
+    address: FabricCellResourceBoundaryAddress,
+    state_digest: digest as NonEmptyStr,
+  }
+}
+
+fn atom_absent() -> FabricCellAddressObservation {
+  AddressAbsent { slot: algebra_slot(), address: FabricCellResourceBoundaryAddress }
+}
+
+fn atom_observed(digest: String) -> FabricCellAddressObservation {
+  AddressObserved { member: algebra_member(digest: digest) }
+}
+
+fn atom_refused(cause: String) -> FabricCellAddressObservation {
+  AddressObservationRefused {
+    slot: algebra_slot(),
+    address: FabricCellResourceBoundaryAddress,
+    cause: cause,
+  }
+}
+
+fn algebra_atoms() -> List<FabricCellAddressObservation> {
+  [
+    atom_absent(),
+    atom_observed(digest: "digest-a"),
+    atom_observed(digest: "digest-b"),
+    atom_refused(cause: "transport reset"),
+    atom_refused(cause: "permission denied"),
+  ]
+}
+
+// TWO PROJECTIONS, AND THE GAP BETWEEN THEM IS THE MEASUREMENT. The class projection is what the
+// plan identity and the routing consume; the full projection is the complete semantic value. A
+// safety fold is not order-independent merely because every permutation reaches the same coproduct
+// arm -- the value inside the arm must satisfy the law too, or a later consumer that reads it
+// reintroduces the order dependence the class-level assertion said was gone.
+fn evidence_class_wire(e: FabricCellAddressEvidence) -> String {
+  match e {
+    NoEvidence => "none"
+    EvidenceRefused { cause: _ } => "refused"
+    EvidenceAbsent => "absent"
+    EvidenceObserved { member: _ } => "observed"
+    EvidenceConflict => "conflict"
+  }
+}
+
+fn evidence_full_wire(e: FabricCellAddressEvidence) -> String {
+  match e {
+    NoEvidence => "none"
+    EvidenceRefused { cause: c } => concat("refused:", c)
+    EvidenceAbsent => "absent"
+    EvidenceObserved { member: m } => concat("observed:", m.state_digest as String)
+    EvidenceConflict => "conflict"
+  }
+}
+
+fn class_of(observations: List<FabricCellAddressObservation>) -> String {
+  evidence_class_wire(e: fabric_cell_address_evidence(observations: observations))
+}
+
+fn full_of(observations: List<FabricCellAddressObservation>) -> String {
+  evidence_full_wire(e: fabric_cell_address_evidence(observations: observations))
+}
+
+// EVERY ORDERING IS QUANTIFIED OVER, NOT LISTED. The laws below fold over the atom set itself, so
+// every ordered pair and every ordered triple is visited -- including the ones with repeats, which
+// is where idempotence lives. Adding an atom widens every law here with no other edit, which is the
+// property a hand-listed scenario table can never have.
+// THE PARAMETER IS NOT NAMED `project`, AND THE RENAME IS A DEFECT RECEIPT RATHER THAN A STYLE
+// CHOICE. It was, and these rows passed under `gunbc run --entry <this file>` and FAILED under the
+// required floor with `call contract mismatch calling 'project': missing required argument
+// 'assignments'`. Three other test.claim modules declare a module-scope `fn project` of two
+// arguments; the floor folds every witness through ONE prepared subject over the whole corpus, so
+// that symbol is in scope there and shadows this function's own parameter, while an entry-scoped
+// run never sees it.
+//
+// THE ARITY IS WHY THIS ONE WAS LOUD. Where the shadowing symbol takes a different number of
+// arguments the call refuses; where it takes the same number it returns the wrong value silently
+// (gunbc#9187, a parameter named `p` against `gunbc.plans.md_helpers` `p`). Same defect, and only
+// the arity decides whether you find out.
+fn all_pairs_agree(observation_wire: fn(List<FabricCellAddressObservation>) -> String) -> Bool {
+  fold(algebra_atoms(), init: true, f: (acc_a, a) =>
+    acc_a && fold(algebra_atoms(), init: true, f: (acc_b, b) =>
+      acc_b && observation_wire([a, b]) == observation_wire([b, a])))
+}
+
+fn all_triples_agree(observation_wire: fn(List<FabricCellAddressObservation>) -> String) -> Bool {
+  fold(algebra_atoms(), init: true, f: (acc_a, a) =>
+    acc_a && fold(algebra_atoms(), init: true, f: (acc_b, b) =>
+      acc_b && fold(algebra_atoms(), init: true, f: (acc_c, c) => {
+        let reference = observation_wire([a, b, c])
+        acc_c
+          && observation_wire([a, c, b]) == reference
+          && observation_wire([b, a, c]) == reference
+          && observation_wire([b, c, a]) == reference
+          && observation_wire([c, a, b]) == reference
+          && observation_wire([c, b, a]) == reference
+      })))
+}
+
+// IDENTITY: an empty observation list is NoEvidence, and NoEvidence is what "nobody looked" means.
+// It is not absence, and the whole population type exists downstream of that distinction.
+test fn evidence_empty_is_no_evidence() -> Bool {
+  full_of(observations: []) == "none"
+}
+
+// IDEMPOTENCE: one atom observed twice says exactly what it said once. A join that failed this
+// would make a duplicated readback -- the ordinary case when two probes cover one address --
+// change the answer.
+test fn evidence_join_is_idempotent() -> Bool {
+  fold(algebra_atoms(), init: true, f: (acc, x) =>
+    acc && full_of(observations: [x, x]) == full_of(observations: [x]))
+}
+
+// PERMUTATION INVARIANCE OF THE PRODUCTION LEFT FOLD, AT THE CLASS THE PLAN IDENTITY CONSUMES.
+// This is what matters for the member-set fingerprint and for routing: whichever order the
+// observations arrive in, the plan must not change.
+//
+// THE NAME IS NARROWER THAN COMMUTATIVITY-AND-ASSOCIATIVITY AND THE NARROWING IS THE POINT. An
+// earlier revision of this comment claimed both. It was false of associativity: these rows permute
+// a THREE-ELEMENT LIST through one left fold, and never compare `join(join(a, b), c)` against
+// `join(a, join(b, c))` -- different parenthesizations, not different orders. No binary
+// evidence-to-evidence join is exposed to compare, so that law is not testable from here at all,
+// and a comment claiming it would be the same overclaim this file exists to refuse: evidence named
+// for a stronger property than it establishes.
+//
+// WHY THE MISSING LAW IS WORTH ITS OWN CHANGE RATHER THAN A SHRUG: associativity is exactly what
+// licenses combining probe batches INCREMENTALLY. An observer that reads a host in chunks and folds
+// each chunk into a running evidence value is relying on it, and permutation invariance over one
+// monolithic list does not establish it. The next-step trigger is a pure binary join the list fold
+// consumes; until that exists this file states the weaker property it can actually measure.
+test fn evidence_class_is_order_independent_over_pairs() -> Bool {
+  all_pairs_agree(observation_wire: class_of)
+}
+
+test fn evidence_class_is_order_independent_over_triples() -> Bool {
+  all_triples_agree(observation_wire: class_of)
+}
+
+// THE DOMAIN LAWS, EACH NAMING THE STATE IT SEPARATES FROM ITS NEIGHBOUR. Order-independence alone
+// is satisfied by a join that returns one constant, so a law set without these is vacuous.
+test fn evidence_domain_laws_hold() -> Bool {
+  let a = atom_observed(digest: "digest-a")
+  let b = atom_observed(digest: "digest-b")
+  let absent = atom_absent()
+  let refused = atom_refused(cause: "transport reset")
+  full_of(observations: [a, a]) == "observed:digest-a"
+    && class_of(observations: [a, b]) == "conflict"
+    && class_of(observations: [a, absent]) == "conflict"
+    && full_of(observations: [absent, absent]) == "absent"
+    && class_of(observations: [refused, a]) == "refused"
+    && class_of(observations: [refused, absent]) == "refused"
+    && class_of(observations: [refused, a, b, absent]) == "refused"
+}
+
+// AND THE ONE THAT IS RED TODAY, ASSERTING THE PROPERTY WE WANT RATHER THAN THE ONE WE HAVE. The
+// class projection above is order-independent; the FULL semantic value is not, because the fold
+// keeps the FIRST refusal cause it saw. Two refusals that differ only in cause text are
+// semantically identical and textually distinct, so `[c1, c2]` and `[c2, c1]` reach the same arm
+// carrying different payloads.
+//
+// THIS ROW ASSERTS EQUALITY AND IS ENROLLED AS EXPECTED-RED, and the direction is the whole point
+// (codex review 55693). An earlier cut asserted the INEQUALITY -- that reversed refusals must stay
+// unequal -- and it passed, which made the defect part of the green contract: whoever canonicalized
+// the join would have been met by a red row whose obvious repair is to DELETE the row protecting
+// the property. That is a witness pinning a defect and thereby acquiring a defender, which is the
+// exact class this lane named one PR earlier and then re-committed here. Asserted this way round
+// the row 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.
+//
+// WHY IT IS NOT FIXED IN THIS PR, stated rather than left as an omission: canonicalizing the
+// refusal changes `EvidenceRefused`'s payload and therefore `AddressUnreadable.cause` and every
+// consumer of it, in a file #9167 is already restructuring. It is a production change belonging in
+// its own diff with its own mutation receipt, not a rider on a witness-only PR. What is NOT true
+// is that it is harmless: the plan identity consumes the CLASS, so the wording does not move the
+// member-set fingerprint today, 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.
+test fn evidence_full_value_is_order_independent() -> Bool {
+  full_of(observations: [atom_refused(cause: "transport reset"), atom_refused(cause: "permission denied")])
+    == full_of(observations: [atom_refused(cause: "permission denied"), atom_refused(cause: "transport reset")])
+}

src/v2/workflow/floor_expected_red.dag

@@ -494,7 +494,7 @@ fn floor_expected_red_chunk_20() -> List<String> {
 // The partition of the 164 and the measurements behind this family are
 // docs/plans/receipts/floor-runtime-error-partition-2026-08-23/.
 fn floor_expected_red_chunk_21() -> List<String> {
-  Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_extra_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_missing_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_wrong_argument_type_must_refuse_at_compile", tail: Empty {} } } }
+  Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_extra_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_missing_argument_must_refuse_at_compile", tail: Cons { head: "test.claim.compile_accepted_unevaluable_program_control.primitive_call_with_wrong_argument_type_must_refuse_at_compile", tail: Cons { head: "test.claim.fabric_cell_evidence_algebra_witness.evidence_full_value_is_order_independent", tail: Empty {} } } } }
 }
 
 fn floor_expected_red_chunks() -> List<List<String>> {