Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 0 additions & 16 deletions dag/gunbc/explicit_witness_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -281,14 +281,6 @@ data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
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<NonEmptyStr>.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",
Expand Down Expand Up @@ -465,14 +457,6 @@ data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
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<Memory, One, Nat>, 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",
Expand Down
76 changes: 76 additions & 0 deletions dag/gunbc/quarantine_outside_gate_decline.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
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 785934a38b6: all nine probes rostered here FAIL
// (their declared red).
type QuarantineOutsideGateDecline {
module: String
function: String
trigger: NonEmptyStr
}

data quarantine_outside_gate_declines: List<QuarantineOutsideGateDecline> = [
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
},
]
Loading
Loading