Documentation

Complexity.Computability.Circuit.Boolean.Modular.Multiply.PolyTime

Native modular multiplier generation #

All shifted partial products, balanced carry-save gates and the final adder are generated from unary width. The output is the full existing circuit code, including unused fallback gates.

Main results #

source
def Cslib.Circuits.Boolean.Modular.multiplyCode (w : ℕ) :
List (Op × List ℕ) × List ℕ

Generate the complete modular multiplier, preserving the half-split reduction topology.

Instances For
    source
    theorem Cslib.Circuits.Boolean.Modular.multiplyCode_eq_code (w : ℕ) :
    multiplyCode w = (multiply w).code

    Raw generation agrees gate-for-gate with the total typed modular multiplier.

    source
    theorem Cslib.Circuits.Boolean.Modular.computableInPolyTime_multiply :
    Turing.MultiTapeTM.ComputableInPolyTime (fun (w : ℕ) => (multiply w).code) Turing.MultiTapeTM.encUnary encCode

    Generation is native polynomial-time in unary width, charging the complete binary code.