From a4b63da2d4e91de61e2e9c6dd80e3e42fce1f7c4 Mon Sep 17 00:00:00 2001
From: Robin Jadoul <robin.jadoul@3milabs.tech>
Date: Tue, 17 Mar 2026 13:15:48 +0100
Subject: [PATCH 1/2] spec: Fix CPU sign bit constraints for `word_instr`

---
 spec/src/cpu.toml | 26 +++++++++-----------------
 1 file changed, 9 insertions(+), 17 deletions(-)

diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml
index 634d00bf9..ab2f20616 100644
--- a/spec/src/cpu.toml
+++ b/spec/src/cpu.toml
@@ -722,16 +722,10 @@ name = "ext"
 prefix = "E"
 
 [[constraints.ext]]
-kind = "arith"
-constraint = "$(#`rv1_sign_bit` or #`arg2_sign_bit` or #`res_sign_bit`) => #`word_instr`$"
-poly = ["*", ["+", "rv1_sign_bit", "arg2_sign_bit", "res_sign_bit"], ["not", "word_instr"]]
-
-[[constraints.ext]]
-kind = "interaction"
-tag = "MSB16"
-input = [["idx", "rv1", 1]]
+kind = "template"
+tag = "SIGN"
+input = [["idx", "rv1", 1], "word_instr"]
 output = "rv1_sign_bit"
-multiplicity = "word_instr"
 
 [[constraints.ext]]
 kind = "arith"
@@ -744,11 +738,10 @@ constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instr`) + (2^(32) - 1) do
 poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instr"], ["idx", "rv1", 2]], ["*", "signed", "rv1_sign_bit", ["-", ["^", 2, 32], 1]]]
 
 [[constraints.ext]]
-kind = "interaction"
-tag = "MSB16"
-input = [["idx", "rv2", 1]]
+kind = "template"
+tag = "SIGN"
+input = [["idx", "rv2", 1], "word_instr"]
 output = "arg2_sign_bit"
-multiplicity = "word_instr"
 
 [[constraints.ext]]
 kind = "arith"
@@ -761,11 +754,10 @@ constraint = "$#`arg2[4:]` = (1 - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]
 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"
-tag = "MSB8"
-input = [["idx", "res", 3]]
+kind = "template"
+tag = "SIGN"
+input = [["idx", ["cast", "res", "DWordHL"], 1],  "word_instr"]
 output = "res_sign_bit"
-multiplicity = "word_instr"
 
 [[constraints.ext]]
 kind = "arith"

From fc824cac530699d401ecb8b5d60b9a978c207c5c Mon Sep 17 00:00:00 2001
From: Robin Jadoul <robin.jadoul@3milabs.tech>
Date: Tue, 24 Mar 2026 14:33:31 +0100
Subject: [PATCH 2/2] naming and assumptions

---
 spec/sign.typ      |  2 ++
 spec/src/cpu.toml  | 31 +++++++++++++++----------------
 spec/src/sign.toml |  3 ---
 3 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/spec/sign.typ b/spec/sign.typ
index fc1b8d0a5..7135ba9c6 100644
--- a/spec/sign.typ
+++ b/spec/sign.typ
@@ -20,6 +20,8 @@ The #sign template operates on three variables:
 The #sign template operates on the following assumptions:
 #render_chip_assumptions(chip, config)
 
+If `sign` is set to $1$, `X` will be range-checked to be a halfword, and hence proving may fail if this is not ensured.
+
 = Constraints
 It takes only two constraints to compute the `sign` of `X`, given whether `X` represents a `signed` value or not. 
 When $#`signed` = 1$, the sign of `X` is equal to its most significant bit. 
diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml
index ab2f20616..a455b854f 100644
--- a/spec/src/cpu.toml
+++ b/spec/src/cpu.toml
@@ -234,9 +234,9 @@ desc = "The value of register `rs2`"
 pad = 0
 
 [[variables.auxiliary]]
-name = "rv1_sign_bit"
+name = "rv1_ext_bit"
 type = "Bit"
-desc = "The sign bit of `rv1` if seen as a 32-bit word"
+desc = "The sign bit of `rv1` if seen as a 32-bit word, used for sign extension with `word_instr`"
 pad = 0
 
 [[variables.auxiliary]]
@@ -246,9 +246,9 @@ desc = "The extended version of `rv1`, depending on `word_instr`"
 pad = 0
 
 [[variables.auxiliary]]
-name = "arg2_sign_bit"
+name = "rv2_ext_bit"
 type = "Bit"
-desc = "The sign bit of `arg2` if seen as a 32-bit word"
+desc = "The sign bit of `rv2` if seen as a 32-bit word, used for sign extension with `word_instr`"
 pad = 0
 
 [[variables.auxiliary]]
@@ -258,9 +258,9 @@ desc = "A multiplexed version of `rv2` and `imm`, to be used as second argument
 pad = 0
 
 [[variables.auxiliary]]
-name = "res_sign_bit"
+name = "res_ext_bit"
 type = "Bit"
-desc = "The sign bit of `res`, if seen as a 32-bit word"
+desc = "The sign bit of `res`, if seen as a 32-bit word, used for sign extension with `word_instr`"
 pad = 0
 
 [[variables.auxiliary]]
@@ -725,7 +725,7 @@ prefix = "E"
 kind = "template"
 tag = "SIGN"
 input = [["idx", "rv1", 1], "word_instr"]
-output = "rv1_sign_bit"
+output = "rv1_ext_bit"
 
 [[constraints.ext]]
 kind = "arith"
@@ -734,14 +734,14 @@ poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 0], ["idx", ["cast", "rv1", "D
 
 [[constraints.ext]]
 kind = "arith"
-constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instr`) + (2^(32) - 1) dot #`rv1_sign_bit` dot #`signed`$"
-poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instr"], ["idx", "rv1", 2]], ["*", "signed", "rv1_sign_bit", ["-", ["^", 2, 32], 1]]]
+constraint = "$#`arg1[4:]` = #`rv1[2]` dot (1 - #`word_instr`) + (2^(32) - 1) dot #`rv1_ext_bit` dot #`signed`$"
+poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instr"], ["idx", "rv1", 2]], ["*", "signed", "rv1_ext_bit", ["-", ["^", 2, 32], 1]]]
 
 [[constraints.ext]]
 kind = "template"
 tag = "SIGN"
 input = [["idx", "rv2", 1], "word_instr"]
