From 15c2eda1cf2b6fc4ba01d989a8401d6bd1ef5f02 Mon Sep 17 00:00:00 2001 From: nyash-codex Date: Thu, 18 Dec 2025 09:13:08 +0900 Subject: [PATCH] feat(control_tree): Phase 130 assign var/add in if-only normalized --- .../normalized_shadow/env_layout.rs | 5 +- .../normalized_shadow/legacy/mod.rs | 120 +++++++++++++++++- .../normalized_shadow/normalized_verifier.rs | 37 ++++++ 3 files changed, 155 insertions(+), 7 deletions(-) diff --git a/src/mir/control_tree/normalized_shadow/env_layout.rs b/src/mir/control_tree/normalized_shadow/env_layout.rs index 2c88aaf4..9d03a0f6 100644 --- a/src/mir/control_tree/normalized_shadow/env_layout.rs +++ b/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 = 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 = contract .reads .iter() .filter(|name| available_inputs.contains_key(*name)) + .filter(|name| !writes_set.contains(name)) .cloned() .collect(); diff --git a/src/mir/control_tree/normalized_shadow/legacy/mod.rs b/src/mir/control_tree/normalized_shadow/legacy/mod.rs index 78b664b1..a85cb064 100644 --- a/src/mir/control_tree/normalized_shadow/legacy/mod.rs +++ b/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, value_ast: &Option, @@ -169,8 +169,9 @@ impl LegacyLowerer { next_value_id: &mut u32, env: &mut BTreeMap, ) -> 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 + 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 + pattern or wait for future phases", + )); + } + + // Left must be variable + let lhs_var = match &**left { + ASTNode::Variable { name, .. } => name.clone(), + _ => { + 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 + ", + )); + } + }; + + // 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 + ", + )); + } + }; + + // 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 + 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(()) + } _ => { - // Phase 128 limitation: only int literal supported + // 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 + Hint: Use supported pattern or wait for future phases" )) } } diff --git a/src/mir/control_tree/normalized_shadow/normalized_verifier.rs b/src/mir/control_tree/normalized_shadow/normalized_verifier.rs index 598b4746..a1a4e279 100644 --- a/src/mir/control_tree/normalized_shadow/normalized_verifier.rs +++ b/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, + 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(()) +}