Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
4523d79
Managed-host cut O1a: evidence-bound rotation route standing + qualif…
Oct 3, 2026
a987c3c
Census: hoist the route-qualification row's reasoning to module grain…
Oct 3, 2026
c05714a
Rotation Apply: bind the approval to the controller, build and reques…
Oct 4, 2026
afcc512
Route module sits below bmc_secure: drop the rotation-event mapping; …
Oct 4, 2026
19be9fc
Merge remote-tracking branch 'origin/session/bright-wolf-485' into se…
Oct 4, 2026
8e5b038
O1a side-chat review: modeled run cannot ground; response bound to su…
Oct 4, 2026
525090a
BmcSecure as a desired state, in shadow: observer clock, secret-order…
Oct 4, 2026
7501fcd
Seal every carrier of an observer-instant ordering field; enroll the …
Oct 4, 2026
ed2e65b
Merge remote-tracking branch 'origin/session/bright-wolf-485' into se…
Oct 4, 2026
0f537fd
Re-merge O1a 8e5b038052: ground the lab routes by citation (a modeled…
Oct 4, 2026
0a643d1
Merge remote-tracking branch 'origin/main' into session/lively-eagle-811
Oct 4, 2026
4bed00c
Rung drop names the renamed unit-hold module; regenerate rung-drops p…
Oct 4, 2026
07423d2
Lab route fixtures: .invalid fixture citation, helpers admitted only …
Oct 4, 2026
6f8d3c2
Side-chat blockers: build from the observation, goal-bound published …
Oct 4, 2026
eca20ca
Merge remote-tracking branch 'origin/main' into session/lively-eagle-811
Oct 4, 2026
0c38376
Merge remote-tracking branch 'origin/main' into session/lively-eagle-811
Oct 4, 2026
86b27f3
Restore rotation_route_consumption_frontier: O1b supplies the consume…
Oct 4, 2026
f18590c
Merge remote-tracking branch 'origin/main' into session/lively-eagle-811
Oct 4, 2026
4255ba0
Observe the goal's break-glass generation in assessment and post-read
Oct 4, 2026
956c851
Merge remote-tracking branch 'origin/main' into session/lively-eagle-811
Oct 4, 2026
745b538
Merge remote-tracking branch 'origin/main' into session/gentle-dove-262
Oct 4, 2026
a68d4f3
machine intake: MachineOperatingEnvironment -> MachineQualificationPo…
Oct 4, 2026
5af901f
Merge remote-tracking branch 'origin/main' into session/lively-eagle-811
Oct 4, 2026
df26a44
Merge remote-tracking branch 'origin/session/lively-eagle-811' into s…
Oct 4, 2026
e9bd547
Merge remote-tracking branch 'origin/main' into session/gentle-dove-262
Oct 5, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions dag/gunbc/deployment_risk.dag
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@ import gunbc.auth.github_apps { DeclaredGitHubApp, gunbai_bot_declared }
//
// Machine qualification is a different subject. It shares DeploymentRiskClass only as what a
// machine ADMITS (MachineQualificationPolicy { admits }); a machine is never itself ProdRisk and
// never confers the prod role. That replacement of gunbc.machine_intake_phase
// MachineOperatingEnvironment lands in its own one-motion migration on top of this module.
// never confers the prod role. The policy's home is gunbc.machine_intake_phase, which consumes
// this class and coins no machine-level environment vocabulary of its own.

// ── The subject ─────────────────────────────────────────────────────────────────────────────────
// THE STABLE IDENTITY OF ONE Deployment -- the convergence subject whose desired state, mutable
Expand Down
62 changes: 30 additions & 32 deletions dag/gunbc/machine_intake/bmc_secure.dag
Original file line number Diff line number Diff line change
Expand Up @@ -74,19 +74,17 @@ import extdeps.network.ipv4 { Ipv4Address }
import extdeps.cloud.gcp.secret_ref { SecretRef, HashPending, gcp_resource_names_this_secret }
import gunbc.auth.github_gcp_federation { fleet_secrets_project_number }
import gunbc.machine_intake_subject { MachineIntakeSubject }
import gunbc.deployment_risk { DeploymentRiskClass, ProdRisk, TestRisk }
import gunbc.machine_intake_phase {
Arrival,
BmcAccess,
BmcSecure,
DevelopmentAndTest,
IntakePhase,
IntakeQualificationPolicy,
MachineOperatingEnvironment,
MachineQualificationPolicy,
OperatorAction,
Production,
QualificationPolicy,
QualificationRefusalOwner,
intake_qualification_policy_digest,
machine_qualification_policy_digest,
}
import gunbc.machine_intake_receipt {
EvidenceRef,
Expand Down Expand Up @@ -223,7 +221,7 @@ type RetainedCredentialKind
// (PublishedCredentialAccountPrecedesRotation); a pre-rotation user-list cannot
// label the post-rotation standing.
// RetainedByPolicy is a third arm: it satisfies the BMC-secure conjunct
// ONLY under DevelopmentAndTest. Production refuses it; that refusal is the
// ONLY under a TestRisk-admitting policy. A ProdRisk-admitting policy refuses it; that refusal is the
// discriminating control for the day a machine is promoted.
type PublishedCredentialAccountObservation
= PublishedCredentialRetired { evidence: EvidenceRef, observed_at: EpochMs }
Expand Down Expand Up @@ -337,7 +335,7 @@ type BmcSecureRefusalCause
| PublishedCredentialCensusMemberUnprobed { channel: IpmiChannelNumber }
| PublishedCredentialProbeDuplicate { channel: IpmiChannelNumber }
| PublishedCredentialProbeUnmatched { channel: IpmiChannelNumber }
| PublishedCredentialRetainedNotAdmittedForProduction
| PublishedCredentialRetainedNotAdmittedByProdRiskPolicy
| PublishedCredentialNotRetained { channel: IpmiChannelNumber }

// NO ARM RETURNS UnitHardware, AND THAT IS THE POINT (design §6: a non-working
Expand Down Expand Up @@ -373,7 +371,7 @@ fn bmc_secure_refusal_owner(cause: BmcSecureRefusalCause) -> QualificationRefusa
PublishedCredentialCensusMemberUnprobed { channel: _ } => BmcAccess
PublishedCredentialProbeDuplicate { channel: _ } => QualificationPolicy
PublishedCredentialProbeUnmatched { channel: _ } => QualificationPolicy
PublishedCredentialRetainedNotAdmittedForProduction => QualificationPolicy
PublishedCredentialRetainedNotAdmittedByProdRiskPolicy => QualificationPolicy
PublishedCredentialNotRetained { channel: _ } => OperatorAction
}
}
Expand Down Expand Up @@ -403,7 +401,7 @@ fn bmc_secure_refusal_label(cause: BmcSecureRefusalCause) -> NonEmptyStr {
PublishedCredentialCensusMemberUnprobed { channel: _ } => "a census LAN member has no matching published-credential probe"
PublishedCredentialProbeDuplicate { channel: _ } => "more than one published-credential probe matched the same census LAN member"
PublishedCredentialProbeUnmatched { channel: _ } => "a published-credential probe matched no census LAN member"
PublishedCredentialRetainedNotAdmittedForProduction => "a retained BMC backdoor is not admitted for production; a fresh census pass that retires or disables the published credential is required"
PublishedCredentialRetainedNotAdmittedByProdRiskPolicy => "a retained BMC backdoor is not admitted under a ProdRisk-admitting qualification policy; a fresh census pass that retires or disables the published credential is required"
PublishedCredentialNotRetained { channel: _ } => "the declared factory-credential retention was not observed on a census LAN member"
}
}
Expand Down Expand Up @@ -439,13 +437,13 @@ type BmcSecureOutcome
// outcome alone and had bmc_secure_phase_receipt take the subject as a
// separate argument, so a standing legitimately derived for host A could be
// handed to the receipt function beside host B's subject. The same hatch
// existed for policy: derive wrote DevelopmentAndTest and the receipt took a
// second Production policy, restamping the digest. The receipt now reads
// existed for policy: derive wrote a TestRisk-admitting policy and the receipt took a
// second ProdRisk-admitting policy, restamping the digest. The receipt now reads
// subject and policy off the standing; there is no parameter left to swap.
// Promotion is a fresh derive_bmc_secure under Production, which refuses
// RetainedByPolicy. There is no observed environment on the unit; the policy
// Promotion is a fresh derive_bmc_secure under a ProdRisk-admitting policy, which refuses
// RetainedByPolicy. There is no observed risk class on the unit, and a machine never holds one; the policy
// is the declared qualification (FleetAdmissionReceipt already binds its
// digest). A caller can still declare DevelopmentAndTest — that is the policy
// digest). A caller can still declare admits: TestRisk — that is the policy
// fact, not a second knob beside the receipt.
//
// So the subject and the outcome are ONE record and the record is
Expand Down Expand Up @@ -475,7 +473,7 @@ type BmcSecureOutcome
// the construction and not the type's usability.
type BmcSecureStanding sole_constructor {
subject: MachineIntakeSubject
policy: IntakeQualificationPolicy
policy: MachineQualificationPolicy
outcome: BmcSecureOutcome
}

