Uniform native computation of serialized GSW keys and ciphertexts

The actual word-valued algorithms are polynomial-time uniformly in their unary dimensions, binary residues and signed binary errors. No shape or canonical-input assumption is needed: defaulted lookup and signed remainder specify the behavior on arbitrary inputs. The certificates charge the complete public key, secret and ciphertext words, as well as all intermediate list framing. They do not use a fixed-dimensional finite-type encoding to obtain efficiency.

Main results

• computableTidilyInPolyTime_publicMatrixSerialized, computableTidilyInPolyTime_secretSerialized: actual deterministic key construction.
• computableTidilyInPolyTime_encryptWithCoinsSerialized: actual public-word encryption.
• isPPTOn_keyGenSerialized, isPPTOn_encryptSerialized: strict PPT for the complete programs, composing the existing independent input samplers with the deterministic computations.

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.computableTidilyInPolyTime_publicRowHead {α : Type} {input : α ↪ List Bool} {n w i : α → ℕ} {inputs : α → SerializedKeyInputs} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hinputs : Turing.MultiTapeTM.ComputableTidilyInPolyTime inputs input encSerializedKeyInputs) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => publicRowHead (n a) (w a) (inputs a) (i a)) input Turing.MultiTapeTM.encNat

Compute a public row's leading residue from arbitrary binary inputs and signed errors.

theorem Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_publicMatrixSerialized {α : Type} {input : α ↪ List Bool} {n m w : α → ℕ} {inputs : α → SerializedKeyInputs} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hinputs : Turing.MultiTapeTM.ComputableTidilyInPolyTime inputs input encSerializedKeyInputs) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => publicMatrixSerialized (n a) (m a) (w a) (inputs a)) input Turing.MultiTapeTM.encBits

Construct the entire public word, charging the runtime number and width of every entry.

theorem Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_secretSerialized {α : Type} {input : α ↪ List Bool} {n w : α → ℕ} {secret : α → List ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hsecret : Turing.MultiTapeTM.ComputableTidilyInPolyTime secret input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => secretSerialized (n a) (w a) (secret a)) input Turing.MultiTapeTM.encBits

Normalize and write the declared number of binary secret coordinates.

theorem Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_encryptEntry {α : Type} {input : α ↪ List Bool} {n m w i k j : α → ℕ} {publicWord : α → List Bool} {message : α → Bool} {coins : α → SerializedCoins} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hpublicWord : Turing.MultiTapeTM.ComputableTidilyInPolyTime publicWord input Turing.MultiTapeTM.encBits) (hmessage : Turing.MultiTapeTM.ComputableTidilyInPolyTime message input Turing.MultiTapeTM.encBool) (hcoins : Turing.MultiTapeTM.ComputableTidilyInPolyTime coins input encSerializedCoins) (hi : Turing.MultiTapeTM.ComputableTidilyInPolyTime i input Turing.MultiTapeTM.encUnary) (hk : Turing.MultiTapeTM.ComputableTidilyInPolyTime k input Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableTidilyInPolyTime j input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => encryptEntry (n a) (m a) (w a) (publicWord a) (message a) (coins a) (i a) (k a) (j a)) input Turing.MultiTapeTM.encNat

Compute a binary entry of the masked public matrix plus the message gadget.

theorem Cslib.Crypto.Homomorphic.GSW.computableTidilyInPolyTime_encryptWithCoinsSerialized {α : Type} {input : α ↪ List Bool} {n m w : α → ℕ} {publicWord : α → List Bool} {message : α → Bool} {coins : α → SerializedCoins} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hpublicWord : Turing.MultiTapeTM.ComputableTidilyInPolyTime publicWord input Turing.MultiTapeTM.encBits) (hmessage : Turing.MultiTapeTM.ComputableTidilyInPolyTime message input Turing.MultiTapeTM.encBool) (hcoins : Turing.MultiTapeTM.ComputableTidilyInPolyTime coins input encSerializedCoins) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => encryptWithCoinsSerialized (n a) (m a) (w a) (publicWord a) (message a) (coins a)) input Turing.MultiTapeTM.encBits

Encrypt from arbitrary public words and coins, charging the complete ciphertext output.

theorem Cslib.Crypto.Homomorphic.GSW.isPPTOn_keyGenSerialized {α : Type} {input : α ↪ List Bool} {n m w η : α → ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hη : Turing.MultiTapeTM.ComputableTidilyInPolyTime η input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (a : α) => keyGenSerialized (n a) (m a) (w a) (η a)

The complete key generator is strict PPT for arbitrary efficient runtime dimensions.

theorem Cslib.Crypto.Homomorphic.GSW.isPPTOn_encryptSerialized {α : Type} {input : α ↪ List Bool} {n m w : α → ℕ} {publicWord : α → List Bool} {message : α → Bool} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hm : Turing.MultiTapeTM.ComputableTidilyInPolyTime m input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableTidilyInPolyTime w input Turing.MultiTapeTM.encUnary) (hpublicWord : Turing.MultiTapeTM.ComputableTidilyInPolyTime publicWord input Turing.MultiTapeTM.encBits) (hmessage : Turing.MultiTapeTM.ComputableTidilyInPolyTime message input Turing.MultiTapeTM.encBool) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => encryptSerialized (n a) (m a) (w a) (publicWord a) (message a)

The complete encryption program is strict PPT on arbitrary public words and messages.