diff --git a/dag/gunbc/auth/authorization_pattern_selection.dag b/dag/gunbc/auth/authorization_pattern_selection.dag index 250c03a864c..442f5b58df5 100644 --- a/dag/gunbc/auth/authorization_pattern_selection.dag +++ b/dag/gunbc/auth/authorization_pattern_selection.dag @@ -110,10 +110,29 @@ type BillingConsequence // statically that the interlock is rostered against the site // (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 +// 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. +type StandingRulingInterlock + = InterlockPending { obligation: NonEmptyStr } + | UnconditionalStanding { reason: NonEmptyStr } + | InterlockedBy { hold: DeclarationRef } + type StandingDestructiveAuthorization { ruling_text: NonEmptyStr effect_subject: NonEmptyStr - interlock: DeclarationRef + interlock: StandingRulingInterlock +} + +fn standing_ruling_discharges_irreversibility(r: StandingDestructiveAuthorization) -> Bool { + match r.interlock { + InterlockPending { obligation: _ } => false + UnconditionalStanding { reason: _ } => true + InterlockedBy { hold: _ } => true + } } type WitnessDischarge @@ -143,7 +162,7 @@ fn witness_required(e: PrivilegedEffect) -> Bool { IrreversibleEffect { what_is_lost: _ } => match e.witness_discharge { NoWitnessDischarge => true - StandingRulingUnderInterlock { ruling: _ } => false + StandingRulingUnderInterlock { ruling: r } => !standing_ruling_discharges_irreversibility(r: r) } ReversibleByReapply => false } @@ -549,11 +568,19 @@ fn minted_reach_text(m: MintedCredentialReach) -> String { // THE RULING IS QUOTED WITH ITS AUTHOR, DATE AND INTERLOCK, so a receipt minted under a standing // authorization is a different decision scope from one minted without it. +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) + } +} + fn witness_discharge_text(d: WitnessDischarge) -> String { match d { NoWitnessDischarge => "NoWitnessDischarge" StandingRulingUnderInterlock { ruling: r } => - join(["StandingRulingUnderInterlock: under ", declaration_ref_display_key(ref: r.interlock), "; ruling ", r.ruling_text as String], "") + join(["StandingRulingUnderInterlock: under ", standing_ruling_interlock_label(r: r), "; ruling ", r.ruling_text as String], "") } } diff --git a/dag/gunbc/auth/privileged_effect_census.dag b/dag/gunbc/auth/privileged_effect_census.dag index 6b741383ffb..630357bfc6c 100644 --- a/dag/gunbc/auth/privileged_effect_census.dag +++ b/dag/gunbc/auth/privileged_effect_census.dag @@ -24,6 +24,7 @@ import gunbc.auth.authorization_pattern_selection { ReversibleByReapply, IrreversibleEffect, BillsExternally, NoBillingConsequence, WitnessDischarge, NoWitnessDischarge, StandingRulingUnderInterlock, StandingDestructiveAuthorization, + InterlockPending, UnconditionalStanding, InterlockedBy, AuthorizationPattern, FederatedScopedGrant, OperatorApprovedCapability, HumanOnlyStep, OperatorOwnSession, PastedOperatorToken, AuthorizationPatternSelection, PatternSelected, ManualStepRequired, NoAdmissiblePattern, @@ -245,7 +246,7 @@ fn accessor_grant(subject: NonEmptyStr) -> PrivilegedEffect { data mtcollins1_operator_ruling: StandingDestructiveAuthorization = StandingDestructiveAuthorization { ruling_text: "the fleet-converge mtcollins1_boot and host_reset_return modes, dispatched from gunb-ai/gunbc main under their workload identity, may attach media to, set the boot device of, power-cycle and capture the console of Mt. Collins unit 1 on every dispatch with no per-run or standing approval, provided each run first takes the unit's maintenance hold. Operator chat rulings 2026-09-23 ('we technically don't even need my approval - would you mind getting rid of that step or making WIF just trust this workflow') and 2026-09-25 ('no I don't want that - can you just remove that check asap')" as NonEmptyStr, effect_subject: "mtcollins1 destructive controller effect: BMC virtual-media attach, one-shot boot-device set, power cycle and SOL capture" as NonEmptyStr, - interlock: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"), + interlock: InterlockedBy { hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof") }, } data mtcollins1_operator_ruling_roots: List = [ @@ -408,39 +409,52 @@ data mtcollins1_hold_owning_roots: List = [ data privileged_effect_interlocks: List = [ PrivilegedEffectInterlock { site: site(module_path: "gunbc.spark.pair_serving_d0_door", decl_name: "d0_standing_grant_for"), - hold: group_a_dev_standing_grant.ruling.interlock, + hold: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant"), 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, }, PrivilegedEffectInterlock { site: site(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_wet"), - hold: mtcollins1_operator_ruling.interlock, + hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"), 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: mtcollins1_operator_ruling.interlock, + hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"), 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, }, ] -// A STANDING RULING IS HONORED ONLY BESIDE ITS INTERLOCK: for every census row whose effect carries -// one, the ruling's interlock must be the hold of an interlock rostered against that same site. +// 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. 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)) } +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 } } + } +} + fn rulings_without_a_rostered_interlock() -> List { flat_map(privileged_effect_census, row => match row.effect.witness_discharge { NoWitnessDischarge => [] StandingRulingUnderInterlock { ruling: r } => - if ruling_interlock_is_rostered(site_ref: row.site, interlock: r.interlock) { [] } else { [row.site] } + match ruling_discharge_interlock_defect(site_ref: row.site, ruling: r) { + Absent => [] + Present { value: s } => [s] + } }) } diff --git a/dag/gunbc/auth/standing_operator_grant.dag b/dag/gunbc/auth/standing_operator_grant.dag index fc6c0b7ba4c..0cca4dbb43f 100644 --- a/dag/gunbc/auth/standing_operator_grant.dag +++ b/dag/gunbc/auth/standing_operator_grant.dag @@ -5,13 +5,13 @@ import product.host_identity { HostIdentity, host_identity_eq } 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 } +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 } +import gunbc.auth.authorization_pattern_selection { StandingDestructiveAuthorization, InterlockedBy, InterlockPending } // ── A STANDING OPERATOR GRANT, COMMITTED AS A RULING ─────────────────────────────────────────── // -// WHAT THIS IS. An operator ruling that authorizes a bounded set of effects over a bounded set of hosts +// WHAT THIS IS. An operator ruling that authorizes a bounded set of effects over a bounded scope // from the moment it was given, with no per-effect approval -- carried as a reviewable row in the source, // never relayed at run time and never written into the authority log by hand. It is the same standing // the selection already models for the Mt. Collins controller (gunbc.auth.authorization_pattern_selection @@ -19,22 +19,31 @@ import gunbc.auth.authorization_pattern_selection { StandingDestructiveAuthoriza // effect it covers and the interlock the effect is conditional on. That ruling discharges the // per-instance witness obligation, which is exactly why no new pattern arm is needed here -- with the // witness discharged, the selection's own fold prefers the run's scoped identity over a per-effect tap, -// and this row adds only what that type does not carry: the group, the exact hosts and the closed set of -// effects, so a consumer can ask whether ONE effect on ONE host is inside the ruling. +// and this row adds only what that type does not carry: the scope (a fabric group, or one named host), +// the exact hosts and the closed set of effects, so a consumer can ask whether ONE effect on ONE host +// is inside the ruling. Scope is not FabricGroup: an mtjade1 grant has no fabric group. // // WHAT IT IS NOT. It is not a capability that skips any wall but the approval: the consumer still takes // its claim, its fresh readings and its readback. And it does not widen: a group, a host or an effect // outside the row is not covered, and the consumer falls back to the per-effect approval it always had. // // THE EFFECTS ARE ONLY THOSE A GATE CONSUMES (DESIGN §3c, review 74624). D0's release is consumed here -// (gunbc.spark.pair_serving_d0_door d0_gate). ArmLaunch is a declared frontier: its consumer is the -// launch gate's released-group arm, gunbc.spark.group_arm_launch group_arm_released_launch_causes, which -// lands in gunbc#13040 (stacked on this change). HostEffectRecover is a declared frontier with the same -// consumer PR: the dispatched recovery of a dead lane's host-effect claim on a Group A host -// (gunbc.spark.host_commitment's release, which settles only after a fresh quiescence read of the host -- -// never on a claim's term alone; ruling of valiant-crab-775, 2026-10-03). The image, checkpoint and teardown -// effects the ruling also covers are NOT rows: nothing gates them on a grant (they are fenced by the -// per-host claim), and an effect row nothing reads would pre-authorize what no wall asks about. +// (gunbc.spark.pair_serving_d0_door d0_gate). ArmLaunch is consumed by gunbc.spark.group_arm_launch +// group_arm_released_launch_causes. HostEffectRecover is consumed by gunbc.spark.standing_host_effect_recover +// recover_covering_grant. The image, checkpoint and teardown effects the Group A ruling also covers are +// NOT rows: nothing gates them on a grant (they are fenced by the per-host claim), and an effect row +// 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. type StandingGrantEffect = StandingD0ReleaseToFleet | StandingArmLaunch @@ -48,16 +57,44 @@ fn standing_grant_effect_wire(e: StandingGrantEffect) -> NonEmptyStr { } } +// A GRANT BOUNDS EITHER A FABRIC GROUP AND ITS HOSTS, OR ONE NAMED HOST. Group A is the first; +// mtjade1 is the second. Hosts live in the arm: a host-scoped grant does not restate its host in a +// parallel list. Coverage still requires every requested host to be in the grant's derived hosts. +type StandingGrantScope + = StandingGrantFabricGroup { group: FabricGroup, hosts: List } + | StandingGrantHost { host: HostIdentity } + type StandingOperatorGrant { identity: NonEmptyStr principal: NonEmptyStr ruled_at: Timestamp ruling: StandingDestructiveAuthorization - group: FabricGroup - hosts: List + scope: StandingGrantScope effects: List } +fn standing_grant_hosts(g: StandingOperatorGrant) -> List { + match g.scope { + StandingGrantFabricGroup { group: _, hosts: hs } => hs + StandingGrantHost { host: h } => [h] + } +} + +fn standing_grant_scope_matches(g: StandingOperatorGrant, scope: StandingGrantScope) -> Bool { + match g.scope { + StandingGrantFabricGroup { group: granted, hosts: _ } => + match scope { + StandingGrantFabricGroup { group: asked, hosts: _ } => (fabric_group_wire(g: granted) as String) == (fabric_group_wire(g: asked) as String) + StandingGrantHost { host: _ } => false + } + StandingGrantHost { host: granted } => + match scope { + StandingGrantHost { host: asked } => host_identity_eq(a: granted, b: asked) + StandingGrantFabricGroup { group: _, hosts: _ } => false + } + } +} + // THE GROUP A DEVELOPMENT GRANT. The words are the operator's, given directly in the parent session on // 2026-10-03 and relayed by valiant-crab-775 (dashboard message msg_2940687d): "you have my permission to // use group A however you want from now on." The operator also ruled that the approval broker and app @@ -71,24 +108,48 @@ data group_a_dev_standing_grant: StandingOperatorGrant = StandingOperatorGrant { ruling: StandingDestructiveAuthorization { ruling_text: "Operator ruling 2026-10-03, given directly in valiant-crab-775's session and relayed by dashboard message msg_2940687d: 'you have my permission to use group A however you want from now on.' The approval broker and app are a separate lane and will not be set up now. Scope as relayed: FabricGroupA hosts srv5-srv8; the D0 release-to-fleet plus the GLM staircase's host effects (image produce and distribute, checkpoint materialize, arm launch and teardown), and, per valiant-crab-775 on 2026-10-03, recovering a dead lane's host-effect claim on a Group A host after a fresh quiescence read. Group B is outside it." as NonEmptyStr, effect_subject: "Group A development effects: the D0 release-to-fleet of Group A's pair-serving authority and the GLM-5.3-Flash staircase's host effects on srv5-srv8" as NonEmptyStr, - interlock: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant"), + interlock: InterlockedBy { hold: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant") }, }, - group: FabricGroupA, - hosts: [operator_host_srv5, operator_host_srv6, operator_host_srv7, operator_host_srv8], + scope: StandingGrantFabricGroup { group: FabricGroupA, hosts: [operator_host_srv5, operator_host_srv6, operator_host_srv7, operator_host_srv8] }, effects: [StandingD0ReleaseToFleet, StandingArmLaunch, StandingHostEffectRecover], } -// COVERAGE IS AN IDENTITY JOIN: the group is the grant's, the effect is one of its effects, and EVERY host +// THE MTJADE1 LIVE-OPS GRANT. The words are the operator's, given directly in eager-gull-22's session +// on 2026-10-06 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." 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. +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 }, + }, + scope: StandingGrantHost { host: operator_host_mtjade1 }, + effects: [] as List, +} + +// COVERAGE IS AN IDENTITY JOIN: the scope is the grant's, the effect is one of its effects, and EVERY host // the effect touches is one of its hosts (a host outside the roster is outside the ruling, however few). // An empty host list touches nothing a ruling could cover, so it is not covered. // SUBSET, NOT SET EQUALITY: std.list list_cover is equality in both directions, and using it here made an // effect on ONE granted host (a host-effect recovery on srv7) uncovered while all four passed -- found by // the recovery's witness (2026-10-03). Every effect host must be granted; the effect need not touch all. -fn standing_grant_covers(g: StandingOperatorGrant, group: FabricGroup, effect: StandingGrantEffect, hosts: List) -> Bool { - (fabric_group_wire(g: g.group) as String) == (fabric_group_wire(g: group) as String) +fn standing_grant_covers(g: StandingOperatorGrant, scope: StandingGrantScope, effect: StandingGrantEffect) -> Bool { + standing_grant_scope_matches(g: g, scope: scope) && any(g.effects, e => (standing_grant_effect_wire(e: e) as String) == (standing_grant_effect_wire(e: effect) as String)) - && length(hosts) != 0 - && all(hosts, h => list_member(xs: g.hosts, x: h, eq: fn(a, b) { host_identity_eq(a: a, b: b) })) + && match scope { + StandingGrantFabricGroup { group: _, hosts: requested } => + length(requested) != 0 + && all(requested, h => list_member(xs: standing_grant_hosts(g: g), x: h, eq: fn(a, b) { host_identity_eq(a: a, b: b) })) + StandingGrantHost { host: h } => + list_member(xs: standing_grant_hosts(g: g), x: h, eq: fn(a, b) { host_identity_eq(a: a, b: b) }) + } } // THE GRANT A CONSUMER ACTS UNDER, MINTED OVER THE EXACT REQUEST: its scopes, subject and intent are the diff --git a/dag/gunbc/fleet/fleet_host_identity.dag b/dag/gunbc/fleet/fleet_host_identity.dag index 53c5d583f94..42deced7e0d 100644 --- a/dag/gunbc/fleet/fleet_host_identity.dag +++ b/dag/gunbc/fleet/fleet_host_identity.dag @@ -32,6 +32,14 @@ data operator_host_srv4: HostIdentity = "srv4" // So this row names the unit and licenses nothing. data operator_host_mtcollins1: HostIdentity = "mtcollins1" +// MTJADE1 (2026-10-06). The operator's Foxconn Ampere Mt. Jade unit. Named here for the same reason +// mtcollins1 is: this module is the HostIdentity authority, and a second home would be a §3 fork. +// NAMING IS NOT ENROLLMENT. This unit is not an executor fleet host and is not a row of +// gunbc.managed_host managed_hosts (that roster is the BmcSecured join; stuffing a grant subject in +// there would enroll a unit). The standing live-ops grant (gunbc.auth.standing_operator_grant +// mtjade1_live_standing_grant) binds this identity as its host scope. +data operator_host_mtjade1: HostIdentity = "mtjade1" + // SPARK-LANE-A (2026-08-06). srv5/srv6 are the operator's HostIdentity slots for the two ordered NVIDIA DGX Spark units (gunbc.spark.dgx_procurement). They live here because HostIdentity naming is this module's single authority — SPARK-0 minted `srv5_reserved`/`srv6_reserved` privately inside the procurement module only because this file was mid-refactor and out of scope, which was a §3 fork of one concept (a host's fleet identity) across two homes; those private rows are deleted and the procurement module imports these. NAMING AN IDENTITY IS NOT ENROLLMENT, and that distinction is carried structurally rather than by this prose: enrollment is membership in `fleet_intent_network.endpoints` (and in gunbc.fleet_intent's ComputeHost list), and srv5/srv6 appear in neither — HALF-SUPERSEDED 2026-09-02, see the DCH-0 clause at the end of this note: the `endpoints` half is now performed and the ComputeHost half is not. Updated 2026-08-07 for the arrived state: both units are now live on the LAN and the operator has authored two static reservations for them (spark-a3ee 192.168.1.222 and spark-3bd5 192.168.1.223, both MACs ARP-confirmed — SUPERSEDED, see the SPARK-WIFI-0 clause at the end of this note), so the missing fact is no longer the addresses. CORRECTED 2026-08-23: THE SLOT ASSIGNMENT IS ALSO NO LONGER MISSING, AND THIS NOTE WENT ON ASSERTING THAT IT WAS. It read that the operator "supplied the router table but never stated the assignment", so authoring an address here would be a 50/50 guess and thus the fabricated-plausible-output failure DESIGN §5 forbids. The decision exists and is one import away: gunbc.spark.dgx_procurement `dgx_spark_router_binding_operator_allocation` records srv5 taking spark-a3ee and srv6 taking spark-3bd5, decided 2026-08-07 under an explicit operator delegation, on an ascending-address-order basis kept precisely so the tie-break is attributable rather than looking like a measurement; `srv5_router_binding` and `srv6_router_binding` are both SlotAssigned carrying it. The two notes are the same date — the stated blocker was resolved the day it was written. THE DOCTRINE WAS INVOKED AGAINST THE WRONG TARGET, which is why this is a correction and not a refresh: §5 forbids fabricating an OBSERVATION, and an attributable ALLOCATION with a decider, a date and a basis is not one. This is the stale-citation class in its expensive form — a rotted REASON rather than a rotted line number — and it propagated: a lane read it, believed Spark work was blocked on an operator fact, and reported that upward before anyone opened the procurement carrier. WHAT WAS STILL TRUE UNTIL DCH-0, and was why no endpoint row was added here (SUPERSEDED — the clause is preserved as written because the DCH-0 clause below is a rebuttal of it rather than a refresh): srv5/srv6 remain absent from `endpoints` and from gunbc.fleet_intent's ComputeHost list, because in this module that membership IS enrollment — authoring the rows would enroll them, not merely describe them — and there is nothing to enroll into while the units are unplugged and the converge timer is retired. A PROJECTED ENDPOINT ALSO CANNOT LIVE HERE, and that is structural rather than a preference: gunbc.spark.dgx_procurement imports THIS module for operator_host_srv5/srv6, so the reverse import is refused by the import graph's one law — measured, not inferred, by adding it and compiling: `circular dependency detected: gunbc.fleet_intent_network -> gunbc.spark.dgx_procurement`. Anyone who later wants the endpoints projected from the binding starts from that constraint. Until enrollment genuinely happens, the address authority stays single because there is only ever one — the reservation rows in the procurement module. SPARK-WIFI-0 (2026-08-27): TWO THINGS IN THIS NOTE WENT STALE AT ONCE, and both are corrected in the procurement module rather than here, because that is where the address authority lives. First, the addresses: the operator moved both units onto the LAN's wireless SSID, unplugged both ethernet cables, and authored fresh CR1000A reservations keyed to the RADIO MACs — spark-a3ee is now 192.168.1.226 (F0:68:E3:B3:1A:40) and spark-3bd5 is now 192.168.1.225 (F0:68:E3:31:AB:E6). A DHCP reservation binds a MAC, and a radio has its own, so the ethernet-keyed rows could not follow the units across the medium change. Second, and more consequentially for anyone reading this note for a reason: THE UNITS ARE NO LONGER UNPLUGGED. The clause above gives "the units are unplugged and the converge timer is retired" as the standing reason there is nothing to enroll into, and the first half of that is now false — both boxes are live, reachable, and answering SSH on their enrolled host keys, which were re-scanned at the new addresses and matched exactly. Enrollment is still NOT performed here, and that is deliberate rather than leftover: membership in `endpoints` IS enrollment in this module, so authoring the rows is the act itself and belongs to the roadmap node that owns it, not to an address correction. What changed is the REASON — from "there is nothing to enroll" to "enrolling is a decision nobody has taken yet" — and that distinction is exactly the rotted-reason class this note already documents itself falling into once. DCH-0 (2026-09-02): THE ENDPOINTS HALF OF ENROLLMENT IS NOW PERFORMED — `srv5_host_lan_endpoint` and `srv6_host_lan_endpoint` are authored below and are members of `endpoints`, which retires the "enrolling is a decision nobody has taken yet" reason for this half and only this half. The decision was taken by the DCH-0 roadmap node (docs/plans/dedicated-coding-harness-plan.md), whose reasoning is that list membership was measured to have ZERO production consumers — 57 non-test modules import this one and none reads `endpoints` or `fleet_intent_network_topology()`; production reads individual rows BY NAME — so the load-bearing act is authoring rows the named-import consumers can reach, and the list is this authority's completeness statement. THE ComputeHost HALF IS DELIBERATELY NOT PERFORMED and is a decision rather than a row (DCH-0c): gunbc.fleet_intent's `fleet_intent_known_hosts` has three production consumers, it mints two RunnerHostSudoersArtifact generated artifacts, and gunbc.runner.runner_host_deploy `admit_runner_host` is a fail-closed enrollment wall returning RunnerHostUnenrolled that today protects these two machines — so enrolling there REMOVES a refusal and needs the host facts the conservation wall consumes. Every sentence in this note about the ComputeHost list therefore still stands unchanged. // SPARK-PAIR-1 (2026-09-02). srv7/srv8 are the operator's HostIdentity slots for the SECOND DGX // Spark pair -- spark-c2b1 at 192.168.1.232 and spark-ac79 at 192.168.1.233 on the wireless LAN, diff --git a/dag/gunbc/spark/group_arm_launch.dag b/dag/gunbc/spark/group_arm_launch.dag index a61c4c1e12a..263ea04cbbd 100644 --- a/dag/gunbc/spark/group_arm_launch.dag +++ b/dag/gunbc/spark/group_arm_launch.dag @@ -4,7 +4,7 @@ import extdeps.huggingface.hub { hub_repo_cache_directory } import gunbc.spark.model_snapshot_acquisition { spark_hub_cache_root } import gunbc.fleet_wireless_link { observe_wireless_link, spark_wireless_link_desired, wireless_link_observation_line, kernel_disconnect_line_count, dgx_spark_wireless_interface } import extdeps.systemd.journalctl { journalctl_kernel_current_boot_argv } -import gunbc.auth.standing_operator_grant { standing_grant_covers, StandingArmLaunch } +import gunbc.auth.standing_operator_grant { standing_grant_covers, StandingArmLaunch, StandingGrantFabricGroup } import gunbc.spark.pair_serving_d0 { d0_standing_grants } import gunbc.spark.pair_serving_d0_door { StandingGrantRowStanding, StandingGrantRowOnMain, StandingGrantRowNotOnMain, fresh_grant_row_standing, executed_grant_row } import extdeps.git @@ -317,7 +317,7 @@ fn group_arm_released_launch_causes(group: FabricGroup, hosts: List) -> List { - if any(d0_standing_grants, g => standing_grant_covers(g: g, group: group, effect: StandingArmLaunch, hosts: hosts)) { + if any(d0_standing_grants, g => standing_grant_covers(g: g, scope: StandingGrantFabricGroup { group: group, hosts: hosts }, effect: StandingArmLaunch)) { [] as List } else { [join([group_label(g: group), " has been released to the fleet and no standing grant covers an arm launch on every planned host (", join(map(hosts, h => h as String), ", "), "); there is no suspension to launch a successor under either"], "")] diff --git a/dag/gunbc/spark/pair_serving_d0.dag b/dag/gunbc/spark/pair_serving_d0.dag index 8432da22030..9ca66a55ae7 100644 --- a/dag/gunbc/spark/pair_serving_d0.dag +++ b/dag/gunbc/spark/pair_serving_d0.dag @@ -1,6 +1,6 @@ module gunbc.spark.pair_serving_d0 -import gunbc.auth.standing_operator_grant { StandingOperatorGrant, group_a_dev_standing_grant, standing_grant_covers, StandingD0ReleaseToFleet } +import gunbc.auth.standing_operator_grant { StandingOperatorGrant, group_a_dev_standing_grant, standing_grant_covers, StandingD0ReleaseToFleet, StandingGrantFabricGroup } import std.types { String, Bool, Int, NonEmptyStr, List, EpochSecs, Port, Timestamp } import std.nat { Nat } import std.measure { Second, second, second_count } @@ -786,7 +786,7 @@ fn d0_standing_grant_for_subject(subject: D0Subject) -> StandingOperatorGrant? { match subject.operation { D0SuspendForSuccessor { successor: _, cleanup: _, term: _ } => none D0ReleaseToFleet { cause: _, approval: _ } => - first(filter(d0_standing_grants, g => standing_grant_covers(g: g, group: subject.group, effect: StandingD0ReleaseToFleet, hosts: subject.hosts))) + first(filter(d0_standing_grants, g => standing_grant_covers(g: g, scope: StandingGrantFabricGroup { group: subject.group, hosts: subject.hosts }, effect: StandingD0ReleaseToFleet))) } } diff --git a/dag/gunbc/spark/standing_host_effect_recover.dag b/dag/gunbc/spark/standing_host_effect_recover.dag index 3555bee031c..ff174f20e18 100644 --- a/dag/gunbc/spark/standing_host_effect_recover.dag +++ b/dag/gunbc/spark/standing_host_effect_recover.dag @@ -5,7 +5,7 @@ import std.process { ProcessExit, ExitSuccess, exit_failure } import std.optional { Present, Absent } import product.host_identity { HostIdentity, host_identity_eq } import product.capacity.event_chain { EventId } -import gunbc.auth.standing_operator_grant { StandingOperatorGrant, standing_grant_covers, StandingHostEffectRecover } +import gunbc.auth.standing_operator_grant { StandingOperatorGrant, standing_grant_covers, StandingHostEffectRecover, StandingGrantFabricGroup } import gunbc.spark.fabric_switch_observed { FabricGroup, FabricGroupA, fabric_group_of_host, fabric_group_wire } import gunbc.spark.pair_serving_d0 { d0_standing_grants } import gunbc.spark.pair_serving_d0_door { StandingGrantRowStanding, StandingGrantRowOnMain, StandingGrantRowNotOnMain, fresh_grant_row_standing, executed_grant_row } @@ -62,7 +62,7 @@ fn recover_claim_selection(host: HostIdentity, effects: List) // THE COVERING GRANT ITSELF, not a yes/no: its identity is what the release records as its authority, so the // provenance is read from the grant that covered rather than restated (review 74852). fn recover_covering_grant(host: HostIdentity, host_group: FabricGroup) -> StandingOperatorGrant? { - first(filter(d0_standing_grants, standing => standing_grant_covers(g: standing, group: host_group, effect: StandingHostEffectRecover, hosts: [host]))) + first(filter(d0_standing_grants, standing => standing_grant_covers(g: standing, scope: StandingGrantFabricGroup { group: host_group, hosts: [host] }, effect: StandingHostEffectRecover))) } type RecoverAuthority diff --git a/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag b/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag new file mode 100644 index 00000000000..e826abf47a3 --- /dev/null +++ b/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag @@ -0,0 +1,211 @@ +module test.claim.auth.standing_operator_grant_mtjade1_witness + +import std.logic { Bool } +import std.types { List, NonEmptyStr, String } +import std.optional { Present, Absent } +import product.host_identity { HostIdentity, host_identity_eq } +import gunbc.fleet_host_identity { + operator_host_mtcollins1, operator_host_mtjade1, + operator_host_srv5, operator_host_srv6, operator_host_srv7, operator_host_srv8, +} +import gunbc.spark.fabric_switch_observed { FabricGroupA, FabricGroupB, fabric_group_hosts } +import gunbc.auth.standing_operator_grant { + group_a_dev_standing_grant, mtjade1_live_standing_grant, + standing_grant_covers, standing_grant_scope_matches, standing_grant_hosts, + StandingGrantFabricGroup, StandingGrantHost, + StandingD0ReleaseToFleet, StandingArmLaunch, StandingHostEffectRecover, +} +import gunbc.auth.authorization_pattern_selection { + PrivilegedEffect, ApiSurface, + WorkloadIdentityStanding, WorkloadIdentityBindable, WorkloadIdentityUnbindable, + MintsNoCredential, MintsResourceScopedCredential, + IrreversibleEffect, + NoBillingConsequence, + WitnessDischarge, NoWitnessDischarge, StandingRulingUnderInterlock, StandingDestructiveAuthorization, + InterlockPending, UnconditionalStanding, InterlockedBy, + FederatedScopedGrant, OperatorApprovedCapability, + PatternSelected, NoAdmissiblePattern, + AuthorizationPatternSelection, + select_authorization_pattern, standing_ruling_discharges_irreversibility, +} +import gunbc.auth.privileged_effect_census { + mtcollins1_operator_ruling, ruling_discharge_interlock_defect, +} +import std.decl_ref { decl_ref } +import std.human_intervention { DeviceOnce, EveryProvision } + +fn group_a_hosts() -> List { + [operator_host_srv5, operator_host_srv6, operator_host_srv7, operator_host_srv8] +} + +fn selected_federated(s: AuthorizationPatternSelection) -> Bool { + match s { + PatternSelected { pattern: FederatedScopedGrant, receipt: _ } => true + _ => false + } +} + +fn selected_approved(s: AuthorizationPatternSelection) -> Bool { + match s { + PatternSelected { pattern: OperatorApprovedCapability, receipt: _ } => true + _ => false + } +} + +fn no_admissible(s: AuthorizationPatternSelection) -> Bool { + match s { + NoAdmissiblePattern { causes: _, scope: _ } => true + _ => false + } +} + +fn mtjade1_session_identity() -> WorkloadIdentityStanding { + WorkloadIdentityUnbindable { cause: "wet operations on mtjade1 run from an operator session over ssh to srv1, not a bound workload identity" as NonEmptyStr } +} + +fn mtjade1_boot_effect(discharge: WitnessDischarge) -> PrivilegedEffect { + PrivilegedEffect { + subject: "mtjade1 boot: attach, boot-device set, power cycle" as NonEmptyStr, + frequency: EveryProvision, + reversibility: IrreversibleEffect { what_is_lost: "a power cycle destroys the unit's RAM and the session it was running; no reapply restores it" as NonEmptyStr }, + surface: ApiSurface, + workload_identity: mtjade1_session_identity(), + minted_reach: MintsNoCredential, + billing: NoBillingConsequence, + witness_discharge: discharge, + } +} + +fn mtjade1_credential_write_effect(discharge: WitnessDischarge) -> PrivilegedEffect { + PrivilegedEffect { + subject: "mtjade1 BMC credential/login write on one controller at one firmware build" as NonEmptyStr, + frequency: DeviceOnce, + reversibility: IrreversibleEffect { what_is_lost: "each account write replaces the value it overwrites; the published factory value is not restored by a reapply" as NonEmptyStr }, + surface: ApiSurface, + workload_identity: mtjade1_session_identity(), + minted_reach: MintsResourceScopedCredential, + billing: NoBillingConsequence, + witness_discharge: discharge, + } +} + +fn mtjade1_megarac_qualification_effect(discharge: WitnessDischarge) -> PrivilegedEffect { + PrivilegedEffect { + subject: "mtjade1 MegaRAC per-build operation qualification write" as NonEmptyStr, + frequency: DeviceOnce, + reversibility: IrreversibleEffect { what_is_lost: "a controller write at a firmware build is not undone by a reapply of a different build's evidence" as NonEmptyStr }, + surface: ApiSurface, + workload_identity: mtjade1_session_identity(), + minted_reach: MintsNoCredential, + billing: NoBillingConsequence, + witness_discharge: discharge, + } +} + +data mtjade1_discharge: WitnessDischarge = StandingRulingUnderInterlock { ruling: mtjade1_live_standing_grant.ruling } + +test fn w_group_a_coverage_is_unchanged() -> Bool { + standing_grant_scope_matches(g: group_a_dev_standing_grant, scope: StandingGrantFabricGroup { group: FabricGroupA, hosts: group_a_hosts() }) + && standing_grant_covers(g: group_a_dev_standing_grant, scope: StandingGrantFabricGroup { group: FabricGroupA, hosts: group_a_hosts() }, effect: StandingD0ReleaseToFleet) + && standing_grant_covers(g: group_a_dev_standing_grant, scope: StandingGrantFabricGroup { group: FabricGroupA, hosts: group_a_hosts() }, effect: StandingArmLaunch) + && standing_grant_covers(g: group_a_dev_standing_grant, scope: StandingGrantFabricGroup { group: FabricGroupA, hosts: [operator_host_srv7] }, effect: StandingHostEffectRecover) + && !standing_grant_covers(g: group_a_dev_standing_grant, scope: StandingGrantFabricGroup { group: FabricGroupA, hosts: [] as List }, effect: StandingArmLaunch) + && !standing_grant_covers(g: group_a_dev_standing_grant, scope: StandingGrantFabricGroup { group: FabricGroupB, hosts: fabric_group_hosts(g: FabricGroupB) }, effect: StandingD0ReleaseToFleet) + && !standing_grant_covers(g: group_a_dev_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingD0ReleaseToFleet) + && !standing_grant_scope_matches(g: group_a_dev_standing_grant, scope: StandingGrantHost { host: operator_host_srv5 }) +} + +test fn w_mtcollins1_is_not_covered() -> Bool { + !standing_grant_scope_matches(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtcollins1 }) + && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtcollins1 }, effect: StandingD0ReleaseToFleet) + && !standing_grant_scope_matches(g: group_a_dev_standing_grant, scope: StandingGrantHost { host: operator_host_mtcollins1 }) +} + +test fn w_an_effect_outside_the_mtjade1_arms_is_not_covered() -> Bool { + standing_grant_scope_matches(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }) + && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingD0ReleaseToFleet) + && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingArmLaunch) + && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtjade1 }, effect: StandingHostEffectRecover) +} + +test fn w_host_scope_hosts_are_derived_from_the_arm() -> Bool { + length(standing_grant_hosts(g: mtjade1_live_standing_grant)) == 1 + && all(standing_grant_hosts(g: mtjade1_live_standing_grant), h => host_identity_eq(a: h, b: operator_host_mtjade1)) + && !any(standing_grant_hosts(g: mtjade1_live_standing_grant), h => host_identity_eq(a: h, b: operator_host_mtcollins1)) +} + +test fn w_the_ruling_text_is_the_operator_quote() -> Bool { + (mtjade1_live_standing_grant.ruling.ruling_text as String) == "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.'" + && match mtjade1_live_standing_grant.ruling.interlock { + InterlockPending { obligation: _ } => true + InterlockedBy { hold: _ } => false + UnconditionalStanding { reason: _ } => false + } + && !standing_ruling_discharges_irreversibility(r: mtjade1_live_standing_grant.ruling) +} + +test fn w_the_selection_fold_over_true_mtjade1_session_attributes() -> Bool { + let boot_ruled = select_authorization_pattern(e: mtjade1_boot_effect(discharge: mtjade1_discharge)) + let boot_bare = select_authorization_pattern(e: mtjade1_boot_effect(discharge: NoWitnessDischarge)) + let cred_ruled = select_authorization_pattern(e: mtjade1_credential_write_effect(discharge: mtjade1_discharge)) + let cred_bare = select_authorization_pattern(e: mtjade1_credential_write_effect(discharge: NoWitnessDischarge)) + let fw_ruled = select_authorization_pattern(e: mtjade1_megarac_qualification_effect(discharge: mtjade1_discharge)) + let fw_bare = select_authorization_pattern(e: mtjade1_megarac_qualification_effect(discharge: NoWitnessDischarge)) + no_admissible(s: boot_ruled) + && no_admissible(s: boot_bare) + && !selected_federated(s: boot_ruled) + && selected_approved(s: cred_ruled) + && selected_approved(s: cred_bare) + && !selected_federated(s: cred_ruled) + && selected_approved(s: fw_ruled) + && selected_approved(s: fw_bare) + && !selected_federated(s: fw_ruled) +} + +fn mtjade1_bindable_identity() -> WorkloadIdentityStanding { + WorkloadIdentityBindable { member: "ghrunner on srv1, the dispatched fleet-converge run's host principal on the placed fabric DB host" as NonEmptyStr } +} + +fn mtjade1_bindable_boot_effect(discharge: WitnessDischarge) -> PrivilegedEffect { + PrivilegedEffect { + subject: "mtjade1 boot: attach, boot-device set, power cycle" as NonEmptyStr, + frequency: EveryProvision, + reversibility: IrreversibleEffect { what_is_lost: "a power cycle destroys the unit's RAM and the session it was running; no reapply restores it" as NonEmptyStr }, + surface: ApiSurface, + workload_identity: mtjade1_bindable_identity(), + minted_reach: MintsNoCredential, + billing: NoBillingConsequence, + witness_discharge: discharge, + } +} + +fn mtjade1_interlocked_ruling() -> StandingDestructiveAuthorization { + StandingDestructiveAuthorization { + ruling_text: mtjade1_live_standing_grant.ruling.ruling_text, + effect_subject: mtjade1_live_standing_grant.ruling.effect_subject, + interlock: InterlockedBy { hold: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant") }, + } +} + +test fn w_bindable_boot_pending_interlock_refuses() -> Bool { + let pending = select_authorization_pattern(e: mtjade1_bindable_boot_effect(discharge: mtjade1_discharge)) + no_admissible(s: pending) && !selected_federated(s: pending) +} + +test fn w_bindable_boot_interlocked_selects_federation() -> Bool { + selected_federated(s: select_authorization_pattern(e: mtjade1_bindable_boot_effect(discharge: StandingRulingUnderInterlock { ruling: mtjade1_interlocked_ruling() }))) +} + +test fn w_census_pending_interlock_is_a_defect() -> Bool { + match ruling_discharge_interlock_defect(site_ref: decl_ref(module_path: "gunbc.auth.standing_operator_grant", decl_name: "mtjade1_live_standing_grant"), ruling: mtjade1_live_standing_grant.ruling) { + Present { value: _ } => true + Absent => false + } +} + +test fn w_census_interlocked_rostered_is_not_a_defect() -> Bool { + match ruling_discharge_interlock_defect(site_ref: decl_ref(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_wet"), ruling: mtcollins1_operator_ruling) { + Absent => true + Present { value: _ } => false + } +} diff --git a/dag/test/claim/spark/pair_serving_d0_release_witness_test.dag b/dag/test/claim/spark/pair_serving_d0_release_witness_test.dag index b0498a90453..3941efd630b 100644 --- a/dag/test/claim/spark/pair_serving_d0_release_witness_test.dag +++ b/dag/test/claim/spark/pair_serving_d0_release_witness_test.dag @@ -25,7 +25,7 @@ import std.scoped_authorization { OperatorGrant, AttemptIdentity, ClaimedBy, aut import gunbc.spark.pair_serving_d0 { d0_standing_grant_for, d0_binding_text, d0_binding_text_with, D0AuthorizationBasis, D0BasisBroker, D0BasisStandingGrant } import gunbc.spark.pair_serving_d0_door { standing_grant_row_judged, d0_honored_standing_grant, StandingGrantRowOnMain, StandingGrantRowNotOnMain, ExecutedGrantRowRead, ExecutedGrantRowUnread, grant_row_standing_over, grant_row_proof_over, GrantRowBlobRead, GrantRowBlobUnread } import gunbc.spark.pair_serving_d0 { D0GrantRowApproved, D0GrantRowUnproven, d0_frozen_filing_text_with, parse_d0_frozen_filing } -import gunbc.auth.standing_operator_grant { group_a_dev_standing_grant, standing_grant_covers, standing_grant_authorization, StandingArmLaunch } +import gunbc.auth.standing_operator_grant { group_a_dev_standing_grant, standing_grant_covers, standing_grant_authorization, StandingArmLaunch, StandingGrantFabricGroup } import gunbc.spark.pair_serving_d0 { D0Subject, D0SuspendForSuccessor, D0ReleaseToFleet, RankVacancyReading, RankOccupancyReading, D0Observation, IncumbentReading, IncumbentDidNotAnswer, IncumbentAnsweredUnread, IncumbentRouteUnread, @@ -299,7 +299,7 @@ test fn rw_an_effect_outside_the_scope_is_not_covered() -> Bool { destructive: true, } foreign_host && match d0_standing_grant_for(request: suspend) { Present { value: _ } => false Absent => true } - && !standing_grant_covers(g: group_a_dev_standing_grant, group: FabricGroupA, effect: StandingArmLaunch, hosts: [] as List) + && !standing_grant_covers(g: group_a_dev_standing_grant, scope: StandingGrantFabricGroup { group: FabricGroupA, hosts: [] as List }, effect: StandingArmLaunch) }) }