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

def Cslib.Crypto.Homomorphic.GSW.decryptResidue (n w : ℕ) (secret ciphertext : List Bool) : ℕ

The selected row multiplied by (1,-secret), reduced only after signed subtraction.

def Cslib.Crypto.Homomorphic.GSW.decryptSerialized (n w : ℕ) (secret ciphertext : List Bool) : Bool

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 Cslib.Crypto.Homomorphic.GSW.nandEntry (n w : ℕ) (left right : List Bool) (i k j : ℕ) : ℕ

One recomposed NAND entry: its gadget value minus the exact selected row product.

def Cslib.Crypto.Homomorphic.GSW.nandSerialized (n w : ℕ) (left right : List Bool) : List Bool

Write all bits of Flatten(I - left * right) using the existing ciphertext order.

theorem Cslib.Crypto.Homomorphic.GSW.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 * w + ↑k) * ((n + 1) * w) + ↑j * w + ↑l) false

Raw ciphertext lookup agrees with its finite row/column view on every input word.

theorem Cslib.Crypto.Homomorphic.GSW.binaryEntry_eq_recompose_decodeCiphertext (n w : ℕ) (word : List Bool) (i : Fin (n + 1)) (k : Fin w) (j : Fin (n + 1)) : ↑(Matrix.binaryEntry (n + 1) w word (↑i * w + ↑k) ↑j) = recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (decodeCiphertext n w word)) (i, k) j

A raw residue word is exactly the recomposition of the decoded ciphertext bits.

theorem Cslib.Crypto.Homomorphic.GSW.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, ⋯⟩)).val

Signed word arithmetic returns exactly the selected modular phase of the decoded inputs.

theorem Cslib.Crypto.Homomorphic.GSW.decryptSerialized_eq (n w : ℕ) (secret ciphertext : List Bool) : decryptSerialized n w secret ciphertext = decrypt (decodeSecret n w secret) (decodeCiphertext n w ciphertext)

The total word algorithm is the original decryption of the total decoded inputs.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.decryptSerialized_serialize {n w : ℕ} (secret : Fin n → ZMod (2 ^ w)) (ciphertext : Ciphertext n w) : decryptSerialized n w (serializeSecret secret) (serializeCiphertext ciphertext) = decrypt secret ciphertext

Canonical words decrypt exactly as their typed secret and ciphertext.

theorem Cslib.Crypto.Homomorphic.GSW.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 ↑k ↑j = ((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

A computed NAND word is the canonical residue of the typed row product.

theorem Cslib.Crypto.Homomorphic.GSW.nandSerialized_eq (n w : ℕ) (left right : List Bool) : nandSerialized n w left right = serializeCiphertext (nand (decodeCiphertext n w left) (decodeCiphertext n w right))

The actual NAND program agrees with the typed operation for every pair of raw words.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.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)

Decoding a raw NAND result recovers the typed operation on the decoded inputs.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.nandSerialized_serialize {n w : ℕ} (left right : Ciphertext n w) : nandSerialized n w (serializeCiphertext left) (serializeCiphertext right) = serializeCiphertext (nand left right)

Canonical input words produce the canonical word of their actual typed NAND.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.length_nandSerialized (n w : ℕ) (left right : List Bool) : (nandSerialized n w left right).length = ((n + 1) * w) ^ 2

Every raw pair produces the complete declared ciphertext word.

theorem Cslib.Crypto.Homomorphic.GSW.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₂)

The actual serialized NAND retains the exact propagated integer error equation.

theorem Cslib.Crypto.Homomorphic.GSW.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 : Fin (n + 1) × Fin w), 4 * (error i).natAbs < 2 ^ w) : decryptSerialized n w secret ciphertext = μ

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 Cslib.Crypto.Homomorphic.GSW.decryptSerialized_encryptWithCoins {n m w bound : ℕ} (B : Matrix (Fin m) (Fin n) (ZMod (2 ^ w))) (secret : Fin n → ZMod (2 ^ w)) (error : Fin m → ℤ) (μ : Bool) (coins : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool) (hw : 0 < w) (herror : ∀ (j : Fin m), (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)) = μ

Canonical actual encryption words decrypt under exactly the typed fresh-noise hypotheses.

theorem Cslib.Crypto.Homomorphic.GSW.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 : Fin (n + 1) × Fin w), (error₁ i).natAbs ≤ bound₁) (herror₂ : ∀ (i : Fin (n + 1) × Fin w), (error₂ i).natAbs ≤ bound₂) (hmargin : 4 * (bound₁ + (n + 1) * w * bound₂) < 2 ^ w) : decryptSerialized n w secret (nandSerialized n w left right) = !(μ₁ && μ₂)

NAND on arbitrary raw ciphertext words is correct under the original propagated-noise margin. No freshness, support, or canonical-length premise is added.

theorem Cslib.Crypto.Homomorphic.GSW.keyGenSerialized_encrypt_correct {n m w η : ℕ} (hw : 0 < w) (hmargin : 4 * (m * η) < 2 ^ w) {keys : List Bool × List Bool} (hkeys : keys ∈ (keyGenSerialized n m w η).eval.support) (μ : Bool) {ciphertext : List Bool} (hciphertext : ciphertext ∈ (encryptSerialized n m w keys.1 μ).eval.support) : decryptSerialized n w keys.2 ciphertext = μ

Every supported actual key and encryption word is correct under the existing fresh margin.

theorem Cslib.Crypto.Homomorphic.GSW.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 ∈ (keyGenSerialized n m w η).eval.support) (μ₁ μ₂ : Bool) {left right : List Bool} (hleft : left ∈ (encryptSerialized n m w keys.1 μ₁).eval.support) (hright : right ∈ (encryptSerialized n m w keys.1 μ₂).eval.support) : decryptSerialized n w keys.2 (nandSerialized n w left right) = !(μ₁ && μ₂)

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.