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.ComputableTidilyInPolyTime (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.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)) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime inputCount input Turing.MultiTapeTM.encUnary) (hcode : Turing.MultiTapeTM.ComputableTidilyInPolyTime 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.