diff --git a/Complexity.lean b/Complexity.lean
index dddfad9a3..32982b1eb 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1318,6 +1318,7 @@ public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Reduction
 public import Complexity.Crypto.Computational.Homomorphic.FixedKey.Security
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Basic
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Decoding
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Gadget
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Hiding
 public import Complexity.Crypto.Computational.Homomorphic.GSW.LWE
@@ -1329,6 +1330,8 @@ public import Complexity.Crypto.Computational.Homomorphic.GSW.Sampling.Serialize
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Security
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Evaluation
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Evaluation.PolyTime
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.PolyTime
 public import Complexity.Crypto.Computational.Homomorphic.KeyChain
 public import Complexity.Crypto.Computational.Homomorphic.KeyChain.Hybrid
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Decoding.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Decoding.lean
index 1c6217cb3..f3351479f 100644
--- a/Complexity/Crypto/Computational/Homomorphic/GSW/Decoding.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Decoding.lean
@@ -9,6 +9,8 @@ module
 
 public import Complexity.Init
 public import Mathlib.Data.ZMod.Basic
+import Mathlib.Data.Nat.Bitwise
+import Mathlib.Tactic.IntervalCases
 
 /-!
 # Scalar decoding for GSW ciphertexts
@@ -27,6 +29,8 @@ by modular wraparound.
 
 * `Cslib.Crypto.Homomorphic.GSW.decode_eq_of_error`: errors of magnitude strictly below
   one quarter of the modulus preserve the encoded bit.
+* `Cslib.Crypto.Homomorphic.GSW.decode_eq_xor_highBits`: for width at least two, decoding
+  is exclusive-or of the two highest bits of the canonical residue, on every input.
 
 ## References
 
@@ -47,6 +51,47 @@ def decode (w : ℕ) (x : ZMod (2 ^ w)) : Bool :=
     decode w x = true ↔ 2 ^ w ≤ 4 * x.val ∧ 4 * x.val < 3 * 2 ^ w := by
   simp [decode]
 
+/-- Width zero has only the zero residue, which decodes to `false`. -/
+@[simp] theorem decode_zero (x : ZMod (2 ^ 0)) : decode 0 x = false := by
+  have hx : x.val = 0 := by
+    have h : x.val < 1 := ZMod.val_lt x
+    omega
+  simp [decode, hx]
+
+/-- At width one, the single bit is already the decoded message. -/
+theorem decode_one (x : ZMod (2 ^ 1)) : decode 1 x = x.val.testBit 0 := by
+  have hx : x.val < 2 := ZMod.val_lt x
+  simp only [decode, pow_one, Nat.testBit_eq_decide_div_mod_eq, pow_zero, Nat.div_one,
+    Nat.mod_eq_of_lt hx]
+  congr 1
+  apply propext
+  omega
+
+/-- The half-open middle interval is exactly the set where the two highest bits differ.
+This identity holds on every residue, including both quarter-boundary ties. -/
+theorem decode_eq_xor_highBits {w : ℕ} (hw : 2 ≤ w) (x : ZMod (2 ^ w)) :
+    decode w x = (x.val.testBit (w - 1) ^^ x.val.testBit (w - 2)) := by
+  obtain ⟨k, rfl⟩ : ∃ k, w = k + 2 := ⟨w - 2, by omega⟩
+  have hp : 0 < 2 ^ k := Nat.two_pow_pos k
+  have hq : 2 ^ (k + 2) = 4 * 2 ^ k := by simp [pow_add, Nat.mul_comm]
+  have hh : 2 ^ (k + 2 - 1) = 2 ^ k * 2 := by
+    rw [show k + 2 - 1 = k + 1 by omega, pow_succ]
+  have hx : x.val / 2 ^ k < 4 := (Nat.div_lt_iff_lt_mul hp).mpr (by
+    have := ZMod.val_lt x
+    omega)
+  have hlo : 1 ≤ x.val / 2 ^ k ↔ 2 ^ k ≤ x.val := by
+    simpa only [one_mul] using (Nat.le_div_iff_mul_le hp :
+      1 ≤ x.val / 2 ^ k ↔ 1 * 2 ^ k ≤ x.val)
+  have hhi : x.val / 2 ^ k < 3 ↔ x.val < 3 * 2 ^ k := Nat.div_lt_iff_lt_mul hp
+  have hdecode : decode (k + 2) x = decide (1 ≤ x.val / 2 ^ k ∧ x.val / 2 ^ k < 3) := by
+    simp only [decode, hq, hlo, hhi]
+    congr 1
+    apply propext
+    omega
+  rw [hdecode, Nat.testBit_eq_decide_div_mod_eq, Nat.testBit_eq_decide_div_mod_eq,
+    hh, Nat.add_sub_cancel, ← Nat.div_div_eq_div_mul]
+  interval_cases h : x.val / 2 ^ k <;> simp
+
 /-- Decoding recovers a bit whenever its integer error has magnitude strictly below one
 quarter of the modulus. The strict inequality excludes the decoder's asymmetric ties. -/
 theorem decode_eq_of_error {w : ℕ} (hw : 0 < w) (μ : Bool) (error : ℤ)
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Decryption.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Decryption.lean
new file mode 100644
index 000000000..88a08ff45
--- /dev/null
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Decryption.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Basic
+import Mathlib.Algebra.BigOperators.Fin
+
+/-!
+# Exact row arithmetic for GSW decryption
+
+The expanded-secret product used by `GSW.decrypt` equals one recomposed ciphertext row
+paired with the unexpanded secret. Its first coordinate is subtracted by the sum of the
+remaining coordinates times the secret entries. For width at least two, decryption is
+exclusive-or of the two highest bits of this residue.
+
+These identities hold on every typed secret and Boolean ciphertext. They require no key
+generation, encryption support or noise hypothesis, as needed for a decryption circuit
+correct on all well-sized raw inputs. They do not yet construct that circuit or bound its depth.
+
+## Main definitions
+
+* `decryptionPhase`: the recomposed row's modular inner product with the secret vector.
+
+## Main results
+
+* `decryptionPhase_eq_mulVec`: the row expression equals the original expanded-secret product.
+* `decrypt_eq_decode_decryptionPhase`: decryption uses the highest row of the leading coordinate.
+* `decrypt_eq_xor_highBits`: the two highest bits determine decryption at width at least two.
+
+## References
+
+* [C. Gentry, A. Sahai and B. Waters, *Homomorphic Encryption from Learning with Errors:
+  Conceptually-Simpler, Asymptotically-Faster, Attribute-Based*][GentrySahaiWaters2013],
+  Sections 3.1 and 3.4.
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Homomorphic.GSW
+
+open Matrix
+open scoped Matrix
+
+/-- Recompose one ciphertext row, then take its inner product with `(1,-t)`. -/
+def decryptionPhase {n w : ℕ} (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w)
+    (row : Fin (n + 1) × Fin w) : ZMod (2 ^ w) :=
+  recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) C) row 0 -
+    ∑ j : Fin n, recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) C) row j.succ * t j
+
+/-- Row recomposition preserves the original multiplication by the expanded secret. -/
+theorem decryptionPhase_eq_mulVec {n w : ℕ} (t : Fin n → ZMod (2 ^ w))
+    (C : Ciphertext n w) (row : Fin (n + 1) × Fin w) :
+    decryptionPhase t C row =
+      (bitMatrix (ZMod (2 ^ w)) C *ᵥ powersOfTwo w (secretVector t)) row := by
+  rw [← recomposeMatrix_mulVec]
+  simp [decryptionPhase, Matrix.mulVec, dotProduct, secretVector, Fin.sum_univ_succ,
+    sub_eq_add_neg]
+
+/-- The total width-zero decryption routine returns `false`. -/
+@[simp] theorem decrypt_zero {n : ℕ} (t : Fin n → ZMod (2 ^ 0)) (C : Ciphertext n 0) :
+    decrypt t C = false := by
+  simp [decrypt]
+
+/-- At positive width, decryption reads the highest digit of the leading coordinate. -/
+theorem decrypt_eq_decode_decryptionPhase {n w : ℕ} (hw : 0 < w)
+    (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) :
+    decrypt t C = decode w (decryptionPhase t C (0, ⟨w - 1, by omega⟩)) := by
+  rw [decryptionPhase_eq_mulVec]
+  simp [decrypt, hw]
+
+/-- At width one, decryption is the sole bit of the selected row's phase. -/
+theorem decrypt_one {n : ℕ} (t : Fin n → ZMod (2 ^ 1)) (C : Ciphertext n 1) :
+    decrypt t C = (decryptionPhase t C (0, 0)).val.testBit 0 := by
+  rw [decrypt_eq_decode_decryptionPhase (by decide), decode_one]
+  rfl
+
+/-- At width at least two, all raw ciphertexts decrypt by exclusive-or of two phase bits. -/
+theorem decrypt_eq_xor_highBits {n w : ℕ} (hw : 2 ≤ w)
+    (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) :
+    decrypt t C =
+      ((decryptionPhase t C (0, ⟨w - 1, by omega⟩)).val.testBit (w - 1) ^^
+        (decryptionPhase t C (0, ⟨w - 1, by omega⟩)).val.testBit (w - 2)) := by
+  rw [decrypt_eq_decode_decryptionPhase (by omega), decode_eq_xor_highBits hw]
+
+end Cslib.Crypto.Homomorphic.GSW
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Gadget.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Gadget.lean
index 1d1d62c99..7c99c94fa 100644
--- a/Complexity/Crypto/Computational/Homomorphic/GSW/Gadget.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Gadget.lean
@@ -40,6 +40,8 @@ redundant; this module uses the minimal `w` digits. Width zero is allowed: its r
 * `decomposeMatrix_mulVec`: decomposition preserves multiplication by the expanded secret.
 * `flattenMatrix_mulVec`: flattening preserves that multiplication on arbitrary modular inputs.
 * `recomposeMatrix_flattenMatrix`: flattening preserves recomposition.
