Skip to content

os_install_actuator_selection witness: pin the declared rosters by whole-list equality - #13573

Closed
gunbai-bot[bot] wants to merge 2 commits into
mainfrom
session/vivid-lynx-377-os-install-optional-eq
Closed

gunbai-bot[bot] wants to merge 2 commits into
mainfrom
session/vivid-lynx-377-os-install-optional-eq

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 8, 2026 •

Copy link
Copy Markdown
Contributor

One file, four lines: dag/test/claim/os_install_actuator_selection_witness_test.dag lines 7/8/29/30 compare List.first() (typed T?) against a required value, which the checker refuses (#13179):

'==' compares an optional value with a required one (the left operand is optional)

Why this PR exists. The file is byte-identical on origin/main and its defining module is untouched by anything in flight — it is a standing silent red on main of the witness_module_absent_from_the_executed_set class: main's floor never compiles the entry. It surfaced on PR #13412's floor (run 37715202561, head 6454153, floor job 113114528524 — 4 blocking diagnostics in this file) because that PR's extdeps.version changes sit in the witness's import closure (gunbc.os_install_actuator_selection <- extdeps.bmc.os_install_actuator_toolchain <- extdeps.tools <- extdeps.version), so changed-witness selection pulled the identity in. Any PR whose closure reaches extdeps.version hits the same four refusals until this lands.

Per-claim diagnosis of run 37728157032 (both claims returned Bool(false) under the first pushed spelling)

Verdict for BOTH claims: neither the product nor the asserted facts are wrong — the assertions' SPELLING was invalidated by a contract fork on List.first(), and the facts they assert are unchanged on current main. The first pushed spelling (first() == Present { value: X }) was wrong and is reverted here.

  • The facts hold on main (2ef4b29). dag/gunbc/os_install_actuator_selection.dag:47-52 declares the kind roster [BmcNetworkReach, ActuatorToolchainGrant, InstallMediaArtifactRealizable, InstallWindowAvailability] and :91 the tie-break order [operator_host_srv1, operator_host_srv2] — exactly what the two claims assert. HostIdentity moves to the leaf product.host_identity (stacked on #13175) #13209's host-identity move and Fleet host identities move to the leaf gunbc.fleet_host_identity (broker closure 196 → 192) #13175/main breakage: new optional-equality refusal rule left os_install_actuator_selection.dag:387 refusing #13547 changed where HostIdentity lives, not these values; the witness's references resolve to the same declared identities.
  • Why the claims returned false anyway. The checker types List.first() as T? (the Native broker 2C/C4: checker refuses T? == T (EqualityOptionalityMismatch) #13179 rule refusing T? == T), while the executing runtime returns the BARE element for first() — the fork recorded in the RFM row cross_type_comparison_answers_instead_of_refusing ("items.front().cloned().unwrap_or(Value::Null)"). Under that fork:
    • the original first() == <required> is refused at compile time (what main's floor would hit if it compiled this module — it never does; that is the silent red this PR closes), and
    • first() == Present { value: X } compiles but executes FALSE: the runtime's bare element and the constructed Present variant are different constructors, so equality answers false. That is exactly run 37728157032's two returned Bool(false) cause=claim_failed adjudications for os_install_actuator_requirements_dispatch_through_kind_rows and srv3_actuator_host_selected_because_requirements_and_policy.
  • main breakage: new optional-equality refusal rule left os_install_actuator_selection.dag:387 refusing #13547 already met this fork in the declaring module — correctly. It rewrote the module's own tie-break read to match order.first() { Present { value: host } => host == operator_host_srv1, Absent => false }. That helper is called only by this witness file, so I measured it directly: claim_batch --claim-run on a 4-probe claim module against this same tree (BuildBuddy invocation b5ff3a8c-1be3-4009-85c1-04f6ed5038c4, completed 2026-10-08T07:25:52Z): PASS probe_tiebreak_helper_boolean (the helper, head IS srv1), PASS probe_order_head_direct_match (the match spelling standalone), PASS probe_order_whole_list_equality (control), FAIL probe_order_first_equality_present (the equality spelling). So the runtime lifts the bare element when MATCHING against Present patterns but not for == against a constructed Optional — main breakage: new optional-equality refusal rule left os_install_actuator_selection.dag:387 refusing #13547's match form is sound; no module repair is needed. The precise defect shape (equality-false / match-true on the identical tree) is the specimen for the cross_type_comparison_answers_instead_of_refusing follow-up receipt.
  • The repair pushed here. Assert the facts by whole-list equality — the runtime-proven pattern (witness_static_site_route_authority_paths_locked pins its route roster the same way): the kind roster and the tie-break order pinned against their declared literals. No first()/skip() remains in the claims, so the spelling is checker-clean AND executes true iff the declared rosters match.

Split out of #13412 per coordinator direction so that PR stays the approved content + main merges + regen. Verification receipts: floor receipt run 37715202561 (4 blocking diagnostics), remote repro of CI's exact --required-ci command with the compile-refusal phase cleared (BuildBuddy dispatch completed 2026-10-08T04:25:29Z, local job jb1fb9a4e), and run 37728157032 for the falsified first spelling.

…st Present

The floor's compile phase refused this witness with four T? == T
diagnostics (checker #13179): List.first() is Optional<T>, and lines
7/8/29/30 compared it against a required value. The file is byte-
identical on main and its defining module is untouched; the refusal
surfaced here because this PR's extdeps.version changes sit in the
witness's import closure (os_install_actuator_toolchain imports
extdeps.tools, which imports extdeps.version), so changed-witness
selection pulled an entry main's floor never compiles -- a standing
silent red of the witness_module_absent_from_the_executed_set class.

Rewrite the four sites with the sanctioned spelling: compare the
optional against Present { value: .. } (Present is in scope via the
BoundToDeclaringModule binding, which imports std.optional). Claim
semantics unchanged: the first two requirement kinds and the first
two operator-host preferences are still asserted by identity, with
an empty list now yielding false instead of a checker refusal.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved at 2ad332d. The four rewrites preserve the intended list-position assertions: List.first()/skip(1).first() return Optional values, so comparing against Present { value: expected } is the exact typed statement; an empty or too-short list now yields false rather than a compiler refusal. Present/Absent are already live in this same witness entry, so this adds no new binding dependency. The diff is confined to these four comparisons and changes no requirement, host-selection, failover, or actuation policy. Queue only after the exact-head witnesses aggregate is green; floor is still running at review time.

…ole-list equality

Run 37728157032 adjudicated both claims Bool(false) under the first
pushed spelling (first() == Present { value: X }): the checker types
List.first() as T? (#13179) while the executing runtime returns the
bare element (the fork recorded in
cross_type_comparison_answers_instead_of_refusing), so a bare-vs-Present
equality answers false even though it type-checks. The asserted facts
are unchanged on main: the kind roster and the tie-break order literals
in gunbc.os_install_actuator_selection match the claims verbatim.

Rewrite the four sites as whole-list equality against the declared
roster literals — the runtime-proven pattern used by
witness_static_site_route_authority_paths_locked. No first()/skip()
remains in the claims, so the spelling is checker-clean and executes
true iff the declared rosters match. Empty or drifted rosters now yield
false instead of a checker refusal or a silent wrong answer.
@gunbai-bot gunbai-bot Bot changed the title os_install_actuator_selection witness: compare optional first() against Present os_install_actuator_selection witness: pin the declared rosters by whole-list equality Oct 8, 2026

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved at a39504a. Delta from the previously approved 2ad332d is exactly one commit and one file: the four first()/skip().first() == Present { ... } comparisons are replaced by two whole-list equality assertions. The expected kind roster is byte-for-byte the owning declaration's [BmcNetworkReach, ActuatorToolchainGrant, InstallMediaArtifactRealizable, InstallWindowAvailability], and the expected tie-break order is the owning declaration's [operator_host_srv1, operator_host_srv2]. This removes every List.first()/Optional representation crossing from these claims. It intentionally strengthens the first claim from pinning only the first two rows to pinning the complete dispatch roster; that is coherent because production folds the complete roster in declaration order. The tie-break list currently has exactly two declared members, so its whole-list assertion preserves the complete policy. The declaring helper continues to use the match-on-Present realization, not constructed-Optional equality. Exact-head run 37740599695 is green, including the nominal floor and aggregate witnesses. No blocker.

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 8, 2026
@gunbai-bot
gunbai-bot Bot removed this pull request from the merge queue due to a manual request Oct 9, 2026
@gunbai-bot

gunbai-bot Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor Author

Closing as superseded: main fixed the same witness independently in 13b9152 (match on the optional .first() instead of T? == T), which uses the runtime-sound match-on-Present form (#13581). This PR now conflicts and adds nothing. — sent from lively-ram-153

@gunbai-bot gunbai-bot Bot closed this Oct 9, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant