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
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
module gunbc.recurring_failure_mode.located_cause_folded_to_its_reason_at_a_result_boundary

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data located_cause_folded_to_its_reason_at_a_result_boundary: RecurringFailureMode = RecurringFailureMode {
identity: "located_cause_folded_to_its_reason_at_a_result_boundary" as NonEmptyStr,

receipts: [
"A failing stage computes a LOCATED, typed cause -- v2.std.diagnostic Diagnostic: reason, locus, correction, and for a rejection the whole NonEmptyDiagnostics chain -- and a result boundary downstream copies ONE FIELD out of it, the reason symbol, into the carrier it hands on. Every consumer past that boundary then reports WHAT refused and cannot report WHERE, and the information was not missing: it was in hand at the stage and discarded at the seam. DESIGN section 5 requires a typed, located refusal; this row is about the location surviving the trip through a result carrier, which the stage having produced it does not by itself secure.",

"THE INVALID STATE, stated so it can be recognised in a diff: a verdict, observation, receipt or row type with a field `reason: Symbol` where the producer that fills it holds a Diagnostic or a NonEmptyDiagnostics. The tell is the constructor: `reason: fatal_reason(d)`, `reason: d.head.reason`, or a projection function whose whole body is a fold to one Symbol. A second tell one layer up is the fold's own name -- `*_fatal_reason`, `*_last_reason` -- spelled per consumer, because each consumer that summarised re-derived the same 'the fatal is the last' fold for itself.",

"RECEIPT ONE, gunbc#11507, recorded on v2.cli.compile_cli: the native CLI's rejected arm carried `d.head.reason` into a ProcessExit whose rendered text was one sentence, so three different entries refused with the same nine words and the located fatal -- file and byte extent, already computed by the parse stage -- was printed nowhere. Repaired there by rendering the fatal's locus through lens_verdict_diagnostic_locus_text.",

"RECEIPT TWO, 2026-09-21, the native test route: v2.compiler.native_test_vocabulary NativeTestVerdict's refused arm was `NativeTestRefused { stage, reason: Symbol }`, filled at every site in v2.compiler.compile by `native_test_fatal_reason(d)`. The persisted population rows the emitted driver wrote and the admission authority judged therefore carried a stage and one symbol per refused identity. An ambiguous reference was reported as `resolve_reason_ambiguous_symbol` and nothing else, while the resolver had computed WHICH lookup was ambiguous (lexical chain, global bare index, qualified head shadowing an absolute hit) and, for the lexical case, the qualified path of every competing binder -- discarded one seam earlier still, at `SymbolIndexAtomAmbiguous`, a bare variant standing where the lookup had answered `LexicalAmbiguous { candidates }`. Repaired by carrying the stage's NonEmptyDiagnostics on the verdict, deriving the reason at the consumer through v2.std.diagnostic diagnostics_fatal_reason, and naming each competing declaration on a DeclarationLocus.",

"THE SAME SHAPE AT ANOTHER GRAIN IN THE SAME LANE, LEFT STANDING AND NAMED: NativeTestFileRefusal carries `head_reason` and `fatal_reason` for a front-end refusal whose diagnostics carry Textual file-and-extent loci -- the most actionable position the pipeline produces. The row is read by the seed host runner's TSV-shaped decoder, so widening it is a change to that decoder as well; it is the declared remainder of the package that filed this row, not an oversight.",

"RECEIPT THREE, the same night, the NEIGHBOURING SHAPE: the refusing link spelled with an ADVISORY'S name. v2.compiler.translate's grounding gate refused emission with `infer_grounding_not_derived` -- the very symbol infer carries as a frontier ADVISORY on its Accepted path for the same node (review 46789 routed the gate through canonical_grounding_from_inferred_facts precisely so that symbol would propagate). The built native CLI's refusal then read as a chain of thirty-five `infer_grounding_not_derived` with the last one picked as the fatal -- correctly picked, and unreadable: one name, two contracts (DESIGN section 3, a meaning fork), so an operator could not tell the refusal from the rows that rode along. The CLI's `reason` field compounded it by carrying `d.head.reason`, the FIRST pending advisory (the grammar-global overlap residue), so every broken entry refused under one indistinguishable reason. Repaired by giving the gate its own fatal `translate_rejected_grounding_not_derived` -- eval's gate had already drawn that line with `eval_rejected_grounding_not_derived` -- and by deriving the CLI's reason through diagnostics_fatal_reason.",

"WHY IT RECURS: the reason symbol is the field every AUTHORITY keys on -- cause-ownership tables, expected-red rosters, exclusion taxonomies all classify by reason -- so a carrier designed for the authority's question carries exactly the authority's key and nothing more, and the operator's question (where) has no field. The fix is never to add a second field beside the reason: it is to carry the Diagnostic and DERIVE the reason, so the authority reads the same symbol and the operator reads the same value.",

"RECOGNITION RULE: at any type that carries a refusal, ask what the PRODUCER held when it filled the field. If the producer held a Diagnostic or NonEmptyDiagnostics and the field is a Symbol, the boundary has folded a located cause to its name. Its neighbour: a stage that REFUSES with a reason another stage also carries as an advisory -- ask, for every `outcome_rejected(...)` whose reason is also minted on an Accepted path's `Some { diagnostics }`, whether a reader of the flat chain can tell which link refused. The counter-tell that keeps this from over-firing: a reason minted by the boundary itself, for a refusal no stage produced, legitimately starts as a Symbol -- and even then it owes a locus (native_test_refused_located demands one).",

"CEILING AND TRIGGER. The class is decidable -- a field typed Symbol filled from a value typed Diagnostic is a shape a lens can read off the Node tree -- so its ceiling is mechanically preventable at least, and structurally guaranteed where the carrier is sealed to a constructor that takes the diagnostics. This row sits at mitigatable: two receipts repaired by hand, and the reading is by reviewer. NEXT-RUNG TRIGGER, naming the capability: a lens over refusal-carrying types that refuses a Symbol-typed field whose fill site projects a Diagnostic's reason, with the file-refusal row above as its first authorable red.",
],

evidence: [],
}
58 changes: 37 additions & 21 deletions dag/gunbc/witness/v2_native_route.dag
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,9 @@ import v2.std.optional { Absent, Optional, Present }
import v2.compiler.native_test_vocabulary {
NativeTestVerdict, NativeTestPassed, NativeTestReturnedFalse, NativeTestReturnedOther, NativeTestRefused,
NativeTestStage, NativeTestStageContext, NativeTestStagePrepare, NativeTestStageEntry, NativeTestStageEval,
NativeTestFileRefusal
NativeTestFileRefusal, native_test_verdict_text
}
import v2.std.diagnostic { diagnostics_fatal_reason }
import v2.workflow.compile_door_cause_ownership {
CauseLane, DiagnosticGrain, FatalGrain, HeadGrain, cause_ownership_lookup, known_frontier_causes
}
Expand Down Expand Up @@ -134,6 +135,18 @@ type NativeRouteMemberRow {
verdict: NativeTestVerdict
}

