diff --git a/src/v2/compiler/self_host/candidate_generation_stage_verdicts.dag b/src/v2/compiler/self_host/candidate_generation_stage_verdicts.dag new file mode 100644 index 00000000000..a0e23454e24 --- /dev/null +++ b/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 + composition_verdict: Symbol + composition_carried_reasons: List +} + +fn non_empty_diagnostic_reasons(d: NonEmptyDiagnostics) -> List { + 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 { + 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 +) -> 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) + ) + } +} diff --git a/src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag b/src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag new file mode 100644 index 00000000000..ba33e9656d8 --- /dev/null +++ b/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) -> 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) } + ) +} diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 018f1a66827..5051120bab5 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -1003,20 +1003,18 @@ fn floor_expected_red_chunk_interpreter_first_optional_divergence() -> List