From 22f4247e690d35959b52418a0c9fa3af4223a614 Mon Sep 17 00:00:00 2001
From: Andrei Kashin <kashin.andrej@gmail.com>
Date: Tue, 30 Jan 2024 14:32:37 +0000
Subject: [PATCH 1/5] Implement full memory load and stores

This PR adds the remaining features necessary to run SHA256 benchmark:

    Misaligned loads and stores
    Loads and stores of size < 64 bit

There instructions are generated by rustc compiler for wasm32 target and are quite common.

The current implementation is not verifiable as it uses external (free) inputs. It turned out to be quite challenging to implement them in a verifiable fashion because they involve many bitwise operations which are quite expensive.

For now, there is value in having a non-verifiable implementation that makes sure we can run tests and benchmarks related to memory. I've linked a few TODOs to do a verifiable implementation, but first, we would need a proper design for that part. Most likely, we will need to modify the zkAsm processor to support these operations efficiently.

Implementation-wise, there are three steps:

    Conversion from address + offset to slot + offset
    Read/write the value at the correct offset
    Narrowing down the value to the desired type width
---
 cranelift/codegen/src/isa/zkasm/inst/args.rs  |  23 ++
 cranelift/codegen/src/isa/zkasm/inst/emit.rs  | 129 ++++++++-
 cranelift/codegen/src/isa/zkasm/inst/mod.rs   |   8 +-
 cranelift/filetests/src/test_zkasm.rs         |   2 +-
 .../sha256/generated/from_rust.zkasm          | 248 +++++++++++++-----
 .../zkasm_data/benchmarks/sha256/state.csv    |   2 +-
 cranelift/zkasm_data/generated/global.zkasm   |  14 +-
 cranelift/zkasm_data/generated/memory.zkasm   |  18 +-
 .../zkasm_data/generated/memory_i32.zkasm     | 109 ++++++--
 cranelift/zkasm_data/state.csv                |   6 +-
 docs/zkasm/test_summary.csv                   |   4 +-
 11 files changed, 462 insertions(+), 101 deletions(-)

diff --git a/cranelift/codegen/src/isa/zkasm/inst/args.rs b/cranelift/codegen/src/isa/zkasm/inst/args.rs
index 75a2e84ae682..6083bad3546c 100644
--- a/cranelift/codegen/src/isa/zkasm/inst/args.rs
+++ b/cranelift/codegen/src/isa/zkasm/inst/args.rs
@@ -802,6 +802,19 @@ impl LoadOP {
             Self::Fld => 0b011,
         }
     }
+    pub(crate) fn width(self) -> u32 {
+        match self {
+            Self::I8 => 1,
+            Self::I16 => 2,
+            Self::I32 => 4,
+            Self::U32 => 4,
+            Self::U8 => 1,
+            Self::U16 => 2,
+            Self::U64 => 8,
+            Self::Flw => unimplemented!(),
+            Self::Fld => unimplemented!(),
+        }
+    }
 }
 
 impl StoreOP {
@@ -843,6 +856,16 @@ impl StoreOP {
             Self::Fsd => 0b011,
         }
     }
+    pub(crate) fn width(self) -> u32 {
+        match self {
+            Self::I8 => 1,
+            Self::I16 => 2,
+            Self::I32 => 4,
+            Self::I64 => 8,
+            Self::Fsw => unimplemented!(),
+            Self::Fsd => unimplemented!(),
+        }
+    }
 }
 
 impl IntSelectOP {
diff --git a/cranelift/codegen/src/isa/zkasm/inst/emit.rs b/cranelift/codegen/src/isa/zkasm/inst/emit.rs
index ceae858d5a8a..80c2582dcce1 100644
--- a/cranelift/codegen/src/isa/zkasm/inst/emit.rs
+++ b/cranelift/codegen/src/isa/zkasm/inst/emit.rs
@@ -591,14 +591,74 @@ impl MachInstEmit for Inst {
                 match from {
                     AMode::RegOffset(r, ..) => {
                         debug_assert_eq!(r, e0());
+                        // TODO(#43): Implement the conversion using verifiable computations.
+                        put_string(
+                            &format!(
+                                "${{ ({}) / 8 }} => {}\n",
+                                access_reg_with_offset(r, offset),
+                                reg_name(r)
+                            ),
+                            sink,
+                        );
+                        let rem = offset % 8;
+                        let width = op.width() as i64;
+
                         put_string(
                             &format!(
                                 "$ => {} :MLOAD(MEM:{})\n",
                                 reg_name(rd.to_reg()),
-                                access_reg_with_offset(r, offset)
+                                reg_name(r)
                             ),
                             sink,
                         );
+                        // TODO(#34): Implement unaligned and narrow reads using verifiable
+                        // computations.
+                        if rem > 0 {
+                            put_string(
+                                &format!(
+                                    "${{ {} >> {} }} => {}\n",
+                                    reg_name(rd.to_reg()),
+                                    8 * rem,
+                                    reg_name(rd.to_reg())
+                                ),
+                                sink,
+                            );
+                        }
+
+                        // Handle the case when read spans two slots.
+                        if rem + width > 8 {
+                            let rem = rem + width - 8;
+                            put_string(
+                                &format!(
+                                    "$ => {} :MLOAD(MEM:{})\n",
+                                    reg_name(d0()),
+                                    access_reg_with_offset(r, 1)
+                                ),
+                                sink,
+                            );
+                            put_string(
+                                &format!(
+                                    "${{ (D << {}) | {} }} => {}\n",
+                                    64 - 8 * rem,
+                                    reg_name(rd.to_reg()),
+                                    reg_name(rd.to_reg()),
+                                ),
+                                sink,
+                            );
+                        }
+
+                        // Mask the value to the width of the resulting type.
+                        if width < 8 {
+                            put_string(
+                                &format!(
+                                    "${{ {} & ((1 << {}) - 1) }} => {}\n",
+                                    reg_name(rd.to_reg()),
+                                    8 * width,
+                                    reg_name(rd.to_reg()),
+                                ),
+                                sink,
+                            );
+                        }
                     }
                     AMode::SPOffset(..) | AMode::NominalSPOffset(..) | AMode::FPOffset(..) => {
                         assert_eq!(offset % 8, 0);
@@ -629,14 +689,77 @@ impl MachInstEmit for Inst {
                 match to {
                     AMode::RegOffset(r, ..) => {
                         debug_assert_eq!(r, e0());
+                        // TODO(#43): Implement the conversion using verifiable computations.
+                        put_string(
+                            &format!(
+                                "${{ ({}) / 8 }} => {}\n",
+                                access_reg_with_offset(r, offset),
+                                reg_name(r)
+                            ),
+                            sink,
+                        );
+                        let rem = offset % 8;
+                        let width = op.width() as i64;
+
+                        if op == StoreOP::I64 && rem == 0 {
+                            put_string(
+                                &format!("{} :MSTORE(MEM:{})\n", reg_name(src), reg_name(r)),
+                                sink,
+                            );
+                            return;
+                        }
+
+                        // TODO(#34): Implement unaligned and narrow writes using verifiable
+                        // computations.
+                        if width < 8 {
+                            put_string(
+                                &format!(
+                                    "${{ {} & ((1 << {}) - 1) }} => {}\n",
+                                    reg_name(src),
+                                    8 * width,
+                                    reg_name(src),
+                                ),
+                                sink,
+                            );
+                        }
+                        put_string(
+                            &format!("$ => {} :MLOAD(MEM:{})\n", reg_name(d0()), reg_name(r)),
+                            sink,
+                        );
                         put_string(
                             &format!(
-                                "{} :MSTORE(MEM:{})\n",
+                                "${{ (D & ~(((1 << {}) - 1) << {})) | ({} << {}) }} :MSTORE(MEM:{})\n",
+                                8 * width,
+                                8 * rem,
                                 reg_name(src),
-                                access_reg_with_offset(r, offset)
+                                8 * rem,
+                                reg_name(r),
                             ),
                             sink,
                         );
+
+                        // Handle the case when write spans two slots.
+                        if rem + width > 8 {
+                            let rem = rem + width - 8;
+                            put_string(
+                                &format!(
+                                    "$ => {} :MLOAD(MEM:{})\n",
+                                    reg_name(d0()),
+                                    access_reg_with_offset(r, 1)
+                                ),
+                                sink,
+                            );
+                            put_string(
+                                &format!(
+                                    "${{ (D & ~((1 << {}) - 1)) | ({} & ((1 << {}) - 1)) }} :MSTORE(MEM:{})\n",
+                                    8 * rem,
+                                    reg_name(src),
+                                    8 * rem,
+                                    access_reg_with_offset(r, 1),
+                                ),
+                                sink,
+                            );
+                        }
                     }
                     AMode::SPOffset(..) | AMode::NominalSPOffset(..) | AMode::FPOffset(..) => {
                         assert_eq!(offset % 8, 0);
diff --git a/cranelift/codegen/src/isa/zkasm/inst/mod.rs b/cranelift/codegen/src/isa/zkasm/inst/mod.rs
index 9eee21590569..fe0fc66f1551 100644
--- a/cranelift/codegen/src/isa/zkasm/inst/mod.rs
+++ b/cranelift/codegen/src/isa/zkasm/inst/mod.rs
@@ -336,13 +336,19 @@ fn zkasm_get_operands<F: Fn(VReg) -> VReg>(inst: &Inst, collector: &mut OperandC
             if let Some(r) = from.get_allocatable_register() {
                 collector.reg_fixed_use(r, e0());
             }
+            let mut clobbered = PRegSet::empty();
+            clobbered.add(d0().to_real_reg().unwrap().into());
+            collector.reg_clobbers(clobbered);
             collector.reg_def(rd);
         }
         &Inst::Store { to, src, .. } => {
             if let Some(r) = to.get_allocatable_register() {
                 collector.reg_fixed_use(r, e0());
             }
-            collector.reg_use(src);
+            let mut clobbered = PRegSet::empty();
+            clobbered.add(d0().to_real_reg().unwrap().into());
+            collector.reg_clobbers(clobbered);
+            collector.reg_late_use(src);
         }
         &Inst::Args { ref args } => {
             for arg in args {
diff --git a/cranelift/filetests/src/test_zkasm.rs b/cranelift/filetests/src/test_zkasm.rs
index 9294d956d94f..0029b28a52e6 100644
--- a/cranelift/filetests/src/test_zkasm.rs
+++ b/cranelift/filetests/src/test_zkasm.rs
@@ -60,7 +60,7 @@ mod tests {
 
         // Generate const data segments definitions.
         for (offset, data) in data_segments {
-            program.push(format!("  {offset} => E"));
+            program.push(format!("  {} => E", offset / 8));
             // Each slot stores 8 consecutive u8 numbers, with earlier addresses stored in lower
             // bits.
             for (i, chunk) in data.chunks(8).enumerate() {
diff --git a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
index 172db25a8d41..553a5ef3bb2c 100644
--- a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
+++ b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
@@ -5,7 +5,7 @@ start:
   2048 :MSTORE(global_0)  ;; Global32(2048)
   2080 :MSTORE(global_1)  ;; Global32(2080)
   2080 :MSTORE(global_2)  ;; Global32(2080)
-  2048 => E
+  256 => E
   13503953895726638695n :MSTORE(MEM:E + 0)
   11912009169889063794n :MSTORE(MEM:E + 1)
   11170449402626986623n :MSTORE(MEM:E + 2)
@@ -38,10 +38,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => C :MLOAD(MEM:E + 2072)
+  ${ (E + 2072) / 8 } => E
+  $ => C :MLOAD(MEM:E)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 2)
   $ => E :ADD
+  ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   16n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
@@ -53,10 +55,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => C :MLOAD(MEM:E + 2064)
+  ${ (E + 2064) / 8 } => E
+  $ => C :MLOAD(MEM:E)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 1)
   $ => E :ADD
+  ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   8n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
@@ -68,10 +72,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => C :MLOAD(MEM:E + 2056)
+  ${ (E + 2056) / 8 } => E
+  $ => C :MLOAD(MEM:E)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
+  ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   50n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
@@ -79,10 +85,11 @@ function_1:
   B => A
   4294967295n => B  ;; LoadConst64
   $ => B :AND
-  0n => D  ;; LoadConst64
+  0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  D :MSTORE(MEM:E)
+  ${ (E) / 8 } => E
+  C :MSTORE(MEM:E)
   58n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => C :ADD
@@ -92,6 +99,7 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   66n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
@@ -102,6 +110,7 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   74n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
@@ -112,6 +121,7 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   82n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
@@ -122,6 +132,7 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   88n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
@@ -129,35 +140,49 @@ function_1:
   B => A
   4294967295n => B  ;; LoadConst64
   $ => B :AND
-  0n => D  ;; LoadConst64
+  0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  D :MSTORE(MEM:E)
+  ${ (E) / 8 } => E
+  C :MSTORE(MEM:E)
   1n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  C :MSTORE(MEM:E + 104)
+  ${ (E + 104) / 8 } => E
+  ${ C & ((1 << 8) - 1) } => C
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 8) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  C :MSTORE(MEM:E + 32)
+  ${ (E + 32) / 8 } => E
+  C :MSTORE(MEM:E)
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  C :MSTORE(MEM:E + 42)
+  ${ (E + 42) / 8 } => E
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << 16)) | (C << 16) } :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << 16) - 1)) | (C & ((1 << 16) - 1)) } :MSTORE(MEM:E + 1)
   32856n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  C :MSTORE(MEM:E + 40)
+  ${ (E + 40) / 8 } => E
+  ${ C & ((1 << 16) - 1) } => C
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 16) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => D :MLOAD(MEM:E + 2048)
+  ${ (E + 2048) / 8 } => E
+  $ => C :MLOAD(MEM:E)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  D :MSTORE(MEM:E)
+  ${ (E) / 8 } => E
+  C :MSTORE(MEM:E)
   96n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => C :ADD
@@ -167,6 +192,7 @@ function_1:
   576460752303423488n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   40n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
@@ -184,40 +210,60 @@ function_1:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 2)
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 12)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 1)
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 11)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 10)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 28)
+  ${ (E + 28) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 9)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 20)
+  ${ (E + 20) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 8)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 12)
+  ${ (E + 12) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 7)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 4)
+  ${ (E + 4) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 6)
   75n => A  ;; LoadConst64
   A :MSTORE(SP + 4)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 5)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -1213,35 +1259,55 @@ function_2:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
