BL-0: three-state frontier disposition, rejection carries diagnostics

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,26 +131,49 @@ 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<Node>) -> 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
   }
 }
 
 fn body_lower_outcome_frontier_disposition(o: Outcome<Node>) -> 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
+      }
   }
 }
 

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
   }
 }
 

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<Node> {
+  Rejected {
+    diagnostics: NonEmptyDiagnostics { head: unrelated_diagnostic(), tail: Empty }
+  }
+}
+
+fn clean_accept() -> Outcome<Node> {
+  Accepted { value: probe_shell(), diagnostics: None }
+}
+
+fn accept_with_unrelated_diagnostic() -> Outcome<Node> {
+  Accepted {
+    value: probe_shell(),
+    diagnostics: Some { diagnostics: diagnostics_singleton(d: unrelated_diagnostic()) }
+  }
+}
+
+fn retention_behind_a_pending_diagnostic() -> Outcome<Node> {
+  Accepted {
+    value: probe_shell(),
+    diagnostics: Some {
+      diagnostics: NonEmptyDiagnostics {
+        head: unrelated_diagnostic(),
+        tail: Cons { head: retained_diagnostic(), tail: Empty }
+      }
+    }
+  }
+}
+
+fn disposition_name(o: Outcome<Node>) -> 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
+}

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
   }
 }