Expand Down Expand Up @@ -940,7 +938,7 @@ fn adjudicate_published_census(
probes: List<PublishedCredentialLanProbe>,
published_user: IpmiUserId,
published_account: PublishedCredentialAccountObservation,
environment: MachineOperatingEnvironment,
admits: DeploymentRiskClass,
) -> BmcSecureOutcome {
let account_at = published_account_observed_at(account: published_account)
if account_at < applied_at {
Expand All @@ -950,9 +948,9 @@ fn adjudicate_published_census(
} else {
match published_account {
PublishedCredentialRetainedByPolicy { retention: _, evidence: _, observed_at: _ } =>
match environment {
Production => BmcSecureRefused { cause: PublishedCredentialRetainedNotAdmittedForProduction }
DevelopmentAndTest =>
match admits {
ProdRisk => BmcSecureRefused { cause: PublishedCredentialRetainedNotAdmittedByProdRiskPolicy }
TestRisk =>
adjudicate_published_census_join(
endpoint: endpoint,
reference: reference,
Expand Down Expand Up @@ -1011,7 +1009,7 @@ fn adjudicate_managed_probe(
applied_at: EpochMs,
rotation_evidence: EvidenceRef,
managed: CredentialProbeOutcome,
environment: MachineOperatingEnvironment,
admits: DeploymentRiskClass,
) -> BmcSecureOutcome {
match managed {
CredentialRejected { evidence: _, observed_at: _ } => BmcSecureRefused { cause: ManagedCredentialRejected }
Expand All @@ -1033,7 +1031,7 @@ fn adjudicate_managed_probe(
probes: observation.published_probes,
published_user: observation.published_user,
published_account: observation.published_account,
environment: environment,
admits: admits,
)
}
}
Expand All @@ -1044,7 +1042,7 @@ fn adjudicate_rotation(
reference: ManagedCredentialReference,
applied_at: EpochMs,
rotation_evidence: EvidenceRef,
environment: MachineOperatingEnvironment,
admits: DeploymentRiskClass,
) -> BmcSecureOutcome {
if (reference.credential_epoch <= observation.previous_credential_epoch) {
BmcSecureRefused {
Expand All @@ -1060,14 +1058,14 @@ fn adjudicate_rotation(
applied_at: applied_at,
rotation_evidence: rotation_evidence,
managed: observation.managed_probe,
environment: environment,
admits: admits,
)
}
}

fn adjudicate_bootstrap(
observation: BmcCredentialRotationObservation,
environment: MachineOperatingEnvironment,
admits: DeploymentRiskClass,
) -> BmcSecureOutcome {
match observation.bootstrap_probe {
CredentialProbeUnestablished { detail: d } => BmcSecureRefused { cause: CredentialStateUnknown { detail: d } }
Expand All @@ -1082,7 +1080,7 @@ fn adjudicate_bootstrap(
reference: r,
applied_at: at,
rotation_evidence: e,
environment: environment,
admits: admits,
)
}
}
Expand All @@ -1091,12 +1089,12 @@ fn adjudicate_bootstrap(
fn derive_bmc_secure(
subject: MachineIntakeSubject,
observation: BmcCredentialRotationObservation,
policy: IntakeQualificationPolicy,
policy: MachineQualificationPolicy,
) -> BmcSecureStanding {
let outcome = if same_intake_subject(left: subject, right: observation.subject) == false {
BmcSecureRefused { cause: RotationObservationForOtherAttempt { expected: subject, found: observation.subject } }
} else {
adjudicate_bootstrap(observation: observation, environment: policy.environment)
adjudicate_bootstrap(observation: observation, admits: policy.admits)
}
BmcSecureStanding { subject: subject, policy: policy, outcome: outcome }
}
Expand Down Expand Up @@ -1130,7 +1128,7 @@ fn bmc_secure_phase_receipt(
subject: standing.subject,
phase: bmc_secure_phase,
producer: producer,
policy_digest: intake_qualification_policy_digest(policy: standing.policy),
policy_digest: machine_qualification_policy_digest(policy: standing.policy),
started_at: started_at,
ended_at: ended_at,
observations: bmc_secure_receipt_observations(standing: standing),
Expand Down Expand Up @@ -1319,7 +1317,7 @@ fn managed_reference_same(a: ManagedCredentialReference, b: ManagedCredentialRef
type BmcSecureGoal {
managed: ManagedCredentialReference
published_break_glass: ManagedCredentialReference
policy: IntakeQualificationPolicy
policy: MachineQualificationPolicy
}

// WHAT AN ASSESSMENT FOUND. The conjunction's own causes, plus the published account's replacement:
Expand Down Expand Up @@ -1361,7 +1359,7 @@ type BmcSecureStateRefusal
// published one still accepted or still holding channel access). An unknown is a reading that did not
// establish a state; it is never a deviation, because writing on an unread controller is the
// absorbing fallback DESIGN §5 forbids. Everything else -- an ordering, a duplicated or unmatched
// reading, a production retention -- refuses the assessment.
// reading, a retention under a ProdRisk-admitting policy -- refuses the assessment.
// THE ONLY ADMITTED ACTION IS A PASSWORD WRITE (IpmiSetUserPassword over a grounded route). It cannot
// give a LAN channel an address, set a channel's privilege to NO ACCESS, or put the factory password
// back, so a deviation only those operations change is not remediable here: it refuses with the
Expand Down Expand Up @@ -1402,7 +1400,7 @@ fn conjunction_cause_class(cause: BmcSecureRefusalCause) -> ConjunctionCauseClas
PublishedCredentialCensusMemberUnprobed { channel: _ } => CauseUnestablishedReading
PublishedCredentialProbeDuplicate { channel: _ } => CauseRefusesAssessment
PublishedCredentialProbeUnmatched { channel: _ } => CauseRefusesAssessment
PublishedCredentialRetainedNotAdmittedForProduction => CauseRefusesAssessment
PublishedCredentialRetainedNotAdmittedByProdRiskPolicy => CauseRefusesAssessment
PublishedCredentialNotRetained { channel: _ } => CauseNeedsUngroundedOperation { operation: PublishedFactoryCredentialRestore }
}
}
Expand Down Expand Up @@ -1431,7 +1429,7 @@ fn conjunction_over_observation(goal: BmcSecureGoal, observed: BmcAccountStateOb
probes: map(observed.published_probes, p => PublishedCredentialLanProbe { channel: p.channel, address: p.address, outcome: observed_probe_at_join(probe: p.probe) }),
published_user: observed.published_user,
published_account: observed_published_account_at_join(account: observed.published_account),
environment: goal.policy.environment,
admits: goal.policy.admits,
)
}
}
Expand Down
58 changes: 28 additions & 30 deletions dag/gunbc/machine_intake/disposition.dag
Original file line number Diff line number Diff line change
Expand Up @@ -10,22 +10,20 @@ import gunbc.machine_intake_subject {
merge_subject_currency,
compare_qualification_subject,
}
import gunbc.deployment_risk { DeploymentRiskClass, ProdRisk, TestRisk }
import gunbc.machine_intake_phase {
ArrivalHardwareQualification,
DevelopmentAndTest,
IntakePhase,
IntakeQualificationPolicy,
MachineQualificationPolicy,
IntakeTransaction,
MachineOperatingEnvironment,
OsProvisioning,
PlacementCommissioning,
Production,
QualificationRefusalOwner,
UnitHardware,
fleet_admission_required_phases,
intake_phase_transaction,
intake_qualification_policy,
intake_qualification_policy_digest,
machine_qualification_policy,
machine_qualification_policy_digest,
}
import gunbc.machine_intake_receipt {
EvidenceRef,
Expand Down Expand Up @@ -125,7 +123,7 @@ type FleetAdmissionReceipt {
subject: QualificationSubject
ledger_terminal_fingerprint: ContentHash
policy_digest: ContentHash
environment: MachineOperatingEnvironment
admits: DeploymentRiskClass
satisfied: List<PhaseReceiptBinding>
derived_at: EpochMs
}
Expand All @@ -138,7 +136,7 @@ type FleetAdmissionStanding
subject_mismatched: List<IntakePhase>
subject_currency: SubjectCurrency
}
| FleetPolicyBarMismatch { ledger_digest: ContentHash, bar: IntakeQualificationPolicy }
| FleetPolicyBarMismatch { ledger_digest: ContentHash, bar: MachineQualificationPolicy }

type AdmissionFold {
satisfied: List<PhaseReceiptBinding>
Expand All @@ -163,10 +161,10 @@ type AdmissionFold {
fn derive_fleet_admission(
observed_subject: QualificationSubject,
ledger: ValidatedIntakeReceiptLedger,
policy: IntakeQualificationPolicy,
policy: MachineQualificationPolicy,
now: EpochMs,
) -> FleetAdmissionStanding {
if content_hash_equal(left: ledger.policy_digest, right: intake_qualification_policy_digest(policy: policy)) == false {
if content_hash_equal(left: ledger.policy_digest, right: machine_qualification_policy_digest(policy: policy)) == false {
FleetPolicyBarMismatch { ledger_digest: ledger.policy_digest, bar: policy }
} else {
let receipts = ledger.ordered_receipts
Expand Down Expand Up @@ -194,7 +192,7 @@ fn derive_fleet_admission(
subject: observed_subject,
ledger_terminal_fingerprint: ledger.terminal_fingerprint,
policy_digest: ledger.policy_digest,
environment: policy.environment,
admits: policy.admits,
satisfied: folded.satisfied,
derived_at: now,
},
Expand Down Expand Up @@ -225,7 +223,7 @@ type PartsHoldReason
| PhaseNotYetObserved { phase: IntakePhase }
| PlacementQualificationPending
| QualificationSubjectStale { currency: SubjectCurrency }
| QualificationPolicyBarMismatch { ledger_digest: ContentHash, bar: IntakeQualificationPolicy }
| QualificationPolicyBarMismatch { ledger_digest: ContentHash, bar: MachineQualificationPolicy }

type MachineIntakeDisposition
= Admitted { admission_receipt: FleetAdmissionReceipt }
Expand Down Expand Up @@ -262,34 +260,34 @@ fn first_phase(phases: List<IntakePhase>) -> IntakePhase? {
// defect inside an open return window is the only path to ReturnWindow; every
// other owner's refusal, every unobserved phase and every stale subject is a
// PartsHold with its reason — loud, and never a false hardware diagnosis.
fn environment_of_qualification_digest(digest: ContentHash) -> MachineOperatingEnvironment? {
if content_hash_equal(left: digest, right: intake_qualification_policy_digest(policy: intake_qualification_policy(environment: DevelopmentAndTest))) {
Present { value: DevelopmentAndTest }
} else if content_hash_equal(left: digest, right: intake_qualification_policy_digest(policy: intake_qualification_policy(environment: Production))) {
Present { value: Production }
fn admitted_class_of_qualification_digest(digest: ContentHash) -> DeploymentRiskClass? {
if content_hash_equal(left: digest, right: machine_qualification_policy_digest(policy: machine_qualification_policy(admits: TestRisk))) {
Present { value: TestRisk }
} else if content_hash_equal(left: digest, right: machine_qualification_policy_digest(policy: machine_qualification_policy(admits: ProdRisk))) {
Present { value: ProdRisk }
} else {
none
}
}

fn policy_bar_mismatch_cause(ledger_digest: ContentHash, bar: IntakeQualificationPolicy) -> NonEmptyStr {
match environment_of_qualification_digest(digest: ledger_digest) {
fn policy_bar_mismatch_cause(ledger_digest: ContentHash, bar: MachineQualificationPolicy) -> NonEmptyStr {
match admitted_class_of_qualification_digest(digest: ledger_digest) {
Absent =>
match bar.environment {
Production => "ledger policy digest does not match the Production admission bar"
DevelopmentAndTest => "ledger policy digest does not match the DevelopmentAndTest admission bar"
match bar.admits {
ProdRisk => "ledger policy digest does not match the ProdRisk-admitting admission bar"
TestRisk => "ledger policy digest does not match the TestRisk-admitting admission bar"
}
Present { value: ledger_env } =>
match ledger_env {
DevelopmentAndTest =>
match bar.environment {
Production => "ledger was derived under DevelopmentAndTest; the admission bar is Production"
DevelopmentAndTest => "ledger policy digest does not match the DevelopmentAndTest admission bar"
TestRisk =>
match bar.admits {
ProdRisk => "ledger was derived under a TestRisk-admitting policy; the admission bar admits ProdRisk"
TestRisk => "ledger policy digest does not match the TestRisk-admitting admission bar"
}
Production =>
match bar.environment {
DevelopmentAndTest => "ledger was derived under Production; the admission bar is DevelopmentAndTest"
Production => "ledger policy digest does not match the Production admission bar"
ProdRisk =>
match bar.admits {
TestRisk => "ledger was derived under a ProdRisk-admitting policy; the admission bar admits TestRisk"
ProdRisk => "ledger policy digest does not match the ProdRisk-admitting admission bar"
}
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,8 @@ import gunbc.machine_intake_subject {
qualification_subject_of,
}
import gunbc.machine_intake_receipt { EvidenceRef }
import gunbc.machine_intake_phase { DevelopmentAndTest, intake_qualification_policy }
import gunbc.deployment_risk { TestRisk }
import gunbc.machine_intake_phase { machine_qualification_policy }
import gunbc.machine_intake_bmc_secure {
BmcCredentialRotationObservation,
BmcSecured,
Expand Down Expand Up @@ -243,7 +244,7 @@ fn mtcollins1_bmc_secure_standing() -> BmcSecureStanding? {
value: derive_bmc_secure(
subject: subject,
observation: observation,
policy: intake_qualification_policy(environment: DevelopmentAndTest),
policy: machine_qualification_policy(admits: TestRisk),
),
}
}
Expand Down
Loading