diff --git a/dag/gunbc/bmc/bmc_implementation_dispatch.dag b/dag/gunbc/bmc/bmc_implementation_dispatch.dag index 95485399cf5..30a783863b3 100644 --- a/dag/gunbc/bmc/bmc_implementation_dispatch.dag +++ b/dag/gunbc/bmc/bmc_implementation_dispatch.dag @@ -1,7 +1,9 @@ module gunbc.bmc_implementation_dispatch -import std.types { List, String } +import std.types { List, NonEmptyStr, String } import std.credentials { FactoryLogin } +import std.dissolution { DissolutionCondition, unbound_dissolution } +import std.decl_ref { DeclarationRef, decl_field_ref } import extdeps.bmc.endpoint { AmiMegaRac, BmcFirmwareFamily, BmcProtocol, OpenBmc } import extdeps.bmc.openbmc { HostStorageBlind, @@ -19,7 +21,16 @@ import extdeps.bmc.megarac { megarac_factory_login, megarac_supported_protocols_ // OpenBMC module import the MegaRAC one — the 'a Chrome change must not require editing // Safari's module' violation named in DESIGN §3, and the reason those functions now live here. // Each is an exhaustive match, so a third implementation refuses to compile here and nowhere -// else; that is the census. Every arm returns what its implementation module CITES at the +// else; that is the census. THAT SENTENCE IS LOAD-BEARING AND IT IS WHY rotation_route_for_family +// LANDED HERE RATHER THAN IN machine_intake (review 63250, gunbc#10952). It was first authored in +// gunbc.machine_intake_bmc_rotation_route as a fourth `match family` -- which would have made +// "here and nowhere else" false the moment it merged, and split the third-implementation census +// across two modules with no cross-reference. The route table is realization keyed on firmware +// family and cites only extdeps.bmc facts, so this is its home by the same reasoning that moved +// the gunbc#9678 arms out of extdeps.bmc.openbmc. What stayed behind is the part that is NOT +// family-keyed: rotation_application_for_route maps a route to a machine_intake +// CredentialRotationApplication, so hoisting it would make this peripheral dispatch module depend +// on machine_intake and invert the layering it exists to keep straight. Every arm returns what its implementation module CITES at the // family grain: MegaRAC's published admin/admin default and IPMI-only protocol floor come from // extdeps.bmc.megarac, whose scope note explains why Redfish presence is a build-scoped fact // carried on the build binding, never here. @@ -51,3 +62,78 @@ fn bmc_firmware_host_storage_visibility(family: BmcFirmwareFamily) -> RedfishHos AmiMegaRac => megarac_host_storage_visibility_floor } } + +// THE AVAILABLE ARM CARRIES REFERENCES, NOT A SENTENCE ABOUT THEM (review 63263). It was a single +// path_note String spelling out the method, the path template, the JSON member, the operation name +// and the executing tool -- and every one of those is ALREADY a modeled fact: the argv is +// `operation SetAccountPassword` on the redfish.Http service, the action shape is the +// SetAccountPassword arm of RedfishSystemAction, and the provenance is the call site in +// gunbc.tools.bmc_onboard. A String leaf hiding named parts is anemic modeling (DESIGN §2), and a +// symbol cited INSIDE a string literal is unreachable from the Node tree, so unlike a +// DeclarationRef it is not harvested by the citation checker -- it can rot with neither end touched. +// +// THE REFS ARE BUILT BY std.decl_ref's OWN CONSTRUCTOR, not spelled as record literals here (review +// 63521). That module's annotation states the rule: a module needing a DeclarationRef imports the +// constructor from the type's own module and never re-mints it. Spelling the literal inline is the +// same re-invention DESIGN §2 forbids, one layer down from the prose leaf this arm already replaced. +// +// AND IT WOULD NOT HAVE SURVIVED ITS OWN FRONTIER. rotation_route_consumption_frontier promises an +// actuator that DERIVES the rotation by calling this table; that actuator needs the operation, not +// a description of it, so the arm would have been rewritten rather than consumed -- §6's reviewer +// test answered "no" on the one arm that is supposed to work. +type BmcRotationRoute + = RotationRouteRedfishAccountService { transport_operation: DeclarationRef, action_shape: DeclarationRef } + | RotationRouteUnavailable { family_note: NonEmptyStr, detail: NonEmptyStr } + +// THE MEGARAC ARM IS UNAVAILABLE AND THAT IS A GROUNDED STATEMENT, NOT A GAP LEFT BLANK. +// extdeps.bmc.megarac declares its own admission rule in its scope note: its REST operation rows +// are "the SP-X interface shape AS EXECUTED on that build - the one place a single-build execution +// grounds a family-grain row - and carry that provenance explicitly". Six operations are rostered +// there and every one was executed against the controller. NO USER-MANAGEMENT OPERATION HAS BEEN +// EXECUTED, so authoring one would put an unexecuted row beside six executed ones under a rule that +// admits only the executed -- the module contradicting itself in its own file. AMI publishes no +// SP-X API reference to cite instead; the module's external authority is a product page. +// +// AND ONE ATTEMPT IS KNOWN TO HAVE REACHED SOMETHING. gunbc#10630 records a rotation attempt whose +// REST path answered "attempt to set previous password" against a policy-conforming secret -- a +// DECIDED response, so an endpoint exists, parses the field and applies a history policy to it. The +// request that produced it was never committed and cannot be recovered from any diff, which is +// filed as gunbc.recurring_failure_mode.ad_hoc_hardware_probe_produces_no_receipt. So the honest +// state is not "MegaRAC cannot rotate" -- it is "we have seen it answer and we cannot say how we +// asked". +fn rotation_route_for_family(family: BmcFirmwareFamily) -> BmcRotationRoute { + match family { + OpenBmc => RotationRouteRedfishAccountService { + transport_operation: decl_field_ref( + module_path: "extdeps.bmc.http", + decl_name: "redfish.Http", + field_name: "SetAccountPassword", + ), + action_shape: decl_field_ref( + module_path: "extdeps.bmc.types", + decl_name: "RedfishSystemAction", + field_name: "SetAccountPassword", + ), + } + AmiMegaRac => RotationRouteUnavailable { + family_note: "AMI MegaRAC serves an SP-X-style /api/ surface and no Redfish service root" as NonEmptyStr, + detail: "no executed user-management operation exists on extdeps.bmc.megarac, whose scope note admits an operation row only as executed; a rotation attempt has answered a password-history refusal, so an endpoint exists, but the request that reached it was never committed" as NonEmptyStr, + } + } +} + +// WHAT RETIRES THE UNAVAILABLE ARM, NAMED AS THE CAPABILITY RATHER THAN AS THE ROW IT WOULD ADD. +// Adding a megarac_op_user_password row is the ARTIFACT; the capability is an EXECUTED user- +// management request against a MegaRAC controller whose request shape and response are committed as +// evidence, which is what that module's own admission rule requires and what neither prior attempt +// produced. Until that exists the arm stays Unavailable. +// +// WHAT THAT DOES NOT YET MEAN, because the first draft said it did: this sentence previously read +// "and the Arrival phase stays unsatisfied for every MegaRAC unit". No unit's Arrival phase reads +// this table today -- BmcCredentialRotationObservation takes `rotation` as a SUPPLIED field -- so +// that was a claim about the terminal architecture in the present tense, the same DESIGN §4b(1) +// inflation corrected in gunbc.machine_intake_bmc_rotation_route. The Arrival consequence arrives +// with the actuator named in rotation_route_consumption_frontier, not with this row. +data megarac_rotation_route_frontier: DissolutionCondition = unbound_dissolution( + description: "dissolves when an executed MegaRAC user-management request against a live controller commits its request shape and response as evidence, so extdeps.bmc.megarac may roster the operation under its as-executed admission rule and this arm can return a route; NOT satisfied by authoring an operation row from AMI documentation, from the srv3/srv4 Redfish shape, or from the uncommitted attempt recorded in gunbc#10630" as NonEmptyStr, +) diff --git a/dag/gunbc/machine_intake/bmc_rotation_route.dag b/dag/gunbc/machine_intake/bmc_rotation_route.dag new file mode 100644 index 00000000000..62fe1e8c05e --- /dev/null +++ b/dag/gunbc/machine_intake/bmc_rotation_route.dag @@ -0,0 +1,117 @@ +module gunbc.machine_intake_bmc_rotation_route + +import std.types { NonEmptyStr, String } +import std.disposition { Disposition, Terminal } +import std.dissolution { DissolutionCondition, unbound_dissolution } +import gunbc.bmc_implementation_dispatch { + BmcRotationRoute, + RotationRouteRedfishAccountService, + RotationRouteUnavailable, +} +import gunbc.machine_intake_bmc_secure { + CredentialRotationApplication, + AccountManagementUnavailable, +} + +// THIS ROW WAS A TYPE ERROR AND IT COMPILED ANYWAY (review 63271). It read +// `Disposition = SingleAuthority`, and SingleAuthority is an arm of ConstructionMechanism, not of +// Disposition -- which has exactly Terminal and Scaffold. Every other `: Disposition =` site in the +// corpus uses one of those two. +// +// THE REVIEW CALLED THE CONSEQUENCE "the module therefore does not compile". IT DOES COMPILE, and +// that is the worse finding rather than a lesser one. This session's own run resolved the closure +// containing this row and failed only on a wrong function name, and gunbc#10952 was green on all +// four required checks with the row present. The reason is a rostered below-floor defect: a wrong +// COPRODUCT value is accepted into a declared field with no diagnostic, while the same check fires +// for primitives and unresolved names. So the ordinary compiler floor -- "values inhabit declared +// types" (DESIGN §4b) -- did not hold, and a plainly wrong row rode four green checks. +// +// The value is Terminal because this module is not scaffolding: it holds one fold that binds a +// route to the application the adjudication refuses on, and there is no construction it dissolves +// into. +data bmc_rotation_route_disposition: Disposition = Terminal { + reason: "The route-to-application binding is the terminal form: gunbc.bmc_implementation_dispatch decides the route by firmware family, and this module maps that route to the machine_intake CredentialRotationApplication the adjudication refuses on. Nothing here is staged pending a different construction." as NonEmptyStr, +} + +// BINDING A ROUTE TO THE APPLICATION THE ADJUDICATION REFUSES ON. The family-keyed dispatch that +// picks the route is NOT here: it is gunbc.bmc_implementation_dispatch rotation_route_for_family, +// alongside the three other family-keyed folds. +// +// THE FIRST VERSION OF THIS MODULE OWNED THAT DISPATCH AND THAT WAS A FORK (review 63250). The +// block comment argued at length that a realization dispatch belongs peripheral to both extdeps +// modules rather than inside either -- which is correct DESIGN §3 reasoning and was the wrong +// conclusion, because the corpus had ALREADY built that peripheral home and the argument never +// mentioned it. gunbc.bmc_implementation_dispatch says of itself that a third implementation +// "refuses to compile here and nowhere else; that is the census", and a fourth `match family` over +// here falsified that sentence the moment it landed -- splitting the third-implementation census +// across two modules with no cross-reference between them. gunbc#9678 already paid for this exact +// fork once, in the other direction. +// +// SO THE DISPATCH MOVED AND THE SPLIT IS AT THE LAYER BOUNDARY, not at a convenience line. What is +// keyed on BmcFirmwareFamily and cites only extdeps.bmc facts went to the dispatch home. What +// remains here is the part that is not family-keyed at all: mapping a route to a machine_intake +// CredentialRotationApplication. Hoisting that would make the peripheral dispatch module import +// machine_intake and invert the layering it exists to keep straight. +// +// THE ROUTE IS KEYED ON AN OBSERVATION, NEVER ON AN EXPECTATION, and that constraint binds the +// caller of the dispatch rather than this fold. The family comes from a +// workflow-layer receipt -- for the held unit, gunbc.machine_intake_mtcollins1_access_observation, +// which carries family AmiMegaRac with committed raw bytes and a digest, and which established +// Redfish absence against a discriminating control: five Redfish paths refused over TLS while the +// same host answered 200 on its web root, so "no Redfish service" is separated from "host +// unreachable". extdeps.ampere.mt_collins_product_brief.bmc holds only an EXPECTATION and forbids +// its own promotion; nothing here may read it, and this module never takes a family from it. + +// THE REFUSAL IS PRODUCED BEFORE ANY CONTROLLER WRITE, WHICH IS THE WHOLE POINT OF PUTTING THE +// ROUTE AHEAD OF THE ATTEMPT. An unavailable route yields AccountManagementUnavailable, which +// gunbc.machine_intake_bmc_secure adjudicates into a typed, located BmcSecure refusal whose owner +// is derived rather than authored. It does not silently skip, and it is not filed as a hardware +// defect: bmc_secure_refusal_owner routes an access state to a PartsHold rather than to the return +// clock, because a firmware we cannot yet drive is not a defect of the unit the seller shipped. +// +// THE SENTENCE ABOVE IS ABOUT THE VALUE THIS FOLD RETURNS, NOT ABOUT ANY UNIT'S ARRIVAL PHASE, and +// the first draft of this block asserted the latter in the PRESENT TENSE (review 63236). It read +// "a unit whose firmware has no rotation transport FAILS ITS ARRIVAL PHASE and is never certified +// as secured". That is not true today and nothing here makes it true: BmcCredentialRotationObservation +// takes `rotation` as a SUPPLIED field, so no unit's arrival phase consults this table. The claim +// described the terminal architecture and wore the tense of the current one, which is DESIGN §4b(1) +// rung inflation -- the executed evidence is this module's witness fold and nothing else, and a +// sentence about arrival phases cited that evidence for a claim it does not support. + +// WHO CONSUMES THIS TABLE, AND BY WHAT ROUTE (DESIGN §3c). The only executing consumer of +// rotation_application_for_route is test.claim.machine_intake_bmc_rotation_route_witness_test, +// which exercises both arms rather than asserting they exist. That is the honest state and it is +// stated rather than left to be discovered, because a declaration whose consumption is described +// in a PR body and absent from the diff is exactly §3c's red. +// +// THE CLAIM IS A NAMED JOIN AND NOT AN ABSENCE, WHICH IS THE FORM THAT SURVIVES. An earlier draft +// opened this block with "Today: nobody in production" -- a live open-world negative with no +// producer that can re-derive it and no consumer whose addition contradicts it, so it would have +// gone silently false the moment an actuator landed. The sentence that replaced it names the +// consumer, and a named join is falsified MECHANICALLY when a caller appears, because its identity +// is reachable through the namespace tree. That is DESIGN §3's cite-the-symbol-rather-than-the- +// position rule applied to a claim about a population, and §3c asks for exactly this: name the +// consumer and the route, never assert the absence of consumers. +// +// THIS IS THE ADMISSIBLE MIDDLE STATE -- consumed by a NAMED consumer landing in a NAMED later +// change -- and the trigger is stated here rather than borrowed from +// gunbc.bmc_implementation_dispatch megarac_rotation_route_frontier, which answers a different +// question: that row dissolves the UNAVAILABLE ARM and says nothing about whether any caller +// exists, so citing it for consumption would be one dissolution condition doing two jobs. (It was +// cited here as "the frontier below" until the arm it guards moved to the dispatch home, which is +// what DESIGN §3 means by naming the symbol rather than the position -- a positional citation is +// invalidated by an edit that never touches either end.) +data rotation_route_consumption_frontier: DissolutionCondition = unbound_dissolution( + description: "dissolves when the effectful rotation actuator named in gunbc.machine_intake_bmc_secure -- the producer of BmcCredentialRotationObservation, gated on the gunbc.bmc_onboarding split -- derives the rotation field by calling rotation_application_for_route on the family read from the controller, rather than receiving it as a supplied argument; at that point a MegaRAC unit's Arrival phase genuinely fails on this table and the present-tense claim becomes authorable. NOT satisfied by this module typechecking, by the witness exercising both arms, or by any caller that passes a route it constructed itself rather than one this table returned" as NonEmptyStr, +) +fn rotation_application_for_route(route: BmcRotationRoute) -> CredentialRotationApplication? { + match route { + RotationRouteRedfishAccountService { transport_operation: _, action_shape: _ } => none + RotationRouteUnavailable { family_note: f, detail: d } => + Present { + value: AccountManagementUnavailable { + detail: join([f as String, ": ", d as String], "") as NonEmptyStr, + }, + } + } +} diff --git a/dag/gunbc/recurring_failure_mode/ad_hoc_hardware_probe_produces_no_receipt.dag b/dag/gunbc/recurring_failure_mode/ad_hoc_hardware_probe_produces_no_receipt.dag new file mode 100644 index 00000000000..6a2e2708e5b --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/ad_hoc_hardware_probe_produces_no_receipt.dag @@ -0,0 +1,26 @@ +module gunbc.recurring_failure_mode.ad_hoc_hardware_probe_produces_no_receipt + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data ad_hoc_hardware_probe_produces_no_receipt: RecurringFailureMode = RecurringFailureMode { + identity: "ad_hoc_hardware_probe_produces_no_receipt" as NonEmptyStr, + + receipts: [ + "**a probe against hardware answers the deciding question and produces no typed observation, so the answer survives only as prose and may not be cited.** INVALID STATE: an attempt is made against a device, the device answers, a human reads the answer, and the run's OUTPUT IS CONSOLE TEXT rather than a receipt. THE DISTINGUISHING FACT IS NOT THAT SOMEBODY FORGOT TO WRITE IT DOWN. Preservation was never available to skip, because the probe's result was never a receipt in the first place -- there is no carrier the run could have committed, so the only artifact that could survive is a recollection, and a recollection is exactly what the corpus refuses as authority. The defect is in the probe's SHAPE, not in the diligence of whoever ran it. ", + + "MEASURED SPECIMEN ONE (2026-08-29): an operator run against a held Mt. Collins unit observed that GET /redfish/v1 returned 404, that the firmware self-reported as `0.32`, and that the service roster was web/kvm/cd-media/hd-media/ssh with no Redfish service. `extdeps.ampere.mt_collins_product_brief.bmc` records that the raw producer output of that run WAS NOT PRESERVED, and therefore types the AMI MegaRAC identification as an EXPECTATION rather than an observation, with its own text forbidding any workflow from reading it as an observation, as a build-grain protocol fact, or as any kind of authority. That module is the corroborating evidence that the corpus already knew and could not act: it names the receipt that would settle the question, and no such receipt is authored. ", + + "MEASURED SPECIMEN TWO (2026-09-06, found 2026-09-10): a credential rotation was attempted against the same controller and the REST path answered `attempt to set previous password` against a policy-conforming secret -- a DECIDED, semantic response proving the endpoint exists, parses the field, and applies a password-history policy to it. gunbc#10630 records the sentence and nothing else. A corpus-wide search for any /api/ user or password request shape returns none: the only rotation body committed anywhere is the Redfish PATCH in `gunbc.tools.bmc_onboard`, whose plans name srv3 and srv4 and which cannot be the call that answered, because a Redfish PATCH against a controller with no Redfish returns 404 rather than a password-policy error. So the request that produced the deciding refusal exists nowhere and cannot be reconstructed from the diff. ", + + "HARM, AND IT IS KEYED ON THE PROBE RATHER THAN ON WHAT HAPPENED AFTERWARDS. The cost is that a fact already obtained must be obtained AGAIN from the device, because the first attempt committed nothing that may be cited. For specimen one that cost was paid and the fact recovered: a second run on 2026-09-05 re-established the firmware identity and the Redfish absence, and `gunbc.machine_intake.mtcollins1_access_observation` preserved it properly -- committed raw bytes, a verified digest, and five Redfish paths refused against a web root that answered 200 as the discriminating control. For specimen two the cost cannot be paid at all today: the request shape is nowhere and the controller answered no ARP from its own /24 on 2026-09-10, so it cannot be re-run until someone physically plugs the unit in. WHETHER RECOVERY IS AVAILABLE IS CONTINGENT -- it needs the hardware to still exist, still be reachable, and someone willing to make the trip -- so a row keyed on `the evidence was destroyed` would be keyed on the consequence and would MISS the recoverable instance entirely. The class is the probe shape, and it fires in both. ", + + "AMENDED 2026-09-10, HOURS AFTER FILING, AND THE REASON IS ITSELF THE MECHANISM. As first written this row claimed the evidence for specimen one was destroyed and that every later lane must re-probe. That overstated the harm: the fact had already been recovered and preserved on 2026-09-05 by the very receipt the extdeps module specified. THE AUTHOR OF THIS ROW REACHED THE WRONG CONCLUSION BY READING `extdeps.ampere.mt_collins_product_brief.bmc` -- which correctly declines to be the authority for an observation outside its layer, and whose sentence that no receipt is authored WAS TRUE WHEN WRITTEN -- as though it were a census of the corpus. It was superseded eight days later by the receipt it named. A module declining authority for something outside its layer is not evidence about what the corpus holds. Recorded here rather than quietly fixed because a failure-mode ledger whose own entries overstate their harm teaches the next reader to discount it, which is the one thing a ledger cannot afford. ", + + "DISTINGUISHING FACTS: this is NOT `production_actuation_unmodeled_beside_a_modeled_probe` -- there is no modeled probe standing beside the ad-hoc one, which is the point; and it is NOT a documentation lapse, because no amount of note-taking discipline produces a citable observation from a run whose output has no carrier. Recognition rule: for any question about an external device that a workflow must later CITE, ask what artifact the probe COMMITS. If the answer is console output, a chat message, or a sentence in a pull request body, the fact is already lost at the moment it is learned, however carefully it is transcribed. ", + + "RUNG FOUND AT: mitigatable, by re-probing the device -- which presupposes the device is reachable and is therefore not always available. CEILING: structurally guaranteed for the class of facts a modeled operation can carry, because a probe whose result is a typed observation by construction cannot produce an uncitable answer; it either yields the carrier or refuses. It is NOT structurally impossible: nothing prevents a human opening a terminal beside the modeled path, and the modeled path cannot forbid that. NEXT-RUNG TRIGGER: an intake operation that performs device identification and returns a typed observation -- Manager payload, service roster, and whether the Redfish service root answers -- committed as an intake receipt keyed to unit, attempt, endpoint and time, such that the identity is a PRODUCT of the trip rather than a premise of it. The receipt must be shaped so that EITHER answer lands cleanly, because a probe designed around the expected firmware is how the unpreserved run became de-facto authority in the first place. ", + ], + + evidence: [], +} diff --git a/dag/gunbc/recurring_failure_mode/declared_type_wall_keyed_on_the_value_being_a_kernel.dag b/dag/gunbc/recurring_failure_mode/declared_type_wall_keyed_on_the_value_being_a_kernel.dag new file mode 100644 index 00000000000..1bc2dcfb2a9 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/declared_type_wall_keyed_on_the_value_being_a_kernel.dag @@ -0,0 +1,30 @@ +module gunbc.recurring_failure_mode.declared_type_wall_keyed_on_the_value_being_a_kernel + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data declared_type_wall_keyed_on_the_value_being_a_kernel: RecurringFailureMode = RecurringFailureMode { + identity: "declared_type_wall_keyed_on_the_value_being_a_kernel" as NonEmptyStr, + + receipts: [ + "**the declared-type inhabitance wall decides on the KIND OF THE OFFENDING VALUE rather than on inhabitance, so it refuses a kernel literal at a declared type and admits a WRONG COPRODUCT ARM at the same position.** DESIGN section 4b puts `values inhabit declared types` in the ordinary compiler floor, so a breach is a below-baseline safety regression and not a rung on the ladder. ", + + "READ FROM THE RELATION, NOT INFERRED FROM ITS NAME. `v1.compiler.infer` `kernel_value_declared_type_mismatch_bounded` short-circuits at its second guard: `if is_kernel_type(name: actual_name) == false || actual_name == \"Unit\" { false }`. A `false` there is `no mismatch`, so an actual value whose authored name is not a kernel type leaves the relation before any formal type is consulted. Every position that consults this relation inherits that exit. ", + + "WHY THIS IS NOT `one more declared-type position needs a member`, which is the natural reading and the wrong one. `test.claim.declared_type_kernel_inhabitance_witness_test` records that the census enumerated fourteen declared-type positions from the grammar -- every `parse_type_expr` call site in `v1.compiler.parse` -- and that seven admitted an `Int` where a coproduct was declared. Those seven were closed. But the guard above sits INSIDE the relation those positions now consult, so closing a position does nothing for a non-kernel wrong value: the record-literal field seam was ALREADY closed for kernels (that witness cites `KHold { subject: 5 }` refusing there) and still admits a wrong coproduct arm. The uncovered half is not a position, it is every position. ", + + "MEASURED SPECIMEN ONE (2026-08-25, `gentle-eagle-360`, controlled fixture): with `AlphaRefusal` and `BetaRefusal` distinct coproducts and `Wrapper = WrapsBeta { cause: BetaRefusal }`, a fn returning `WrapsBeta { cause: c }` for `c: AlphaRefusal` is ACCEPTED, while the same field given an `Int` is refused and given an undeclared constructor is refused. The two refusals are what make the acceptance a measurement rather than an absence of checking. ", + + "MEASURED SPECIMEN TWO (2026-09-10, gunbc#10952, found by review 63271): `data bmc_rotation_route_disposition: Disposition = SingleAuthority`, where `SingleAuthority` is an arm of `ConstructionMechanism` and `Disposition` declares only `Terminal` and `Scaffold`. It rode FOUR GREEN REQUIRED CHECKS. Two independent observations that it compiled rather than being skipped: a `gunbc run` over that closure resolved it and failed only on a wrong function name, and the pull request was green on all four required checks with the row present. ", + + "HARM, AND IT IS THE SECOND SPECIMEN THAT SHOWS THE SHAPE. The review that found it concluded `the module therefore does not compile, and with it the whole witness closure` -- reasonable, and false. So the defect does not merely admit a wrong value: it makes a reader who assumes the floor holds derive a WRONG CONSEQUENCE from a correct observation. The author had four green checks saying the row was fine and a reviewer saying the module was absent, and neither was true. ", + + "DISTINGUISHING FACTS: this is NOT the evidence-overreach family (a receipt supporting more than its instrument established) -- nothing here is a receipt, and the claim is not about coverage. It is NOT `check_subject_shape_cannot_represent_the_state_the_check_detects` -- the relation can represent the state perfectly; it declines to look. The tell is a wall whose guard names a property of the OFFENDING VALUE (`is_kernel_type`) where the property under test is a RELATION between the value and its declared type. ", + + "RUNG FOUND AT: below the floor, which is not a rung. The class is decidable and the authority exists -- `lookup_type_by_name` and the declared-type env are already in hand at the guard that exits -- so this is DESIGN section 5's `wall after grounding` with the grounding already present. CEILING: structurally guaranteed; a wrong-typed literal is authorable in source, so impossibility is not available, but no `Accepted` program need contain one. NEXT-RUNG TRIGGER, NAMED AS A CAPABILITY: an inhabitance judgment that decides from the FORMAL type's declaration for an actual value of ANY kind -- kernel, coproduct arm, record literal, alias -- SUFFICIENT FOR removing `is_kernel_type` from the guard entirely rather than adding a second relation beside it. A second relation keyed on coproducts would be the fork this row exists to prevent. ", + + "NOT CLAIMED HERE: how many of the fourteen positions admit a wrong coproduct. The guard's placement implies all of them, and I did not measure them one at a time. A census across the fourteen positions with a non-kernel wrong value is the honest next measurement, and it is probably worth more than any single new witness member. ", + ], + + evidence: [], +} diff --git a/dag/test/claim/machine_intake/machine_intake_bmc_rotation_route_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_bmc_rotation_route_witness_test.dag new file mode 100644 index 00000000000..d0291509384 --- /dev/null +++ b/dag/test/claim/machine_intake/machine_intake_bmc_rotation_route_witness_test.dag @@ -0,0 +1,97 @@ +module test.claim.machine_intake_bmc_rotation_route_witness_test + +import std.types { Bool, NonEmptyStr } +import std.decl_ref { NamedField, decl_field_eq } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import extdeps.bmc.endpoint { OpenBmc, AmiMegaRac } +import gunbc.machine_intake_bmc_secure { + CredentialRotationApplication, AccountManagementUnavailable, + RotationApplied, RotationNotAttempted, +} +import gunbc.bmc_implementation_dispatch { + BmcRotationRoute, RotationRouteRedfishAccountService, RotationRouteUnavailable, + rotation_route_for_family, +} +import gunbc.machine_intake_bmc_rotation_route { rotation_application_for_route } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE DISCRIMINATING PAIR. Both arms are exercised against the SAME fold, because a witness that +// only ever asks the unavailable arm cannot tell a correct route table from one that refuses +// everything -- and refusing everything would also make a MegaRAC unit fail Arrival, for the wrong +// reason, invisibly. + +test fn megarac_has_no_rotation_route_today() -> Bool { + match rotation_route_for_family(family: AmiMegaRac) { + RotationRouteUnavailable { family_note: _, detail: _ } => true + RotationRouteRedfishAccountService { transport_operation: _, action_shape: _ } => false + } +} + +test fn openbmc_routes_to_redfish_account_service() -> Bool { + match rotation_route_for_family(family: OpenBmc) { + RotationRouteRedfishAccountService { transport_operation: _, action_shape: _ } => true + RotationRouteUnavailable { family_note: _, detail: _ } => false + } +} + +// THE AVAILABLE ARM'S PAYLOAD IS READ, NOT MERELY CARRIED. Review 63263 found the arm holding a +// prose path_note that no consumer touched -- dead data by §4c's own test. Replacing the sentence +// with DeclarationRefs only fixes half of that: a reference nothing reads is still unconsumed. So +// the witness destructures the arm and asserts the operation it names. +// +// AND THE FIRST VERSION OF THIS CHECK DID NOT CHECK THE OPERATION (review 63271). It asserted +// module_path and decl_name on both refs and never touched `field` -- which is the ONLY position +// the operation name lives in. So a table returning NamedField { field_name: "DeleteAccount" } +// would have GREENED, while the comment above it claimed a wrong operation would red. That is a +// check whose subject is narrower than its stated claim, which is the §4b(1) inflation this PR has +// now corrected three times in three different rows: the claim must equal what the evidence +// executes. The field is now compared through std.decl_ref decl_field_eq, so the assertion and the +// sentence describe the same test. +// +// AND THE FIRST FIX RE-INVENTED THE COMPARISON IT NEEDED (review 63521). It hand-rolled a +// decl_field_name fold over DeclField when std.decl_ref already owns decl_field_eq, whose module +// states the rule in its own annotation: a module needing a DeclarationRef imports the constructor +// from the type's own module and never re-mints it. DESIGN §2 -- net concepts must not grow by +// re-invention. The WholeDeclaration arm compounded it by returning "" , a fabricated plausible +// value where the canonical surface refuses to conflate the two shapes (§5); it compared false and +// stayed fail-closed here, which was luck of the call site rather than a property of the helper. + +test fn the_openbmc_route_names_the_set_account_password_operation() -> Bool { + match rotation_route_for_family(family: OpenBmc) { + RotationRouteRedfishAccountService { transport_operation: op, action_shape: act } => + op.module_path == "extdeps.bmc.http" + && op.decl_name == "redfish.Http" + && decl_field_eq(a: op.field, b: NamedField { field_name: "SetAccountPassword" as NonEmptyStr }) + && act.module_path == "extdeps.bmc.types" + && act.decl_name == "RedfishSystemAction" + && decl_field_eq(a: act.field, b: NamedField { field_name: "SetAccountPassword" as NonEmptyStr }) + RotationRouteUnavailable { family_note: _, detail: _ } => false + } +} + +// THE ARM THAT MATTERS FOR SAFETY: an unavailable route must yield the application arm the +// adjudication refuses on, so a MegaRAC unit cannot reach a controller write at all. A route table +// that returned `none` here would let the caller proceed with RotationNotAttempted and adjudicate +// into a DIFFERENT refusal, which would read as "nobody tried" rather than "there is no way to try". +test fn an_unavailable_route_yields_account_management_unavailable() -> Bool { + match rotation_application_for_route(route: rotation_route_for_family(family: AmiMegaRac)) { + Present { value: app } => + match app { + AccountManagementUnavailable { detail: _ } => true + RotationApplied { reference: _, applied_at: _, evidence: _ } => false + RotationNotAttempted => false + } + Absent => false + } +} + +// AND THE POSITIVE CONTROL ON THAT SAME FOLD: a route that EXISTS must not manufacture a refusal. +// Without this, an implementation that returned AccountManagementUnavailable unconditionally would +// pass the test above and silently block the OpenBMC fleet too. +test fn an_available_route_yields_no_refusal_application() -> Bool { + match rotation_application_for_route(route: rotation_route_for_family(family: OpenBmc)) { + Absent => true + Present { value: _ } => false + } +}