diff --git a/dag/gunbc/doc_graph_roots.dag b/dag/gunbc/doc_graph_roots.dag index 8748591c604..45756705e98 100644 --- a/dag/gunbc/doc_graph_roots.dag +++ b/dag/gunbc/doc_graph_roots.dag @@ -1632,9 +1632,9 @@ data hand_authored_doc_bind_incomings: List = [ slug: "self-host-cargo-refusal-root-partition", primary_work: DeclarationRef { module_path: "v2.compiler.self_host.v2_emitter_direct_rust_door_contract", decl_name: "v2_emitter_direct_rust_door_contract_dissolution_note", field: WholeDeclaration }, additional_works: [ - DeclarationRef { module_path: "v2.compiler.infer", decl_name: "node_grounding_frontier_note", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.compiler.infer", decl_name: "inferred_facts_not_derived", field: WholeDeclaration }, ], - dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the root partition this document coordinates is confirmed, its roots are owned, and the emitted Rust compiles for at least one module — at which point the wall it describes is history and the document deletes with this bind. Registered at subject grain: the bound declarations are the three carriers whose movement would make this document's framing false — the Band A readiness note that routes the blocker to the namespace cut, the inference frontier note whose counted-not-refused status is the correction this document records, and the direct-door dissolution note that says emission is already reached. It is a shared coordination surface for two sessions rather than an authority, which is why every claim in it names its measurement and the unconfirmed hypotheses are labelled as such; a coordination narrative that outlived its lanes would be the parallel-ledger shape DESIGN section 6 warns about.") }, + dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the root partition this document coordinates is confirmed, its roots are owned, and the emitted Rust compiles for at least one module — at which point the wall it describes is history and the document deletes with this bind. Registered at subject grain: the bound declarations are the three carriers whose movement would make this document's framing false — the Band A readiness note that routes the blocker to the namespace cut, the inference frontier producer (v2.compiler.infer inferred_facts_not_derived) whose Accepted-with-counted-diagnostic result is the correction this document records, and the direct-door dissolution note that says emission is already reached. It is a shared coordination surface for two sessions rather than an authority, which is why every claim in it names its measurement and the unconfirmed hypotheses are labelled as such; a coordination narrative that outlived its lanes would be the parallel-ledger shape DESIGN section 6 warns about.") }, }, HandAuthoredDocBind { home: PlanDoc, diff --git a/dag/gunbc/recurring_failure_mode/call_expression_erased_at_v2_body_lowering.dag b/dag/gunbc/recurring_failure_mode/call_expression_erased_at_v2_body_lowering.dag index 69375af7890..80d58630908 100644 --- a/dag/gunbc/recurring_failure_mode/call_expression_erased_at_v2_body_lowering.dag +++ b/dag/gunbc/recurring_failure_mode/call_expression_erased_at_v2_body_lowering.dag @@ -15,7 +15,7 @@ data call_expression_erased_at_v2_body_lowering: RecurringFailureMode = Recurrin "RECEIPT (2026-09-12, still-eagle-447, NAMESPACE XL-2 scoping). The normalized tree was dumped for five bodies via prepare_grammar, parse_module_prepared and normalize -- the calls v2.compiler.program_assembly program_assembly_read_to_normalized_root_prepared makes, and so the census route's own hand-off (v2.compiler.compile native_test_context_from_ingest). (That composition was DELETED by gunbc#11985, which threaded one occurrence allocator across the ingest and left it with no caller; the receipt is dated and its reading stands, but the live route is now program_assembly_read_to_normalized_root_seeded.) `{ k }` keeps `Atom:k`. `{ x }` over a parameter keeps `Atom:x`. `{ g(x: 1) }` with g declared, `{ zzz(x: 1) }` and `{ zzz(1) }` with zzz undeclared all become `Transform [ Atom:dag_token_lbrace ]`. The unprepared parse_module route (v2.compiler.staged_front_end run_front_end) dumps identically, so this is not a second lossy route beside a faithful one.", - "EVIDENCE LEVEL, stated so the receipt is not read one rung high. The dumps ran the v2 .dag through the gunbc interpreter at main f9d37e43a1, and a structural node-count fold (not a printer) agrees: the parse tree grows with a call's arguments and nesting, while the normalized body of { g(x: 1) } is exactly one node larger than { k } -- the Transform and its lbrace atom -- and { g(x: h(y: 5)) } is no larger than that. A second named argument adds one node, so the lowering keeps something per extra argument, but none of the callee or argument content. That the natively emitted normalize behaves identically is not executed. The native route gives no contrary evidence: its receipt on the #10940 head (eager-raven-113, 2026-09-12) holds exactly one Passed identity, a literal-bodied smoke test, and every richer body refuses before or at eval (v2.compiler.infer node_grounding_frontier_note). So no route has been observed to lower a call faithfully.", + "EVIDENCE LEVEL, stated so the receipt is not read one rung high. The dumps ran the v2 .dag through the gunbc interpreter at main f9d37e43a1, and a structural node-count fold (not a printer) agrees: the parse tree grows with a call's arguments and nesting, while the normalized body of { g(x: 1) } is exactly one node larger than { k } -- the Transform and its lbrace atom -- and { g(x: h(y: 5)) } is no larger than that. A second named argument adds one node, so the lowering keeps something per extra argument, but none of the callee or argument content. That the natively emitted normalize behaves identically is not executed. The native route gives no contrary evidence: its receipt on the #10940 head (eager-raven-113, 2026-09-12) holds exactly one Passed identity, a literal-bodied smoke test, and every richer body refuses before or at eval (v2.compiler.inferred_tree NodeGrounding). So no route has been observed to lower a call faithfully.", "RUNG FOUND AT: outside the ladder -- silent wrongness. The compiler Accepts a program with an undeclared callee and reports nothing.", diff --git a/dag/gunbc/witness/v2_native_route.dag b/dag/gunbc/witness/v2_native_route.dag index 5c28547ba8b..04efd64094d 100644 --- a/dag/gunbc/witness/v2_native_route.dag +++ b/dag/gunbc/witness/v2_native_route.dag @@ -1,6 +1,8 @@ module gunbc.witness_v2_native_route -import v2.std.algebra { any, count_where, filter, fold_list, is_empty, length, list_append, list_snoc_item } +import v2.std.algebra { + any, count_where, filter, fold_list, is_empty, length, list_append, list_find_first, list_snoc_item +} import v2.std.collection { List } import v2.std.integer { Int } import v2.std.logic { Bool } @@ -16,7 +18,8 @@ import v2.compiler.native_test_vocabulary { } import v2.std.diagnostic { Some, diagnostics_fatal_reason, diagnostics_has_reason } import v2.workflow.compile_door_cause_ownership { - CauseLane, DiagnosticGrain, FatalGrain, HeadGrain, cause_ownership_lookup, known_frontier_causes + CauseLane, DiagnosticGrain, FatalGrain, FrontierRetirement, HeadGrain, cause_ownership_lookup, + known_frontier_causes, known_frontier_retirements } import std.dissolution { DissolutionCondition, unbound_dissolution } import v2.workflow.floor_expected_red { floor_expected_red_roster } @@ -648,6 +651,7 @@ type NativeRouteAdmissionRefusalCause | UnattributedFileRefusalsPresent | UnattributedHeadAdvisoriesPresent | ContextRefusalsUnbacked + | FrontierRetirementCausesUnowned | FalseControlNotObserved | TrueControlNotObserved | LivePairObservedWhileEnrolledRed @@ -846,6 +850,62 @@ fn native_route_file_refusal_tally(receipt: NativeRouteReceipt) -> List Bool { + any(xs: retirement.causes, predicate: fn(c) { c == reason }) +} + +fn native_route_frontier_population(retirement: FrontierRetirement, receipt: NativeRouteReceipt) -> Int { + count_where(xs: receipt.file_refusals, predicate: fn(fr) { + native_route_frontier_cause_member(retirement: retirement, reason: fr.fatal_reason) + }) + + count_where(xs: receipt.population, predicate: fn(row) { + match row.verdict { + NativeTestRefused { stage: _, diagnostics: d } => + native_route_frontier_cause_member(retirement: retirement, reason: diagnostics_fatal_reason(d: d)) + NativeTestPassed => false + NativeTestReturnedFalse => false + NativeTestReturnedOther => false + } + }) +} + +fn native_route_frontier_retirement_standing( + retirement: FrontierRetirement, + receipt: NativeRouteReceipt +) -> FrontierRetirementStanding { + let unowned: Optional = list_find_first(xs: retirement.causes, predicate: fn(c) { + match cause_ownership_lookup(cause: c, grain: FatalGrain) { + Present { value: _ } => false + Absent => true + } + }) + let remaining = native_route_frontier_population(retirement: retirement, receipt: receipt) + match unowned { + Present { value: c } => FrontierRetirementCauseUnowned { cause: c } + Absent => + if remaining == 0 { FrontierRetired } else { FrontierOpen { remaining: remaining } } + } +} + +fn native_route_frontier_retirements_owned(receipt: NativeRouteReceipt) -> Bool { + !any(xs: known_frontier_retirements, predicate: fn(r) { + match native_route_frontier_retirement_standing(retirement: r, receipt: receipt) { + FrontierRetirementCauseUnowned { cause: _ } => true + FrontierOpen { remaining: _ } => false + FrontierRetired => false + } + }) +} + // THE HEAD REASON IS NOT DEAD RECEIPT DATA. rejected_with_pending prepends the non-fatal // advisory, so the head reason is a real observation of the frontier at a different grain — the // same observation the door ledger's own rows carry. Every file refusal's head reason must be @@ -1091,7 +1151,8 @@ fn native_route_admission_with(receipt: NativeRouteReceipt, live_pair: NativeRou NativeRouteClauseCheck { holds: native_route_exclusions_all_classified(census: census), cause: UnattributedExclusionsPresent }, NativeRouteClauseCheck { holds: native_route_file_refusals_attributed(receipt: receipt), cause: UnattributedFileRefusalsPresent }, NativeRouteClauseCheck { holds: native_route_head_advisories_attributed(receipt: receipt), cause: UnattributedHeadAdvisoriesPresent }, - NativeRouteClauseCheck { holds: native_route_context_refusals_backed(receipt: receipt), cause: ContextRefusalsUnbacked } + NativeRouteClauseCheck { holds: native_route_context_refusals_backed(receipt: receipt), cause: ContextRefusalsUnbacked }, + NativeRouteClauseCheck { holds: native_route_frontier_retirements_owned(receipt: receipt), cause: FrontierRetirementCausesUnowned } ] let after_live_pair: List = [ NativeRouteClauseCheck { holds: native_route_malformed_control_holds(receipt: receipt), cause: MalformedControlAcceptedByRoute }, @@ -1138,6 +1199,7 @@ fn native_route_admission_refusal_cause_name(cause: NativeRouteAdmissionRefusalC UnattributedFileRefusalsPresent => "unattributed_file_refusals_present" UnattributedHeadAdvisoriesPresent => "unattributed_head_advisories_present" ContextRefusalsUnbacked => "context_refusals_unbacked" + FrontierRetirementCausesUnowned => "frontier_retirement_causes_unowned" FalseControlNotObserved => "false_control_not_observed" TrueControlNotObserved => "true_control_not_observed" LivePairObservedWhileEnrolledRed => "live_pair_observed_while_enrolled_red" diff --git a/docs/plans/self-host-cargo-refusal-root-partition.md b/docs/plans/self-host-cargo-refusal-root-partition.md index d5a61577aff..6d010c1e4c3 100644 --- a/docs/plans/self-host-cargo-refusal-root-partition.md +++ b/docs/plans/self-host-cargo-refusal-root-partition.md @@ -30,11 +30,11 @@ Three separate places still say otherwise and are known-stale: - `docs/plans/v2-self-hosting.md` — "0/27 self-host-green" is still true, but its framing invites the emission reading. -**A wrong root to avoid.** `v2.compiler.infer` `node_grounding_frontier_note` says v2 derives -only 3 of 12 node kinds; the other nine carry `infer_grounding_not_derived`. True, and NOT a -blocker — `GroundingNotDerived` sits on the **Accepted** path (DESIGN §4b names it a live -specimen of `FrontierAccepted`, "the typed-located-counted diagnostic whose phase result is -still `Accepted`"). smart-ram-730 read that count as a refusal and had to withdraw it. +**A wrong root to avoid.** A node infer cannot ground carries `infer_grounding_not_derived`, +and that is NOT a blocker: `v2.compiler.infer` `inferred_facts_not_derived` returns it on the +**Accepted** path (DESIGN §4b names it a live specimen of `FrontierAccepted`, "the +typed-located-counted diagnostic whose phase result is still `Accepted`"). How many nodes carry it +is counted by that diagnostic, not by a kind count. smart-ram-730 read that diagnostic as a refusal and had to withdraw it. Likewise `v2_emitter_direct_rust_door_contract` IS red, but it refuses on **source fidelity** against a canned string with ~17 hand-authored groundings — a fixture-exactness check, not the emission path. Do not generalize from either. diff --git a/docs/plans/v2-self-host-direct-path-2026-09-06.md b/docs/plans/v2-self-host-direct-path-2026-09-06.md index ef0416f5ee0..51e680ba943 100644 --- a/docs/plans/v2-self-host-direct-path-2026-09-06.md +++ b/docs/plans/v2-self-host-direct-path-2026-09-06.md @@ -30,7 +30,7 @@ What you do **not** get (§7's honesty boundary): the compiler does not invent u Each line names the producer that re-derives the state. Run it; do not believe this sentence. - **Axis A — the real path, slice by slice.** The add slice (the `add` fn of `std.integer`) is green end-to-end on the dag path as of #10673: infer derives grounding by declared-inhabitant roster membership, and the ingest→compile round trip is byte-faithful. Instrument: `gunbc run --source-root dag --source-root src/v2 --entry src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag --function add_slice_stage_verdicts_entry`. The **direct-rust-door** (roadmap `v2-emitter-direct-rust-door`) is **green by execution as of 2026-09-06**: the production walk reaches `ArtifactProduced`, all five leaf projections establish (source fidelity byte-equal to `direct_rust_door_expected_source`, producer identity, seed-emitter absence, `SourceProduced` qualification, missing-rule refusal), and the known-red admission row deleted per its own dissolution, promoting the group root to the lane's permanent regression wall. Instrument: `claim_batch --source-root dag --source-root src/v2 --entry src/v2/test/claim/long/direct_rust_door_production_group_test.dag --functions direct_rust_door_production_group_closing_expectation_holds` (a `long/` row — it reconstructs the pipeline per evaluation; the cost defect is declared in the test module's header). -- **The grounding frontier.** The door specimen's frontier is closed, and the parse-product family followed on 2026-09-07: the declared-inhabitant roster-membership derivation widened from the dag roster to the closed ingest set (dag, python, typescript), closing the python and typescript fixtures' frontiers and greening the four same-language round-trips. The add-slice stall's trigger fired and it retired per §4b(4). Six derivation rules now cover declared-inhabitants roster membership (language-general), binding denotation, Conj/Arrow product introduction, canonical-operations and grammar-productions roster membership, and binding references from the enclosing arrow's domain. The remaining frontier is the six node kinds with no derivation rule yet (the `node_grounding_frontier_note` in `04_infer.dag` is the standing carrier). +- **The grounding frontier.** The door specimen's frontier is closed, and the parse-product family followed on 2026-09-07: the declared-inhabitant roster-membership derivation widened from the dag roster to the closed ingest set (dag, python, typescript), closing the python and typescript fixtures' frontiers and greening the four same-language round-trips. The add-slice stall's trigger fired and it retired per §4b(4). The remaining frontier is counted, not transcribed: `v2.workflow.compile_door_cause_ownership` `node_grounding_frontier_retirement` names its causes, and `gunbc.witness_v2_native_route` `native_route_frontier_retirement_standing` joins them to the route's observed population. - **Axis B — the native closure (XL-N).** The XL-0 gate (`cargo check` = 0 on the emitted compiler closure) is **not satisfied**; the issue's own receipt table records that the closure reached complete rustc type checking for the first time at XL-0A and carries the honest error population there. gunbc#10266 (fabricated runtime panics on representation-identical casts) is filed as an independent compiler slice on this path. Instrument (the issue's own): `gunbc compile --source-root dag --source-root src/v2 --entry src/v2/compiler/00_compile.dag --target rust --output-dir /tmp/v2emit && cd /tmp/v2emit && cargo check --message-format short`. - **Axis C — the seed dissolves.** `v2.compiler.self_host.seed_retention_frontier` holds every retained seed file as a declared row; `undeclared_reason_rows()` is the prioritizable debt, and the census refuses unrostered retention in three directions. `v2.compiler.self_host.emit_coverage_frontier`'s `interpreter_retained_rows()` and `v2.compiler.self_host.native_routing_frontier`'s roster cover the witness-execution axes. The first InterpreterRetained → SelfEmittedNative promotion after classical_not landed 2026-09-07: the add family's row flipped when `emit_host_native_only_add_holds` (+ its wrong-octet broken control) landed in the file-grain-enrolled native-only verdict entry — the emitted add crate's stdout pinned to its expected octet with `eval()` never called, program-side discrimination staying with the family's equals_eval primitive-five/six pair. **The emit coverage frontier closed 2026-09-08: all fifteen roster rows are SelfEmittedNative, `interpreter_retained_rows()` is empty**, each row backed by a native-only verdict arm (positive + wrong-octet broken control) in the same enrolled entry, and the `retained_via_eval_agreement` row constructor was deleted with the last flip (DESIGN §3c). This closes axis (a) — witness-body-runs-native — only; it says nothing about which engine compiled the compiler itself (axis (b), the regen-grain flip, remains operator-gated below). Instrument: `claim_batch --source-root dag --source-root src/v2 --entry src/v2/test/claim/execution/long/emit_host_native_only_verdict_test.dag` (offline wet legs — real cargo build and native run per leg). - **Wave position.** Per the wave doc, Wave 1's four exit items all carry landed receipts; Wave 2 (first real flips — emit-surface tracks self-emit, behaviorally verify, and **replace** their v1 counterparts) is the open wave. The wave doc's header records that its roster carrier was deleted and per-module dispositions must be re-derived from the emitter — which is what the door-first sequence below does. diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 0656216d9e0..6bc56cb15c2 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -121,7 +121,7 @@ type AlgebraRef { witness: Node } -// TWO POSITION-SCOPED DERIVATIONS SIT BESIDE THE KIND RULES THIS ROW LISTS. An accepted int +// TWO POSITION-SCOPED DERIVATIONS SIT BESIDE THE KIND RULES. An accepted int // literal's magnitude payload derives against the integer authority's own types // (infer_literal_payload_entries), and a childless Conj in an Arrow's domain position derives as // the empty product (infer_arrow_empty_domain_edge). A node's KIND does not decide whether it @@ -129,7 +129,6 @@ type AlgebraRef { // door probe (fixture.native_cli_door.door_probe) met this frontier only through Atom and Conj // nodes, because body lowering handed infer a data declaration's surface tokens (fixed at // v2.compiler.body_lowering_fold body_lower_data_decl_to_member). -data node_grounding_frontier_note: String = "GroundingNotDerived is v2's typed inference frontier, not a failure arm and not an escape hatch. v2 derives a node's type for six of the closed vocabulary's twelve node kinds (Branch, Match, Loop, Transform add-shape only, and Conj and Arrow by product introduction — 6 connectives + 6 behaviors = 12); the other six kinds, and every other Transform shape, have no derivation rule yet. The Conj and Arrow rules are compositional: a non-roster Conj or Arrow whose every child carries DerivedGrounding derives with the same shape re-formed over the children's grounding evidence as its evidence, and one with any frontier or absent child stays frontier — the derivation discharges only on a fully-evidenced child spine. Above the kind rules sit five specimen-scope derivations, all lookups into declared authorities rather than inventions: a node declared in any ingested language authority's declared-inhabitants roster derives with that roster root as its grounding evidence (infer_node_declared_in_language_inhabitants) — deep subtree membership over the closed ingest set (dag, python, typescript), so a declared inhabitant's leaf fact atoms derive exactly as the inhabitant node itself does; an Atom whose identity is a canonical dag binding with a declared denotation derives with that denotation as its evidence (dag_binding_denotation) — the resolver already bound the surface spelling to the canonical binding, and the authority fixes what the binding denotes; a node that is a member of the target-model authority's canonical-operations roster derives with that roster root as its evidence (infer_node_declared_in_canonical_operations) — the resolver canonicalizes surface operators to those declared operations; a node that is a member of the dag grammar authority's productions roster derives with that roster root as its evidence (infer_node_declared_in_dag_grammar_productions) — the bridge projects a production's parse into (identity atom, captured content) pairs; and an Atom whose binding an enclosing arrow's domain declares derives with the declared domain type as its evidence (infer_find_arrow_domain_type_in_tree) — the declaration-site annotation, itself derived. The binding-reference lookup is scope-naive (whole-tree, first match), the same interim the branch-operand path already uses. All five delete in favor of consuming resolution output when the resolver hands infer declaration-resolved identities directly (the namespace migration's completed state); specimens no authority declares stay on the frontier unchanged. Before this carrier existed the nine were routed through solve_constraints with the singleton candidate set [root] under a predicate that reduces to root == root, and the resulting grounding carried the SOURCE NODE as its structural evidence — i.e. as the node's resolved type (inferred_facts_resolved_type reads that field), so every literal, binding and operation in v2 was typed as itself and every downstream consumer read that as an established judgment. Each frontier node now carries a typed, located, counted diagnostic (infer_grounding_not_derived) on the Accepted path, so the deficit's frequency is observable and prioritizable rather than zeroed by construction (DESIGN §5). dissolve-on: a behavior-specific derivation rule lands for a kind, at which point that kind moves to DerivedGrounding and its frontier count drops; the carrier deletes when all twelve kinds derive." fn infer_grounding_not_derived_diagnostic(at: Locus) -> Diagnostic { Diagnostic { @@ -566,7 +565,7 @@ fn infer_node_declared_in_language_inhabitants_bool(n: Node) -> Bool { // child spine is evidenced, so a partially-derived product can never masquerade as grounded // (DESIGN section 5). Roster members keep their roster evidence (the authority's declaration // outranks composition for what the language itself declares), and a childless Conj or Arrow has -// no evidence to compose and stays frontier. This is the frontier note's dissolve-on for these +// no evidence to compose and stays frontier. This discharges the frontier for these // two kinds: the kind-level rule the specimen-scope roster lookups stood in for. fn infer_type_node_awaits_product_row(n: Node) -> Bool { @@ -814,7 +813,7 @@ fn inferred_facts_witness_for_node(tree: InferredTree, node: Node) -> Witness Outcome { // THE CHECK READS INFER'S OWN FRONTIER DIAGNOSTICS, ONE PASS. Infer carries a typed // `infer_grounding_not_derived` on its Accepted path for every node it leaves on the frontier -// (v2.compiler.infer node_grounding_frontier_note), so "no such diagnostic" is "every recorded node +// (v2.compiler.inferred_tree NodeGrounding), so "no such diagnostic" is "every recorded node // derived", which is what translate's gate reads. An earlier cut looked every node up in the facts // map, which is a linear scan per node, and cost 81k eval steps per claim on the required floor // against a 72.3k budget. The claim's subject is infer's verdict, not the lookup. diff --git a/src/v2/test/native_lane_smoke_test.dag b/src/v2/test/native_lane_smoke_test.dag index 7c72ec98e1d..6ee7e6ed05d 100644 --- a/src/v2/test/native_lane_smoke_test.dag +++ b/src/v2/test/native_lane_smoke_test.dag @@ -10,7 +10,7 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } // one member to reach NativeTestPassed where the floor expects pass. The body is deliberately // the grounded fragment only: a Bool literal, the shape the lane's live-verdict control pair // (v2.native_lane_fixture.control) already proves reaches a verdict — every richer body today -// meets the node grounding frontier (v2.compiler.infer node_grounding_frontier_note) at the +// meets the node grounding frontier (v2.compiler.inferred_tree NodeGrounding) at the // eval gate, measured 2026-09-10 at 261 members across 110 modules. This member is the // route's canary, not a stand-in for the frontier: the census's typed exclusion counts carry // the frontier's size, and as grounding derivation covers more node kinds the positive diff --git a/src/v2/test/v2_native_route_test.dag b/src/v2/test/v2_native_route_test.dag index 68250f3d24f..615bcf6c8ae 100644 --- a/src/v2/test/v2_native_route_test.dag +++ b/src/v2/test/v2_native_route_test.dag @@ -35,7 +35,12 @@ import gunbc.witness_v2_native_route { native_route_admission_summary, native_route_live_control_module, NativeRouteCauseTally, - native_route_file_refusal_tally + native_route_file_refusal_tally, + FrontierRetirementStanding, FrontierOpen, FrontierRetired, FrontierRetirementCauseUnowned, + native_route_frontier_retirement_standing +} +import v2.workflow.compile_door_cause_ownership { + FrontierRetirement, node_grounding_frontier_retirement } import gunbc.repo_self_warning_policy { repo_self_warning_denial_rustflags } import v2.compiler.compile { @@ -1574,6 +1579,83 @@ test fn the_refusal_tally_counts_each_refusal_once_at_fatal_grain() -> Bool { && (fold_list(xs: rows, empty: 0, cons: fn(acc, row) { acc + row.file_refusals }) == 3) } +// ── a frontier's retirement, joined to the route's population ── +// +// THE GROUNDING FRONTIER COUNTS BOTH POPULATIONS. One file refusal and one eval-stage member +// refusal under two different grounding causes are both the frontier; a refusal under an +// unrelated cause is not. So the standing is Open with exactly two remaining. A standing that +// read only the file tally would say one, and one that matched any cause would say three. +fn grounding_frontier_probe_receipt() -> NativeRouteReceipt { + receipt_over( + universe: [], + module_source_index: [], + population: [ + refused_row( + module: "v2.test.frontier_probe", + declaration: "eval_refused", + stage: NativeTestStageEval, + reason: ^eval_rejected_grounding_not_derived + ), + refused_row( + module: "v2.test.frontier_probe", + declaration: "resolve_refused", + stage: NativeTestStagePrepare, + reason: ^resolve_reason_unbound_symbol + ) + ], + file_refusals: [ + file_refusal_row(path: ^frontier_a, head: ^infer_grounding_not_derived, fatal: ^translate_rejected_grounding_not_derived) + ] + ) +} + +test fn the_grounding_frontier_is_open_over_both_populations() -> Bool { + match native_route_frontier_retirement_standing( + retirement: node_grounding_frontier_retirement, + receipt: grounding_frontier_probe_receipt() + ) { + FrontierOpen { remaining: n } => n == 2 + FrontierRetired => false + FrontierRetirementCauseUnowned { cause: _ } => false + } +} + +// POSITIVE CONTROL: a population none of whose refusals is a grounding cause retires the frontier. +test fn the_grounding_frontier_retires_when_no_cause_is_observed() -> Bool { + match native_route_frontier_retirement_standing( + retirement: node_grounding_frontier_retirement, + receipt: receipt_over( + universe: [], + module_source_index: [], + population: [], + file_refusals: [ + file_refusal_row(path: ^frontier_b, head: ^resolve_reason_unbound_symbol, fatal: ^resolve_reason_unbound_symbol) + ] + ) + ) { + FrontierRetired => true + FrontierOpen { remaining: _ } => false + FrontierRetirementCauseUnowned { cause: _ } => false + } +} + +// THE DISCRIMINATING RED: a retirement over a cause the ownership table does not count at fatal +// grain would read zero, and so Retired, forever. It must stand Unowned, naming the cause, and +// that must hold even when the observed population is empty. +test fn a_retirement_over_an_unowned_cause_is_not_retired() -> Bool { + match native_route_frontier_retirement_standing( + retirement: FrontierRetirement { + frontier: ^frontier_probe, + causes: [^infer_grounding_not_derived, ^frontier_probe_cause_nobody_owns] + }, + receipt: receipt_over(universe: [], module_source_index: [], population: [], file_refusals: []) + ) { + FrontierRetirementCauseUnowned { cause: c } => c == ^frontier_probe_cause_nobody_owns + FrontierRetired => false + FrontierOpen { remaining: _ } => false + } +} + // ── the live pair, enrolled expecting-red (manager ruling 2026-09-21) ── // A REAL REFUSAL CHAIN: the lookup class first (advisory), the fatal reason last -- the carriage diff --git a/src/v2/workflow/compile_door_cause_ownership.dag b/src/v2/workflow/compile_door_cause_ownership.dag index 41ea557437c..2df7d29432f 100644 --- a/src/v2/workflow/compile_door_cause_ownership.dag +++ b/src/v2/workflow/compile_door_cause_ownership.dag @@ -201,29 +201,54 @@ data known_frontier_causes: List = [ cause: ^infer_grounding_not_derived, grain: FatalGrain, lane: SharedSelfHostCriticalPath, - flip_trigger: "the node grounding frontier (v2.compiler.infer node_grounding_frontier_note) observed at prepare, where the carried diagnostic is fatal rather than eval-gated; flips to Blocking when the count zeroes, which the frontier note's dissolve-on conditions own. Measured 2026-09-10 at fatal grain by the gunbc.witness_v2_native_route census over the lane's source roots dag + src/v2 (2 v2.test.* members, both in v2.test.manual.recompute_trace_probe)" + flip_trigger: "the node grounding frontier (v2.compiler.inferred_tree NodeGrounding) observed at prepare, where the carried diagnostic is fatal rather than eval-gated; retires under node_grounding_frontier_retirement. Measured 2026-09-10 at fatal grain by the gunbc.witness_v2_native_route census over the lane's source roots dag + src/v2 (2 v2.test.* members, both in v2.test.manual.recompute_trace_probe)" }, CauseOwnership { cause: ^infer_grounding_demanded_not_derived, grain: FatalGrain, lane: SharedSelfHostCriticalPath, - flip_trigger: "a consumer demanded a canonical grounding (coercion, translate's coerce fold, eval's constraints) of a node the grounding frontier left underived (v2.compiler.infer node_grounding_frontier_note). Until 2026-09-21 this refusal was spelled with the advisory's own symbol, infer_grounding_not_derived; same frontier, split out so a chain can tell the refusing link from the frontier rows in front of it. Flips to Blocking when the count zeroes, which the frontier note's dissolve-on conditions own" + flip_trigger: "a consumer demanded a canonical grounding (coercion, translate's coerce fold, eval's constraints) of a node the grounding frontier left underived (v2.compiler.inferred_tree NodeGrounding). Until 2026-09-21 this refusal was spelled with the advisory's own symbol, infer_grounding_not_derived; same frontier, split out so a chain can tell the refusing link from the frontier rows in front of it. Retires under node_grounding_frontier_retirement" }, CauseOwnership { cause: ^translate_rejected_grounding_not_derived, grain: FatalGrain, lane: SharedSelfHostCriticalPath, - flip_trigger: "translate's grounding gate refuses a node it must emit whose inferred facts carry no DerivedGrounding -- the node grounding frontier (v2.compiler.infer node_grounding_frontier_note) observed at emission. Until 2026-09-21 this refusal was spelled with the advisory's own symbol, infer_grounding_not_derived, so its population was counted under that row; it is the same frontier at the emit stage, split out so a chain can tell the refusing link from the frontier rows in front of it. Flips to Blocking when the count zeroes, which the frontier note's dissolve-on conditions own" + flip_trigger: "translate's grounding gate refuses a node it must emit whose inferred facts carry no DerivedGrounding -- the node grounding frontier (v2.compiler.inferred_tree NodeGrounding) observed at emission. Until 2026-09-21 this refusal was spelled with the advisory's own symbol, infer_grounding_not_derived, so its population was counted under that row; it is the same frontier at the emit stage, split out so a chain can tell the refusing link from the frontier rows in front of it. Retires under node_grounding_frontier_retirement" }, CauseOwnership { cause: ^eval_rejected_grounding_not_derived, grain: FatalGrain, lane: SharedSelfHostCriticalPath, - flip_trigger: "eval's grounding gate refuses a body whose inferred facts carry no DerivedGrounding — the node grounding frontier (v2.compiler.infer node_grounding_frontier_note); flips to Blocking when the count zeroes, which the frontier note's dissolve-on conditions own. Measured 2026-09-10 at fatal grain by the gunbc.witness_v2_native_route census over the lane's source roots dag + src/v2 (261 v2.test.* members across 110 modules)" + flip_trigger: "eval's grounding gate refuses a body whose inferred facts carry no DerivedGrounding — the node grounding frontier (v2.compiler.inferred_tree NodeGrounding); retires under node_grounding_frontier_retirement. Measured 2026-09-10 at fatal grain by the gunbc.witness_v2_native_route census over the lane's source roots dag + src/v2 (261 v2.test.* members across 110 modules)" } ] +// A FRONTIER'S RETIREMENT CONDITION, TYPED. A frontier observed under several causes (one per stage +// that meets it) retires when EVERY one of its causes counts zero at fatal grain over the route's +// population. Each cause must also be owned by a fatal-grain row of known_frontier_causes, because a +// retirement over a cause nobody counts would read as retired at zero forever. +// gunbc.witness_v2_native_route native_route_frontier_retirement_standing joins this condition to +// the route's derived tally, and admission refuses a retirement whose causes are unowned. +type FrontierRetirement { + frontier: Symbol + causes: List +} + +// The node grounding frontier: v2.compiler.inferred_tree NodeGrounding's GroundingNotDerived arm, +// counted by infer's own advisory and by each stage that refuses an underived node. +data node_grounding_frontier_retirement: FrontierRetirement = FrontierRetirement { + frontier: ^node_grounding_frontier, + causes: [ + ^infer_grounding_not_derived, + ^infer_grounding_demanded_not_derived, + ^translate_rejected_grounding_not_derived, + ^eval_rejected_grounding_not_derived + ] +} + +data known_frontier_retirements: List = [node_grounding_frontier_retirement] + fn cause_ownership_lookup(cause: Symbol, grain: DiagnosticGrain) -> Optional { list_find_first( xs: known_frontier_causes,