From 46139a3aa9470ed779e3159489a423028ce216bd Mon Sep 17 00:00:00 2001
From: Robin Jadoul <robin.jadoul@3milabs.tech>
Date: Mon, 9 Feb 2026 16:45:14 +0100
Subject: [PATCH 1/3] spec: separate ALU path for STORE to enable byte
 representation of rv2 to exist in arg2

---
 spec/src/cpu.toml | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml
index 994fda508..291eb0ebb 100644
--- a/spec/src/cpu.toml
+++ b/spec/src/cpu.toml
@@ -559,10 +559,16 @@ prefix = "A"
 [[constraints.alu]]
 kind = "template"
 tag = "ADD"
-cond = ["+", "ADD", "LOAD", "STORE"]
+cond = ["+", "ADD", "LOAD"]
 input = [["cast", "arg1", "DWordWL"], ["cast", "arg2", "DWordWL"]]
 output = ["cast", "res", "DWordWL"]
 
+[[constraints.alu]]
+kind = "template"
+tag = "add"
+cond = "STORE"
+input = [["cast", "arg1", "DWordWL"], "imm"]
+
 [[constraints.alu]]
 kind = "template"
 tag = "SUB"
@@ -689,7 +695,7 @@ multiplicity = "LOAD"
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [0, "res", "rv2", ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"]
+input = [0, "res", ["cast", "arg2", ["Byte", 8]], ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"]
 multiplicity = "STORE"
 
 # TODO: no types available, so no casting yet
@@ -754,13 +760,13 @@ multiplicity = "word_instr"
 
 [[constraints.ext]]
 kind = "arith"
-constraint = "$#`arg2[:4]` = (1 - #`STORE` - #`LOAD`) dot #`rv2[:2]` + (1 - #`BEQ` - #`BLT`) dot #`imm[0]`$"
-poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 0], ["*", ["-", 1, "STORE", "LOAD"], ["idx", ["cast", "rv2", "DWordWL"], 0]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 0]]]
+constraint = "$#`arg2[:4]` = (1 - #`LOAD`) dot #`rv2[:2]` + (1 - #`BEQ` - #`BLT` - #`STORE`) dot #`imm[0]`$"
+poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 0], ["*", ["not", "LOAD"], ["idx", ["cast", "rv2", "DWordWL"], 0]], ["*", ["-", 1, "BEQ", "BLT", "STORE"], ["idx", "imm", 0]]]
 
 [[constraints.ext]]
 kind = "arith"
-constraint = "$#`arg2[4:]` = (1 - #`STORE` - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT`) dot #`imm[1]`$"
-poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["-", 1, "STORE", "LOAD"], ["not", "word_instr"], ["idx", "rv2", 2]], ["*", ["-", 1, "STORE", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 1]]]
+constraint = "$#`arg2[4:]` = (1 - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT`) dot #`imm[1]`$"
+poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["not", "LOAD"], ["not", "word_instr"], ["idx", "rv2", 2]], ["*", ["not", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT", "STORE"], ["idx", "imm", 1]]]
 
 [[constraints.ext]]
 kind = "interaction"

From 86640cbe5deef609391ad14b031b9f7112b44fed Mon Sep 17 00:00:00 2001
From: Robin Jadoul <robin.jadoul@3milabs.tech>
Date: Tue, 10 Feb 2026 10:48:23 +0100
Subject: [PATCH 2/3] Apply review suggestion

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>
---
 spec/src/cpu.toml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml
index 291eb0ebb..4e47ff06e 100644
--- a/spec/src/cpu.toml
+++ b/spec/src/cpu.toml
@@ -565,9 +565,10 @@ output = ["cast", "res", "DWordWL"]
 
 [[constraints.alu]]
 kind = "template"
-tag = "add"
+tag = "ADD"
 cond = "STORE"
 input = [["cast", "arg1", "DWordWL"], "imm"]
+output = ["cast", "res", "DWordWL"]
 
 [[constraints.alu]]
 kind = "template"

From fd2d0a6243f95fbcc5ca118511412e846d533f1c Mon Sep 17 00:00:00 2001
From: Robin Jadoul <robin.jadoul@3milabs.tech>
Date: Tue, 10 Feb 2026 11:06:31 +0100
Subject: [PATCH 3/3] Update spec/src/cpu.toml

Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com>
---
 spec/src/cpu.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml
index 4e47ff06e..d1027636f 100644
--- a/spec/src/cpu.toml
+++ b/spec/src/cpu.toml
@@ -766,7 +766,7 @@ poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 0], ["*", ["not", "LOAD"], ["i
 
 [[constraints.ext]]
 kind = "arith"
-constraint = "$#`arg2[4:]` = (1 - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT`) dot #`imm[1]`$"
+constraint = "$#`arg2[4:]` = (1 - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`arg2_sign_bit` dot (2^(32) - 1)) + (1 - #`BEQ` - #`BLT` - `#STORE`) dot #`imm[1]`$"
 poly = ["-", ["idx", ["cast", "arg2", "DWordWL"], 1], ["*", ["not", "LOAD"], ["not", "word_instr"], ["idx", "rv2", 2]], ["*", ["not", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT", "STORE"], ["idx", "imm", 1]]]
 
 [[constraints.ext]]