Skip to content

Range-check multiplicities wherever needed for soundness #1017

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

Merged
RobinJadoul merged 3 commits into from
Oct 12, 2026
Merged

Range-check multiplicities wherever needed for soundness #1017

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
92b5093
Range-check multiplicities wherever needed for soundness
RobinJadoul Oct 7, 2026
256e397
Make some byte checks unconditional if they could create loops on the…
RobinJadoul Oct 12, 2026
fe3097b
add note
erik-3milabs Oct 12, 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
2 changes: 1 addition & 1 deletion spec/chapters/memw.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ provide these below.

#render_constraint_table(alignedchip, config, groups: "assumptions")

#render_constraint_table(alignedchip, config)
#render_constraint_table(alignedchip, config, groups: ("consistency", "memory", "output"))

== Padding
The table can be padded to the next power of two with the following value assignments:
Expand Down
1 change: 1 addition & 0 deletions spec/chapters/signatures.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@

#let interactions = signatures.signatures.filter(s => s.kind == "interaction")
The following lists signatures of the #interactions.len() interactions in this VM.
#show figure: set block(breakable: true)
#figure(table(
columns: (1fr, auto),
inset: 7pt,
Expand Down
17 changes: 17 additions & 0 deletions spec/chapters/verifier.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,21 @@
#import "../meta.typ": todo
// TODO:
// - sigma protocol, layout the various steps
// - Fiat Shamir transformation into non-interactive protocol.
//

= Auxiliary verification steps
#todo[
*Verify that the number of tables used by the prover in an epoch/proof is
lower than some bound.*
Without this restriction, a prover can construct an interaction multiplicity
of $-1$ by repeating a table row a large number of times.
While this strategy this would result in a large increase of
proof size, the excess can be purged during recursion.
This could e.g. be used to bypass range checks.

TODO: determine the right bound. The `IS_WH` chip with its multiplicity of type
`B20` induces an upper bound: it requires $approx 2^43$ rows
(or $approx 2^23$ tables) to achieve a multiplicity sum of $-1$.
This can then be used to forge an `IS_HALF` check.
]
2 changes: 1 addition & 1 deletion spec/meta.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@
)
)

#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: 20%, stroke: black)[
#let todo(background: white, foreground: black, name: none, body) = block(fill: background, outset: 0.4em, radius: .5em, stroke: black)[
#set text(fill: foreground)
*TODO #if name != none { [(#name)] }*: #body
]
Expand Down
8 changes: 6 additions & 2 deletions spec/src/branch.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ def = {idx = "i", polys = [

[[variables.multiplicity]]
name = "μ"
type = "Bit"
type = "Byte"
desc = ""
pad = 0

Expand Down Expand Up @@ -109,6 +109,11 @@ input = ["JALR"]
[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "template"
tag = "IS_BYTE"
input = ["μ"]

[[constraints.all]]
kind = "template"
tag = "ADD"
Expand All @@ -127,7 +132,6 @@ cond = "JALR"
kind = "template"
tag = "IS_BYTE"
input = [["idx", "next_pc_low", 1]]
cond = "μ"

[[constraints.all]]
kind = "interaction"
Expand Down
7 changes: 6 additions & 1 deletion spec/src/bytewise.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,13 +26,18 @@ pad = 0

[[variables.multiplicity]]
name = "μ"
type = "BaseField"
type = "Byte"
desc = ""
pad = 0

[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "template"
tag = "IS_BYTE"
input = ["μ"]

[[constraints.all]]
kind = "interaction"
tag = "BYTE_ALU"
Expand Down
14 changes: 12 additions & 2 deletions spec/src/dvrm.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,13 +171,13 @@ def = ["+", "μ_q", "μ_r"]

[[variables.multiplicity]]
name = "μ_q"
type = "BaseField"
type = "Byte"
desc = ""
pad = 0

[[variables.multiplicity]]
name = "μ_r"
type = "BaseField"
type = "Byte"
desc = ""
pad = 0

Expand All @@ -187,6 +187,16 @@ pad = 0
[[constraint_groups]]
name = "range"

[[constraints.range]]
kind = "template"
tag = "IS_BYTE"
input = ["μ_q"]

[[constraints.range]]
kind = "template"
tag = "IS_BYTE"
input = ["μ_r"]

Comment thread
erik-3milabs marked this conversation as resolved.
Resolved
[[constraints.range]]
kind = "interaction"
tag = "IS_HALF"
Expand Down
7 changes: 6 additions & 1 deletion spec/src/eq.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ pad = 0

[[variables.multiplicity]]
name = "μ"
type = "BaseField"
type = "Bit"
Comment thread
erik-3milabs marked this conversation as resolved.
Resolved
desc = ""
pad = 0

Expand All @@ -55,6 +55,11 @@ iter = ["i", 0, 1]
[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.all]]
kind = "interaction"
tag = "IS_HALF"
Expand Down
5 changes: 5 additions & 0 deletions spec/src/fext_fma.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,11 @@ pad = 0
[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.all]]
kind = "template"
tag = "REG"
Expand Down
5 changes: 5 additions & 0 deletions spec/src/fext_load.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,11 @@ pad = 0
[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.all]]
kind = "template"
tag = "REG"
Expand Down
5 changes: 5 additions & 0 deletions spec/src/fext_zero.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,11 @@ pad = 0
[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.all]]
kind = "template"
tag = "REG"
Expand Down
8 changes: 7 additions & 1 deletion spec/src/is_wh.toml
View file
Open in desktop

@erik-3milabs erik-3milabs Oct 12, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

This IS_B20 got me thinking: what if the prover introduces sufficiently many rows with large, positive μ and have them collectively mimic a single μ= -1?

