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
43 changes: 43 additions & 0 deletions src/v2/test/v2_native_route_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ import gunbc.witness_v2_native_route {
required_v2_native_job_name,
native_route_admission, native_route_admitted, native_route_admission_refused_with,
native_route_admission_summary,
native_route_file_refusals_attributed,
native_route_live_control_module,
NativeRouteCauseTally,
native_route_file_refusal_tally,
Expand Down Expand Up @@ -71,6 +72,7 @@ import v2.std.diagnostic {
Accepted, Outcome, Rejected, invariant_port_locus, Diagnostic, NonEmptyDiagnostics, Unavailable, ExternalContractUnknown
}
import v2.std.collection { List }
import std.algebra { Cons }
import v2.std.algebra { fold_list, length }
import v2.std.logic { Bool }
import v2.std.node { Symbol }
Expand Down Expand Up @@ -903,6 +905,47 @@ test fn an_unattributed_file_refusal_is_refused() -> Bool {
)
}

// THE BODY-LOWERING FATAL CAUSES OF THE BROAD RUN AT main bd2c586926b9 ARE OWNED. Supplied rows
// in the receipt's shape (DESIGN section 3, a witness discriminates at one interface): one file
// refusal per cause the run measured unowned, and the file-refusal clause holds over them. The
// paired control keeps the clause discriminating -- the same receipt plus one row whose fatal
// cause has no ownership row still fails it, so the owned rows did not become a catch-all.
fn body_lowering_frontier_refusals() -> List<NativeTestFileRefusal> {
[
file_refusal_row(path: ^bl_a, head: ^parse_grammar_choice_overlap_residue, fatal: ^body_lowering_reason_call_argument_unread),
file_refusal_row(path: ^bl_b, head: ^parse_grammar_choice_overlap_residue, fatal: ^body_lowering_reason_operator_operand_unread),
file_refusal_row(path: ^bl_c, head: ^parse_grammar_choice_overlap_residue, fatal: ^body_lowering_reason_type_annotation_not_carried),
file_refusal_row(path: ^bl_d, head: ^parse_grammar_choice_overlap_residue, fatal: ^body_lowering_reason_paren_group_unread)
]
}

test fn the_body_lowering_frontier_causes_are_owned_at_fatal_grain() -> Bool {
native_route_file_refusals_attributed(receipt: receipt_over(
universe: [],
module_source_index: [],
population: [],
file_refusals: body_lowering_frontier_refusals()
))
&& match classify_native_refusal(stage: NativeTestStageContext, reason: ^body_lowering_reason_call_argument_unread) {
CompilerFrontierAttributed { reason: _ } => true
NativeEntryResolutionLimit { reason: _ } => false
NativeEvalBoundary { reason: _ } => false
UnattributedRefusal { reason: _ } => false
}
}

test fn an_unknown_fatal_cause_beside_the_owned_ones_still_refuses_unowned() -> Bool {
!native_route_file_refusals_attributed(receipt: receipt_over(
universe: [],
module_source_index: [],
population: [],
file_refusals: Cons {
head: file_refusal_row(path: ^bl_e, head: ^parse_grammar_choice_overlap_residue, fatal: ^some_unowned_cause),
tail: body_lowering_frontier_refusals()
}
))
}

test fn an_unattributed_head_advisory_is_refused() -> Bool {
native_route_admission_refused_with(
admission: native_route_admission_with(live_pair: LivePairRequired, receipt: receipt_over(
Expand Down
24 changes: 24 additions & 0 deletions src/v2/workflow/compile_door_cause_ownership.dag
Original file line number Diff line number Diff line change
Expand Up @@ -167,6 +167,30 @@ data known_frontier_causes: List<CauseOwnership> = [
lane: SharedSelfHostCriticalPath,
flip_trigger: "a record-literal field value, match-arm body or if condition the value reader cannot lower (a function value, chiefly) is carried as its shell under this advisory instead of being dropped or truncated. (call arguments are read by gunbc#12108's reader and refuse under its own causes instead). Flips when every value shape lowers. Measured 2026-09-22 at head grain by the workload adjudicate over dag + src/v2 (count on the PR)"
},
CauseOwnership {
cause: ^body_lowering_reason_call_argument_unread,
grain: FatalGrain,
lane: SharedSelfHostCriticalPath,
flip_trigger: "value-position lowering: a call argument whose value v2.compiler.body_lowering_fold body_lower_call_arg_value cannot read refuses its module here. Dominated by function values in argument position (inline lambdas and fn literals, gunbc.recurring_failure_mode lambda_has_no_lowered_function_value_form), which gunbc#12210 lowers to the generic fn Arrow; the positional fold-step residue is gunbc#12272. Flips to Blocking when the count zeroes after both land. Measured at fatal grain by the gunbc.witness_v2_native_route census at main bd2c586926b9 over dag + src/v2 (count on the PR)"
},
CauseOwnership {
cause: ^body_lowering_reason_operator_operand_unread,
grain: FatalGrain,
lane: SharedSelfHostCriticalPath,
flip_trigger: "body-lowering modeling pass (gentle-koi-724's lane): an operator operand body_lower_read_operator_expression cannot lower -- a caret symbol (gunbc.recurring_failure_mode caret_symbol_has_no_lowered_form) or a parenthesised `as` cast (as_cast_has_no_lowered_form, whose typed cast node is gunbc#12315). Flips to Blocking when every operand shape lowers and the count zeroes. Measured at fatal grain by the gunbc.witness_v2_native_route census at main bd2c586926b9 over dag + src/v2 (count on the PR)"
},
CauseOwnership {
cause: ^body_lowering_reason_type_annotation_not_carried,
grain: FatalGrain,
lane: SharedSelfHostCriticalPath,
flip_trigger: "an authored type annotation with no carrier: a statement-form let annotation (gunbc.rung_drop typed_statement_let_refuses_until_the_bind_annotation_carrier, retired by the let-annotation Bind carrier gunbc#12322) or a fn literal's return annotation; an `as` cast's target type rides the typed cast node gunbc#12315. Flips to Blocking when both carriers land and the count zeroes. Measured at fatal grain by the gunbc.witness_v2_native_route census at main bd2c586926b9 over dag + src/v2 (count on the PR)"
},
CauseOwnership {
cause: ^body_lowering_reason_paren_group_unread,
grain: FatalGrain,
lane: SharedSelfHostCriticalPath,
flip_trigger: "value-position lowering: raised by v2.compiler.body_lowering_fold body_lower_paren_group_lowered when a parenthesised group's inner expression neither lowered bottom-up nor reads as an operand (gunbc#12173 introduced the refusal in place of the left-element narrowing). The group adds no semantics, so it owns nothing of its own: it flips when the inner value shapes lower -- function values (gunbc#12210) and `as` casts (gunbc#12315) -- and the count zeroes. Measured at fatal grain by the gunbc.witness_v2_native_route census at main bd2c586926b9 over dag + src/v2 (count on the PR)"
},
CauseOwnership {
cause: ^body_lowering_reason_statement_precedes_without_binding,
grain: FatalGrain,
Expand Down