Skip to content

spec: rv2 as DWordBL in CPU due to STORE #297

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
RobinJadoul wants to merge 2 commits into from
Closed

spec: rv2 as DWordBL in CPU due to STORE #297

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
49deff9
spec: rv2 as DWordBL in CPU due to STORE
RobinJadoul Feb 6, 2026
293dcb8
Whoops, forgot to range check rv2 for soundness
RobinJadoul Feb 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 22 additions & 20 deletions spec/src/cpu.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,7 @@ pad = 0

[[variables.auxiliary]]
name = "rv2"
type = "DWordWHH"
type = "DWordBL"
desc = "The value of register `rs2`"
pad = 0

Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -643,12 +650,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]
Comment on lines +656 to +657
Copy link
Copy Markdown
Collaborator

@erik-3milabs erik-3milabs Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While I agree that pushing rv1 into the array this way is correct, I'd be inclined to apply cast to the second appearance of "rv1" in either array as well, just to make it easier to read.

multiplicity = "read_register1"

[[constraints.mem]]
Expand All @@ -657,25 +663,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]]
Expand All @@ -685,19 +689,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"]


Expand Down Expand Up @@ -747,20 +749,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]]]
Comment on lines +759 to +765
Copy link
Copy Markdown
Collaborator

@erik-3milabs erik-3milabs Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe we decided to move away from slicing. Shall we use this opportunity to remove the slices in these two constraints?

Copy link
Copy Markdown
Collaborator Author

@RobinJadoul RobinJadoul Feb 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I mostly mind them in the "formal" polys, less so in the descriptive constraint


[[constraints.ext]]
kind = "interaction"
Expand Down