Fixed-key homomorphic bootstrapping

Generate one base key and publish encryptions of its secret bits under the same public key. Every compiled circuit layer reuses this artifact. The private key and ciphertext representation remain those of the base scheme: no tag, depth budget or key transition is needed.

Evaluation accepts every finite De Morgan circuit, and all algorithms are total on their raw inputs. Decryption executes the actual decryption circuit on padded or truncated input. The correctness and native runtime theorems are separate; the self-encrypted secret requires an explicit circular-security assumption in the security development.

Main definitions

• Cslib.Crypto.Homomorphic.FixedKey.keyGen: sample one key and its self-encrypted secret.
• Cslib.Crypto.Homomorphic.FixedKey.evaluateCircuit: compile and evaluate under the same key.
• Cslib.Crypto.Homomorphic.FixedKey.scheme: the actual construction for every finite circuit.

Main results

• Cslib.Crypto.Homomorphic.FixedKey.mem_support_keyGen_iff: exact supported key artifacts.

References

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

def Cslib.Crypto.Homomorphic.FixedKey.keyGen (E : Scheme) (n : ℕ) : ProbComp (List Bool × List Bool)

Sample one supported key and encrypt every secret bit under its own public key.

def Cslib.Crypto.Homomorphic.FixedKey.encrypt (E : Scheme) (n : ℕ) (pk : List Bool) (bit : Bool) : ProbComp (List Bool)

Decode the public artifact and use ordinary base encryption, without adding a tag.

theorem Cslib.Crypto.Homomorphic.FixedKey.mem_support_keyGen_iff (E : Scheme) (n : ℕ) (output : List Bool × List Bool) : output ∈ (keyGen E n).eval.support ↔ ∃ (keys : List Bool × List Bool) (encryptedKey : List (List Bool)), keys ∈ (E.keyGen n).eval.support ∧ E.FreshInputs n keys.1 keys.2 encryptedKey ∧ output = (encPublicKey (keys.1, encryptedKey), keys.2)

Every supported serialized artifact comes from one actual key sample and supported pointwise encryptions of that same key's secret.

def Cslib.Crypto.Homomorphic.FixedKey.decrypt {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (sk ciphertext : List Bool) : Bool

Execute the decryption circuit on every input word, padding or truncating as necessary.

def Cslib.Crypto.Homomorphic.FixedKey.evaluateCircuit {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (pk : List Bool) (encryptedKey inputs : List (List Bool)) (inputCount : ℕ) (code : List (Circuits.Boolean.Op × List ℕ) × List ℕ) : ProbComp (List (List Bool))

Compile arbitrary raw code and reuse the same public key and encrypted secret at each scheduled layer. The repetition count is computed from the actual code.

def Cslib.Crypto.Homomorphic.FixedKey.evaluate {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (n : ℕ) (pk : List Bool) (c : (m : ℕ) × Circuits.Circuit Circuits.Boolean.signature m 1) (inputs : List (List Bool)) : ProbComp (List Bool)

Evaluate a finite single-output circuit under the one serialized public artifact.

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

Fixed-key bootstrapping permits every finite Boolean circuit. Correctness, uniform efficiency and circular-security hypotheses are not bundled into the algorithms.