Correctness of fixed-key homomorphic evaluation

The same supported base key and self-encrypted secret can be reused at every compiled layer. The proof requires pointwise supported secret-bit encryptions, not independent copies of their randomness. Inputs need only have the base ciphertext width and the desired decryption; this includes outputs of previous evaluations. Every finite circuit preserves the same key and exact ciphertext width.

Main results

• Cslib.Crypto.Homomorphic.FixedKey.encryptedWires_evaluateCircuit: arbitrary circuit outputs retain their plaintexts and width under the same key.
• Cslib.Crypto.Homomorphic.FixedKey.evaluate_spec: the constructed evaluator accepts earlier evaluated ciphertexts with the correct width and decryption.
• Cslib.Crypto.Homomorphic.FixedKey.correct: perfect correctness for every finite circuit.
• Cslib.Crypto.Homomorphic.FixedKey.fixedWidth: unchanged secret and ciphertext widths.
• Cslib.Crypto.Homomorphic.FixedKey.decryptionCircuits: reuse the actual decryption circuit.

References

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

theorem Cslib.Crypto.Homomorphic.FixedKey.decrypt_eq {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (sk ciphertext : List Bool) (hsk : sk.length = secretWidth n) (hc : ciphertext.length = ciphertextWidth n) : decrypt D n sk ciphertext = E.decrypt n sk ciphertext

Executing the decryption circuit agrees with base decryption on every well-sized word.

theorem Cslib.Crypto.Homomorphic.FixedKey.encryptedWires_iff {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (sk : List Bool) (hsk : sk.length = secretWidth n) (bits : List Bool) (inputs : List (List Bool)) : (scheme D).EncryptedWires ciphertextWidth n sk bits inputs ↔ E.EncryptedWires ciphertextWidth n sk bits inputs

On the unchanged secret and ciphertext representation, both schemes have the same well-sized encrypted-wire relation. No freshness hypothesis is needed.

theorem Cslib.Crypto.Homomorphic.FixedKey.encryptedWires_evaluateCircuit {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (E.keyGen n).eval.support) (encryptedKey : List (List Bool)) (hlink : E.FreshInputs n keys.1 keys.2 encryptedKey) {inputCount outputCount : ℕ} (c : Circuits.Circuit Circuits.Boolean.signature inputCount outputCount) (x : Fin inputCount → Bool) (inputs : List (List Bool)) (hinputs : E.EncryptedWires ciphertextWidth n keys.2 (List.ofFn x) inputs) (outputs : List (List Bool)) (houtputs : outputs ∈ (evaluateCircuit D n keys.1 encryptedKey inputs inputCount c.code).eval.support) : E.EncryptedWires ciphertextWidth n keys.2 (List.ofFn (c.eval Circuits.Boolean.interpretation x)) outputs

Repeating one supported key and its self-encrypted secret evaluates any finite circuit. The starting wires may already have been evaluated; output selection also handles depth zero.

theorem Cslib.Crypto.Homomorphic.FixedKey.encrypt_spec {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ ((scheme D).keyGen n).eval.support) (bit : Bool) (ciphertext : List Bool) (hc : ciphertext ∈ ((scheme D).encrypt n keys.1 bit).eval.support) : ciphertext.length = ciphertextWidth n ∧ (scheme D).decrypt n keys.2 ciphertext = bit

Fresh fixed-key encryptions retain the exact base width and decrypt under the base secret.

theorem Cslib.Crypto.Homomorphic.FixedKey.freshInputs_encryptedWires {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) {n : ℕ} {keys : List Bool × List Bool} (hkeys : keys ∈ ((scheme D).keyGen n).eval.support) {bits : List Bool} {inputs : List (List Bool)} (hinputs : (scheme D).FreshInputs n keys.1 bits inputs) : (scheme D).EncryptedWires ciphertextWidth n keys.2 bits inputs

Fresh inputs satisfy the constructed scheme's stronger wire invariant.

theorem Cslib.Crypto.Homomorphic.FixedKey.evaluate_spec {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ ((scheme D).keyGen n).eval.support) (c : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1) (bits : List Bool) (inputs : List (List Bool)) (hbits : bits.length = c.fst) (hinputs : (scheme D).EncryptedWires ciphertextWidth n keys.2 bits inputs) (ciphertext : List Bool) (hc : ciphertext ∈ ((scheme D).evaluate n keys.1 c inputs).eval.support) : ciphertext.length = ciphertextWidth n ∧ (scheme D).decrypt n keys.2 ciphertext = c.snd.eval Circuits.Boolean.interpretation (BitString.ofList c.fst bits) 0

Every supported evaluator result has the exact base width and correct decryption under the same secret key. The inputs may be prior evaluation outputs; they need not be fresh.

theorem Cslib.Crypto.Homomorphic.FixedKey.correct {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) : (scheme D).Correct

Actual bootstrapping constructs a correct scheme permitting every finite Boolean circuit.

theorem Cslib.Crypto.Homomorphic.FixedKey.fixedWidth {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (hE : E.Correct) (hwidth : E.FixedWidth secretWidth ciphertextWidth) (hD : Scheme.Bootstrappable D) : (scheme D).FixedWidth secretWidth ciphertextWidth

Secret keys and all valid ciphertexts retain exactly the base widths, independently of the evaluated circuit and any previous sequence of evaluations.

def Cslib.Crypto.Homomorphic.FixedKey.decryptionCircuits {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) : DecryptionCircuits (scheme D) secretWidth ciphertextWidth

The constructed scheme executes the same decryption circuit, including on malformed data.