diff --git a/dag/gunbc/auth/authorization_pattern_selection.dag b/dag/gunbc/auth/authorization_pattern_selection.dag index 442f5b58df5..923e5d974fc 100644 --- a/dag/gunbc/auth/authorization_pattern_selection.dag +++ b/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) } } diff --git a/dag/gunbc/auth/privileged_effect_census.dag b/dag/gunbc/auth/privileged_effect_census.dag index 630357bfc6c..237bfd0daf9 100644 --- a/dag/gunbc/auth/privileged_effect_census.dag +++ b/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 } +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 = [ data privileged_effect_interlocks: List = [ 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, }, 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, + }, ] // 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 } } } diff --git a/dag/gunbc/auth/standing_operator_grant.dag b/dag/gunbc/auth/standing_operator_grant.dag index 0cca4dbb43f..85b1e751a81 100644 --- a/dag/gunbc/auth/standing_operator_grant.dag +++ b/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,8 +118,7 @@ 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, @@ -128,10 +126,10 @@ data mtjade1_live_standing_grant: StandingOperatorGrant = StandingOperatorGrant 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, + effects: [StandingBmcSecureAccountWrite], } // COVERAGE IS AN IDENTITY JOIN: the scope is the grant's, the effect is one of its effects, and EVERY host diff --git a/dag/gunbc/fleet/convergence_fold.dag b/dag/gunbc/fleet/convergence_fold.dag index 432da9faf74..ae8065babc0 100644 --- a/dag/gunbc/fleet/convergence_fold.dag +++ b/dag/gunbc/fleet/convergence_fold.dag @@ -42,12 +42,18 @@ import gunbc.host_convergence_census { // independent readback does not ground. Incomplete is neither refused (the domain decided not to act, // or acting was refused before any effect) nor converged, and it never satisfies a precondition. // +// WHAT THIS HOME CARRIES SINCE O1c-3, with BmcSecure as first gated consumer +// (gunbc.machine_intake_arrival_converge): a step is Ungated or GatedOnAuthorization; a gated +// instance whose receipt declares that authorization was required (the Apply arm) refuses without a +// discharge for that (run, step, subject); Noop does not require one (parent D4). A discharge's +// principal is NonEmptyStr at the sole constructor, so the fold does not re-check emptiness. +// The pattern itself is selected before the fold (DESIGN §3d); the fold only checks discharge. +// // WHAT IT STILL DOES NOT CARRY, because no consumer exercises it yet and a designed fixture is not an -// inhabitant (DESIGN §3 pairing obligation): the authorization gate and its discharge, principals, -// mutation lanes, pending with re-attach across runs, subject quantifiers (all-of / any-of over a -// subject set), the domain-declared cheap readback, and order derived from preconditions alone where -// no order authority exists. Each lands with its first real consumer: O1c-3 (BmcSecure and -// ManagedHostAdmission), the Spark arm. +// inhabitant (DESIGN §3 pairing obligation): pending with re-attach across runs, subject quantifiers +// (all-of / any-of over a subject set), the domain-declared cheap readback, and order derived from +// preconditions alone where no order authority exists. Each lands with its first real consumer: the +// Spark arm. // A RUN AND A SUBJECT ARE THE CALLER'S IDENTITIES, BRANDED SO NEITHER IS READ AS THE OTHER. The // subject key is the domain's canonical spelling of what one step instance converges: for the arrival @@ -96,10 +102,26 @@ fn precondition_key(p: StepPrecondition, key: StepInstanceKey) -> StepInstanceKe // A STEP: its census identity, the ONE member of the order authority it is bound to, and its // preconditions. The member type is the authority's own (for the arrival prefix // gunbc.machine_intake_phase IntakePhase); the fold reads it only through the authority's rank. +// A STEP IS UNGATED, OR GATED ON AN AUTHORIZATION DISCHARGED FOR THAT INSTANCE. Selected before the +// fold: the caller names which pattern discharged it. The fold never selects a pattern. +type StepGate + = StepUngated + | StepGatedOnAuthorization + type ConvergenceStep { identity: DeclarationRef order_member: M preconditions: List + gate: StepGate +} + +fn ungated_readonly_step(identity: DeclarationRef, order_member: M, preconditions: List) -> ConvergenceStep { + ConvergenceStep { + identity: identity, + order_member: order_member, + preconditions: preconditions, + gate: StepUngated, + } } // THE ORDER AUTHORITY: which declaration owns the order, and its ranking. Absent is an unranked @@ -309,17 +331,48 @@ fn step_outcome_incomplete(outcome: StepOutcome) -> I? { type ConvergenceReceiptProjection sole_constructor { key_of: fn(R) -> StepInstanceKey consumed_of: fn(R) -> List + authorization_required_of: fn(R) -> Bool } -fn convergence_receipt_projection(key_of: fn(R) -> StepInstanceKey, consumed_of: fn(R) -> List) -> ConvergenceReceiptProjection +fn convergence_receipt_projection(key_of: fn(R) -> StepInstanceKey, consumed_of: fn(R) -> List, authorization_required_of: fn(R) -> Bool) -> ConvergenceReceiptProjection admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "arrival_receipt_projection"), decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_precondition_is_not_satisfied_by_a_receipt_for_another_subject"), decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_precondition_is_not_satisfied_by_a_receipt_from_another_run"), decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_an_incomplete_instance_satisfies_no_dependent_and_the_run_is_incomplete"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_noop_needs_no_discharge"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_without_discharge_refuses"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "apply_fold_undischarged"), + ] +{ + ConvergenceReceiptProjection { key_of: key_of, consumed_of: consumed_of, authorization_required_of: authorization_required_of } +} + +// A DISCHARGE FOR ONE GATED INSTANCE, sealed: the domain verifies the selected pattern (operator +// capability, standing grant coverage, or federated workload principal) and mints this row; the fold +// only checks that a gated Apply has one for this key. Noop never requires it. +type InstanceAuthorization sole_constructor { + key: StepInstanceKey + principal: NonEmptyStr +} + +fn instance_authorization(key: StepInstanceKey, principal: NonEmptyStr) -> InstanceAuthorization + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "discharge_bmc_secure_apply"), + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "capability_discharge"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_without_discharge_refuses"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_noop_needs_no_discharge"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "apply_fold_undischarged"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_discharge_for_another_run_refuses"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_discharge_for_another_unit_refuses"), ] { - ConvergenceReceiptProjection { key_of: key_of, consumed_of: consumed_of } + InstanceAuthorization { key: key, principal: principal } +} + +fn instance_authorization_for(discharges: List, key: StepInstanceKey) -> InstanceAuthorization? { + discharges |> filter(d => step_instance_key_eq(a: d.key, b: key)) |> first() } type StepInstanceRefusal @@ -327,6 +380,7 @@ type StepInstanceRefusal | StepOutcomeAbsent | PreconditionUnmet { precondition: StepInstanceKey, consumed: List } | ConsumedReceiptNotAPrecondition { consumed: StepInstanceKey } + | AuthorizationUndischarged type StepInstanceStanding = InstanceConverged { key: StepInstanceKey, receipt: R } @@ -472,6 +526,7 @@ fn walk_instance( subject: StepSubjectKey, outcomes: List>, projection: ConvergenceReceiptProjection, + discharges: List, ) -> LedgerWalk { let key = step_instance_key(run: run, step: ranked.step.identity, subject: subject) match acc.line { @@ -483,11 +538,31 @@ fn walk_instance( Present { value: o } => match o { StepRefused { key: _, cause: c } => InstanceRefused { key: key, cause: DomainRefused { cause: c } } - StepIncomplete { key: _, cause: i } => InstanceIncomplete { key: key, cause: i } + StepIncomplete { key: _, cause: i } => + match ranked.step.gate { + StepUngated => InstanceIncomplete { key: key, cause: i } + StepGatedOnAuthorization => + match instance_authorization_for(discharges: discharges, key: key) { + Absent => InstanceRefused { key: key, cause: AuthorizationUndischarged } + Present { value: _ } => InstanceIncomplete { key: key, cause: i } + } + } StepEstablished { receipt: r } => match precondition_refusal(step: ranked.step, key: key, consumed: projection.consumed_of(r), ledger: acc.instances) { Present { value: why } => InstanceRefused { key: key, cause: why } - Absent => InstanceConverged { key: key, receipt: r } + Absent => + match ranked.step.gate { + StepUngated => InstanceConverged { key: key, receipt: r } + StepGatedOnAuthorization => + if projection.authorization_required_of(r) { + match instance_authorization_for(discharges: discharges, key: key) { + Absent => InstanceRefused { key: key, cause: AuthorizationUndischarged } + Present { value: _ } => InstanceConverged { key: key, receipt: r } + } + } else { + InstanceConverged { key: key, receipt: r } + } + } } } } @@ -496,20 +571,19 @@ fn walk_instance( } } -// THE RUN FOLD: one ledger per run, each instance converged, refused, incomplete or not reached, in the admitted -// order. The verdict is derived from the ledger and names the instance the line stopped at. fn fold_convergence_run( plan: AdmittedConvergencePlan, run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>, projection: ConvergenceReceiptProjection, + discharges: List, ) -> ConvergenceRunVerdict { match first_outcome_refusal(run: run, subject: subject, plan: plan, keys: map(outcomes, o => outcome_key(outcome: o, projection: projection))) { Present { value: r } => RunOutcomesRefused { cause: r } Absent => { let walked = fold(plan.steps, init: LedgerWalk { line: LineOpen, instances: [] }, f: (acc, s) => - walk_instance(acc: acc, ranked: s, run: run, subject: subject, outcomes: outcomes, projection: projection)) + walk_instance(acc: acc, ranked: s, run: run, subject: subject, outcomes: outcomes, projection: projection, discharges: discharges)) let ledger = ConvergenceRunLedger { run: run, subject: subject, order_authority: plan.authority, instances: walked.instances } match walked.line { LineOpen => RunConverged { run: ConvergedRun { ledger: ledger } } diff --git a/dag/gunbc/fleet/fleet_host_identity.dag b/dag/gunbc/fleet/fleet_host_identity.dag index 42deced7e0d..dc4ab9bdd99 100644 --- a/dag/gunbc/fleet/fleet_host_identity.dag +++ b/dag/gunbc/fleet/fleet_host_identity.dag @@ -1,5 +1,7 @@ module gunbc.fleet_host_identity +import std.types { List, NonEmptyStr, String } +import v2.std.algebra { filter } import product.host_identity { HostIdentity } // THE FLEET'S HOST IDENTITIES, as a leaf. These rows were authored in gunbc.fleet_intent_network, @@ -80,3 +82,26 @@ data operator_host_srv11: HostIdentity = "srv11" // lease table the day the fabric switch was cabled and landed on switch lane qsfp56-dd-2-3. srv12 // is its identity slot, assigned by the same ascending-address rule. data operator_host_srv12: HostIdentity = "srv12" + +// THE NAMED ROSTER, ONE LIST BESIDE THE ROWS. A step subject or other label resolves to a host only +// by joining this membership; a spelling that is not a row here is not a fleet host. +data operator_hosts: List = [ + operator_host_srv1, + operator_host_srv2, + operator_host_srv3, + operator_host_srv4, + operator_host_mtcollins1, + operator_host_mtjade1, + operator_host_srv5, + operator_host_srv6, + operator_host_srv7, + operator_host_srv8, + operator_host_srv9, + operator_host_srv10, + operator_host_srv11, + operator_host_srv12, +] + +fn operator_host_named(label: NonEmptyStr) -> HostIdentity? { + operator_hosts |> filter(h => (h as String) == (label as String)) |> first() +} diff --git a/dag/gunbc/guarantee_stall/authored_record_field_list_standing_for_type_population_stall.dag b/dag/gunbc/guarantee_stall/authored_record_field_list_standing_for_type_population_stall.dag new file mode 100644 index 00000000000..0b65eff47d5 --- /dev/null +++ b/dag/gunbc/guarantee_stall/authored_record_field_list_standing_for_type_population_stall.dag @@ -0,0 +1,39 @@ +module gunbc.guarantee_stall.authored_record_field_list_standing_for_type_population_stall + +import gunbc.guarantee_rung { Mitigatable, StructurallyImpossible } +import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation, climbs_when } + +// WHY THIS IS A STALL AND NOT A SECTION 4b(3) DROP. Nothing was lowered. Before the BmcSecure +// observation join grew past four fields, the join already bound an authored subset; extending it +// to the rest of BmcAccountStateObservation except controller_clock did not drop a rung that had +// been held. DESIGN section 4b(2) requires a class below its ceiling to name its next-rung trigger. +// +// HOMES CHECKED BEFORE MINTING, so this is not a nickname of an existing class: +// gunbc.guarantee_stall.axis_list_re_enumerates_its_variant_type_stall -- authored list mirroring a +// declared COPRODUCT constructor population; waits on constructor enumeration. Record field +// identity-and-type is a different primitive. +// gunbc.guarantee_stall.roster_re_enumerates_its_own_rows_stall -- authored roster of DATA +// declarations; waits on declaration VALUE BINDING. A List is not a record field set. +// gunbc.recurring_failure_mode.optional_equality_answers_by_representation -- Optional == answering +// by representation (interpreter `first` vs Present). That is one ARM of this row's OR trigger, not +// the authored-field-list class. +// gunbc.recurring_failure_mode.handwritten_population_wrong_by_gain_and_by_loss, +// gunbc.recurring_failure_mode.roster_is_its_own_denominator -- waiter/report lists, not type fields. +// gunbc.recurring_failure_mode.kind_carried_but_its_fields_stay_optional -- Node payload optionality. +// gunbc.recurring_failure_mode.a_pattern_binding_a_subset_of_fields_is_an_implicit_wildcard -- match +// wildcards, not equality adapters. +data authored_record_field_list_standing_for_type_population_stall: GuaranteeStall = GuaranteeStall { + subject: "an authored field list stands for a record type's declared population, so a new field or a new Optional can fall out of an equality join silently", + current: Mitigatable, + ceiling: StructurallyImpossible, + blocker: AwaitsOneGrounding { + grounding: "a value-layer read of a record's declared fields with their types, sufficient to refuse an unhandled field or Optional at a join; or structural == that is value-exact over Optionals (gunbc#13488), after which clock blanking and the hand match delete", + }, + population: BoundedPopulation { + members: [ + "gunbc.machine_intake_bmc_secure bmc_account_state_observation_same", + "gunbc.machine_intake_bmc_secure controller_clock_reading_same", + ], + }, + next_rung_trigger: climbs_when(capability: "a value-layer read of a record's declared fields with their types, sufficient to refuse an unhandled field or an unhandled Optional at this join, checked by field identity and declared type never by count; OR gunbc#13488 making structural == value-exact over Optionals, after which observation_with_controller_clock blanking and controller_clock_reading_same are deleted. A count of fields, a comment claiming completeness, or a second authored list is not this capability"), +} diff --git a/dag/gunbc/guarantee_stall/roster.dag b/dag/gunbc/guarantee_stall/roster.dag index 2240a5c4741..92beb2a3a50 100644 --- a/dag/gunbc/guarantee_stall/roster.dag +++ b/dag/gunbc/guarantee_stall/roster.dag @@ -77,6 +77,7 @@ import gunbc.guarantee_stall.free_semigroup_text_crossing_decided_by_spelling_st import gunbc.guarantee_stall.emitted_inline_crate_path_edges_unreturned_stall { emitted_inline_crate_path_edges_unreturned_stall } import gunbc.guarantee_stall.compile_pool_provision_wired_but_unreachable_stall { compile_pool_provision_wired_but_unreachable_stall } import gunbc.guarantee_stall.filesystem_read_outcome_node_grain_census_stall { filesystem_read_outcome_node_grain_census_stall } +import gunbc.guarantee_stall.authored_record_field_list_standing_for_type_population_stall { authored_record_field_list_standing_for_type_population_stall } // THE COHORT PROVENANCE NOTES BELOW WERE AUTHORED WHEN EVERY ROW SAT IN ONE FILE, and they are // carried here verbatim rather than split across the row modules they describe. Their membership @@ -249,6 +250,7 @@ data all_guarantee_stalls: List = [ accumulator_copy_untyped_combiner_refusals_stall, keyed_apply_patch_rebuilds_rows_per_hunk_stall, filesystem_read_outcome_node_grain_census_stall, + authored_record_field_list_standing_for_type_population_stall, ] // THE FOUR SUBJECTS RESTORED TO THE ROSTER, PINNED BY IDENTITY SO THEIR LOSS REFUSES. diff --git a/dag/gunbc/host_convergence_census.dag b/dag/gunbc/host_convergence_census.dag index fe27735eb1a..8b6b122ca71 100644 --- a/dag/gunbc/host_convergence_census.dag +++ b/dag/gunbc/host_convergence_census.dag @@ -848,6 +848,15 @@ data host_convergence_census_rows: List = [ disposition: RetainAuthority, first_consumer: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_prefix"), ), + census_row( + identity: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure"), + subject: MachineIntakeArrival, + phases: protocol_phases(false, true, true, true, false, true, false), + current_authority: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure"), + persistent_host_effect: ReachesPersistentHostMutation, + disposition: RetainAuthority, + first_consumer: cite(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_through_bmc_secure"), + ), ] data host_convergence_census_standing: HostConvergenceCensus = admit_host_convergence_census(rows: host_convergence_census_rows) diff --git a/dag/gunbc/machine_intake/arrival_converge.dag b/dag/gunbc/machine_intake/arrival_converge.dag index 53321df64ec..7611439accd 100644 --- a/dag/gunbc/machine_intake/arrival_converge.dag +++ b/dag/gunbc/machine_intake/arrival_converge.dag @@ -1,6 +1,7 @@ module gunbc.machine_intake_arrival_converge -import std.types { List, NonEmptyStr, String } +import std.types { Bool, Int, List, NonEmptyStr, String } +import std.content_hash { content_hash_equal } import std.decl_ref { DeclarationRef, decl_ref } import std.goal_assessment { ObservationAttempt, @@ -19,7 +20,7 @@ import std.upsert_decision { UpsertDecision, Noop, Apply, Refuse } import extdeps.bmc.endpoint { BmcControllerEndpoint, BmcEndpoint, BmcFirmwareFamily, Redfish } import extdeps.bmc.capability { BmcFirmwareReleaseIdentity, bmc_firmware_release_identity_of_wire } import extdeps.bmc.access_profile { SurfaceManagerIdentity } -import gunbc.machine_intake_receipt { EvidenceRef } +import gunbc.machine_intake_receipt { EvidenceRef, same_intake_subject } import gunbc.machine_intake_phase { ArrivalPhase, AccessDiscover, @@ -40,6 +41,7 @@ import gunbc.machine_intake_phase { Placement, arrival_phases_all, intake_phase_rank, + machine_qualification_policy_digest, } import gunbc.machine_intake_subject { AssemblyManifest, @@ -77,6 +79,7 @@ import gunbc.machine_intake_mtjade1_access_observation { fru_gap_text, smbios_gap_text, sol_session_controller, + mtjade1_smbios_sol_attribution, provisional_assembly_of_fru, read_mtjade1_current_manager_read, read_mtjade1_fru, @@ -85,9 +88,12 @@ import gunbc.machine_intake_mtjade1_access_observation { import gunbc.machine_intake_mtcollins1_bmc_secure_observation { mtcollins1_unit_key_standing } import gunbc.machine_intake_bmc_rotation_route { BmcRotationRouteStanding, + BmcAccountWriteRequest, ObservedSurfaceRead, rotation_route_candidate, redfish_account_password_write, + rotation_apply_authority, + rotation_route_request_identity, } import gunbc.machine_intake_bmc_rotation_route_evidence { manager_read_receipt, mtjade1_observed_endpoint } import gunbc.host_convergence_protocol { HostEffectDomainProjection, inspect_via_host_effect_projection } @@ -104,6 +110,38 @@ import gunbc.machine_intake_prior_life_boundary { prior_life_receipt_key, prior_life_receipt_consumed_identity, } +import gunbc.machine_intake_bmc_secure { + BmcSecureGoal, + BmcAccountStateObservation, + BmcSecureStateInspected, + BmcSecureStateUnobserved, + BmcSecurePhaseConverged, + BmcSecurePhaseRefused, + BmcSecurePhaseNoop, + BmcSecurePhaseApplied, + BmcSecurePhaseReceipt, + inspect_bmc_secure_state, + bmc_secure_phase_noop, + bmc_secure_phase_applied, + BmcAccountApplication, + ManagedCredentialReference, + managed_reference_same, + bmc_account_state_observation_same, +} +import gunbc.auth.authorization_pattern_selection { + InterlockedBy, InterlockPending, +} +import gunbc.auth.standing_operator_grant { + StandingOperatorGrant, + StandingGrantHost, + StandingBmcSecureAccountWrite, + standing_grant_covers, +} +import gunbc.auth.privileged_effect_census { ruling_interlock_is_rostered } +import product.host_identity { HostIdentity, host_identity_eq } +import gunbc.fleet_host_identity { operator_host_named, operator_host_mtjade1 } +import gunbc.auth.approval_capability { ProposeApprove, ProposeDeny } +import gunbc.auth.approval_broker { Redemption, RedemptionAdmitted, RedemptionRefused } import gunbc.fleet.convergence_fold { ConvergenceRunId, StepSubjectKey, @@ -127,20 +165,27 @@ import gunbc.fleet.convergence_fold { fold_convergence_run, step_instance_key, step_outcome_receipt, + ungated_readonly_step, + StepGatedOnAuthorization, + InstanceAuthorization, + instance_authorization, } -// THE ARRIVAL CONVERGENCE PREFIX (docs/plans/managed-host-untangle.md, cuts O1c-1 and O1c-2): the first -// real consumer of gunbc.fleet.convergence_fold. Its three steps are the first three phases of -// gunbc.machine_intake_phase arrival_phases_all -- AccessDiscover, IdentityBindProvisional and -// PriorLifeBoundary -- each a protocol step through gunbc.host_convergence_protocol +// THE ARRIVAL CONVERGENCE PREFIX (docs/plans/managed-host-untangle.md, cuts O1c-1 through O1c-3): the +// first real consumer of gunbc.fleet.convergence_fold. Its four steps are the first four phases of +// gunbc.machine_intake_phase arrival_phases_all -- AccessDiscover, IdentityBindProvisional, +// PriorLifeBoundary and BmcSecure -- each a protocol step through gunbc.host_convergence_protocol // HostEffectDomainProjection (observe, assess, decide) with its own row in // gunbc.host_convergence_census. The first two are read-only: the only decision either can reach is // Noop (the phase's goal is read back as already holding) or Refuse; neither has an Apply, so an Apply // decision is itself a typed refusal, and the read each consumes is a committed capture. // PriorLifeBoundary is the first effectful step: its archive arm writes the controller's prior-life // records to the evidence store and reads them back, DRY in this cut -// (gunbc.machine_intake_prior_life_boundary), so it is the one step that can be INCOMPLETE. Nothing -// here performs a live BMC call or a live store write. gunbc.bmc_onboarding is not imported. +// (gunbc.machine_intake_prior_life_boundary), so it is the one step that can be INCOMPLETE. +// BmcSecure is the first GATED step: Apply refuses unless authorization is discharged for that unit +// and that run (standing grant, operator capability, or federated workload principal selected before +// the fold); Noop needs no discharge. Nothing here performs a live BMC credential write. +// gunbc.bmc_onboarding is not imported. // // ORDERING TIME. No field of the read-only steps is an ordering clock. The controller's own DateTime is // kept as an AccessDiscover observation only; the observer clock (gunbc.clock_read) orders the @@ -154,6 +199,8 @@ data identity_bind_provisional_step_ref: DeclarationRef = decl_ref(module_path: data prior_life_boundary_step_ref: DeclarationRef = decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "prior_life_boundary") +data bmc_secure_step_ref: DeclarationRef = decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure") + // A read-only phase has no remedy. The plan type of its projection is sealed to this module and this // module constructs none, so an Apply over a read-only phase has no value to carry. type ReadOnlyPhaseRemedy sole_constructor { @@ -454,6 +501,7 @@ type ArrivalStepReceipt = AccessDiscoverReceipt { receipt: AccessDiscoverEstablished } | IdentityBindReceipt { receipt: IdentityBoundProvisional } | PriorLifeBoundaryReceipt { receipt: PriorLifeBoundaryEstablished } + | BmcSecureReceipt { receipt: BmcSecureStepEstablished } type ArrivalStepRefusal = AccessDiscoverObserveRefused { cause: AccessObserveRefusal } @@ -464,17 +512,37 @@ type ArrivalStepRefusal | ReadOnlyPhaseSatisfiedWithoutEvidence { phase: ArrivalPhase } | PriorLifeIdentityForAnotherInstance { identity: StepInstanceKey } | PriorLifeBoundaryRefused { cause: PriorLifeRefusal } + | BmcSecureIdentityForAnotherInstance { identity: StepInstanceKey } + | BmcSecureAuthorizationUndischarged + | BmcSecurePhaseDomainRefused + | BmcSecureApplyInputsMissing + | BmcSecureApplicationForAnotherInstance { subject: MachineIntakeSubject } + | BmcSecureApplicationNotTheInspectedTransition -// A STEP WHOSE EFFECT WAS ATTEMPTED AND IS NOT GROUNDED BY ITS READBACK. Only PriorLifeBoundary has -// an effect in this prefix; the read-only phases cannot be incomplete. type ArrivalStepIncomplete = PriorLifeBoundaryIncomplete { cause: PriorLifeIncomplete } +type BmcSecureStepEstablished sole_constructor { + key: StepInstanceKey + consumed_prior_life: StepInstanceKey + phase: BmcSecurePhaseReceipt +} + +fn bmc_secure_step_established(key: StepInstanceKey, consumed_prior_life: StepInstanceKey, phase: BmcSecurePhaseReceipt) -> BmcSecureStepEstablished + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure"), + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure_bound"), + ] +{ + BmcSecureStepEstablished { key: key, consumed_prior_life: consumed_prior_life, phase: phase } +} + fn arrival_receipt_key(r: ArrivalStepReceipt) -> StepInstanceKey { match r { AccessDiscoverReceipt { receipt: a } => a.key IdentityBindReceipt { receipt: i } => i.key PriorLifeBoundaryReceipt { receipt: p } => prior_life_receipt_key(r: p) + BmcSecureReceipt { receipt: b } => b.key } } @@ -483,11 +551,25 @@ fn arrival_receipt_consumed(r: ArrivalStepReceipt) -> List { AccessDiscoverReceipt { receipt: _ } => [] IdentityBindReceipt { receipt: i } => [i.consumed_access] PriorLifeBoundaryReceipt { receipt: p } => [prior_life_receipt_consumed_identity(r: p)] + BmcSecureReceipt { receipt: b } => [b.consumed_prior_life] + } +} + +fn arrival_receipt_authorization_required(r: ArrivalStepReceipt) -> Bool { + match r { + AccessDiscoverReceipt { receipt: _ } => false + IdentityBindReceipt { receipt: _ } => false + PriorLifeBoundaryReceipt { receipt: _ } => false + BmcSecureReceipt { receipt: b } => + match b.phase.decision { + BmcSecurePhaseNoop { observation: _ } => false + BmcSecurePhaseApplied { plan: _, application: _, post_read: _ } => true + } } } fn arrival_receipt_projection() -> ConvergenceReceiptProjection { - convergence_receipt_projection(key_of: arrival_receipt_key, consumed_of: arrival_receipt_consumed) + convergence_receipt_projection(key_of: arrival_receipt_key, consumed_of: arrival_receipt_consumed, authorization_required_of: arrival_receipt_authorization_required) } fn read_only_refusal(phase: ArrivalPhase, decision: UpsertDecision) -> ArrivalStepRefusal { @@ -582,6 +664,251 @@ fn prior_life_boundary(key: StepInstanceKey, identity: IdentityBoundProvisional, } } +type BmcSecureApplyInputs { + application: BmcAccountApplication + post_read: BmcAccountStateObservation +} + +type BmcSecureInputs { + goal: BmcSecureGoal + reading: BmcAccountStateObservation + grant: StandingOperatorGrant? + capability: Redemption? + apply: BmcSecureApplyInputs? +} + +// A federated principal is not a discharge input. StandingBmcSecureAccountWrite on the operator-ssh +// units is WorkloadIdentityUnbindable, so FederatedScopedGrant is not a selected pattern for this +// effect. A NonEmptyStr here was a silent widen (review 38602): any string minted Apply. + +fn bmc_secure_account_rotation_site() -> DeclarationRef { + decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "plan_bmc_account_action") +} + +fn grant_discharges_bmc_secure_account_write(g: StandingOperatorGrant, host: HostIdentity) -> Bool { + standing_grant_covers(g: g, scope: StandingGrantHost { host: host }, effect: StandingBmcSecureAccountWrite) + && match g.ruling.interlock { + InterlockPending { obligation: _ } => false + InterlockedBy { hold: h } => + ruling_interlock_is_rostered(site_ref: bmc_secure_account_rotation_site(), interlock: h) + } +} + +fn capability_discharges_bmc_secure_account_write( + r: Redemption, + standing: BmcRotationRouteStanding, + request: BmcAccountWriteRequest, + key: StepInstanceKey, +) -> Bool { + match r { + RedemptionRefused { cause: _ } => false + RedemptionAdmitted { claims: cl, decided_by: _ } => + match cl.decision { + ProposeDeny => false + ProposeApprove => + cl.authority == rotation_apply_authority + && (cl.attempt as NonEmptyStr) == (key.run as NonEmptyStr) + && (cl.request_revision as String) == (rotation_route_request_identity(standing: standing, request: request) as String) + } + } +} + +fn bound_bmc_secure_host(key: StepInstanceKey) -> HostIdentity? { + operator_host_named(label: key.subject as NonEmptyStr) +} + +fn bound_host_owns_this_controller(host: HostIdentity, endpoint: BmcControllerEndpoint) -> Bool { + host_identity_eq(a: host, b: operator_host_mtjade1) + && (endpoint.host as String) == (sol_session_controller(a: mtjade1_smbios_sol_attribution).host as String) +} + +fn bmc_secure_instance_joins_this_controller( + key: StepInstanceKey, + identity_subject: MachineIntakeSubject, + reading: BmcAccountStateObservation, + standing: BmcRotationRouteStanding, +) -> Bool { + same_intake_subject(left: reading.subject, right: identity_subject) + && (key.run as String) == (identity_subject.attempt_id as String) + && (standing.endpoint.host as String) == (reading.endpoint.host as String) + && match bound_bmc_secure_host(key: key) { + Absent => false + Present { value: host } => bound_host_owns_this_controller(host: host, endpoint: standing.endpoint) + } +} + +fn capability_discharge( + key: StepInstanceKey, + inputs: BmcSecureInputs, + standing: BmcRotationRouteStanding, + request: BmcAccountWriteRequest, +) -> InstanceAuthorization? + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "discharge_bmc_secure_apply"), + ] +{ + match inputs.capability { + Present { value: r } => + if capability_discharges_bmc_secure_account_write(r: r, standing: standing, request: request, key: key) { + match r { + RedemptionAdmitted { claims: _, decided_by: by } => Present { value: instance_authorization(key: key, principal: by) } + RedemptionRefused { cause: _ } => none + } + } else { + none + } + Absent => none + } +} + +fn discharge_bmc_secure_apply( + key: StepInstanceKey, + identity_subject: MachineIntakeSubject, + inputs: BmcSecureInputs, + standing: BmcRotationRouteStanding, + request: BmcAccountWriteRequest, +) -> InstanceAuthorization? + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure_bound"), + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_through_bmc_secure"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_uncovered_grant_falls_through_to_capability"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_uncovered_grant_refuses_a_capability_for_another_request"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_foreign_bound_host_key_cannot_mint_from_this_instance_controller"), + ] +{ + if !bmc_secure_instance_joins_this_controller(key: key, identity_subject: identity_subject, reading: inputs.reading, standing: standing) { + none + } else { + match bound_bmc_secure_host(key: key) { + Absent => none + Present { value: host } => + match inputs.grant { + Present { value: g } => + if grant_discharges_bmc_secure_account_write(g: g, host: host) { + Present { value: instance_authorization(key: key, principal: g.principal) } + } else { + capability_discharge(key: key, inputs: inputs, standing: standing, request: request) + } + Absent => + capability_discharge(key: key, inputs: inputs, standing: standing, request: request) + } + } + } +} + +fn managed_generation_advances_the_requested(requested: ManagedCredentialReference, planned: ManagedCredentialReference) -> Bool { + requested.account == planned.account + && requested.role == planned.role + && (requested.secret.project as String) == (planned.secret.project as String) + && requested.secret.secret == planned.secret.secret + && planned.credential_epoch > requested.credential_epoch +} + +fn bmc_account_observation_is_the_inspected_pre_state(inspected: BmcAccountStateObservation, diverged: BmcAccountStateObservation) -> Bool { + bmc_account_state_observation_same(a: inspected, b: diverged) +} + +fn bmc_secure_application_joins_this_instance( + identity_subject: MachineIntakeSubject, + inspected_reading: BmcAccountStateObservation, + requested_goal: BmcSecureGoal, + application: BmcAccountApplication, +) -> ArrivalStepRefusal? { + if !same_intake_subject(left: application.plan.subject, right: identity_subject) { + Present { value: BmcSecureApplicationForAnotherInstance { subject: application.plan.subject } } + } else if !bmc_account_observation_is_the_inspected_pre_state(inspected: inspected_reading, diverged: application.plan.diverged) { + Present { value: BmcSecureApplicationNotTheInspectedTransition } + } else if !managed_reference_same(a: requested_goal.published_break_glass, b: application.plan.goal.published_break_glass) { + Present { value: BmcSecureApplicationNotTheInspectedTransition } + } else if !content_hash_equal(left: machine_qualification_policy_digest(policy: requested_goal.policy), right: machine_qualification_policy_digest(policy: application.plan.goal.policy)) { + Present { value: BmcSecureApplicationNotTheInspectedTransition } + } else if !managed_generation_advances_the_requested(requested: requested_goal.managed, planned: application.plan.goal.managed) { + Present { value: BmcSecureApplicationNotTheInspectedTransition } + } else { + none + } +} + +// Apply and discharge consume the bound subject's identity and the instance keys, not the +// AccessDiscover/IdentityBind capture parses. Those steps remain the prefix; this is the BMC +// grain after PriorLifeBoundary. +fn bmc_secure_bound( + key: StepInstanceKey, + identity_key: StepInstanceKey, + identity_subject: MachineIntakeSubject, + prior_key: StepInstanceKey, + inputs: BmcSecureInputs, +) -> StepOutcome + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "bmc_secure"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "bmc_secure_bound_refuses_foreign_apply"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_without_authorization_refuses_after_a_real_apply"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_channel_state_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_present_controller_clock_over_absent_is_refused"), + ] +{ + if (identity_key.run as NonEmptyStr) != (key.run as NonEmptyStr) || (identity_key.subject as NonEmptyStr) != (key.subject as NonEmptyStr) { + StepRefused { key: key, cause: BmcSecureIdentityForAnotherInstance { identity: identity_key } } + } else if (prior_key.run as NonEmptyStr) != (key.run as NonEmptyStr) || (prior_key.subject as NonEmptyStr) != (key.subject as NonEmptyStr) { + StepRefused { key: key, cause: BmcSecureIdentityForAnotherInstance { identity: prior_key } } + } else { + match inspect_bmc_secure_state(subject: identity_subject, goal: inputs.goal, reading: inputs.reading) { + BmcSecureStateUnobserved { cause: _ } => StepRefused { key: key, cause: BmcSecurePhaseDomainRefused } + BmcSecureStateInspected { observed: _, assessment: a, decision: d } => + match d { + Noop => + match bmc_secure_phase_noop(subject: identity_subject, goal: inputs.goal, reading: inputs.reading) { + BmcSecurePhaseConverged { receipt: phase } => + StepEstablished { receipt: BmcSecureReceipt { receipt: bmc_secure_step_established(key: key, consumed_prior_life: prior_key, phase: phase) } } + BmcSecurePhaseRefused { cause: _ } => StepRefused { key: key, cause: BmcSecurePhaseDomainRefused } + } + Refuse { reason: _ } => StepRefused { key: key, cause: BmcSecurePhaseDomainRefused } + Apply { plan: _ } => + match inputs.apply { + Absent => StepRefused { key: key, cause: BmcSecureApplyInputsMissing } + Present { value: ap } => + match bmc_secure_application_joins_this_instance( + identity_subject: identity_subject, + inspected_reading: inputs.reading, + requested_goal: inputs.goal, + application: ap.application, + ) { + Present { value: c } => StepRefused { key: key, cause: c } + Absent => + match discharge_bmc_secure_apply( + key: key, + identity_subject: identity_subject, + inputs: inputs, + standing: ap.application.plan.managed_write.route, + request: ap.application.plan.managed_write.request, + ) { + Absent => StepRefused { key: key, cause: BmcSecureAuthorizationUndischarged } + Present { value: _ } => + match bmc_secure_phase_applied(application: ap.application, post_read: ap.post_read) { + BmcSecurePhaseConverged { receipt: phase } => + StepEstablished { receipt: BmcSecureReceipt { receipt: bmc_secure_step_established(key: key, consumed_prior_life: prior_key, phase: phase) } } + BmcSecurePhaseRefused { cause: _ } => StepRefused { key: key, cause: BmcSecurePhaseDomainRefused } + } + } + } + } + } + } + } +} + +fn bmc_secure(key: StepInstanceKey, identity: IdentityBoundProvisional, prior: PriorLifeBoundaryEstablished, inputs: BmcSecureInputs) -> StepOutcome { + bmc_secure_bound( + key: key, + identity_key: identity.key, + identity_subject: identity.subject, + prior_key: prior_life_receipt_key(r: prior), + inputs: inputs, + ) +} + // ── THE PLAN: a prefix of the authority's order, never a second list ─────────────────────────── fn arrival_order_authority() -> ConvergenceOrderAuthority { @@ -599,10 +926,15 @@ fn arrival_planning_authority() -> ConvergencePlanningAuthority { // the plan; it is never skipped. fn arrival_step_of_phase(phase: ArrivalPhase) -> ConvergenceStep? { match phase { - AccessDiscover => Present { value: ConvergenceStep { identity: access_discover_step_ref, order_member: Arrival { phase: AccessDiscover }, preconditions: [] } } - IdentityBindProvisional => Present { value: ConvergenceStep { identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: [SameSubject { step: access_discover_step_ref }] } } - PriorLifeBoundary => Present { value: ConvergenceStep { identity: prior_life_boundary_step_ref, order_member: Arrival { phase: PriorLifeBoundary }, preconditions: [SameSubject { step: identity_bind_provisional_step_ref }] } } - BmcSecure => none + AccessDiscover => Present { value: ungated_readonly_step(identity: access_discover_step_ref, order_member: Arrival { phase: AccessDiscover }, preconditions: []) } + IdentityBindProvisional => Present { value: ungated_readonly_step(identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: [SameSubject { step: access_discover_step_ref }]) } + PriorLifeBoundary => Present { value: ungated_readonly_step(identity: prior_life_boundary_step_ref, order_member: Arrival { phase: PriorLifeBoundary }, preconditions: [SameSubject { step: identity_bind_provisional_step_ref }]) } + BmcSecure => Present { value: ConvergenceStep { + identity: bmc_secure_step_ref, + order_member: Arrival { phase: BmcSecure }, + preconditions: [SameSubject { step: prior_life_boundary_step_ref }], + gate: StepGatedOnAuthorization, + } } BootDeliveryEstablish => none DiagnosticBootAttest => none InventoryConform => none @@ -682,21 +1014,56 @@ fn arrival_prefix_outcomes(run: ConvergenceRunId, subject: StepSubjectKey, read: [access, identity, prior_life_boundary(key: step_instance_key(run: run, step: prior_life_boundary_step_ref, subject: subject), identity: i, platform: prior_life.platform, world: prior_life.world)] AccessDiscoverReceipt { receipt: _ } => [access, identity] PriorLifeBoundaryReceipt { receipt: _ } => [access, identity] + BmcSecureReceipt { receipt: _ } => [access, identity] } Absent => [access, identity] } } IdentityBindReceipt { receipt: _ } => [access] PriorLifeBoundaryReceipt { receipt: _ } => [access] + BmcSecureReceipt { receipt: _ } => [access] + } + } +} + +fn arrival_prefix_outcomes_through_bmc_secure(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead, inputs: IdentityBindInputs, prior_life: PriorLifeInputs, bmc: BmcSecureInputs) -> List> { + let prefix = arrival_prefix_outcomes(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life) + match prefix.last() { + Absent => prefix + Present { value: last } => + match step_outcome_receipt(outcome: last) { + Absent => prefix + Present { value: r } => + match r { + PriorLifeBoundaryReceipt { receipt: p } => + match prefix |> filter(o => match step_outcome_receipt(outcome: o) { Present { value: ir } => match ir { IdentityBindReceipt { receipt: _ } => true _ => false } Absent => false }) |> first() { + Absent => prefix + Present { value: id_out } => + match step_outcome_receipt(outcome: id_out) { + Absent => prefix + Present { value: ir } => + match ir { + IdentityBindReceipt { receipt: i } => + concat(prefix, [bmc_secure(key: step_instance_key(run: run, step: bmc_secure_step_ref, subject: subject), identity: i, prior: p, inputs: bmc)]) + AccessDiscoverReceipt { receipt: _ } => prefix + PriorLifeBoundaryReceipt { receipt: _ } => prefix + BmcSecureReceipt { receipt: _ } => prefix + } + } + } + AccessDiscoverReceipt { receipt: _ } => prefix + IdentityBindReceipt { receipt: _ } => prefix + BmcSecureReceipt { receipt: _ } => prefix + } } } } -fn fold_arrival_prefix(steps: List>, run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>) -> ArrivalPrefixVerdict { +fn fold_arrival_prefix(steps: List>, run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>, discharges: List) -> ArrivalPrefixVerdict { match admit_convergence_plan(planning: arrival_planning_authority(), steps: steps) { ConvergencePlanRefused { cause: c } => ArrivalPlanRefused { cause: c } ConvergencePlanAdmitted { plan: plan } => - ArrivalRunFolded { verdict: fold_convergence_run(plan: plan, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection()) } + ArrivalRunFolded { verdict: fold_convergence_run(plan: plan, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection(), discharges: discharges) } } } @@ -704,7 +1071,34 @@ fn converge_arrival_prefix(run: ConvergenceRunId, subject: StepSubjectKey, read: match arrival_prefix_steps(phases: arrival_prefix_through(last: arrival_prefix_last)) { ArrivalPrefixPhaseUnstepped { phase: p } => ArrivalPrefixUnstepped { phase: p } ArrivalPrefixStepped { steps: steps } => - fold_arrival_prefix(steps: steps, run: run, subject: subject, outcomes: arrival_prefix_outcomes(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life)) + fold_arrival_prefix(steps: steps, run: run, subject: subject, outcomes: arrival_prefix_outcomes(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life), discharges: []) + } +} + +// Apply mints through discharge_bmc_secure_apply. Noop never requires a fold discharge +// (arrival_receipt_authorization_required is false on BmcSecurePhaseNoop), so a grant +// copied here would be unused. +fn converge_arrival_through_bmc_secure(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentManagerRead, inputs: IdentityBindInputs, prior_life: PriorLifeInputs, bmc: BmcSecureInputs) -> ArrivalPrefixVerdict { + match arrival_prefix_steps(phases: arrival_prefix_through(last: BmcSecure)) { + ArrivalPrefixPhaseUnstepped { phase: p } => ArrivalPrefixUnstepped { phase: p } + ArrivalPrefixStepped { steps: steps } => { + let key = step_instance_key(run: run, step: bmc_secure_step_ref, subject: subject) + let discharges = match bmc.apply { + Present { value: ap } => + match discharge_bmc_secure_apply( + key: key, + identity_subject: bmc.reading.subject, + inputs: bmc, + standing: ap.application.plan.managed_write.route, + request: ap.application.plan.managed_write.request, + ) { + Present { value: d } => [d] + Absent => [] + } + Absent => [] + } + fold_arrival_prefix(steps: steps, run: run, subject: subject, outcomes: arrival_prefix_outcomes_through_bmc_secure(run: run, subject: subject, read: read, inputs: inputs, prior_life: prior_life, bmc: bmc), discharges: discharges) + } } } @@ -742,3 +1136,14 @@ fn converge_mtjade1_arrival_prefix(run: ConvergenceRunId, prior_life: DryPriorLi prior_life: PriorLifeInputs { platform: mt_jade_platform_ref, world: prior_life }, ) } + +fn converge_mtjade1_arrival_through_bmc_secure(run: ConvergenceRunId, prior_life: DryPriorLifeWorld, bmc: BmcSecureInputs) -> ArrivalPrefixVerdict uses fs: std.resources.Filesystem { + converge_arrival_through_bmc_secure( + run: run, + subject: "mtjade1" as StepSubjectKey, + read: read_mtjade1_current_manager_read(), + inputs: mtjade1_identity_bind_inputs(), + prior_life: PriorLifeInputs { platform: mt_jade_platform_ref, world: prior_life }, + bmc: bmc, + ) +} diff --git a/dag/gunbc/machine_intake/bmc_rotation_route.dag b/dag/gunbc/machine_intake/bmc_rotation_route.dag index b997639aa7c..5deebbaa799 100644 --- a/dag/gunbc/machine_intake/bmc_rotation_route.dag +++ b/dag/gunbc/machine_intake/bmc_rotation_route.dag @@ -152,6 +152,8 @@ fn rotation_route_from_citation( decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "cited_lab_route_managed_user"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "cited_lab_route_published_user"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "cited_lab_route_managed_user_previous_build"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "cited_mtjade1_managed_route"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "cited_mtjade1_published_route"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "an_open_channel_is_closed_only_over_a_grounded_channel_access_route"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_channel_close_readback_is_bound_to_the_observed_run_and_account"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "a_planned_channel_close_is_applied_read_back_and_converges"), diff --git a/dag/gunbc/machine_intake/bmc_secure.dag b/dag/gunbc/machine_intake/bmc_secure.dag index 473f2ae3885..4a3b782bd43 100644 --- a/dag/gunbc/machine_intake/bmc_secure.dag +++ b/dag/gunbc/machine_intake/bmc_secure.dag @@ -3,7 +3,7 @@ module gunbc.machine_intake_bmc_secure import std.types { Bool, EpochMs, Int, List, Map, NonEmptyStr, String, list_length } import v2.std.algebra { filter } import std.decl_ref { decl_ref } -import std.content_hash { ContentHash, content_hash_of_value } +import std.content_hash { ContentHash, content_hash_of_value, content_hash_equal } import std.dissolution { DissolutionCondition, unbound_dissolution } import std.algebra { FreeSemigroup } import std.goal_assessment { @@ -1286,6 +1286,7 @@ fn observed_bmc_account_state( ) -> BmcAccountStateObservation admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "dry_read_bmc_account_state"), + decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "observation_with_controller_clock"), ] { BmcAccountStateObservation { @@ -1328,6 +1329,35 @@ fn observed_published_account_at_join(account: ObservedPublishedAccount) -> Publ } } +fn observation_with_controller_clock(base: BmcAccountStateObservation, controller_clock: ControllerClockReading?) -> BmcAccountStateObservation + admit_callers: [ + decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "bmc_account_state_observation_same"), + decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "apply_with_diverged_controller_clock"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_present_controller_clock_over_absent_is_refused"), + ] +{ + observed_bmc_account_state( + subject: base.subject, + endpoint: base.endpoint, + firmware: base.firmware, + managed: base.managed, + managed_user: base.managed_user, + attempt: base.attempt, + read_floor: base.read_floor, + managed_probe: base.managed_probe, + channel_census: base.channel_census, + census_evidence: base.census_evidence, + census_observed_at: base.census_observed_at, + published_probes: base.published_probes, + published_user: base.published_user, + published_account: base.published_account, + break_glass: base.break_glass, + break_glass_probe: base.break_glass_probe, + controller_clock: controller_clock, + ) +} + fn managed_reference_same(a: ManagedCredentialReference, b: ManagedCredentialReference) -> Bool { a.account == b.account && a.role == b.role @@ -1337,6 +1367,34 @@ fn managed_reference_same(a: ManagedCredentialReference, b: ManagedCredentialRef && a.credential_epoch == b.credential_epoch } +// THE OBSERVATION IS THE PAYLOAD, NOT A START TIME. Record `==` is the language's structural +// relation on the closed type, except controller_clock: ControllerClockReading? inherits +// optional_equality_answers_by_representation, so that field is matched explicitly and the rest +// compared by `==` after zeroing it. That match and observation_with_controller_clock are still +// authored field lists: a new ControllerClockReading field or a new Optional on the observation +// is not derived from the type declaration (no .dag value-layer reader of declared fields). The +// class is gunbc.guarantee_stall.authored_record_field_list_standing_for_type_population_stall +// authored_record_field_list_standing_for_type_population_stall -- a stall below ceiling, not a +// section 4b(3) drop. +fn controller_clock_reading_same(left: ControllerClockReading?, right: ControllerClockReading?) -> Bool { + match left { + Absent => match right { Absent => true Present { value: _ } => false } + Present { value: a } => match right { + Absent => false + Present { value: b } => + (a.reported_millis as Int) == (b.reported_millis as Int) + && a.evidence.label == b.evidence.label + && content_hash_equal(left: a.evidence.digest, right: b.evidence.digest) + } + } +} + +fn bmc_account_state_observation_same(a: BmcAccountStateObservation, b: BmcAccountStateObservation) -> Bool { + controller_clock_reading_same(left: a.controller_clock, right: b.controller_clock) + && (observation_with_controller_clock(base: a, controller_clock: none) + == observation_with_controller_clock(base: b, controller_clock: none)) +} + // WHAT THE PHASE REQUIRES OF THE CONTROLLER: this managed generation accepted, the published // credential closed, under this qualification policy. // published_break_glass is the exact generation the published account is retired TO (or, under a @@ -2065,6 +2123,34 @@ type BmcAccountApplication sole_constructor { applied_at: ObserverClockInstant } +fn apply_with_diverged_controller_clock(application: BmcAccountApplication, controller_clock: ControllerClockReading?) -> BmcAccountApplication + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused"), + ] +{ + let p = application.plan + BmcAccountApplication { + plan: BmcAccountActionPlan { + subject: p.subject, + endpoint: p.endpoint, + firmware: p.firmware, + goal: p.goal, + diverged: observation_with_controller_clock(base: p.diverged, controller_clock: controller_clock), + due: p.due, + managed_write: p.managed_write, + published_write: p.published_write, + channel_writes: p.channel_writes, + planned_at: p.planned_at, + }, + managed_write_completed: application.managed_write_completed, + published_write_completed: application.published_write_completed, + channel_writes_completed: application.channel_writes_completed, + request_receipt: application.request_receipt, + response_receipt: application.response_receipt, + applied_at: application.applied_at, + } +} + type BmcSecurePhaseDecision = BmcSecurePhaseNoop { observation: BmcAccountStateObservation } | BmcSecurePhaseApplied { plan: BmcAccountActionPlan, application: BmcAccountApplication, post_read: BmcAccountStateObservation } @@ -2189,6 +2275,8 @@ fn dry_bmc_account_instant(millis: EpochMs) -> ObserverClockInstant admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "dry_read_bmc_account_state"), decl_ref(module_path: "gunbc.machine_intake_bmc_secure", decl_name: "dry_apply_bmc_account_plan"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_fetched_generation"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), ] { observer_clock_modeled(millis: millis, realization: bmc_secure_dry_realization_name) @@ -2260,6 +2348,11 @@ fn dry_read_bmc_account_state( ) -> BmcAccountStateObservation admit_callers: [ decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "read_in"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_mtjade1_converges_through_bmc_secure_noop_on_the_real_prefix"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_mtjade1_bmc_secure_apply_inputs_missing_refuses_on_the_real_path"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_channel_state_is_refused"), ] { let at = dry_bmc_account_instant(millis: read_at_millis) @@ -2323,6 +2416,7 @@ fn dry_apply_bmc_account_plan( decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "applied_with"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "the_post_read_is_independent_of_the_reading_that_diverged"), decl_ref(module_path: "test.claim.machine_intake_bmc_secure_state_witness", decl_name: "a_planned_channel_close_is_applied_read_back_and_converges"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), ] { let managed_step = match dry_fetch_resolves(fetch: managed_fetch, write: plan.managed_write) { diff --git a/dag/gunbc/rung_drop/bmc_secure_apply_converge_new_witness_eval_step_cost.dag b/dag/gunbc/rung_drop/bmc_secure_apply_converge_new_witness_eval_step_cost.dag new file mode 100644 index 00000000000..aeedaeaa13f --- /dev/null +++ b/dag/gunbc/rung_drop/bmc_secure_apply_converge_new_witness_eval_step_cost.dag @@ -0,0 +1,38 @@ +module gunbc.rung_drop.bmc_secure_apply_converge_new_witness_eval_step_cost + +import std.types { String, List, NonEmptyStr } +import gunbc.rung_drop { RungDrop, Standing, TypedDeclaration, ReplacementStaged } +import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable } +import v2.workflow.floor_eval_step_cost_drop { floor_eval_step_cost_drop_bmc_secure_apply_converge_rows } + +// DECLARED 4b(3) DROP (gunbc#13517, 2026-10-07). Pairing requires one Apply through +// converge_arrival_through_bmc_secure; that path still bills the arrival prefix plus the dry Apply +// in the seed interpreter. The DECLARATION lives here; the POPULATION's authority is +// `v2.workflow.floor_eval_step_cost_drop` `floor_eval_step_cost_drop_bmc_secure_apply_converge_rows`. +// +// WHAT IS LOST IS ONE WALL, AND THE CLAIM IS UNTOUCHED. The identity stays on the gate: planned, +// executed and measured on every run, its eval_steps recorded; a semantic red and a wall-clock +// crossing still block. Only an eval-step overrun is reported under the declared drop rather than +// refusing. The budget is not raised. + +data bmc_secure_apply_converge_new_witness_eval_step_cost_population: List = floor_eval_step_cost_drop_bmc_secure_apply_converge_rows |> map(m => concat(concat(m.identity, ": over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_bmc_secure_apply_converge_rows; measured by "), m.measured_by)) + +data bmc_secure_apply_converge_new_witness_eval_step_cost: RungDrop = RungDrop { + identity: "bmc_secure_apply_converge_new_witness_eval_step_cost" as NonEmptyStr, + + subject: "new-witness eval-step cost gate over the one Apply inhabitance of converge_arrival_through_bmc_secure: it still executes, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered", + + declared: "2026-10-07", + + standing: Standing, + + declaration: TypedDeclaration { + previous: MechanicallyPreventable, + temporary: Mitigatable, + reason: ReplacementStaged { + replacement: "converge_arrival_through_bmc_secure executing as natively emitted code rather than in the seed interpreter, so the one Apply inhabitance fits the NewWitnessTier eval-step budget", + }, + population: bmc_secure_apply_converge_new_witness_eval_step_cost_population, + restoration_trigger: "THE CAPABILITY: converge_arrival_through_bmc_secure (AccessDiscover through BmcSecure Apply, including the fold's Apply-discharge mint) executing as natively emitted code in a claim frame. WHAT THAT MUST BE SUFFICIENT FOR: test.claim.machine_intake_arrival_converge_witness.w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world, still calling that entry with Apply+grant and still asserting the Applied route, measures under the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives. Deleting the identity, hard-coding discharges: [] in the entry, or relocating the claim off the required gate satisfies none of it.", + } +} 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 index e826abf47a3..f51d4b756cc 100644 --- a/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag +++ b/dag/test/claim/auth/standing_operator_grant_mtjade1_witness_test.dag @@ -13,7 +13,7 @@ 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, + StandingD0ReleaseToFleet, StandingArmLaunch, StandingHostEffectRecover, StandingBmcSecureAccountWrite, } import gunbc.auth.authorization_pattern_selection { PrivilegedEffect, ApiSurface, @@ -22,7 +22,7 @@ import gunbc.auth.authorization_pattern_selection { IrreversibleEffect, NoBillingConsequence, WitnessDischarge, NoWitnessDischarge, StandingRulingUnderInterlock, StandingDestructiveAuthorization, - InterlockPending, UnconditionalStanding, InterlockedBy, + InterlockPending, InterlockedBy, FederatedScopedGrant, OperatorApprovedCapability, PatternSelected, NoAdmissiblePattern, AuthorizationPatternSelection, @@ -123,6 +123,8 @@ test fn w_mtcollins1_is_not_covered() -> Bool { 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: StandingBmcSecureAccountWrite) + && !standing_grant_covers(g: mtjade1_live_standing_grant, scope: StandingGrantHost { host: operator_host_mtcollins1 }, effect: StandingBmcSecureAccountWrite) && !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) @@ -137,11 +139,12 @@ test fn w_host_scope_hosts_are_derived_from_the_arm() -> Bool { 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 + InterlockedBy { hold: h } => + (h.module_path as String) == "gunbc.machine_intake_bmc_rotation_route" + && (h.decl_name as String) == "admit_rotation_apply" + InterlockPending { obligation: _ } => false } - && !standing_ruling_discharges_irreversibility(r: mtjade1_live_standing_grant.ruling) + && standing_ruling_discharges_irreversibility(r: mtjade1_live_standing_grant.ruling) } test fn w_the_selection_fold_over_true_mtjade1_session_attributes() -> Bool { @@ -162,6 +165,12 @@ test fn w_the_selection_fold_over_true_mtjade1_session_attributes() -> Bool { && !selected_federated(s: fw_ruled) } +test fn w_operator_ssh_bmc_write_still_selects_operator_approved_capability() -> Bool { + selected_approved(s: select_authorization_pattern(e: mtjade1_credential_write_effect(discharge: mtjade1_discharge))) + && selected_approved(s: select_authorization_pattern(e: mtjade1_credential_write_effect(discharge: NoWitnessDischarge))) + && !selected_federated(s: select_authorization_pattern(e: mtjade1_credential_write_effect(discharge: mtjade1_discharge))) +} + 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 } } @@ -179,6 +188,14 @@ fn mtjade1_bindable_boot_effect(discharge: WitnessDischarge) -> PrivilegedEffect } } +fn mtjade1_pending_ruling() -> StandingDestructiveAuthorization { + StandingDestructiveAuthorization { + ruling_text: mtjade1_live_standing_grant.ruling.ruling_text, + effect_subject: mtjade1_live_standing_grant.ruling.effect_subject, + interlock: InterlockPending { obligation: "hold not named" as NonEmptyStr }, + } +} + fn mtjade1_interlocked_ruling() -> StandingDestructiveAuthorization { StandingDestructiveAuthorization { ruling_text: mtjade1_live_standing_grant.ruling.ruling_text, @@ -188,7 +205,7 @@ fn mtjade1_interlocked_ruling() -> StandingDestructiveAuthorization { } test fn w_bindable_boot_pending_interlock_refuses() -> Bool { - let pending = select_authorization_pattern(e: mtjade1_bindable_boot_effect(discharge: mtjade1_discharge)) + let pending = select_authorization_pattern(e: mtjade1_bindable_boot_effect(discharge: StandingRulingUnderInterlock { ruling: mtjade1_pending_ruling() })) no_admissible(s: pending) && !selected_federated(s: pending) } @@ -197,7 +214,7 @@ test fn w_bindable_boot_interlocked_selects_federation() -> Bool { } 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) { + match ruling_discharge_interlock_defect(site_ref: decl_ref(module_path: "gunbc.auth.standing_operator_grant", decl_name: "mtjade1_live_standing_grant"), ruling: mtjade1_pending_ruling()) { Present { value: _ } => true Absent => false } diff --git a/dag/test/claim/authorization_pattern_selection_witness_test.dag b/dag/test/claim/authorization_pattern_selection_witness_test.dag index 6697a259935..e323ae009bc 100644 --- a/dag/test/claim/authorization_pattern_selection_witness_test.dag +++ b/dag/test/claim/authorization_pattern_selection_witness_test.dag @@ -15,6 +15,7 @@ import gunbc.auth.authorization_pattern_selection { PatternSelected, ManualStepRequired, NoAdmissiblePattern, PatternSelectionNeedsEvidence, PatternSelectionNeedsPolicy, PatternSelectionRefused, AuthorizationPatternSelection, + InterlockPending, InterlockedBy, select_authorization_pattern, witness_required, } import gunbc.auth.privileged_effect_census { @@ -22,8 +23,9 @@ import gunbc.auth.privileged_effect_census { unrostered_unreasoned_divergences, rostered_but_not_diverging, follow_up_sites, reasoned_divergences, reasoned_divergences_with_fired_triggers, site_verdict, Conforms, DivergesWithReason, Diverges, SiteNotDecidable, - mtcollins1_boot_effect, privileged_effect_interlocks, interlocked_sites_missing_from_census, rulings_without_a_rostered_interlock, + mtcollins1_boot_effect, privileged_effect_interlocks, privileged_effect_interlock_hold, interlocked_sites_missing_from_census, rulings_without_a_rostered_interlock, ruling_roots_missing_from_census, census_sites_outside_ruling_roots, + mtcollins1_operator_ruling, RealizedFederatedGrant, RealizedRunSelected, RealizedApprovalCapability, RealizedHumanStep, RealizedOperatorSession, RealizedUnauthorized, } import std.human_intervention { @@ -366,6 +368,17 @@ test fn every_standing_ruling_has_its_interlock_rostered() -> Bool { (rulings_without_a_rostered_interlock() |> count) == 0 } +test fn pending_rulings_do_not_invent_a_rostered_hold() -> Bool { + match privileged_effect_interlock_hold(interlock: InterlockPending { obligation: "unnamed" as NonEmptyStr }) { + Absent => true + Present { value: _ } => false + } + && match privileged_effect_interlock_hold(interlock: mtcollins1_operator_ruling.interlock) { + Absent => false + Present { value: h } => (h.decl_name as String) == "UnitHoldProof" + } +} + // THE CENSUS SHOWS THE INTERLOCK: every interlocked site is a census row, and the boot's names the // unit hold and the refusal fold that honors it. test fn the_mtcollins1_boot_interlock_is_rostered_against_a_census_row() -> Bool { diff --git a/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag index ea735d8e396..79c50ebb349 100644 --- a/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag +++ b/dag/test/claim/machine_intake/machine_intake_arrival_converge_forged_probe_witness_test.dag @@ -17,7 +17,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // outside its module; this witness hands the source to the compiler through the diagnostic-census // harness and requires SoleConstructorViolation at each SUBJECT by name. The class-scoped control shows // a clean source reading the same modules through their real producers emits none. -data forged_probe_source: String = "module probe_arrival_converge_forged\n\nimport std.types { Int, List, NonEmptyStr, String }\nimport std.decl_ref { decl_ref }\nimport gunbc.machine_intake_phase { Arrival, AccessDiscover, IntakePhase }\nimport gunbc.machine_intake_subject { MachineIntakeSubject, BoardSerialObservation, AssemblyManifest, UnitKey }\nimport gunbc.machine_intake_bmc_rotation_route { BmcRotationRouteStanding }\nimport gunbc.machine_intake_mtjade1_factory_network { ObservedBmcNetwork }\nimport gunbc.machine_intake_mtjade1_access_observation {\n CurrentManagerRead, RecordedManagerIdentityObservation, ControllerClockReading, current_manager_read_of,\n FruRead, SmbiosRead, FruIdentityFields, RecordedFruObservation, RecordedSmbiosObservation, SolSessionAttribution,\n}\nimport gunbc.fleet.convergence_fold {\n AdmittedConvergencePlan, RankedStep, StepInstanceKey, ConvergenceRunId, StepSubjectKey, ConvergenceOrderAuthority, ConvergencePlanningAuthority,\n ConvergenceReceiptProjection, ConvergenceRunLedger, ConvergedRun, StepInstanceStanding,\n convergence_planning_authority, convergence_receipt_projection,\n}\nimport gunbc.machine_intake_arrival_converge {\n AccessDiscoverEstablished, IdentityBoundProvisional, ReadOnlyPhaseRemedy, AccessObservation,\n IdentityBindInputs, ArrivalStepReceipt, ArrivalStepRefusal, ArrivalStepIncomplete, BoardSerialAgreement,\n}\n\nfn forged_access(key: StepInstanceKey, access: AccessObservation, route: BmcRotationRouteStanding) -> AccessDiscoverEstablished {\n AccessDiscoverEstablished { key: key, access: access, route: route }\n}\n\nfn forged_identity(key: StepInstanceKey, subject: MachineIntakeSubject) -> IdentityBoundProvisional {\n IdentityBoundProvisional { key: key, consumed_access: key, subject: subject }\n}\n\nfn forged_plan(steps: List>, key: StepInstanceKey) -> AdmittedConvergencePlan {\n AdmittedConvergencePlan { authority: key.step_identity, steps: steps }\n}\n\nfn forged_remedy() -> ReadOnlyPhaseRemedy {\n ReadOnlyPhaseRemedy { phase: AccessDiscover }\n}\n\nfn any_rank(phase: IntakePhase) -> Int? {\n Present { value: 0 }\n}\n\nfn authored_order() -> ConvergenceOrderAuthority {\n ConvergenceOrderAuthority { authority: decl_ref(module_path: \"gunbc.machine_intake_phase\", decl_name: \"arrival_phases_all\"), rank_of: any_rank }\n}\n\nfn forged_planning_literal() -> ConvergencePlanningAuthority {\n ConvergencePlanningAuthority { order: authored_order() }\n}\n\nfn forged_planning_via_mint() -> ConvergencePlanningAuthority {\n convergence_planning_authority(order: authored_order())\n}\n\nfn rekey(r: ArrivalStepReceipt) -> StepInstanceKey {\n StepInstanceKey { run: \"forged\" as ConvergenceRunId, step_identity: decl_ref(module_path: \"gunbc.machine_intake_arrival_converge\", decl_name: \"access_discover\"), subject: \"mtjade1\" as StepSubjectKey }\n}\n\nfn consumed_nothing(r: ArrivalStepReceipt) -> List {\n []\n}\n\nfn forged_projection_literal() -> ConvergenceReceiptProjection {\n ConvergenceReceiptProjection { key_of: rekey, consumed_of: consumed_nothing }\n}\n\nfn forged_projection_via_mint() -> ConvergenceReceiptProjection {\n convergence_receipt_projection(key_of: rekey, consumed_of: consumed_nothing)\n}\n\nfn forged_ledger(key: StepInstanceKey, instances: List>) -> ConvergenceRunLedger {\n ConvergenceRunLedger { run: key.run, subject: key.subject, order_authority: key.step_identity, instances: instances }\n}\n\nfn forged_converged_run(ledger: ConvergenceRunLedger) -> ConvergedRun {\n ConvergedRun { ledger: ledger }\n}\n\nfn forged_manager_read(identity: RecordedManagerIdentityObservation, clock: ControllerClockReading) -> CurrentManagerRead {\n CurrentManagerRead { identity: identity, controller_clock: clock }\n}\n\nfn forged_manager_read_via_mint(content: String, endpoint: ObservedBmcNetwork) -> CurrentManagerRead {\n current_manager_read_of(content: content, expected_sha256: \"00\" as NonEmptyStr, endpoint: endpoint, link: none, capture_path: \"forged\" as NonEmptyStr)\n}\n\nfn forged_identity_inputs(fru: FruRead, smbios: SmbiosRead, units: List) -> IdentityBindInputs {\n IdentityBindInputs { fru: fru, smbios: smbios, other_units: units }\n}\n\nfn forged_fru(fields: FruIdentityFields) -> RecordedFruObservation {\n RecordedFruObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", fields: fields }\n}\n\nfn forged_smbios(attribution: SolSessionAttribution) -> RecordedSmbiosObservation {\n RecordedSmbiosObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", sol_session: attribution, serial: \"B810301000412080005AJ0C1\" }\n}\n\nfn forged_agreement(fru: RecordedFruObservation, smbios: RecordedSmbiosObservation) -> BoardSerialAgreement {\n BoardSerialAgreement { fru: fru, smbios: smbios, serial: \"B810301000412080005AJ0C1\" }\n}\n" +data forged_probe_source: String = "module probe_arrival_converge_forged\n\nimport std.types { Bool, Int, List, NonEmptyStr, String }\nimport std.decl_ref { decl_ref }\nimport gunbc.machine_intake_phase { Arrival, AccessDiscover, IntakePhase }\nimport gunbc.machine_intake_subject { MachineIntakeSubject, BoardSerialObservation, AssemblyManifest, UnitKey }\nimport gunbc.machine_intake_bmc_rotation_route { BmcRotationRouteStanding }\nimport gunbc.machine_intake_mtjade1_factory_network { ObservedBmcNetwork }\nimport gunbc.machine_intake_mtjade1_access_observation {\n CurrentManagerRead, RecordedManagerIdentityObservation, ControllerClockReading, current_manager_read_of,\n FruRead, SmbiosRead, FruIdentityFields, RecordedFruObservation, RecordedSmbiosObservation, SolSessionAttribution,\n}\nimport gunbc.fleet.convergence_fold {\n AdmittedConvergencePlan, RankedStep, StepInstanceKey, ConvergenceRunId, StepSubjectKey, ConvergenceOrderAuthority, ConvergencePlanningAuthority,\n ConvergenceReceiptProjection, ConvergenceRunLedger, ConvergedRun, StepInstanceStanding,\n convergence_planning_authority, convergence_receipt_projection,\n}\nimport gunbc.machine_intake_arrival_converge {\n AccessDiscoverEstablished, IdentityBoundProvisional, ReadOnlyPhaseRemedy, AccessObservation,\n IdentityBindInputs, ArrivalStepReceipt, ArrivalStepRefusal, ArrivalStepIncomplete, BoardSerialAgreement,\n}\n\nfn forged_access(key: StepInstanceKey, access: AccessObservation, route: BmcRotationRouteStanding) -> AccessDiscoverEstablished {\n AccessDiscoverEstablished { key: key, access: access, route: route }\n}\n\nfn forged_identity(key: StepInstanceKey, subject: MachineIntakeSubject) -> IdentityBoundProvisional {\n IdentityBoundProvisional { key: key, consumed_access: key, subject: subject }\n}\n\nfn forged_plan(steps: List>, key: StepInstanceKey) -> AdmittedConvergencePlan {\n AdmittedConvergencePlan { authority: key.step_identity, steps: steps }\n}\n\nfn forged_remedy() -> ReadOnlyPhaseRemedy {\n ReadOnlyPhaseRemedy { phase: AccessDiscover }\n}\n\nfn any_rank(phase: IntakePhase) -> Int? {\n Present { value: 0 }\n}\n\nfn authored_order() -> ConvergenceOrderAuthority {\n ConvergenceOrderAuthority { authority: decl_ref(module_path: \"gunbc.machine_intake_phase\", decl_name: \"arrival_phases_all\"), rank_of: any_rank }\n}\n\nfn forged_planning_literal() -> ConvergencePlanningAuthority {\n ConvergencePlanningAuthority { order: authored_order() }\n}\n\nfn forged_planning_via_mint() -> ConvergencePlanningAuthority {\n convergence_planning_authority(order: authored_order())\n}\n\nfn rekey(r: ArrivalStepReceipt) -> StepInstanceKey {\n StepInstanceKey { run: \"forged\" as ConvergenceRunId, step_identity: decl_ref(module_path: \"gunbc.machine_intake_arrival_converge\", decl_name: \"access_discover\"), subject: \"mtjade1\" as StepSubjectKey }\n}\n\nfn consumed_nothing(r: ArrivalStepReceipt) -> List {\n []\n}\n\nfn auth_never(r: ArrivalStepReceipt) -> Bool {\n false\n}\n\nfn forged_projection_literal() -> ConvergenceReceiptProjection {\n ConvergenceReceiptProjection { key_of: rekey, consumed_of: consumed_nothing, authorization_required_of: auth_never }\n}\n\nfn forged_projection_via_mint() -> ConvergenceReceiptProjection {\n convergence_receipt_projection(key_of: rekey, consumed_of: consumed_nothing, authorization_required_of: auth_never)\n}\n\nfn forged_ledger(key: StepInstanceKey, instances: List>) -> ConvergenceRunLedger {\n ConvergenceRunLedger { run: key.run, subject: key.subject, order_authority: key.step_identity, instances: instances }\n}\n\nfn forged_converged_run(ledger: ConvergenceRunLedger) -> ConvergedRun {\n ConvergedRun { ledger: ledger }\n}\n\nfn forged_manager_read(identity: RecordedManagerIdentityObservation, clock: ControllerClockReading) -> CurrentManagerRead {\n CurrentManagerRead { identity: identity, controller_clock: clock }\n}\n\nfn forged_manager_read_via_mint(content: String, endpoint: ObservedBmcNetwork) -> CurrentManagerRead {\n current_manager_read_of(content: content, expected_sha256: \"00\" as NonEmptyStr, endpoint: endpoint, link: none, capture_path: \"forged\" as NonEmptyStr)\n}\n\nfn forged_identity_inputs(fru: FruRead, smbios: SmbiosRead, units: List) -> IdentityBindInputs {\n IdentityBindInputs { fru: fru, smbios: smbios, other_units: units }\n}\n\nfn forged_fru(fields: FruIdentityFields) -> RecordedFruObservation {\n RecordedFruObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", fields: fields }\n}\n\nfn forged_smbios(attribution: SolSessionAttribution) -> RecordedSmbiosObservation {\n RecordedSmbiosObservation { subject: \"mtjade1\", capture_path: \"forged\", capture_sha256: \"00\", sol_session: attribution, serial: \"B810301000412080005AJ0C1\" }\n}\n\nfn forged_agreement(fru: RecordedFruObservation, smbios: RecordedSmbiosObservation) -> BoardSerialAgreement {\n BoardSerialAgreement { fru: fru, smbios: smbios, serial: \"B810301000412080005AJ0C1\" }\n}\n" data harness_control_source: String = "module probe_arrival_converge_harness_control\nimport gunbc.fleet.convergence_fold { ConvergencePlanAdmission, admit_convergence_plan }\nimport gunbc.machine_intake_phase { IntakePhase }\nimport gunbc.machine_intake_arrival_converge { arrival_planning_authority, arrival_receipt_projection, ArrivalStepReceipt }\nimport gunbc.fleet.convergence_fold { ConvergenceReceiptProjection }\nimport gunbc.machine_intake_mtjade1_access_observation { CurrentManagerRead, read_mtjade1_current_manager_read }\nfn admission() -> ConvergencePlanAdmission { admit_convergence_plan(planning: arrival_planning_authority(), steps: []) }\nfn projection() -> ConvergenceReceiptProjection { arrival_receipt_projection() }\nfn read() -> CurrentManagerRead { read_mtjade1_current_manager_read() }\n" @@ -91,3 +91,18 @@ test fn authored_arrival_inputs_are_refused() -> Bool { && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "RecordedSmbiosObservation") >= 1 && blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "BoardSerialAgreement") >= 1 } + +data outside_mtjade1_bmc_reading_probe_source: String = "module probe_mtjade1_bmc_reading_outside\nimport std.types { String }\nimport test.claim.machine_intake_arrival_converge_witness { mtjade1_intake_subject, mtjade1_dry_applied_bmc, mtjade1_fetched_generation, mtjade1_bmc_goal }\nimport gunbc.machine_intake_arrival_converge { BmcSecureApplyInputs }\nimport gunbc.machine_intake_bmc_secure { ManagedCredentialGenerationFetched }\nfn leak_apply() -> BmcSecureApplyInputs? { mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) }\nfn leak_generation() -> ManagedCredentialGenerationFetched? { mtjade1_fetched_generation(current: mtjade1_bmc_goal().managed, secret: \"bmc-lab-o1b-gunbc\", version: \"2\", bytes: \"x\") }\n" + +data bmc_account_state_observation_literal_probe_source: String = "module probe_bmc_account_state_observation_literal\nimport std.types { List }\nimport std.scoped_authorization { AttemptIdentity }\nimport gunbc.clock_read { ObserverClockInstant }\nimport gunbc.machine_intake_receipt { EvidenceRef }\nimport gunbc.machine_intake_subject { MachineIntakeSubject }\nimport gunbc.machine_intake_bmc_secure {\n BmcAccountStateObservation, ManagedCredentialReference, ObservedCredentialProbe, ObservedPublishedLanProbe, ObservedPublishedAccount, ControllerClockReading,\n}\nimport extdeps.bmc.endpoint { BmcControllerEndpoint }\nimport extdeps.bmc.capability { BmcFirmwareReleaseIdentity }\nimport extdeps.bmc.ipmi_channel { IpmiUserId, IpmiControllerChannelCensus }\nfn leak(\n subject: MachineIntakeSubject,\n endpoint: BmcControllerEndpoint,\n firmware: BmcFirmwareReleaseIdentity,\n managed: ManagedCredentialReference,\n managed_user: IpmiUserId,\n attempt: AttemptIdentity,\n read_floor: ObserverClockInstant,\n managed_probe: ObservedCredentialProbe,\n channel_census: IpmiControllerChannelCensus,\n census_evidence: EvidenceRef,\n census_observed_at: ObserverClockInstant,\n published_probes: List,\n published_user: IpmiUserId,\n published_account: ObservedPublishedAccount,\n break_glass: ManagedCredentialReference,\n break_glass_probe: ObservedCredentialProbe,\n controller_clock: ControllerClockReading?,\n) -> BmcAccountStateObservation {\n BmcAccountStateObservation {\n subject: subject,\n endpoint: endpoint,\n firmware: firmware,\n managed: managed,\n managed_user: managed_user,\n attempt: attempt,\n read_floor: read_floor,\n managed_probe: managed_probe,\n channel_census: channel_census,\n census_evidence: census_evidence,\n census_observed_at: census_observed_at,\n published_probes: published_probes,\n published_user: published_user,\n published_account: published_account,\n break_glass: break_glass,\n break_glass_probe: break_glass_probe,\n controller_clock: controller_clock,\n }\n}\n" + +test fn the_mtjade1_bmc_reading_helpers_refuse_an_outside_caller() -> Bool { + let c = compile_dag_diagnostic_census(outside_mtjade1_bmc_reading_probe_source) + blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "mtjade1_dry_applied_bmc") >= 1 + && blocking_count_for_class_and_subject(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "mtjade1_fetched_generation") >= 1 +} + +test fn a_bmc_account_state_observation_literal_is_refused_outside_its_mint() -> Bool { + let c = compile_dag_diagnostic_census(bmc_account_state_observation_literal_probe_source) + blocking_count_for_class_and_subject(c: c, wanted: "SoleConstructorViolation", subject: "BmcAccountStateObservation") >= 1 +} diff --git a/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag b/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag index 2849178fd7f..22e510c0e60 100644 --- a/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag +++ b/dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag @@ -1,6 +1,6 @@ module test.claim.machine_intake_arrival_converge_witness -import std.types { Bool, Int, List, NonEmptyStr, String } +import std.types { Bool, EpochMs, Int, List, NonEmptyStr, Secret, String } import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq } import std.scoped_authorization { AttemptIdentity } import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } @@ -8,11 +8,12 @@ import v2.std.algebra { filter, length } import extdeps.crypto.mac { MacKeyId } import extdeps.bmc.endpoint { AmiMegaRac, OpenBmc, BmcControllerEndpoint } import gunbc.auth.approval_capability { ApprovalCapabilityClaims, ProposeApprove, approval_capability_protocol } +import product.host_identity { HostIdentity, host_identity_eq } import gunbc.auth.approval_broker { Redemption, RedemptionAdmitted } -import gunbc.machine_intake_phase { Arrival, AccessDiscover, IdentityBindProvisional, PriorLifeBoundary, BmcSecure, IntakePhase } +import gunbc.machine_intake_phase { Arrival, AccessDiscover, IdentityBindProvisional, PriorLifeBoundary, BmcSecure, BootDeliveryEstablish, IntakePhase, machine_qualification_policy } import gunbc.machine_intake_subject { AssemblyManifest, BoardSerialObservation, BmcFru, HostSmbios, ChassisComponent, ComponentIdentity, BoardSerialAbsent, - FirmwareEntry, FirmwareManifest, UnitKey, + FirmwareEntry, FirmwareManifest, UnitKey, MachineIntakeSubject, IntakeAttemptId, qualification_subject_of, } import gunbc.machine_intake_mtjade1_access_observation { @@ -24,6 +25,7 @@ import gunbc.machine_intake_bmc_rotation_route { RedfishAccountPasswordWrite, IpmiSetUserPassword, IpmiSetUserPrivilegeLimit, ObservedSurfaceRead, PublicStandardOperation, RotationApplyAdmitted, RotationApplyRouteNotGrounded, rotation_apply_authority, rotation_route_request_identity, rotation_route_is_grounded, admit_rotation_apply, + rotation_route_ungrounded, rotation_route_from_citation, route_qualification_authority, } import gunbc.host_convergence_census { HostConvergenceCensus, CensusWellFormed, host_convergence_census_rows, host_convergence_census_standing, @@ -40,14 +42,27 @@ import gunbc.fleet.convergence_fold { admit_convergence_plan, classify_convergence_plan, PlanClassifiedAdmissible, PlanClassifiedRefused, ConvergenceReceiptProjection, convergence_receipt_projection, fold_convergence_run, step_instance_key, step_outcome_receipt, step_outcome_refusal, + ungated_readonly_step, AuthorizationUndischarged, instance_authorization, + step_instance_key_eq, InstanceAuthorization, } import gunbc.machine_intake_prior_life_boundary { DryPriorLifeWorld, DryArchiveStore, DryArchiveStoreLosesWrites, ArchiveWrittenButNotReadBack, ArchiveWritten, LogsArchivedWithBaselineCursor, mt_jade_platform_ref, prior_life_receipt_archive, prior_life_receipt_application, prior_life_receipt_boundary, prior_life_receipt_realization, prior_life_receipt_consumed_identity, prior_life_archive_digest, baseline_cursor_archive, baseline_cursor_sel_final_record, } -import std.content_hash { content_hash_equal } +import std.content_hash { content_hash_equal, content_hash_of_value } +import gunbc.machine_intake_receipt { EvidenceRef } import test.claim.machine_intake_prior_life_boundary_witness { prior_life_minimal_dry_world } +import gunbc.auth.standing_operator_grant { + mtjade1_live_standing_grant, standing_grant_covers, StandingGrantHost, StandingBmcSecureAccountWrite, + StandingOperatorGrant, +} +import gunbc.auth.authorization_pattern_selection { + InterlockPending, InterlockedBy, StandingDestructiveAuthorization, + select_authorization_pattern, StandingRulingUnderInterlock, NoWitnessDischarge, + PatternSelected, OperatorApprovedCapability, AuthorizationPatternSelection, +} +import gunbc.fleet_host_identity { operator_host_mtjade1, operator_host_mtcollins1 } import gunbc.machine_intake_arrival_converge { ArrivalPrefixVerdict, ArrivalRunFolded, ArrivalPlanRefused, ArrivalPrefixUnstepped, ArrivalStepReceipt, AccessDiscoverReceipt, IdentityBindReceipt, PriorLifeBoundaryReceipt, ArrivalStepRefusal, @@ -57,8 +72,38 @@ import gunbc.machine_intake_arrival_converge { access_discover_step_ref, identity_bind_provisional_step_ref, arrival_order_authority, arrival_planning_authority, arrival_prefix_through, arrival_prefix_steps, ArrivalPrefixStepped, ArrivalPrefixPhaseUnstepped, arrival_prefix_last, arrival_receipt_projection, access_discover, identity_bind_provisional, - converge_mtjade1_arrival_prefix, converge_arrival_prefix, mtjade1_identity_bind_inputs, + converge_mtjade1_arrival_prefix, converge_mtjade1_arrival_through_bmc_secure, converge_arrival_prefix, converge_arrival_through_bmc_secure, mtjade1_identity_bind_inputs, + bmc_secure_step_ref, BmcSecureReceipt, + BmcSecureInputs, BmcSecureApplyInputs, BmcSecureAuthorizationUndischarged, BmcSecureApplyInputsMissing, + BmcSecureApplicationForAnotherInstance, BmcSecureApplicationNotTheInspectedTransition, + grant_discharges_bmc_secure_account_write, + capability_discharges_bmc_secure_account_write, + discharge_bmc_secure_apply, + bound_bmc_secure_host, + bmc_secure_bound, +} +import gunbc.machine_intake_bmc_secure { + BmcSecureGoal, BmcAccountStateObservation, dry_read_bmc_account_state, dry_apply_bmc_account_plan, plan_bmc_account_action, + BmcAccountPlanned, BmcAccountPlanRefused, PublishedAccountRetired, ManagedCredentialReference, + BmcSecurePhaseNoop, BmcSecurePhaseApplied, ControllerClockReading, + observation_with_controller_clock, apply_with_diverged_controller_clock, controller_clock_reading_same, + admit_stored_generation, admit_fetched_generation, dry_bmc_account_instant, + GenerationStored, GenerationStoreRefused, GenerationFetched, GenerationFetchRefused, ManagedCredentialGenerationFetched, } +import gunbc.auth.secret_ref_credential { SecretCredentialFetch, SecretCredentialReady } +import extdeps.cloud.gcp.secret_manager { SmResolvedVersionIdentity } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { uri_https } +import gunbc.deployment_risk { TestRisk } +import extdeps.bmc.types { AccountRoleAdministrator } +import extdeps.bmc.capability { BmcFirmwareReleaseIdentity, bmc_firmware_release_identity_of_wire } +import extdeps.bmc.ipmi_channel { + IpmiControllerChannelCensus, IpmiMedium8023Lan, IpmiMediumSerialAsync, IpmiPrivilegeNoAccess, IpmiPrivilegeAdministrator, + IpmiUserId, ipmi_controller_channel_census, ipmi_lan_channel_member, ipmi_non_lan_channel_member, ipmi_user_channel_access, +} +import extdeps.network.ipv4 { ipv4_address } +import extdeps.cloud.gcp.secret_ref { HashPending, SecretRef } +import gunbc.bmc_model { BmcWorld, BmcIpmiUser, BmcPowerOn, bmc_world, bmc_with_ipmi_users, bmc_with_ipmi_user_access } data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree @@ -109,6 +154,7 @@ fn access_established_as_read(s: StepInstanceStanding false PriorLifeBoundaryReceipt { receipt: _ } => false + BmcSecureReceipt { receipt: _ } => false } InstanceRefused { key: _, cause: _ } => false InstanceIncomplete { key: _, cause: _ } => false @@ -132,6 +178,7 @@ fn identity_bound_from_committed_captures(s: StepInstanceStanding false PriorLifeBoundaryReceipt { receipt: _ } => false + BmcSecureReceipt { receipt: _ } => false } InstanceRefused { key: _, cause: _ } => false InstanceIncomplete { key: _, cause: _ } => false @@ -169,6 +216,7 @@ fn prior_life_archived_from_the_bound_subject(s: StepInstanceStanding false IdentityBindReceipt { receipt: _ } => false + BmcSecureReceipt { receipt: _ } => false } InstanceRefused { key: _, cause: _ } => false InstanceIncomplete { key: _, cause: _ } => false @@ -201,6 +249,407 @@ test fn w_mtjade1_converges_the_prefix_through_its_dry_prior_life_archive() -> B } } +data mtjade1_bmc_read_at: EpochMs = 1791072000000 +data mtjade1_bmc_plan_at: EpochMs = 1791072030000 +data mtjade1_bmc_apply_at: EpochMs = 1791072040000 +data mtjade1_bmc_readback_at: EpochMs = 1791072050000 +data mtjade1_managed_ipmi_user: IpmiUserId = 3 +data mtjade1_published_ipmi_user: IpmiUserId = 2 +data mtjade1_managed_password_v2: String = "managed-generation-2!" +data mtjade1_route_fixture_citation: ExternalAuthority = ExternalAuthority { + uri: uri_https(locator: "fixture-not-an-authority.invalid/test.claim.machine_intake_arrival_converge_witness/mtjade1-route" as NonEmptyStr), +} + +fn mtjade1_intake_subject_for(attempt: IntakeAttemptId) -> MachineIntakeSubject { + MachineIntakeSubject { + subject: qualification_subject_of(unit_key: "B810301000412080005AJ0C1" as UnitKey, assembly: expected_mtjade1_assembly, firmware: expected_mtjade1_firmware), + attempt_id: attempt, + } +} + +fn mtjade1_intake_subject() -> MachineIntakeSubject { + mtjade1_intake_subject_for(attempt: "o1c1-witness-run-a" as IntakeAttemptId) +} + +fn mtjade1_bmc_endpoint() -> BmcControllerEndpoint { + BmcControllerEndpoint { host: "192.168.1.246" } +} + +fn mtjade1_bmc_firmware() -> BmcFirmwareReleaseIdentity { + bmc_firmware_release_identity_of_wire(family: AmiMegaRac, wire: "2.11.104000" as NonEmptyStr) +} + +fn cited_mtjade1_managed_route() -> BmcRotationRouteStanding + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), + ] +{ + rotation_route_from_citation( + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + request: IpmiSetUserPassword { user: mtjade1_managed_ipmi_user }, + citation: mtjade1_route_fixture_citation, + ) +} + +fn cited_mtjade1_published_route() -> BmcRotationRouteStanding + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), + ] +{ + rotation_route_from_citation( + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + request: IpmiSetUserPassword { user: mtjade1_published_ipmi_user }, + citation: mtjade1_route_fixture_citation, + ) +} + +fn mtjade1_bmc_goal() -> BmcSecureGoal { + BmcSecureGoal { + managed: ManagedCredentialReference { + account: "gunbc", + role: AccountRoleAdministrator, + secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-gunbc", version: "1", hash_state: HashPending }, + credential_epoch: 1, + }, + published_break_glass: ManagedCredentialReference { + account: "admin", + role: AccountRoleAdministrator, + secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-admin", version: "4", hash_state: HashPending }, + credential_epoch: 4, + }, + policy: machine_qualification_policy(admits: TestRisk), + } +} + +fn mtjade1_bmc_goal_with_break_glass_epoch(epoch: Int, version: String) -> BmcSecureGoal { + BmcSecureGoal { + managed: mtjade1_bmc_goal().managed, + published_break_glass: ManagedCredentialReference { + account: "admin", + role: AccountRoleAdministrator, + secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-admin", version: version, hash_state: HashPending }, + credential_epoch: epoch, + }, + policy: machine_qualification_policy(admits: TestRisk), + } +} + +fn mtjade1_grant_without_bmc_secure_effect() -> StandingOperatorGrant { + let g = mtjade1_live_standing_grant + StandingOperatorGrant { + identity: g.identity, + principal: g.principal, + ruled_at: g.ruled_at, + ruling: g.ruling, + scope: g.scope, + effects: [], + } +} + +fn mtjade1_bmc_census(published_lan_privilege_closed: Bool) -> IpmiControllerChannelCensus { + let lan_privilege = if published_lan_privilege_closed { IpmiPrivilegeNoAccess } else { IpmiPrivilegeAdministrator } + ipmi_controller_channel_census( + members: [ + ipmi_lan_channel_member(channel: 1, medium: IpmiMedium8023Lan, address: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 246)), + ipmi_non_lan_channel_member(channel: 2, medium: IpmiMediumSerialAsync), + ipmi_lan_channel_member(channel: 8, medium: IpmiMedium8023Lan, address: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 247)), + ], + user_access: [ + ipmi_user_channel_access(channel: 1, user: mtjade1_published_ipmi_user, privilege: lan_privilege), + ipmi_user_channel_access(channel: 2, user: mtjade1_published_ipmi_user, privilege: IpmiPrivilegeNoAccess), + ipmi_user_channel_access(channel: 8, user: mtjade1_published_ipmi_user, privilege: lan_privilege), + ], + ) +} + +fn mtjade1_account_world(users: List, published_lan_privilege_closed: Bool) -> BmcWorld { + let census_value = mtjade1_bmc_census(published_lan_privilege_closed: published_lan_privilege_closed) + bmc_with_ipmi_user_access( + world: bmc_with_ipmi_users(world: bmc_world(power: BmcPowerOn), users: users), + rows: census_value.user_access, + ) +} + +fn mtjade1_version_identity(secret: String, version: String) -> SmResolvedVersionIdentity { + join(["projects/gunbai-secrets/secrets/", secret, "/versions/", version], "") as SmResolvedVersionIdentity +} + +fn mtjade1_ready(secret: String, version: String, bytes: String) -> SecretCredentialFetch { + SecretCredentialReady { credential: bytes as Secret, resolved_version: mtjade1_version_identity(secret: secret, version: version) } +} + +fn mtjade1_fetched_generation( + current: ManagedCredentialReference, + secret: String, + version: String, + bytes: String, +) -> ManagedCredentialGenerationFetched? + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "mtjade1_dry_applied_bmc"), + ] +{ + let store_at = dry_bmc_account_instant(millis: 1791072010000) + let fetch_at = dry_bmc_account_instant(millis: 1791072020000) + match admit_stored_generation(current: current, added: mtjade1_version_identity(secret: secret, version: version), stored_at: store_at) { + GenerationStoreRefused { cause: _ } => none + GenerationStored { stored: st } => + match admit_fetched_generation(stored: st, fetch: mtjade1_ready(secret: secret, version: version, bytes: bytes), fetched_at: fetch_at) { + GenerationFetchRefused { cause: _ } => none + GenerationFetched { fetched: f } => Present { value: f } + } + } +} + +fn mtjade1_rotation_approval(s: BmcRotationRouteStanding, user: IpmiUserId) -> Redemption { + RedemptionAdmitted { + claims: ApprovalCapabilityClaims { + protocol: approval_capability_protocol, + issuer: "gunbc-approval-broker" as NonEmptyStr, + audience: "srv1" as NonEmptyStr, + authority: rotation_apply_authority, + escalation_id: "o1c3b-apply-witness" as NonEmptyStr, + request_revision: rotation_route_request_identity(standing: s, request: IpmiSetUserPassword { user: user }), + decision: ProposeApprove, + attempt: "o1c1-witness-run-a" as AttemptIdentity, + issued_at: "2026-10-04T00:00:00Z", + expires_at: "2026-10-04T00:15:00Z", + key_id: "broker-2026-10" as MacKeyId, + }, + decided_by: "operator" as NonEmptyStr, + } +} + +fn mtjade1_dry_applied_bmc(subject: MachineIntakeSubject) -> BmcSecureApplyInputs? + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "bmc_secure_bound_refuses_foreign_apply"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_without_authorization_refuses_after_a_real_apply"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_uncovered_grant_falls_through_to_capability"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_uncovered_grant_refuses_a_capability_for_another_request"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_channel_state_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_a_present_controller_clock_over_absent_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_a_foreign_bound_host_key_cannot_mint_from_this_instance_controller"), + ] +{ + let census_value = mtjade1_bmc_census(published_lan_privilege_closed: true) + let world = mtjade1_account_world( + users: [BmcIpmiUser { id: 3, password: "managed-generation-1!" }, BmcIpmiUser { id: 2, password: "admin" }], + published_lan_privilege_closed: true, + ) + let reading = dry_read_bmc_account_state( + world: world, + subject: subject, + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: mtjade1_bmc_goal().managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: "managed-generation-1!", + census: census_value, + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: mtjade1_bmc_goal().published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: (subject.attempt_id as NonEmptyStr) as AttemptIdentity, + read_at_millis: mtjade1_bmc_read_at, + ) + match mtjade1_fetched_generation(current: mtjade1_bmc_goal().managed, secret: "bmc-lab-o1b-gunbc", version: "2", bytes: mtjade1_managed_password_v2) { + Absent => none + Present { value: mg } => + match mtjade1_fetched_generation( + current: ManagedCredentialReference { + account: "admin", + role: AccountRoleAdministrator, + secret: SecretRef { project: "gunbai-secrets", secret: "bmc-lab-o1b-admin", version: "3", hash_state: HashPending }, + credential_epoch: 3, + }, + secret: "bmc-lab-o1b-admin", + version: "4", + bytes: "break-glass-generation-4!", + ) { + Absent => none + Present { value: bg } => { + let managed_route = cited_mtjade1_managed_route() + let published_route = cited_mtjade1_published_route() + match plan_bmc_account_action( + subject: subject, + goal: mtjade1_bmc_goal(), + reading: reading, + managed_user: mtjade1_managed_ipmi_user, + managed_route: managed_route, + managed_approval: mtjade1_rotation_approval(s: managed_route, user: mtjade1_managed_ipmi_user), + managed_generation: mg, + published_route: published_route, + published_approval: mtjade1_rotation_approval(s: published_route, user: mtjade1_published_ipmi_user), + published_generation: bg, + channel_close: none, + planned_at: dry_bmc_account_instant(millis: mtjade1_bmc_plan_at), + ) { + BmcAccountPlanRefused { cause: _ } => none + BmcAccountPlanned { plan: p } => { + let step = dry_apply_bmc_account_plan( + world: world, + plan: p, + managed_fetch: mtjade1_ready(secret: "bmc-lab-o1b-gunbc", version: "2", bytes: mtjade1_managed_password_v2), + published_fetch: mtjade1_ready(secret: "bmc-lab-o1b-admin", version: "4", bytes: "break-glass-generation-4!"), + applied_at_millis: mtjade1_bmc_apply_at, + ) + let post_read = dry_read_bmc_account_state( + world: step.world, + subject: subject, + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: p.goal.managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: mtjade1_managed_password_v2, + census: census_value, + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: p.goal.published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: (subject.attempt_id as NonEmptyStr) as AttemptIdentity, + read_at_millis: mtjade1_bmc_readback_at, + ) + Present { value: BmcSecureApplyInputs { application: step.application, post_read: post_read } } + } + } + } + } + } +} + +fn mtjade1_bmc_inputs(reading: BmcAccountStateObservation, grant: StandingOperatorGrant?, apply: BmcSecureApplyInputs?, capability: Redemption?) -> BmcSecureInputs { + BmcSecureInputs { + goal: mtjade1_bmc_goal(), + reading: reading, + grant: grant, + capability: capability, + apply: apply, + } +} + +fn bmc_secure_applied_established(s: StepInstanceStanding) -> Bool { + match s { + InstanceConverged { key: k, receipt: r } => + declaration_ref_eq(a: k.step_identity, b: bmc_secure_step_ref) + && match r { + BmcSecureReceipt { receipt: b } => + match b.phase.decision { + BmcSecurePhaseApplied { plan: _, application: _, post_read: _ } => true + BmcSecurePhaseNoop { observation: _ } => false + } + AccessDiscoverReceipt { receipt: _ } => false + IdentityBindReceipt { receipt: _ } => false + PriorLifeBoundaryReceipt { receipt: _ } => false + } + _ => false + } +} + +fn bmc_secure_noop_established(s: StepInstanceStanding) -> Bool { + match s { + InstanceConverged { key: k, receipt: r } => + declaration_ref_eq(a: k.step_identity, b: bmc_secure_step_ref) + && match r { + BmcSecureReceipt { receipt: b } => + match b.phase.decision { + BmcSecurePhaseNoop { observation: _ } => true + BmcSecurePhaseApplied { plan: _, application: _, post_read: _ } => false + } + AccessDiscoverReceipt { receipt: _ } => false + IdentityBindReceipt { receipt: _ } => false + PriorLifeBoundaryReceipt { receipt: _ } => false + } + _ => false + } +} + +test fn w_mtjade1_converges_through_bmc_secure_noop_on_the_real_prefix() -> Bool { + let census_value = mtjade1_bmc_census(published_lan_privilege_closed: true) + let reading = dry_read_bmc_account_state( + world: mtjade1_account_world( + users: [BmcIpmiUser { id: 3, password: "managed-generation-1!" }, BmcIpmiUser { id: 2, password: "break-glass-generation-4!" }], + published_lan_privilege_closed: true, + ), + subject: mtjade1_intake_subject(), + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: mtjade1_bmc_goal().managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: "managed-generation-1!", + census: census_value, + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: mtjade1_bmc_goal().published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: "o1c1-witness-run-a" as AttemptIdentity, + read_at_millis: mtjade1_bmc_read_at, + ) + match converge_mtjade1_arrival_through_bmc_secure(run: run_a, prior_life: prior_life_minimal_dry_world(), bmc: mtjade1_bmc_inputs(reading: reading, grant: none, apply: none, capability: none)) { + ArrivalRunFolded { verdict: v } => + match v { + RunConverged { run: r } => + length(xs: r.ledger.instances) == 4 + && match r.ledger.instances.first() { Present { value: s } => access_established_as_read(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: identity_bind_provisional_step_ref)) |> first() { Present { value: s } => identity_bound_from_committed_captures(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: prior_life_boundary_step_ref)) |> first() { Present { value: s } => prior_life_archived_from_the_bound_subject(s: s) Absent => false } + && match r.ledger.instances.last() { Present { value: s } => bmc_secure_noop_established(s: s) Absent => false } + _ => false + } + _ => false + } +} + +test fn w_mtjade1_bmc_secure_apply_inputs_missing_refuses_on_the_real_path() -> Bool { + let census_value = mtjade1_bmc_census(published_lan_privilege_closed: true) + let reading = dry_read_bmc_account_state( + world: mtjade1_account_world( + users: [BmcIpmiUser { id: 3, password: "managed-generation-1!" }, BmcIpmiUser { id: 2, password: "admin" }], + published_lan_privilege_closed: true, + ), + subject: mtjade1_intake_subject(), + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: mtjade1_bmc_goal().managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: "managed-generation-1!", + census: census_value, + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: mtjade1_bmc_goal().published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: "o1c1-witness-run-a" as AttemptIdentity, + read_at_millis: mtjade1_bmc_read_at, + ) + match converge_mtjade1_arrival_through_bmc_secure(run: run_a, prior_life: prior_life_minimal_dry_world(), bmc: mtjade1_bmc_inputs(reading: reading, grant: none, apply: none, capability: none)) { + ArrivalRunFolded { verdict: v } => + match v { + RunStopped { ledger: l, at: at } => + declaration_ref_eq(a: at.step_identity, b: bmc_secure_step_ref) + && match l.instances.last() { + Present { value: s } => match s { + InstanceRefused { key: _, cause: c } => match c { + DomainRefused { cause: d } => match d { BmcSecureApplyInputsMissing => true _ => false } + AuthorizationUndischarged => false + _ => false + } + _ => false + } + Absent => false + } + _ => false + } + _ => false + } +} + // AN ARCHIVE WRITE THE STORE LOSES LEAVES THE RUN INCOMPLETE, NOT STOPPED AND NOT CONVERGED, at the // PriorLifeBoundary instance, which records the write as written-but-not-read-back. Same real route, // the store the only difference. @@ -315,8 +764,8 @@ test fn w_the_roster_is_the_three_phase_prefix_of_the_authority() -> Bool { // A phase of the prefix with no step refuses rather than being skipped: through BmcSecure the prefix // reaches BmcSecure itself, which has no step in this cut (O1c-3 brings it with its gate). test fn w_a_prefix_phase_with_no_step_refuses() -> Bool { - match arrival_prefix_steps(phases: arrival_prefix_through(last: BmcSecure)) { - ArrivalPrefixPhaseUnstepped { phase: p } => p == Arrival { phase: BmcSecure } + match arrival_prefix_steps(phases: arrival_prefix_through(last: BootDeliveryEstablish)) { + ArrivalPrefixPhaseUnstepped { phase: p } => p == Arrival { phase: BootDeliveryEstablish } ArrivalPrefixStepped { steps: _ } => false } } @@ -331,11 +780,11 @@ fn real_steps() -> List> { } fn access_step_bound_to(phase: IntakePhase) -> ConvergenceStep { - ConvergenceStep { identity: access_discover_step_ref, order_member: phase, preconditions: [] } + ungated_readonly_step(identity: access_discover_step_ref, order_member: phase, preconditions: []) } fn identity_step_with(preconditions: List) -> ConvergenceStep { - ConvergenceStep { identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: preconditions } + ungated_readonly_step(identity: identity_bind_provisional_step_ref, order_member: Arrival { phase: IdentityBindProvisional }, preconditions: preconditions) } fn plan_refusal(admission: ConvergencePlanAdmission) -> ConvergencePlanRefusal? { @@ -381,7 +830,7 @@ test fn w_an_unknown_precondition_refuses() -> Bool { // converge_arrival_prefix is a real declaration with no census row: as a step it refuses. test fn w_a_step_with_no_census_row_refuses() -> Bool { let uncensused = decl_ref(module_path: "gunbc.machine_intake_arrival_converge", decl_name: "converge_arrival_prefix") - match plan_refusal(admission: admit_convergence_plan(planning: arrival_planning_authority(), steps: [ConvergenceStep { identity: uncensused, order_member: Arrival { phase: AccessDiscover }, preconditions: [] }])) { + match plan_refusal(admission: admit_convergence_plan(planning: arrival_planning_authority(), steps: [ungated_readonly_step(identity: uncensused, order_member: Arrival { phase: AccessDiscover }, preconditions: [])])) { Present { value: c } => match c { StepMissingFromCensus { step: s } => declaration_ref_eq(a: s, b: uncensused) _ => false } Absent => false } @@ -409,14 +858,14 @@ fn real_access(run: ConvergenceRunId, subject: StepSubjectKey, read: CurrentMana fn established_access(o: StepOutcome) -> AccessDiscoverEstablished? { match step_outcome_receipt(outcome: o) { - Present { value: r } => match r { AccessDiscoverReceipt { receipt: a } => Present { value: a } IdentityBindReceipt { receipt: _ } => none PriorLifeBoundaryReceipt { receipt: _ } => none } + Present { value: r } => match r { AccessDiscoverReceipt { receipt: a } => Present { value: a } IdentityBindReceipt { receipt: _ } => none PriorLifeBoundaryReceipt { receipt: _ } => none BmcSecureReceipt { receipt: _ } => none } Absent => none } } fn fold_real(run: ConvergenceRunId, subject: StepSubjectKey, outcomes: List>) -> ConvergenceRunVerdict? { match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { - ConvergencePlanAdmitted { plan: p } => Present { value: fold_convergence_run(plan: p, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection()) } + ConvergencePlanAdmitted { plan: p } => Present { value: fold_convergence_run(plan: p, run: run, subject: subject, outcomes: outcomes, projection: arrival_receipt_projection(), discharges: []) } ConvergencePlanRefused { cause: _ } => none } } @@ -471,6 +920,583 @@ fn probe_consumed(r: ProbeReceipt) -> List { r.consumed } +fn probe_auth_never(r: ProbeReceipt) -> Bool { + false +} + +fn probe_auth_on_bmc_secure(r: ProbeReceipt) -> Bool { + declaration_ref_eq(a: r.key.step_identity, b: bmc_secure_step_ref) +} + +fn four_steps() -> List> { + match arrival_prefix_steps(phases: arrival_prefix_through(last: BmcSecure)) { + ArrivalPrefixStepped { steps: ss } => ss + ArrivalPrefixPhaseUnstepped { phase: _ } => [] + } +} + +test fn w_the_four_step_plan_through_bmc_secure_is_admitted() -> Bool { + match admit_convergence_plan(planning: arrival_planning_authority(), steps: four_steps()) { + ConvergencePlanAdmitted { plan: _ } => length(xs: four_steps()) == 4 + ConvergencePlanRefused { cause: _ } => false + } +} + +test fn w_bmc_secure_noop_needs_no_discharge() -> Bool { + let access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: mtjade1_key) + let outcomes: List> = [ + StepEstablished { receipt: ProbeReceipt { key: access, consumed: [] } }, + StepEstablished { receipt: ProbeReceipt { key: identity, consumed: [access] } }, + StepEstablished { receipt: ProbeReceipt { key: prior, consumed: [identity] } }, + StepEstablished { receipt: ProbeReceipt { key: bmc, consumed: [prior] } }, + ] + match admit_convergence_plan(planning: arrival_planning_authority(), steps: four_steps()) { + ConvergencePlanAdmitted { plan: p } => + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_never), discharges: []) { + RunConverged { run: r } => length(xs: r.ledger.instances) == 4 + _ => false + } + ConvergencePlanRefused { cause: _ } => false + } +} + +test fn w_bmc_secure_apply_without_discharge_refuses() -> Bool { + let access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: mtjade1_key) + let outcomes: List> = [ + StepEstablished { receipt: ProbeReceipt { key: access, consumed: [] } }, + StepEstablished { receipt: ProbeReceipt { key: identity, consumed: [access] } }, + StepEstablished { receipt: ProbeReceipt { key: prior, consumed: [identity] } }, + StepEstablished { receipt: ProbeReceipt { key: bmc, consumed: [prior] } }, + ] + match admit_convergence_plan(planning: arrival_planning_authority(), steps: four_steps()) { + ConvergencePlanAdmitted { plan: p } => + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_on_bmc_secure), discharges: []) { + RunStopped { ledger: l, at: at } => + step_instance_key_eq(a: at, b: bmc) + && match l.instances.last() { + Present { value: s } => match s { + InstanceRefused { key: _, cause: c } => match c { AuthorizationUndischarged => true _ => false } + _ => false + } + Absent => false + } + _ => false + } + ConvergencePlanRefused { cause: _ } => false + } +} + +fn mtjade1_grant_with_interlock_pending() -> StandingOperatorGrant { + let g = mtjade1_live_standing_grant + StandingOperatorGrant { + identity: g.identity, + principal: g.principal, + ruled_at: g.ruled_at, + ruling: StandingDestructiveAuthorization { + ruling_text: g.ruling.ruling_text, + effect_subject: g.ruling.effect_subject, + interlock: InterlockPending { obligation: "hold not named" as NonEmptyStr }, + }, + scope: g.scope, + effects: g.effects, + } +} + +fn mtjade1_grant_with_foreign_interlock() -> StandingOperatorGrant { + let g = mtjade1_live_standing_grant + StandingOperatorGrant { + identity: g.identity, + principal: g.principal, + ruled_at: g.ruled_at, + ruling: StandingDestructiveAuthorization { + ruling_text: g.ruling.ruling_text, + effect_subject: g.ruling.effect_subject, + interlock: InterlockedBy { hold: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant") }, + }, + scope: g.scope, + effects: g.effects, + } +} + +fn apply_fold_undischarged(discharges: List) -> Bool { + let access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: mtjade1_key) + let outcomes: List> = [ + StepEstablished { receipt: ProbeReceipt { key: access, consumed: [] } }, + StepEstablished { receipt: ProbeReceipt { key: identity, consumed: [access] } }, + StepEstablished { receipt: ProbeReceipt { key: prior, consumed: [identity] } }, + StepEstablished { receipt: ProbeReceipt { key: bmc, consumed: [prior] } }, + ] + match admit_convergence_plan(planning: arrival_planning_authority(), steps: four_steps()) { + ConvergencePlanAdmitted { plan: p } => + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_on_bmc_secure), discharges: discharges) { + RunStopped { ledger: l, at: at } => + step_instance_key_eq(a: at, b: bmc) + && match l.instances.last() { + Present { value: s } => match s { + InstanceRefused { key: _, cause: c } => match c { AuthorizationUndischarged => true _ => false } + _ => false + } + Absent => false + } + _ => false + } + ConvergencePlanRefused { cause: _ } => false + } +} + +test fn w_bmc_secure_apply_pending_interlock_refuses_at_discharge() -> Bool { + grant_discharges_bmc_secure_account_write(g: mtjade1_grant_with_interlock_pending(), host: operator_host_mtjade1) == false + && grant_discharges_bmc_secure_account_write(g: mtjade1_grant_with_foreign_interlock(), host: operator_host_mtjade1) == false + && grant_discharges_bmc_secure_account_write(g: mtjade1_live_standing_grant, host: operator_host_mtjade1) +} + +test fn w_mtcollins1_is_not_discharged_by_the_mtjade1_grant() -> Bool { + grant_discharges_bmc_secure_account_write(g: mtjade1_live_standing_grant, host: operator_host_mtcollins1) == false +} + +fn mtjade1_capability_standing() -> BmcRotationRouteStanding { + rotation_route_ungrounded(endpoint: mtjade1_bmc_endpoint(), firmware: mtjade1_bmc_firmware()) +} + +fn mtjade1_stale_capability_standing() -> BmcRotationRouteStanding { + rotation_route_ungrounded( + endpoint: mtjade1_bmc_endpoint(), + firmware: bmc_firmware_release_identity_of_wire(family: AmiMegaRac, wire: "0.32" as NonEmptyStr), + ) +} + +fn mtjade1_managed_write_request() -> BmcAccountWriteRequest { + IpmiSetUserPassword { user: mtjade1_managed_ipmi_user } +} + +fn mtjade1_published_write_request() -> BmcAccountWriteRequest { + IpmiSetUserPassword { user: mtjade1_published_ipmi_user } +} + +fn rotation_capability_for( + standing: BmcRotationRouteStanding, + request: BmcAccountWriteRequest, + attempt_text: String, + authority: NonEmptyStr, +) -> Redemption { + RedemptionAdmitted { + claims: ApprovalCapabilityClaims { + protocol: approval_capability_protocol, + issuer: "gunbc-approval-broker" as NonEmptyStr, + audience: "srv1" as NonEmptyStr, + authority: authority, + escalation_id: "o1c3b-witness" as NonEmptyStr, + request_revision: rotation_route_request_identity(standing: standing, request: request), + decision: ProposeApprove, + attempt: attempt_text as AttemptIdentity, + issued_at: "2026-10-04T00:00:00Z", + expires_at: "2026-10-04T00:15:00Z", + key_id: "broker-2026-10" as MacKeyId, + }, + decided_by: "operator" as NonEmptyStr, + } +} + +fn bmc_secure_apply_key() -> StepInstanceKey { + step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: mtjade1_key) +} + +test fn w_bmc_secure_apply_capability_for_another_authority_does_not_discharge() -> Bool { + capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: mtjade1_capability_standing(), request: mtjade1_managed_write_request(), attempt_text: run_a as String, authority: route_qualification_authority), + standing: mtjade1_capability_standing(), + request: mtjade1_managed_write_request(), + key: bmc_secure_apply_key(), + ) == false +} + +test fn w_bmc_secure_apply_capability_for_another_request_does_not_discharge() -> Bool { + capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: mtjade1_capability_standing(), request: mtjade1_managed_write_request(), attempt_text: run_a as String, authority: rotation_apply_authority), + standing: mtjade1_capability_standing(), + request: mtjade1_published_write_request(), + key: bmc_secure_apply_key(), + ) == false +} + +test fn w_bmc_secure_apply_capability_for_another_build_does_not_discharge() -> Bool { + capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: mtjade1_capability_standing(), request: mtjade1_managed_write_request(), attempt_text: run_a as String, authority: rotation_apply_authority), + standing: mtjade1_stale_capability_standing(), + request: mtjade1_managed_write_request(), + key: bmc_secure_apply_key(), + ) == false +} + +test fn w_bmc_secure_apply_capability_for_another_run_does_not_discharge() -> Bool { + capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: mtjade1_capability_standing(), request: mtjade1_managed_write_request(), attempt_text: run_b as String, authority: rotation_apply_authority), + standing: mtjade1_capability_standing(), + request: mtjade1_managed_write_request(), + key: bmc_secure_apply_key(), + ) == false +} + +test fn w_bmc_secure_apply_admitted_capability_for_the_canonical_rotation_identity_discharges() -> Bool { + let standing = mtjade1_capability_standing() + let request = mtjade1_managed_write_request() + (rotation_route_request_identity(standing: standing, request: request) as String) != "" + && capability_discharges_bmc_secure_account_write( + r: rotation_capability_for(standing: standing, request: request, attempt_text: run_a as String, authority: rotation_apply_authority), + standing: standing, + request: request, + key: bmc_secure_apply_key(), + ) +} + +test fn w_bmc_secure_apply_discharge_for_another_run_refuses() -> Bool { + let foreign = step_instance_key(run: run_b, step: bmc_secure_step_ref, subject: mtjade1_key) + apply_fold_undischarged(discharges: [instance_authorization(key: foreign, principal: mtjade1_live_standing_grant.principal)]) +} + +test fn w_bmc_secure_apply_discharge_for_another_unit_refuses() -> Bool { + let foreign = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: "mtcollins1" as StepSubjectKey) + apply_fold_undischarged(discharges: [instance_authorization(key: foreign, principal: mtjade1_live_standing_grant.principal)]) +} + +// PAIRING: the census first_consumer mints the Apply discharge list. Hard-coding discharges: [] +// there must redden this claim. Prefix captures are the production readers; this claim supplies +// Apply+grant and runs converge_arrival_through_bmc_secure, not a probe fold beside it. +test fn w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world() -> Bool { + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => + match converge_arrival_through_bmc_secure( + run: run_a, + subject: mtjade1_key, + read: read_mtjade1_current_manager_read(), + inputs: mtjade1_identity_bind_inputs(), + prior_life: PriorLifeInputs { platform: mt_jade_platform_ref, world: prior_life_minimal_dry_world() }, + bmc: mtjade1_bmc_inputs( + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: none, + ), + ) { + ArrivalRunFolded { verdict: v } => + match v { + RunConverged { run: r } => + length(xs: r.ledger.instances) == 4 + && match r.ledger.instances.first() { Present { value: s } => access_established_as_read(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: identity_bind_provisional_step_ref)) |> first() { Present { value: s } => identity_bound_from_committed_captures(s: s) Absent => false } + && match r.ledger.instances |> filter(s => instance_step_is(s: s, step: prior_life_boundary_step_ref)) |> first() { Present { value: s } => prior_life_archived_from_the_bound_subject(s: s) Absent => false } + && match r.ledger.instances.last() { Present { value: s } => bmc_secure_applied_established(s: s) Absent => false } + _ => false + } + _ => false + } + } +} + +fn bmc_secure_bound_refuses_foreign_apply(foreign_subject: MachineIntakeSubject) -> Bool + admit_callers: [ + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_attempt_is_refused"), + decl_ref(module_path: "test.claim.machine_intake_arrival_converge_witness", decl_name: "w_bmc_secure_apply_of_another_unit_is_refused"), + ] +{ + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: own } => + match mtjade1_dry_applied_bmc(subject: foreign_subject) { + Absent => false + Present { value: foreign } => { + let inputs = mtjade1_bmc_inputs( + reading: own.application.plan.diverged, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: foreign }, + capability: none, + ) + match bmc_secure_bound(key: bmc_key, identity_key: identity, identity_subject: mtjade1_intake_subject(), prior_key: prior, inputs: inputs) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationForAnotherInstance { subject: _ } => true _ => false } + _ => false + } + } + } + } +} + +test fn w_bmc_secure_apply_of_another_attempt_is_refused() -> Bool { + bmc_secure_bound_refuses_foreign_apply(foreign_subject: mtjade1_intake_subject_for(attempt: "o1c1-witness-run-b" as IntakeAttemptId)) +} + +test fn w_bmc_secure_apply_of_another_unit_is_refused() -> Bool { + bmc_secure_bound_refuses_foreign_apply(foreign_subject: MachineIntakeSubject { + subject: qualification_subject_of(unit_key: "B810301000412080005AJ0C2" as UnitKey, assembly: expected_mtjade1_assembly, firmware: expected_mtjade1_firmware), + attempt_id: "o1c1-witness-run-a" as IntakeAttemptId, + }) +} + +test fn w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + let requested = mtjade1_bmc_goal_with_break_glass_epoch(epoch: 5, version: "5") + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: BmcSecureInputs { + goal: requested, + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: none, + }, + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationNotTheInspectedTransition => true _ => false } + _ => false + } + } +} + +data mtjade1_controller_clock_x_millis: EpochMs = 1 +data mtjade1_controller_clock_y_millis: EpochMs = 2 + +fn mtjade1_controller_clock(millis: EpochMs, label: String) -> ControllerClockReading { + ControllerClockReading { + reported_millis: millis, + evidence: EvidenceRef { label: label as NonEmptyStr, digest: content_hash_of_value(value: label) }, + } +} + +test fn w_matching_present_controller_clocks_compare_equal() -> Bool { + let clock = mtjade1_controller_clock(millis: mtjade1_controller_clock_x_millis, label: "controller-clock-x") + controller_clock_reading_same(left: Present { value: clock }, right: Present { value: clock }) +} + +test fn w_bmc_secure_apply_of_a_different_present_controller_clock_is_refused() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let clock_x = mtjade1_controller_clock(millis: mtjade1_controller_clock_x_millis, label: "controller-clock-x") + let clock_y = mtjade1_controller_clock(millis: mtjade1_controller_clock_y_millis, label: "controller-clock-y") + let reading = observation_with_controller_clock(base: apply.application.plan.diverged, controller_clock: Present { value: clock_y }) + let stamped = apply_with_diverged_controller_clock(application: apply.application, controller_clock: Present { value: clock_x }) + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: BmcSecureInputs { + goal: mtjade1_bmc_goal(), + reading: reading, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: BmcSecureApplyInputs { application: stamped, post_read: apply.post_read } }, + capability: none, + }, + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationNotTheInspectedTransition => true _ => false } + _ => false + } + } + } +} + +test fn w_bmc_secure_apply_of_a_present_controller_clock_over_absent_is_refused() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let reading = observation_with_controller_clock( + base: apply.application.plan.diverged, + controller_clock: Present { value: mtjade1_controller_clock(millis: mtjade1_controller_clock_x_millis, label: "controller-clock-x") }, + ) + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: BmcSecureInputs { + goal: mtjade1_bmc_goal(), + reading: reading, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: none, + }, + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationNotTheInspectedTransition => true _ => false } + _ => false + } + } + } +} + +test fn w_bmc_secure_apply_of_another_channel_state_is_refused() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + let reading = dry_read_bmc_account_state( + world: mtjade1_account_world( + users: [BmcIpmiUser { id: 3, password: "managed-generation-1!" }, BmcIpmiUser { id: 2, password: "admin" }], + published_lan_privilege_closed: false, + ), + subject: mtjade1_intake_subject(), + endpoint: mtjade1_bmc_endpoint(), + firmware: mtjade1_bmc_firmware(), + managed: mtjade1_bmc_goal().managed, + managed_user: mtjade1_managed_ipmi_user, + managed_password: "managed-generation-1!", + census: mtjade1_bmc_census(published_lan_privilege_closed: false), + published_user: mtjade1_published_ipmi_user, + published_password: "admin", + published_account: PublishedAccountRetired, + break_glass: mtjade1_bmc_goal().published_break_glass, + break_glass_password: "break-glass-generation-4!", + attempt: "o1c1-witness-run-a" as AttemptIdentity, + read_at_millis: mtjade1_bmc_read_at, + ) + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: BmcSecureInputs { + goal: mtjade1_bmc_goal(), + reading: reading, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: none, + }, + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureApplicationNotTheInspectedTransition => true _ => false } + _ => false + } + } +} + +test fn w_bmc_secure_apply_without_authorization_refuses_after_a_real_apply() -> Bool { + let identity = step_instance_key(run: run_a, step: identity_bind_provisional_step_ref, subject: mtjade1_key) + let prior = step_instance_key(run: run_a, step: prior_life_boundary_step_ref, subject: mtjade1_key) + let bmc_key = bmc_secure_apply_key() + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => + match bmc_secure_bound( + key: bmc_key, + identity_key: identity, + identity_subject: mtjade1_intake_subject(), + prior_key: prior, + inputs: mtjade1_bmc_inputs(reading: apply.application.plan.diverged, grant: none, apply: Present { value: apply }, capability: none), + ) { + StepRefused { key: _, cause: c } => match c { BmcSecureAuthorizationUndischarged => true _ => false } + _ => false + } + } +} + +test fn w_bmc_secure_apply_uncovered_grant_falls_through_to_capability() -> Bool { + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let standing = apply.application.plan.managed_write.route + let request = apply.application.plan.managed_write.request + let key = bmc_secure_apply_key() + match discharge_bmc_secure_apply( + key: key, + identity_subject: mtjade1_intake_subject(), + inputs: mtjade1_bmc_inputs( + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_grant_without_bmc_secure_effect() }, + apply: Present { value: apply }, + capability: Present { value: rotation_capability_for(standing: standing, request: request, attempt_text: run_a as String, authority: rotation_apply_authority) }, + ), + standing: standing, + request: request, + ) { + Present { value: _ } => true + Absent => false + } + } + } +} + +test fn w_bmc_secure_apply_uncovered_grant_refuses_a_capability_for_another_request() -> Bool { + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let standing = apply.application.plan.managed_write.route + let request = apply.application.plan.managed_write.request + let key = bmc_secure_apply_key() + match discharge_bmc_secure_apply( + key: key, + identity_subject: mtjade1_intake_subject(), + inputs: mtjade1_bmc_inputs( + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_grant_without_bmc_secure_effect() }, + apply: Present { value: apply }, + capability: Present { value: rotation_capability_for(standing: standing, request: mtjade1_published_write_request(), attempt_text: run_a as String, authority: rotation_apply_authority) }, + ), + standing: standing, + request: request, + ) { + Absent => true + Present { value: _ } => false + } + } + } +} + +test fn w_a_foreign_bound_host_key_cannot_mint_from_this_instance_controller() -> Bool { + match mtjade1_dry_applied_bmc(subject: mtjade1_intake_subject()) { + Absent => false + Present { value: apply } => { + let standing = apply.application.plan.managed_write.route + let request = apply.application.plan.managed_write.request + let key = step_instance_key(run: run_a, step: bmc_secure_step_ref, subject: "mtcollins1" as StepSubjectKey) + match bound_bmc_secure_host(key: key) { + Absent => false + Present { value: host } => + host_identity_eq(a: host, b: operator_host_mtcollins1) + && match discharge_bmc_secure_apply( + key: key, + identity_subject: mtjade1_intake_subject(), + inputs: mtjade1_bmc_inputs( + reading: apply.application.plan.diverged, + grant: Present { value: mtjade1_live_standing_grant }, + apply: Present { value: apply }, + capability: Present { value: rotation_capability_for(standing: standing, request: request, attempt_text: run_a as String, authority: rotation_apply_authority) }, + ), + standing: standing, + request: request, + ) { + Absent => true + Present { value: _ } => false + } + } + } + } +} + test fn w_a_precondition_is_not_satisfied_by_a_receipt_for_another_subject() -> Bool { let own_access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: mtjade1_key) let foreign_access = step_instance_key(run: run_a, step: access_discover_step_ref, subject: "mtjade2" as StepSubjectKey) @@ -481,7 +1507,7 @@ test fn w_a_precondition_is_not_satisfied_by_a_receipt_for_another_subject() -> ] match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { ConvergencePlanAdmitted { plan: p } => - stopped_on_unmet_access_precondition(v: Present { value: fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed)) }) + stopped_on_unmet_access_precondition(v: Present { value: fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_never), discharges: []) }) ConvergencePlanRefused { cause: _ } => false } } @@ -497,7 +1523,7 @@ test fn w_a_precondition_is_not_satisfied_by_a_receipt_from_another_run() -> Boo ] match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { ConvergencePlanAdmitted { plan: p } => - stopped_on_unmet_access_precondition(v: Present { value: fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed)) }) + stopped_on_unmet_access_precondition(v: Present { value: fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_never), discharges: []) }) ConvergencePlanRefused { cause: _ } => false } } @@ -518,7 +1544,7 @@ test fn w_an_incomplete_instance_satisfies_no_dependent_and_the_run_is_incomplet ] match admit_convergence_plan(planning: arrival_planning_authority(), steps: real_steps()) { ConvergencePlanAdmitted { plan: p } => - match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed)) { + match fold_convergence_run(plan: p, run: run_a, subject: mtjade1_key, outcomes: outcomes, projection: convergence_receipt_projection(key_of: probe_key, consumed_of: probe_consumed, authorization_required_of: probe_auth_never), discharges: []) { RunIncomplete { ledger: l, at: at } => declaration_ref_eq(a: at.step_identity, b: identity_bind_provisional_step_ref) && match l.instances.last() { diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 7d2c709ff07..7a1b37073a2 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -40,6 +40,10 @@ new-witness eval-step cost gate over the one real-path claim of each approval-re two serving processes on one host can both open the single-writer approval store, and which of them may write is decided by a declaration they agree to consult rather than by a permission either one cannot bypass: RUNG DROP, structurally impossible -> mechanically preventable (replacement staged: gunbc.auth.approval_writer_authority approval_write_admission, consulted by both mutating routes before any store effect; the terminal replacement is a POSIX-principal restriction on the store generations). Population: gunbc-roadmap.service and gunbc-approval-broker.service on srv1, for the window in which both run under the service principal with gunbc.auth.approval_decision_store approval_decision_store_root readable and both keyrings loadable, any gunbc serve process started by hand from a checkout whose revision predates gunbc.auth.approval_writer_authority, which reads no such declaration at all. Restored when: THE CAPABILITY: the approval store's generations are writable by exactly ONE POSIX principal, and the other serving process's account cannot open them -- so a second writer is refused by the kernel rather than by agreement. SUFFICIENT FOR: attempting a store write as the non-writer principal and observing the OS refusal, with the broker principal alone holding the submission MAC key, the capability MAC key, the publisher token and the store, and the roadmap principal unable to read any of them. Nothing smaller retires this row. IN PARTICULAR, A PERMISSION-BITS READBACK DOES NOT: a receipt reporting owner, group, exact mode and forbidden bits establishes that only the declared principals HOLD permission, which is a statement about metadata and not about access. This trigger asks whether the non-writer CAN OPEN THE STORE, and only an attempt answers that: the execution-as-another-principal leg IS the evidence, and a metadata receipt is not a weaker form of it but a different observation. It is named here because it is the artifact that will exist and will therefore be reached for (raised by merry-bear-816 through zesty-crane-846, 2026-09-19, against the generalized custody work that produces exactly such a receipt). Nor does moving writer authority to the broker retire it -- that changes which process refuses, not whether the guarantee is by agreement; nor does deleting the roadmap's approval routes, because the roadmap process would still hold a principal that can open the store; nor does a claim over approval_write_admission, which establishes that the fold refuses and not that a process which skips the fold is stopped. +### new-witness eval-step cost gate over the one Apply inhabitance of converge_arrival_through_bmc_secure: it still executes, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered — declared 2026-10-07 + +new-witness eval-step cost gate over the one Apply inhabitance of converge_arrival_through_bmc_secure: it still executes, eval_steps stay recorded, a semantic red and a wall-clock crossing still block; only the eval-step cost-gate rung is lowered: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: converge_arrival_through_bmc_secure executing as natively emitted code rather than in the seed interpreter, so the one Apply inhabitance fits the NewWitnessTier eval-step budget). Population: test.claim.machine_intake_arrival_converge_witness.w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world: over the new-witness eval-step budget, rostered in v2.workflow.floor_eval_step_cost_drop floor_eval_step_cost_drop_bmc_secure_apply_converge_rows; measured by claim_batch --hermetic --source-root dag --source-root src/v2 --entry dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag --function w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world (BuildBuddy, GUNBC_BIND_MEMORY_CGROUP_BYTES=30064771072): PASS, eval_steps over the new-witness budget. The billed work is converge_arrival_through_bmc_secure over the production prefix captures plus dry Apply+grant, which this claim is the only Apply execution of. Restored when: THE CAPABILITY: converge_arrival_through_bmc_secure (AccessDiscover through BmcSecure Apply, including the fold's Apply-discharge mint) executing as natively emitted code in a claim frame. WHAT THAT MUST BE SUFFICIENT FOR: test.claim.machine_intake_arrival_converge_witness.w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world, still calling that entry with Apply+grant and still asserting the Applied route, measures under the NewWitnessTier budget that v2.workflow.required_floor claim_ceiling_eval_step_budget derives. Deleting the identity, hard-coding discharges: [] in the entry, or relocating the claim off the required gate satisfies none of it. + ### Arity agreement between a declared builtin parameter name and its derived algebra template — declared 2026-09-01 Builtin signature grounding -- **RUNG DROP, DECLARED (2026-09-01).** PREVIOUS RUNG: none to lower -- this declares that a class created by this change lands below its attainable ceiling rather than at it. v1.compiler.infer_method pairs each row's DECLARED parameter names with the parameter TYPES derived from std.algebra. When the two lists disagree in length, pair_declared_names yields AlgebraTypeVariable { id: "unpaired_declared_parameter" } for the unpaired position instead of refusing. That is a value standing where a refusal belongs -- DESIGN section 5's fabricated-plausible-output arm -- and it is declared here rather than left as a marker that reads like a wall. TEMPORARY RUNG: mitigatable. The marker is distinctive, greppable, and reaches src/v1/stage0/src/v1_compiler_infer_method.rs, so a mismatch is DISCOVERABLE by inspection of a generated artifact. It is not mechanically preventable, because NO CONSUMER ASSERTS ITS ABSENCE: an unchecked marker is an inert lens, and DESIGN is explicit that the tier where the machinery exists and nothing gates on it is itself a lie. REASON: builtin_function_registry is a `data` initializer and a .dag data initializer has no refusal channel -- there is nowhere at construction for a typed, located diagnostic to go, so the only arms available were a fabricated value or a silently shorter list, and a marked fabrication is the more honest of the two. POPULATION: bounded and closed at 20 rows -- exactly the registry names that std.algebra also declares and that therefore pair at all (count, to_int, substring, to_string, concat, map_insert, map_merge, with, map_contains_key, map_has, lookup, map_get, map_keys, map_values, get, reverse, list_push, length, starts_with, replace). The other 112 rows author their types directly and cannot reach this arm. Zero occurrences of the marker in the tree today, which is the state this row exists to keep observable. RESTORATION TRIGGER: construction-time refusal available inside a `data` initializer -- SUFFICIENT FOR a declared/derived arity disagreement to stop the line with a typed, located diagnostic at the row that causes it, rather than to produce a marked value that construction accepts. The trigger names that capability and not any artifact that would contribute to one; a witness asserting the marker's absence would raise this to mechanically preventable but would NOT retire the row, because the invalid state would still be writable. diff --git a/src/v2/workflow/floor_eval_step_cost_drop.dag b/src/v2/workflow/floor_eval_step_cost_drop.dag index 14228f13a85..aaf054450e6 100644 --- a/src/v2/workflow/floor_eval_step_cost_drop.dag +++ b/src/v2/workflow/floor_eval_step_cost_drop.dag @@ -38,6 +38,8 @@ import std.types { NonEmptyStr, List } // of the dag target (`dag_text_round_trip_nested_bind_new_witness_eval_step_cost`). // - `floor_eval_step_cost_drop_coproduct_fragment_normalize_rows`: the three coproduct type-declaration // fragment-lowering claims (`coproduct_fragment_normalize_new_witness_eval_step_cost`). +// - `floor_eval_step_cost_drop_bmc_secure_apply_converge_rows`: the one Apply inhabitance of +// converge_arrival_through_bmc_secure (`bmc_secure_apply_converge_new_witness_eval_step_cost`). // The loss is a WORKFLOW fact -- which // identities the eval-step ceiling does not refuse -- so it lives beside the other two rosters the // ceiling consults (`v2.workflow.floor_grandfathered_roster`, `v2.workflow.floor_cost_debt`) and @@ -442,8 +444,15 @@ data floor_eval_step_cost_drop_coproduct_fragment_normalize_rows: List = [ + EvalStepCostDropMeasurement { + identity: "test.claim.machine_intake_arrival_converge_witness.w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world" as NonEmptyStr, + measured_by: "claim_batch --hermetic --source-root dag --source-root src/v2 --entry dag/test/claim/machine_intake/machine_intake_arrival_converge_witness_test.dag --function w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world (BuildBuddy, GUNBC_BIND_MEMORY_CGROUP_BYTES=30064771072): PASS, eval_steps over the new-witness budget. The billed work is converge_arrival_through_bmc_secure over the production prefix captures plus dry Apply+grant, which this claim is the only Apply execution of" as NonEmptyStr, + }, +] + fn floor_eval_step_cost_drop_all_rows() -> List { - concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(floor_eval_step_cost_drop_rows, floor_eval_step_cost_drop_apply_render_rows), floor_eval_step_cost_drop_live_forecast_rows), floor_eval_step_cost_drop_page_style_rows), floor_eval_step_cost_drop_interpreted_crypto_rows), floor_eval_step_cost_drop_app_attest_verifier_rows), floor_eval_step_cost_drop_span_program_rows), floor_eval_step_cost_drop_python_to_typescript_inhabitance_rows), floor_eval_step_cost_drop_boot_matrix_rows), floor_eval_step_cost_drop_dark_install_render_rows), floor_eval_step_cost_drop_build_job_membership_rows), floor_eval_step_cost_drop_dag_emit_round_trip_rows), floor_eval_step_cost_drop_approval_intent_digest_rows), floor_eval_step_cost_drop_dag_text_round_trip_rows), floor_eval_step_cost_drop_coproduct_fragment_normalize_rows) + concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(concat(floor_eval_step_cost_drop_rows, floor_eval_step_cost_drop_apply_render_rows), floor_eval_step_cost_drop_live_forecast_rows), floor_eval_step_cost_drop_page_style_rows), floor_eval_step_cost_drop_interpreted_crypto_rows), floor_eval_step_cost_drop_app_attest_verifier_rows), floor_eval_step_cost_drop_span_program_rows), floor_eval_step_cost_drop_python_to_typescript_inhabitance_rows), floor_eval_step_cost_drop_boot_matrix_rows), floor_eval_step_cost_drop_dark_install_render_rows), floor_eval_step_cost_drop_build_job_membership_rows), floor_eval_step_cost_drop_dag_emit_round_trip_rows), floor_eval_step_cost_drop_approval_intent_digest_rows), floor_eval_step_cost_drop_dag_text_round_trip_rows), floor_eval_step_cost_drop_coproduct_fragment_normalize_rows), floor_eval_step_cost_drop_bmc_secure_apply_converge_rows) } // THE PROJECTION THE SEED RUNNER READS AND THE MODEL TESTS AGAINST. The runner refuses an empty or