Land the add-slice per-stage verdict instrument named as the floor_expected_red note's producer

src/v2/compiler/self_host/candidate_generation_stage_verdicts.dag

@@ -0,0 +1,120 @@
+module v2.compiler.self_host.candidate_generation_stage_verdicts
+
+import v2.compiler.infer { infer }
+import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate }
+import v2.std.algebra { Cons, Empty, fold_list, list_snoc_item }
+import v2.std.collection { List }
+import v2.std.compilers.target_model { TargetModel }
+import v2.std.diagnostic {
+  Accepted,
+  Diagnostics,
+  NonEmptyDiagnostics,
+  None,
+  Rejected,
+  Some
+}
+import v2.std.node { Node, Symbol }
+
+// THE PER-STAGE VERDICT INSTRUMENT `v2.workflow.floor_expected_red` NAMES AS THE REPRODUCIBLE
+// PRODUCER of its add-slice receipt. That receipt was measured once, at main 3a8344b5c, by a
+// throwaway probe: `infer(dag_add_emitted_root)` answered `infer_accepted` while
+// `generate_translate_self_emit_candidate` over the same root and `dag_add_target_model` refused
+// headed by `infer_grounding_not_derived`. No `.dag` entry re-derived it, so a reader could not
+// re-run it; this module is the standing entry, parameterized over the one root and target so
+// the seam is measured, never transcribed (DESIGN section 6).
+//
+// THE VERDICT VOCABULARY IS THE RECEIPT'S. `infer_verdict` is `infer_accepted` or
+// `infer_rejected`. `composition_verdict` is `candidate_accepted` when the infer-then-translate
+// composition accepts, and otherwise the rejection's head reason -- today
+// `infer_grounding_not_derived`, the typed frontier `v2.compiler.infer`
+// `node_grounding_frontier_note` declares: infer derives grounding for four of the closed
+// vocabulary's twelve kinds and records GroundingNotDerived for the rest, which
+// `translate_grounding_derived_gate_subtree` then refuses.
+//
+// THE CARRIED-REASONS FIELDS ARE THE LOAD-BEARING HALF THE VERDICT SYMBOLS CANNOT SAY. Infer
+// ACCEPTS this root while CARRYING the frontier diagnostic on its accepted path, so the enrolled
+// witness's `d == None` conjunct fails even where the composition reaches acceptance -- the
+// roster note's "both conjuncts fail for the one cause". `infer_carried_reasons` surfaces what
+// infer carried; `composition_carried_reasons` is the composition's accepted-path diagnostics or,
+// on refusal, the full rejection chain head-first (which bind_outcome prefixes with infer's
+// pending diagnostics, so today it is the one frontier reason repeated).
+//
+// THIS INSTRUMENT DOES NOT RETIRE WHEN THE ADD-SLICE STALL
+// (`gunbc.guarantee_stall.self_host_candidate_generation_add_slice_stall`) DISSOLVES. It is the
+// standing measurement of a production seam, and its verdicts flipping to
+// `candidate_accepted` with empty carried lists is the signal the stall's trigger fired. It
+// retires only if the `generate_translate_self_emit_candidate` seam itself dissolves.
+
+type CandidateGenerationStageVerdicts {
+  infer_verdict: Symbol
+  infer_carried_reasons: List<Symbol>
+  composition_verdict: Symbol
+  composition_carried_reasons: List<Symbol>
+}
+
+fn non_empty_diagnostic_reasons(d: NonEmptyDiagnostics) -> List<Symbol> {
+  Cons {
+    head: d.head.reason,
+    tail: fold_list(
+      xs: d.tail,
+      empty: Empty,
+      cons: fn(acc, diag) { list_snoc_item(xs: acc, item: diag.reason) }
+    )
+  }
+}
+
+fn diagnostics_carried_reasons(d: Diagnostics) -> List<Symbol> {
+  match d {
+    None => Empty
+    Some { diagnostics: ne } => non_empty_diagnostic_reasons(d: ne)
+  }
+}
+
+fn candidate_generation_composition_verdicts(
+  resolved_module: Node,
+  dag_target: TargetModel,
+  infer_verdict: Symbol,
+  infer_carried_reasons: List<Symbol>
+) -> CandidateGenerationStageVerdicts {
+  match generate_translate_self_emit_candidate(
+    resolved_module: resolved_module,
+    dag_target: dag_target
+  ) {
+    Accepted { value: _, diagnostics: d } =>
+      CandidateGenerationStageVerdicts {
+        infer_verdict: infer_verdict,
+        infer_carried_reasons: infer_carried_reasons,
+        composition_verdict: ^candidate_accepted,
+        composition_carried_reasons: diagnostics_carried_reasons(d: d)
+      }
+    Rejected { diagnostics: d } =>
+      CandidateGenerationStageVerdicts {
+        infer_verdict: infer_verdict,
+        infer_carried_reasons: infer_carried_reasons,
+        composition_verdict: d.head.reason,
+        composition_carried_reasons: non_empty_diagnostic_reasons(d: d)
+      }
+  }
+}
+
+fn candidate_generation_stage_verdicts(
+  resolved_module: Node,
+  dag_target: TargetModel
+) -> CandidateGenerationStageVerdicts {
+  match infer(tree: resolved_module) {
+    Accepted { value: _, diagnostics: d } =>
+      candidate_generation_composition_verdicts(
+        resolved_module: resolved_module,
+        dag_target: dag_target,
+        infer_verdict: ^infer_accepted,
+        infer_carried_reasons: diagnostics_carried_reasons(d: d)
+      )
+    Rejected { diagnostics: d } =>
+      candidate_generation_composition_verdicts(
+        resolved_module: resolved_module,
+        dag_target: dag_target,
+        infer_verdict: ^infer_rejected,
+        infer_carried_reasons: non_empty_diagnostic_reasons(d: d)
+      )
+  }
+}

