HOST-0: program-scoped host assimilation (unblocks srv5/srv6 enrollment)

dag/gunbc/host_assimilation_program.dag

@@ -138,9 +138,29 @@ fn assimilation_program_for(intent: HostEnrollmentIntent) -> HostAssimilationPro
 
 data host_enrollment_participation_nonempty_note: String = "Enrollment participation is authored as a non-empty list at every fleet enrollment site today. An empty list would yield an empty program identity (invalid NonEmptyStr) and zero completion obligations; a NonEmptyList carrier on HostEnrollmentIntent is deferred until enrollment validation walls land."
 
+data fleet_participation_canonical_roster_note: String = "Participation has SET semantics but is carried as a List, and identity must not be able to tell the two apart. Step selection already reads the list as membership -- step_serves_any asks only whether SOME participation claims the step -- so order and repetition are invisible to which obligations exist. Deriving the identity from the raw list did let them through: [CiRunner, InferenceServing] and [InferenceServing, CiRunner] and [CiRunner, CiRunner, InferenceServing] select exactly the same steps while producing three different identity strings, which is a second representation of one program (DESIGN section 3) and would fork any consumer that keys on identity. The correction projects through a FIXED roster instead of reading the caller's list order: filtering the roster by membership yields at most one occurrence of each participation, in one order, whatever the caller wrote. That is the construction half -- a duplicate or a reordering cannot reach the identity, so there is no post-hoc canonicalization check to remember to call. The roster's own completeness is the residue this cannot construct away, and it is walled by an EXHAUSTIVE match in fleet_participation_in_canonical_roster: a newly added participation does not compile until it is stated there, and its witness reds if it is stated but left out of the roster."
+
+data fleet_participation_canonical_roster: List<FleetParticipation> = [
+  CiRunnerParticipation,
+  InferenceServingParticipation,
+]
+
+fn fleet_participation_in_canonical_roster(p: FleetParticipation) -> Bool {
+  match p {
+    CiRunnerParticipation =>
+      participation_list_contains(ps: fleet_participation_canonical_roster, wanted: CiRunnerParticipation)
+    InferenceServingParticipation =>
+      participation_list_contains(ps: fleet_participation_canonical_roster, wanted: InferenceServingParticipation)
+  }
+}
+
+fn canonical_participation(ps: List<FleetParticipation>) -> List<FleetParticipation> {
+  filter(fleet_participation_canonical_roster, c => participation_list_contains(ps: ps, wanted: c))
+}
+
 fn host_enrollment_program_identity(intent: HostEnrollmentIntent) -> NonEmptyStr {
   join(
-    map(intent.participation, p => fleet_participation_label(p: p)),
+    map(canonical_participation(ps: intent.participation), p => fleet_participation_label(p: p)),
     "+"
   ) as NonEmptyStr
 }

dag/test/claim/host_phase_status_witness_test.dag

@@ -198,6 +198,67 @@ test fn witness_inference_program_is_strictly_smaller_than_the_spine() -> Bool {
   inference > 0 && inference < host_standup_spine.length()
 }
 
+data synthetic_reordered_enrollment: HostEnrollmentIntent = HostEnrollmentIntent {
+  host: operator_host_srv3,
+  participation: [InferenceServingParticipation, CiRunnerParticipation],
+}
+
+data synthetic_forward_order_enrollment: HostEnrollmentIntent = HostEnrollmentIntent {
+  host: operator_host_srv3,
+  participation: [CiRunnerParticipation, InferenceServingParticipation],
+}
+
+data synthetic_duplicated_enrollment: HostEnrollmentIntent = HostEnrollmentIntent {
+  host: operator_host_srv3,
+  participation: [CiRunnerParticipation, CiRunnerParticipation, InferenceServingParticipation],
+}
+
+data witness_participation_set_semantics_note: String = "Participation is a set wearing a list's carrier, so the three enrollments below must be one program under BOTH readings -- the steps they select and the identity they derive. Selection was already order-blind and duplicate-blind because step_serves_any asks only whether SOME participation claims a step; identity was not, and joined whatever the caller happened to write. These conjuncts are the discriminating controls for that repair: each one reds against the pre-repair identity derivation, which is what distinguishes a real construction wall from a canonicalization function nobody calls."
+
+test fn witness_participation_order_does_not_change_program_identity() -> Bool {
+  let forward = assimilation_program_for(intent: synthetic_forward_order_enrollment)
+  let reversed = assimilation_program_for(intent: synthetic_reordered_enrollment)
+  forward.identity == reversed.identity
+    && program_step_count(program: forward) == program_step_count(program: reversed)
+}
+
+test fn witness_duplicate_participation_is_identity_neutral() -> Bool {
+  let once = assimilation_program_for(intent: synthetic_forward_order_enrollment)
+  let twice = assimilation_program_for(intent: synthetic_duplicated_enrollment)
+  once.identity == twice.identity
+    && program_step_count(program: once) == program_step_count(program: twice)
+}
+
+test fn witness_distinct_participation_changes_identity_and_obligations() -> Bool {
+  let ci = assimilation_program_for(intent: synthetic_ci_enrollment)
+  let inference = assimilation_program_for(intent: synthetic_inference_enrollment)
+  let both = assimilation_program_for(intent: synthetic_forward_order_enrollment)
+  ci.identity != inference.identity
+    && both.identity != ci.identity
+    && program_step_count(program: inference) < program_step_count(program: ci)
+}
+
+data witness_identity_is_exactly_canonical_note: String = "The DISCRIMINATING control, and the reason the three conjuncts above are not satisfied by any function that merely returns a constant. It pins the derived identity to an independently authored literal rather than to another projection of the same computation, and the literal is what the canonical roster REQUIRES it to be, not what the current code was measured to emit. Pre-repair, the duplicated enrollment joined its raw list and derived 'ci-runner+ci-runner+inference-serving'; this conjunct asserts that exact string is NOT the identity while the canonical two-label form IS. So it reds against the derivation this change replaced, which is what makes the repair a wall rather than a canonicalization helper sitting beside a still-writable path."
+
+test fn witness_program_identity_is_exactly_the_canonical_projection() -> Bool {
+  let duplicated = assimilation_program_for(intent: synthetic_duplicated_enrollment)
+  let reordered = assimilation_program_for(intent: synthetic_reordered_enrollment)
+  (duplicated.identity as String) == "ci-runner+inference-serving"
+    && (reordered.identity as String) == "ci-runner+inference-serving"
+    && (duplicated.identity as String) != "ci-runner+ci-runner+inference-serving"
+    && (reordered.identity as String) != "inference-serving+ci-runner"
+}
+
+test fn witness_single_participation_identities_are_distinct_labels() -> Bool {
+  (assimilation_program_for(intent: synthetic_ci_enrollment).identity as String) == "ci-runner"
+    && (assimilation_program_for(intent: synthetic_inference_enrollment).identity as String) == "inference-serving"
+}
+
+test fn witness_every_participation_is_in_the_canonical_roster() -> Bool {
+  fleet_participation_in_canonical_roster(p: CiRunnerParticipation)
+    && fleet_participation_in_canonical_roster(p: InferenceServingParticipation)
+}
+
 test fn witness_inference_enrollment_carries_no_runner_or_bmc_obligation() -> Bool {
   let cells = host_phase_cells_for_enrollment(intent: synthetic_inference_enrollment)
   let forbidden = filter(cells, c => cell_label_is_runner_only(c: c))