Uniform native certificates for fixed-key bootstrapping #

The actual sampler encrypts one secret key under its own public key. Evaluation repeats that public artifact across the compiled circuit layers; the key sampler takes no circuit or depth parameter. The certificates charge the complete keys, encrypted secret, circuit code, ciphertext inputs and outputs. Total decoding and evaluation also cover malformed artifacts and raw codes.

The only runtime premises concern the base algorithms and a uniform generator for the actual decryption circuits. Correctness, bootstrappability, circular security and valid input widths are not used to supply a runtime bound. Both unchanged widths and the decryption-circuit size are polynomially bounded as a consequence of the generator certificate.

Main results #

Cslib.Crypto.Homomorphic.FixedKey.isPPTOn_keyGen: generate the fixed public artifact.
Cslib.Crypto.Homomorphic.FixedKey.isPPTOn_encrypt: encrypt after total artifact decoding.
Cslib.Crypto.Homomorphic.FixedKey.computableTidilyInPolyTime_decrypt: execute decryption.
Cslib.Crypto.Homomorphic.FixedKey.isPPTOn_evaluate: evaluate the complete circuit uniformly.
Cslib.Crypto.Homomorphic.FixedKey.polynomiallyBounded_widths: bound both unchanged widths.
Cslib.Crypto.Homomorphic.FixedKey.polynomiallyBounded_decryptionSize: bound circuit size.

References #

C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2, the self-loop construction

source

Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (a : α) => keyGen E (n a)

Generate one base key, encrypt its entire secret under that key, and serialize the artifact. The key generator has no circuit-size or depth parameter.

source

Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => encrypt E (n a) (pk a) (bit a)

Decode any public word and encrypt under the decoded base public key.

source

Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => decrypt D (n a) (sk a) (ciphertext a)) input Turing.MultiTapeTM.encBool

Execute the generated decryption circuit on every encoded secret and ciphertext, with the circuit evaluator's total padding and truncation conventions.

source

theorem Cslib.Crypto.Homomorphic.FixedKey.isPPTOn_evaluateCircuit {α : Type} {input : α ↪ List Bool} {E : Scheme} (hencrypt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Bool) => E.encrypt p.1 p.2.1 p.2.2) {n : α → ℕ} {pk : α → List Bool} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) (hevaluate : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List (List Bool)) => E.evaluate p.1 p.2.1 p.2.2.1 p.2.2.2) {inputCount : α → ℕ} {encryptedKey inputs : α → List (List Bool)} {code : α → List (Circuits.Boolean.Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hpk : Turing.MultiTapeTM.ComputableTidilyInPolyTime pk input Turing.MultiTapeTM.encBits) (hek : Turing.MultiTapeTM.ComputableTidilyInPolyTime encryptedKey input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hinputs : Turing.MultiTapeTM.ComputableTidilyInPolyTime inputs input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hcode : Turing.MultiTapeTM.ComputableTidilyInPolyTime code input Circuits.Boolean.encCode) :

Probability.IsPPTOn input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) fun (a : α) => evaluateCircuit D (n a) (pk a) (encryptedKey a) (inputs a) (inputCount a) (code a)

Compute the actual output depth, repeat the public artifact, and run the compiler and encrypted evaluator. Both binary indices and all copied artifact data are charged.

source

Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => evaluate D (n a) (pk a) (c a) (inputs a)

One uniform native certificate evaluates all finite circuits under the same public artifact. It charges the complete encoded circuit and inputs without any correctness or width premise.

source

theorem Cslib.Crypto.Homomorphic.FixedKey.polynomiallyBounded_widths {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) :

PolynomiallyBounded secretWidth ∧ PolynomiallyBounded ciphertextWidth

Unary input arity in the emitted decryption circuit bounds both unchanged widths polynomially in the security parameter. No separate width-computability premise is needed.

source