From 52c45b38258725d691434299a1f8c05a25343722 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 24 Dec 2025 17:47:42 +0100 Subject: [PATCH 01/32] spec: rough draft SHIFT chip --- spec/book.typ | 3 +- spec/shift.typ | 37 ++++++++ spec/src/config.toml | 5 + spec/src/shift.toml | 219 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 263 insertions(+), 1 deletion(-) create mode 100644 spec/shift.typ create mode 100644 spec/src/shift.toml diff --git a/spec/book.typ b/spec/book.typ index f50d7ed29..bf58da7dd 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -6,7 +6,8 @@ #book-meta( title: "Lambda VM specification", summary: [ - #chapter("variables.typ")[Variables] + #chapter("variables.typ")[Variables], + #chapter("shift.typ")[SHIFT chip], ] ) diff --git a/spec/shift.typ b/spec/shift.typ new file mode 100644 index 000000000..c5e3bbbc2 --- /dev/null +++ b/spec/shift.typ @@ -0,0 +1,37 @@ +#import "/book.typ": book-page +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, + render_chip_assumptions +) + +#let config = load_config() +#let chip = load_chip("src/shift.toml", config) + +#show: book-page.with(title: "SHIFT chip") + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) + +// == Assumptions +// #render_chip_assumptions(chip, config) + +== Constraints +#render_constraint_table(chip, config, groups:("defs", )) + +#render_constraint_table(chip, config, groups:("intra_limb_left_shifting", "intra_limb_right_shifting")) + +#render_constraint_table(chip, config, groups:("limb_left_shifting", )) + +// #render_constraint_table(chip, config, groups:("equality", )) + +// #render_constraint_table(chip, config, groups:("abs_diff", )) + +// #render_constraint_table(chip, config, groups:("output", )) diff --git a/spec/src/config.toml b/spec/src/config.toml index 1977b9155..f9b09fb62 100644 --- a/spec/src/config.toml +++ b/spec/src/config.toml @@ -102,6 +102,11 @@ label = "Half[3]" subtypes = ["Half", "Half", "Half"] desc = "Three halfwords" +[[variables.types]] +label = "Half[4]" +subtypes = ["Half", "Half", "Half", "Half"] +desc = "Four halfwords" + [[variables.types]] label = "Half[8]" subtypes = ["Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half"] diff --git a/spec/src/shift.toml b/spec/src/shift.toml new file mode 100644 index 000000000..669292a03 --- /dev/null +++ b/spec/src/shift.toml @@ -0,0 +1,219 @@ +name = "SHIFT" + +# Input + +[[variables.input]] +name = "in" +type = "DWordHL" +desc = "The word being shifted" + +[[variables.input]] +name = "shift" +type = "BaseField" +desc = "Number of bits to shift `in` by." + +[[variables.input]] +name = "direction" +type = "Bit" +desc = "Whether to shift left (0) or right (1)." + +[[variables.input]] +name = "signed" +type = "Bit" +desc = "Whether to interpret `in` as a signed integer." + + +# Output + +[[variables.output]] +name = "shifted" +type = "DWordHL" +desc = "`in <> (shift % 64)`" + + +# Auxiliary +[[variables.auxiliary]] +name = "bit_shift" +type = "Byte" +desc = "`shift && 0x0F`" + +[[variables.auxiliary]] +name = "limb_shift_odd" +type = "Byte" +desc = "`shift && 0x10`" + +[[variables.auxiliary]] +name = "limb_shift_even" +type = "Byte" +desc = "`shift && 0x20`" + +[[variables.auxiliary]] +name = "bit_shifted_uncarried" +type = "Half[4]" +desc = "result of left/right shifting the individual limbs of `in` by `bit_shift`, i.e., without the carry values." + +[[variables.auxiliary]] +name = "carry" +type = "Half[3]" +desc = "the carry values left/right shifting `in` by `bit_shift`. Note: one fewer limb is needed, since the last carry is shifted off." + +# Virtual + +[[variables.virtual]] +name = "left" +type = "Bit" +desc = "Whether to perform a left-shift." +poly = ["not", "direction"] + +[[variables.virtual]] +name = "right" +type = "Bit" +desc = "Whether to perform a right-shift." +poly = "direction" + +[[variables.virtual]] +name = "bit_shifted" +type = "DWordHL" +desc = "`in <> (shift % 16)`" +poly = ["+", ["idx", "bit_shifted_uncarried", "i"], ["idx", "carry", "i"]] + +# Multiplicities + +[[variables.multiplicity]] +name = "μ" +type = "Bit" +desc = "" + + + + +# Constraints + +[[constraint_groups]] +name = "defs" + +[[constraints.defs]] +kind = "interaction" +tag = "AND_BYTE" +input = ["shift", "0x0F"] +output = "bit_shift" +ref = "shift:c:bit_shift" +multiplicity = "μ" + +[[constraints.defs]] +kind = "interaction" +tag = "AND_BYTE" +input = ["shift", "0x10"] +output = "limb_shift_odd" +ref = "shift:c:limb_shift_odd" +multiplicity = "μ" + +[[constraints.defs]] +kind = "interaction" +tag = "AND_BYTE" +input = ["shift", "0x20"] +output = "limb_shift_even" +ref = "shift:c:limb_shift_even" +multiplicity = "μ" + + +[[constraint_groups]] +name = "intra_limb_left_shifting" + +[[constraints.intra_limb_left_shifting]] +kind = "interaction" +tag = "HWSL" +input = [["idx", "in", "i"], "bit_shift"] +output = ["idx", "bit_shifted_uncarried", "i"] +range = ["i", 0, 3] +multiplicity = "μ - direction" +ref = "shift:c:hwsl" + + +[[constraints.intra_limb_left_shifting]] +kind = "interaction" +tag = "HWSLC" +input = [["idx", "in", "i"], "bit_shift"] +output = ["idx", "carry", "i"] +range = ["i", 0, 2] +multiplicity = "μ - direction" +ref = "shift:c:hwsl" + +[[constraints.intra_limb_left_shifting]] +kind = "arith" +constraint = "$#`left` => #`carry[3]` = 0$" +poly = ["*", "left", ["idx", "carry", 3]] +ref = "shift:c:left_zero_carry" + + +[[constraint_groups]] +name = "intra_limb_right_shifting" + +[[constraints.intra_limb_right_shifting]] +kind = "interaction" +tag = "HWSR" +input = [["idx", "in", "i"], "bit_shift"] +output = ["idx", "bit_shifted_uncarried", "i"] +range = ["i", 0, 3] +multiplicity = "direction" +ref = "shift:c:hwsr" + +[[constraints.intra_limb_right_shifting]] +kind = "interaction" +tag = "HWSRC" +input = [["idx", "in", "i"], "bit_shift"] +output = ["idx", "carry", "i"] +range = ["i", 1, 3] +multiplicity = "direction" +ref = "shift:c:hwsrc" + +[[constraints.intra_limb_right_shifting]] +kind = "arith" +constraint = "$#`left` => #`carry[0]` = 0$" +poly = ["*", "left", ["idx", "carry", 0]] +ref = "shift:c:right_zero_carry" + + +[[constraint_groups]] +name = "limb_left_shifting" + +[[constraints.limb_left_shifting]] +kind = "arith" +constraint = "$#`left` and #`!limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i]`$" +poly = ["*", "left", ["-", 16, "limb_shift_odd"], ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i"]]] +range = ["i", 0, 3] + +[[constraints.limb_left_shifting]] +kind = "arith" +constraint = "$#`left` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i-1]`$" +poly = ["*", "left", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i-1"]]] +range = ["i", 1, 3] + +[[constraints.limb_left_shifting]] +kind = "arith" +constraint = "$#`left` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[0]` = 0$" +poly = ["*", "left", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["idx", "shifted", 0]] + +[[constraints.limb_left_shifting]] +kind = "arith" +constraint = "$#`left` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`bit_shifted[i-2]`$" +poly = ["*", "left", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i-2"]]] +range = ["i", 2, 3] + +[[constraints.limb_left_shifting]] +kind = "arith" +constraint = "$#`left` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = 0$" +poly = ["*", "left", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["idx", "shifted", "i"]] +range = ["i", 0, 2] + + +[[constraints.limb_left_shifting]] +kind = "arith" +constraint = "$#`left` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[3]` = #`bit_shifted[0]`$" +poly = ["*", "left", "limb_shift_odd", "limb_shift_even", ["-", ["idx", "shifted", 3], ["idx", "bit_shifted", 0]]] + +[[constraints.limb_left_shifting]] +kind = "arith" +constraint = "$#`left` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = 0$" +poly = ["*", "left", "limb_shift_odd", "limb_shift_even", ["idx", "shifted", "i"]] +range = ["i", 0, 3] \ No newline at end of file From 7b5721b6d0fe9ffa119baac755fb21b52de811d7 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 29 Dec 2025 15:36:58 +0100 Subject: [PATCH 02/32] various minor fixes --- spec/src/shift.toml | 46 ++++++++++++++++++++++++--------------------- 1 file changed, 25 insertions(+), 21 deletions(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 669292a03..c2c6dd332 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -54,8 +54,8 @@ desc = "result of left/right shifting the individual limbs of `in` by `bit_shift [[variables.auxiliary]] name = "carry" -type = "Half[3]" -desc = "the carry values left/right shifting `in` by `bit_shift`. Note: one fewer limb is needed, since the last carry is shifted off." +type = "Half[4]" +desc = "the carry values of left/right shifting `in` by `bit_shift`." # Virtual @@ -63,7 +63,7 @@ desc = "the carry values left/right shifting `in` by `bit_shift`. Note: one fewe name = "left" type = "Bit" desc = "Whether to perform a left-shift." -poly = ["not", "direction"] +poly = ["-", "μ", "direction"] [[variables.virtual]] name = "right" @@ -116,6 +116,12 @@ output = "limb_shift_even" ref = "shift:c:limb_shift_even" multiplicity = "μ" +[[constraints.defs]] +kind = "arith" +constraint = "$#`direction` => #`μ`$" +poly = ["*", "direction", ["-", 1, "μ"]] +ref = "shift:c:direction_implies_mu" + [[constraint_groups]] name = "intra_limb_left_shifting" @@ -126,23 +132,22 @@ tag = "HWSL" input = [["idx", "in", "i"], "bit_shift"] output = ["idx", "bit_shifted_uncarried", "i"] range = ["i", 0, 3] -multiplicity = "μ - direction" +multiplicity = "left" ref = "shift:c:hwsl" - [[constraints.intra_limb_left_shifting]] kind = "interaction" tag = "HWSLC" -input = [["idx", "in", "i"], "bit_shift"] +input = [["idx", "in", ["-", "i", 1]], "bit_shift"] output = ["idx", "carry", "i"] -range = ["i", 0, 2] -multiplicity = "μ - direction" +range = ["i", 1, 3] +multiplicity = "left" ref = "shift:c:hwsl" [[constraints.intra_limb_left_shifting]] kind = "arith" -constraint = "$#`left` => #`carry[3]` = 0$" -poly = ["*", "left", ["idx", "carry", 3]] +constraint = "$#`left` => #`carry[0]` = 0$" +poly = ["*", "left", ["idx", "carry", 0]] ref = "shift:c:left_zero_carry" @@ -155,22 +160,22 @@ tag = "HWSR" input = [["idx", "in", "i"], "bit_shift"] output = ["idx", "bit_shifted_uncarried", "i"] range = ["i", 0, 3] -multiplicity = "direction" +multiplicity = "right" ref = "shift:c:hwsr" [[constraints.intra_limb_right_shifting]] kind = "interaction" tag = "HWSRC" -input = [["idx", "in", "i"], "bit_shift"] +input = [["idx", "in", ["+", "i", 1]], "bit_shift"] output = ["idx", "carry", "i"] -range = ["i", 1, 3] -multiplicity = "direction" +range = ["i", 0, 2] +multiplicity = "right" ref = "shift:c:hwsrc" [[constraints.intra_limb_right_shifting]] kind = "arith" -constraint = "$#`left` => #`carry[0]` = 0$" -poly = ["*", "left", ["idx", "carry", 0]] +constraint = "$#`right` => #`carry[3]` = 0$" +poly = ["*", "right", ["idx", "carry", 3]] ref = "shift:c:right_zero_carry" @@ -186,7 +191,7 @@ range = ["i", 0, 3] [[constraints.limb_left_shifting]] kind = "arith" constraint = "$#`left` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i-1]`$" -poly = ["*", "left", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i-1"]]] +poly = ["*", "left", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 1]]]] range = ["i", 1, 3] [[constraints.limb_left_shifting]] @@ -197,15 +202,14 @@ poly = ["*", "left", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["idx", "sh [[constraints.limb_left_shifting]] kind = "arith" constraint = "$#`left` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`bit_shifted[i-2]`$" -poly = ["*", "left", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i-2"]]] +poly = ["*", "left", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] range = ["i", 2, 3] [[constraints.limb_left_shifting]] kind = "arith" constraint = "$#`left` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = 0$" poly = ["*", "left", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["idx", "shifted", "i"]] -range = ["i", 0, 2] - +range = ["i", 0, 1] [[constraints.limb_left_shifting]] kind = "arith" @@ -216,4 +220,4 @@ poly = ["*", "left", "limb_shift_odd", "limb_shift_even", ["-", ["idx", "shifted kind = "arith" constraint = "$#`left` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = 0$" poly = ["*", "left", "limb_shift_odd", "limb_shift_even", ["idx", "shifted", "i"]] -range = ["i", 0, 3] \ No newline at end of file +range = ["i", 0, 2] \ No newline at end of file From 4bf57b36ac60fb8662b53ebb7045cba175f64891 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 29 Dec 2025 16:26:41 +0100 Subject: [PATCH 03/32] implement right-limb shifting --- spec/shift.typ | 13 +++---- spec/src/shift.toml | 85 ++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 84 insertions(+), 14 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index c5e3bbbc2..3ac43b585 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -5,7 +5,7 @@ total_nr_variables, total_nr_instantiated_columns, render_constraint_table, - render_chip_assumptions + render_chip_assumptions, ) #let config = load_config() @@ -24,11 +24,12 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed usin // #render_chip_assumptions(chip, config) == Constraints -#render_constraint_table(chip, config, groups:("defs", )) - -#render_constraint_table(chip, config, groups:("intra_limb_left_shifting", "intra_limb_right_shifting")) - -#render_constraint_table(chip, config, groups:("limb_left_shifting", )) +#render_constraint_table(chip, config, groups: "defs") +#render_constraint_table(chip, config, groups: "intra_limb_left_shifting") +#render_constraint_table(chip, config, groups: "intra_limb_right_shifting") +#render_constraint_table(chip, config, groups: "limb_shifting") +#render_constraint_table(chip, config, groups: "limb_left_shifting") +#render_constraint_table(chip, config, groups: "limb_right_shifting") // #render_constraint_table(chip, config, groups:("equality", )) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index c2c6dd332..18727a855 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -57,6 +57,16 @@ name = "carry" type = "Half[4]" desc = "the carry values of left/right shifting `in` by `bit_shift`." +[[variables.auxiliary]] +name = "msb" +type = "Bit" +desc = "the most significant bit of `in`." + +[[variables.auxiliary]] +name = "extension" +type = "Half" +desc = "sign extension of `in`." + # Virtual [[variables.virtual]] @@ -116,6 +126,7 @@ output = "limb_shift_even" ref = "shift:c:limb_shift_even" multiplicity = "μ" + [[constraints.defs]] kind = "arith" constraint = "$#`direction` => #`μ`$" @@ -172,22 +183,42 @@ range = ["i", 0, 2] multiplicity = "right" ref = "shift:c:hwsrc" +[[constraints.intra_limb_right_shifting]] +kind = "interaction" +tag = "MSB16" +input = [["idx", "in", 3]] +output = "msb" +multiplicity = "right" +ref = "shift:c:msb" + [[constraints.intra_limb_right_shifting]] kind = "arith" -constraint = "$#`right` => #`carry[3]` = 0$" -poly = ["*", "right", ["idx", "carry", 3]] -ref = "shift:c:right_zero_carry" +constraint = "$#`extension` = 65535 dot #`signed` dot #`msb`$" +poly = ["-", "extension", ["*", 65535, "signed", "msb"]] +ref = "shift:c:extension" + +[[constraints.intra_limb_right_shifting]] +kind = "interaction" +tag = "HWSRC" +input = ["extension", "bit_shift"] +output = ["idx", "carry", 3] +multiplicity = "right" +ref = "shift:c:right_sign_extend" [[constraint_groups]] -name = "limb_left_shifting" +name = "limb_shifting" -[[constraints.limb_left_shifting]] +[[constraints.limb_shifting]] kind = "arith" -constraint = "$#`left` and #`!limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i]`$" -poly = ["*", "left", ["-", 16, "limb_shift_odd"], ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i"]]] +constraint = "$#`!limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i]`$" +poly = ["*", ["-", 16, "limb_shift_odd"], ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i"]]] range = ["i", 0, 3] + +[[constraint_groups]] +name = "limb_left_shifting" + [[constraints.limb_left_shifting]] kind = "arith" constraint = "$#`left` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i-1]`$" @@ -220,4 +251,42 @@ poly = ["*", "left", "limb_shift_odd", "limb_shift_even", ["-", ["idx", "shifted kind = "arith" constraint = "$#`left` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = 0$" poly = ["*", "left", "limb_shift_odd", "limb_shift_even", ["idx", "shifted", "i"]] -range = ["i", 0, 2] \ No newline at end of file +range = ["i", 0, 2] + + +[[constraint_groups]] +name = "limb_right_shifting" + +[[constraints.limb_right_shifting]] +kind = "arith" +constraint = "$#`right` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i+1]`$" +poly = ["*", "right", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["+", "i", 1]]]] +range = ["i", 0, 2] + +[[constraints.limb_right_shifting]] +kind = "arith" +constraint = "$#`right` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[3]` = #`extension`$" +poly = ["*", "right", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", 3], "extension"]] + +[[constraints.limb_right_shifting]] +kind = "arith" +constraint = "$#`right` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`bit_shifted[i+2]`$" +poly = ["*", "right", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] +range = ["i", 0, 1] + +[[constraints.limb_right_shifting]] +kind = "arith" +constraint = "$#`right` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`extension`$" +poly = ["*", "right", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["-", ["idx", "shifted", "i"], "extension"]] +range = ["i", 2, 3] + +[[constraints.limb_right_shifting]] +kind = "arith" +constraint = "$#`right` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[0]` = #`bit_shifted[3]`$" +poly = ["*", "right", "limb_shift_odd", "limb_shift_even", ["-", ["idx", "shifted", 0], ["idx", "bit_shifted", 3]]] + +[[constraints.limb_right_shifting]] +kind = "arith" +constraint = "$#`right` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`extension`$" +poly = ["*", "right", "limb_shift_odd", "limb_shift_even", ["-", ["idx", "shifted", "i"], "extension"]] +range = ["i", 1, 3] \ No newline at end of file From c9c0d8b0d6140be961cd695b262bc0b39c311d6c Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 29 Dec 2025 16:48:11 +0100 Subject: [PATCH 04/32] Update rendering "polynomial constriant" in table --- spec/chip.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/chip.typ b/spec/chip.typ index c694db90a..e3123f4f9 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -135,7 +135,7 @@ } (..for poly in polys { - ([_polynomial constraint_], [], $#expr_to_math(poly) = 0$, []) + (table.cell(colspan: 2, align: right, emph("polynomial constraint")), $#expr_to_math(poly) = 0$, []) },) } From c2ba8fe095d8cf738653bde226cba4359921e143 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 29 Dec 2025 16:53:13 +0100 Subject: [PATCH 05/32] fix degree 4 issues --- spec/src/shift.toml | 82 +++++++++++++++++++++++++++++++-------------- 1 file changed, 57 insertions(+), 25 deletions(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 18727a855..6ba61178b 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -67,6 +67,21 @@ name = "extension" type = "Half" desc = "sign extension of `in`." +[[variables.auxiliary]] +name = "shift_1_limb" +type = "Half" +desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 1 mod 4$." + +[[variables.auxiliary]] +name = "shift_2_limbs" +type = "Half" +desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 2 mod 4$." + +[[variables.auxiliary]] +name = "shift_3_limbs" +type = "Half" +desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 3 mod 4$." + # Virtual [[variables.virtual]] @@ -126,13 +141,30 @@ output = "limb_shift_even" ref = "shift:c:limb_shift_even" multiplicity = "μ" - [[constraints.defs]] kind = "arith" constraint = "$#`direction` => #`μ`$" poly = ["*", "direction", ["-", 1, "μ"]] ref = "shift:c:direction_implies_mu" +[[constraints.defs]] +kind = "arith" +constraint = "$#`shift_1_limb` = #`limb_shift_odd` dot (32 - #`limb_shift_even`)$" +poly = ["-", "shift_1_limb", ["*", "limb_shift_odd", ["-", 32, "limb_shift_even"]]] +ref = "shift:c:shift_1_limb" + +[[constraints.defs]] +kind = "arith" +constraint = "$#`shift_2_limbs` = (16 - #`limb_shift_odd`) dot #`limb_shift_even`$" +poly = ["-", "shift_2_limbs", ["*", ["-", 16, "limb_shift_odd"], "limb_shift_even"]] +ref = "shift:c:shift_2_limbs" + +[[constraints.defs]] +kind = "arith" +constraint = "$#`shift_3_limbs` = #`limb_shift_odd` dot #`limb_shift_even`$" +poly = ["-", "shift_3_limbs", ["*", "limb_shift_odd", "limb_shift_even"]] +ref = "shift:c:shift_3_limbs" + [[constraint_groups]] name = "intra_limb_left_shifting" @@ -221,36 +253,36 @@ name = "limb_left_shifting" [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i-1]`$" -poly = ["*", "left", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 1]]]] +constraint = "$#`left` and #`shift_1_limb` => #`shifted[i]` = #`bit_shifted[i-1]`$" +poly = ["*", "left", "shift_1_limb", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 1]]]] range = ["i", 1, 3] [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[0]` = 0$" -poly = ["*", "left", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["idx", "shifted", 0]] +constraint = "$#`left` and #`shift_1_limb` => #`shifted[0]` = 0$" +poly = ["*", "left", "shift_1_limb", ["idx", "shifted", 0]] [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`bit_shifted[i-2]`$" -poly = ["*", "left", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] +constraint = "$#`left` and #`shift_2_limbs` => #`shifted[i]` = #`bit_shifted[i-2]`$" +poly = ["*", "left", "shift_2_limbs", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] range = ["i", 2, 3] [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = 0$" -poly = ["*", "left", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["idx", "shifted", "i"]] +constraint = "$#`left` and #`shift_2_limbs` => #`shifted[i]` = 0$" +poly = ["*", "left", "shift_2_limbs", ["idx", "shifted", "i"]] range = ["i", 0, 1] [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[3]` = #`bit_shifted[0]`$" -poly = ["*", "left", "limb_shift_odd", "limb_shift_even", ["-", ["idx", "shifted", 3], ["idx", "bit_shifted", 0]]] +constraint = "$#`left` and #`shift_3_limbs` => #`shifted[3]` = #`bit_shifted[0]`$" +poly = ["*", "left", "shift_3_limbs", ["-", ["idx", "shifted", 3], ["idx", "bit_shifted", 0]]] [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = 0$" -poly = ["*", "left", "limb_shift_odd", "limb_shift_even", ["idx", "shifted", "i"]] +constraint = "$#`left` and #`shift_3_limbs` => #`shifted[i]` = 0$" +poly = ["*", "left", "shift_3_limbs", ["idx", "shifted", "i"]] range = ["i", 0, 2] @@ -259,34 +291,34 @@ name = "limb_right_shifting" [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i+1]`$" -poly = ["*", "right", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["+", "i", 1]]]] +constraint = "$#`right` and #`shift_1_limb` => #`shifted[i]` = #`bit_shifted[i+1]`$" +poly = ["*", "right", "shift_1_limb", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["+", "i", 1]]]] range = ["i", 0, 2] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`limb_shift_odd` and #`!limb_shift_even` => #`shifted[3]` = #`extension`$" -poly = ["*", "right", "limb_shift_odd", ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", 3], "extension"]] +constraint = "$#`right` and #`shift_1_limb` => #`shifted[3]` = #`extension`$" +poly = ["*", "right", "shift_1_limb", ["-", ["idx", "shifted", 3], "extension"]] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`bit_shifted[i+2]`$" -poly = ["*", "right", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] +constraint = "$#`right` and #`shift_2_limbs` => #`shifted[i]` = #`bit_shifted[i+2]`$" +poly = ["*", "right", "shift_2_limbs", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] range = ["i", 0, 1] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`!limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`extension`$" -poly = ["*", "right", ["-", 16, "limb_shift_odd"], "limb_shift_even", ["-", ["idx", "shifted", "i"], "extension"]] +constraint = "$#`right` and #`shift_2_limbs` => #`shifted[i]` = #`extension`$" +poly = ["*", "right", "shift_2_limbs", ["-", ["idx", "shifted", "i"], "extension"]] range = ["i", 2, 3] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[0]` = #`bit_shifted[3]`$" -poly = ["*", "right", "limb_shift_odd", "limb_shift_even", ["-", ["idx", "shifted", 0], ["idx", "bit_shifted", 3]]] +constraint = "$#`right` and #`shift_3_limbs` => #`shifted[0]` = #`bit_shifted[3]`$" +poly = ["*", "right", "shift_3_limbs", ["-", ["idx", "shifted", 0], ["idx", "bit_shifted", 3]]] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`limb_shift_odd` and #`limb_shift_even` => #`shifted[i]` = #`extension`$" -poly = ["*", "right", "limb_shift_odd", "limb_shift_even", ["-", ["idx", "shifted", "i"], "extension"]] +constraint = "$#`right` and #`shift_3_limbs` => #`shifted[i]` = #`extension`$" +poly = ["*", "right", "shift_3_limbs", ["-", ["idx", "shifted", "i"], "extension"]] range = ["i", 1, 3] \ No newline at end of file From bec746fad7d86e1a2a1ae3ad8b31118ca9e22c77 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 29 Dec 2025 17:55:29 +0100 Subject: [PATCH 06/32] Further update to SHIFT chip --- spec/shift.typ | 37 +++++++++++--- spec/src/shift.toml | 118 +++++++++++++++++++++++--------------------- 2 files changed, 91 insertions(+), 64 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 3ac43b585..86f1bd798 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -13,7 +13,10 @@ #show: book-page.with(title: "SHIFT chip") -== Columns + +#outline() + += Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) @@ -23,16 +26,36 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed usin // == Assumptions // #render_chip_assumptions(chip, config) -== Constraints += Constraints +== Definitions +For starters, constrain the auxiliary variables `bit_shift`, `limb_shift_odd`, `limb_shift_even`, `limb_shift_1`, `limb_shift_2` and `limb_shift_3` according to their definitions. #render_constraint_table(chip, config, groups: "defs") +*Implementation note*: one could remove the $1/512$ factor listed in the definitions of `limb_shift_1`, `limb_shift_2` and `limb_shift_3`. +While this would mean that the three are no longer `Bit`s, this fact does not impact the correctness of the chip: all constraints using these variables only require the variables to be _non-zero_, not specifically $1$. + +== Left shifting +Shifting (both left and right) is achieved in a two-step process: first, shift `in` by `bit_shift`, and then shift the limbs in `bit_shift` the required number of full limbs to form the `shifted` output. +Since left shifting does not need to concern itself with the signedness of `in`, it is slightly more straightforward, and therefore treated first. + #render_constraint_table(chip, config, groups: "intra_limb_left_shifting") -#render_constraint_table(chip, config, groups: "intra_limb_right_shifting") + +When $floor.l #`bit_shift`/16 floor.r = 0 mod 4$, `bit_shifted` already contains the output. +As such, it suffices to set require `bit_shifted` and `shifted`. +This holds irrespective of whether we are shifting `left` or `right`. #render_constraint_table(chip, config, groups: "limb_shifting") + +When $floor.l #`bit_shift`/16 floor.r eq.not 0 mod 4$, the limbs in `bit_shifted` need to be shifted over by a multiple of 16 bits to form `shifted`. +This exact number is indicated by the variables `limb_shift_1`, `limb_shift_2`, and `limb_shift_3`. +By construction, exactly one of the three is $1$, while the other two are $0$. +In the following, each case is given its own separate set of constraints. +Here, the limbs in `shifted` are constrained to match those of `bit_shift`, shifted over by the number specified by `limb_shift_x`. #render_constraint_table(chip, config, groups: "limb_left_shifting") -#render_constraint_table(chip, config, groups: "limb_right_shifting") -// #render_constraint_table(chip, config, groups:("equality", )) +To complete the output, the lower bits of `shifted` are set to zero, based on the number of limbs `bit_shifted` is shifted over to form `shifted`. +#render_constraint_table(chip, config, groups: "limb_left_shifting_zero") -// #render_constraint_table(chip, config, groups:("abs_diff", )) +== Right shifting -// #render_constraint_table(chip, config, groups:("output", )) +#render_constraint_table(chip, config, groups: "intra_limb_right_shifting") +#render_constraint_table(chip, config, groups: "limb_right_shifting") +#render_constraint_table(chip, config, groups: "limb_right_shifting_extension") diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 6ba61178b..14648a082 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -68,18 +68,18 @@ type = "Half" desc = "sign extension of `in`." [[variables.auxiliary]] -name = "shift_1_limb" -type = "Half" +name = "limb_shift_1" +type = "Bit" desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 1 mod 4$." [[variables.auxiliary]] -name = "shift_2_limbs" -type = "Half" +name = "limb_shift_2" +type = "Bit" desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 2 mod 4$." [[variables.auxiliary]] -name = "shift_3_limbs" -type = "Half" +name = "limb_shift_3" +type = "Bit" desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 3 mod 4$." # Virtual @@ -143,27 +143,21 @@ multiplicity = "μ" [[constraints.defs]] kind = "arith" -constraint = "$#`direction` => #`μ`$" -poly = ["*", "direction", ["-", 1, "μ"]] -ref = "shift:c:direction_implies_mu" +constraint = "$#`limb_shift_1` = (#`limb_shift_odd` dot (32 - #`limb_shift_even`)) / 512$" +poly = ["-", "limb_shift_1", ["/", ["*", "limb_shift_odd", ["-", 32, "limb_shift_even"]], 512]] +ref = "shift:c:limb_shift_1" [[constraints.defs]] kind = "arith" -constraint = "$#`shift_1_limb` = #`limb_shift_odd` dot (32 - #`limb_shift_even`)$" -poly = ["-", "shift_1_limb", ["*", "limb_shift_odd", ["-", 32, "limb_shift_even"]]] -ref = "shift:c:shift_1_limb" +constraint = "$#`limb_shift_2` = ((16 - #`limb_shift_odd`) dot #`limb_shift_even`) / 512$" +poly = ["-", "limb_shift_2", ["/", ["*", ["-", 16, "limb_shift_odd"], "limb_shift_even"], 512]] +ref = "shift:c:limb_shift_2" [[constraints.defs]] kind = "arith" -constraint = "$#`shift_2_limbs` = (16 - #`limb_shift_odd`) dot #`limb_shift_even`$" -poly = ["-", "shift_2_limbs", ["*", ["-", 16, "limb_shift_odd"], "limb_shift_even"]] -ref = "shift:c:shift_2_limbs" - -[[constraints.defs]] -kind = "arith" -constraint = "$#`shift_3_limbs` = #`limb_shift_odd` dot #`limb_shift_even`$" -poly = ["-", "shift_3_limbs", ["*", "limb_shift_odd", "limb_shift_even"]] -ref = "shift:c:shift_3_limbs" +constraint = "$#`limb_shift_3` = (#`limb_shift_odd` dot #`limb_shift_even`) / 512$" +poly = ["-", "limb_shift_3", ["/", ["*", "limb_shift_odd", "limb_shift_even"], 512]] +ref = "shift:c:limb_shift_3" [[constraint_groups]] @@ -187,6 +181,12 @@ range = ["i", 1, 3] multiplicity = "left" ref = "shift:c:hwsl" +[[constraints.intra_limb_left_shifting]] +kind = "arith" +constraint = "$#`direction` => #`μ`$" +poly = ["*", "direction", ["-", 1, "μ"]] +ref = "shift:c:direction_implies_mu" + [[constraints.intra_limb_left_shifting]] kind = "arith" constraint = "$#`left` => #`carry[0]` = 0$" @@ -253,37 +253,40 @@ name = "limb_left_shifting" [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`shift_1_limb` => #`shifted[i]` = #`bit_shifted[i-1]`$" -poly = ["*", "left", "shift_1_limb", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 1]]]] +constraint = "$#`left` and #`limb_shift_1` => #`shifted[i]` = #`bit_shifted[i-1]`$" +poly = ["*", "left", "limb_shift_1", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 1]]]] range = ["i", 1, 3] -[[constraints.limb_left_shifting]] -kind = "arith" -constraint = "$#`left` and #`shift_1_limb` => #`shifted[0]` = 0$" -poly = ["*", "left", "shift_1_limb", ["idx", "shifted", 0]] [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`shift_2_limbs` => #`shifted[i]` = #`bit_shifted[i-2]`$" -poly = ["*", "left", "shift_2_limbs", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] +constraint = "$#`left` and #`limb_shift_2` => #`shifted[i]` = #`bit_shifted[i-2]`$" +poly = ["*", "left", "limb_shift_2", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] range = ["i", 2, 3] + [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`shift_2_limbs` => #`shifted[i]` = 0$" -poly = ["*", "left", "shift_2_limbs", ["idx", "shifted", "i"]] -range = ["i", 0, 1] +constraint = "$#`left` and #`limb_shift_3` => #`shifted[3]` = #`bit_shifted[0]`$" +poly = ["*", "left", "limb_shift_3", ["-", ["idx", "shifted", 3], ["idx", "bit_shifted", 0]]] -[[constraints.limb_left_shifting]] +[[constraint_groups]] +name = "limb_left_shifting_zero" + +[[constraints.limb_left_shifting_zero]] kind = "arith" -constraint = "$#`left` and #`shift_3_limbs` => #`shifted[3]` = #`bit_shifted[0]`$" -poly = ["*", "left", "shift_3_limbs", ["-", ["idx", "shifted", 3], ["idx", "bit_shifted", 0]]] +constraint = "$#`left` and (#`limb_shift_1` or #`limb_shift_2` or #`limb_shift_3`) => #`shifted[0]` = 0$" +poly = ["*", "left", ["+", "limb_shift_1", "limb_shift_2", "limb_shift_3"], ["idx", "shifted", 0]] -[[constraints.limb_left_shifting]] +[[constraints.limb_left_shifting_zero]] kind = "arith" -constraint = "$#`left` and #`shift_3_limbs` => #`shifted[i]` = 0$" -poly = ["*", "left", "shift_3_limbs", ["idx", "shifted", "i"]] -range = ["i", 0, 2] +constraint = "$#`left` and (#`limb_shift_2` or #`limb_shift_3`) => #`shifted[1]` = 0$" +poly = ["*", "left", ["+", "limb_shift_2", "limb_shift_3"], ["idx", "shifted", 1]] + +[[constraints.limb_left_shifting_zero]] +kind = "arith" +constraint = "$#`left` and #`limb_shift_3` => #`shifted[2]` = 0$" +poly = ["*", "left", "limb_shift_3", ["idx", "shifted", 2]] [[constraint_groups]] @@ -291,34 +294,35 @@ name = "limb_right_shifting" [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`shift_1_limb` => #`shifted[i]` = #`bit_shifted[i+1]`$" -poly = ["*", "right", "shift_1_limb", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["+", "i", 1]]]] +constraint = "$#`right` and #`limb_shift_1` => #`shifted[i]` = #`bit_shifted[i+1]`$" +poly = ["*", "right", "limb_shift_1", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["+", "i", 1]]]] range = ["i", 0, 2] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`shift_1_limb` => #`shifted[3]` = #`extension`$" -poly = ["*", "right", "shift_1_limb", ["-", ["idx", "shifted", 3], "extension"]] +constraint = "$#`right` and #`limb_shift_2` => #`shifted[i]` = #`bit_shifted[i+2]`$" +poly = ["*", "right", "limb_shift_2", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] +range = ["i", 0, 1] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`shift_2_limbs` => #`shifted[i]` = #`bit_shifted[i+2]`$" -poly = ["*", "right", "shift_2_limbs", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] -range = ["i", 0, 1] +constraint = "$#`right` and #`limb_shift_3` => #`shifted[0]` = #`bit_shifted[3]`$" +poly = ["*", "right", "limb_shift_3", ["-", ["idx", "shifted", 0], ["idx", "bit_shifted", 3]]] -[[constraints.limb_right_shifting]] +[[constraint_groups]] +name = "limb_right_shifting_extension" + +[[constraints.limb_right_shifting_extension]] kind = "arith" -constraint = "$#`right` and #`shift_2_limbs` => #`shifted[i]` = #`extension`$" -poly = ["*", "right", "shift_2_limbs", ["-", ["idx", "shifted", "i"], "extension"]] -range = ["i", 2, 3] +constraint = "$#`right` and (#`limb_shift_1` or #`limb_shift_2` or #`limb_shift_3`) => #`shifted[3]` = #`extension`$" +poly = ["*", "right", ["+", "limb_shift_1", "limb_shift_2", "limb_shift_3"], ["-", ["idx", "shifted", 3], "extension"]] -[[constraints.limb_right_shifting]] +[[constraints.limb_right_shifting_extension]] kind = "arith" -constraint = "$#`right` and #`shift_3_limbs` => #`shifted[0]` = #`bit_shifted[3]`$" -poly = ["*", "right", "shift_3_limbs", ["-", ["idx", "shifted", 0], ["idx", "bit_shifted", 3]]] +constraint = "$#`right` and (#`limb_shift_2` or #`limb_shift_3`) => #`shifted[2]` = #`extension`$" +poly = ["*", "right", ["+", "limb_shift_2", "limb_shift_3"], ["-", ["idx", "shifted", 2], "extension"]] -[[constraints.limb_right_shifting]] +[[constraints.limb_right_shifting_extension]] kind = "arith" -constraint = "$#`right` and #`shift_3_limbs` => #`shifted[i]` = #`extension`$" -poly = ["*", "right", "shift_3_limbs", ["-", ["idx", "shifted", "i"], "extension"]] -range = ["i", 1, 3] \ No newline at end of file +constraint = "$#`right` and #`limb_shift_3` => #`shifted[1]` = #`extension`$" +poly = ["*", "right", "limb_shift_3", ["-", ["idx", "shifted", 1], "extension"]] From 2882d42c56cd6006b5f5f2307f7620fd5bd303eb Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 30 Dec 2025 09:18:40 +0100 Subject: [PATCH 07/32] Clean up SHIFT --- spec/shift.typ | 18 +----------------- spec/src/shift.toml | 16 +++++++++++----- 2 files changed, 12 insertions(+), 22 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 86f1bd798..7b0687ea3 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -28,34 +28,18 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed usin = Constraints == Definitions -For starters, constrain the auxiliary variables `bit_shift`, `limb_shift_odd`, `limb_shift_even`, `limb_shift_1`, `limb_shift_2` and `limb_shift_3` according to their definitions. +Constrain the auxiliary variables `bit_shift`, `limb_shift_odd`, `limb_shift_even`, `limb_shift_1`, `limb_shift_2` and `limb_shift_3` according to their definitions. #render_constraint_table(chip, config, groups: "defs") *Implementation note*: one could remove the $1/512$ factor listed in the definitions of `limb_shift_1`, `limb_shift_2` and `limb_shift_3`. While this would mean that the three are no longer `Bit`s, this fact does not impact the correctness of the chip: all constraints using these variables only require the variables to be _non-zero_, not specifically $1$. == Left shifting -Shifting (both left and right) is achieved in a two-step process: first, shift `in` by `bit_shift`, and then shift the limbs in `bit_shift` the required number of full limbs to form the `shifted` output. -Since left shifting does not need to concern itself with the signedness of `in`, it is slightly more straightforward, and therefore treated first. - #render_constraint_table(chip, config, groups: "intra_limb_left_shifting") - -When $floor.l #`bit_shift`/16 floor.r = 0 mod 4$, `bit_shifted` already contains the output. -As such, it suffices to set require `bit_shifted` and `shifted`. -This holds irrespective of whether we are shifting `left` or `right`. #render_constraint_table(chip, config, groups: "limb_shifting") - -When $floor.l #`bit_shift`/16 floor.r eq.not 0 mod 4$, the limbs in `bit_shifted` need to be shifted over by a multiple of 16 bits to form `shifted`. -This exact number is indicated by the variables `limb_shift_1`, `limb_shift_2`, and `limb_shift_3`. -By construction, exactly one of the three is $1$, while the other two are $0$. -In the following, each case is given its own separate set of constraints. -Here, the limbs in `shifted` are constrained to match those of `bit_shift`, shifted over by the number specified by `limb_shift_x`. #render_constraint_table(chip, config, groups: "limb_left_shifting") - -To complete the output, the lower bits of `shifted` are set to zero, based on the number of limbs `bit_shifted` is shifted over to form `shifted`. #render_constraint_table(chip, config, groups: "limb_left_shifting_zero") == Right shifting - #render_constraint_table(chip, config, groups: "intra_limb_right_shifting") #render_constraint_table(chip, config, groups: "limb_right_shifting") #render_constraint_table(chip, config, groups: "limb_right_shifting_extension") diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 14648a082..fa14704ce 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -84,6 +84,12 @@ desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 3 mod 4$." # Virtual +[[variables.virtual]] +name = "limb_shift_0" +type = "Bit" +desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 0 mod 4$." +poly = ["/", ["*", ["-", 16, "limb_shift_odd"], ["-", 32, "limb_shift_even"]], 512] + [[variables.virtual]] name = "left" type = "Bit" @@ -144,19 +150,19 @@ multiplicity = "μ" [[constraints.defs]] kind = "arith" constraint = "$#`limb_shift_1` = (#`limb_shift_odd` dot (32 - #`limb_shift_even`)) / 512$" -poly = ["-", "limb_shift_1", ["/", ["*", "limb_shift_odd", ["-", 32, "limb_shift_even"]], 512]] +poly = ["-", ["*", 512, "limb_shift_1"], ["*", "limb_shift_odd", ["-", 32, "limb_shift_even"]]] ref = "shift:c:limb_shift_1" [[constraints.defs]] kind = "arith" constraint = "$#`limb_shift_2` = ((16 - #`limb_shift_odd`) dot #`limb_shift_even`) / 512$" -poly = ["-", "limb_shift_2", ["/", ["*", ["-", 16, "limb_shift_odd"], "limb_shift_even"], 512]] +poly = ["-", ["*", 512, "limb_shift_2"], ["*", ["-", 16, "limb_shift_odd"], "limb_shift_even"]] ref = "shift:c:limb_shift_2" [[constraints.defs]] kind = "arith" constraint = "$#`limb_shift_3` = (#`limb_shift_odd` dot #`limb_shift_even`) / 512$" -poly = ["-", "limb_shift_3", ["/", ["*", "limb_shift_odd", "limb_shift_even"], 512]] +poly = ["-", ["*", 512, "limb_shift_3"], ["*", "limb_shift_odd", "limb_shift_even"]] ref = "shift:c:limb_shift_3" @@ -243,8 +249,8 @@ name = "limb_shifting" [[constraints.limb_shifting]] kind = "arith" -constraint = "$#`!limb_shift_odd` and #`!limb_shift_even` => #`shifted[i]` = #`bit_shifted[i]`$" -poly = ["*", ["-", 16, "limb_shift_odd"], ["-", 32, "limb_shift_even"], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i"]]] +constraint = "$#`limb_shift_0` => #`shifted[i]` = #`bit_shifted[i]`$" +poly = ["*", "limb_shift_0", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i"]]] range = ["i", 0, 3] From 7484000eb7d0f0397ffb99988e932d94cc979bb1 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 30 Dec 2025 09:24:15 +0100 Subject: [PATCH 08/32] spec/shift: add assumption --- spec/shift.typ | 4 ++-- spec/src/shift.toml | 8 ++++++++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 7b0687ea3..93fca29f4 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -23,8 +23,8 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: #render_chip_column_table(chip, config) -// == Assumptions -// #render_chip_assumptions(chip, config) += Assumptions +#render_chip_assumptions(chip, config) = Constraints == Definitions diff --git a/spec/src/shift.toml b/spec/src/shift.toml index fa14704ce..66aee8557 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -117,6 +117,14 @@ desc = "" +# Assumptions + +[[assumptions]] +desc = "`IS_HALFWORD[in[i]]`" +range = ["i", 0, 3] +ref = "shift:a:range_in" + + # Constraints From f27d16e7f2f82d4e5bc6cee8e9def5b77e55309d Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 30 Dec 2025 10:35:13 +0100 Subject: [PATCH 09/32] spec/shift: Add lookup constraint --- spec/shift.typ | 3 +++ spec/src/shift.toml | 14 ++++++++++++++ 2 files changed, 17 insertions(+) diff --git a/spec/shift.typ b/spec/shift.typ index 93fca29f4..870ea676c 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -43,3 +43,6 @@ While this would mean that the three are no longer `Bit`s, this fact does not im #render_constraint_table(chip, config, groups: "intra_limb_right_shifting") #render_constraint_table(chip, config, groups: "limb_right_shifting") #render_constraint_table(chip, config, groups: "limb_right_shifting_extension") + +== Lookup +#render_constraint_table(chip, config, groups: "lookups") \ No newline at end of file diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 66aee8557..5c59e37a4 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -340,3 +340,17 @@ poly = ["*", "right", ["+", "limb_shift_2", "limb_shift_3"], ["-", ["idx", "shif kind = "arith" constraint = "$#`right` and #`limb_shift_3` => #`shifted[1]` = #`extension`$" poly = ["*", "right", "limb_shift_3", ["-", ["idx", "shifted", 1], "extension"]] + + +# Lookups + +[[constraint_groups]] +name = "lookups" + +[[constraints.lookups]] +kind = "interaction" +tag = "SHIFT" +input = ["in", "shift", "direction", "signed"] +output = "shifted" +multiplicity = "-μ" +ref = "shift:c:lookup" From e18df6003dff1981cef904eaac7e679abd67cd0e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 30 Dec 2025 12:50:28 +0100 Subject: [PATCH 10/32] spec/shift: make extension virtual Kudos to Robin for uncovering this! --- spec/src/shift.toml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 5c59e37a4..f5cdc3225 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -58,14 +58,9 @@ type = "Half[4]" desc = "the carry values of left/right shifting `in` by `bit_shift`." [[variables.auxiliary]] -name = "msb" +name = "is_negative" type = "Bit" -desc = "the most significant bit of `in`." - -[[variables.auxiliary]] -name = "extension" -type = "Half" -desc = "sign extension of `in`." +desc = "whether `in` is negative." [[variables.auxiliary]] name = "limb_shift_1" @@ -90,6 +85,12 @@ type = "Bit" desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 0 mod 4$." poly = ["/", ["*", ["-", 16, "limb_shift_odd"], ["-", 32, "limb_shift_even"]], 512] +[[variables.virtual]] +name = "extension" +type = "Half" +desc = "sign extension of `in`." +poly = ["*", 65535, "is_negative"] + [[variables.virtual]] name = "left" type = "Bit" @@ -233,15 +234,14 @@ ref = "shift:c:hwsrc" kind = "interaction" tag = "MSB16" input = [["idx", "in", 3]] -output = "msb" -multiplicity = "right" -ref = "shift:c:msb" +output = "is_negative" +multiplicity = "signed" +ref = "shift:c:is_negative" [[constraints.intra_limb_right_shifting]] kind = "arith" -constraint = "$#`extension` = 65535 dot #`signed` dot #`msb`$" -poly = ["-", "extension", ["*", 65535, "signed", "msb"]] -ref = "shift:c:extension" +constraint = "$#`!signed` => #`is_negative` = 0$" +poly = ["*", ["-", 1, "signed"], "is_negative"] [[constraints.intra_limb_right_shifting]] kind = "interaction" From dd3df408c1add4da609b924a8958e72ad96b5969 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 30 Dec 2025 13:04:53 +0100 Subject: [PATCH 11/32] spec/shift: Simplify limb-situation Kudos to Robin for pointing this out! --- spec/shift.typ | 4 +-- spec/src/shift.toml | 72 ++++++++++++++++++++------------------------- 2 files changed, 33 insertions(+), 43 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 870ea676c..793bab5a8 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -28,10 +28,8 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed usin = Constraints == Definitions -Constrain the auxiliary variables `bit_shift`, `limb_shift_odd`, `limb_shift_even`, `limb_shift_1`, `limb_shift_2` and `limb_shift_3` according to their definitions. +Constrain the auxiliary variables `bit_shift`, `limb_shift_0`, `limb_shift_1`, `limb_shift_2` and `limb_shift_3` according to their definitions. #render_constraint_table(chip, config, groups: "defs") -*Implementation note*: one could remove the $1/512$ factor listed in the definitions of `limb_shift_1`, `limb_shift_2` and `limb_shift_3`. -While this would mean that the three are no longer `Bit`s, this fact does not impact the correctness of the chip: all constraints using these variables only require the variables to be _non-zero_, not specifically $1$. == Left shifting #render_constraint_table(chip, config, groups: "intra_limb_left_shifting") diff --git a/spec/src/shift.toml b/spec/src/shift.toml index f5cdc3225..d984284ab 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -37,16 +37,6 @@ name = "bit_shift" type = "Byte" desc = "`shift && 0x0F`" -[[variables.auxiliary]] -name = "limb_shift_odd" -type = "Byte" -desc = "`shift && 0x10`" - -[[variables.auxiliary]] -name = "limb_shift_even" -type = "Byte" -desc = "`shift && 0x20`" - [[variables.auxiliary]] name = "bit_shifted_uncarried" type = "Half[4]" @@ -62,29 +52,28 @@ name = "is_negative" type = "Bit" desc = "whether `in` is negative." +[[variables.auxiliary]] +name = "limb_shift_0" +type = "Bit" +desc = "Whether $floor.l #`bit_shift` / 16 floor.r equiv 0 mod 4$." + [[variables.auxiliary]] name = "limb_shift_1" type = "Bit" -desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 1 mod 4$." +desc = "Whether $floor.l #`bit_shift` / 16 floor.r equiv 1 mod 4$." [[variables.auxiliary]] name = "limb_shift_2" type = "Bit" -desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 2 mod 4$." +desc = "Whether $floor.l #`bit_shift` / 16 floor.r equiv 2 mod 4$." [[variables.auxiliary]] name = "limb_shift_3" type = "Bit" -desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 3 mod 4$." +desc = "Whether $floor.l #`bit_shift` / 16 floor.r equiv 3 mod 4$." # Virtual -[[variables.virtual]] -name = "limb_shift_0" -type = "Bit" -desc = "Whether $floor.l #`bit_shift` / 16 floor.r = 0 mod 4$." -poly = ["/", ["*", ["-", 16, "limb_shift_odd"], ["-", 32, "limb_shift_even"]], 512] - [[variables.virtual]] name = "extension" type = "Half" @@ -143,37 +132,40 @@ multiplicity = "μ" [[constraints.defs]] kind = "interaction" tag = "AND_BYTE" -input = ["shift", "0x10"] -output = "limb_shift_odd" -ref = "shift:c:limb_shift_odd" +input = ["shift", "0x30"] +output = ["+", ["-", 1, "limb_shift_0"], ["*", 15, "limb_shift_1"], ["*", 31, "limb_shift_1"], ["*", 47, "limb_shift_1"]] +ref = "shift:c:limb_shift_x" multiplicity = "μ" [[constraints.defs]] -kind = "interaction" -tag = "AND_BYTE" -input = ["shift", "0x20"] -output = "limb_shift_even" -ref = "shift:c:limb_shift_even" -multiplicity = "μ" +kind = "template" +tag = "IS_BIT" +input = ["limb_shift_0"] +ref = "shift:c:limb_shift_0_is_bit" [[constraints.defs]] -kind = "arith" -constraint = "$#`limb_shift_1` = (#`limb_shift_odd` dot (32 - #`limb_shift_even`)) / 512$" -poly = ["-", ["*", 512, "limb_shift_1"], ["*", "limb_shift_odd", ["-", 32, "limb_shift_even"]]] -ref = "shift:c:limb_shift_1" +kind = "template" +tag = "IS_BIT" +input = ["limb_shift_1"] +ref = "shift:c:limb_shift_1_is_bit" [[constraints.defs]] -kind = "arith" -constraint = "$#`limb_shift_2` = ((16 - #`limb_shift_odd`) dot #`limb_shift_even`) / 512$" -poly = ["-", ["*", 512, "limb_shift_2"], ["*", ["-", 16, "limb_shift_odd"], "limb_shift_even"]] -ref = "shift:c:limb_shift_2" +kind = "template" +tag = "IS_BIT" +input = ["limb_shift_2"] +ref = "shift:c:limb_shift_2_is_bit" [[constraints.defs]] -kind = "arith" -constraint = "$#`limb_shift_3` = (#`limb_shift_odd` dot #`limb_shift_even`) / 512$" -poly = ["-", ["*", 512, "limb_shift_3"], ["*", "limb_shift_odd", "limb_shift_even"]] -ref = "shift:c:limb_shift_3" +kind = "template" +tag = "IS_BIT" +input = ["limb_shift_3"] +ref = "shift:c:limb_shift_3_is_bit" +[[constraints.defs]] +kind = "template" +tag = "IS_BIT" +input = [["+", "limb_shift_0", "limb_shift_1", "limb_shift_2", "limb_shift_3"]] +ref = "shift:c:limb_shift_sum_is_bit" [[constraint_groups]] name = "intra_limb_left_shifting" From b21041d30e184b56a47e7dc0324d221650b1253d Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 30 Dec 2025 14:48:16 +0100 Subject: [PATCH 12/32] spec/SHIFT: fix typo --- spec/src/shift.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index d984284ab..bde93f472 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -133,7 +133,7 @@ multiplicity = "μ" kind = "interaction" tag = "AND_BYTE" input = ["shift", "0x30"] -output = ["+", ["-", 1, "limb_shift_0"], ["*", 15, "limb_shift_1"], ["*", 31, "limb_shift_1"], ["*", 47, "limb_shift_1"]] +output = ["+", ["-", 1, "limb_shift_0"], ["*", 15, "limb_shift_1"], ["*", 31, "limb_shift_2"], ["*", 47, "limb_shift_3"]] ref = "shift:c:limb_shift_x" multiplicity = "μ" From 7b0810bf141228f50317ca52e753e48ad4e590c2 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 30 Dec 2025 17:35:20 +0100 Subject: [PATCH 13/32] Turn `limb_shift_x` into array --- spec/shift.typ | 3 +- spec/src/shift.toml | 110 +++++++++++++++----------------------------- 2 files changed, 38 insertions(+), 75 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 793bab5a8..91159ca82 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -28,8 +28,9 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed usin = Constraints == Definitions -Constrain the auxiliary variables `bit_shift`, `limb_shift_0`, `limb_shift_1`, `limb_shift_2` and `limb_shift_3` according to their definitions. +Constrain the auxiliary variables `bit_shift`, and `limb_shift` according to their definitions. #render_constraint_table(chip, config, groups: "defs") +*Note*: although exactly $1$ of the bits in `limb_shift` should equal $1$ while the others are zero, this does not have to be constrained explicitly: @shift:c:limb_shift_is_bit enforces that all values are bits, while @shift:c:limb_shift_lookup can be satisfied if and only if exactly one of the four values equals $1$. == Left shifting #render_constraint_table(chip, config, groups: "intra_limb_left_shifting") diff --git a/spec/src/shift.toml b/spec/src/shift.toml index bc5ff4c73..2c196eb15 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -37,6 +37,11 @@ name = "bit_shift" type = "Byte" desc = "`shift && 0x0F`" +[[variables.auxiliary]] +name = "limb_shift" +type = ["Bit", 4] +desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod 4$." + [[variables.auxiliary]] name = "bit_shifted_uncarried" type = ["Half", 4] @@ -52,26 +57,6 @@ name = "is_negative" type = "Bit" desc = "whether `in` is negative." -[[variables.auxiliary]] -name = "limb_shift_0" -type = "Bit" -desc = "Whether $floor.l #`bit_shift` / 16 floor.r equiv 0 mod 4$." - -[[variables.auxiliary]] -name = "limb_shift_1" -type = "Bit" -desc = "Whether $floor.l #`bit_shift` / 16 floor.r equiv 1 mod 4$." - -[[variables.auxiliary]] -name = "limb_shift_2" -type = "Bit" -desc = "Whether $floor.l #`bit_shift` / 16 floor.r equiv 2 mod 4$." - -[[variables.auxiliary]] -name = "limb_shift_3" -type = "Bit" -desc = "Whether $floor.l #`bit_shift` / 16 floor.r equiv 3 mod 4$." - # Virtual [[variables.virtual]] @@ -133,39 +118,16 @@ multiplicity = "μ" kind = "interaction" tag = "AND_BYTE" input = ["shift", "0x30"] -output = ["+", ["-", 1, "limb_shift_0"], ["*", 15, "limb_shift_1"], ["*", 31, "limb_shift_2"], ["*", 47, "limb_shift_3"]] -ref = "shift:c:limb_shift_x" +output = ["+", ["-", 1, ["idx", "limb_shift", 0]], ["*", 15, ["idx", "limb_shift", 1]], ["*", 31, ["idx", "limb_shift", 2]], ["*", 47, ["idx", "limb_shift", 3]]] +ref = "shift:c:limb_shift_lookup" multiplicity = "μ" [[constraints.defs]] kind = "template" tag = "IS_BIT" -input = ["limb_shift_0"] -ref = "shift:c:limb_shift_0_is_bit" - -[[constraints.defs]] -kind = "template" -tag = "IS_BIT" -input = ["limb_shift_1"] -ref = "shift:c:limb_shift_1_is_bit" - -[[constraints.defs]] -kind = "template" -tag = "IS_BIT" -input = ["limb_shift_2"] -ref = "shift:c:limb_shift_2_is_bit" - -[[constraints.defs]] -kind = "template" -tag = "IS_BIT" -input = ["limb_shift_3"] -ref = "shift:c:limb_shift_3_is_bit" - -[[constraints.defs]] -kind = "template" -tag = "IS_BIT" -input = [["+", "limb_shift_0", "limb_shift_1", "limb_shift_2", "limb_shift_3"]] -ref = "shift:c:limb_shift_sum_is_bit" +input = [["idx", "limb_shift", "i"]] +range = ["i", 0, 4] +ref = "shift:c:limb_shift_is_bit" [[constraint_groups]] name = "intra_limb_left_shifting" @@ -249,8 +211,8 @@ name = "limb_shifting" [[constraints.limb_shifting]] kind = "arith" -constraint = "$#`limb_shift_0` => #`shifted[i]` = #`bit_shifted[i]`$" -poly = ["*", "limb_shift_0", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i"]]] +constraint = "$#`limb_shift[0]` => #`shifted[i]` = #`bit_shifted[i]`$" +poly = ["*", ["idx", "limb_shift", 0], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i"]]] range = ["i", 0, 3] @@ -259,40 +221,40 @@ name = "limb_left_shifting" [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`limb_shift_1` => #`shifted[i]` = #`bit_shifted[i-1]`$" -poly = ["*", "left", "limb_shift_1", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 1]]]] +constraint = "$#`left` and #`limb_shift[1]` => #`shifted[i]` = #`bit_shifted[i-1]`$" +poly = ["*", "left", ["idx", "limb_shift", 1], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 1]]]] range = ["i", 1, 3] [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`limb_shift_2` => #`shifted[i]` = #`bit_shifted[i-2]`$" -poly = ["*", "left", "limb_shift_2", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] +constraint = "$#`left` and #`limb_shift[2]` => #`shifted[i]` = #`bit_shifted[i-2]`$" +poly = ["*", "left", ["idx", "limb_shift", 2], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] range = ["i", 2, 3] [[constraints.limb_left_shifting]] kind = "arith" -constraint = "$#`left` and #`limb_shift_3` => #`shifted[3]` = #`bit_shifted[0]`$" -poly = ["*", "left", "limb_shift_3", ["-", ["idx", "shifted", 3], ["idx", "bit_shifted", 0]]] +constraint = "$#`left` and #`limb_shift[3]` => #`shifted[3]` = #`bit_shifted[0]`$" +poly = ["*", "left", ["idx", "limb_shift", 3], ["-", ["idx", "shifted", 3], ["idx", "bit_shifted", 0]]] [[constraint_groups]] name = "limb_left_shifting_zero" [[constraints.limb_left_shifting_zero]] kind = "arith" -constraint = "$#`left` and (#`limb_shift_1` or #`limb_shift_2` or #`limb_shift_3`) => #`shifted[0]` = 0$" -poly = ["*", "left", ["+", "limb_shift_1", "limb_shift_2", "limb_shift_3"], ["idx", "shifted", 0]] +constraint = "$#`left` and (#`limb_shift[1]` or #`limb_shift[2]` or #`limb_shift[3]`) => #`shifted[0]` = 0$" +poly = ["*", "left", ["+", ["idx", "limb_shift", 1], ["idx", "limb_shift", 2], ["idx", "limb_shift", 3]], ["idx", "shifted", 0]] [[constraints.limb_left_shifting_zero]] kind = "arith" -constraint = "$#`left` and (#`limb_shift_2` or #`limb_shift_3`) => #`shifted[1]` = 0$" -poly = ["*", "left", ["+", "limb_shift_2", "limb_shift_3"], ["idx", "shifted", 1]] +constraint = "$#`left` and (#`limb_shift[2]` or #`limb_shift[3]`) => #`shifted[1]` = 0$" +poly = ["*", "left", ["+", ["idx", "limb_shift", 2], ["idx", "limb_shift", 3]], ["idx", "shifted", 1]] [[constraints.limb_left_shifting_zero]] kind = "arith" -constraint = "$#`left` and #`limb_shift_3` => #`shifted[2]` = 0$" -poly = ["*", "left", "limb_shift_3", ["idx", "shifted", 2]] +constraint = "$#`left` and #`limb_shift[3]` => #`shifted[2]` = 0$" +poly = ["*", "left", ["idx", "limb_shift", 3], ["idx", "shifted", 2]] [[constraint_groups]] @@ -300,38 +262,38 @@ name = "limb_right_shifting" [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`limb_shift_1` => #`shifted[i]` = #`bit_shifted[i+1]`$" -poly = ["*", "right", "limb_shift_1", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["+", "i", 1]]]] +constraint = "$#`right` and #`limb_shift[1]` => #`shifted[i]` = #`bit_shifted[i+1]`$" +poly = ["*", "right", ["idx", "limb_shift", 1], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["+", "i", 1]]]] range = ["i", 0, 2] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`limb_shift_2` => #`shifted[i]` = #`bit_shifted[i+2]`$" -poly = ["*", "right", "limb_shift_2", ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] +constraint = "$#`right` and #`limb_shift[2]` => #`shifted[i]` = #`bit_shifted[i+2]`$" +poly = ["*", "right", ["idx", "limb_shift", 2], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] range = ["i", 0, 1] [[constraints.limb_right_shifting]] kind = "arith" -constraint = "$#`right` and #`limb_shift_3` => #`shifted[0]` = #`bit_shifted[3]`$" -poly = ["*", "right", "limb_shift_3", ["-", ["idx", "shifted", 0], ["idx", "bit_shifted", 3]]] +constraint = "$#`right` and #`limb_shift[3]` => #`shifted[0]` = #`bit_shifted[3]`$" +poly = ["*", "right", ["idx", "limb_shift", 3], ["-", ["idx", "shifted", 0], ["idx", "bit_shifted", 3]]] [[constraint_groups]] name = "limb_right_shifting_extension" [[constraints.limb_right_shifting_extension]] kind = "arith" -constraint = "$#`right` and (#`limb_shift_1` or #`limb_shift_2` or #`limb_shift_3`) => #`shifted[3]` = #`extension`$" -poly = ["*", "right", ["+", "limb_shift_1", "limb_shift_2", "limb_shift_3"], ["-", ["idx", "shifted", 3], "extension"]] +constraint = "$#`right` and (#`limb_shift[1]` or #`limb_shift[2]` or #`limb_shift[3]`) => #`shifted[3]` = #`extension`$" +poly = ["*", "right", ["+", ["idx", "limb_shift", 1], ["idx", "limb_shift", 2], ["idx", "limb_shift", 3]], ["-", ["idx", "shifted", 3], "extension"]] [[constraints.limb_right_shifting_extension]] kind = "arith" -constraint = "$#`right` and (#`limb_shift_2` or #`limb_shift_3`) => #`shifted[2]` = #`extension`$" -poly = ["*", "right", ["+", "limb_shift_2", "limb_shift_3"], ["-", ["idx", "shifted", 2], "extension"]] +constraint = "$#`right` and (#`limb_shift[2]` or #`limb_shift[3]`) => #`shifted[2]` = #`extension`$" +poly = ["*", "right", ["+", ["idx", "limb_shift", 2], ["idx", "limb_shift", 3]], ["-", ["idx", "shifted", 2], "extension"]] [[constraints.limb_right_shifting_extension]] kind = "arith" -constraint = "$#`right` and #`limb_shift_3` => #`shifted[1]` = #`extension`$" -poly = ["*", "right", "limb_shift_3", ["-", ["idx", "shifted", 1], "extension"]] +constraint = "$#`right` and #`limb_shift[3]` => #`shifted[1]` = #`extension`$" +poly = ["*", "right", ["idx", "limb_shift", 3], ["-", ["idx", "shifted", 1], "extension"]] # Lookups From 668dba8d0330d1d5ba830d3e3c03cd5a66cfcb85 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 30 Dec 2025 11:28:32 +0100 Subject: [PATCH 14/32] spec: support "sum" expression in math --- spec/expr.typ | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/spec/expr.typ b/spec/expr.typ index d5a2e4d8d..ccf2d304e 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -24,6 +24,7 @@ // 3 : / // 4 : not (e.g., 5 => 1-5) // 5 : + +// 5 : sum // 6 : - // 7 : [] // 8 : = @@ -97,6 +98,10 @@ "idx": (pp, rec, e) => $#rec(7, e.at(1))_(#rec(7, e.at(2)))$, "not": (pp, rec, e) => mwrap($1 - #rec(4, e.at(1))$, pp < 4), "+": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(5)).join($+$)$, pp < 5), + "sum": (pp, rec, e) => { + assert(e.len() == 4, message: "invalid sum:" + repr(e)) + mwrap($sum_(#rec(10, e.at(1)))^#rec(10, e.at(2)) #rec(5, e.at(3))$, pp < 5) + }, "*": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(3)).join($dot$)$, pp < 3), "/": (pp, rec, e) => $#rec(3, e.at(1)) / #rec(3, e.at(2))$, "^": (pp, rec, e) => { From 0fc25d28f7f5652d1c335d3c5f60562ff969d0b5 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 31 Dec 2025 10:29:38 +0100 Subject: [PATCH 15/32] Simplify limb-shifting constraint --- spec/shift.typ | 12 +++---- spec/src/shift.toml | 84 ++------------------------------------------- 2 files changed, 6 insertions(+), 90 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 91159ca82..000420f24 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -32,16 +32,12 @@ Constrain the auxiliary variables `bit_shift`, and `limb_shift` according to the #render_constraint_table(chip, config, groups: "defs") *Note*: although exactly $1$ of the bits in `limb_shift` should equal $1$ while the others are zero, this does not have to be constrained explicitly: @shift:c:limb_shift_is_bit enforces that all values are bits, while @shift:c:limb_shift_lookup can be satisfied if and only if exactly one of the four values equals $1$. -== Left shifting +== Intra limb shifting #render_constraint_table(chip, config, groups: "intra_limb_left_shifting") -#render_constraint_table(chip, config, groups: "limb_shifting") -#render_constraint_table(chip, config, groups: "limb_left_shifting") -#render_constraint_table(chip, config, groups: "limb_left_shifting_zero") - -== Right shifting #render_constraint_table(chip, config, groups: "intra_limb_right_shifting") -#render_constraint_table(chip, config, groups: "limb_right_shifting") -#render_constraint_table(chip, config, groups: "limb_right_shifting_extension") + +== Limb shifting +#render_constraint_table(chip, config, groups: "limb_shifting") == Lookup #render_constraint_table(chip, config, groups: "lookups") \ No newline at end of file diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 2c196eb15..fbe140f04 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -211,91 +211,11 @@ name = "limb_shifting" [[constraints.limb_shifting]] kind = "arith" -constraint = "$#`limb_shift[0]` => #`shifted[i]` = #`bit_shifted[i]`$" -poly = ["*", ["idx", "limb_shift", 0], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", "i"]]] +constraint = "$#`shifted[i]` = #`left` dot sum_(j=0)^i #`limb_shift[j]` dot #`bit_shifted[i-j]` + #`right` dot (sum_(j=0)^(3-i) #`limb_shift[j]` dot #`bit_shifted[i+j]` + sum_(j=3-i)^3 #`limb_shift[j]` dot #`extension`)$" +poly = ["-", ["idx", "shifted", "i"], ["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "bit_shifted", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "bit_shifted", ["+", "i", "j"]]]], ["sum", ["=", "j", ["-", 3, "i"]], 3, ["*", "extension", ["idx", "limb_shift", "j"]]]]]]] range = ["i", 0, 3] -[[constraint_groups]] -name = "limb_left_shifting" - -[[constraints.limb_left_shifting]] -kind = "arith" -constraint = "$#`left` and #`limb_shift[1]` => #`shifted[i]` = #`bit_shifted[i-1]`$" -poly = ["*", "left", ["idx", "limb_shift", 1], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 1]]]] -range = ["i", 1, 3] - - -[[constraints.limb_left_shifting]] -kind = "arith" -constraint = "$#`left` and #`limb_shift[2]` => #`shifted[i]` = #`bit_shifted[i-2]`$" -poly = ["*", "left", ["idx", "limb_shift", 2], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] -range = ["i", 2, 3] - - -[[constraints.limb_left_shifting]] -kind = "arith" -constraint = "$#`left` and #`limb_shift[3]` => #`shifted[3]` = #`bit_shifted[0]`$" -poly = ["*", "left", ["idx", "limb_shift", 3], ["-", ["idx", "shifted", 3], ["idx", "bit_shifted", 0]]] - -[[constraint_groups]] -name = "limb_left_shifting_zero" - -[[constraints.limb_left_shifting_zero]] -kind = "arith" -constraint = "$#`left` and (#`limb_shift[1]` or #`limb_shift[2]` or #`limb_shift[3]`) => #`shifted[0]` = 0$" -poly = ["*", "left", ["+", ["idx", "limb_shift", 1], ["idx", "limb_shift", 2], ["idx", "limb_shift", 3]], ["idx", "shifted", 0]] - -[[constraints.limb_left_shifting_zero]] -kind = "arith" -constraint = "$#`left` and (#`limb_shift[2]` or #`limb_shift[3]`) => #`shifted[1]` = 0$" -poly = ["*", "left", ["+", ["idx", "limb_shift", 2], ["idx", "limb_shift", 3]], ["idx", "shifted", 1]] - -[[constraints.limb_left_shifting_zero]] -kind = "arith" -constraint = "$#`left` and #`limb_shift[3]` => #`shifted[2]` = 0$" -poly = ["*", "left", ["idx", "limb_shift", 3], ["idx", "shifted", 2]] - - -[[constraint_groups]] -name = "limb_right_shifting" - -[[constraints.limb_right_shifting]] -kind = "arith" -constraint = "$#`right` and #`limb_shift[1]` => #`shifted[i]` = #`bit_shifted[i+1]`$" -poly = ["*", "right", ["idx", "limb_shift", 1], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["+", "i", 1]]]] -range = ["i", 0, 2] - -[[constraints.limb_right_shifting]] -kind = "arith" -constraint = "$#`right` and #`limb_shift[2]` => #`shifted[i]` = #`bit_shifted[i+2]`$" -poly = ["*", "right", ["idx", "limb_shift", 2], ["-", ["idx", "shifted", "i"], ["idx", "bit_shifted", ["-", "i", 2]]]] -range = ["i", 0, 1] - -[[constraints.limb_right_shifting]] -kind = "arith" -constraint = "$#`right` and #`limb_shift[3]` => #`shifted[0]` = #`bit_shifted[3]`$" -poly = ["*", "right", ["idx", "limb_shift", 3], ["-", ["idx", "shifted", 0], ["idx", "bit_shifted", 3]]] - -[[constraint_groups]] -name = "limb_right_shifting_extension" - -[[constraints.limb_right_shifting_extension]] -kind = "arith" -constraint = "$#`right` and (#`limb_shift[1]` or #`limb_shift[2]` or #`limb_shift[3]`) => #`shifted[3]` = #`extension`$" -poly = ["*", "right", ["+", ["idx", "limb_shift", 1], ["idx", "limb_shift", 2], ["idx", "limb_shift", 3]], ["-", ["idx", "shifted", 3], "extension"]] - -[[constraints.limb_right_shifting_extension]] -kind = "arith" -constraint = "$#`right` and (#`limb_shift[2]` or #`limb_shift[3]`) => #`shifted[2]` = #`extension`$" -poly = ["*", "right", ["+", ["idx", "limb_shift", 2], ["idx", "limb_shift", 3]], ["-", ["idx", "shifted", 2], "extension"]] - -[[constraints.limb_right_shifting_extension]] -kind = "arith" -constraint = "$#`right` and #`limb_shift[3]` => #`shifted[1]` = #`extension`$" -poly = ["*", "right", ["idx", "limb_shift", 3], ["-", ["idx", "shifted", 1], "extension"]] - - # Lookups [[constraint_groups]] From 79c1d05d97ac0d781bc56de9d8eee7bf0ff34089 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Sat, 3 Jan 2026 14:05:49 +0100 Subject: [PATCH 16/32] spec: attempt at refactoring `shift` --- spec/shift.typ | 43 ++++++++--- spec/src/shift.toml | 184 +++++++++++++++++++++++++++----------------- 2 files changed, 146 insertions(+), 81 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 000420f24..2e2672a5b 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -14,8 +14,6 @@ #show: book-page.with(title: "SHIFT chip") -#outline() - = Columns #let nr_variables = total_nr_variables(chip) #let nr_columns = total_nr_instantiated_columns(chip, config) @@ -26,18 +24,41 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed usin = Assumptions #render_chip_assumptions(chip, config) += About +This chip is designed to enforce that +$ +#`out` := cases( + #`in` #`<<` #`s` " if" #`direction` = 0, + #`in` #`>>` #`s` " if" #`direction` = 1 and #`signed` = 0, + #`in` #`>>>` #`s` "if" #`direction` = 1 and #`signed` = 1, +) +$ +where +$ +#`s` := cases( + #`shift` mod 32 "if" #`word_instr` = 1, + #`shift` mod 64 "if" #`word_instr` = 0, +) +$ +Here, `<<` and `>>` denote the _logical_ left and right shift operations, while `>>>` denotes the _arithmetic_ right shift operation. + +Note that, while they share many similarities, these six different operations are sufficiently different that the resulting compact design is rather complex. +Pay close attention as we work through the constraints put in place to enforce `out` is the correct value. + + = Constraints -== Definitions -Constrain the auxiliary variables `bit_shift`, and `limb_shift` according to their definitions. #render_constraint_table(chip, config, groups: "defs") -*Note*: although exactly $1$ of the bits in `limb_shift` should equal $1$ while the others are zero, this does not have to be constrained explicitly: @shift:c:limb_shift_is_bit enforces that all values are bits, while @shift:c:limb_shift_lookup can be satisfied if and only if exactly one of the four values equals $1$. -== Intra limb shifting -#render_constraint_table(chip, config, groups: "intra_limb_left_shifting") -#render_constraint_table(chip, config, groups: "intra_limb_right_shifting") +== Left shift +Left shifting, when `bit_shift != 0`. +#render_constraint_table(chip, config, groups: "intra_limb_left_shift") + +== Right shift +Right shifting, when `bit_shift != 0`. +#render_constraint_table(chip, config, groups: "logical_right") -== Limb shifting +== Full-limb shifting #render_constraint_table(chip, config, groups: "limb_shifting") -== Lookup -#render_constraint_table(chip, config, groups: "lookups") \ No newline at end of file +== Lookups +#render_constraint_table(chip, config, groups: "lookups") diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 62b37eff2..d5da4a9db 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -5,7 +5,7 @@ name = "SHIFT" [[variables.input]] name = "in" type = "DWordHL" -desc = "The word being shifted" +desc = "The value being shifted" [[variables.input]] name = "shift" @@ -22,45 +22,56 @@ name = "signed" type = "Bit" desc = "Whether to interpret `in` as a signed integer." +[[variables.input]] +name = "word_instr" +type = "Bit" +desc = "Whether this is a Word-instruction (1) or not (0)." + # Output [[variables.output]] -name = "shifted" +name = "out" type = "DWordHL" desc = "`in <> (shift % 64)`" # Auxiliary + +[[variables.auxiliary]] +name = "is_negative" +type = "Bit" +desc = "Whether `in` is negative" + [[variables.auxiliary]] name = "bit_shift" type = "Byte" -desc = "`shift && 0x0F`" +desc = "Value by which to shift `in` to obtain `bit_shifted`" [[variables.auxiliary]] -name = "limb_shift" -type = ["Bit", 4] -desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod 4$." +name = "zbs" +type = "Bit" +desc = "Whether `bit_shift` is zero (1) or not (0)." [[variables.auxiliary]] -name = "bit_shifted_uncarried" +name = "X" type = ["Half", 4] -desc = "result of left/right shifting the individual limbs of `in` by `bit_shift`, i.e., without the carry values." +desc = "scratch variable." [[variables.auxiliary]] -name = "carry" +name = "Y" type = ["Half", 4] -desc = "the carry values of left/right shifting `in` by `bit_shift`." +desc = "scratch variable." [[variables.auxiliary]] -name = "is_negative" -type = "Bit" -desc = "whether `in` is negative." +name = "limb_shift" +type = ["Bit", 4] +desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod 4$." # Virtual [[variables.virtual]] -name = "extension" +name = "ext" type = "Half" desc = "sign extension of `in`." def = ["*", 65535, "is_negative"] @@ -81,7 +92,7 @@ def = "direction" name = "bit_shifted" type = "DWordHL" desc = "`in <> (shift % 16)`" -def = {idx="i", range=[0, 3], poly=["+", ["idx", "bit_shifted_uncarried", "i"], ["idx", "carry", "i"]]} +def = {idx="i", range=[0, 3], poly=["+", ["*", "zbs", ["idx", "in", "i"]], ["*", ["not", "zbs"], ["+", ["idx", "X", "i"], ["idx", "Y", "i"]]]]} # Multiplicities @@ -107,103 +118,136 @@ ref = "shift:a:range_in" name = "defs" [[constraints.defs]] -kind = "interaction" -tag = "AND_BYTE" -input = ["shift", "0x0F"] -output = "bit_shift" -ref = "shift:c:bit_shift" -multiplicity = "μ" +kind = "arith" +desc = "enforce `left` is `Bit`" +constraint = "$#`direction` => #`μ` = 1$" +poly = ["*", "direction", ["not", "μ"]] +ref = "shift:c:direction_implies_mu" [[constraints.defs]] kind = "interaction" -tag = "AND_BYTE" -input = ["shift", "0x30"] -output = ["+", ["-", 1, ["idx", "limb_shift", 0]], ["*", 15, ["idx", "limb_shift", 1]], ["*", 31, ["idx", "limb_shift", 2]], ["*", 47, ["idx", "limb_shift", 3]]] -ref = "shift:c:limb_shift_lookup" -multiplicity = "μ" +tag = "MSB16" +input = [["idx", "in", 3]] +output = "is_negative" +multiplicity = "signed" +ref = "shift:c:is_negative_if_signed" + +[[constraints.defs]] +kind = "arith" +constraint = "$#`!signed` => #`is_negative` = 0$" +poly = ["*", ["not", "signed"], "is_negative"] +ref = "shift:c:is_negative_if_unsigned" [[constraints.defs]] kind = "template" -tag = "IS_BIT" -input = [["idx", "limb_shift", "i"]] -range = ["i", 0, 4] -ref = "shift:c:limb_shift_is_bit" +tag = "IsZero" +input = ["bit_shift"] +output = "zbs" +ref = "shift:c:zbs" +multiplicity = "μ" + [[constraint_groups]] -name = "intra_limb_left_shifting" +name = "intra_limb_left_shift" -[[constraints.intra_limb_left_shifting]] +[[constraints.intra_limb_left_shift]] +kind = "interaction" +tag = "AND_BYTE" +input = ["shift", "0x0F"] +output = "bit_shift" +ref = "shift:c:bit_shift_if_left" +multiplicity = "left" + +[[constraints.intra_limb_left_shift]] kind = "interaction" tag = "HWSL" input = [["idx", "in", "i"], "bit_shift"] -output = ["idx", "bit_shifted_uncarried", "i"] +output = ["idx", "X", "i"] range = ["i", 0, 3] +ref = "shift:c:hwsl_if_left" multiplicity = "left" -ref = "shift:c:hwsl" -[[constraints.intra_limb_left_shifting]] +[[constraints.intra_limb_left_shift]] kind = "interaction" tag = "HWSLC" input = [["idx", "in", ["-", "i", 1]], "bit_shift"] -output = ["idx", "carry", "i"] +output = ["idx", "Y", "i"] range = ["i", 1, 3] +ref = "shift:c:hwslc_if_left" multiplicity = "left" -ref = "shift:c:hwsl" -[[constraints.intra_limb_left_shifting]] +[[constraints.intra_limb_left_shift]] kind = "arith" -constraint = "$#`direction` => #`μ`$" -poly = ["*", "direction", ["-", 1, "μ"]] -ref = "shift:c:direction_implies_mu" - -[[constraints.intra_limb_left_shifting]] -kind = "arith" -constraint = "$#`left` => #`carry[0]` = 0$" -poly = ["*", "left", ["idx", "carry", 0]] -ref = "shift:c:left_zero_carry" +constraint = "$#`left` => #`Y[0]` = 0$" +poly = ["*", "left", ["idx", "Y", 0]] +ref = "shift:c:left_implies_y_zero" [[constraint_groups]] -name = "intra_limb_right_shifting" +name = "logical_right" -[[constraints.intra_limb_right_shifting]] +[[constraints.logical_right]] kind = "interaction" -tag = "HWSR" -input = [["idx", "in", "i"], "bit_shift"] -output = ["idx", "bit_shifted_uncarried", "i"] -range = ["i", 0, 3] +tag = "AND_BYTE" +input = [["-", ["^", 2, 32], "shift"], "0x0F"] +output = "bit_shift" +ref = "shift:c:bit_shift_if_right" multiplicity = "right" -ref = "shift:c:hwsr" -[[constraints.intra_limb_right_shifting]] +[[constraints.logical_right]] kind = "interaction" -tag = "HWSRC" +tag = "HWSL" input = [["idx", "in", ["+", "i", 1]], "bit_shift"] -output = ["idx", "carry", "i"] +output = ["idx", "X", "i"] range = ["i", 0, 2] +ref = "shift:c:hwsl_if_right" +multiplicity = "right" + +[[constraints.logical_right]] +kind = "interaction" +tag = "HWSL" +input = ["extension", "bit_shift"] +output = ["idx", "X", 3] +ref = "shift:c:hwsl_ext" +multiplicity = "right" + +[[constraints.logical_right]] +kind = "interaction" +tag = "HWSLC" +input = [["idx", "in", "i"], "bit_shift"] +output = ["idx", "Y", "i"] +range = ["i", 0, 3] +ref = "shift:c:hwslc_if_right" multiplicity = "right" -ref = "shift:c:hwsrc" -[[constraints.intra_limb_right_shifting]] + +[[constraint_groups]] +name = "is_negative" + + +[[constraints.is_negative]] kind = "interaction" tag = "MSB16" input = [["idx", "in", 3]] output = "is_negative" multiplicity = "signed" -ref = "shift:c:is_negative" +ref = "shift:c:is_negative_if_signed" -[[constraints.intra_limb_right_shifting]] +[[constraints.is_negative]] kind = "arith" constraint = "$#`!signed` => #`is_negative` = 0$" -poly = ["*", ["-", 1, "signed"], "is_negative"] +poly = ["*", ["not", "signed"], "is_negative"] +ref = "shift:c:is_negative_if_unsigned" -[[constraints.intra_limb_right_shifting]] + + +[[constraints.limb_shifting]] kind = "interaction" -tag = "HWSRC" -input = ["extension", "bit_shift"] -output = ["idx", "carry", 3] -multiplicity = "right" -ref = "shift:c:right_sign_extend" +tag = "AND_BYTE" +input = ["shift", ["+", "0x10", ["*", "0x20", ["not", "word_instr"]]]] +output = ["+", ["-", 1, ["idx", "limb_shift", 0]], ["*", 15, ["idx", "limb_shift", 1]], ["*", 31, ["idx", "limb_shift", 2]], ["*", 47, ["idx", "limb_shift", 3]]] +ref = "shift:c:limb_shift_lookup" +multiplicity = "μ" [[constraint_groups]] @@ -211,8 +255,8 @@ name = "limb_shifting" [[constraints.limb_shifting]] kind = "arith" -constraint = "$#`shifted[i]` = #`left` dot sum_(j=0)^i #`limb_shift[j]` dot #`bit_shifted[i-j]` + #`right` dot (sum_(j=0)^(3-i) #`limb_shift[j]` dot #`bit_shifted[i+j]` + sum_(j=3-i)^3 #`limb_shift[j]` dot #`extension`)$" -poly = ["-", ["idx", "shifted", "i"], ["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "bit_shifted", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "bit_shifted", ["+", "i", "j"]]]], ["sum", ["=", "j", ["-", 3, "i"]], 3, ["*", "extension", ["idx", "limb_shift", "j"]]]]]]] +constraint = "$#`out[i]` = #`left` dot sum_(j=0)^i #`limb_shift[j]` dot #`bit_shifted[i-j]` + #`right` dot (sum_(j=0)^(3-i) #`limb_shift[j]` dot #`bit_shifted[i+j]` + sum_(j=3-i)^3 #`limb_shift[j]` dot #`extension`)$" +poly = ["-", ["idx", "out", "i"], ["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "bit_shifted", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "bit_shifted", ["+", "i", "j"]]]], ["sum", ["=", "j", ["-", 3, "i"]], 3, ["*", "extension", ["idx", "limb_shift", "j"]]]]]]] range = ["i", 0, 3] From 22cd50cb65b2e43a8df88b0cd5780a4e54ab33c8 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Mon, 5 Jan 2026 18:05:00 +0100 Subject: [PATCH 17/32] spec: overhaul SHIFT --- spec/shift.typ | 73 +++++++++++------- spec/src/shift.toml | 176 ++++++++++++++++++++++---------------------- 2 files changed, 136 insertions(+), 113 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 2e2672a5b..6a00eef07 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -1,4 +1,4 @@ -#import "/book.typ": book-page +#import "/book.typ": book-page, et #import "/src.typ": load_config, load_chip #import "/chip.typ": ( render_chip_column_table, @@ -11,23 +11,28 @@ #let config = load_config() #let chip = load_chip("src/shift.toml", config) -#show: book-page.with(title: "SHIFT chip") - - -= Columns -#let nr_variables = total_nr_variables(chip) -#let nr_columns = total_nr_instantiated_columns(chip, config) +#let shift = raw(chip.name) -The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: -#render_chip_column_table(chip, config) +#show: book-page.with(title: "SHIFT chip") -= Assumptions -#render_chip_assumptions(chip, config) += #shift chip -= About -This chip is designed to enforce that +== Interface +The #shift chip has the following interface: +#block(radius: 5pt, width: 100%, inset: 1.5em, fill: luma(240), +``` +// param in: the value being shifted +// param shift: the number of bits to shift `in` by +// param direction: whether to shift left (0) or right (1) +// param signed: whether to interpret `in` as a signed (1) or unsigned (0) integer +// param word_instr: whether to execute the SLL/SR* (0) or SLLW/SR*W (1) instruction +// out shifted: the resulting value +SHIFT[shifted: DWord; in: DWord, shift: Byte, direction: Bit, signed: Bit, word_instr: Bit] +``` +) +In other words, the #shift chip is designed to constrain that $ -#`out` := cases( +#`shifted` := cases( #`in` #`<<` #`s` " if" #`direction` = 0, #`in` #`>>` #`s` " if" #`direction` = 1 and #`signed` = 0, #`in` #`>>>` #`s` "if" #`direction` = 1 and #`signed` = 1, @@ -42,23 +47,39 @@ $ $ Here, `<<` and `>>` denote the _logical_ left and right shift operations, while `>>>` denotes the _arithmetic_ right shift operation. -Note that, while they share many similarities, these six different operations are sufficiently different that the resulting compact design is rather complex. -Pay close attention as we work through the constraints put in place to enforce `out` is the correct value. +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `SHIFT` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns: +#render_chip_column_table(chip, config) +== Assumptions +#render_chip_assumptions(chip, config) -= Constraints -#render_constraint_table(chip, config, groups: "defs") +== Constraints +First, we constraint `bit_shift` based on whether we are left or right-shifting. +#render_constraint_table(chip, config, groups: "bit_shift") -== Left shift -Left shifting, when `bit_shift != 0`. -#render_constraint_table(chip, config, groups: "intra_limb_left_shift") +Next, we apply shift the limbs of `in` left and right, storing them in `X` and `Y` respectively. +When `right`-shifting and `bit_shift = 0`, the output is incorrect. +As such, we override `Y[i] := in[i]` and `X[i] := 0`. -== Right shift -Right shifting, when `bit_shift != 0`. -#render_constraint_table(chip, config, groups: "logical_right") +The case of `left`-shifting and `bit_shift = 0` will be used for padding rows. +To prevent unnecessary lookups in padding rows, we also override `X[i] := in[i]` and `Y[i] := 0` in this case. +#render_constraint_table(chip, config, groups: "intra_limb_shift") -== Full-limb shifting +=== Full-limb shifting +Lastly, `X` and `Y` are combined in the right way to form the limbs of `output`. #render_constraint_table(chip, config, groups: "limb_shifting") -== Lookups +=== Miscellaneous +To make sure `left` is actually a `Bit`, we introduce constraint @shift:c:direction_implies_mu. +Moreover, @shift:c:is_negative_if_signed is included to compute if `in` is negative. +Since `in` cannot be negative in the unsigned case, @shift:c:is_negative_if_unsigned constrains that `is_negative` will be $0$ in that case. +#render_constraint_table(chip, config, groups: "left_flag") +#render_constraint_table(chip, config, groups: "is_negative") + +=== Lookups +This chip adds the following interaction to the lookup. #render_constraint_table(chip, config, groups: "lookups") diff --git a/spec/src/shift.toml b/spec/src/shift.toml index d5da4a9db..cc9d8688f 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -31,7 +31,7 @@ desc = "Whether this is a Word-instruction (1) or not (0)." # Output [[variables.output]] -name = "out" +name = "shifted" type = "DWordHL" desc = "`in <> (shift % 64)`" @@ -55,7 +55,7 @@ desc = "Whether `bit_shift` is zero (1) or not (0)." [[variables.auxiliary]] name = "X" -type = ["Half", 4] +type = ["Half", 5] desc = "scratch variable." [[variables.auxiliary]] @@ -71,7 +71,7 @@ desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i # Virtual [[variables.virtual]] -name = "ext" +name = "extensions" type = "Half" desc = "sign extension of `in`." def = ["*", 65535, "is_negative"] @@ -89,10 +89,19 @@ desc = "Whether to perform a right-shift." def = "direction" [[variables.virtual]] -name = "bit_shifted" +name = "intra_limb_left" +type = "DWordHL" +desc = "`in << (shift % 16)` if `left`" +def = {idx="i", polys=[ + {range=0, poly=["idx", "X", 0]}, + {range=[1, 3], poly=["+", ["idx", "X", "i"], ["idx", "Y", ["-", "i", 1]]]}, +]} + +[[variables.virtual]] +name = "intra_limb_right" type = "DWordHL" -desc = "`in <> (shift % 16)`" -def = {idx="i", range=[0, 3], poly=["+", ["*", "zbs", ["idx", "in", "i"]], ["*", ["not", "zbs"], ["+", ["idx", "X", "i"], ["idx", "Y", "i"]]]]} +desc = "`in >>> (shift % 16)` if `right` and `signed`;\\ `in >> (shift % 16)` if `right` and `!signed`" +def = {idx="i", range=[0, 3], poly=["+", ["idx", "Y", "i"], ["idx", "X", ["+", "i", 1]]]} # Multiplicities @@ -110,21 +119,39 @@ desc = "`IS_HALFWORD[in[i]]`" range = ["i", 0, 3] ref = "shift:a:range_in" +[[assumptions]] +desc = "`IS_BYTE[shift]`" +ref = "shift:a:range_shift" +[[assumptions]] +desc = "`IS_BIT`" +ref = "shift:a:direction" + +[[assumptions]] +desc = "`IS_BIT`" +ref = "shift:a:signed" + +[[assumptions]] +desc = "`IS_BIT`" +ref = "shift:a:word_instr" # Constraints [[constraint_groups]] -name = "defs" +name = "left_flag" -[[constraints.defs]] +[[constraints.left_flag]] kind = "arith" -desc = "enforce `left` is `Bit`" +desc = "enforces `left` is `Bit`; cheaper than `IS_BIT`." constraint = "$#`direction` => #`μ` = 1$" poly = ["*", "direction", ["not", "μ"]] ref = "shift:c:direction_implies_mu" -[[constraints.defs]] + +[[constraint_groups]] +name = "is_negative" + +[[constraints.is_negative]] kind = "interaction" tag = "MSB16" input = [["idx", "in", 3]] @@ -132,25 +159,17 @@ output = "is_negative" multiplicity = "signed" ref = "shift:c:is_negative_if_signed" -[[constraints.defs]] +[[constraints.is_negative]] kind = "arith" constraint = "$#`!signed` => #`is_negative` = 0$" poly = ["*", ["not", "signed"], "is_negative"] ref = "shift:c:is_negative_if_unsigned" -[[constraints.defs]] -kind = "template" -tag = "IsZero" -input = ["bit_shift"] -output = "zbs" -ref = "shift:c:zbs" -multiplicity = "μ" - [[constraint_groups]] -name = "intra_limb_left_shift" +name = "bit_shift" -[[constraints.intra_limb_left_shift]] +[[constraints.bit_shift]] kind = "interaction" tag = "AND_BYTE" input = ["shift", "0x0F"] @@ -158,88 +177,75 @@ output = "bit_shift" ref = "shift:c:bit_shift_if_left" multiplicity = "left" -[[constraints.intra_limb_left_shift]] -kind = "interaction" -tag = "HWSL" -input = [["idx", "in", "i"], "bit_shift"] -output = ["idx", "X", "i"] -range = ["i", 0, 3] -ref = "shift:c:hwsl_if_left" -multiplicity = "left" - -[[constraints.intra_limb_left_shift]] -kind = "interaction" -tag = "HWSLC" -input = [["idx", "in", ["-", "i", 1]], "bit_shift"] -output = ["idx", "Y", "i"] -range = ["i", 1, 3] -ref = "shift:c:hwslc_if_left" -multiplicity = "left" - -[[constraints.intra_limb_left_shift]] -kind = "arith" -constraint = "$#`left` => #`Y[0]` = 0$" -poly = ["*", "left", ["idx", "Y", 0]] -ref = "shift:c:left_implies_y_zero" - - -[[constraint_groups]] -name = "logical_right" - -[[constraints.logical_right]] +[[constraints.bit_shift]] kind = "interaction" tag = "AND_BYTE" -input = [["-", ["^", 2, 32], "shift"], "0x0F"] +input = [["-", ["^", 2, 8], "shift"], "0x0F"] output = "bit_shift" ref = "shift:c:bit_shift_if_right" multiplicity = "right" -[[constraints.logical_right]] +[[constraints.bit_shift]] +kind = "template" +tag = "IsZero" +input = ["bit_shift"] +output = "zbs" +ref = "shift:c:zbs" +multiplicity = "μ" + + +[[constraint_groups]] +name = "intra_limb_shift" + +[[constraints.intra_limb_shift]] kind = "interaction" tag = "HWSL" -input = [["idx", "in", ["+", "i", 1]], "bit_shift"] +input = [["idx", "in", "i"], "bit_shift"] output = ["idx", "X", "i"] -range = ["i", 0, 2] -ref = "shift:c:hwsl_if_right" -multiplicity = "right" +range = ["i", 0, 3] +ref = "shift:c:hwsl_if_not_zero" +multiplicity = ["not", "zbs"] -[[constraints.logical_right]] +[[constraints.intra_limb_shift]] +kind = "arith" +constraint = "$#`zbs` => #`X[i]` = #`in[i]` dot #`left`$" +poly = ["*", "zbs", ["-", ["idx", "X", "i"], ["*", ["idx", "in", "i"], "left"]]] +range = ["i", 0, 3] +ref = "shift:c:zbs_implies_X" + +[[constraints.intra_limb_shift]] kind = "interaction" tag = "HWSL" input = ["extension", "bit_shift"] -output = ["idx", "X", 3] -ref = "shift:c:hwsl_ext" -multiplicity = "right" +output = ["idx", "X", 4] +ref = "shift:c:hwsl_x4_if_not_zero" +multiplicity = ["not", "zbs"] + +[[constraints.intra_limb_shift]] +kind = "arith" +constraint = "$#`zbs` => #`X[4]` = 0$" +poly = ["*", "zbs", ["idx", "X", 4]] +ref = "shift:c:zbs_implies_X_4" -[[constraints.logical_right]] +[[constraints.intra_limb_shift]] kind = "interaction" tag = "HWSLC" input = [["idx", "in", "i"], "bit_shift"] output = ["idx", "Y", "i"] range = ["i", 0, 3] -ref = "shift:c:hwslc_if_right" -multiplicity = "right" - - -[[constraint_groups]] -name = "is_negative" - +ref = "shift:c:hwslc_if_not_zero" +multiplicity = ["not", "zbs"] -[[constraints.is_negative]] -kind = "interaction" -tag = "MSB16" -input = [["idx", "in", 3]] -output = "is_negative" -multiplicity = "signed" -ref = "shift:c:is_negative_if_signed" - -[[constraints.is_negative]] +[[constraints.intra_limb_shift]] kind = "arith" -constraint = "$#`!signed` => #`is_negative` = 0$" -poly = ["*", ["not", "signed"], "is_negative"] -ref = "shift:c:is_negative_if_unsigned" +constraint = "$#`zbs` => #`Y[i]` = #`in[i]` dot #`right`$" +poly = ["*", "zbs", ["-", ["idx", "Y", "i"], ["*", ["idx", "in", "i"], "right"]]] +range = ["i", 0, 3] +ref = "shift:c:zbs_implies_Y" +[[constraint_groups]] +name = "limb_shifting" [[constraints.limb_shifting]] kind = "interaction" @@ -249,14 +255,10 @@ output = ["+", ["-", 1, ["idx", "limb_shift", 0]], ["*", 15, ["idx", "limb_shift ref = "shift:c:limb_shift_lookup" multiplicity = "μ" - -[[constraint_groups]] -name = "limb_shifting" - [[constraints.limb_shifting]] kind = "arith" -constraint = "$#`out[i]` = #`left` dot sum_(j=0)^i #`limb_shift[j]` dot #`bit_shifted[i-j]` + #`right` dot (sum_(j=0)^(3-i) #`limb_shift[j]` dot #`bit_shifted[i+j]` + sum_(j=3-i)^3 #`limb_shift[j]` dot #`extension`)$" -poly = ["-", ["idx", "out", "i"], ["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "bit_shifted", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "bit_shifted", ["+", "i", "j"]]]], ["sum", ["=", "j", ["-", 3, "i"]], 3, ["*", "extension", ["idx", "limb_shift", "j"]]]]]]] +constraint = "$#`shifted[i]` = #`left` dot sum_(j=0)^i #`limb_shift[j]` dot #`intra_limb_left[i-j]` + #`right` dot (sum_(j=0)^(3-i) #`limb_shift[j]` dot #`intra_limb_right[i+j]` + #`extension` dot sum_(j=3-i)^3 #`limb_shift[j]`)$" +poly = ["-", ["idx", "shifted", "i"], ["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_left", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_right", ["+", "i", "j"]]]], ["*", "extension", ["sum", ["=", "j", ["-", 3, "i"]], 3, ["idx", "limb_shift", "j"]]]]]]] range = ["i", 0, 3] @@ -268,7 +270,7 @@ name = "lookups" [[constraints.lookups]] kind = "interaction" tag = "SHIFT" -input = ["in", "shift", "direction", "signed"] +input = ["in", "shift", "direction", "signed", "word_instr"] output = "shifted" multiplicity = "-μ" ref = "shift:c:lookup" From 4af8d167bb6698f0bfa30bc09b0ffb92a5d3af0c Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Wed, 7 Jan 2026 14:26:05 +0100 Subject: [PATCH 18/32] spec: SHIFT: rename `extensions` as `extension` Co-authored-by: Robin Jadoul --- spec/src/shift.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index cc9d8688f..50e41def1 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -71,7 +71,7 @@ desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i # Virtual [[variables.virtual]] -name = "extensions" +name = "extension" type = "Half" desc = "sign extension of `in`." def = ["*", 65535, "is_negative"] From a9740a099ca7723a1053ab337a248bbc7d735116 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 7 Jan 2026 14:22:13 +0100 Subject: [PATCH 19/32] spec: SHIFT: make `shift` of type Byte --- spec/src/shift.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 50e41def1..13a0597f6 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -9,7 +9,7 @@ desc = "The value being shifted" [[variables.input]] name = "shift" -type = "BaseField" +type = "Byte" desc = "Number of bits to shift `in` by." [[variables.input]] From af6f3bd1fcdf501e57372808456d365be99c447d Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 7 Jan 2026 14:22:55 +0100 Subject: [PATCH 20/32] spec: SHIFT: replace variable '0x' with constant 0x --- spec/src/shift.toml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 13a0597f6..b79cf46a1 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -172,7 +172,7 @@ name = "bit_shift" [[constraints.bit_shift]] kind = "interaction" tag = "AND_BYTE" -input = ["shift", "0x0F"] +input = ["shift", 0x0F] output = "bit_shift" ref = "shift:c:bit_shift_if_left" multiplicity = "left" @@ -180,7 +180,7 @@ multiplicity = "left" [[constraints.bit_shift]] kind = "interaction" tag = "AND_BYTE" -input = [["-", ["^", 2, 8], "shift"], "0x0F"] +input = [["-", ["^", 2, 8], "shift"], 0x0F] output = "bit_shift" ref = "shift:c:bit_shift_if_right" multiplicity = "right" @@ -250,7 +250,7 @@ name = "limb_shifting" [[constraints.limb_shifting]] kind = "interaction" tag = "AND_BYTE" -input = ["shift", ["+", "0x10", ["*", "0x20", ["not", "word_instr"]]]] +input = ["shift", ["-", 0x30, ["*", 0x20, "word_instr"]]] output = ["+", ["-", 1, ["idx", "limb_shift", 0]], ["*", 15, ["idx", "limb_shift", 1]], ["*", 31, ["idx", "limb_shift", 2]], ["*", 47, ["idx", "limb_shift", 3]]] ref = "shift:c:limb_shift_lookup" multiplicity = "μ" From 594c8df3850a9b4b7a4ccd8aed02dd05bcc704c9 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 7 Jan 2026 14:24:36 +0100 Subject: [PATCH 21/32] spec: SHIFT: remove "cheaper" remark --- spec/src/shift.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index b79cf46a1..6aa1c02a1 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -142,7 +142,7 @@ name = "left_flag" [[constraints.left_flag]] kind = "arith" -desc = "enforces `left` is `Bit`; cheaper than `IS_BIT`." +desc = "enforces `left` is `Bit`." constraint = "$#`direction` => #`μ` = 1$" poly = ["*", "direction", ["not", "μ"]] ref = "shift:c:direction_implies_mu" From 08e13fa8e23657ff8dce369fb7b7741d50706004 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 7 Jan 2026 14:38:25 +0100 Subject: [PATCH 22/32] spec: SHIFT: fix `shifted` description --- spec/src/shift.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 6aa1c02a1..f20c07164 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -33,7 +33,7 @@ desc = "Whether this is a Word-instruction (1) or not (0)." [[variables.output]] name = "shifted" type = "DWordHL" -desc = "`in <> (shift % 64)`" +desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" # Auxiliary From 27d05ef9e981d9802271690c6dabd2d1930ffbc8 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 7 Jan 2026 14:58:03 +0100 Subject: [PATCH 23/32] spec: SHIFT: make output a DWordWL --- spec/src/shift.toml | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index f20c07164..f7e96c887 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -31,11 +31,10 @@ desc = "Whether this is a Word-instruction (1) or not (0)." # Output [[variables.output]] -name = "shifted" -type = "DWordHL" +name = "out" +type = "DWordWL" desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" - # Auxiliary [[variables.auxiliary]] @@ -103,6 +102,12 @@ type = "DWordHL" desc = "`in >>> (shift % 16)` if `right` and `signed`;\\ `in >> (shift % 16)` if `right` and `!signed`" def = {idx="i", range=[0, 3], poly=["+", ["idx", "Y", "i"], ["idx", "X", ["+", "i", 1]]]} +[[variables.virtual]] +name = "shifted" +type = "DWordHL" +desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" +def = {idx="i", range=[0, 3], poly=["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_left", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_right", ["+", "i", "j"]]]], ["*", "extension", ["sum", ["=", "j", ["-", 3, "i"]], 3, ["idx", "limb_shift", "j"]]]]]]} + # Multiplicities [[variables.multiplicity]] @@ -257,9 +262,10 @@ multiplicity = "μ" [[constraints.limb_shifting]] kind = "arith" -constraint = "$#`shifted[i]` = #`left` dot sum_(j=0)^i #`limb_shift[j]` dot #`intra_limb_left[i-j]` + #`right` dot (sum_(j=0)^(3-i) #`limb_shift[j]` dot #`intra_limb_right[i+j]` + #`extension` dot sum_(j=3-i)^3 #`limb_shift[j]`)$" -poly = ["-", ["idx", "shifted", "i"], ["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_left", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_right", ["+", "i", "j"]]]], ["*", "extension", ["sum", ["=", "j", ["-", 3, "i"]], 3, ["idx", "limb_shift", "j"]]]]]]] -range = ["i", 0, 3] +constraint = "$#`out[:2]` = #`shifted[:4]`$" +poly = ["-", ["idx", "out", "i"], ["idx", ["cast", "shifted", "DWordWL"], "i"]] +range = ["i", 0, 1] +ref = "shift:c:out_eq_shifted" # Lookups @@ -271,6 +277,6 @@ name = "lookups" kind = "interaction" tag = "SHIFT" input = ["in", "shift", "direction", "signed", "word_instr"] -output = "shifted" +output = "out" multiplicity = "-μ" ref = "shift:c:lookup" From 055c228754e2a6812bbb7d75179dd4cc3bf2f3a5 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 7 Jan 2026 15:30:05 +0100 Subject: [PATCH 24/32] spec: SHIFT --- spec/shift.typ | 4 +--- spec/src/shift.toml | 6 ------ 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 6a00eef07..088967c54 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -74,9 +74,7 @@ Lastly, `X` and `Y` are combined in the right way to form the limbs of `output`. #render_constraint_table(chip, config, groups: "limb_shifting") === Miscellaneous -To make sure `left` is actually a `Bit`, we introduce constraint @shift:c:direction_implies_mu. -Moreover, @shift:c:is_negative_if_signed is included to compute if `in` is negative. -Since `in` cannot be negative in the unsigned case, @shift:c:is_negative_if_unsigned constrains that `is_negative` will be $0$ in that case. +To make sure `left` is actually a `Bit`, we introduce constraint @shift:c:direction_implies_mu. #render_constraint_table(chip, config, groups: "left_flag") #render_constraint_table(chip, config, groups: "is_negative") diff --git a/spec/src/shift.toml b/spec/src/shift.toml index f7e96c887..e72927f20 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -164,12 +164,6 @@ output = "is_negative" multiplicity = "signed" ref = "shift:c:is_negative_if_signed" -[[constraints.is_negative]] -kind = "arith" -constraint = "$#`!signed` => #`is_negative` = 0$" -poly = ["*", ["not", "signed"], "is_negative"] -ref = "shift:c:is_negative_if_unsigned" - [[constraint_groups]] name = "bit_shift" From d06fb88d82d942b6b705fe23243aefc592420106 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 7 Jan 2026 17:22:49 +0100 Subject: [PATCH 25/32] spec: SHIFT: introduce explanation; update some constraint elaborations --- spec/shift.typ | 82 ++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 73 insertions(+), 9 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 088967c54..ded2c26a8 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -57,26 +57,90 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed usin == Assumptions #render_chip_assumptions(chip, config) +== Explanation +This chip has a rather complex design as a result of designing it to fit in as few columns possible. +We briefly discuss the intricacies of the design, attempting to illustrate on its correctness. + +The chip's design revolves around a two-phase shifting process: +1. shift `in` by $#`shift` mod 16$ bits, +2. shift that result by $`shift` mod 64$ (or $mod 32$ if $ #`word_instr` = 1$). +The intermediate value representing the state between the two phases is stored in the scratch variables `X` and `Y`. +The definition of `shifted` describes how one can combine the `X`, `Y` and `extension` variables to constructed the output value as described using `Half`-limbs. +The output variable `out` is equivalent to `shifted`, but expressed using `Word`-limbs. + +=== First phase +We zoom in on the first step. +Here, we make use of the two lookup operations +- $#`HWSL[x: Half, y: B4]` := (#`x` #`<<` #`y`) mod 2^16$, and +- $#`HWSLC[x: Half, y: B4]` := #`x` #`>>` (16-#`y`)$ +Note here that one can use these two lookups to compute `out: Half[4] := in << y` as: +$ + #`out[`i#`]` = cases( + #`HWSL[in[`0#`], y]` &"if" i = 0, + #`HWSL[in[`i#`], y] || HWSLC[in[`i-1#`], y]` &"if" i > 0 + ) +$ +as long as $#`y` < 16$. +Observing that +$#`HWSL[x,` 16-#`y]` = (#`x` #`<<` (16-#`y`)) mod 2^16$, and +$#`HWSLC[x,` 16-#`y]` = #`x` #`>>` #`y`$ for $#`y` in [1, 15]$, +one can also use these lookups to compute `out := in >> y` as +$ + #`out[`i#`]` = cases( + #`HWSLC[in[`i#`],` 16-#`y] || HWSL[in[`i+1#`], y]` &"if" i < 3, + #`HWSL[in[`3#`],` 16-#`y]` &"if" i = 3 + ) +$ +as long as $0 < #`y` < 16$. + +Observe now that the values being looked up are (almost) only independent from the direction of the shift: only the shift-amount varies slightly. +When we now define +$ + #`bit_shift` := cases( + #`shift` mod 16 & "when shifting left", + (16-#`shift`) mod 16 & "when shifting right" + ), +$ +it only takes some rearranging and combining of the values $#`X[`i#`] := HWSL[in[`i#`], bit_shift]`$ and $#`Y[`i#`] := HWSLC[in[`i#`], bit_shift]`$ to form the limbs of $#`in <> shift` mod 16$. +In the exceptional case that `right = 1` and $#`shift` = 0 mod 16$, the limbs of $#`in <> shift` mod 16$ simply match those of `in`. + +=== Second phase +Note that, since we're operating on 16-bit limbs, all the limbs in $#`in <> shift`$ must also occur somewhere in $#`in <> shift` mod 16$. +The number of full-limbs we still need to shift is determined by the fifth and sixth least significant bit of `shift`. +With `limb_shift` containing a unary decoding of the integer represented by these two bits, we find that the intermediate value needs to be shifted over by $i$ limbs (to the `left` or `right`) when $#`limb_shift[`i#`]` = 1$. +These things combined yield `shifted`'s definition. + +Of course, when $#`word_instr` = 1$ and, thus, only $#`shift` mod 32$ should be considered, the bit-mask for the lookup constraining `limb_shift` is adjusted appropriately (see @shift:c:limb_shift_lookup). + +=== Arithmetic right shift +Lastly, we discuss the case of performing the _arithmetic_ right shift. +Here, `extension` is constrained to contain a repetition of `in`'s most significant bit. +Copies of this variable are used for any full limbs shifted in when $#`right` = #`signed` = 1$. +Moreover, `X[4]` contains a copy of `extension` shifted over by the right number of bits, to allow the construction of $#`in >>> shift` mod 16$ as the appropriate intermediate. + == Constraints First, we constraint `bit_shift` based on whether we are left or right-shifting. +@shift:c:zbs makes sure `zbs` is set to `1` if and only if `bit_shift = 0`. +This flag is used to indicate the special case that $#`right` = 1$ and $#`shift` = 0 mod 16$. #render_constraint_table(chip, config, groups: "bit_shift") -Next, we apply shift the limbs of `in` left and right, storing them in `X` and `Y` respectively. -When `right`-shifting and `bit_shift = 0`, the output is incorrect. -As such, we override `Y[i] := in[i]` and `X[i] := 0`. +Next, we shift the limbs of `in` left and right by the appropriate amount, storing the results in `X` and `Y` respectively. +When `zbs = 1`, the output cannot be used to compose $#`in >>/>>> shift` mod 16$. +To resolve this, we override `Y[i] := in[i]` and `X[i] := 0` in this case. -The case of `left`-shifting and `bit_shift = 0` will be used for padding rows. -To prevent unnecessary lookups in padding rows, we also override `X[i] := in[i]` and `Y[i] := 0` in this case. +The case of `left`-shifting and $#`bit_shift` = 0$ will be used for padding rows. +To prevent unnecessary lookups in padding rows, we override $#`X[i]` := #`in[i]`$ and $#`Y[i]` := 0$ here. #render_constraint_table(chip, config, groups: "intra_limb_shift") === Full-limb shifting -Lastly, `X` and `Y` are combined in the right way to form the limbs of `output`. +Next, we only have to constrain that `limb_shift` is a proper unary encoding of the fifth (and sixth if `word_instr = 0`) bit of `shift`. +Hereafter, one must only check that `out` is the proper cast of `shifted` into a `DWordWL`. #render_constraint_table(chip, config, groups: "limb_shifting") === Miscellaneous -To make sure `left` is actually a `Bit`, we introduce constraint @shift:c:direction_implies_mu. -#render_constraint_table(chip, config, groups: "left_flag") -#render_constraint_table(chip, config, groups: "is_negative") +#render_constraint_table(chip, config, groups: ("left_flag", "is_negative")) +*Note*: `is_negative` is not used when `signed = 0`. +As such, there is no problem with it being unconstrained in this case. === Lookups This chip adds the following interaction to the lookup. From 8aa5da304403bdf7cbef09baebca7ef35995973b Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Thu, 8 Jan 2026 09:42:51 +0100 Subject: [PATCH 26/32] Apply suggestions from the code review Co-authored-by: Robin Jadoul --- spec/shift.typ | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index ded2c26a8..48b5aada0 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -77,7 +77,7 @@ Note here that one can use these two lookups to compute `out: Half[4] := in << y $ #`out[`i#`]` = cases( #`HWSL[in[`0#`], y]` &"if" i = 0, - #`HWSL[in[`i#`], y] || HWSLC[in[`i-1#`], y]` &"if" i > 0 + #`HWSL[in[`i#`], y] | HWSLC[in[`i-1#`], y]` &"if" i > 0 ) $ as long as $#`y` < 16$. @@ -87,13 +87,13 @@ $#`HWSLC[x,` 16-#`y]` = #`x` #`>>` #`y`$ for $#`y` in [1, 15]$, one can also use these lookups to compute `out := in >> y` as $ #`out[`i#`]` = cases( - #`HWSLC[in[`i#`],` 16-#`y] || HWSL[in[`i+1#`], y]` &"if" i < 3, + #`HWSLC[in[`i#`],` 16-#`y] | HWSL[in[`i+1#`], y]` &"if" i < 3, #`HWSL[in[`3#`],` 16-#`y]` &"if" i = 3 ) $ as long as $0 < #`y` < 16$. -Observe now that the values being looked up are (almost) only independent from the direction of the shift: only the shift-amount varies slightly. +Observe now that the values being looked up are (almost) independent from the direction of the shift: only the shift-amount varies slightly. When we now define $ #`bit_shift` := cases( @@ -102,10 +102,10 @@ $ ), $ it only takes some rearranging and combining of the values $#`X[`i#`] := HWSL[in[`i#`], bit_shift]`$ and $#`Y[`i#`] := HWSLC[in[`i#`], bit_shift]`$ to form the limbs of $#`in <> shift` mod 16$. -In the exceptional case that `right = 1` and $#`shift` = 0 mod 16$, the limbs of $#`in <> shift` mod 16$ simply match those of `in`. +In the remaining case that `right = 1` and $#`shift` = 0 mod 16$, the limbs of $#`in <> shift` mod 16$ simply match those of `in`. === Second phase -Note that, since we're operating on 16-bit limbs, all the limbs in $#`in <> shift`$ must also occur somewhere in $#`in <> shift` mod 16$. +Since we're operating on 16-bit limbs, all the limbs in $#`in <> shift`$ must also occur somewhere in $#`in <> shift` mod 16$. The number of full-limbs we still need to shift is determined by the fifth and sixth least significant bit of `shift`. With `limb_shift` containing a unary decoding of the integer represented by these two bits, we find that the intermediate value needs to be shifted over by $i$ limbs (to the `left` or `right`) when $#`limb_shift[`i#`]` = 1$. These things combined yield `shifted`'s definition. From c5241889f45b4591864fab3136472941b6dacf6e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 8 Jan 2026 09:32:29 +0100 Subject: [PATCH 27/32] spec: SHIFT: update `bits_shift` desc --- spec/src/shift.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index e72927f20..31aa5b49e 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -45,7 +45,7 @@ desc = "Whether `in` is negative" [[variables.auxiliary]] name = "bit_shift" type = "Byte" -desc = "Value by which to shift `in` to obtain `bit_shifted`" +desc = "Value by which to shift `in` to obtain `X` and `Y`" [[variables.auxiliary]] name = "zbs" From 725c55adf902ca4641a0d627de3ee8a6e6574771 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 8 Jan 2026 09:34:12 +0100 Subject: [PATCH 28/32] spec: SHIFT: update `limb_shift` desc --- spec/src/shift.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 31aa5b49e..b2adeb0a2 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -65,7 +65,7 @@ desc = "scratch variable." [[variables.auxiliary]] name = "limb_shift" type = ["Bit", 4] -desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod 4$." +desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod s$, where $s = 2$ when $#`word_instr` = 1$ and $4$ otherwise.." # Virtual From 4753deed639674214601f98bf52dfb62248e16fb Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 8 Jan 2026 11:09:58 +0100 Subject: [PATCH 29/32] spec: SHIFT: add missing IS_BIT constraint for limb_shift --- spec/src/shift.toml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/spec/src/shift.toml b/spec/src/shift.toml index b2adeb0a2..17ce27f35 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -246,6 +246,13 @@ ref = "shift:c:zbs_implies_Y" [[constraint_groups]] name = "limb_shifting" +[[constraints.limb_shifting]] +kind = "template" +tag = "IS_BIT" +input = [["idx", "limb_shift", "i"]] +range = ["i", 0, 3] +ref = "shift:c:limb_shift_is_bit" + [[constraints.limb_shifting]] kind = "interaction" tag = "AND_BYTE" From ce4ebf54e91b25246b061022c029d334d1b0a083 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 8 Jan 2026 11:10:12 +0100 Subject: [PATCH 30/32] spec: SHIFT: update description --- spec/shift.typ | 48 ++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 38 insertions(+), 10 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index 48b5aada0..f907cbff7 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -62,22 +62,25 @@ This chip has a rather complex design as a result of designing it to fit in as f We briefly discuss the intricacies of the design, attempting to illustrate on its correctness. The chip's design revolves around a two-phase shifting process: -1. shift `in` by $#`shift` mod 16$ bits, -2. shift that result by $`shift` mod 64$ (or $mod 32$ if $ #`word_instr` = 1$). +1. shift `in` by $x := #`shift` mod 16$ bits, +2. shift that result by $(#`shift`-x) mod 64$ (or $mod 32$ if $ #`word_instr` = 1$). The intermediate value representing the state between the two phases is stored in the scratch variables `X` and `Y`. -The definition of `shifted` describes how one can combine the `X`, `Y` and `extension` variables to constructed the output value as described using `Half`-limbs. +The definition of `shifted` describes how one can combine the `X`, `Y` and `extension` variables to construct the output value as described using `Half`-limbs. The output variable `out` is equivalent to `shifted`, but expressed using `Word`-limbs. +In the following, we cover how these two phases were designed to complement one another. +Here, we start with discussing the _logical_ left/right shift operations only; the modifications required to compute the _arithmetic_ right shift will be discussed at the end. + === First phase We zoom in on the first step. Here, we make use of the two lookup operations -- $#`HWSL[x: Half, y: B4]` := (#`x` #`<<` #`y`) mod 2^16$, and -- $#`HWSLC[x: Half, y: B4]` := #`x` #`>>` (16-#`y`)$ +- $#`HWSL[x: Half, y: B4]` := (#`x` #`<<` #`y`) mod 2^16$ (short for "HalfWord Shift Left"), and +- $#`HWSLC[x: Half, y: B4]` := #`x` #`>>` (16-#`y`)$ (short for "HalfWord Shift Left's Carry") Note here that one can use these two lookups to compute `out: Half[4] := in << y` as: $ #`out[`i#`]` = cases( #`HWSL[in[`0#`], y]` &"if" i = 0, - #`HWSL[in[`i#`], y] | HWSLC[in[`i-1#`], y]` &"if" i > 0 + #`HWSL[in[`i#`], y] | HWSLC[in[`i-1#`], y]` &"if" i in [1, 3] ) $ as long as $#`y` < 16$. @@ -87,8 +90,8 @@ $#`HWSLC[x,` 16-#`y]` = #`x` #`>>` #`y`$ for $#`y` in [1, 15]$, one can also use these lookups to compute `out := in >> y` as $ #`out[`i#`]` = cases( - #`HWSLC[in[`i#`],` 16-#`y] | HWSL[in[`i+1#`], y]` &"if" i < 3, - #`HWSL[in[`3#`],` 16-#`y]` &"if" i = 3 + #`HWSLC[in[`i#`],` 16-#`y] | HWSL[in[`i+1#`], y]` &"if" i in [0, 2], + #`HWSLC[in[`3#`],` 16-#`y]` &"if" i = 3 ) $ as long as $0 < #`y` < 16$. @@ -102,7 +105,7 @@ $ ), $ it only takes some rearranging and combining of the values $#`X[`i#`] := HWSL[in[`i#`], bit_shift]`$ and $#`Y[`i#`] := HWSLC[in[`i#`], bit_shift]`$ to form the limbs of $#`in <> shift` mod 16$. -In the remaining case that `right = 1` and $#`shift` = 0 mod 16$, the limbs of $#`in <> shift` mod 16$ simply match those of `in`. +In the remaining case that $#`right` = 1$ and $#`shift` = 0 mod 16$, the limbs of $#`in <> shift` mod 16$ simply match those of `in`. === Second phase Since we're operating on 16-bit limbs, all the limbs in $#`in <> shift`$ must also occur somewhere in $#`in <> shift` mod 16$. @@ -133,7 +136,32 @@ To prevent unnecessary lookups in padding rows, we override $#`X[i]` := #`in[i]` #render_constraint_table(chip, config, groups: "intra_limb_shift") === Full-limb shifting -Next, we only have to constrain that `limb_shift` is a proper unary encoding of the fifth (and sixth if `word_instr = 0`) bit of `shift`. +Next, we constrain that `limb_shift` is a proper unary encoding of the fifth (and sixth if $#`word_instr` = 0$) bit of `shift`. +For this to be the case, three requirements must be satisfied: ++ *unary(0)*: $#`limb_shift[`i#`]` in {0, 1}$ for $i in [0, 3]$, ++ *unary(1)*: $#`limb_shift[`i#`]` = 1$ for exactly one $i$, and ++ *proper encoding*: $#`limb_shift[`i#`]` = 1 <=> 1/16 (#`shift &` (48-32 dot #`word_instr`)) = i$ +The first requirement is enforced by constraint @shift:c:limb_shift_is_bit. +To construct a constraint for the second and third requirement, observe that +$ +1/16 dot (#`shift &` (48-32 dot #`word_instr`)) in cases( + {0, 1, 2, 3} &"if" #`word_instr` = 0, + {0, 1} &"if" #`word_instr` = 1 +) +$ +Observe moreover that, assuming *unary(0)*, the expression +$ + 1/16 dot (1 + sum_(i=0)^3 (16i-1) dot #`limb_shift[`i#`]`) +$ +can evaluate to $i$ if and only if $#`limb_shift[`i#`]` = 1$, while the others are $0$. +This means that the relation +$ + 1 + sum_(i=0)^3 (16i-1) dot #`limb_shift[`i#`]` = #`shift &` (48-32 dot #`word_instr`) +$ +enforces both *unary(1)* and *proper encoding*. +This is the exact relation @shift:c:limb_shift_lookup enforces. + + Hereafter, one must only check that `out` is the proper cast of `shifted` into a `DWordWL`. #render_constraint_table(chip, config, groups: "limb_shifting") From a0822a3f1aefe5929ec8a2d57f0e90053aaa5d53 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 8 Jan 2026 11:55:25 +0100 Subject: [PATCH 31/32] spec: SHIFT: fix sum's expr-to-math --- spec/expr.typ | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/spec/expr.typ b/spec/expr.typ index e29905e1c..547f2cad2 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -137,7 +137,10 @@ "+": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(PREC.add)).join($+$)$, pp < PREC.add), "sum": (pp, rec, e) => { assert(e.len() == 4, message: "invalid sum:" + repr(e)) - mwrap($sum_(#rec(PREC.MAX, e.at(1)))^#rec(PREC.MAX, e.at(2)) #rec(PREC.sum, e.at(3))$, pp < 5) + mwrap( + $sum_(#rec(PREC.MAX, e.at(1)))^#rec(PREC.MAX, e.at(2)) #rec(if pp <= PREC.sub {PREC.MAX} else {PREC.sum}, e.at(3))$, + pp <= PREC.sub + ) }, "*": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(PREC.mul)).join($dot$)$, pp < PREC.mul), "/": (pp, rec, e) => $#rec(PREC.div, e.at(1)) / #rec(PREC.div, e.at(2))$, From fa7e0576207e7eee9366c133e0f30d1f6610964b Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Fri, 9 Jan 2026 09:10:51 +0100 Subject: [PATCH 32/32] Minor language pass Co-authored-by: Robin Jadoul --- spec/shift.typ | 4 ++-- spec/src/shift.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/shift.typ b/spec/shift.typ index f907cbff7..3555d64e4 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -59,7 +59,7 @@ The `SHIFT` chip is comprised of #nr_variables variables that are expressed usin == Explanation This chip has a rather complex design as a result of designing it to fit in as few columns possible. -We briefly discuss the intricacies of the design, attempting to illustrate on its correctness. +We briefly discuss the intricacies of the design, attempting to illustrate its correctness. The chip's design revolves around a two-phase shifting process: 1. shift `in` by $x := #`shift` mod 16$ bits, @@ -122,7 +122,7 @@ Copies of this variable are used for any full limbs shifted in when $#`right` = Moreover, `X[4]` contains a copy of `extension` shifted over by the right number of bits, to allow the construction of $#`in >>> shift` mod 16$ as the appropriate intermediate. == Constraints -First, we constraint `bit_shift` based on whether we are left or right-shifting. +First, we constrain `bit_shift` based on whether we are left or right-shifting. @shift:c:zbs makes sure `zbs` is set to `1` if and only if `bit_shift = 0`. This flag is used to indicate the special case that $#`right` = 1$ and $#`shift` = 0 mod 16$. #render_constraint_table(chip, config, groups: "bit_shift") diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 17ce27f35..e2ddfa12b 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -65,7 +65,7 @@ desc = "scratch variable." [[variables.auxiliary]] name = "limb_shift" type = ["Bit", 4] -desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod s$, where $s = 2$ when $#`word_instr` = 1$ and $4$ otherwise.." +desc = "One-hot vector indicating whether $floor.l #`shift` / 16 floor.r equiv i mod s$, where $s = 2$ when $#`word_instr` = 1$ and $4$ otherwise." # Virtual