Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 30 additions & 3 deletions dag/gunbc/auth/authorization_pattern_selection.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
}
Expand Down Expand Up @@ -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], "")
}
}

Expand Down
28 changes: 21 additions & 7 deletions dag/gunbc/auth/privileged_effect_census.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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<DeclarationRef> = [
Expand Down Expand Up @@ -408,39 +409,52 @@ 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: 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<InterlockRoot>,
},
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<DeclarationRef> {
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]
}
})
}

Expand Down
Loading