src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag

@@ -0,0 +1,110 @@
+module v2.test.execution.self_host_candidate_generation_stage_verdicts
+
+import std.process { ExitSuccess, ProcessExit, exit_failure }
+import v2.compiler.self_host.candidate_generation_stage_verdicts {
+  CandidateGenerationStageVerdicts,
+  candidate_generation_stage_verdicts
+}
+import v2.test.execution.dag_add_emit_round_trip {
+  dag_add_emitted_root,
+  dag_add_target_model
+}
+import v2.std.algebra { Empty, fold_list, is_empty, list_snoc_item }
+import v2.std.collection { List }
+import v2.std.compilers.lexing { symbol_lexeme }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import v2.std.logic { Bool }
+import v2.std.node { Symbol }
+import v2.std.text { String, string_join }
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+// THE ADD-SLICE BINDING OF `v2.compiler.self_host.candidate_generation_stage_verdicts` -- the
+// instrument the `v2.workflow.floor_expected_red` add-slice roster note names as the producer of
+// its per-stage receipt. `add_slice_stage_verdicts` is the pure entry over the slice's own
+// fixture (`dag_add_emitted_root`, `dag_add_target_model`); `add_slice_stage_verdicts_entry` is
+// the runnable `gunbc run --function` form, exiting nonzero with the verdicts rendered while the
+// composition refuses, and ExitSuccess only when infer accepts clean and the composition accepts
+// clean -- the enrolled witness's green state.
+//
+// THE TWO WITNESSES ARE DELIBERATELY ASYMMETRIC. `add_slice_infer_accepts_holds` is a PERMANENT
+// positive control: infer accepting this root is the fact the roster note's structural account
+// could not establish, and it stays true after the repair lands.
+// `add_slice_composition_refuses_at_the_grounding_frontier_holds` pins TODAY's frontier state --
+// composition refusal headed by `infer_grounding_not_derived`, with infer carrying that same
+// reason and nothing else -- so the instrument's composition arm has a discriminating consumer
+// (DESIGN section 5). It is expected to RED on the day
+// `gunbc.guarantee_stall.self_host_candidate_generation_add_slice_stall`'s trigger lands; the
+// repair rewrites it to assert `candidate_accepted` with empty carried lists -- the DESIGN 4b(4)
+// flip from frontier guard to permanent regression control -- in the same change that removes the
+// roster row.
+
+fn add_slice_stage_verdicts() -> CandidateGenerationStageVerdicts {
+  candidate_generation_stage_verdicts(
+    resolved_module: dag_add_emitted_root,
+    dag_target: dag_add_target_model
+  )
+}
+
+fn symbol_list_text(xs: List<Symbol>) -> String {
+  string_join(
+    fields: fold_list(
+      xs: xs,
+      empty: Empty,
+      cons: fn(acc, sym) { list_snoc_item(xs: acc, item: symbol_lexeme(sym: sym)) }
+    ),
+    separator: ", "
+  )
+}
+
+fn add_slice_stage_verdicts_text(v: CandidateGenerationStageVerdicts) -> String {
+  concat(
+    "add-slice per-stage verdicts: infer=",
+    concat(
+      symbol_lexeme(sym: v.infer_verdict),
+      concat(
+        " infer_carried=[",
+        concat(
+          symbol_list_text(xs: v.infer_carried_reasons),
+          concat(
+            "] composition=",
+            concat(
+              symbol_lexeme(sym: v.composition_verdict),
+              concat(
+                " composition_carried=[",
+                concat(symbol_list_text(xs: v.composition_carried_reasons), "]")
+              )
+            )
+          )
+        )
+      )
+    )
+  )
+}
+
+fn add_slice_stage_verdicts_entry() -> ProcessExit {
+  let verdicts = add_slice_stage_verdicts()
+  if (verdicts.infer_verdict == ^infer_accepted)
+    && is_empty(xs: verdicts.infer_carried_reasons)
+    && (verdicts.composition_verdict == ^candidate_accepted)
+    && is_empty(xs: verdicts.composition_carried_reasons) {
+    ExitSuccess
+  } else {
+    exit_failure(reason: add_slice_stage_verdicts_text(v: verdicts))
+  }
+}
+
+test fn add_slice_infer_accepts_holds() -> Bool {
+  add_slice_stage_verdicts().infer_verdict == ^infer_accepted
+}
+
+test fn add_slice_composition_refuses_at_the_grounding_frontier_holds() -> Bool {
+  let verdicts = add_slice_stage_verdicts()
+  (verdicts.composition_verdict == ^infer_grounding_not_derived)
+    && !is_empty(xs: verdicts.infer_carried_reasons)
+    && fold_list(
+      xs: verdicts.infer_carried_reasons,
+      empty: true,
+      cons: fn(acc, reason) { acc && (reason == ^infer_grounding_not_derived) }
+    )
+}

