Managed-host cut O1c-3b: BmcSecure gated through the convergence fold

dag/gunbc/auth/authorization_pattern_selection.dag

@@ -111,14 +111,13 @@ type BillingConsequence
 // (gunbc.auth.privileged_effect_census rulings_without_a_rostered_interlock), and the site's
 // realization must take that hold before any write.
 //
-// THREE INTERLOCK STATES, NOT AN OPTIONAL HOLD. InterlockPending is a hold not yet named: it must
+// TWO INTERLOCK STATES, NOT AN OPTIONAL HOLD. InterlockPending is a hold not yet named: it must
 // refuse, never discharge (a bindable irreversible effect under a pending ruling still owes a
-// witness). UnconditionalStanding is an intentional no-hold discharge, with its reason. InterlockedBy
-// is a named hold the census must roster against the site. Only UnconditionalStanding and
-// InterlockedBy discharge the irreversibility ground.
+// witness). InterlockedBy is a named hold the census must roster against the site; only that arm
+// discharges the irreversibility ground. A grant arm that writes BMC credentials must be InterlockedBy
+// the grounded Apply admission (admit_rotation_apply), never pending.
 type StandingRulingInterlock
   = InterlockPending { obligation: NonEmptyStr }
-  | UnconditionalStanding { reason: NonEmptyStr }
   | InterlockedBy { hold: DeclarationRef }
 
 type StandingDestructiveAuthorization {
@@ -130,7 +129,6 @@ type StandingDestructiveAuthorization {
 fn standing_ruling_discharges_irreversibility(r: StandingDestructiveAuthorization) -> Bool {
   match r.interlock {
     InterlockPending { obligation: _ } => false
-    UnconditionalStanding { reason: _ } => true
     InterlockedBy { hold: _ } => true
   }
 }
@@ -571,7 +569,6 @@ fn minted_reach_text(m: MintedCredentialReach) -> String {
 fn standing_ruling_interlock_label(r: StandingDestructiveAuthorization) -> String {
   match r.interlock {
     InterlockPending { obligation: o } => join(["InterlockPending: ", o as String], "")
-    UnconditionalStanding { reason: s } => join(["UnconditionalStanding: ", s as String], "")
     InterlockedBy { hold: i } => declaration_ref_display_key(ref: i)
   }
 }

dag/gunbc/auth/privileged_effect_census.dag

@@ -1,6 +1,6 @@
 module gunbc.auth.privileged_effect_census
 
-import gunbc.auth.standing_operator_grant { group_a_dev_standing_grant }
+import gunbc.auth.standing_operator_grant { group_a_dev_standing_grant, mtjade1_live_standing_grant }
 import std.types { Bool, List, NonEmptyStr, String }
 import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_in_list, declaration_ref_eq }
 import std.dissolution {
@@ -24,7 +24,7 @@ import gunbc.auth.authorization_pattern_selection {
   ReversibleByReapply, IrreversibleEffect,
   BillsExternally, NoBillingConsequence,
   WitnessDischarge, NoWitnessDischarge, StandingRulingUnderInterlock, StandingDestructiveAuthorization,
-  InterlockPending, UnconditionalStanding, InterlockedBy,
+  InterlockPending, InterlockedBy, StandingRulingInterlock,
   AuthorizationPattern, FederatedScopedGrant, OperatorApprovedCapability, HumanOnlyStep,
   OperatorOwnSession, PastedOperatorToken,
   AuthorizationPatternSelection, PatternSelected, ManualStepRequired, NoAdmissiblePattern,
@@ -331,14 +331,16 @@ fn route_qualification_channel_access_effect() -> PrivilegedEffect {
   }
 }
 
-// BMCSECURE ACCOUNT ROTATION (cut O1b). The Apply arm of the state-shaped BmcSecure: set the managed
-// account to a stored and exact-fetched generation and retire the published account to a break-glass
-// generation, each write over a route admitted by admit_rotation_apply. IRREVERSIBLE, AND SAID SO: the
-// value each write replaces is gone, and the published factory value is not restorable by a reapply
-// (artifacts/bmc/mtcollins1-user2-retire-2026-09-13.txt). One controller's accounts, so its reach is one
-// resource. No dispatched run carries it: in this cut it is modeled, with a dry realization only, and
-// the plan mint takes an operator-approved capability (gunbc.auth.approval_broker Redemption) per write,
-// bound to the exact controller, build and request.
+// BMCSECURE ACCOUNT ROTATION (cut O1b, discharge O1c-3). The Apply arm of the state-shaped BmcSecure:
+// set the managed account to a stored and exact-fetched generation and retire the published account
+// to a break-glass generation, each write over a route admitted by admit_rotation_apply.
+// IRREVERSIBLE, AND SAID SO: the value each write replaces is gone, and the published factory value is
+// not restorable by a reapply (artifacts/bmc/mtcollins1-user2-retire-2026-09-13.txt). One controller's
+// accounts, so its reach is one resource. No dispatched run carries it: modeled with a dry realization
+// only. Irreversibility is discharged by the mtjade1 live-ops standing ruling under admit_rotation_apply
+// (gunbc.auth.standing_operator_grant mtjade1_live_standing_grant); a write still needs a grounded
+// route. Operator-approved capability remains the selected pattern while the workload identity is
+// unbindable, and is the fallback when the grant does not cover the host.
 fn bmc_secure_account_rotation_effect() -> PrivilegedEffect {
   PrivilegedEffect {
     subject: "rotate a BMC's managed account to a stored generation and retire its published account, over admitted routes on one controller at one firmware build" as NonEmptyStr,
@@ -348,7 +350,7 @@ fn bmc_secure_account_rotation_effect() -> PrivilegedEffect {
     workload_identity: WorkloadIdentityUnbindable { cause: "no dispatched run carries the BmcSecure account rotation; in cut O1b it is modeled with a dry realization only" as NonEmptyStr },
     minted_reach: MintsResourceScopedCredential,
     billing: NoBillingConsequence,
-    witness_discharge: NoWitnessDischarge,
+    witness_discharge: StandingRulingUnderInterlock { ruling: mtjade1_live_standing_grant.ruling },
   }
 }
 
@@ -361,12 +363,19 @@ fn bmc_secure_account_rotation_effect() -> PrivilegedEffect {
 // active hold.
 type PrivilegedEffectInterlock {
   site: DeclarationRef
-  hold: DeclarationRef
+  hold: DeclarationRef?
   refusal: DeclarationRef
   premise: NonEmptyStr
   hold_owning_roots: List<InterlockRoot>
 }
 
+fn privileged_effect_interlock_hold(interlock: StandingRulingInterlock) -> DeclarationRef? {
+  match interlock {
+    InterlockedBy { hold: i } => Present { value: i }
+    InterlockPending { obligation: _ } => none
+  }
+}
+
 // EVERY PRODUCTION ROOT THAT REACHES A GATED WRITE ON THE UNIT, and the live acquire it owns. The set
 // is closed by the compiler rather than by this list: the BMC write wrappers take a sole_constructor
 // UnitHoldProof, and the generic operations beneath them are admit_callers-sealed to the callers named
@@ -409,38 +418,48 @@ data mtcollins1_hold_owning_roots: List<InterlockRoot> = [
 data privileged_effect_interlocks: List<PrivilegedEffectInterlock> = [
   PrivilegedEffectInterlock {
     site: site(module_path: "gunbc.spark.pair_serving_d0_door", decl_name: "d0_standing_grant_for"),
-    hold: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant"),
+    hold: privileged_effect_interlock_hold(interlock: group_a_dev_standing_grant.ruling.interlock),
     refusal: site(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_decide_release"),
     premise: "the release runs only under D0's durable claim of the consent slot and its pending state, and refuses (D0HostNotQuiescent) unless a fresh reading taken at filing time finds every host quiescent; an unanswering host refuses as unobserved" as NonEmptyStr,
     hold_owning_roots: [] as List<InterlockRoot>,
   },
   PrivilegedEffectInterlock {
     site: site(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_wet"),
-    hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"),
+    hold: privileged_effect_interlock_hold(interlock: mtcollins1_operator_ruling.interlock),
     refusal: site(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire"),
     premise: "the boot takes the unit's one durable exclusive hold before any BMC write and refuses FileHoldOccupied naming the holder" as NonEmptyStr,
     hold_owning_roots: mtcollins1_hold_owning_roots,
   },
   PrivilegedEffectInterlock {
     site: site(module_path: "gunbc.host_reset_return_run", decl_name: "host_reset_return_wet"),
-    hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"),
+    hold: privileged_effect_interlock_hold(interlock: mtcollins1_operator_ruling.interlock),
     refusal: site(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire"),
     premise: "host reset-return takes the same unit hold before it sets the boot device or power-cycles the unit" as NonEmptyStr,
     hold_owning_roots: mtcollins1_hold_owning_roots,
   },
+  PrivilegedEffectInterlock {
+    site: site(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "plan_bmc_account_action"),
+    hold: privileged_effect_interlock_hold(interlock: mtjade1_live_standing_grant.ruling.interlock),
+    refusal: site(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "grant_discharges_bmc_secure_account_write"),
+    premise: "BmcSecure Apply discharges the mtjade1 standing ruling only when admit_rotation_apply is rostered against this site; InterlockPending never discharges, and a named hold that is not this site's rostered interlock does not discharge" as NonEmptyStr,
+    hold_owning_roots: [] as List<InterlockRoot>,
+  },
 ]
 
 // A STANDING RULING IS HONORED ONLY BESIDE ITS INTERLOCK. InterlockPending never discharges and is
-// always a defect. UnconditionalStanding discharges without a rostered hold. InterlockedBy discharges
-// only when that hold is rostered against the same site.
+// always a defect. InterlockedBy discharges only when that hold is rostered against the same site.
 fn ruling_interlock_is_rostered(site_ref: DeclarationRef, interlock: DeclarationRef) -> Bool {
-  any(privileged_effect_interlocks, i => declaration_ref_eq(a: i.site, b: site_ref) && declaration_ref_eq(a: i.hold, b: interlock))
+  any(privileged_effect_interlocks, i =>
+    declaration_ref_eq(a: i.site, b: site_ref)
+      && match i.hold {
+        Present { value: h } => declaration_ref_eq(a: h, b: interlock)
+        Absent => false
+      })
 }
 
 fn ruling_discharge_interlock_defect(site_ref: DeclarationRef, ruling: StandingDestructiveAuthorization) -> DeclarationRef? {
   match ruling.interlock {
     InterlockPending { obligation: _ } => Present { value: site_ref }
-    UnconditionalStanding { reason: _ } => none
     InterlockedBy { hold: i } =>
       if ruling_interlock_is_rostered(site_ref: site_ref, interlock: i) { none } else { Present { value: site_ref } }
   }

dag/gunbc/auth/standing_operator_grant.dag

@@ -1,13 +1,14 @@
 module gunbc.auth.standing_operator_grant
 
-import std.types { String, Bool, List, NonEmptyStr, Timestamp }
+import v2.std.algebra { length }
 import product.host_identity { HostIdentity, host_identity_eq }
+import std.optional { Present }
 import std.list { list_member }
 import std.scoped_authorization { OperatorGrant, ScopedAuthorization, AuthorizationGranted, AuthorizationRequest, Unclaimed }
 import std.decl_ref { DeclarationRef, decl_ref }
 import gunbc.fleet_host_identity { operator_host_srv5, operator_host_srv6, operator_host_srv7, operator_host_srv8, operator_host_mtjade1 }
 import gunbc.spark.fabric_switch_observed { FabricGroup, FabricGroupA, fabric_group_wire }
-import gunbc.auth.authorization_pattern_selection { StandingDestructiveAuthorization, InterlockedBy, InterlockPending }
+import gunbc.auth.authorization_pattern_selection { StandingDestructiveAuthorization, InterlockedBy }
 
 // ── A STANDING OPERATOR GRANT, COMMITTED AS A RULING ───────────────────────────────────────────
 //
@@ -35,25 +36,23 @@ import gunbc.auth.authorization_pattern_selection { StandingDestructiveAuthoriza
 // nothing reads would pre-authorize what no wall asks about.
 //
 // MTJADE1 LIVE OPS (operator ruling 2026-10-06, msg_7402f8df-7917-4b24-bb86-c4e7d51991f7) names BMC
-// reads/writes, boots, and firmware qualification. Those classes are a declared frontier: the first
-// consuming gate lands in gunbc#13497 (stern-ibex-771 route A -- bindable fleet-converge principal,
-// effect arm in the same closure as the secret/cell fetch) and must call standing_grant_covers for a
-// named arm -- O1c-3's BmcSecure authorization discharge, managed_host_boot admission/authorization,
-// or MegaRAC per-build operation evidence / admit_megarac_host_at_current_build. The prior-life archive
-// is a BMC read (it writes only our store) and has no grant arm. The mtjade1 grant's effects list is
-// empty until that change lands the arm. The interlock is InterlockPending until a consuming gate names
-// a hold: that state refuses to discharge irreversibility, so a bindable boot under this row does not
-// select federation.
+// reads/writes, boots, and firmware qualification. O1c-3's BmcSecure Apply discharge is the first
+// consuming gate: StandingBmcSecureAccountWrite, InterlockedBy admit_rotation_apply (the grounded
+// route standing; that admission already runs administrator_retention_refusal, the pre-write lockout).
+// managed_host_boot and MegaRAC current-build admission remain frontiers. The prior-life archive is a
+// BMC read (it writes only our store) and has no grant arm.
 type StandingGrantEffect
   = StandingD0ReleaseToFleet
   | StandingArmLaunch
   | StandingHostEffectRecover
+  | StandingBmcSecureAccountWrite
 
 fn standing_grant_effect_wire(e: StandingGrantEffect) -> NonEmptyStr {
   match e {
     StandingD0ReleaseToFleet => "d0-release-to-fleet" as NonEmptyStr
     StandingArmLaunch => "arm-launch" as NonEmptyStr
     StandingHostEffectRecover => "host-effect-recover" as NonEmptyStr
+    StandingBmcSecureAccountWrite => "bmc-secure-account-write" as NonEmptyStr
   }
 }
 
@@ -119,19 +118,18 @@ data group_a_dev_standing_grant: StandingOperatorGrant = StandingOperatorGrant {
 // on mtjade1 are authorized whenever, indefinitely. That covers BMC reads and writes (history archive,
 // login/credential change), boots, and firmware qualification on Mt. Jade, with no per-run approval
 // needed. Scope is mtjade1 only; mtcollins1 wet steps still need their own go-ahead." Quote unchanged.
-// Effects list empty: no consuming gate has landed (O1c-3 BmcSecure discharge, managed_host_boot
-// authorization, MegaRAC current-build admission). The prior-life archive is not an arm.
+// StandingBmcSecureAccountWrite lands with O1c-3's BmcSecure Apply reader. The prior-life archive is not an arm.
 data mtjade1_live_standing_grant: StandingOperatorGrant = StandingOperatorGrant {
   identity: "mtjade1-live-standing-grant-2026-10-06" as NonEmptyStr,
   principal: "operator" as NonEmptyStr,
   ruled_at: "2026-10-06T00:00:00Z",
   ruling: StandingDestructiveAuthorization {
     ruling_text: "Operator ruling 2026-10-06, given directly in eager-gull-22's session and relayed by dashboard message msg_7402f8df-7917-4b24-bb86-c4e7d51991f7: 'live operations on mtjade1 are authorized whenever, indefinitely. That covers BMC reads and writes (history archive, login/credential change), boots, and firmware qualification on Mt. Jade, with no per-run approval needed. Scope is mtjade1 only; mtcollins1 wet steps still need their own go-ahead.'" as NonEmptyStr,
     effect_subject: "mtjade1 live operations: BMC credential/login writes, boots, and MegaRAC firmware qualification -- effect rows only as consuming gates land" as NonEmptyStr,
-    interlock: InterlockPending { obligation: "consuming gates (O1c-3 BmcSecure authorization discharge, managed_host_boot admission, MegaRAC current-build admission) have not named a hold" as NonEmptyStr },
+    interlock: InterlockedBy { hold: decl_ref(module_path: "gunbc.machine_intake_bmc_rotation_route", decl_name: "admit_rotation_apply") },
   },
   scope: StandingGrantHost { host: operator_host_mtjade1 },
-  effects: [] as List<StandingGrantEffect>,
+  effects: [StandingBmcSecureAccountWrite],
 }
 
 // COVERAGE IS AN IDENTITY JOIN: the scope is the grant's, the effect is one of its effects, and EVERY host