Executable serialized GSW keys and ciphertexts

Residues are written with exactly w bits, least significant first, and matrices are row major. The dimensions are explicit inputs to the algorithms. Missing list entries and bits are zero; excess data is ignored. Integer errors are reduced by Euclidean remainder, so negative errors wrap correctly. These conventions specify total behavior on malformed inputs.

The programs below compute the public matrix and ciphertext of Gentry, Sahai and Waters, Section 3.1. The computational certificates are separate from the exact algebraic bridges. No security or bootstrappability is asserted.

Main definitions

• serializePublicMatrix, serializeSecret, serializeCiphertext: canonical typed words.
• publicMatrixSerialized, encryptWithCoinsSerialized: total deterministic computations.
• keyGenSerialized, encryptSerialized: the actual probabilistic word-valued algorithms.

Main results

• decode_serializeSecret, decode_serializeCiphertext: exact typed roundtrips.
• length_serializePublicMatrix, length_serializeSecret, length_serializeCiphertext: complete fixed-width output lengths.

Exact deterministic and distributional bridges are in GSW.Serialized.Correctness; native certificates for the complete programs are in GSW.Serialized.PolyTime.

References

• C. Gentry, A. Sahai and B. Waters, Homomorphic Encryption from Learning with Errors: Conceptually-Simpler, Asymptotically-Faster, Attribute-Based, Section 3.1

def Cslib.Crypto.Homomorphic.GSW.serializePublicMatrix {n m w : ℕ} (A : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) : List Bool

Canonical public matrices use the generic fixed-width row-major representation.

def Cslib.Crypto.Homomorphic.GSW.serializeSecret {n w : ℕ} (secret : Fin n → ZMod (2 ^ w)) : List Bool

Canonical secret residues are consecutive low-order-first words.

def Cslib.Crypto.Homomorphic.GSW.decodeSecret (n w : ℕ) (word : List Bool) : Fin n → ZMod (2 ^ w)

Total secret decoding reads the declared number of residue words, padding with zero bits.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.decode_serializeSecret {n w : ℕ} (secret : Fin n → ZMod (2 ^ w)) : decodeSecret n w (serializeSecret secret) = secret

Canonical secret words retain every residue.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.length_serializePublicMatrix {n m w : ℕ} (A : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) : (serializePublicMatrix A).length = m * (n + 1) * w

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.length_serializeSecret {n w : ℕ} (secret : Fin n → ZMod (2 ^ w)) : (serializeSecret secret).length = n * w

def Cslib.Crypto.Homomorphic.GSW.serializeCiphertext {n w : ℕ} (C : Ciphertext n w) : List Bool

Ciphertext coordinates (i, k) are ordered by i * w + k, in rows and columns.

def Cslib.Crypto.Homomorphic.GSW.decodeCiphertext (n w : ℕ) (word : List Bool) : Ciphertext n w

Total ciphertext decoding uses the declared dimensions and pads absent bits with false.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.decode_serializeCiphertext {n w : ℕ} (C : Ciphertext n w) : decodeCiphertext n w (serializeCiphertext C) = C

Canonical ciphertext words retain every bit.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.length_serializeCiphertext {n w : ℕ} (C : Ciphertext n w) : (serializeCiphertext C).length = ((n + 1) * w) ^ 2

The complete ciphertext has the expected square number of bits.

def Cslib.Crypto.Homomorphic.GSW.publicRowHead (n w : ℕ) (inputs : SerializedKeyInputs) (i : ℕ) : ℕ

Compute the leading entry B * secret + error of a public row in binary arithmetic.

def Cslib.Crypto.Homomorphic.GSW.publicMatrixSerialized (n m w : ℕ) (inputs : SerializedKeyInputs) : List Bool

Compute the public word from arbitrary serialized sampled inputs.

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

Normalize and serialize an arbitrary secret list to the declared dimensions.

def Cslib.Crypto.Homomorphic.GSW.encryptEntry (n m w : ℕ) (publicWord : List Bool) (message : Bool) (coins : SerializedCoins) (i k j : ℕ) : ℕ

One entry of message * G + R * A, before its bit decomposition.

def Cslib.Crypto.Homomorphic.GSW.encryptWithCoinsSerialized (n m w : ℕ) (publicWord : List Bool) (message : Bool) (coins : SerializedCoins) : List Bool

Compute all ciphertext bits from the actual public word, message and Boolean coins.

noncomputable def Cslib.Crypto.Homomorphic.GSW.keyGenSerialized (n m w η : ℕ) : ProbComp (List Bool × List Bool)

Sample the existing random inputs and run the actual public-key computation.

noncomputable def Cslib.Crypto.Homomorphic.GSW.encryptSerialized (n m w : ℕ) (publicWord : List Bool) (message : Bool) : ProbComp (List Bool)

Sample the existing Boolean coins and run the actual ciphertext computation.