-  $ => D :MLOAD(MEM:E + 28)
-  D :MSTORE(SP + 9)
+  ${ (E + 28) / 8 } => E
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 32 } => E
+  ${ E & ((1 << 32) - 1) } => E
+  E :MSTORE(SP + 9)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => C :MLOAD(MEM:E + 24)
+  ${ (E + 24) / 8 } => E
+  $ => C :MLOAD(MEM:E)
+  ${ C & ((1 << 32) - 1) } => C
   C :MSTORE(SP + 10)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => C :MLOAD(MEM:E + 20)
+  ${ (E + 20) / 8 } => E
+  $ => C :MLOAD(MEM:E)
+  ${ C >> 32 } => C
+  ${ C & ((1 << 32) - 1) } => C
   C :MSTORE(SP + 11)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 16)
+  ${ (E + 16) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 12)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => E :MLOAD(MEM:E + 12)
+  ${ (E + 12) / 8 } => E
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 32 } => E
+  ${ E & ((1 << 32) - 1) } => E
   E :MSTORE(SP + 13)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => D :MLOAD(MEM:E + 8)
-  D :MSTORE(SP + 14)
+  ${ (E + 8) / 8 } => E
+  $ => E :MLOAD(MEM:E)
+  ${ E & ((1 << 32) - 1) } => E
+  E :MSTORE(SP + 14)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => C :MLOAD(MEM:E + 4)
+  ${ (E + 4) / 8 } => E
+  $ => C :MLOAD(MEM:E)
+  ${ C >> 32 } => C
+  ${ C & ((1 << 32) - 1) } => C
   C :MSTORE(SP + 15)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 16)
   0n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 2)
@@ -1529,7 +1595,9 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1165)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -1738,7 +1806,10 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 4)
+  ${ (E + 4) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1155)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -2073,7 +2144,9 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 8)
+  ${ (E + 8) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1139)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -2408,7 +2481,10 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 12)
+  ${ (E + 12) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1123)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -2743,7 +2819,9 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 16)
+  ${ (E + 16) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1107)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -3077,7 +3155,10 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 20)
+  ${ (E + 20) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1091)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -3412,7 +3493,9 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 24)
+  ${ (E + 24) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1075)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -3747,7 +3830,10 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 28)
+  ${ (E + 28) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1059)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -4082,7 +4168,9 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 32)
+  ${ (E + 32) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1043)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -4417,7 +4505,10 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 36)
+  ${ (E + 36) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1027)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -4752,7 +4843,9 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 40)
+  ${ (E + 40) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 1011)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -5087,7 +5180,10 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 44)
+  ${ (E + 44) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 995)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -5422,7 +5518,9 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 48)
+  ${ (E + 48) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 979)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -5757,7 +5855,10 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 52)
+  ${ (E + 52) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 963)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -6092,7 +6193,9 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 56)
+  ${ (E + 56) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 947)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -6427,7 +6530,10 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 60)
+  ${ (E + 60) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 32 } => A
+  ${ A & ((1 << 32) - 1) } => A
   A :MSTORE(SP + 931)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
@@ -27566,12 +27672,12 @@ label_2_3:
   $ => B :AND
   $ => A :MLOAD(SP + 25)
   $ => A :ADD
-  B => E
+  B => D
   4294967295n => B  ;; LoadConst64
-  $ => C :AND
+  $ => E :AND
   $ => A :MLOAD(SP + 29)
   $ => B :MLOAD(SP + 1)
-  C :MSTORE(SP + 16)
+  E :MSTORE(SP + 16)
   $ => A :ADD
   4294967295n => B  ;; LoadConst64
   $ => C :AND
@@ -27581,7 +27687,7 @@ label_2_3:
   $ => A :ADD
   4294967295n => B  ;; LoadConst64
   $ => A :AND
-  E => B
+  D => B
   $ => A :ADD
   4294967295n => B  ;; LoadConst64
   $ => A :AND
@@ -27608,8 +27714,8 @@ label_2_3:
   $ => A :MLOAD(SP + 36)
   $ => A :ADD
   4294967295n => B  ;; LoadConst64
-  $ => B :AND
-  B :MSTORE(SP + 10)
+  $ => A :AND
+  A :MSTORE(SP + 10)
   $ => B :MLOAD(SP + 4)
   $ => A :MLOAD(SP + 54)
   $ => A :ADD
@@ -27653,35 +27759,59 @@ label_2_7:
   $ => B :MLOAD(SP)
   $ => E :ADD
   $ => A :MLOAD(SP + 9)
-  A :MSTORE(MEM:E + 28)
+  ${ (E + 28) / 8 } => E
+  ${ A & ((1 << 32) - 1) } => A
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 32)) | (A << 32) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => C :MLOAD(SP + 10)
-  C :MSTORE(MEM:E + 24)
+  $ => A :MLOAD(SP + 10)
+  ${ (E + 24) / 8 } => E
+  ${ A & ((1 << 32) - 1) } => A
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 0)) | (A << 0) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 11)
-  C :MSTORE(MEM:E + 20)
+  ${ (E + 20) / 8 } => E
+  ${ C & ((1 << 32) - 1) } => C
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => A :MLOAD(SP + 12)
-  A :MSTORE(MEM:E + 16)
+  ${ (E + 16) / 8 } => E
+  ${ A & ((1 << 32) - 1) } => A
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 0)) | (A << 0) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => D :MLOAD(SP + 13)
-  D :MSTORE(MEM:E + 12)
+  $ => C :MLOAD(SP + 13)
+  ${ (E + 12) / 8 } => E
+  ${ C & ((1 << 32) - 1) } => C
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => D :MLOAD(SP + 14)
-  D :MSTORE(MEM:E + 8)
+  $ => C :MLOAD(SP + 14)
+  ${ (E + 8) / 8 } => E
+  ${ C & ((1 << 32) - 1) } => C
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 15)
-  C :MSTORE(MEM:E + 4)
+  ${ (E + 4) / 8 } => E
+  ${ C & ((1 << 32) - 1) } => C
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => B :MLOAD(SP + 16)
-  B :MSTORE(MEM:E)
+  ${ (E) / 8 } => E
+  ${ B & ((1 << 32) - 1) } => B
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 0)) | (B << 0) } :MSTORE(MEM:E)
   SP + 1182 => SP
   $ => C :MLOAD(SP - 1)
   $ => D :MLOAD(SP - 2)