src/v2/workflow/floor_expected_red.dag

@@ -1003,20 +1003,18 @@ fn floor_expected_red_chunk_interpreter_first_optional_divergence() -> List<Stri
 // dag add slice and holds only on `Accepted`, with the emitted node equal to
 // `dag_emitted_add_fn_node()` and no diagnostic carried.
 //
-// A RECEIPT, AND EXPLICITLY NOT AN INSTRUMENT -- stated because DESIGN's
-// name-the-instrument-never-transcribe-its-output ruling reaches this paragraph, and half of it
-// bites here. At main 3a8344b5c, a probe module returning each stage's verdict as a Symbol
-// answered `infer_accepted` for `infer(dag_add_emitted_root)` and `infer_grounding_not_derived`
-// for `generate_translate_self_emit_candidate` over that same root and `dag_add_target_model`.
-// Infer ACCEPTS; the composition refuses.
-//
-// WHAT THE RULING DOES AND DOES NOT REACH HERE. Its subject is a live claim transcribed as a
-// standing figure, which rots because the thing it describes moves. This one names a fixed tree,
-// so it stays true of that tree forever -- the dated-receipt half the ruling preserves. What it
-// DOES reach is reproducibility: the probe was a throwaway module and no `.dag` entry point
-// re-derives this, so a reader cannot re-run it. That gap is this note's own next-rung trigger: a
-// `.dag` entry returning the per-stage verdicts for one root would let this paragraph name a
-// producer instead of a commit.
+// A RECEIPT THAT NOW NAMES ITS PRODUCER. At main 3a8344b5c, a throwaway probe module returning
+// each stage's verdict as a Symbol answered `infer_accepted` for `infer(dag_add_emitted_root)`
+// and `infer_grounding_not_derived` for `generate_translate_self_emit_candidate` over that same
+// root and `dag_add_target_model`. Infer ACCEPTS; the composition refuses. The measurement stays
+// because it is a dated receipt about a fixed tree, true of that tree forever. The
+// reproducibility gap this note named as its own next-rung trigger is now CLOSED:
+// `v2.compiler.self_host.candidate_generation_stage_verdicts` `candidate_generation_stage_verdicts`
+// returns the per-stage verdicts for one root and target, and
+// `v2.test.execution.self_host_candidate_generation_stage_verdicts` binds it to this slice --
+// `add_slice_stage_verdicts` the pure entry, `add_slice_stage_verdicts_entry` the runnable
+// `gunbc run --function` form -- so this paragraph names a producer instead of a commit, as
+// DESIGN's name-the-instrument-never-transcribe-its-output ruling requires.
 //
 // IT IS NOT DELETED IN FAVOUR OF THE STRUCTURAL ACCOUNT BELOW, because that account cannot
 // establish it. Reading the gate tells you translate CAN refuse an underived grounding; it cannot