diff --git a/spec/bitwise.typ b/spec/bitwise.typ index d0b3d89e2..06a2ce822 100644 --- a/spec/bitwise.typ +++ b/spec/bitwise.typ @@ -42,5 +42,4 @@ The following ideas may prove to be optimizations for the #bitwise chip: + Drop `MSB8` column, and instead define the `MSB8` lookup as `MSB8 := MSB16[256X]`. Note: currently, `MSB8` also implicity range checks the input `X` (the lookup fails if `X` is not a `Byte`). This optimization should only be executed when all chips leveraging `MSB8` do _not_ need this implicit range check. -+ Place the 16-bit (`AND`, `OR`, `XOR`, `MSB16`, etc.) and 20-bit (`HWSL`, `HWSLC`, `IS_B20`, `ZERO`) lookups in separate tables. -+ Combine `HWSL` and `HWSLC` into a single lookup (see also \#119). ++ Place the 16-bit (`AND`, `OR`, `XOR`, `MSB16`, etc.) and 20-bit (`HWSL`, `IS_B20`, `ZERO`) lookups in separate tables. diff --git a/spec/shift.typ b/spec/shift.typ index b705adb32..289ade1d7 100644 --- a/spec/shift.typ +++ b/spec/shift.typ @@ -59,25 +59,24 @@ Here, we start with discussing the _logical_ left/right shift operations only; t == 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$ (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: +Here, we make use of the lookup operation `HWSL` (short for "HalfWord Shift Left"): +$ #`HWSL[x: Half, y: B4]` := [(#`x` #`<<` #`y`) mod 2^16, #`x` #`>>` (16 - #`y`)]. $ +One can use this 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 in [1, 3] + #`HWSL[in[`0#`], y]`_0 &"if" i = 0, + #`HWSL[in[`i#`], y]`_0 | #`HWSL[in[`i-1#`], y]`_1 &"if" i in [1, 3] ) $ 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 +$#`HWSL[x,` 16-#`y]`_0 = (#`x` #`<<` (16-#`y`)) mod 2^16$, and +$#`HWSL[x,` 16-#`y]`_1 = #`x` #`>>` #`y`$ for $#`y` in [1, 15]$, +one can also use it to compute `out := in >> y` as $ #`out[`i#`]` = cases( - #`HWSLC[in[`i#`],` 16-#`y] | HWSL[in[`i+1#`], y]` &"if" i in [0, 2], - #`HWSLC[in[`3#`],` 16-#`y]` &"if" i = 3 + #`HWSL[in[`i#`],` 16-#`y]`_1 | #`HWSL[in[`i+1#`], y]`_0 &"if" i in [0, 2], + #`HWSL[in[`3#`],` 16-#`y]`_1 &"if" i = 3 ) $ as long as $0 < #`y` < 16$. @@ -90,7 +89,7 @@ $ (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$. +it only takes some rearranging and combining of the values $#`X[`i#`] := HWSL[in[`i#`], bit_shift]`_0$ and $#`Y[`i#`] := HWSL[in[`i#`], bit_shift]`_1$ 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`. == Second phase diff --git a/spec/src/bitwise.toml b/spec/src/bitwise.toml index 75e8faee4..67d73facd 100644 --- a/spec/src/bitwise.toml +++ b/spec/src/bitwise.toml @@ -116,11 +116,6 @@ name = "μ_HWSL" type = "BaseField" desc = "" -[[variables.multiplicity]] -name = "μ_HWSLC" -type = "BaseField" -desc = "" - [[constraint_groups]] name = "contributions" @@ -189,12 +184,5 @@ multiplicity = ["-", "μ_IS_B20"] kind = "interaction" tag = "HWSL" input = [["+", "X", ["*", 256, "Y"]], "Z"] -output = "SLL" +output = ["arr", "SLL", "SLLC"] multiplicity = ["-", "μ_HWSL"] - -[[constraints.contributions]] -kind = "interaction" -tag = "HWSLC" -input = [["+", "X", ["*", 256, "Y"]], "Z"] -output = "SLLC" -multiplicity = ["-", "μ_HWSLC"] diff --git a/spec/src/shift.toml b/spec/src/shift.toml index 45c00b064..bbe22a5d9 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -74,13 +74,22 @@ desc = "scratch variable." pad = ["arr", 0, 0, 0, 0] [[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." -pad = ["arr", 0, 0, 0, 0] +name = "limb_shift_raw" +type = ["Bit", 3] +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. These columns store the first 3 values, and the 4th is derived from the one-hot property." +pad = ["arr", 0, 0, 0] # Virtual +[[variables.virtual]] +name = "limb_shift" +type = ["Bit", 4] +desc = "" +def = {idx = "i", polys = [ + {iter = [0, 2], poly = ["idx", "limb_shift_raw", "i"]}, + {iter = 3, poly = ["-", 1, ["sum", ["=", "j", 0], 2, ["idx", "limb_shift_raw", "j"]]]}, +]} + [[variables.virtual]] name = "extension" type = "Half" @@ -118,7 +127,7 @@ def = {idx="i", iter=[0, 3], poly=["+", ["idx", "Y", "i"], ["idx", "X", ["+", "i name = "shifted" type = "DWordHL" desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" -def = {idx="i", iter=[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"]]]]]]} +def = {idx="i", iter=[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", ["-", 4, "i"]], 3, ["idx", "limb_shift", "j"]]]]]]} # Multiplicities @@ -192,7 +201,7 @@ multiplicity = "left" [[constraints.bit_shift]] kind = "interaction" tag = "AND_BYTE" -input = [["-", ["^", 2, 8], "shift"], 0x0F] +input = [["-", ["^", 2, 8], ["*", 16, "zbs"], "shift"], 0x0F] output = "bit_shift" ref = "shift:c:bit_shift_if_right" multiplicity = "right" @@ -213,7 +222,7 @@ name = "intra_limb_shift" kind = "interaction" tag = "HWSL" input = [["idx", "in", "i"], "bit_shift"] -output = ["idx", "X", "i"] +output = ["arr", ["idx", "X", "i"], ["idx", "Y", "i"]] iter = ["i", 0, 3] ref = "shift:c:hwsl_if_not_zero" multiplicity = ["not", "zbs"] @@ -225,11 +234,18 @@ poly = ["*", "zbs", ["-", ["idx", "X", "i"], ["*", ["idx", "in", "i"], "left"]]] iter = ["i", 0, 3] ref = "shift:c:zbs_implies_X" +[[constraints.intra_limb_shift]] +kind = "arith" +constraint = "$#`zbs` => #`Y[i]` = #`in[i]` dot #`right`$" +poly = ["*", "zbs", ["-", ["idx", "Y", "i"], ["*", ["idx", "in", "i"], "right"]]] +iter = ["i", 0, 3] +ref = "shift:c:zbs_implies_Y" + [[constraints.intra_limb_shift]] kind = "interaction" tag = "HWSL" input = ["extension", "bit_shift"] -output = ["idx", "X", 4] +output = ["arr", ["idx", "X", 4], ["-", "extension", ["idx", "X", 4]]] ref = "shift:c:hwsl_x4_if_not_zero" multiplicity = ["not", "zbs"] @@ -239,22 +255,6 @@ constraint = "$#`zbs` => #`X[4]` = 0$" poly = ["*", "zbs", ["idx", "X", 4]] ref = "shift:c:zbs_implies_X_4" -[[constraints.intra_limb_shift]] -kind = "interaction" -tag = "HWSLC" -input = [["idx", "in", "i"], "bit_shift"] -output = ["idx", "Y", "i"] -iter = ["i", 0, 3] -ref = "shift:c:hwslc_if_not_zero" -multiplicity = ["not", "zbs"] - -[[constraints.intra_limb_shift]] -kind = "arith" -constraint = "$#`zbs` => #`Y[i]` = #`in[i]` dot #`right`$" -poly = ["*", "zbs", ["-", ["idx", "Y", "i"], ["*", ["idx", "in", "i"], "right"]]] -iter = ["i", 0, 3] -ref = "shift:c:zbs_implies_Y" - [[constraint_groups]] name = "limb_shifting" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 69a839d2e..17ecd3933 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -180,14 +180,7 @@ input = ["B20"] tag = "HWSL" kind = "interaction" input = ["Half", "B4"] -output = "Half" - -# HWSLC[res; X, shift] -[[signatures]] -tag = "HWSLC" -kind = "interaction" -input = ["Half", "B4"] -output = "Half" +output = ["Half", 2] # The actual memory tokens, see MEMW and PAGE [[signatures]]