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

dag/gunbc/toolchain_coherence.dag

@@ -0,0 +1,128 @@
+module gunbc.toolchain_coherence
+
+import std.types { String, NonEmptyStr, FilePath, List, Bool }
+import std.content_hash {
+  ContentHash,
+  ContentHashComparison,
+  ContentHashEqual,
+  ContentHashDifferent,
+  ContentHashCrossFamilyIncomparable,
+  compare_content_hash,
+}
+import extdeps.realization.emit_on_demand_host { ObservedToolIdentity }
+import gunbc.build_cache_instance { RunnerSlotIdentity }
+import v2.std.optional { Present, Absent }
+import std.disposition { Disposition, Terminal }
+
+// THE RELATION IS TERMINAL; ITS PRODUCTION STANDING IS A STALL. Those are two facts and this row
+// keeps them apart, because naming the carrier as though coherence had been achieved is the rung
+// inflation DESIGN 4b(1) calls worse than sitting low. NEXT-RUNG TRIGGER, named as a seam rather
+// than as "observe later": 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 to a
+// capacity-only reader -- a bespoke producer would give this fact a second home.
+data gunbc_toolchain_coherence_disposition: Disposition = Terminal {
+  reason: "Relation-only carrier: classifies spawn observations as Single, Differed, or one of three NotEvaluated causes. NO PRODUCER EXISTS. Nothing in this repository observes a spawn, so no production claim of toolchain coherence is available from it and it must not be cited as coverage that successive spawns reached the same bytes -- they are unmeasured. SpawnObservationProducerAbsent is the honest standing today; ToolchainNeverObserved is reserved for an observation transaction that RAN and found no comparable spawn pair, and the fold cannot return the former because a fold speaks only about the list it was handed. Witnesses establish the classifier's distinctions and nothing about any host."
+}
+
+// THE SUBJECT IS ONE SPAWN, NOT ONE JOB, and that grain is the whole point of the carrier. 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 denominator error where
+// a fact about a population is asserted from a sample of one. The digest is taken AT SPAWN and
+// travels with the observation, rather than being resolved once and looked up later: resolving a
+// pathname and re-launching it afterwards is the defect this carrier exists to detect, so a shape
+// that permits it would be the defect wearing a receipt.
+type ToolchainSpawn {
+  pass: NonEmptyStr
+  spawn: NonEmptyStr
+  slot: RunnerSlotIdentity
+  resolved_executable: FilePath
+  observed: ObservedToolIdentity
+}
+
+// NOT-EVALUATED IS REACHED BY CONSTRUCTION, NEVER BY REMEMBERING TO SET IT. The empty observation
+// list folds to ToolchainNeverObserved because that is what the fold's base case IS, so absence of
+// evidence cannot render as agreement. That direction is the fail-closed one: a masked run and a
+// clean run must not produce the same value, and today's standing -- nothing establishes that
+// successive spawns reached the same bytes -- is honestly NotEvaluated rather than passed.
+//
+// THE CAUSES ARE NOT COLLAPSED, and the split is not cosmetic: "we could not tell" and "we checked
+// and they differed" have opposite remedies. Incomparable is its own cause rather than a silent
+// false because std.content_hash refuses to collapse a cross-family pair -- comparing an fnv1a64
+// fingerprint against a sha256 digest establishes nothing about the bytes, and reporting that as
+// "differed" would manufacture a finding while reporting it as "equal" would manufacture a pass.
+// PRODUCER-ABSENT IS NOT NEVER-OBSERVED, and collapsing them is the execution-provenance loss
+// DESIGN names: a masked run and a clean run must not render identically. ToolchainNeverObserved
+// is what an observation transaction returns when it RAN and its subject held no comparable spawn
+// pair. SpawnObservationProducerAbsent is what holds when nothing observes spawns at all -- which
+// is the standing today. The fold below can never return it, and that is correct rather than a
+// dead arm: the fold speaks only about the list it was handed, while producer absence is a claim
+// about the world that only a declaration or a real observation transaction may make. Without this
+// split, the first producer to be wired would render its own absence as "we checked and found no
+// pair", which is the absent-as-clean failure this carrier exists to refuse.
+type ToolchainCoherenceUnevaluated
+  = ToolchainNeverObserved
+  | SpawnObservationProducerAbsent { cause: NonEmptyStr }
+  | ToolchainIdentityIncomparable { tool_name: NonEmptyStr }
+
+// DIFFERED IS A FINDING AND SITS BESIDE NotEvaluated RATHER THAN INSIDE IT. It is the one arm that
+// says the shared mutable path actually bit: two spawns of one tool in one pass reached different
+// bytes. Folding it into NotEvaluated would lose exactly the signal the carrier was built to carry.
+type ToolchainCoherence
+  = ToolchainCoherenceNotEvaluated { cause: ToolchainCoherenceUnevaluated }
+  | ToolchainIdentitiesDiffered {
+      tool_name: NonEmptyStr
+      baseline: ToolchainSpawn
+      divergent: ToolchainSpawn
+    }
+  | ToolchainIdentitySingle { tool_name: NonEmptyStr }
+
+// THE SCAN IS EXPLICIT RECURSION rather than a fold, and the reason is short-circuit: the first
+// divergence decides the verdict, so a fold would keep comparing hashes after the answer is fixed.
+// An earlier revision of this note claimed the corpus had no lambda-taking fold. That was false --
+// std.graph and std.markdown both use one -- and it is corrected rather than softened, because a
+// note asserting a corpus-wide absence is a claim about a population nobody measured.
+fn toolchain_coherence_scan(
+  spawns: List<ToolchainSpawn>,
+  baseline: ToolchainSpawn,
+  tool: NonEmptyStr
+) -> ToolchainCoherence {
+  match spawns.first() {
+    Absent => ToolchainIdentitySingle { tool_name: tool }
+    Present { value: s } =>
+      match compare_content_hash(
+        left: baseline.observed.observed_identity,
+        right: s.observed.observed_identity
+      ) {
+        ContentHashDifferent =>
+          ToolchainIdentitiesDiffered {
+            tool_name: tool,
+            baseline: baseline,
+            divergent: s
+          }
+        ContentHashCrossFamilyIncomparable =>
+          ToolchainCoherenceNotEvaluated {
+            cause: ToolchainIdentityIncomparable { tool_name: tool }
+          }
+        ContentHashEqual =>
+          toolchain_coherence_scan(
+            spawns: spawns.skip(n: 1),
+            baseline: baseline,
+            tool: tool
+          )
+      }
+  }
+}
+
+fn toolchain_coherence_of(spawns: List<ToolchainSpawn>) -> ToolchainCoherence {
+  match spawns.first() {
+    Absent => ToolchainCoherenceNotEvaluated { cause: ToolchainNeverObserved }
+    Present { value: head } =>
+      toolchain_coherence_scan(
+        spawns: spawns.skip(n: 1),
+        baseline: head,
+        tool: head.observed.tool_name
+      )
+  }
+}