diff --git a/cranelift/zkasm_data/benchmarks/sha256/state.csv b/cranelift/zkasm_data/benchmarks/sha256/state.csv
index 1a67b026287f..d6983d88bcac 100644
--- a/cranelift/zkasm_data/benchmarks/sha256/state.csv
+++ b/cranelift/zkasm_data/benchmarks/sha256/state.csv
@@ -1,2 +1,2 @@
 Test,Status,Cycles
-from_rust,runtime error,
+from_rust,pass,27166
diff --git a/cranelift/zkasm_data/generated/global.zkasm b/cranelift/zkasm_data/generated/global.zkasm
index dcadef7cd266..8a9e92eeba98 100644
--- a/cranelift/zkasm_data/generated/global.zkasm
+++ b/cranelift/zkasm_data/generated/global.zkasm
@@ -11,10 +11,11 @@ function_1:
   SP - 1 => SP
   RR :MSTORE(SP)
   D :MSTORE(SP - 1)
-  B :MSTORE(SP - 2)
-  SP - 2 => SP
-  3n => D  ;; LoadConst32
-  D :MSTORE(global_1)
+  E :MSTORE(SP - 2)
+  B :MSTORE(SP - 3)
+  SP - 4 => SP
+  3n => E  ;; LoadConst32
+  E :MSTORE(global_1)
   $ => A :MLOAD(global_0)
   $ => B :MLOAD(global_1)
   $ => A :ADD
@@ -22,9 +23,10 @@ function_1:
   $ => A :AND
   1n => B  ;; LoadConst32
   B :ASSERT
-  SP + 2 => SP
+  SP + 4 => SP
   $ => D :MLOAD(SP - 1)
-  $ => B :MLOAD(SP - 2)
+  $ => E :MLOAD(SP - 2)
+  $ => B :MLOAD(SP - 3)
   $ => RR :MLOAD(SP)
   SP + 1 => SP
   :JMP(RR)
diff --git a/cranelift/zkasm_data/generated/memory.zkasm b/cranelift/zkasm_data/generated/memory.zkasm
index 64c76ec69288..c255b6877c56 100644
--- a/cranelift/zkasm_data/generated/memory.zkasm
+++ b/cranelift/zkasm_data/generated/memory.zkasm
@@ -15,22 +15,32 @@ function_1:
   2n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  C :MSTORE(MEM:E)
+  ${ (E) / 8 } => E
+  ${ C & ((1 << 32) - 1) } => C
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
   8n => B  ;; LoadConst32
   3n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  C :MSTORE(MEM:E)
+  ${ (E) / 8 } => E
+  ${ C & ((1 << 32) - 1) } => C
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
-  A => D
+  ${ A & ((1 << 32) - 1) } => A
+  A => C
   8n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => B :MLOAD(MEM:E)
-  D => A
+  ${ B & ((1 << 32) - 1) } => B
+  C => A
   $ => A :ADD
   4294967295n => B  ;; LoadConst64
   $ => A :AND
diff --git a/cranelift/zkasm_data/generated/memory_i32.zkasm b/cranelift/zkasm_data/generated/memory_i32.zkasm
index d7fbbc37eb59..6c0a6e60b906 100644
--- a/cranelift/zkasm_data/generated/memory_i32.zkasm
+++ b/cranelift/zkasm_data/generated/memory_i32.zkasm
@@ -11,162 +11,229 @@ start:
 function_1:
   SP - 1 => SP
   RR :MSTORE(SP)
-  E :MSTORE(SP - 1)
-  B :MSTORE(SP - 2)
-  SP - 2 => SP
+  D :MSTORE(SP - 1)
+  E :MSTORE(SP - 2)
+  B :MSTORE(SP - 3)
+  SP - 4 => SP
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 8) - 1) } => A
   97n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 8) - 1) } => A
   97n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 1)
+  ${ (E + 1) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 8) - 1) } => A
   98n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 2)
+  ${ (E + 2) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 16 } => A
+  ${ A & ((1 << 8) - 1) } => A
   99n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 25)
+  ${ (E + 25) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 8) - 1) } => A
   122n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 8) - 1) } => A
   97n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 8) - 1) } => A
   97n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 1)
+  ${ (E + 1) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 8) - 1) } => A
   98n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 2)
+  ${ (E + 2) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 16 } => A
+  ${ A & ((1 << 8) - 1) } => A
   99n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 25)
+  ${ (E + 25) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 8) - 1) } => A
   122n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 16) - 1) } => A
   25185n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 16) - 1) } => A
   25185n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 1)
+  ${ (E + 1) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 16) - 1) } => A
   25442n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 2)
+  ${ (E + 2) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 16 } => A
+  ${ A & ((1 << 16) - 1) } => A
   25699n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 25)
+  ${ (E + 25) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 16) - 1) } => A
   122n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 16) - 1) } => A
   25185n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 16) - 1) } => A
   25185n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 1)
+  ${ (E + 1) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 16) - 1) } => A
   25442n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 2)
+  ${ (E + 2) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 16 } => A
+  ${ A & ((1 << 16) - 1) } => A
   25699n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 25)
+  ${ (E + 25) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 16) - 1) } => A
   122n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   1684234849n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ (E) / 8 } => E
   $ => A :MLOAD(MEM:E)
+  ${ A & ((1 << 32) - 1) } => A
   1684234849n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 1)
+  ${ (E + 1) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 32) - 1) } => A
   1701077858n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 2)
+  ${ (E + 2) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 16 } => A
+  ${ A & ((1 << 32) - 1) } => A
   1717920867n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(MEM:E + 25)
+  ${ (E + 25) / 8 } => E
+  $ => A :MLOAD(MEM:E)
+  ${ A >> 8 } => A
+  ${ A & ((1 << 32) - 1) } => A
   122n => B  ;; LoadConst32
   B :ASSERT
-  SP + 2 => SP
-  $ => E :MLOAD(SP - 1)
-  $ => B :MLOAD(SP - 2)
+  SP + 4 => SP
+  $ => D :MLOAD(SP - 1)
+  $ => E :MLOAD(SP - 2)
+  $ => B :MLOAD(SP - 3)
   $ => RR :MLOAD(SP)
   SP + 1 => SP
   :JMP(RR)
diff --git a/cranelift/zkasm_data/state.csv b/cranelift/zkasm_data/state.csv
index ae085c37eef5..c86bc341214c 100644
--- a/cranelift/zkasm_data/state.csv
+++ b/cranelift/zkasm_data/state.csv
@@ -7,7 +7,7 @@ counter,pass,124
 div,pass,27
 eqz,pass,27
 fibonacci,pass,224
-global,pass,26
+global,pass,28
 i32_add_overflows,pass,20
 i32_const,pass,16
 i32_mul_overflows,pass,26
@@ -20,8 +20,8 @@ locals,pass,20
 locals_simple,pass,16
 lt_s,pass,55
 lt_u,pass,27
-memory,pass,44
-memory_i32,runtime error,
+memory,pass,54
+memory_i32,pass,237
 mul,pass,26
 ne,pass,29
 nop,pass,16
diff --git a/docs/zkasm/test_summary.csv b/docs/zkasm/test_summary.csv
index 53dec36d5d78..938c07edf6b7 100644
--- a/docs/zkasm/test_summary.csv
+++ b/docs/zkasm/test_summary.csv
@@ -1,7 +1,7 @@
 Suite path,Passing count,Total count,Total cycles
-cranelift/zkasm_data,27,29,1023
+cranelift/zkasm_data,28,29,1272
 cranelift/zkasm_data/benchmarks/fibonacci,3,3,238058
-cranelift/zkasm_data/benchmarks/sha256,0,1,0
+cranelift/zkasm_data/benchmarks/sha256,1,1,27166
 cranelift/zkasm_data/spectest/conversions,12,24,192
 cranelift/zkasm_data/spectest/i32,287,364,8275
 cranelift/zkasm_data/spectest/i64,291,374,7353

From 23e3d60eb65b64ef81a80d5db92aa069add3504c Mon Sep 17 00:00:00 2001
From: Andrei Kashin <kashin.andrej@gmail.com>
Date: Tue, 30 Jan 2024 15:10:59 +0000
Subject: [PATCH 2/5] Add assert about aligned addresses

---
 cranelift/codegen/src/isa/zkasm/inst/emit.rs  |  10 +
 cranelift/codegen/src/isa/zkasm/inst/mod.rs   |   2 +
 .../sha256/generated/from_rust.zkasm          | 383 ++++++++++++------
 cranelift/zkasm_data/generated/global.zkasm   |  18 +-
 cranelift/zkasm_data/generated/memory.zkasm   |  14 +-
 .../zkasm_data/generated/memory_i32.zkasm     | 219 ++++++----
 6 files changed, 436 insertions(+), 210 deletions(-)

