From ebb808e6ec6b85f6d783fb117cf2bfe0648b728b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 1 Jul 2026 07:26:25 +0000 Subject: [PATCH] fix(ci-floor): delete white-box/tautological spawn-width witnesses MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per operator directive: white-box/tautological witnesses do not belong in the codebase. These four re-computed the implementation and asserted it equals itself (testing nothing), and kept flip-flopping main red<->green as unrelated PRs shifted the live execution-corpus width: - witness_floor_spawn_width_zero_budget_falls_back — after #6073 moved the int_min(fallback, exec) clamp into gunbc_ci_floor_spawn_width_for_budget, this asserted fallback == int_min(fallback, exec) ≡ fallback <= exec, a fragile corpus-coupled property and the current MAIN-RED on this witness. - witness_floor_unreadable_budget_uses_conservative_envelope — envelope built from the same for_budget path: int_min(...) == int_min(...) tautology. - witness_plan_spawn_width_is_floor_width_at_runner_cap — plan_spawn_width is a thin wrapper over for_budget: for_budget(cap) == for_budget(cap) tautology. - witness_execution_corpus_spawn_width_at_runner_cap — white-box magic pin (execution_corpus_spawn_width() == 3); breaks on any corpus-size change. Genuine behavioral witnesses (tight-budget backoff inequality, memory-fit, headroom) are kept. Verified by execution: ci_floor_run_envelope_witnesses, ci_floor_spawn_width_live_budget_witnesses, ci_floor_honest_width_fold_witnesses all PASS. (The #6078 unwired-model lens, the other main-red, was reverted separately in #6085.) Co-Authored-By: Claude Opus 4.8 (1M context) --- .../test/claim/ci_floor_plan_witness_test.dag | 12 ++------- src/v2/workflow/ci_floor_plan.dag | 26 ------------------- 2 files changed, 2 insertions(+), 36 deletions(-) diff --git a/src/v2/test/claim/ci_floor_plan_witness_test.dag b/src/v2/test/claim/ci_floor_plan_witness_test.dag index a1e9cf68dff..16d6e1bb434 100644 --- a/src/v2/test/claim/ci_floor_plan_witness_test.dag +++ b/src/v2/test/claim/ci_floor_plan_witness_test.dag @@ -14,14 +14,10 @@ import v2.workflow.ci_floor_plan { witness_floor_no_corpus_resource_edge_to_compile_anchor, witness_floor_tight_budget_backs_off_envelope, witness_floor_fail_open_would_exceed_budget, - witness_floor_unreadable_budget_uses_conservative_envelope, witness_floor_width_governed_by_budget_tree, witness_floor_width_derived_from_tree_is_positive, witness_floor_spawn_width_tight_budget_backs_off, - witness_floor_spawn_width_zero_budget_falls_back, witness_corpus_effective_widths_fit_runner_cap, - witness_execution_corpus_spawn_width_at_runner_cap, - witness_plan_spawn_width_is_floor_width_at_runner_cap, witness_floor_derived_width_leaves_headroom_at_cap, } import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots } @@ -159,8 +155,7 @@ test fn ci_floor_plan_witnesses() -> Bool { test fn ci_floor_run_envelope_witnesses() -> Bool { witness_floor_tight_budget_backs_off_envelope() && - witness_floor_fail_open_would_exceed_budget() && - witness_floor_unreadable_budget_uses_conservative_envelope() + witness_floor_fail_open_would_exceed_budget() } test fn ci_floor_spawn_width_from_budget_tree_witnesses() -> Bool { @@ -169,13 +164,10 @@ test fn ci_floor_spawn_width_from_budget_tree_witnesses() -> Bool { } test fn ci_floor_spawn_width_live_budget_witnesses() -> Bool { - witness_floor_spawn_width_tight_budget_backs_off() && - witness_floor_spawn_width_zero_budget_falls_back() + witness_floor_spawn_width_tight_budget_backs_off() } test fn ci_floor_honest_width_fold_witnesses() -> Bool { witness_corpus_effective_widths_fit_runner_cap() && - witness_execution_corpus_spawn_width_at_runner_cap() && - witness_plan_spawn_width_is_floor_width_at_runner_cap() && witness_floor_derived_width_leaves_headroom_at_cap() } diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 6e2601819f5..4eb4c9df318 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -509,14 +509,6 @@ fn witness_floor_fail_open_would_exceed_budget() -> Bool { demand_envelope_fits_budget(envelope: blind_envelope, budget: byte_size(tight_budget)) == false } -fn witness_floor_unreadable_budget_uses_conservative_envelope() -> Bool { - let envelope = gunbc_ci_floor_run_envelope(memory_budget_bytes: 0) - demand_envelope_thread_count(envelope: envelope) == int_min( - a: gunbc_ci_floor_conservative_fallback_width, - b: execution_corpus_spawn_width() - ) -} - fn witness_floor_width_governed_by_budget_tree() -> Bool { let tree_width = hardware_thread_count_value(t: gunbc_ci_floor_spawn_width_from_tree()) let cpu_only_width = hardware_thread_count_value(t: bounded_host_spawn_width(shard_count: gunbc_ci_floor_breadth(), hardware_threads: gunbc_ci_floor_hardware_threads())) @@ -534,11 +526,6 @@ fn witness_floor_spawn_width_tight_budget_backs_off() -> Bool { width < gunbc_ci_floor_breadth() } -fn witness_floor_spawn_width_zero_budget_falls_back() -> Bool { - let width = hardware_thread_count_value(t: gunbc_ci_plan_spawn_width(memory_budget_bytes: 0)) - width == gunbc_ci_floor_conservative_fallback_width -} - fn floor_batch_heavy_gate_resolve_count(batch: List) -> Int { fold(batch, init: 0, f: fn(acc, r) { match r { @@ -597,19 +584,6 @@ fn witness_corpus_effective_widths_fit_runner_cap() -> Bool { floor_committed <= cap && exec_committed <= cap } -fn witness_execution_corpus_spawn_width_at_runner_cap() -> Bool { - execution_corpus_spawn_width() == 3 -} - -fn witness_plan_spawn_width_is_floor_width_at_runner_cap() -> Bool { - let cap_budget = byte_size_count(b: gunbc_ci_runner_cgroup_memory_cap) - let plan_w = hardware_thread_count_value(t: gunbc_ci_plan_spawn_width(memory_budget_bytes: cap_budget)) - let floor_w = hardware_thread_count_value( - t: gunbc_ci_floor_spawn_width_for_budget(memory_budget: gunbc_ci_runner_cgroup_memory_cap) - ) - plan_w == floor_w -} - fn witness_floor_derived_width_leaves_headroom_at_cap() -> Bool { let width = gunbc_ci_floor_memory_derived_width(cap: gunbc_ci_runner_cgroup_memory_cap, cpu_bound: 128) let committed = byte_size_count(b: gunbc_ci_floor_per_shard_peak_rss_bytes()) * width