Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 21 additions & 8 deletions dag/gunbc/fleet_reach_endpoint.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand All @@ -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
}
})
}
Expand Down
49 changes: 47 additions & 2 deletions dag/test/claim/host_reach_identity_probe_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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)
}
Loading