cli_run.rs hollowing: retype the gate-global builtins to typed receipts and cut the GenerateNow areas

dag/gunbc/ci_gate.dag

@@ -1,5 +1,8 @@
 module gunbc.ci_gate
 
+import std.types { NonEmptyStr, String }
+import std.process { ProcessExit, ExitSuccess, exit_failure }
+
 type Gate
   = EmitHostGate
   | CheapClaimPoolGate
@@ -9,3 +12,54 @@ type Gate
   | ExtdepsScopePlacementGate
   | ProseRowIntroductionGate
   | SourceRootIngestGate
+
+data gate_receipt_state_split_note: String = "WHY A GATE ANSWERS A RECEIPT AND NOT A Bool. The two host gate consumers behind DagCompileCleanGate and GeneratedArtifactDriftGate used to answer through a process-global read collapsed to Bool, with a second String builtin beside it carrying the located detail. consume_floor_compile_clean_gate_verdict folded FIVE distinct states into false -- receipt lock poisoned, receipt install failed, no in-run receipt at all, the receipt's own typed Refused arm, and a genuine Compiled ok:false -- and folded the scope disposition's Skipped into true. So a gate that never ran in this process was indistinguishable from a compile that found hard diagnostics, and a scope disposition selecting nothing was indistinguishable from a clean tree. That is DESIGN's execution-provenance-loss row (a masked run and a clean run rendered identically) sitting underneath not-applicable-rendered-as-malformed, in one Bool. The detail companion did not repair it: it was a SECOND builtin over the SAME global, so a caller had to correlate two reads to recover one fact, and the generated-artifact one FABRICATED prose ('gate body did not run in this process') for the very state the Bool had already erased. THE THREE ARMS ARE THE THREE OWNERS, which is why this is a construction and not a wider enum. GateObserved means the gate reached its subject and decided; its GateOutcome carries the located detail on the failing side, so the detail can no longer be read without the verdict that produced it. GateNotApplicable means the gate's own scope disposition selected nothing to check, an answer whose owner is the disposition and whose remedy is never 'fix the tree'. GateNotRun means could-not-measure: the instrument did not arrive at its subject, whose owner is the instrument and whose remedy is never 'fix the tree' either. The line still stops on GateNotRun (gate_receipt_exit refuses it), so this is not a relaxation: what changes is that the stop is typed and located, and analysis can precede restart. MODELLED ON gunbc.compile_diagnostic_census, deliberately and not coincidentally: that carrier splits CensusObserved from CensusNotRunnable for exactly this reason, and its census_projection_note records that exporting a reader which answers empty on the not-runnable arm was the fail-open it existed to prevent. The same rule holds here, and it is why no accessor hands back a Bool from a GateReceipt: the only way to a verdict is to match the coproduct."
+
+type GateOutcome
+  = GateClean
+  | GateFailed { detail: NonEmptyStr }
+
+type GateReceipt
+  = GateObserved { outcome: GateOutcome }
+  | GateNotApplicable { reason: NonEmptyStr }
+  | GateNotRun { cause: NonEmptyStr }
+
+data gate_receipt_exit_note: String = "The one place a receipt becomes a line-stop, so the three arms cannot drift apart across gates. GateNotRun exits FAILURE and says so in its OWN vocabulary rather than borrowing the subject's: a reader of the exit reason can tell 'the gate did not run' from 'the gate ran and refused the tree', which is the whole distinction the Bool destroyed. GateNotApplicable exits SUCCESS and that is not a widen: the scope disposition is the authority for what this gate covers, so a disposition selecting nothing is an answer, not an absence of one, and its reason travels in the receipt for any consumer that wants to count it."
+
+fn gate_outcome_exit(outcome: GateOutcome) -> ProcessExit {
+  match outcome {
+    GateClean => ExitSuccess
+    GateFailed { detail: detail } => exit_failure(reason: (detail as String))
+  }
+}
+
+fn gate_receipt_exit(r: GateReceipt) -> ProcessExit {
+  match r {
+    GateObserved { outcome: outcome } => gate_outcome_exit(outcome: outcome)
+    GateNotApplicable { reason: _ } => ExitSuccess
+    GateNotRun { cause: cause } => exit_failure(
+      reason: concat("gate did not run over its subject: ", (cause as String))
+    )
+  }
+}
+
+data gate_receipt_failure_detail_note: String = "THE COMPANION PROJECTION, and it is a String only because its consumer is. claim_executor derives a <witness>_failure_receipt companion from a Bool witness's own name and evaluates it to explain a red (tools.floor_effect_gate_witness floor_gate_failure_receipt_note is that mechanism's authority), so the two CI gates must still be able to hand back a located line. What changes is where the line comes from: it is now PROJECTED from the same receipt that produced the verdict, instead of read out of a second builtin over the same process global. That is the §3 half of this retype -- one authority, two projections -- and it is why no arm here answers a detail the verdict did not produce. Each arm keeps its OWN vocabulary: a gate that did not run says so, and never borrows the subject's ('compile-clean failed'), which is precisely what the two-builtin form could not avoid, because the detail read had no idea which state the verdict read had been in."
+
+fn gate_outcome_failure_detail(outcome: GateOutcome) -> String {
+  match outcome {
+    GateClean => ""
+    GateFailed { detail: detail } => (detail as String)
+  }
+}
+
+fn gate_receipt_failure_detail(r: GateReceipt) -> String {
+  match r {
+    GateObserved { outcome: outcome } => gate_outcome_failure_detail(outcome: outcome)
+    GateNotApplicable { reason: reason } => concat(
+      "gate not applicable over its subject: ", (reason as String)
+    )
+    GateNotRun { cause: cause } => concat(
+      "gate did not run over its subject: ", (cause as String)
+    )
+  }
+}

