From 2ad332de0971e34852c87a365b3276a4f9d0627d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 8 Oct 2026 04:31:16 +0000 Subject: [PATCH 1/2] os_install_actuator_selection witness: compare optional first() against Present The floor's compile phase refused this witness with four T? == T diagnostics (checker #13179): List.first() is Optional, 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. --- .../claim/os_install_actuator_selection_witness_test.dag | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/dag/test/claim/os_install_actuator_selection_witness_test.dag b/dag/test/claim/os_install_actuator_selection_witness_test.dag index 9f0a35508c4..6242938af19 100644 --- a/dag/test/claim/os_install_actuator_selection_witness_test.dag +++ b/dag/test/claim/os_install_actuator_selection_witness_test.dag @@ -4,8 +4,8 @@ module test.claim.os_install_actuator_selection data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly test fn os_install_actuator_requirements_dispatch_through_kind_rows() -> Bool { - os_install_actuator_requirement_kinds.first() == BmcNetworkReach - && os_install_actuator_requirement_kinds.skip(n: 1).first() == ActuatorToolchainGrant + os_install_actuator_requirement_kinds.first() == Present { value: BmcNetworkReach } + && os_install_actuator_requirement_kinds.skip(n: 1).first() == Present { value: ActuatorToolchainGrant } && os_install_actuator_requirement_satisfied( kind: BmcNetworkReach, candidate: srv1_host, @@ -26,8 +26,8 @@ test fn srv3_actuator_host_selected_because_requirements_and_policy() -> Bool { && srv3_os_install_actuator_host_is_derived_srv1() && match srv3_os_install_actuator_tie_break_policy { OperatorHostPreference { order: order } => - order.first() == operator_host_srv1 - && order.skip(n: 1).first() == operator_host_srv2 + order.first() == Present { value: operator_host_srv1 } + && order.skip(n: 1).first() == Present { value: operator_host_srv2 } _ => false } } From a39504add10d9212da0a33541083630ffc0f12c1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 8 Oct 2026 06:58:01 +0000 Subject: [PATCH 2/2] os_install_actuator_selection witness: pin the declared rosters by whole-list equality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- ...s_install_actuator_selection_witness_test.dag | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/dag/test/claim/os_install_actuator_selection_witness_test.dag b/dag/test/claim/os_install_actuator_selection_witness_test.dag index 6242938af19..d631ba33a9c 100644 --- a/dag/test/claim/os_install_actuator_selection_witness_test.dag +++ b/dag/test/claim/os_install_actuator_selection_witness_test.dag @@ -3,9 +3,18 @@ module test.claim.os_install_actuator_selection data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly +// The dispatch consumes the kind rows in declaration order; pin the declared +// roster by whole-list equality. List.first() cannot be used here: the checker +// types it T? (#13179) while the executing runtime returns the bare element +// (the fork recorded in cross_type_comparison_answers_instead_of_refusing), so +// no first()-based comparison both type-checks and executes true. test fn os_install_actuator_requirements_dispatch_through_kind_rows() -> Bool { - os_install_actuator_requirement_kinds.first() == Present { value: BmcNetworkReach } - && os_install_actuator_requirement_kinds.skip(n: 1).first() == Present { value: ActuatorToolchainGrant } + os_install_actuator_requirement_kinds == [ + BmcNetworkReach, + ActuatorToolchainGrant, + InstallMediaArtifactRealizable, + InstallWindowAvailability, + ] && os_install_actuator_requirement_satisfied( kind: BmcNetworkReach, candidate: srv1_host, @@ -26,8 +35,7 @@ test fn srv3_actuator_host_selected_because_requirements_and_policy() -> Bool { && srv3_os_install_actuator_host_is_derived_srv1() && match srv3_os_install_actuator_tie_break_policy { OperatorHostPreference { order: order } => - order.first() == Present { value: operator_host_srv1 } - && order.skip(n: 1).first() == Present { value: operator_host_srv2 } + order == [operator_host_srv1, operator_host_srv2] _ => false } }