From f8d6060d9e393dd584209ab05b64afb9f8ed8f5a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 29 Sep 2026 18:27:36 +0000 Subject: [PATCH 1/4] Quarantine: NeverRunDeclinedOutsideGate holds the ten probes the required floor never plans, per row, joined on module identity; english_emit_add leaves the quarantine Operator-manager ruling (option B): the fold gains a fifth holder, WitnessNeverRuns, for a probe with a gunbc.quarantine_outside_gate_decline row whose module required_gate_admits refuses. Each row carries its own module and next-rung trigger. A row whose module the gate admits derives no holder. english_emit_add_ingest_round_trip_holds PASSES (measured), so its admission row and its transitional-exception entry delete and the witness stays as a regression control. Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/explicit_witness_admission.dag | 8 -- dag/gunbc/quarantine_outside_gate_decline.dag | 83 ++++++++++++ dag/gunbc/quarantine_probe_disposition.dag | 35 +++++- .../transitional_admission_exception.dag | 1 - ...rantine_probe_disposition_witness_test.dag | 119 +++++++++++++++--- 5 files changed, 222 insertions(+), 24 deletions(-) create mode 100644 dag/gunbc/quarantine_outside_gate_decline.dag diff --git a/dag/gunbc/explicit_witness_admission.dag b/dag/gunbc/explicit_witness_admission.dag index 28bcdd4b36f..5e43612a060 100644 --- a/dag/gunbc/explicit_witness_admission.dag +++ b/dag/gunbc/explicit_witness_admission.dag @@ -281,14 +281,6 @@ data explicit_witness_admissions: List = [ reason: "THE DISCRIMINATING RED FOR #8592 (v1 infer: use each method arg's own declared parameter type, not the receiver's element_type), red on main for a reason that is not this fix's defect: the witness host builtin compile_dag_rust_emit_check executes the COMPILED stage0 mirror, and the fix lives in src/v1/04_infer.dag and src/v1/04_lookup.dag (declared_arg_types_for_method) authority only. Measured directly at 98d7147f9e (BuildBuddy 1047f203) by building gunbc from both 98d7147f9e and its parent and running each on the discriminating fixture (List.get called with a NonEmptyStr where the declared contract requires Int): BOTH binaries compile the fixture clean with zero diagnostics of any severity, byte-identical emitted output. grep on src/v1/stage0/src/v1_compiler_infer.rs confirms declared_arg_types_for_method appears in ZERO stage0 .rs files, and the pre-fix scalar_shaped_builtin_method_arg_type whitelist function is still present and still called — the #8592 commit touched only .dag authority plus 38 unrelated lines in required_regen_host.rs, and its own commit message records that required-regen's v2 self-compile refused with 11 source-annotation diagnostics, blocking the mirror regen for this exact change. This row is therefore NOT a feature gap in the fix; it is the identical authority/mirror gap independently found and quarantined the same day for the where-refinement wall — owned by the required-regen lane. THAT PRECEDENT ROW HAS SINCE DISSOLVED (2026-08-20): its 04_infer mirror was regenerated on gunbc#8619 and the row deleted in that same change, per its own trigger, so this sentence no longer names it as a live row. The precedent stands as a recorded instance of the class, not as a citation a reader can resolve. The witness function itself is written to assert the CORRECTED behavior (compile_dag_rust_emit_check must refuse) so that regenerating the mirror greens it with no edit; today, run against the committed (unmirrored) binary, it evaluates false because the ill-typed call is silently accepted. COVERAGE, checked rather than assumed (2026-08-20, per deep-ant-102): this witness's module (test.claim.method_arg_declared_contract_witness_test) is NOT under dag/test/claim/long/ and matches none of the required floor's long-home exclusion prefixes, so it IS discovered and executed by the required floor regardless of cadence — unlike the where-refinement precedent's witness file dag/test/claim/long/where_refinement_enforcement_witness_test.dag, which sits under that excluded directory and is discovered nowhere (the row itself is gone as recorded above; the fact was always about the FILE's home, and that home is unchanged by the row's dissolution). That floor execution is the row's real, present protection. Separately, this row's cadence field (QuarantineProbeExpectRed, from known_red_probe) also names it for the periodic falsifier re-probe cadence, whose consumer (falsifier.yml) was deleted in the 2026-08-15 floor cut and is not yet re-added — so the cadence tag should not be read as implying that second, currently-inert consumer.", dissolution: unbound_dissolution(description: "the 04_infer and 04_lookup stage0 mirrors are regenerated so the compiled harness contains declared_arg_types_for_method — this row deletes in that same change, promoting the unchanged witness to ordinary DiscoverySelection as the permanent regression control for #8572/#8579/#8592 (infer method args against the declared param contract, never the receiver element type)") ), - known_red_probe( - entry: "src/v2/test/claim/manual/english_emit_add_test.dag", - f: "english_emit_add_ingest_round_trip_holds", - kind: CorpusWitnessKind, - budget: FastLaneEvalBudget, - reason: "the english-language emit-ingest round trip returns false undiagnosed. Owner: the S2 emit family / behavioral-closure lane.", - dissolution: unbound_dissolution(description: "the S2 behavioral-closure lane greens it locally, then this row deletes") - ), known_red_probe( entry: "dag/test/claim/legacy_test_behavior_disposition_acceptance_test.dag", f: "legacy_test_behavior_unclassified_frontier_is_zero", diff --git a/dag/gunbc/quarantine_outside_gate_decline.dag b/dag/gunbc/quarantine_outside_gate_decline.dag new file mode 100644 index 00000000000..50d19a35efd --- /dev/null +++ b/dag/gunbc/quarantine_outside_gate_decline.dag @@ -0,0 +1,83 @@ +module gunbc.quarantine_outside_gate_decline + +import std.types { NonEmptyStr } +import v2.std.collection { List } +import v2.std.text { String } + +// QUARANTINE PROBES THE REQUIRED FLOOR NEVER PLANS, ONE ROW PER PROBE, EACH WITH ITS OWN TRIGGER. +// +// A known-red quarantine probe whose module no v2.workflow.required_floor selector admits is +// declined before execution: nothing runs it, so nothing asserts its red. These rows RECORD that +// state so gunbc.quarantine_probe_disposition can derive a holder for it -- the +// NeverRunDeclinedOutsideGate arm, whose verification standing is WitnessNeverRuns. A row here is +// NOT coverage: it is an unenforced red named in the open, and the fold only honours it while its +// module really is outside the gate (joined on the module's identity against +// required_gate_admits), so a probe inside the gate cannot be parked here. +// +// Each row names its own module and its own next-rung trigger rather than sharing a blanket one, +// so this list cannot become the place unrun reds go to be ignored (DESIGN section 5, the +// absorbing fallback). The population is the scope of the declared drop gunbc.rung_drop +// required_gate_bankruptcy, member "every witness outside the roster". +// +// MEASURED 2026-09-29 with claim_batch on main: all nine algebra_receiver probes FAIL (their +// declared red). The file_hold probe returned no verdict -- claim_batch refused its entry with +// UnimportedBareProvider RosterStale for `#filter`, a separate stale-roster defect -- so its red is +// ADMITTED, not measured, and its row says so by standing beside that receipt. +type QuarantineOutsideGateDecline { + module: String + function: String + trigger: NonEmptyStr +} + +data quarantine_outside_gate_declines: List = [ + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_callable_witness_test", + function: "shorthand_match_binder_is_callable", + trigger: "the module test.claim.algebra_receiver_callable_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_callable_witness_test", + function: "explicit_match_binder_pool_free_name_is_callable", + trigger: "the module test.claim.algebra_receiver_callable_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_callable_witness_test", + function: "shorthand_match_binder_pool_free_name_is_callable", + trigger: "the module test.claim.algebra_receiver_callable_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_callable_witness_test", + function: "explicit_match_binder_colliding_name_is_callable", + trigger: "the module test.claim.algebra_receiver_callable_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_callable_witness_test", + function: "nested_let_in_match_arm_is_callable", + trigger: "the module test.claim.algebra_receiver_callable_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_callable_witness_test", + function: "function_parameter_is_callable", + trigger: "the module test.claim.algebra_receiver_callable_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_alias_witness_test", + function: "alias_return_is_a_refusal_fixture", + trigger: "the module test.claim.algebra_receiver_alias_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_alias_witness_test", + function: "alias_field_is_a_refusal_fixture", + trigger: "the module test.claim.algebra_receiver_alias_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.algebra_receiver_alias_witness_test", + function: "explicit_initializer_is_an_acceptance_fixture", + trigger: "the module test.claim.algebra_receiver_alias_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, + QuarantineOutsideGateDecline { + module: "test.claim.file_hold_plan_refusal_probe_witness_test", + function: "the_harness_runs_and_a_clean_source_over_the_hold_store_is_clean", + trigger: "the module test.claim.file_hold_plan_refusal_probe_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr + }, +] diff --git a/dag/gunbc/quarantine_probe_disposition.dag b/dag/gunbc/quarantine_probe_disposition.dag index 9c9825aee5c..d9045ce13a8 100644 --- a/dag/gunbc/quarantine_probe_disposition.dag +++ b/dag/gunbc/quarantine_probe_disposition.dag @@ -6,6 +6,8 @@ import v2.std.algebra { Cons, Empty, fold_list } import v2.std.collection { List } import v2.std.logic { Bool } import v2.std.text { String } +import std.types { NonEmptyStr } +import gunbc.quarantine_outside_gate_decline { QuarantineOutsideGateDecline } // WHICH MECHANISM HOLDS A QUARANTINE PROBE, DERIVED TOTALLY -- NOT "IS IT IN THE ROSTER". // @@ -131,6 +133,7 @@ type QuarantineProbeHolder = | NeverRunDeclinedByHomePolicy { matched_prefix: String } | NeverRunDeclinedByLiveTreeRead { entry: String } | NeverRunPathExcluded { matched_substring: String } + | NeverRunDeclinedOutsideGate { module: String, trigger: NonEmptyStr } // THE SUBJECT: one probe, named the way the floor names it. // @@ -151,6 +154,8 @@ type QuarantineProbeHoldingFacts { home_prefixes: List live_tree_declined_entries: List path_exclusion_substrings: List + outside_gate_declines: List + gate_admits: fn(String) -> Bool } // THE ALARM IS AN ARM OF THE OUTCOME, NEVER A STABLE DISPOSITION. @@ -189,6 +194,7 @@ fn quarantine_probe_verification_standing(holder: QuarantineProbeHolder) -> Quar NeverRunDeclinedByHomePolicy { matched_prefix: p } => WitnessNeverRuns {} NeverRunDeclinedByLiveTreeRead { entry: e } => WitnessNeverRuns {} NeverRunPathExcluded { matched_substring: sub } => WitnessNeverRuns {} + NeverRunDeclinedOutsideGate { module: m, trigger: t } => WitnessNeverRuns {} } } @@ -287,18 +293,45 @@ fn quarantine_probe_holders( empty: Empty {}, cons: fn(acc, needle) { Cons { head: NeverRunPathExcluded { matched_substring: needle }, tail: acc } } ) + let outside_gate = outside_gate_holders(subject: subject, facts: facts) concat_holders( a: floor_held, b: concat_holders( a: route_held, b: concat_holders( a: home_declined, - b: concat_holders(a: live_declined, b: path_excluded) + b: concat_holders(a: live_declined, b: concat_holders(a: path_excluded, b: outside_gate)) ) ) ) } +// NeverRunDeclinedOutsideGate -- the probe has a row in gunbc.quarantine_outside_gate_decline AND +// the floor's own admission decision (supplied as gate_admits, v2.workflow.required_floor +// required_gate_admits in production) refuses the probe's authored module. BOTH halves are joined +// on identity: the row's module and function must equal the subject's, and the module must be +// outside the gate. A row naming a module the gate admits derives no holder, so a probe the +// floor would run cannot be parked here; the probe then derives NowPassing and reds the witness. +// The arm is WitnessNeverRuns: it names an unenforced red, it is never coverage. +fn outside_gate_holders(subject: QuarantineProbeSubject, facts: QuarantineProbeHoldingFacts) -> List { + let admits = facts.gate_admits + if admits(subject.module) { + Empty {} + } else { + fold_list( + xs: facts.outside_gate_declines, + empty: Empty {}, + cons: fn(acc, row) { + if row.module == subject.module && row.function == subject.function { + Cons { head: NeverRunDeclinedOutsideGate { module: row.module, trigger: row.trigger }, tail: acc } + } else { + acc + } + } + ) + } +} + fn concat_holders(a: List, b: List) -> List { match a { Empty {} => b diff --git a/dag/gunbc/rung_drop/transitional_admission_exception.dag b/dag/gunbc/rung_drop/transitional_admission_exception.dag index 0ca92d5ca1b..d2971f53c73 100644 --- a/dag/gunbc/rung_drop/transitional_admission_exception.dag +++ b/dag/gunbc/rung_drop/transitional_admission_exception.dag @@ -17,7 +17,6 @@ import gunbc.guarantee_rung { OutsideTheLadder, Mitigatable } data transitional_admission_exception_identities: List = [ "dag/test/claim/method_arg_declared_contract_witness_test.dag::w_method_arg_infers_against_declared_contract_not_element_type_test", - "src/v2/test/claim/manual/english_emit_add_test.dag::english_emit_add_ingest_round_trip_holds", "dag/test/claim/legacy_test_behavior_disposition_acceptance_test.dag::legacy_test_behavior_unclassified_frontier_is_zero", "dag/test/claim/observation_raw_print_retirement_acceptance_test.dag::observation_emit_frontier_is_zero", "dag/test/claim/long/g2_data_reference_under_selection_witness_test.dag::specimen_classifies_as_runtime_read", diff --git a/dag/test/claim/quarantine_probe_disposition_witness_test.dag b/dag/test/claim/quarantine_probe_disposition_witness_test.dag index 3d2d463372e..7aed7cb63ef 100644 --- a/dag/test/claim/quarantine_probe_disposition_witness_test.dag +++ b/dag/test/claim/quarantine_probe_disposition_witness_test.dag @@ -7,6 +7,7 @@ import gunbc.quarantine_probe_disposition { NeverRunDeclinedByHomePolicy, NeverRunDeclinedByLiveTreeRead, NeverRunPathExcluded, + NeverRunDeclinedOutsideGate, QuarantineProbeSubject, QuarantineProbeHoldingFacts, QuarantineProbeDisposition, @@ -17,18 +18,23 @@ import gunbc.quarantine_probe_disposition { quarantine_probe_disposition_holds, quarantine_probe_dispositions_all_hold, quarantine_probe_admissions, - quarantine_probe_identity + quarantine_probe_identity, + quarantine_probe_verification_standing, + QuarantineProbeVerificationStanding, + WitnessNeverRuns } import gunbc.explicit_witness_admission { ExplicitWitnessAdmission, explicit_witness_admissions } import v2.lens.module_graph { ModuleDeclarationFact, module_declaration_facts_live } import v2.workflow.floor_expected_red { floor_expected_red_roster } import v2.workflow.floor_route_gap { floor_route_gap_roster } -import v2.workflow.required_floor { long_home_prefixes } +import v2.workflow.required_floor { long_home_prefixes, required_gate_admits } +import gunbc.quarantine_outside_gate_decline { QuarantineOutsideGateDecline, quarantine_outside_gate_declines } import extdeps.filesystem.filesystem_io { Filesystem } import v2.std.algebra { Cons, Empty, fold_list } import v2.std.collection { List } import v2.std.logic { Bool } import v2.std.text { String } +import std.types { NonEmptyStr } // THE LIVE JOIN plus its discriminating controls. The model is in // gunbc.quarantine_probe_disposition; this file supplies the three live populations from the @@ -104,7 +110,9 @@ fn live_quarantine_probe_facts() -> QuarantineProbeHoldingFacts { route_gap_roster: floor_route_gap_roster(), home_prefixes: long_home_prefixes(), live_tree_declined_entries: Empty {}, - path_exclusion_substrings: Empty {} + path_exclusion_substrings: Empty {}, + outside_gate_declines: quarantine_outside_gate_declines, + gate_admits: fn(m) { required_gate_admits(module_path: m) } } } @@ -136,6 +144,7 @@ test fn every_supplied_population_is_load_bearing_on_the_live_claim() -> Bool { !quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_facts_without_expected_red()) && !quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_facts_without_route_gap()) && !quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_facts_without_home_prefixes()) + && !quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_facts_without_outside_gate()) && quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_quarantine_probe_facts()) } @@ -143,6 +152,23 @@ fn probe_no_strings() -> List { Empty {} } +fn probe_no_declines() -> List { + Empty {} +} + +fn live_facts_without_outside_gate() -> QuarantineProbeHoldingFacts { + let f = live_quarantine_probe_facts() + QuarantineProbeHoldingFacts { + expected_red_roster: f.expected_red_roster, + route_gap_roster: f.route_gap_roster, + home_prefixes: f.home_prefixes, + live_tree_declined_entries: f.live_tree_declined_entries, + path_exclusion_substrings: f.path_exclusion_substrings, + outside_gate_declines: probe_no_declines(), + gate_admits: f.gate_admits + } +} + fn live_facts_without_expected_red() -> QuarantineProbeHoldingFacts { let f = live_quarantine_probe_facts() QuarantineProbeHoldingFacts { @@ -150,7 +176,9 @@ fn live_facts_without_expected_red() -> QuarantineProbeHoldingFacts { route_gap_roster: f.route_gap_roster, home_prefixes: f.home_prefixes, live_tree_declined_entries: f.live_tree_declined_entries, - path_exclusion_substrings: f.path_exclusion_substrings + path_exclusion_substrings: f.path_exclusion_substrings, + outside_gate_declines: f.outside_gate_declines, + gate_admits: f.gate_admits } } @@ -161,7 +189,9 @@ fn live_facts_without_route_gap() -> QuarantineProbeHoldingFacts { route_gap_roster: probe_no_strings(), home_prefixes: f.home_prefixes, live_tree_declined_entries: f.live_tree_declined_entries, - path_exclusion_substrings: f.path_exclusion_substrings + path_exclusion_substrings: f.path_exclusion_substrings, + outside_gate_declines: f.outside_gate_declines, + gate_admits: f.gate_admits } } @@ -172,7 +202,9 @@ fn live_facts_without_home_prefixes() -> QuarantineProbeHoldingFacts { route_gap_roster: f.route_gap_roster, home_prefixes: probe_no_strings(), live_tree_declined_entries: f.live_tree_declined_entries, - path_exclusion_substrings: f.path_exclusion_substrings + path_exclusion_substrings: f.path_exclusion_substrings, + outside_gate_declines: f.outside_gate_declines, + gate_admits: f.gate_admits } } @@ -198,7 +230,9 @@ fn probe_fixture_no_facts() -> QuarantineProbeHoldingFacts { route_gap_roster: Empty {}, home_prefixes: Empty {}, live_tree_declined_entries: Empty {}, - path_exclusion_substrings: Empty {} + path_exclusion_substrings: Empty {}, + outside_gate_declines: probe_no_declines(), + gate_admits: fn(m) { false } } } @@ -208,7 +242,9 @@ fn facts_with_expected_red() -> QuarantineProbeHoldingFacts { route_gap_roster: Empty {}, home_prefixes: Empty {}, live_tree_declined_entries: Empty {}, - path_exclusion_substrings: Empty {} + path_exclusion_substrings: Empty {}, + outside_gate_declines: probe_no_declines(), + gate_admits: fn(m) { false } } } @@ -218,7 +254,9 @@ fn facts_with_route_gap() -> QuarantineProbeHoldingFacts { route_gap_roster: Cons { head: probe_fixture_identity(), tail: Empty {} }, home_prefixes: Empty {}, live_tree_declined_entries: Empty {}, - path_exclusion_substrings: Empty {} + path_exclusion_substrings: Empty {}, + outside_gate_declines: probe_no_declines(), + gate_admits: fn(m) { false } } } @@ -228,7 +266,9 @@ fn facts_with_home_prefix() -> QuarantineProbeHoldingFacts { route_gap_roster: Empty {}, home_prefixes: Cons { head: "test.claim.synthetic_", tail: Empty {} }, live_tree_declined_entries: Empty {}, - path_exclusion_substrings: Empty {} + path_exclusion_substrings: Empty {}, + outside_gate_declines: probe_no_declines(), + gate_admits: fn(m) { false } } } @@ -238,7 +278,9 @@ fn facts_with_live_tree_decline() -> QuarantineProbeHoldingFacts { route_gap_roster: Empty {}, home_prefixes: Empty {}, live_tree_declined_entries: Cons { head: probe_fixture_entry, tail: Empty {} }, - path_exclusion_substrings: Empty {} + path_exclusion_substrings: Empty {}, + outside_gate_declines: probe_no_declines(), + gate_admits: fn(m) { false } } } @@ -248,7 +290,9 @@ fn facts_with_path_exclusion() -> QuarantineProbeHoldingFacts { route_gap_roster: Empty {}, home_prefixes: Empty {}, live_tree_declined_entries: Empty {}, - path_exclusion_substrings: Cons { head: "test/claim/synthetic_", tail: Empty {} } + path_exclusion_substrings: Cons { head: "test/claim/synthetic_", tail: Empty {} }, + outside_gate_declines: probe_no_declines(), + gate_admits: fn(m) { false } } } @@ -258,7 +302,9 @@ fn facts_with_two_holders() -> QuarantineProbeHoldingFacts { route_gap_roster: Cons { head: probe_fixture_identity(), tail: Empty {} }, home_prefixes: Empty {}, live_tree_declined_entries: Empty {}, - path_exclusion_substrings: Empty {} + path_exclusion_substrings: Empty {}, + outside_gate_declines: probe_no_declines(), + gate_admits: fn(m) { false } } } @@ -292,6 +338,10 @@ fn quarantine_probe_holder_eq(a: QuarantineProbeHolder, b: QuarantineProbeHolder NeverRunPathExcluded { matched_substring: sb } => sa == sb _ => false } + NeverRunDeclinedOutsideGate { module: ma, trigger: ta } => match b { + NeverRunDeclinedOutsideGate { module: mb, trigger: tb } => ma == mb && (ta as String) == (tb as String) + _ => false + } } } @@ -367,7 +417,9 @@ test fn a_roster_row_that_merely_contains_the_identity_does_not_hold_it() -> Boo route_gap_roster: Empty {}, home_prefixes: Empty {}, live_tree_declined_entries: Empty {}, - path_exclusion_substrings: Empty {} + path_exclusion_substrings: Empty {}, + outside_gate_declines: probe_no_declines(), + gate_admits: fn(m) { false } } disposition_is_now_passing(disposition: fixture_disposition(facts: near_miss)) && disposition_is_held_by(disposition: fixture_disposition(facts: facts_with_expected_red()), expected: FloorExpectedRedHeld {}) @@ -396,3 +448,42 @@ test fn the_live_tree_declaration_read_discriminates() -> Bool { entry_declares_reads_live_tree_for_selection(entry: "dag/test/claim/legacy_test_behavior_disposition_acceptance_test.dag") && !entry_declares_reads_live_tree_for_selection(entry: "dag/test/claim/method_arg_declared_contract_witness_test.dag") } + +// THE OUTSIDE-GATE ARM HOLDS ONLY OUTSIDE THE GATE, AND ONLY AS NEVER-RUN. A decline row for the +// fixture probe holds it while the supplied gate refuses the module, and the holder's standing is +// WitnessNeverRuns -- an unenforced red, never coverage. The SAME row under a gate that admits the +// module derives no holder, so the probe reads NowPassing: a probe the floor would execute cannot +// be parked here. The pair is the discriminating control for the join on module identity. +fn probe_fixture_outside_gate_row() -> List { + [ + QuarantineOutsideGateDecline { + module: probe_fixture_module, + function: probe_fixture_function, + trigger: "fixture: its module entering the required gate" as NonEmptyStr + }, + ] +} + +fn facts_with_outside_gate(gate_admits_fixture: Bool) -> QuarantineProbeHoldingFacts { + QuarantineProbeHoldingFacts { + expected_red_roster: Empty {}, + route_gap_roster: Empty {}, + home_prefixes: Empty {}, + live_tree_declined_entries: Empty {}, + path_exclusion_substrings: Empty {}, + outside_gate_declines: probe_fixture_outside_gate_row(), + gate_admits: fn(m) { gate_admits_fixture && m == probe_fixture_module } + } +} + +test fn an_outside_gate_row_holds_only_while_the_gate_refuses_the_module_and_only_as_never_run() -> Bool { + let outside = fixture_disposition(facts: facts_with_outside_gate(gate_admits_fixture: false)) + let inside = fixture_disposition(facts: facts_with_outside_gate(gate_admits_fixture: true)) + (match outside { + HeldByExactlyOne { identity: _, holder: h } => + (match h { NeverRunDeclinedOutsideGate { module: m, trigger: _ } => m == probe_fixture_module _ => false }) + && (match quarantine_probe_verification_standing(holder: h) { WitnessNeverRuns => true _ => false }) + _ => false + }) + && disposition_is_now_passing(disposition: inside) +} From 1479f862a2ead296797216a5eef31f33feb86dff Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 29 Sep 2026 18:55:18 +0000 Subject: [PATCH 2/4] Quarantine: file_hold probe leaves the quarantine; it passes on main (its dissolution, #12132, landed) The #filter bare-provider refusal that hid its verdict was already retired by #12609. On main 785934a38b6 the probe PASSES, which its own dissolution names as the row's deletion condition. The nine algebra_receiver probes remain red (re-measured on the same main). Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/explicit_witness_admission.dag | 8 -------- dag/gunbc/quarantine_outside_gate_decline.dag | 11 ++--------- 2 files changed, 2 insertions(+), 17 deletions(-) diff --git a/dag/gunbc/explicit_witness_admission.dag b/dag/gunbc/explicit_witness_admission.dag index 5e43612a060..c8b40ebe48b 100644 --- a/dag/gunbc/explicit_witness_admission.dag +++ b/dag/gunbc/explicit_witness_admission.dag @@ -457,14 +457,6 @@ data explicit_witness_admissions: List = [ reason: "Admitted RED whose cited boundary NO LONGER EXISTS: gunbc#10245 replaced the witness entry import closure with a caller-declared pool, so the population is exactly origin_probe_subject_files, and run_direct_rust_door_emit_write_compile_smoke lives in dag/test/claim/direct_rust_door_write_compile_witness_test.dag, which that subject does not name. The cause is the declared subject and is decidable by reading it; it is neither the marshal nor the reachability horizon. Owner: witness-evidence-lifecycle lane.", dissolution: unbound_dissolution(description: "a population authority enumerates fn-arrow declarations repository-wide within this lane's budget, so the direct-door smoke declaration is in the probe's subject without the witness naming its file one by one; this witness greens and this row deletes. Naming that one file in origin_probe_subject_files would also green it and is NOT the trigger: it would green the row without the capability the row stands for") ), - known_red_probe( - entry: "dag/test/claim/file_hold_plan_refusal_probe_witness_test.dag", - f: "the_harness_runs_and_a_clean_source_over_the_hold_store_is_clean", - kind: CorpusWitnessKind, - budget: FastLaneEvalBudget, - reason: "RED ON THIS STACK FOR A MAIN-WIDE COMPILER DEFECT, NOT FOR THE HOLD STORE. The claim asserts a census of the hold-store harness has zero blocking rows. Bisected to 9945e9268f1 (its parent is clean): cas_slot_keys began importing std.decimal, whose closure reaches std.measure through std.bytes and std.integer, and the census's measured compile (gunbc.type_ref_hit_ne_bind_measure) charges std.measure's own unit variants, passed as phantom type arguments in Measure, as missing imports -- 38 blocking UnresolvedType rows here, and 147 for a source importing std.measure alone on plain main. The unmeasured resolve admits the same leaves, so the two routes of one compiler disagree; the measure is the wrong side. Kept enrolled rather than deleted or loosened: it is the discriminating red that shows the census is not yet fit for any closure reaching std.measure.", - dissolution: unbound_dissolution(description: "the measured compile's binding authority (v1.compiler.infer_env type_ref_measure_binding_authority) treats a zero-payload variant as bound exactly when the observed unit_variant_index keys it, and its regenerated stage0 mirror is what claim_batch executes -- SUFFICIENT FOR a census whose closure reaches std.measure to report zero blocking UnresolvedType rows for std.measure's own unit variants. Delivered by gunbc#12132; this row deletes when #12132 is merged into this branch and the claim reads green."), - ), source_root_ingest_gate_admitted_witness( entry: "src/v2/test/claim/self_host/compiler_closure_emit_from_ingest_test.dag", f: "compiler_closure_scoped_ingest_module_count_ok_holds", diff --git a/dag/gunbc/quarantine_outside_gate_decline.dag b/dag/gunbc/quarantine_outside_gate_decline.dag index 50d19a35efd..937fe5b346f 100644 --- a/dag/gunbc/quarantine_outside_gate_decline.dag +++ b/dag/gunbc/quarantine_outside_gate_decline.dag @@ -19,10 +19,8 @@ import v2.std.text { String } // absorbing fallback). The population is the scope of the declared drop gunbc.rung_drop // required_gate_bankruptcy, member "every witness outside the roster". // -// MEASURED 2026-09-29 with claim_batch on main: all nine algebra_receiver probes FAIL (their -// declared red). The file_hold probe returned no verdict -- claim_batch refused its entry with -// UnimportedBareProvider RosterStale for `#filter`, a separate stale-roster defect -- so its red is -// ADMITTED, not measured, and its row says so by standing beside that receipt. +// MEASURED 2026-09-29 with claim_batch on main 785934a38b6: all nine probes rostered here FAIL +// (their declared red). type QuarantineOutsideGateDecline { module: String function: String @@ -75,9 +73,4 @@ data quarantine_outside_gate_declines: List = [ function: "explicit_initializer_is_an_acceptance_fixture", trigger: "the module test.claim.algebra_receiver_alias_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr }, - QuarantineOutsideGateDecline { - module: "test.claim.file_hold_plan_refusal_probe_witness_test", - function: "the_harness_runs_and_a_clean_source_over_the_hold_store_is_clean", - trigger: "the module test.claim.file_hold_plan_refusal_probe_witness_test is admitted by v2.workflow.required_floor required_gate_admits (a family prefix or an authored-module row priced by the floor's cost receipt), after which the floor executes this probe and it moves to v2.workflow.floor_expected_red; or a recorded operator decision to keep the module outside the gate, which this row then cites" as NonEmptyStr - }, ] From 0022ff06b5220ee003bc786c339b62d6bf226623 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 30 Sep 2026 03:05:38 +0000 Subject: [PATCH 3/4] quarantine witness: load-bearing claim reads every population's holder off one live evaluation (was five live folds, 808,294 eval steps) Co-Authored-By: Claude Opus 5.5 (1M context) --- ...rantine_probe_disposition_witness_test.dag | 99 +++++++------------ 1 file changed, 34 insertions(+), 65 deletions(-) diff --git a/dag/test/claim/quarantine_probe_disposition_witness_test.dag b/dag/test/claim/quarantine_probe_disposition_witness_test.dag index 7aed7cb63ef..d4c817ffd57 100644 --- a/dag/test/claim/quarantine_probe_disposition_witness_test.dag +++ b/dag/test/claim/quarantine_probe_disposition_witness_test.dag @@ -16,6 +16,7 @@ import gunbc.quarantine_probe_disposition { QuarantineProbeHeldByMoreThanOne, quarantine_probe_disposition, quarantine_probe_disposition_holds, + quarantine_probe_dispositions, quarantine_probe_dispositions_all_hold, quarantine_probe_admissions, quarantine_probe_identity, @@ -132,20 +133,40 @@ test fn every_quarantine_probe_derives_exactly_one_disposition() -> Bool { ) } -// THE LIVE CLAIM IS NOT VACUOUS, PROVEN BY MUTATION RATHER THAN ASSERTED. Each of the three -// supplied live populations is dropped in turn and the live claim must go RED, then the unmutated -// fold must go green. Without this, a fold that answered "held" for everything -- or a join that -// silently matched nothing -- would pass the live claim exactly as it does now. Measured on -// 967b5bc1b92: dropping the expected-red roster unholds 5 probes, the route-gap roster 6, the -// home prefixes 7. The live-tree and path-exclusion axes are not mutated here because the -// required floor no longer has a live-tree decline and neither arm holds a live row. +// THE LIVE CLAIM IS NOT VACUOUS: every supplied live population holds at least one live probe. +// Under exactly-one holding, dropping a population turns every probe it solely holds into +// NowPassing, so "removing P reds the live claim" IS "some live probe's one holder is P". That +// equivalence is read off ONE live evaluation rather than re-folding the whole join once per +// dropped population: the earlier mutation form paid the live join five times and was refused at +// 808,294 eval steps (CI run 36656467027), cost that bought no discrimination the single reading +// lacks (DESIGN section 3, a witness discriminates at one interface). The mutation half of the +// equivalence -- that a dropped population really does unhold -- is asserted on supplied facts by +// the fixture claims below (a_probe_held_by_nothing_is_an_alarm_and_does_not_hold, and the +// outside-gate pair), where it costs nothing. The live-tree and path-exclusion axes are not +// required here because the required floor no longer has a live-tree decline and neither arm +// holds a live row. +fn live_dispositions() -> List { + quarantine_probe_dispositions(subjects: live_quarantine_probe_subjects(), facts: live_quarantine_probe_facts()) +} + +fn disposition_holds_by(d: QuarantineProbeDisposition, kind: fn(QuarantineProbeHolder) -> Bool) -> Bool { + match d { + HeldByExactlyOne { identity: _, holder: h } => kind(h) + _ => false + } +} + +fn some_disposition_holds_by(ds: List, kind: fn(QuarantineProbeHolder) -> Bool) -> Bool { + fold_list(xs: ds, empty: false, cons: fn(acc, d) { acc || disposition_holds_by(d: d, kind: kind) }) +} + test fn every_supplied_population_is_load_bearing_on_the_live_claim() -> Bool { - let subjects = live_quarantine_probe_subjects() - !quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_facts_without_expected_red()) - && !quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_facts_without_route_gap()) - && !quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_facts_without_home_prefixes()) - && !quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_facts_without_outside_gate()) - && quarantine_probe_dispositions_all_hold(subjects: subjects, facts: live_quarantine_probe_facts()) + let ds = live_dispositions() + fold_list(xs: ds, empty: true, cons: fn(acc, d) { acc && quarantine_probe_disposition_holds(disposition: d) }) + && some_disposition_holds_by(ds: ds, kind: fn(h) { match h { FloorExpectedRedHeld => true _ => false } }) + && some_disposition_holds_by(ds: ds, kind: fn(h) { match h { RouteGapHeldNoVerdict => true _ => false } }) + && some_disposition_holds_by(ds: ds, kind: fn(h) { match h { NeverRunDeclinedByHomePolicy { matched_prefix: _ } => true _ => false } }) + && some_disposition_holds_by(ds: ds, kind: fn(h) { match h { NeverRunDeclinedOutsideGate { module: _, trigger: _ } => true _ => false } }) } fn probe_no_strings() -> List { @@ -156,58 +177,6 @@ fn probe_no_declines() -> List { Empty {} } -fn live_facts_without_outside_gate() -> QuarantineProbeHoldingFacts { - let f = live_quarantine_probe_facts() - QuarantineProbeHoldingFacts { - expected_red_roster: f.expected_red_roster, - route_gap_roster: f.route_gap_roster, - home_prefixes: f.home_prefixes, - live_tree_declined_entries: f.live_tree_declined_entries, - path_exclusion_substrings: f.path_exclusion_substrings, - outside_gate_declines: probe_no_declines(), - gate_admits: f.gate_admits - } -} - -fn live_facts_without_expected_red() -> QuarantineProbeHoldingFacts { - let f = live_quarantine_probe_facts() - QuarantineProbeHoldingFacts { - expected_red_roster: probe_no_strings(), - route_gap_roster: f.route_gap_roster, - home_prefixes: f.home_prefixes, - live_tree_declined_entries: f.live_tree_declined_entries, - path_exclusion_substrings: f.path_exclusion_substrings, - outside_gate_declines: f.outside_gate_declines, - gate_admits: f.gate_admits - } -} - -fn live_facts_without_route_gap() -> QuarantineProbeHoldingFacts { - let f = live_quarantine_probe_facts() - QuarantineProbeHoldingFacts { - expected_red_roster: f.expected_red_roster, - route_gap_roster: probe_no_strings(), - home_prefixes: f.home_prefixes, - live_tree_declined_entries: f.live_tree_declined_entries, - path_exclusion_substrings: f.path_exclusion_substrings, - outside_gate_declines: f.outside_gate_declines, - gate_admits: f.gate_admits - } -} - -fn live_facts_without_home_prefixes() -> QuarantineProbeHoldingFacts { - let f = live_quarantine_probe_facts() - QuarantineProbeHoldingFacts { - expected_red_roster: f.expected_red_roster, - route_gap_roster: f.route_gap_roster, - home_prefixes: probe_no_strings(), - live_tree_declined_entries: f.live_tree_declined_entries, - path_exclusion_substrings: f.path_exclusion_substrings, - outside_gate_declines: f.outside_gate_declines, - gate_admits: f.gate_admits - } -} - data probe_fixture_module: String = "test.claim.synthetic_quarantine_probe_witness" data probe_fixture_entry: String = "dag/test/claim/synthetic_quarantine_probe_witness_test.dag" data probe_fixture_function: String = "synthetic_probe_holds" From 42cbe999fa1814028aaa056c3c9ab9ed1ba3e91e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 30 Sep 2026 03:46:10 +0000 Subject: [PATCH 4/4] quarantine witness: key both joins (788k -> 43.6k eval steps per live claim); regenerate the rung-drop projection Chain re-derived from the budget refusal (808,294 steps, CI run 36656467027), measured with claim_batch: the corpus census host read is 10 steps; live subject derivation was 677,277 because module_for_entry folded the whole census once per admission row, and the disposition fold scanned each roster once per probe. Now: admission entries keyed once, the census read over the entries' own directories (derived, never authored) in one pass; the two rosters keyed once per population in quarantine_probe_dispositions. Both live claims 43.6k steps; all nine claims PASS; emptying the outside-gate roster reds both live claims. docs/design-rung-drops.md regenerated via tools.docs_projection_gate regen: english_emit_add leaves the transitional_admission_exception population. Co-Authored-By: Claude Opus 5.5 (1M context) --- dag/gunbc/quarantine_probe_disposition.dag | 51 +++++++++++++++-- ...rantine_probe_disposition_witness_test.dag | 57 +++++++++++++------ docs/design-rung-drops.md | 2 +- 3 files changed, 85 insertions(+), 25 deletions(-) diff --git a/dag/gunbc/quarantine_probe_disposition.dag b/dag/gunbc/quarantine_probe_disposition.dag index d9045ce13a8..85764c30138 100644 --- a/dag/gunbc/quarantine_probe_disposition.dag +++ b/dag/gunbc/quarantine_probe_disposition.dag @@ -3,8 +3,9 @@ module gunbc.quarantine_probe_disposition import gunbc.explicit_witness_admission { ExplicitWitnessAdmission } import std.witness_admission { WitnessConsumerCadence, QuarantineProbeExpectRed } import v2.std.algebra { Cons, Empty, fold_list } -import v2.std.collection { List } +import v2.std.collection { List, Map, empty_map, map_insert, map_lookup } import v2.std.logic { Bool } +import v2.std.optional { Absent, Present } import v2.std.text { String } import std.types { NonEmptyStr } import gunbc.quarantine_outside_gate_decline { QuarantineOutsideGateDecline } @@ -206,6 +207,34 @@ fn quarantine_probe_subject_identity(subject: QuarantineProbeSubject) -> String quarantine_probe_identity(module: subject.module, function: subject.function) } +// THE TWO QUALIFIED-NAME ROSTERS, KEYED ONCE PER POPULATION. The join is still exact identity +// (a key either equals the probe's identity or is absent), but it is keyed rather than scanned: +// scanning each roster once per probe made the fold rows x roster, and the live claim paid that +// product on every run (DESIGN section 6, bare minimum cost). quarantine_probe_dispositions +// builds the index once and every subject reads it. +type QuarantineProbeRosterIndex { + expected_red: Map + route_gap: Map +} + +fn exact_key_set(population: List) -> Map { + fold_list(xs: population, empty: empty_map(), cons: fn(acc, row) { map_insert(m: acc, key: row, value: true) }) +} + +fn quarantine_probe_roster_index(facts: QuarantineProbeHoldingFacts) -> QuarantineProbeRosterIndex { + QuarantineProbeRosterIndex { + expected_red: exact_key_set(population: facts.expected_red_roster), + route_gap: exact_key_set(population: facts.route_gap_roster) + } +} + +fn exact_key_member(needle: String, keys: Map) -> Bool { + match map_lookup(m: keys, key: needle) { + Present { value: _ } => true + Absent => false + } +} + // EXACT MEMBERSHIP, NEVER CONTAINMENT. Both populations joined this way -- the two qualified-name // rosters and the entry-path list -- are keyed by full identity and joined by EQUALITY. A probe // whose function name is a prefix or a substring of an enrolled one is NOT held by it, and a @@ -262,17 +291,18 @@ fn first_matching_substring(entry: String, substrings: List) -> List List { let identity = quarantine_probe_subject_identity(subject: subject) let floor_held = - if exact_member(needle: identity, population: facts.expected_red_roster) { + if exact_key_member(needle: identity, keys: index.expected_red) { Cons { head: FloorExpectedRedHeld {}, tail: Empty {} } } else { Empty {} } let route_held = - if exact_member(needle: identity, population: facts.route_gap_roster) { + if exact_key_member(needle: identity, keys: index.route_gap) { Cons { head: RouteGapHeldNoVerdict {}, tail: Empty {} } } else { Empty {} @@ -346,7 +376,15 @@ fn quarantine_probe_disposition( subject: QuarantineProbeSubject, facts: QuarantineProbeHoldingFacts ) -> QuarantineProbeDisposition { - let holders = quarantine_probe_holders(subject: subject, facts: facts) + quarantine_probe_disposition_indexed(subject: subject, facts: facts, index: quarantine_probe_roster_index(facts: facts)) +} + +fn quarantine_probe_disposition_indexed( + subject: QuarantineProbeSubject, + facts: QuarantineProbeHoldingFacts, + index: QuarantineProbeRosterIndex +) -> QuarantineProbeDisposition { + let holders = quarantine_probe_holders(subject: subject, facts: facts, index: index) match holders { Empty {} => QuarantineProbeNowPassing { identity: quarantine_probe_subject_identity(subject: subject), @@ -379,11 +417,12 @@ fn quarantine_probe_dispositions( subjects: List, facts: QuarantineProbeHoldingFacts ) -> List { + let index = quarantine_probe_roster_index(facts: facts) fold_list( xs: subjects, empty: Empty {}, cons: fn(acc, subject) { - Cons { head: quarantine_probe_disposition(subject: subject, facts: facts), tail: acc } + Cons { head: quarantine_probe_disposition_indexed(subject: subject, facts: facts, index: index), tail: acc } } ) } diff --git a/dag/test/claim/quarantine_probe_disposition_witness_test.dag b/dag/test/claim/quarantine_probe_disposition_witness_test.dag index d4c817ffd57..f51671a38dc 100644 --- a/dag/test/claim/quarantine_probe_disposition_witness_test.dag +++ b/dag/test/claim/quarantine_probe_disposition_witness_test.dag @@ -32,7 +32,8 @@ import v2.workflow.required_floor { long_home_prefixes, required_gate_admits } import gunbc.quarantine_outside_gate_decline { QuarantineOutsideGateDecline, quarantine_outside_gate_declines } import extdeps.filesystem.filesystem_io { Filesystem } import v2.std.algebra { Cons, Empty, fold_list } -import v2.std.collection { List } +import v2.std.collection { List, Map, empty_map, map_insert, map_lookup } +import v2.std.optional { Absent, Present } import v2.std.logic { Bool } import v2.std.text { String } import std.types { NonEmptyStr } @@ -56,10 +57,6 @@ import std.types { NonEmptyStr } // alarm, and held-by-two is shown to refuse. The controls therefore prove the fold DISCRIMINATES // rather than merely agreeing with today's tree. -fn witness_pool_roots() -> List { - ["dag", "src/v2"] -} - // THE ENTRY-PATH -> AUTHORED-MODULE JOIN, from the same declaration the floor reads. // // A path-shaped guess is NOT available here and the corpus proves it: the admission entry @@ -67,44 +64,68 @@ fn witness_pool_roots() -> List { // dropping a segment and a suffix, and dag/test/claim/self_host_03_normalize_behavioral_witness_test.dag // declares test.claim.self_host_03_normalize_behavioral_witness. Deriving the identity from the // path would silently miss the roster this fold joins against, and a miss reads as an alarm. -fn module_for_entry(facts: List, entry: String) -> String { +// ONE PASS OVER THE CORPUS CENSUS. The admission entries are keyed first, then the census is +// read once and only the entries' own rows are kept, so each subject reads its module by key. +// The earlier shape folded the whole census once per admission row -- rows x corpus, 677,277 +// eval steps of the live claim's ~788k measured with claim_batch -- to name a few dozen modules +// (DESIGN section 6, bare minimum cost). +fn entry_modules(facts: List, rows: List) -> Map { + let wanted = fold_list(xs: rows, empty: empty_map(), cons: fn(acc, row) { map_insert(m: acc, key: row.witness.entry, value: true) }) fold_list( xs: facts, - empty: "", - cons: fn(acc, fact) { if fact.path == entry { fact.module } else { acc } } + empty: empty_map(), + cons: fn(acc, fact) { + match map_lookup(m: wanted, key: fact.path) { + Present { value: _ } => map_insert(m: acc, key: fact.path, value: fact.module) + Absent => acc + } + } ) } -// `LiveTreeDisposition` still owns affected-set selection eligibility after the required-floor -// decline is deleted. This scan exercises that surviving declaration question only; it does not -// predict whether the interpreter can execute the witness hermetically. fn entry_declares_reads_live_tree_for_selection(entry: String) -> Bool { let source = filesystem_read(path: entry).content source.contains("LiveTreeDisposition") && source.contains("ReadsLiveTree") } fn subject_for_admission( - facts: List, + modules: Map, row: ExplicitWitnessAdmission ) -> QuarantineProbeSubject { QuarantineProbeSubject { - module: module_for_entry(facts: facts, entry: row.witness.entry), + module: match map_lookup(m: modules, key: row.witness.entry) { + Present { value: m } => m + Absent => "" + }, entry: row.witness.entry, function: row.witness.function } } +// THE CENSUS IS READ OVER THE ENTRIES' OWN DIRECTORIES, not the whole pool: the only rows the +// join keeps are the admission entries', so scanning the rest of dag and src/v2 was work no +// consumer read. The roots are derived from the entries (each entry's parent directory, once), +// never authored, so an admission added anywhere is covered by construction; an entry whose +// declaration is not found still derives an empty module and reds the live claim as NowPassing. +fn entry_parent_dir(entry: String) -> String { + let parts = split(s: entry, delimiter: "/") + join(parts |> take(n: count(parts) - 1), "/") +} + +fn entry_census_roots(rows: List) -> List { + sorted_map_keys(fold_list(xs: rows, empty: empty_map(), cons: fn(acc, row) { map_insert(m: acc, key: entry_parent_dir(entry: row.witness.entry), value: true) })) +} + fn live_quarantine_probe_subjects() -> List { - let facts = module_declaration_facts_live(pool_roots: witness_pool_roots()) + let rows = quarantine_probe_admissions(rows: explicit_witness_admissions) + let modules = entry_modules(facts: module_declaration_facts_live(pool_roots: entry_census_roots(rows: rows)), rows: rows) fold_list( - xs: quarantine_probe_admissions(rows: explicit_witness_admissions), + xs: rows, empty: Empty {}, - cons: fn(acc, row) { Cons { head: subject_for_admission(facts: facts, row: row), tail: acc } } + cons: fn(acc, row) { Cons { head: subject_for_admission(modules: modules, row: row), tail: acc } } ) } -// Declaring ReadsLiveTree still controls affected-set eligibility, but no longer declines -// execution at the required-floor root. This holder population therefore has no live rows. fn live_quarantine_probe_facts() -> QuarantineProbeHoldingFacts { QuarantineProbeHoldingFacts { expected_red_roster: floor_expected_red_roster(), diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 22a709e6079..85fb5dafaa8 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -224,7 +224,7 @@ Transitive determinism reachability over the fn-arrow call graph: RUNG DROP, mec ### admission rows on falsifier-family cadences with no scheduled route, awaiting transition to a cadence that executes — declared 2026-09-08 -admission rows on falsifier-family cadences with no scheduled route, awaiting transition to a cadence that executes: RUNG DROP, mitigatable -> outside the ladder (lost as a passenger of .github/workflows/falsifier.yml, deleted at 611fd02770 (#8283)). Population: dag/test/claim/method_arg_declared_contract_witness_test.dag::w_method_arg_infers_against_declared_contract_not_element_type_test, src/v2/test/claim/manual/english_emit_add_test.dag::english_emit_add_ingest_round_trip_holds, dag/test/claim/legacy_test_behavior_disposition_acceptance_test.dag::legacy_test_behavior_unclassified_frontier_is_zero, dag/test/claim/observation_raw_print_retirement_acceptance_test.dag::observation_emit_frontier_is_zero, dag/test/claim/long/g2_data_reference_under_selection_witness_test.dag::specimen_classifies_as_runtime_read, dag/test/claim/long/g2_data_reference_under_selection_witness_test.dag::specimen_does_not_classify_as_local_read, dag/test/claim/source_integration_proof_kernel_acceptance_test.dag::witness_p1_proof_kernel_acceptance_contract_holds, dag/test/claim/namespace_reference_derived_closure_acceptance_test.dag::witness_namespace_reference_derived_closure_closing_contract_holds, src/v2/test/claim/long/direct_rust_door_production_group_test.dag::direct_rust_door_production_group_closing_expectation_holds, dag/test/claim/self_host_use_site_verdict_behavioral_witness_test.dag::self_host_use_site_verdict_behavioral_receipt_holds, dag/test/claim/self_host_body_producer_behavioral_witness_test.dag::self_host_body_producer_behavioral_receipt_holds, dag/test/claim/self_host_discovery_enumeration_behavioral_witness_test.dag::self_host_discovery_enumeration_behavioral_receipt_holds, dag/test/claim/self_host_target_carriers_behavioral_witness_test.dag::self_host_target_carriers_behavioral_receipt_holds, dag/test/claim/self_host_03_normalize_behavioral_witness_test.dag::self_host_03_normalize_behavioral_receipt_holds, src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag::witness_live_scope_fixture_origin_discoverable_in_entry_closure_reds, src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag::witness_live_structural_fixture_mint_site_discovered_reds, src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag::witness_ingest_mint_surface_requires_call_occurrence_frontier_reds, src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag::witness_direct_door_smoke_requires_closure_or_call_occurrence_frontier_reds, src/v2/test/claim/self_host/compiler_closure_emit_from_ingest_test.dag::compiler_closure_scoped_ingest_module_count_ok_holds, src/v2/test/claim/self_host/compiler_closure_emit_from_ingest_test.dag::compiler_closure_ingest_overflow_refuses_never_empty_holds, src/v2/test/claim/self_host/compiler_closure_ingest_boundary_witness_test.dag::compiler_closure_ingest_boundary_exact_cap_transport_holds, src/v2/test/claim/long/infer_transform_binary_infix_witness_test.dag::infer_transform_add_vertical_witness_holds. Restored when: each named identity carries a cadence with a live scheduled route, at which point each row above is removed from transitional_admission_exception_identities and the identity's exception in explicit_witness_admission.dag is deleted (the gate consumes the list, so removing from the list retires the exception). The cadence category those routes need is gunbc.rung_drop.shared_capability missing_cadence_category; the remainder is the per-identity migration onto a live route. Waiters whose remaining unsatisfied condition is only that capability retire together. When the category fires and any named identity still lacks a live scheduled route, this identity is removed from missing_cadence_category.waiter_identities in the SAME change as those retirements (delist, not SplitRetirement) and this row stays Standing until every named identity has that route. If every named identity already has a live scheduled route when the category fires, retire with the enrolled set. +admission rows on falsifier-family cadences with no scheduled route, awaiting transition to a cadence that executes: RUNG DROP, mitigatable -> outside the ladder (lost as a passenger of .github/workflows/falsifier.yml, deleted at 611fd02770 (#8283)). Population: dag/test/claim/method_arg_declared_contract_witness_test.dag::w_method_arg_infers_against_declared_contract_not_element_type_test, dag/test/claim/legacy_test_behavior_disposition_acceptance_test.dag::legacy_test_behavior_unclassified_frontier_is_zero, dag/test/claim/observation_raw_print_retirement_acceptance_test.dag::observation_emit_frontier_is_zero, dag/test/claim/long/g2_data_reference_under_selection_witness_test.dag::specimen_classifies_as_runtime_read, dag/test/claim/long/g2_data_reference_under_selection_witness_test.dag::specimen_does_not_classify_as_local_read, dag/test/claim/source_integration_proof_kernel_acceptance_test.dag::witness_p1_proof_kernel_acceptance_contract_holds, dag/test/claim/namespace_reference_derived_closure_acceptance_test.dag::witness_namespace_reference_derived_closure_closing_contract_holds, src/v2/test/claim/long/direct_rust_door_production_group_test.dag::direct_rust_door_production_group_closing_expectation_holds, dag/test/claim/self_host_use_site_verdict_behavioral_witness_test.dag::self_host_use_site_verdict_behavioral_receipt_holds, dag/test/claim/self_host_body_producer_behavioral_witness_test.dag::self_host_body_producer_behavioral_receipt_holds, dag/test/claim/self_host_discovery_enumeration_behavioral_witness_test.dag::self_host_discovery_enumeration_behavioral_receipt_holds, dag/test/claim/self_host_target_carriers_behavioral_witness_test.dag::self_host_target_carriers_behavioral_receipt_holds, dag/test/claim/self_host_03_normalize_behavioral_witness_test.dag::self_host_03_normalize_behavioral_receipt_holds, src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag::witness_live_scope_fixture_origin_discoverable_in_entry_closure_reds, src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag::witness_live_structural_fixture_mint_site_discovered_reds, src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag::witness_ingest_mint_surface_requires_call_occurrence_frontier_reds, src/v2/test/claim/long/production_qualification_origin_probe_witness_test.dag::witness_direct_door_smoke_requires_closure_or_call_occurrence_frontier_reds, src/v2/test/claim/self_host/compiler_closure_emit_from_ingest_test.dag::compiler_closure_scoped_ingest_module_count_ok_holds, src/v2/test/claim/self_host/compiler_closure_emit_from_ingest_test.dag::compiler_closure_ingest_overflow_refuses_never_empty_holds, src/v2/test/claim/self_host/compiler_closure_ingest_boundary_witness_test.dag::compiler_closure_ingest_boundary_exact_cap_transport_holds, src/v2/test/claim/long/infer_transform_binary_infix_witness_test.dag::infer_transform_add_vertical_witness_holds. Restored when: each named identity carries a cadence with a live scheduled route, at which point each row above is removed from transitional_admission_exception_identities and the identity's exception in explicit_witness_admission.dag is deleted (the gate consumes the list, so removing from the list retires the exception). The cadence category those routes need is gunbc.rung_drop.shared_capability missing_cadence_category; the remainder is the per-identity migration onto a live route. Waiters whose remaining unsatisfied condition is only that capability retire together. When the category fires and any named identity still lacks a live scheduled route, this identity is removed from missing_cadence_category.waiter_identities in the SAME change as those retirements (delist, not SplitRetirement) and this row stays Standing until every named identity has that route. If every named identity already has a live scheduled route when the category fires, retire with the enrolled set. ### The v2 native route (emitted-native compiler over the derived v2.test.* universe) as a required CI lane — declared 2026-09-11