From f097c4130f0e26e22cbffc84dd7393e285ddd3e8 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 06:07:29 +0000 Subject: [PATCH 1/9] Classify the five scoped witness entries, and put their disposition carrier where both worlds can see it The scoped witness batch declares SelectionApplied, and its authority note claims normal affected-set selection avoids the measured closure materialization on unrelated PRs. Neither was true. None of the five entries declared a live_tree_disposition row; undeclared fail-closes to ReadsLiveTree; a ReadsLiveTree row can never predict-skip. All 31 test functions therefore ran on every pull request and the ~376s dag+src/v1 world was materialized unconditionally. The derived axis was not forcing it: all five closures carry zero path-like data rows and zero host-effect sinks, so the always-run behavior came only from the missing declarations. They could not be declared. LiveTreeDisposition lived only in src/v2/std/live_tree.dag, and the scoped subject universe is exactly dag plus src/v1 with src/v2 deliberately excluded, so the annotation would have been a hard UnresolvedType. The nine-line carrier moves under dag/ keeping module v2.std.live_tree, so every one of its 632 existing importers is untouched and a src/v1 entry can finally declare its own disposition at entry grain, where the carrier's own authority says the fact belongs. Paths are discriminators, not gospel; renaming the module to std.live_tree is a separate migration, not collateral to this repair. WitnessRefusalCause gains three cause FAMILIES rather than one arm per leaf failure: subject observation, dependency observation, and disposition-authority disagreement. The leaf detail stays in `reason`. Overloading FrontierQueryRefusal with dependency and subject ignorance would re-collapse three different remedies into one label, which is the state-space conflation this coproduct exists to have deleted. The three exhaustive matches are updated arm-by-arm; no wildcard is introduced, so every existing consumer states what it does about the new ignorance classes. Two stale claims in the carrier's own notes are corrected here rather than left as historical context: that a SubstrateInputsOnly row is re-checked by no text scan, and that the nightly falsifier is its enforcement. A derived closure scan does re-check it, and the falsifier could never have enforced it for a src/v1 subject because its lanes resolve over dag plus src/v2. This commit changes no execution behavior on its own: the entries become selection-eligible, but the scoped child is still spawned unconditionally. The admission that consumes this classification lands in the next commit; neither half is separable, because the classification without the admission changes coverage for nothing and the admission without the classification routes around a live never-skip wall. Co-Authored-By: Claude Opus 5 (1M context) --- dag/std/live_tree.dag | 13 +++++++++++++ src/v1/tests/claim/caret_parse_smoke_test.dag | 3 +++ ...d_closure_production_admissions_witness_test.dag | 3 +++ .../claim/ordinary_frontend_observation_test.dag | 3 +++ .../claim/pattern_binder_declaration_node_test.dag | 3 +++ .../claim/v1_complexity_eviction_hazard_test.dag | 3 +++ src/v2/std/live_tree.dag | 9 --------- .../provenance_fail_closed_contract_test.dag | 6 ++++++ src/v2/workflow/affected_set_floor_runner.dag | 13 +++++++++++++ src/v2/workflow/affected_set_floor_runner_test.dag | 9 +++++++++ 10 files changed, 56 insertions(+), 9 deletions(-) create mode 100644 dag/std/live_tree.dag delete mode 100644 src/v2/std/live_tree.dag diff --git a/dag/std/live_tree.dag b/dag/std/live_tree.dag new file mode 100644 index 00000000000..88f61722f38 --- /dev/null +++ b/dag/std/live_tree.dag @@ -0,0 +1,13 @@ +module v2.std.live_tree + +data live_tree_disposition_note: String = "Declared witness input-domain disposition (ROADMAP 2-host-scaffold-classifier-defork): a witness entry declares whether its evaluation reads the live host tree (filesystem/corpus state outside its resolved substrate closure). The single authority is a `data live_tree_disposition: LiveTreeDisposition = ...` row in the WITNESS ENTRY FILE itself - entry grain, so the fact holds no matter where the read hides behind imports. Undeclared = ReadsLiveTree (fail-closed): a row must declare SubstrateInputsOnly to become affected-set selection-eligible. This dissolves the interim floor:host_scaffold marker and the Rust text classifier witness_test_fn_uses_live_host_scan (deleted with this model). + +CORRECTED 2026-08-11 (session lively-bat-548). This note previously read 'a row that declares SubstrateInputsOnly while actually reading live state is NOT re-checked by any text scan; the nightly affected-set falsifier is the enforcement'. Both halves were false in the live tree. A derived text scan over the entry's whole import closure DOES re-check the declaration - cli_run effect_reach_derived_reads_live_tree_for_entry, over effect_reach_host_sink_callee_symbols_v0 (v2.std.effect_reach) - and reads_live_tree_effective is the OR of declared and derived, so a lying row is caught at selection time rather than a cadence window later. The falsifier could not have been the enforcement for every subject either: its lanes resolve over dag plus src/v2, so a src/v1 witness entry is unresolvable there. Where a declaration is CONSUMED to admit expensive work, the OR is additionally too weak on its own: silently upgrading a stale SubstrateInputsOnly row to ReadsLiveTree hides a broken authority behind an always-run answer, so gunbc.scoped_floor_execution refuses that disagreement as DispositionAuthorityRefusal instead of degrading. + +FILE HOME. This module is authored under dag/ while keeping the module path v2.std.live_tree, because a witness entry under src/v1 must be able to declare its own disposition and the scoped witness subject universe is exactly dag plus src/v1 - src/v2 is deliberately excluded from it. Under src/v2 the carrier was invisible to half the corpus it classifies, so no src/v1 entry could declare the row at all and all of them inherited the fail-closed default. Paths are discriminators, not gospel (DESIGN section 3); the module path is unchanged, so every existing importer is untouched. Renaming the module to std.live_tree is a separate authority migration, not collateral to this repair." + +data live_tree_disposition_stamp_provenance: String = "Migration stamp provenance (2026-07-11, machine-stamped batch): the initial corpus-wide SubstrateInputsOnly rows were stamped from the deleted entry-text classifier's verdict (entry file contains none of: floor:host_scaffold, layer_import_facts, _live(, _facts_live(, filesystem_read) - ENTRY-TEXT GRAIN, so they inherit that classifier's declared blind spot: a live read hidden behind an import was invisible to it (the former cli_run.rs cross-file deficit). A stamped row is therefore machine-vouched, not author-vouched. Enforcement is the derived closure scan described in live_tree_disposition_note, which closes exactly the cross-file blind spot the entry-text classifier declared. Dissolves-at: G2 call-reachability live-read classification (import-closure walk over LiveReadCarrier registry + fn-arrow DependencyView) per docs/plans/live-read-witness-classification-design.md — when stamps can be re-derived from proven runtime-read closure." + +type LiveTreeDisposition + = ReadsLiveTree + | SubstrateInputsOnly diff --git a/src/v1/tests/claim/caret_parse_smoke_test.dag b/src/v1/tests/claim/caret_parse_smoke_test.dag index 5dfd9701a2b..088a173c214 100644 --- a/src/v1/tests/claim/caret_parse_smoke_test.dag +++ b/src/v1/tests/claim/caret_parse_smoke_test.dag @@ -26,6 +26,9 @@ import v1.compiler.parse { } import v1.compiler.compile { compile_sources, compile_to_resolved, SourceFile } import v1.compiler.artifact { Rust } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data caret_parse_smoke_parser_transport_enrollment: String = "Scheduled per PR through gunbc.ci_layer_roots v1_claim_scoped_witness_entries and v1_claim_scoped_witness_batch, enrolled by scoped_witness_batches; v2.workflow.ci_floor_plan gunbc_ci_floor_ordinary_batches folds those generic instances into the floor. The scoped batch supplies exactly dag plus src/v1 without widening ordinary witness discovery. Local reproduction: target/release/claim_batch --source-root dag --source-root src/v1 --entry src/v1/tests/claim/caret_parse_smoke_test.dag --functions w_caret_tokenizes_as_sh_caret,w_caret_paren_tokenizes_as_caret_then_lparen,w_parse_caret_ident_produces_literal,w_parse_caret_paren_produces_discriminant_call,w_parse_expr_caret_paren_full_pipeline,w_parse_expr_caret_var_arg_produces_discriminant_call,w_parse_module_let_caret_paren. The native compile and emit claims remain on cargo test -p v1-compiler --lib caret_parse_smoke_native_compile_emit_witnesses until v1.compile_sources is interpreter-runnable (same map_keys gap as probe_emit_interp.dag)." diff --git a/src/v1/tests/claim/namespace_reference_derived_closure_production_admissions_witness_test.dag b/src/v1/tests/claim/namespace_reference_derived_closure_production_admissions_witness_test.dag index c48aaa74371..e90e326adb6 100644 --- a/src/v1/tests/claim/namespace_reference_derived_closure_production_admissions_witness_test.dag +++ b/src/v1/tests/claim/namespace_reference_derived_closure_production_admissions_witness_test.dag @@ -31,6 +31,9 @@ import v1.gunbc.namespace_reference_derived_closure_production_observations { namespace_structural_binding_observations_a_through_d, } import std.types { Bool, Int, List } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data namespace_reference_derived_closure_production_admissions_witness_note: String = "N3-A production and assessment witnesses under src/v1/tests/claim — outside witness_layer_roots compile-clean entries, scheduled via v1_claim_scoped_witness_batch (dag plus src/v1 envelope). v1 production returns neutral ReferenceBindingObservation carriers; assess_reference_binding_observation projects capability admissions here. The namespace-structural-observations roadmap row stays ExecutionContractUnspecified until a semantic closing carrier lands (prior variant-presence predicate retracted 2026-08-04). Discriminating RED: witness_closing_contract_still_reds_until_dependency_clauses_land exercises the parent frontier count." diff --git a/src/v1/tests/claim/ordinary_frontend_observation_test.dag b/src/v1/tests/claim/ordinary_frontend_observation_test.dag index 83a53771b56..12a3c6b9894 100644 --- a/src/v1/tests/claim/ordinary_frontend_observation_test.dag +++ b/src/v1/tests/claim/ordinary_frontend_observation_test.dag @@ -5,6 +5,9 @@ import v1.compiler.frontend_observation { OrdinaryFrontendObservation, observe_ordinary_frontend } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // Enrollment: the v1_claim_scoped_witness_entries roster (dag + src/v1), the // same scoped batch caret_parse_smoke_test rides. The roster module is named diff --git a/src/v1/tests/claim/pattern_binder_declaration_node_test.dag b/src/v1/tests/claim/pattern_binder_declaration_node_test.dag index aa2023491b4..bf4208192a0 100644 --- a/src/v1/tests/claim/pattern_binder_declaration_node_test.dag +++ b/src/v1/tests/claim/pattern_binder_declaration_node_test.dag @@ -48,6 +48,9 @@ import std.occurrence_identity { authored_token_ordinal_space_from_allocator, OccurrenceIdAllocator, } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data pattern_binder_declaration_node_parser_transport_enrollment: String = "Scheduled per PR through gunbc.ci_layer_roots v1_claim_scoped_witness_entries and v1_claim_scoped_witness_batch, enrolled by scoped_witness_batches; v2.workflow.ci_floor_plan gunbc_ci_floor_ordinary_batches folds those generic instances into the floor. The scoped batch supplies exactly dag plus src/v1 without widening ordinary witness discovery. Local reproduction: target/release/claim_batch --source-root dag --source-root src/v1 --entry src/v1/tests/claim/pattern_binder_declaration_node_test.dag --functions w_pattern_parser_materializes_dedicated_declaration_nodes,w_shorthand_wrapper_and_declaration_roles_remain_distinct,w_let_initializer_retains_lexical_reference_category,w_sequential_parse_uses_disjoint_authored_token_ordinal_ranges,w_parse_error_preserves_authored_token_ordinal_space,w_production_frontend_accepts_valid_occurrence_transport,w_production_frontend_refuses_missing_occurrence_identity,w_production_frontend_refuses_duplicate_occurrence_identity,w_production_frontend_refuses_wrong_occurrence_role,w_production_frontend_refuses_index_terminal_mismatch,w_production_frontend_refuses_ancestor_path_mismatch,w_production_frontend_refuses_duplicate_declaration_rows,w_production_frontend_refuses_duplicate_reference_rows" diff --git a/src/v1/tests/claim/v1_complexity_eviction_hazard_test.dag b/src/v1/tests/claim/v1_complexity_eviction_hazard_test.dag index 3cd3bf5039b..c042142b7f6 100644 --- a/src/v1/tests/claim/v1_complexity_eviction_hazard_test.dag +++ b/src/v1/tests/claim/v1_complexity_eviction_hazard_test.dag @@ -13,6 +13,9 @@ import v1.compiler.complexity { lookup_summary, evict_summary, } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data eviction_hazard_home_note: String = "Homed under src/v1/tests/claim/ because it IMPORTS v1.compiler.complexity to execute the seed, and that is the only home with an EXECUTING consumer for a v1-importing witness: gunbc.ci_layer_roots v1_claim_scoped_witness_entries runs this directory on the scoped batch whose source roots are exactly dag plus src/v1. Two earlier homes were tried and both were wrong, each refuted by the floor rather than by argument. dag/test/claim/long/ failed compile-clean at the import line (unresolved import: module v1.compiler.complexity not found) — a dag/ entry cannot import v1 under compile-clean scope, though it CAN reach v1 declarations through decl_facts pool roots, which is how the sibling resolution census works. src/v2/test/manual/ compiled, but the witness-admission wall refused it: an OfflineLocalRecipe directory stopped being an admission answer on 2026-08-04, because a directory cannot decide that a witness runs, and moving a file under an offline path executes it NOWHERE. That refusal is the same coverage-by-illusion this census argues against, caught in the census itself." diff --git a/src/v2/std/live_tree.dag b/src/v2/std/live_tree.dag deleted file mode 100644 index 6d9b256e43e..00000000000 --- a/src/v2/std/live_tree.dag +++ /dev/null @@ -1,9 +0,0 @@ -module v2.std.live_tree - -data live_tree_disposition_note: String = "Declared witness input-domain disposition (ROADMAP 2-host-scaffold-classifier-defork): a witness entry declares whether its evaluation reads the live host tree (filesystem/corpus state outside its resolved substrate closure). The single authority is a `data live_tree_disposition: LiveTreeDisposition = ...` row in the WITNESS ENTRY FILE itself - entry grain, so the fact holds no matter where the read hides behind imports. Undeclared = ReadsLiveTree (fail-closed): a row must declare SubstrateInputsOnly to become affected-set selection-eligible. A row that declares SubstrateInputsOnly while actually reading live state is NOT re-checked by any text scan; the nightly affected-set falsifier (predict-only cold run) is the enforcement - a lying row surfaces as a counted divergence within one cadence window. This dissolves the interim floor:host_scaffold marker and the Rust text classifier witness_test_fn_uses_live_host_scan (deleted with this model)." - -data live_tree_disposition_stamp_provenance: String = "Migration stamp provenance (2026-07-11, machine-stamped batch): the initial corpus-wide SubstrateInputsOnly rows were stamped from the deleted entry-text classifier's verdict (entry file contains none of: floor:host_scaffold, layer_import_facts, _live(, _facts_live(, filesystem_read) - ENTRY-TEXT GRAIN, so they inherit that classifier's declared blind spot: a live read hidden behind an import was invisible to it (the former cli_run.rs cross-file deficit). A stamped row is therefore machine-vouched, not author-vouched. Enforcement is the nightly affected-set falsifier (counted divergence within one cadence window). Dissolves-at: G2 call-reachability live-read classification (import-closure walk over LiveReadCarrier registry + fn-arrow DependencyView) per docs/plans/live-read-witness-classification-design.md — when stamps can be re-derived from proven runtime-read closure." - -type LiveTreeDisposition - = ReadsLiveTree - | SubstrateInputsOnly diff --git a/src/v2/test/claim/workflow/provenance_fail_closed_contract_test.dag b/src/v2/test/claim/workflow/provenance_fail_closed_contract_test.dag index 0637fc0b8de..4a5ee270db4 100644 --- a/src/v2/test/claim/workflow/provenance_fail_closed_contract_test.dag +++ b/src/v2/test/claim/workflow/provenance_fail_closed_contract_test.dag @@ -30,6 +30,9 @@ import v2.workflow.affected_set_floor_runner { Refused, DiffObservationRefusal, FrontierQueryRefusal, + SubjectObservationRefusal, + DependencyObservationRefusal, + DispositionAuthorityRefusal, floor_precompute_would_skip, floor_witness_run_disposition } @@ -85,6 +88,9 @@ test fn provenance_fail_closed_contract_holds() -> Bool { match cause { FrontierQueryRefusal { reason: reason } => reason == "provenance unavailable" DiffObservationRefusal { reason: _ } => false + SubjectObservationRefusal { reason: _ } => false + DependencyObservationRefusal { reason: _ } => false + DispositionAuthorityRefusal { reason: _ } => false } RunWitness { reason: _ } => false SkipAssumedGreen => false diff --git a/src/v2/workflow/affected_set_floor_runner.dag b/src/v2/workflow/affected_set_floor_runner.dag index e1930e43a25..3b4b900d152 100644 --- a/src/v2/workflow/affected_set_floor_runner.dag +++ b/src/v2/workflow/affected_set_floor_runner.dag @@ -23,9 +23,22 @@ type FloorRerunFrontier = FrontierProduced { nodes: List } | FrontierFailClosed { reason: String } +// Cause FAMILIES, not one arm per leaf failure. Each family names a distinct +// ignorance state whose remedy differs; the leaf detail stays in `reason` so a +// new failure mode inside a family costs no arm. The three added families let a +// consumer that admits expensive work off this disposition state what it does +// about evidence that is neither a diff gap nor a frontier gap: a subject that +// is not the tree we measured, a dependency population that could not be +// derived, and a declared disposition the derived facts contradict. Overloading +// FrontierQueryRefusal with those would re-collapse three remedies into one +// label, which is the state-space conflation this coproduct exists to have +// deleted. type WitnessRefusalCause = DiffObservationRefusal { reason: String } | FrontierQueryRefusal { reason: String } + | SubjectObservationRefusal { reason: String } + | DependencyObservationRefusal { reason: String } + | DispositionAuthorityRefusal { reason: String } type WitnessRunDisposition = RunWitness { reason: String } diff --git a/src/v2/workflow/affected_set_floor_runner_test.dag b/src/v2/workflow/affected_set_floor_runner_test.dag index 5a497aa77e2..26ed2d1caf5 100644 --- a/src/v2/workflow/affected_set_floor_runner_test.dag +++ b/src/v2/workflow/affected_set_floor_runner_test.dag @@ -32,6 +32,9 @@ import v2.workflow.affected_set_floor_runner { Refused, DiffObservationRefusal, FrontierQueryRefusal, + SubjectObservationRefusal, + DependencyObservationRefusal, + DispositionAuthorityRefusal, floor_any_claim_touches_rerun_frontier, floor_claim_touches_rerun_frontier, floor_row_would_skip, @@ -227,6 +230,9 @@ test fn floor_test_diff_fail_closed_refuses_holds() -> Bool { match cause { DiffObservationRefusal { reason: reason } => reason == "git diff unavailable" FrontierQueryRefusal { reason: _ } => false + SubjectObservationRefusal { reason: _ } => false + DependencyObservationRefusal { reason: _ } => false + DispositionAuthorityRefusal { reason: _ } => false } RunWitness { reason: _ } => false SkipAssumedGreen => false @@ -246,6 +252,9 @@ test fn floor_test_frontier_fail_closed_refuses_holds() -> Bool { match cause { FrontierQueryRefusal { reason: reason } => reason == "provenance unavailable" DiffObservationRefusal { reason: _ } => false + SubjectObservationRefusal { reason: _ } => false + DependencyObservationRefusal { reason: _ } => false + DispositionAuthorityRefusal { reason: _ } => false } RunWitness { reason: _ } => false SkipAssumedGreen => false From 7ba5954bb67edcff0a26fe8e12ab6aab8922fb60 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 06:11:28 +0000 Subject: [PATCH 2/9] The scoped admission decision, as a pure fold over observed standings gunbc.scoped_floor_execution returns the EXISTING WitnessRunDisposition rather than a second admission coproduct: run, skip-assumed-green and typed refusal are the same three answers v2.workflow.affected_set_floor_runner already models, and a scoped-only sum would be a second name for them. The affected relation is NOT authored here. An earlier draft carried the five entries' dependency population as rows, which would have been a second edge producer beside dependency_resolution_facts_live - forbidden in terms by the module_graph authority - and a hand-authored population is exactly the roster that counts the subjects someone remembered to author. The question is asked of v2.lens.module_graph entry_affected_by_touched_paths at the scoped batch's own pool roots instead, so this module inherits the strict-tier reference-derived union for free and keeps answering correctly when the import grammar is deleted. The live projection is one declaration, held apart from the decision on purpose. scoped_affected_standing_live is the only thing here that reads the corpus; the decision is a pure fold over standings already observed. Fusing them would have made the witness itself a live-tree reader - the exact class the disposition wall in the previous commit exists to refuse - and would have put a corpus scan on every discriminating control. Affectedness and its ignorance state share one carrier. ScopedAffectedStanding is affected, unaffected, or undecidable, because a Bool beside a flag is how "could not decide" starts reading as "unaffected". Undecidable refuses. So does a subject that is not the tree the diff describes, a diff that could not be observed, and a declared disposition the derived facts contradict - the last one refusing rather than degrading to always-run, because degrading is operationally safe and epistemically silent, and hides a broken authority behind a green answer. A departed path runs the batch. It is a deletion, rename or copy whose pre-image is not in the head tree, so a head-only closure cannot reach the file whose absence is the question. That is a declared response to an observed change class, not a fallback from an instrument failure. The witness discriminates all four refusal axes and both positive arms on synthetic standings. The unaffected-skips control is load-bearing: without it the refusal controls would all pass on a decision that never skips anything, and would therefore prove nothing about the cost this change exists to remove. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/scoped_floor_execution.dag | 173 ++++++++++++++ .../scoped_floor_execution_witness_test.dag | 226 ++++++++++++++++++ 2 files changed, 399 insertions(+) create mode 100644 dag/gunbc/scoped_floor_execution.dag create mode 100644 dag/test/claim/scoped_floor_execution_witness_test.dag diff --git a/dag/gunbc/scoped_floor_execution.dag b/dag/gunbc/scoped_floor_execution.dag new file mode 100644 index 00000000000..505145db4ab --- /dev/null +++ b/dag/gunbc/scoped_floor_execution.dag @@ -0,0 +1,173 @@ +module gunbc.scoped_floor_execution + +import v2.std.algebra { any, length } +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.text { String } +import v2.lens.module_graph { + entry_affected_by_touched_paths, + module_declaration_facts_live +} +import v2.workflow.affected_set_floor_runner { + DiffObservationRefusal, + DiffObservationFailClosed, + DiffPathsProduced, + DependencyObservationRefusal, + DispositionAuthorityRefusal, + FloorDiffObservation, + Refused, + RunWitness, + SkipAssumedGreen, + SubjectObservationRefusal, + WitnessRunDisposition +} + +// WHY THIS EXISTS. The scoped witness batch (gunbc.ci_layer_roots +// v1_claim_scoped_witness_batch) materializes a SECOND semantic world over the +// source roots dag plus src/v1 to run five entries. That world costs a measured +// ~376 seconds and, before this module, was constructed on EVERY pull request: +// the batch declares SelectionApplied, but none of its five entries declared a +// live_tree_disposition row, undeclared fail-closes to ReadsLiveTree, and a +// ReadsLiveTree row can never predict-skip. So the declared selection was inert +// and the batch's own note - claiming normal affected-set selection avoided the +// closure materialization on unrelated PRs - described behavior the tree did not +// have. +// +// WHERE THE DECISION HAD TO GO, and why not the plan. The floor plan is a pure +// argument-free fold evaluated under ExecutionMode Hermetic, where the git diff +// effect refuses; a diff-dependent plan shape is therefore not merely awkward, +// it is unavailable at that layer. The ordinary floor worker, by contrast, +// already observes the diff Wet and already projects the list of scoped batch +// ids into a manifest that the coordinator spawns children from. An empty +// manifest already yields zero scoped workers and a successful coordinator, so +// gating that projection is the whole incision: no plan reshaping, no batch +// renumbering, and no change to the scoped child itself. +// +// WHY THERE IS NO PATH ROSTER HERE. An earlier draft of this module carried the +// entries' dependency population as authored rows. That would have been a second +// edge producer beside dependency_resolution_facts_live, which the module_graph +// authority forbids in terms ("Do not add a second edge producer beside +// dependency_resolution_facts_live; the swap replaces its body"), and a +// hand-authored population is exactly the roster that counts the subjects +// someone remembered to author. The closure question is asked of the existing +// authority instead, per entry, with the scoped batch's own pool roots - so this +// module inherits the reference-derived union for free and keeps working when +// the import grammar is deleted. +data scoped_floor_execution_note: String = "Pre-construction admission for the dag plus src/v1 scoped witness batch. Returns the EXISTING v2.workflow.affected_set_floor_runner WitnessRunDisposition rather than a second admission coproduct: run, skip-assumed-green, and typed refusal are the same three answers that lane already models, and a scoped-only sum would be a second name for them. The affected relation is v2.lens.module_graph entry_affected_by_touched_paths asked at the scoped pool roots, not a roster authored here. Every ignorance state refuses; none widens and none narrows. The consumer is the ordinary floor worker's scoped-batch manifest projection in claim_executor, which writes the batch id on RunWitness, an empty manifest on SkipAssumedGreen, and fails loudly on Refused." + +// The tested tree must be the tree the observations describe. A subject standing +// exists as its own axis because a diff taken against one commit and a closure +// derived from another is not a weaker answer, it is a different question, and +// silently answering it is how a skip becomes unfalsifiable. +type ScopedSubjectStanding + = ScopedSubjectMatched + | ScopedSubjectMismatched { reason: String } + +// Declared-versus-derived disagreement is a DEFECT, not a conservative input. +// The seed's reads_live_tree_effective is the OR of declared and derived, which +// is operationally safe - it degrades to always-run - but where a declaration is +// consumed to ADMIT expensive work, silently upgrading a stale SubstrateInputsOnly +// row to ReadsLiveTree hides a broken authority behind a green answer. This axis +// refuses instead, so the stale row is repaired rather than absorbed. +type ScopedDispositionStanding + = ScopedDispositionAgrees + | ScopedDispositionContradicted { reason: String } + +// The affected verdict and its ignorance state in ONE carrier, because they are +// answers to the same question and splitting them into a Bool beside a flag is +// how "could not decide" starts reading as "unaffected". Undecidable is not a +// weaker unaffected: a widen is merely expensive, a narrow is silently uncovered. +type ScopedAffectedStanding + = ScopedEntriesAffected + | ScopedEntriesUnaffected + | ScopedAffectedUndecidable { reason: String } + +// LIVE PROJECTION - the only declaration in this module that reads the tree. +// It is deliberately separated from the decision below so the decision stays a +// pure fold over observed facts: a witness can then discriminate every arm on +// synthetic standings without paying a corpus scan, and this projection is +// exercised by the floor run that consumes it. Mixing them would have made the +// witness itself a live-tree reader, which is the exact class the disposition +// wall in this change exists to refuse. +fn scoped_affected_standing_live( + entries: List, + pool_roots: List, + touched_paths: List +) -> ScopedAffectedStanding { + if length(xs: entries) == 0 { + ScopedAffectedUndecidable { + reason: "scoped entry roster is empty; no entry population to decide against" + } + } else if length(xs: module_declaration_facts_live(pool_roots: pool_roots)) == 0 { + ScopedAffectedUndecidable { + reason: "scoped pool roots declared zero modules; the dependency authority could not answer" + } + } else if any( + xs: entries, + predicate: fn(entry) { + entry_affected_by_touched_paths( + entry_path: entry, + pool_roots: pool_roots, + touched_paths: touched_paths + ) + } + ) { + ScopedEntriesAffected + } else { + ScopedEntriesUnaffected + } +} + +// A departed path is a deletion, rename, or copy. Its pre-image is not in the +// head tree, so a head-only closure cannot decide whether it was a dependency: +// the file whose absence matters is exactly the file the closure can no longer +// reach. Until base and head closures are compared exactly, any departure runs +// the batch. This is a declared response to an observed change class, not a +// fallback from an instrument failure - the observation succeeded and reported +// departures. +fn scoped_departure_forces_run(departed_paths: List) -> Bool { + length(xs: departed_paths) > 0 +} + +// The decision - a pure fold over already-observed standings. Refusals come +// first and are exhaustive over the four ignorance axes; only inside a fully +// observed, non-contradicted world does the positive-evidence ladder run, and +// its fall-through is the skip. The diff's changed paths are not re-read here +// because the affected standing already answered the question they exist to ask; +// an empty diff therefore reaches SkipAssumedGreen through ScopedEntriesUnaffected +// rather than through a special case, matching floor_witness_run_disposition. +fn scoped_witness_run_disposition( + subject: ScopedSubjectStanding, + disposition: ScopedDispositionStanding, + diff: FloorDiffObservation, + departed_paths: List, + affected: ScopedAffectedStanding +) -> WitnessRunDisposition { + match subject { + ScopedSubjectMismatched { reason: reason } => + Refused { cause: SubjectObservationRefusal { reason: reason } } + ScopedSubjectMatched => + match disposition { + ScopedDispositionContradicted { reason: reason } => + Refused { cause: DispositionAuthorityRefusal { reason: reason } } + ScopedDispositionAgrees => + match diff { + DiffObservationFailClosed { reason: reason } => + Refused { cause: DiffObservationRefusal { reason: reason } } + DiffPathsProduced { changed_paths: _ } => + match affected { + ScopedAffectedUndecidable { reason: reason } => + Refused { cause: DependencyObservationRefusal { reason: reason } } + ScopedEntriesAffected => + RunWitness { reason: "scoped entry dependency closure intersects a changed path" } + ScopedEntriesUnaffected => + if scoped_departure_forces_run(departed_paths: departed_paths) { + RunWitness { reason: "scoped diff reports a departed path; head-only closure cannot bound it" } + } else { + SkipAssumedGreen + } + } + } + } + } +} diff --git a/dag/test/claim/scoped_floor_execution_witness_test.dag b/dag/test/claim/scoped_floor_execution_witness_test.dag new file mode 100644 index 00000000000..169c349ca12 --- /dev/null +++ b/dag/test/claim/scoped_floor_execution_witness_test.dag @@ -0,0 +1,226 @@ +module test.claim.scoped_floor_execution_witness_test + +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.text { String } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.workflow.affected_set_floor_runner { + DiffObservationRefusal, + DiffObservationFailClosed, + DiffPathsProduced, + DependencyObservationRefusal, + DispositionAuthorityRefusal, + FloorDiffObservation, + FrontierQueryRefusal, + Refused, + RunWitness, + SkipAssumedGreen, + SubjectObservationRefusal, + WitnessRunDisposition +} +import gunbc.scoped_floor_execution { + ScopedAffectedStanding, + ScopedAffectedUndecidable, + ScopedDispositionStanding, + ScopedDispositionAgrees, + ScopedDispositionContradicted, + ScopedEntriesAffected, + ScopedEntriesUnaffected, + ScopedSubjectStanding, + ScopedSubjectMatched, + ScopedSubjectMismatched, + scoped_witness_run_disposition +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data w_subject_note: String = "SUBJECT: the admission that decides whether the dag plus src/v1 scoped world is constructed at all. Every ignorance axis must refuse rather than answer, because a false skip here is silently uncovered rather than merely expensive: the batch it gates carries 31 behavioral test functions whose only other execution route is the main-push SelectionOff control. The positive control pins that an unaffected diff really does reach SkipAssumedGreen - a refusal-only witness would pass on a decision that never skips anything and therefore never saved the 376 seconds this exists to save. These witnesses discriminate the PURE decision on synthetic standings; the live projection scoped_affected_standing_live is the one declaration that reads the corpus, and it is exercised by the floor run that consumes it rather than by a witness that would have to scan the tree to assert anything." + +data unrelated_diff: FloorDiffObservation = DiffPathsProduced { + changed_paths: ["docs/plans/some-note.md", "src/v2/lens/affected_set.dag"] +} + +data touching_diff: FloorDiffObservation = DiffPathsProduced { + changed_paths: ["src/v1/compiler/tokenize.dag"] +} + +data empty_diff: FloorDiffObservation = DiffPathsProduced { + changed_paths: [] +} + +fn decide( + subject: ScopedSubjectStanding, + disposition: ScopedDispositionStanding, + diff: FloorDiffObservation, + departed_paths: List, + affected: ScopedAffectedStanding +) -> WitnessRunDisposition { + scoped_witness_run_disposition( + subject: subject, + disposition: disposition, + diff: diff, + departed_paths: departed_paths, + affected: affected + ) +} + +fn is_skip(d: WitnessRunDisposition) -> Bool { + match d { + SkipAssumedGreen => true + RunWitness { reason: _ } => false + Refused { cause: _ } => false + } +} + +fn is_run(d: WitnessRunDisposition) -> Bool { + match d { + RunWitness { reason: _ } => true + SkipAssumedGreen => false + Refused { cause: _ } => false + } +} + +// POSITIVE CONTROL - the arm the whole change exists to reach. Without this the +// refusal controls below would all pass on a decision that never skips. +test fn w_unaffected_diff_skips_the_scoped_world() -> Bool { + is_skip(d: decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: unrelated_diff, + departed_paths: [], + affected: ScopedEntriesUnaffected + )) +} + +test fn w_affected_closure_runs_the_scoped_batch() -> Bool { + is_run(d: decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: touching_diff, + departed_paths: [], + affected: ScopedEntriesAffected + )) +} + +// The empty diff must reach the skip through the general affected arm, not a +// special-cased branch - the same law floor_witness_run_disposition holds. +test fn w_empty_diff_flows_the_general_skip_arm() -> Bool { + is_skip(d: decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: empty_diff, + departed_paths: [], + affected: ScopedEntriesUnaffected + )) +} + +// A departure is an OBSERVED change class, so it runs rather than refuses - but +// it must never skip, because a head-only closure cannot reach the file whose +// absence is the question. +test fn w_departed_path_runs_even_when_the_closure_reports_unaffected() -> Bool { + is_run(d: decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: unrelated_diff, + departed_paths: ["src/v1/compiler/tokenize.dag"], + affected: ScopedEntriesUnaffected + )) +} + +// RED - a declared SubstrateInputsOnly row the derived facts contradict is a +// broken authority. It must refuse, not degrade to always-run: degrading is +// operationally safe and epistemically silent, and the stale row would never be +// repaired. The affected standing here says UNAFFECTED, so a decision that +// ignored the disposition axis would skip. +test fn red_contradicted_disposition_refuses_and_names_the_authority() -> Bool { + match decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionContradicted { reason: "entry declares SubstrateInputsOnly but derived closure reaches a host-effect sink" }, + diff: unrelated_diff, + departed_paths: [], + affected: ScopedEntriesUnaffected + ) { + Refused { cause: cause } => + match cause { + DispositionAuthorityRefusal { reason: _ } => true + DiffObservationRefusal { reason: _ } => false + FrontierQueryRefusal { reason: _ } => false + SubjectObservationRefusal { reason: _ } => false + DependencyObservationRefusal { reason: _ } => false + } + RunWitness { reason: _ } => false + SkipAssumedGreen => false + } +} + +// RED - an undecidable affected standing is ignorance, not an empty +// intersection. Answering "nothing is affected" from a query that could not +// complete is the empty-observation narrow. +test fn red_undecidable_affected_standing_refuses() -> Bool { + match decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: unrelated_diff, + departed_paths: [], + affected: ScopedAffectedUndecidable { reason: "scoped pool roots declared zero modules; the dependency authority could not answer" } + ) { + Refused { cause: cause } => + match cause { + DependencyObservationRefusal { reason: _ } => true + DiffObservationRefusal { reason: _ } => false + FrontierQueryRefusal { reason: _ } => false + SubjectObservationRefusal { reason: _ } => false + DispositionAuthorityRefusal { reason: _ } => false + } + RunWitness { reason: _ } => false + SkipAssumedGreen => false + } +} + +// RED - an unobserved diff refuses on its own axis, and is not laundered into a +// dependency or subject refusal. +test fn red_unobserved_diff_refuses_on_the_diff_axis() -> Bool { + match decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: DiffObservationFailClosed { reason: "git diff unavailable" }, + departed_paths: [], + affected: ScopedEntriesUnaffected + ) { + Refused { cause: cause } => + match cause { + DiffObservationRefusal { reason: _ } => true + DependencyObservationRefusal { reason: _ } => false + FrontierQueryRefusal { reason: _ } => false + SubjectObservationRefusal { reason: _ } => false + DispositionAuthorityRefusal { reason: _ } => false + } + RunWitness { reason: _ } => false + SkipAssumedGreen => false + } +} + +// RED - a closure derived from one tree and a diff taken against another is a +// different question, not a weaker answer. The affected standing here says +// AFFECTED, so a decision that ignored the subject axis would run and look +// harmless; the refusal is what makes the mismatch visible. +test fn red_subject_mismatch_refuses_before_any_affected_reading() -> Bool { + match decide( + subject: ScopedSubjectMismatched { reason: "closure derived at a revision other than the tested head" }, + disposition: ScopedDispositionAgrees, + diff: touching_diff, + departed_paths: [], + affected: ScopedEntriesAffected + ) { + Refused { cause: cause } => + match cause { + SubjectObservationRefusal { reason: _ } => true + DiffObservationRefusal { reason: _ } => false + FrontierQueryRefusal { reason: _ } => false + DependencyObservationRefusal { reason: _ } => false + DispositionAuthorityRefusal { reason: _ } => false + } + RunWitness { reason: _ } => false + SkipAssumedGreen => false + } +} From 63df5022dcd0e358533c932a217e8c3570f672a2 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 06:18:10 +0000 Subject: [PATCH 3/9] chore: regenerate drifted generated artifacts (ci auto-heal) --- .gitattributes | 1 + dag/gunbc/stage0_emit_plan_generated.dag | 2 ++ 2 files changed, 3 insertions(+) diff --git a/.gitattributes b/.gitattributes index b0a29311293..688be46a820 100644 --- a/.gitattributes +++ b/.gitattributes @@ -213,6 +213,7 @@ src/v1/stage0/src/v1_tests_claim_v1_annotation_erasure_test.rs merge=generated-a src/v1/stage0/src/v1_tests_claim_v1_annotation_round_trip_test.rs merge=generated-artifact src/v1/stage0/src/v1_tests_claim_v1_annotation_target_emission_test.rs merge=generated-artifact src/v1/stage0/src/v1_tests_claim_v1_complexity_eviction_hazard_test.rs merge=generated-artifact +src/v1/stage0/src/v2_std_live_tree.rs merge=generated-artifact src/v1/stage0/src/wt_a.rs merge=generated-artifact src/v1/stage0/src/wt_b.rs merge=generated-artifact src/v1/stage0/src/wt_common.rs merge=generated-artifact diff --git a/dag/gunbc/stage0_emit_plan_generated.dag b/dag/gunbc/stage0_emit_plan_generated.dag index 6d0381bc3b9..34b8c8f4983 100644 --- a/dag/gunbc/stage0_emit_plan_generated.dag +++ b/dag/gunbc/stage0_emit_plan_generated.dag @@ -141,6 +141,7 @@ data generated_stage0_files: List = [ "v1_tests_claim_v1_annotation_round_trip_test.rs", "v1_tests_claim_v1_annotation_target_emission_test.rs", "v1_tests_claim_v1_complexity_eviction_hazard_test.rs", + "v2_std_live_tree.rs", "wt_a.rs", "wt_b.rs", "wt_common.rs" @@ -283,6 +284,7 @@ data generated_stage0_paths: List = [ "src/v1/stage0/src/v1_tests_claim_v1_annotation_round_trip_test.rs", "src/v1/stage0/src/v1_tests_claim_v1_annotation_target_emission_test.rs", "src/v1/stage0/src/v1_tests_claim_v1_complexity_eviction_hazard_test.rs", + "src/v1/stage0/src/v2_std_live_tree.rs", "src/v1/stage0/src/wt_a.rs", "src/v1/stage0/src/wt_b.rs", "src/v1/stage0/src/wt_common.rs" From 2f909c5f8f38a1a5cc6a0b4f899783be2393e1a3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 06:36:33 +0000 Subject: [PATCH 4/9] =?UTF-8?q?The=20seed=20observes;=20the=20.dag=20decid?= =?UTF-8?q?es=20=E2=80=94=20and=20a=20cold=20lane=20keeps=20it=20honest?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The scoped batch's manifest projection was unconditional, so every pull request paid the ~376s dag+src/v1 world. This gates that projection on gunbc.scoped_floor_execution rather than reshaping the plan: the plan is a pure argument-free fold evaluated Hermetic, where the git diff effect refuses, so a diff-dependent plan shape is unavailable at that layer, while the ordinary worker already observes the diff Wet and already projects the manifest an empty version of which yields zero children. Three observations cross the boundary — which tree the diff describes, the Wet name-status diff, and the declared-versus-derived disposition standing of the batch's own roster — and the fold returns the existing WitnessRunDisposition. No second admission coproduct: run, skip, and typed refusal are the three answers that lane already models. The disposition axis refuses rather than degrading. reads_live_tree_effective is the OR of declared and derived, which is operationally safe and epistemically silent; where a declaration ADMITS expensive work, a stale SubstrateInputsOnly row silently upgraded to always-run is a broken authority behind a green answer. entry_roster_disposition_conflict deliberately returns the CONFLICT, not the OR. And because the 31 scoped test functions lose their unconditional route the moment this can skip, the same change enrolls their control: scoped_execution_policy_for_event predicts only on pull_request, so every other event admits the batch and turns node frontier selection Off inside the child. Admitting while leaving selection applied would re-derive the same prediction one layer down and back-stop nothing. The policy sits BEHIND the subject and disposition axes — a broken authority is a defect on every event, and a backstop that amnestied it would leave main green while nobody repaired the row. Also corrects two stale notes in gunbc.ci_layer_roots that this measured: the batch note claimed normal affected-set selection already avoided the closure on unrelated PRs, and the dissolve-on note claimed a header-only ledger reds visibly when its decoder has no production consumer. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/ci_layer_roots.dag | 4 +- dag/gunbc/scoped_floor_execution.dag | 136 +++++++-- .../scoped_floor_execution_witness_test.dag | 91 ++++++ src/v1/stage0/src/bin/claim_executor.rs | 276 +++++++++++++++++- src/v1/stage0/src/cli_run.rs | 36 ++- 5 files changed, 516 insertions(+), 27 deletions(-) diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index d483b4d7f57..0c11576ff89 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -914,7 +914,7 @@ data v1_claim_scoped_witness_dissolve_on: List = [ ScheduleWitnessEntry { @@ -944,7 +944,7 @@ data v1_claim_scoped_witness_entries: List = [ }, ] -data v1_claim_scoped_witness_batch_note: String = "This is one INSTANCE of std.realization_schedule ScopedWitnessBatch, not a parser branch in the floor mechanism. The four file-grain rows expand through ScheduleWitnessEntry's empty-function authority, so adding or renaming a test fn changes no roster. Their dag plus src/v1 source-root envelope admits the v1 compiler closure without widening witness_layer_roots for unrelated witnesses. SelectionApplied is deliberate: normal affected-set selection avoids paying the measured closure materialization on unrelated PRs; every unselected roster row still emits an exact-head ScopedWitnessSelectionSkipped receipt with provenance, while a provenance failure refuses loudly and never widens. The executor's own module universe is a distinct fact carried by ScopedWitnessBatch.execution_authority as InheritedWalkSourceRoots: the worker resolves affected_set_floor_runner, witness_entry_eligibility_census, and post-discovery cost/attribution projectors from the enclosing walk's roots while the witness subject index remains exactly dag plus src/v1. Adding src/v2 to this batch's witness roots was considered and refused because it widens the subject envelope, moves the receipt digest, and invalidates the measured clamp basis; executor-authority dependencies never enter the witness roots as an absorbing fallback. The profile declares a substantial whole-tree resolve, Hermetic effects, a batch-owned 480-second clamp, and SequentialChildProcess isolation. RECEIPTED RAISE (2026-08-08, PR #7924 CI run 31223532865 @ 93b1373751): scoped child FLOOR-BATCH-OVER-BUDGET wall_ms=375553 clamp_ms=360000 units=27 — reproduced locally on the same commit after merge with main. Prior 360s basis (199.393s arm64 x 1.8 = 358.9s) is stale: post-merge scoped-worker stage wall is ~376s on x86_local with the full executor-authority projector path. Sizing follows gunbc.ci_spec gunbc_ci_floor_batch_clamp_note fleet-margin policy (measured worst wall x 1.2, not host roulette): 375.553s x 1.2 = 451s, rounded up to 480s whole-minute grain (+33% over the retired 360s row). THE ENROLLMENT THAT GREW THE BATCH: none — wall is closure-materialization dominated, not a roster edit. The earlier 180-second basis measured only 96 seconds before the cost projector and renderers were reachable from the narrow scoped envelope, so it no longer described the executing batch. COST DISPOSITION: the approximately 103-second increase correlated with making the cost projector, histogram, and slowest-attribution renderer reachable while witness row evaluations themselves remain negligible per-row; that reporting/closure cost has not been decomposed in this scoped-scheduling change and is tracked by the real ROADMAP module-grain-materialization lane. Its trigger is a per-projector resolve/materialization attribution showing whether the three projections recompute identical semantic facts, followed by cached-vs-cold receipts before any optimization claim. The larger clamp must not normalize that open cost question into proportionality. per_unit_ms remains zero because row evaluation is negligible; this catches closure growth and deliberately does not price row-count growth until a file brings a distinct closure. Exact-head run 30713632253 proves SharedWalkProcess cannot satisfy this instance: ordinary discovery completed at 7.113GB RSS, then the floor vanished while materializing this second root closure before a batch-start line. The kernel cause is unclassified, but additive same-process residency is established. SequentialChildProcess makes the ordinary worker exit before this worker starts, releasing the first live set without claiming the stronger fresh-cgroup semantics of FreshJobProcess. v1_claim_scoped_witness_dissolve_on fires when the v2 parser owns these claims." +data v1_claim_scoped_witness_batch_note: String = "This is one INSTANCE of std.realization_schedule ScopedWitnessBatch, not a parser branch in the floor mechanism. The four file-grain rows expand through ScheduleWitnessEntry's empty-function authority, so adding or renaming a test fn changes no roster. Their dag plus src/v1 source-root envelope admits the v1 compiler closure without widening witness_layer_roots for unrelated witnesses. SelectionApplied is deliberate; every unselected roster row still emits an exact-head ScopedWitnessSelectionSkipped receipt with provenance, while a provenance failure refuses loudly and never widens. CORRECTED 2026-08-11 (session lively-bat-548): this sentence previously claimed that normal affected-set selection avoided paying the measured closure materialization on unrelated PRs. It did not, and could not have. None of the five entries declared a live_tree_disposition row, undeclared fail-closes to ReadsLiveTree, and a ReadsLiveTree row can never predict-skip, so the declared SelectionApplied was INERT and all 31 expanded rows ran on every pull request. The derived axis was not what forced it: all five closures carry zero path-like data rows and zero host-effect sinks. Two things had to change before the claim became true. The entries now declare SubstrateInputsOnly, which required moving the LiveTreeDisposition carrier under dag/ because the scoped subject universe excludes src/v2 and the annotation was otherwise a hard UnresolvedType. And selection alone would still not have saved the wall, because it runs INSIDE the child after process_shared_index has already materialized the dag plus src/v1 world: the saving comes from gunbc.scoped_floor_execution, which decides admission BEFORE the ordinary worker projects this batch id into the scoped manifest, so an unaffected diff spawns no child at all. The executor's own module universe is a distinct fact carried by ScopedWitnessBatch.execution_authority as InheritedWalkSourceRoots: the worker resolves affected_set_floor_runner, witness_entry_eligibility_census, and post-discovery cost/attribution projectors from the enclosing walk's roots while the witness subject index remains exactly dag plus src/v1. Adding src/v2 to this batch's witness roots was considered and refused because it widens the subject envelope, moves the receipt digest, and invalidates the measured clamp basis; executor-authority dependencies never enter the witness roots as an absorbing fallback. The profile declares a substantial whole-tree resolve, Hermetic effects, a batch-owned 480-second clamp, and SequentialChildProcess isolation. RECEIPTED RAISE (2026-08-08, PR #7924 CI run 31223532865 @ 93b1373751): scoped child FLOOR-BATCH-OVER-BUDGET wall_ms=375553 clamp_ms=360000 units=27 — reproduced locally on the same commit after merge with main. Prior 360s basis (199.393s arm64 x 1.8 = 358.9s) is stale: post-merge scoped-worker stage wall is ~376s on x86_local with the full executor-authority projector path. Sizing follows gunbc.ci_spec gunbc_ci_floor_batch_clamp_note fleet-margin policy (measured worst wall x 1.2, not host roulette): 375.553s x 1.2 = 451s, rounded up to 480s whole-minute grain (+33% over the retired 360s row). THE ENROLLMENT THAT GREW THE BATCH: none — wall is closure-materialization dominated, not a roster edit. The earlier 180-second basis measured only 96 seconds before the cost projector and renderers were reachable from the narrow scoped envelope, so it no longer described the executing batch. COST DISPOSITION: the approximately 103-second increase correlated with making the cost projector, histogram, and slowest-attribution renderer reachable while witness row evaluations themselves remain negligible per-row; that reporting/closure cost has not been decomposed in this scoped-scheduling change and is tracked by the real ROADMAP module-grain-materialization lane. Its trigger is a per-projector resolve/materialization attribution showing whether the three projections recompute identical semantic facts, followed by cached-vs-cold receipts before any optimization claim. The larger clamp must not normalize that open cost question into proportionality. per_unit_ms remains zero because row evaluation is negligible; this catches closure growth and deliberately does not price row-count growth until a file brings a distinct closure. Exact-head run 30713632253 proves SharedWalkProcess cannot satisfy this instance: ordinary discovery completed at 7.113GB RSS, then the floor vanished while materializing this second root closure before a batch-start line. The kernel cause is unclassified, but additive same-process residency is established. SequentialChildProcess makes the ordinary worker exit before this worker starts, releasing the first live set without claiming the stronger fresh-cgroup semantics of FreshJobProcess. v1_claim_scoped_witness_dissolve_on fires when the v2 parser owns these claims." data v1_claim_scoped_witness_batch: ScopedWitnessBatch = scoped_witness_batch( batch_id: "v1-claim-scoped-witnesses" as ScopedWitnessBatchId, diff --git a/dag/gunbc/scoped_floor_execution.dag b/dag/gunbc/scoped_floor_execution.dag index 505145db4ab..66c3f97bf73 100644 --- a/dag/gunbc/scoped_floor_execution.dag +++ b/dag/gunbc/scoped_floor_execution.dag @@ -118,6 +118,32 @@ fn scoped_affected_standing_live( } } +// THE COLD BACKSTOP, and why it is an axis rather than a caller's choice. Once +// the admission below can skip, the five entries' 31 test functions have no +// unconditional execution route left, and an affected-set prediction that is +// never independently falsified is a claim with no control. A pull request asks +// "is this change relevant to the scoped world"; every other event asks "does +// the scoped world still hold", and the second question has no diff to narrow +// by. The policy is therefore stated positively over the ONE event that +// predicts, so an event string the harness could not supply - or one nobody has +// modelled yet - executes the full roster instead of inheriting a skip it was +// never tested under. The same verdict turns node frontier selection OFF inside +// the child, because admitting the batch while leaving selection applied would +// re-derive the same prediction one layer down and back-stop nothing. +type ScopedExecutionPolicy + = ScopedPolicyPredictsFromDiff + | ScopedPolicyRequiresFullExecution { reason: String } + +fn scoped_execution_policy_for_event(event: String) -> ScopedExecutionPolicy { + if event == "pull_request" { + ScopedPolicyPredictsFromDiff + } else { + ScopedPolicyRequiresFullExecution { + reason: "event is not pull_request; the scoped roster executes cold as the affected-set prediction's control" + } + } +} + // A departed path is a deletion, rename, or copy. Its pre-image is not in the // head tree, so a head-only closure cannot decide whether it was a dependency: // the file whose absence matters is exactly the file the closure can no longer @@ -129,16 +155,79 @@ fn scoped_departure_forces_run(departed_paths: List) -> Bool { length(xs: departed_paths) > 0 } -// The decision - a pure fold over already-observed standings. Refusals come -// first and are exhaustive over the four ignorance axes; only inside a fully -// observed, non-contradicted world does the positive-evidence ladder run, and -// its fall-through is the skip. The diff's changed paths are not re-read here -// because the affected standing already answered the question they exist to ask; -// an empty diff therefore reaches SkipAssumedGreen through ScopedEntriesUnaffected -// rather than through a special case, matching floor_witness_run_disposition. +// HOST TRANSPORT. The seed observes bytes and git; it does not decide. This +// adapter exists so the host can hand over what it observed without constructing +// coproduct values across the interpreter boundary, and its flattened Bool-plus- +// reason parameters are a WIRE SHAPE, not the model: the standings are rebuilt +// here, immediately, and every arm below reads the coproducts. Keeping the +// flattening at this one seam is what stops it from spreading into the decision, +// where a Bool beside a reason string would be the state-space conflation the +// standings exist to prevent. +fn scoped_witness_run_disposition_from_host( + event: String, + subject_matched: Bool, + subject_mismatch_reason: String, + disposition_agrees: Bool, + disposition_conflict_reason: String, + diff_observed: Bool, + diff_failure_reason: String, + changed_paths: List, + departed_paths: List, + entries: List, + pool_roots: List +) -> WitnessRunDisposition { + let subject = if subject_matched { + ScopedSubjectMatched + } else { + ScopedSubjectMismatched { reason: subject_mismatch_reason } + } + let disposition = if disposition_agrees { + ScopedDispositionAgrees + } else { + ScopedDispositionContradicted { reason: disposition_conflict_reason } + } + let diff = if diff_observed { + DiffPathsProduced { changed_paths: changed_paths } + } else { + DiffObservationFailClosed { reason: diff_failure_reason } + } + // The live projection is evaluated even on a backstop event, where the + // decision below will not read it. That is deliberate: the alternative is to + // hand the fold a fabricated ScopedEntriesAffected the closure never + // produced, which is the fabricated-plausible-output failure aimed at the one + // input a reader would take for evidence. One corpus scan inside a job that + // is about to spend 376 seconds is the honest price. + scoped_witness_run_disposition( + subject: subject, + disposition: disposition, + policy: scoped_execution_policy_for_event(event: event), + diff: diff, + departed_paths: departed_paths, + affected: scoped_affected_standing_live( + entries: entries, + pool_roots: pool_roots, + touched_paths: changed_paths + ) + ) +} + +// The decision - a pure fold over already-observed standings. The two axes that +// are facts ABOUT THE OBSERVATIONS THEMSELVES come first: a subject mismatch +// means the standings describe different trees, and a contradicted disposition +// means the authority admitting the work is broken - both are defects on every +// event, so neither is reachable past the policy. The policy arm sits next and +// runs unconditionally; it is not a failure arm widening to a superset but a +// declared statement that this event class has no diff to narrow by. Only +// inside a predicting event do the remaining ignorance axes refuse and the +// positive-evidence ladder run, with the skip as its fall-through. The diff's +// changed paths are not re-read below because the affected standing already +// answered the question they exist to ask; an empty diff therefore reaches +// SkipAssumedGreen through ScopedEntriesUnaffected rather than through a +// special case, matching floor_witness_run_disposition. fn scoped_witness_run_disposition( subject: ScopedSubjectStanding, disposition: ScopedDispositionStanding, + policy: ScopedExecutionPolicy, diff: FloorDiffObservation, departed_paths: List, affected: ScopedAffectedStanding @@ -151,20 +240,25 @@ fn scoped_witness_run_disposition( ScopedDispositionContradicted { reason: reason } => Refused { cause: DispositionAuthorityRefusal { reason: reason } } ScopedDispositionAgrees => - match diff { - DiffObservationFailClosed { reason: reason } => - Refused { cause: DiffObservationRefusal { reason: reason } } - DiffPathsProduced { changed_paths: _ } => - match affected { - ScopedAffectedUndecidable { reason: reason } => - Refused { cause: DependencyObservationRefusal { reason: reason } } - ScopedEntriesAffected => - RunWitness { reason: "scoped entry dependency closure intersects a changed path" } - ScopedEntriesUnaffected => - if scoped_departure_forces_run(departed_paths: departed_paths) { - RunWitness { reason: "scoped diff reports a departed path; head-only closure cannot bound it" } - } else { - SkipAssumedGreen + match policy { + ScopedPolicyRequiresFullExecution { reason: reason } => + RunWitness { reason: reason } + ScopedPolicyPredictsFromDiff => + match diff { + DiffObservationFailClosed { reason: reason } => + Refused { cause: DiffObservationRefusal { reason: reason } } + DiffPathsProduced { changed_paths: _ } => + match affected { + ScopedAffectedUndecidable { reason: reason } => + Refused { cause: DependencyObservationRefusal { reason: reason } } + ScopedEntriesAffected => + RunWitness { reason: "scoped entry dependency closure intersects a changed path" } + ScopedEntriesUnaffected => + if scoped_departure_forces_run(departed_paths: departed_paths) { + RunWitness { reason: "scoped diff reports a departed path; head-only closure cannot bound it" } + } else { + SkipAssumedGreen + } } } } diff --git a/dag/test/claim/scoped_floor_execution_witness_test.dag b/dag/test/claim/scoped_floor_execution_witness_test.dag index 169c349ca12..64474cc5dc3 100644 --- a/dag/test/claim/scoped_floor_execution_witness_test.dag +++ b/dag/test/claim/scoped_floor_execution_witness_test.dag @@ -26,9 +26,13 @@ import gunbc.scoped_floor_execution { ScopedDispositionContradicted, ScopedEntriesAffected, ScopedEntriesUnaffected, + ScopedExecutionPolicy, + ScopedPolicyPredictsFromDiff, + ScopedPolicyRequiresFullExecution, ScopedSubjectStanding, ScopedSubjectMatched, ScopedSubjectMismatched, + scoped_execution_policy_for_event, scoped_witness_run_disposition } @@ -48,6 +52,9 @@ data empty_diff: FloorDiffObservation = DiffPathsProduced { changed_paths: [] } +// Every case below that is not ABOUT the policy holds it at +// ScopedPolicyPredictsFromDiff, because a case that back-stopped would run for +// a reason unrelated to what it claims to discriminate. fn decide( subject: ScopedSubjectStanding, disposition: ScopedDispositionStanding, @@ -58,12 +65,36 @@ fn decide( scoped_witness_run_disposition( subject: subject, disposition: disposition, + policy: ScopedPolicyPredictsFromDiff, diff: diff, departed_paths: departed_paths, affected: affected ) } +fn decide_under_policy( + policy: ScopedExecutionPolicy, + disposition: ScopedDispositionStanding, + diff: FloorDiffObservation, + affected: ScopedAffectedStanding +) -> WitnessRunDisposition { + scoped_witness_run_disposition( + subject: ScopedSubjectMatched, + disposition: disposition, + policy: policy, + diff: diff, + departed_paths: [], + affected: affected + ) +} + +fn policy_is_full_execution(policy: ScopedExecutionPolicy) -> Bool { + match policy { + ScopedPolicyRequiresFullExecution { reason: _ } => true + ScopedPolicyPredictsFromDiff => false + } +} + fn is_skip(d: WitnessRunDisposition) -> Bool { match d { SkipAssumedGreen => true @@ -224,3 +255,63 @@ test fn red_subject_mismatch_refuses_before_any_affected_reading() -> Bool { SkipAssumedGreen => false } } + +// The backstop's whole purpose: an event with nothing to run - unrelated diff, +// unaffected closure, no departures - still executes the roster. Without this +// the 31 scoped test functions would have no unconditional execution route once +// the admission above can skip. +test fn w_non_pull_request_event_executes_despite_an_unaffected_closure() -> Bool { + is_run(d: decide_under_policy( + policy: scoped_execution_policy_for_event(event: "push"), + disposition: ScopedDispositionAgrees, + diff: unrelated_diff, + affected: ScopedEntriesUnaffected + )) +} + +// The backstop must not be reachable from the event the prediction is FOR - +// otherwise it would fire on every pull request and the change would save +// nothing. This is the discriminating half of the pair above. +test fn w_pull_request_event_predicts_and_therefore_skips() -> Bool { + is_skip(d: decide_under_policy( + policy: scoped_execution_policy_for_event(event: "pull_request"), + disposition: ScopedDispositionAgrees, + diff: unrelated_diff, + affected: ScopedEntriesUnaffected + )) +} + +// An event string the harness could not supply is not a pull request, so it +// executes. A default that predicted would be an untested skip. +test fn w_unsupplied_event_executes_rather_than_predicting() -> Bool { + policy_is_full_execution(policy: scoped_execution_policy_for_event(event: "")) +} + +test fn w_unmodelled_event_executes_rather_than_predicting() -> Bool { + policy_is_full_execution(policy: scoped_execution_policy_for_event(event: "workflow_dispatch")) +} + +// RED - the backstop is a policy, not an amnesty. A contradicted disposition is +// a broken authority on every event, so it must still refuse on the cold lane +// where the batch would otherwise run anyway. If the policy arm sat ahead of the +// disposition axis, a stale declaration would be repaired by nobody because main +// would stay green. +test fn red_backstop_event_still_refuses_a_contradicted_disposition() -> Bool { + match decide_under_policy( + policy: scoped_execution_policy_for_event(event: "push"), + disposition: ScopedDispositionContradicted { reason: "entry declares SubstrateInputsOnly but derived closure reaches a host-effect sink" }, + diff: unrelated_diff, + affected: ScopedEntriesUnaffected + ) { + Refused { cause: cause } => + match cause { + DispositionAuthorityRefusal { reason: _ } => true + DiffObservationRefusal { reason: _ } => false + FrontierQueryRefusal { reason: _ } => false + SubjectObservationRefusal { reason: _ } => false + DependencyObservationRefusal { reason: _ } => false + } + RunWitness { reason: _ } => false + SkipAssumedGreen => false + } +} diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 6dbad8ae39c..c62fe87010b 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -9612,6 +9612,248 @@ fn write_floor_worker_terminal(outcome: &str, detail: &str) -> Result<(), String fs::rename(&tmp, &path).map_err(|e| format!("publish worker terminal {}: {e}", path.display())) } +const SCOPED_ADMISSION_ENTRY: &str = "dag/gunbc/scoped_floor_execution.dag"; + +/// Render the `.dag` verdict into (journal state, detail). A `Refused` arm is an +/// `Err`: "I could not decide" and "nothing is affected" project onto the same +/// zero manifest ids, so they must not share a success arm — an empty manifest is +/// evidence of a skip only when a `SkipAssumedGreen` was actually observed. +fn scoped_admission_projection( + ctx: &InterpContext, + verdict: &Value, + batch_id: &str, +) -> Result<(&'static str, String), String> { + let reason_of = |fields: &_| -> String { + match ctx.field(fields, "reason") { + Some(Value::Str(s)) => s.clone(), + _ => String::new(), + } + }; + match verdict { + Value::Variant { + variant_name, + fields, + .. + } if ctx.sym_eq(*variant_name, "RunWitness") => { + Ok(("run", format!("reason={}", reason_of(fields)))) + } + Value::Variant { variant_name, .. } if ctx.sym_eq(*variant_name, "SkipAssumedGreen") => Ok(( + "skip", + "reason=scoped entry dependency closure unaffected by the observed diff".to_string(), + )), + Value::Variant { + variant_name, + fields, + .. + } if ctx.sym_eq(*variant_name, "Refused") => { + // Named exhaustively rather than rendered: only `sym_eq` is public, and an + // unrecognised cause must be an error, not an unlabelled refusal. A refusal + // whose class the operator cannot read sends them round the loop to find it. + let cause = match ctx.field(fields, "cause") { + Some(Value::Variant { + variant_name: cause_name, + fields: cause_fields, + .. + }) => { + let label = [ + "DiffObservationRefusal", + "FrontierQueryRefusal", + "SubjectObservationRefusal", + "DependencyObservationRefusal", + "DispositionAuthorityRefusal", + ] + .into_iter() + .find(|name| ctx.sym_eq(*cause_name, name)) + .ok_or_else(|| { + format!( + "scoped admission refusal carries an unmodelled WitnessRefusalCause \ + for batch {batch_id}" + ) + })?; + format!("{label} detail={}", reason_of(cause_fields)) + } + _ => { + return Err(format!( + "scoped admission Refused for batch {batch_id} carries no `cause` field" + )) + } + }; + Err(format!( + "SCOPED-ADMISSION-REFUSED batch={batch_id} cause={cause} — the scoped batch \ + is neither run nor skipped on unobserved evidence" + )) + } + other => Err(format!( + "scoped_witness_run_disposition_from_host returned `{}`, expected WitnessRunDisposition", + ctx.format_value(other) + )), + } +} + +/// The cold-lane control, read from `gunbc.scoped_floor_execution` +/// `scoped_execution_policy_for_event`: on any event other than `pull_request` the +/// scoped roster executes in full, so node-frontier selection is turned OFF inside +/// the child. Admitting the batch while leaving selection applied would re-derive +/// the same prediction one layer down and back-stop nothing — the 31 scoped test +/// functions would still be gated by the affected-set answer whose control this is. +/// +/// The failure arms EXECUTE rather than predict, and that direction is the point: +/// on the one lane whose job is to falsify skips, an unresolvable policy that +/// skipped would be a silent hole in the control itself. +fn scoped_backstop_requires_full_execution(walk_source_roots: &[String]) -> bool { + let event = std::env::var("GITHUB_EVENT_NAME").unwrap_or_default(); + let (graph, indices) = + match resolve_entry_graph_shared(walk_source_roots, SCOPED_ADMISSION_ENTRY) { + Ok(pair) => pair, + Err(e) => { + eprintln!( + "claim_executor: scoped backstop policy unresolvable ({e}); \ + executing the full scoped roster" + ); + return true; + } + }; + let ctx = make_eval_context(&graph, indices, ExecutionMode::Hermetic); + match run_in_context_with_args( + &ctx, + "scoped_execution_policy_for_event", + &[(Some("event".to_string()), Value::Str(event))], + false, + ) { + Ok(Value::Variant { variant_name, .. }) => { + if ctx.sym_eq(variant_name, "ScopedPolicyPredictsFromDiff") { + false + } else if ctx.sym_eq(variant_name, "ScopedPolicyRequiresFullExecution") { + true + } else { + eprintln!( + "claim_executor: unmodelled ScopedExecutionPolicy variant; \ + executing the full scoped roster" + ); + true + } + } + Ok(other) => { + eprintln!( + "claim_executor: scoped_execution_policy_for_event returned `{}`; \ + executing the full scoped roster", + ctx.format_value(&other) + ); + true + } + Err(msg) => { + eprintln!( + "claim_executor: scoped_execution_policy_for_event unavailable ({msg}); \ + executing the full scoped roster" + ); + true + } + } +} + +/// Pre-construction admission for scoped witness batches. +/// +/// A scoped batch materializes a SECOND semantic world (its own `source_roots`, +/// today dag plus src/v1) inside a child process the coordinator spawns from the +/// manifest this feeds. Before this gate the manifest was projected +/// unconditionally, so every pull request paid that world; the batch's declared +/// `SelectionApplied` could not help, because its entries were undeclared and +/// therefore fail-closed `ReadsLiveTree`, which can never predict-skip. +/// +/// The seed observes; `gunbc.scoped_floor_execution` decides. Exactly three +/// observations cross the boundary — the comparison readout that says which tree +/// the diff describes, the Wet name-status diff itself, and the declared-versus- +/// derived disposition standing of the batch's own roster — and the `.dag` fold +/// returns the ordinary `WitnessRunDisposition`. +fn scoped_batch_admitted_ids( + candidates: &[(String, Vec, Vec)], + walk_source_roots: &[String], +) -> Result, String> { + if candidates.is_empty() { + return Ok(Vec::new()); + } + let (subject_matched, subject_mismatch_reason) = + match v1_compiler::cli_run::floor_diff_comparison_readout() { + Ok(_) => (true, String::new()), + Err(msg) => (false, msg), + }; + let (diff_observed, changed_paths, departed_paths, diff_failure_reason) = + match v1_compiler::cli_run::floor_git_diff_name_status_range() { + Ok((changed, departed)) => { + let mut departed: Vec = departed.into_iter().collect(); + departed.sort(); + (true, changed, departed, String::new()) + } + Err(msg) => (false, Vec::new(), Vec::new(), msg), + }; + let (graph, indices) = resolve_entry_graph_shared(walk_source_roots, SCOPED_ADMISSION_ENTRY) + .map_err(|e| format!("scoped admission resolve ({SCOPED_ADMISSION_ENTRY}): {e}"))?; + let ctx = make_eval_context(&graph, indices, ExecutionMode::Wet); + let mut admitted = Vec::new(); + for (batch_id, pool_roots, entries) in candidates { + let conflict = + v1_compiler::cli_run::entry_roster_disposition_conflict(entries, pool_roots)?; + let args = [ + ( + Some("event".to_string()), + Value::Str(std::env::var("GITHUB_EVENT_NAME").unwrap_or_default()), + ), + ( + Some("subject_matched".to_string()), + Value::Bool(subject_matched), + ), + ( + Some("subject_mismatch_reason".to_string()), + Value::Str(subject_mismatch_reason.clone()), + ), + ( + Some("disposition_agrees".to_string()), + Value::Bool(conflict.is_none()), + ), + ( + Some("disposition_conflict_reason".to_string()), + Value::Str(conflict.unwrap_or_default()), + ), + ( + Some("diff_observed".to_string()), + Value::Bool(diff_observed), + ), + ( + Some("diff_failure_reason".to_string()), + Value::Str(diff_failure_reason.clone()), + ), + ( + Some("changed_paths".to_string()), + str_list_value(&changed_paths), + ), + ( + Some("departed_paths".to_string()), + str_list_value(&departed_paths), + ), + (Some("entries".to_string()), str_list_value(entries)), + (Some("pool_roots".to_string()), str_list_value(pool_roots)), + ]; + let verdict = run_in_context_with_args( + &ctx, + "scoped_witness_run_disposition_from_host", + &args, + false, + ) + .map_err(|e| format!("scoped_witness_run_disposition_from_host ({batch_id}): {e}"))?; + let (state, detail) = scoped_admission_projection(&ctx, &verdict, batch_id)?; + append_floor_phase_journal( + "scoped-admission", + state, + &format!("batch={batch_id} {detail}"), + ); + eprintln!("[scoped-admission] batch={batch_id} disposition={state} {detail}"); + if state == "run" { + admitted.push(batch_id.clone()); + } + } + Ok(admitted) +} + fn write_scoped_witness_batch_manifest(batch_ids: &[String]) -> Result<(), String> { let path = Path::new(SCOPED_WITNESS_BATCH_MANIFEST_PATH); if let Some(parent) = path.parent() { @@ -10398,20 +10640,36 @@ fn run() -> Result { let plan_declared_no_finalization = floor_finalization.is_none(); match floor_worker_role.as_ref() { Some(FloorWorkerRole::Ordinary) => { - let child_batch_ids: Vec = batches + let scoped_candidates: Vec<(String, Vec, Vec)> = batches .iter() .flatten() .filter_map(|runnable| match runnable { Runnable::ScopedWitnessBatch { batch_id, + source_roots, + entries, process_isolation: ScopedProcessIsolation::SequentialChildProcess | ScopedProcessIsolation::FreshJobProcess, .. - } => Some(batch_id.clone()), + } => { + let mut entry_paths: Vec = + entries.iter().map(|row| row.entry.clone()).collect(); + entry_paths.sort(); + entry_paths.dedup(); + Some((batch_id.clone(), source_roots.clone(), entry_paths)) + } _ => None, }) .collect(); + let child_batch_ids = match scoped_batch_admitted_ids(&scoped_candidates, &source_roots) + { + Ok(ids) => ids, + Err(msg) => { + eprintln!("claim_executor: scoped admission refusal: {msg}"); + return Err(ExitCode::from(1)); + } + }; if let Err(msg) = write_scoped_witness_batch_manifest(&child_batch_ids) { eprintln!("claim_executor: ordinary floor worker manifest refusal: {msg}"); return Err(ExitCode::from(1)); @@ -10451,6 +10709,20 @@ fn run() -> Result { ); return Err(ExitCode::from(1)); } + if scoped_backstop_requires_full_execution(&source_roots) { + if let Runnable::ScopedWitnessBatch { + node_frontier_selection, + .. + } = &mut selected[0] + { + *node_frontier_selection = NodeFrontierSelectionMode::Off; + eprintln!( + "claim_executor: SCOPED-BACKSTOP batch={batch_id} \ + node_frontier_selection=Off — the full scoped roster executes as the \ + affected-set prediction's control" + ); + } + } batches = vec![selected]; on_success_stages.clear(); floor_finalization = None; diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 7c48d38b930..bda3bdcf93a 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -21409,7 +21409,7 @@ fn floor_git_diff_range() -> Result { /// answers "which ref" for a diagnostic, and a DECIDING consumer that takes it has to invent the /// missing head and relation. Inventing them is what shipped the merge-base-on-every-arm fail-open, /// so the deciding consumers read this one and a `ComparisonReadoutRefused` propagates. -pub(crate) fn floor_diff_comparison_readout() -> Result { +pub fn floor_diff_comparison_readout() -> Result { use v1_interpreter::Value; let roots = default_source_roots(); let entry = "src/v2/workflow/floor_diff_observe.dag"; @@ -21543,7 +21543,7 @@ fn string_list_from_value(val: &v1_interpreter::Value, field: &str) -> Result Result<(Vec, HashSet), String> { +pub fn floor_git_diff_name_status_range() -> Result<(Vec, HashSet), String> { use v1_interpreter::Value; let roots = default_source_roots(); let entry = "src/v2/workflow/floor_diff_observe.dag"; @@ -22272,6 +22272,38 @@ fn parse_entry_live_tree_disposition(entry: &str, content: &str) -> Result Result, String> { + let facts = build_module_graph_facts_live(pool_roots); + for entry in entries { + let declared_live = read_entry_live_tree_disposition(entry)?; + if declared_live { + continue; + } + if effect_reach_derived_reads_live_tree_for_entry(entry, &facts) { + return Ok(Some(format!( + "entry {entry} declares SubstrateInputsOnly but its derived effect reach \ + finds a path-like data row and a host-effect sink in its closure" + ))); + } + } + Ok(None) +} + fn read_entry_live_tree_disposition(entry: &str) -> Result { let content = std::fs::read_to_string(entry).map_err(|e| { format!( From a9f91654dfb725a262e3d356f49e803f533eef7e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 06:47:44 +0000 Subject: [PATCH 5/9] The backstop's failure arms refuse instead of widening MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit scoped_backstop_requires_full_execution answered "run the full roster" on every failure — unresolvable entry, non-variant return, unmodelled variant, eval error. Operationally that is safe, which is exactly what makes it the absorbing fallback wearing this seam's own name: a widened cold run is byte-for-byte indistinguishable from a normal cold run, so the frequency of "the policy authority could not be reached" is zero by construction and the deficit never ranks for fixing. The arms now return Err and the worker exits 1 with SCOPED-BACKSTOP-REFUSED. The two modelled variants are the only answers. Co-Authored-By: Claude Opus 5 (1M context) --- src/v1/stage0/src/bin/claim_executor.rs | 71 +++++++++++-------------- 1 file changed, 32 insertions(+), 39 deletions(-) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index c62fe87010b..b4029720998 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -9697,57 +9697,43 @@ fn scoped_admission_projection( /// the same prediction one layer down and back-stop nothing — the 31 scoped test /// functions would still be gated by the affected-set answer whose control this is. /// -/// The failure arms EXECUTE rather than predict, and that direction is the point: -/// on the one lane whose job is to falsify skips, an unresolvable policy that -/// skipped would be a silent hole in the control itself. -fn scoped_backstop_requires_full_execution(walk_source_roots: &[String]) -> bool { +/// Every failure arm REFUSES; none widens to "run everything". Widening here is +/// the absorbing fallback wearing this seam's own name: the safe-looking arm is +/// indistinguishable from a normal cold run, so the frequency of "the policy +/// authority could not be reached" would be zero by construction and the deficit +/// would never rank for fixing. The line stops instead, typed and located. +fn scoped_backstop_requires_full_execution(walk_source_roots: &[String]) -> Result { let event = std::env::var("GITHUB_EVENT_NAME").unwrap_or_default(); - let (graph, indices) = - match resolve_entry_graph_shared(walk_source_roots, SCOPED_ADMISSION_ENTRY) { - Ok(pair) => pair, - Err(e) => { - eprintln!( - "claim_executor: scoped backstop policy unresolvable ({e}); \ - executing the full scoped roster" - ); - return true; - } - }; + let (graph, indices) = resolve_entry_graph_shared(walk_source_roots, SCOPED_ADMISSION_ENTRY) + .map_err(|e| { + format!("scoped backstop policy unresolvable ({SCOPED_ADMISSION_ENTRY}): {e}") + })?; let ctx = make_eval_context(&graph, indices, ExecutionMode::Hermetic); match run_in_context_with_args( &ctx, "scoped_execution_policy_for_event", - &[(Some("event".to_string()), Value::Str(event))], + &[(Some("event".to_string()), Value::Str(event.clone()))], false, ) { Ok(Value::Variant { variant_name, .. }) => { if ctx.sym_eq(variant_name, "ScopedPolicyPredictsFromDiff") { - false + Ok(false) } else if ctx.sym_eq(variant_name, "ScopedPolicyRequiresFullExecution") { - true + Ok(true) } else { - eprintln!( - "claim_executor: unmodelled ScopedExecutionPolicy variant; \ - executing the full scoped roster" - ); - true + Err(format!( + "scoped_execution_policy_for_event returned an unmodelled \ + ScopedExecutionPolicy variant for event `{event}`" + )) } } - Ok(other) => { - eprintln!( - "claim_executor: scoped_execution_policy_for_event returned `{}`; \ - executing the full scoped roster", - ctx.format_value(&other) - ); - true - } - Err(msg) => { - eprintln!( - "claim_executor: scoped_execution_policy_for_event unavailable ({msg}); \ - executing the full scoped roster" - ); - true - } + Ok(other) => Err(format!( + "scoped_execution_policy_for_event returned `{}`, expected ScopedExecutionPolicy", + ctx.format_value(&other) + )), + Err(msg) => Err(format!( + "scoped_execution_policy_for_event unavailable for event `{event}`: {msg}" + )), } } @@ -10709,7 +10695,14 @@ fn run() -> Result { ); return Err(ExitCode::from(1)); } - if scoped_backstop_requires_full_execution(&source_roots) { + let backstop = match scoped_backstop_requires_full_execution(&source_roots) { + Ok(b) => b, + Err(msg) => { + eprintln!("claim_executor: SCOPED-BACKSTOP-REFUSED batch={batch_id}: {msg}"); + return Err(ExitCode::from(1)); + } + }; + if backstop { if let Runnable::ScopedWitnessBatch { node_frontier_selection, .. From 8f56fdd57262d14a192f0fa8c87b557a88a95531 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 07:02:53 +0000 Subject: [PATCH 6/9] =?UTF-8?q?Take=20the=20heal's=20ci.yml=20regeneration?= =?UTF-8?q?=20=E2=80=94=20the=20workflow=20credential=20cannot?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `heal_generated_artifacts` regenerated `.github/workflows/ci.yml` at a9f91654dfb and then refused to push it: workflow paths are author-commit-required (`cause=ActionsJobCredentialScopeUnavailable`), so it uploaded the repair as an artifact instead. This is that artifact, taken whole. The drift is exactly one token, and it is derived rather than authored: moving `live_tree.dag` under `dag/` put `v2.std.live_tree` inside the stage0 emit closure, so the generated-artifact exclusion list the heal's own conflict check reads gained `':(exclude)src/v1/stage0/src/v2_std_live_tree.rs'`. One hunk, one added list element, verified token-by-token against the committed file. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f1e9e889e4d..abc4d2fbe52 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -402,7 +402,7 @@ jobs: git config user.email gunbc-ci-auto-heal@users.noreply.github.com if ! git merge --no-edit "$BUILT_FROM"; then CONFLICTS="$(git diff --name-only --diff-filter=U)" - AUTHORED_CONFLICTS="$(git diff --name-only --diff-filter=U -- . ':(exclude).github/workflows/ci.yml' ':(exclude).github/workflows/falsifier.yml' ':(exclude).gitignore' ':(exclude).gitattributes' ':(exclude)ROADMAP.md' ':(exclude)DESIGN.md' ':(exclude).githooks/pre-push' ':(exclude).githooks/pre-commit' ':(exclude).githooks/generated-artifact-merge' ':(exclude)dag/gunbc/stage0_crate_layout_generated.dag' ':(exclude)src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs' ':(exclude)dag/gunbc/stage0_crate_partition_generated.dag' ':(exclude)dag/gunbc/stage0_emit_plan_generated.dag' ':(exclude)src/v1/stage0/src/v1_interpreter_dispatch_generated.rs' ':(exclude)docs/plans/idea-machine.md' ':(exclude)docs/plans/algebraic-rewrite-optimization.md' ':(exclude)docs/plans/dag-v2-defork-audit.md' ':(exclude)docs/plans/v2-self-hosting.md' ':(exclude)docs/plans/m5-fixture-store-consolidation.md' ':(exclude)docs/plans/model-realization-fork.md' ':(exclude)docs/plans/value-null-split.md' ':(exclude)docs/plans/ci-merge-freshness.md' ':(exclude)docs/plans/seed-debt-bundle-item-2.md' ':(exclude)docs/plans/axiom-syllogism-lens.md' ':(exclude)docs/plans/invert-hand-maintained.md' ':(exclude)docs/plans/fail-closed-lockdown.md' ':(exclude)docs/plans/format-model-reconciliation.md' ':(exclude)docs/plans/regime2-shared-emission-fold.md' ':(exclude)docs/plans/shell-emission-model.md' ':(exclude)docs/plans/construction-justification-rule.md' ':(exclude)docs/plans/emission-ingestion-inverse.md' ':(exclude)docs/plans/testgen-oracle.md' ':(exclude)docs/plans/disposition-carrier.md' ':(exclude)docs/plans/fold-ergonomics.md' ':(exclude)docs/plans/m4-universal-hermetic-corpus.md' ':(exclude)docs/plans/wiring-liveness-preflight.md' ':(exclude)docs/plans/interpreter-kernel-d.md' ':(exclude)docs/plans/inert-layer-lens.md' ':(exclude)docs/plans/compile-clean-forcecheck.md' ':(exclude)docs/plans/expressibility-frontier.md' ':(exclude)docs/plans/p1-where-clause-lowering.md' ':(exclude)docs/plans/intent-linearity-design-draft.md' ':(exclude)docs/plans/solve-higher-order-design.md' ':(exclude)docs/plans/language-target-self-host-frontier.md' ':(exclude)docs/plans/self-applying-lenses.md' ':(exclude)docs/plans/budget-tree.md' ':(exclude)docs/plans/cardinality-refinement.md' ':(exclude)docs/plans/compute-envelope-model.md' ':(exclude)docs/plans/input-envelope-roadmap.md' ':(exclude)docs/plans/ci-selection-vs-scheduling.md' ':(exclude)docs/plans/ci-process-end-to-end.md' ':(exclude)docs/plans/ci-oom-reclassification.md' ':(exclude)docs/plans/bounded-input-cost-envelope-scheduling.md' ':(exclude)docs/plans/ci-humming.md' ':(exclude)docs/plans/edge-b-rust-dag-provenance-brief.md' ':(exclude)docs/plans/resolver-type-name-collision-wall.md' ':(exclude)docs/plans/realization-measurement-loop.md' ':(exclude)docs/plans/host-effect-orchestration.md' ':(exclude)docs/plans/ci-floor-fractal-gantt.md' ':(exclude)docs/plans/resolver-pathology-profile-receipt.md' ':(exclude)docs/plans/representation-minimization.md' ':(exclude)docs/plans/reference-grounding-migration.md' ':(exclude)docs/plans/typescript-gap-census.md' ':(exclude)docs/plans/cli-run-hollowing-plan.md' ':(exclude)docs/plans/fleet-acceptance-criteria.md' ':(exclude)docs/plans/structural-quadratic-wall-coverage-audit.md' ':(exclude)docs/plans/ci-performance-tanking-evidence.md' ':(exclude)docs/plans/extdeps-modeling-preflight.md' ':(exclude)docs/plans/discrete-cost-derivation.md' ':(exclude)docs/plans/v2-complexity-capability-parity.md' ':(exclude)src/v1/stage0/src/compiler_tests.rs' ':(exclude)src/v1/stage0/src/extdeps_cargo.rs' ':(exclude)src/v1/stage0/src/extdeps_cargo_version.rs' ':(exclude)src/v1/stage0/src/extdeps_container_oci_digest.rs' ':(exclude)src/v1/stage0/src/extdeps_external_authority.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_dag_emit.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_dag_syntax.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_dag_types.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_go_emit.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_go_syntax.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_go_types.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_python_emit.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_python_syntax.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_python_types.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_rust_emit.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_rust_syntax.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_rust_types.rs' ':(exclude)src/v1/stage0/src/extdeps_units_dimensionless.rs' ':(exclude)src/v1/stage0/src/extdeps_units_iec_80000_13.rs' ':(exclude)src/v1/stage0/src/extdeps_units_iso8601.rs' ':(exclude)src/v1/stage0/src/extdeps_uri.rs' ':(exclude)src/v1/stage0/src/extdeps_uri_path.rs' ':(exclude)src/v1/stage0/src/extdeps_version.rs' ':(exclude)src/v1/stage0/src/extdeps_version_semver.rs' ':(exclude)src/v1/stage0/src/gunbc_namespace_reference_derived_closure_admission.rs' ':(exclude)src/v1/stage0/src/gunbc_namespace_reference_derived_closure_contract.rs' ':(exclude)src/v1/stage0/src/gunbc_rust_decl_type_overlay.rs' ':(exclude)src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs' ':(exclude)src/v1/stage0/src/gunbc_stage0_crate_partition_generated.rs' ':(exclude)src/v1/stage0/src/lib.rs' ':(exclude)src/v1/stage0/src/std_algebra.rs' ':(exclude)src/v1/stage0/src/std_coercion.rs' ':(exclude)src/v1/stage0/src/std_computation.rs' ':(exclude)src/v1/stage0/src/std_constructors.rs' ':(exclude)src/v1/stage0/src/std_content_hash.rs' ':(exclude)src/v1/stage0/src/std_currency.rs' ':(exclude)src/v1/stage0/src/std_decl_ref.rs' ':(exclude)src/v1/stage0/src/std_disposition.rs' ':(exclude)src/v1/stage0/src/std_dissolution.rs' ':(exclude)src/v1/stage0/src/std_effects.rs' ':(exclude)src/v1/stage0/src/std_emit_model.rs' ':(exclude)src/v1/stage0/src/std_error_primitives.rs' ':(exclude)src/v1/stage0/src/std_execution_mode.rs' ':(exclude)src/v1/stage0/src/std_graph.rs' ':(exclude)src/v1/stage0/src/std_http_path.rs' ':(exclude)src/v1/stage0/src/std_induction.rs' ':(exclude)src/v1/stage0/src/std_integer.rs' ':(exclude)src/v1/stage0/src/std_interface_summary.rs' ':(exclude)src/v1/stage0/src/std_iteration.rs' ':(exclude)src/v1/stage0/src/std_keyed_roster.rs' ':(exclude)src/v1/stage0/src/std_keyed_row.rs' ':(exclude)src/v1/stage0/src/std_logic.rs' ':(exclude)src/v1/stage0/src/std_machine_constraints.rs' ':(exclude)src/v1/stage0/src/std_magnitude.rs' ':(exclude)src/v1/stage0/src/std_measure.rs' ':(exclude)src/v1/stage0/src/std_nat.rs' ':(exclude)src/v1/stage0/src/std_node.rs' ':(exclude)src/v1/stage0/src/std_occurrence_binding.rs' ':(exclude)src/v1/stage0/src/std_occurrence_binding_candidates.rs' ':(exclude)src/v1/stage0/src/std_occurrence_binding_resolve.rs' ':(exclude)src/v1/stage0/src/std_occurrence_identity.rs' ':(exclude)src/v1/stage0/src/std_pareto.rs' ':(exclude)src/v1/stage0/src/std_process_termination.rs' ':(exclude)src/v1/stage0/src/std_realization_schedule.rs' ':(exclude)src/v1/stage0/src/std_reference_binding_observation.rs' ':(exclude)src/v1/stage0/src/std_roster_frontier.rs' ':(exclude)src/v1/stage0/src/std_serialization.rs' ':(exclude)src/v1/stage0/src/std_source_annotation.rs' ':(exclude)src/v1/stage0/src/std_syntax.rs' ':(exclude)src/v1/stage0/src/std_termination.rs' ':(exclude)src/v1/stage0/src/std_trait_derive_shape.rs' ':(exclude)src/v1/stage0/src/std_types.rs' ':(exclude)src/v1/stage0/src/std_unicode_types.rs' ':(exclude)src/v1/stage0/src/std_witness_admission.rs' ':(exclude)src/v1/stage0/src/v1_compiler_annotation_bind.rs' ':(exclude)src/v1/stage0/src/v1_compiler_artifact.rs' ':(exclude)src/v1/stage0/src/v1_compiler_closure_stub_v2_std_integer_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_closure_stub_v2_std_text_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_coercion.rs' ':(exclude)src/v1/stage0/src/v1_compiler_compile.rs' ':(exclude)src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_complexity.rs' ':(exclude)src/v1/stage0/src/v1_compiler_dag_collect.rs' ':(exclude)src/v1/stage0/src/v1_compiler_dag_collect_support.rs' ':(exclude)src/v1/stage0/src/v1_compiler_effect_derivation.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit_core_support.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit_go.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit_python.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_frontend_observation.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_access.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_cycle.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_emit_info.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_env.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_items.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_lookup.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_method.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_occurrence_binding.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_patterns.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_resolve.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_service.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_sigs.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_types.rs' ':(exclude)src/v1/stage0/src/v1_compiler_languages.rs' ':(exclude)src/v1/stage0/src/v1_compiler_normalize.rs' ':(exclude)src/v1/stage0/src/v1_compiler_ownership.rs' ':(exclude)src/v1/stage0/src/v1_compiler_parse.rs' ':(exclude)src/v1/stage0/src/v1_compiler_resolve.rs' ':(exclude)src/v1/stage0/src/v1_compiler_runtime_go.rs' ':(exclude)src/v1/stage0/src/v1_compiler_runtime_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_stage0_crates.rs' ':(exclude)src/v1/stage0/src/v1_compiler_tokenize.rs' ':(exclude)src/v1/stage0/src/v1_compiler_trace.rs' ':(exclude)src/v1/stage0/src/v1_compiler_trait_derive_emit.rs' ':(exclude)src/v1/stage0/src/v1_compiler_workspace_members.rs' ':(exclude)src/v1/stage0/src/v1_gunbc_namespace_reference_derived_closure_production_observations.rs' ':(exclude)src/v1/stage0/src/v1_gunbc_occurrence_binding_parser_walk.rs' ':(exclude)src/v1/stage0/src/v1_probe_emit_interp.rs' ':(exclude)src/v1/stage0/src/v1_rt.rs' ':(exclude)src/v1/stage0/src/v1_std_core.rs' ':(exclude)src/v1/stage0/src/v1_test_non_ascii_perf_fixture.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_caret_parse_smoke_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_namespace_reference_derived_closure_production_admissions_witness_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_occurrence_binding_parser_walk_witness_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_occurrence_identity_debt_receipt_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_ordinary_frontend_observation_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_pattern_binder_declaration_node_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_required_expr_newline_continuation_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_binding_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_capture_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_erasure_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_round_trip_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_target_emission_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_complexity_eviction_hazard_test.rs' ':(exclude)src/v1/stage0/src/wt_a.rs' ':(exclude)src/v1/stage0/src/wt_b.rs' ':(exclude)src/v1/stage0/src/wt_common.rs')" + AUTHORED_CONFLICTS="$(git diff --name-only --diff-filter=U -- . ':(exclude).github/workflows/ci.yml' ':(exclude).github/workflows/falsifier.yml' ':(exclude).gitignore' ':(exclude).gitattributes' ':(exclude)ROADMAP.md' ':(exclude)DESIGN.md' ':(exclude).githooks/pre-push' ':(exclude).githooks/pre-commit' ':(exclude).githooks/generated-artifact-merge' ':(exclude)dag/gunbc/stage0_crate_layout_generated.dag' ':(exclude)src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs' ':(exclude)dag/gunbc/stage0_crate_partition_generated.dag' ':(exclude)dag/gunbc/stage0_emit_plan_generated.dag' ':(exclude)src/v1/stage0/src/v1_interpreter_dispatch_generated.rs' ':(exclude)docs/plans/idea-machine.md' ':(exclude)docs/plans/algebraic-rewrite-optimization.md' ':(exclude)docs/plans/dag-v2-defork-audit.md' ':(exclude)docs/plans/v2-self-hosting.md' ':(exclude)docs/plans/m5-fixture-store-consolidation.md' ':(exclude)docs/plans/model-realization-fork.md' ':(exclude)docs/plans/value-null-split.md' ':(exclude)docs/plans/ci-merge-freshness.md' ':(exclude)docs/plans/seed-debt-bundle-item-2.md' ':(exclude)docs/plans/axiom-syllogism-lens.md' ':(exclude)docs/plans/invert-hand-maintained.md' ':(exclude)docs/plans/fail-closed-lockdown.md' ':(exclude)docs/plans/format-model-reconciliation.md' ':(exclude)docs/plans/regime2-shared-emission-fold.md' ':(exclude)docs/plans/shell-emission-model.md' ':(exclude)docs/plans/construction-justification-rule.md' ':(exclude)docs/plans/emission-ingestion-inverse.md' ':(exclude)docs/plans/testgen-oracle.md' ':(exclude)docs/plans/disposition-carrier.md' ':(exclude)docs/plans/fold-ergonomics.md' ':(exclude)docs/plans/m4-universal-hermetic-corpus.md' ':(exclude)docs/plans/wiring-liveness-preflight.md' ':(exclude)docs/plans/interpreter-kernel-d.md' ':(exclude)docs/plans/inert-layer-lens.md' ':(exclude)docs/plans/compile-clean-forcecheck.md' ':(exclude)docs/plans/expressibility-frontier.md' ':(exclude)docs/plans/p1-where-clause-lowering.md' ':(exclude)docs/plans/intent-linearity-design-draft.md' ':(exclude)docs/plans/solve-higher-order-design.md' ':(exclude)docs/plans/language-target-self-host-frontier.md' ':(exclude)docs/plans/self-applying-lenses.md' ':(exclude)docs/plans/budget-tree.md' ':(exclude)docs/plans/cardinality-refinement.md' ':(exclude)docs/plans/compute-envelope-model.md' ':(exclude)docs/plans/input-envelope-roadmap.md' ':(exclude)docs/plans/ci-selection-vs-scheduling.md' ':(exclude)docs/plans/ci-process-end-to-end.md' ':(exclude)docs/plans/ci-oom-reclassification.md' ':(exclude)docs/plans/bounded-input-cost-envelope-scheduling.md' ':(exclude)docs/plans/ci-humming.md' ':(exclude)docs/plans/edge-b-rust-dag-provenance-brief.md' ':(exclude)docs/plans/resolver-type-name-collision-wall.md' ':(exclude)docs/plans/realization-measurement-loop.md' ':(exclude)docs/plans/host-effect-orchestration.md' ':(exclude)docs/plans/ci-floor-fractal-gantt.md' ':(exclude)docs/plans/resolver-pathology-profile-receipt.md' ':(exclude)docs/plans/representation-minimization.md' ':(exclude)docs/plans/reference-grounding-migration.md' ':(exclude)docs/plans/typescript-gap-census.md' ':(exclude)docs/plans/cli-run-hollowing-plan.md' ':(exclude)docs/plans/fleet-acceptance-criteria.md' ':(exclude)docs/plans/structural-quadratic-wall-coverage-audit.md' ':(exclude)docs/plans/ci-performance-tanking-evidence.md' ':(exclude)docs/plans/extdeps-modeling-preflight.md' ':(exclude)docs/plans/discrete-cost-derivation.md' ':(exclude)docs/plans/v2-complexity-capability-parity.md' ':(exclude)src/v1/stage0/src/compiler_tests.rs' ':(exclude)src/v1/stage0/src/extdeps_cargo.rs' ':(exclude)src/v1/stage0/src/extdeps_cargo_version.rs' ':(exclude)src/v1/stage0/src/extdeps_container_oci_digest.rs' ':(exclude)src/v1/stage0/src/extdeps_external_authority.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_dag_emit.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_dag_syntax.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_dag_types.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_go_emit.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_go_syntax.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_go_types.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_python_emit.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_python_syntax.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_python_types.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_rust_emit.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_rust_syntax.rs' ':(exclude)src/v1/stage0/src/extdeps_languages_rust_types.rs' ':(exclude)src/v1/stage0/src/extdeps_units_dimensionless.rs' ':(exclude)src/v1/stage0/src/extdeps_units_iec_80000_13.rs' ':(exclude)src/v1/stage0/src/extdeps_units_iso8601.rs' ':(exclude)src/v1/stage0/src/extdeps_uri.rs' ':(exclude)src/v1/stage0/src/extdeps_uri_path.rs' ':(exclude)src/v1/stage0/src/extdeps_version.rs' ':(exclude)src/v1/stage0/src/extdeps_version_semver.rs' ':(exclude)src/v1/stage0/src/gunbc_namespace_reference_derived_closure_admission.rs' ':(exclude)src/v1/stage0/src/gunbc_namespace_reference_derived_closure_contract.rs' ':(exclude)src/v1/stage0/src/gunbc_rust_decl_type_overlay.rs' ':(exclude)src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs' ':(exclude)src/v1/stage0/src/gunbc_stage0_crate_partition_generated.rs' ':(exclude)src/v1/stage0/src/lib.rs' ':(exclude)src/v1/stage0/src/std_algebra.rs' ':(exclude)src/v1/stage0/src/std_coercion.rs' ':(exclude)src/v1/stage0/src/std_computation.rs' ':(exclude)src/v1/stage0/src/std_constructors.rs' ':(exclude)src/v1/stage0/src/std_content_hash.rs' ':(exclude)src/v1/stage0/src/std_currency.rs' ':(exclude)src/v1/stage0/src/std_decl_ref.rs' ':(exclude)src/v1/stage0/src/std_disposition.rs' ':(exclude)src/v1/stage0/src/std_dissolution.rs' ':(exclude)src/v1/stage0/src/std_effects.rs' ':(exclude)src/v1/stage0/src/std_emit_model.rs' ':(exclude)src/v1/stage0/src/std_error_primitives.rs' ':(exclude)src/v1/stage0/src/std_execution_mode.rs' ':(exclude)src/v1/stage0/src/std_graph.rs' ':(exclude)src/v1/stage0/src/std_http_path.rs' ':(exclude)src/v1/stage0/src/std_induction.rs' ':(exclude)src/v1/stage0/src/std_integer.rs' ':(exclude)src/v1/stage0/src/std_interface_summary.rs' ':(exclude)src/v1/stage0/src/std_iteration.rs' ':(exclude)src/v1/stage0/src/std_keyed_roster.rs' ':(exclude)src/v1/stage0/src/std_keyed_row.rs' ':(exclude)src/v1/stage0/src/std_logic.rs' ':(exclude)src/v1/stage0/src/std_machine_constraints.rs' ':(exclude)src/v1/stage0/src/std_magnitude.rs' ':(exclude)src/v1/stage0/src/std_measure.rs' ':(exclude)src/v1/stage0/src/std_nat.rs' ':(exclude)src/v1/stage0/src/std_node.rs' ':(exclude)src/v1/stage0/src/std_occurrence_binding.rs' ':(exclude)src/v1/stage0/src/std_occurrence_binding_candidates.rs' ':(exclude)src/v1/stage0/src/std_occurrence_binding_resolve.rs' ':(exclude)src/v1/stage0/src/std_occurrence_identity.rs' ':(exclude)src/v1/stage0/src/std_pareto.rs' ':(exclude)src/v1/stage0/src/std_process_termination.rs' ':(exclude)src/v1/stage0/src/std_realization_schedule.rs' ':(exclude)src/v1/stage0/src/std_reference_binding_observation.rs' ':(exclude)src/v1/stage0/src/std_roster_frontier.rs' ':(exclude)src/v1/stage0/src/std_serialization.rs' ':(exclude)src/v1/stage0/src/std_source_annotation.rs' ':(exclude)src/v1/stage0/src/std_syntax.rs' ':(exclude)src/v1/stage0/src/std_termination.rs' ':(exclude)src/v1/stage0/src/std_trait_derive_shape.rs' ':(exclude)src/v1/stage0/src/std_types.rs' ':(exclude)src/v1/stage0/src/std_unicode_types.rs' ':(exclude)src/v1/stage0/src/std_witness_admission.rs' ':(exclude)src/v1/stage0/src/v1_compiler_annotation_bind.rs' ':(exclude)src/v1/stage0/src/v1_compiler_artifact.rs' ':(exclude)src/v1/stage0/src/v1_compiler_closure_stub_v2_std_integer_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_closure_stub_v2_std_text_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_coercion.rs' ':(exclude)src/v1/stage0/src/v1_compiler_compile.rs' ':(exclude)src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_complexity.rs' ':(exclude)src/v1/stage0/src/v1_compiler_dag_collect.rs' ':(exclude)src/v1/stage0/src/v1_compiler_dag_collect_support.rs' ':(exclude)src/v1/stage0/src/v1_compiler_effect_derivation.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit_core_support.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit_go.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit_python.rs' ':(exclude)src/v1/stage0/src/v1_compiler_emit_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_frontend_observation.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_access.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_cycle.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_emit_info.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_env.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_items.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_lookup.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_method.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_occurrence_binding.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_patterns.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_resolve.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_service.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_sigs.rs' ':(exclude)src/v1/stage0/src/v1_compiler_infer_types.rs' ':(exclude)src/v1/stage0/src/v1_compiler_languages.rs' ':(exclude)src/v1/stage0/src/v1_compiler_normalize.rs' ':(exclude)src/v1/stage0/src/v1_compiler_ownership.rs' ':(exclude)src/v1/stage0/src/v1_compiler_parse.rs' ':(exclude)src/v1/stage0/src/v1_compiler_resolve.rs' ':(exclude)src/v1/stage0/src/v1_compiler_runtime_go.rs' ':(exclude)src/v1/stage0/src/v1_compiler_runtime_rust.rs' ':(exclude)src/v1/stage0/src/v1_compiler_stage0_crates.rs' ':(exclude)src/v1/stage0/src/v1_compiler_tokenize.rs' ':(exclude)src/v1/stage0/src/v1_compiler_trace.rs' ':(exclude)src/v1/stage0/src/v1_compiler_trait_derive_emit.rs' ':(exclude)src/v1/stage0/src/v1_compiler_workspace_members.rs' ':(exclude)src/v1/stage0/src/v1_gunbc_namespace_reference_derived_closure_production_observations.rs' ':(exclude)src/v1/stage0/src/v1_gunbc_occurrence_binding_parser_walk.rs' ':(exclude)src/v1/stage0/src/v1_probe_emit_interp.rs' ':(exclude)src/v1/stage0/src/v1_rt.rs' ':(exclude)src/v1/stage0/src/v1_std_core.rs' ':(exclude)src/v1/stage0/src/v1_test_non_ascii_perf_fixture.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_caret_parse_smoke_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_namespace_reference_derived_closure_production_admissions_witness_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_occurrence_binding_parser_walk_witness_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_occurrence_identity_debt_receipt_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_ordinary_frontend_observation_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_pattern_binder_declaration_node_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_required_expr_newline_continuation_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_binding_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_capture_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_erasure_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_round_trip_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_annotation_target_emission_test.rs' ':(exclude)src/v1/stage0/src/v1_tests_claim_v1_complexity_eviction_hazard_test.rs' ':(exclude)src/v1/stage0/src/v2_std_live_tree.rs' ':(exclude)src/v1/stage0/src/wt_a.rs' ':(exclude)src/v1/stage0/src/wt_b.rs' ':(exclude)src/v1/stage0/src/wt_common.rs')" if [ -n "$AUTHORED_CONFLICTS" ]; then echo "heal refused: binary/source revision skew, and the remedy CONFLICTS in authored files" >&2 echo " conflicting paths:" >&2 From 628e8d6b240781a1f45f61de5d5096c3df06aa69 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 07:14:54 +0000 Subject: [PATCH 7/9] Move the verdict decode into the model, where the coproduct is declared MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The seed was matching WitnessRunDisposition and ScopedExecutionPolicy by comparing interned symbol names against name arrays it carried itself — including a hardcoded five-element roster of WitnessRefusalCause. That is a second copy of those vocabularies written in a language that cannot be told when they grow: add a cause and the Rust arm goes silently unmatched. scoped_admission_state / scoped_admission_detail / scoped_refusal_detail and scoped_event_requires_full_execution keep the match where the type is declared, so a new variant is a compile error in the model. The seed now passes the verdict Value straight back and reads a String or a Bool it never interprets structurally; zero sym_eq calls remain in this seam. The projections are load-bearing — the host writes the manifest on "run" and exits 1 on "refuse" — so a RunWitness projected as "skip" would be exactly the silent false skip this module exists to prevent. Four witnesses pin each tag against the arm that produces it, and one pins that the refusal detail names its cause family and carries the reason. Rust net across cli_run.rs + claim_executor.rs: +297 -> +253. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/scoped_floor_execution.dag | 53 ++++++- .../scoped_floor_execution_witness_test.dag | 52 +++++++ src/v1/stage0/src/bin/claim_executor.rs | 134 ++++++------------ 3 files changed, 148 insertions(+), 91 deletions(-) diff --git a/dag/gunbc/scoped_floor_execution.dag b/dag/gunbc/scoped_floor_execution.dag index 66c3f97bf73..4332e243da2 100644 --- a/dag/gunbc/scoped_floor_execution.dag +++ b/dag/gunbc/scoped_floor_execution.dag @@ -9,16 +9,18 @@ import v2.lens.module_graph { module_declaration_facts_live } import v2.workflow.affected_set_floor_runner { - DiffObservationRefusal, + DependencyObservationRefusal, DiffObservationFailClosed, + DiffObservationRefusal, DiffPathsProduced, - DependencyObservationRefusal, DispositionAuthorityRefusal, FloorDiffObservation, + FrontierQueryRefusal, Refused, RunWitness, SkipAssumedGreen, SubjectObservationRefusal, + WitnessRefusalCause, WitnessRunDisposition } @@ -265,3 +267,50 @@ fn scoped_witness_run_disposition( } } } + +// HOST PROJECTIONS. The seed must not re-derive what the fold already decided. +// A host arm matching over WitnessRunDisposition or WitnessRefusalCause can only +// compare interned symbol names against names it carries itself, which is a +// second copy of this vocabulary written in a language that cannot be told when +// the vocabulary grows: add a cause here and the Rust arm goes silently +// unmatched. These two projections keep the match where the coproduct is +// declared, so a new variant is a compile error in the model and the seed reads +// two strings it never interprets structurally. +// +// The state tag is a WIRE encoding at the same seam as the flattened arguments +// above, and it is exhaustive by construction: there is no fall-through arm, so +// a fourth disposition cannot acquire a default. +fn scoped_admission_state(disposition: WitnessRunDisposition) -> String { + match disposition { + RunWitness { reason: _ } => "run" + SkipAssumedGreen => "skip" + Refused { cause: _ } => "refuse" + } +} + +fn scoped_admission_detail(disposition: WitnessRunDisposition) -> String { + match disposition { + RunWitness { reason: reason } => "reason={reason}" + SkipAssumedGreen => "no scoped entry closure intersects a changed path, and no path departed" + Refused { cause: cause } => scoped_refusal_detail(cause: cause) + } +} + +fn scoped_refusal_detail(cause: WitnessRefusalCause) -> String { + match cause { + DiffObservationRefusal { reason: reason } => "DiffObservationRefusal detail={reason}" + FrontierQueryRefusal { reason: reason } => "FrontierQueryRefusal detail={reason}" + SubjectObservationRefusal { reason: reason } => "SubjectObservationRefusal detail={reason}" + DependencyObservationRefusal { reason: reason } => "DependencyObservationRefusal detail={reason}" + DispositionAuthorityRefusal { reason: reason } => "DispositionAuthorityRefusal detail={reason}" + } +} + +// The backstop, projected to the one Bool the child needs. Same reason: the +// child was matching ScopedExecutionPolicy variant names in Rust. +fn scoped_event_requires_full_execution(event: String) -> Bool { + match scoped_execution_policy_for_event(event: event) { + ScopedPolicyRequiresFullExecution { reason: _ } => true + ScopedPolicyPredictsFromDiff => false + } +} diff --git a/dag/test/claim/scoped_floor_execution_witness_test.dag b/dag/test/claim/scoped_floor_execution_witness_test.dag index 64474cc5dc3..ef079856504 100644 --- a/dag/test/claim/scoped_floor_execution_witness_test.dag +++ b/dag/test/claim/scoped_floor_execution_witness_test.dag @@ -32,6 +32,8 @@ import gunbc.scoped_floor_execution { ScopedSubjectStanding, ScopedSubjectMatched, ScopedSubjectMismatched, + scoped_admission_detail, + scoped_admission_state, scoped_execution_policy_for_event, scoped_witness_run_disposition } @@ -315,3 +317,53 @@ test fn red_backstop_event_still_refuses_a_contradicted_disposition() -> Bool { SkipAssumedGreen => false } } + +// The host reads these two strings and acts on them: "run" writes the batch id +// into the manifest, "skip" writes an empty one, "refuse" exits 1. A wrong tag +// here is therefore not a cosmetic defect - a RunWitness projected as "skip" is +// a silent false skip, the exact failure the whole module exists to prevent - +// so each tag is pinned against the arm that produces it. +test fn w_run_projects_the_run_state() -> Bool { + scoped_admission_state(disposition: decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: touching_diff, + departed_paths: [], + affected: ScopedEntriesAffected + )) == "run" +} + +test fn w_skip_projects_the_skip_state() -> Bool { + scoped_admission_state(disposition: decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: unrelated_diff, + departed_paths: [], + affected: ScopedEntriesUnaffected + )) == "skip" +} + +test fn w_refusal_projects_the_refuse_state() -> Bool { + scoped_admission_state(disposition: decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionAgrees, + diff: DiffObservationFailClosed { reason: "git diff unavailable" }, + departed_paths: [], + affected: ScopedEntriesUnaffected + )) == "refuse" +} + +// The detail must NAME the cause family. A refusal whose class the operator +// cannot read from the journal row sends them round the loop to find it, which +// is the located half of "typed, located, counted". +test fn w_refusal_detail_names_the_cause_family_and_carries_its_reason() -> Bool { + let detail = scoped_admission_detail(disposition: decide( + subject: ScopedSubjectMatched, + disposition: ScopedDispositionContradicted { reason: "derived closure reaches a host-effect sink" }, + diff: unrelated_diff, + departed_paths: [], + affected: ScopedEntriesUnaffected + )) + string_contains(detail, "DispositionAuthorityRefusal") + && string_contains(detail, "derived closure reaches a host-effect sink") +} diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index b4029720998..b8e418c68e1 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -9614,79 +9614,29 @@ fn write_floor_worker_terminal(outcome: &str, detail: &str) -> Result<(), String const SCOPED_ADMISSION_ENTRY: &str = "dag/gunbc/scoped_floor_execution.dag"; -/// Render the `.dag` verdict into (journal state, detail). A `Refused` arm is an -/// `Err`: "I could not decide" and "nothing is affected" project onto the same -/// zero manifest ids, so they must not share a success arm — an empty manifest is -/// evidence of a skip only when a `SkipAssumedGreen` was actually observed. -fn scoped_admission_projection( +/// Read one `String`-returning projection of the already-computed verdict. +/// +/// The verdict `Value` is passed straight back into the model rather than +/// destructured here: the seed carries no copy of `WitnessRunDisposition` or +/// `WitnessRefusalCause`, so a variant added to either is a compile error where +/// the coproduct is declared instead of an arm this file silently fails to match. +fn scoped_admission_projection_str( ctx: &InterpContext, + projection: &str, verdict: &Value, - batch_id: &str, -) -> Result<(&'static str, String), String> { - let reason_of = |fields: &_| -> String { - match ctx.field(fields, "reason") { - Some(Value::Str(s)) => s.clone(), - _ => String::new(), - } - }; - match verdict { - Value::Variant { - variant_name, - fields, - .. - } if ctx.sym_eq(*variant_name, "RunWitness") => { - Ok(("run", format!("reason={}", reason_of(fields)))) - } - Value::Variant { variant_name, .. } if ctx.sym_eq(*variant_name, "SkipAssumedGreen") => Ok(( - "skip", - "reason=scoped entry dependency closure unaffected by the observed diff".to_string(), - )), - Value::Variant { - variant_name, - fields, - .. - } if ctx.sym_eq(*variant_name, "Refused") => { - // Named exhaustively rather than rendered: only `sym_eq` is public, and an - // unrecognised cause must be an error, not an unlabelled refusal. A refusal - // whose class the operator cannot read sends them round the loop to find it. - let cause = match ctx.field(fields, "cause") { - Some(Value::Variant { - variant_name: cause_name, - fields: cause_fields, - .. - }) => { - let label = [ - "DiffObservationRefusal", - "FrontierQueryRefusal", - "SubjectObservationRefusal", - "DependencyObservationRefusal", - "DispositionAuthorityRefusal", - ] - .into_iter() - .find(|name| ctx.sym_eq(*cause_name, name)) - .ok_or_else(|| { - format!( - "scoped admission refusal carries an unmodelled WitnessRefusalCause \ - for batch {batch_id}" - ) - })?; - format!("{label} detail={}", reason_of(cause_fields)) - } - _ => { - return Err(format!( - "scoped admission Refused for batch {batch_id} carries no `cause` field" - )) - } - }; - Err(format!( - "SCOPED-ADMISSION-REFUSED batch={batch_id} cause={cause} — the scoped batch \ - is neither run nor skipped on unobserved evidence" - )) - } - other => Err(format!( - "scoped_witness_run_disposition_from_host returned `{}`, expected WitnessRunDisposition", - ctx.format_value(other) +) -> Result { + match run_in_context_with_args( + ctx, + projection, + &[(Some("disposition".to_string()), verdict.clone())], + false, + ) { + Ok(Value::Str(s)) => Ok(s), + Ok(other) => Err(format!( + "{projection} returned `{}`, expected String", + ctx.format_value(&other) )), + Err(msg) => Err(format!("{projection}: {msg}")), } } @@ -9711,28 +9661,17 @@ fn scoped_backstop_requires_full_execution(walk_source_roots: &[String]) -> Resu let ctx = make_eval_context(&graph, indices, ExecutionMode::Hermetic); match run_in_context_with_args( &ctx, - "scoped_execution_policy_for_event", + "scoped_event_requires_full_execution", &[(Some("event".to_string()), Value::Str(event.clone()))], false, ) { - Ok(Value::Variant { variant_name, .. }) => { - if ctx.sym_eq(variant_name, "ScopedPolicyPredictsFromDiff") { - Ok(false) - } else if ctx.sym_eq(variant_name, "ScopedPolicyRequiresFullExecution") { - Ok(true) - } else { - Err(format!( - "scoped_execution_policy_for_event returned an unmodelled \ - ScopedExecutionPolicy variant for event `{event}`" - )) - } - } + Ok(Value::Bool(b)) => Ok(b), Ok(other) => Err(format!( - "scoped_execution_policy_for_event returned `{}`, expected ScopedExecutionPolicy", + "scoped_event_requires_full_execution returned `{}` for event `{event}`, expected Bool", ctx.format_value(&other) )), Err(msg) => Err(format!( - "scoped_execution_policy_for_event unavailable for event `{event}`: {msg}" + "scoped_event_requires_full_execution unavailable for event `{event}`: {msg}" )), } } @@ -9826,15 +9765,32 @@ fn scoped_batch_admitted_ids( false, ) .map_err(|e| format!("scoped_witness_run_disposition_from_host ({batch_id}): {e}"))?; - let (state, detail) = scoped_admission_projection(&ctx, &verdict, batch_id)?; + let state = scoped_admission_projection_str(&ctx, "scoped_admission_state", &verdict)?; + let detail = scoped_admission_projection_str(&ctx, "scoped_admission_detail", &verdict)?; append_floor_phase_journal( "scoped-admission", - state, + &state, &format!("batch={batch_id} {detail}"), ); eprintln!("[scoped-admission] batch={batch_id} disposition={state} {detail}"); - if state == "run" { - admitted.push(batch_id.clone()); + // "Could not decide" and "nothing is affected" project onto the same zero + // manifest ids, so they must not share a success arm — an empty manifest is + // evidence of a skip only when a skip was actually observed. + match state.as_str() { + "run" => admitted.push(batch_id.clone()), + "skip" => {} + "refuse" => { + return Err(format!( + "SCOPED-ADMISSION-REFUSED batch={batch_id} {detail} — the scoped batch \ + is neither run nor skipped on unobserved evidence" + )) + } + other => { + return Err(format!( + "scoped_admission_state returned unmodelled state `{other}` for batch \ + {batch_id}" + )) + } } } Ok(admitted) From 4731f22ef606f18139c3cc33b25813e34e0fbf03 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 07:56:38 +0000 Subject: [PATCH 8/9] regen the stage0 seed for the relocated live_tree carrier MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `regen` red at 628e8d6b240 with `read committed src/v1/stage0/src/v2_std_live_tree.rs: No such file or directory`. Moving the carrier under `dag/` put `v2.std.live_tree` inside the stage0 emit closure, and the two jobs that regenerate artifacts in CI do not write this class: `heal_generated_artifacts` runs `generated_artifact_gate main_wet`, which derives the emit plan, `.gitattributes` and `ci.yml` — it produced those three and passed — while the `regen` job only VERIFIES the seed against a fresh self-compile. Emitting the module is the local `regen_stage0` bootstrap, and that is what this commit carries. Fixed point proven by execution, not by one pass: regen_stage0 round 1 — wrote the module + lib.rs + 5 test modules cargo build --release the emitter reads the partition compiled into itself regen_stage0 round 2 — no further change regen_stage0 --verify regen_divergence_count=0 main_wet no change (heal had already settled it) Seven files, all generated: the new module, `lib.rs`'s registration, and the five emitted test modules that now carry the `live_tree_disposition` row their `.dag` sources declare. Co-Authored-By: Claude Opus 5 (1M context) --- src/v1/stage0/src/lib.rs | 1 + .../v1_tests_claim_caret_parse_smoke_test.rs | 11 +++++ ...sure_production_admissions_witness_test.rs | 11 +++++ ...laim_ordinary_frontend_observation_test.rs | 11 +++++ ...im_pattern_binder_declaration_node_test.rs | 11 +++++ ...laim_v1_complexity_eviction_hazard_test.rs | 11 +++++ src/v1/stage0/src/v2_std_live_tree.rs | 42 +++++++++++++++++++ 7 files changed, 98 insertions(+) create mode 100644 src/v1/stage0/src/v2_std_live_tree.rs diff --git a/src/v1/stage0/src/lib.rs b/src/v1/stage0/src/lib.rs index a64640d370f..c49379f1721 100644 --- a/src/v1/stage0/src/lib.rs +++ b/src/v1/stage0/src/lib.rs @@ -149,6 +149,7 @@ pub mod v1_tests_claim_v1_annotation_erasure_test; pub mod v1_tests_claim_v1_annotation_round_trip_test; pub mod v1_tests_claim_v1_annotation_target_emission_test; pub mod v1_tests_claim_v1_complexity_eviction_hazard_test; +pub mod v2_std_live_tree; pub mod wt_a; pub mod wt_b; pub mod wt_common; diff --git a/src/v1/stage0/src/v1_tests_claim_caret_parse_smoke_test.rs b/src/v1/stage0/src/v1_tests_claim_caret_parse_smoke_test.rs index f548a11a0ed..babef2afc04 100644 --- a/src/v1/stage0/src/v1_tests_claim_caret_parse_smoke_test.rs +++ b/src/v1/stage0/src/v1_tests_claim_caret_parse_smoke_test.rs @@ -16,11 +16,22 @@ pub use crate::v1_std_core::{ diagnostic_to_message, empty_intern_table, expr_call_func_at, is_error_diagnostic, }; pub use crate::v1_std_core::{ErrorNode, NewlineIndex, Node, TokenShape}; +pub use crate::v2_std_live_tree::LiveTreeDisposition; +use crate::v2_std_live_tree::LiveTreeDisposition::SubstrateInputsOnly; use crate::NonEmptyBTreeSet; use crate::NonEmptyVec; use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; use std::rc::Rc; +pub fn live_tree_disposition() -> LiveTreeDisposition { + thread_local! { + static CACHED: LiveTreeDisposition = { + LiveTreeDisposition::SubstrateInputsOnly + }; + } + CACHED.with(|c: &LiveTreeDisposition| c.clone()) +} + pub fn caret_parse_smoke_parser_transport_enrollment() -> String { thread_local! { static CACHED: String = { diff --git a/src/v1/stage0/src/v1_tests_claim_namespace_reference_derived_closure_production_admissions_witness_test.rs b/src/v1/stage0/src/v1_tests_claim_namespace_reference_derived_closure_production_admissions_witness_test.rs index 6403a2a6651..3d67beedd84 100644 --- a/src/v1/stage0/src/v1_tests_claim_namespace_reference_derived_closure_production_admissions_witness_test.rs +++ b/src/v1/stage0/src/v1_tests_claim_namespace_reference_derived_closure_production_admissions_witness_test.rs @@ -18,6 +18,17 @@ use crate::std_reference_binding_observation::ReferenceBindingObservation::{Dist pub use crate::v1_gunbc_namespace_reference_derived_closure_production_observations::{namespace_structural_binding_observations_a_through_d}; pub use crate::std_types::{Bool, List}; use crate::std_types::Bool::*; +pub use crate::v2_std_live_tree::{LiveTreeDisposition}; +use crate::v2_std_live_tree::LiveTreeDisposition::{SubstrateInputsOnly}; + +pub fn live_tree_disposition() -> LiveTreeDisposition { + thread_local! { + static CACHED: LiveTreeDisposition = { + LiveTreeDisposition::SubstrateInputsOnly + }; + } + CACHED.with(|c: &LiveTreeDisposition| c.clone()) +} pub fn namespace_reference_derived_closure_production_admissions_witness_note() -> String { thread_local! { diff --git a/src/v1/stage0/src/v1_tests_claim_ordinary_frontend_observation_test.rs b/src/v1/stage0/src/v1_tests_claim_ordinary_frontend_observation_test.rs index 70355aa576f..d7b1eddce8b 100644 --- a/src/v1/stage0/src/v1_tests_claim_ordinary_frontend_observation_test.rs +++ b/src/v1/stage0/src/v1_tests_claim_ordinary_frontend_observation_test.rs @@ -6,11 +6,22 @@ pub use crate::v1_compiler_frontend_observation::observe_ordinary_frontend; pub use crate::v1_compiler_frontend_observation::OrdinaryFrontendObservation; use crate::v1_rt; use crate::v1_rt::{VecCompat, VecJoin}; +pub use crate::v2_std_live_tree::LiveTreeDisposition; +use crate::v2_std_live_tree::LiveTreeDisposition::SubstrateInputsOnly; use crate::NonEmptyBTreeSet; use crate::NonEmptyVec; use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; use std::rc::Rc; +pub fn live_tree_disposition() -> LiveTreeDisposition { + thread_local! { + static CACHED: LiveTreeDisposition = { + LiveTreeDisposition::SubstrateInputsOnly + }; + } + CACHED.with(|c: &LiveTreeDisposition| c.clone()) +} + pub fn probe_keyed_literal() -> Rc> { thread_local! { static CACHED: Rc> = { diff --git a/src/v1/stage0/src/v1_tests_claim_pattern_binder_declaration_node_test.rs b/src/v1/stage0/src/v1_tests_claim_pattern_binder_declaration_node_test.rs index 26e04af402d..65ababffe55 100644 --- a/src/v1/stage0/src/v1_tests_claim_pattern_binder_declaration_node_test.rs +++ b/src/v1/stage0/src/v1_tests_claim_pattern_binder_declaration_node_test.rs @@ -31,11 +31,22 @@ pub use crate::v1_std_core::{ intern_table_with_authored_token_ordinals, merge_intern_tables, }; pub use crate::v1_std_core::{CompilerDiagnostic, ExprData, MatchPattern, NewlineIndex, Node}; +pub use crate::v2_std_live_tree::LiveTreeDisposition; +use crate::v2_std_live_tree::LiveTreeDisposition::SubstrateInputsOnly; use crate::NonEmptyBTreeSet; use crate::NonEmptyVec; use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; use std::rc::Rc; +pub fn live_tree_disposition() -> LiveTreeDisposition { + thread_local! { + static CACHED: LiveTreeDisposition = { + LiveTreeDisposition::SubstrateInputsOnly + }; + } + CACHED.with(|c: &LiveTreeDisposition| c.clone()) +} + pub fn pattern_binder_declaration_node_parser_transport_enrollment() -> String { thread_local! { static CACHED: String = { diff --git a/src/v1/stage0/src/v1_tests_claim_v1_complexity_eviction_hazard_test.rs b/src/v1/stage0/src/v1_tests_claim_v1_complexity_eviction_hazard_test.rs index 5d2403bdf5f..c14ca099830 100644 --- a/src/v1/stage0/src/v1_tests_claim_v1_complexity_eviction_hazard_test.rs +++ b/src/v1/stage0/src/v1_tests_claim_v1_complexity_eviction_hazard_test.rs @@ -11,11 +11,22 @@ pub use crate::v1_compiler_complexity::{ pub use crate::v1_compiler_complexity::{Certainty, ComplexitySummary, CostExpr, CostInternTable}; use crate::v1_rt; use crate::v1_rt::{VecCompat, VecJoin}; +pub use crate::v2_std_live_tree::LiveTreeDisposition; +use crate::v2_std_live_tree::LiveTreeDisposition::SubstrateInputsOnly; use crate::NonEmptyBTreeSet; use crate::NonEmptyVec; use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; use std::rc::Rc; +pub fn live_tree_disposition() -> LiveTreeDisposition { + thread_local! { + static CACHED: LiveTreeDisposition = { + LiveTreeDisposition::SubstrateInputsOnly + }; + } + CACHED.with(|c: &LiveTreeDisposition| c.clone()) +} + pub fn eviction_hazard_home_note() -> String { thread_local! { static CACHED: String = { diff --git a/src/v1/stage0/src/v2_std_live_tree.rs b/src/v1/stage0/src/v2_std_live_tree.rs new file mode 100644 index 00000000000..351e4118524 --- /dev/null +++ b/src/v1/stage0/src/v2_std_live_tree.rs @@ -0,0 +1,42 @@ +// Generated by v1 compiler -- do not edit. +// Source module: v2.std.live_tree + +use self::LiveTreeDisposition::*; +use crate::v1_rt; +use crate::v1_rt::{VecCompat, VecJoin}; +use crate::NonEmptyBTreeSet; +use crate::NonEmptyVec; +use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; +use std::rc::Rc; + +pub fn live_tree_disposition_note() -> String { + thread_local! { + static CACHED: String = { + "Declared witness input-domain disposition (ROADMAP 2-host-scaffold-classifier-defork): a witness entry declares whether its evaluation reads the live host tree (filesystem/corpus state outside its resolved substrate closure). The single authority is a `data live_tree_disposition: LiveTreeDisposition = ...` row in the WITNESS ENTRY FILE itself - entry grain, so the fact holds no matter where the read hides behind imports. Undeclared = ReadsLiveTree (fail-closed): a row must declare SubstrateInputsOnly to become affected-set selection-eligible. This dissolves the interim floor:host_scaffold marker and the Rust text classifier witness_test_fn_uses_live_host_scan (deleted with this model).\n\nCORRECTED 2026-08-11 (session lively-bat-548). This note previously read 'a row that declares SubstrateInputsOnly while actually reading live state is NOT re-checked by any text scan; the nightly affected-set falsifier is the enforcement'. Both halves were false in the live tree. A derived text scan over the entry's whole import closure DOES re-check the declaration - cli_run effect_reach_derived_reads_live_tree_for_entry, over effect_reach_host_sink_callee_symbols_v0 (v2.std.effect_reach) - and reads_live_tree_effective is the OR of declared and derived, so a lying row is caught at selection time rather than a cadence window later. The falsifier could not have been the enforcement for every subject either: its lanes resolve over dag plus src/v2, so a src/v1 witness entry is unresolvable there. Where a declaration is CONSUMED to admit expensive work, the OR is additionally too weak on its own: silently upgrading a stale SubstrateInputsOnly row to ReadsLiveTree hides a broken authority behind an always-run answer, so gunbc.scoped_floor_execution refuses that disagreement as DispositionAuthorityRefusal instead of degrading.\n\nFILE HOME. This module is authored under dag/ while keeping the module path v2.std.live_tree, because a witness entry under src/v1 must be able to declare its own disposition and the scoped witness subject universe is exactly dag plus src/v1 - src/v2 is deliberately excluded from it. Under src/v2 the carrier was invisible to half the corpus it classifies, so no src/v1 entry could declare the row at all and all of them inherited the fail-closed default. Paths are discriminators, not gospel (DESIGN section 3); the module path is unchanged, so every existing importer is untouched. Renaming the module to std.live_tree is a separate authority migration, not collateral to this repair.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + +pub fn live_tree_disposition_stamp_provenance() -> String { + thread_local! { + static CACHED: String = { + "Migration stamp provenance (2026-07-11, machine-stamped batch): the initial corpus-wide SubstrateInputsOnly rows were stamped from the deleted entry-text classifier's verdict (entry file contains none of: floor:host_scaffold, layer_import_facts, _live(, _facts_live(, filesystem_read) - ENTRY-TEXT GRAIN, so they inherit that classifier's declared blind spot: a live read hidden behind an import was invisible to it (the former cli_run.rs cross-file deficit). A stamped row is therefore machine-vouched, not author-vouched. Enforcement is the derived closure scan described in live_tree_disposition_note, which closes exactly the cross-file blind spot the entry-text classifier declared. Dissolves-at: G2 call-reachability live-read classification (import-closure walk over LiveReadCarrier registry + fn-arrow DependencyView) per docs/plans/live-read-witness-classification-design.md — when stamps can be re-derived from proven runtime-read closure.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum LiveTreeDisposition { + ReadsLiveTree, + SubstrateInputsOnly, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct ReadsLiveTree; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct SubstrateInputsOnly; From 91865ac9eea033545d4765fe89c6f8d7984f017d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 11 Aug 2026 08:34:39 +0000 Subject: [PATCH 9/9] Hoist a source annotation out of a declaration body MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `scoped_witness_run_disposition_from_host` carried a six-line `//` block between its `let` bindings and its return expression. DESIGN §4c admits annotations only as standalone leading blocks on module-scope declarations, and the parser enforces it exactly: scoped_floor_execution.dag:199:3: error: source annotation sits inside a declaration body. Only module-item grain is modeled; move it above the declaration it describes. Found by executing a probe against the live corpus, not by review or by CI — the compile-clean gate would have caught it, but the floor never reached batch 1 while `regen` was red ahead of it. The prose is unchanged and now sits in the function's leading block. Swept the other four `.dag` files this branch touches: zero indented annotations remain. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/scoped_floor_execution.dag | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/dag/gunbc/scoped_floor_execution.dag b/dag/gunbc/scoped_floor_execution.dag index 4332e243da2..191cca7bcbf 100644 --- a/dag/gunbc/scoped_floor_execution.dag +++ b/dag/gunbc/scoped_floor_execution.dag @@ -165,6 +165,13 @@ fn scoped_departure_forces_run(departed_paths: List) -> Bool { // flattening at this one seam is what stops it from spreading into the decision, // where a Bool beside a reason string would be the state-space conflation the // standings exist to prevent. +// +// The live projection is evaluated even on a backstop event, where the decision +// will not read it. That is deliberate: the alternative is to hand the fold a +// fabricated ScopedEntriesAffected the closure never produced, which is the +// fabricated-plausible-output failure aimed at the one input a reader would take +// for evidence. One corpus scan inside a job that is about to spend 376 seconds +// is the honest price. fn scoped_witness_run_disposition_from_host( event: String, subject_matched: Bool, @@ -193,12 +200,6 @@ fn scoped_witness_run_disposition_from_host( } else { DiffObservationFailClosed { reason: diff_failure_reason } } - // The live projection is evaluated even on a backstop event, where the - // decision below will not read it. That is deliberate: the alternative is to - // hand the fold a fabricated ScopedEntriesAffected the closure never - // produced, which is the fabricated-plausible-output failure aimed at the one - // input a reader would take for evidence. One corpus scan inside a job that - // is about to spend 376 seconds is the honest price. scoped_witness_run_disposition( subject: subject, disposition: disposition,