diff --git a/spec/bitwise.typ b/spec/bitwise.typ index 82f9e36f9..332bef3d9 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -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 := 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. diff --git a/spec/book.typ b/spec/book.typ index 3b65642f9..cbea7ab47 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -18,6 +18,7 @@ )), ("TEMPLATES", ( ("is_bit.typ", [`IS_BIT` template], ), + ("is_byte.typ", [`IS_BYTE` template], ), ("sign.typ", [`SIGN` template], ), ("add.typ", [`ADD`/`SUB` template], ), ("neg.typ", [`NEG` template], ), diff --git a/spec/is_byte.typ b/spec/is_byte.typ new file mode 100644 index 000000000..09bf78e98 --- /dev/null +++ b/spec/is_byte.typ @@ -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) \ No newline at end of file diff --git a/spec/src/bitwise.toml b/spec/src/bitwise.toml index 67d73facd..30875a810 100644 --- a/spec/src/bitwise.toml +++ b/spec/src/bitwise.toml @@ -101,6 +101,11 @@ name = "μ_IS_BYTE" type = "BaseField" desc = "" +[[variables.multiplicity]] +name = "μ_ARE_BYTES" +type = "BaseField" +desc = "" + [[variables.multiplicity]] name = "μ_IS_HALF" type = "BaseField" @@ -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" diff --git a/spec/src/branch.toml b/spec/src/branch.toml index a98974678..49a7833a3 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -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" diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index a455b854f..f2131d729 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -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]] diff --git a/spec/src/is_byte.toml b/spec/src/is_byte.toml new file mode 100644 index 000000000..c9f8ee363 --- /dev/null +++ b/spec/src/is_byte.toml @@ -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"] +multiplicity = "cond" +ref = "isbyte:c:isbyte" diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml index 548cb5151..d41b7c472 100644 --- a/spec/src/keccak_round.toml +++ b/spec/src/keccak_round.toml @@ -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" @@ -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" diff --git a/spec/src/page.toml b/spec/src/page.toml index dff939558..b6247a7c7 100644 --- a/spec/src/page.toml +++ b/spec/src/page.toml @@ -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" diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index 4cd4de9ba..78d022515 100644 --- a/spec/src/sha256.toml +++ b/spec/src/sha256.toml @@ -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" diff --git a/spec/src/sha256msgsched.toml b/spec/src/sha256msgsched.toml index 79664a797..402f7459a 100644 --- a/spec/src/sha256msgsched.toml +++ b/spec/src/sha256msgsched.toml @@ -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" @@ -130,10 +130,10 @@ output = "s1" multiplicity = "μ" [[constraints.calc]] -kind = "interaction" +kind = "template" tag = "IS_BYTE" input = ["carry"] -multiplicity = "μ" +cond = "μ" [[constraints.calc]] kind = "interaction" diff --git a/spec/src/sha256round.toml b/spec/src/sha256round.toml index 8ec93ea36..2469b560c 100644 --- a/spec/src/sha256round.toml +++ b/spec/src/sha256round.toml @@ -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" @@ -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" diff --git a/spec/src/shift.toml b/spec/src/shift.toml index bbe22a5d9..18c03ecad 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -147,7 +147,7 @@ iter = ["i", 0, 3] ref = "shift:a:range_in" [[assumptions]] -desc = "`IS_BYTE[shift]`" +desc = "`IS_BYTE`" ref = "shift:a:range_shift" [[assumptions]] diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index b04b3d561..e93c87b05 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -5,6 +5,13 @@ kind = "template" input = ["BaseField"] cond = "BaseField" +# IS_BYTE +[[signatures]] +tag = "IS_BYTE" +kind = "template" +input = ["BaseField"] +cond = "BaseField" + # cond => ADD [[signatures]] tag = "ADD" @@ -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]]