From 3bdac839b9bf15d5b73a833f8c645c79f732a49b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 13 Aug 2026 03:59:28 +0000 Subject: [PATCH] BL-0: give the body-lowering frontier its third state MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The observer carried two arms over three reachable states, and the missing arm failed OPEN: every Rejected outcome fell to the else branch and reported BodyLoweringLowered. The instrument used to measure the body-lowering gap was counting failures as successes, so any population read through it undercounted by exactly the refusals. That arm is reachable by construction, not in theory: the rejection- propagation repair deliberately made body_lower_finish_for_normalize propagate genuine rejection through rejected_with_pending, and this classifier then discarded the distinction it created. Recognition had the same fail-open by a second route. It read the diagnostic HEAD alone, while retention travels through diagnostics_merge and rejected_with_pending — both of which place OUTER diagnostics first — so a retained body behind any pending diagnostic also read as lowered. It now scans the whole list. Six claims green by execution. RED verified by restoring the previous classifier: the rejection claim, the rejection-diagnostics claim and the behind-a-pending-diagnostic claim all red, while the three negative controls stay green — so the claims pin these two defects rather than failing broadly. The controls are the load-bearing half: a classifier that answered retained more often would satisfy the positive claims and destroy the count. Two existing consumers gain the third arm. Residue declared on the carrier: recognition still reads an encoding rather than a producer-returned variant, correct for every encoding the single retention producer can emit, with dissolve-on naming the producer change that makes this function the identity. First step of the sequence gunbc.roadmap_authority already declares: honest frontier, then the normalized-tree construction boundary, then the retained population to zero. Co-Authored-By: Claude Opus 5 (1M context) --- src/v2/compiler/body_lowering_fold.dag | 36 +++++- .../fn_body_seam_witness_helpers.dag | 2 + .../frontier_three_state_test.dag | 118 ++++++++++++++++++ ...ymbol_index_body_producer_witness_test.dag | 2 + 4 files changed, 152 insertions(+), 6 deletions(-) create mode 100644 src/v2/test/claim/body_lowering/frontier_three_state_test.dag diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index 92348887877..c4a9b3942c9 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -31,7 +31,7 @@ import v2.extdeps.languages.dag { parse_production_emitted_identity_optional, qualified_name_from_module_node, } -import v2.std.algebra { list_append, list_snoc_item, length, zip_eq } +import v2.std.algebra { fold_list, list_append, list_snoc_item, length, zip_eq } import v2.std.collection { List, list_at_optional @@ -50,6 +50,7 @@ import v2.std.diagnostic { Accepted, Diagnostic, Diagnostics, + NonEmptyDiagnostics, ExternalContractUnknown, Outcome, Rejected, @@ -130,15 +131,30 @@ fn body_lowering_forward_fold_surface_identities_agree() -> Bool { } } +data body_lowering_frontier_three_state_note: String = "THE FRONTIER OBSERVER MUST SPAN THE STATE SPACE THE PRODUCER CAN REACH. It carried two arms over three reachable states, and the missing arm failed OPEN: every Rejected outcome fell to the else branch and reported BodyLoweringLowered — a body that failed to lower, counted as one that lowered. That is the instrument used to measure the body-lowering gap reporting failures as successes, so every population derived through it undercounted by exactly the refusals. Reachability is not hypothetical: body_lower_finish_for_normalize propagates genuine rejection through rejected_with_pending by construction (see the rejection-propagation note above), so the arm this classifier lacked is the one that repair deliberately created.\n\nRecognition also read the diagnostic HEAD alone. Retention travels through diagnostics_merge and rejected_with_pending, which place OUTER diagnostics first, so a retained body behind any pending diagnostic classified as Lowered — the same fail-open by a second route. It now scans the whole diagnostic list for the retained reason.\n\nRESIDUE, declared rather than closed: recognition still reads diagnostics rather than the producer returning a variant, so this is a classifier over an encoding, not a structural read. It is correct for every encoding the single retention producer (body_lower_wrapper_retained_shell) can emit, and it would be wrong if a second producer ever emitted retention differently — which is why retention keeps exactly one producer. Dissolve-on: body_lower_after_children returns BodyLoweringFrontierDisposition directly, at which point this function is the identity and disappears with the encoding." + type BodyLoweringFrontierDisposition = BodyLoweringLowered | BodyLoweringWrapperRetained { reason: Symbol } + | BodyLoweringRejected { diagnostics: NonEmptyDiagnostics } + +fn body_lowering_diagnostic_is_wrapper_retained(d: Diagnostic) -> Bool { + d.reason == ^body_lowering_reason_wrapper_retained_emitted +} + +fn body_lowering_any_diagnostic_is_wrapper_retained(ne: NonEmptyDiagnostics) -> Bool { + fold_list( + xs: ne.tail, + empty: body_lowering_diagnostic_is_wrapper_retained(d: ne.head), + cons: fn(found, d) { found || body_lowering_diagnostic_is_wrapper_retained(d: d) } + ) +} fn body_lower_outcome_is_wrapper_retained(o: Outcome) -> Bool { match o { Accepted { value: _, diagnostics: d } => match d { - Some { diagnostics: ne } => ne.head.reason == ^body_lowering_reason_wrapper_retained_emitted + Some { diagnostics: ne } => body_lowering_any_diagnostic_is_wrapper_retained(ne: ne) None => false } Rejected { diagnostics: _ } => false @@ -146,10 +162,18 @@ fn body_lower_outcome_is_wrapper_retained(o: Outcome) -> Bool { } fn body_lower_outcome_frontier_disposition(o: Outcome) -> BodyLoweringFrontierDisposition { - if body_lower_outcome_is_wrapper_retained(o: o) { - BodyLoweringWrapperRetained { reason: ^body_lowering_reason_wrapper_retained_emitted } - } else { - BodyLoweringLowered + match o { + Rejected { diagnostics: r } => BodyLoweringRejected { diagnostics: r } + Accepted { value: _, diagnostics: d } => + match d { + Some { diagnostics: ne } => + if body_lowering_any_diagnostic_is_wrapper_retained(ne: ne) { + BodyLoweringWrapperRetained { reason: ^body_lowering_reason_wrapper_retained_emitted } + } else { + BodyLoweringLowered + } + None => BodyLoweringLowered + } } } diff --git a/src/v2/test/claim/body_lowering/fn_body_seam_witness_helpers.dag b/src/v2/test/claim/body_lowering/fn_body_seam_witness_helpers.dag index 958871750bd..dfba44d3db3 100644 --- a/src/v2/test/claim/body_lowering/fn_body_seam_witness_helpers.dag +++ b/src/v2/test/claim/body_lowering/fn_body_seam_witness_helpers.dag @@ -2,6 +2,7 @@ module v2.test.claim.body_lowering.fn_body_seam_witness_helpers import v2.compiler.body_lowering_fold { BodyLoweringLowered, + BodyLoweringRejected, BodyLoweringWrapperRetained, body_lower_fn_body_shell, body_lower_outcome_frontier_disposition @@ -126,6 +127,7 @@ fn wave1_gate1_a1_fn_body_seam_red_invalid_shell_wrapper_retained_holds() -> Boo match body_lower_outcome_frontier_disposition(o: body_lower_fn_body_shell(shell: shell)) { BodyLoweringWrapperRetained { reason: r } => r == ^body_lowering_reason_wrapper_retained_emitted BodyLoweringLowered => false + BodyLoweringRejected { diagnostics: _ } => false } } diff --git a/src/v2/test/claim/body_lowering/frontier_three_state_test.dag b/src/v2/test/claim/body_lowering/frontier_three_state_test.dag new file mode 100644 index 00000000000..892473ae6d7 --- /dev/null +++ b/src/v2/test/claim/body_lowering/frontier_three_state_test.dag @@ -0,0 +1,118 @@ +module v2.test.claim.body_lowering.frontier_three_state + +import v2.compiler.body_lowering_fold { + BodyLoweringLowered, + BodyLoweringRejected, + BodyLoweringWrapperRetained, + body_lower_outcome_frontier_disposition, + body_lower_wrapper_retained_shell +} +import std.algebra { Cons, Empty } +import v2.std.diagnostic { + Accepted, + Diagnostic, + NonEmptyDiagnostics, + None, + Outcome, + Rejected, + Some, + Textual, + Unavailable, + UserInputBoundary, + WholeFile, + diagnostics_singleton +} +import v2.std.logic { Bool } +import v2.std.node { Conj, Node, Symbol, TypeNode, node_synthetic } +import v2.std.text { String } + +data frontier_three_state_note: String = "The frontier observer over the three states its producer can reach. It carried two arms, and the missing one failed OPEN: a Rejected outcome fell to the else branch and reported BodyLoweringLowered — the instrument that measures the body-lowering gap counting failures as successes, so every population read through it undercounted by exactly the refusals. Recognition also read the diagnostic HEAD alone, while retention travels through diagnostics_merge and rejected_with_pending, which put OUTER diagnostics first — so a retained body behind any pending diagnostic was also reported lowered. Both routes are asserted here, and both are the executed RED: on the previous classifier the rejection claim and the behind-a-pending-diagnostic claim return Lowered. The negative controls matter as much: an unrelated diagnostic must NOT manufacture retention, and a clean accept must stay lowered — a classifier that answered retained more often would satisfy the positive claims while destroying the count." + +fn probe_shell() -> Node { + node_synthetic(kind: TypeNode { connective: Conj }, children: []) +} + +fn unrelated_diagnostic() -> Diagnostic { + Diagnostic { + reason: ^frontier_three_state_unrelated_reason, + at: Textual { file: ^frontier_three_state_probe_file, extent: WholeFile }, + correction: Unavailable { reason: UserInputBoundary } + } +} + +fn retained_diagnostic() -> Diagnostic { + Diagnostic { + reason: ^body_lowering_reason_wrapper_retained_emitted, + at: Textual { file: ^frontier_three_state_probe_file, extent: WholeFile }, + correction: Unavailable { reason: UserInputBoundary } + } +} + +fn rejected_outcome() -> Outcome { + Rejected { + diagnostics: NonEmptyDiagnostics { head: unrelated_diagnostic(), tail: Empty } + } +} + +fn clean_accept() -> Outcome { + Accepted { value: probe_shell(), diagnostics: None } +} + +fn accept_with_unrelated_diagnostic() -> Outcome { + Accepted { + value: probe_shell(), + diagnostics: Some { diagnostics: diagnostics_singleton(d: unrelated_diagnostic()) } + } +} + +fn retention_behind_a_pending_diagnostic() -> Outcome { + Accepted { + value: probe_shell(), + diagnostics: Some { + diagnostics: NonEmptyDiagnostics { + head: unrelated_diagnostic(), + tail: Cons { head: retained_diagnostic(), tail: Empty } + } + } + } +} + +fn disposition_name(o: Outcome) -> Symbol { + match body_lower_outcome_frontier_disposition(o: o) { + BodyLoweringLowered => ^disposition_lowered + BodyLoweringWrapperRetained { reason: _ } => ^disposition_wrapper_retained + BodyLoweringRejected { diagnostics: _ } => ^disposition_rejected + } +} + +fn rejected_disposition_keeps_its_reason() -> Symbol { + match body_lower_outcome_frontier_disposition(o: rejected_outcome()) { + BodyLoweringRejected { diagnostics: ne } => ne.head.reason + BodyLoweringWrapperRetained { reason: _ } => ^not_rejected + BodyLoweringLowered => ^not_rejected + } +} + +test fn a_rejection_is_never_reported_as_lowered_holds() -> Bool { + disposition_name(o: rejected_outcome()) == ^disposition_rejected +} + +test fn a_rejection_carries_its_diagnostics_through_holds() -> Bool { + rejected_disposition_keeps_its_reason() == ^frontier_three_state_unrelated_reason +} + +test fn retention_behind_a_pending_diagnostic_is_still_retention_holds() -> Bool { + disposition_name(o: retention_behind_a_pending_diagnostic()) == ^disposition_wrapper_retained +} + +test fn the_sole_retention_producer_reads_as_retention_holds() -> Bool { + disposition_name(o: body_lower_wrapper_retained_shell(shell: probe_shell())) == ^disposition_wrapper_retained +} + +test fn an_unrelated_diagnostic_does_not_manufacture_retention_holds() -> Bool { + disposition_name(o: accept_with_unrelated_diagnostic()) == ^disposition_lowered +} + +test fn a_clean_accept_is_lowered_holds() -> Bool { + disposition_name(o: clean_accept()) == ^disposition_lowered +} diff --git a/src/v2/test/claim/self_host/wave1_gate1_a1_symbol_index_body_producer_witness_test.dag b/src/v2/test/claim/self_host/wave1_gate1_a1_symbol_index_body_producer_witness_test.dag index 300a73bff5c..44a13f306e1 100644 --- a/src/v2/test/claim/self_host/wave1_gate1_a1_symbol_index_body_producer_witness_test.dag +++ b/src/v2/test/claim/self_host/wave1_gate1_a1_symbol_index_body_producer_witness_test.dag @@ -9,6 +9,7 @@ import v2.compiler.body_lowering_fold { body_lowering_match_spine_identity_absent_dispatch_holds, body_lowering_match_spine_identity_absent_sniff_holds, BodyLoweringLowered, + BodyLoweringRejected, BodyLoweringWrapperRetained } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -44,6 +45,7 @@ fn wave1_gate1_a1_wrapper_retained_red_control_holds() -> Bool { match body_lower_outcome_frontier_disposition(o: body_lower_fn_decl_to_arrow(shell: shell)) { BodyLoweringWrapperRetained { reason: r } => r == ^body_lowering_reason_wrapper_retained_emitted BodyLoweringLowered => false + BodyLoweringRejected { diagnostics: _ } => false } }