PR-A: typed per-cause Refusals; empty diff dissolved into the general disposition; hunkless diffs attribute at path grain

.github/workflows/ci.yml

@@ -278,4 +278,3 @@ jobs:
           "$ROOT/target/release/claim_executor" --verify-build-artifacts "$ROOT/target/release/claim_executor" "$ROOT/target/release/gunbc"
           sccache --show-stats 2>/dev/null || true
           "$ROOT/target/release/gunbc" run --source-root dag --source-root src/v2 --entry dag/gunbc/live_deploy/apply.dag --function live_deploy_apply_srv1_wet
-

DESIGN.md

@@ -58,7 +58,7 @@ Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes
 
 A third named trap, the subtlest because it wears this section's own name: **the absorbing fallback — degradation is disguised fail-open.** When a mechanism cannot compute its precise answer, the tempting failure arm substitutes the *superset* instead: can't compute the affected set → rerun the entire suite; cache key uncertain → scan all keys; provenance unavailable → always run. Nothing is *missed*, so the arm gets labeled fail-closed — but it is the fabricated plausible output one level up: **⊤-as-answer conflated with ⊤-as-ignorance** (state-space conflation on the answer lattice — "everything is affected" and "I could not compute what is affected" are different states whose remedies differ), and it fails open twice. On safety: absorption destroys the only signal that the precise mechanism has a deficit — the failure's frequency is zero *by construction*, so the deficit never ranks for fixing (§6 prices by displaced cost, and a masked cost displaces nothing) and the anemia compounds (the scan-all-keys heuristic in the receipt below was this exact absorption; removing it exposed 8 deficits its silence had hidden). On cost: the fallback is denominated in the *corpus*, not the *change*, so it grows with the repo until the *budget* breaks instead of the build — later, loudly, at interest: §1's safety debt paid in §1's cost currency. And the confidence **threshold** that selects such an arm is a smuggled heuristic — §4 already rules a heuristic never necessary in a closed system — so the threshold's very existence *locates* the anemic modeling it papers over: a solution that must keep degrading to stay green is not a solution being cautious, it is a model being wrong. The rule, and the review tell: **a failure arm must refuse, never widen** — every degradation a typed, located, *countable* diagnostic, so its frequency is observable and prioritizable, never an absorbed rerun. Two neighbors are not this pattern (check the *trigger*: structure vs failure-state): a structural over-approximation computed *as* the answer (a dependency-closure superset is the model's precision frontier, not an absorption), and a deliberate interim fallback that is loud, budget-bounded, and lands with its §6 dissolution trigger. Silent unbounded absorption is never the third.
 
-- *e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 { x + y }`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types. The absorbing fallback, live in tree: `floor_witness_run_disposition` (`src/v2/workflow/affected_set_floor_runner.dag:122-130`) answers `DiffObservationFailClosed`, `FrontierFailClosed`, *and* the empty diff with `RunWitness` — one arm literally `"empty diff — run full corpus (fail-closed)"`, with tests *asserting the string* (`affected_set_floor_runner_test.dag:194`, `provenance_fail_closed_contract_test.dag`) so the degradation is enshrined as the contract — and the corpus-denominated cost duly surfaced as CI's 90-minute timeout, not as a diagnostic (the Building-&-checks enrollment inversion is the loud half of the repair; converting those arms to typed refusals is the rest).
+- *e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 { x + y }`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types. The absorbing fallback, formerly live in tree: `floor_witness_run_disposition` (`src/v2/workflow/affected_set_floor_runner.dag`) answered `DiffObservationFailClosed`, `FrontierFailClosed`, *and* the empty diff with `RunWitness` — one arm literally `"empty diff — run full corpus (fail-closed)"`, with tests *asserting the string* so the degradation was enshrined as the contract — and the corpus-denominated cost duly surfaced as CI's 90-minute timeout, not as a diagnostic. Repaired in two halves: the Building-&-checks enrollment inversion (the loud half), then the arms converted to typed refusals — `Refused` with per-cause variants, per-row counted, siblings continue — with the empty diff dissolved into the general disposition, never a special arm (operator rulings, 2026-07-05).
 
 ## 6. How to work (given §1–§5 — these coexist)
 

dag/gunbc/design_document.dag

@@ -103,7 +103,7 @@ fn section_5_blocks() -> List<MarkdownBlock> {
     p(text: "Minimizing cost and complexity (§2–§4) is worthless if a wrong thing passes silently — this is §1's safety axis made concrete. This code is digital: a wrong answer is a **loud error, never a warning** — a bridge collapses, it does not warn. Every path succeeds fully or fails with a typed, located diagnostic; no fabricated plausible output (a bounded \"forever\" ≠ an \"unknown\" error). Relax toward application-layer leniency only under protest, and lean to infra so others can build on your work. Stronger than *catching* a wrong state is making it **unwritable** — **correctness by construction, not validation.** A check that re-states a constraint the model already carries is a *second representation* of it (§2/§3): so prefer a single authority from which the realization is *derived* — the bad state cannot be written — over a check that flags it after the fact, which concedes the bad state *is* writable. The tell that a check was validation standing where construction was available: it can be satisfied by editing the *declaration* while the realization still lies (a key-completeness check went green when the spec was edited while the realizer kept faking the cache key). Reserve post-hoc checks for the genuinely **unstructurable** residue (§6 complexity / necessity — you cannot structurally forbid an *unnecessary* loop). Construction makes a class unwritable only when membership is **decidable**, so every class is one of three: a *wall now* (decidable and grounded — nicknaming, dead scaffolds, effect leaks); a *wall after grounding* (decidable but waiting on its single authority — the cross-representation `==` straddle is one only once `Int = GroupCompletion<Nat>` grounds it); or a *ratchet forever* (undecidable — optimality, by Rice, never reaches \"never\"). The word **\"never\" is the trap**: it lets a ratchet masquerade as a wall, so check decidability before claiming one — the undecidable residue is the §6 lens, honestly and permanently. The deepest trap is **specification-without-execution**: a typecheck and a `.contains()` grep are *not* consumers — \"done\" means a real consumer **green by execution** plus a discriminating input that goes *red* when the behavior is wrong. (For the LLM agent: fluent, type-checking, grep-passing output is precisely the artifact that looks finished without running. Treat your own output as unverified until a consumer runs it green.)"),
     p(text: "A third named trap, the subtlest because it wears this section's own name: **the absorbing fallback — degradation is disguised fail-open.** When a mechanism cannot compute its precise answer, the tempting failure arm substitutes the *superset* instead: can't compute the affected set → rerun the entire suite; cache key uncertain → scan all keys; provenance unavailable → always run. Nothing is *missed*, so the arm gets labeled fail-closed — but it is the fabricated plausible output one level up: **⊤-as-answer conflated with ⊤-as-ignorance** (state-space conflation on the answer lattice — \"everything is affected\" and \"I could not compute what is affected\" are different states whose remedies differ), and it fails open twice. On safety: absorption destroys the only signal that the precise mechanism has a deficit — the failure's frequency is zero *by construction*, so the deficit never ranks for fixing (§6 prices by displaced cost, and a masked cost displaces nothing) and the anemia compounds (the scan-all-keys heuristic in the receipt below was this exact absorption; removing it exposed 8 deficits its silence had hidden). On cost: the fallback is denominated in the *corpus*, not the *change*, so it grows with the repo until the *budget* breaks instead of the build — later, loudly, at interest: §1's safety debt paid in §1's cost currency. And the confidence **threshold** that selects such an arm is a smuggled heuristic — §4 already rules a heuristic never necessary in a closed system — so the threshold's very existence *locates* the anemic modeling it papers over: a solution that must keep degrading to stay green is not a solution being cautious, it is a model being wrong. The rule, and the review tell: **a failure arm must refuse, never widen** — every degradation a typed, located, *countable* diagnostic, so its frequency is observable and prioritizable, never an absorbed rerun. Two neighbors are not this pattern (check the *trigger*: structure vs failure-state): a structural over-approximation computed *as* the answer (a dependency-closure superset is the model's precision frontier, not an absorption), and a deliberate interim fallback that is loud, budget-bounded, and lands with its §6 dissolution trigger. Silent unbounded absorption is never the third."),
     ul(items: [
-      li(text: "*e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 \{ x + y \}`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types. The absorbing fallback, live in tree: `floor_witness_run_disposition` (`src/v2/workflow/affected_set_floor_runner.dag:122-130`) answers `DiffObservationFailClosed`, `FrontierFailClosed`, *and* the empty diff with `RunWitness` — one arm literally `\"empty diff — run full corpus (fail-closed)\"`, with tests *asserting the string* (`affected_set_floor_runner_test.dag:194`, `provenance_fail_closed_contract_test.dag`) so the degradation is enshrined as the contract — and the corpus-denominated cost duly surfaced as CI's 90-minute timeout, not as a diagnostic (the Building-&-checks enrollment inversion is the loud half of the repair; converting those arms to typed refusals is the rest)."),
+      li(text: "*e.g.* a compiler-sized `.dag` corpus typechecked and passed its grep claims, yet `emit` hung >600s on `fn add` → rebuilt `emit = serialize_target ∘ translate` (43 lines), proven by *running* `emit(add)` against the literal `fn add(x: i32, y: i32) -> i32 \{ x + y \}`. Removing a scan-all-keys fail-open heuristic (`0331b526ee`) exposed 8 real inference deficits its fabrication had hidden; the parser's dummy `LitNull` nodes once fed inference bogus types. The absorbing fallback, formerly live in tree: `floor_witness_run_disposition` (`src/v2/workflow/affected_set_floor_runner.dag`) answered `DiffObservationFailClosed`, `FrontierFailClosed`, *and* the empty diff with `RunWitness` — one arm literally `\"empty diff — run full corpus (fail-closed)\"`, with tests *asserting the string* so the degradation was enshrined as the contract — and the corpus-denominated cost duly surfaced as CI's 90-minute timeout, not as a diagnostic. Repaired in two halves: the Building-&-checks enrollment inversion (the loud half), then the arms converted to typed refusals — `Refused` with per-cause variants, per-row counted, siblings continue — with the empty diff dissolved into the general disposition, never a special arm (operator rulings, 2026-07-05)."),
     ]),
   ]
 }

