diff --git a/dag/extdeps/bmc/megarac.dag b/dag/extdeps/bmc/megarac.dag index 089d83597a2..a2de9802433 100644 --- a/dag/extdeps/bmc/megarac.dag +++ b/dag/extdeps/bmc/megarac.dag @@ -44,9 +44,17 @@ data megarac_vendor: Vendor = ami // The family answer is the PUBLISHED default - which is what FactoryLogin's // published_password field means - admin/admin being AMI's widely published MegaRAC // default; the Foxconn Mt. Collins build observation (its bmc binding module) is -// corroboration, not the basis. An ODM build may ship differently; a workflow treats -// this as the first credential to TRY, and a refusal as an already-rotated or -// differently-shipped build, never as an error to force past. +// corroboration, not the basis. +// +// THIS IS THE ONE CREDENTIAL A WORKFLOW TESTS, NOT THE FIRST OF SEVERAL +// (NO-FALLBACK-0). It used to read "the first credential to TRY", which describes an +// ordered search: try this, and on refusal try the next. There is no next. An ODM +// build may ship differently, and a refusal here is a TERMINAL, typed fact about +// this unit - the build shipped other credentials, or they have already been rotated +// - which ends the attempt and is carried by a workflow-layer intake receipt. It is +// neither an error to force past nor a cue to guess again: a second credential +// attempted after the first is refused is exactly the fallback this model exists to +// refuse, and it is also how a fleet locks itself out. data megarac_factory_login: FactoryLogin = FactoryLogin { username: "admin", published_password: "admin", diff --git a/dag/gunbc/boot_artifact_delivery.dag b/dag/gunbc/boot_artifact_delivery.dag index 3e9aef9df86..b7ed20fc8d1 100644 --- a/dag/gunbc/boot_artifact_delivery.dag +++ b/dag/gunbc/boot_artifact_delivery.dag @@ -289,7 +289,7 @@ type BootArtifactStagingBinding { } // The staging binding of a path that staged nothing. Every offer Absent, so a -// caller that has no staging service refuses at CandidateStagingAbsent rather +// caller that has no staging service refuses at CandidateIneligible { cause: CandidateStagingAbsent } rather // than fabricating an offer. data boot_artifact_staging_unbound: BootArtifactStagingBinding = BootArtifactStagingBinding { redfish_image: none, @@ -352,9 +352,15 @@ fn boot_delivery_preference_order(preference: BootDeliveryPreference) -> List } | CandidateNetworkBootUnestablished { missing: List } +type BootDeliveryCandidateStanding + = CandidateEligible + | CandidateIneligible { cause: BootDeliveryCandidateIneligibility } + type BootDeliveryCandidateVerdict { candidate: BootDeliveryCandidate standing: BootDeliveryCandidateStanding } +// WHAT A CANDIDATE IS *IN A PLAN*, WHICH IS NOT WHAT IT WAS DURING SOLVING +// (NO-FALLBACK-0). Solving asks "is this eligible"; a plan answers "this is the +// transport, and here is why every other candidate is NOT one". Those are +// different questions and they had one type, so a plan carried a second +// CandidateEligible verdict beside the selected one -- an executor holding the +// plan could read it as the next thing to attempt when the first failed, which +// is the ordered-fallback workflow this model refuses. +// +// After selection no candidate in a plan reads as available. A candidate the +// policy outranked is recorded as OUTRANKED BY the transport that was chosen, +// naming it, so the row states a completed decision rather than an offer; there +// is deliberately no arm meaning "eligible and not selected". The raw standing +// survives on the refusal path, where nothing was selected and the whole +// considered set is the evidence. +type BootDeliveryPlanCandidateDisposition + = PlanCandidateSelected + | PlanCandidateOutrankedBy { selected: BootDeliveryCandidate } + | PlanCandidateIneligible { cause: BootDeliveryCandidateIneligibility } + +type BootDeliveryPlanCandidateVerdict { + candidate: BootDeliveryCandidate + disposition: BootDeliveryPlanCandidateDisposition +} + +// The one place a solving verdict becomes a plan verdict. CandidateEligible is +// the only standing that can become either arm, and which one it becomes is +// decided by identity against the selected candidate -- never by list position. +fn plan_candidate_disposition( + verdict: BootDeliveryCandidateVerdict, + selected: BootDeliveryCandidate, +) -> BootDeliveryPlanCandidateDisposition { + if verdict.candidate == selected { + PlanCandidateSelected + } else { + match verdict.standing { + CandidateEligible => PlanCandidateOutrankedBy { selected: selected } + CandidateIneligible { cause: c } => PlanCandidateIneligible { cause: c } + } + } +} + +fn plan_candidate_verdict( + verdict: BootDeliveryCandidateVerdict, + selected: BootDeliveryCandidate, +) -> BootDeliveryPlanCandidateVerdict { + BootDeliveryPlanCandidateVerdict { + candidate: verdict.candidate, + disposition: plan_candidate_disposition(verdict: verdict, selected: selected), + } +} + +fn plan_candidate_verdicts( + verdicts: List, + selected: BootDeliveryCandidate, +) -> List { + verdicts |> map(v => plan_candidate_verdict(verdict: v, selected: selected)) +} + // The evidence particular to the SELECTED candidate (ruling 4 §1): a // CandidateEligible verdict alone does not tell an executor what made it // eligible. Profile-shaped candidates are eligible from the profile/observation @@ -395,7 +463,7 @@ type BootDeliveryEligibilityProvenance { profile_provenance: BmcAccessProfileProvenance evidence_manifest: List selected: SelectedCandidateEvidence - considered: List + considered: List } // PLANNED, NOT ESTABLISHED. A plan is a candidate the bound profile and the @@ -458,9 +526,9 @@ fn bind_boot_delivery_target(target: BootDeliveryTarget, access: BoundBmcAccessC fn surface_candidate_standing(ctx: BoundBmcAccessContext, surface: BmcAccessSurface) -> BootDeliveryCandidateStanding { match bmc_surface_eligibility(profile: ctx.profile, observation: ctx.observation, surface: surface) { SurfaceEligible => CandidateEligible - SurfaceAbsentFromProfile => CandidateSurfaceAbsentFromProfile { surface: surface } - SurfaceAbsentFromLiveObservation => CandidateLiveSurfaceAbsent { surface: surface } - SurfaceProfileObservationIdentityMismatch { profile: _, observed: _ } => CandidateProfileObservationIdentityMismatch { surface: surface } + SurfaceAbsentFromProfile => CandidateIneligible { cause: CandidateSurfaceAbsentFromProfile { surface: surface } } + SurfaceAbsentFromLiveObservation => CandidateIneligible { cause: CandidateLiveSurfaceAbsent { surface: surface } } + SurfaceProfileObservationIdentityMismatch { profile: _, observed: _ } => CandidateIneligible { cause: CandidateProfileObservationIdentityMismatch { surface: surface } } } } @@ -468,7 +536,7 @@ fn staged_digest_standing(offered: ContentHash, requested: ContentHash) -> BootD if content_hash_equal(left: offered, right: requested) { CandidateEligible } else { - CandidateStagedArtifactMismatch { offered: offered, requested: requested } + CandidateIneligible { cause: CandidateStagedArtifactMismatch { offered: offered, requested: requested } } } } @@ -480,23 +548,23 @@ fn staged_digest_standing(offered: ContentHash, requested: ContentHash) -> BootD fn redfish_probe_standing(receipt: RedfishVirtualMediaProbeReceipt, offered: RedfishVirtualMediaTransferProtocol) -> BootDeliveryCandidateStanding { match redfish_probe_receipt_coherence(receipt: receipt) { ProbeReceiptProtocolsWithoutFloor { progress: progress, admitted: admitted } => - CandidateRedfishProbeContradictory { progress: progress, admitted: admitted } + CandidateIneligible { cause: CandidateRedfishProbeContradictory { progress: progress, admitted: admitted } } ProbeReceiptFloorWithoutProtocols { progress: progress } => - CandidateRedfishProbeContradictory { progress: progress, admitted: receipt.admitted_protocols } + CandidateIneligible { cause: CandidateRedfishProbeContradictory { progress: progress, admitted: receipt.admitted_protocols } } ProbeReceiptBelowFloor { progress: progress } => - CandidateRedfishProbeBelowPlanFloor { progress: progress } + CandidateIneligible { cause: CandidateRedfishProbeBelowPlanFloor { progress: progress } } ProbeReceiptAtFloor { admitted: admitted } => if redfish_transfer_protocol_in(protocols: admitted, protocol: offered) { CandidateEligible } else { - CandidateRedfishProtocolNotAdmitted { offered: offered, admitted: admitted } + CandidateIneligible { cause: CandidateRedfishProtocolNotAdmitted { offered: offered, admitted: admitted } } } } } fn redfish_virtual_media_candidate(ctx: BoundBmcAccessContext, request: BootDeliveryRequest) -> BootDeliveryCandidateStanding { if release_row_has_capability(row: ctx.capability_row, cap: CapabilityVirtualMedia) == false { - CandidateCapabilityAbsent + CandidateIneligible { cause: CandidateCapabilityAbsent } } else { let standing = surface_candidate_standing(ctx: ctx, surface: SurfaceRedfishVirtualMedia) let surface_ok = standing == CandidateEligible @@ -504,10 +572,10 @@ fn redfish_virtual_media_candidate(ctx: BoundBmcAccessContext, request: BootDeli standing } else { match ctx.observation.redfish_virtual_media_probe { - Absent => CandidateRedfishProbeAbsent + Absent => CandidateIneligible { cause: CandidateRedfishProbeAbsent } Present { value: receipt } => match request.staging.redfish_image { - Absent => CandidateStagingAbsent + Absent => CandidateIneligible { cause: CandidateStagingAbsent } Present { value: offer } => { let digest = staged_digest_standing(offered: offer.artifact_digest, requested: request.artifact.digest) let digest_ok = digest == CandidateEligible @@ -525,7 +593,7 @@ fn redfish_virtual_media_candidate(ctx: BoundBmcAccessContext, request: BootDeli fn nbd_proxy_websocket_candidate(ctx: BoundBmcAccessContext, request: BootDeliveryRequest) -> BootDeliveryCandidateStanding { if release_row_has_capability(row: ctx.capability_row, cap: CapabilityNbdProxyVirtualMedia) == false { - CandidateCapabilityAbsent + CandidateIneligible { cause: CandidateCapabilityAbsent } } else { let standing = surface_candidate_standing(ctx: ctx, surface: SurfaceOemNbdWebsocket) let surface_ok = standing == CandidateEligible @@ -533,10 +601,10 @@ fn nbd_proxy_websocket_candidate(ctx: BoundBmcAccessContext, request: BootDelive standing } else { match bmc_profile_nbd_websocket_path(profile: ctx.profile) { - Absent => CandidateRouteAbsent { surface: SurfaceOemNbdWebsocket } + Absent => CandidateIneligible { cause: CandidateRouteAbsent { surface: SurfaceOemNbdWebsocket } } Present { value: _ } => match request.staging.nbd_export { - Absent => CandidateStagingAbsent + Absent => CandidateIneligible { cause: CandidateStagingAbsent } Present { value: offer } => staged_digest_standing(offered: offer.artifact_digest, requested: request.artifact.digest) } } @@ -550,7 +618,7 @@ fn nbd_proxy_websocket_candidate(ctx: BoundBmcAccessContext, request: BootDelive // the executed refusal (opaque codes 13410/13460) modeled as a standing. fn megarac_rest_remote_media_candidate(ctx: BoundBmcAccessContext, request: BootDeliveryRequest) -> BootDeliveryCandidateStanding { if release_row_has_capability(row: ctx.capability_row, cap: CapabilityOemRemoteMedia) == false { - CandidateCapabilityAbsent + CandidateIneligible { cause: CandidateCapabilityAbsent } } else { let standing = surface_candidate_standing(ctx: ctx, surface: SurfaceOemRestRemoteMedia) let surface_ok = standing == CandidateEligible @@ -558,13 +626,13 @@ fn megarac_rest_remote_media_candidate(ctx: BoundBmcAccessContext, request: Boot standing } else { match bmc_profile_megarac_image_redirection(profile: ctx.profile) { - Absent => CandidateRouteAbsent { surface: SurfaceOemRestRemoteMedia } + Absent => CandidateIneligible { cause: CandidateRouteAbsent { surface: SurfaceOemRestRemoteMedia } } Present { value: redirection } => match redirection { - MegaRacImageRedirectionUnset => CandidateOemParameterUnset { surface: SurfaceOemRestRemoteMedia } + MegaRacImageRedirectionUnset => CandidateIneligible { cause: CandidateOemParameterUnset { surface: SurfaceOemRestRemoteMedia } } MegaRacImageRedirectionEnabled => match request.staging.megarac_share { - Absent => CandidateStagingAbsent + Absent => CandidateIneligible { cause: CandidateStagingAbsent } Present { value: offer } => staged_digest_standing(offered: offer.artifact_digest, requested: request.artifact.digest) } } @@ -579,19 +647,19 @@ fn megarac_rest_remote_media_candidate(ctx: BoundBmcAccessContext, request: Boot // THIS request's target, plus a staged export naming the requested digest. fn configfs_usb_gadget_candidate(ev: BoundBootDeliveryEvidence, request: BootDeliveryRequest) -> BootDeliveryCandidateStanding { match ev.configfs { - ReinstallPathObservationForOtherTarget { requested: _, found: f } => CandidateEvidenceForOtherTarget { evidence_target: f } + ReinstallPathObservationForOtherTarget { requested: _, found: f } => CandidateIneligible { cause: CandidateEvidenceForOtherTarget { evidence_target: f } } TargetBoundReinstallPath { target: t, standing: s, observations: _ } => if same_boot_delivery_target(left: t, right: request.target) == false { - CandidateEvidenceForOtherTarget { evidence_target: t } + CandidateIneligible { cause: CandidateEvidenceForOtherTarget { evidence_target: t } } } else { match s { ReinstallPathEstablished { qualified_by: _ } => match request.staging.configfs_gadget { - Absent => CandidateStagingAbsent + Absent => CandidateIneligible { cause: CandidateStagingAbsent } Present { value: offer } => staged_digest_standing(offered: offer.artifact_digest, requested: request.artifact.digest) } - ReinstallPathUnestablished { missing_probes: m } => CandidateConfigfsUnestablished { missing: m } - ReinstallPathRefused { observed_absent: a } => CandidateConfigfsRefused { observed_absent: a } + ReinstallPathUnestablished { missing_probes: m } => CandidateIneligible { cause: CandidateConfigfsUnestablished { missing: m } } + ReinstallPathRefused { observed_absent: a } => CandidateIneligible { cause: CandidateConfigfsRefused { observed_absent: a } } } } } @@ -601,11 +669,11 @@ fn uefi_http_candidate(ev: BoundBootDeliveryEvidence, request: BootDeliveryReque match ev.uefi_http { UefiHttpDeliveryEstablished { target: t, params: p, evidence: _ } => if same_boot_delivery_target(left: t, right: request.target) == false { - CandidateEvidenceForOtherTarget { evidence_target: t } + CandidateIneligible { cause: CandidateEvidenceForOtherTarget { evidence_target: t } } } else { staged_digest_standing(offered: p.artifact_digest, requested: request.artifact.digest) } - UefiHttpDeliveryUnestablished { missing: m } => CandidateUefiHttpUnestablished { missing: m } + UefiHttpDeliveryUnestablished { missing: m } => CandidateIneligible { cause: CandidateUefiHttpUnestablished { missing: m } } } } @@ -613,17 +681,22 @@ fn pxe_chain_candidate(ev: BoundBootDeliveryEvidence, request: BootDeliveryReque match ev.network_boot { NetworkBootDeliveryEstablished { evidence: e } => if same_boot_delivery_target(left: e.target, right: request.target) == false { - CandidateEvidenceForOtherTarget { evidence_target: e.target } + CandidateIneligible { cause: CandidateEvidenceForOtherTarget { evidence_target: e.target } } } else { staged_digest_standing(offered: e.artifact_digest, requested: request.artifact.digest) } - NetworkBootDeliveryUnestablished { missing: m } => CandidateNetworkBootUnestablished { missing: m } + NetworkBootDeliveryUnestablished { missing: m } => CandidateIneligible { cause: CandidateNetworkBootUnestablished { missing: m } } } } // A built delivery together with the evidence that made its candidate // eligible, so the plan's provenance is read off the same selection. +// The candidate identity travels WITH the built delivery (NO-FALLBACK-0). The +// plan's per-candidate dispositions are decided by identity against this field, +// so "which one was selected" is read off the construction rather than +// re-derived from the preference list's position. type BuiltBootArtifactDelivery { + candidate: BootDeliveryCandidate delivery: BootArtifactDelivery selected: SelectedCandidateEvidence } @@ -671,6 +744,7 @@ fn build_boot_artifact_delivery( Present { value: offer } => Present { value: BuiltBootArtifactDelivery { + candidate: candidate, delivery: RedfishVirtualMediaPull { params: RedfishVirtualMediaParams { media: receipt.locator, image: offer.image, transfer_protocol: offer.transfer_protocol }, }, @@ -685,6 +759,7 @@ fn build_boot_artifact_delivery( Present { value: offer } => Present { value: BuiltBootArtifactDelivery { + candidate: candidate, delivery: MegaRacRestRemoteMedia { params: MegaRacRemoteMediaParams { share_type: offer.share_type, @@ -707,6 +782,7 @@ fn build_boot_artifact_delivery( Present { value: offer } => Present { value: BuiltBootArtifactDelivery { + candidate: candidate, delivery: OpenBmcNbdProxyWebsocket { params: NbdProxyWebsocatParams { session_token: offer.session_token, ws_path: ws_path, local_nbd_port: offer.local_nbd_port }, }, @@ -726,6 +802,7 @@ fn build_boot_artifact_delivery( Present { value: offer } => Present { value: BuiltBootArtifactDelivery { + candidate: candidate, delivery: OpenBmcConfigfsUsbGadget { params: ConfigfsGadgetParams { nbd_server_host: offer.nbd_server_host, @@ -746,20 +823,25 @@ fn build_boot_artifact_delivery( CandidateUefiHttpBoot => match ev.uefi_http { UefiHttpDeliveryEstablished { target: _, params: p, evidence: evs } => - Present { value: BuiltBootArtifactDelivery { delivery: UefiHttpBoot { params: p }, selected: SelectedFromUefiHttpEvidence { evidence: evs } } } + Present { value: BuiltBootArtifactDelivery { candidate: candidate, delivery: UefiHttpBoot { params: p }, selected: SelectedFromUefiHttpEvidence { evidence: evs } } } UefiHttpDeliveryUnestablished { missing: _ } => none } CandidatePxeChainBoot => match ev.network_boot { NetworkBootDeliveryEstablished { evidence: e } => - Present { value: BuiltBootArtifactDelivery { delivery: PxeChainBoot { evidence: e }, selected: SelectedFromNetworkBootEstablishment { establishment: e } } } + Present { value: BuiltBootArtifactDelivery { candidate: candidate, delivery: PxeChainBoot { evidence: e }, selected: SelectedFromNetworkBootEstablishment { establishment: e } } } NetworkBootDeliveryUnestablished { missing: _ } => none } } } -// The first candidate in the POLICY's order that is eligible, built. -fn first_eligible_boot_artifact_delivery( +// THE ONE TRANSPORT THE POLICY SELECTS, built. The policy's order is a total +// ranking over a set already decided by evidence, so this walk RANKS -- it does +// not search, and it never attempts. Every candidate's eligibility is settled +// before this runs; taking the highest-ranked eligible one is a completed +// decision, and the plan records the rest as outranked rather than as +// alternatives (NO-FALLBACK-0). +fn selected_boot_artifact_delivery( ctx: BoundBmcAccessContext, ev: BoundBootDeliveryEvidence, request: BootDeliveryRequest, @@ -789,7 +871,7 @@ fn select_boot_artifact_delivery( control_route: BmcBootControlRouteObservation, verdicts: List, ) -> BootDeliverySolution { - match first_eligible_boot_artifact_delivery(ctx: ctx, ev: ev, request: request, policy: policy, verdicts: verdicts) { + match selected_boot_artifact_delivery(ctx: ctx, ev: ev, request: request, policy: policy, verdicts: verdicts) { Present { value: built } => BootDeliveryPlanned { plan: BootDeliveryPlan { @@ -802,7 +884,7 @@ fn select_boot_artifact_delivery( profile_provenance: ctx.profile_provenance, evidence_manifest: ctx.evidence_manifest, selected: built.selected, - considered: verdicts, + considered: plan_candidate_verdicts(verdicts: verdicts, selected: built.candidate), }, }, } @@ -953,7 +1035,7 @@ fn boot_delivery_candidate_standing_of( ) -> BootDeliveryCandidateStanding { fold( verdicts, - init: CandidateCapabilityAbsent, + init: CandidateIneligible { cause: CandidateCapabilityAbsent }, f: (acc, v) => if v.candidate == candidate { v.standing } else { acc }, ) } diff --git a/dag/test/claim/machine_intake/boot_artifact_delivery_witness_test.dag b/dag/test/claim/machine_intake/boot_artifact_delivery_witness_test.dag index f6fa2f192ac..870142703e4 100644 --- a/dag/test/claim/machine_intake/boot_artifact_delivery_witness_test.dag +++ b/dag/test/claim/machine_intake/boot_artifact_delivery_witness_test.dag @@ -1,6 +1,6 @@ module test.claim.boot_artifact_delivery_witness_test -import std.types { Bool, List, NonEmptyStr, String, list_length } +import std.types { Bool, Int, List, NonEmptyStr, String, list_length } import std.content_hash { ContentHash, content_hash_of_value } import std.decl_ref { DeclarationRef, WholeDeclaration } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -144,6 +144,7 @@ import gunbc.boot_artifact_delivery { BoundBootDeliveryEvidence, CandidateConfigfsUnestablished, CandidateEvidenceForOtherTarget, + CandidateIneligible, CandidateLiveSurfaceAbsent, CandidateNetworkBootUnestablished, CandidateOemParameterUnset, @@ -155,6 +156,10 @@ import gunbc.boot_artifact_delivery { CandidateRedfishProtocolNotAdmitted, CandidateRedfishVirtualMedia, CandidateMegaRacRestRemoteMedia, + PlanCandidateIneligible, + PlanCandidateSelected, + PlanCandidateOutrankedBy, + BootDeliveryPlanCandidateVerdict, CandidateStagedArtifactMismatch, ConfigfsGadgetOffer, DeliveryAccessUnbound, @@ -580,7 +585,7 @@ test fn redfish_virtual_media_planned_from_bound_context_and_probe_receipt() -> } // RED (ruling 3 §1) — the staged URI serves digest B while the request names -// digest A: the Redfish candidate stops at CandidateStagedArtifactMismatch and +// digest A: the Redfish candidate stops at CandidateIneligible { cause: CandidateStagedArtifactMismatch } and // nothing is planned. test fn staged_artifact_digest_mismatch_refuses_the_plan() -> Bool { match solve(profile: vm_profile, receipt: observed(surfaces: [SurfaceBootControl, SurfaceRedfishVirtualMedia], probe: Present { value: probe_https }), staging: staging_wrong_redfish_digest) { @@ -588,7 +593,7 @@ test fn staged_artifact_digest_mismatch_refuses_the_plan() -> Bool { match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateRedfishVirtualMedia) { - CandidateStagedArtifactMismatch { offered: _, requested: _ } => true + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateStagedArtifactMismatch { offered: _, requested: _ } => true _ => false } _ => false } _ => false @@ -748,7 +753,7 @@ test fn offered_protocol_not_admitted_by_the_probe_refuses() -> Bool { match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateRedfishVirtualMedia) { - CandidateRedfishProtocolNotAdmitted { offered: o, admitted: a } => o == TransferHttps && list_length(items: a) == 1 + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateRedfishProtocolNotAdmitted { offered: o, admitted: a } => o == TransferHttps && list_length(items: a) == 1 _ => false } _ => false } _ => false @@ -765,7 +770,7 @@ test fn absent_probe_receipt_refuses_the_redfish_arm() -> Bool { match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateRedfishVirtualMedia) { - CandidateRedfishProbeAbsent => true + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateRedfishProbeAbsent => true _ => false } _ => false } _ => false @@ -781,7 +786,7 @@ test fn redfish_collection_discovery_alone_does_not_plan() -> Bool { match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateRedfishVirtualMedia) { - CandidateRedfishProbeBelowPlanFloor { progress: p } => p == CollectionDiscovered + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateRedfishProbeBelowPlanFloor { progress: p } => p == CollectionDiscovered _ => false } _ => false } _ => false @@ -799,7 +804,7 @@ fn refuses_as_probe_contradiction(s: BootDeliverySolution, expected: RedfishVirt match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateRedfishVirtualMedia) { - CandidateRedfishProbeContradictory { progress: p, admitted: a } => p == expected && list_length(items: a) == 1 + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateRedfishProbeContradictory { progress: p, admitted: a } => p == expected && list_length(items: a) == 1 _ => false } _ => false } _ => false @@ -823,7 +828,7 @@ test fn live_boot_control_absent_refuses_despite_catalog_capability_and_live_med match c { DeliveryBootControlSurfaceUnestablished { standing: s } => match s { - CandidateLiveSurfaceAbsent { surface: sf } => sf == SurfaceBootControl + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateLiveSurfaceAbsent { surface: sf } => sf == SurfaceBootControl _ => false } _ => false } _ => false @@ -912,7 +917,7 @@ test fn megarac_route_without_image_redirection_refuses() -> Bool { match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateMegaRacRestRemoteMedia) { - CandidateOemParameterUnset { surface: s } => s == SurfaceOemRestRemoteMedia + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateOemParameterUnset { surface: s } => s == SurfaceOemRestRemoteMedia _ => false } _ => false } _ => false @@ -929,7 +934,7 @@ test fn redfish_virtual_media_absent_from_live_observation_is_not_selected() -> match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateRedfishVirtualMedia) { - CandidateLiveSurfaceAbsent { surface: s } => s == SurfaceRedfishVirtualMedia + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateLiveSurfaceAbsent { surface: s } => s == SurfaceRedfishVirtualMedia _ => false } _ => false } _ => false @@ -1008,7 +1013,7 @@ test fn no_virtual_media_and_no_network_boot_evidence_refuses_without_pxe() -> B match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidatePxeChainBoot) { - CandidateNetworkBootUnestablished { missing: m } => list_length(items: m) == 4 + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateNetworkBootUnestablished { missing: m } => list_length(items: m) == 4 _ => false } _ => false } _ => false @@ -1064,7 +1069,7 @@ test fn empty_configfs_observation_population_does_not_establish() -> Bool { match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateOpenBmcConfigfsUsbGadget) { - CandidateConfigfsUnestablished { missing: m } => list_length(items: m) == 8 + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateConfigfsUnestablished { missing: m } => list_length(items: m) == 8 _ => false } _ => false } _ => false @@ -1088,7 +1093,7 @@ test fn configfs_path_established_for_another_target_is_refused() -> Bool { match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidateOpenBmcConfigfsUsbGadget) { - CandidateEvidenceForOtherTarget { evidence_target: t } => (t.subject.attempt_id as NonEmptyStr) == (attempt_two as NonEmptyStr) + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateEvidenceForOtherTarget { evidence_target: t } => (t.subject.attempt_id as NonEmptyStr) == (attempt_two as NonEmptyStr) _ => false } _ => false } _ => false @@ -1149,7 +1154,7 @@ test fn established_network_boot_naming_the_artifact_selects_pxe_and_another_dig match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidatePxeChainBoot) { - CandidateStagedArtifactMismatch { offered: _, requested: _ } => true + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateStagedArtifactMismatch { offered: _, requested: _ } => true _ => false } _ => false } _ => false @@ -1166,7 +1171,7 @@ test fn established_network_boot_naming_the_artifact_selects_pxe_and_another_dig match c { DeliveryNoEligibleTransport { firmware: _, considered: considered } => match boot_delivery_candidate_standing_of(verdicts: considered, candidate: CandidatePxeChainBoot) { - CandidateEvidenceForOtherTarget { evidence_target: t } => t.endpoint == other_controller + CandidateIneligible { cause: ineligibility } => match ineligibility { CandidateEvidenceForOtherTarget { evidence_target: t } => t.endpoint == other_controller _ => false } _ => false } _ => false @@ -1215,3 +1220,60 @@ test fn redfish_transport_inhabits_the_shared_axis_with_dmtf_action_path() -> Bo virtual_media_transport_kind(transport: transport) == "redfish-virtualmedia" && redfish_virtual_media_insert_action_path(locator: params.media) == "/redfish/v1/Managers/1/VirtualMedia/CD1/Actions/VirtualMedia.InsertMedia" } + +// NO-FALLBACK-0: A PLAN NAMES ONE TRANSPORT AND OFFERS NO SECOND ONE. +// +// This is the only shape that separates a plan from an ordered fallback list, +// and no other control in this module reaches it: every other plan witness +// asserts what the SELECTED transport is, which a model that also hands over a +// spare would satisfy identically. The fixture is deliberately the two-eligible +// case — the profile and the live observation admit BOTH Redfish VirtualMedia +// and the MegaRAC REST remote-media surface — so the policy has a real choice +// to make and a real loser to record. +// +// The loser must appear as OUTRANKED BY the selected transport, naming it: a +// completed decision, not an offer. If plan verdicts still carried the solving +// standing, MegaRAC would read CandidateEligible here and an executor holding +// this plan could attempt it after Redfish failed. The first two assertions +// pin exactly one selection; the third is what makes the test non-vacuous, +// because without an outranked row the fixture would have had only one eligible +// candidate and would prove nothing about fallback at all. +fn plan_selected_count(verdicts: List) -> Int { + fold(verdicts, init: 0, f: fn(acc, v) { + match v.disposition { + PlanCandidateSelected => acc + 1 + PlanCandidateOutrankedBy { selected: _ } => acc + PlanCandidateIneligible { cause: _ } => acc + } + }) +} + +fn plan_outranked_by_redfish_count(verdicts: List) -> Int { + fold(verdicts, init: 0, f: fn(acc, v) { + match v.disposition { + PlanCandidateSelected => acc + PlanCandidateOutrankedBy { selected: sel } => if (sel == CandidateRedfishVirtualMedia) { acc + 1 } else { acc } + PlanCandidateIneligible { cause: _ } => acc + } + }) +} + +fn plan_selected_is_redfish_count(verdicts: List) -> Int { + fold(verdicts, init: 0, f: fn(acc, v) { + match v.disposition { + PlanCandidateSelected => if (v.candidate == CandidateRedfishVirtualMedia) { acc + 1 } else { acc } + PlanCandidateOutrankedBy { selected: _ } => acc + PlanCandidateIneligible { cause: _ } => acc + } + }) +} + +test fn a_plan_names_one_transport_and_records_the_rest_as_outranked() -> Bool { + match solve(profile: vm_profile, receipt: observed(surfaces: [SurfaceBootControl, SurfaceRedfishVirtualMedia, SurfaceOemRestRemoteMedia], probe: Present { value: probe_https }), staging: staging_all) { + BootDeliveryPlanned { plan: p } => + plan_selected_count(verdicts: p.eligibility.considered) == 1 + && plan_selected_is_redfish_count(verdicts: p.eligibility.considered) == 1 + && plan_outranked_by_redfish_count(verdicts: p.eligibility.considered) >= 1 + BootDeliveryRefused { cause: _ } => false + } +} diff --git a/dag/test/claim/machine_intake/no_fallback_plan_ineligibility_wall_test.dag b/dag/test/claim/machine_intake/no_fallback_plan_ineligibility_wall_test.dag new file mode 100644 index 00000000000..508d313a084 --- /dev/null +++ b/dag/test/claim/machine_intake/no_fallback_plan_ineligibility_wall_test.dag @@ -0,0 +1,49 @@ +module test.claim.machine_intake.no_fallback_plan_ineligibility_wall_test + +import std.types { Bool, String } +import gunbc.compile_diagnostic_census { CompileDiagnosticCensus, CensusObserved, CensusNotRunnable } +import gunbc.guarantee_probe_corpus { census_blocking_count_for_class } +import v2.std.optional { Absent, Present } + +// THE WALL IS REAL, PROVEN WHERE ITS RED IS AUTHORABLE (DESIGN §4b). +// NO-FALLBACK-0's claim is that a plan cannot carry a spare available +// transport. The accepted corpus can no longer express the violation — +// PlanCandidateIneligible carries BootDeliveryCandidateIneligibility, which has +// no eligible inhabitant — so asking for the refusal inside the corpus would be +// asking for a check whose RED is unwritable, i.e. a decoration. +// +// §4b names the second boundary that decides it: a state unrepresentable in the +// ACCEPTED corpus is still representable as SOURCE HANDED TO THE COMPILER BY A +// FIXTURE. These two sources differ on exactly one axis — the value placed in +// the plan's ineligible arm — so the verdict cannot be attributed to anything +// else. The RED places CandidateEligible there and must be refused; the GREEN +// places a real ineligibility cause and must compile. +data plan_ineligible_eligible_red_source: String = "module probe_no_fallback_plan_ineligible_eligible_red\nimport gunbc.boot_artifact_delivery { BootDeliveryPlanCandidateDisposition, CandidateEligible, PlanCandidateIneligible }\nfn f() -> BootDeliveryPlanCandidateDisposition { PlanCandidateIneligible { cause: CandidateEligible } }\n" + +data plan_ineligible_cause_green_source: String = "module probe_no_fallback_plan_ineligible_cause_green\nimport gunbc.boot_artifact_delivery { BootDeliveryPlanCandidateDisposition, CandidateStagingAbsent, PlanCandidateIneligible }\nfn f() -> BootDeliveryPlanCandidateDisposition { PlanCandidateIneligible { cause: CandidateStagingAbsent } }\n" + +// THE DISCRIMINATING RED. Before the refusal-only split this source compiled, +// because PlanCandidateIneligible carried the whole standing and CandidateEligible +// inhabited it. It is the exact contradictory row NO-FALLBACK-0 forbids: a +// candidate recorded as ineligible whose stated cause is that it was eligible — +// an executor reading the plan finds a spare transport to try next. +test fn an_eligible_standing_cannot_be_placed_in_a_plans_ineligible_arm() -> Bool { + match census_blocking_count_for_class(census: compile_dag_diagnostic_census(plan_ineligible_eligible_red_source), wanted: "TypeMismatch") { + Present { value: n } => n >= 1 + Absent => false + } +} + +// THE POSITIVE CONTROL. Without it the RED above could be green for any reason +// at all — a broken import, a misspelled type — and would still look like a +// wall. +test fn a_real_ineligibility_cause_is_still_admitted_in_that_arm() -> Bool { + match compile_dag_diagnostic_census(plan_ineligible_cause_green_source) { + CensusObserved { rows: rows } => + match census_blocking_count_for_class(census: CensusObserved { rows: rows }, wanted: "TypeMismatch") { + Present { value: n } => n == 0 + Absent => false + } + CensusNotRunnable { cause: _ } => false + } +}