XL-2 carrier: occurrence projection progress, match arms 3+ delivered, silent-drop arms outstanding

dag/gunbc/compiler_frontend_program_status.dag

@@ -222,6 +222,10 @@ type Xl2Prerequisite
   | ElseLessIfStatementLowering
   | WildcardMatchArmResolution
   | QualifiedFieldTypeVisibility
+  | MatchEveryArmLowered
+  | EnclosingExpressionLoweredWhole
+  | DataInitializerMatchScrutineeLowering
+  | MatchArmStatementBodyLowering
 
 type Xl2PrerequisiteEvidence {
   pr: Int
@@ -262,6 +266,10 @@ data xl2_prerequisites: List<Xl2Prerequisite> = [
   ElseLessIfStatementLowering,
   WildcardMatchArmResolution,
   QualifiedFieldTypeVisibility,
+  MatchEveryArmLowered,
+  EnclosingExpressionLoweredWhole,
+  DataInitializerMatchScrutineeLowering,
+  MatchArmStatementBodyLowering,
 ]
 
 fn xl2_prerequisite_label(p: Xl2Prerequisite) -> String {
@@ -285,6 +293,10 @@ fn xl2_prerequisite_label(p: Xl2Prerequisite) -> String {
     WildcardMatchArmResolution => "a wildcard match arm `_` is a pattern form resolve does not look up, so a correct match is not refused as an unbound name"
     QualifiedFieldTypeVisibility => "a QUALIFIED field-position type name reaches the census, so field position is established as a whole, not only for bare names"
     LoweringOccurrenceProjection => "every lowered node built from an authored atom keeps that atom's minted occurrence, so a census row locates back to one source occurrence"
+    MatchEveryArmLowered => "a match lowers every arm, the third and later arms included, in source order"
+    EnclosingExpressionLoweredWhole => "an expression that contains a match or if (an operator, call or record around the block) lowers to itself with the block as one part, not to the block alone or its scrutinee"
+    DataInitializerMatchScrutineeLowering => "a match in a data initializer reads its scrutinee from the scrutinee position, not from an arm"
+    MatchArmStatementBodyLowering => "a match arm whose body is a statement block lowers the whole block, not its first expression"
   }
 }
 
@@ -375,7 +387,27 @@ fn xl2_prerequisite_standing(p: Xl2Prerequisite) -> Xl2PrerequisiteStanding {
     }
     LoweringOccurrenceProjection => PrerequisiteOutstanding {
       tracked_by: decl_ref(module_path: "gunbc.recurring_failure_mode.lowering_rebuilds_an_authored_atom_without_its_occurrence", decl_name: "lowering_rebuilds_an_authored_atom_without_its_occurrence"),
-      why: "reference-position atoms that lowering rebuilds do not keep their minted occurrence through normalize: record-literal tags and pattern constructors are lowered from their enclosing shell (v2.std.node_query construct_tag_edge), and dotted-spine segments are rebuilt as node_synthetic (v2.std.qualified_name qualified_name_spine_node). Their census rows therefore cannot be located back to a source occurrence, and XL-5's waves are exact occurrence rewrites. Binders and labels are also locus-erased but are outside the XL-2 residual. Design and ranked sites: docs/plans/lowering-occurrence-projection-design.md. The per-module count is the conservation check's, re-derived by v2.compiler.reference_conservation_census reference_conservation_stratified_sample_census rather than transcribed here. No fix has merged." as NonEmptyStr,
+      why: "Reference-position atoms that lowering rebuilds now carry their authored token's occurrence at the two sites that rebuilt them: record-literal tags and pattern constructors are lowered from their tag token (gunbc#12305, 6c3c84f7f3), and dotted-spine segments from their own tokens (gunbc#12314, b40c7f6067). The occurrence-role producer (gunbc#12317, 3ae62b426c) and the conservation census that consumes it (gunbc#12334, 60ef76cc5a) route an erased atom with a recorded DeclarationRole, or a ReferenceRole whose category is not module-scope, to `role_excluded` and a module-header segment to `header_channel` -- all outside the XL-2 residual -- so `locus_erased` counts only references that lost their locus FOR ROLE-READ PRODUCTIONS: an erased atom with no role entry is classified ErasedReference by v2.compiler.reference_conservation erased_atom_disposition and still counts in `locus_erased`, and the binders under NameRoleNotYetRead productions (below) are counted separately as `role_not_yet_read` (a reader refusal as `role_reader_refused`) without leaving it; the census sample's rule is one fold checked against its pin at the pin's revision (gunbc#12475, 987c55d26c), and every token after a line comment is located at its real source position since the lexer locus fix (gunbc#12313, 285ea309cf). The per-module count is re-derived by v2.compiler.reference_conservation_census reference_conservation_stratified_sample_census rather than transcribed here. Design: docs/plans/lowering-occurrence-projection-design.md. The rehearsal's excluded populations stand as gunbc.namespace_xl2_rehearsal_census Xl2ExcludedPopulation HeaderSegmentsNotRefusalSites (no resolve refusal locates at a header segment; counted by the census header_channel) and NestingScopedReferencesUncounted (as that arm states it; the nesting-scope ruling is pending). STILL OUTSTANDING: v2.compiler.occurrence_role dag_name_production_rows types ten binder-bearing productions NameRoleNotYetRead -- param_list, field_decl_block, generic_params, let_expr, fn_literal, arrow_lambda, operation, transport, input_block, output_block -- so a binder under any of them is still counted in locus_erased rather than role-separated, and the arm cannot be delivered until each has its reader." as NonEmptyStr,
+    }
+    MatchEveryArmLowered => PrerequisiteDelivered {
+      owner: decl_ref(module_path: "v2.test.claim.body_lowering.match_arm_list_structure", decl_name: "a_four_arm_match_lowers_exactly_four_arms"),
+      evidence: Xl2PrerequisiteEvidence { pr: 12383, merge_sha: "8ebd8b671d" as NonEmptyStr, measured_at: "8ebd8b671d" as NonEmptyStr },
+      qualification: "the arm list is read by the one comma-list reader, so a match lowers every arm in source order with each pattern keeping its own body (the_arms_keep_source_order_and_each_pattern_keeps_its_own_body), and a malformed later arm refuses rather than shortening the list (a_malformed_third_arm_refuses_rather_than_shortening_the_list); the MatchLaterArm accepted drop is retired (gunbc.recurring_failure_mode.match_arms_after_the_second_are_dropped_at_v2_body_lowering, rostered by gunbc#12309, 15bcbfa95e). Bounded to the arm LIST: what an arm's body and a data initializer's scrutinee lower to are MatchArmStatementBodyLowering and DataInitializerMatchScrutineeLowering." as NonEmptyStr,
+    }
+    EnclosingExpressionLoweredWhole => PrerequisiteDelivered {
+      owner: decl_ref(module_path: "v2.test.claim.body_lowering.enclosing_expression_structure", decl_name: "an_operand_beside_a_match_lowers_as_the_operator_over_both_operands"),
+      evidence: Xl2PrerequisiteEvidence { pr: 12436, merge_sha: "d28bf20f0e" as NonEmptyStr, measured_at: "d28bf20f0e" as NonEmptyStr },
+      qualification: "two links repaired in v2.compiler.body_lowering_fold: the body walker descends only through what does not change the expression, so a control form is lowered as the whole value only where it IS the value; and a primary whose capture is already lowered core substrate is that node, so the primary reducer no longer answers a lowered match with its scrutinee atom. `t && match w {..}` lowers as the operator over both operands and `h(a: match .., b: s)` as the call over every argument, on the value reader and on the body walker (a_call_with_a_match_argument_lowers_as_the_call_over_every_argument, the_body_walker_lowers_an_operand_beside_a_match_as_the_operator_over_both_operands, the_body_walker_lowers_a_call_with_a_match_argument_as_the_call_over_every_argument); this closes the `call(..) && match g(..) {..}` operand-collapse route. Delivers the trigger capability of gunbc.recurring_failure_mode.expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body_lowering (rostered by gunbc#12309, 15bcbfa95e). NOT claimed: body_lower_operand_ref_optional's own first-match fallback, which remains OptionalAccessorLocatedRefusal." as NonEmptyStr,
+    }
+    DataInitializerMatchScrutineeLowering => PrerequisiteDelivered {
+      owner: decl_ref(module_path: "v2.test.claim.body_lowering.match_position_structure", decl_name: "a_data_initializer_match_lowers_its_scrutinee_from_the_match_position_holds"),
+      evidence: Xl2PrerequisiteEvidence { pr: 12510, merge_sha: "b768b0f431" as NonEmptyStr, measured_at: "b768b0f431" as NonEmptyStr },
+      qualification: "v2.compiler.body_lowering_fold reads a match scrutinee from its grammar position (the binary_expr after `match`) rather than the first binary_expr found in the match subtree, so a data initializer's scrutinee, folded bottom-up before its declaration is dispatched, is no longer read from the first arm; the same match as a fn body lowers identically (the_same_match_as_a_fn_body_lowers_its_scrutinee_from_the_match_position_holds), and a spine not headed by `match` refuses as match_arm_navigation_refused. Delivers the trigger capability of gunbc.recurring_failure_mode.data_initializer_match_reads_its_scrutinee_from_an_arm_at_v2_body_lowering (rostered by gunbc#12364, b1b7aea9aa). Bounded to the scrutinee position: an expression enclosing the match is EnclosingExpressionLoweredWhole." as NonEmptyStr,
+    }
+    MatchArmStatementBodyLowering => PrerequisiteDelivered {
+      owner: decl_ref(module_path: "v2.test.claim.body_lowering.match_position_structure", decl_name: "a_match_arm_statement_body_lowers_to_the_let_binding_its_continuation_holds"),
+      evidence: Xl2PrerequisiteEvidence { pr: 12510, merge_sha: "b768b0f431" as NonEmptyStr, measured_at: "b768b0f431" as NonEmptyStr },
+      qualification: "a match arm's body is read from the right of its `=>` and a statement body lowers through the statement authority body_lower_stmt_spine that fn bodies and if-arms already use, so `X =>` then `let t = v` then `e` lowers to the let binding with its continuation instead of to `v`. Delivers the trigger capability of gunbc.recurring_failure_mode.match_arm_statement_body_lowers_to_its_first_expression_at_v2_body_lowering (rostered by gunbc#12364, b1b7aea9aa). Bounded to the arm body: the arm list is MatchEveryArmLowered." as NonEmptyStr,
     }
   }
 }

