diff --git a/Cryptlib.lean b/Cryptlib.lean
index 6031b209..be25c957 100644
--- a/Cryptlib.lean
+++ b/Cryptlib.lean
@@ -19,6 +19,7 @@ import Cryptlib.Util.UInt32
 import Cryptlib.Util.Serial
 import Cryptlib.Util.Combine
 import Cryptlib.Util.Bytes
+import Cryptlib.Util.ConstantTime
 import Cryptlib.Util.UniformHit
 import Cryptlib.Data.MerkleHashTree
 import Cryptlib.Primitives.KEM.KEM
diff --git a/Cryptlib/Primitives/Cipher/AES.lean b/Cryptlib/Primitives/Cipher/AES.lean
index 43db0638..66b8f0fa 100644
--- a/Cryptlib/Primitives/Cipher/AES.lean
+++ b/Cryptlib/Primitives/Cipher/AES.lean
@@ -7,8 +7,13 @@ namespace Cryptlib.Primitives.Cipher.AES
 
 /-! # AES-128 and AES-256
 
-Encryption direction only. The S-box is computed from its FIPS-197 definition rather than
-transcribed. Not constant time.
+Encryption direction only. The table S-box `sbox`, computed from its FIPS-197 definition rather
+than transcribed, and the bit-serial `mul` are the specification. `subBytes` instead evaluates the
+Boyar–Peralta S-box circuit, bitsliced across the bytes of the state, and `mixColumns` doubles with
+mask arithmetic; both are proved equal to the table versions. The cipher and key schedule are
+written without secret-dependent branches or secret-indexed memory accesses. Lean compiles through
+C, and neither compiler is proven to preserve that, so the machine code is not verified to be
+constant time.
 -/
 
 /-- Multiplication in `GF(2^8)` modulo AES's `x^8 + x^4 + x^3 + x + 1`. -/
@@ -45,6 +50,321 @@ def sboxByte (a : UInt8) : UInt8 :=
 /-- `sboxByte` tabulated over all 256 inputs. -/
 def sbox : Array UInt8 := (Array.range 256).map fun i => sboxByte (UInt8.ofNat i)
 
+def subBytesSpec (s : Array UInt8) : Array UInt8 := s.map fun b => sbox[b.toNat]!
+
+/-- Each column multiplied by the fixed polynomial `{03}x³ + {01}x² + {01}x + {02}`. -/
+def mixColumnsSpec (s : Array UInt8) : Array UInt8 :=
+  Array.ofFn fun i : Fin 16 =>
+    let a := fun j => s[4 * (i.val / 4) + j]!
+    match i.val % 4 with
+    | 0 => mul (a 0) 2 ^^^ mul (a 1) 3 ^^^ a 2 ^^^ a 3
+    | 1 => a 0 ^^^ mul (a 1) 2 ^^^ mul (a 2) 3 ^^^ a 3
+    | 2 => a 0 ^^^ a 1 ^^^ mul (a 2) 2 ^^^ mul (a 3) 3
+    | _ => mul (a 0) 3 ^^^ a 1 ^^^ a 2 ^^^ mul (a 3) 2
+
+/-! ## Constant-time S-box -/
+
+/-- The S-box circuit of Boyar and Peralta, "A depth-16 circuit for the AES S-box" (2011): 128
+gates, 34 of them AND, over any carrier of bitwise operations. `u0` is the most significant input
+bit, and the result lists the output bits from the most significant down. -/
+def sboxCircuit {α : Type} [XorOp α] [AndOp α] [Complement α] (u0 u1 u2 u3 u4 u5 u6 u7 : α) :
+    Vector α 8 :=
+  let t1 := u0 ^^^ u3
+  let t2 := u0 ^^^ u5
+  let t3 := u0 ^^^ u6
+  let t4 := u3 ^^^ u5
+  let t5 := u4 ^^^ u6
+  let t6 := t1 ^^^ t5
+  let t7 := u1 ^^^ u2
+  let t8 := u7 ^^^ t6
+  let t9 := u7 ^^^ t7
+  let t10 := t6 ^^^ t7
+  let t11 := u1 ^^^ u5
+  let t12 := u2 ^^^ u5
+  let t13 := t3 ^^^ t4
+  let t14 := t6 ^^^ t11
+  let t15 := t5 ^^^ t11
+  let t16 := t5 ^^^ t12
+  let t17 := t9 ^^^ t16
+  let t18 := u3 ^^^ u7
+  let t19 := t7 ^^^ t18
+  let t20 := t1 ^^^ t19
+  let t21 := u6 ^^^ u7
+  let t22 := t7 ^^^ t21
+  let t23 := t2 ^^^ t22
+  let t24 := t2 ^^^ t10
+  let t25 := t20 ^^^ t17
+  let t26 := t3 ^^^ t16
+  let t27 := t1 ^^^ t12
+  let m1 := t13 &&& t6
+  let m2 := t23 &&& t8
+  let m3 := t14 ^^^ m1
+  let m4 := t19 &&& u7
+  let m5 := m4 ^^^ m1
+  let m6 := t3 &&& t16
+  let m7 := t22 &&& t9
+  let m8 := t26 ^^^ m6
+  let m9 := t20 &&& t17
+  let m10 := m9 ^^^ m6
+  let m11 := t1 &&& t15
+  let m12 := t4 &&& t27
+  let m13 := m12 ^^^ m11
+  let m14 := t2 &&& t10
+  let m15 := m14 ^^^ m11
+  let m16 := m3 ^^^ m2
+  let m17 := m5 ^^^ t24
+  let m18 := m8 ^^^ m7
+  let m19 := m10 ^^^ m15
+  let m20 := m16 ^^^ m13
+  let m21 := m17 ^^^ m15
+  let m22 := m18 ^^^ m13
+  let m23 := m19 ^^^ t25
+  let m24 := m22 ^^^ m23
+  let m25 := m22 &&& m20
+  let m26 := m21 ^^^ m25
+  let m27 := m20 ^^^ m21
+  let m28 := m23 ^^^ m25
+  let m29 := m28 &&& m27
+  let m30 := m26 &&& m24
+  let m31 := m20 &&& m23
+  let m32 := m27 &&& m31
+  let m33 := m27 ^^^ m25
+  let m34 := m21 &&& m22
+  let m35 := m24 &&& m34
+  let m36 := m24 ^^^ m25
+  let m37 := m21 ^^^ m29
+  let m38 := m32 ^^^ m33
+  let m39 := m23 ^^^ m30
+  let m40 := m35 ^^^ m36
+  let m41 := m38 ^^^ m40
+  let m42 := m37 ^^^ m39
+  let m43 := m37 ^^^ m38
+  let m44 := m39 ^^^ m40
+  let m45 := m42 ^^^ m41
+  let m46 := m44 &&& t6
+  let m47 := m40 &&& t8
+  let m48 := m39 &&& u7
+  let m49 := m43 &&& t16
+  let m50 := m38 &&& t9
+  let m51 := m37 &&& t17
+  let m52 := m42 &&& t15
+  let m53 := m45 &&& t27
+  let m54 := m41 &&& t10
+  let m55 := m44 &&& t13
+  let m56 := m40 &&& t23
+  let m57 := m39 &&& t19
+  let m58 := m43 &&& t3
+  let m59 := m38 &&& t22
+  let m60 := m37 &&& t20
+  let m61 := m42 &&& t1
+  let m62 := m45 &&& t4
+  let m63 := m41 &&& t2
+  let l0 := m61 ^^^ m62
+  let l1 := m50 ^^^ m56
+  let l2 := m46 ^^^ m48
+  let l3 := m47 ^^^ m55
+  let l4 := m54 ^^^ m58
+  let l5 := m49 ^^^ m61
+  let l6 := m62 ^^^ l5
+  let l7 := m46 ^^^ l3
+  let l8 := m51 ^^^ m59
+  let l9 := m52 ^^^ m53
+  let l10 := m53 ^^^ l4
+  let l11 := m60 ^^^ l2
+  let l12 := m48 ^^^ m51
+  let l13 := m50 ^^^ l0
+  let l14 := m52 ^^^ m61
+  let l15 := m55 ^^^ l1
+  let l16 := m56 ^^^ l0
+  let l17 := m57 ^^^ l1
+  let l18 := m58 ^^^ l8
+  let l19 := m63 ^^^ l4
+  let l20 := l0 ^^^ l1
+  let l21 := l1 ^^^ l7
+  let l22 := l3 ^^^ l12
+  let l23 := l18 ^^^ l2
+  let l24 := l15 ^^^ l9
+  let l25 := l6 ^^^ l10
+  let l26 := l7 ^^^ l9
+  let l27 := l8 ^^^ l10
+  let l28 := l11 ^^^ l14
+  let l29 := l11 ^^^ l17
+  let s0 := l6 ^^^ l24
+  let s1 := ~~~(l16 ^^^ l26)
+  let s2 := ~~~(l19 ^^^ l28)
+  let s3 := l6 ^^^ l21
+  let s4 := l20 ^^^ l22
+  let s5 := l25 ^^^ l29
+  let s6 := ~~~(l13 ^^^ l27)
+  let s7 := ~~~(l6 ^^^ l23)
+  #v[s0, s1, s2, s3, s4, s5, s6, s7]
+
+/-- Lane `k` of a bit plane. -/
+def lane (k : Nat) (x : UInt64) : Bool := x.toBitVec.getLsbD k
+
+private def bitTerm (b : UInt8) (j m : Nat) : UInt64 :=
+  ((b >>> (7 - j).toUInt8) &&& 1).toUInt64 <<< m.toUInt64
+
+/-- Bit `7 - j` of the first `n` bytes, byte `k` in lane `k`. -/
+private def planeAux (s : Array UInt8) (j : Nat) : Nat → UInt64
+  | 0 => 0
+  | n + 1 => planeAux s j n ||| bitTerm s[n]! j n
+
+/-- Byte `k` of the result, gathered from lane `k` of the output planes. -/
+private def unpack (o : Vector UInt64 8) (k : Nat) : UInt8 :=
+  let b := fun j : Fin 8 => ((o[j] >>> k.toUInt64) &&& 1).toUInt8
+  b 0 <<< 7 ||| b 1 <<< 6 ||| b 2 <<< 5 ||| b 3 <<< 4 ||| b 4 <<< 3 ||| b 5 <<< 2 ||| b 6 <<< 1 |||
+    b 7
+
+/-- The S-box on up to 64 bytes at once, one byte per lane. -/
+private def sliced (s : Array UInt8) : Array UInt8 :=
+  let p := fun j => planeAux s j s.size
+  let o := sboxCircuit (p 0) (p 1) (p 2) (p 3) (p 4) (p 5) (p 6) (p 7)
+  Array.ofFn fun k : Fin s.size => unpack o k.val
+
+def subBytes (s : Array UInt8) : Array UInt8 :=
+  if s.size ≤ 64 then sliced s else s.map fun b => (sliced #[b])[0]!
+
+/-- Multiplication by `x`, reducing with a mask rather than a branch. -/
+def xtime (x : UInt8) : UInt8 := (x <<< 1) ^^^ ((0x1b : UInt8) &&& ((0 : UInt8) - (x >>> 7)))
+
+def mixColumns (s : Array UInt8) : Array UInt8 :=
+  Array.ofFn fun i : Fin 16 =>
+    let a := fun j => s[4 * (i.val / 4) + j]!
+    let d := fun j => xtime (a j)
+    match i.val % 4 with
+    | 0 => d 0 ^^^ d 1 ^^^ a 1 ^^^ a 2 ^^^ a 3
+    | 1 => a 0 ^^^ d 1 ^^^ d 2 ^^^ a 2 ^^^ a 3
+    | 2 => a 0 ^^^ a 1 ^^^ d 2 ^^^ d 3 ^^^ a 3
+    | _ => d 0 ^^^ a 0 ^^^ a 1 ^^^ a 2 ^^^ d 3
+
+/-! ### Agreement with the specification -/
+
+section
+local instance : XorOp Bool := ⟨Bool.xor⟩
+local instance : AndOp Bool := ⟨and⟩
+local instance : Complement Bool := ⟨not⟩
+
+private def ofBits (o : Vector Bool 8) : UInt8 :=
+  o[0].toUInt8 <<< 7 ||| o[1].toUInt8 <<< 6 ||| o[2].toUInt8 <<< 5 ||| o[3].toUInt8 <<< 4 |||
+    o[4].toUInt8 <<< 3 ||| o[5].toUInt8 <<< 2 ||| o[6].toUInt8 <<< 1 ||| o[7].toUInt8
+
+private def bit (b : UInt8) (i : Nat) : Bool := b.toBitVec.getLsbD i
+
+/-- The circuit on the bits of one byte. -/
+private def sboxBits (b : UInt8) : UInt8 :=
+  ofBits
+    (sboxCircuit (bit b 7) (bit b 6) (bit b 5) (bit b 4) (bit b 3) (bit b 2) (bit b 1) (bit b 0))
+
+private theorem sboxBits_eq_fin :
+    ∀ i : Fin 256, sboxBits (UInt8.ofNat i) = sboxByte (UInt8.ofNat i) := by
+  decide +kernel
+
+theorem sboxBits_eq (b : UInt8) : sboxBits b = sboxByte b := by
+  simpa using sboxBits_eq_fin ⟨b.toNat, b.toNat_lt⟩
+
+private theorem lane_xor (k : Nat) (a b : UInt64) : lane k (a ^^^ b) = (lane k a ^^^ lane k b) := by
+  simp [lane]; rfl
+
+private theorem lane_and (k : Nat) (a b : UInt64) : lane k (a &&& b) = (lane k a &&& lane k b) := by
+  simp [lane]; rfl
+
+private theorem lane_not (k : Nat) (hk : k < 64) (a : UInt64) : lane k (~~~a) = ~~~(lane k a) := by
+  show _ = not _
+  simp [lane, hk]
+
+/-- The bitsliced circuit computes the circuit in every lane. -/
+theorem sboxCircuit_lane (k : Nat) (hk : k < 64) (u0 u1 u2 u3 u4 u5 u6 u7 : UInt64) :
+    (sboxCircuit u0 u1 u2 u3 u4 u5 u6 u7).map (lane k) =
+      sboxCircuit (lane k u0) (lane k u1) (lane k u2) (lane k u3) (lane k u4) (lane k u5)
+        (lane k u6) (lane k u7) := by
+  simp only [sboxCircuit, Vector.map_mk, List.map_toArray, List.map_cons, List.map_nil, lane_xor,
+    lane_and, lane_not k hk]
+
+private theorem lane_bitTerm (b : UInt8) (j k m : Nat) (hj : j < 8) (hk : k < 64) (hm : m < 64) :
+    lane k (bitTerm b j m) = (decide (k = m) && bit b (7 - j)) := by
+  simp [lane, bitTerm, bit]
+  rw [Nat.mod_eq_of_lt hm, Nat.mod_eq_of_lt (by omega : 7 - j < 8),
+    Nat.mod_eq_of_lt (by omega : 7 - j < 64)]
+  by_cases h : k = m
+  · subst h; simp [hk]; omega
+  · simp [h]; omega
+
+private theorem lane_planeAux (s : Array UInt8) (j k : Nat) (hj : j < 8) (hk : k < 64) :
+    ∀ n, n ≤ 64 → lane k (planeAux s j n) = (decide (k < n) && bit s[k]! (7 - j))
+  | 0, _ => by simp [planeAux, lane]
+  | n + 1, hn => by
+    have ih := lane_planeAux s j k hj hk n (by omega)
+    simp only [planeAux]
+    rw [show lane k (planeAux s j n ||| bitTerm s[n]! j n) =
+        (lane k (planeAux s j n) || lane k (bitTerm s[n]! j n)) by simp [lane]]
+    rw [ih, lane_bitTerm _ _ _ _ hj hk (by omega)]
+    by_cases h : k = n
+    · subst h; simp
+    · have : (k < n + 1) = (k < n) := by apply propext; omega
+      simp [h, this]
+
+private theorem lane_extract (x : UInt64) (k : Nat) (hk : k < 64) :
+    ((x >>> k.toUInt64) &&& 1).toUInt8 = (lane k x).toUInt8 := by
+  apply UInt8.toNat_inj.mp
+  simp [lane, Nat.mod_eq_of_lt hk]
+  rcases Nat.mod_two_eq_zero_or_one (x.toNat >>> k) with h | h <;>
+    simp [BitVec.getLsbD, Nat.testBit, Nat.one_and_eq_mod_two, h] <;> rfl
+
+private theorem unpack_eq (o : Vector UInt64 8) (k : Nat) (hk : k < 64) :
+    unpack o k = ofBits (o.map (lane k)) := by
+  simp only [unpack, ofBits, lane_extract _ _ hk, Vector.getElem_map]
+  rfl
+
+private theorem sliced_getElem (s : Array UInt8) (hs : s.size ≤ 64) (k : Nat) (hk : k < s.size) :
+    (sliced s)[k]'(by simp [sliced, hk]) = sboxByte s[k] := by
+  simp only [sliced, Array.getElem_ofFn]
+  rw [unpack_eq _ _ (by omega), sboxCircuit_lane _ (by omega)]
+  have hp : ∀ j, j < 8 → lane k (planeAux s j s.size) = bit s[k] (7 - j) := fun j hj => by
+    rw [lane_planeAux s j k hj (by omega) s.size hs, decide_eq_true hk, Bool.true_and,
+      getElem!_pos s k hk]
+  simp only [hp 0 (by omega), hp 1 (by omega), hp 2 (by omega), hp 3 (by omega), hp 4 (by omega),
+    hp 5 (by omega), hp 6 (by omega), hp 7 (by omega)]
+  exact sboxBits_eq s[k]
+
+private theorem sbox_getElem (b : UInt8) : sbox[b.toNat]! = sboxByte b := by
+  simp [sbox, getElem!_pos, b.toNat_lt]
+
+theorem subBytes_eq_spec : subBytes = subBytesSpec := by
+  funext s
+  apply Array.ext
+  · simp [subBytes, subBytesSpec, sliced]; split <;> simp
+  · intro k h1 h2
+    have hk : k < s.size := by simpa [subBytesSpec] using h2
+    simp only [subBytesSpec, Array.getElem_map, sbox_getElem]
+    unfold subBytes
+    split
+    · next hs => exact sliced_getElem s hs k hk
+    · simp only [Array.getElem_map]
+      simp only [getElem!_pos (sliced #[s[k]]) 0 (by simp [sliced])]
+      exact sliced_getElem #[s[k]] (by simp) 0 (by simp)
+
+end
+
+theorem xtime_eq (x : UInt8) : xtime x = mul x 2 := by
+  have : ∀ i : Fin 256, xtime (UInt8.ofNat i) = mul (UInt8.ofNat i) 2 := by decide +kernel
+  simpa using this ⟨x.toNat, x.toNat_lt⟩
+
+theorem xtime_xor_eq (x : UInt8) : xtime x ^^^ x = mul x 3 := by
+  have : ∀ i : Fin 256, xtime (UInt8.ofNat i) ^^^ UInt8.ofNat i = mul (UInt8.ofNat i) 3 := by
+    decide +kernel
+  simpa using this ⟨x.toNat, x.toNat_lt⟩
+
+theorem mixColumns_eq_spec : mixColumns = mixColumnsSpec := by
+  funext s
+  apply Array.ext
+  · simp [mixColumns, mixColumnsSpec]
+  · intro i h1 h2
+    simp only [mixColumns, mixColumnsSpec, Array.getElem_ofFn, ← xtime_eq, ← xtime_xor_eq]
+    split <;> ac_rfl
+
+/-! ## Key schedule and cipher -/
+
 /-- The key schedule round constant `x^i` in `GF(2^8)`. -/
 private def rcon (i : Nat) : UInt8 := Id.run do
   let mut c : UInt8 := 1
@@ -52,55 +372,69 @@ private def rcon (i : Nat) : UInt8 := Id.run do
     c := mul c 2
   return c
 
-/-- The FIPS-197 §5.2 key schedule for an `nk`-word key: `4 * (nk + 7)` words, `nk + 7` round
-keys. -/
-private def expand (nk : Nat) (key : Array UInt8) : Array UInt8 := Id.run do
+/-- The FIPS-197 §5.2 key schedule for an `nk`-word key, `4 * (nk + 7)` words and `nk + 7` round
+keys, with `sub` as SubWord. -/
+private def expand (sub : Array UInt8 → Array UInt8) (nk : Nat) (key : Array UInt8) :
+    Array UInt8 := Id.run do
   let mut w := key
   for i in [nk:4 * (nk + 7)] do
     let mut t := #[w[4*i - 4]!, w[4*i - 3]!, w[4*i - 2]!, w[4*i - 1]!]
     if i % nk == 0 then
-      t := #[sbox[t[1]!.toNat]! ^^^ rcon (i / nk - 1), sbox[t[2]!.toNat]!,
-             sbox[t[3]!.toNat]!, sbox[t[0]!.toNat]!]
+      let u := sub #[t[1]!, t[2]!, t[3]!, t[0]!]
+      t := u.set! 0 (u[0]! ^^^ rcon (i / nk - 1))
     else if nk > 6 && i % nk == 4 then
-      t := t.map fun b => sbox[b.toNat]!
+      t := sub t
     for j in [0:4] do
       w := w.push (w[4*(i - nk) + j]! ^^^ t[j]!)
   return w
 
 /-- The AES-256 key schedule: sixty 4-byte words, fifteen round keys. -/
-def expandKey (key : Vector UInt8 32) : Array UInt8 := expand 8 key.toArray
+def expandKey (key : Vector UInt8 32) : Array UInt8 := expand subBytes 8 key.toArray
 
 /-- The AES-128 key schedule: forty-four 4-byte words, eleven round keys. -/
-def expandKey128 (key : Vector UInt8 16) : Array UInt8 := expand 4 key.toArray
+def expandKey128 (key : Vector UInt8 16) : Array UInt8 := expand subBytes 4 key.toArray
+
+def expandKeySpec (key : Vector UInt8 32) : Array UInt8 := expand subBytesSpec 8 key.toArray
 
-def subBytes (s : Array UInt8) : Array UInt8 := s.map fun b => sbox[b.toNat]!
+def expandKey128Spec (key : Vector UInt8 16) : Array UInt8 := expand subBytesSpec 4 key.toArray
+
+theorem expandKey_eq_spec : expandKey = expandKeySpec := by
+  funext key
+  simp only [expandKey, expandKeySpec, subBytes_eq_spec]
+
+theorem expandKey128_eq_spec : expandKey128 = expandKey128Spec := by
+  funext key
+  simp only [expandKey128, expandKey128Spec, subBytes_eq_spec]
 
 /-- Byte `i` of the state is row `i % 4`, column `i / 4`; row `r` rotates left by `r` columns. -/
 def shiftRows (s : Array UInt8) : Array UInt8 :=
   Array.ofFn fun i : Fin 16 => s[(i.val + 4 * (i.val % 4)) % 16]!
 
-/-- Each column multiplied by the fixed polynomial `{03}x³ + {01}x² + {01}x + {02}`. -/
-def mixColumns (s : Array UInt8) : Array UInt8 :=
-  Array.ofFn fun i : Fin 16 =>
-    let a := fun j => s[4 * (i.val / 4) + j]!
-    match i.val % 4 with
-    | 0 => mul (a 0) 2 ^^^ mul (a 1) 3 ^^^ a 2 ^^^ a 3
-    | 1 => a 0 ^^^ mul (a 1) 2 ^^^ mul (a 2) 3 ^^^ a 3
-    | 2 => a 0 ^^^ a 1 ^^^ mul (a 2) 2 ^^^ mul (a 3) 3
-    | _ => mul (a 0) 3 ^^^ a 1 ^^^ a 2 ^^^ mul (a 3) 2
-
 private def addRoundKey (s : Array UInt8) (rk : Array UInt8) (round : Nat) : Array UInt8 :=
   Array.ofFn fun i : Fin 16 => s[i.val]! ^^^ rk[16 * round + i.val]!
 
-/-- AES on one block, against an expanded key schedule; the round count follows from its length. -/
-def encryptBlock (rk : Array UInt8) (input : Vector UInt8 16) : Vector UInt8 16 := Id.run do
+/-- The FIPS-197 cipher on one block, against an expanded key schedule, with the given SubBytes
+and MixColumns; the round count follows from the schedule's length. -/
+private def cipher (sub mix : Array UInt8 → Array UInt8) (rk : Array UInt8)
+    (input : Vector UInt8 16) : Vector UInt8 16 := Id.run do
   let rounds := rk.size / 16 - 1
   let mut s := addRoundKey input.toArray rk 0
   for round in [1:rounds] do
-    s := addRoundKey (mixColumns (shiftRows (subBytes s))) rk round
-  s := addRoundKey (shiftRows (subBytes s)) rk rounds
+    s := addRoundKey (mix (shiftRows (sub s))) rk round
+  s := addRoundKey (shiftRows (sub s)) rk rounds
   return Vector.ofFn fun i : Fin 16 => s[i.val]!
 
+/-- AES on one block, against an expanded key schedule. -/
+def encryptBlock (rk : Array UInt8) (input : Vector UInt8 16) : Vector UInt8 16 :=
+  cipher subBytes mixColumns rk input
+
+def encryptBlockSpec (rk : Array UInt8) (input : Vector UInt8 16) : Vector UInt8 16 :=
+  cipher subBytesSpec mixColumnsSpec rk input
+
+theorem encryptBlock_eq_spec : encryptBlock = encryptBlockSpec := by
+  funext rk input
+  simp only [encryptBlock, encryptBlockSpec, subBytes_eq_spec, mixColumns_eq_spec]
+
 /-- Expand the key and encrypt one block. -/
 def encryptBlockWithKey (key : Vector UInt8 32) (input : Vector UInt8 16) : Vector UInt8 16 :=
   encryptBlock (expandKey key) input
diff --git a/Cryptlib/Primitives/Cipher/AESGCM.lean b/Cryptlib/Primitives/Cipher/AESGCM.lean
index 5623c0e5..63e3e2ac 100644
--- a/Cryptlib/Primitives/Cipher/AESGCM.lean
+++ b/Cryptlib/Primitives/Cipher/AESGCM.lean
@@ -7,6 +7,7 @@ import Cryptlib.Primitives.Cipher.AEAD
 import Cryptlib.Primitives.Cipher.AES
 import Cryptlib.Primitives.Cipher.GHash
 import Cryptlib.Util.Bytes
+import Cryptlib.Util.ConstantTime
 
 namespace Cryptlib.Primitives.Cipher.AESGCM
 
@@ -14,6 +15,7 @@ open Cryptlib.Primitives.Cipher.AEAD
 open Cryptlib.Primitives.Cipher.AES
 open Cryptlib.Primitives.Cipher.GHash (ghash)
 open Cryptlib.Util.Bytes
+open Cryptlib.Util.ConstantTime (ctEq ctEq_iff)
 
 /-! # AES-GCM (NIST SP 800-38D), 96-bit nonces and 128-bit tags
 
@@ -58,13 +60,13 @@ def encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) : ByteArray :=
   let ct := gctr key n pt
   ct ++ tagOf key n ad ct
 
-/-- Structural equality on the tag; a deployed implementation must compare in constant time. -/
+/-- The tag is compared with `ctEq`, which reads every byte before deciding. -/
 def decrypt (key : Key) (n : Nonce) (ad ct : ByteArray) : Option ByteArray :=
   if ct.size < 16 then none
   else
     let body := ct.extract 0 (ct.size - 16)
     let tag := ct.extract (ct.size - 16) ct.size
-    if (tagOf key n ad body).data = tag.data then some (gctr key n body) else none
+    if ctEq (tagOf key n ad body) tag then some (gctr key n body) else none
 
 @[simp] private theorem size_gctr (key : Key) (n : Nonce) (d : ByteArray) :
     (gctr key n d).size = d.size := by
@@ -92,7 +94,7 @@ private theorem size_encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) :
 private theorem decrypt_append (key : Key) (n : Nonce) (ad body tag : ByteArray)
     (h16 : tag.size = 16) :
     decrypt key n ad (body ++ tag) =
-      if (tagOf key n ad body).data = tag.data then some (gctr key n body) else none := by
+      if ctEq (tagOf key n ad body) tag then some (gctr key n body) else none := by
   have hs : (body ++ tag).size = body.size + 16 := by rw [ByteArray.size_append, h16]
   have hcut : (body ++ tag).size - 16 = body.size := by omega
   have hleft : (body ++ tag).extract 0 ((body ++ tag).size - 16) = body := by
@@ -105,7 +107,7 @@ private theorem decrypt_append (key : Key) (n : Nonce) (ad body tag : ByteArray)
 
 private theorem decrypt_encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) :
     decrypt key n ad (encrypt key n ad pt) = some pt := by
-  rw [encrypt, decrypt_append _ _ _ _ _ (size_tagOf _ _ _ _), if_pos rfl, gctr_gctr]
+  rw [encrypt, decrypt_append _ _ _ _ _ (size_tagOf _ _ _ _), if_pos ((ctEq_iff _ _).mpr rfl), gctr_gctr]
 
 theorem decrypt_sound (key : Key) (n : Nonce) (ad ct pt : ByteArray)
     (h : decrypt key n ad ct = some pt) : encrypt key n ad pt = ct := by
@@ -119,7 +121,7 @@ theorem decrypt_sound (key : Key) (n : Nonce) (ad ct pt : ByteArray)
     rw [← hsplit, decrypt_append _ _ _ _ _ h16] at h
     split at h
     · rename_i htag
-      rw [← Option.some.inj h, encrypt, gctr_gctr, ByteArray.ext htag]
+      rw [← Option.some.inj h, encrypt, gctr_gctr, (ctEq_iff _ _).mp htag]
       exact hsplit
     · exact absurd h (by simp)
 
diff --git a/Cryptlib/Primitives/Cipher/AESGCMSIV.lean b/Cryptlib/Primitives/Cipher/AESGCMSIV.lean
index c9cf37ea..b366c51f 100644
--- a/Cryptlib/Primitives/Cipher/AESGCMSIV.lean
+++ b/Cryptlib/Primitives/Cipher/AESGCMSIV.lean
@@ -7,6 +7,7 @@ import Cryptlib.Primitives.Cipher.AEAD
 import Cryptlib.Primitives.Cipher.AES
 import Cryptlib.Primitives.Cipher.Polyval
 import Cryptlib.Util.Bytes
+import Cryptlib.Util.ConstantTime
 
 namespace Cryptlib.Primitives.Cipher.AESGCMSIV
 
@@ -14,6 +15,7 @@ open Cryptlib.Primitives.Cipher.AEAD
 open Cryptlib.Primitives.Cipher.AES
 open Cryptlib.Primitives.Cipher.Polyval
 open Cryptlib.Util.Bytes
+open Cryptlib.Util.ConstantTime (ctEq ctEq_iff)
 
 /-! # AES-256-GCM-SIV
 
@@ -128,15 +130,15 @@ def encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) : ByteArray :=
   let tag := ofVector (tagOf key n ad pt)
   ctrXor (encKey key n) (counterBlock tag) pt ++ tag
 
-/-- Split off the tag, decrypt, recompute the tag and accept only on equality. The comparison is
-not constant time. -/
+/-- Split off the tag, decrypt, recompute the tag and accept only on equality, compared with
+`ctEq`, which reads every byte before deciding. -/
 def decrypt (key : Key) (n : Nonce) (ad ct : ByteArray) : Option ByteArray :=
   if ct.size < 16 then none
   else
     let tag := ct.extract (ct.size - 16) ct.size
     let body := ct.extract 0 (ct.size - 16)
     let pt := ctrXor (encKey key n) (counterBlock tag) body
-    if (ofVector (tagOf key n ad pt)).data = tag.data then some pt else none
+    if ctEq (ofVector (tagOf key n ad pt)) tag then some pt else none
 
 /-! ### The `AEAD` instance -/
 
@@ -148,8 +150,7 @@ private theorem size_encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) :
 private theorem decrypt_append (key : Key) (n : Nonce) (ad body tag : ByteArray)
     (h16 : tag.size = 16) :
     decrypt key n ad (body ++ tag) =
-      (if (ofVector (tagOf key n ad (ctrXor (encKey key n) (counterBlock tag) body))).data
-            = tag.data
+      (if ctEq (ofVector (tagOf key n ad (ctrXor (encKey key n) (counterBlock tag) body))) tag
        then some (ctrXor (encKey key n) (counterBlock tag) body)
        else none) := by
   have hs : (body ++ tag).size = body.size + 16 := by rw [ByteArray.size_append, h16]
@@ -164,7 +165,7 @@ private theorem decrypt_append (key : Key) (n : Nonce) (ad body tag : ByteArray)
 
 private theorem decrypt_encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) :
     decrypt key n ad (encrypt key n ad pt) = some pt := by
-  rw [encrypt, decrypt_append _ _ _ _ _ (size_ofVector _), ctrXor_ctrXor, if_pos rfl]
+  rw [encrypt, decrypt_append _ _ _ _ _ (size_ofVector _), ctrXor_ctrXor, if_pos ((ctEq_iff _ _).mpr rfl)]
 
 theorem decrypt_sound (key : Key) (n : Nonce) (ad ct pt : ByteArray)
     (h : decrypt key n ad ct = some pt) : encrypt key n ad pt = ct := by
@@ -178,7 +179,7 @@ theorem decrypt_sound (key : Key) (n : Nonce) (ad ct pt : ByteArray)
     rw [← hsplit, decrypt_append _ _ _ _ _ h16] at h
     split at h
     · rename_i htag
-      rw [← Option.some.inj h, encrypt, ByteArray.ext htag, ctrXor_ctrXor]
+      rw [← Option.some.inj h, encrypt, (ctEq_iff _ _).mp htag, ctrXor_ctrXor]
       exact hsplit
     · exact absurd h (by simp)
 
diff --git a/Cryptlib/Primitives/Cipher/ChaChaPoly.lean b/Cryptlib/Primitives/Cipher/ChaChaPoly.lean
index e6ad64d8..0c24f648 100644
--- a/Cryptlib/Primitives/Cipher/ChaChaPoly.lean
+++ b/Cryptlib/Primitives/Cipher/ChaChaPoly.lean
@@ -6,11 +6,13 @@ SPDX-License-Identifier: AGPL-3.0-only
 import Cryptlib.Primitives.Cipher.AEAD
 import Cryptlib.Primitives.Cipher.ChaCha20
 import Cryptlib.Util.Bytes
+import Cryptlib.Util.ConstantTime
 
 namespace Cryptlib.Primitives.Cipher.ChaChaPoly
 
 open Cryptlib.Primitives.Cipher.AEAD
 open Cryptlib.Util.Bytes
+open Cryptlib.Util.ConstantTime (ctEq ctEq_iff)
 
 /-! # ChaCha20-Poly1305 (RFC 8439)
 
@@ -69,13 +71,13 @@ def encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) : ByteArray :=
   let ct := chacha20 key n pt
   ct ++ tagOf key n ad ct
 
-/-- Structural equality on the tag; a deployed implementation must compare in constant time. -/
+/-- The tag is compared with `ctEq`, which reads every byte before deciding. -/
 def decrypt (key : Key) (n : Nonce) (ad ct : ByteArray) : Option ByteArray :=
   if ct.size < 16 then none
   else
     let body := ct.extract 0 (ct.size - 16)
     let tag := ct.extract (ct.size - 16) ct.size
-    if (tagOf key n ad body).data = tag.data then some (chacha20 key n body) else none
+    if ctEq (tagOf key n ad body) tag then some (chacha20 key n body) else none
 
 @[simp] private theorem size_chacha20 (key : Key) (n : Nonce) (d : ByteArray) :
     (chacha20 key n d).size = d.size := by
@@ -103,7 +105,7 @@ private theorem size_encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) :
 private theorem decrypt_append (key : Key) (n : Nonce) (ad body tag : ByteArray)
     (h16 : tag.size = 16) :
     decrypt key n ad (body ++ tag) =
-      if (tagOf key n ad body).data = tag.data then some (chacha20 key n body) else none := by
+      if ctEq (tagOf key n ad body) tag then some (chacha20 key n body) else none := by
   have hs : (body ++ tag).size = body.size + 16 := by rw [ByteArray.size_append, h16]
   have hcut : (body ++ tag).size - 16 = body.size := by omega
   have hleft : (body ++ tag).extract 0 ((body ++ tag).size - 16) = body := by
@@ -116,7 +118,7 @@ private theorem decrypt_append (key : Key) (n : Nonce) (ad body tag : ByteArray)
 
 private theorem decrypt_encrypt (key : Key) (n : Nonce) (ad pt : ByteArray) :
     decrypt key n ad (encrypt key n ad pt) = some pt := by
-  rw [encrypt, decrypt_append _ _ _ _ _ (size_tagOf _ _ _ _), if_pos rfl, chacha20_chacha20]
+  rw [encrypt, decrypt_append _ _ _ _ _ (size_tagOf _ _ _ _), if_pos ((ctEq_iff _ _).mpr rfl), chacha20_chacha20]
 
 theorem decrypt_sound (key : Key) (n : Nonce) (ad ct pt : ByteArray)
     (h : decrypt key n ad ct = some pt) : encrypt key n ad pt = ct := by
@@ -130,7 +132,7 @@ theorem decrypt_sound (key : Key) (n : Nonce) (ad ct pt : ByteArray)
     rw [← hsplit, decrypt_append _ _ _ _ _ h16] at h
     split at h
     · rename_i htag
-      rw [← Option.some.inj h, encrypt, chacha20_chacha20, ByteArray.ext htag]
+      rw [← Option.some.inj h, encrypt, chacha20_chacha20, (ctEq_iff _ _).mp htag]
       exact hsplit
     · exact absurd h (by simp)
 
diff --git a/Cryptlib/Primitives/Cipher/GHash.lean b/Cryptlib/Primitives/Cipher/GHash.lean
index 7fa81785..9b17affe 100644
--- a/Cryptlib/Primitives/Cipher/GHash.lean
+++ b/Cryptlib/Primitives/Cipher/GHash.lean
@@ -3,13 +3,23 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
+import Cryptlib.Util.ConstantTime
+
 namespace Cryptlib.Primitives.Cipher.GHash
 
+open Cryptlib.Util.ConstantTime (mask and_mask)
+
 /-! # GHASH, the GCM authenticator (NIST SP 800-38D §6.4)
 
 Blocks are read as big-endian 128-bit integers. GCM numbers bits from the most significant end,
 so the coefficient of `x⁰` is the integer's top bit and multiplying by `x` is a right shift,
-reduced by `R = 0xE1 ‖ 0¹²⁰`. -/
+reduced by `R = 0xE1 ‖ 0¹²⁰`.
+
+`mul` and `ghashSpec` over `Nat` are the specification. `ghash` keeps the hash state and key in a
+pair of `UInt64` words and runs the same bit-serial multiplication with masks in place of its
+branches; `ghash_eq_spec` proves the two equal. It is written without secret-dependent branches
+or memory indexing, but Lean compiles through C and neither compiler is proven to preserve that,
+so the machine code is not verified to be constant time. -/
 
 def R : Nat := 0xE1 <<< 120
 
@@ -18,15 +28,18 @@ def ofBytes (b : Array UInt8) : Nat := b.foldl (fun acc x => (acc <<< 8) ||| x.t
 def toBytes (n : Nat) : Vector UInt8 16 :=
   Vector.ofFn fun i : Fin 16 => UInt8.ofNat (n >>> (8 * (15 - i.val)))
 
+/-- Step `i` of SP 800-38D Algorithm 1 on `(Z, V)`. -/
+def mulStep (x : Nat) (zv : Nat × Nat) (i : Nat) : Nat × Nat :=
+  let (z, v) := zv
+  let z := if x.testBit (127 - i) then z ^^^ v else z
+  let v := if v.testBit 0 then (v >>> 1) ^^^ R else v >>> 1
+  (z, v)
+
 /-- SP 800-38D Algorithm 1, `X • Y` in `GF(2¹²⁸)`. -/
-def mul (x y : Nat) : Nat :=
-  ((List.range 128).foldl (fun (z, v) i =>
-    let z := if x.testBit (127 - i) then z ^^^ v else z
-    let v := if v.testBit 0 then (v >>> 1) ^^^ R else v >>> 1
-    (z, v)) (0, y)).1
+def mul (x y : Nat) : Nat := ((List.range 128).foldl (mulStep x) (0, y)).1
 
 /-- `GHASH_H` over a byte string, a short final block read as zero-padded. -/
-def ghash (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16 :=
+def ghashSpec (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16 :=
   let hf := ofBytes h.toArray
   -- `ByteArray.data` copies, so convert once rather than per block
   let b := blocks.data
@@ -34,4 +47,258 @@ def ghash (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16 :=
     let chunk := b.extract (16 * i) (16 * i + 16)
     mul (y ^^^ (ofBytes chunk <<< (8 * (16 - chunk.size)))) hf) 0
 
+/-! ## Two-word field elements -/
+
+/-- A field element as its high and low 64 bits. -/
+structure Elem where
+  hi : UInt64
+  lo : UInt64
+
+/-- The element as a 128-bit integer, `hi` on top. -/
+def Elem.toNat (a : Elem) : Nat := a.hi.toNat <<< 64 ||| a.lo.toNat
+
+private theorem testBit_toNat (a : Elem) (i : Nat) :
+    a.toNat.testBit i = if i < 64 then a.lo.toNat.testBit i else a.hi.toNat.testBit (i - 64) := by
+  simp only [Elem.toNat, Nat.testBit_or, Nat.testBit_shiftLeft]
+  split
+  · have : ¬ (i ≥ 64) := by omega
+    simp [this]
+  · have : a.lo.toNat.testBit i = false :=
+      Nat.testBit_lt_two_pow
+        (Nat.lt_of_lt_of_le a.lo.toNat_lt (Nat.pow_le_pow_right (by omega) (by omega)))
+    simp [this]; omega
+
+private theorem toNat_xor (a b : Elem) :
+    (Elem.mk (a.hi ^^^ b.hi) (a.lo ^^^ b.lo)).toNat = a.toNat ^^^ b.toNat := by
+  apply Nat.eq_of_testBit_eq; intro i
+  simp only [testBit_toNat, Nat.testBit_xor, UInt64.toNat_xor]
+  split <;> rfl
+
+def Elem.xor (a b : Elem) : Elem := ⟨a.hi ^^^ b.hi, a.lo ^^^ b.lo⟩
+
+private def shr1 (v : Elem) : Elem := ⟨v.hi >>> 1, (v.lo >>> 1) ||| (v.hi <<< 63)⟩
+
+private theorem toNat_shr1 (v : Elem) : (shr1 v).toNat = v.toNat >>> 1 := by
+  apply Nat.eq_of_testBit_eq; intro i
+  simp only [testBit_toNat, shr1, Nat.testBit_shiftRight, UInt64.toNat_shiftRight, UInt64.toNat_or,
+    UInt64.toNat_shiftLeft, Nat.testBit_or, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft]
+  rw [show UInt64.toNat 1 % 64 = 1 from rfl, show UInt64.toNat 63 % 64 = 63 from rfl]
+  rcases Nat.lt_or_ge i 63 with h | h
+  · have : ¬ i ≥ 63 := by omega
+    simp [this, show i < 64 by omega, Nat.add_comm]
+  · rcases Nat.lt_or_ge i 64 with h' | h'
+    · have hi : i = 63 := by omega
+      subst hi; simp [Nat.testBit_lt_two_pow v.lo.toNat_lt]
+    · simp [show ¬ i < 64 by omega, show ¬ 1 + i < 64 by omega]; congr 1; omega
+
+/-- All ones if bit `127 - i` of `xh ‖ xl` is set, else zero. -/
+private def bitMask (xh xl : UInt64) (i : Nat) : UInt64 :=
+  if i < 64 then mask (xh >>> (63 - i).toUInt64) else mask (xl >>> (127 - i).toUInt64)
+
+/-- Algorithm 1 from step `i`, for `n` more steps, with `Z` and `V` unpacked. -/
+private def mulLoop (xh xl : UInt64) : Nat → Nat → UInt64 → UInt64 → UInt64 → UInt64 → Elem
+  | 0, _, zh, zl, _, _ => ⟨zh, zl⟩
+  | n + 1, i, zh, zl, vh, vl =>
+    let m := bitMask xh xl i
+    let r := mask vl
+    mulLoop xh xl n (i + 1) (zh ^^^ (vh &&& m)) (zl ^^^ (vl &&& m))
+      ((vh >>> 1) ^^^ (0xE100000000000000 &&& r)) ((vl >>> 1) ||| (vh <<< 63))
+
+/-- `mul` on two-word elements. -/
+def mulCT (x y : Elem) : Elem := mulLoop x.hi x.lo 128 0 0 0 y.hi y.lo
+
+private theorem testBit_shr (w : UInt64) (s : Nat) (hs : s < 64) :
+    (w >>> s.toUInt64).toNat.testBit 0 = w.toNat.testBit s := by
+  simp [Nat.mod_eq_of_lt hs]
+
+private theorem bitMask_eq (xh xl : UInt64) (i : Nat) (x : UInt64) :
+    x &&& bitMask xh xl i = if (Elem.mk xh xl).toNat.testBit (127 - i) then x else 0 := by
+  rw [testBit_toNat, bitMask]
+  split
+  · rw [and_mask, testBit_shr _ _ (by omega)]
+    simp only [show ¬ (127 - i < 64) by omega, if_false]
+    rw [show 127 - i - 64 = 63 - i by omega]
+  · rw [and_mask, testBit_shr _ _ (by omega)]
+    simp only [show 127 - i < 64 by omega, if_true]
+
+private theorem toNat_R : (Elem.mk 0xE100000000000000 0).toNat = R := by decide
+
+private theorem mulLoop_spec (xh xl : UInt64) : ∀ n i zh zl vh vl,
+    (mulLoop xh xl n i zh zl vh vl).toNat =
+      ((List.range' i n).foldl (mulStep (Elem.mk xh xl).toNat)
+        ((Elem.mk zh zl).toNat, (Elem.mk vh vl).toNat)).1
+  | 0, _, _, _, _, _ => rfl
+  | n + 1, i, zh, zl, vh, vl => by
+    rw [mulLoop, mulLoop_spec xh xl n, List.range'_succ, List.foldl_cons]
+    congr 2
+    simp only [mulStep]
+    rw [bitMask_eq, bitMask_eq, and_mask]
+    have hb : (Elem.mk vh vl).toNat.testBit 0 = vl.toNat.testBit 0 := by
+      rw [testBit_toNat, if_pos (by omega)]
+    have hz := toNat_xor ⟨zh, zl⟩ ⟨vh, vl⟩
+    have hs := toNat_shr1 ⟨vh, vl⟩
+    have hR := toNat_xor (shr1 ⟨vh, vl⟩) ⟨0xE100000000000000, 0⟩
+    simp only [shr1, toNat_R, UInt64.xor_zero] at hz hs hR
+    rw [hb]
+    split <;> split <;> simp_all
+
+theorem mulCT_spec (x y : Elem) : (mulCT x y).toNat = mul x.toNat y.toNat := by
+  rw [mulCT, mulLoop_spec, mul, List.range_eq_range']
+  rfl
+
+/-! ## Loading and storing blocks -/
+
+/-- The big-endian value of `f 0, …, f (n - 1)`. -/
+private def bytesNat (f : Nat → UInt8) : Nat → Nat
+  | 0 => 0
+  | n + 1 => bytesNat f n <<< 8 ||| (f n).toNat
+
+private theorem shl8_or (x : Nat) (b : UInt8) : x <<< 8 ||| b.toNat = x * 256 + b.toNat := by
+  rw [← Nat.shiftLeft_add_eq_or_of_lt b.toNat_lt, Nat.shiftLeft_eq]
+
+private theorem bytesNat_lt (f : Nat → UInt8) : ∀ n, bytesNat f n < 2 ^ (8 * n)
+  | 0 => by simp [bytesNat]
+  | n + 1 => by
+    have ih := bytesNat_lt f n
+    have hb := (f n).toNat_lt
+    rw [bytesNat, shl8_or, show 8 * (n + 1) = 8 * n + 8 by omega, Nat.pow_add]
+    have : (2:Nat) ^ 8 = 256 := rfl
+    rw [this] at hb ⊢
+    omega
+
+private theorem bytesNat_congr (f g : Nat → UInt8) :
+    ∀ n, (∀ j, j < n → f j = g j) → bytesNat f n = bytesNat g n
+  | 0, _ => rfl
+  | n + 1, h => by
+    rw [bytesNat, bytesNat, bytesNat_congr f g n (fun j hj => h j (by omega)), h n (by omega)]
+
+private theorem ofBytes_eq (a : Array UInt8) : ofBytes a = bytesNat (a.getD · 0) a.size := by
+  rcases a with ⟨l⟩
+  simp only [ofBytes, List.foldl_toArray', List.size_toArray]
+  suffices h : ∀ r : List UInt8, r.reverse.foldl (fun acc x => (acc <<< 8) ||| x.toNat) 0 =
+      bytesNat (fun j => r.reverse.toArray.getD j 0) r.reverse.length by
+    simpa using h l.reverse
+  intro r
+  induction r with
+  | nil => rfl
+  | cons x r ih =>
+    rw [List.reverse_cons, List.foldl_append, ih, List.length_append, List.length_singleton,
+      bytesNat]
+    simp only [List.foldl_cons, List.foldl_nil]
+    congr 1
+    · congr 1
+      apply bytesNat_congr
+      intro j hj
+      have hj' : j < r.reverse.length + 1 := by omega
+      simp only [Array.getD, List.size_toArray, List.length_append, List.length_singleton, hj, hj',
+        dite_true, Array.getInternal_eq_getElem, List.getElem_toArray, List.getElem_append_left hj]
+    · simp [Array.getD]
+
+private theorem bytesNat_append_zero (f : Nat → UInt8) (n : Nat) (hf : ∀ j, n ≤ j → f j = 0) :
+    ∀ k, bytesNat f (n + k) = bytesNat f n <<< (8 * k)
+  | 0 => by simp
+  | k + 1 => by
+    rw [← Nat.add_assoc, bytesNat, bytesNat_append_zero f n hf k, hf _ (by omega)]
+    simp [Nat.shiftLeft_add, Nat.mul_add]
+
+private theorem bytesNat_split (f : Nat → UInt8) (m : Nat) :
+    ∀ n, bytesNat f (m + n) = bytesNat f m <<< (8 * n) ||| bytesNat (fun j => f (m + j)) n
+  | 0 => by simp [bytesNat]
+  | n + 1 => by
+    rw [← Nat.add_assoc, bytesNat, bytesNat_split f m n, bytesNat, Nat.shiftLeft_or_distrib,
+      ← Nat.shiftLeft_add, Nat.or_assoc]
+    rfl
+
+/-- `bytesNat` in a `UInt64`, for `n ≤ 8`. -/
+private def wordAux (f : Nat → UInt8) : Nat → UInt64
+  | 0 => 0
+  | n + 1 => wordAux f n <<< 8 ||| (f n).toUInt64
+
+private theorem wordAux_toNat (f : Nat → UInt8) : ∀ n, n ≤ 8 → (wordAux f n).toNat = bytesNat f n
+  | 0, _ => rfl
+  | n + 1, hn => by
+    have ih := wordAux_toNat f n (by omega)
+    have hl := bytesNat_lt f n
+    simp only [wordAux, bytesNat, UInt64.toNat_or, UInt64.toNat_shiftLeft, ih, UInt8.toNat_toUInt64]
+    rw [show UInt64.toNat 8 % 64 = 8 from rfl, Nat.mod_eq_of_lt]
+    rw [Nat.shiftLeft_eq]
+    have : 2 ^ (8 * n) * 2 ^ 8 ≤ 2 ^ 64 := by
+      rw [← Nat.pow_add]; exact Nat.pow_le_pow_right (by omega) (by omega)
+    have : (2:Nat) ^ 8 = 256 := rfl
+    have := Nat.mul_lt_mul_of_pos_right hl (show 0 < 2 ^ 8 by omega)
+    omega
+
+/-- The 16 bytes at `off`, zero-padded past the end. -/
+def load (a : Array UInt8) (off : Nat) : Elem :=
+  ⟨wordAux (fun j => a.getD (off + j) 0) 8, wordAux (fun j => a.getD (off + 8 + j) 0) 8⟩
+
+private theorem getD_extract (a : Array UInt8) (off j : Nat) (hj : j < 16) :
+    (a.extract off (off + 16)).getD j 0 = a.getD (off + j) 0 := by
+  simp only [Array.getD, Array.size_extract]
+  by_cases h : off + j < a.size
+  · rw [dif_pos (by omega), dif_pos h]; simp
+  · rw [dif_neg (by omega), dif_neg h]
+
+theorem load_toNat (a : Array UInt8) (off : Nat) :
+    (load a off).toNat =
+      ofBytes (a.extract off (off + 16)) <<< (8 * (16 - (a.extract off (off + 16)).size)) := by
+  have hs : (a.extract off (off + 16)).size ≤ 16 := by simp; omega
+  rw [ofBytes_eq, ← bytesNat_append_zero _ _
+      (fun j hj => by simp only [Array.getD, dif_neg (Nat.not_lt.mpr hj)]),
+    Nat.add_sub_cancel' hs,
+    bytesNat_congr _ (fun j => a.getD (off + j) 0) 16 (fun j hj => getD_extract a off j hj),
+    show 16 = 8 + 8 from rfl, bytesNat_split, Elem.toNat, load, wordAux_toNat _ _ (by omega),
+    wordAux_toNat _ _ (by omega)]
+  congr 2
+  funext j
+  rw [Nat.add_assoc]
+
+/-- An element as 16 big-endian bytes. -/
+def store (e : Elem) : Vector UInt8 16 :=
+  Vector.ofFn fun i : Fin 16 =>
+    if i.val < 8 then (e.hi >>> (8 * (7 - i.val)).toUInt64).toUInt8
+    else (e.lo >>> (8 * (15 - i.val)).toUInt64).toUInt8
+
+theorem store_eq (e : Elem) : store e = toBytes e.toNat := by
+  ext i hi
+  simp only [store, toBytes, Vector.getElem_ofFn]
+  apply UInt8.toNat_inj.mp
+  apply Nat.eq_of_testBit_eq
+  intro j
+  split
+  · simp only [UInt64.toNat_toUInt8, UInt64.toNat_shiftRight, UInt8.toNat_ofNat',
+      UInt64.toNat_ofNat']
+    simp only [Nat.testBit_mod_two_pow, Nat.testBit_shiftRight, testBit_toNat]
+    rw [Nat.mod_eq_of_lt (by omega : 8 * (7 - i) % 2 ^ 64 < 64),
+      Nat.mod_eq_of_lt (by omega : 8 * (7 - i) < 2 ^ 64)]
+    by_cases hj : j < 8
+    · rw [if_neg (by omega)]; simp only [hj, decide_true, Bool.true_and]; congr 1; omega
+    · simp [hj]
+  · simp only [UInt64.toNat_toUInt8, UInt64.toNat_shiftRight, UInt8.toNat_ofNat',
+      UInt64.toNat_ofNat']
+    simp only [Nat.testBit_mod_two_pow, Nat.testBit_shiftRight, testBit_toNat]
+    rw [Nat.mod_eq_of_lt (by omega : 8 * (15 - i) % 2 ^ 64 < 64),
+      Nat.mod_eq_of_lt (by omega : 8 * (15 - i) < 2 ^ 64)]
+    by_cases hj : j < 8
+    · rw [if_pos (by omega)]
+    · simp [hj]
+
+/-- `GHASH_H` over a byte string, a short final block read as zero-padded. -/
+def ghash (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16 :=
+  let hf := load h.toArray 0
+  -- `ByteArray.data` copies, so convert once rather than per block
+  let b := blocks.data
+  store <| (List.range ((blocks.size + 15) / 16)).foldl
+    (fun y i => mulCT (y.xor (load b (16 * i))) hf) ⟨0, 0⟩
+
+theorem ghash_eq_spec (h : Vector UInt8 16) (blocks : ByteArray) :
+    ghash h blocks = ghashSpec h blocks := by
+  simp only [ghash, ghashSpec, store_eq]
+  congr 1
+  refine (List.foldl_hom Elem.toNat (fun y i => ?_)).symm
+  rw [mulCT_spec, Elem.xor, toNat_xor, load_toNat, load_toNat]
+  have : h.toArray.extract 0 16 = h.toArray := by
+    apply Array.ext <;> simp
+  simp [this]
+
 end Cryptlib.Primitives.Cipher.GHash
diff --git a/Cryptlib/Primitives/Cipher/Polyval.lean b/Cryptlib/Primitives/Cipher/Polyval.lean
index 6dee9d04..a312e1a7 100644
--- a/Cryptlib/Primitives/Cipher/Polyval.lean
+++ b/Cryptlib/Primitives/Cipher/Polyval.lean
@@ -3,13 +3,24 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
+import Cryptlib.Util.ConstantTime
+
 namespace Cryptlib.Primitives.Cipher.Polyval
 
+open Cryptlib.Util.ConstantTime (mask and_mask)
+
 /-! # POLYVAL, the GCM-SIV authenticator
 
 RFC 8452 §3: `POLYVAL(H, X₁, …, Xₛ) = Σᵢ Xᵢ • H^(s-i+1)` where `a • b = a·b·x⁻¹²⁸`, over
 `GF(2)[x] / (x¹²⁸ + x¹²⁷ + x¹²⁶ + x¹²¹ + 1)`. Field elements are little-endian `Nat`s: byte `j`,
 bit `i` is the coefficient of `x^(8j+i)`.
+
+The `Nat` functions and `polyvalSpec` are the specification. `polyval` keeps the hash state and
+key in two `UInt64` words and the double-width product in four, runs the same bit-serial
+multiplication and reduction with masks in place of branches, and is proved equal to
+`polyvalSpec` by `polyval_eq_spec`. It is written without secret-dependent branches or memory
+indexing, but Lean compiles through C and neither compiler is proven to preserve that, so the
+machine code is not verified to be constant time.
 -/
 
 /-- `x¹²⁸ + x¹²⁷ + x¹²⁶ + x¹²¹ + 1`, as bits of a `Nat`. -/
@@ -41,9 +52,425 @@ private def blockAt (b : ByteArray) (i : Nat) : Nat :=
   (b.extract (16 * i) (16 * i + 16)).data.foldr (fun x acc => (acc <<< 8) ||| x.toNat) 0
 
 /-- `POLYVAL(H, X₁ ‖ … ‖ Xₛ)`, in Horner form: `Sⱼ = (Sⱼ₋₁ + Xⱼ) • H`. -/
-def polyval (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16 :=
+def polyvalSpec (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16 :=
   let hf := ofBytes h
   toBytes <| (List.range ((blocks.size + 15) / 16)).foldl
     (fun s i => dot (s ^^^ blockAt blocks i) hf) 0
 
+/-! ## Two- and four-word arithmetic -/
+
+/-- Four words as a 256-bit integer, `w3` on top. -/
+private def val4 (w3 w2 w1 w0 : UInt64) : Nat :=
+  w3.toNat <<< 192 ||| w2.toNat <<< 128 ||| w1.toNat <<< 64 ||| w0.toNat
+
+private theorem testBit_word (w : UInt64) (i : Nat) (h : 64 ≤ i) : w.toNat.testBit i = false :=
+  Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le w.toNat_lt (Nat.pow_le_pow_right (by omega) h))
+
+private theorem testBit_val4 (w3 w2 w1 w0 : UInt64) (i : Nat) :
+    (val4 w3 w2 w1 w0).testBit i =
+      if i < 64 then w0.toNat.testBit i
+      else if i < 128 then w1.toNat.testBit (i - 64)
+      else if i < 192 then w2.toNat.testBit (i - 128)
+      else w3.toNat.testBit (i - 192) := by
+  simp only [val4, Nat.testBit_or, Nat.testBit_shiftLeft]
+  by_cases h0 : i < 64
+  · simp [h0, show ¬ i ≥ 64 by omega, show ¬ i ≥ 128 by omega, show ¬ i ≥ 192 by omega]
+  by_cases h1 : i < 128
+  · simp [h0, h1, show i ≥ 64 by omega, show ¬ i ≥ 128 by omega, show ¬ i ≥ 192 by omega,
+      testBit_word w0 i (by omega)]
+  by_cases h2 : i < 192
+  · simp [h0, h1, h2, show i ≥ 64 by omega, show i ≥ 128 by omega, show ¬ i ≥ 192 by omega,
+      testBit_word w0 i (by omega), testBit_word w1 (i - 64) (by omega)]
+  · simp [h0, h1, h2, show i ≥ 64 by omega, show i ≥ 128 by omega, show i ≥ 192 by omega,
+      testBit_word w0 i (by omega), testBit_word w1 (i - 64) (by omega),
+      testBit_word w2 (i - 128) (by omega)]
+
+private theorem val4_xor (a3 a2 a1 a0 b3 b2 b1 b0 : UInt64) :
+    val4 (a3 ^^^ b3) (a2 ^^^ b2) (a1 ^^^ b1) (a0 ^^^ b0) =
+      val4 a3 a2 a1 a0 ^^^ val4 b3 b2 b1 b0 := by
+  apply Nat.eq_of_testBit_eq; intro i
+  simp only [testBit_val4, Nat.testBit_xor, UInt64.toNat_xor]
+  split <;> (try split) <;> (try split) <;> rfl
+
+private theorem val4_and_mask (a3 a2 a1 a0 m : UInt64) :
+    val4 (a3 &&& mask m) (a2 &&& mask m) (a1 &&& mask m) (a0 &&& mask m) =
+      if m.toNat.testBit 0 then val4 a3 a2 a1 a0 else 0 := by
+  simp only [and_mask]; split <;> rfl
+
+private theorem tb_congr (x : Nat) {a b : Nat} (h : a = b) : x.testBit a = x.testBit b := h ▸ rfl
+
+private theorem dand (p : Prop) [Decidable p] (b : Bool) :
+    (decide p && b) = if p then b else false := by
+  by_cases h : p <;> simp [h]
+
+private theorem val4_shr1 (w3 w2 w1 w0 : UInt64) :
+    val4 (w3 >>> 1) ((w2 >>> 1) ||| (w3 <<< 63)) ((w1 >>> 1) ||| (w2 <<< 63))
+      ((w0 >>> 1) ||| (w1 <<< 63)) = val4 w3 w2 w1 w0 >>> 1 := by
+  apply Nat.eq_of_testBit_eq; intro i
+  simp only [testBit_val4, Nat.testBit_shiftRight, UInt64.toNat_shiftRight, UInt64.toNat_or,
+    UInt64.toNat_shiftLeft, Nat.testBit_or, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft]
+  rw [show UInt64.toNat 1 % 64 = 1 from rfl, show UInt64.toNat 63 % 64 = 63 from rfl]
+  simp only [dand]
+  repeat' split
+  all_goals first
+    | omega
+    | (simp (disch := omega) only [testBit_word, Bool.or_false, Bool.false_or]
+       first | done | exact tb_congr _ (by omega))
+    | exact tb_congr _ (by omega)
+
+private theorem val4_shl1 (w3 w2 w1 w0 : UInt64) :
+    val4 ((w3 <<< 1) ||| (w2 >>> 63)) ((w2 <<< 1) ||| (w1 >>> 63)) ((w1 <<< 1) ||| (w0 >>> 63))
+      (w0 <<< 1) = (val4 w3 w2 w1 w0 <<< 1) % 2 ^ 256 := by
+  apply Nat.eq_of_testBit_eq; intro i
+  simp only [testBit_val4, Nat.testBit_shiftRight, UInt64.toNat_shiftRight, UInt64.toNat_or,
+    UInt64.toNat_shiftLeft, Nat.testBit_or, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft]
+  rw [show UInt64.toNat 1 % 64 = 1 from rfl, show UInt64.toNat 63 % 64 = 63 from rfl]
+  simp only [dand]
+  repeat' split
+  all_goals first
+    | omega
+    | (simp (disch := omega) only [testBit_word, Bool.or_false, Bool.false_or]
+       first | done | exact tb_congr _ (by omega))
+    | exact tb_congr _ (by omega)
+
+private theorem val4_lt (w3 w2 w1 w0 : UInt64) : val4 w3 w2 w1 w0 < 2 ^ 256 := by
+  apply Nat.lt_pow_two_of_testBit
+  intro i hi
+  rw [testBit_val4]
+  repeat' split
+  all_goals first | omega | exact testBit_word _ _ (by omega)
+
+private theorem val4_low (w3 w2 w1 w0 : UInt64) (h : val4 w3 w2 w1 w0 < 2 ^ 128) :
+    val4 w3 w2 w1 w0 = val4 0 0 w1 w0 := by
+  apply Nat.eq_of_testBit_eq; intro i
+  by_cases hi : i < 128
+  · simp only [testBit_val4]
+    repeat' split
+    all_goals first | omega | rfl
+  · rw [Nat.testBit_lt_two_pow (Nat.lt_of_lt_of_le h (Nat.pow_le_pow_right (by omega) (by omega)))]
+    simp only [testBit_val4]
+    repeat' split
+    all_goals first | omega | simp
+
+private def divStep (c : Nat) : Nat := if c.testBit 0 then (c ^^^ modulus) >>> 1 else c >>> 1
+
+private theorem divX128_eq (c : Nat) :
+    divX128 c = (List.range 128).foldl (fun c _ => divStep c) c := rfl
+
+private theorem modulus_lt : modulus < 2 ^ 129 := by decide
+
+private theorem divStep_lt (c n : Nat) (h : c < 2 ^ (n + 1)) (hn : 129 ≤ n + 1) :
+    divStep c < 2 ^ n := by
+  have hm : modulus < 2 ^ (n + 1) :=
+    Nat.lt_of_lt_of_le modulus_lt (Nat.pow_le_pow_right (by omega) hn)
+  unfold divStep
+  split
+  · rw [Nat.shiftRight_eq_div_pow, Nat.pow_one]
+    have := Nat.xor_lt_two_pow h hm
+    rw [Nat.pow_succ] at this; omega
+  · rw [Nat.shiftRight_eq_div_pow, Nat.pow_one]
+    rw [Nat.pow_succ] at h; omega
+
+private theorem foldl_divStep_lt :
+    ∀ (n : Nat) (l : List Nat) (c : Nat), l.length = n → c < 2 ^ (128 + n) →
+    l.foldl (fun c _ => divStep c) c < 2 ^ 128
+  | 0, [], c, _, h => by simpa using h
+  | n + 1, _ :: l, c, hl, h => by
+    rw [List.foldl_cons]
+    exact foldl_divStep_lt n l _ (by simpa using hl)
+      (divStep_lt c _ (by rw [show 128 + n + 1 = 128 + (n + 1) by omega]; exact h) (by omega))
+
+private theorem divX128_lt (c : Nat) (h : c < 2 ^ 256) : divX128 c < 2 ^ 128 :=
+  foldl_divStep_lt 128 _ c (by simp) h
+
+/-- Four words, for the double-width product. -/
+private structure W4 where
+  w3 : UInt64
+  w2 : UInt64
+  w1 : UInt64
+  w0 : UInt64
+
+private def W4.toNat (c : W4) : Nat := val4 c.w3 c.w2 c.w1 c.w0
+
+/-- Bit `i` of `ah ‖ al` in bit 0. -/
+private def bitAt (ah al : UInt64) (i : Nat) : UInt64 :=
+  if i < 64 then al >>> i.toUInt64 else ah >>> (i - 64).toUInt64
+
+private theorem testBit_shr (w : UInt64) (s : Nat) (hs : s < 64) :
+    (w >>> s.toUInt64).toNat.testBit 0 = w.toNat.testBit s := by
+  simp [Nat.mod_eq_of_lt hs]
+
+private theorem testBit_bitAt (ah al : UInt64) (i : Nat) (hi : i < 128) :
+    (bitAt ah al i).toNat.testBit 0 = (val4 0 0 ah al).testBit i := by
+  rw [testBit_val4, bitAt]
+  split
+  · rw [testBit_shr _ _ (by omega)]
+  · rw [testBit_shr _ _ (by omega)]
+
+/-- Steps `i, …, i + n - 1` of `clmul`, with `s = b <<< i`. -/
+private def clmulLoop (ah al : UInt64) :
+    Nat → Nat → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → UInt64 → W4
+  | 0, _, c3, c2, c1, c0, _, _, _, _ => ⟨c3, c2, c1, c0⟩
+  | n + 1, i, c3, c2, c1, c0, s3, s2, s1, s0 =>
+    let m := mask (bitAt ah al i)
+    clmulLoop ah al n (i + 1) (c3 ^^^ (s3 &&& m)) (c2 ^^^ (s2 &&& m)) (c1 ^^^ (s1 &&& m))
+      (c0 ^^^ (s0 &&& m)) ((s3 <<< 1) ||| (s2 >>> 63)) ((s2 <<< 1) ||| (s1 >>> 63))
+      ((s1 <<< 1) ||| (s0 >>> 63)) (s0 <<< 1)
+
+private def clmulStep (a b : Nat) (acc : Nat) (i : Nat) : Nat :=
+  if a.testBit i then acc ^^^ (b <<< i) else acc
+
+private theorem clmul_eq (a b : Nat) : clmul a b = (List.range 128).foldl (clmulStep a b) 0 := rfl
+
+private theorem clmulLoop_spec (ah al : UInt64) (b : Nat) (hb : b < 2 ^ 128) :
+    ∀ n i c3 c2 c1 c0 s3 s2 s1 s0, i + n ≤ 128 → val4 s3 s2 s1 s0 = b <<< i →
+      (clmulLoop ah al n i c3 c2 c1 c0 s3 s2 s1 s0).toNat =
+        (List.range' i n).foldl (clmulStep (val4 0 0 ah al) b) (val4 c3 c2 c1 c0) := by
+  intro n
+  induction n with
+  | zero => intros; rfl
+  | succ n ih =>
+    intro i c3 c2 c1 c0 s3 s2 s1 s0 hn hs
+    have hlt : b <<< (i + 1) < 2 ^ 256 := by
+      rw [Nat.shiftLeft_eq]
+      calc b * 2 ^ (i + 1) < 2 ^ 128 * 2 ^ (i + 1) :=
+            Nat.mul_lt_mul_of_pos_right hb (Nat.two_pow_pos _)
+        _ = 2 ^ (128 + (i + 1)) := (Nat.pow_add _ _ _).symm
+        _ ≤ 2 ^ 256 := Nat.pow_le_pow_right (by omega) (by omega)
+    have hs' : val4 ((s3 <<< 1) ||| (s2 >>> 63)) ((s2 <<< 1) ||| (s1 >>> 63))
+        ((s1 <<< 1) ||| (s0 >>> 63)) (s0 <<< 1) = b <<< (i + 1) := by
+      rw [val4_shl1, hs, ← Nat.shiftLeft_add]
+      exact Nat.mod_eq_of_lt hlt
+    rw [clmulLoop, ih _ _ _ _ _ _ _ _ _ (by omega) hs', List.range'_succ, List.foldl_cons]
+    refine congrArg
+      (fun z => List.foldl (clmulStep (val4 0 0 ah al) b) z (List.range' (i + 1) n)) ?_
+    rw [val4_xor, val4_and_mask, testBit_bitAt _ _ _ (by omega), hs, clmulStep]
+    split <;> simp
+
+/-- `n` steps of `divX128`. -/
+private def divLoop : Nat → UInt64 → UInt64 → UInt64 → UInt64 → W4
+  | 0, c3, c2, c1, c0 => ⟨c3, c2, c1, c0⟩
+  | n + 1, c3, c2, c1, c0 =>
+    let m := mask c0
+    let c2 := c2 ^^^ (1 &&& m)
+    let c1 := c1 ^^^ (0xC200000000000000 &&& m)
+    let c0 := c0 ^^^ (1 &&& m)
+    divLoop n (c3 >>> 1) ((c2 >>> 1) ||| (c3 <<< 63)) ((c1 >>> 1) ||| (c2 <<< 63))
+      ((c0 >>> 1) ||| (c1 <<< 63))
+
+private theorem modulus_eq : val4 0 1 0xC200000000000000 1 = modulus := by decide
+
+private theorem divLoop_spec : ∀ (n : Nat) (l : List Nat) c3 c2 c1 c0, l.length = n →
+    (divLoop n c3 c2 c1 c0).toNat = l.foldl (fun c _ => divStep c) (val4 c3 c2 c1 c0)
+  | 0, [], _, _, _, _, _ => rfl
+  | n + 1, _ :: l, c3, c2, c1, c0, hl => by
+    rw [divLoop, divLoop_spec n l _ _ _ _ (by simpa using hl), List.foldl_cons]
+    congr 1
+    have hx := val4_xor c3 c2 c1 c0 (0 &&& mask c0) (1 &&& mask c0) (0xC200000000000000 &&& mask c0)
+      (1 &&& mask c0)
+    rw [val4_and_mask, modulus_eq] at hx
+    have h0 : (val4 c3 c2 c1 c0).testBit 0 = c0.toNat.testBit 0 := by
+      rw [testBit_val4, if_pos (by omega)]
+    simp only [UInt64.zero_and, UInt64.xor_zero] at hx
+    rw [divStep, h0, val4_shr1, hx]
+    split <;> simp
+
+/-- A field element as its high and low 64 bits. -/
+structure Elem where
+  hi : UInt64
+  lo : UInt64
+
+/-- The element as a 128-bit integer, `hi` on top. -/
+def Elem.toNat (a : Elem) : Nat := val4 0 0 a.hi a.lo
+
+theorem Elem.toNat_lt (a : Elem) : a.toNat < 2 ^ 128 := by
+  apply Nat.lt_pow_two_of_testBit
+  intro i hi
+  rw [Elem.toNat, testBit_val4]
+  repeat' split
+  all_goals first | omega | exact testBit_word _ _ (by omega) | simp
+
+def Elem.xor (a b : Elem) : Elem := ⟨a.hi ^^^ b.hi, a.lo ^^^ b.lo⟩
+
+theorem Elem.toNat_xor (a b : Elem) : (a.xor b).toNat = a.toNat ^^^ b.toNat := by
+  simp only [Elem.xor, Elem.toNat]
+  rw [← val4_xor, UInt64.xor_zero]
+
+/-- `dot` on two-word elements: `clmul` into four words, then 128 masked halvings. -/
+def dotCT (a b : Elem) : Elem :=
+  let p := clmulLoop a.hi a.lo 128 0 0 0 0 0 0 0 b.hi b.lo
+  let c := divLoop 128 p.w3 p.w2 p.w1 p.w0
+  ⟨c.w1, c.w0⟩
+
+theorem dotCT_spec (a b : Elem) : (dotCT a b).toNat = dot a.toNat b.toNat := by
+  have hp := clmulLoop_spec a.hi a.lo b.toNat b.toNat_lt 128 0 0 0 0 0 0 0 b.hi b.lo (by omega)
+    (by rw [Nat.shiftLeft_zero]; rfl)
+  simp only [dotCT]
+  generalize clmulLoop a.hi a.lo 128 0 0 0 0 0 0 0 b.hi b.lo = P at hp ⊢
+  have hP : val4 P.w3 P.w2 P.w1 P.w0 = clmul a.toNat b.toNat := by
+    rw [clmul_eq, List.range_eq_range']; exact hp
+  have hc := divLoop_spec 128 (List.range 128) P.w3 P.w2 P.w1 P.w0 (by simp)
+  rw [← divX128_eq, hP] at hc
+  generalize divLoop 128 P.w3 P.w2 P.w1 P.w0 = C at hc ⊢
+  have hlt : C.toNat < 2 ^ 128 := hc ▸ divX128_lt _ (hP ▸ val4_lt _ _ _ _)
+  rw [dot, ← hc]
+  exact (val4_low _ _ _ _ hlt).symm
+
+/-! ## Loading and storing blocks -/
+
+/-- The little-endian value of `f 0, …, f (n - 1)`. -/
+private def leNat (f : Nat → UInt8) : Nat → Nat
+  | 0 => 0
+  | n + 1 => leNat (fun j => f (j + 1)) n <<< 8 ||| (f 0).toNat
+
+private theorem shl8_or (x : Nat) (b : UInt8) : x <<< 8 ||| b.toNat = x * 256 + b.toNat := by
+  rw [← Nat.shiftLeft_add_eq_or_of_lt b.toNat_lt, Nat.shiftLeft_eq]
+
+private theorem leNat_lt : ∀ (n : Nat) (f : Nat → UInt8), leNat f n < 2 ^ (8 * n)
+  | 0, _ => by simp [leNat]
+  | n + 1, f => by
+    have ih := leNat_lt n (fun j => f (j + 1))
+    have hb := (f 0).toNat_lt
+    rw [leNat, shl8_or, show 8 * (n + 1) = 8 * n + 8 by omega, Nat.pow_add]
+    have : (2:Nat) ^ 8 = 256 := rfl
+    rw [this] at hb ⊢
+    omega
+
+private theorem leNat_congr : ∀ (n : Nat) (f g : Nat → UInt8), (∀ j, j < n → f j = g j) →
+    leNat f n = leNat g n
+  | 0, _, _, _ => rfl
+  | n + 1, f, g, h => by
+    rw [leNat, leNat, leNat_congr n _ (fun j => g (j + 1)) (fun j hj => h _ (by omega)),
+      h 0 (by omega)]
+
+private theorem leNat_zero : ∀ (k : Nat) (f : Nat → UInt8), (∀ j, f j = 0) → leNat f k = 0
+  | 0, _, _ => rfl
+  | k + 1, f, h => by rw [leNat, leNat_zero k _ (fun j => h _), h 0]; rfl
+
+private theorem leNat_extend : ∀ (n k : Nat) (f : Nat → UInt8), (∀ j, n ≤ j → f j = 0) →
+    leNat f (n + k) = leNat f n
+  | 0, k, f, h => by rw [Nat.zero_add, leNat_zero k f (fun j => h j (by omega))]; rfl
+  | n + 1, k, f, h => by
+    rw [show n + 1 + k = (n + k) + 1 by omega, leNat, leNat,
+      leNat_extend n k _ (fun j hj => h _ (by omega))]
+
+private theorem leNat_split : ∀ (m n : Nat) (f : Nat → UInt8),
+    leNat f (m + n) = leNat (fun j => f (m + j)) n <<< (8 * m) ||| leNat f m
+  | 0, n, f => by simp [leNat]
+  | m + 1, n, f => by
+    rw [show m + 1 + n = (m + n) + 1 by omega, leNat, leNat, leNat_split m n,
+      Nat.shiftLeft_or_distrib, ← Nat.shiftLeft_add, Nat.or_assoc,
+      show 8 * m + 8 = 8 * (m + 1) by omega]
+    congr 3
+    funext j
+    rw [show m + j + 1 = m + 1 + j by omega]
+
+/-- `leNat` in a `UInt64`, for `n ≤ 8`. -/
+private def wordLE (f : Nat → UInt8) : Nat → UInt64
+  | 0 => 0
+  | n + 1 => wordLE (fun j => f (j + 1)) n <<< 8 ||| (f 0).toUInt64
+
+private theorem wordLE_toNat : ∀ (n : Nat) (f : Nat → UInt8), n ≤ 8 → (wordLE f n).toNat = leNat f n
+  | 0, _, _ => rfl
+  | n + 1, f, hn => by
+    have ih := wordLE_toNat n (fun j => f (j + 1)) (by omega)
+    have hl := leNat_lt n (fun j => f (j + 1))
+    simp only [wordLE, leNat, UInt64.toNat_or, UInt64.toNat_shiftLeft, ih, UInt8.toNat_toUInt64]
+    rw [show UInt64.toNat 8 % 64 = 8 from rfl, Nat.mod_eq_of_lt]
+    rw [Nat.shiftLeft_eq]
+    have : 2 ^ (8 * n) * 2 ^ 8 ≤ 2 ^ 64 := by
+      rw [← Nat.pow_add]; exact Nat.pow_le_pow_right (by omega) (by omega)
+    have : (2:Nat) ^ 8 = 256 := rfl
+    have := Nat.mul_lt_mul_of_pos_right hl (show 0 < 2 ^ 8 by omega)
+    omega
+
+private theorem foldr_eq (l : List UInt8) :
+    l.foldr (fun b acc => (acc <<< 8) ||| b.toNat) 0 = leNat (fun j => l.getD j 0) l.length := by
+  induction l with
+  | nil => rfl
+  | cons x l ih =>
+    rw [List.foldr_cons, ih, List.length_cons, leNat]
+    simp
+
+private theorem array_foldr_eq (a : Array UInt8) :
+    a.foldr (fun b acc => (acc <<< 8) ||| b.toNat) 0 = leNat (fun j => a.getD j 0) a.size := by
+  rcases a with ⟨l⟩
+  rw [List.foldr_toArray', foldr_eq, List.size_toArray]
+  · apply leNat_congr
+    intro j hj
+    simp [Array.getD, hj]
+  · rfl
+
+/-- The 16 bytes at `off`, little-endian, zero-padded past the end. -/
+def load (a : Array UInt8) (off : Nat) : Elem :=
+  ⟨wordLE (fun j => a.getD (off + 8 + j) 0) 8, wordLE (fun j => a.getD (off + j) 0) 8⟩
+
+private theorem getD_extract (a : Array UInt8) (off j : Nat) (hj : j < 16) :
+    (a.extract off (off + 16)).getD j 0 = a.getD (off + j) 0 := by
+  simp only [Array.getD, Array.size_extract]
+  by_cases h : off + j < a.size
+  · rw [dif_pos (by omega), dif_pos h]; simp
+  · rw [dif_neg (by omega), dif_neg h]
+
+theorem load_toNat (a : Array UInt8) (off : Nat) :
+    (load a off).toNat =
+      (a.extract off (off + 16)).foldr (fun b acc => (acc <<< 8) ||| b.toNat) 0 := by
+  have hs : (a.extract off (off + 16)).size ≤ 16 := by simp; omega
+  rw [array_foldr_eq, ← leNat_extend _ (16 - (a.extract off (off + 16)).size) _
+      (fun j hj => by simp only [Array.getD, dif_neg (Nat.not_lt.mpr hj)]),
+    Nat.add_sub_cancel' hs,
+    leNat_congr 16 _ (fun j => a.getD (off + j) 0) (fun j hj => getD_extract a off j hj),
+    show 16 = 8 + 8 from rfl, leNat_split, load, Elem.toNat,
+    ← wordLE_toNat 8 _ (by omega), ← wordLE_toNat 8 _ (by omega)]
+  simp [val4, Nat.add_assoc]
+
+/-- An element as 16 little-endian bytes. -/
+def store (e : Elem) : Vector UInt8 16 :=
+  Vector.ofFn fun i : Fin 16 =>
+    if i.val < 8 then (e.lo >>> (8 * i.val).toUInt64).toUInt8
+    else (e.hi >>> (8 * (i.val - 8)).toUInt64).toUInt8
+
+theorem store_eq (e : Elem) : store e = toBytes e.toNat := by
+  ext i hi
+  simp only [store, toBytes, Vector.getElem_ofFn]
+  apply UInt8.toNat_inj.mp
+  apply Nat.eq_of_testBit_eq
+  intro j
+  rw [UInt8.toNat_ofNat', Nat.mod_mod]
+  split
+  · simp only [UInt64.toNat_toUInt8, UInt64.toNat_shiftRight, UInt64.toNat_ofNat']
+    simp only [show (256 : Nat) = 2 ^ 8 from rfl, Nat.testBit_mod_two_pow, Nat.testBit_shiftRight,
+      Elem.toNat, testBit_val4]
+    rw [Nat.mod_eq_of_lt (by omega : 8 * i % 2 ^ 64 < 64),
+      Nat.mod_eq_of_lt (by omega : 8 * i < 2 ^ 64)]
+    by_cases hj : j < 8
+    · rw [if_pos (by omega)]
+    · simp [hj]
+  · simp only [UInt64.toNat_toUInt8, UInt64.toNat_shiftRight, UInt64.toNat_ofNat']
+    simp only [show (256 : Nat) = 2 ^ 8 from rfl, Nat.testBit_mod_two_pow, Nat.testBit_shiftRight,
+      Elem.toNat, testBit_val4]
+    rw [Nat.mod_eq_of_lt (by omega : 8 * (i - 8) % 2 ^ 64 < 64),
+      Nat.mod_eq_of_lt (by omega : 8 * (i - 8) < 2 ^ 64)]
+    by_cases hj : j < 8
+    · rw [if_neg (by omega), if_pos (by omega),
+        tb_congr e.hi.toNat (by omega : 8 * (i - 8) + j = 8 * i + j - 64)]
+    · simp [hj]
+
+def polyval (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16 :=
+  let hf := load h.toArray 0
+  -- `ByteArray.data` copies, so convert once rather than per block
+  let b := blocks.data
+  store <| (List.range ((blocks.size + 15) / 16)).foldl
+    (fun s i => dotCT (s.xor (load b (16 * i))) hf) ⟨0, 0⟩
+
+theorem polyval_eq_spec (h : Vector UInt8 16) (blocks : ByteArray) :
+    polyval h blocks = polyvalSpec h blocks := by
+  simp only [polyval, polyvalSpec, store_eq]
+  congr 1
+  refine (List.foldl_hom Elem.toNat (fun y i => ?_)).symm
+  rw [dotCT_spec, Elem.toNat_xor, load_toNat, load_toNat]
+  have : h.toArray.extract 0 (0 + 16) = h.toArray := by
+    apply Array.ext <;> simp
+  simp only [blockAt, ofBytes, ByteArray.data_extract, this]
+
 end Cryptlib.Primitives.Cipher.Polyval
diff --git a/Cryptlib/Primitives/Cipher/test.lean b/Cryptlib/Primitives/Cipher/test.lean
index d68edcbb..589926e9 100644
--- a/Cryptlib/Primitives/Cipher/test.lean
+++ b/Cryptlib/Primitives/Cipher/test.lean
@@ -5,6 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.Cipher.AESGCMSIV
+import Cryptlib.Primitives.Cipher.GHash
 import Cryptlib.Util.HexBytes
 
 /-!
@@ -67,6 +68,38 @@ def aes128BlockOk : Bool :=
   let input : Vector UInt8 16 := Vector.ofFn fun i : Fin 16 => UInt8.ofNat (17 * i.val)
   hexOf (AES.encryptBlockWithKey128 key input) == "69c4e0d86a7b0430d8cdb78070b4c55a"
 
+/-- A byte stream from a 64-bit LCG, for comparing implementations on arbitrary inputs. -/
+def lcgBytes (seed : UInt64) (n : Nat) : ByteArray := Id.run do
+  let mut x := seed
+  let mut out := ByteArray.emptyWithCapacity n
+  for _ in [0:n] do
+    x := x * 6364136223846793005 + 1442695040888963407
+    out := out.push (x >>> 56).toUInt8
+  return out
+
+def vec16 (b : ByteArray) : Vector UInt8 16 := Vector.ofFn fun i : Fin 16 => b.data.getD i.val 0
+
+/-- The circuit-S-box cipher against the table specification on `n` random keys and blocks. -/
+def aesAgreesWithSpec (n : Nat) : Bool := (List.range n).all fun i =>
+  let r := lcgBytes (UInt64.ofNat i) 64
+  let k128 := vec16 r
+  let k256 : Vector UInt8 32 := Vector.ofFn fun j : Fin 32 => r.data.getD (16 + j.val) 0
+  let x := vec16 (r.extract 48 64)
+  AES.encryptBlock (AES.expandKey128 k128) x == AES.encryptBlockSpec (AES.expandKey128Spec k128) x &&
+    AES.encryptBlock (AES.expandKey k256) x == AES.encryptBlockSpec (AES.expandKeySpec k256) x
+
+/-- Two-word GHASH against the `Nat` specification on `n` random keys and lengths. -/
+def ghashAgreesWithSpec (n : Nat) : Bool := (List.range n).all fun i =>
+  let h := vec16 (lcgBytes (UInt64.ofNat (1000 + i)) 16)
+  let msg := lcgBytes (UInt64.ofNat (2000 + i)) (i * 7 % 100)
+  GHash.ghash h msg == GHash.ghashSpec h msg
+
+/-- Two-word POLYVAL against the `Nat` specification on `n` random keys and lengths. -/
+def polyvalAgreesWithSpec (n : Nat) : Bool := (List.range n).all fun i =>
+  let h := vec16 (lcgBytes (UInt64.ofNat (3000 + i)) 16)
+  let msg := lcgBytes (UInt64.ofNat (4000 + i)) (i * 7 % 100)
+  Polyval.polyval h msg == Polyval.polyvalSpec h msg
+
 /-- Decode an inline hex literal. -/
 def hex (s : String) : Except String ByteArray :=
   match hexStringToByteArray s with
@@ -85,7 +118,7 @@ def main : IO UInt32 := do
 
   IO.println "AES-256 block (FIPS-197 C.3)"
   if aesBlockOk then
-    IO.println "  ok    single block, computed S-box"
+    IO.println "  ok    single block"
   else
     ok := false
     IO.println "  FAIL  single block"
@@ -93,11 +126,29 @@ def main : IO UInt32 := do
   IO.println ""
   IO.println "AES-128 block (FIPS-197 C.1)"
   if aes128BlockOk then
-    IO.println "  ok    single block, computed S-box"
+    IO.println "  ok    single block"
   else
     ok := false
     IO.println "  FAIL  single block"
 
+  IO.println ""
+  IO.println "Constant-time implementations against their specifications"
+  if aesAgreesWithSpec 200 then
+    IO.println "  ok    AES-128 and AES-256, 200 random keys and blocks"
+  else
+    ok := false
+    IO.println "  FAIL  AES against the table specification"
+  if ghashAgreesWithSpec 200 then
+    IO.println "  ok    GHASH, 200 random keys and lengths"
+  else
+    ok := false
+    IO.println "  FAIL  GHASH against the Nat specification"
+  if polyvalAgreesWithSpec 200 then
+    IO.println "  ok    POLYVAL, 200 random keys and lengths"
+  else
+    ok := false
+    IO.println "  FAIL  POLYVAL against the Nat specification"
+
   IO.println ""
   IO.println "POLYVAL (RFC 8452 §3 worked example)"
   let h ← unwrap (do fixed 16 "H" (← hex "25629347589242761d31f826ba4b757b"))
diff --git a/Cryptlib/Util/ConstantTime.lean b/Cryptlib/Util/ConstantTime.lean
new file mode 100644
index 00000000..21da46f5
--- /dev/null
+++ b/Cryptlib/Util/ConstantTime.lean
@@ -0,0 +1,69 @@
+/-
+SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
+SPDX-License-Identifier: AGPL-3.0-only
+-/
+
+namespace Cryptlib.Util.ConstantTime
+
+/-! # Branch-free helpers
+
+Selection by masks and a byte-string comparison without an early exit, each proved equal to its
+branching counterpart. Lengths and loop bounds are treated as public. Lean compiles through C and
+neither compiler is proven to preserve the absence of secret-dependent branches, so this is a
+property of the source, not a verified property of the machine code. -/
+
+/-- All ones if bit 0 of `b` is set, else zero. -/
+def mask (b : UInt64) : UInt64 := 0 - (b &&& 1)
+
+theorem and_one (b : UInt64) : b &&& 1 = if b.toNat.testBit 0 then 1 else 0 := by
+  apply UInt64.toNat_inj.mp
+  rcases Nat.mod_two_eq_zero_or_one b.toNat with h | h <;>
+    simp [Nat.testBit, Nat.and_one_is_mod, h] <;> rfl
+
+theorem and_mask (x b : UInt64) : x &&& mask b = if b.toNat.testBit 0 then x else 0 := by
+  rw [mask, and_one]; split <;> simp
+
+/-- The OR of `a[i] ^^^ b[i]` over `i < n`. -/
+private def diff (a b : ByteArray) (n : Nat) : UInt8 :=
+  Nat.fold n (fun i _ acc => acc ||| (a[i]! ^^^ b[i]!)) 0
+
+/-- Byte-string equality that reads every byte: XOR differences are OR-accumulated over the full
+length and tested once at the end. -/
+def ctEq (a b : ByteArray) : Bool := a.size == b.size && diff a b a.size == 0
+
+private theorem diff_eq_zero (a b : ByteArray) :
+    ∀ n, diff a b n = 0 ↔ ∀ i, i < n → a[i]! = b[i]!
+  | 0 => by simp [diff]
+  | n + 1 => by
+    show (diff a b n ||| (a[n]! ^^^ b[n]!)) = 0 ↔ _
+    rw [UInt8.or_eq_zero_iff, diff_eq_zero a b n, UInt8.xor_eq_zero_iff]
+    constructor
+    · rintro ⟨h, hn⟩ i hi
+      rcases Nat.lt_succ_iff_lt_or_eq.mp hi with hi | rfl
+      · exact h i hi
+      · exact hn
+    · intro h
+      exact ⟨fun i hi => h i (by omega), h n (by omega)⟩
+
+theorem ctEq_iff (a b : ByteArray) : ctEq a b = true ↔ a = b := by
+  simp only [ctEq, Bool.and_eq_true, beq_iff_eq, diff_eq_zero]
+  constructor
+  · rintro ⟨hs, h⟩
+    apply ByteArray.ext
+    apply Array.ext (by simpa using hs)
+    intro i h1 h2
+    have h1' : i < a.size := by simpa using h1
+    have h2' : i < b.size := by simpa using h2
+    have := h i h1'
+    rw [getElem!_pos a i h1', getElem!_pos b i h2'] at this
+    exact this
+  · rintro rfl
+    exact ⟨rfl, fun _ _ => rfl⟩
+
+theorem ctEq_eq_decide (a b : ByteArray) : ctEq a b = decide (a = b) := by
+  by_cases h : a = b
+  · simp [h, (ctEq_iff b b).mpr rfl]
+  · simp only [h, decide_false]
+    exact Bool.eq_false_iff.mpr fun h' => h ((ctEq_iff a b).mp h')
+
+end Cryptlib.Util.ConstantTime
diff --git a/bench/CryptlibBench/Cipher.lean b/bench/CryptlibBench/Cipher.lean
index f471c91d..b7c6182e 100644
--- a/bench/CryptlibBench/Cipher.lean
+++ b/bench/CryptlibBench/Cipher.lean
@@ -6,9 +6,11 @@ SPDX-License-Identifier: AGPL-3.0-only
 import Cryptlib.Primitives.Cipher.ChaChaPoly
 import Cryptlib.Primitives.Cipher.Polyval
 import Cryptlib.Primitives.Cipher.AESGCMSIV
+import Cryptlib.Primitives.Cipher.AESGCM
 import LeanBench
 
-/-! # ChaCha20, Poly1305, POLYVAL and AES-GCM-SIV benchmarks at growing message sizes
+/-! # ChaCha20, Poly1305, POLYVAL and AES-GCM-SIV benchmarks at growing message sizes, and AES,
+GHASH and AES-128-GCM on one packet, against their specifications where those differ
 
 Inputs are read from refs so the compiler cannot hoist the work out of the timed action. -/
 
@@ -17,6 +19,8 @@ namespace CryptlibBench.Cipher
 open Cryptlib.Primitives.Cipher.ChaChaPoly (chacha20 poly1305)
 open Cryptlib.Primitives.Cipher.Polyval (polyval)
 open Cryptlib.Util.Bytes (ofVector)
+open Cryptlib.Primitives.Cipher.AES (encryptBlock encryptBlockSpec expandKey expandKey128)
+open Cryptlib.Primitives.Cipher.GHash (ghash ghashSpec)
 
 private def cfg : LeanBench.BenchConfig := { suite := some "cipher", samples := 10, warmup := 1 }
 
@@ -40,6 +44,31 @@ def benches : IO (Array LeanBench.Bench) := do
                     action := do
                       out.set (Cryptlib.Primitives.Cipher.AESGCMSIV.encrypt (← key.get) (← nonce.get)
                         ByteArray.empty (← msg.get)) }
+  let blk ← IO.mkRef (Vector.replicate 16 (5 : UInt8))
+  let blkOut ← IO.mkRef (Vector.replicate 16 (0 : UInt8))
+  let rk128 ← IO.mkRef (expandKey128 (Vector.replicate 16 (1 : UInt8)))
+  let rk256 ← IO.mkRef (expandKey (Vector.replicate 32 (1 : UInt8)))
+  bs := bs.push { name := "aes-128 block", config := cfg,
+                  action := do blkOut.set (encryptBlock (← rk128.get) (← blk.get)) }
+  bs := bs.push { name := "aes-256 block", config := cfg,
+                  action := do blkOut.set (encryptBlock (← rk256.get) (← blk.get)) }
+  bs := bs.push { name := "aes-128 block, table spec", config := cfg,
+                  action := do blkOut.set (encryptBlockSpec (← rk128.get) (← blk.get)) }
+  let packet ← IO.mkRef (ByteArray.mk (Array.ofFn fun (i : Fin 1200) => (i.val * 7 % 251).toUInt8))
+  let ghashIn ← IO.mkRef (ByteArray.mk (Array.ofFn fun (i : Fin 1232) => (i.val * 7 % 251).toUInt8))
+  bs := bs.push { name := "ghash 1232B", config := cfg,
+                  action := do blkOut.set (ghash (← h.get) (← ghashIn.get)) }
+  bs := bs.push { name := "ghash 1232B, Nat spec", config := cfg,
+                  action := do blkOut.set (ghashSpec (← h.get) (← ghashIn.get)) }
+  bs := bs.push { name := "polyval 1232B", config := cfg,
+                  action := do blkOut.set (polyval (← h.get) (← ghashIn.get)) }
+  bs := bs.push { name := "polyval 1232B, Nat spec", config := cfg,
+                  action := do
+                    blkOut.set (Cryptlib.Primitives.Cipher.Polyval.polyvalSpec (← h.get) (← ghashIn.get)) }
+  bs := bs.push { name := "aes-128-gcm encrypt 1200B", config := cfg,
+                  action := do
+                    out.set (Cryptlib.Primitives.Cipher.AESGCM.encrypt (← rk128.get) (← nonce.get)
+                      ByteArray.empty (← packet.get)) }
   pure bs
 
 end CryptlibBench.Cipher