Native generation of carry-lookahead circuit codes

All constructors return the actual binary gate-and-output encoding. Widths and loop counts are unary; distances and wire references are binary. The prefix loop carries its already generated code and appends one fixed-width round at a time. Bounds on the complete intermediate encoding justify the loop, including tags, delimiters and output references.

Main definitions

• Cslib.Circuits.Boolean.CarryLookahead.stepCode: one round on raw parameters.

Main results

• Cslib.Circuits.Boolean.CarryLookahead.stepCode_eq: agreement with the typed round.
• Cslib.Circuits.Boolean.computableInPolyTime_carryLookahead: native generation of the complete adder code from unary width.
• Cslib.Circuits.Boolean.computableInPolyTime_carryLookaheadAdd, computableInPolyTime_carryLookaheadFinish: the modular and carry-save finishing codes.

def Cslib.Circuits.Boolean.CarryLookahead.neighbourIndex (k distance i : ℕ) : ℕ

The total raw neighbour rule used by the doubling layer.

def Cslib.Circuits.Boolean.CarryLookahead.generateCode (k distance i : ℕ) : List (Op × List ℕ) × List ℕ

The generate cell's full code, also defined on out-of-range raw coordinates.

def Cslib.Circuits.Boolean.CarryLookahead.propagateCode (k distance i : ℕ) : List (Op × List ℕ) × List ℕ

The propagate cell's full code.

def Cslib.Circuits.Boolean.CarryLookahead.stepCode (k distance : ℕ) : List (Op × List ℕ) × List ℕ

Bundle the fixed-size generate and propagate blocks of one doubling round.

theorem Cslib.Circuits.Boolean.CarryLookahead.stepCode_eq (k distance : ℕ) : stepCode k distance = (step k distance).code

The raw round is exactly the typed circuit's code, with no malformed-input assumption.

theorem Cslib.Circuits.Boolean.CarryLookahead.computableInPolyTime_stepCode {α : Type} {enc : α ↪ List Bool} {k distance : α → ℕ} (hk : Turing.MultiTapeTM.ComputableInPolyTime k enc Turing.MultiTapeTM.encUnary) (hd : Turing.MultiTapeTM.ComputableInPolyTime distance enc Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => stepCode (k a) (distance a)) enc encCode

A doubling round is generated uniformly from a unary width and a binary distance.

theorem Cslib.Circuits.Boolean.CarryLookahead.computableInPolyTime_scan : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => (scan p.1 p.2).code) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCode

Generate any number of doubling rounds from unary width and round count. The native loop keeps the accumulated code and unary round counter, with polynomial intermediate encoded length.

def Cslib.Circuits.Boolean.CarryLookahead.initialGenerateCode (w i : ℕ) : List (Op × List ℕ) × List ℕ

The generate gate of an initial cell, expressed as raw circuit data.

def Cslib.Circuits.Boolean.CarryLookahead.initialPropagateCode (w i : ℕ) : List (Op × List ℕ) × List ℕ

The propagate gate of an initial cell, expressed as raw circuit data.

def Cslib.Circuits.Boolean.CarryLookahead.initialCode (w : ℕ) : List (Op × List ℕ) × List ℕ

The whole initial row, with one gate per generate or propagate cell.

theorem Cslib.Circuits.Boolean.CarryLookahead.computableInPolyTime_initial : Turing.MultiTapeTM.ComputableInPolyTime (fun (w : ℕ) => (initial w).code) Turing.MultiTapeTM.encUnary encCode

Native generation of the complete initial carry row from unary width.

theorem Cslib.Circuits.Boolean.CarryLookahead.computableInPolyTime_carries : Turing.MultiTapeTM.ComputableInPolyTime (fun (w : ℕ) => (carries w).code) Turing.MultiTapeTM.encUnary encCode

Native generation of all the input carries from unary word width.

def Cslib.Circuits.Boolean.CarryLookahead.sumCode (w i : ℕ) : List (Op × List ℕ) × List ℕ

The sum cell's raw code, using the original inputs and the reversed carry row.

def Cslib.Circuits.Boolean.CarryLookahead.finishCode (w : ℕ) : List (Op × List ℕ) × List ℕ

The full final-output code, including the carry-out reference.

theorem Cslib.Circuits.Boolean.CarryLookahead.computableInPolyTime_finish : Turing.MultiTapeTM.ComputableInPolyTime (fun (w : ℕ) => (finish w).code) Turing.MultiTapeTM.encUnary encCode

Native generation of sum-bit and carry-out wiring from unary width.

theorem Cslib.Circuits.Boolean.computableInPolyTime_carryLookahead : Turing.MultiTapeTM.ComputableInPolyTime (fun (w : ℕ) => (carryLookahead w).code) Turing.MultiTapeTM.encUnary encCode

One native polynomial-time algorithm generates the entire logarithmic-depth adder code from unary width. Every binary gate reference, output reference and framing bit is charged.

theorem Cslib.Circuits.Boolean.computableInPolyTime_carryLookaheadAdd : Turing.MultiTapeTM.ComputableInPolyTime (fun (w : ℕ) => (carryLookaheadAdd w).code) Turing.MultiTapeTM.encUnary encCode

The modular adder is generated by the same uniform native algorithm plus free output wiring and one hardwired carry gate.

theorem Cslib.Circuits.Boolean.computableInPolyTime_carryLookaheadFinish : Turing.MultiTapeTM.ComputableInPolyTime (fun (w : ℕ) => (carryLookaheadFinish w).code) Turing.MultiTapeTM.encUnary encCode

Generate the complete carry-save finishing code, including its repeated zero output wires.