Skip to content

spec: ARE_BYTES #532

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
erik-3milabs merged 9 commits into from
Apr 28, 2026
Merged

spec: ARE_BYTES #532

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
e89a0e2
spec/ARE_BYTES: introduce ARE_BYTES signature
erik-3milabs Apr 23, 2026
7e86d3d
spec/ARE_BYTES: introduce ARE_BYTES lookup
erik-3milabs Apr 23, 2026
9f93d5c
spec/ARE_BYTES: introduce IS_BYTE template
erik-3milabs Apr 23, 2026
285ee04
spec/ARE_BYTES: switch IS_BYTE lookup to IS_BYTE template
erik-3milabs Apr 23, 2026
ca217ff
spec/ARE_BYTES: drop IS_BYTE interaction
erik-3milabs Apr 23, 2026
315ebdc
spec/ARE_BYTES: drop IS_BYTE lookup signature
erik-3milabs Apr 23, 2026
c2c13d7
spec/ARE_BYTES: turn multiplicity into cond
erik-3milabs Apr 28, 2026
f8a0595
spec/ARE_BYTES: remove as potential optimization
erik-3milabs Apr 28, 2026
75216c8
spec/ARE_BYTES: update assumptions using IS_BYTE
erik-3milabs Apr 28, 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: 0 additions & 2 deletions spec/bitwise.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,6 @@ This chip adds the following interactions to the lookup:

