bmc_secure: seal the dry realization's mints (dry_bmc_account_instant constructor proxy)

[gunbai-bot]

Follow-up to #13242 (requested by warm-crane-577; the proxy was found by deep-lynx-731 on O1c-2).

The defect

gunbc.machine_intake_bmc_secure dry_bmc_account_instant(millis: EpochMs) turned any number into a sealed ObserverClockInstant for any caller. It was a constructor proxy for the observer clock. The seed does not refuse a record at an EpochMs formal (gunbc#13385), so an admission list is the only wall.

The seal

function	now admits only
dry_bmc_account_instant	dry_read_bmc_account_state, dry_apply_bmc_account_plan
dry_read_bmc_account_state	witness read_in
dry_apply_bmc_account_plan	witness applied_with, the_post_read_is_independent_of_the_reading_that_diverged, a_planned_channel_close_is_applied_read_back_and_converges
observed_reading	dry_probe
observed_published_account	dry_read_bmc_account_state

Sealing only the instant would have moved the proxy up a level, since the dry read and the dry apply take scalar milliseconds. That is why the whole chain is admit-restricted.

The forged probe gains the_dry_realization_mints_refuse_an_outside_caller. It pins ConstructorCallAdmissionRefused at all five functions for outside calls.

Sweep of bmc_secure: other functions that mint a sealed carrier from supplied scalars, NOT changed here

• observed_bmc_credential_rotation. It is the event-path mint, called by gunbc.machine_intake_mtcollins1_bmc_secure_observation and three witnesses. That path is the X scheduled for deletion by bmc_secure_state_cutover_frontier, so it is left frozen rather than invested in.
• The O1b witness helpers. read_in, and read, read_with and secured_read above it, return sealed observations built from supplied values. That is the same facade pattern the side chat refused for the readback. Confining them means restructuring the O1b witness so each claim consumes its own reading, which is a separate change.
• Outside bmc_secure. gunbc.clock_read observer_clock_modeled admits the witness helper observer_at, which returns a sealed instant for any number.

Receipt at exact head 99ade6b

gunbc 0de13c61c2592f7d24d56b2a8fb20fd50086f89efa382d5d085284e371324c9b, claim_batch b919f42610f9fd894cccdc1edf770082e4cfce8d929285e58d4ad0e2640aeb67, built at the pin on BuildBuddy in a self-bound cgroup.

witness	result
bmc_secure_state forged probe	7/0
bmc_secure_state	18/0
Hermetic bmc_secure_state	18/0
arrival_converge	20/0
Hermetic arrival_converge	20/0
arrival_converge forged probe	7/0
bmc_secure	45/0
mtcollins1_bmc_secure_standing	4/0
mtcollins_firmware_converge	69/0
managed_host / its forged probe	5/0, 5/0
managed_host_boot_federation	6/0
route witness	26/0

Same-path RED S1: removing dry_bmc_account_instant's admit list FAILs the_dry_realization_mints_refuse_an_outside_caller only (6 PASS). Restored clean.

No fleet or workflow file changes. No hardware, no live call.

🤖 Generated with Claude Code

[briansrls]

REQUEST_CHANGES at exact requested head 99ade6b1d5c3898bd67eec84947c09d43b07b499, against DESIGN.md §§3, 4b, 5 and 6b. One remaining transitive-constructor-confinement blocker, with two reachable helper paths. The direct-call seals and their callee-specific probe are accepted, but they do not yet close the dry mint chain.

[P1] The admitted helpers still expose the carriers the new seals protect

dry_read_bmc_account_state now admits only test.claim.machine_intake_bmc_secure_state_witness::read_in, but read_in itself has no admit list. It accepts caller-supplied at: EpochMs, passes it unchanged as read_at_millis, and returns the sealed BmcAccountStateObservation. The caller can project read_floor from that observation. The resulting path is:

outside caller choosing m
  -> witness.read_in(..., at: m)
  -> dry_read_bmc_account_state(..., read_at_millis: m)
  -> dry_bmc_account_instant(millis: m)
  -> returned_observation.read_floor

Every newly restricted edge on that path is an admitted edge. The caller obtains an ObserverClockInstant for its chosen number without calling any of the five forbidden functions directly. The unrestricted read / read_with wrappers expose the same path. The fixed lab endpoint does not close it: the extracted clock carrier has no endpoint restriction. This counterexample uses a valid EpochMs; it does not depend on #13385's record-at-scalar defect and would survive that checker repair.

That makes the acknowledged read_in residue part of this very repair, not an independent neighboring defect. I accept that the direct door is improved and am not claiming this PR introduced the pre-existing wrapper. But the claimed whole-chain confinement is still false, and leaving this wrapper for after the seal lands leaves the original supplied-number-to-sealed-instant capability available under a different entry.

A second branch of the same class remains inside the production module: observed_reading admits only dry_probe, while dry_probe is unrestricted. An outside caller supplying a BmcWorld and an existing ObserverClockInstant can call it and receive an ObservedCredentialAccepted or ObservedCredentialRejected containing the newly protected ObservedReading. dry_published_lan_probes is another unrestricted carrier-returning route through dry_probe. Restricting only the final literal mint does not confine these intermediary producers.

Bounded correction and discriminator

Close the admitted helper chain through the actual carrier-returning wrappers. The existing admit-list mechanism is sufficient: confine read_in and every wrapper that can return its observation to their legitimate internal callers, terminating at claims or diagnostics that do not return a protected carrier. Likewise confine dry_probe and its carrier-returning published-probe wrapper to the dry read's construction path. Alternatively, have each admitted claim construct and consume its own observation internally. No new identity type or broad witness-framework rewrite is required.

Extend the compiler probe to call the exposed wrappers, not only the five underlying mints. In particular, an outside call through read_in that returns .read_floor must refuse at the relevant callee; a direct outside dry_probe call must not export the protected reading. Keep a clean admitted read/apply path, and show that removing the wrapper restriction makes its targeted control fail. A separate follow-up can author this work, but its effective confinement needs to be present in the landing tree reviewed for this repair.

applied_with is not the same problem: I inspected it, and it returns String after consuming the plan, application and post-read internally. Its name appearing in an admit list is not itself a blocker. The two directly admitted apply claims likewise remain appropriate non-carrier endpoints.

Accepted scope and evidence

The five new direct-call checks require blocking ConstructorCallAdmissionRefused at the named callee; CensusNotRunnable cannot satisfy them. S1 therefore tests the direct instant seal, but it does not exercise the wrapper path above. The existing literal, readback-projection and clock controls are preserved. The diff changes admission metadata and probe source, not the dry account-write ordering, version checks, world readback or phase verdicts.

The frozen observed_bmc_credential_rotation event path and #13419's separately authored observer_at repair are not additional work requested here. This finding is about paths through the mints this PR changes. No live read, credential write, held O1b cutover, workflow change or CI-lane restoration is required.

Verified exact-head workflow 37347183224: floor, generated, emit-build and aggregate witnesses all completed successfully. The BuildBuddy witness batches and S1 remain author-run evidence; I inspected source and controls but did not execute claims or compiler mutants. The bypasses above are source-derived, not claimed local test results. The requested head was unchanged and mergeable immediately before submission.

[briansrls]

APPROVE at exact requested head 892d783493ad9718ce48eddcdfa63f43d37cfe02, against DESIGN.md §§3, 4b, 5 and 6b. This closes the transitive-constructor-confinement finding in review 5419800425. No remaining semantic blocker in this re-review; required CI is not yet green.

Both previously exposed helper paths are confined

The witness read chain is now restricted at every carrier-returning wrapper: read, read_with, read_in and secured_read. Following their admit lists reaches the named Bool claims or the already accepted text-producing consumers applied_with and decision_on, not an unrestricted helper returning the observation. The old outside call read_in(..., at: m) cannot obtain the observation from which to project read_floor: it now refuses at read_in itself. The indirect read/read_with and secured-reading entries no longer provide another route around that admission.

The production probe branch is closed too. dry_probe admits only dry_read_bmc_account_state and dry_published_lan_probes; the latter admits only the dry read. The dry read still admits only the now-confined read_in. Thus an outside caller cannot acquire ObservedReading by calling the admitted probe wrapper around observed_reading, either directly or through the published-probe list. The five underlying mint seals remain intact.

The relevant endpoints consume their protected values. applied_with still runs plan/write/post-read/phase and returns String; the directly admitted application claims return Bool. No new carrier-returning facade replaces the ones this revision confines. These restrictions address the valid-EpochMs bypass in the previous review independently of the separate record-at-scalar checker repair.

The new control tests the wrappers, not only their callees

the_read_helpers_refuse_an_outside_caller compiles actual outside calls to all six wrappers and requires blocking ConstructorCallAdmissionRefused separately at read, read_with, read_in, secured_read, dry_probe and dry_published_lan_probes. A refusal elsewhere or an unmeasurable census cannot satisfy the six conjuncts. The source attempts to return the protected observation/probe itself; refusal before that return also closes the subsequent projection route that motivated the finding.

The existing five-mint control, literal-forgery controls and class-scoped clean control remain. The admitted state witnesses retain the real dry read, plan, world mutation, independent post-read and phase judgment. The reported R1–R6 single-helper removals discriminate the new wrapper claim; those mutation results and the exact-head BuildBuddy batches remain author-run evidence, not tests I executed.

Scope and CI

The frozen rotation-event path and the separately authored observer_at repair remain outside this bounded finding, as stated in the previous review. This approval does not claim every observer-clock producer in the repository is confined, discharge the held O1b cutover, or authorize a live account write. The older PR-body paragraph saying the read-helper work is deferred is superseded by this exact commit and the re-review request.

Verified requested-SHA workflow 37367214509: floor, generated and emit-build succeeded; rust-unit-tests and the aggregate witnesses job failed. The Rust job log explicitly reports that the unit-test action timed out after 40 minutes. I have not independently established the timeout's repository-wide attribution or reviewed #13445 here. This approval is not a waiver: queue only after all required checks succeed on the landing head. A code-changing integration head needs its own reconfirmation.

I inspected the exact-head source, prior review, wrapper callers, compiler controls and CI/log evidence; I did not execute claims, mutants or hardware actions. The requested SHA remained unchanged and mergeable immediately before submission.