diff --git a/cranelift/codegen/src/isa/zkasm/inst/emit.rs b/cranelift/codegen/src/isa/zkasm/inst/emit.rs
index 80c2582dcce1..3a6e276f6079 100644
--- a/cranelift/codegen/src/isa/zkasm/inst/emit.rs
+++ b/cranelift/codegen/src/isa/zkasm/inst/emit.rs
@@ -591,6 +591,11 @@ impl MachInstEmit for Inst {
                 match from {
                     AMode::RegOffset(r, ..) => {
                         debug_assert_eq!(r, e0());
+                        // For simplicity we assume that register address is word-aligned.
+                        // This was the case for Rust-generated code, but might be violated in the
+                        // future.
+                        put_string(&format!("${{ {} % 8 }} => A\n", reg_name(r)), sink);
+                        put_string(&format!("0: ASSERT\n"), sink);
                         // TODO(#43): Implement the conversion using verifiable computations.
                         put_string(
                             &format!(
@@ -689,6 +694,11 @@ impl MachInstEmit for Inst {
                 match to {
                     AMode::RegOffset(r, ..) => {
                         debug_assert_eq!(r, e0());
+                        // For simplicity we assume that register address is word-aligned.
+                        // This was the case for Rust-generated code, but might be violated in the
+                        // future.
+                        put_string(&format!("${{ {} % 8 }} => A\n", reg_name(r)), sink);
+                        put_string(&format!("0: ASSERT\n"), sink);
                         // TODO(#43): Implement the conversion using verifiable computations.
                         put_string(
                             &format!(
diff --git a/cranelift/codegen/src/isa/zkasm/inst/mod.rs b/cranelift/codegen/src/isa/zkasm/inst/mod.rs
index fe0fc66f1551..6a2e4e8ce82e 100644
--- a/cranelift/codegen/src/isa/zkasm/inst/mod.rs
+++ b/cranelift/codegen/src/isa/zkasm/inst/mod.rs
@@ -337,6 +337,7 @@ fn zkasm_get_operands<F: Fn(VReg) -> VReg>(inst: &Inst, collector: &mut OperandC
                 collector.reg_fixed_use(r, e0());
             }
             let mut clobbered = PRegSet::empty();
+            clobbered.add(a0().to_real_reg().unwrap().into());
             clobbered.add(d0().to_real_reg().unwrap().into());
             collector.reg_clobbers(clobbered);
             collector.reg_def(rd);
@@ -346,6 +347,7 @@ fn zkasm_get_operands<F: Fn(VReg) -> VReg>(inst: &Inst, collector: &mut OperandC
                 collector.reg_fixed_use(r, e0());
             }
             let mut clobbered = PRegSet::empty();
+            clobbered.add(a0().to_real_reg().unwrap().into());
             clobbered.add(d0().to_real_reg().unwrap().into());
             collector.reg_clobbers(clobbered);
             collector.reg_late_use(src);
diff --git a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
index 553a5ef3bb2c..10b4e18ea822 100644
--- a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
+++ b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
@@ -22,14 +22,17 @@ function_1:
   E :MSTORE(SP - 3)
   B :MSTORE(SP - 4)
   SP - 18 => SP
-  $ => A :MLOAD(global_0)
+  $ => E :MLOAD(global_0)
+  E => A
   112n => B  ;; LoadConst32
   $ => A :SUB
   4294967295n => B  ;; LoadConst64
   $ => A :AND
+  A => B
   A :MSTORE(SP + 13)
-  A :MSTORE(global_0)
+  B :MSTORE(global_0)
   24n => B  ;; LoadConst32
+  $ => A :MLOAD(SP + 13)
   $ => D :ADD
   D => A
   4294967295n => B  ;; LoadConst64
@@ -38,11 +41,15 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2072) / 8 } => E
   $ => C :MLOAD(MEM:E)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 2)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   16n => B  ;; LoadConst32
@@ -55,11 +62,15 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2064) / 8 } => E
   $ => C :MLOAD(MEM:E)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 1)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   8n => B  ;; LoadConst32
@@ -72,11 +83,15 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2056) / 8 } => E
   $ => C :MLOAD(MEM:E)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   50n => B  ;; LoadConst32
@@ -88,6 +103,8 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   58n => B  ;; LoadConst32
@@ -99,6 +116,8 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   66n => B  ;; LoadConst32
@@ -110,6 +129,8 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   74n => B  ;; LoadConst32
@@ -121,6 +142,8 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   82n => B  ;; LoadConst32
@@ -132,6 +155,8 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   88n => B  ;; LoadConst32
@@ -143,12 +168,16 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   1n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 104) / 8 } => E
   ${ C & ((1 << 8) - 1) } => C
   $ => D :MLOAD(MEM:E)
@@ -156,11 +185,15 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 32) / 8 } => E
   C :MSTORE(MEM:E)
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 42) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << 16)) | (C << 16) } :MSTORE(MEM:E)
@@ -169,6 +202,8 @@ function_1:
   32856n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 40) / 8 } => E
   ${ C & ((1 << 16) - 1) } => C
   $ => D :MLOAD(MEM:E)
@@ -176,11 +211,15 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2048) / 8 } => E
   $ => C :MLOAD(MEM:E)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   96n => B  ;; LoadConst32
@@ -192,6 +231,8 @@ function_1:
   576460752303423488n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   C :MSTORE(MEM:E)
   40n => B  ;; LoadConst32
@@ -200,9 +241,9 @@ function_1:
   D => A
   4294967295n => B  ;; LoadConst64
   $ => B :AND
-  1n => A  ;; LoadConst32
+  1n => C  ;; LoadConst32
   SP - 1 => SP
-  A :MSTORE(SP)
+  C :MSTORE(SP)
   $ => A :MLOAD(SP + 14)
   zkPC + 2 => RR
   :JMP(function_2)
@@ -210,61 +251,81 @@ function_1:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 2)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 12)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 12)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 1)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 11)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 11)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 10)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 10)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 28) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 9)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 9)
   0n => A  ;; LoadConst32
+  $ => B :MLOAD(SP + 13)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 20) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 8)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 8)
   0n => A  ;; LoadConst32
+  $ => B :MLOAD(SP + 13)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 12) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 7)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 7)
   0n => A  ;; LoadConst32
+  $ => B :MLOAD(SP + 13)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 4) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 6)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 6)
   75n => A  ;; LoadConst64
   A :MSTORE(SP + 4)
   0n => A  ;; LoadConst32
+  $ => B :MLOAD(SP + 13)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 5)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 5)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -283,11 +344,11 @@ function_1:
   65280n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 5)
   $ => B :AND
-  B => C
+  B => D
   8n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
-  C => A
+  D => A
 ;;NEED_INCLUDE: 2-exp
   zkPC + 2 => RR
     :JMP(@two_power + E)
@@ -378,11 +439,11 @@ function_1:
   $ => A :MLOAD(SP + 4)
   B :ASSERT
   56n => A  ;; LoadConst64
-  A => C
+  A => D
   255n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 5)
   $ => B :AND
-  C => A
+  D => A
   B :ASSERT
   71n => A  ;; LoadConst64
   A :MSTORE(SP + 4)
@@ -404,11 +465,11 @@ function_1:
   65280n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 6)
   $ => B :AND
-  B => C
+  B => D
   8n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
-  C => A
+  D => A
 ;;NEED_INCLUDE: 2-exp
   zkPC + 2 => RR
     :JMP(@two_power + E)
@@ -499,11 +560,11 @@ function_1:
   $ => A :MLOAD(SP + 4)
   B :ASSERT
   125n => A  ;; LoadConst64
-  A => E
+  A => C
   255n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 6)
   $ => B :AND
-  E => A
+  C => A
   B :ASSERT
   108n => A  ;; LoadConst64
   A :MSTORE(SP + 4)
@@ -525,11 +586,11 @@ function_1:
   65280n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 10)
   $ => E :AND
-  E => C
+  E => D
   8n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
-  C => A
+  D => A
 ;;NEED_INCLUDE: 2-exp
   zkPC + 2 => RR
     :JMP(@two_power + E)
@@ -646,11 +707,10 @@ function_1:
   65280n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 7)
   $ => D :AND
-  D => C
   8n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
-  C => A
+  D => A
 ;;NEED_INCLUDE: 2-exp
   zkPC + 2 => RR
     :JMP(@two_power + E)
@@ -741,11 +801,11 @@ function_1:
   $ => A :MLOAD(SP + 4)
   B :ASSERT
   163n => A  ;; LoadConst64
-  A => D
+  A => E
   255n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 7)
   $ => B :AND
-  D => A
+  E => A
   B :ASSERT
   94n => A  ;; LoadConst64
   A :MSTORE(SP + 4)
@@ -767,10 +827,11 @@ function_1:
   65280n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 11)
   $ => C :AND
+  C => D
   8n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
-  C => A
+  D => A
 ;;NEED_INCLUDE: 2-exp
   zkPC + 2 => RR
     :JMP(@two_power + E)
@@ -887,11 +948,11 @@ function_1:
   65280n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 8)
   $ => B :AND
-  B => C
+  B => D
   8n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
-  C => A
+  D => A
 ;;NEED_INCLUDE: 2-exp
   zkPC + 2 => RR
     :JMP(@two_power + E)
@@ -982,11 +1043,11 @@ function_1:
   $ => A :MLOAD(SP + 4)
   B :ASSERT
   244n => A  ;; LoadConst64
-  A => C
+  A => D
   255n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 8)
   $ => B :AND
-  C => A
+  D => A
   B :ASSERT
   221n => A  ;; LoadConst64
   A :MSTORE(SP + 4)
@@ -1008,11 +1069,11 @@ function_1:
   65280n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 12)
   $ => B :AND
-  B => C
+  B => D
   8n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
-  C => A
+  D => A
 ;;NEED_INCLUDE: 2-exp
   zkPC + 2 => RR
     :JMP(@two_power + E)
@@ -1103,11 +1164,11 @@ function_1:
   $ => A :MLOAD(SP + 3)
   B :ASSERT
   93n => A  ;; LoadConst64
-  A => E
+  A => C
   255n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 12)
   $ => B :AND
-  E => A
+  C => A
   B :ASSERT
   246n => A  ;; LoadConst64
   A :MSTORE(SP + 3)
@@ -1129,11 +1190,11 @@ function_1:
   65280n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 9)
   $ => E :AND
-  E => C
+  E => D
   8n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
-  C => A
+  D => A
 ;;NEED_INCLUDE: 2-exp
   zkPC + 2 => RR
     :JMP(@two_power + E)
@@ -1234,8 +1295,8 @@ function_1:
   $ => A :MLOAD(SP + 13)
   $ => A :ADD
   4294967295n => B  ;; LoadConst64
-  $ => A :AND
-  A :MSTORE(global_0)
+  $ => B :AND
+  B :MSTORE(global_0)
   SP + 18 => SP
   $ => C :MLOAD(SP - 1)
   $ => D :MLOAD(SP - 2)
@@ -1254,11 +1315,13 @@ function_2:
   SP - 1182 => SP
   A :MSTORE(SP)
   B :MSTORE(SP + 1)
-  $ => A :MLOAD(SP + 1183)
-  A :MSTORE(SP + 2)
+  $ => B :MLOAD(SP + 1183)
+  B :MSTORE(SP + 2)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 28) / 8 } => E
   $ => E :MLOAD(MEM:E)
   ${ E >> 32 } => E