src/v1/stage0/src/bin/floor_skip_discovery_witness.rs

@@ -142,27 +142,38 @@ fn discovery_corpus_skip_disabled_runs_without_panic() {
     );
 }
 
-fn discovery_corpus_skip_enabled_empty_diff_runs_corpus() {
+fn discovery_corpus_skip_enabled_empty_diff_skips_unaffected() {
     let _base = EnvVarGuard::set("GUNBC_CI_DIFF_BASE", "HEAD");
     let _head = EnvVarGuard::set("GUNBC_CI_DIFF_HEAD", "HEAD");
     let summary = run_explicit_roster(true).expect("empty diff path must not panic");
+    // Ruling 2026-07-05: empty diff is not a state — an empty touched-path set
+    // flows through the general disposition, so every unaffected row skips.
+    // The old assertion here (skipped == 0, "fail-closed run-all") enshrined
+    // the absorbing fallback this contract now forbids.
+    assert!(
+        summary.skipped >= 1,
+        "empty diff = computed ∅ — unaffected rows must skip (got {} skips)",
+        summary.skipped
+    );
     assert_eq!(
-        summary.skipped, 0,
-        "empty diff → fail-closed run-all (no stateless skip)"
+        summary.passed, 0,
+        "empty diff must not run unaffected witnesses (run-all is the absorbing arm)"
     );
-    assert!(summary.passed >= 1);
 }
 
-fn discovery_corpus_skip_enabled_git_observation_fail_closed_runs() {
+fn discovery_corpus_skip_enabled_git_observation_refuses() {
     let _base = EnvVarGuard::set("GUNBC_CI_DIFF_BASE", "__gunbc_invalid_diff_base__");
     let _head = EnvVarGuard::set("GUNBC_CI_DIFF_HEAD", "HEAD");
     let _merge = EnvVarGuard::set("GUNBC_CI_DIFF_MERGE_BASE", "0");
-    let summary = run_explicit_roster(true).expect("git observation fail-closed must not panic");
-    assert_eq!(
-        summary.skipped, 0,
-        "git diff failure → skip inactive → run full explicit roster"
+    // Ruling 2026-07-05: observation failure is the one ignorance state and it
+    // REFUSES — a typed, counted error naming its cause — never a silent
+    // run-everything or a silent selection-off.
+    let err = run_explicit_roster(true)
+        .expect_err("git observation failure must refuse, not run or skip");
+    assert!(
+        err.contains("DiffObservationRefusal"),
+        "refusal must name its cause (got: {err})"
     );
-    assert!(summary.passed >= 1);
 }
 
 fn node_precise_referenced_runs_orphan_skips_by_execution() {
@@ -403,12 +414,12 @@ fn main() -> ExitCode {
             discovery_corpus_skip_disabled_runs_without_panic,
         ),
         (
-            "discovery_corpus_skip_enabled_empty_diff_runs_corpus",
-            discovery_corpus_skip_enabled_empty_diff_runs_corpus,
+            "discovery_corpus_skip_enabled_empty_diff_skips_unaffected",
+            discovery_corpus_skip_enabled_empty_diff_skips_unaffected,
         ),
         (
-            "discovery_corpus_skip_enabled_git_observation_fail_closed_runs",
-            discovery_corpus_skip_enabled_git_observation_fail_closed_runs,
+            "discovery_corpus_skip_enabled_git_observation_refuses",
+            discovery_corpus_skip_enabled_git_observation_refuses,
         ),
         (
             "node_precise_referenced_runs_orphan_skips_by_execution",