Given that we're working with a 64-bit prime, this IS_B20 lookup allows this to be achieved with 2^44 rows, which fit in 2^24 tables of 2^20 rows each. 2^24 tables is a lot, but, given that (with the exception of one, maybe) all of these tables are identical, the prover overhead is negligible (right?). Sure, the proof would be large, but that is something you can reduce through recursion.

So: the verifier will have to ensure the number of tables being used during proving are not excessively large.

@RobinJadoul RobinJadoul Oct 12, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

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

Yeah, fair point, we may need some bound on total number of tables (or tables per epoch)

@erik-3milabs erik-3milabs Oct 12, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

added it as a note

Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,19 @@ pad = 0

[[variables.multiplicity]]
name = "μ"
type = "BaseField"
type = "B20"
desc = ""
pad = 0

[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "interaction"
tag = "IS_B20"
input = ["μ"]
multiplicity = 1

[[constraints.all]]
kind = "interaction"
tag = "IS_HALF"
Expand Down
2 changes: 1 addition & 1 deletion spec/src/is_whh.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ code = "WHH"

[[variables.condition]]
name = "cond"
type = "BaseField"
type = "Bit"
desc = "the multiplicity with which to apply the interactions"

[[variables.input]]
Expand Down
5 changes: 5 additions & 0 deletions spec/src/keccak.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,11 @@ pad = 0
[[constraint_groups]]
name = "output"

[[constraints.output]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.output]]
kind = "interaction"
tag = "ECALL"
Expand Down
8 changes: 5 additions & 3 deletions spec/src/keccak_round.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,11 @@ desc = ""
[[constraint_groups]]
name = "io"

[[constraints.io]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.io]]
kind = "interaction"
tag = "KECCAK"
Expand Down Expand Up @@ -227,7 +232,6 @@ kind = "template"
tag = "IS_BYTE"
input = [["idx", ["idx", "Cxz_left", "x"], "z"]]
iters = [["x", 0, 4], ["z", 0, 7]]
cond = "μ"

[[constraints.theta]]
kind = "template"
Expand Down Expand Up @@ -275,15 +279,13 @@ kind = "template"
tag = "IS_BYTE"
input = [["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"]]
iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]]
cond = "μ"
ref = "keccak:c:range_rot_left"

[[constraints.rho]]
kind = "template"
tag = "IS_BYTE"
input = [["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"]]
iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]]
cond = "μ"
ref = "keccak:c:range_rot_right"

[[constraint_groups]]
Expand Down
5 changes: 5 additions & 0 deletions spec/src/load.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,11 @@ desc = "`IS_WORD[timestamp]`"
[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.all]]
kind = "template"
tag = "IS_BIT"
Expand Down
7 changes: 6 additions & 1 deletion spec/src/lt.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ def = ["idx", "carry", 1]

[[variables.multiplicity]]
name = "μ"
type = "Bit"
type = "Byte"
desc = ""
pad = 0

Expand All @@ -101,6 +101,11 @@ ref = "lt:a:range_rhs"
name = "range"
desc = "Range-check the inputs"

[[constraints.range]]
kind = "template"
tag = "IS_BYTE"
input = ["μ"]

[[constraints.range]]
kind = "interaction"
tag = "IS_HALF"
Expand Down
14 changes: 12 additions & 2 deletions spec/src/mul.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,13 +111,13 @@ def = ["+", "μ_lo", "μ_hi"]

[[variables.multiplicity]]
name = "μ_lo"
type = "BaseField"
type = "Byte"
desc = ""
pad = 0

[[variables.multiplicity]]
name = "μ_hi"
type = "BaseField"
type = "Byte"
desc = ""
pad = 0

Expand All @@ -126,6 +126,16 @@ pad = 0
[[constraint_groups]]
name = "def"

[[constraints.def]]
kind = "template"
tag = "IS_BYTE"
input = ["μ_lo"]

[[constraints.def]]
kind = "template"
tag = "IS_BYTE"
input = ["μ_hi"]

[[constraints.def]]
kind = "template"
tag = "IS_BIT"
Expand Down
2 changes: 1 addition & 1 deletion spec/src/reg_read.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ name = "REG"

[[variables.condition]]
name = "cond"
type = "BaseField"
type = "Bit"
desc = "the multiplicity with which to apply the interaction"

[[variables.input]]
Expand Down
2 changes: 1 addition & 1 deletion spec/src/reg_write.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ name = "REGW"

[[variables.condition]]
name = "cond"
type = "BaseField"
type = "Bit"
desc = "the multiplicity with which to apply the interaction"

[[variables.input]]
Expand Down
7 changes: 6 additions & 1 deletion spec/src/rotxor.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ pad = 0

[[variables.multiplicity]]
name = "μ"
type = "BaseField"
type = "Bit"
desc = ""
pad = 0

Expand Down Expand Up @@ -179,6 +179,11 @@ iter = ["i", 0, 3]
[[constraint_groups]]
name = "output"

[[constraints.output]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.output]]
kind = "interaction"
tag = "ROTXOR"
Expand Down
5 changes: 5 additions & 0 deletions spec/src/sha256round.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,6 +276,11 @@ cond = "μ"
[[constraint_groups]]
name = "output"

[[constraints.output]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.output]]
kind = "interaction"
tag = "SHA256ROUND"
Expand Down
10 changes: 10 additions & 0 deletions spec/src/shift.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -182,6 +182,16 @@ tag = "IS_BIT"
input = ["word_instr"]
ref = "shift:c:word_instr"

[[constraints.input]]
kind = "template"
tag = "IS_BIT"
input = ["μ"]

[[constraints.input]]
kind = "template"
tag = "IS_BIT"
input = ["zbs"]

[[constraint_groups]]
name = "left_flag"

Expand Down
Loading