@@ -1266,12 +1329,16 @@ function_2:
   E :MSTORE(SP + 9)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 24) / 8 } => E
   $ => C :MLOAD(MEM:E)
   ${ C & ((1 << 32) - 1) } => C
   C :MSTORE(SP + 10)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 20) / 8 } => E
   $ => C :MLOAD(MEM:E)
   ${ C >> 32 } => C
@@ -1279,12 +1346,16 @@ function_2:
   C :MSTORE(SP + 11)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 16) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 12)
+  $ => C :MLOAD(MEM:E)
+  ${ C & ((1 << 32) - 1) } => C
+  C :MSTORE(SP + 12)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 12) / 8 } => E
   $ => E :MLOAD(MEM:E)
   ${ E >> 32 } => E
@@ -1292,12 +1363,16 @@ function_2:
   E :MSTORE(SP + 13)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 8) / 8 } => E
   $ => E :MLOAD(MEM:E)
   ${ E & ((1 << 32) - 1) } => E
   E :MSTORE(SP + 14)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 4) / 8 } => E
   $ => C :MLOAD(MEM:E)
   ${ C >> 32 } => C
@@ -1305,6 +1380,8 @@ function_2:
   C :MSTORE(SP + 15)
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   $ => B :MLOAD(MEM:E)
   ${ B & ((1 << 32) - 1) } => B
@@ -1595,10 +1672,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1165)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1165)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -1806,11 +1885,13 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 4) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1155)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1155)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -2144,10 +2225,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 8) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1139)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1139)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -2481,11 +2564,13 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 12) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1123)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1123)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -2819,10 +2904,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 16) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1107)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1107)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -3155,11 +3242,13 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 20) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1091)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1091)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -3493,10 +3582,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 24) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1075)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1075)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -3830,11 +3921,13 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 28) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1059)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1059)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -4168,10 +4261,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 32) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1043)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1043)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -4505,11 +4600,13 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 36) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1027)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1027)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -4843,10 +4940,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 40) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 1011)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 1011)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -5180,11 +5279,13 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 44) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 995)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 995)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -5518,10 +5619,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 48) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 979)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 979)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -5855,11 +5958,13 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 52) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 963)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 963)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -6193,10 +6298,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 56) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 947)
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 947)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -6530,11 +6637,13 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 60) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 32 } => A
-  ${ A & ((1 << 32) - 1) } => A
-  A :MSTORE(SP + 931)
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 32 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B :MSTORE(SP + 931)
   24n => A  ;; LoadConst32
   31n => B  ;; LoadConst64
   $ => E :AND
@@ -27758,35 +27867,45 @@ label_2_7:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
-  $ => A :MLOAD(SP + 9)
+  $ => C :MLOAD(SP + 9)
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 28) / 8 } => E
-  ${ A & ((1 << 32) - 1) } => A
+  ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 32)) | (A << 32) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(SP + 10)
+  $ => C :MLOAD(SP + 10)
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 24) / 8 } => E
-  ${ A & ((1 << 32) - 1) } => A
+  ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 0)) | (A << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 11)
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 20) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  $ => A :MLOAD(SP + 12)
+  $ => C :MLOAD(SP + 12)
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 16) / 8 } => E
-  ${ A & ((1 << 32) - 1) } => A
+  ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 0)) | (A << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 13)
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 12) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
@@ -27794,6 +27913,8 @@ label_2_7:
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 14)
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 8) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
@@ -27801,6 +27922,8 @@ label_2_7:
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 15)
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 4) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
@@ -27808,6 +27931,8 @@ label_2_7:
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => B :MLOAD(SP + 16)
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   ${ B & ((1 << 32) - 1) } => B
   $ => D :MLOAD(MEM:E)
diff --git a/cranelift/zkasm_data/generated/global.zkasm b/cranelift/zkasm_data/generated/global.zkasm
index 8a9e92eeba98..465a3ddc9429 100644
--- a/cranelift/zkasm_data/generated/global.zkasm
+++ b/cranelift/zkasm_data/generated/global.zkasm
@@ -10,23 +10,27 @@ start:
 function_1:
   SP - 1 => SP
   RR :MSTORE(SP)
-  D :MSTORE(SP - 1)
-  E :MSTORE(SP - 2)
-  B :MSTORE(SP - 3)
+  C :MSTORE(SP - 1)
+  D :MSTORE(SP - 2)
+  E :MSTORE(SP - 3)
+  B :MSTORE(SP - 4)
   SP - 4 => SP
   3n => E  ;; LoadConst32
   E :MSTORE(global_1)
-  $ => A :MLOAD(global_0)
+  $ => E :MLOAD(global_0)
+  E => C
   $ => B :MLOAD(global_1)
+  C => A
   $ => A :ADD
   4294967295n => B  ;; LoadConst64
   $ => A :AND
   1n => B  ;; LoadConst32
   B :ASSERT
   SP + 4 => SP
-  $ => D :MLOAD(SP - 1)
-  $ => E :MLOAD(SP - 2)
-  $ => B :MLOAD(SP - 3)
+  $ => C :MLOAD(SP - 1)
+  $ => D :MLOAD(SP - 2)
+  $ => E :MLOAD(SP - 3)
+  $ => B :MLOAD(SP - 4)
   $ => RR :MLOAD(SP)
   SP + 1 => SP
   :JMP(RR)
diff --git a/cranelift/zkasm_data/generated/memory.zkasm b/cranelift/zkasm_data/generated/memory.zkasm
index c255b6877c56..fcd3c1ac387d 100644
--- a/cranelift/zkasm_data/generated/memory.zkasm
+++ b/cranelift/zkasm_data/generated/memory.zkasm
@@ -15,6 +15,8 @@ function_1:
   2n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
@@ -23,6 +25,8 @@ function_1:
   3n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
@@ -30,13 +34,17 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
-  A => C
+  $ => E :MLOAD(MEM:E)
+  ${ E & ((1 << 32) - 1) } => E
+  E => C
   8n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
   $ => B :MLOAD(MEM:E)
   ${ B & ((1 << 32) - 1) } => B
diff --git a/cranelift/zkasm_data/generated/memory_i32.zkasm b/cranelift/zkasm_data/generated/memory_i32.zkasm
index 6c0a6e60b906..0311d85675ed 100644
--- a/cranelift/zkasm_data/generated/memory_i32.zkasm
+++ b/cranelift/zkasm_data/generated/memory_i32.zkasm
@@ -11,229 +11,306 @@ start:
 function_1:
   SP - 1 => SP
   RR :MSTORE(SP)
-  D :MSTORE(SP - 1)
-  E :MSTORE(SP - 2)
-  B :MSTORE(SP - 3)
+  C :MSTORE(SP - 1)
+  D :MSTORE(SP - 2)
+  E :MSTORE(SP - 3)
+  B :MSTORE(SP - 4)
   SP - 4 => SP
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 8) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 8) - 1) } => B
+  B => A
   97n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 8) - 1) } => A
+  $ => C :MLOAD(MEM:E)
+  ${ C & ((1 << 8) - 1) } => C
+  C => A
   97n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 1) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 8) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 8 } => E
+  ${ E & ((1 << 8) - 1) } => E
+  E => A
   98n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 16 } => A
-  ${ A & ((1 << 8) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 16 } => E
+  ${ E & ((1 << 8) - 1) } => E
+  E => A
   99n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 25) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 8) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 8 } => B
+  ${ B & ((1 << 8) - 1) } => B
+  B => A
   122n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 8) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 8) - 1) } => B
+  B => A
   97n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 8) - 1) } => A
+  $ => C :MLOAD(MEM:E)
+  ${ C & ((1 << 8) - 1) } => C
+  C => A
   97n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 1) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 8) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 8 } => E
+  ${ E & ((1 << 8) - 1) } => E
+  E => A
   98n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 16 } => A
-  ${ A & ((1 << 8) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 16 } => E
+  ${ E & ((1 << 8) - 1) } => E
+  E => A
   99n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 25) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 8) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 8 } => B
+  ${ B & ((1 << 8) - 1) } => B
+  B => A
   122n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 16) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 16) - 1) } => B
+  B => A
   25185n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 16) - 1) } => A
+  $ => C :MLOAD(MEM:E)
+  ${ C & ((1 << 16) - 1) } => C
+  C => A
   25185n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 1) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 16) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 8 } => E
+  ${ E & ((1 << 16) - 1) } => E
+  E => A
   25442n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 16 } => A
-  ${ A & ((1 << 16) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 16 } => E
+  ${ E & ((1 << 16) - 1) } => E
+  E => A
   25699n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 25) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 16) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 8 } => B
+  ${ B & ((1 << 16) - 1) } => B
+  B => A
   122n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 16) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 16) - 1) } => B
+  B => A
   25185n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 16) - 1) } => A
+  $ => C :MLOAD(MEM:E)
+  ${ C & ((1 << 16) - 1) } => C
+  C => A
   25185n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 1) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 16) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 8 } => E
+  ${ E & ((1 << 16) - 1) } => E
+  E => A
   25442n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 16 } => A
-  ${ A & ((1 << 16) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 16 } => E
+  ${ E & ((1 << 16) - 1) } => E
+  E => A
   25699n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 25) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 16) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 8 } => B
+  ${ B & ((1 << 16) - 1) } => B
+  B => A
   122n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B & ((1 << 32) - 1) } => B
+  B => A
   1684234849n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A & ((1 << 32) - 1) } => A
+  $ => C :MLOAD(MEM:E)
+  ${ C & ((1 << 32) - 1) } => C
+  C => A
   1684234849n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 1) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 32) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 8 } => E
+  ${ E & ((1 << 32) - 1) } => E
+  E => A
   1701077858n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 2) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 16 } => A
-  ${ A & ((1 << 32) - 1) } => A
+  $ => E :MLOAD(MEM:E)
+  ${ E >> 16 } => E
+  ${ E & ((1 << 32) - 1) } => E
+  E => A
   1717920867n => B  ;; LoadConst32
   B :ASSERT
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
+  ${ E % 8 } => A
+  0: ASSERT
   ${ (E + 25) / 8 } => E
-  $ => A :MLOAD(MEM:E)
-  ${ A >> 8 } => A
-  ${ A & ((1 << 32) - 1) } => A
+  $ => B :MLOAD(MEM:E)
+  ${ B >> 8 } => B
+  ${ B & ((1 << 32) - 1) } => B
+  B => A
   122n => B  ;; LoadConst32
   B :ASSERT
   SP + 4 => SP
