Skip to content

Add extra constraints to prevent register side effects in CPU32 padding rows #646

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

Open
RobinJadoul wants to merge 2 commits into
base: spec/main
Choose a base branch
from
+16 −0
Open

Add extra constraints to prevent register side effects in CPU32 padding rows #646

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
49f2e36
Add extra constraints to prevent register side effects in CPU32 paddi…
RobinJadoul Jun 3, 2026
943c2aa
fixes
RobinJadoul Jun 3, 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
1 change: 1 addition & 0 deletions spec/cpu32.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ provide these below.

Most constraints correspond to those already present in the CPU, and we present them here first,
including some updates to the range checking corresponding to the differing types.
We also need to make sure that for padding rows ($mu = 0$), no side effects can occur.

#render_constraint_table(chip, config, groups: ("decode", "range", "alu", "mem", "logup"))

Expand Down
15 changes: 15 additions & 0 deletions spec/src/cpu32.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -350,6 +350,21 @@ multiplicity = "write_register"
[[constraint_groups]]
name = "logup"

[[constraints.logup]]
kind = "arith"
constraint = "$#`!μ` => #`read_register1 = 0`$"
poly = ["*", ["not", "μ"], "read_register1"]

[[constraints.logup]]
kind = "arith"
constraint = "$#`!μ` => #`read_register2 = 0`$"
poly = ["*", ["not", "μ"], "read_register2"]

[[constraints.logup]]
kind = "arith"
constraint = "$#`!μ` => #`write_register = 0`$"
poly = ["*", ["not", "μ"], "write_register"]
Comment on lines +353 to +366
Copy link
Copy Markdown

@claude claude Bot Jun 3, 2026

Choose a reason for hiding this comment

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

Potential gap: ALU interaction multiplicity is not gated on μ

The three new constraints correctly prevent register read/write side effects in padding rows. However, there is a similar interaction in the alu group:

[[constraints.alu]]
kind = "interaction"
tag = "ALU"
...
multiplicity = "ALU"

ALU is constrained to be a bit, but there is no constraint !μ => ALU = 0. A malicious prover could set ALU = 1 in a padding row (μ = 0) and inject a spurious entry into the ALU logup bus. Whether this is exploitable depends on whether the ALU chip has independent constraints preventing it from matching against rows not associated with real instructions.

If the ALU chip is not separately constrained, a !μ => ALU = 0 constraint should be added here alongside the three existing ones.

Copy link
Copy Markdown
Collaborator Author

@RobinJadoul RobinJadoul Jun 3, 2026

Choose a reason for hiding this comment

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

ALU should be free of side-effects, and is similarly not gated on word_instr in the CPU chip


[[constraints.logup]]
kind = "interaction"
tag = "CPU32"
Expand Down
Loading