Model the spawn-coherence relation: producer-absence and never-observed are different states

[briansrls]

Summary

Adds gunbc.toolchain_coherence: the relation by which spawn observations are classified as coherent, divergent, or unevaluated. Model-only, by operator ruling.

The question it answers is not digest A == digest B. It is: two spawns claiming to inhabit one tool role, inside one pass, reached the same executable bytes. The subject is ONE SPAWN, not one job — a job that spawns rustfmt eleven times has eleven opportunities to exec different bytes, so a job-grained receipt would report a coherence it never established. The digest is taken at spawn and travels with the observation, because resolving a pathname and re-launching it afterwards is precisely the defect the carrier exists to detect.

What this PR does NOT claim

Stated first, because the ruling turns on it:

• No production spawn has been observed. Nothing in this repository observes a spawn.
• No host is established to have used the same executable twice.
• Toolchain coherence is not guaranteed by anything here, and this carrier must not be cited as coverage that successive spawns reached the same bytes. They are unmeasured.

The relation is terminal; its production standing is a stall. gunbc_toolchain_coherence_disposition records both, so the declaration is not named as though coherence had been achieved (DESIGN §4b(1) rung inflation).

Three states the design turns on

SpawnObservationProducerAbsent ≠ ToolchainNeverObserved. Before this split the fold returned NeverObserved for an empty list, so the first producer wired to the carrier would have rendered its own absence as "we checked and found no comparable pair" — the execution-provenance loss DESIGN names, where a masked run and a clean run render identically. NeverObserved is now reserved for an observation transaction that RAN and found no comparable pair. The fold cannot return ProducerAbsent, which is correct rather than a dead arm: a fold speaks only about the list it was handed; producer absence is a claim about the world.

ToolchainIdentityIncomparable is its own cause. std.content_hash refuses to collapse a cross-family pair. Reporting that as "differed" would manufacture a finding; reporting it as "equal" would manufacture a pass.

Differed is a finding beside NotEvaluated, never inside it. "We could not tell" and "we checked and they differed" have opposite remedies. No outcome projects to Bool.

Grain: the finding must pick the remedy

ToolchainSpawn carries pass, spawn identity, slot, resolved executable, and the observed digest. Without the resolved path, two spawns diverging at ONE path (the binary was replaced under us) and at DIFFERENT paths (we ran two different binaries) collapse into one verdict — opposite repairs. The Differed arm carries both spawns so the consumer can tell them apart. std.types.FilePath is reused rather than minting a path type.

Not a nickname for ObservedToolIdentityDuplicate

That arm folds one ResolvedBuildContext roster and carries only a count, discarding the identities — it cannot answer whether the duplicates agreed. It is a name-multiplicity fact over one snapshot; this is a byte-agreement fact over a spawn sequence.

Next-rung trigger

A spawn operation emits tool identity, resolved executable, executable digest, pass identity and spawn identity at the moment of spawn; two such observations sharing one tool role within one pass are handed to toolchain_coherence_of. That producer belongs to the shared spawn/execution substrate the aggregate-demand instrument will also read — not a capacity-only producer, which would give this fact a second home.

Test plan

claim_batch --source-root dag --source-root src/v2 --hermetic --entry dag/test/claim/toolchain_coherence_witness_test.dag — 6/6 PASS:

witness	establishes
no_observation_is_not_evaluated	empty folds to NotEvaluated, never agreement
same_bytes_across_passes_is_single	three agreeing spawns are Single
differing_bytes_mid_run_is_a_finding	discriminating RED — divergence is a finding, not NotEvaluated
one_spawn_is_single	one spawn cannot disagree with itself
producer_absent_is_not_never_observed	the two absence states are distinct constructions
divergence_carries_the_paths_that_pick_the_remedy	asserted in BOTH directions — same-path and different-path divergence are distinguishable

Focused green is preflight; required CI is the completion receipt. The witnesses establish the classifier's distinctions and nothing about any host.