Polynomial-time encrypted evaluation of ordinary circuits

The native certificate composes the actual compiler, layered evaluator, and output selection. It includes the complete circuit code and handles malformed references and keys. It requires efficient base encryption, base evaluation, and the decryption-circuit generator; correctness and security assumptions play no role in this runtime statement.

Main results

• Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateCircuit: strict polynomial-time evaluation of raw Boolean circuit code, uniformly across its input and output arities.

theorem Cslib.Crypto.Homomorphic.Scheme.isPPTOn_evaluateCircuit {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.ComputableInPolyTime (fun (n : ℕ) => ⟨secretWidth n + ciphertextWidth n, D.circuit n⟩) Turing.MultiTapeTM.encUnary (Circuits.Boolean.encCircuit 1)) {α : Type} {input : α ↪ List Bool} {n inputCount : α → ℕ} {publicKeys inputs : α → List (List Bool)} {encryptedKeys : α → List (List (List Bool))} {code : α → List (Circuits.Boolean.Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hpks : Turing.MultiTapeTM.ComputableInPolyTime publicKeys input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (heks : Turing.MultiTapeTM.ComputableInPolyTime encryptedKeys input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits))) (hinputs : Turing.MultiTapeTM.ComputableInPolyTime inputs input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hcount : Turing.MultiTapeTM.ComputableInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hcode : Turing.MultiTapeTM.ComputableInPolyTime code input Circuits.Boolean.encCode) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) fun (a : α) => evaluateCircuit D (n a) (publicKeys a) (encryptedKeys a) (inputs a) (inputCount a) (code a)

Compile, evaluate, and select outputs in native polynomial time. The compiler computes its own depth table; there is no supplied runtime, depth, validity, or correctness certificate.