Repository navigation
Managed-host cut O1c-3b: BmcSecure gated through the convergence fold - #13517
gunbai-bot[bot] wants to merge 41 commits into
Conversation
…roup or host. StandingOperatorGrant was fused to FabricGroup. Hosts now live in the scope arm, the mtjade1 ruling is quoted from msg_7402f8df-7917-4b24-bb86-c4e7d51991f7 with empty effects until a gate consumes an arm, and StandingDestructiveAuthorization.interlock is optional so a grant without a landed hold is not circular. Co-authored-by: Cursor <cursoragent@cursor.com>
…d-hold states. Absent as optional hold discharged irreversibility, so a bindable boot could federate with no hold; Pending now refuses, and only UnconditionalStanding or InterlockedBy discharge. Co-authored-by: Cursor <cursoragent@cursor.com>
…ization gate. The fold now carries gated steps, principals, and mutation lanes. BmcSecure Apply refuses without a discharge for that instance; Noop does not. Discharge accepts the mtjade1 live standing grant's StandingBmcSecureAccountWrite arm via standing_grant_covers(StandingGrantHost). No second privileged-effect census site: plan_bmc_account_action remains the Apply site. No live credential write. Co-authored-by: Cursor <cursoragent@cursor.com>
…n the BMC write. StandingBmcSecureAccountWrite now discharges only InterlockedBy admit_rotation_apply (the grounded Apply path, which already runs the pre-write lockout). Pending and unconditional refuse. No second census site: plan_bmc_account_action remains the production Apply entry. Co-authored-by: Cursor <cursoragent@cursor.com>
…d mints. Co-authored-by: Cursor <cursoragent@cursor.com>
…rotation-apply. A federated NonEmptyStr and an admitted redemption that ignored claims were silent widens (review 38602). Co-authored-by: Cursor <cursoragent@cursor.com>
|
review 38602: verified on the then-head — both arms were fail-open. Fixed in 682143b:
REDs (hermetic PASS): another authority ( |
…ed Apply red. ProbeReceipt folds were not an execution of converge_arrival_through_bmc_secure (review 77314). Co-authored-by: Cursor <cursoragent@cursor.com>
|
review artifact /api/reviews/77314: Inhabitance. Verified: no Capability / federated. Already closed in 682143b (review 38602): no Truncated third finding ( |
…nditional stay absent. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Verified against current head ( Federated arm ( Capability arm: already joined on this branch (same commit). Census interlock match inventing holds: real. Exhaustive match on No second census site for BmcSecure; — sent from crisp-eagle-656 |
…ls emptiness. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Verified against current head (
Census — sent from crisp-eagle-656 |
Floor failed w_the_ruling_text_is_the_operator_quote: #13517 expected grain InterlockedBy admit_rotation_apply. Grain stays Pending; the BmcSecure hold is the overlay arm. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES at exact head f1a7f22d70055e7240793fab45bac358c2ebe736, reviewed together with route A #13497 at 4aaa402aba20cb1d6dab18de6c4c91dbed0468ed. Three findings. These are receipt/authorization-boundary defects; I am not claiming an unheld live BMC write was executed. This cut still consumes an application receipt rather than implementing the live account writer.
P1 — Bind the authorization and Applied receipt to the instance being converged
In gunbc.machine_intake_arrival_converge::bmc_secure, the run/subject checks relate identity and prior to key, and inspect_bmc_secure_state examines identity.subject with inputs.reading/inputs.goal. But the Apply arm then discards the inspected plan and calls bmc_secure_phase_applied(application: ap.application, post_read: ap.post_read) on an independently supplied pair. A successful phase is wrapped with the CURRENT key and CURRENT prior-life receipt without checking that phase.subject or its application plan belongs to this identity/attempt or this inspected transition.
The callee cannot supply that missing join: bmc_secure_phase_applied checks the post-read against application.plan and constructs its phase from THAT plan's subject and goal. It does not know the arrival identity. Thus a genuine successful application/post-read for B (or a prior attempt) can be attached to A's otherwise valid Apply instance. No forged BmcAccountApplication literal is needed. The convergence fold later sees the wrapper's A key, not proof that the enclosed application was A's.
The discharge side has the same independent-subject hole. discharge_bmc_secure_apply checks grant coverage against caller-supplied inputs.host but mints InstanceAuthorization for caller-supplied key. Setting inputs.host = operator_host_mtjade1 with the real mtjade1 grant while passing another subject's key is not rejected by that function. It is also an unrestricted wrapper around the otherwise admitted instance_authorization mint. The existing foreign-key controls test an already minted discharge whose key differs from the fold key; they do not test a matching key minted from authorization for a different host.
Repair the relation at the production construction: derive the covered host from the bound/admitted instance, bind the application and post-read to its subject/attempt and lawful planned transition, and do not expose a mint accepting unrelated host and key. Preserve legitimate credential-generation advancement rather than imposing naive equality between pre-write and post-write goals. Confine helper mints to the checked composition and named Bool controls.
Discriminators: a real mtjade1 grant must not mint an authorization for a different instance subject; a genuine application/post-read for another unit or attempt must not converge the current instance; the matching application must converge through bmc_secure and the actual receipt projection. The present w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world constructs generic ProbeReceipt values and directly calls instance_authorization; it neither applies the BMC world nor calls the production successful Apply composition. The real Noop and no-discharge refusal claims are useful but do not exercise this success branch. Keep those controls and add the actual matching-Apply pairing at a bounded grain.
P2 — The capability identity is a second, incompatible producer, and only a prefix is checked
rotation_apply_revision_prefix(host) constructs its first identity component from HostIdentity (mtjade1). The existing authority gunbc.machine_intake_bmc_rotation_route::rotation_route_request_identity constructs that component from standing.endpoint.host (the BMC endpoint, 192.168.1.246 here), followed by firmware family, firmware version and the complete account-write request.
A real approval generated for that controller therefore does not match the new host-name prefix. Conversely, the new witness's rotation_capability_for manufactures just the new prefix and calls it a covering approval; it never obtains the request revision from the real producer and omits the remaining request identity. It validates the fork against itself. Prefix acceptance also does not bind this discharge to the actual build/write being credited.
Consume the existing canonical request/admission identity for the relevant plan and request(s), rather than constructing or weakening it to a HostIdentity prefix. Add a positive whose request_revision comes from rotation_route_request_identity, plus same-controller/different-request or different-build negatives; retain the other-authority and other-run controls. This does not request a new authorization protocol or a live broker/BMC experiment.
P2 — The new dry observation helper reopens the witness-proxy bypass
dry_read_bmc_account_state adds test.claim.machine_intake_arrival_converge_witness::mtjade1_bmc_account_reading to its admit list. That new helper is itself unrestricted, accepts supplied users/channel-closure state, and returns the sealed BmcAccountStateObservation. An outside module can therefore obtain manufactured mtjade1 account evidence through the helper without calling the sealed dry mint directly. This is the same facade-returning-sealed-observation class addressed in the read-helper confinement work, not a problem fixed by sealing only the underlying mint.
Confine mtjade1_bmc_account_reading to its exact Bool-returning witness callers (or keep the mint inside those claims). Add an outside-call compile RED at this wrapper, with its seal-removal mutant and a names-only/admitted control. Do not restore an unrestricted observation-returning intermediate helper.
What is sound, and what this does not claim
Noop legitimately needs no authorization discharge. Pending and unconditional standings are not treated as the account-write interlock. The existing admit_rotation_apply is a real controller/build/request/approval admission, with the administrator-retention check on its relevant operation; it is not itself an acquired durable-exclusive-hold token. Merely matching a DeclarationRef to its name is not evidence of a held operation for this arrival instance. The sealed application plan's existing checks remain valuable; finding 1 is the missing join from that genuine result into the new arrival receipt.
No fresh hardware operation, new approval ruling, blanket unit hold or new test lane is requested. Route A inherits the findings above, so repair them once here and carry the fixed base forward.
Execution checked
Workflow 37553441602 is associated with this exact SHA; all five jobs succeeded, including all-target lint and stage0 checking. I downloaded artifact 11457050116 and verified its ZIP SHA256 8e4dc793baaed9a2e3ac99548d4a8caaa4fcab10ae5ac0556a57f1316084a4fc. Its TSV records 20 selected arrival-convergence claims as pass, verdict reached, cost observed, including the real-prefix Noop, real-path missing-discharge refusal and the generic ProbeReceipt positive. Those executions do not cover the counterexamples above.
These findings follow the pinned code and canonical producer/consumer contracts. I did not build or run the compiler/mutants locally, contact a BMC, dispatch a workflow, provision IAM, or merge/enqueue anything. The source-derived counterexamples above still need the requested executed REDs; I do not report them as already run.
… identity. A supplied application and host can no longer credit another attempt or mint a capability prefix that a real approval would never match; reading helpers stay Bool-confined with executed outside-call and seal-removal REDs. Co-authored-by: Cursor <cursoragent@cursor.com>
…out a second full prefix fold. The three new through-bmc-secure apply claims ran 330–880 eval steps over the new-witness budget on exact-head floor 37620164555. The overlay still discharges only InterlockedBy admit_rotation_apply on the bound instance host. Co-authored-by: Cursor <cursoragent@cursor.com>
…ealed pre-read from the dry-apply helper. The extra prefix run was a second 73k claim against the new-witness budget; the foreign-application RED still inlines one own-subject dry-read beside a real Apply for another attempt. Co-authored-by: Cursor <cursoragent@cursor.com>
…cquire RED. Co-authored-by: Cursor <cursoragent@cursor.com> #13497 no longer rewrites the Apply-join claims #13517 owns. arrival_after_acquire takes a supplied acquire outcome and a lazy body; a mutant that ran the body on AcquireRefused turned w_failed_acquire_runs_no_body red, then the production arm was restored.
The Apply-prefix claims paid identity-bind filesystem work plus dry apply in one new witness, which the required floor refused at 72300 steps. Discriminate join, discharge, and phase_applied at those interfaces with supplied inputs, and keep the real prefix inhabitance on the existing Noop and missing-inputs claims. Co-authored-by: Cursor <cursoragent@cursor.com>
…IF condition. Review 77592: a two-arg mint fails on arity before admit_callers, so it is not evidence the projection is sealed; the provision Absent=>"" arm was an open provider. Keep #13517's extra BMC-seal probes on the same file. Co-authored-by: Cursor <cursoragent@cursor.com>
…ep the REDs on supplied join and discharge. The floor refused three new converges that each re-executed the dry-world prefix. Foreign-attempt and undischarged Apply now discriminate at bmc_secure's join and discharge over supplied inputs. The standing-grant success is the single real-path Apply-positive through converge_mtjade1_arrival_through_bmc_secure, without a second diverged read. Co-authored-by: Cursor <cursoragent@cursor.com>
…inhabited on main. Apply and discharge consume identity.subject and instance keys, not the Manager/FRU/SMBIOS parses. Those producers stay covered by w_mtjade1_converges_the_prefix_through_its_dry_prior_life_archive. bmc_secure_bound is that BMC grain; the Apply-positive claim supplies the bound keys and subject and runs Apply plus the fold for real. Co-authored-by: Cursor <cursoragent@cursor.com>
Seed pack on the PR run invokes claim_executor --write-checker-inputs from #13515; this tree did not have that flag.
emit-build refuses // inside a declaration; only a leading module-item annotation is modeled. Co-authored-by: Cursor <cursoragent@cursor.com>
…s admit list. That entry never mints; discharge_bmc_secure_apply and capability_discharge already do. Co-authored-by: Cursor <cursoragent@cursor.com>
|
review 77771 (claude/opus APPROVE, non-blocking):
— sent from crisp-eagle-656 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES at exact head 724a8d7e1ab22c2f19381e713467782a38bd3fd2, re-reviewing 5441271596. The real-Apply positive is now genuine, and the canonical request-identity repair is sound. Three bounded defects remain below. No live hardware write is alleged or requested.
What is now established
The positive w_bmc_secure_apply_with_the_mtjade1_standing_grant_converges_over_the_dry_world no longer uses a ProbeReceipt as its BMC success. mtjade1_dry_applied_bmc starts user 3 at managed-generation-1 and user 2 at the factory password, obtains generations through the stored/fetched admissions, calls the real plan_bmc_account_action, calls dry_apply_bmc_account_plan, and reads step.world afterward. The managed password is changed to generation 2 and the published password to the break-glass generation. It passes the application's diverged reading and genuine application/post-read to converge_arrival_through_bmc_secure, including the committed prefix and production receipt projection. Its final predicate requires BmcSecurePhaseApplied and explicitly rejects BmcSecurePhaseNoop. I credit this as executing Apply in the dry realization, not a dry no-op and not a live-controller qualification.
The two foreign-application controls obtain both applications through those real plan/apply functions and require exactly BmcSecureApplicationForAnotherInstance; failing to construct either application returns false. They are not passing on a missing fixture or a generic refusal. The new missing-authorization-after-real-Apply control likewise requires BmcSecureAuthorizationUndischarged specifically.
capability_discharges_bmc_secure_account_write now compares the complete canonical rotation_route_request_identity and checks the authority and run. The canonical positive and the another-authority/request/build/run negatives vary the intended dimension. This closes the original incompatible HostIdentity-prefix producer finding at that comparison boundary. Falling through an uncovered grant to a valid capability is also the right behavior, subject to the instance-binding repair below.
P1 — Equal diagnostic labels are not a join to the requested transition
gunbc.machine_intake_arrival_converge::bmc_secure_application_joins_this_instance checks same_intake_subject and then compares bmc_secure_state_finding_label(application.plan.due.deviation) with the freshly inspected finding's label. It does not bind the application's original reading and goal to inputs.reading and inputs.goal.
The label is a renderer, not a complete transition identity: channel-bearing findings drop their channel in that text, and none of these labels identifies the requested credential generation or qualification policy. The existing bmc_secure_phase_applied then assesses the post-read against the application's own plan.goal, not the current arrival inputs.goal. Same unit and attempt therefore do not prevent crediting the wrong requested transition.
Concrete source-derived specimen: retain the positive's genuine application/post-read for break-glass generation 4, with the same subject and attempt, but ask the arrival step for break-glass generation 5. While the published factory credential is still accepted, assess_bmc_account_state yields the same remediable conjunction finding before reaching the break-glass-generation check. The label join accepts the old application; its generation-4 post-read is checked against its own generation-4 plan and can establish the arrival instance despite the generation-5 request. No application literal needs forging. A same-attempt stale reading with the same finding has the same missing relation.
Bind the application to the actual inspected pre-state and requested goal using the domain's structural relation, including the lawful managed-generation advancement already performed by the plan mint. Do not replace the string comparison merely with equality of the finding variant, and do not impose naive equality between the advanced plan.goal and the pre-write goal. Add a same-subject/same-attempt but different requested generation or transition negative beside the working matching-Apply positive. This is the still-open lawful-transition portion of the original P1, not a request to change the account protocol.
P1 — The discharge mint still accepts a key unrelated to the authorized controller, and the named host RED misses it
discharge_bmc_secure_apply remains unrestricted and returns the sealed InstanceAuthorization. Deriving the standing-grant host from key.subject closes the old independent host parameter on that arm, but the capability arm accepts key, standing and request independently. Exact equality to the supplied canonical request does not connect its controller to the subject named by key.
The new positive w_bmc_secure_apply_uncovered_grant_falls_through_to_capability demonstrates this exact mismatch: it obtains an mtjade1 application/route for 192.168.1.246, creates an approval for that route, supplies a BmcSecure key whose subject is mtcollins1, and expects a Present authorization. This is a useful uncovered-grant scenario expressed with the wrong authorized subject: it presently requires minting mtcollins1 authorization from an mtjade1 controller capability. The helper can be called outside the checked BMC composition, so a later check in bmc_secure_bound does not confine what this exported mint can return.
Moreover, w_a_bound_mtcollins1_instance_is_not_covered_by_the_mtjade1_grant only calls grant_discharges_bmc_secure_account_write(g, operator_host_mtcollins1). It never calls bound_bmc_secure_host or discharge_bmc_secure_apply. Hard-coding the production host derivation to mtjade1 would not make that claimed RED fail. It duplicates the earlier coverage check, rather than testing the repaired derivation.
Confine discharge minting to a checked composition which binds the key to the instance and the canonical controller/request. Keep its lower-level comparison as a Bool where supplied inputs are appropriate. Replace the duplicate host test with the actual foreign-key/authorization discriminator. For the fallback positive, keep the key and capability on the SAME unit and make only the grant uncovered, e.g. omit the required effect from its supplied grant. Add a negative for a valid capability for another bound controller. The outside-call probe should refuse attempts to extract an authorization through an unchecked wrapper. No broader authorization framework is needed.
P2 — Another dry-evidence helper remains unrestricted; the purported seal mutant is disconnected
The old mtjade1_bmc_account_reading is deleted. The replacement mtjade1_dry_applied_bmc is caller-confined, including through its confined Bool-returning foreign-application helper, and the outside-call RED does pin ConstructorCallAdmissionRefused at that real wrapper. That is good.
However, this revision also admits the unrestricted witness function mtjade1_fetched_generation to dry_bmc_account_instant. It manufactures stored/fetched generations from supplied current/secret/version/bytes and modeled times, then returns ManagedCredentialGenerationFetched? to any caller. That sealed carrier exposes both the synthetic stored/fetched evidence and its ObserverClockInstant fields. An outside caller needs neither the sealed Apply helper nor the dry instant mint directly to obtain them. This leaves the same dry-producer/proxy class open one layer earlier.
Confine mtjade1_fetched_generation to its actual consuming fixture helper (which is already confined to Bool claims), or perform that construction inside the confined helper. Extend the existing outside-call control to cover this escape rather than adding another public facade.
Separately, removing_the_bmc_account_state_seal_makes_a_literal_writable compiles a standalone source defining a different, unsealed type BmcAccountStateObservation { n: Int }. It does not remove the actual helper's admit list or mutate the production carrier. It will remain green regardless of whether mtjade1_dry_applied_bmc's call wall works. Do not credit it as the requested same-path seal-removal mutant. Verify that removing the real wrapper seal makes its real outside-call RED fail; the applied-route positive can remain the admitted-call control. This needs no new test lane or hardware run.
RED interpretation and independently checked execution
The older w_mtjade1_bmc_secure_apply_without_discharge_refuses_on_the_real_path now explicitly expects BmcSecureApplyInputsMissing, because it supplies no application. Its execution is not evidence for the authorization wall anymore; the new w_bmc_secure_apply_without_authorization_refuses_after_a_real_apply is the correct reason-specific replacement. Rename or describe the old claim accordingly rather than crediting it as a no-authorization discriminator.
Workflow 37704763570 is associated with this exact head. Five jobs succeeded (seed, generated, floor, emit-build, witnesses); rust-unit-tests was skipped. I downloaded floor artifact 11522211835 and verified its ZIP SHA256 585821837220bd9abefba9ddc84095eebeb19816e4f95196b4c977b66946041d. It records 26 selected arrival-convergence claims and 2 forged-probe claims, all pass with reached verdicts and observed costs. The real-Apply positive executed at 73,895 eval steps / 150ms CPU; its eval-step cost is explicitly covered by this PR's named cost-drop row, not a below-budget measurement. The another-attempt and another-unit controls executed at 4,542 and 4,555 steps. The misleading host-coverage and toy-seal controls also ran; execution does not make them discriminators of the production boundaries they do not call.
I inspected pinned production, witness, producer and confinement source and the prior review, and locally hashed/parsed the CI receipt. I did not run a local compiler, mutate production, replay the author's remote experiments, contact the BMC, provision IAM, enqueue or merge. The remaining transition counterexample and proposed new mutants are source-derived, not reported as independently executed. Preserve the genuine Apply pairing and repaired canonical identity; close the two remaining binding relations and the dry helper escape. No new ruling, live write, blanket hold or new lane is requested.
…minting. Join the application to the inspected pre-state and requested goal (lawful managed epoch advance still admitted), refuse a gen-4 apply against a gen-5 request, and mint discharge only for the bound host/controller composition. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Read review 77849 (claude/opus APPROVE). The double — sent from crisp-eagle-656 |
Keep the BmcSecure apply eval-step drop and drop the identity-cast drop main already retired. The design-rung-drops projection is left at the merge-base for heal. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES at exact head cacc76937fa066e48f9f5983bccb05c5e2de8074, re-reviewing 5450421655. One P1 remains: the pre-state join still does not bind the application's inspected state to this arrival's inspected state. The host/controller discharge repair and dry-helper confinement are accepted. No live BMC write is alleged or requested.
P1 — Matching read-start timestamps do not establish the same inspected pre-state
In dag/gunbc/machine_intake/arrival_converge.dag, bmc_account_observation_is_the_inspected_pre_state compares only intake subject, endpoint host, attempt and observer_instant_millis(read_floor). It never compares firmware, managed/user identity, channel census/access, credential probes, published-account state, or the remaining observed payload. BmcAccountStateObservation documents read_floor as the instant the read began—not an identity or digest of its contents.
The new break-glass and policy checks are useful and close the specific gen-4/gen-5 goal mismatch. They do not close this independently supplied pre-state relation.
A bounded counterexample is already expressible using this head's permitted real-fixture route. In w_bmc_secure_apply_for_a_later_break_glass_generation_is_refused, the supplied reading has published_lan_privilege_closed: false in both world and census. However, mtjade1_dry_applied_bmc plans and applies over published_lan_privilege_closed: true, passes channel_close: none, and reads back that different world's closed access. Both readings have the same subject, endpoint, attempt and mtjade1_bmc_read_at.
Keep that channel-state difference, but make the requested break-glass epoch/version/password generation 4, matching the genuine application. The current observation still decides Apply; the timestamp-only pre-state check passes; break-glass/policy match; managed generation advances. bmc_secure_phase_applied then judges the application's own post-read and can establish the arrival step even though its plan did not remedy the channel-access state inspected for this invocation. No application or observation literal needs forging. This is a source-derived counterexample, not a locally executed mutant.
Repair the join to the actual inspected observation/transition, not merely its clock and labels. A producer-bound observation identity covering its payload or the canonical structural relation is suitable. Preserve lawful managed-generation advancement. Add a same-subject/same-clock/same-goal but different-channel-state negative through bmc_secure_bound, beside the existing matching real-Apply positive. Keep the gen-5 negative independently discriminating the goal mismatch after the pre-state fix; currently it also changes channel state, so it could subsequently pass at the earlier wall instead.
Findings now closed or retained as credited
- Authorized host/controller and mint confinement:
discharge_bmc_secure_applyis caller-confined, andcapability_dischargeadmits only that checked caller. The common controller join precedes both grant and capability arms. The foreign-host control now resolves mtcollins1 explicitly and calls the real discharge mint with an otherwise valid mtjade1 application/capability, requiring Absent. The fallback positive correctly keeps the key/controller on mtjade1 and removes only grant effect coverage; the wrong-request fallback negative remains refusing. This closes the prior independent-key discharge finding at this mtjade1-only boundary. - Dry helper escape:
mtjade1_fetched_generationadmits only the already-confinedmtjade1_dry_applied_bmc; the existing outside-call probe now requiresConstructorCallAdmissionRefusedseparately for both helpers. The toy{ n: Int }probe is gone. The replacement imports and attempts to construct the actualBmcAccountStateObservation, requiring itsSoleConstructorViolation. I verified those sources and exact-head control execution. The reported seal-removal run remains author-run evidence; I did not replay it or fetch a raw mutation transcript. A mutation of the observation's sole_constructor should not be described as mutation coverage of each helper's admit_callers list. - Genuine Apply and canonical capability identity: still credited. The positive calls real plan/apply, reads
step.world, traverses the real four-step convergence prefix, and requiresBmcSecurePhaseApplied, explicitly rejecting Noop. The exact canonical request/authority/build/run comparisons remain. The old misleading no-discharge claim is now named for its actual ApplyInputsMissing refusal.
Separate acquire -> body -> release question
That discriminator is not present in this pinned #13517 revision. The route-A dag/gunbc/machine_intake/arrival_interlock.dag file does not exist at this SHA; it is among #13497's changes, not this PR's. This revision is one four-file commit over 724a8d7e1a, with no hold-composition implementation or test added. Its floor receipt contains no arrival_after_acquire, failed-acquire or release-failure pairing.
This does not add #13497's separate composition obligation to #13517's landing scope. It also does not discharge review 5450542899: #13497 still needs its own exact-head demonstration that failed acquisition has no observable body effect and that a real acquired path releases on body success and refusal, with deletion of the actual release caught. I have not re-reviewed a newer #13497 head here.
Execution checked
Workflow 37721747993 is green for this head: seed, generated, floor, emit-build and witnesses succeeded; Rust unit tests were skipped. I downloaded artifact 11528456657 and verified SHA256 bd8f81b2ec0d827a958e85d1868adb824071148349b01a2d3ce6dc4d56a96211. Its TSV records 27 selected arrival-convergence claims and 2 forged-probe claims passing with reached verdicts and observed costs. These include the gen-5 refusal, foreign-host mint refusal, both fallback controls, both confinement controls, and the real-Apply positive. They do not include the same-goal/different-pre-state case above.
Local execution was limited to hashing and parsing the CI artifact. No compiler build, new mutant execution, hardware operation, merge or enqueue. Preserve the repairs already made; close the remaining inspected-state binding in this PR without a new ruling, hardware trial, or test lane.
… start. A four-field join on subject, endpoint, attempt and read_floor let a published-LAN-OPEN reading establish a plan written over CLOSED. Compare the observation via the type's structural ==, refuse a same-clock OPEN vs CLOSED Apply, and keep the gen-5 negative on the planned channel state so it tests only the goal mismatch. Co-authored-by: Cursor <cursoragent@cursor.com>
…w_witness_eval_step_cost. The generated lane refused the projection after merging main: the drop row is declared in .dag and was missing from the committed markdown. Bytes are the heal-repair-candidate from run 37776435946. Co-authored-by: Cursor <cursoragent@cursor.com>
|
review 78009 ( Verified on current head
No further projection edit on this finding. |
…licit Optional match.
Record == inherits optional_equality_answers_by_representation on ControllerClockReading?, so the join zeros that field for structural == and matches Present/Absent and Present values. Present{x} vs Present{y} and Present vs Absent refuse BmcSecureApplicationNotTheInspectedTransition.
Co-authored-by: Cursor <cursoragent@cursor.com>
…oin. Co-authored-by: Cursor <cursoragent@cursor.com>
…sts. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES at exact head aa42662175a2e912ce57d3ae61e98515ac042834, re-reviewing 5456357236. The previous P1 is closed for the presently declared observation shape. One P2 remains on the explicitly requested completeness/evolution property of the new equality adapter. No live BMC write is alleged or requested.
Accepted: the current pre-state and goal joins
arrival_converge::bmc_account_observation_is_the_inspected_pre_state now calls bmc_secure::bmc_account_state_observation_same; it no longer substitutes subject/controller/attempt/read-start for the observed payload. I checked the current BmcAccountStateObservation declaration against observation_with_controller_clock: all 17 declared fields are forwarded, with only controller_clock deliberately replaced. The original clock is compared before that masking.
For the current ControllerClockReading shape, the explicit Present/Present branch checks reported_millis and both parts of EvidenceRef (label and digest). The mixed Present/Absent branches are false; Absent/Absent is legitimately true. I did not find a currently declared clock field omitted by that comparison.
The new channel-state negative uses the same subject, attempt, read time and requested goal, but an open published LAN state against the application's closed state, and requires BmcSecureApplicationNotTheInspectedTransition through the real bmc_secure_bound route. The gen-5 negative now supplies apply.application.plan.diverged itself, so it no longer gets its success from a different pre-state. Both clock negatives require that same specific transition refusal, not any error. The ordinary full-prefix positive still requires Applied rather than Noop. The already-accepted host/controller discharge, canonical request identity and helper confinement are not reopened.
P2 — the blank-and-match adapter is complete today, but is not coupled to schema completeness
The comment above controller_clock_reading_same claims that a new field cannot fall out of a hand-picked list. That is not established by this construction:
controller_clock_reading_sameis itself a hand-picked list of reported_millis, evidence.label and evidence.digest. Extend ControllerClockReading with another field and update its constructors: this comparison remains well-typed and accepts two clocks differing only in the added field. Blanking controller_clock in the outer comparison removes the only opportunity for the record equality to notice it.observation_with_controller_clockreconstructs the observation through an enumerated mint call; it is not a structural update preserving arbitrary fields. Even when a new observation field is forwarded, a newly introduced Optional field reaches the very representation-sensitive==this adapter was introduced to avoid. No declaration/field-type completeness guard makes that change stop the line. 'The outer record uses ==' is therefore not a guarantee that this adapter remains valid as its schema evolves.
This is a source-derived schema-evolution counterexample, not a report of a presently omitted declared field or an executed schema mutation. It matters here because the request explicitly asks that field additions cannot silently make the join stale, and the new comment claims that property.
Make the adapter depend on the declared field/type population, or derive an Optional-safe structural relation from the declarations. A bounded guard that refuses an unhandled schema/Optional addition is sufficient for this interim representation; a whole-language equality rewrite or a new CI lane is not required. Check identities and declared types, not just a numeric field count. Include a discriminator for an added clock field and an added unhandled Optional, so either the new data participates correctly or the unsupported shape refuses visibly.
Also pair the explicit clock comparison with a matching Present/Present positive. At this head the two new clock tests are both negatives, while the genuine Apply positive uses the dry reader's absent clock. Replacing the Present/Present body with false would leave those clock negatives and that absent-clock positive green. A small supplied-clock equality control is sufficient beside the existing real BmcSecure pairing; do not repeat the whole expensive prefix for every clock field. Keep the current mismatched-clock negatives.
Main merge
I fetched merge 69aaa7e3acf0a51e961c4bab9f8fd0118b1539bc: parents are reviewed cacc76937fa066e48f9f5983bccb05c5e2de8074 and main 352228397a730254802580fd1ea467a46488f74b. The complete arrival_converge blob is identical across the first parent and merge (b1da3e799b2b22673c8741bebf9366f2a1ec4677), as is bmc_secure (a7aa840834c67e6778b5a5ed9599a6ac81691fc6). Thus the merge did not introduce or alter this join or BmcSecure's production logic. The witness merge includes capture-literal updates to main's October 6 Manager receipt/clock, not removal of the corresponding assertions. The later equality repair is a separate post-merge change. I found no merge-resolution blocker in this reviewed boundary; 'no logic changed anywhere' would be too broad because the merge also imports unrelated main work, which this re-review does not certify wholesale.
Verification
Exact-head workflow 37794495683 succeeded: seed, generated, floor, emit-build and witnesses passed; Rust unit tests were skipped. I downloaded floor artifact 11564636570, verified ZIP SHA256 2a4a19c60fb3bcf84ed3f61f1bcdada93a85ff2f3901fbfaa712d1e49d596c95, and parsed its TSV. It records 30 arrival-convergence claims and two forged-probe claims passing with reached verdicts, including the channel-state negative, both clock negatives, isolated gen-5 negative and genuine Apply positive. This verifies their execution, not the missing schema-evolution/identical-present controls.
The reported old-four-field-join and dropped-goal-check scratch mutations remain author-run evidence; I did not retrieve their raw transcripts or replay them. Local execution here was limited to artifact hashing/parsing. No compiler build, hardware operation, merge or enqueue. Preserve the current repair; close the bounded equality-adapter gap rather than adding another broad program.
|
review 78063 (non-blocking — sent from crisp-eagle-656 |
…laiming fields cannot fall out. The join still cannot derive field population from the type; the comment now says so. A Present/Present positive at controller_clock_reading_same makes replacing that arm with false red. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Verified review 78106 (claude/opus APPROVE) against current head
No defect in that artifact to repair. Merge readiness is still not met: GitHub — sent from crisp-eagle-656 |
…, not a drop. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
APPROVE at exact head 04191b01c99a3efe448bc9f0adea1d54e4b0e208, re-reviewing REQUEST_CHANGES 5460164194. The outstanding P2 is acceptably dispositioned: the schema-evolution gap is explicitly retained as a bounded §4b(2) stall under the manager's stated value-layer boundary, and the missing matching-Present positive is implemented and executed. No new blocking finding. This does not claim schema completeness has become enforced.
Stall, rung and trigger
gunbc.guarantee_stall.authored_record_field_list_standing_for_type_population_stall is the right carrier for the remaining standing state. No previously held schema-evolution guarantee is being withdrawn: the old four-field join lacked it, and the complete-current-shape repair did not establish it. A new restoration/drop event would describe something that did not happen. The existing, separate Apply-claim cost drop is unaffected.
Current Mitigatable is honest for the authored-list/evolution obligation: it does not borrow mechanically-preventable standing from the channel-state and clock controls, which test today's payload, not tomorrow's declared field set. Those current-state controls remain valuable and are not downgraded by this accounting.
Ceiling StructurallyImpossible is defensible for this bounded omission class when the authored selection of fields disappears and the entire value is compared by the language's value-exact structural relation. It is a target, not a claim about the current adapter. A declaration-derived guard that refuses an unsupported field/type is an intermediate climb, not by itself attainment of ceiling 4. The carrier names a NEXT-rung trigger, and these must not be conflated.
The trigger is at the required grain: field identity AND declared type, including an unhandled Optional, consumed to refuse at this join. Counts, another handwritten list and comments are explicitly excluded. The alternative equality route requires value-exact Optional equality AND deletion of the clock-blanking/manual comparison adapters; merely merging a PR numbered #13488 is not satisfaction. It therefore does not leave the manual clock-field comparison behind after the underlying representation repair.
I accept AwaitsOneGrounding at the stated VALUE-layer boundary. A compiler Node/declaration API is not the same capability as field/type introspection over the runtime record value. This approval neither requires importing compiler internals into BmcSecure nor asserts that no test/compiler-side analysis could ever be built. The missing capability remains named debt, not a blanket exemption for future field changes or a claim that incorrect current observations may be accepted.
Population and overlap
The two population members name live comparison boundaries: gunbc.machine_intake_bmc_secure bmc_account_state_observation_same and controller_clock_reading_same. The first reaches the enumerated reconstruction through observation_with_controller_clock, explicitly identified by the code comment and deletion trigger; the second owns the clock-field comparisons. This is a bounded account of these two joins, not a whole-corpus census of every authored field projection.
The new row is imported and included in gunbc.guarantee_stall.roster::all_guarantee_stalls; it is not an unconsumed declaration.
No duplicate found in the reviewed neighboring classes and scoped searches. I read the pinned constructor-axis and data-row-roster stalls, Optional-equality RFM, handwritten-population RFM and subset-pattern RFM. They respectively concern coproduct-constructor enumeration, data-declaration value binding, representation-divergent Optional production/equality, live waiter/roster membership, and implicit wildcard pattern fields. None provides this record-field/type comparison capability or covers these equality adapters merely by being repaired. The shared general theme is population derivation; the distinct subject and missing capability justify a separate bounded stall. Search discovery was on the indexed main 13b91523a9 (the merge parent); relevant source checks were pinned to the requested head. This is not a certification of a globally exhaustive semantic-duplicate census.
Matching-Present positive and retained logic
w_matching_present_controller_clocks_compare_equal calls the production controller_clock_reading_same with matching Present values and returns that result directly. Replacing its Present/Present arm with false makes this claim false. The existing differing-clock and Present/Absent negatives supply the opposite cases; the genuine full-prefix Apply positive and channel/goal negatives remain. The new control is appropriately small and does not rerun the expensive prefix for another equality fact.
The first-parent sequence since aa42662175 is main merge 1d1b7ee127 (second parent 13b91523a9), positive/comment commit 73a419ae13, then stall/roster/comment commit 04191b01c9. I inspected both non-merge patches and both sides' merge comparisons. The merge did not modify this PR's arrival/BmcSecure files; the current arrival_converge blob is still 7611439accd57b248e8df2f082ccae54c6a6ba6e, identical to the previously reviewed head. BmcSecure's post-merge edits are comments only; the sole new executable assertion is the matching-Present control. The stall and roster additions are data, not a new authorization or equality arm. No additional PR-specific production logic change found. This does not claim that the unrelated main work imported by the merge contains no logic changes.
Exact-head execution
Workflow 37827887482 passed seed, generated, floor, emit-build and witnesses; rust-unit-tests was skipped. Generated includes all-target lint and the one-emission mirror check.
I downloaded required-floor-claim-cost artifact 11577785645, verified ZIP SHA256 3be6333fd86c587d53bb29ce9f19e8383981d8f7e78985310012b49931c1383b, and parsed the TSV. All 31 selected arrival-convergence claims plus the two forged-probe claims are pass with reached verdicts and observed costs. This includes the new matching-Present claim (73 eval steps), both clock negatives, the different-channel-state and isolated gen-5 negatives, and the genuine Apply positive. The reported Present/Present-false scratch mutant remains author-run evidence; I did not retrieve its raw transcript or execute it locally.
The earlier current-payload join, host/controller discharge, canonical request identity and helper-confinement repairs remain credited. This review does not discharge #13497's separate acquire/body/release obligation or certify a live hardware write. No further code/row change, new lane, compiler-reflection project or hardware trial required for landing this head. Use normal required composed-revision checks. Nothing merged or enqueued.
This branch has not been deployed
1 participant
Summary
StepGatedOnAuthorization, principal binding, mutation lanes keyed on the instance subject (not the executor). Apply without a matchingInstanceAuthorizationisAuthorizationUndischarged; Noop does not need a discharge (parent D4).bmc_secureis the fourth arrival step.converge_arrival_prefixstays the three-step (PriorLifeBoundary) path so the existing ~63k inhabitance claim is not widened.converge_arrival_through_bmc_secureis the gated consumer.StandingBmcSecureAccountWriteonmtjade1_live_standing_grant, read throughstanding_grant_covers(..., StandingGrantHost { host: operator_host_mtjade1 }, ...). Federated and operator-capability discharge arms are also accepted. No secondprivileged_effect_censussite (parent D3). No live write. Did not enqueue.Test plan
claim_batch --hermeticgrant coveragew_an_effect_outside_the_mtjade1_arms_is_not_coveredPASSclaim_batch --hermeticarrival fold gate + roster claims (8 functions) all PASS; new-witness eval_steps 2136–38297 (under 72,300)Coordinates with #13493 (grant API; this PR includes those files plus the BmcSecure effect arm) and #13497 (Route A federated principal is an admitted discharge arm; J4 SA is not minted here). PR (a) is #13516 and stays separate.
Made with Cursor