where-refinement: credit a guaranteed minimum length as evidence for a min-length demand

dag/gunbc/explicit_witness_admission.dag

@@ -131,15 +131,15 @@ fn known_red_pre_verdict_probe(
   )
 }
 
-data known_red_class_note: String = "WHAT A KNOWN-RED ADMISSION IS: a witness red on main for a feature gap owned by a named lane. It is a RED CONTROL for that lane, not a broken test — deleting it would discard the discriminating input, while leaving it in per-PR discovery would red every wide PR on a debt that PR did not create. Greening is the counted un-quarantine event of std.witness_admission: the row deletes in the SAME change that lands the fix, which promotes the unchanged witness to ordinary DiscoverySelection as a permanent regression control (DESIGN 4b(4) — the climb deletes the quarantine machinery, never the evidence). The roster must not grow silently: a new admission carries a reason naming the diagnosis and owner plus a dissolve_on, both refused empty by NonEmptyStr, and a row whose witness runs green locally is stale and deletes. Local recipe per row: claim_batch --source-root dag --source-root src/v2 --entry <entry> --functions <function>. CorpusWitnessKind rows run on the hermetic falsifier probe batch; ExecutionWitnessKind rows run on the falsifier wet quarantine batch."
+data known_red_class_note: String = "WHAT A KNOWN-RED ADMISSION IS: a witness red on main for a feature gap owned by a named lane. It is a RED CONTROL for that lane, not a broken test — deleting it would discard the discriminating input, while leaving it in per-PR discovery would red every wide PR on a debt that PR did not create. Greening is the counted un-quarantine event of std.witness_admission: the row deletes in the SAME change that lands the fix, which promotes the unchanged witness to ordinary DiscoverySelection as a permanent regression control (DESIGN 4b(4) — the climb deletes the quarantine machinery, never the evidence). A DISSOLVE_ON MUST NAME A FACT THAT IS FALSE TODAY AND BECOMES TRUE EXACTLY WHEN THE FIX LANDS, and this requirement is here because two rows failed it in one night. A trigger keyed on a condition already satisfied is not a trigger, it is a deletion licence with a date on it: whoever next reads it dissolves a quarantine standing in for a defect that is still live, and the row reads as dissolved-per-its-own-terms while the wall it substituted for does not exist. RECEIPT 1, another lane's: the #8592 row's trigger read 'the mirrors are regenerated so the compiled harness CONTAINS declared_arg_types_for_method' — that symbol has been present in v1_compiler_infer_lookup.rs all along, so the trigger was satisfiable from the moment it was written, while the defect it quarantines is live (on main the function still takes no TypeEnv, which is precisely the bug). RECEIPT 2, MY OWN, AND IT IS THE MORE INSTRUCTIVE ONE BECAUSE THE DELETION WAS STILL CORRECT: the min-length row's trigger read 'the compiled harness contains the wall'. Measured, where_refinement_predicates_covered has 2 occurrences in that mirror on main and always did, so a reader checking 'the wall' would have dissolved the row at any point in the preceding weeks. It dissolved correctly only because the author happened to grep where_predicate_guaranteed_min_length, which was 0 on main and 2 after the regen. THE TRIGGER DID NOT ENCODE WHICH FACT DECIDED IT; the right answer came from the reader, not the row. So: name the symbol, signature or behaviour whose ABSENCE is the gap — a new parameter, a specific new function, a named repro passing — never a category word like 'the wall' or 'the fix', and never a symbol that predates the change. The test a reviewer applies: run the trigger's check against main TODAY, and if it passes, the trigger is defective and the row is unprotected. The roster must not grow silently: a new admission carries a reason naming the diagnosis and owner plus a dissolve_on, both refused empty by NonEmptyStr, and a row whose witness runs green locally is stale and deletes. Local recipe per row: claim_batch --source-root dag --source-root src/v2 --entry <entry> --functions <function>. CorpusWitnessKind rows run on the hermetic falsifier probe batch; ExecutionWitnessKind rows run on the falsifier wet quarantine batch."
 
 data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
   known_red_probe(
     entry: "dag/test/claim/method_arg_declared_contract_witness_test.dag",
     f: "w_method_arg_infers_against_declared_contract_not_element_type_test",
     kind: CorpusWitnessKind,
     budget: FastLaneEvalBudget,
-    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 (dag.gunbc.explicit_witness_admission, where_refinement_lower_hex_40_implies_non_empty_credits_evidence) — owned by the required-regen lane. 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 row above, whose file sits under that excluded directory and is discovered nowhere. 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.",
+    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(

dag/test/claim/long/where_refinement_enforcement_witness_test.dag

@@ -5,6 +5,7 @@ import gunbc.compile_diagnostic_census {
   CompileDiagnosticCensus,
   CensusObserved,
   CensusNotRunnable,
+  census_advisory_rows,
   census_blocking_rows,
   census_rows_of_class,
   census_total_count,
@@ -563,3 +564,41 @@ test fn where_refinement_wrong_kind_literal_direct_return_refuses() -> Bool {
 test fn where_refinement_wrong_kind_literal_direct_return_accepts() -> Bool {
   w_wrong_kind_literal_direct_return_green()
 }
+
+data where_refinement_promotion_is_not_execution_note: String = "MY OWN DISSOLUTION COMMIT CLAIMED SOMETHING THIS FILE'S HOME MAKES FALSE, AND THE CORRECTION BELONGS HERE RATHER THAN IN THE COMMIT THAT CANNOT BE READ FROM THE TREE. gunbc#8619 deleted the known-red row for where_refinement_lower_hex_40_implies_non_empty_credits_evidence once its trigger was satisfied (the 04_infer stage0 mirror regenerated, so the compiled harness carries the min-length implication), and said the witness thereby PROMOTES TO ORDINARY DiscoverySelection AS THE PERMANENT REGRESSION CONTROL. THAT SECOND HALF IS FALSE FOR A FILE UNDER dag/test/claim/long/. That prefix is excluded from witness discovery AT DIR GRAIN (gunbc.ci_layer_roots long_lane_exclusion_note), so ordinary discovery never reaches this module. Deleting the row removed the only thing that NAMED these witnesses; the home ensures nothing else does. The honest state is therefore not promoted-to-executing but EXECUTED NOWHERE. CORRECTED, SAME DAY, BEFORE ANYONE ACTED ON IT: an earlier revision of this row added that this is 'strictly worse than the quarantine it replaced, because a known-red row is at least counted'. THAT IS FALSE and the correction matters because it changes what is owed. v2.workflow.required_floor is explicit that EVERY DISCOVERED SITE gets exactly one RequiredFloorDisposition keyed by its qualified module.function identity (operator ruling 2026-08-19), and the long home is one of its Declined arms rather than an absence. So these identities ARE discovered and ARE counted at identity grain as declined, and aggregate into the floor's declined_long figure. What was lost by deleting the known-red row is not counting; it is the row's own reason string and owner. Counted-and-declined is a weaker protection than executed, and a better one than silence. A SECOND CORRECTION IN THE SAME BREATH, because it changes the remedy: admission is tested against the module's AUTHORED NAME, not its file path -- long_home_prefixes() holds 'test.claim.long.' and this module's first line declares test.claim.long.where_refinement_enforcement_witness. Moving the FILE while keeping the module name would therefore change nothing, and the next-rung options below must be read as renaming the module (with its file), never as relocating a file. WORTH STATING BLUNTLY BECAUSE IT IS THE WHOLE LESSON: required_floor's own header records that the previous host tested a PATH, which 'made a directory the admission authority', and names that as the root cause the 2026-08-04 ruling identifies. I proposed to fix this by moving a directory. I reproduced the exact mistake the mechanism was built to stop, inside the mechanism that stops it, while reading the file that says so. WHY THE ROW WAS STILL RIGHT TO DELETE: it asserted a RED that is no longer red, and re-adding it would be a false claim about the current tree. The defect is not the deletion, it is that promotion presumes a discovering consumer this file does not have. RUNG: this file's witnesses sit at MITIGATABLE, protected by the local recipe and by review diligence, not by any executing gate -- claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/long/where_refinement_enforcement_witness_test.dag --functions <csv>. NEXT-RUNG TRIGGER, and it is a decision I did not take unilaterally because it trades one real cost for another: either this module is RENAMED out of the test.claim.long. prefix (and its file moved with it) so the floor admits it -- which puts its per-witness eval cost into the executed roster, the exact thing the home exists to keep out, and with the per-witness eval deadline dropped in the 2026-08-15 floor cut nothing would REFUSE an over-budget witness, so the cost would land silently on every run -- or the long home acquires an executing consumer, which the same floor cut deleted with falsifier.yml and has not re-added. The first is not this lane's to take unilaterally and the second is not this lane's to build. NOT A ROUTE: v2.workflow.floor_route_gap, which landed 2026-08-20 for unexecuted witnesses, is scoped to identities the floor EXECUTES that reach a host effect with no hermetic arm. These identities do not execute at all, and that roster's own reverse join reds the build on an enrolled identity that did not execute -- so enrolling here would be a false claim, not a shortcut. THE PROVENANCE OF THAT SENTENCE, marked because this corpus was burned by exactly this today: it is READ FROM THAT MODULE'S CONTRACT PROSE, not observed. A carrier's description of its own mechanism is not evidence the mechanism behaves that way -- a gate that never executed and a lens reading a file that exists nowhere were both fully described in prose. It is accepted here on two narrow grounds: the claim is about a REFUSAL rather than a green, so trusting it wrongly yields a weaker refusal rather than a silent accept; and exercising it would mean authoring a knowingly-false row to red a build. If a free way to exercise that join appears, take it; do not manufacture one. WHAT MUST NOT HAPPEN MEANWHILE: nobody should read the absence of red here as evidence that the min-length implication holds. Nothing has executed these assertions on CI. See gunbc.explicit_witness_admission known_red_class_note for the trigger-discipline rule this same episode produced."
+
+data where_refinement_min_length_implication_witness_note: String = "WHY THESE ASSERT A COUNT AND NOT A Bool, which is the whole reason this block exists. WhereRefinementUnenforced is ADVISORY — compile-clean GREEN. So compile_dag_rust_emit_check returns true for the implication sites both BEFORE and AFTER the fix, and a Bool-shaped witness pair over them would have passed identically against the unfixed compiler: a green control satisfied by the fact that nothing ever refused. That is the specification-without-execution trap in its exact local form, and the only instrument that escapes it is the one that can see a diagnostic the severity filter discards. These therefore go through compile_dag_diagnostic_census and assert the ADVISORY WhereRefinementUnenforced count at each site, which moves 1 -> 0 for a credited implication and STAYS 1 for an uncredited one. THE THIRD WITNESS IS THE ONE THAT MATTERS MOST and it is a fail-open control, not a feature: a formal lower_hex_64 position fed a lower_hex_128 value must REMAIN advisory. If where_predicate_required_min_length ever grows a lower_hex_* row — the single most natural-looking edit anyone will propose to this table, since it already sits beside a guaranteed-length table carrying exactly those names — then 128 >= 64 credits a 128-digit string as a valid sha256 hex and this witness goes red. It is a permanent regression control on the asymmetry, not a probe of a landed behavior, and it does not retire when the wall lands (DESIGN 4b meta-obligation 4: a climb deletes the redundant production machinery, never the evidence)."
+
+fn where_refinement_advisory_count(source: String) -> Int {
+  match compile_dag_diagnostic_census(source) {
+    CensusObserved { rows: rows } =>
+      census_total_count(
+        rows: census_advisory_rows(
+          rows: census_rows_of_class(rows: rows, wanted: "WhereRefinementUnenforced")
+        )
+      )
+    CensusNotRunnable { cause: _ } => -1
+  }
+}
+
+test fn where_refinement_lower_hex_40_implies_non_empty_credits_evidence() -> Bool {
+  where_refinement_advisory_count(
+    source: "module whereref_minlen_implies\nimport std.types { NonEmptyStr }\ntype Sha1Hex = String where lower_hex_40\nfn f(h: Sha1Hex) -> NonEmptyStr { h as NonEmptyStr }\n"
+  ) == 0
+}
+
+test fn where_refinement_bare_string_at_non_empty_stays_advisory() -> Bool {
+  where_refinement_advisory_count(
+    source: "module whereref_minlen_bare\nimport std.types { NonEmptyStr }\nfn f(s: String) -> NonEmptyStr { s as NonEmptyStr }\n"
+  ) == 1
+}
+
+test fn where_refinement_exact_length_predicate_is_not_a_min_length_demander() -> Bool {
+  where_refinement_advisory_count(
+    source: "module whereref_minlen_failopen_control\ntype Hex128 = String where lower_hex_128\ntype Hex64 = String where lower_hex_64\nfn f(h: Hex128) -> Hex64 { h as Hex64 }\n"
+  ) == 1
+}
+
+test fn where_refinement_min_length_implication_does_not_relax_literal_refusal() -> Bool {
+  !w_non_empty_string_cast_literal_red()
+}