-  $ => D :MLOAD(SP - 1)
-  $ => E :MLOAD(SP - 2)
-  $ => B :MLOAD(SP - 3)
+  $ => C :MLOAD(SP - 1)
+  $ => D :MLOAD(SP - 2)
+  $ => E :MLOAD(SP - 3)
+  $ => B :MLOAD(SP - 4)
   $ => RR :MLOAD(SP)
   SP + 1 => SP
   :JMP(RR)

From b35b2942e25666459662458011c6341876c01cde Mon Sep 17 00:00:00 2001
From: Andrei Kashin <kashin.andrej@gmail.com>
Date: Fri, 2 Feb 2024 16:41:15 +0000
Subject: [PATCH 3/5] Handle misaligned base address

---
 cranelift/codegen/src/isa/zkasm/inst/emit.rs  | 141 +++---
 .../sha256/generated/from_rust.zkasm          | 428 +++++++++++-------
 cranelift/zkasm_data/generated/memory.zkasm   |  28 +-
 .../zkasm_data/generated/memory_i32.zkasm     | 165 ++++---
 4 files changed, 449 insertions(+), 313 deletions(-)

diff --git a/cranelift/codegen/src/isa/zkasm/inst/emit.rs b/cranelift/codegen/src/isa/zkasm/inst/emit.rs
index 3a6e276f6079..b99d1e2ff915 100644
--- a/cranelift/codegen/src/isa/zkasm/inst/emit.rs
+++ b/cranelift/codegen/src/isa/zkasm/inst/emit.rs
@@ -591,12 +591,11 @@ impl MachInstEmit for Inst {
                 match from {
                     AMode::RegOffset(r, ..) => {
                         debug_assert_eq!(r, e0());
-                        // For simplicity we assume that register address is word-aligned.
-                        // This was the case for Rust-generated code, but might be violated in the
-                        // future.
-                        put_string(&format!("${{ {} % 8 }} => A\n", reg_name(r)), sink);
-                        put_string(&format!("0: ASSERT\n"), sink);
                         // TODO(#43): Implement the conversion using verifiable computations.
+                        put_string(
+                            &format!("${{ ({}) % 8 }} => A\n", access_reg_with_offset(r, offset),),
+                            sink,
+                        );
                         put_string(
                             &format!(
                                 "${{ ({}) / 8 }} => {}\n",
@@ -605,9 +604,18 @@ impl MachInstEmit for Inst {
                             ),
                             sink,
                         );
-                        let rem = offset % 8;
-                        let width = op.width() as i64;
 
+                        // Handle the case when read spans two slots.
+                        // We do this read first in case `rd == r == E` which will clobber the
+                        // address register after second `MLOAD`.
+                        put_string(
+                            &format!(
+                                "$ => {} :MLOAD(MEM:{})\n",
+                                reg_name(d0()),
+                                access_reg_with_offset(r, 1)
+                            ),
+                            sink,
+                        );
                         put_string(
                             &format!(
                                 "$ => {} :MLOAD(MEM:{})\n",
@@ -618,47 +626,33 @@ impl MachInstEmit for Inst {
                         );
                         // TODO(#34): Implement unaligned and narrow reads using verifiable
                         // computations.
-                        if rem > 0 {
-                            put_string(
-                                &format!(
-                                    "${{ {} >> {} }} => {}\n",
-                                    reg_name(rd.to_reg()),
-                                    8 * rem,
-                                    reg_name(rd.to_reg())
-                                ),
-                                sink,
-                            );
-                        }
+                        put_string(
+                            &format!(
+                                "${{ {} >> (8 * A) }} => {}\n",
+                                reg_name(rd.to_reg()),
+                                reg_name(rd.to_reg())
+                            ),
+                            sink,
+                        );
 
-                        // Handle the case when read spans two slots.
-                        if rem + width > 8 {
-                            let rem = rem + width - 8;
-                            put_string(
-                                &format!(
-                                    "$ => {} :MLOAD(MEM:{})\n",
-                                    reg_name(d0()),
-                                    access_reg_with_offset(r, 1)
-                                ),
-                                sink,
-                            );
-                            put_string(
-                                &format!(
-                                    "${{ (D << {}) | {} }} => {}\n",
-                                    64 - 8 * rem,
-                                    reg_name(rd.to_reg()),
-                                    reg_name(rd.to_reg()),
-                                ),
-                                sink,
-                            );
-                        }
+                        // Merge in the read from the second slot.
+                        put_string(
+                            &format!(
+                                "${{ (D << (128 - 8 * (A + {}))) | {} }} => {}\n",
+                                op.width(),
+                                reg_name(rd.to_reg()),
+                                reg_name(rd.to_reg()),
+                            ),
+                            sink,
+                        );
 
                         // Mask the value to the width of the resulting type.
-                        if width < 8 {
+                        if op.width() < 8 {
                             put_string(
                                 &format!(
                                     "${{ {} & ((1 << {}) - 1) }} => {}\n",
                                     reg_name(rd.to_reg()),
-                                    8 * width,
+                                    8 * op.width(),
                                     reg_name(rd.to_reg()),
                                 ),
                                 sink,
@@ -694,12 +688,11 @@ impl MachInstEmit for Inst {
                 match to {
                     AMode::RegOffset(r, ..) => {
                         debug_assert_eq!(r, e0());
-                        // For simplicity we assume that register address is word-aligned.
-                        // This was the case for Rust-generated code, but might be violated in the
-                        // future.
-                        put_string(&format!("${{ {} % 8 }} => A\n", reg_name(r)), sink);
-                        put_string(&format!("0: ASSERT\n"), sink);
                         // TODO(#43): Implement the conversion using verifiable computations.
+                        put_string(
+                            &format!("${{ ({}) % 8 }} => A\n", access_reg_with_offset(r, offset)),
+                            sink,
+                        );
                         put_string(
                             &format!(
                                 "${{ ({}) / 8 }} => {}\n",
@@ -708,19 +701,10 @@ impl MachInstEmit for Inst {
                             ),
                             sink,
                         );
-                        let rem = offset % 8;
-                        let width = op.width() as i64;
-
-                        if op == StoreOP::I64 && rem == 0 {
-                            put_string(
-                                &format!("{} :MSTORE(MEM:{})\n", reg_name(src), reg_name(r)),
-                                sink,
-                            );
-                            return;
-                        }
 
                         // TODO(#34): Implement unaligned and narrow writes using verifiable
                         // computations.
+                        let width = op.width() as i64;
                         if width < 8 {
                             put_string(
                                 &format!(
@@ -738,38 +722,35 @@ impl MachInstEmit for Inst {
                         );
                         put_string(
                             &format!(
-                                "${{ (D & ~(((1 << {}) - 1) << {})) | ({} << {}) }} :MSTORE(MEM:{})\n",
+                                "${{ (D & ~(((1 << {}) - 1) << (8 * A))) | ({} << (8 * A)) }} :MSTORE(MEM:{})\n",
                                 8 * width,
-                                8 * rem,
                                 reg_name(src),
-                                8 * rem,
                                 reg_name(r),
                             ),
                             sink,
                         );
 
                         // Handle the case when write spans two slots.
-                        if rem + width > 8 {
-                            let rem = rem + width - 8;
-                            put_string(
-                                &format!(
-                                    "$ => {} :MLOAD(MEM:{})\n",
-                                    reg_name(d0()),
-                                    access_reg_with_offset(r, 1)
-                                ),
-                                sink,
-                            );
-                            put_string(
-                                &format!(
-                                    "${{ (D & ~((1 << {}) - 1)) | ({} & ((1 << {}) - 1)) }} :MSTORE(MEM:{})\n",
-                                    8 * rem,
-                                    reg_name(src),
-                                    8 * rem,
-                                    access_reg_with_offset(r, 1),
-                                ),
-                                sink,
-                            );
-                        }
+                        put_string(
+                            &format!("${{ (A + {width} > 8) ? (A + {width} - 8) : 0 }} => A\n"),
+                            sink,
+                        );
+                        put_string(
+                            &format!(
+                                "$ => {} :MLOAD(MEM:{})\n",
+                                reg_name(d0()),
+                                access_reg_with_offset(r, 1)
+                            ),
+                            sink,
+                        );
+                        put_string(
+                            &format!(
+                                "${{ (D & ~((1 << (8 * A)) - 1)) | ({} & ((1 << (8 * A)) - 1)) }} :MSTORE(MEM:{})\n",
+                                reg_name(src),
+                                access_reg_with_offset(r, 1),
+                            ),
+                            sink,
+                        );
                     }
                     AMode::SPOffset(..) | AMode::NominalSPOffset(..) | AMode::FPOffset(..) => {
                         assert_eq!(offset % 8, 0);
diff --git a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
index 10b4e18ea822..3324c375b74c 100644
--- a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
+++ b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
@@ -41,17 +41,22 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2072) % 8 } => A
   ${ (E + 2072) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 8))) | C } => C
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 2)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   16n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => E :ADD
@@ -62,17 +67,22 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2064) % 8 } => A
   ${ (E + 2064) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 8))) | C } => C
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 1)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   8n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => B :ADD
@@ -83,17 +93,22 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2056) % 8 } => A
   ${ (E + 2056) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 8))) | C } => C
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   50n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => B :ADD
@@ -103,10 +118,13 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   58n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => C :ADD
@@ -116,10 +134,13 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   66n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => D :ADD
@@ -129,10 +150,13 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   74n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => E :ADD
@@ -142,10 +166,13 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   82n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => B :ADD
@@ -155,10 +182,13 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   88n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => B :ADD
@@ -168,60 +198,75 @@ function_1:
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   1n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 104) % 8 } => A
   ${ (E + 104) / 8 } => E
   ${ C & ((1 << 8) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 8) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 8) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 1 > 8) ? (A + 1 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 32) % 8 } => A
   ${ (E + 32) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 42) % 8 } => A
   ${ (E + 42) / 8 } => E
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 64) - 1) << 16)) | (C << 16) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
-  ${ (D & ~((1 << 16) - 1)) | (C & ((1 << 16) - 1)) } :MSTORE(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   32856n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 40) % 8 } => A
   ${ (E + 40) / 8 } => E
   ${ C & ((1 << 16) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 16) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 16) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 2 > 8) ? (A + 2 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2048) % 8 } => A
   ${ (E + 2048) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 8))) | C } => C
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   96n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => C :ADD
@@ -231,10 +276,13 @@ function_1:
   576460752303423488n => C  ;; LoadConst64
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
-  C :MSTORE(MEM:E)
+  $ => D :MLOAD(MEM:E)
+  ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   40n => B  ;; LoadConst32
   $ => A :MLOAD(SP + 13)
   $ => D :ADD