= Notes/Optimizations
The following ideas may prove to be optimizations for the #bitwise chip:
+ Extend `IS_BYTE[X]` to `ARE_BYTES[X, Y]`, such that two bytes are range checked at once.
When only a single check is required, one can still execute `IS_BYTE[X] := ARE_BYTES[X, 0]`.
+ Drop `MSB8` column, and instead define the `MSB8` lookup as `MSB8<X> := MSB16[256X]`.
Note: currently, `MSB8` also implicity range checks the input `X` (the lookup fails if `X` is not a `Byte`).
This optimization should only be executed when all chips leveraging `MSB8` do _not_ need this implicit range check.
Expand Down
1 change: 1 addition & 0 deletions spec/book.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
)),
("TEMPLATES", (
("is_bit.typ", [`IS_BIT` template], <isbit>),
("is_byte.typ", [`IS_BYTE` template], <isbyte>),
("sign.typ", [`SIGN` template], <sign>),
("add.typ", [`ADD`/`SUB` template], <add>),
("neg.typ", [`NEG` template], <neg>),
Expand Down
22 changes: 22 additions & 0 deletions spec/is_byte.typ
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
#import "/book.typ": book-page
#import "/src.typ": load_config, load_chip
#import "/chip.typ": render_chip_variable_table, render_constraint_table, compute_nr_interactions, total_nr_variables, total_nr_instantiated_columns

#let config = load_config()
#let chip = load_chip("src/is_byte.toml", config)

#show: book-page(chip.name)
#let is_byte = raw(chip.name)

#is_byte is a constraint template that is used to assert that a variable lies in the range $[0, 255]$ under the condition that `cond` is non-zero. Note: when `cond` is omitted, it defaults to $1$.

When a chip leverages this template twice or more, implementors are encouraged to merge pairs of #is_byte interactions with identical conditions into `ARE_BYTES` interactions; the #is_byte template is included for convenience of notation, and to complete the specification of chips that use an odd number of #is_byte range checks.

= Variables
#let nr_interactions = compute_nr_interactions(chip)

The #is_byte template leverages #nr_interactions interaction(s):
#render_chip_variable_table(chip, config)

= Constraints
#render_constraint_table(chip, config)
11 changes: 8 additions & 3 deletions spec/src/bitwise.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,11 @@ name = "μ_IS_BYTE"
type = "BaseField"
desc = ""
Copy link
Copy Markdown

@claude claude Bot Apr 23, 2026

Choose a reason for hiding this comment

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

Medium – Dead multiplicity variable

μ_IS_BYTE is no longer referenced in any constraint in this file. Since IS_BYTE is now a template (not an interaction), BITWISE no longer contributes to an IS_BYTE interaction, so this multiplicity column serves no purpose. It should be removed.

Suggested change
desc = ""


[[variables.multiplicity]]
name = "μ_ARE_BYTES"
type = "BaseField"
desc = ""

[[variables.multiplicity]]
name = "μ_IS_HALF"
type = "BaseField"
Expand Down Expand Up @@ -164,9 +169,9 @@ multiplicity = ["-", "μ_ZERO"]

[[constraints.contributions]]
kind = "interaction"
tag = "IS_BYTE"
input = ["X"]
multiplicity = ["-", "μ_IS_BYTE"]
tag = "ARE_BYTES"
input = ["X", "Y"]
multiplicity = ["-", "μ_ARE_BYTES"]

[[constraints.contributions]]
kind = "interaction"
Expand Down
4 changes: 2 additions & 2 deletions spec/src/branch.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,10 +116,10 @@ output = "next_pc_unmasked"
cond = "JALR"

[[constraints.all]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", "next_pc_low", 1]]
multiplicity = "μ"
cond = "μ"

[[constraints.all]]
kind = "interaction"
Expand Down
18 changes: 6 additions & 12 deletions spec/src/cpu.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -511,43 +511,37 @@ input = ["EBREAK"]
ref = "cpu:c:range_EBREAK"

[[constraints.range]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = ["rs1"]
multiplicity = 1

[[constraints.range]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = ["rs2"]
multiplicity = 1

[[constraints.range]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = ["rd"]
multiplicity = 1

[[constraints.range]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", "arg1", "i"]]
iter = ["i", 0, 7]
multiplicity = 1

[[constraints.range]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", "arg2", "i"]]
iter = ["i", 0, 7]
multiplicity = 1

[[constraints.range]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", "res", "i"]]
iter = ["i", 0, 7]
multiplicity = 1


[[constraint_groups]]
Expand Down
21 changes: 21 additions & 0 deletions spec/src/is_byte.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
name = "IS_BYTE"

[[variables.condition]]
name = "cond"
type = "BaseField"
desc = ""

[[variables.input]]
name = "X"
type = "BaseField"
desc = "Value for which to assert that it lies in the range $[0, 255]$."

[[constraint_groups]]
name = "all"

[[constraints.all]]
kind = "interaction"
tag = "ARE_BYTES"
input = [0, "X"]
Copy link
Copy Markdown

@claude claude Bot Apr 23, 2026

Choose a reason for hiding this comment

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

Low – Constant 0 consumes a BITWISE row slot unnecessarily

IS_BYTE<X, μ> expands to ARE_BYTES[0, X], always using the first byte slot as the constant 0. This means every IS_BYTE invocation occupies a full BITWISE row while only constraining one variable.

This is by design (the template exists for chips with an odd number of byte range-checks), but it's worth noting in the spec that the "waste" is intentional and that implementors should prefer pairing directly into ARE_BYTES[X, Y] whenever possible, as is_byte.typ already encourages.

No code change required — just flagging for visibility.

Copy link
Copy Markdown
Collaborator Author

@erik-3milabs erik-3milabs Apr 24, 2026

Choose a reason for hiding this comment

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

that implementors should prefer pairing directly into ARE_BYTES[X, Y] whenever possible ...

This is exactly what is written in the IS_BYTE template description.

multiplicity = "cond"
ref = "isbyte:c:isbyte"
18 changes: 9 additions & 9 deletions spec/src/keccak_round.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,18 +211,18 @@ multiplicity = "μ"
# Cxz_left = [-1, 256, -1, 256, -1, 256, -1, 256] and
# Cxz_right = [ 1, -256, 1, -256, 1, -256, 1, -256]
[[constraints.theta]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", ["idx", "Cxz_left", "x"], "z"]]
iters = [["x", 0, 4], ["z", 0, 7]]
multiplicity = "μ"
cond = "μ"

[[constraints.theta]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", ["idx", "Cxz_right", "x"], "z"]]
iters = [["x", 0, 4], ["z", 0, 7]]
multiplicity = "μ"
cond = "μ"

[[constraints.theta]]
kind = "interaction"
Expand Down Expand Up @@ -257,18 +257,18 @@ multiplicity = "μ"
# rot_left = [-1, 256, -1, 256, -1, 256, -1, 256] and
# rot_right = [ 1, -256, 1, -256, 1, -256, 1, -256]
[[constraints.rho]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"]]
iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]]
multiplicity = "μ"
iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]]
cond = "μ"

[[constraints.rho]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"]]
iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]]
multiplicity = "μ"
cond = "μ"

[[constraint_groups]]
name = "chi"
Expand Down
6 changes: 2 additions & 4 deletions spec/src/page.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,16 +40,14 @@ def = ["+", "page", ["*", "offset", ["cast", 1, "DWordWL"]]]
name = "all"

[[constraints.all]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = ["init"]
multiplicity = 1

[[constraints.all]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = ["fini"]
multiplicity = 1

[[constraints.all]]
kind = "interaction"
Expand Down
4 changes: 2 additions & 2 deletions spec/src/sha256.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -232,11 +232,11 @@ input = ["timestamp", "last_round_out", 64]
multiplicity = ["-", "μ"]

[[constraints.compress]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["idx", "out", "i"]]
multiplicity = "μ"
iter = ["i", 0, 31]
cond = "μ"

[[constraints.compress]]
kind = "template"
Expand Down
8 changes: 4 additions & 4 deletions spec/src/sha256msgsched.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,10 +79,10 @@ desc = "#`IS_WORD[SHA256_M[timestamp, i]]` for $0 <= i < #`index`$"
name = "lookback"

[[constraints.lookback]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = [["-", "index", 16]]
multiplicity = "μ"
cond = "μ"

[[constraints.lookback]]
kind = "interaction"
Expand Down Expand Up @@ -130,10 +130,10 @@ output = "s1"
multiplicity = "μ"

[[constraints.calc]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = ["carry"]
multiplicity = "μ"
cond = "μ"

[[constraints.calc]]
kind = "interaction"
Expand Down
8 changes: 4 additions & 4 deletions spec/src/sha256round.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -254,10 +254,10 @@ multiplicity = "μ"
iter = ["i", 0, 1]

[[constraints.addition]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = ["carry_a"]
multiplicity = "μ"
cond = "μ"

[[constraints.addition]]
kind = "interaction"
Expand All @@ -267,10 +267,10 @@ multiplicity = "μ"
iter = ["i", 0, 1]

[[constraints.addition]]
kind = "interaction"
kind = "template"
tag = "IS_BYTE"
input = ["carry_e"]
multiplicity = "μ"
cond = "μ"

[[constraint_groups]]
name = "output"
Expand Down
2 changes: 1 addition & 1 deletion spec/src/shift.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ iter = ["i", 0, 3]
ref = "shift:a:range_in"

[[assumptions]]
desc = "`IS_BYTE[shift]`"
desc = "`IS_BYTE<shift>`"
ref = "shift:a:range_shift"

[[assumptions]]
Expand Down
13 changes: 10 additions & 3 deletions spec/src/signatures.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,13 @@ kind = "template"
input = ["BaseField"]
cond = "BaseField"

# IS_BYTE<X, μ>
[[signatures]]
tag = "IS_BYTE"
kind = "template"
input = ["BaseField"]
cond = "BaseField"

# cond => ADD<sum; lhs, rhs>
[[signatures]]
tag = "ADD"
Expand Down Expand Up @@ -157,11 +164,11 @@ kind = "interaction"
input = ["B20"]
output = "Bit"

# IS_BYTE[X]
# ARE_BYTES[X, Y]
[[signatures]]
tag = "IS_BYTE"
tag = "ARE_BYTES"
kind = "interaction"
input = ["Byte"]
input = ["Byte", "Byte"]

# IS_HALF[X]
[[signatures]]
Expand Down
Loading