# This is a combination of 16 commits.

# This is the 1st commit message:

wip: issue/88

# This is the commit message leanEthereum#2:

wip: issue/88

# This is the commit message leanEthereum#3:

wip: issue/88

# This is the commit message leanEthereum#4:

wip: issue/88

# This is the commit message leanEthereum#5:

wip: issue/88

# This is the commit message leanEthereum#6:

shrink test_match

# This is the commit message leanEthereum#7:

wip: issue/88

# This is the commit message leanEthereum#8:

remove mark_vars_as_declared

# This is the commit message leanEthereum#9:

wip: issue/88

# This is the commit message leanEthereum#10:

wip: issue/88

# This is the commit message leanEthereum#11:

wip: issue/88

# This is the commit message leanEthereum#12:

reverse stack trace order

# This is the commit message leanEthereum#13:

add failing test case from shrinking WHIR recursion

# This is the commit message leanEthereum#14:

wip: issue/88: bugfix: eliminate name shadowing

# This is the commit message leanEthereum#15:

refactor: remove declared_vars

# This is the commit message leanEthereum#16:

wip: issue/88

Author: morganthomas

crates/lean_compiler/src/a_simplify_lang.rs

@@ -326,7 +326,7 @@ fn check_expr_scoping(expr: &Expression, ctx: &Context) {
 fn check_simple_expr_scoping(expr: &SimpleExpr, ctx: &Context) {
     match expr {
         SimpleExpr::Var(v) => {
-            assert!(ctx.defines(&v), "Variable defined but not used: {:?}", v)
+            assert!(ctx.defines(&v), "Variable used but not defined: {:?}", v)
         },
         SimpleExpr::Constant(_) => {},
         SimpleExpr::ConstMallocAccess { .. } => {},
@@ -636,8 +636,6 @@ fn simplify_lines(
                     counter: const_malloc.counter,
                     ..ConstMalloc::default()
                 };
-                // TODO: what is array manager, and does it need to be updated
-                // to make block-level scoping work?
                 let valid_aux_vars_in_array_manager_before = array_manager.valid.clone();
                 array_manager.valid.clear();
                 let simplified_body = simplify_lines(
@@ -1597,6 +1595,10 @@ fn handle_inlined_functions_helper(
                 if let Some(func) = inlined_functions.get(&*function_name) {
                     let mut inlined_lines = vec![];
 
+                    for var in return_data.iter() {
+                        inlined_lines.push(Line::ForwardDeclaration { var : var.clone() });
+                    }
+
                     let mut simplified_args = vec![];
                     for arg in args {
                         if let Expression::Value(simple_expr) = arg {

crates/lean_compiler/src/b_compile_intermediate.rs

@@ -147,13 +147,11 @@ fn compile_function(
     compiler.stack_size = stack_pos;
     compiler.args_count = function.arguments.len();
 
-    let mut declared_vars: BTreeSet<Var> = function.arguments.iter().cloned().collect();
     compile_lines(
         &Label::function(function.name.clone()),
         &function.instructions,
         compiler,
         None,
-        &mut declared_vars,
     )
 }
 
@@ -162,14 +160,13 @@ fn compile_lines(
     lines: &[SimpleLine],
     compiler: &mut Compiler,
     final_jump: Option<Label>,
-    declared_vars: &mut BTreeSet<Var>,
 ) -> Result<Vec<IntermediateInstruction>, String> {
     let mut instructions = Vec::new();
 
     for (i, line) in lines.iter().enumerate() {
         match line {
             SimpleLine::ForwardDeclaration { var } => {
-                let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
                 current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
                 compiler.stack_pos += 1;
             }
@@ -183,9 +180,8 @@ fn compile_lines(
                 let arg0 = IntermediateValue::from_simple_expr(arg0, compiler);
                 let arg1 = IntermediateValue::from_simple_expr(arg1, compiler);
 
-                if let VarOrConstMallocAccess::Var(var) = var {
-                    declared_vars.insert(var.clone());
-                    let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                if let VarOrConstMallocAccess::Var(var) = var && !compiler.is_in_scope(var) {
+                    let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
                     current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
                     compiler.stack_pos += 1;
                 }
@@ -219,21 +215,14 @@ fn compile_lines(
                 let saved_stack_pos = compiler.stack_pos;
                 let mut new_stack_pos = saved_stack_pos;
                 for (i, arm) in arms.iter().enumerate() {
-                    let mut arm_declared_vars = declared_vars.clone();
                     compiler.stack_pos = saved_stack_pos;
                     let arm_instructions = compile_lines(
                         function_name,
                         arm,
                         compiler,
                         Some(end_label.clone()),
-                        &mut arm_declared_vars,
                     )?;
                     compiled_arms.push(arm_instructions);
-                    *declared_vars = if i == 0 {
-                        arm_declared_vars
-                    } else {
-                        declared_vars.intersection(&arm_declared_vars).cloned().collect()
-                    };
                     new_stack_pos = new_stack_pos.max(compiler.stack_pos);
                 }
                 compiler.stack_pos = new_stack_pos;
@@ -268,7 +257,7 @@ fn compile_lines(
                     updated_fp: None,
                 });
 
-                let remaining = compile_lines(function_name, &lines[i + 1..], compiler, final_jump, declared_vars)?;
+                let remaining = compile_lines(function_name, &lines[i + 1..], compiler, final_jump)?;
                 compiler.bytecode.insert(end_label, remaining);
 
                 compiler.stack_frame_layout.scopes.pop();
@@ -287,8 +276,6 @@ fn compile_lines(
             } => {
                 compiler.stack_frame_layout.scopes.push(ScopeLayout::default());
 
-                validate_vars_declared(&[condition], declared_vars)?;
-
                 let if_id = compiler.if_counter;
                 compiler.if_counter += 1;
 
@@ -363,24 +350,20 @@ fn compile_lines(
 
                 let saved_stack_pos = compiler.stack_pos;
 
-                let mut then_declared_vars = declared_vars.clone();
                 let then_instructions = compile_lines(
                     function_name,
                     then_branch,
                     compiler,
                     Some(end_label.clone()),
-                    &mut then_declared_vars,
                 )?;
 
                 let then_stack_pos = compiler.stack_pos;
                 compiler.stack_pos = saved_stack_pos;
-                let mut else_declared_vars = declared_vars.clone();
                 let else_instructions = compile_lines(
                     function_name,
                     else_branch,
                     compiler,
                     Some(end_label.clone()),
-                    &mut else_declared_vars,
                 )?;
 
                 compiler.bytecode.insert(if_label, then_instructions);
@@ -389,7 +372,7 @@ fn compile_lines(
                 compiler.stack_frame_layout.scopes.pop();
                 compiler.stack_pos = compiler.stack_pos.max(then_stack_pos);
 
-                let remaining = compile_lines(function_name, &lines[i + 1..], compiler, final_jump, declared_vars)?;
+                let remaining = compile_lines(function_name, &lines[i + 1..], compiler, final_jump)?;
                 compiler.bytecode.insert(end_label, remaining);
                 // It is not necessary to update compiler.stack_size here because the preceding call to
                 // compile_lines should have done so.
@@ -398,11 +381,8 @@ fn compile_lines(
             }
 
             SimpleLine::RawAccess { res, index, shift } => {
-                // TODO: why is validate_vars_declared here?
-                validate_vars_declared(&[index], declared_vars)?;
                 if let SimpleExpr::Var(var) = res && !compiler.is_in_scope(var) {
-                    declared_vars.insert(var.clone());
-                    let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                    let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
                     current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
                     compiler.stack_pos += 1;
                 }
@@ -438,13 +418,12 @@ fn compile_lines(
                     compiler,
                 )?);
 
-                // TODO: why is validate_vars_declared here?
-                validate_vars_declared(args, declared_vars)?;
-                declared_vars.extend(return_data.iter().cloned());
                 for var in return_data.iter() {
-                    let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
-                    current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
-                    compiler.stack_pos += 1;
+                    if !compiler.is_in_scope(var) {
+                        let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                        current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
+                        compiler.stack_pos += 1;
+                    }
                 }
 
                 let after_call = {
@@ -466,7 +445,6 @@ fn compile_lines(
                         &lines[i + 1..],
                         compiler,
                         final_jump,
-                        declared_vars,
                     )?);
 
                     instructions
@@ -522,10 +500,11 @@ fn compile_lines(
                 vectorized,
                 vectorized_len,
             } => {
-                let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
-                current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
-                compiler.stack_pos += 1;
-                declared_vars.insert(var.clone());
+                if !compiler.is_in_scope(var) {
+                    let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                    current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
+                    compiler.stack_pos += 1;
+                }
                 instructions.push(IntermediateInstruction::RequestMemory {
                     offset: compiler.get_offset(&var.clone().into()),
                     size: IntermediateValue::from_simple_expr(size, compiler),
@@ -535,23 +514,23 @@ fn compile_lines(
             }
             SimpleLine::ConstMalloc { var, size, label } => {
                 let size = size.naive_eval().unwrap().to_usize(); // TODO not very good;
-                declared_vars.insert(var.clone());
-                let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
-                current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
-                compiler.stack_pos += 1;
-                current_scope_layout.const_mallocs.insert(*label, compiler.stack_pos);
-                handle_const_malloc(declared_vars, &mut instructions, compiler, var, size, label);
-                compiler.stack_pos += size;
+                if !compiler.is_in_scope(var) {
+                    let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                    current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
+                    compiler.stack_pos += 1;
+                }
+                handle_const_malloc(&mut instructions, compiler, var, size, label);
             }
             SimpleLine::DecomposeBits {
                 var,
                 to_decompose,
                 label,
             } => {
-                declared_vars.insert(var.clone());
-                let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
-                current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
-                compiler.stack_pos += 1;
+                if !compiler.is_in_scope(var) {
+                    let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                    current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
+                    compiler.stack_pos += 1;
+                }
 
                 instructions.push(IntermediateInstruction::DecomposeBits {
                     res_offset: compiler.stack_pos,
@@ -562,24 +541,23 @@ fn compile_lines(
                 });
 
                 handle_const_malloc(
-                    declared_vars,
                     &mut instructions,
                     compiler,
                     var,
                     F::bits() * to_decompose.len(),
                     label,
                 );
-                compiler.stack_pos += F::bits() * to_decompose.len();
             }
             SimpleLine::DecomposeCustom {
                 var,
                 to_decompose,
                 label,
             } => {
-                declared_vars.insert(var.clone());
-                let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
-                current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
-                compiler.stack_pos += 1;
+                if !compiler.is_in_scope(var) {
+                    let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                    current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
+                    compiler.stack_pos += 1;
+                }
 
                 instructions.push(IntermediateInstruction::DecomposeCustom {
                     res_offset: compiler.stack_pos,
@@ -590,20 +568,19 @@ fn compile_lines(
                 });
 
                 handle_const_malloc(
-                    declared_vars,
                     &mut instructions,
                     compiler,
                     var,
                     F::bits() * to_decompose.len(),
                     label,
                 );
-                compiler.stack_pos += F::bits() * to_decompose.len();
             }
             SimpleLine::CounterHint { var } => {
-                let mut current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
-                current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
-                compiler.stack_pos += 1;
-                declared_vars.insert(var.clone());
+                if !compiler.is_in_scope(var) {
+                    let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+                    current_scope_layout.var_positions.insert(var.clone(), compiler.stack_pos);
+                    compiler.stack_pos += 1;
+                }
                 instructions.push(IntermediateInstruction::CounterHint {
                     res_offset: compiler
                         .get_offset(&var.clone().into())
@@ -640,13 +617,14 @@ fn compile_lines(
 }
 
 fn handle_const_malloc(
-    declared_vars: &mut BTreeSet<Var>,
     instructions: &mut Vec<IntermediateInstruction>,
     compiler: &mut Compiler,
     var: &Var,
     size: usize,
     label: &ConstMallocLabel,
 ) {
+    let current_scope_layout = compiler.stack_frame_layout.scopes.last_mut().unwrap();
+    current_scope_layout.const_mallocs.insert(*label, compiler.stack_pos);
     instructions.push(IntermediateInstruction::Computation {
         operation: Operation::Add,
         arg_a: IntermediateValue::Constant(compiler.stack_pos.into()),
@@ -655,18 +633,7 @@ fn handle_const_malloc(
             offset: compiler.get_offset(&var.clone().into()),
         },
     });
-}
-
-// Helper functions
-fn validate_vars_declared<VoC: Borrow<SimpleExpr>>(vocs: &[VoC], declared: &BTreeSet<Var>) -> Result<(), String> {
-    for voc in vocs {
-        if let SimpleExpr::Var(v) = voc.borrow()
-            && !declared.contains(v)
-        {
-            return Err(format!("Variable {v} not declared"));
-        }
-    }
-    Ok(())
+    compiler.stack_pos += size;
 }
 
 fn setup_function_call(

crates/lean_compiler/src/parser/parsers/statement.rs

@@ -40,7 +40,7 @@ impl Parse<Line> for StatementParser {
 pub struct ForwardDeclarationParser;
 
 impl Parse<Line> for ForwardDeclarationParser {
-    fn parse(pair: ParsePair<'_>, ctx: &mut ParseContext) -> ParseResult<Line> {
+    fn parse(pair: ParsePair<'_>, _ctx: &mut ParseContext) -> ParseResult<Line> {
         let mut inner = pair.into_inner();
         let var = next_inner_pair(&mut inner, "variable name")?.as_str().to_string();
         Ok(Line::ForwardDeclaration { var })

crates/lean_compiler/tests/test_compiler.rs

@@ -381,6 +381,27 @@ fn test_inlined() {
     compile_and_run(program.to_string(), (&[], &[]), DEFAULT_NO_VEC_RUNTIME_MEMORY, false);
 }
 
+#[test]
+fn test_inlined_2() {
+    let program = r#"
+    fn main() {
+        b = is_one();
+        c = b;
+        return;
+    }
+
+    fn is_one() inline -> 1 {
+        if 1 {
+            return 1;
+        } else {
+            return 0;
+        }
+    }
+   "#;
+    compile_and_run(program.to_string(), (&[], &[]), DEFAULT_NO_VEC_RUNTIME_MEMORY, false);
+
+}
+
 #[test]
 fn test_match() {
     let program = r#"

crates/lean_vm/src/execution/tests.rs

@@ -13,7 +13,7 @@ fn test_basic_memory_operations() {
     assert_eq!(memory.get(5).unwrap(), F::from_usize(42));
 
     // Test undefined memory access
-    assert!(matches!(memory.get(1), Err(RunnerError::UndefinedMemory)));
+    assert!(matches!(memory.get(1), Err(RunnerError::UndefinedMemory(1))));
 }
 
 #[test]

crates/rec_aggregation/recursion_program.lean_lang

@@ -334,6 +334,8 @@ fn sample_stir_indexes_and_fold(fs_state, num_queries, merkle_leaves_in_basefiel
         states = malloc(1 + folded_domain_size);
         states[0] = leaf_hashes[i];
         for j in 0..folded_domain_size {
+            var left;
+            var right;
             if stir_index_bits[j] == 1 {
                 left = merkle_path + j;
                 right = states[j];