Update keccak HWSL constraints to equivalent arith constraints

spec/keccak.typ

@@ -84,6 +84,8 @@ That is, $#`rho_offset[x][y]` = #`rnc[x][y]` + 16 dot #`rbc[x][y][0]` + 32 dot #
 
 The following constraints ensure that `theta` captures the state after applying the first subpermutation of the round-permutation: $theta$.
 Note here that `Cxz_left` and `Cxz_right` do have to be range-checked; it cannot be assumed that this implicitly follows from @keccak:c:Dxz combined with `rotated_Cxz`'s definition.
+Both here and in the constraints for `rho`, we can represent a halfword shift by a byte amount directly with
+an arithmetic constraint, avoiding the need for an interaction with `HWSL`.
 #render_constraint_table(round_chip, config, groups: "theta")
 
 Next, we constrain that `rho` captures the state after applying subpermutation $rho$.
@@ -115,6 +117,8 @@ Lastly, the round chip contributes the following interactions to the lookup:
 - $#`rc[2]` = #`rc[4]` = #`rc[5]` = #`rc[6]` = 0$. As such, those elements need not be stored in `rc`, and need not be XORed into the state in the $iota$-step. This saves 8 columns and 4 `XOR_BYTE` interactions.
 - when executed in large volumnes, `KECCAK_RND` could benefit from having a three-way XOR lookup table. With this in place, the 80 interactions in @keccak:c:theta_cxz_start and @keccak:c:theta_cxz could be dropped.
   Likewise, 80 columns could be removed from the chip (a \~5% savings).
+- Since we don't need to strictly split `rho` into `Half`s for interactions with `HWSL`, we may be able to do a larger part of the round constant at once and reduce the need for `rbc`
+- At the cost of complicating the padding, the degree of the shift constraints in `theta` and `rho` can be reduced to 2, by omitting the dependency on the multiplicity.
 
 = Round constant lookup
 #let rc_chip = load_chip("src/keccak_rc.toml", config)
@@ -126,4 +130,4 @@ Lastly, the round chip contributes the following interactions to the lookup:
 
 We provide the round constants through a short precomputed lookup table: #keccak_rc.
 #render_chip_variable_table(rc_chip, config)
-#render_constraint_table(rc_chip, config)
+#render_constraint_table(rc_chip, config)

spec/src/keccak_round.toml

@@ -209,15 +209,14 @@ multiplicity = "μ"
 ref = "keccak:c:theta_cxz"
 
 [[constraints.theta]]
-kind = "interaction"
-tag = "HWSL"
-input = [["idx", ["cast", ["idx", ["idx", "Cxz", "x"], 3], "DWordHL"], "z"], 1]
-output = ["arr", 
-    ["idx", ["cast", ["idx", "Cxz_left", "x"], "DWordHL"], "z"], 
-    ["cast", ["idx", ["idx", "Cxz_right", "x"], "z"], "Half"]
-]
+kind = "arith"
+constraint = "$μ => 2 dot #`(Cxz[x][3] as DWordHL)[z]` = #`(Cxz_left[x] as DWordHL)[z]` + 2^16 dot #`Cxz_right[x][z]`$"
+poly = ["*", "μ", ["-",
+    ["*", 2, ["idx", ["cast", ["idx", ["idx", "Cxz", "x"], 3], "DWordHL"], "z"]],
+    ["idx", ["cast", ["idx", "Cxz_left", "x"], "DWordHL"], "z"],
+    ["*", ["^", 2, 16], ["idx", ["idx", "Cxz_right", "x"], "z"]]
+]]
 iters = [["x", 0, 4], ["z", 0, 3]]
-multiplicity = "μ"
 
 # Note: these IS_BYTE checks are necessary.
 # Without them, it is possible to prove 0 <<< S evaluates to -1 by setting
@@ -257,12 +256,14 @@ multiplicity = "μ"
 name = "rho"
 
 [[constraints.rho]]
-kind = "interaction"
-tag = "HWSL"
-input = [["idx", ["cast", ["idx", ["idx", "theta", "x"], "y"], "DWordHL"], "z"], ["idx", ["idx", "rnc", "x"], "y"]]
-output = ["arr", ["idx", ["cast", ["idx", ["idx", "rot_left", "x"], "y"], "DWordHL"], "z"], ["idx", ["cast", ["idx", ["idx", "rot_right", "x"], "y"], "DWordHL"], "z"]]
+kind = "arith"
+constraint = "$μ => 2^#`rnc[x][y]` dot #`(theta[x][y] as DWordHL)[z]` = #`(rot_left[x][y] as DWordHL)[z]` + 2^16 dot #`(rot_right[x][y] as DWordHL)[z]`$"
+poly = ["*", "μ", ["-",
+    ["*", ["^", 2, ["idx", ["idx", "rnc", "x"], "y"]], ["idx", ["cast", ["idx", ["idx", "theta", "x"], "y"], "DWordHL"], "z"]],
+    ["idx", ["cast", ["idx", ["idx", "rot_left", "x"], "y"], "DWordHL"], "z"],
+    ["*", ["^", 2, 16], ["idx", ["cast", ["idx", ["idx", "rot_right", "x"], "y"], "DWordHL"], "z"]]
+]]
 iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]]
-multiplicity = "μ"
 ref = "keccak:c:rho_rotation"
 
 # Note: these IS_BYTE checks are necessary.

spec/tooling/chip.py

@@ -1051,7 +1051,13 @@ def typecheck(self) -> Iterable[Signature]:
                 t = v.type
             typemap[v.name] = t
 
-        env = Environment(self.config, {}, typemap)
+        valmap = {}
+        for v in self.variables:
+            if v.category != "constant":
+                continue
+            valmap[v.name] = CastExpr(LitExpr(0), v.type).typecheck(Environment(self.config, {}, {}))
+
+        env = Environment(self.config, valmap, typemap)
         for v in self.virtual_vars:
             with reporter.context(v.name):
                 v.typecheck(env)