BmcSecure gets a route table, and the MegaRAC arm refuses before any controller write

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,
+)

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,
+        },
+      }
+  }
+}