// THE OPERATOR'S LINE FOR ONE ROW: the subject the lane keys on, then the verdict as the
// vocabulary renders it. The driver prints this on stderr for every row that did not pass,
// beside the JSON row it persists on stdout, so the command an operator runs names the failing
// subject with its stage, its cause and where the cause is -- read off the same value the row
// carries, never re-derived by the host from the bytes it wrote.
fn native_route_member_row_text(row: NativeRouteMemberRow) -> String {
concat(
native_route_identity_qualified(identity: row.identity),
concat(" ", native_test_verdict_text(verdict: row.verdict))
)
}

// THE MODULE → SOURCE-PATH RELATION, OVER THE UNIVERSE'S OWN MODULES. A Context-stage row is a
// derived classification minted by the host from a file refusal, and the derivation's join key
// is this relation: the observation names a module, the file refusal names a path, and only the
Expand Down Expand Up @@ -262,22 +275,25 @@ fn native_route_disposition(
FloorRouteGapRefusal => NativeDivergence { cause: NativeReachedRouteGap }
}
NativeTestReturnedOther => NativeDivergence { cause: NativeReturnedOtherVerdict }
NativeTestRefused { stage: stage, reason: reason } =>
match reference {
FloorRouteGapRefusal =>
match stage {
NativeTestStageEval =>
if native_route_reason_member(reason: reason, roster: native_route_effect_boundary_reasons) {
NativeAgreementRouteGap
} else {
NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
}
NativeTestStageContext => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
NativeTestStagePrepare => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
NativeTestStageEntry => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
}
FloorExpectedPass => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
FloorExpectedRed => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
NativeTestRefused { stage: stage, diagnostics: d } =>
{
let reason = diagnostics_fatal_reason(d: d)
match reference {
FloorRouteGapRefusal =>
match stage {
NativeTestStageEval =>
if native_route_reason_member(reason: reason, roster: native_route_effect_boundary_reasons) {
NativeAgreementRouteGap
} else {
NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
}
NativeTestStageContext => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
NativeTestStagePrepare => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
NativeTestStageEntry => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
}
FloorExpectedPass => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
FloorExpectedRed => NativeExclusion { cause: classify_native_refusal(stage: stage, reason: reason) }
}
}
}
}
Expand Down Expand Up @@ -791,13 +807,13 @@ fn native_route_head_advisories_attributed(receipt: NativeRouteReceipt) -> Bool
fn native_route_context_refusals_backed(receipt: NativeRouteReceipt) -> Bool {
!any(xs: receipt.population, predicate: fn(row) {
match row.verdict {
NativeTestRefused { stage: stage, reason: reason } =>
NativeTestRefused { stage: stage, diagnostics: d } =>
match stage {
NativeTestStageContext =>
!any(xs: receipt.module_source_index, predicate: fn(ms) {
ms.module == row.identity.module
&& any(xs: receipt.file_refusals, predicate: fn(fr) {
fr.path == ms.path && fr.fatal_reason == reason
fr.path == ms.path && fr.fatal_reason == diagnostics_fatal_reason(d: d)
})
})
NativeTestStagePrepare => false
Expand Down Expand Up @@ -832,7 +848,7 @@ fn native_route_false_control_holds(receipt: NativeRouteReceipt) -> Bool {
NativeTestReturnedFalse => true
NativeTestPassed => false
NativeTestReturnedOther => false
NativeTestRefused { stage: _, reason: _ } => false
NativeTestRefused { stage: _, diagnostics: _ } => false
}
Absent => false
}
Expand All @@ -845,7 +861,7 @@ fn native_route_true_control_holds(receipt: NativeRouteReceipt) -> Bool {
NativeTestPassed => true
NativeTestReturnedFalse => false
NativeTestReturnedOther => false
NativeTestRefused { stage: _, reason: _ } => false
NativeTestRefused { stage: _, diagnostics: _ } => false
}
Absent => false
}
Expand Down
6 changes: 5 additions & 1 deletion dag/std/compiler_entry.dag
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,11 @@ import std.measure {
// native_test_resolve_module / native_test_infer_resolved) and carries decls=. Its outcome names
// which arm decided the module: accepted, infer_refused, resolve_refused, or context_refused --
// the last for a module whose FILE this context already refused, which never enters the resolver,
// so its resolve span is the refusal lookup and not a resolution it did not perform. The
// so its resolve span is the refusal lookup and not a resolution it did not perform. Beside
// each persisted population row that did not pass it prints one `[native-verdict]` line on
// stderr -- gunbc.witness_v2_native_route native_route_member_row_text: the subject, the stage,
// the fatal cause and the located diagnostic chain the failing stage produced -- so the operator
// command that drains this stderr names WHERE a subject failed, not only that it did. The
// `[native-cost-partition]` verdict is native_driver_cost_account over NativeDriverExclusiveRows,
// not a second copy of the reconcile law: remainder_nanos is that fold's residual, and
// OverAttributed carries no remainder field (underflow is not a number). A non-Reconciled
Expand Down
17 changes: 16 additions & 1 deletion src/v1/05_emit_rust.dag
Original file line number Diff line number Diff line change
Expand Up @@ -17129,8 +17129,9 @@ fn emit_source_root_eval_driver_main_rs(crate_name: String, pipeline_module: Str
"\};", "\n",
"use ", crate_name, "::gunbc_witness_v2_native_route::\{", "\n",
" native_route_admission, native_route_admission_summary, native_route_admitted,", "\n",
" native_route_file_refusal_tally,", "\n",
" native_route_file_refusal_tally, native_route_member_row_text,", "\n",
"\};", "\n",
"use ", crate_name, "::v2_compiler_native_test_vocabulary::NativeTestVerdict;", "\n",
"use ", crate_name, "::v2_compiler_source_authority::\{source_root_for_storage_path, DagSourceReadWitness\};", "\n",
"use ", crate_name, "::v2_std_artifact::\{Artifact, ArtifactKind\};", "\n",
"use ", crate_name, "::v2_std_diagnostic::Outcome;", "\n",
Expand Down Expand Up @@ -17827,6 +17828,20 @@ fn emit_source_root_eval_driver_main_rs(crate_name: String, pipeline_module: Str
" \}", "\n",
" for row in population.iter() \{", "\n",
" println!(\"{}\", serde_json::to_string(row).unwrap());", "\n",
" // THE OPERATOR'S LINE, BESIDE THE PERSISTED ROW. The JSON above is the receipt; this is", "\n",
" // the same value rendered by the authority for a reader of the command's output, so a", "\n",
" // row that did not pass names its subject, stage, cause and position without anyone", "\n",
" // re-deriving them from the bytes just written. Passing rows print nothing here: the", "\n",
" // terminal marker carries their count. EXHAUSTIVE ON PURPOSE -- a verdict arm added to", "\n",
" // the vocabulary must decide here whether it is operator-visible.", "\n",
" match &*row.verdict \{", "\n",
" NativeTestVerdict::NativeTestPassed => \{\}", "\n",
" NativeTestVerdict::NativeTestReturnedFalse", "\n",
" | NativeTestVerdict::NativeTestReturnedOther", "\n",
" | NativeTestVerdict::NativeTestRefused \{ .. \} => \{", "\n",
" eprintln!(\"[native-verdict] {}\", native_route_member_row_text(row.clone()));", "\n",
" \}", "\n",
" \}", "\n",
" \}", "\n",
" let row_serialization_nanos = span_nanos(serialization_started);", "\n",
"", "\n",
Expand Down
2 changes: 1 addition & 1 deletion src/v1/stage0/src/v1_compiler_emit_rust.rs

Large diffs are not rendered by default.

36 changes: 14 additions & 22 deletions src/v2/cli/compile_cli.dag
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ import v2.compiler.self_host.compiler_closure_emit {
import v2.compiler.source_authority { SourceRootIngest }
import v2.extdeps.languages.rust { rust_target_model }
import v2.std.algebra { fold_list, length, list_reverse }
import v2.std.compilers.lexing { symbol_lexeme }
import v2.std.diagnostic { Accepted, Diagnostic, NonEmptyDiagnostics, Rejected }
import v2.std.lens_verdict { lens_verdict_diagnostic_locus_text }

import v2.std.diagnostic { Accepted, NonEmptyDiagnostics, Rejected, diagnostics_fatal, diagnostics_fatal_reason }
import v2.std.lens_verdict { lens_verdict_diagnostic_locus_text, lens_verdict_diagnostics_located_chain_text }
import v2.std.node { Symbol }
import v2.std.qualified_name { qualified_name_from_dotted_string }
import v2.std.text { String }
Expand Down Expand Up @@ -254,8 +254,9 @@ type CliRunOutcome
| CliRunRefused { reason: Symbol, detail: String }

// THE REFUSAL PRINTS ITS CAUSE, AND FOR ONE GENERATION IT DID NOT. The rejected arm already
// CARRIED `d.head.reason`, and the detail beside it said "the located cause is this refusal's
// reason" -- true of the value and false of the artifact, because the rendered main prints only the
// CARRIED `d.head.reason` (now the FATAL reason -- the head was the first advisory that happened
// to be pending, which is the wrong link for a `reason` field to name), and the detail beside it said
// "the located cause is this refusal's reason" -- true of the value and false of the artifact, because the rendered main prints only the
// `ProcessExit` reason string that `detail` becomes. So generation two refused with a sentence
// pointing at a symbol nobody could read, which is DESIGN section 5's located-where-the-author-can-
// act failure in its quietest form: the cause was computed, carried, and then dropped at the last
Expand All @@ -265,20 +266,11 @@ type CliRunOutcome
// THE WHOLE ORDERED CHAIN, BECAUSE THE HEAD IS NOT THE CAUSE. Rendering only the head answers
// `parse_grammar_choice_overlap_residue` for every entry tried; that is a grammar-global ADVISORY
// and never the fatal. The fatal diagnostic is the last one, and `parse_g0_tokens_remain_diagnostic`
// builds its locus from the first remaining token. File+extent is
// `lens_verdict_diagnostic_locus_text` — not a second `match d.at` here (DESIGN section 3).

fn cli_fatal_diagnostic(d: NonEmptyDiagnostics) -> Diagnostic {
fold_list(xs: d.tail, empty: d.head, cons: fn(acc, diag) { diag })
}

fn cli_diagnostic_chain(d: NonEmptyDiagnostics) -> String {
fold_list(
xs: d.tail,
empty: symbol_lexeme(sym: d.head.reason),
cons: fn(acc, diag) { concat(concat(acc, " -> "), symbol_lexeme(sym: diag.reason)) }
)
}
// builds its locus from the first remaining token. The fatal pick is `v2.std.diagnostic`
// `diagnostics_fatal`, the chain is `lens_verdict_diagnostics_located_chain_text` (every link with
// its locus, so thirty-five advisories in front of the fatal each say where they are), and
// file+extent is `lens_verdict_diagnostic_locus_text` — none a second spelling here (DESIGN
// section 3).

// THE EMPTY INGEST IS A REFUSAL AND NOT AN EMPTY PROGRAM, and this arm is the whole reason
// `v2_cli_run` does not call the emitter first and ask questions after.
Expand Down Expand Up @@ -315,10 +307,10 @@ fn v2_cli_run(plan: CliPlan, ingest: SourceRootIngest) -> CliRunOutcome {
}
Rejected { diagnostics: d } =>
CliRunRefused {
reason: d.head.reason,
reason: diagnostics_fatal_reason(d: d),
detail: concat(
concat("the closure did not emit; diagnostic chain: ", cli_diagnostic_chain(d: d)),
concat(" | FATAL AT ", lens_verdict_diagnostic_locus_text(d: cli_fatal_diagnostic(d: d)))
concat("the closure did not emit; diagnostic chain: ", lens_verdict_diagnostics_located_chain_text(d: d)),
concat(" | FATAL AT ", lens_verdict_diagnostic_locus_text(d: diagnostics_fatal(d: d)))
)
}
}
Expand Down
Loading