Exact bridges for the serialized GSW algorithms

The executable word algorithms agree with the typed modular formulas, for every serialized input under the specified total decoders. The equalities do not require a noise bound or a security assumption. Composition with the exact sampling laws retains the complete joint key distribution and the encryption distribution.

Main results

• publicMatrixSerialized_eq, encryptWithCoinsSerialized_eq: exact deterministic bridges.
• eval_keyGenSerialized, eval_encryptSerialized: exact probabilistic bridges.

References

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

theorem Cslib.Crypto.Homomorphic.GSW.publicRowHead_eq {n m w : ℕ} (inputs : SerializedKeyInputs) (i : Fin m) : publicRowHead n w inputs ↑i = (publicMatrix (decodeKeyInputs n m w inputs).publicPart (decodeKeyInputs n m w inputs).secret (decodeKeyInputs n m w inputs).error i 0).val

The binary signed-remainder computation returns the canonical leading public residue.

theorem Cslib.Crypto.Homomorphic.GSW.publicMatrixSerialized_eq (n m w : ℕ) (inputs : SerializedKeyInputs) : publicMatrixSerialized n m w inputs = serializePublicMatrix (publicMatrix (decodeKeyInputs n m w inputs).publicPart (decodeKeyInputs n m w inputs).secret (decodeKeyInputs n m w inputs).error)

The total public-key computation is exactly the typed public matrix of the decoded inputs.

theorem Cslib.Crypto.Homomorphic.GSW.secretSerialized_eq (n w : ℕ) (secret : List ℕ) : secretSerialized n w secret = serializeSecret fun (i : Fin n) => ↑(secret.getD (↑i) 0)

The total secret computation agrees with the same padded and modularly normalized inputs.

theorem Cslib.Crypto.Homomorphic.GSW.encryptEntry_eq (n m w : ℕ) (publicWord : List Bool) (message : Bool) (coins : SerializedCoins) (i : Fin (n + 1)) (k : Fin w) (j : Fin (n + 1)) : encryptEntry n m w publicWord message coins ↑i ↑k ↑j = ((↑message.toNat • gadgetMatrix n w + bitMatrix (ZMod (2 ^ w)) (decodeCoins n m w coins) * Matrix.ofBinary m (n + 1) w publicWord) (i, k) j).val

A computed ciphertext entry is the canonical residue of the actual modular formula.

theorem Cslib.Crypto.Homomorphic.GSW.encryptWithCoinsSerialized_eq (n m w : ℕ) (publicWord : List Bool) (message : Bool) (coins : SerializedCoins) : encryptWithCoinsSerialized n m w publicWord message coins = serializeCiphertext (encryptWithCoins (Matrix.ofBinary m (n + 1) w publicWord) message (decodeCoins n m w coins))

All bits of the total ciphertext computation agree with encryption of the decoded inputs.

theorem Cslib.Crypto.Homomorphic.GSW.publicMatrixSerialized_serializeKeyInputs {n m w : ℕ} (inputs : KeyInputs n m w) : publicMatrixSerialized n m w (serializeKeyInputs inputs) = serializePublicMatrix (publicMatrix inputs.publicPart inputs.secret inputs.error)

Canonical sampled inputs produce exactly the original typed public key.

theorem Cslib.Crypto.Homomorphic.GSW.secretSerialized_serializeKeyInputs {n m w : ℕ} (inputs : KeyInputs n m w) : secretSerialized n w (serializeKeyInputs inputs).1 = serializeSecret inputs.secret

Canonical sampled inputs produce exactly the original typed secret key.

theorem Cslib.Crypto.Homomorphic.GSW.encryptWithCoinsSerialized_serialize {n m w : ℕ} (A : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) (message : Bool) (coins : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool) : encryptWithCoinsSerialized n m w (serializePublicMatrix A) message (serializeCoins coins) = serializeCiphertext (encryptWithCoins A message coins)

Serialization commutes with the actual typed encryption on canonical inputs.

theorem Cslib.Crypto.Homomorphic.GSW.length_publicMatrixSerialized (n m w : ℕ) (inputs : SerializedKeyInputs) : (publicMatrixSerialized n m w inputs).length = m * (n + 1) * w

Every arbitrary input produces the complete declared public word.

theorem Cslib.Crypto.Homomorphic.GSW.length_secretSerialized (n w : ℕ) (secret : List ℕ) : (secretSerialized n w secret).length = n * w

Secret normalization retains exactly the declared number of residue bits.

theorem Cslib.Crypto.Homomorphic.GSW.length_encryptWithCoinsSerialized (n m w : ℕ) (publicWord : List Bool) (message : Bool) (coins : SerializedCoins) : (encryptWithCoinsSerialized n m w publicWord message coins).length = ((n + 1) * w) ^ 2

Encryption writes every bit of its square ciphertext, on arbitrary input words and coins.

theorem Cslib.Crypto.Homomorphic.GSW.eval_keyGenSerialized (n m w η : ℕ) : (keyGenSerialized n m w η).eval = PMF.map (fun (keys : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) × (Fin n → ZMod (2 ^ w))) => (serializePublicMatrix keys.1, serializeSecret keys.2)) (keyGen n m w η).eval

The efficient key sampler retains the typed construction's complete public/secret joint law.

theorem Cslib.Crypto.Homomorphic.GSW.eval_encryptSerialized (n m w : ℕ) (publicWord : List Bool) (message : Bool) : (encryptSerialized n m w publicWord message).eval = PMF.map serializeCiphertext (encrypt (Matrix.ofBinary m (n + 1) w publicWord) message).eval

The efficient encryption sampler agrees with typed encryption of every decoded public word.

theorem Cslib.Crypto.Homomorphic.GSW.eval_encryptSerialized_serializePublicMatrix {n m w : ℕ} (A : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) (message : Bool) : (encryptSerialized n m w (serializePublicMatrix A) message).eval = PMF.map serializeCiphertext (encrypt A message).eval

Canonical public words have the exact original typed encryption distribution.