dag/test/claim/toolchain_coherence_witness_test.dag

@@ -0,0 +1,154 @@
+module test.claim.toolchain_coherence_witness_test
+
+import std.types { String, NonEmptyStr, List, Bool }
+import std.nat { Nat }
+import std.content_hash { as_content_hash_structural, content_hash_atom }
+import extdeps.realization.emit_on_demand_host { ObservedToolIdentity }
+import gunbc.build_cache_instance { RunnerSlotIdentity }
+import gunbc.fleet_intent_network { operator_host_srv1 }
+import gunbc.toolchain_coherence {
+  ToolchainSpawn,
+  ToolchainCoherence,
+  ToolchainCoherenceNotEvaluated,
+  ToolchainIdentitiesDiffered,
+  ToolchainIdentitySingle,
+  ToolchainNeverObserved,
+  SpawnObservationProducerAbsent,
+  ToolchainIdentityIncomparable,
+  toolchain_coherence_of,
+}
+
+fn spawn_of(pass: String, bytes: String) -> ToolchainSpawn {
+  spawn_at(pass: pass, bytes: bytes, exe: "/usr/local/rustup/toolchains/stable/bin/rustfmt")
+}
+
+fn spawn_at(pass: String, bytes: String, exe: String) -> ToolchainSpawn {
+  ToolchainSpawn {
+    pass: pass,
+    spawn: pass,
+    resolved_executable: exe,
+    slot: RunnerSlotIdentity { host: operator_host_srv1, slot_index: 9 },
+    observed: ObservedToolIdentity {
+      tool_name: "rustfmt",
+      observed_identity: as_content_hash_structural(
+        structural: content_hash_atom(value: bytes)
+      )
+    }
+  }
+}
+
+// THE EMPTY CASE IS THE ONE THAT MATTERS MOST and it is asserted first deliberately. An observation
+// list nobody populated must fold to NotEvaluated by construction, never to agreement -- if this arm
+// ever returns Single, absence of evidence has started rendering as a pass and the carrier is worse
+// than absent, because it would then be cited as coverage.
+test fn no_observation_is_not_evaluated() -> Bool {
+  match toolchain_coherence_of(spawns: []) {
+    ToolchainCoherenceNotEvaluated { cause: c } =>
+      match c {
+        ToolchainNeverObserved => true
+        SpawnObservationProducerAbsent { cause: _ } => false
+        ToolchainIdentityIncomparable { tool_name: _ } => false
+      }
+    ToolchainIdentitiesDiffered { tool_name: _, baseline: _, divergent: _ } => false
+    ToolchainIdentitySingle { tool_name: _ } => false
+  }
+}
+
+test fn same_bytes_across_passes_is_single() -> Bool {
+  match toolchain_coherence_of(spawns: [
+    spawn_of(pass: "fmt-pass-1", bytes: "rustup-bytes-A"),
+    spawn_of(pass: "fmt-pass-2", bytes: "rustup-bytes-A"),
+    spawn_of(pass: "fmt-pass-3", bytes: "rustup-bytes-A")
+  ]) {
+    ToolchainIdentitySingle { tool_name: _ } => true
+    ToolchainIdentitiesDiffered { tool_name: _, baseline: _, divergent: _ } => false
+    ToolchainCoherenceNotEvaluated { cause: _ } => false
+  }
+}
+
+// THE DISCRIMINATING RED. One pass in the middle reaches different bytes -- exactly what a shared
+// rustup binary replaced mid-job produces -- and it must be a FINDING rather than a NotEvaluated,
+// because "we checked and they differed" and "we could not tell" have opposite remedies.
+test fn differing_bytes_mid_run_is_a_finding() -> Bool {
+  match toolchain_coherence_of(spawns: [
+    spawn_of(pass: "fmt-pass-1", bytes: "rustup-bytes-A"),
+    spawn_of(pass: "fmt-pass-2", bytes: "rustup-bytes-B"),
+    spawn_of(pass: "fmt-pass-3", bytes: "rustup-bytes-A")
+  ]) {
+    ToolchainIdentitiesDiffered { tool_name: t, baseline: _, divergent: _ } => t == "rustfmt"
+    ToolchainIdentitySingle { tool_name: _ } => false
+    ToolchainCoherenceNotEvaluated { cause: _ } => false
+  }
+}
+
+// A SINGLE SPAWN IS NOT COHERENCE EVIDENCE OF A POPULATION, but it is honestly Single: one spawn
+// cannot disagree with itself. Recorded so the per-PASS grain is visible -- the carrier reports what
+// it observed, and a job that spawned once has established coherence over exactly one spawn.
+test fn one_spawn_is_single() -> Bool {
+  match toolchain_coherence_of(spawns: [spawn_of(pass: "only", bytes: "rustup-bytes-A")]) {
+    ToolchainIdentitySingle { tool_name: _ } => true
+    ToolchainIdentitiesDiffered { tool_name: _, baseline: _, divergent: _ } => false
+    ToolchainCoherenceNotEvaluated { cause: _ } => false
+  }
+}
+
+// PRODUCER-ABSENT AND NEVER-OBSERVED MUST NOT BE THE SAME VALUE. This is the distinction the
+// carrier is most likely to lose later: the first wired producer that cannot observe its subject
+// will be tempted to report the empty fold, and that renders its own absence as "we checked and
+// found no pair". Asserting they are distinct constructions keeps the eventual producer honest.
+// The fold cannot RETURN ProducerAbsent -- it speaks only about the list it was handed -- so this
+// arm is authored directly, which is exactly how a real observation transaction would raise it.
+test fn producer_absent_is_not_never_observed() -> Bool {
+  let absent = ToolchainCoherenceNotEvaluated {
+    cause: SpawnObservationProducerAbsent { cause: "nothing observes spawns" }
+  }
+  let empty = toolchain_coherence_of(spawns: [])
+  match absent {
+    ToolchainCoherenceNotEvaluated { cause: a } =>
+      match a {
+        SpawnObservationProducerAbsent { cause: _ } =>
+          match empty {
+            ToolchainCoherenceNotEvaluated { cause: e } =>
+              match e {
+                ToolchainNeverObserved => true
+                SpawnObservationProducerAbsent { cause: _ } => false
+                ToolchainIdentityIncomparable { tool_name: _ } => false
+              }
+            ToolchainIdentitiesDiffered { tool_name: _, baseline: _, divergent: _ } => false
+            ToolchainIdentitySingle { tool_name: _ } => false
+          }
+        ToolchainNeverObserved => false
+        ToolchainIdentityIncomparable { tool_name: _ } => false
+      }
+    ToolchainIdentitiesDiffered { tool_name: _, baseline: _, divergent: _ } => false
+    ToolchainIdentitySingle { tool_name: _ } => false
+  }
+}
+
+// THE FINDING MUST CARRY ENOUGH GRAIN TO PICK THE REMEDY. Two spawns diverging at ONE resolved
+// path means the binary was replaced under us; two spawns diverging at DIFFERENT paths means we
+// ran two different binaries. Those have opposite repairs, so a finding that reported only
+// "differed" would hand the consumer a verdict it cannot act on. Both directions are asserted so
+// the evidence does the work rather than the arm's name.
+test fn divergence_carries_the_paths_that_pick_the_remedy() -> Bool {
+  let one_path = toolchain_coherence_of(spawns: [
+    spawn_at(pass: "p1", bytes: "A", exe: "/usr/local/bin/rustfmt"),
+    spawn_at(pass: "p2", bytes: "B", exe: "/usr/local/bin/rustfmt")
+  ])
+  let two_paths = toolchain_coherence_of(spawns: [
+    spawn_at(pass: "p1", bytes: "A", exe: "/usr/local/bin/rustfmt"),
+    spawn_at(pass: "p2", bytes: "B", exe: "/home/node/.cargo/bin/rustfmt")
+  ])
+  match one_path {
+    ToolchainIdentitiesDiffered { tool_name: _, baseline: b, divergent: d } =>
+      (b.resolved_executable as String) == (d.resolved_executable as String)
+        && match two_paths {
+             ToolchainIdentitiesDiffered { tool_name: _, baseline: b2, divergent: d2 } =>
+               (b2.resolved_executable as String) != (d2.resolved_executable as String)
+             ToolchainIdentitySingle { tool_name: _ } => false
+             ToolchainCoherenceNotEvaluated { cause: _ } => false
+           }
+    ToolchainIdentitySingle { tool_name: _ } => false
+    ToolchainCoherenceNotEvaluated { cause: _ } => false
+  }
+}