feat(crypto): certify native GSW decryption and NAND

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

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 : ℤ)

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

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))) :