A depth-budgeted homomorphic scheme

For a depth budget B, generate 2 * B + 1 independent base keys and encrypt each secret under the next public key. Evaluation compiles the circuit and pads its schedule with identity refresh layers to exactly 2 * B transitions. All permitted circuits therefore end at the same final key, including circuits with no gates. Output selection requires no further transition.

The public artifact contains only public keys and encrypted links. The private artifact contains the two endpoint secrets. A leading ciphertext bit selects the initial secret for fresh encryptions and the final secret for evaluated ciphertexts. This adapts Gentry's leveled construction to Scheme.Correct, which requires the same decryption algorithm for both forms. The tag does not claim to hide whether a ciphertext is fresh or evaluated. There is no encrypted link from the final key back to the initial key.

All algorithms are total. Decryption executes the supplied decryption circuit on a padded or truncated input, rather than relying on unspecified behavior of the base decryption algorithm on malformed words. Correctness, native efficiency and security are separate obligations.

Main definitions

• Cslib.Crypto.Homomorphic.Leveled.keyPair: serialize the public and private artifacts.
• Cslib.Crypto.Homomorphic.Leveled.evaluateCircuit: pad and evaluate a raw circuit schedule.
• Cslib.Crypto.Homomorphic.Leveled.scheme: the actual depth-budgeted encryption scheme.

References

• C. Gentry, Fully homomorphic encryption using ideal lattices, Section 2

def Cslib.Crypto.Homomorphic.Leveled.keyPair (depth : ℕ) (keys : List (List Bool × List Bool)) (links : List (List (List Bool))) : List Bool × List Bool

Public keys and encrypted links are public; only the endpoint secrets are retained privately. The intermediate secrets used to construct the links are omitted from both artifacts.

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

Sample the actual acyclic chain and serialize its public and private projections.

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

A fresh ciphertext contains a false tag and an encryption under the initial public key.

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

Execute the certified decryption circuit with the endpoint selected by the tag. This algorithm is independent of the depth budget, including on malformed keys and ciphertexts.

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

Compile, pad with identity refreshes, evaluate, and select the original ordered outputs. publicKeys starts with the first target key, omitting the initial input-encryption key. For an over-budget raw code, padTo retains the full compiled schedule; no correctness claim is made for such inputs.

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

Strip fresh tags, evaluate the padded circuit under the public chain, and tag the result for the final endpoint secret. The correctness contract takes fresh encryptions as inputs.

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

The depth-budgeted scheme. Efficiency of the budget family is a separate hypothesis for the uniform runtime certificates. No correctness or runtime conclusion is bundled as input.