spec/keccak: update core chip

Author: erik-3milabs

spec/keccak.typ

@@ -15,7 +15,14 @@
 #show: book-page(chip.name)
 #let keccak = raw(chip.name)
 
-The #keccak chip applies the keccak permutation.
+The #keccak chip applies the keccak permutation $kappa$ to a given memory range.
+
+This permutation $kappa: FF_2^1600 -> FF_2^1600$ operates on 1600 bits and is composed of 24 applications of round-permutation $Lambda: FF_2^1600 times NN -> FF_2^1600$, where the additional parameter is the round constant.
+$Lambda$ is defined as the composition $iota compose chi compose pi compose rho compose theta$, where only $iota$ depends on the round constant.
+#footnote("More details on the KECCAK permutation: FIPS 202, NIST, " + link("https://csrc.nist.gov/pubs/fips/202/final"))
+
+The keccak accelerator comprises two chips: a core chip that interacts with the memory, and a round chip that applies the round permutation.
+
 
 = Core chip
 == Columns
@@ -25,27 +32,21 @@ The #keccak chip applies the keccak permutation.
 The #keccak chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
 #render_chip_variable_table(chip, config)
 
-== Assumptions
-
-// #render_chip_assumptions(chip, config)
-
 == Constraints
 In this VM, we assign syscall number -2 to the #keccak accelerator.
 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 are passed in as argument `A0 = x10`.
-This address is read into `addr`, from which `state_ptr` --- the collection of pointers to all lanes of the state --- is derived.
-The state is then read into `input_state`, while the `output_state` is written back to the indicated address.
+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 state is then read into `input_state`, while the `output_state` is written back to the indicated address (@keccack:c:load_store_state).
 #render_constraint_table(chip, config, groups: "mem")
 
-Lastly, the input state is pushed to the Keccak-round function, while the output after 24 rounds is taken off the bus.
+Lastly, the input state is pushed to the Keccak-round function, while the output after 24 rounds is taken off the bus:
 #render_constraint_table(chip, config, groups: "round")
 
 == Padding
-
-The table can be padded to the next power of two with the following value assignments:
-
+The #keccak table can be padded to the next power of two with the following value assignments:
 #render_chip_padding_table(chip, config)
 
 = Round chip

spec/src/keccak.toml

@@ -60,13 +60,15 @@ tag = "MEMW"
 input = [1, ["cast", ["*", 2, 10], "DWordWL"], "addr", "timestamp", 1, 0, 0]
 output = "addr"
 multiplicity = "μ"
+ref = "keccak:c:read_addr"
 
 [[constraints.mem]]
 kind = "template"
 tag = "ADD"
 input = [["cast", "addr", "DWordWL"], ["cast", ["*", 8, ["+", ["*", 5, "x"], "y"]], "DWordWL"]]
 output = ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"]
 iters = [["x", 0, 4], ["y", 0, 4]]
+ref = "keccak:c:state_ptr"
 
 [[constraints.mem]]
 kind = "interaction"
@@ -82,6 +84,7 @@ input = [0, ["cast", ["idx", ["idx", "state_ptr", "x"], "y"], "DWordWL"], ["idx"
 output = ["idx", ["idx", "input_state", "x"], "y"]
 iters = [["x", 0, 4], ["y", 0, 4]]
 multiplicity = "μ"
+ref = "keccack:c:load_store_state"
 
 [[constraint_groups]]
 name = "round"