Managed-host cut O1a-2: IPMI Set User Access as a second route request shape

[gunbai-bot]

Stacked on #13177 (base session/bright-wolf-485, which is in the merge queue); the diff is O1a-2 only. Ruled by eager-gull-22, 2026-10-04, dispatched by warm-crane-577.

Why

The only grounded account operation was IpmiSetUserPassword, and a password write cannot set a channel privilege limit to NO ACCESS. The BmcSecure conjunction needs the published account refused on every LAN census member, so O1b (#13221) refuses mtcollins1's post-reflash state with a typed cause naming a missing operation. That operation is IPMI Set User Access (IPMI v2.0, App 43h).

What

• Request shape. BmcAccountWriteRequest gains IpmiSetUserAccess { access: IpmiUserChannelAccess }. It reuses extdeps.bmc.ipmi_channel's (channel, user, privilege) row, the shape Get User Access returns; no parallel vocabulary.

  • account_write_request_eq compares every field.
  • rotation_route_request_identity encodes user, channel and privilege, each length-prefixed (canonical_ipmi_privilege).

• Apply admission names its request.

  • New signature: admit_rotation_apply(standing, target_endpoint, target_firmware, request, approval).
  • A route grounds an operation: account_write_request_same_operation compares command kind, and for Redfish both refs.
  • A grounded route of one operation refuses an Apply of another with RotationApplyRouteForAnotherOperation {grounded, requested}.
  • The approval identity still binds the exact request, every field.

• gunbc.bmc_model transition.

  • BmcWorld gains ipmi_user_access: List<IpmiUserChannelAccess>; every literal site is in the module.
  • bmc_ipmi_set_user_access sets exactly one (channel, user) row, and only for a user the IPMI table holds.
  • bmc_ipmi_get_user_access is the readback.

• Dry path. dry_route_qualification_request gains the Set User Access arm. It mints only ModeledRouteQualificationResponse, so, exactly as for the password shape, it cannot ground a production route.

• mtcollins1 row (gunbc.machine_intake_bmc_rotation_route_evidence mtcollins1_channel_access_route_standing): a RouteQualificationCandidate, not grounded, because no execution is committed.

  • Endpoint 192.168.1.228.
  • Build 0.45.3, the installed release mt_collins_bmc_0_45_3_hpm; the reflash is recorded by credential_effect_of. It is not 0.32, and the executed password route at 0.32 does not carry over: an Apply at 0.45.3 refuses another-build.
  • Request: published user 2 → NO ACCESS on channel 2. The channel is the operator's report that admin holds ch2/ch3 after the reflash. That report is not a committed observation.
  • Evidence: PublicStandardOperation (the IPMI v2.0 spec) only.
  • Missing read-only observations, none committed: Get Channel Info for channels 0h–Fh (the post-reflash census); Get User Access for the published user on every channel the census returns; a version readback (Get Device ID / mc info) of the installed BMC build.

• mtjade1 gets nothing in this cut.

• Census. New row route_qualification_channel_access_effect() at site qualify_rotation_route, with its own characteristics:

  • DeviceOnce;
  • IrreversibleEffect: a privilege write to the wrong user or channel can remove the last administrator's LAN access;
  • ApiSurface;
  • unbindable workload identity;
  • MintsNoCredential;
  • realized RealizedApprovalCapability.

  The witness executes select_authorization_pattern on that row: OperatorApprovedCapability, Conforms.

No live call, no workflow change, no hardware. The live qualification on mtcollins1 is operator-gated and not in this PR. lively-eagle-811 (O1b) has the type names and the signature change.

Terminal receipt (exact head 0f35b65)

Binaries were built at the pin on BuildBuddy in a self-bound 20 GiB cgroup: gunbc 26e123acafc40ebe92a38a354af37d55566d07a590b89f1240ef6a60595d28f7, claim_batch 568d0abcaa3ac89fb85e908c9a34060c8f99b3df67e416c14a9c009c3c08ed71.

Roster. The changed roots are the same as #13177's (bmc_model, the route module and its evidence, privileged_effect_census), so the consumer roster is #13177's, recomputed.

witness	mode	result
machine_intake_bmc_rotation_route_witness_test	wet	18/0 (13 + 5 new)
forged probe	wet	3/0
operation_realization	claim_batch --hermetic	18/0
mtcollins1_boot_acceptance_matrix	claim_batch --hermetic	28/0
bmc_factory_credential	wet	2/0
observability_channel_routing	wet	6/0
authorization_pattern_selection	wet	23/0
approval_broker_helper_grant	wet	18/1 (pre-existing)
bmc_model_web_kvm	wet	9/0
boot_world_models	wet	7/0
bmc_onboarding_quarantine	wet	4/0
mtjade1_recorded_manager_capture	wet	2/0
kvm_observer_protocol_wet	wet	7/7 (pre-existing)
gcp_iam_converge	wet	UNMEASURED: same resolve error set as base, lines 387–399

Every result matches #13177's head and its base except the new claims. The fleet-converge yml digest is e7a83734ce133890, len 344860, identical.

New controls:

• channel_access_requests_differing_in_any_one_field_are_different_requests: varying only the channel, only the privilege, or only the user makes the requests unequal, and each refuses as another request.
• mtcollins1_channel_access_route_is_an_ungrounded_candidate_on_its_current_build
• a_modeled_channel_access_run_would_qualify_but_grounds_nothing
• a_grounded_password_route_does_not_admit_a_channel_access_apply (RED: grounded password route + channel-access Apply → another-operation; positive: a password Apply on the same route → admitted)
• the_channel_access_qualification_effect_is_classified_by_executing_the_selection

Same-path REDs (each mutation applied, the witness run, the tree restored clean; only the listed claim FAILs):

mutation	FAILs
N1: identity and equality drop the channel	channel_access_requests_differing_in_any_one_field…
N2: operation check collapsed across the IPMI shapes	a_grounded_password_route_does_not_admit_a_channel_access_apply
N3: modeled Set User Access completes but writes nothing	a_modeled_channel_access_run_would_qualify_but_grounds_nothing
N4: mtcollins1 candidate keyed on pre-reflash 0.32	mtcollins1_channel_access_route_is_an_ungrounded_candidate_on_its_current_build
N5: census row realized by federation	the_channel_access_qualification_effect_is_classified_by_executing_the_selection

Sweep. No name was deleted in this cut. The only signature change is admit_rotation_apply's new request parameter; its callers are this witness and, once it lands, O1b.

🤖 Generated with Claude Code

[briansrls]

Reviewed current exact head 7887d74ed29fd8127fa141e274df9a9162ff1737. The requested 0f35b65e34 head advanced by two commits while I was reviewing; those commits add the lockout guard, so this review is anchored to the stronger current head.

The core request modeling is directionally sound: Set User Access has structural equality over user/channel/privilege, the approval identity carries all of those fields, Apply distinguishes password vs channel-access operations, the dry realization cannot ground a production route, and mtcollins1 remains only a current-build candidate. The requested lockout rule is also present in one place: ordinary admit_rotation_apply refuses an absent, cross-attempt, same-user, or wrong-channel administrator readback.

Four load-bearing issues remain.

1. The lockout guard runs after the first dangerous write

The first real Set User Access write will be the route-qualification effect, not the later BmcSecure Apply. The mtcollins1 candidate itself is user 2 -> NO ACCESS on channel 2. A future live realization must execute that write before it can mint RouteQualificationLiveResponse; only afterwards does qualify_rotation_route ground the route.

administrator_retention_refusal currently runs only inside admit_rotation_apply, after a route is already grounded. Therefore it protects a later ordinary Apply but not the qualification write that can cause the lockout in the first place. route_qualification_live_frontier also does not require this precondition.

The live qualification boundary needs its own pre-write admission. It should accept a sealed qualification subject plus the same administrator-retention receipt and produce the only value from which the transport call may be made. Alternatively, qualify the operation with a demonstrably non-destructive request rather than closing the factory administrator.

Required RED:

mtcollins1 channel-access candidate
+ exact qualification approval
+ no current managed-administrator receipt
-> cannot issue the transport request or mint a live response

A modeled response or a post-write check is not that control.

2. ManagedAdministratorReadback is authored data, not a readback standing

The type is an open record containing only {attempt, managed_user, access}. Any caller can author the successful row the witness authors. It is not bound to:

• the machine/intake subject;
• endpoint or firmware build;
• the goal-bound managed account;
• successful authentication of that account;
• content-addressed Get User Access evidence;
• an observer time ordered before the write;
• a unique (channel, user) result.

The any(...) test also accepts an Administrator row beside a contradictory duplicate row. Comparing a caller-authored attempt string with the approval attempt does not establish “read in this run.”

Replace this with a sealed, evidence-bound receipt projected from the current account observation/read path. It should bind at least subject, endpoint, firmware, attempt, goal-bound managed user, exact channel, unique Administrator result, evidence, and pre-write ordering. Missing, unreadable, duplicated/conflicting, stale, another-controller/build, or another-account observations must refuse.

The witness should obtain the positive carrier through that mint rather than spelling ManagedAdministratorReadback { ... } directly, and a forged-literal probe should refuse.

3. The privileged-effect census has two incompatible rows for one site identity

Both rows use the exact same key:

gunbc.machine_intake_bmc_rotation_route::qualify_rotation_route

but one effect says MintsResourceScopedCredential and the other says MintsNoCredential. PrivilegedEffectSite.site is only a DeclarationRef, and SiteVerdict retains only that site. The new witness distinguishes the duplicate rows by searching free-text effect.subject for “channel-access route,” which is a hidden second key rather than a typed authority.

Split the password and channel-access qualification effects into distinct effect entrypoints that may delegate to one shared classifier; or extend the census identity with a typed request/effect discriminator. If the site remains one function, it needs one conservative effect classification. Two meanings under one declaration identity violate the census’s own site-grain model.

4. The stated landing order is not represented by this head

This branch is still based only on #13177. Current #13221 calls the pre-O1a-2 admit_rotation_apply signature and does not handle IpmiSetUserAccess, RotationApplyRouteForAnotherOperation, RotationApplyWouldLeaveNoAdministrator, or the administrator receipt. After #13221 lands, this PR must merge/rebase it and make O1b consume the new request and sealed precondition on the real planning path. The final stacked head needs another exact-head integration review; the old 0f35 receipt does not cover either the two lockout commits or that merge.

One precision obligation should be pinned while doing this: the modeled request is specifically the privilege-limit-only form of Set User Access. IpmiUserChannelAccess is the Get User Access projection, while the full command has additional controls. Name or type the restricted operation and require the future live transport to use that mode; do not ground a broader generic Set User Access operation from the narrower model.

No exact-head CI run is attached to 7887d74 yet. The existing witness receipt is useful for the original request/equality changes, but it does not close the construction and effect-order findings above.

[gunbai-bot]

Lockout hazard is now a refusal (warm-crane-577's addition), head 7887d74.

• admit_rotation_apply gains a typed admission input, managed_readback: ManagedAdministratorReadback?, with fields {attempt: AttemptIdentity, managed_user: IpmiUserId, access: List<IpmiUserChannelAccess>}.
• A Set User Access write that lowers a privilege (anything but ADMINISTRATOR) is admitted only if:
  • the readback names the approval's own attempt, i.e. it was read back in the same run;
  • its managed user is not the user being closed;
  • it shows that managed user at ADMINISTRATOR on the same channel.
• Otherwise it refuses with RotationApplyWouldLeaveNoAdministrator { channel, cause }. The cause is one of ManagedReadbackAbsent, ManagedReadbackFromAnotherRun, ManagedAccountIsTheClosedAccount or ManagedAccountNotAdministratorOnChannel.
• The readback's producer is O1b's BmcSecure observation; here it is an admission input.

New claim a_channel_access_write_that_could_lock_out_every_administrator_is_unplannable (grounded channel-access route, exact approval of closing user 2 on ch2):

• no readback → refused;
• managed user 3 at ADMINISTRATOR on ch2 in the same attempt → admitted;
• the same readback from another run → refused;
• a readback whose managed account is the closed one → refused;
• administrator only on ch1 → refused.

Receipt at 7887d74 (gunbc 32898386a190488eecea107a6cdbdbd9afd18d4e882239aeb15b0665ea9deec3, built at the pin on BuildBuddy):

• route witness 19/0;
• forged probe 3/0;
• same-path RED L1 (precondition not required) → the new claim FAILs;
• same-path RED L2 (readback not bound to the run) → the new claim FAILs;
• every other claim PASSes; restored clean.

The first push (6ee95d0) failed to resolve because the citation mint admitted the test function while its helper lockout_verdict made the call. That was fixed in 7887d74, so the first run measured nothing.

— sent from bright-wolf-485

[gunbai-bot]

ManagedAdministratorReadback is sealed (warm-crane-577's check), head b66626e.

• Sealed carrier: the type is sole_constructor { endpoint, firmware, attempt, managed_user, access }.
• No production mint: its only production mint, the live Get User Access read in the run, does not exist in this cut. That is the declared managed_administrator_readback_live_frontier: until it lands, every privilege-lowering channel-access write refuses in production.
• Witness fixture: the one other mint, managed_administrator_readback_fixture, is admit_callers-restricted to the witness helper readback_at.
• Binding: the admission checks the readback's endpoint and build against the route standing (ManagedReadbackFromAnotherController / ManagedReadbackFromAnotherBuild), then its attempt against the approval.
• Controls:
  • a_readback_from_another_controller_or_build_does_not_unlock_a_close: an A-readback on a B-route refuses, another build refuses, and the same readback on its own controller is admitted.
  • The forged probe now also pins SoleConstructorViolation at ManagedAdministratorReadback and ConstructorCallAdmissionRefused at managed_administrator_readback_fixture.

Receipt at b66626e (gunbc c98fddd319a9618cfe069e8ac10976aa2cf6b81deb3dabe3ea06407394948877, built at the pin on BuildBuddy):

• route witness 20/0;
• forged probe 3/0.

Same-path REDs, each restored clean:

mutation	result
R1: unsealed	forged-literal claim FAILs, 2 PASS
R2: endpoint binding removed	A/B claim FAILs, 19 PASS
R3: fixture unrestricted	mint claim FAILs, 2 PASS

— sent from bright-wolf-485

[gunbai-bot]

Side-chat review of 7887d74: items 1, 3 and the precision point are addressed at 44f35f6. Items 2 and 4 complete after #13221 lands.

Item 1: pre-write qualification admission.

• AdmittedRouteQualificationRequest is sealed and minted only by the two per-shape effect entrypoints, admit_password_route_qualification and admit_privilege_limit_route_qualification. It is the only input route_qualification_live_frontier permits a live transport call from.
• A privilege-limit request needs, before any write, a same-run ManagedAdministratorReadback for the same controller and build, showing the managed account at ADMINISTRATOR on that channel as the unique (channel, user) row. A lowering write also requires that the managed account is not the one being lowered.
• The qualifying request is non-destructive. mtcollins1's candidate now re-asserts the managed account's own ADMINISTRATOR limit on channel 1 (user 3, its pre-reflash id). The pre-write admission requires the same-run readback to show exactly that value already, so the write changes no access but still exercises the command and its readback. If the post-reflash id or channel differs, the readback refuses and nothing is written. Closing the factory administrator becomes an Apply over the grounded route, under the same retention precondition.
• Controls:
  • the_mtcollins1_channel_access_candidate_cannot_issue_a_request_without_a_current_receipt: candidate + exact qualification approval + no receipt refuses before any write (ManagedReadbackAbsent), so there is no admitted request and no transport call. The password entrypoint refuses the candidate as another operation.
  • the_prewrite_admission_admits_only_with_the_same_run_receipt
  • a_duplicated_managed_readback_row_refuses: an ADMINISTRATOR row beside a contradictory NO ACCESS row refuses.

Item 3: the census rows are keyed by the two entrypoint sites, with no second key in prose, and each is classified by executing the selection.

Precision: the arm is renamed IpmiSetUserPrivilegeLimit, the privilege-limit-only form of Set User Access (request byte 1 bit 7 clear; callback, link-auth and IPMI-messaging bits unchanged; no session limit). Its text, canonical tag and census subject say so. The live transport must issue exactly that mode, and a route grounded by it grounds only that operation.

Receipt at 44f35f6 (gunbc f6a5a939a487240379d16e32a0acc8eb46308cc2ec9f763991167edb88ffd86d, built at the pin on BuildBuddy): route witness 23/0, forged probe 3/0, which now also pins SoleConstructorViolation at AdmittedRouteQualificationRequest.

Same-path REDs, each restored clean:

mutation	FAILs
Q1: pre-write admission skips the receipt	both pre-write claims; 21 PASS
Q2: admitted request unsealed	the forged-literal claim
Q3: duplicate rows accepted	a_duplicated_managed_readback_row_refuses
Q4: the two census rows share one site again	both classification claims

The merge head cc8d6cd had the full roster re-run: identical to base except the route witnesses, and the yml digest is unchanged.

— sent from bright-wolf-485

[gunbai-bot]

Discrimination of the qualifying request (warm-crane-577's question): chose (b), at head 6d27741.

• RouteGroundedByExecutedRequest now carries effect: RouteEffectStanding = EffectObserved | AcceptedEffectUnobserved.
• It is computed, not declared. Both response carriers hold the effect standing, set at their mint by effect_of(before_matched, after_matched): EffectObserved only when the reading before the write differed from the requested value and the readback after matched. The dry realization reads the world before and after. The live mint, when it exists, is bound by route_qualification_live_frontier to make the same comparison.
• mtcollins1's idempotent qualifying request (re-assert managed user 3 at ADMINISTRATOR on ch1) therefore grounds acceptance only.
• The closing write needs the effect. admit_rotation_apply refuses a privilege-lowering write unless the route's effect was observed (RotationApplyRouteEffectUnobserved). A cited source for the build counts as stating the effect.
• mtcollins1's committed password grounding is EffectObserved. The value set was a newly minted secret the account did not hold, and step (d) authenticated with it.
• Why (b), not (a): no committed post-reflash observation identifies a disabled or unused slot, so (a) would refuse on every input today. A discriminating qualification of the privilege-limit operation must wait for that read-only observation, or for a non-destructive request whose before-reading differs.

RED: an_accept_only_grounding_does_not_admit_the_closing_write. A grounded privilege-limit route with AcceptedEffectUnobserved, given an exact approval of closing user 2 on ch2 and a valid same-run managed-administrator readback, refuses effect-unobserved; the same with EffectObserved is admitted. Also an_idempotent_qualifying_write_grounds_acceptance_only: the modeled run reports accepted-only when the value was already present, and observed when it differed.

Rung.

• Structurally guaranteed (rung 3) for the admission decision: no admitted program reaches RotationApplyAdmitted for a lowering write over an accept-only grounding. The witness's executed-route fixture is admit_callers-restricted, and the forged probe pins ConstructorCallAdmissionRefused at it.
• Mechanically preventable (rung 2) for the effect standing's truth on the live path: it depends on the future live mint computing the before/after comparison, which is a frontier obligation enforced by review, not construction.

Receipt at 6d27741 (gunbc 2de2cbe518b3c10e83b3e70ca42b001161f7b164d3f60bf4e0e7e5c5c699e363, built at the pin on BuildBuddy): route witness 25/0, forged probe 3/0.

Same-path REDs, each restored clean:

mutation	FAILs
E1: the lowering Apply does not require EffectObserved	the accept-only RED only; 24 PASS
E2: effect computed from the readback alone	the idempotent claim only; 24 PASS

— sent from bright-wolf-485

[briansrls]

REQUEST_CHANGES at current exact head 6d277411fdb4d5f5d280dbe8edc70137812ab243, against DESIGN.md §§3, 3c, 4b and 5.

Accepted repairs: the request is now explicitly privilege-limit-only; pre-write qualification admission exists; password and privilege-limit census sites have distinct declaration identities; retention rejects another controller/build/attempt and duplicate rows; idempotent acceptance is distinguished from an observed effect; a lowering Apply refuses accept-only grounding. mtcollins1 is still a candidate, not an executed channel-access route.

1. Two sanctioned-constructor proxies still export authored production evidence. The restricted managed_administrator_readback_fixture admits witness helper readback_at, but that helper is unrestricted and returns ManagedAdministratorReadback? for arbitrary endpoint/build/attempt/user/rows. An outside caller can call it to satisfy the supposedly unavailable production retention precondition. Likewise, the restricted rotation_route_executed_fixture admits unrestricted executed_route_at, which returns BmcRotationRouteStanding with a freely chosen request and EffectObserved at the lab endpoint/build. The forged probes call the underlying restricted mints directly, not these admitted wrappers. Delete the exported-carrier facades or confine them to exact tests which consume their carriers internally and return only diagnostic values. Add outside-call REDs through both wrappers. The comment claiming no production caller can satisfy the precondition is false while readback_at remains callable.

2. The chosen qualification is not yet guaranteed to be an idempotent reassertion of the managed account. For mtcollins1's candidate (user 3, channel 1, ADMINISTRATOR), administrator_retention_refusal permits a receipt whose managed_user is 4 with a unique Administrator row for user 4 on channel 1. It does not require the request's target user to be that managed user or to have already held the requested value. A post-reflash managed-id change can therefore admit this candidate, contrary to the evidence row's explicit promise that a differing managed id refuses; the request could instead grant user 3 a new privilege. At the non-destructive qualification boundary, establish that the exact target pair already has the requested limit, using the goal-bound managed account. Add the discriminator: target user 3 + receipt only for managed user 4 -> no qualification request; target user 3 + its exact current Administrator reading -> admitted. This need not prohibit separately modeled, operator-approved effectful qualification requests.

3. The live frontiers still name less than the previously required capability. managed_administrator_readback_live_frontier requires controller/build/run plus response bytes but does not require successful authentication of the goal-bound managed account or an observation ordered before this write. route_qualification_live_frontier also does not require the before/after comparison that the latest comment says will establish EffectObserved. A future mint could meet those written triggers while labeling a cached access row as retention or an idempotent write as an observed effect. Preserve the full missing capability in the frontiers: goal/account authentication and subject binding, unique channel/user access evidence, pre-write ordering, and for effect standing, an established differing pre-read plus the matching post-read. Missing/unread pre-state is not evidence of difference. This is a frontier correction, not a demand to implement live writes in this cut.

The #13221 integration/order remains a separate exact-head obligation when that stack is assembled; #13285 is not covered by this review. The reported 25/0 and 3/0 receipts cover their executed controls, not the wrapper paths above. No live write or local test was performed by this reviewer.

[gunbai-bot]

Side-chat review of 6d27741: all three items are addressed at e12070a.

1. No carrier-returning facades.

• The witness helpers readback_at and executed_route_at are deleted.
• managed_administrator_readback_fixture and rotation_route_executed_fixture are now admit_callers-restricted to the exact claims that mint and consume their carrier and return only a Bool.
• No function in the witness returns a ManagedAdministratorReadback or a grounded standing. The remaining standing-returning helpers return only open-mint candidates, and lockout_verdict / closing_verdict return diagnostic strings.
• Because the wrappers no longer exist, there is no wrapper path for an outside caller. The outside-call REDs remain at the underlying mints in the forged probe (ConstructorCallAdmissionRefused at both fixtures).
• The comment that no production caller can satisfy the precondition is now true and is restated in the frontier.

2. Idempotent qualification re-asserts the managed account's own current value.

• qualification_retention_refusal, used only at the pre-write qualification boundary, requires a non-lowering request's target user to be the readback's managed account.
• Combined with retention, which already requires that account's unique ADMINISTRATOR row on the target channel, the exact target pair must already hold the requested limit. A non-lowering request is always ADMINISTRATOR.
• An earlier revision (4fe9f69) also carried an explicit holds-value check. Its REDs showed the check was implied, so it is deleted rather than kept as a decoration.
• Discriminator the_idempotent_qualification_requires_the_target_pair_to_already_hold_the_value, for target user 3 on ch1:
  • a receipt for managed user 4 → target-not-managed, even though it carries an ADMINISTRATOR row for user 3;
  • user 3 at OPERATOR on ch1 → not-administrator-on-channel;
  • user 3's exact ADMINISTRATOR reading → admitted.

3. The live frontiers name the full capability.

• managed_administrator_readback_live_frontier requires: authentication of the goal-bound managed account bound to the machine/intake subject; the endpoint, build and attempt observed in the run; unique per-pair Get User Access evidence, content-addressed; and observer time ordered before the write. Missing, unreadable, duplicated, conflicting, stale, other-controller, other-build and other-account readings refuse.
• route_qualification_live_frontier requires the transport call only from an AdmittedRouteQualificationRequest whose receipt met that in full, and EffectObserved only from an established differing pre-read plus a matching post-read. A missing or unread pre-state is never a difference.
• Frontier text only; no live write.

Receipt at exact head e12070a (gunbc 8c7032f4d0ca81cf1dea1f2ee0b8fe470c69aedbaf59ac7df8e9867e24a10bf9, claim_batch f94cd846722b66050b6773c3339b4e8954f49abec629f3acc50d0ac0ee9f268f, built at the pin on BuildBuddy in a self-bound cgroup):

witness	result
route witness	26/0
forged probe	3/0
claim_batch --hermetic operation_realization	18/0
claim_batch --hermetic mtcollins1_boot_acceptance_matrix	28/0
bmc_factory_credential	2/0
observability_channel_routing	6/0
authorization_pattern_selection	23/0
approval_broker_helper_grant	18/1 (pre-existing)
bmc_model_web_kvm	9/0
boot_world_models	7/0
bmc_onboarding_quarantine	4/0
mtjade1_recorded_manager_capture	2/0
kvm_observer_protocol_wet	7/7 (pre-existing)
gcp_iam_converge	UNMEASURED: same resolve error set as base, lines 387–399

The fleet-converge yml digest is e7a83734ce133890, len 344860, unchanged.

Same-path REDs at e12070a, each restored clean:

mutation	FAILs
T1: target need not be the managed account	the discriminator only; 25 PASS
T2: the managed account need not hold ADMINISTRATOR on the channel	the discriminator and the lockout claim; 24 PASS

— sent from bright-wolf-485

[briansrls]

APPROVE at exact head e12070ae03d57004769b851dba056fc012b4890b, against DESIGN.md §§3, 4b and 5. All three items from the review of 6d277411fdb4d5f5d280dbe8edc70137812ab243 are closed.

1. The fixture-constructor proxies are deleted. readback_at and executed_route_at no longer exist. managed_administrator_readback_fixture admits six exact claims, and rotation_route_executed_fixture admits only an_accept_only_grounding_does_not_admit_the_closing_write. I checked those callers: they mint and consume their carriers internally and return Bool. The remaining verdict helpers return diagnostic strings, not readbacks or executed groundings. The enrolled forged probe directly calls both surviving fixture mints and requires ConstructorCallAdmissionRefused at each exact callee; its clean-source control requires neither wall class. With the exporting wrappers gone, those probes cover the remaining fixture-construction boundary.

2. The idempotent qualification now requires the target to be the readback's managed account, after the ordinary retention check. The removed holds-value check is genuinely redundant here: lowers_privilege is false only for ADMINISTRATOR, while successful retention already requires exactly one ADMINISTRATOR row for the managed user on the requested channel. Joining the target user to that managed user therefore establishes that the exact target pair already holds the requested value. No separate duplicate check is needed. The control discriminates managed user 4 even when user 3 also has an ADMINISTRATOR row, user 3 at OPERATOR, and the exact user-3 ADMINISTRATOR positive. The reported T1/T2 mutants exercise the target join and existing retention authority respectively. Effectful lowering qualification still requires ordinary administrator retention; an accept-only grounding still cannot authorize a later lowering Apply.

3. Both live frontiers now state the missing capability in full. The managed readback requires successful authentication of the goal-bound account and machine/intake binding, the endpoint/build/attempt observed in the run, unique per-pair Get User Access evidence with content-addressed response bytes, and pre-write ordering. Qualification must consume its admitted request and satisfy that precondition; EffectObserved requires an established differing pre-state plus a matching post-state. Missing or unread pre-state is not a difference. These remain live implementation obligations, not claims that the fixture or the dry realization executed a controller write.

Reviewed the two-commit, two-file correction from the prior head, the exact-head retention and qualification paths, all admitted fixture callers, the existing compiler probes, DESIGN, and the updated execution receipt in the discussion. Route 26/0, forged 3/0, Hermetic operation_realization 18/0, matrix 28/0, unchanged YAML and the T1/T2 results are author-reported; I did not run tests, regenerate YAML or perform controller actions. Reported pre-existing failures remain unresolved baseline findings, not passes.

GitHub reports exact-head witnesses run 37248943145 completed successfully. The requested head was unchanged immediately before submission. No semantic blocker remains on this O1a-2 head. This approval does not discharge the live frontiers, authorize hardware writes, or cover the later O1b/#13285 integration head; preserve the normal required merge checks and exact-head review of that integration.

[briansrls]

REQUEST_CHANGES at the REQUESTED exact head 8960bbe51174fe68ce49603ef5bb9656f253cb44, against DESIGN.md §§3/3c, 4b and 5. The PR advanced during review to a68bb7adf65af5703fc2c42d2bffb75ded32a045; that later head is not covered here.

The original O1a-2 repairs approved at e12070a remain accepted. The merge incorporates main c84dd1e and adds the O1b/arrival signature adaptations. Moving channel access from an unimplemented-operation assessment refusal to a deviation is coherent only because the plan must now admit the particular channel writes; the new no-route, ungrounded-route, absent-approval and missing-administrator controls exercise that distinction. The production event-root remains in place and the new state-shaped route remains shadow. No live qualification or cutover is requested by this review.

Three integration blockers remain.

1. The new readback mint has an unrestricted constructor proxy

managed_administrator_readback_projected admits only gunbc.machine_intake_bmc_secure::project_managed_administrator_readback, but that wrapper is unrestricted and returns ManagedAdministratorReadback?. Any outside caller can pass it a supplied BmcAccountStateObservation, chosen managed_user and chosen attempt and receive the sealed production precondition. The wrapper does not run the subject/goal assessment. The underlying observation mint is itself an existing supplied-value interface, so sole_constructor on the observation is not provenance for this new use.

Thus the comment that this projection runs only inside the checked plan and is never received from a caller is false. The old fixture-only admission was closed; this integration opens a different export path. Confine the projection to the checked production path, with no admitted carrier-returning witness facade, or require evidence-bound input sufficient to establish its result. Add an outside-caller compiler RED through project_managed_administrator_readback, not only through the restricted literal/fixture mint.

2. Even inside the real plan, the projection relabels the attempt and managed user

admitted_channel_writes passes cl.attempt from the chosen approval into the projection. The projection copies that value into the readback; administrator_retention_refusal then compares it with the very same approval attempt. This establishes equality by assignment, not that the reading belongs to the approved run. A valid old observation from A, reused with an otherwise exact approval for B, receives a readback labelled B without any B observation. Restricting the wrapper alone will not fix this: the normal plan makes the same call.

The managed IPMI id is similarly supplied independently. The observation retains the managed credential reference and an accepted probe but does not retain the numeric user that probe authenticated. Filtering access rows for a caller-selected user does not prove that user is the goal-bound authenticated account. A receipt for that account must derive its user from the read's bound identity, not relabel another user's Administrator row.

Carry the independently established attempt and authenticated goal/account-to-IPMI-user binding from the observation producer, preserve them in this projection, and refuse disagreement with the approval/plan. Preserve the observation/evidence and pre-write ordering at this boundary as well: the present checks only establish probe/census >= read_floor, while planning checks planned_at >= read_floor; those inequalities do not establish probe/census <= planned_at. The claimed 'all ordered before the plan' does not follow.

Required discriminators on the actual plan/projection path: A's otherwise valid read plus B's approval refuses; A/A admits; another user's Administrator row cannot replace the authenticated managed user's row; a reading later than the plan cannot authorize that plan. These are modeling/dry-route controls, not a demand for a live controller read. If the production evidence binding remains unavailable, keep that carrier unavailable rather than claiming the frontier's guarantee through an authored projection.

3. The new channel-write integration has no independent dry readback

dry_apply_bmc_account_plan now changes BmcWorld.ipmi_user_access, but dry_read_bmc_account_state still assigns channel_census: census from its supplied argument. It never reads the updated world's Get User Access table. Retaining the old supplied census reports the channel open even after a successful write; supplying a hand-updated closed census can report it closed without the write. That is not an independent observation of this newly modeled effect.

The new an_open_channel_is_closed_only_over_a_grounded_channel_access_route control stops at planned:1. Existing whole-Apply controls call plan_default, which supplies channel_close:none; they do not execute a nonempty channel-write plan. The separate O1a Set User Access model test does not exercise this new plan -> application -> phase integration.

Read the relevant channel-access rows from the resulting dry world (the supplied topology may still define the census population), and exercise one nonempty real plan through dry_apply and the independent post-read/phase result. Assert the exact target user/channel/NoAccess state and the retained administrator. A mutant that drops the real channel transition while claiming completion must fail that control, rather than greening because the witness supplies a closed census. The no-route/no-approval refusals must remain. No hardware run is needed.

Reviewed the complete residual nine-file diff, merge parents, exact-head DESIGN, the new plan/projection, readback mint and retention consumer, and the existing/new dry witnesses and realization. No local tests, mutants or hardware actions were run by this reviewer. Historical O1a receipts do not measure these new integration paths; exact-head witnesses run 37259234324 is still in progress.

[gunbai-bot]

Re review 76211, on request_channel returning 0 for the password and Redfish arms: agreed it's a placeholder. As the review traces, it is unreachable: RotationApplyWouldLeaveNoAdministrator is built only after administrator_retention_refusal returns a cause, and that happens only for IpmiSetUserPrivilegeLimit.

I'm not pushing it onto this head. The exact-head roster, the Hermetic runs and the side-chat re-review are in flight at 111316f, and a push would restart all three.

The right fix is to have administrator_retention_refusal return the channel together with the cause, from inside the privilege-limit arm, so no other arm has a channel to fabricate. That goes in the next change touching this module (O1c consumes it), unless the side chat asks for it here first.

— sent from bright-wolf-485

[gunbai-bot]

Addressed in e2e8259.

Review 76265:

• ipmi_privilege_eq is deleted. account_write_request_eq and the dry readback compare IpmiChannelPrivilegeLimit with direct ==, the same route published_channels_left_open uses. canonical_ipmi_privilege remains only for the canonical identity encoding and the rendered text.
• bmc_ipmi_get_user_access takes channel: IpmiChannelNumber, so the range refinement holds at the readback. The callers pass the row's channel directly; the as Int casts are gone.

Review 76211 (the deferred request_channel placeholder), since this push restarts the runs anyway:

• request_channel is deleted.
• RotationApplyWouldLeaveNoAdministrator.channel is IpmiChannelNumber, taken from the privilege-limit request inside its own arm. The password and Redfish arms carry no channel to fabricate.

Exact-head roster, Hermetic runs and REDs are re-running at this head.

— sent from bright-wolf-485

[gunbai-bot]

Review 76375: agreed, and fixed in 5cec3b2.

The idempotent re-assertion candidate can ground only AcceptedEffectUnobserved, because its before and after readings match by construction. admit_rotation_apply refuses every privilege-lowering Apply over such a route, so the factory administrator's close is not reachable from this candidate. The evidence comment claimed it was; that wording is corrected and the gap is now stated.

The missing step is declared as mtcollins1_channel_close_effect_qualification_frontier. It needs a non-destructive and discriminating qualification with an established differing pre-read and a matching post-read, for example a spare slot identified by a committed post-reflash Get User Access observation. Neither the accept-only candidate nor a modeled run satisfies it.

That matches the exact-head comment on option (b) earlier in this PR. This is a comment and frontier change only; no code path changes.

— sent from bright-wolf-485

[gunbai-bot]

Exact-head receipt at 5cec3b2 (the O1b/O1c-1 integration plus the #13285 merge), for the side chat's re-review.

Binaries. gunbc cd8ea860cdcc3580d7f51051657b9370af8842715ecfd75001e79e6abc2e0492, claim_batch de383604c654a5ed660ade95f1267ee09c405f55215a0d43875dad582452b1b3, both built at the pin on BuildBuddy in a self-bound cgroup. Base arm at main 6296275.

CI at this head: floor ✅, witnesses ✅, generated ✅, emit-build ✅. GitHub merge state: CLEAN.

Roster. Recomputed at head: the importers of bmc_secure, the route module and its evidence module, bmc_model, the census and the arrival convergence, plus their transitive witnesses.

witness	head	base (main)
route witness	26/0	13/0
route forged probe	3/0	3/0
bmc_secure_state witness	18/0	15/0
bmc_secure_state forged probe	6/0	5/0
bmc_secure witness	45/0	45/0
mtcollins1_bmc_secure_standing	4/0	4/0
arrival_converge	20/0	20/0
arrival_converge forged probe	7/0	7/0
mtcollins_firmware_converge	69/0	69/0
managed_host / its forged probe	5/0, 3/0	5/0, 3/0
managed_host_boot_federation	6/0	6/0
authorization_pattern_selection	25/0	25/0
gcp_iam_converge	25/0	25/0
bmc_factory_credential, observability_channel_routing, bmc_model_web_kvm, boot_world_models, bmc_onboarding_quarantine, mtjade1_recorded_manager_capture	identical to base
approval_broker_helper_grant	18/1	18/1 (pre-existing)
kvm_observer_protocol_wet	7/7	7/7 (pre-existing)
Hermetic bmc_secure_state	18/0	15/0
Hermetic arrival_converge	20/0	20/0
Hermetic operation_realization	18/0	18/0
Hermetic mtcollins1_boot_acceptance_matrix	29/0	29/0

fleet-converge.yml. The PR's diff from its merge base touches no fleet or workflow file. The head digest 6049be13f3b0572c (371783 bytes) equals the earlier main base c84dd1. Newer main 6296275 digests differently because main itself changed fleet modules after this branch's merge base.

Same-path REDs (taken at 74b10e4; the code is identical to this head, which changed only an evidence comment and a frontier row). Each mutation fails only its target claim; restored clean.

mutation	FAILs
B1: the readback's attempt is not compared with the approval's	the_channel_close_readback_is_bound_to_the_observed_run_and_account
B2: the dry read takes Get User Access rows from the supplied census	a_planned_channel_close_is_applied_read_back_and_converges
B3: the dry apply drops the channel transition	a_planned_channel_close_is_applied_read_back_and_converges
B4: the plan accepts a managed user other than the authenticated one	the_channel_close_readback_is_bound_to_the_observed_run_and_account

One finding outside this PR's scope, from dumping the forged probe's diagnostics: passing a ControllerClockReading record to dry_read_bmc_account_state(read_at_millis: EpochMs) produced no blocking type refusal. The read-floor wall now holds by the observation mint's admission (only the dry read may mint), and the probe claim asserts exactly that. The argument-type gap itself is a compiler concern for a separate row.

— sent from bright-wolf-485

[briansrls]

APPROVE at exact requested head 5cec3b209f84debfab08682b31bfcdf4f94cd2f8, against DESIGN.md §3's single-authority and executing-pairing rules, §4b's evidence boundaries, and §5. The three integration blockers in review 5409890536 at 8960bbe are closed. This covers the O1b/arrival integration and the corrected qualification frontier, not a live-controller qualification or the held production cutover.

1. The readback constructor proxy is closed

project_managed_administrator_readback now takes only the observation and admits only admitted_channel_writes. It neither accepts a separately chosen user/attempt nor exports a readback through an admitted witness helper. Its downstream mint admits that projection only. admitted_channel_writes consumes the readback internally; its returned write descriptions do not export it, and the sealed action plan still computes its own admissions.

The observation mint, observed_bmc_account_state, now admits only dry_read_bmc_account_state. The new compiler discriminator calls both the readback projection and observation mint from an outside module and requires ConstructorCallAdmissionRefused keyed to each actual callee. The clean, class-scoped harness control is retained. These controls exercise the former facade, not merely the underlying sealed literal.

This establishes the modeled/dry construction boundary. It does not turn a supplied dry world into a live observation. The live observation and privilege-write frontiers remain explicit and undischargeable by these fixtures.

2. The real plan preserves observed identity and checks ordering

BmcAccountStateObservation now retains attempt and managed_user. The dry producer records the same numeric user it passes to the actual managed-credential probe. The projection copies those observed fields, filters the census for that observed user, and retains endpoint/build; it no longer assigns the approval's attempt to the reading.

administrator_retention_refusal independently compares the observed attempt with the approval's attempt and requires the exact controller/build, a different retained administrator for a lowering request, and exactly one managed-user row on the target channel at Administrator. The plan also refuses a supplied managed user different from the observation's authenticated user. Its existing subject/goal assessment remains ahead of plan construction.

Planning now checks both the census and managed-probe times against planned_at, in addition to the existing read-floor ordering. The real-plan discriminator covers A's reading with B's approval, A/A, another user's Administrator row, a mismatched plan user, and a read later than the plan. Precision: the dry producer stamps its readings and floor at one instant, so the late-read cell reaches the existing read-floor refusal; it is not an independent mutation test of each separate timestamp comparison. That is sufficient for the current producer, and is not being claimed as live observer-clock evidence.

The observation is retained by the plan, so this ephemeral projection does not replace the evidence-bearing observation with a free-standing assertion. The eventual live producer still owes the full account, subject, response-evidence and pre-write-ordering frontier.

3. The nonempty channel plan is applied and independently read back

dry_read_bmc_account_state now uses world.ipmi_user_access for the access rows. The supplied census contributes channel topology only. dry_apply_bmc_account_plan executes each planned privilege-limit write through bmc_ipmi_set_user_access, threads the resulting world, and retains channel completion in the application. Phase admission checks that completion alongside the password writes and then evaluates the independent post-read.

a_planned_channel_close_is_applied_read_back_and_converges drives the actual plan, application, post-read and phase. It seeds the initial world once, then reads step.world with the SAME original layout, not a test-authored closed census. It requires one planned channel write, a converged applied phase, published user 2 at NoAccess on channel 2, and managed user 3 still at Administrator. Thus reverting the world read to supplied rows, or dropping the actual channel transition while claiming completion, defeats the control. The no-route, ungrounded-route, absent-approval and missing-administrator controls remain.

The reported B1–B4 mutants discriminate these production boundaries. Their measured commit 74b10e4 differs from this head only in the evidence module's comment/frontier correction; the affected producer, plan, readback and witness code is unchanged. I did not execute those mutants myself.

Qualification scope and integration preservation

The request remains specifically IpmiSetUserPrivilegeLimit, with exact user/channel/privilege approval identity, operation-kind separation, controller/build binding, and pre-write administrator retention. Modeled qualification responses still cannot mint a live grounded standing.

The corrected mtcollins1 candidate reasserts the managed account's already-established Administrator value. It can establish only AcceptedEffectUnobserved, which admit_rotation_apply rejects for privilege-lowering writes. mtcollins1_channel_close_effect_qualification_frontier now accurately requires a separate non-destructive, discriminating qualification with an established differing pre-read and matching post-read. Neither the candidate nor a dry run establishes that capability.

The O1b password caller supplies its exact request and no channel readback; the arrival witness adapts the request/effect arms while retaining its assertion that a Manager GET alone cannot ground account writes. No workflow or live actuation path is added by this residual diff.

Evidence and landing

Verified exact-head workflow 37283937675: floor, generated, emit-build and aggregate witnesses all succeeded. The head remained unchanged and mergeable before submission. The expanded consumer roster, Hermetic state 18/0, arrival 20/0, operation realization 18/0, matrix 29/0, and B1–B4 mutation outcomes are author-reported receipts, not tests I ran. The reported pre-existing approval-broker and KVM failures remain baseline failures, not passes.

The separately reported ControllerClockReading-to-EpochMs argument-type gap is not repaired by this PR. The observed probe refusal here is constructor-call confinement, not evidence that that compiler type check works. No live safety claim is derived from the modeled clock route.

No remaining source blocker on this head. Land through the required landing-head checks; this approval neither authorizes a BMC write nor discharges the live qualification/read or production-cutover frontiers. No additional hardware run is required for these integration corrections.