@@ -251,68 +299,78 @@ function_1:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 2)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 12)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 1)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 11)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 10)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 28) % 8 } => A
   ${ (E + 28) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 9)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 20) % 8 } => A
   ${ (E + 20) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 8)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 12) % 8 } => A
   ${ (E + 12) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 7)
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 4) % 8 } => A
   ${ (E + 4) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 6)
   75n => A  ;; LoadConst64
@@ -320,10 +378,12 @@ function_1:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 13)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 5)
   24n => A  ;; LoadConst32
@@ -1320,70 +1380,82 @@ function_2:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 28) % 8 } => A
   ${ (E + 28) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 32 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 4))) | E } => E
   ${ E & ((1 << 32) - 1) } => E
   E :MSTORE(SP + 9)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 24) % 8 } => A
   ${ (E + 24) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 4))) | C } => C
   ${ C & ((1 << 32) - 1) } => C
   C :MSTORE(SP + 10)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 20) % 8 } => A
   ${ (E + 20) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
-  ${ C >> 32 } => C
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 4))) | C } => C
   ${ C & ((1 << 32) - 1) } => C
   C :MSTORE(SP + 11)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 16) % 8 } => A
   ${ (E + 16) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 4))) | C } => C
   ${ C & ((1 << 32) - 1) } => C
   C :MSTORE(SP + 12)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 12) % 8 } => A
   ${ (E + 12) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 32 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 4))) | E } => E
   ${ E & ((1 << 32) - 1) } => E
   E :MSTORE(SP + 13)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 8) % 8 } => A
   ${ (E + 8) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 4))) | E } => E
   ${ E & ((1 << 32) - 1) } => E
   E :MSTORE(SP + 14)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 4) % 8 } => A
   ${ (E + 4) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
-  ${ C >> 32 } => C
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 4))) | C } => C
   ${ C & ((1 << 32) - 1) } => C
   C :MSTORE(SP + 15)
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 16)
   0n => B  ;; LoadConst32
@@ -1672,10 +1744,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1165)
   24n => A  ;; LoadConst32
@@ -1885,11 +1959,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 4) % 8 } => A
   ${ (E + 4) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1155)
   24n => A  ;; LoadConst32
@@ -2225,10 +2300,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 8) % 8 } => A
   ${ (E + 8) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1139)
   24n => A  ;; LoadConst32
@@ -2564,11 +2641,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 12) % 8 } => A
   ${ (E + 12) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1123)
   24n => A  ;; LoadConst32
@@ -2904,10 +2982,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 16) % 8 } => A
   ${ (E + 16) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1107)
   24n => A  ;; LoadConst32
@@ -3242,11 +3322,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 20) % 8 } => A
   ${ (E + 20) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1091)
   24n => A  ;; LoadConst32
@@ -3582,10 +3663,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 24) % 8 } => A
   ${ (E + 24) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1075)
   24n => A  ;; LoadConst32
@@ -3921,11 +4004,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 28) % 8 } => A
   ${ (E + 28) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1059)
   24n => A  ;; LoadConst32
@@ -4261,10 +4345,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 32) % 8 } => A
   ${ (E + 32) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1043)
   24n => A  ;; LoadConst32
@@ -4600,11 +4686,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 36) % 8 } => A
   ${ (E + 36) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1027)
   24n => A  ;; LoadConst32
@@ -4940,10 +5027,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 40) % 8 } => A
   ${ (E + 40) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 1011)
   24n => A  ;; LoadConst32
@@ -5279,11 +5368,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 44) % 8 } => A
   ${ (E + 44) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 995)
   24n => A  ;; LoadConst32
@@ -5619,10 +5709,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 48) % 8 } => A
   ${ (E + 48) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 979)
   24n => A  ;; LoadConst32
@@ -5958,11 +6050,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 52) % 8 } => A
   ${ (E + 52) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 963)
   24n => A  ;; LoadConst32
@@ -6298,10 +6391,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 56) % 8 } => A
   ${ (E + 56) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 947)
   24n => A  ;; LoadConst32
@@ -6637,11 +6732,12 @@ label_2_3:
   0n => A  ;; LoadConst32
   $ => B :MLOAD(SP + 8)
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 60) % 8 } => A
   ${ (E + 60) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 32 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B :MSTORE(SP + 931)
   24n => A  ;; LoadConst32
@@ -27868,75 +27964,91 @@ label_2_7:
   $ => B :MLOAD(SP)
   $ => E :ADD
   $ => C :MLOAD(SP + 9)
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 28) % 8 } => A
   ${ (E + 28) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 10)
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 24) % 8 } => A
   ${ (E + 24) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 11)
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 20) % 8 } => A
   ${ (E + 20) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 12)
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 16) % 8 } => A
   ${ (E + 16) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 13)
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 12) % 8 } => A
   ${ (E + 12) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 14)
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 8) % 8 } => A
   ${ (E + 8) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => C :MLOAD(SP + 15)
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 4) % 8 } => A
   ${ (E + 4) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 32)) | (C << 32) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
   $ => E :ADD
   $ => B :MLOAD(SP + 16)
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
   ${ B & ((1 << 32) - 1) } => B
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 0)) | (B << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (B << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (B & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   SP + 1182 => SP
   $ => C :MLOAD(SP - 1)
   $ => D :MLOAD(SP - 2)
diff --git a/cranelift/zkasm_data/generated/memory.zkasm b/cranelift/zkasm_data/generated/memory.zkasm
index fcd3c1ac387d..f318101c67b6 100644
--- a/cranelift/zkasm_data/generated/memory.zkasm
+++ b/cranelift/zkasm_data/generated/memory.zkasm
@@ -15,38 +15,46 @@ function_1:
   2n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   8n => B  ;; LoadConst32
   3n => C  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
-  ${ (D & ~(((1 << 32) - 1) << 0)) | (C << 0) } :MSTORE(MEM:E)
+  ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
+  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  $ => D :MLOAD(MEM:E + 1)
+  ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 4))) | E } => E
   ${ E & ((1 << 32) - 1) } => E
   E => C
   8n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   C => A
   $ => A :ADD
diff --git a/cranelift/zkasm_data/generated/memory_i32.zkasm b/cranelift/zkasm_data/generated/memory_i32.zkasm
index 0311d85675ed..cf9e3dddc9f8 100644
--- a/cranelift/zkasm_data/generated/memory_i32.zkasm
+++ b/cranelift/zkasm_data/generated/memory_i32.zkasm
@@ -19,10 +19,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 1))) | B } => B
   ${ B & ((1 << 8) - 1) } => B
   B => A
   97n => B  ;; LoadConst32
@@ -30,10 +32,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 1))) | C } => C
   ${ C & ((1 << 8) - 1) } => C
   C => A
   97n => B  ;; LoadConst32
@@ -41,11 +45,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 1) % 8 } => A
   ${ (E + 1) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 8 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 1))) | E } => E
   ${ E & ((1 << 8) - 1) } => E
   E => A
   98n => B  ;; LoadConst32
@@ -53,11 +58,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2) % 8 } => A
   ${ (E + 2) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 16 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 1))) | E } => E
   ${ E & ((1 << 8) - 1) } => E
   E => A
   99n => B  ;; LoadConst32
@@ -65,11 +71,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 25) % 8 } => A
   ${ (E + 25) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 8 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 1))) | B } => B
   ${ B & ((1 << 8) - 1) } => B
   B => A
   122n => B  ;; LoadConst32
@@ -77,10 +84,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 1))) | B } => B
   ${ B & ((1 << 8) - 1) } => B
   B => A
   97n => B  ;; LoadConst32
@@ -88,10 +97,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 1))) | C } => C
   ${ C & ((1 << 8) - 1) } => C
   C => A
   97n => B  ;; LoadConst32
@@ -99,11 +110,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 1) % 8 } => A
   ${ (E + 1) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 8 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 1))) | E } => E
   ${ E & ((1 << 8) - 1) } => E
   E => A
   98n => B  ;; LoadConst32
@@ -111,11 +123,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2) % 8 } => A
   ${ (E + 2) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 16 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 1))) | E } => E
   ${ E & ((1 << 8) - 1) } => E
   E => A
   99n => B  ;; LoadConst32
@@ -123,11 +136,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 25) % 8 } => A
   ${ (E + 25) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 8 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 1))) | B } => B
   ${ B & ((1 << 8) - 1) } => B
   B => A
   122n => B  ;; LoadConst32
@@ -135,10 +149,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 2))) | B } => B
   ${ B & ((1 << 16) - 1) } => B
   B => A
   25185n => B  ;; LoadConst32
@@ -146,10 +162,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 2))) | C } => C
   ${ C & ((1 << 16) - 1) } => C
   C => A
   25185n => B  ;; LoadConst32
@@ -157,11 +175,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 1) % 8 } => A
   ${ (E + 1) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 8 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 2))) | E } => E
   ${ E & ((1 << 16) - 1) } => E
   E => A
   25442n => B  ;; LoadConst32
@@ -169,11 +188,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2) % 8 } => A
   ${ (E + 2) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 16 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 2))) | E } => E
   ${ E & ((1 << 16) - 1) } => E
   E => A
   25699n => B  ;; LoadConst32
@@ -181,11 +201,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 25) % 8 } => A
   ${ (E + 25) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 8 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 2))) | B } => B
   ${ B & ((1 << 16) - 1) } => B
   B => A
   122n => B  ;; LoadConst32
@@ -193,10 +214,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 2))) | B } => B
   ${ B & ((1 << 16) - 1) } => B
   B => A
   25185n => B  ;; LoadConst32
@@ -204,10 +227,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 2))) | C } => C
   ${ C & ((1 << 16) - 1) } => C
   C => A
   25185n => B  ;; LoadConst32
