Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions dag/gunbc/doc_graph_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1632,9 +1632,9 @@ data hand_authored_doc_bind_incomings: List<HandAuthoredDocBind> = [
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,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.",

Expand Down
68 changes: 65 additions & 3 deletions dag/gunbc/witness/v2_native_route.dag
Original file line number Diff line number Diff line change
@@ -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 }
Expand All @@ -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 }
Expand Down Expand Up @@ -648,6 +651,7 @@ type NativeRouteAdmissionRefusalCause
| UnattributedFileRefusalsPresent
| UnattributedHeadAdvisoriesPresent
| ContextRefusalsUnbacked
| FrontierRetirementCausesUnowned
| FalseControlNotObserved
| TrueControlNotObserved
| LivePairObservedWhileEnrolledRed
Expand Down Expand Up @@ -846,6 +850,62 @@ fn native_route_file_refusal_tally(receipt: NativeRouteReceipt) -> List<NativeRo
)
}

// A FRONTIER RETIREMENT, JOINED TO WHAT THE ROUTE OBSERVED. The frontier's population on one run
// is every file refusal and every refused member whose fatal reason is one of the retirement's
// causes. A cause with no fatal-grain ownership row makes the standing Unowned rather than
// Retired, because an uncounted cause always reads zero.
type FrontierRetirementStanding
= FrontierOpen { remaining: Int }
| FrontierRetired
| FrontierRetirementCauseUnowned { cause: Symbol }

fn native_route_frontier_cause_member(retirement: FrontierRetirement, reason: Symbol) -> 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<Symbol> = 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
Expand Down Expand Up @@ -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> = [
NativeRouteClauseCheck { holds: native_route_malformed_control_holds(receipt: receipt), cause: MalformedControlAcceptedByRoute },
Expand Down Expand Up @@ -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"
Expand Down
10 changes: 5 additions & 5 deletions docs/plans/self-host-cargo-refusal-root-partition.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion docs/plans/v2-self-host-direct-path-2026-09-06.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading