From fb45c43daf028ecc55c94c88ed825100e42bcde9 Mon Sep 17 00:00:00 2001
From: tomoaki <whiteunyora@gmail.com>
Date: Mon, 29 Dec 2025 17:02:21 +0900
Subject: [PATCH] phase29am(p2): verify core loop body effect-only

---
 src/mir/builder/control_flow/plan/verifier.rs | 120 ++++++++++++++++++
 1 file changed, 120 insertions(+)

diff --git a/src/mir/builder/control_flow/plan/verifier.rs b/src/mir/builder/control_flow/plan/verifier.rs
index 3377f544..d9d0c407 100644
--- a/src/mir/builder/control_flow/plan/verifier.rs
+++ b/src/mir/builder/control_flow/plan/verifier.rs
@@ -18,6 +18,7 @@
 //! - V9: block_effects contains header_bb
 //! - V10: body_bb effects go in loop_plan.body (block_effects[body_bb] must be empty)
 //! - V11: Exit must be last in Seq/If branch
+//! - V12: Loop.body must be Effect-only (Seq-of-effects allowed)
 //!
 //! Phase 273 P3: V1 (Carrier completeness) removed with CoreCarrierInfo
 
@@ -124,6 +125,7 @@ impl PlanVerifier {
         }
 
         // Verify body plans (now in_loop = true)
+        Self::verify_loop_body_effect_only(&loop_plan.body, depth)?;
         for (i, plan) in loop_plan.body.iter().enumerate() {
             Self::verify_plan(plan, depth + 1, true).map_err(|e| {
                 format!("[Loop.body[{}]] {}", i, e)
@@ -278,6 +280,47 @@ impl PlanVerifier {
         Ok(())
     }
 
+    fn verify_loop_body_effect_only(plans: &[CorePlan], depth: usize) -> Result<(), String> {
+        for (i, plan) in plans.iter().enumerate() {
+            let path = format!("Loop.body[{}]", i);
+            Self::verify_body_plan_effect_only(plan, depth, &path)?;
+        }
+        Ok(())
+    }
+
+    fn verify_body_plan_effect_only(
+        plan: &CorePlan,
+        depth: usize,
+        path: &str,
+    ) -> Result<(), String> {
+        match plan {
+            CorePlan::Effect(_) => Ok(()),
+            CorePlan::Seq(plans) => {
+                for (i, nested) in plans.iter().enumerate() {
+                    let nested_path = format!("{}.Seq[{}]", path, i);
+                    Self::verify_body_plan_effect_only(nested, depth + 1, &nested_path)?;
+                }
+                Ok(())
+            }
+            _ => Err(format!(
+                "[V12] Loop body contains non-effect plan {} at depth {} ({})",
+                Self::plan_kind(plan),
+                depth,
+                path
+            )),
+        }
+    }
+
+    fn plan_kind(plan: &CorePlan) -> &'static str {
+        match plan {
+            CorePlan::Seq(_) => "Seq",
+            CorePlan::Loop(_) => "Loop",
+            CorePlan::If(_) => "If",
+            CorePlan::Effect(_) => "Effect",
+            CorePlan::Exit(_) => "Exit",
+        }
+    }
+
     /// V6: Basic ValueId validity check
     ///
     /// Note: This is a basic check. Full validity would require builder context.
@@ -297,6 +340,40 @@ mod tests {
     use crate::mir::builder::control_flow::plan::CorePhiInfo;
     use std::collections::BTreeMap;
 
+    fn make_loop_plan(body: Vec<CorePlan>) -> CoreLoopPlan {
+        let preheader_bb = BasicBlockId(0);
+        let header_bb = BasicBlockId(1);
+        let body_bb = BasicBlockId(2);
+        let step_bb = BasicBlockId(3);
+        let after_bb = BasicBlockId(4);
+
+        CoreLoopPlan {
+            preheader_bb,
+            header_bb,
+            body_bb,
+            step_bb,
+            after_bb,
+            found_bb: after_bb,
+            body,
+            cond_loop: ValueId(100),
+            cond_match: ValueId(101),
+            block_effects: vec![
+                (preheader_bb, vec![]),
+                (header_bb, vec![]),
+                (body_bb, vec![]),
+                (step_bb, vec![]),
+            ],
+            phis: vec![CorePhiInfo {
+                block: header_bb,
+                dst: ValueId(102),
+                inputs: vec![(preheader_bb, ValueId(103)), (step_bb, ValueId(104))],
+                tag: "test_phi".to_string(),
+            }],
+            frag: Frag::new(header_bb),
+            final_values: vec![("i".to_string(), ValueId(102))],
+        }
+    }
+
     #[test]
     fn test_verify_empty_seq_fails() {
         let plan = CorePlan::Seq(vec![]);
@@ -323,6 +400,49 @@ mod tests {
         assert!(result.is_ok());
     }
 
+    #[test]
+    fn test_verify_loop_body_seq_effects_ok() {
+        let body = vec![CorePlan::Seq(vec![
+            CorePlan::Effect(CoreEffectPlan::Const {
+                dst: ValueId(10),
+                value: ConstValue::Integer(1),
+            }),
+            CorePlan::Seq(vec![CorePlan::Effect(CoreEffectPlan::Const {
+                dst: ValueId(11),
+                value: ConstValue::Integer(2),
+            })]),
+        ])];
+        let plan = CorePlan::Loop(make_loop_plan(body));
+        let result = PlanVerifier::verify(&plan);
+        assert!(result.is_ok());
+    }
+
+    #[test]
+    fn test_verify_loop_body_if_fails() {
+        let if_plan = CoreIfPlan {
+            condition: ValueId(1),
+            then_plans: vec![CorePlan::Effect(CoreEffectPlan::Const {
+                dst: ValueId(2),
+                value: ConstValue::Integer(1),
+            })],
+            else_plans: None,
+        };
+        let plan = CorePlan::Loop(make_loop_plan(vec![CorePlan::If(if_plan)]));
+        let result = PlanVerifier::verify(&plan);
+        assert!(result.is_err());
+        assert!(result.unwrap_err().contains("[V12]"));
+    }
+
+    #[test]
+    fn test_verify_loop_body_exit_fails() {
+        let plan = CorePlan::Loop(make_loop_plan(vec![CorePlan::Exit(
+            CoreExitPlan::Return(None),
+        )]));
+        let result = PlanVerifier::verify(&plan);
+        assert!(result.is_err());
+        assert!(result.unwrap_err().contains("[V12]"));
+    }
+
     #[test]
     fn test_verify_if_empty_else_fails() {
         let if_plan = CoreIfPlan {