Polynomial-time generation of NAND-augmented circuits

The concrete augmentation transformer duplicates the encoded circuit, relocates its two input blocks, and connects their outputs to the fixed two-gate NAND circuit. Existing code composition certificates account for every binary wire lookup and relocation and the complete emitted code. The circuit encoding records its input count in unary and its wire indices in binary.

Main results

• Cslib.Crypto.Homomorphic.computableTidilyInPolyTime_augmentNand: uniform polynomial-time construction of the actual NAND augmentation.

References

• C. Gentry, Fully Homomorphic Encryption Using Ideal Lattices, Section 2

theorem Cslib.Crypto.Homomorphic.computableTidilyInPolyTime_augmentNand : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (D : (n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) => ⟨D.fst + D.fst, augmentNand D.snd⟩) (Circuits.Boolean.encCircuit 1) (Circuits.Boolean.encCircuit 1)

Generate the concrete NAND augmentation in uniform polynomial time. The input arity and all gates, wire indices and output references are read and written through encCircuit 1.