Documentation

Complexity.Crypto.Computational.Homomorphic.GSW.DecryptionCircuit.PolyTime

Native generation of complete GSW decryption circuits #

Unary dimension and word width generate the full code of the actual raw-input decryptor, without an assumed generator or runtime certificate. All matrix selectors and arithmetic circuits are charged, even on inputs outside key-generation or encryption support.

Main results #

source
def Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.code (n w : ℕ) :
List (Circuits.Boolean.Op × List ℕ) × List ℕ

Generate the full selected-row GSW decryptor, including width-zero fallback behavior.

Instances For
    source
    theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.code_eq_code (n w : ℕ) :
    code n w = (circuit n w).code

    The native constructor returns every gate and designated output of the actual circuit.

    source
    theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.computableInPolyTime_code :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => code p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Circuits.Boolean.encCode

    One native polynomial-time algorithm generates the full decryptor from unary parameters.

    source
    theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.computableInPolyTime_circuit :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => ⟨inputWidth p.1 p.2, circuit p.1 p.2⟩) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Circuits.Boolean.encCircuit 1)

    Generate the actual circuit together with its unary input arity in native polynomial time.

    source
    theorem Cslib.Crypto.Homomorphic.GSW.DecryptionCircuit.computableInPolyTime_layeredAugment :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => Circuits.Boolean.Layered.compile (inputWidth p.1 p.2 + inputWidth p.1 p.2) (augmentNand (circuit p.1 p.2)).code) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Circuits.Boolean.Layered.encCompiled

    Generate the complete layered NAND augmentation, including its schedule and selectors.