From 211ae39371fe23f11259d64388f64b7e0763572b Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Fri, 24 Apr 2026 08:43:41 +0200
Subject: [PATCH 1/8] spec/keccak: fix cyclic-shift indexing mistakes

---
 spec/src/keccak_round.toml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml
index 548cb5151..eb715f4f8 100644
--- a/spec/src/keccak_round.toml
+++ b/spec/src/keccak_round.toml
@@ -75,7 +75,7 @@ desc = "state update following from step $iota$."
 name = "rotated_Cxz"
 type = [["Byte", 8], 5]
 desc = "$#`Cxz[x,`3#`,z]` <<< 1$"
-def = {iters=[["x", 0, 4], ["z", 0, 7]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], ["mod", ["-", "z", 1], 8]]]}
+def = {iters=[["x", 0, 4], ["z", 0, 7]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], ["mod", ["-", "z", 2], 8]]]}
 
 [[variables.virtual]]
 name = "out"
@@ -99,7 +99,7 @@ def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[
         ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1]],
         ["+",
             ["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"], 
-            ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 1], 8]],
+            ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 2], 8]],
         ]
     ],
     ["*", 
@@ -107,7 +107,7 @@ def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[
         ["not", ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1]],
         ["+",
             ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 2], 8]], 
-            ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 3], 8]],
+            ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 4], 8]],
         ]
     ],
     ["*",
@@ -115,7 +115,7 @@ def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[
         ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1],
         ["+",
             ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 4], 8]], 
-            ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 5], 8]],
+            ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 6], 8]],
         ]
     ],
     ["*", 
@@ -123,7 +123,7 @@ def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[
         ["idx", ["idx", ["idx", "rbc", "x"], "y"], 1],
         ["+",
             ["idx", ["idx", ["idx", "rot_left", "x"], "y"], ["mod", ["-", "z", 6], 8]], 
-            ["idx", ["idx", ["idx", "rot_right", "x"], "y"], ["mod", ["-", "z", 7], 8]],
+            ["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"],
         ]
     ],
 ]}

From 9904998505ddc3dc057256bf6bd75a3d7613bfdc Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Fri, 24 Apr 2026 08:49:16 +0200
Subject: [PATCH 2/8] spec/ecall: fix negative ECALL numbering

---
 spec/src/keccak.toml | 2 +-
 spec/src/sha256.toml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml
index b8f2d91c2..1c3bade44 100644
--- a/spec/src/keccak.toml
+++ b/spec/src/keccak.toml
@@ -48,7 +48,7 @@ name = "output"
 [[constraints.output]]
 kind = "interaction"
 tag = "ECALL"
-input = ["timestamp", ["arr", ["-", ["^", 2, 32], 1], ["-", ["^", 2, 32], 2]]]
+input = ["timestamp", ["cast", ["-", ["^", 2, 64], 2], "DWordWL"]]
 multiplicity = ["-", "μ"]
 
 [[constraint_groups]]
diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml
index 4cd4de9ba..faecd43ed 100644
--- a/spec/src/sha256.toml
+++ b/spec/src/sha256.toml
@@ -266,5 +266,5 @@ input = ["μ"]
 [[constraints.lookup]]
 kind = "interaction"
 tag = "ECALL"
-input = ["timestamp", ["arr", ["-", ["^", 2, 32], 1], ["-", ["^", 2, 32], 1]]]
+input = ["timestamp", ["cast", ["-", ["^", 2, 64], 1], "DWordWL"]]
 multiplicity = ["-", "μ"]

From d75944ee8438e9b087b831e39da0bca8f9f77150 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 28 Apr 2026 10:00:10 +0200
Subject: [PATCH 3/8] spec/keccak: optimize Cxz_right from Byte to Bit

---
 spec/src/keccak_round.toml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml
index eb715f4f8..bfe4cb5a2 100644
--- a/spec/src/keccak_round.toml
+++ b/spec/src/keccak_round.toml
@@ -28,8 +28,8 @@ desc = "the left-rotated component of `rotated_Cxz`"
 
 [[variables.auxiliary]]
 name = "Cxz_right"
-type = [["Byte", 8], 5]
-desc = "the right-rotated component of `rotated_Cxz`"
+type = [["Bit", 4], 5]
+desc = "the right-rotated component of `rotated_Cxz` (which is a single bit)"
 
 [[variables.auxiliary]]
 name = "Dxz"
