Uniform polynomial-time evaluation of encrypted layers

The actual evaluator has one uniform polynomial clock for the full encoded public input. Binary wire lookups are bounded before unary conversion. Every node's output is truncated at the generated decryption circuit's unary input arity, which bounds state growth even on malformed keys, links, ciphertexts and node references. Correctness, fixed widths and secrecy assumptions are not used in these runtime certificates.

Main results

• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateNode: evaluate one node and truncate its output.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateLayer: traverse a complete layer.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateLayerStep: advance the public loop state.
• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateLayers: execute the complete public loop.

References

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

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateNode {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (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) (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) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {pk : α → List Bool} {encryptedKey inputs : α → List (List Bool)} {node : α → Circuits.Boolean.Layered.Node} (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)) (hnode : Turing.MultiTapeTM.ComputableTidilyInPolyTime node input Circuits.Boolean.Layered.encNode) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => evaluateNode D (n a) (pk a) (encryptedKey a) (inputs a) (node a)

Execute the actual node program, including binary lookups and unconditional truncation.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateLayer {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (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) (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) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {pk : α → List Bool} {encryptedKey inputs : α → List (List Bool)} {layer : α → List Circuits.Boolean.Layered.Node} (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)) (hlayer : Turing.MultiTapeTM.ComputableTidilyInPolyTime layer input (Turing.MultiTapeTM.encList Circuits.Boolean.Layered.encNode)) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) fun (a : α) => evaluateLayer D (n a) (pk a) (encryptedKey a) (inputs a) (layer a)

Evaluate every node of a computed layer, charging the entire input and output lists.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateLayerStep {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (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) (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) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {publicKeys : α → List (List Bool)} {encryptedKeys : α → List (List (List Bool))} {layers : α → List (List Circuits.Boolean.Layered.Node)} {state : α → ℕ × List (List Bool)} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hpks : Turing.MultiTapeTM.ComputableTidilyInPolyTime publicKeys input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (heks : Turing.MultiTapeTM.ComputableTidilyInPolyTime encryptedKeys input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))) (hlayers : Turing.MultiTapeTM.ComputableTidilyInPolyTime layers input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Circuits.Boolean.Layered.encNode))) (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (a : α) => evaluateLayerStep D (n a) (publicKeys a) (encryptedKeys a) (layers a) (state a)

Read the next public key, encrypted link and layer with a unary loop index, then advance it.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateLayers {E : Scheme} {secretWidth ciphertextWidth : ℕ → ℕ} (D : DecryptionCircuits E secretWidth ciphertextWidth) (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) (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) (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {inputs publicKeys : α → List (List Bool)} {encryptedKeys : α → List (List (List Bool))} {layers : α → List (List Circuits.Boolean.Layered.Node)} (hn : Turing.MultiTapeTM.ComputableTidilyInPolyTime n input Turing.MultiTapeTM.encUnary) (hpks : Turing.MultiTapeTM.ComputableTidilyInPolyTime publicKeys input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (heks : Turing.MultiTapeTM.ComputableTidilyInPolyTime encryptedKeys input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))) (hinputs : Turing.MultiTapeTM.ComputableTidilyInPolyTime inputs input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hlayers : Turing.MultiTapeTM.ComputableTidilyInPolyTime layers input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Circuits.Boolean.Layered.encNode))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) fun (a : α) => evaluateLayers D (n a) (publicKeys a) (encryptedKeys a) (inputs a) (layers a)

Evaluate all layers with a strict polynomial clock in their full public encoding. The state bound covers malformed keys and references, without Scheme.Correct, FixedWidth or input validity premises. Secret keys are not arguments to the algorithm.