feat(control_tree): Phase 130 assign var/add in if-only normalized

src/mir/control_tree/normalized_shadow/env_layout.rs

@@ -27,12 +27,15 @@ impl EnvLayout {
     ) -> Self {
         // Phase 125 P2: writes from contract
         let writes: Vec<String> = contract.writes.iter().cloned().collect();
+        let writes_set: std::collections::BTreeSet<&String> = contract.writes.iter().collect();
 
-        // Phase 125 P2: inputs = reads ∩ available_inputs (deterministic order)
+        // Phase 125 P2: inputs = (reads ∩ available_inputs) \ writes
+        // inputs are read-only by definition; if a variable is written, it must not be treated as an input.
         let inputs: Vec<String> = contract
             .reads
             .iter()
             .filter(|name| available_inputs.contains_key(*name))
+            .filter(|name| !writes_set.contains(name))
             .cloned()
             .collect();
 

src/mir/control_tree/normalized_shadow/legacy/mod.rs

@@ -161,7 +161,7 @@ impl LegacyLowerer {
         }
     }
 
-    /// Phase 128: Lower assign statement (int literal only)
+    /// Phase 128-130: Lower assign statement (int literal, variable, add)
     pub fn lower_assign_stmt(
         target: &Option<String>,
         value_ast: &Option<crate::mir::control_tree::step_tree::AstNodeHandle>,
@@ -169,8 +169,9 @@ impl LegacyLowerer {
         next_value_id: &mut u32,
         env: &mut BTreeMap<String, ValueId>,
     ) -> Result<(), String> {
-        use crate::ast::{ASTNode, LiteralValue};
-        use crate::mir::join_ir::{ConstValue, JoinInst, MirLikeInst};
+        use crate::ast::{ASTNode, BinaryOperator, LiteralValue};
+        use crate::mir::join_ir::{BinOpKind, ConstValue, JoinInst, MirLikeInst};
+        use crate::mir::join_ir::lowering::error_tags;
 
         // Check target
         let target_name = target
@@ -182,8 +183,9 @@ impl LegacyLowerer {
             "[phase128/assign/value] Assign value AST is missing".to_string()
         })?;
 
-        // Parse value - Phase 128: int literal only
+        // Parse value - Phase 128: int literal, Phase 130 P1: variable, Phase 130 P2: add
         match value_ast.0.as_ref() {
+            // Phase 128: Integer literal
             ASTNode::Literal {
                 value: LiteralValue::Integer(i),
                 ..
@@ -202,10 +204,116 @@ impl LegacyLowerer {
 
                 Ok(())
             }
+            // Phase 130 P1: Variable (x = y)
+            ASTNode::Variable { name, .. } => {
+                // RHS must resolve from env (writes or inputs)
+                let src_vid = env.get(name).copied().ok_or_else(|| {
+                    error_tags::freeze_with_hint(
+                        "phase130/assign/var/rhs_missing",
+                        &format!("RHS variable '{name}' not found in env"),
+                        "ensure the variable is defined before assignment (in writes or inputs)",
+                    )
+                })?;
+
+                // Phase 130 P1: Variable assignment in Normalized IR
+                // In the continuation-passing style, we just update the env map.
+                // The actual SSA phi/merge happens at function boundaries via env args.
+                // No instruction emission needed here.
+                env.insert(target_name.clone(), src_vid);
+
+                Ok(())
+            }
+            // Phase 130 P2: BinaryOp (x = x + <int literal> only)
+            ASTNode::BinaryOp {
+                operator,
+                left,
+                right,
+                ..
+            } => {
+                // Phase 130 P2 contract: only Add with specific shape
+                if !matches!(operator, BinaryOperator::Add) {
+                    return Err(error_tags::freeze_with_hint(
+                        "phase130/assign/add/unsupported_op",
+                        &format!("Phase 130 only supports Add operator, got {:?}", operator),
+                        "use x = x + <literal> pattern or wait for future phases",
+                    ));
+                }
+
+                // Left must be variable
+                let lhs_var = match &**left {
+                    ASTNode::Variable { name, .. } => name.clone(),
                     _ => {
-                // Phase 128 limitation: only int literal supported
+                        return Err(error_tags::freeze_with_hint(
+                            "phase130/assign/add/lhs_not_var",
+                            "Phase 130 Add: LHS must be a variable",
+                            "use pattern x = x + <literal>",
+                        ));
+                    }
+                };
+
+                // Right must be integer literal
+                let rhs_int = match &**right {
+                    ASTNode::Literal {
+                        value: LiteralValue::Integer(i),
+                        ..
+                    } => *i,
+                    _ => {
+                        return Err(error_tags::freeze_with_hint(
+                            "phase130/assign/add/rhs_not_int_literal",
+                            "Phase 130 Add: RHS must be integer literal",
+                            "use pattern x = x + <literal>",
+                        ));
+                    }
+                };
+
+                // Phase 130 P2 contract: dst must equal lhs (x = x + 3, not y = x + 3)
+                if target_name != &lhs_var {
+                    return Err(error_tags::freeze_with_hint(
+                        "phase130/assign/add/dst_neq_lhs",
+                        &format!(
+                            "Phase 130 Add: dst '{}' must equal lhs '{}' (x = x + 3 pattern)",
+                            target_name, lhs_var
+                        ),
+                        "use pattern x = x + <literal> where dst == lhs",
+                    ));
+                }
+
+                // Load lhs from env
+                let lhs_vid = env.get(&lhs_var).copied().ok_or_else(|| {
+                    error_tags::freeze_with_hint(
+                        "phase130/assign/add/lhs_missing",
+                        &format!("Add LHS variable '{}' not found in env", lhs_var),
+                        "ensure the variable is defined before the add operation",
+                    )
+                })?;
+
+                // Create constant for RHS
+                let rhs_vid = ValueId(*next_value_id);
+                *next_value_id += 1;
+                body.push(JoinInst::Compute(MirLikeInst::Const {
+                    dst: rhs_vid,
+                    value: ConstValue::Integer(rhs_int),
+                }));
+
+                // Generate BinOp Add
+                let result_vid = ValueId(*next_value_id);
+                *next_value_id += 1;
+                body.push(JoinInst::Compute(MirLikeInst::BinOp {
+                    dst: result_vid,
+                    op: BinOpKind::Add,
+                    lhs: lhs_vid,
+                    rhs: rhs_vid,
+                }));
+
+                // Update env
+                env.insert(target_name.clone(), result_vid);
+
+                Ok(())
+            }
+            _ => {
+                // Out of scope
                 Err(format!(
-                    "[phase128/assign/unsupported] Phase128 supports int literal only  Hint: Assign RHS must be an integer literal (e.g., x = 42)"
+                    "[phase130/assign/unsupported] Phase 130 supports: int literal, variable, or x = x + <int literal>  Hint: Use supported pattern or wait for future phases"
                 ))
             }
         }

src/mir/control_tree/normalized_shadow/normalized_verifier.rs

@@ -5,6 +5,8 @@
 
 use crate::mir::join_ir::{JoinFuncId, JoinInst, JoinModule};
 use crate::mir::join_ir::lowering::error_tags;
+use super::env_layout::EnvLayout;
+use std::collections::BTreeMap;
 
 /// Verify Normalized JoinModule structure emitted by the shadow lowerer.
 ///
@@ -224,3 +226,38 @@ pub fn verify_normalized_structure(
         )),
     }
 }
+
+/// Phase 130 P3: Verify env map keyset stays within env layout
+///
+/// ## Contract
+/// - The env map must not introduce variables outside the env layout (`writes + inputs`)
+///
+/// ## Implementation Note
+/// This is a structural check only. It does not (yet) prove that `inputs` are never
+/// reassigned; it only ensures the env map does not grow beyond the declared layout.
+pub fn verify_env_writes_discipline(
+    env_map: &BTreeMap<String, crate::mir::ValueId>,
+    env_layout: &EnvLayout,
+    context: &str,
+) -> Result<(), String> {
+    let expected_fields: std::collections::BTreeSet<&String> = env_layout
+        .writes
+        .iter()
+        .chain(env_layout.inputs.iter())
+        .collect();
+
+    for var_name in env_map.keys() {
+        if !expected_fields.contains(var_name) {
+            return Err(error_tags::freeze_with_hint(
+                "phase130/verifier/env_unexpected_var",
+                &format!(
+                    "{}: unexpected variable '{}' in env map (not in writes or inputs)",
+                    context, var_name
+                ),
+                "ensure env updates only reference variables from the env layout (writes + inputs)",
+            ));
+        }
+    }
+
+    Ok(())
+}