@@ -75,7 +75,7 @@ desc = "state update following from step $iota$."
 name = "rotated_Cxz"
 type = [["Byte", 8], 5]
 desc = "$#`Cxz[x,`3#`,z]` <<< 1$"
-def = {iters=[["x", 0, 4], ["z", 0, 7]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], ["mod", ["-", "z", 2], 8]]]}
+def = {iters=[["x", 0, 4], ["z", 0, 7]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["*", ["-", 1, ["mod", "z", 2]], ["idx", ["idx", "Cxz_right", "x"], ["mod", ["-", ["/", "z", 2], 1], 4]]]]}
 
 [[variables.virtual]]
 name = "out"
@@ -202,7 +202,10 @@ ref = "keccak:c:theta_cxz"
 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"], ["idx", ["cast", ["idx", "Cxz_right", "x"], "DWordHL"], "z"]]
+output = ["arr", 
+    ["idx", ["cast", ["idx", "Cxz_left", "x"], "DWordHL"], "z"], 
+    ["cast", ["idx", ["idx", "Cxz_right", "x"], "z"], "Half"]
+]
 iters = [["x", 0, 4], ["z", 0, 3]]
 multiplicity = "μ"
 
@@ -218,11 +221,11 @@ iters = [["x", 0, 4], ["z", 0, 7]]
 multiplicity = "μ"
 
 [[constraints.theta]]
-kind = "interaction"
-tag = "IS_BYTE"
+kind = "template"
+tag = "IS_BIT"
 input = [["idx", ["idx", "Cxz_right", "x"], "z"]]
-iters = [["x", 0, 4], ["z", 0, 7]]
-multiplicity = "μ"
+iters = [["x", 0, 4], ["z", 0, 3]]
+cond = "μ"
 
 [[constraints.theta]]
 kind = "interaction"

From b07515841137c707f4cf567f638ae2f92e46724e Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 28 Apr 2026 10:29:07 +0200
Subject: [PATCH 4/8] spec/KECCAK: add potential optimization

rot_left and rot_right contain 96 constant zero-columns, which can be dropped. Additionally, those zeroes do not have to be byte-checked.
---
 spec/keccak.typ            | 4 ++++
 spec/src/keccak_round.toml | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/spec/keccak.typ b/spec/keccak.typ
index e6e16f43f..7ce968932 100644
--- a/spec/keccak.typ
+++ b/spec/keccak.typ
@@ -105,6 +105,10 @@ Lastly, the round chip contributes the following interactions to the lookup:
 == Notes/potential optimizations
 - one does not have to repeat `addr` in `state_ptr`; this saves 4 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.
+  This means 96 columns can be removed from the chip at no cost.
+  Likewise, 96 `IS_BYTE` interactions can be dropped from @keccak:c:range_rot_left and @keccak:c:range_rot_right.
 - $#`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).
diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml
index bfe4cb5a2..df3979a56 100644
--- a/spec/src/keccak_round.toml
+++ b/spec/src/keccak_round.toml
@@ -254,6 +254,7 @@ input = [["idx", ["cast", ["idx", ["idx", "theta", "x"], "y"], "DWordHL"], "z"],
 output = ["arr", ["idx", ["cast", ["idx", ["idx", "rot_left", "x"], "y"], "DWordHL"], "z"], ["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.
 # Without them, it is possible to prove 0 <<< S evaluates to -1 by setting
@@ -265,6 +266,7 @@ tag = "IS_BYTE"
 input = [["idx", ["idx", ["idx", "rot_left", "x"], "y"], "z"]]
 iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]]
 multiplicity = "μ"
+ref = "keccak:c:range_rot_left"
 
 [[constraints.rho]]
 kind = "interaction"
@@ -272,6 +274,7 @@ tag = "IS_BYTE"
 input = [["idx", ["idx", ["idx", "rot_right", "x"], "y"], "z"]]
 iters = [["x", 0, 4], ["y", 0, 4], ["z", 0, 7]]
 multiplicity = "μ"
+ref = "keccak:c:range_rot_right"
 
 [[constraint_groups]]
 name = "chi"

From f5af065dd6246019899b2b7e6fc45398cbe573a3 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 28 Apr 2026 10:29:45 +0200
Subject: [PATCH 5/8] spec/KECCAK: fix typo

---
 spec/src/keccak_round.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml
index df3979a56..408f43026 100644
--- a/spec/src/keccak_round.toml
+++ b/spec/src/keccak_round.toml
@@ -91,7 +91,7 @@ def = {polys=[
 [[variables.virtual]]
 name = "rho"
 type = [[["Byte", 8], 5], 5]
-desc = "$(rho compose theta)(#`start`)$; the state state after applying $rho$"
+desc = "$(rho compose theta)(#`start`)$; the state after applying $rho$"
 def = {iters=[["x", 0, 4], ["y", 0, 4], ["z", 0, 7]], poly=[
     "+", 
     ["*", 

From 7fa693d943db4f5f292277d223ad29aa8bcc8728 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 28 Apr 2026 12:20:08 +0200
Subject: [PATCH 6/8] spec/KECCAK: list another potential optimization

---
 spec/keccak.typ | 1 +
 1 file changed, 1 insertion(+)

diff --git a/spec/keccak.typ b/spec/keccak.typ
index 7ce968932..11d900c73 100644
--- a/spec/keccak.typ
+++ b/spec/keccak.typ
@@ -109,6 +109,7 @@ Lastly, the round chip contributes the following interactions to the lookup:
   Since `rnc` is constant, @keccak:c:rho_rotation makes those zero-bytes show up in `rot_left` and `rot_right` at constant locations.
   This means 96 columns can be removed from the chip at no cost.
   Likewise, 96 `IS_BYTE` interactions can be dropped from @keccak:c:range_rot_left and @keccak:c:range_rot_right.
+  - the shift-constants are equivalent to $1 mod 16$ for $(#`x`, #`y`) = (1, 0)$ and $-1 mod 16$ for $(2, 3)$. This means that for those lanes it suffices to constrain `rot_left`/`rot_right` as `Bit`s rather than `Byte`s, saving an additional 8 `IS_BYTE` interactions.
 - $#`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).

From 9143370f4cfa19a50b8237da3a39a6fe8a5e6966 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 28 Apr 2026 14:31:10 +0200
Subject: [PATCH 7/8] spec/keccak: fix index division problems

---
 spec/src/keccak_round.toml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml
index 408f43026..d8ae48bb5 100644
--- a/spec/src/keccak_round.toml
+++ b/spec/src/keccak_round.toml
@@ -75,7 +75,16 @@ desc = "state update following from step $iota$."
 name = "rotated_Cxz"
 type = [["Byte", 8], 5]
 desc = "$#`Cxz[x,`3#`,z]` <<< 1$"
-def = {iters=[["x", 0, 4], ["z", 0, 7]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["*", ["-", 1, ["mod", "z", 2]], ["idx", ["idx", "Cxz_right", "x"], ["mod", ["-", ["/", "z", 2], 1], 4]]]]}
+def = {polys=[
+    {iters=[["x", 0, 4], ["z", 0]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], 3]]},
+    {iters=[["x", 0, 4], ["z", 1]], poly=["idx", ["idx", "Cxz_left", "x"], "z"]},
+    {iters=[["x", 0, 4], ["z", 2]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], 0]]},
+    {iters=[["x", 0, 4], ["z", 3]], poly=["idx", ["idx", "Cxz_left", "x"], "z"]},
+    {iters=[["x", 0, 4], ["z", 4]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], 1]]},
+    {iters=[["x", 0, 4], ["z", 5]], poly=["idx", ["idx", "Cxz_left", "x"], "z"]},
+    {iters=[["x", 0, 4], ["z", 6]], poly=["+", ["idx", ["idx", "Cxz_left", "x"], "z"], ["idx", ["idx", "Cxz_right", "x"], 2]]},
+    {iters=[["x", 0, 4], ["z", 7]], poly=["idx", ["idx", "Cxz_left", "x"], "z"]},
+]}
 
 [[variables.virtual]]
 name = "out"

From b53d6c328457aa7ccb41f7b662ea738f37fc1f03 Mon Sep 17 00:00:00 2001
From: Erik Takke <erik.takke@3milabs.tech>
Date: Tue, 28 Apr 2026 17:25:47 +0200
Subject: [PATCH 8/8] spec/keccak: remove condition from IS_BIT

---
 spec/src/keccak_round.toml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml
index d8ae48bb5..727e1f346 100644
--- a/spec/src/keccak_round.toml
+++ b/spec/src/keccak_round.toml
@@ -234,7 +234,6 @@ kind = "template"
 tag = "IS_BIT"
 input = [["idx", ["idx", "Cxz_right", "x"], "z"]]
 iters = [["x", 0, 4], ["z", 0, 3]]
-cond = "μ"
 
 [[constraints.theta]]
 kind = "interaction"