Add translator support for local word memory ops, locaddr, and u32div

Unblocks translation of sha256.masm (and other files using local word
memory). Adds LocLoadWBe, LocLoadWLe, LocStoreWBe, LocStoreWLe,
Locaddr, U32Div, and U32DivImm to the instruction translator, stack
effect metadata, and multi-instruction count list. Includes 17 new
tests (positive translations, negative constant errors, stack effects,
and instruction count verification).

Note: The Lean model (Instruction.lean, Semantics.lean) needs matching
constructors and handlers added separately for the generated Lean to
compile.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: MarcIlunga

masm-to-lean/src/instruction.rs

@@ -311,6 +311,11 @@ pub fn translate_instruction(inst: &Instruction) -> Result<String> {
         U32WideningMadd => ".u32WidenMadd".into(),
         U32WrappingMadd => ".u32WrappingMadd".into(),
 
+        U32Div => ".u32Div".into(),
+        U32DivImm(imm) => {
+            let v = u32_imm(imm)?;
+            return Ok(format!(".inst (.push {v}), .inst .u32Div"));
+        }
         U32DivMod => ".u32DivMod".into(),
         U32DivModImm(imm) => {
             let v = u32_imm(imm)?;
@@ -366,6 +371,11 @@ pub fn translate_instruction(inst: &Instruction) -> Result<String> {
         // Procedure locals
         LocLoad(idx) => format!(".locLoad {}", u16_imm(idx)?),
         LocStore(idx) => format!(".locStore {}", u16_imm(idx)?),
+        LocLoadWBe(idx) => format!(".locLoadwBe {}", u16_imm(idx)?),
+        LocLoadWLe(idx) => format!(".locLoadwLe {}", u16_imm(idx)?),
+        LocStoreWBe(idx) => format!(".locStorewBe {}", u16_imm(idx)?),
+        LocStoreWLe(idx) => format!(".locStorewLe {}", u16_imm(idx)?),
+        Locaddr(idx) => format!(".locaddr {}", u16_imm(idx)?),
 
         // Advice stack
         AdvPush(imm) => match imm {
@@ -400,11 +410,102 @@ pub fn translate_instruction(inst: &Instruction) -> Result<String> {
 #[cfg(test)]
 mod tests {
     use super::translate_instruction;
-    use miden_assembly_syntax::ast::Instruction;
+    use miden_assembly_syntax::ast::{ImmU16, ImmU32, Instruction};
+    use miden_assembly_syntax::debuginfo::Span;
 
     #[test]
     fn translates_u32_wrapping_madd() {
         let lean = translate_instruction(&Instruction::U32WrappingMadd).unwrap();
         assert_eq!(lean, ".u32WrappingMadd");
     }
+
+    // --- Local word memory instructions ---
+
+    #[test]
+    fn translates_loc_loadw_be() {
+        let imm = ImmU16::Value(Span::unknown(4u16));
+        let lean = translate_instruction(&Instruction::LocLoadWBe(imm)).unwrap();
+        assert_eq!(lean, ".locLoadwBe 4");
+    }
+
+    #[test]
+    fn translates_loc_loadw_le() {
+        let imm = ImmU16::Value(Span::unknown(8u16));
+        let lean = translate_instruction(&Instruction::LocLoadWLe(imm)).unwrap();
+        assert_eq!(lean, ".locLoadwLe 8");
+    }
+
+    #[test]
+    fn translates_loc_storew_be() {
+        let imm = ImmU16::Value(Span::unknown(0u16));
+        let lean = translate_instruction(&Instruction::LocStoreWBe(imm)).unwrap();
+        assert_eq!(lean, ".locStorewBe 0");
+    }
+
+    #[test]
+    fn translates_loc_storew_le() {
+        let imm = ImmU16::Value(Span::unknown(12u16));
+        let lean = translate_instruction(&Instruction::LocStoreWLe(imm)).unwrap();
+        assert_eq!(lean, ".locStorewLe 12");
+    }
+
+    #[test]
+    fn translates_locaddr() {
+        let imm = ImmU16::Value(Span::unknown(32u16));
+        let lean = translate_instruction(&Instruction::Locaddr(imm)).unwrap();
+        assert_eq!(lean, ".locaddr 32");
+    }
+
+    #[test]
+    fn translates_loc_loadw_be_zero_index() {
+        let imm = ImmU16::Value(Span::unknown(0u16));
+        let lean = translate_instruction(&Instruction::LocLoadWBe(imm)).unwrap();
+        assert_eq!(lean, ".locLoadwBe 0");
+    }
+
+    // --- U32Div instructions ---
+
+    #[test]
+    fn translates_u32_div() {
+        let lean = translate_instruction(&Instruction::U32Div).unwrap();
+        assert_eq!(lean, ".u32Div");
+    }
+
+    #[test]
+    fn translates_u32_div_imm() {
+        let imm = ImmU32::Value(Span::unknown(4u32));
+        let lean = translate_instruction(&Instruction::U32DivImm(imm)).unwrap();
+        // Should expand to push + op (multi-instruction)
+        assert_eq!(lean, ".inst (.push 4), .inst .u32Div");
+    }
+
+    // --- Negative: constant immediates should error ---
+
+    #[test]
+    fn loc_loadw_be_constant_errors() {
+        let imm = ImmU16::Constant(
+            miden_assembly_syntax::ast::Ident::new("SOME_CONST").unwrap(),
+        );
+        let result = translate_instruction(&Instruction::LocLoadWBe(imm));
+        assert!(result.is_err());
+        assert!(result.unwrap_err().to_string().contains("unresolved constant"));
+    }
+
+    #[test]
+    fn locaddr_constant_errors() {
+        let imm = ImmU16::Constant(
+            miden_assembly_syntax::ast::Ident::new("OFFSET").unwrap(),
+        );
+        let result = translate_instruction(&Instruction::Locaddr(imm));
+        assert!(result.is_err());
+    }
+
+    #[test]
+    fn u32_div_imm_constant_errors() {
+        let imm = ImmU32::Constant(
+            miden_assembly_syntax::ast::Ident::new("DIVISOR").unwrap(),
+        );
+        let result = translate_instruction(&Instruction::U32DivImm(imm));
+        assert!(result.is_err());
+    }
 }

masm-to-lean/src/instruction_info.rs

@@ -990,6 +990,11 @@ pub fn instruction_info(inst: &Instruction) -> InstructionInfo {
             info.comment_name = "u32Div".into();
             info.is_known = true;
         }
+        U32DivImm(_) => {
+            info.stack_effect = Some(StackEffect::new(1, 1));
+            info.comment_name = "u32Div (imm)".into();
+            info.is_known = true;
+        }
         U32Mod => {
             info.stack_effect = Some(StackEffect::new(2, 1));
             info.comment_name = "u32Mod".into();
@@ -1199,6 +1204,31 @@ pub fn instruction_info(inst: &Instruction) -> InstructionInfo {
             info.comment_name = "locStore".into();
             info.is_known = true;
         }
+        LocLoadWBe(_) | LocLoadWLe(_) => {
+            // Overwrites top 4 elements with word from local memory
+            info.stack_effect = Some(StackEffect::with_depth(4, 4, 4));
+            info.comment_name = if matches!(inst, LocLoadWBe(_)) {
+                "locLoadwBe".into()
+            } else {
+                "locLoadwLe".into()
+            };
+            info.is_known = true;
+        }
+        LocStoreWBe(_) | LocStoreWLe(_) => {
+            // Stores top 4 elements to local memory (keeps them on stack)
+            info.stack_effect = Some(StackEffect::with_depth(0, 0, 4));
+            info.comment_name = if matches!(inst, LocStoreWBe(_)) {
+                "locStorewBe".into()
+            } else {
+                "locStorewLe".into()
+            };
+            info.is_known = true;
+        }
+        Locaddr(_) => {
+            info.stack_effect = Some(StackEffect::new(0, 1));
+            info.comment_name = "locaddr".into();
+            info.is_known = true;
+        }
 
         // === Advice stack ===
         AdvPush(imm) => {

masm-to-lean/src/stack_effect.rs

@@ -191,6 +191,7 @@ impl<'a> StackSimulator<'a> {
                         | Instruction::U32WrappingSubImm(_)
                         | Instruction::U32WideningMulImm(_)
                         | Instruction::U32WrappingMulImm(_)
+                        | Instruction::U32DivImm(_)
                         | Instruction::U32DivModImm(_)
                         | Instruction::U32ModImm(_)
                 ) {
@@ -466,6 +467,65 @@ mod tests {
         assert_eq!(effect.net_effect, -1);
     }
 
+    #[test]
+    fn test_instruction_effect_loc_loadw_be() {
+        use miden_assembly_syntax::ast::ImmU16;
+        let imm = ImmU16::Value(Span::unknown(4u16));
+        let effect = instruction_effect(&Instruction::LocLoadWBe(imm)).unwrap();
+        // Overwrites top 4 elements with word from local memory
+        assert_eq!(effect.pops, 4);
+        assert_eq!(effect.pushes, 4);
+        assert_eq!(effect.required_depth, 4);
+    }
+
+    #[test]
+    fn test_instruction_effect_loc_storew_be() {
+        use miden_assembly_syntax::ast::ImmU16;
+        let imm = ImmU16::Value(Span::unknown(0u16));
+        let effect = instruction_effect(&Instruction::LocStoreWBe(imm)).unwrap();
+        // Stores top 4 elements, keeps them on stack
+        assert_eq!(effect.pops, 0);
+        assert_eq!(effect.pushes, 0);
+        assert_eq!(effect.required_depth, 4);
+    }
+
+    #[test]
+    fn test_instruction_effect_locaddr() {
+        use miden_assembly_syntax::ast::ImmU16;
+        let imm = ImmU16::Value(Span::unknown(32u16));
+        let effect = instruction_effect(&Instruction::Locaddr(imm)).unwrap();
+        // Pushes one address onto the stack
+        assert_eq!(effect.pops, 0);
+        assert_eq!(effect.pushes, 1);
+    }
+
+    #[test]
+    fn test_instruction_effect_u32_div() {
+        let effect = instruction_effect(&Instruction::U32Div).unwrap();
+        assert_eq!(effect.pops, 2);
+        assert_eq!(effect.pushes, 1);
+    }
+
+    #[test]
+    fn test_instruction_effect_u32_div_imm() {
+        use miden_assembly_syntax::ast::ImmU32;
+        let imm = ImmU32::Value(Span::unknown(4u32));
+        let effect = instruction_effect(&Instruction::U32DivImm(imm)).unwrap();
+        // Imm variant: consumes 1 (the dividend), produces 1 (quotient)
+        assert_eq!(effect.pops, 1);
+        assert_eq!(effect.pushes, 1);
+    }
+
+    #[test]
+    fn test_u32_div_imm_counts_as_two_instructions() {
+        use miden_assembly_syntax::ast::ImmU32;
+        let imm = ImmU32::Value(Span::unknown(4u32));
+        let block = make_block(vec![Instruction::U32DivImm(imm)]);
+        let effect = analyze_block(&block);
+        // U32DivImm expands to push + u32Div = 2 instructions
+        assert_eq!(effect.instruction_count, 2);
+    }
+
     #[test]
     fn test_analyze_block_with_callees() {
         // Block with exec that calls a known procedure