dag/gunbc/ci_spec.dag

@@ -243,7 +243,7 @@ data gunbc_ci_floor_batch_clamp_params: List<RunnableBatchClamp> = [
   gunbc_ci_floor_positional_clamp(overhead_seconds: 125, per_unit_ms: 0),
 ]
 
-data gunbc_ci_compile_clean_clamp_note: String = "COMPILE-CLEAN LEG CLAMP (prelude coverage, first slice): discharges the compile-clean portion of gunbc_ci_floor_batch_clamp_note FOLLOW-UP ROW (a) — the eager compile-clean install ran OUTSIDE every batch budget and could only red at the step cap, which is how a 15m32s green gate grew past 49 minutes across #7398/#7438 with nothing naming the growth (typecheck-perf investigation, PR #7490). Same shape as the batch clamps: clamp_ms = overhead_seconds*1000 + closure_units * per_unit_ms, where closure_units is the compiled closure's MODULE COUNT — a runtime fact of the scope disposition (whole-tree ~2725 today, affected-set proportional to the diff), so the clamp re-denominates with scope exactly as batch clamps re-denominate with the affected set. Over-clamp is FLOOR-COMPILE-CLEAN-OVER-BUDGET: a typed, located walk refusal (admission grain — the compile receipt's ok is untouched, per the signed admission/verdict split in gunbc_ci_floor_batch_wall_budget_note); never a rerun, never a widen. RED-control hook GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS lowers the computed clamp (min), never raises. GROWTH DETECTION at row grain is NOT this clamp's job (the family margin ruling, 2026-07-25): per-row 2x drift against dated basis rows rides gunbc.witness_row_cost's comparator over dag/gunbc/compile_clean_cost_basis.tsv — the pass + module_typecheck rows of target/floor-compile-clean-cost-receipt.tsv, basis rows citing arm64 fleet run ids only, BasisAbsent counted until seeded from a cited run's own receipt FILE (the #7475 seeding pattern; an empty basis must count loudly, never read as no-drift). SEEDING SOURCE CORRECTED: this clause used to name the [compile-clean-cost] log lines, because the receipt file had no way off the runner and every row was mirrored into the step log to compensate — ~1,690 lines per floor run, and the same shape cost 8,614 more on the disclosure receipt. THAT REPLACEMENT ROUTE IS NOW GONE TOO, which is the correction this clause carries: it used to say the ci job uploads the receipts as the floor-receipts artifact via gunbc.ci_workflow ci_floor_receipts_upload_step, so seeding downloads the TSV instead of scraping a log. No live workflow carries that step -- it died with ci.yml in the floor cut. TRANSPORT IS NOW PARTIAL RATHER THAN ABSENT, and this clause is written at that grain because the coarser claim went stale within a day: gunbc#8875 (2026-08-22) added an upload to witnesses.yml, so DISPOSITION receipts DO leave the runner today. gunbc#8877 then replaced that single bundled artifact with one artifact per file -- required-floor-disposition, expected-red-roster-join and long-home-storage-agreement -- because the bundled form evaluates if-no-files-found once over the combined list and so cannot report a single missing file. A reader looking for the name required-floor-receipts will not find it; the population is unchanged and none of the cost receipts this note names are in any of the three. So the gap is no longer the absence of any transport; it is that the transport which exists carries a different population, and a reader who sees an artifact on a green run must not infer that these receipts are in it. So this note deliberately retired the log route in favour of an artifact route that was then deleted underneath it, and both of its named routes are inoperative. THE PRODUCER IS UNREACHABLE ON THE NAMED INVOCATION AS WELL, so restoring transport alone would not seed anything: install_floor_compile_clean_receipt's claim_executor caller sits below the required_floor_mode early return, and the only path that could reach it under required CI is the consume_floor_compile_clean_gate_verdict builtin, whose live .dag caller sits in dag/tools/dag_compile_clean_transport -- reached by compile-clean witnesses that are themselves ROUTE-GAPPED and never arrive at their subject. Measured on the certified main run: zero compile-clean-cost markers. NO BASIS MAY BE INFERRED FROM THE AGGREGATE LOG OR FABRICATED FROM AN ABSENT RECEIPT -- an empty basis must count loudly, exactly as this note already requires of BasisAbsent, and that requirement is what forbids papering over the gap while it stands, and the writers no longer mirror their bodies. The log lines are GONE, not merely deprecated: a seeding attempt that greps a run log for them will find nothing, which is why this clause is corrected rather than left to rot. BASIS OF THE CONSTANTS (worker-sized, 2026-07-31, from run 30602520347 @ 0ecb898, host srv1-01 arm64, post-#7490 fixes): whole-tree pass 258s over the ~1648-unit whole-tree entry closure (units = the leg's compiled closure module count, receipted by the first [compile-clean-cost] execution — NOT the ~2725-file module index, which overcounts by pool files outside every entry closure) = ~157ms/unit observed; per_unit_ms 320 is ~2x that rate, funding a full 2x fleet-spread host on top of the observed wall (the family margin ruling: a breach means content grew, never which host answered; pre-fix completing runs spread ~1.8x across hosts) — the batch family's 1000ms coefficient carries 1.4-1.7x the same way; overhead 60s covers the closure-size-independent tail (census fill parse ~13s fleet + governor arm). Whole-tree clamp = 60s + 1648*320ms = ~587s (~2.3x the observed 258s fleet wall). MECHANISM RECEIPTS (local x86, logic-not-cost host): green e2e via gunbc_ci_plan_artifact_plan — pass 310127ms/1648 units, WithinBudget, 1204 module rows, drift basis_absent=1205 counted, exit 0 (run at the pre-resize 200ms sizing; the arm proof is arithmetic-independent and the formula is witness-pinned at the final constants); RED control via GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS=1 receipted beside it. DISPATCH: operator direction this session ('can we add the budget gating ... i suggest we share that model' — briansrls, 2026-07-31). OPERATOR SIGNATURE (briansrls, 2026-07-31): the worker-sized constants are affirmed as proposed — overhead_seconds 60, per_unit_ms 320 ('the clamp constants you chose are fine, please proceed') — so the refusal arm is signed-live per the family raise discipline; TIGHTENING may still land by ordinary receipt note, and the first fleet observations should tighten per_unit_ms toward the measured rate."
+data gunbc_ci_compile_clean_clamp_note: String = "COMPILE-CLEAN LEG CLAMP (prelude coverage, first slice): discharges the compile-clean portion of gunbc_ci_floor_batch_clamp_note FOLLOW-UP ROW (a) — the eager compile-clean install ran OUTSIDE every batch budget and could only red at the step cap, which is how a 15m32s green gate grew past 49 minutes across #7398/#7438 with nothing naming the growth (typecheck-perf investigation, PR #7490). Same shape as the batch clamps: clamp_ms = overhead_seconds*1000 + closure_units * per_unit_ms, where closure_units is the compiled closure's MODULE COUNT — a runtime fact of the scope disposition (whole-tree ~2725 today, affected-set proportional to the diff), so the clamp re-denominates with scope exactly as batch clamps re-denominate with the affected set. Over-clamp is FLOOR-COMPILE-CLEAN-OVER-BUDGET: a typed, located walk refusal (admission grain — the compile receipt's ok is untouched, per the signed admission/verdict split in gunbc_ci_floor_batch_wall_budget_note); never a rerun, never a widen. RED-control hook GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS lowers the computed clamp (min), never raises. GROWTH DETECTION at row grain is NOT this clamp's job (the family margin ruling, 2026-07-25): per-row 2x drift against dated basis rows rides gunbc.witness_row_cost's comparator over dag/gunbc/compile_clean_cost_basis.tsv — the pass + module_typecheck rows of target/floor-compile-clean-cost-receipt.tsv, basis rows citing arm64 fleet run ids only, BasisAbsent counted until seeded from a cited run's own receipt FILE (the #7475 seeding pattern; an empty basis must count loudly, never read as no-drift). SEEDING SOURCE CORRECTED: this clause used to name the [compile-clean-cost] log lines, because the receipt file had no way off the runner and every row was mirrored into the step log to compensate — ~1,690 lines per floor run, and the same shape cost 8,614 more on the disclosure receipt. THAT REPLACEMENT ROUTE IS NOW GONE TOO, which is the correction this clause carries: it used to say the ci job uploads the receipts as the floor-receipts artifact via gunbc.ci_workflow ci_floor_receipts_upload_step, so seeding downloads the TSV instead of scraping a log. No live workflow carries that step -- it died with ci.yml in the floor cut. TRANSPORT IS NOW PARTIAL RATHER THAN ABSENT, and this clause is written at that grain because the coarser claim went stale within a day: gunbc#8875 (2026-08-22) added an upload to witnesses.yml, so DISPOSITION receipts DO leave the runner today. gunbc#8877 then replaced that single bundled artifact with one artifact per file -- required-floor-disposition, expected-red-roster-join and long-home-storage-agreement -- because the bundled form evaluates if-no-files-found once over the combined list and so cannot report a single missing file. A reader looking for the name required-floor-receipts will not find it; the population is unchanged and none of the cost receipts this note names are in any of the three. So the gap is no longer the absence of any transport; it is that the transport which exists carries a different population, and a reader who sees an artifact on a green run must not infer that these receipts are in it. So this note deliberately retired the log route in favour of an artifact route that was then deleted underneath it, and both of its named routes are inoperative. THE PRODUCER IS UNREACHABLE ON THE NAMED INVOCATION AS WELL, so restoring transport alone would not seed anything: install_floor_compile_clean_receipt's claim_executor caller sits below the required_floor_mode early return, and the only path that could reach it under required CI is the install_or_consume_floor_compile_clean_gate_receipt builtin, whose live .dag caller sits in dag/tools/dag_compile_clean_transport -- reached by compile-clean witnesses that are themselves ROUTE-GAPPED and never arrive at their subject. Measured on the certified main run: zero compile-clean-cost markers. NO BASIS MAY BE INFERRED FROM THE AGGREGATE LOG OR FABRICATED FROM AN ABSENT RECEIPT -- an empty basis must count loudly, exactly as this note already requires of BasisAbsent, and that requirement is what forbids papering over the gap while it stands, and the writers no longer mirror their bodies. The log lines are GONE, not merely deprecated: a seeding attempt that greps a run log for them will find nothing, which is why this clause is corrected rather than left to rot. BASIS OF THE CONSTANTS (worker-sized, 2026-07-31, from run 30602520347 @ 0ecb898, host srv1-01 arm64, post-#7490 fixes): whole-tree pass 258s over the ~1648-unit whole-tree entry closure (units = the leg's compiled closure module count, receipted by the first [compile-clean-cost] execution — NOT the ~2725-file module index, which overcounts by pool files outside every entry closure) = ~157ms/unit observed; per_unit_ms 320 is ~2x that rate, funding a full 2x fleet-spread host on top of the observed wall (the family margin ruling: a breach means content grew, never which host answered; pre-fix completing runs spread ~1.8x across hosts) — the batch family's 1000ms coefficient carries 1.4-1.7x the same way; overhead 60s covers the closure-size-independent tail (census fill parse ~13s fleet + governor arm). Whole-tree clamp = 60s + 1648*320ms = ~587s (~2.3x the observed 258s fleet wall). MECHANISM RECEIPTS (local x86, logic-not-cost host): green e2e via gunbc_ci_plan_artifact_plan — pass 310127ms/1648 units, WithinBudget, 1204 module rows, drift basis_absent=1205 counted, exit 0 (run at the pre-resize 200ms sizing; the arm proof is arithmetic-independent and the formula is witness-pinned at the final constants); RED control via GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS=1 receipted beside it. DISPATCH: operator direction this session ('can we add the budget gating ... i suggest we share that model' — briansrls, 2026-07-31). OPERATOR SIGNATURE (briansrls, 2026-07-31): the worker-sized constants are affirmed as proposed — overhead_seconds 60, per_unit_ms 320 ('the clamp constants you chose are fine, please proceed') — so the refusal arm is signed-live per the family raise discipline; TIGHTENING may still land by ordinary receipt note, and the first fleet observations should tighten per_unit_ms toward the measured rate."
 
 data gunbc_ci_compile_clean_clamp: RunnableBatchClamp = RunnableBatchClamp {
   overhead: second(count: 60),