dag/test/claim/compiler_frontend_program_status_witness_test.dag

@@ -697,8 +697,8 @@ fn xl2_label_is(p: Xl2Prerequisite, want: Xl2Prerequisite) -> Bool {
   xl2_prerequisite_label(p: p) == xl2_prerequisite_label(p: want)
 }
 
-test fn xl2_prerequisites_partition_into_eleven_delivered_and_eight_outstanding() -> Bool {
-  count(xl2_prerequisites) == 19
+test fn xl2_prerequisites_partition_into_fifteen_delivered_and_eight_outstanding() -> Bool {
+  count(xl2_prerequisites) == 23
     && xl2_delivered_by(p: PlainCallArgumentReferenceVisibility, pr: 12108, merge_sha: "b0d307c31b")
     && xl2_delivered_by(p: BareFieldTypeVisibility, pr: 11574, merge_sha: "b705d17c45")
     && xl2_delivered_by(p: WholeTreeResolveCensus, pr: 11738, merge_sha: "c6b4e7ed2c")
@@ -718,6 +718,10 @@ test fn xl2_prerequisites_partition_into_eleven_delivered_and_eight_outstanding(
     && xl2_outstanding_tracked_by(p: ElseLessIfStatementLowering, decl_name: "else_less_if_statement_has_no_lowered_form")
     && xl2_delivered_by(p: WildcardMatchArmResolution, pr: 12297, merge_sha: "0579afae7f")
     && xl2_outstanding_tracked_by(p: QualifiedFieldTypeVisibility, decl_name: "a_qualified_field_type_mention_is_absent_from_the_census_today")
+    && xl2_delivered_by(p: MatchEveryArmLowered, pr: 12383, merge_sha: "8ebd8b671d")
+    && xl2_delivered_by(p: EnclosingExpressionLoweredWhole, pr: 12436, merge_sha: "d28bf20f0e")
+    && xl2_delivered_by(p: DataInitializerMatchScrutineeLowering, pr: 12510, merge_sha: "b768b0f431")
+    && xl2_delivered_by(p: MatchArmStatementBodyLowering, pr: 12510, merge_sha: "b768b0f431")
     && count(xl2_prerequisites_outstanding()) == 8
     && all(xl2_prerequisites_outstanding(),
          p => xl2_label_is(p: p, want: OptionalAccessorLocatedRefusal)
@@ -733,10 +737,10 @@ test fn xl2_prerequisites_partition_into_eleven_delivered_and_eight_outstanding(
 }
 
 // THE INVARIANT THE PARTITION MUST NOT MOVE: prerequisites are necessary, not sufficient, so
-// XL-2 stays NotDerivable and the producer literal stays Unavailable with ten of eighteen delivered
-// -- and would stay so with eighteen of eighteen, because the producer is its own deliverable.
+// XL-2 stays NotDerivable and the producer literal stays Unavailable with fifteen of twenty-three delivered
+// -- and would stay so with twenty-three of twenty-three, because the producer is its own deliverable.
 test fn xl2_stays_not_derivable_with_its_prerequisites_mostly_delivered() -> Bool {
-  count(xl2_prerequisites |> filter(p => xl2_prerequisite_is_delivered(p: p))) == 10
+  count(xl2_prerequisites |> filter(p => xl2_prerequisite_is_delivered(p: p))) == 15
     && standing_is(want: ClassNotDerivable, s: stage_status(s: StageXL2RootDeletionRehearsal))
     && match rehearsal_producer_standing() {
          RehearsalProducerUnavailable { why: _, cause: _ } => true