spec: fix keccak's addr handling

spec/keccak.typ

@@ -42,7 +42,7 @@ The chip therefore contributes the following interaction to the lookup-argument:
 #render_constraint_table(chip, config, groups: "output")
 
 The address containing the state to be permuted is passed in as argument `A0 = x10`.
-The following constraints describe that this address is read into `addr` (@keccak:c:read_addr), from which `state_ptr` --- the collection of pointers to all lanes of the state --- is derived (@keccak:c:state_ptr).
+The following constraints describe that this address is read into `state_ptr[0][0]` (@keccak:c:read_state_ptr), from which full `state_ptr` --- the collection of pointers to all lanes of the state --- is derived (@keccak:c:state_ptr); @keccak:c:range_state_ptr is included to satisfy @add:a:lhs respectively @add:a:sum.
 The state is then read into `input_state`, while the `output_state` is written back to the indicated address (@keccak:c:load_store_state).
 #render_constraint_table(chip, config, groups: "mem")
 
@@ -103,7 +103,9 @@ Lastly, the round chip contributes the following interactions to the lookup:
 #render_constraint_table(round_chip, config, groups: "io")
 
 == Notes/potential optimizations
-- one does not have to repeat `addr` in `state_ptr`; this saves 4 columns and 4 `IS_HALF` checks.
+- one does not have to range check `state_ptr[0][0]` since it is read from memory.
+  Moreover, it could be represented as a `DWordWL`. 
+  All this would save 2 columns and 4 `IS_HALF` checks.
 - step $rho$ does not need to be applied to `state[0][0]`; its has a zero-shift. This saves 16 columns and 4 `HWSL` interactions.
 - when the output of `HWSL` are `Byte`s mapped as `Half`s, we find that out of every four output bytes, at least one is zero. 
   Since `rnc` is constant, @keccak:c:rho_rotation makes those zero-bytes show up in `rot_left` and `rot_right` at constant locations.

spec/src/keccak.toml

@@ -6,12 +6,6 @@ type = "DWordWL"
 desc = "timestamp at which the permutation is performed"
 pad = 0
 
-[[variables.input]]
-name = "addr"
-type = "DWordBL"
-desc = "memory address storing the first bit of the state"
-pad = 0
-
 [[variables.input]]
 name = "input_state"
 type = [[["Byte", 8], 5], 5]
@@ -54,18 +48,19 @@ multiplicity = ["-", "μ"]
 [[constraint_groups]]
 name = "mem"
 
+
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["cast", ["*", 2, 10], "DWordWL"], "addr", "timestamp", 1, 0, 0]
-output = "addr"
+input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["arr", ["idx", ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], 0], ["idx", ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0]
+output = ["arr", ["idx", ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], 0], ["idx", ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
 multiplicity = "μ"
-ref = "keccak:c:read_addr"
+ref = "keccak:c:read_state_ptr"
 
 [[constraints.mem]]
 kind = "template"
 tag = "ADD"
-input = [["cast", "addr", "DWordWL"], ["cast", ["*", 8, ["+", ["*", 5, "y"], "x"]], "DWordWL"]]
+input = [["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], ["cast", ["*", 8, ["+", ["*", 5, "y"], "x"]], "DWordWL"]]
 output = ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"]
 iters = [["x", 0, 4], ["y", 0, 4]]
 ref = "keccak:c:state_ptr"
@@ -76,6 +71,7 @@ tag = "IS_HALF"
 input = [["idx", ["idx", ["idx", "state_ptr", "x"], "y"], "z"]]
 iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 3]]
 multiplicity = "μ"
+ref = "keccak:c:range_state_ptr"
 
 [[constraints.mem]]
 kind = "interaction"