-output = "arg2_sign_bit"
+output = "rv2_ext_bit"
 
 [[constraints.ext]]
 kind = "arith"
@@ -750,14 +750,14 @@ 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` - #`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]]]
+constraint = "$#`arg2[4:]` = (1 - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[2]` + #`signed` dot #`rv2_ext_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", "rv2_ext_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT", "STORE"], ["idx", "imm", 1]]]
 
 [[constraints.ext]]
 kind = "template"
 tag = "SIGN"
 input = [["idx", ["cast", "res", "DWordHL"], 1],  "word_instr"]
-output = "res_sign_bit"
+output = "res_ext_bit"
 
 [[constraints.ext]]
 kind = "arith"
@@ -766,10 +766,9 @@ poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 0], ["idx", ["cast", "res", "
 
 [[constraints.ext]]
 kind = "arith"
-constraint = "$#`!LOAD` => #`rvd[1]` = (1 - #`word_instr`) dot #`res[4:]` + #`res_sign_bit` dot (2^(32) - 1)$"
+constraint = "$#`!LOAD` => #`rvd[1]` = (1 - #`word_instr`) dot #`res[4:]` + #`res_ext_bit` dot (2^(32) - 1)$"
 desc = "_Sign_ extend the output if it wasn't a `LOAD`. Only `LOAD` has both `write_register = 1` and `rvd ≠ res`. `LOAD` and `word_instr` are disjoint"
-poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 1], ["*", ["not", "word_instr"], ["idx", ["cast", "res", "DWordWL"], 1]], ["*", "res_sign_bit", ["-", ["^", 2, 32], 1]]]]
-
+poly = ["*", ["not", "LOAD"], ["-", ["idx", "rvd", 1], ["*", ["not", "word_instr"], ["idx", ["cast", "res", "DWordWL"], 1]], ["*", "res_ext_bit", ["-", ["^", 2, 32], 1]]]]
 
 
 [[constraint_groups]]
diff --git a/spec/src/sign.toml b/spec/src/sign.toml
index ca799e0cc..24e99bd0e 100644
--- a/spec/src/sign.toml
+++ b/spec/src/sign.toml
@@ -16,9 +16,6 @@ type = "Bit"
 desc = "Sign of `X`"
 
 
-[[assumptions]]
-desc = "`IS_HALF[X]`"
-
 [[assumptions]]
 desc = "`IS_BIT<signed>`"