From 0327bcf8d8ef20700b5b8b79553d8b54bc65a241 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 8 Oct 2026 20:32:11 +0000 Subject: [PATCH 1/2] wip --- .../claim/target_invocation_witness_test.dag | 29 +++++++++++++------ 1 file changed, 20 insertions(+), 9 deletions(-) diff --git a/dag/test/claim/target_invocation_witness_test.dag b/dag/test/claim/target_invocation_witness_test.dag index c919bfbf374..fb72e21a86a 100644 --- a/dag/test/claim/target_invocation_witness_test.dag +++ b/dag/test/claim/target_invocation_witness_test.dag @@ -507,8 +507,18 @@ test fn the_instrument_target_and_its_binding_are_the_same_identity() -> Bool { LabelNonCanonical { cause: _ } => false }) && (render_label(l: t.label) == differential_operand()) - && ((instrument_targets() |> count) == 8) - && ((instrument_bindings() |> count) == 8) + && registry_and_bindings_are_one_population() +} + +// THE REGISTRY AND ITS BINDINGS ARE ONE POPULATION, JOINED AT IDENTITY GRAIN. Completeness is an +// identity join and never a count (DESIGN section 5): a literal count of the live registry is a +// measurement copied from the tree it measures, and it went false the first time a row was added. +// Both directions are asserted, so a target with no binding AND a binding for no registered +// target each fail -- a count equality passes a registry that swapped one row for another. +fn registry_and_bindings_are_one_population() -> Bool { + let bound = instrument_bindings() |> map(b => b.target) + fold(instrument_targets(), init: true, f: fn(acc, t) { acc && label_in(labels: bound, wanted: t) }) + && fold(bound, init: true, f: fn(acc, l) { acc && label_in(labels: instrument_targets(), wanted: l) }) } // THE ABSENCE PROOF, MEASURED OVER THE DERIVED POPULATION RATHER THAN ASSERTED IN PROSE. @@ -524,15 +534,16 @@ test fn the_instrument_target_and_its_binding_are_the_same_identity() -> Bool { // // THE PLANNED SITE'S MODULE PATH MUST SIT INSIDE THE STATIC GATE. Since the 2026-08-29 bankruptcy // ruling, `v2.workflow.required_floor` `required_gate_prefixes` is a static roster and a site -// outside it dispositions `DeclinedOutsideRequiredGate` -- which is what happened to the original -// `test.claim.some_witness` fixture path: the presence conjunct above went silently red while the -// module itself sat off-gate and unexecuted. `v2.test.` is a rostered prefix, so the fixture's -// planned site plans again; a future roster shrink that drops the prefix reds this test loudly, -// which is the control working rather than a new fragility. +// outside it dispositions `DeclinedOutsideRequiredGate`, so the presence conjunct below goes +// silently red while the fixture itself sits off-gate. This fixture has been bitten twice: the +// original `test.claim.some_witness` path, and then `v2.test.some_witness`, whose `v2.test.` prefix +// the revert of gunbc#12582 (gunbc#12852) removed from the roster. The path now rides the +// `test.claim.infer_` family row, which has been in the roster throughout; a future roster change +// that drops it reds the planned-site conjunct, which is the control working. fn census_fixture_sites() -> List { [ DiscoveredSite { - module_path: "v2.test.some_witness", + module_path: "test.claim.infer_some_witness", function: "a_planned_site", reads_live_tree: SubstrateInputsOnly {} }, @@ -546,7 +557,7 @@ fn census_fixture_sites() -> List { fn planned_site_label() -> Label { Label { - package: PackagePath { segments: ["v2", "test", "some_witness"] } + package: PackagePath { segments: ["test", "claim", "infer_some_witness"] } target: TargetName { name: "a_planned_site" } } } From d1d7fbf1f643b9bd514b88d0e965f344747889b3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 8 Oct 2026 20:42:21 +0000 Subject: [PATCH 2/2] target_invocation witness: repair two false claims (identity join, in-gate fixture site); file the 43 unplanned claims under the body-change-unplanned class Co-Authored-By: Claude Sonnet 5.5 --- ...or_executes_no_claim_whose_verdict_a_body_change_can_move.dag | 1 + 1 file changed, 1 insertion(+) diff --git a/dag/gunbc/recurring_failure_mode/green_floor_executes_no_claim_whose_verdict_a_body_change_can_move.dag b/dag/gunbc/recurring_failure_mode/green_floor_executes_no_claim_whose_verdict_a_body_change_can_move.dag index c7fec68baa2..bab505487aa 100644 --- a/dag/gunbc/recurring_failure_mode/green_floor_executes_no_claim_whose_verdict_a_body_change_can_move.dag +++ b/dag/gunbc/recurring_failure_mode/green_floor_executes_no_claim_whose_verdict_a_body_change_can_move.dag @@ -21,6 +21,7 @@ data green_floor_executes_no_claim_whose_verdict_a_body_change_can_move: Recurri "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: the required floor executes, on every pull request, every enrolled claim whose declaration reach contains a declaration the diff changed, at the diff's base and at its head. A claim blocks only when it held at base and fails at head, and a selection over its declared budget refuses with a typed cause rather than truncating or widening. The design was ruled by neat-boar-16 on 2026-09-26. It makes `v2.test.*` claims differentially merge-blocking for the first time. The operator ruled on 2026-09-27 that the per-PR v2 claim comparison is merge-blocking over this selection intersected with the v2 claim set, never over the whole set, and the enabling step is its own change (work item adhoc-6969b422-bec). LANDED WITH THIS ROW, observe-only: `namespace_baseline` `body_reach_from_changed_declarations` closes the diff's changed declarations under every read channel over the index the parse phase already built. Its seeds are the declaration grain of the floor's own line attribution plus every interface change. The floor prints one `[floor-plan] BodyReachWitness` line per reached witness declaration and a `[floor-phase] phase=body-reach-selection` summary, and plans nothing from it. The propagation rule is modeled as `v2.workflow.floor_subject_seed` `reach_propagates`: a body read propagates for `ClaimExecution` and not for `StrictPreparation`. The executed red is `a_body_only_change_reaches_the_witness_two_calls_away`: the compile walk plans nothing, and the reach walk selects the witness two calls away and neither the idle importer nor the unrelated witness. THE BASE-VERDICT CACHE THE ENABLING STEP NEEDS is a materialization (`std.materialization_ladder`). Its key must cover the claim identity, a digest of the base tree over every declaration in the claim's reach, and the seed and interpreter identity, or it is a stale-answer source.", "THE BOUND, STATED SO THE OBSERVE-ONLY GREEN IS NOT OVER-READ. (1) Until the enabling switch lands, nothing in this row blocks a merge. The class is still below rung 1 on the merge path and is now counted rather than silent. (2) Reach is at the grain of the reference index: a read only through an INFERRED type that no declaration on the path spells is not reached (the same limit as the compile-grain peer, with the same trigger, the resolver's own reference relation replacing name occurrences). (3) A reached declaration is a witness only if its module is a fixture carrier (`declaration_index` `module_is_fixture_carrier`). The floor's own discovery decides which of those are claims. (4) MEASURED ON THE REAL HISTORY (srv1 planning receipts, replay heads on branches `replay/cool-otter-576/*`): #12361's replay reaches all ten of its base-pass/head-fail claims among 3655 witness declarations; the unrelated-diff control (#12353) reaches 522, confined to readers of what it changed; a one-declaration body edit to `v2.std.node` reaches 3286; and the selection costs about 1.8 s of wall time in each. The first round of the same replay FAILED its control (13147 for the unrelated diff) through two defects, and both are the reason this walk does not simply reuse the compile walk's flat channel: a dotted field access (`cfg.root`) and an ambiguous bare name were read as reads of a changed top-level declaration, and an import edit seeded every declaration in its file. The cost of EXECUTING a selection at base and head is the enabling step's receipt, not this row's.", + "SPECIMEN, WHOLE-MODULE FORM (gunbc#13556, floor run 37707872269; node adhoc-01443378-ec9). `test.claim.target_invocation_witness` (dag/test/claim/target_invocation_witness_test.dag) is named by neither `required_gate_prefixes` nor `required_gate_authored_modules`, so the static gate plans none of its claims; the only population planned on a pull request is the changed witnesses, the test fns whose own line range the diff edits. The PR added five claims and renamed one, and the floor's `required_floor_claim_cost` artifact lists exactly 14 of the module's 57 claims. THE OTHER CLAIMS WERE ENROLLED IN THE CORPUS AND EXECUTED BY NO LANE, AND TWO OF THEM WERE FALSE ON MAIN at 13b91523a9: `the_instrument_target_and_its_binding_are_the_same_identity` compared the live instrument registry to the literal 8 (a measurement copied from the tree it measures, false once the registry grew), and `the_instrument_label_is_absent_from_the_derived_required_aggregate` placed its planned fixture site at `v2.test.some_witness`, whose `v2.test.` prefix the revert gunbc#12852 removed from the gate roster, so the presence conjunct read DeclinedOutsideRequiredGate. Both were repaired in the change that files this receipt (identity-grain join of targets to bindings in place of the counts; the planned fixture site moved onto the `test.claim.infer_` family row); a standalone claim_batch over the module read 57/57 after, 55/57 before. NOT claim_batch-only: neither false claim depends on the harness, both reduce to a pure fold over a live population the claim literal disagreed with. THE UNPLANNED POPULATION AT THE BASE, BY IDENTITY, ALL FOR THE SAME REASON (module outside the static gate, claim not edited by the diff): `a_binary_whose_inputs_did_not_move_is_fresh`, `a_moved_bare_channel_gate_does_not_hold`, `an_absent_bare_channel_fixture_root_is_not_a_moved_gate`, `an_input_from_another_worktree_outranks_staleness`, `an_invented_population_routes_through_the_same_fold`, `an_unreached_subject_is_not_reported_as_a_failed_reading`, `a_prefix_of_a_registered_label_is_not_the_registered_target`, `a_registered_target_with_no_producer_refuses_as_a_registry_gap`, `a_relative_operand_refuses_as_not_absolute_and_not_as_a_pattern`, `a_subtree_is_not_contained_in_a_package_pattern`, `a_well_formed_label_naming_no_registered_target_refuses`, `every_behavioral_instrument_operand_routes_to_its_own_producer`, `narrowing_holds_while_divergence_does_not`, `target_patterns_refuse_with_the_cited_grammars_own_cause`, `the_acceptance_operand_routes_to_the_real_differential_producer`, `the_bare_channel_instrument_is_a_real_row_on_the_shared_registry`, `the_bare_channel_join_is_at_identity_grain_and_total`, `the_bare_channel_rendering_names_the_channel_and_the_pull_set`, `the_bare_channel_standing_rendering_locates_an_unreached_subject`, `the_bare_channel_standing_rendering_reports_the_read_populations`, `the_canonicality_cause_reaches_the_rendered_refusal`, `the_canonicality_cause_survives_into_the_routes_refusal`, `the_dependency_demand_census_operand_routes_to_its_own_producer`, `the_diagnostic_census_operand_routes_to_its_own_producer`, `the_diagnostic_census_refusal_renders_its_own_cause`, `the_diagnostic_census_rendering_reports_the_raw_counts_and_identity`, `the_diagnostic_census_wall_is_class_specific_and_severity_independent`, `the_direct_standing_is_not_the_aggregate_verdict_nor_the_blaze_export`, `the_evaluation_store_address_exact_head_operand_routes_to_its_own_producer`, `the_first_changed_input_is_named_as_stale`, `the_generic_identity_census_operand_routes_to_its_own_producer`, `the_instrument_label_is_absent_from_the_derived_required_aggregate`, `the_instrument_target_and_its_binding_are_the_same_identity`, `the_interpolation_hole_census_operand_routes_to_its_own_producer`, `the_nearest_discoverable_site_label_is_still_not_the_instrument_label`, `the_primitive_egress_census_operand_routes_to_its_own_producer`, `the_primitive_egress_census_v2_operand_routes_to_its_own_producer`, `the_regen_round_cost_operand_routes_to_its_own_producer`, `the_rendering_reports_the_populations_the_differential_measured`, `the_required_lane_resolution_census_operand_routes_to_its_own_producer`, `the_self_host_behavioral_equivalence_operand_routes_to_its_own_producer`, `the_universe_contains_itself_and_not_its_siblings`, `unreadable_dep_info_is_undecided_not_fresh`. Re-derive it with the artifact diff named above, never by transcribing this list as a count. This is the executed instance of the class, not a new class: the climb is the trigger above, and a module-grain gate row (`required_gate_authored_modules`) would be the stopgap, which is a gate change owed to a ruling and is NOT made here.", ], evidence: [