+* `recomposeMatrix_sub`, `recomposeMatrix_mul`: row recomposition commutes with subtraction
+  and left matrix multiplication, as used by serialized NAND.
 
 ## References
 
@@ -137,6 +139,21 @@ theorem recomposeMatrix_add (w : ℕ) (A B : Matrix ρ (ι × Fin w) (ZMod (2 ^
   funext i
   exact bitCompose_add w (A i) (B i)
 
+/-- Row recomposition preserves subtraction before the resulting residues are decomposed. -/
+theorem recomposeMatrix_sub (w : ℕ) (A B : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) :
+    recomposeMatrix w (A - B) = recomposeMatrix w A - recomposeMatrix w B := by
+  ext i j
+  simp [recomposeMatrix, bitCompose, sub_mul, Finset.sum_sub_distrib]
+
+/-- Recompose a matrix product by recomposing the right operand, retaining all modular counts. -/
+theorem recomposeMatrix_mul [Fintype κ] (w : ℕ)
+    (A : Matrix ρ κ (ZMod (2 ^ w))) (B : Matrix κ (ι × Fin w) (ZMod (2 ^ w))) :
+    recomposeMatrix w (A * B) = A * recomposeMatrix w B := by
+  ext i j
+  simp only [recomposeMatrix, bitCompose, Matrix.mul_apply,
+    Finset.sum_mul, Finset.mul_sum, mul_assoc]
+  rw [Finset.sum_comm]
+
 /-- Recomposition commutes with modular scalar multiplication. -/
 theorem recomposeMatrix_smul (w : ℕ) (a : ZMod (2 ^ w))
     (C : Matrix ρ (ι × Fin w) (ZMod (2 ^ w))) :
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean
new file mode 100644
index 000000000..658e1b64c
--- /dev/null
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean
@@ -0,0 +1,289 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption
+import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.Nat.Bits
+
+/-!
+# Total serialized GSW decryption and NAND
+
+The algorithms read the existing fixed-width, row-major words. Missing bits are `false` and
+excess bits are ignored. Arithmetic uses signed subtraction before reduction modulo `2 ^ w`;
+NAND retains integer matrix-product counts before decomposing the resulting residues.
+
+## Main definitions
+
+* `decryptResidue`, `decryptSerialized`: the selected modular row product and its scalar decoder.
+* `nandEntry`, `nandSerialized`: the actual modular NAND computation and complete output word.
+
+## Main results
+
+* `decryptSerialized_eq`, `nandSerialized_eq`: agreement with the typed operations on all words.
+* `length_nandSerialized`: the exact square ciphertext width on every input.
+* `decryptSerialized_nand`: correctness from the actual input error equations and bounds.
+* `keyGenSerialized_encrypt_correct`, `keyGenSerialized_nand_correct`: correctness for every
+  supported draw of the actual word-valued key generator and encryption programs.
+
+## References
+
+* [Gentry, Sahai and Waters, Sections 3.1 and 3.3][GentrySahaiWaters2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Homomorphic.GSW
+
+open Probability BitString
+open scoped BigOperators _root_.Matrix
+
+/-- The selected row multiplied by `(1,-secret)`, reduced only after signed subtraction. -/
+def decryptResidue (n w : ℕ) (secret ciphertext : List Bool) : ℕ :=
+  (((Cslib.Matrix.binaryEntry (n + 1) w ciphertext (w - 1) 0 : ℤ) -
+    (((List.range n).map fun j =>
+      Cslib.Matrix.binaryEntry (n + 1) w ciphertext (w - 1) (j + 1) *
+        Cslib.Matrix.binaryEntry n w secret 0 j).sum : ℕ)) % (2 ^ w : ℤ)).toNat
+
+/-- Decode the selected residue. Width zero returns `false`; every positive width uses the
+same half-open middle-half test as the typed decoder, including width one. -/
+def decryptSerialized (n w : ℕ) (secret ciphertext : List Bool) : Bool :=
+  if w = 0 then false else
+    let value := decryptResidue n w secret ciphertext
+    decide (2 ^ w ≤ 4 * value ∧ 4 * value < 3 * 2 ^ w)
+
+/-- One recomposed NAND entry: its gadget value minus the exact selected row product. -/
+def nandEntry (n w : ℕ) (left right : List Bool) (i k j : ℕ) : ℕ :=
+  ((((if i = j then 2 ^ k else 0 : ℕ) : ℤ) -
+    (((List.range ((n + 1) * w)).map fun r =>
+      if left.getD ((i * w + k) * ((n + 1) * w) + r) false then
+        Cslib.Matrix.binaryEntry (n + 1) w right r j else 0).sum : ℕ)) % (2 ^ w : ℤ)).toNat
+
+/-- Write all bits of `Flatten(I - left * right)` using the existing ciphertext order. -/
+def nandSerialized (n w : ℕ) (left right : List Bool) : List Bool :=
+  (List.range (n + 1)).flatMap fun i =>
+    (List.range w).flatMap fun k =>
+      (List.range (n + 1)).flatMap fun j => lowBits w (nandEntry n w left right i k j)
+
+/-- Raw ciphertext lookup agrees with its finite row/column view on every input word. -/
+theorem decodeCiphertext_apply (n w : ℕ) (word : List Bool)
+    (i j : Fin (n + 1)) (k l : Fin w) :
+    decodeCiphertext n w word (i, k) (j, l) =
+      word.getD ((i.val * w + k.val) * ((n + 1) * w) + j.val * w + l.val) false := by
+  simp only [decodeCiphertext, block, ofList, finProdFinEquiv, Equiv.coe_fn_mk]
+  congr 1
+  ring
+
+/-- A raw residue word is exactly the recomposition of the decoded ciphertext bits. -/
+theorem binaryEntry_eq_recompose_decodeCiphertext (n w : ℕ) (word : List Bool)
+    (i : Fin (n + 1)) (k : Fin w) (j : Fin (n + 1)) :
+    (Cslib.Matrix.binaryEntry (n + 1) w word (i.val * w + k.val) j.val : ZMod (2 ^ w)) =
+      recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (decodeCiphertext n w word)) (i, k) j := by
+  unfold Cslib.Matrix.binaryEntry
+  have hbound : (i.val * w + k.val) * (n + 1) + j.val < ((n + 1) * w) * (n + 1) := by
+    simpa [finProdFinEquiv, Nat.add_comm, Nat.mul_comm] using
+      (finProdFinEquiv (finProdFinEquiv (i, k), j)).isLt
+  rw [listRow_eq_ofFn w
+    (⟨(i.val * w + k.val) * (n + 1) + j.val, hbound⟩ : Fin (((n + 1) * w) * (n + 1)))]
+  rw [Nat.foldr_bit_ofFn, Nat.cast_sum]
+  apply Finset.sum_congr rfl
+  intro l hl
+  simp only [Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat, bitMatrix_apply,
+    decodeCiphertext_apply, block, ofList, finProdFinEquiv, Equiv.coe_fn_mk]
+  congr 4
+  ring
+
+/-- Signed word arithmetic returns exactly the selected modular phase of the decoded inputs. -/
+theorem decryptResidue_eq {n w : ℕ} (hw : 0 < w) (secret ciphertext : List Bool) :
+    decryptResidue n w secret ciphertext =
+      (decryptionPhase (decodeSecret n w secret) (decodeCiphertext n w ciphertext)
+        (0, ⟨w - 1, by omega⟩)).val := by
+  let value : ℤ := (Cslib.Matrix.binaryEntry (n + 1) w ciphertext (w - 1) 0 : ℤ) -
+    ((∑ j : Fin n, Cslib.Matrix.binaryEntry (n + 1) w ciphertext (w - 1) (j.val + 1) *
+      Cslib.Matrix.binaryEntry n w secret 0 j.val : ℕ) : ℤ)
+  have hcast : (value : ZMod (2 ^ w)) =
+      decryptionPhase (decodeSecret n w secret) (decodeCiphertext n w ciphertext)
+        (0, ⟨w - 1, by omega⟩) := by
+    simp only [value, Int.cast_sub, Int.cast_sum, Int.cast_mul, Int.cast_natCast,
+      Nat.cast_sum, Nat.cast_mul,
+      decryptionPhase, ← binaryEntry_eq_recompose_decodeCiphertext,
+      decodeSecret, Cslib.Matrix.ofBinary_apply, Fin.val_zero, Fin.val_succ,
+      Nat.zero_mul, Nat.zero_add]
+  unfold decryptResidue
+  rw [List.map_range_eq_ofFn, List.sum_ofFn]
+  change (value % (2 ^ w : ℤ)).toNat = _
+  rw [← hcast]
+  exact (congrArg Int.toNat (ZMod.val_intCast (n := 2 ^ w) value)).symm
+
+/-- The total word algorithm is the original decryption of the total decoded inputs. -/
+theorem decryptSerialized_eq (n w : ℕ) (secret ciphertext : List Bool) :
+    decryptSerialized n w secret ciphertext =
+      decrypt (decodeSecret n w secret) (decodeCiphertext n w ciphertext) := by
+  by_cases hw : w = 0
+  · subst w
+    simp [decryptSerialized]
+  · have hpos : 0 < w := by omega
+    rw [decrypt_eq_decode_decryptionPhase hpos]
+    simp only [decryptSerialized, hw, ↓reduceIte, decode, decryptResidue_eq hpos]
+
+/-- Canonical words decrypt exactly as their typed secret and ciphertext. -/
+@[simp] theorem decryptSerialized_serialize {n w : ℕ} (secret : Fin n → ZMod (2 ^ w))
+    (ciphertext : Ciphertext n w) :
+    decryptSerialized n w (serializeSecret secret) (serializeCiphertext ciphertext) =
+      decrypt secret ciphertext := by
+  rw [decryptSerialized_eq, decode_serializeSecret, decode_serializeCiphertext]
+
+private theorem nand_eq_decomposeMatrix {n w : ℕ} (left right : Ciphertext n w) :
+    nand left right = decomposeMatrix w
+      (gadgetMatrix n w - bitMatrix (ZMod (2 ^ w)) left *
+        recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) right)) := by
+  rw [nand, flattenMatrix, recomposeMatrix_sub, recomposeMatrix_mul]
+  rfl
+
+/-- A computed NAND word is the canonical residue of the typed row product. -/
+theorem nandEntry_eq (n w : ℕ) (left right : List Bool)
+    (i : Fin (n + 1)) (k : Fin w) (j : Fin (n + 1)) :
+    nandEntry n w left right i.val k.val j.val =
+      ((gadgetMatrix n w - bitMatrix (ZMod (2 ^ w)) (decodeCiphertext n w left) *
+        recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (decodeCiphertext n w right)))
+          (i, k) j).val := by
+  let value : ℤ := ((if i.val = j.val then 2 ^ k.val else 0 : ℕ) : ℤ) -
+    ((∑ r : Fin ((n + 1) * w),
+      if left.getD ((i.val * w + k.val) * ((n + 1) * w) + r.val) false then
+        Cslib.Matrix.binaryEntry (n + 1) w right r.val j.val else 0 : ℕ) : ℤ)
+  have hcast : (value : ZMod (2 ^ w)) =
+      (gadgetMatrix n w - bitMatrix (ZMod (2 ^ w)) (decodeCiphertext n w left) *
+        recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (decodeCiphertext n w right)))
+          (i, k) j := by
+    simp only [value, Int.cast_sub, Int.cast_sum, Int.cast_natCast, Nat.cast_sum,
+      _root_.Matrix.sub_apply, _root_.Matrix.mul_apply, gadgetMatrix_apply]
+    congr 1
+    · by_cases h : i = j
+      · simp [h]
+      · have hv : i.val ≠ j.val := fun hij => h (Fin.ext hij)
+        simp [h, hv]
+    · rw [← (finProdFinEquiv : Fin (n + 1) × Fin w ≃ Fin ((n + 1) * w)).sum_comp]
+      apply Finset.sum_congr rfl
+      rintro ⟨r, l⟩ hr
+      rw [bitMatrix_apply, decodeCiphertext_apply,
+        ← binaryEntry_eq_recompose_decodeCiphertext]
+      simp only [finProdFinEquiv, Equiv.coe_fn_mk, Nat.add_assoc, Nat.mul_comm,
+        Nat.add_comm]
+      split_ifs with h <;> simp_all
+  unfold nandEntry
+  rw [List.map_range_eq_ofFn, List.sum_ofFn]
+  change (value % (2 ^ w : ℤ)).toNat = _
+  rw [← hcast]
+  exact (congrArg Int.toNat (ZMod.val_intCast (n := 2 ^ w) value)).symm
+
+/-- The actual NAND program agrees with the typed operation for every pair of raw words. -/
+theorem nandSerialized_eq (n w : ℕ) (left right : List Bool) :
+    nandSerialized n w left right = serializeCiphertext
+      (nand (decodeCiphertext n w left) (decodeCiphertext n w right)) := by
+  rw [nand_eq_decomposeMatrix]
+  simp only [nandSerialized, serializeCiphertext, List.flatMap_def,
+    List.map_range_eq_ofFn, lowBits_eq_ofFn, ofFn_blocksEquiv_symm,
+    nandEntry_eq, decomposeMatrix, bitDecomp]
+
+/-- Decoding a raw NAND result recovers the typed operation on the decoded inputs. -/
+@[simp] theorem decode_nandSerialized (n w : ℕ) (left right : List Bool) :
+    decodeCiphertext n w (nandSerialized n w left right) =
+      nand (decodeCiphertext n w left) (decodeCiphertext n w right) := by
+  rw [nandSerialized_eq, decode_serializeCiphertext]
+
+/-- Canonical input words produce the canonical word of their actual typed NAND. -/
+@[simp] theorem nandSerialized_serialize {n w : ℕ} (left right : Ciphertext n w) :
+    nandSerialized n w (serializeCiphertext left) (serializeCiphertext right) =
+      serializeCiphertext (nand left right) := by
+  rw [nandSerialized_eq, decode_serializeCiphertext, decode_serializeCiphertext]
+
+/-- Every raw pair produces the complete declared ciphertext word. -/
+@[simp] theorem length_nandSerialized (n w : ℕ) (left right : List Bool) :
+    (nandSerialized n w left right).length = ((n + 1) * w) ^ 2 := by
+  simp [nandSerialized, List.length_flatMap, pow_two, Nat.mul_assoc]
+
+/-- The actual serialized NAND retains the exact propagated integer error equation. -/
+theorem nandSerialized_hasError {n w : ℕ} (secret left right : List Bool) (μ₁ μ₂ : Bool)
+    (error₁ error₂ : Fin (n + 1) × Fin w → ℤ)
+    (hleft : HasError (decodeSecret n w secret) (decodeCiphertext n w left) μ₁ error₁)
+    (hright : HasError (decodeSecret n w secret) (decodeCiphertext n w right) μ₂ error₂) :
+    HasError (decodeSecret n w secret) (decodeCiphertext n w (nandSerialized n w left right))
+      (!(μ₁ && μ₂)) (nandError (decodeCiphertext n w left) μ₂ error₁ error₂) := by
+  rw [decode_nandSerialized]
+  exact nand_hasError _ _ _ _ _ _ _ hleft hright
+
+/-- Any raw ciphertext satisfying the modular equation decrypts under the original strict
+noise margin. The ciphertext may be an output of previous homomorphic operations. -/
+theorem decryptSerialized_eq_of_hasError {n w : ℕ} (hw : 0 < w)
+    (secret ciphertext : List Bool) (μ : Bool) (error : Fin (n + 1) × Fin w → ℤ)
+    (hC : HasError (decodeSecret n w secret) (decodeCiphertext n w ciphertext) μ error)
+    (herror : ∀ i, 4 * (error i).natAbs < 2 ^ w) :
+    decryptSerialized n w secret ciphertext = μ := by
+  rw [decryptSerialized_eq]
+  exact decrypt_eq_of_hasError hw _ _ _ _ hC herror
+
+/-- Canonical actual encryption words decrypt under exactly the typed fresh-noise hypotheses. -/
+theorem decryptSerialized_encryptWithCoins {n m w bound : ℕ}
+    (B : _root_.Matrix (Fin m) (Fin n) (ZMod (2 ^ w))) (secret : Fin n → ZMod (2 ^ w))
+    (error : Fin m → ℤ) (μ : Bool) (coins : _root_.Matrix (Fin (n + 1) × Fin w) (Fin m) Bool)
+    (hw : 0 < w) (herror : ∀ j, (error j).natAbs ≤ bound)
+    (hmargin : 4 * (m * bound) < 2 ^ w) :
+    decryptSerialized n w (serializeSecret secret)
+      (encryptWithCoinsSerialized n m w (serializePublicMatrix (publicMatrix B secret error))
+        μ (serializeCoins coins)) = μ := by
+  rw [encryptWithCoinsSerialized_serialize, decryptSerialized_serialize]
+  exact decrypt_encryptWithCoins B secret error μ coins hw herror hmargin
+
+/-- NAND on arbitrary raw ciphertext words is correct under the original propagated-noise
+margin. No freshness, support, or canonical-length premise is added. -/
+theorem decryptSerialized_nand {n w bound₁ bound₂ : ℕ}
+    (secret left right : List Bool) (μ₁ μ₂ : Bool)
+    (error₁ error₂ : Fin (n + 1) × Fin w → ℤ)
+    (hleft : HasError (decodeSecret n w secret) (decodeCiphertext n w left) μ₁ error₁)
+    (hright : HasError (decodeSecret n w secret) (decodeCiphertext n w right) μ₂ error₂)
+    (hw : 0 < w)
+    (herror₁ : ∀ i, (error₁ i).natAbs ≤ bound₁)
+    (herror₂ : ∀ i, (error₂ i).natAbs ≤ bound₂)
+    (hmargin : 4 * (bound₁ + ((n + 1) * w) * bound₂) < 2 ^ w) :
+    decryptSerialized n w secret (nandSerialized n w left right) = !(μ₁ && μ₂) := by
+  rw [decryptSerialized_eq, decode_nandSerialized]
+  exact decrypt_nand _ _ _ _ _ _ _ hleft hright hw herror₁ herror₂ hmargin
+
+/-- Every supported actual key and encryption word is correct under the existing fresh margin. -/
+theorem keyGenSerialized_encrypt_correct {n m w η : ℕ} (hw : 0 < w)
+    (hmargin : 4 * (m * η) < 2 ^ w) {keys : List Bool × List Bool}
+    (hkeys : keys ∈ (ProbComp.eval (keyGenSerialized n m w η)).support) (μ : Bool)
+    {ciphertext : List Bool}
+    (hciphertext : ciphertext ∈ (ProbComp.eval (encryptSerialized n m w keys.1 μ)).support) :
+    decryptSerialized n w keys.2 ciphertext = μ := by
+  rw [eval_keyGenSerialized, PMF.mem_support_map_iff] at hkeys
+  obtain ⟨typedKeys, htypedKeys, rfl⟩ := hkeys
+  rw [eval_encryptSerialized_serializePublicMatrix, PMF.mem_support_map_iff] at hciphertext
+  obtain ⟨typedCiphertext, htypedCiphertext, rfl⟩ := hciphertext
+  rw [decryptSerialized_serialize]
+  exact keyGen_encrypt_correct hw hmargin htypedKeys μ htypedCiphertext
+
+/-- Every pair of supported fresh actual encryption words has a correct actual NAND under the
+same strict fresh-NAND margin as the typed sampler theorem. -/
+theorem keyGenSerialized_nand_correct {n m w η : ℕ} (hw : 0 < w)
+    (hmargin : 4 * ((1 + (n + 1) * w) * (m * η)) < 2 ^ w) {keys : List Bool × List Bool}
+    (hkeys : keys ∈ (ProbComp.eval (keyGenSerialized n m w η)).support) (μ₁ μ₂ : Bool)
+    {left right : List Bool}
+    (hleft : left ∈ (ProbComp.eval (encryptSerialized n m w keys.1 μ₁)).support)
+    (hright : right ∈ (ProbComp.eval (encryptSerialized n m w keys.1 μ₂)).support) :
+    decryptSerialized n w keys.2 (nandSerialized n w left right) = !(μ₁ && μ₂) := by
+  rw [eval_keyGenSerialized, PMF.mem_support_map_iff] at hkeys
+  obtain ⟨typedKeys, htypedKeys, rfl⟩ := hkeys
+  rw [eval_encryptSerialized_serializePublicMatrix, PMF.mem_support_map_iff] at hleft hright
+  obtain ⟨typedLeft, htypedLeft, rfl⟩ := hleft
+  obtain ⟨typedRight, htypedRight, rfl⟩ := hright
+  rw [nandSerialized_serialize, decryptSerialized_serialize]
+  exact keyGen_nand_correct hw hmargin htypedKeys μ₁ μ₂ htypedLeft htypedRight
+
+end Cslib.Crypto.Homomorphic.GSW
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation/PolyTime.lean
new file mode 100644
index 000000000..d494201aa
--- /dev/null
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation/PolyTime.lean
@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Evaluation
+public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.PolyTime
+
+/-!
+# Uniform native GSW decryption and NAND
+
+The actual serialized operations have uniform native polynomial-time certificates. Dimensions
+and loop indices are unary; modular values and signed differences are binary. Complete input
+words, intermediate sums and all output bits are charged. The certificates apply to arbitrary
+raw words, without shape, noise, support or security assumptions.
+
+## Main results
+
+* `computableTidilyInPolyTime_decryptSerialized`: the actual total raw-word decryption test.
+* `computableTidilyInPolyTime_nandSerialized`: the complete actual NAND ciphertext computation.
+
+## References
+
+* [Gentry, Sahai and Waters, Sections 3.1 and 3.3][GentrySahaiWaters2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Crypto.Homomorphic.GSW
+
+open Turing.MultiTapeTM Turing.MultiTapeTM.ComputableTidilyInPolyTime
+
+variable {α : Type} {input : α ↪ List Bool} {n w i k j : α → ℕ}
+
+/-- Compute the selected phase uniformly from every pair of raw secret and ciphertext words. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_decryptResidue {secret ciphertext : α → List Bool}
+    (hn : ComputableTidilyInPolyTime n input encUnary)
+    (hw : ComputableTidilyInPolyTime w input encUnary)
+    (hsecret : ComputableTidilyInPolyTime secret input encBits)
+    (hciphertext : ComputableTidilyInPolyTime ciphertext input encBits) :
+    ComputableTidilyInPolyTime
+      (fun a => decryptResidue (n a) (w a) (secret a) (ciphertext a)) input encNat := by
+  have hterm : ComputableTidilyInPolyTime
+      (fun p : α × ℕ => Matrix.binaryEntry (n p.1 + 1) (w p.1) (ciphertext p.1)
+        (w p.1 - 1) (p.2 + 1) * Matrix.binaryEntry (n p.1) (w p.1) (secret p.1) 0 p.2)
+      (encPair input encUnary) encNat := by
+    apply binary_mul'
+    · exact matrixBinaryEntry (by fun_prop) (by fun_prop) (by fun_prop)
+        (by fun_prop) (by fun_prop)
+    · exact matrixBinaryEntry (by fun_prop) (by fun_prop) (by fun_prop)
+        (const 0) (snd input encUnary)
+  have hsum := binary_sum.comp (mapWithInput
+    (f := fun a j => Matrix.binaryEntry (n a + 1) (w a) (ciphertext a) (w a - 1) (j + 1) *
+      Matrix.binaryEntry (n a) (w a) (secret a) 0 j) (range.comp hn) hterm)
+  have hfirst := matrixBinaryEntry (by fun_prop) hw hciphertext (by fun_prop) (const 0)
+    (cols := fun a => n a + 1) (row := fun a => w a - 1)
+  unfold decryptResidue
+  simpa only [Function.comp_apply, Nat.cast_pow, Nat.cast_ofNat] using
+    intBin_emodNat' (intBin_sub' (intBin_natCast.comp hfirst) (intBin_natCast.comp hsum))
+      (binary_pow' (const 2) hw)
+
+/-- The total decoder is polynomial-time on the complete inputs, including malformed words. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_decryptSerialized {secret ciphertext : α → List Bool}
+    (hn : ComputableTidilyInPolyTime n input encUnary)
+    (hw : ComputableTidilyInPolyTime w input encUnary)
+    (hsecret : ComputableTidilyInPolyTime secret input encBits)
+    (hciphertext : ComputableTidilyInPolyTime ciphertext input encBits) :
+    ComputableTidilyInPolyTime
+      (fun a => decryptSerialized (n a) (w a) (secret a) (ciphertext a)) input encBool := by
+  have hvalue := computableTidilyInPolyTime_decryptResidue hn hw hsecret hciphertext
+  have hq := binary_pow' (const 2) hw
+  have hfour := binary_mul' (const 4) hvalue
+  have htest : ComputableTidilyInPolyTime
+      (fun a => decide (2 ^ w a ≤ 4 * decryptResidue (n a) (w a) (secret a) (ciphertext a) ∧
+        4 * decryptResidue (n a) (w a) (secret a) (ciphertext a) < 3 * 2 ^ w a))
+      input encBool :=
+    decide_and (binary_le' hq hfour) (binary_lt' hfour (binary_mul' (const 3) hq))
+  simpa only [decryptSerialized, beq_iff_eq] using
+    (unary_beq hw (const 0)).ite' (const false) htest
+
+/-- Compute one actual NAND residue, keeping the complete binary sum before signed reduction. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_nandEntry {left right : α → List Bool}
+    (hn : ComputableTidilyInPolyTime n input encUnary)
+    (hw : ComputableTidilyInPolyTime w input encUnary)
+    (hleft : ComputableTidilyInPolyTime left input encBits)
+    (hright : ComputableTidilyInPolyTime right input encBits)
+    (hi : ComputableTidilyInPolyTime i input encUnary)
+    (hk : ComputableTidilyInPolyTime k input encUnary)
+    (hj : ComputableTidilyInPolyTime j input encUnary) :
+    ComputableTidilyInPolyTime
+      (fun a => nandEntry (n a) (w a) (left a) (right a) (i a) (k a) (j a)) input encNat := by
+  have hterm : ComputableTidilyInPolyTime
+      (fun p : α × ℕ =>
+        if (left p.1).getD ((i p.1 * w p.1 + k p.1) * ((n p.1 + 1) * w p.1) + p.2) false
+        then Matrix.binaryEntry (n p.1 + 1) (w p.1) (right p.1) p.2 (j p.1) else 0)
+      (encPair input encUnary) encNat := by
+    apply ((bitsGetD false).comp ((hleft.comp (fst input encUnary)).prod (by fun_prop))).ite'
+    · exact matrixBinaryEntry (by fun_prop) (by fun_prop) (by fun_prop)
+        (snd input encUnary) (by fun_prop)
+    · exact const 0
+  have hsum := binary_sum.comp (mapWithInput
+    (f := fun a r => if (left a).getD ((i a * w a + k a) * ((n a + 1) * w a) + r) false
+      then Matrix.binaryEntry (n a + 1) (w a) (right a) r (j a) else 0)
+    (range.comp (show ComputableTidilyInPolyTime (fun a => (n a + 1) * w a)
+      input encUnary by fun_prop)) hterm)
+  have hgadget : ComputableTidilyInPolyTime
+      (fun a => if i a = j a then 2 ^ k a else 0) input encNat := by
+    simpa only [beq_iff_eq] using
+      (unary_beq hi hj).ite' (binary_pow' (const 2) hk) (const 0)
+  unfold nandEntry
+  simpa only [Function.comp_apply, Nat.cast_pow, Nat.cast_ofNat] using
+    intBin_emodNat' (intBin_sub' (intBin_natCast.comp hgadget) (intBin_natCast.comp hsum))
+      (binary_pow' (const 2) hw)
+
+/-- Compute the full square ciphertext with a single uniform native polynomial clock. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_nandSerialized {left right : α → List Bool}
+    (hn : ComputableTidilyInPolyTime n input encUnary)
+    (hw : ComputableTidilyInPolyTime w input encUnary)
+    (hleft : ComputableTidilyInPolyTime left input encBits)
+    (hright : ComputableTidilyInPolyTime right input encBits) :
+    ComputableTidilyInPolyTime
+      (fun a => nandSerialized (n a) (w a) (left a) (right a)) input encBits := by
+  unfold nandSerialized
+  apply flatMapToBitsWithInput (range.comp (by fun_prop))
+  apply flatMapToBitsWithInput (range.comp (by fun_prop))
+  apply flatMapToBitsWithInput (range.comp (by fun_prop))
+  fun_prop
+
+end Cslib.Crypto.Homomorphic.GSW
diff --git a/Complexity/Foundations/Data/Nat/Bits.lean b/Complexity/Foundations/Data/Nat/Bits.lean
index d61c5b7bc..8b3a2e42f 100644
--- a/Complexity/Foundations/Data/Nat/Bits.lean
+++ b/Complexity/Foundations/Data/Nat/Bits.lean
@@ -8,7 +8,9 @@ module
 -- upstream: candidate (Mathlib, `Mathlib/Data/Nat/Bits.lean`)
 
 public import Complexity.Init
+public import Mathlib.Algebra.BigOperators.Fin
 public import Mathlib.Data.Nat.Bits
+import Mathlib.Data.List.OfFn
 import Mathlib.Data.Nat.Size
 
 /-!
@@ -21,10 +23,24 @@ with initial value zero reconstructs the original number.
 
 * `Nat.foldr_bit_bits`: folding `Nat.bit` over the binary representation of `n` gives `n`.
 * `Nat.foldr_bit_lt`, `Nat.foldr_bit_testBit`: fixed-width little-endian reconstruction.
+* `Nat.foldr_bit_ofFn`: reconstruction is the sum of the digits' binary place values.
 -/
 
 @[expose] public section
 
+open scoped BigOperators
+
+/-- Reconstructing a finite little-endian word sums the digits' binary place values. -/
+theorem Nat.foldr_bit_ofFn {w : ℕ} (bits : Fin w → Bool) :
+    (List.ofFn bits).foldr Nat.bit 0 = ∑ k : Fin w, (bits k).toNat * 2 ^ k.val := by
+  induction w with
+  | zero => simp
+  | succ w ih =>
+    rw [List.ofFn_succ, List.foldr_cons, ih]
+    simp only [Fin.sum_univ_succ, Fin.val_zero, pow_zero, mul_one, Fin.val_succ,
+      pow_succ, Nat.bit_val, ← Nat.mul_assoc, ← Finset.sum_mul]
+    omega
+
 /-- Folding `Nat.bit` over the binary representation of `n` gives back `n`. -/
 @[simp]
 theorem Nat.foldr_bit_bits (n : ℕ) : n.bits.foldr Nat.bit 0 = n := by
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index fcc5f3bf5..7b748a683 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -117,6 +117,8 @@ import ComplexityTests.Crypto.Encryption
 import ComplexityTests.Crypto.FixedKeySecurity
 import ComplexityTests.Crypto.GMWPointwise
 import ComplexityTests.Crypto.GSW
+import ComplexityTests.Crypto.GSWDecryption
+import ComplexityTests.Crypto.GSWEvaluation
 import ComplexityTests.Crypto.GSWHiding
 import ComplexityTests.Crypto.GSWNative
 import ComplexityTests.Crypto.GSWParameters
diff --git a/ComplexityTests/Crypto/GSWDecryption.lean b/ComplexityTests/Crypto/GSWDecryption.lean
new file mode 100644
index 000000000..759538026
--- /dev/null
+++ b/ComplexityTests/Crypto/GSWDecryption.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption
+import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized
+
+/-!
+Raw GSW decryption regressions. The ciphertext rows below are chosen directly, without a key
+generator, encryption coins or noise witness. Boundary residues check the decoder's half-open
+convention; negative inner products check modular wraparound. These tests do not assert a
+shallow circuit or bootstrappability.
+-/
+
+namespace ComplexityTests.GSWDecryption
+
+open Cslib.Crypto.Homomorphic.GSW
+
+private def rawCiphertext (w : ℕ) (a b : ZMod (2 ^ w)) : Ciphertext 1 w :=
+  fun _ j => (if j.1 = 0 then a else b).val.testBit j.2.val
+
+-- The selected row's recomposed entries are the chosen a,b, so its phase is a-b*t.
+example : ([0, 1, 2, 3, 4, 5, 6, 7] : List (ZMod (2 ^ 3))).map
+    (fun a => (decryptionPhase (fun _ => 0) (rawCiphertext 3 a 0) (0, 2)).val) =
+      [0, 1, 2, 3, 4, 5, 6, 7] := by
+  decide +kernel
+
+example : ([0, 1, 2, 3, 4, 5, 6, 7] : List (ZMod (2 ^ 3))).map
+    (fun a => decrypt (fun _ => 0) (rawCiphertext 3 a 0)) =
+      [false, false, true, true, true, true, false, false] := by
+  decide +kernel
+
+-- The raw signed products -1 and -5 wrap to 7 and 3 modulo 8.
+example : ([1, 5] : List (ZMod (2 ^ 3))).map
+    (fun b => ((decryptionPhase (fun _ => 1) (rawCiphertext 3 0 b) (0, 2)).val,
+      decrypt (fun _ => 1) (rawCiphertext 3 0 b))) = [(7, false), (3, true)] := by
+  decide +kernel
+
+example : ([0, 1] : List (ZMod (2 ^ 1))).map
+    (fun a => decrypt (fun _ => 0) (rawCiphertext 1 a 0)) = [false, true] := by
+  decide +kernel
+
+example : decrypt (fun _ => 0) (rawCiphertext 0 0 0) = false := by
+  decide +kernel
+
+-- The row identity applies after separate total decoding of arbitrary input words.
+example (n w : ℕ) (hw : 0 < w) (secret ciphertext : List Bool) :
+    decrypt (decodeSecret n w secret) (decodeCiphertext n w ciphertext) =
+      decode w (decryptionPhase (decodeSecret n w secret)
+        (decodeCiphertext n w ciphertext) (0, ⟨w - 1, by omega⟩)) :=
+  decrypt_eq_decode_decryptionPhase hw _ _
+
+-- At the lower boundary the two top bits differ; at the upper boundary they agree.
+example : ((2 : ZMod (2 ^ 3)).val.testBit 2 ^^ (2 : ZMod (2 ^ 3)).val.testBit 1) = true ∧
+    ((6 : ZMod (2 ^ 3)).val.testBit 2 ^^ (6 : ZMod (2 ^ 3)).val.testBit 1) = false := by
+  decide +kernel
+
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.decode_eq_xor_highBits' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms decode_eq_xor_highBits
+
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.decryptionPhase_eq_mulVec' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms decryptionPhase_eq_mulVec
+
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.decrypt_eq_xor_highBits' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms decrypt_eq_xor_highBits
+
+end ComplexityTests.GSWDecryption
diff --git a/ComplexityTests/Crypto/GSWEvaluation.lean b/ComplexityTests/Crypto/GSWEvaluation.lean
new file mode 100644
index 000000000..45ee51fdf
--- /dev/null
+++ b/ComplexityTests/Crypto/GSWEvaluation.lean
@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Evaluation.PolyTime
+
+/-!
+The actual word algorithms are tested on malformed inputs, small widths, signed wraparound,
+integer carries and asymmetric matrix products. A positive-noise supported fixture exercises
+both plaintexts, and a growing-input client composes key generation, encryption, NAND and
+decryption through their native certificates. No security or bootstrappability is assumed.
+-/
+
+namespace ComplexityTests.GSWEvaluation
+
+open Cslib Cslib.Probability Cslib.Crypto.Homomorphic.GSW
+open Turing.MultiTapeTM
+
+example (n : ℕ) (secret ciphertext left right : List Bool) :
+    decryptSerialized n 0 secret ciphertext = false ∧ nandSerialized n 0 left right = [] := by
+  constructor
+  · simp [decryptSerialized]
+  · apply List.eq_nil_of_length_eq_zero
+    simp
+
+-- Width one is not the width-zero convention: either plaintext can be recovered.
+example : decryptSerialized 0 1 [] [true] = true ∧
+    decryptSerialized 0 1 [] [] = false := by decide +kernel
+
+private def phaseWord (value : ℕ) : List Bool := List.replicate 6 false ++ BitString.lowBits 3 value
+
+-- Both half-open endpoints are tested through the actual raw-word program.
+example : decryptSerialized 0 3 [] (phaseWord 1) = false ∧
+    decryptSerialized 0 3 [] (phaseWord 2) = true ∧
+    decryptSerialized 0 3 [] (phaseWord 5) = true ∧
+    decryptSerialized 0 3 [] (phaseWord 6) = false := by decide +kernel
+
+-- The selected row is [0,2], secret is 1: signed subtraction gives -2 mod4 = 2.
+private def negativePhase : List Bool := [false, false, false, false, false, false, false, true]
+
+example : decryptResidue 1 2 [true] negativePhase = 2 ∧
+    decryptSerialized 1 2 [true] negativePhase = true := by decide +kernel
+
+-- Missing secret/ciphertext bits are zero; bits beyond the declared widths are ignored.
+example : decryptSerialized 1 2 [true] negativePhase =
+      decryptSerialized 1 2 [true, false] (negativePhase ++ List.replicate 8 false) ∧
+    decryptSerialized 1 2 [true, false, true, true]
+      (negativePhase ++ List.replicate 8 false ++ [true, true]) = true := by decide +kernel
+
+private def leftWord : List Bool := [true, true, false, false]
+private def rightWord : List Bool := [true, false, true, false]
+
+-- The forward product contains a count of 2. The reverse product is different; both have
+-- negative entries before modular reduction, so parity or truncated subtraction is detected.
+example : nandSerialized 0 2 leftWord rightWord = [true, true, false, true] ∧
+    nandSerialized 0 2 rightWord leftWord = [false, true, true, true] := by decide +kernel
+
+-- Off-diagonal gadget zero minus one must wrap to 3, not truncate to zero.
+example : nandEntry 1 2 [true] [false, false, true] 0 0 1 = 3 := by decide +kernel
+
+example : nandSerialized 0 2 [true] [true] = [false, false, false, true] ∧
+    nandSerialized 0 2 (leftWord ++ [true, false, true]) (rightWord ++ [true, true]) =
+      nandSerialized 0 2 leftWord rightWord := by decide +kernel
+
+example (n w : ℕ) (left right : List Bool) :
+    (nandSerialized n w left right).length = ((n + 1) * w) ^ 2 :=
+  length_nandSerialized n w left right
+
+-- All-word semantic bridges carry no shape, support, or noise premise.
+example (n w : ℕ) (secret ciphertext : List Bool) :
+    decryptSerialized n w secret ciphertext =
+      decrypt (decodeSecret n w secret) (decodeCiphertext n w ciphertext) :=
+  decryptSerialized_eq n w secret ciphertext
+
+example (n w : ℕ) (left right : List Bool) :
+    nandSerialized n w left right =
+      serializeCiphertext (nand (decodeCiphertext n w left) (decodeCiphertext n w right)) :=
+  nandSerialized_eq n w left right
+
+private def keyInputs : KeyInputs 1 1 6 :=
+  ⟨fun _ => 5, fun _ _ => 3, fun _ => 1⟩
+
+private def typedKeys :=
+  (publicMatrix keyInputs.publicPart keyInputs.secret keyInputs.error, keyInputs.secret)
+
+private def wordKeys : List Bool × List Bool :=
+  (serializePublicMatrix typedKeys.1, serializeSecret typedKeys.2)
+
+private def coins : _root_.Matrix (Fin 2 × Fin 6) (Fin 1) Bool := fun _ _ => true
+
+private def wordCipher (message : Bool) : List Bool :=
+  encryptWithCoinsSerialized 1 1 6 wordKeys.1 message (serializeCoins coins)
+
+private theorem keys_supported :
+    wordKeys ∈ (ProbComp.eval (keyGenSerialized 1 1 6 1)).support := by
+  rw [eval_keyGenSerialized, PMF.mem_support_map_iff]
+  refine ⟨typedKeys, ?_, rfl⟩
+  simp only [keyGen, ProbComp.eval_bind, ProbComp.eval_pure, PMF.mem_support_bind_iff,
+    PMF.mem_support_pure_iff]
+  refine ⟨keyInputs, ?_, rfl⟩
+  rw [mem_support_sampleKeyInputs_iff]
+  decide +kernel
+
+private theorem cipher_supported (message : Bool) :
+    wordCipher message ∈ (ProbComp.eval (encryptSerialized 1 1 6 wordKeys.1 message)).support := by
+  rw [show wordKeys.1 = serializePublicMatrix typedKeys.1 from rfl,
+    eval_encryptSerialized_serializePublicMatrix, PMF.mem_support_map_iff]
+  refine ⟨encryptWithCoins typedKeys.1 message coins, ?_, ?_⟩
+  · exact (mem_support_encrypt_iff _ _ _).mpr ⟨coins, rfl⟩
+  · exact (encryptWithCoinsSerialized_serialize typedKeys.1 message coins).symm
+
+example (message : Bool) : decryptSerialized 1 6 wordKeys.2 (wordCipher message) = message :=
+  keyGenSerialized_encrypt_correct (by decide) (by decide) keys_supported message
+    (cipher_supported message)
+
+example (left right : Bool) :
+    decryptSerialized 1 6 wordKeys.2 (nandSerialized 1 6 (wordCipher left) (wordCipher right)) =
+      !(left && right) :=
+  keyGenSerialized_nand_correct (by decide) (by decide) keys_supported left right
+    (cipher_supported left) (cipher_supported right)
+
+-- Both dimensions and both entire raw words vary with the input.
+example : ComputableTidilyInPolyTime
+    (fun p : ℕ × ℕ × List Bool × List Bool => decryptSerialized p.1 p.2.1 p.2.2.1 p.2.2.2)
+    (encPair encUnary (encPair encUnary (encPair encBits encBits))) encBool := by fun_prop
+
+example : ComputableTidilyInPolyTime
+    (fun p : ℕ × ℕ × List Bool × List Bool => nandSerialized p.1 p.2.1 p.2.2.1 p.2.2.2)
+    (encPair encUnary (encPair encUnary (encPair encBits encBits))) encBits := by fun_prop
+
+private noncomputable def completeClient (p : ℕ × ℕ × ℕ × ℕ × Bool × Bool) : ProbComp Bool := do
+  let keys ← keyGenSerialized p.1 p.2.1 p.2.2.1 p.2.2.2.1
+  let left ← encryptSerialized p.1 p.2.1 p.2.2.1 keys.1 p.2.2.2.2.1
+  let right ← encryptSerialized p.1 p.2.1 p.2.2.1 keys.1 p.2.2.2.2.2
+  return decryptSerialized p.1 p.2.2.1 keys.2 (nandSerialized p.1 p.2.2.1 left right)
+
+example : IsPPTOn
+    (encPair encUnary (encPair encUnary (encPair encUnary
+      (encPair encUnary (encPair encBool encBool))))) encBool completeClient := by
+  unfold completeClient
+  ppt
+
+end ComplexityTests.GSWEvaluation
+
+open Cslib.Crypto.Homomorphic.GSW
+
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.decryptSerialized_eq' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in
+#print axioms decryptSerialized_eq
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.nandSerialized_eq' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in
+#print axioms nandSerialized_eq
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.keyGenSerialized_nand_correct' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in
+#print axioms keyGenSerialized_nand_correct
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_decryptSerialized' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms computableTidilyInPolyTime_decryptSerialized
+/--
+info: 'Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_nandSerialized' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms computableTidilyInPolyTime_nandSerialized
diff --git a/ROADMAP.md b/ROADMAP.md
index 8fa66dcb0..4e752933e 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -223,6 +223,15 @@ existing developments, source credit and saved branches remain available for a f
    `m*(n+1)*w` and `n*w`, and all `N^2` ciphertext bits.
    [Runtime tests](ComplexityTests/Crypto/GSWNative.lean) cover signed wraparound, ragged and
    truncated inputs, zero dimensions, bit order and growing-parameter clients.
+   [Serialized decryption and NAND](Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean)
+   agree with the typed operations on every raw word, padding missing bits with zero and ignoring
+   excess bits. NAND retains modular integer counts and produces exactly `N^2` bits. Their
+   [native certificates](Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation/PolyTime.lean)
+   charge the full inputs and output with uniformly varying unary dimensions and binary arithmetic.
+   Correctness transports the existing strict noise margins, including every supported actual
+   key and encryption draw. [Regressions](ComplexityTests/Crypto/GSWEvaluation.lean) check small
+   widths, negative wraparound, asymmetric NAND products, positive noise and a native client
+   composing key generation, encryption, NAND and decryption.
    The [statistical hiding theorem](Complexity/Crypto/Computational/Homomorphic/GSW/Hiding.lean)
    proves the uniform-public-matrix step of their security argument. For `d = n + 1` and
    `N = d * w`, the actual ciphertext gives any randomized two-stage adversary acceptance
@@ -252,11 +261,10 @@ existing developments, source credit and saved branches remain available for a f
    spells out both algorithms, their native efficiency and this precise conditional security
    result. It remains outside the curated headline catalogue while the full FHE recovery is open.
    Hardness for the specified noise family is assumed; no worst-case lattice reduction is supplied.
-   Native decryption/NAND/evaluation certificates, bootstrappability with compatible parameters
-   and the concrete FHE instantiation remain open in #486. This parameter family proves fresh
-   and one-NAND correctness; it does not yet supply the augmented-decryption circuit or the
-   separate joint circular-security assumption needed
-   for the fixed-key endpoint.
+   Full native circuit evaluation, shallow decryption circuits, bootstrappability with compatible
+   parameters and the concrete FHE instantiation remain open in #486. This parameter family
+   proves fresh and one-NAND correctness; it does not yet supply the augmented-decryption circuit
+   or the separate joint circular-security assumption needed for the fixed-key endpoint.
    The [code-composition API](Complexity/Computability/Circuit/Boolean/CodeComposition.lean)
    provides a native polynomial-time constructor for shared-input blocks with different gate
    counts, checked against the existing carry-save circuit without padding. This supports the