From 49deff91c39a13cada77e6d9f1373be8fb161280 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 6 Feb 2026 17:48:11 +0100 Subject: [PATCH 1/2] spec: rv2 as DWordBL in CPU due to STORE This is a (temporary, for now) change to the CPU to have `rv2` available as `DWordBL` so that the `MEMW` interaction on the `STORE` path can work correctly. It already builds on top of the array expressions to clean up the signatures for all MEMW calls from the CPU along the way. --- spec/src/cpu.toml | 35 +++++++++++++++-------------------- 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 994fda508..e85991791 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -231,7 +231,7 @@ pad = 0 [[variables.auxiliary]] name = "rv2" -type = "DWordWHH" +type = "DWordBL" desc = "The value of register `rs2`" pad = 0 @@ -643,12 +643,11 @@ multiplicity = "DIVREM" name = "mem" prefix = "M" -# TODO: no types available, so no casting yet [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [1, ["*", 2, "rs1"], "rv1", ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0] -output = "rv1" +input = [1, ["*", 2, "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0] multiplicity = "read_register1" [[constraints.mem]] @@ -657,25 +656,23 @@ constraint = "$#`!read_register1` => #`rv1[i]` = 0$" poly = ["*", ["not", "read_register1"], ["idx", "rv1", "i"]] iter = ["i", 0, 2] -# TODO: no types available, so no casting yet [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [1, ["*", 2, "rs2"], "rv2", ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] -output = "rv2" +input = [1, ["*", 2, "rs2"], ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", ["cast", "rv2", "DWordWL"], 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", ["cast", "rv2", "DWordWL"], 1], 0, 0, 0, 0, 0, 0] multiplicity = "read_register2" [[constraints.mem]] kind = "arith" constraint = "$#`!read_register2` => #`rv2[i]` = 0$" poly = ["*", ["not", "read_register2"], ["idx", "rv2", "i"]] -iter = ["i", 0, 2] +iter = ["i", 0, 7] -# TODO: no types available, so no casting yet [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [1, ["*", 2, "rd"], "rvd", ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0] +input = [1, ["*", 2, "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0] multiplicity = "write_register" [[constraints.mem]] @@ -685,19 +682,17 @@ input = [0, "res", ["+", "timestamp", ["cast", 0, "DWordWL"]], "memory_2bytes", output = "rvd" multiplicity = "LOAD" -# TODO: no types available, so no casting yet [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [0, "res", "rv2", ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"] +input = [0, "res", ["cast", "rv2", ["Byte", 8]], ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"] multiplicity = "STORE" -# TODO: no types available, so no casting yet [[constraints.mem]] kind = "interaction" tag = "MEMW" -input = [1, ["*", 2, 255], "next_pc", ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] -output = "pc" +input = [1, ["*", 2, 255], ["arr", ["idx", "next_pc", 0], ["idx", "next_pc", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0] +output = ["arr", ["idx", "pc", 0], ["idx", "pc", 1], 0, 0, 0, 0, 0, 0] multiplicity = ["not", "pad"] @@ -747,20 +742,20 @@ poly = ["-", ["idx", ["cast", "arg1", "DWordWL"], 1], ["*", ["not", "word_instr" [[constraints.ext]] kind = "interaction" -tag = "MSB16" -input = [["idx", "rv2", 1]] +tag = "MSB8" +input = [["idx", "rv2", 3]] output = "arg2_sign_bit" multiplicity = "word_instr" [[constraints.ext]] kind = "arith" -constraint = "$#`arg2[:4]` = (1 - #`STORE` - #`LOAD`) dot #`rv2[:2]` + (1 - #`BEQ` - #`BLT`) dot #`imm[0]`$" +constraint = "$#`arg2[:4]` = (1 - #`STORE` - #`LOAD`) dot #`rv2[:4]` + (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]]] [[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 - #`STORE` - #`LOAD`) dot ((1 - #`word_instr`) dot #`rv2[4:]` + #`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", ["cast", "rv2", "DWordWL"], 1]], ["*", ["-", 1, "STORE", "LOAD"], "signed", "arg2_sign_bit", ["-", ["^", 2, 32], 1]], ["*", ["-", 1, "BEQ", "BLT"], ["idx", "imm", 1]]] [[constraints.ext]] kind = "interaction" From 293dcb80c3e342accdae8f1bc7997344a117f382 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Fri, 6 Feb 2026 17:53:56 +0100 Subject: [PATCH 2/2] Whoops, forgot to range check rv2 for soundness --- spec/src/cpu.toml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index e85991791..f38b2ed1b 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -530,6 +530,13 @@ tag = "IS_BYTE" input = ["rd"] multiplicity = 1 +[[constraints.range]] +kind = "interaction" +tag = "IS_BYTE" +input = [["idx", "rv2", "i"]] +iter = ["i", 0, 7] +multiplicity = 1 + [[constraints.range]] kind = "interaction" tag = "IS_BYTE"