diff --git a/dag/gunbc/fleet_reach_endpoint.dag b/dag/gunbc/fleet_reach_endpoint.dag index e09e8366da4..5992315adad 100644 --- a/dag/gunbc/fleet_reach_endpoint.dag +++ b/dag/gunbc/fleet_reach_endpoint.dag @@ -6,6 +6,7 @@ import gunbc.spark.dgx_procurement { DgxSparkRouterBinding, SlotAssigned, SlotUnassigned, + router_binding_identity, dgx_spark_router_bindings, } import extdeps.network.ipv4 { render_ipv4_address } @@ -31,16 +32,28 @@ fn spark_endpoint_for_binding(binding: DgxSparkRouterBinding) -> String? { // Fleet-wide: a host with a modeled endpoint probes AT that endpoint; every other host // probes by name (srv1-srv4 resolve via the LAN today). The receipt stays keyed by the // fleet IDENTITY either way — the endpoint is transport addressing, not identity. +// +// THIS FOLD USED TO RE-DERIVE THE PROJECTION INSTEAD OF CALLING IT (repaired 2026-08-23): it +// matched SlotAssigned itself and carried its own inline `render_ipv4_address(addr: +// r.ipv4_address) as String`, so one concept — a binding's transport address — had two +// implementations inside a single file, and the NAMED one was the dead one +// (spark_endpoint_for_binding had zero callers in the corpus; the only occurrence was its own +// declaration). That is the §2 failure at its smallest scale, and its cost is specific rather +// than stylistic: the refusal guarantee spark_endpoint_for_binding states in its header — an +// unassigned slot yields NO endpoint, never a placeholder — was enforced only in the copy +// nothing called, so tightening it there would have left the probe path untouched. The fold now +// consumes the projection, and the identity it dispatches on comes from +// gunbc.spark.dgx_procurement router_binding_identity, which is total over the coproduct, rather +// than from an arm that only the assigned variant reaches. fn fleet_probe_endpoint_for(host: String) -> String { fold(dgx_spark_router_bindings, init: host, f: fn(acc, b) { - match b { - SlotAssigned { identity: i, reservation: r, allocation: _ } => - if (i as String) == host { - render_ipv4_address(addr: r.ipv4_address) as String - } else { - acc - } - SlotUnassigned { identity: _ } => acc + if (router_binding_identity(binding: b) as String) == host { + match spark_endpoint_for_binding(binding: b) { + Absent => acc + Present { value: endpoint } => endpoint + } + } else { + acc } }) } diff --git a/dag/test/claim/host_reach_identity_probe_witness_test.dag b/dag/test/claim/host_reach_identity_probe_witness_test.dag index 25a0cb05309..f6f3a55b00c 100644 --- a/dag/test/claim/host_reach_identity_probe_witness_test.dag +++ b/dag/test/claim/host_reach_identity_probe_witness_test.dag @@ -5,8 +5,14 @@ import gunbc.srv3_os_install_diagnostic { srv3_install_hang_no_router_lease_ms } import std.types { Bool, String, NonEmptyStr, List } import std.upsert_decision { ObservationVerdict, Converged, Drifted, Conflict, Inaccessible, UnknownRefused } import product.placement_supply { HostIdentity } -import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv3 } -import gunbc.fleet_reach_endpoint { fleet_probe_endpoint_for } +import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv3, operator_host_srv5 } +import gunbc.fleet_reach_endpoint { fleet_probe_endpoint_for, spark_endpoint_for_binding } +import gunbc.spark.dgx_procurement { + DgxSparkRouterBinding, + SlotUnassigned, + srv5_router_binding, + srv6_router_binding, +} import gunbc.host_reach_identity_probe { ReachProbeOutcome, ProbeReachable, @@ -196,3 +202,42 @@ test fn spark_probe_targets_are_modeled_addresses_not_names() -> Bool { && fleet_probe_endpoint_for(host: "srv6") == "192.168.1.223" && fleet_probe_endpoint_for(host: "srv1") == "srv1" } + +// The undecided slot exists only as a fixture: both production bindings are SlotAssigned, so this +// arm has zero live occupancy. Per DESIGN's reachability-read-as-occupancy rule that is a healthy +// guard being quiet — SlotUnassigned is a constructible variant a third unit lands in before its +// allocation is decided, and it is reachable from this projection's denominator, which is any +// binding at all. +data fixture_undecided_spark_slot: DgxSparkRouterBinding = SlotUnassigned { identity: operator_host_srv5 } + +fn spark_endpoint_or_empty(binding: DgxSparkRouterBinding) -> String { + match spark_endpoint_for_binding(binding: binding) { + Absent => "" + Present { value: endpoint } => endpoint + } +} + +// AN UNDECIDED SLOT YIELDS NO ENDPOINT — not a fabricated address and not a placeholder. This is +// the refusal spark_endpoint_for_binding's header claims, asserted through the projection rather +// than about it, and it is why the fold below must CALL that function instead of re-deriving: +// enforcing the refusal in a copy nothing consumes leaves the probe path unguarded. +test fn undecided_spark_slot_projects_no_endpoint() -> Bool { + match spark_endpoint_for_binding(binding: fixture_undecided_spark_slot) { + Absent => true + Present { value: _ } => false + } +} + +// THE DISCRIMINATING CONTROL FOR THE 2026-08-23 DUPLICATE REMOVAL. fleet_probe_endpoint_for used +// to re-derive the projection with its own inline render instead of calling +// spark_endpoint_for_binding, so the two could silently drift. Each side of this comparison is +// computed by a DIFFERENT entry point over the same binding, which is the whole content: a mutant +// that restores the inline derivation and changes it — a different render, a dropped cast, a +// stale address — TYPECHECKS and reds here. After the repair one implementation feeds both, so +// this is a permanent regression control rather than a probe that retires: it stays enrolled as +// the executing evidence that the two entry points have not forked again (§4b meta-obligation 4 — +// a climb deletes the redundant production machinery, never the evidence). +test fn probe_endpoint_agrees_with_the_projection_it_consumes() -> Bool { + fleet_probe_endpoint_for(host: "srv5") == spark_endpoint_or_empty(binding: srv5_router_binding) + && fleet_probe_endpoint_for(host: "srv6") == spark_endpoint_or_empty(binding: srv6_router_binding) +}