From cd77cefb32fe1cab1d872fe2246dcb22382d8967 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 11:58:50 -0300
Subject: [PATCH 01/12] Support misaligned load/store in executor memory

---
 executor/src/vm/memory.rs | 123 ++++++++++++++++++++++++--------------
 1 file changed, 77 insertions(+), 46 deletions(-)

diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs
index c94376e76..47e0f6a28 100644
--- a/executor/src/vm/memory.rs
+++ b/executor/src/vm/memory.rs
@@ -81,77 +81,108 @@ impl Memory {
     }
 
     pub fn load_word(&self, address: u64) -> Result<u32, MemoryError> {
-        if !address.is_multiple_of(4) {
-            return Err(MemoryError::UnalignedAccess);
+        if address.is_multiple_of(4) {
+            let bytes = self.cells.get(&address).cloned().unwrap_or_default();
+            Ok(u32::from_le_bytes(bytes))
+        } else {
+            Ok(u32::from_le_bytes([
+                self.load_byte(address),
+                self.load_byte(address.wrapping_add(1)),
+                self.load_byte(address.wrapping_add(2)),
+                self.load_byte(address.wrapping_add(3)),
+            ]))
         }
-        let bytes = self.cells.get(&address).cloned().unwrap_or_default();
-        Ok(u32::from_le_bytes(bytes))
     }
 
     pub fn store_word(&mut self, address: u64, value: u32) -> Result<(), MemoryError> {
-        if !address.is_multiple_of(4) {
-            return Err(MemoryError::UnalignedAccess);
-        }
         let bytes = value.to_le_bytes();
-        self.cells.insert(address, bytes);
+        if address.is_multiple_of(4) {
+            self.cells.insert(address, bytes);
+        } else {
+            for (i, b) in bytes.iter().enumerate() {
+                self.store_byte(address.wrapping_add(i as u64), *b);
+            }
+        }
         Ok(())
     }
 
     /// Load a doubleword (64-bit) from memory - for LD instruction
     pub fn load_doubleword(&self, address: u64) -> Result<u64, MemoryError> {
-        if !address.is_multiple_of(8) {
-            return Err(MemoryError::UnalignedAccess);
+        if address.is_multiple_of(4) {
+            let low_bytes = self.cells.get(&address).cloned().unwrap_or_default();
+            let high_bytes = self
+                .cells
+                .get(&address.wrapping_add(4))
+                .cloned()
+                .unwrap_or_default();
+            let low = u32::from_le_bytes(low_bytes) as u64;
+            let high = u32::from_le_bytes(high_bytes) as u64;
+            Ok(low | (high << 32))
+        } else {
+            let mut bytes = [0u8; 8];
+            for (i, b) in bytes.iter_mut().enumerate() {
+                *b = self.load_byte(address.wrapping_add(i as u64));
+            }
+            Ok(u64::from_le_bytes(bytes))
         }
-        let low_bytes = self.cells.get(&address).cloned().unwrap_or_default();
-        let high_bytes = self.cells.get(&(address + 4)).cloned().unwrap_or_default();
-        let low = u32::from_le_bytes(low_bytes) as u64;
-        let high = u32::from_le_bytes(high_bytes) as u64;
-        Ok(low | (high << 32))
     }
 
     /// Store a doubleword (64-bit) to memory - for SD instruction
     pub fn store_doubleword(&mut self, address: u64, value: u64) -> Result<(), MemoryError> {
-        if !address.is_multiple_of(8) {
-            return Err(MemoryError::UnalignedAccess);
+        if address.is_multiple_of(4) {
+            let low = (value & 0xFFFFFFFF) as u32;
+            let high = (value >> 32) as u32;
+            self.cells.insert(address, low.to_le_bytes());
+            self.cells
+                .insert(address.wrapping_add(4), high.to_le_bytes());
+        } else {
+            let bytes = value.to_le_bytes();
+            for (i, b) in bytes.iter().enumerate() {
+                self.store_byte(address.wrapping_add(i as u64), *b);
+            }
         }
-        let low = (value & 0xFFFFFFFF) as u32;
-        let high = (value >> 32) as u32;
-        self.cells.insert(address, low.to_le_bytes());
-        self.cells.insert(address + 4, high.to_le_bytes());
         Ok(())
     }
 
     pub fn load_half(&self, address: u64) -> Result<u16, MemoryError> {
-        if !address.is_multiple_of(2) {
-            unimplemented!(
-                "Unaligned load half memory access at address 0x{:016x}",
-                address
-            );
+        // A halfword fits in a single 4-byte cell when the byte offset is 0, 1,
+        // or 2. Offset 3 straddles into the next cell.
+        if address % 4 <= 2 {
+            let aligned_address = address - address % 4;
+            let bytes = self
+                .cells
+                .get(&aligned_address)
+                .cloned()
+                .unwrap_or_default();
+            let offset = (address % 4) as usize;
+            Ok(u16::from_le_bytes(
+                bytes[offset..offset + 2]
+                    .try_into()
+                    .map_err(|_| MemoryError::LoadHalf)?,
+            ))
+        } else {
+            Ok(u16::from_le_bytes([
+                self.load_byte(address),
+                self.load_byte(address.wrapping_add(1)),
+            ]))
         }
-        let aligned_address = address - address % 4;
-        let bytes = self
-            .cells
-            .get(&aligned_address)
-            .cloned()
-            .unwrap_or_default();
-        let value = &bytes[(address % 4) as usize..(address % 4) as usize + 2];
-        Ok(u16::from_le_bytes(
-            value.try_into().map_err(|_| MemoryError::LoadHalf)?,
-        ))
     }
 
     pub fn store_half(&mut self, address: u64, value: u16) -> Result<(), MemoryError> {
-        if !address.is_multiple_of(2) {
-            return Err(MemoryError::UnalignedAccess);
-        }
-        let aligned_address = address - address % 4;
-        let entry = self
-            .cells
-            .entry(aligned_address)
-            .or_insert_with(|| [0, 0, 0, 0]);
         let bytes = value.to_le_bytes();
-        entry[(address % 4) as usize] = bytes[0];
-        entry[(address % 4) as usize + 1] = bytes[1];
+        if address % 4 <= 2 {
+            let aligned_address = address - address % 4;
+            let entry = self
+                .cells
+                .entry(aligned_address)
+                .or_insert_with(|| [0, 0, 0, 0]);
+            let offset = (address % 4) as usize;
+            entry[offset] = bytes[0];
+            entry[offset + 1] = bytes[1];
+        } else {
+            self.store_byte(address, bytes[0]);
+            self.store_byte(address.wrapping_add(1), bytes[1]);
+        }
         Ok(())
     }
 

From a988fbeb6c24f6b3313c432161cf30187e0d7792 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 12:23:23 -0300
Subject: [PATCH 02/12] Add misaligned load/store regression tests

---
 executor/programs/asm/misalign_ld.s  | 16 +++++
 executor/programs/asm/misalign_lh.s  | 14 +++++
 executor/programs/asm/misalign_lhu.s | 14 +++++
 executor/programs/asm/misalign_lw.s  | 14 +++++
 executor/programs/asm/misalign_lwu.s | 14 +++++
 executor/programs/asm/misalign_sd.s  | 11 ++++
 executor/programs/asm/misalign_sh.s  | 11 ++++
 executor/programs/asm/misalign_sw.s  | 11 ++++
 executor/tests/asm.rs                | 41 ++++++++++++-
 prover/src/tests/prove_elfs_tests.rs | 91 ++++++++++++++++++++++++++++
 10 files changed, 236 insertions(+), 1 deletion(-)
 create mode 100644 executor/programs/asm/misalign_ld.s
 create mode 100644 executor/programs/asm/misalign_lh.s
 create mode 100644 executor/programs/asm/misalign_lhu.s
 create mode 100644 executor/programs/asm/misalign_lw.s
 create mode 100644 executor/programs/asm/misalign_lwu.s
 create mode 100644 executor/programs/asm/misalign_sd.s
 create mode 100644 executor/programs/asm/misalign_sh.s
 create mode 100644 executor/programs/asm/misalign_sw.s

diff --git a/executor/programs/asm/misalign_ld.s b/executor/programs/asm/misalign_ld.s
new file mode 100644
index 000000000..889ca9841
--- /dev/null
+++ b/executor/programs/asm/misalign_ld.s
@@ -0,0 +1,16 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Misaligned LD at offset 1 from a 4-aligned base.
+	# Access reads bytes [33..40], crossing three 4-byte cells.
+	li	t0, 32
+	li	t1, 0x80FF1234
+	sw	t1, 0(t0)
+	li	t1, 0xDEADBEEF
+	sw	t1, 4(t0)
+	li	t1, 0x000000AA
+	sw	t1, 8(t0)
+	ld	a0, 1(t0)
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_lh.s b/executor/programs/asm/misalign_lh.s
new file mode 100644
index 000000000..f45c88107
--- /dev/null
+++ b/executor/programs/asm/misalign_lh.s
@@ -0,0 +1,14 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Misaligned LH at offset 3 from a 4-aligned base.
+	# Access reads bytes [35, 36], crossing two 4-byte cells.
+	li	t0, 32
+	li	t1, 0x3412FF80
+	sw	t1, 0(t0)
+	li	t1, 0x000000AA
+	sw	t1, 4(t0)
+	lh	a0, 3(t0)
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_lhu.s b/executor/programs/asm/misalign_lhu.s
new file mode 100644
index 000000000..eaabc0621
--- /dev/null
+++ b/executor/programs/asm/misalign_lhu.s
@@ -0,0 +1,14 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Misaligned LHU at offset 3 from a 4-aligned base.
+	# Access reads bytes [35, 36], crossing two 4-byte cells.
+	li	t0, 32
+	li	t1, 0x3412FF80
+	sw	t1, 0(t0)
+	li	t1, 0x000000AA
+	sw	t1, 4(t0)
+	lhu	a0, 3(t0)
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_lw.s b/executor/programs/asm/misalign_lw.s
new file mode 100644
index 000000000..673523ee4
--- /dev/null
+++ b/executor/programs/asm/misalign_lw.s
@@ -0,0 +1,14 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Misaligned LW at offset 1 from a 4-aligned base.
+	# Access reads bytes [33, 34, 35, 36], crossing two 4-byte cells.
+	li	t0, 32
+	li	t1, 0x80FF1234
+	sw	t1, 0(t0)
+	li	t1, 0x000000AA
+	sw	t1, 4(t0)
+	lw	a0, 1(t0)
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_lwu.s b/executor/programs/asm/misalign_lwu.s
new file mode 100644
index 000000000..95ad92b60
--- /dev/null
+++ b/executor/programs/asm/misalign_lwu.s
@@ -0,0 +1,14 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Misaligned LWU at offset 1 from a 4-aligned base.
+	# Access reads bytes [33, 34, 35, 36], crossing two 4-byte cells.
+	li	t0, 32
+	li	t1, 0x80FF1234
+	sw	t1, 0(t0)
+	li	t1, 0x000000AA
+	sw	t1, 4(t0)
+	lwu	a0, 1(t0)
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_sd.s b/executor/programs/asm/misalign_sd.s
new file mode 100644
index 000000000..35d45acbd
--- /dev/null
+++ b/executor/programs/asm/misalign_sd.s
@@ -0,0 +1,11 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Misaligned SD at offset 1 from a 4-aligned base.
+	# Writes bytes to addresses [65..72], crossing three 4-byte cells.
+	li	t0, 64
+	li	t1, 0x123456789ABCDEF0
+	sd	t1, 1(t0)
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_sh.s b/executor/programs/asm/misalign_sh.s
new file mode 100644
index 000000000..cdfdfd112
--- /dev/null
+++ b/executor/programs/asm/misalign_sh.s
@@ -0,0 +1,11 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Misaligned SH at offset 3 from a 4-aligned base.
+	# Writes bytes to addresses [67, 68], crossing two 4-byte cells.
+	li	t0, 64
+	li	t1, 0xAA12
+	sh	t1, 3(t0)
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_sw.s b/executor/programs/asm/misalign_sw.s
new file mode 100644
index 000000000..d8d0fee81
--- /dev/null
+++ b/executor/programs/asm/misalign_sw.s
@@ -0,0 +1,11 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Misaligned SW at offset 1 from a 4-aligned base.
+	# Writes bytes to addresses [65..68], crossing two 4-byte cells.
+	li	t0, 64
+	li	t1, 0xDEADBEEF
+	sw	t1, 1(t0)
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/tests/asm.rs b/executor/tests/asm.rs
index 86722b82c..4b3c8fbcc 100644
--- a/executor/tests/asm.rs
+++ b/executor/tests/asm.rs
@@ -424,12 +424,51 @@ fn test_lw_sw_offset() {
     run_program("./program_artifacts/asm/lw_sw_offset.elf");
 }
 
-#[ignore = "Unaligned memory access not properly implemented yet"]
 #[test]
 fn test_lw_sw_offset_odd() {
     run_program("./program_artifacts/asm/lw_sw_offset_odd.elf");
 }
 
+#[test]
+fn test_misalign_lh() {
+    run_program("./program_artifacts/asm/misalign_lh.elf");
+}
+
+#[test]
+fn test_misalign_lhu() {
+    run_program("./program_artifacts/asm/misalign_lhu.elf");
+}
+
+#[test]
+fn test_misalign_lw() {
+    run_program("./program_artifacts/asm/misalign_lw.elf");
+}
+
+#[test]
+fn test_misalign_lwu() {
+    run_program("./program_artifacts/asm/misalign_lwu.elf");
+}
+
+#[test]
+fn test_misalign_ld() {
+    run_program("./program_artifacts/asm/misalign_ld.elf");
+}
+
+#[test]
+fn test_misalign_sh() {
+    run_program("./program_artifacts/asm/misalign_sh.elf");
+}
+
+#[test]
+fn test_misalign_sw() {
+    run_program("./program_artifacts/asm/misalign_sw.elf");
+}
+
+#[test]
+fn test_misalign_sd() {
+    run_program("./program_artifacts/asm/misalign_sd.elf");
+}
+
 #[test]
 fn test_auipc() {
     run_program("./program_artifacts/asm/auipc.elf");
diff --git a/prover/src/tests/prove_elfs_tests.rs b/prover/src/tests/prove_elfs_tests.rs
index fe97911b9..1fec514c2 100644
--- a/prover/src/tests/prove_elfs_tests.rs
+++ b/prover/src/tests/prove_elfs_tests.rs
@@ -498,6 +498,97 @@ fn test_prove_elfs_sign_ext_edge_cases_8() {
     );
 }
 
+// Misaligned load/store regression tests. Each program issues one load or
+// store whose effective address is not naturally aligned to the access width,
+// crossing one or more 4-byte cell boundaries in the executor's memory map.
+#[test]
+fn test_prove_elfs_misalign_lh() {
+    let (elf, logs, _instructions) = run_asm_elf("misalign_lh");
+    let mut traces =
+        Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
+    assert!(
+        prove_and_verify_vm_minimal(&elf, &mut traces),
+        "misalign_lh failed"
+    );
+}
+
+#[test]
+fn test_prove_elfs_misalign_lhu() {
+    let (elf, logs, _instructions) = run_asm_elf("misalign_lhu");
+    let mut traces =
+        Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
+    assert!(
+        prove_and_verify_vm_minimal(&elf, &mut traces),
+        "misalign_lhu failed"
+    );
+}
+
+#[test]
+fn test_prove_elfs_misalign_lw() {
+    let (elf, logs, _instructions) = run_asm_elf("misalign_lw");
+    let mut traces =
+        Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
+    assert!(
+        prove_and_verify_vm_minimal(&elf, &mut traces),
+        "misalign_lw failed"
+    );
+}
+
+#[test]
+fn test_prove_elfs_misalign_lwu() {
+    let (elf, logs, _instructions) = run_asm_elf("misalign_lwu");
+    let mut traces =
+        Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
+    assert!(
+        prove_and_verify_vm_minimal(&elf, &mut traces),
+        "misalign_lwu failed"
+    );
+}
+
+#[test]
+fn test_prove_elfs_misalign_ld() {
+    let (elf, logs, _instructions) = run_asm_elf("misalign_ld");
+    let mut traces =
+        Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
+    assert!(
+        prove_and_verify_vm_minimal(&elf, &mut traces),
+        "misalign_ld failed"
+    );
+}
+
+#[test]
+fn test_prove_elfs_misalign_sh() {
+    let (elf, logs, _instructions) = run_asm_elf("misalign_sh");
+    let mut traces =
+        Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
+    assert!(
+        prove_and_verify_vm_minimal(&elf, &mut traces),
+        "misalign_sh failed"
+    );
+}
+
+#[test]
+fn test_prove_elfs_misalign_sw() {
+    let (elf, logs, _instructions) = run_asm_elf("misalign_sw");
+    let mut traces =
+        Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
+    assert!(
+        prove_and_verify_vm_minimal(&elf, &mut traces),
+        "misalign_sw failed"
+    );
+}
+
+#[test]
+fn test_prove_elfs_misalign_sd() {
+    let (elf, logs, _instructions) = run_asm_elf("misalign_sd");
+    let mut traces =
+        Traces::from_elf_and_logs_minimal(&elf, &logs, &Default::default(), &[]).unwrap();
+    assert!(
+        prove_and_verify_vm_minimal(&elf, &mut traces),
+        "misalign_sd failed"
+    );
+}
+
 #[test]
 fn test_prove_elfs_test_shift_8() {
     let (elf, logs, instructions) = run_asm_elf("test_shift_8");

From fe1e1b5c418a985d16578158b00049ab867dbb80 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 16:15:52 -0300
Subject: [PATCH 03/12] Tighten misalign asm test comments

---
 executor/programs/asm/misalign_ld.s  | 3 +--
 executor/programs/asm/misalign_lh.s  | 3 +--
 executor/programs/asm/misalign_lhu.s | 3 +--
 executor/programs/asm/misalign_lw.s  | 3 +--
 executor/programs/asm/misalign_lwu.s | 3 +--
 executor/programs/asm/misalign_sd.s  | 3 +--
 executor/programs/asm/misalign_sh.s  | 3 +--
 executor/programs/asm/misalign_sw.s  | 3 +--
 8 files changed, 8 insertions(+), 16 deletions(-)

diff --git a/executor/programs/asm/misalign_ld.s b/executor/programs/asm/misalign_ld.s
index 889ca9841..4e0048622 100644
--- a/executor/programs/asm/misalign_ld.s
+++ b/executor/programs/asm/misalign_ld.s
@@ -1,8 +1,7 @@
 	.attribute	5, "rv64i2p1_m2p0"
 	.globl	main
 main:
-	# Misaligned LD at offset 1 from a 4-aligned base.
-	# Access reads bytes [33..40], crossing three 4-byte cells.
+	# Misaligned LD: 8-byte load at address 33.
 	li	t0, 32
 	li	t1, 0x80FF1234
 	sw	t1, 0(t0)
diff --git a/executor/programs/asm/misalign_lh.s b/executor/programs/asm/misalign_lh.s
index f45c88107..d48b88b34 100644
--- a/executor/programs/asm/misalign_lh.s
+++ b/executor/programs/asm/misalign_lh.s
@@ -1,8 +1,7 @@
 	.attribute	5, "rv64i2p1_m2p0"
 	.globl	main
 main:
-	# Misaligned LH at offset 3 from a 4-aligned base.
-	# Access reads bytes [35, 36], crossing two 4-byte cells.
+	# Misaligned LH: 2-byte load at address 35.
 	li	t0, 32
 	li	t1, 0x3412FF80
 	sw	t1, 0(t0)
diff --git a/executor/programs/asm/misalign_lhu.s b/executor/programs/asm/misalign_lhu.s
index eaabc0621..cacf04217 100644
--- a/executor/programs/asm/misalign_lhu.s
+++ b/executor/programs/asm/misalign_lhu.s
@@ -1,8 +1,7 @@
 	.attribute	5, "rv64i2p1_m2p0"
 	.globl	main
 main:
-	# Misaligned LHU at offset 3 from a 4-aligned base.
-	# Access reads bytes [35, 36], crossing two 4-byte cells.
+	# Misaligned LHU: 2-byte load at address 35.
 	li	t0, 32
 	li	t1, 0x3412FF80
 	sw	t1, 0(t0)
diff --git a/executor/programs/asm/misalign_lw.s b/executor/programs/asm/misalign_lw.s
index 673523ee4..73dde03e3 100644
--- a/executor/programs/asm/misalign_lw.s
+++ b/executor/programs/asm/misalign_lw.s
@@ -1,8 +1,7 @@
 	.attribute	5, "rv64i2p1_m2p0"
 	.globl	main
 main:
-	# Misaligned LW at offset 1 from a 4-aligned base.
-	# Access reads bytes [33, 34, 35, 36], crossing two 4-byte cells.
+	# Misaligned LW: 4-byte load at address 33.
 	li	t0, 32
 	li	t1, 0x80FF1234
 	sw	t1, 0(t0)
diff --git a/executor/programs/asm/misalign_lwu.s b/executor/programs/asm/misalign_lwu.s
index 95ad92b60..9256ec0e4 100644
--- a/executor/programs/asm/misalign_lwu.s
+++ b/executor/programs/asm/misalign_lwu.s
@@ -1,8 +1,7 @@
 	.attribute	5, "rv64i2p1_m2p0"
 	.globl	main
 main:
-	# Misaligned LWU at offset 1 from a 4-aligned base.
-	# Access reads bytes [33, 34, 35, 36], crossing two 4-byte cells.
+	# Misaligned LWU: 4-byte load at address 33.
 	li	t0, 32
 	li	t1, 0x80FF1234
 	sw	t1, 0(t0)
diff --git a/executor/programs/asm/misalign_sd.s b/executor/programs/asm/misalign_sd.s
index 35d45acbd..e28b5d7fd 100644
--- a/executor/programs/asm/misalign_sd.s
+++ b/executor/programs/asm/misalign_sd.s
@@ -1,8 +1,7 @@
 	.attribute	5, "rv64i2p1_m2p0"
 	.globl	main
 main:
-	# Misaligned SD at offset 1 from a 4-aligned base.
-	# Writes bytes to addresses [65..72], crossing three 4-byte cells.
+	# Misaligned SD: 8-byte store at address 65.
 	li	t0, 64
 	li	t1, 0x123456789ABCDEF0
 	sd	t1, 1(t0)
diff --git a/executor/programs/asm/misalign_sh.s b/executor/programs/asm/misalign_sh.s
index cdfdfd112..533c8d1ec 100644
--- a/executor/programs/asm/misalign_sh.s
+++ b/executor/programs/asm/misalign_sh.s
@@ -1,8 +1,7 @@
 	.attribute	5, "rv64i2p1_m2p0"
 	.globl	main
 main:
-	# Misaligned SH at offset 3 from a 4-aligned base.
-	# Writes bytes to addresses [67, 68], crossing two 4-byte cells.
+	# Misaligned SH: 2-byte store at address 67.
 	li	t0, 64
 	li	t1, 0xAA12
 	sh	t1, 3(t0)
diff --git a/executor/programs/asm/misalign_sw.s b/executor/programs/asm/misalign_sw.s
index d8d0fee81..88c769702 100644
--- a/executor/programs/asm/misalign_sw.s
+++ b/executor/programs/asm/misalign_sw.s
@@ -1,8 +1,7 @@
 	.attribute	5, "rv64i2p1_m2p0"
 	.globl	main
 main:
-	# Misaligned SW at offset 1 from a 4-aligned base.
-	# Writes bytes to addresses [65..68], crossing two 4-byte cells.
+	# Misaligned SW: 4-byte store at address 65.
 	li	t0, 64
 	li	t1, 0xDEADBEEF
 	sw	t1, 1(t0)

From 821137a0e553831586804985a31960cbc3af7ada Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 16:21:38 -0300
Subject: [PATCH 04/12] Drop single-cell fast path from load_half/store_half

---
 executor/src/vm/memory.rs | 42 ++++++---------------------------------
 1 file changed, 6 insertions(+), 36 deletions(-)

diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs
index 47e0f6a28..b8fc7c23d 100644
--- a/executor/src/vm/memory.rs
+++ b/executor/src/vm/memory.rs
@@ -145,44 +145,16 @@ impl Memory {
     }
 
     pub fn load_half(&self, address: u64) -> Result<u16, MemoryError> {
-        // A halfword fits in a single 4-byte cell when the byte offset is 0, 1,
-        // or 2. Offset 3 straddles into the next cell.
-        if address % 4 <= 2 {
-            let aligned_address = address - address % 4;
-            let bytes = self
-                .cells
-                .get(&aligned_address)
-                .cloned()
-                .unwrap_or_default();
-            let offset = (address % 4) as usize;
-            Ok(u16::from_le_bytes(
-                bytes[offset..offset + 2]
-                    .try_into()
-                    .map_err(|_| MemoryError::LoadHalf)?,
-            ))
-        } else {
-            Ok(u16::from_le_bytes([
-                self.load_byte(address),
-                self.load_byte(address.wrapping_add(1)),
-            ]))
-        }
+        Ok(u16::from_le_bytes([
+            self.load_byte(address),
+            self.load_byte(address.wrapping_add(1)),
+        ]))
     }
 
     pub fn store_half(&mut self, address: u64, value: u16) -> Result<(), MemoryError> {
         let bytes = value.to_le_bytes();
-        if address % 4 <= 2 {
-            let aligned_address = address - address % 4;
-            let entry = self
-                .cells
-                .entry(aligned_address)
-                .or_insert_with(|| [0, 0, 0, 0]);
-            let offset = (address % 4) as usize;
-            entry[offset] = bytes[0];
-            entry[offset + 1] = bytes[1];
-        } else {
-            self.store_byte(address, bytes[0]);
-            self.store_byte(address.wrapping_add(1), bytes[1]);
-        }
+        self.store_byte(address, bytes[0]);
+        self.store_byte(address.wrapping_add(1), bytes[1]);
         Ok(())
     }
 
@@ -264,8 +236,6 @@ impl Memory {
 
 #[derive(thiserror::Error, Debug)]
 pub enum MemoryError {
-    #[error("Failed to convert bytes to u16")]
-    LoadHalf,
     #[error("Unaligned memory access")]
     UnalignedAccess,
     #[error("Public output commit size exceeded")]

From 74922ff7bfb7600f8f3815b31921ca32e47012c7 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 16:42:05 -0300
Subject: [PATCH 05/12] Trap misaligned PC in instruction fetch

---
 executor/programs/asm/misaligned_pc.s |  8 ++++++++
 executor/src/vm/execution.rs          |  5 +++++
 executor/tests/asm.rs                 | 24 +++++++++++++++++++++++-
 3 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 executor/programs/asm/misaligned_pc.s

diff --git a/executor/programs/asm/misaligned_pc.s b/executor/programs/asm/misaligned_pc.s
new file mode 100644
index 000000000..832f27678
--- /dev/null
+++ b/executor/programs/asm/misaligned_pc.s
@@ -0,0 +1,8 @@
+	.attribute	5, "rv64i2p1_m2p0"
+	.globl	main
+main:
+	# Jump to PC = 2 (not 4-aligned).
+	jalr	zero, zero, 2
+	li	a0, 0
+	li	a7, 93
+	ecall
diff --git a/executor/src/vm/execution.rs b/executor/src/vm/execution.rs
index 37dcf0198..614aad649 100644
--- a/executor/src/vm/execution.rs
+++ b/executor/src/vm/execution.rs
@@ -64,6 +64,9 @@ impl Executor {
         self.logs.clear();
 
         while self.pc != 0 && self.logs.len() < CHUNK_SIZE {
+            if !self.pc.is_multiple_of(4) {
+                return Err(ExecutorError::InstructionAddressMisaligned(self.pc));
+            }
             let instruction = match self.instructions.get(self.pc) {
                 Some(&instr) => instr,
                 None => {
@@ -252,4 +255,6 @@ pub enum ExecutorError {
     ExecutionError(#[from] ExecutionError),
     #[error("Memory error: {0}")]
     MemoryError(#[from] MemoryError),
+    #[error("Instruction address misaligned: {0:#018x}")]
+    InstructionAddressMisaligned(u64),
 }
diff --git a/executor/tests/asm.rs b/executor/tests/asm.rs
index 4b3c8fbcc..f19241a6a 100644
--- a/executor/tests/asm.rs
+++ b/executor/tests/asm.rs
@@ -1,4 +1,7 @@
-use executor::{elf::Elf, vm::execution::Executor};
+use executor::{
+    elf::Elf,
+    vm::execution::{Executor, ExecutorError},
+};
 
 /// Run a program and verify it exits successfully (exit code 0).
 ///
@@ -469,6 +472,25 @@ fn test_misalign_sd() {
     run_program("./program_artifacts/asm/misalign_sd.elf");
 }
 
+#[test]
+fn test_misaligned_pc_traps() {
+    let elf_data = std::fs::read("./program_artifacts/asm/misaligned_pc.elf").unwrap();
+    let program = Elf::load(&elf_data).unwrap();
+    let mut executor = Executor::new(&program, vec![]).expect("Failed to create executor");
+    let err = loop {
+        match executor.resume() {
+            Ok(Some(_)) => continue,
+            Ok(None) => panic!("expected misaligned PC trap, program halted normally"),
+            Err(e) => break e,
+        }
+    };
+    assert!(
+        matches!(err, ExecutorError::InstructionAddressMisaligned(2)),
+        "expected InstructionAddressMisaligned(2), got {:?}",
+        err
+    );
+}
+
 #[test]
 fn test_auipc() {
     run_program("./program_artifacts/asm/auipc.elf");

From a6e15d87f651ee0f4d3270df51f7530109d755b1 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 17:03:50 -0300
Subject: [PATCH 06/12] Verify loaded value in misalign load tests

---
 executor/programs/asm/misalign_ld.s  | 6 ++++++
 executor/programs/asm/misalign_lh.s  | 6 ++++++
 executor/programs/asm/misalign_lhu.s | 6 ++++++
 executor/programs/asm/misalign_lw.s  | 6 ++++++
 executor/programs/asm/misalign_lwu.s | 6 ++++++
 5 files changed, 30 insertions(+)

diff --git a/executor/programs/asm/misalign_ld.s b/executor/programs/asm/misalign_ld.s
index 4e0048622..9572db15e 100644
--- a/executor/programs/asm/misalign_ld.s
+++ b/executor/programs/asm/misalign_ld.s
@@ -10,6 +10,12 @@ main:
 	li	t1, 0x000000AA
 	sw	t1, 8(t0)
 	ld	a0, 1(t0)
+	li	t2, 0xAADEADBEEF80FF12
+	bne	a0, t2, .Lfail
 	li	a0, 0
 	li	a7, 93
 	ecall
+.Lfail:
+	li	a0, 1
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_lh.s b/executor/programs/asm/misalign_lh.s
index d48b88b34..08cff504e 100644
--- a/executor/programs/asm/misalign_lh.s
+++ b/executor/programs/asm/misalign_lh.s
@@ -8,6 +8,12 @@ main:
 	li	t1, 0x000000AA
 	sw	t1, 4(t0)
 	lh	a0, 3(t0)
+	li	t2, 0xFFFFFFFFFFFFAA34
+	bne	a0, t2, .Lfail
 	li	a0, 0
 	li	a7, 93
 	ecall
+.Lfail:
+	li	a0, 1
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_lhu.s b/executor/programs/asm/misalign_lhu.s
index cacf04217..9a9aed7a1 100644
--- a/executor/programs/asm/misalign_lhu.s
+++ b/executor/programs/asm/misalign_lhu.s
@@ -8,6 +8,12 @@ main:
 	li	t1, 0x000000AA
 	sw	t1, 4(t0)
 	lhu	a0, 3(t0)
+	li	t2, 0xAA34
+	bne	a0, t2, .Lfail
 	li	a0, 0
 	li	a7, 93
 	ecall
+.Lfail:
+	li	a0, 1
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_lw.s b/executor/programs/asm/misalign_lw.s
index 73dde03e3..246c955b3 100644
--- a/executor/programs/asm/misalign_lw.s
+++ b/executor/programs/asm/misalign_lw.s
@@ -8,6 +8,12 @@ main:
 	li	t1, 0x000000AA
 	sw	t1, 4(t0)
 	lw	a0, 1(t0)
+	li	t2, 0xFFFFFFFFAA80FF12
+	bne	a0, t2, .Lfail
 	li	a0, 0
 	li	a7, 93
 	ecall
+.Lfail:
+	li	a0, 1
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_lwu.s b/executor/programs/asm/misalign_lwu.s
index 9256ec0e4..f990d8cdb 100644
--- a/executor/programs/asm/misalign_lwu.s
+++ b/executor/programs/asm/misalign_lwu.s
@@ -8,6 +8,12 @@ main:
 	li	t1, 0x000000AA
 	sw	t1, 4(t0)
 	lwu	a0, 1(t0)
+	li	t2, 0xAA80FF12
+	bne	a0, t2, .Lfail
 	li	a0, 0
 	li	a7, 93
 	ecall
+.Lfail:
+	li	a0, 1
+	li	a7, 93
+	ecall

From 210bbd78a97be40baf19346a9f22fdff0f4a1549 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 17:04:03 -0300
Subject: [PATCH 07/12] Restore load_half/store_half fast paths

---
 executor/src/vm/memory.rs | 36 ++++++++++++++++++++++++++++++------
 1 file changed, 30 insertions(+), 6 deletions(-)

diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs
index b8fc7c23d..a42d589e8 100644
--- a/executor/src/vm/memory.rs
+++ b/executor/src/vm/memory.rs
@@ -145,16 +145,40 @@ impl Memory {
     }
 
     pub fn load_half(&self, address: u64) -> Result<u16, MemoryError> {
-        Ok(u16::from_le_bytes([
-            self.load_byte(address),
-            self.load_byte(address.wrapping_add(1)),
-        ]))
+        if address % 4 <= 2 {
+            let aligned_address = address - address % 4;
+            let bytes = self
+                .cells
+                .get(&aligned_address)
+                .cloned()
+                .unwrap_or_default();
+            let offset = (address % 4) as usize;
+            Ok(u16::from_le_bytes(
+                bytes[offset..offset + 2].try_into().unwrap(),
+            ))
+        } else {
+            Ok(u16::from_le_bytes([
+                self.load_byte(address),
+                self.load_byte(address.wrapping_add(1)),
+            ]))
+        }
     }
 
     pub fn store_half(&mut self, address: u64, value: u16) -> Result<(), MemoryError> {
         let bytes = value.to_le_bytes();
-        self.store_byte(address, bytes[0]);
-        self.store_byte(address.wrapping_add(1), bytes[1]);
+        if address % 4 <= 2 {
+            let aligned_address = address - address % 4;
+            let entry = self
+                .cells
+                .entry(aligned_address)
+                .or_insert_with(|| [0, 0, 0, 0]);
+            let offset = (address % 4) as usize;
+            entry[offset] = bytes[0];
+            entry[offset + 1] = bytes[1];
+        } else {
+            self.store_byte(address, bytes[0]);
+            self.store_byte(address.wrapping_add(1), bytes[1]);
+        }
         Ok(())
     }
 

From 6bac80bd35c57a16b7d57aef4da6d52f31acf465 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 17:13:27 -0300
Subject: [PATCH 08/12] Use natural alignment in load/store fast paths

---
 executor/src/vm/memory.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs
index a42d589e8..8c137a91e 100644
--- a/executor/src/vm/memory.rs
+++ b/executor/src/vm/memory.rs
@@ -108,7 +108,7 @@ impl Memory {
 
     /// Load a doubleword (64-bit) from memory - for LD instruction
     pub fn load_doubleword(&self, address: u64) -> Result<u64, MemoryError> {
-        if address.is_multiple_of(4) {
+        if address.is_multiple_of(8) {
             let low_bytes = self.cells.get(&address).cloned().unwrap_or_default();
             let high_bytes = self
                 .cells
@@ -129,7 +129,7 @@ impl Memory {
 
     /// Store a doubleword (64-bit) to memory - for SD instruction
     pub fn store_doubleword(&mut self, address: u64, value: u64) -> Result<(), MemoryError> {
-        if address.is_multiple_of(4) {
+        if address.is_multiple_of(8) {
             let low = (value & 0xFFFFFFFF) as u32;
             let high = (value >> 32) as u32;
             self.cells.insert(address, low.to_le_bytes());
@@ -145,7 +145,7 @@ impl Memory {
     }
 
     pub fn load_half(&self, address: u64) -> Result<u16, MemoryError> {
-        if address % 4 <= 2 {
+        if address.is_multiple_of(2) {
             let aligned_address = address - address % 4;
             let bytes = self
                 .cells
@@ -166,7 +166,7 @@ impl Memory {
 
     pub fn store_half(&mut self, address: u64, value: u16) -> Result<(), MemoryError> {
         let bytes = value.to_le_bytes();
-        if address % 4 <= 2 {
+        if address.is_multiple_of(2) {
             let aligned_address = address - address % 4;
             let entry = self
                 .cells

From 5f0ad40089a6631dcf2253deaa8b5ca441cedd54 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 19:07:31 -0300
Subject: [PATCH 09/12] Drop infallible .unwrap() in load_half fast path

---
 executor/src/vm/memory.rs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs
index 8c137a91e..92b87eda4 100644
--- a/executor/src/vm/memory.rs
+++ b/executor/src/vm/memory.rs
@@ -153,9 +153,7 @@ impl Memory {
                 .cloned()
                 .unwrap_or_default();
             let offset = (address % 4) as usize;
-            Ok(u16::from_le_bytes(
-                bytes[offset..offset + 2].try_into().unwrap(),
-            ))
+            Ok(u16::from_le_bytes([bytes[offset], bytes[offset + 1]]))
         } else {
             Ok(u16::from_le_bytes([
                 self.load_byte(address),

From 95ca239bcf67dbc06ecdd8dd1b06fd59f144a40d Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 19:07:39 -0300
Subject: [PATCH 10/12] Verify stored bytes in misalign store tests

---
 executor/programs/asm/misalign_sd.s | 13 +++++++++++++
 executor/programs/asm/misalign_sh.s | 10 ++++++++++
 executor/programs/asm/misalign_sw.s | 10 ++++++++++
 3 files changed, 33 insertions(+)

diff --git a/executor/programs/asm/misalign_sd.s b/executor/programs/asm/misalign_sd.s
index e28b5d7fd..159af7032 100644
--- a/executor/programs/asm/misalign_sd.s
+++ b/executor/programs/asm/misalign_sd.s
@@ -5,6 +5,19 @@ main:
 	li	t0, 64
 	li	t1, 0x123456789ABCDEF0
 	sd	t1, 1(t0)
+	lwu	a1, 0(t0)
+	li	t2, 0xBCDEF000
+	bne	a1, t2, .Lfail
+	lwu	a1, 4(t0)
+	li	t2, 0x3456789A
+	bne	a1, t2, .Lfail
+	lwu	a1, 8(t0)
+	li	t2, 0x00000012
+	bne	a1, t2, .Lfail
 	li	a0, 0
 	li	a7, 93
 	ecall
+.Lfail:
+	li	a0, 1
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_sh.s b/executor/programs/asm/misalign_sh.s
index 533c8d1ec..4769869ac 100644
--- a/executor/programs/asm/misalign_sh.s
+++ b/executor/programs/asm/misalign_sh.s
@@ -5,6 +5,16 @@ main:
 	li	t0, 64
 	li	t1, 0xAA12
 	sh	t1, 3(t0)
+	lwu	a1, 0(t0)
+	li	t2, 0x12000000
+	bne	a1, t2, .Lfail
+	lwu	a1, 4(t0)
+	li	t2, 0x000000AA
+	bne	a1, t2, .Lfail
 	li	a0, 0
 	li	a7, 93
 	ecall
+.Lfail:
+	li	a0, 1
+	li	a7, 93
+	ecall
diff --git a/executor/programs/asm/misalign_sw.s b/executor/programs/asm/misalign_sw.s
index 88c769702..124a8cee8 100644
--- a/executor/programs/asm/misalign_sw.s
+++ b/executor/programs/asm/misalign_sw.s
@@ -5,6 +5,16 @@ main:
 	li	t0, 64
 	li	t1, 0xDEADBEEF
 	sw	t1, 1(t0)
+	lwu	a1, 0(t0)
+	li	t2, 0xADBEEF00
+	bne	a1, t2, .Lfail
+	lwu	a1, 4(t0)
+	li	t2, 0x000000DE
+	bne	a1, t2, .Lfail
 	li	a0, 0
 	li	a7, 93
 	ecall
+.Lfail:
+	li	a0, 1
+	li	a7, 93
+	ecall

From b9ac3b87c3d761a007e3fc52efbebc367f372e53 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Tue, 26 May 2026 19:22:29 -0300
Subject: [PATCH 11/12] Reject misaligned load/store crossing u64::MAX

---
 executor/src/tests/memory_tests.rs | 30 +++++++++++++++++++++++++++++
 executor/src/vm/memory.rs          | 31 +++++++++++++++---------------
 2 files changed, 46 insertions(+), 15 deletions(-)

diff --git a/executor/src/tests/memory_tests.rs b/executor/src/tests/memory_tests.rs
index fcc0e07b9..6c3b3f2ed 100644
--- a/executor/src/tests/memory_tests.rs
+++ b/executor/src/tests/memory_tests.rs
@@ -109,3 +109,33 @@ fn test_commit_public_output_total_cap() {
     let err = memory.commit_public_output(0x1_0000, 1).unwrap_err();
     assert!(matches!(err, MemoryError::CommitSizeExceeded));
 }
+
+#[test]
+fn test_misaligned_load_store_overflow_errors() {
+    let mut memory = Memory::default();
+
+    assert!(matches!(
+        memory.load_half(u64::MAX).unwrap_err(),
+        MemoryError::AddressOverflow
+    ));
+    assert!(matches!(
+        memory.store_half(u64::MAX, 0).unwrap_err(),
+        MemoryError::AddressOverflow
+    ));
+    assert!(matches!(
+        memory.load_word(u64::MAX - 1).unwrap_err(),
+        MemoryError::AddressOverflow
+    ));
+    assert!(matches!(
+        memory.store_word(u64::MAX - 1, 0).unwrap_err(),
+        MemoryError::AddressOverflow
+    ));
+    assert!(matches!(
+        memory.load_doubleword(u64::MAX - 6).unwrap_err(),
+        MemoryError::AddressOverflow
+    ));
+    assert!(matches!(
+        memory.store_doubleword(u64::MAX - 6, 0).unwrap_err(),
+        MemoryError::AddressOverflow
+    ));
+}
diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs
index 92b87eda4..4de58b17a 100644
--- a/executor/src/vm/memory.rs
+++ b/executor/src/vm/memory.rs
@@ -85,11 +85,12 @@ impl Memory {
             let bytes = self.cells.get(&address).cloned().unwrap_or_default();
             Ok(u32::from_le_bytes(bytes))
         } else {
+            address.checked_add(3).ok_or(MemoryError::AddressOverflow)?;
             Ok(u32::from_le_bytes([
                 self.load_byte(address),
-                self.load_byte(address.wrapping_add(1)),
-                self.load_byte(address.wrapping_add(2)),
-                self.load_byte(address.wrapping_add(3)),
+                self.load_byte(address + 1),
+                self.load_byte(address + 2),
+                self.load_byte(address + 3),
             ]))
         }
     }
@@ -99,8 +100,9 @@ impl Memory {
         if address.is_multiple_of(4) {
             self.cells.insert(address, bytes);
         } else {
+            address.checked_add(3).ok_or(MemoryError::AddressOverflow)?;
             for (i, b) in bytes.iter().enumerate() {
-                self.store_byte(address.wrapping_add(i as u64), *b);
+                self.store_byte(address + i as u64, *b);
             }
         }
         Ok(())
@@ -110,18 +112,15 @@ impl Memory {
     pub fn load_doubleword(&self, address: u64) -> Result<u64, MemoryError> {
         if address.is_multiple_of(8) {
             let low_bytes = self.cells.get(&address).cloned().unwrap_or_default();
-            let high_bytes = self
-                .cells
-                .get(&address.wrapping_add(4))
-                .cloned()
-                .unwrap_or_default();
+            let high_bytes = self.cells.get(&(address + 4)).cloned().unwrap_or_default();
             let low = u32::from_le_bytes(low_bytes) as u64;
             let high = u32::from_le_bytes(high_bytes) as u64;
             Ok(low | (high << 32))
         } else {
+            address.checked_add(7).ok_or(MemoryError::AddressOverflow)?;
             let mut bytes = [0u8; 8];
             for (i, b) in bytes.iter_mut().enumerate() {
-                *b = self.load_byte(address.wrapping_add(i as u64));
+                *b = self.load_byte(address + i as u64);
             }
             Ok(u64::from_le_bytes(bytes))
         }
@@ -133,12 +132,12 @@ impl Memory {
             let low = (value & 0xFFFFFFFF) as u32;
             let high = (value >> 32) as u32;
             self.cells.insert(address, low.to_le_bytes());
-            self.cells
-                .insert(address.wrapping_add(4), high.to_le_bytes());
+            self.cells.insert(address + 4, high.to_le_bytes());
         } else {
+            address.checked_add(7).ok_or(MemoryError::AddressOverflow)?;
             let bytes = value.to_le_bytes();
             for (i, b) in bytes.iter().enumerate() {
-                self.store_byte(address.wrapping_add(i as u64), *b);
+                self.store_byte(address + i as u64, *b);
             }
         }
         Ok(())
@@ -155,9 +154,10 @@ impl Memory {
             let offset = (address % 4) as usize;
             Ok(u16::from_le_bytes([bytes[offset], bytes[offset + 1]]))
         } else {
+            address.checked_add(1).ok_or(MemoryError::AddressOverflow)?;
             Ok(u16::from_le_bytes([
                 self.load_byte(address),
-                self.load_byte(address.wrapping_add(1)),
+                self.load_byte(address + 1),
             ]))
         }
     }
@@ -174,8 +174,9 @@ impl Memory {
             entry[offset] = bytes[0];
             entry[offset + 1] = bytes[1];
         } else {
+            address.checked_add(1).ok_or(MemoryError::AddressOverflow)?;
             self.store_byte(address, bytes[0]);
-            self.store_byte(address.wrapping_add(1), bytes[1]);
+            self.store_byte(address + 1, bytes[1]);
         }
         Ok(())
     }

From b1a88d6956f30e1564b93156cbd35d2241353652 Mon Sep 17 00:00:00 2001
From: gabrielbosio <gabrielbosio95@gmail.com>
Date: Wed, 27 May 2026 11:52:58 -0300
Subject: [PATCH 12/12] Document why aligned doubleword +4 needs no overflow
 guard

---
 executor/src/vm/memory.rs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/executor/src/vm/memory.rs b/executor/src/vm/memory.rs
index 4de58b17a..ea84e2620 100644
--- a/executor/src/vm/memory.rs
+++ b/executor/src/vm/memory.rs
@@ -111,6 +111,7 @@ impl Memory {
     /// Load a doubleword (64-bit) from memory - for LD instruction
     pub fn load_doubleword(&self, address: u64) -> Result<u64, MemoryError> {
         if address.is_multiple_of(8) {
+            // 8-alignment bounds `address` to `u64::MAX - 7`, so `address + 4` can't overflow.
             let low_bytes = self.cells.get(&address).cloned().unwrap_or_default();
             let high_bytes = self.cells.get(&(address + 4)).cloned().unwrap_or_default();
             let low = u32::from_le_bytes(low_bytes) as u64;
@@ -131,6 +132,7 @@ impl Memory {
         if address.is_multiple_of(8) {
             let low = (value & 0xFFFFFFFF) as u32;
             let high = (value >> 32) as u32;
+            // 8-alignment bounds `address` to `u64::MAX - 7`, so `address + 4` can't overflow.
             self.cells.insert(address, low.to_le_bytes());
             self.cells.insert(address + 4, high.to_le_bytes());
         } else {