@@ -215,11 +240,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 1) % 8 } => A
   ${ (E + 1) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 8 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 2))) | E } => E
   ${ E & ((1 << 16) - 1) } => E
   E => A
   25442n => B  ;; LoadConst32
@@ -227,11 +253,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2) % 8 } => A
   ${ (E + 2) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 16 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 2))) | E } => E
   ${ E & ((1 << 16) - 1) } => E
   E => A
   25699n => B  ;; LoadConst32
@@ -239,11 +266,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 25) % 8 } => A
   ${ (E + 25) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 8 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 2))) | B } => B
   ${ B & ((1 << 16) - 1) } => B
   B => A
   122n => B  ;; LoadConst32
@@ -251,10 +279,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B => A
   1684234849n => B  ;; LoadConst32
@@ -262,10 +292,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E) % 8 } => A
   ${ (E) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => C :MLOAD(MEM:E)
+  ${ C >> (8 * A) } => C
+  ${ (D << (128 - 8 * (A + 4))) | C } => C
   ${ C & ((1 << 32) - 1) } => C
   C => A
   1684234849n => B  ;; LoadConst32
@@ -273,11 +305,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 1) % 8 } => A
   ${ (E + 1) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 8 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 4))) | E } => E
   ${ E & ((1 << 32) - 1) } => E
   E => A
   1701077858n => B  ;; LoadConst32
@@ -285,11 +318,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 2) % 8 } => A
   ${ (E + 2) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => E :MLOAD(MEM:E)
-  ${ E >> 16 } => E
+  ${ E >> (8 * A) } => E
+  ${ (D << (128 - 8 * (A + 4))) | E } => E
   ${ E & ((1 << 32) - 1) } => E
   E => A
   1717920867n => B  ;; LoadConst32
@@ -297,11 +331,12 @@ function_1:
   0n => B  ;; LoadConst32
   0n => A  ;; LoadConst32
   $ => E :ADD
-  ${ E % 8 } => A
-  0: ASSERT
+  ${ (E + 25) % 8 } => A
   ${ (E + 25) / 8 } => E
+  $ => D :MLOAD(MEM:E + 1)
   $ => B :MLOAD(MEM:E)
-  ${ B >> 8 } => B
+  ${ B >> (8 * A) } => B
+  ${ (D << (128 - 8 * (A + 4))) | B } => B
   ${ B & ((1 << 32) - 1) } => B
   B => A
   122n => B  ;; LoadConst32

From 087fda60bd1b3d091bbe33059468cd4aa2d2947b Mon Sep 17 00:00:00 2001
From: Andrei Kashin <kashin.andrej@gmail.com>
Date: Fri, 2 Feb 2024 16:43:41 +0000
Subject: [PATCH 4/5] Update state files

---
 cranelift/zkasm_data/benchmarks/sha256/state.csv | 2 +-
 cranelift/zkasm_data/state.csv                   | 6 +++---
 docs/zkasm/test_summary.csv                      | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/cranelift/zkasm_data/benchmarks/sha256/state.csv b/cranelift/zkasm_data/benchmarks/sha256/state.csv
index d6983d88bcac..6fe66c05fc76 100644
--- a/cranelift/zkasm_data/benchmarks/sha256/state.csv
+++ b/cranelift/zkasm_data/benchmarks/sha256/state.csv
@@ -1,2 +1,2 @@
 Test,Status,Cycles
-from_rust,pass,27166
+from_rust,pass,27403
diff --git a/cranelift/zkasm_data/state.csv b/cranelift/zkasm_data/state.csv
index c86bc341214c..96dea8f62920 100644
--- a/cranelift/zkasm_data/state.csv
+++ b/cranelift/zkasm_data/state.csv
@@ -7,7 +7,7 @@ counter,pass,124
 div,pass,27
 eqz,pass,27
 fibonacci,pass,224
-global,pass,28
+global,pass,32
 i32_add_overflows,pass,20
 i32_const,pass,16
 i32_mul_overflows,pass,26
@@ -20,8 +20,8 @@ locals,pass,20
 locals_simple,pass,16
 lt_s,pass,55
 lt_u,pass,27
-memory,pass,54
-memory_i32,pass,237
+memory,pass,70
+memory_i32,pass,349
 mul,pass,26
 ne,pass,29
 nop,pass,16
diff --git a/docs/zkasm/test_summary.csv b/docs/zkasm/test_summary.csv
index 938c07edf6b7..754d7dea3407 100644
--- a/docs/zkasm/test_summary.csv
+++ b/docs/zkasm/test_summary.csv
@@ -1,7 +1,7 @@
 Suite path,Passing count,Total count,Total cycles
-cranelift/zkasm_data,28,29,1272
+cranelift/zkasm_data,28,29,1404
 cranelift/zkasm_data/benchmarks/fibonacci,3,3,238058
-cranelift/zkasm_data/benchmarks/sha256,1,1,27166
+cranelift/zkasm_data/benchmarks/sha256,1,1,27403
 cranelift/zkasm_data/spectest/conversions,12,24,192
 cranelift/zkasm_data/spectest/i32,287,364,8275
 cranelift/zkasm_data/spectest/i64,291,374,7353

From 2f5bc5585191ab03767a058a6f181b0bdd749cc9 Mon Sep 17 00:00:00 2001
From: Andrei Kashin <kashin.andrej@gmail.com>
Date: Tue, 6 Feb 2024 11:09:32 +0000
Subject: [PATCH 5/5] Fix bug due to operator ordering

The statement A + 3 > 8 seems to be parsed as A + (3 > 8) after the
translaction by zkAsm intrepreter, so adding parenthesis to disambiguate
this.
---
 cranelift/codegen/src/isa/zkasm/inst/emit.rs  |  2 +-
 .../sha256/generated/from_rust.zkasm          | 46 +++++++++----------
 cranelift/zkasm_data/generated/memory.zkasm   |  4 +-
 3 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/cranelift/codegen/src/isa/zkasm/inst/emit.rs b/cranelift/codegen/src/isa/zkasm/inst/emit.rs
index b99d1e2ff915..037f724f9db7 100644
--- a/cranelift/codegen/src/isa/zkasm/inst/emit.rs
+++ b/cranelift/codegen/src/isa/zkasm/inst/emit.rs
@@ -732,7 +732,7 @@ impl MachInstEmit for Inst {
 
                         // Handle the case when write spans two slots.
                         put_string(
-                            &format!("${{ (A + {width} > 8) ? (A + {width} - 8) : 0 }} => A\n"),
+                            &format!("${{ ((A + {width}) > 8) ? (A + {width} - 8) : 0 }} => A\n"),
                             sink,
                         );
                         put_string(
diff --git a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
index 3324c375b74c..3c90be2eab0a 100644
--- a/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
+++ b/cranelift/zkasm_data/benchmarks/sha256/generated/from_rust.zkasm
@@ -54,7 +54,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   16n => B  ;; LoadConst32
@@ -80,7 +80,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   8n => B  ;; LoadConst32
@@ -106,7 +106,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   50n => B  ;; LoadConst32
@@ -122,7 +122,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   58n => B  ;; LoadConst32
@@ -138,7 +138,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   66n => B  ;; LoadConst32
@@ -154,7 +154,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   74n => B  ;; LoadConst32
@@ -170,7 +170,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   82n => B  ;; LoadConst32
@@ -186,7 +186,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   88n => B  ;; LoadConst32
@@ -202,7 +202,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   1n => C  ;; LoadConst32
@@ -214,7 +214,7 @@ function_1:
   ${ C & ((1 << 8) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 8) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 1 > 8) ? (A + 1 - 8) : 0 } => A
+  ${ ((A + 1) > 8) ? (A + 1 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => C  ;; LoadConst64
@@ -224,7 +224,7 @@ function_1:
   ${ (E + 32) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => C  ;; LoadConst64
@@ -234,7 +234,7 @@ function_1:
   ${ (E + 42) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   32856n => C  ;; LoadConst32
@@ -245,7 +245,7 @@ function_1:
   ${ C & ((1 << 16) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 16) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 2 > 8) ? (A + 2 - 8) : 0 } => A
+  ${ ((A + 2) > 8) ? (A + 2 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => B  ;; LoadConst32
@@ -264,7 +264,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   96n => B  ;; LoadConst32
@@ -280,7 +280,7 @@ function_1:
   ${ (E) / 8 } => E
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 64) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 8 > 8) ? (A + 8 - 8) : 0 } => A
+  ${ ((A + 8) > 8) ? (A + 8 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   40n => B  ;; LoadConst32
@@ -27969,7 +27969,7 @@ label_2_7:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
@@ -27980,7 +27980,7 @@ label_2_7:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
@@ -27991,7 +27991,7 @@ label_2_7:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
@@ -28002,7 +28002,7 @@ label_2_7:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
@@ -28013,7 +28013,7 @@ label_2_7:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
@@ -28024,7 +28024,7 @@ label_2_7:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
@@ -28035,7 +28035,7 @@ label_2_7:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => A  ;; LoadConst32
@@ -28046,7 +28046,7 @@ label_2_7:
   ${ B & ((1 << 32) - 1) } => B
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (B << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (B & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   SP + 1182 => SP
diff --git a/cranelift/zkasm_data/generated/memory.zkasm b/cranelift/zkasm_data/generated/memory.zkasm
index f318101c67b6..0f85157eacd3 100644
--- a/cranelift/zkasm_data/generated/memory.zkasm
+++ b/cranelift/zkasm_data/generated/memory.zkasm
@@ -20,7 +20,7 @@ function_1:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   8n => B  ;; LoadConst32
@@ -32,7 +32,7 @@ function_1:
   ${ C & ((1 << 32) - 1) } => C
   $ => D :MLOAD(MEM:E)
   ${ (D & ~(((1 << 32) - 1) << (8 * A))) | (C << (8 * A)) } :MSTORE(MEM:E)
-  ${ (A + 4 > 8) ? (A + 4 - 8) : 0 } => A
+  ${ ((A + 4) > 8) ? (A + 4 - 8) : 0 } => A
   $ => D :MLOAD(MEM:E + 1)
   ${ (D & ~((1 << (8 * A)) - 1)) | (C & ((1 << (8 * A)) - 1)) } :MSTORE(MEM:E + 1)
   0n => B  ;; LoadConst32