spec: Some fixes and improvements for SHIFT

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<X> := MSB16[256X]`.
   Note: currently, `MSB8` also implicity range checks the input `X` (the lookup fails if `X` is not a `Byte`).
   This optimization should only be executed when all chips leveraging `MSB8` do _not_ need this implicit range check.
-+ 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.

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

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"]

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"

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]]