Native generation of carry-save circuits

Fixed three-input formula templates generate each sum and carry bit. The lowest carry bit is a constant, so the carry blocks have different gate counts. appendCodes assembles their actual codes without padding. Composition then generates the existing four-to-two reducer.

The width is unary, and all emitted gate and output references are binary. These certificates charge the full code and hold uniformly at every width, including zero.

Main definitions

• Cslib.Circuits.Boolean.csa3to2Code: raw code generation for the three-to-two reducer.
• Cslib.Circuits.Boolean.csa4to2Code: raw code generation for the four-to-two reducer.

Main results

• Cslib.Circuits.Boolean.csa3to2Code_eq_code, Cslib.Circuits.Boolean.csa4to2Code_eq_code: exact agreement with the existing circuits.
• Cslib.Circuits.Boolean.computableInPolyTime_csa3to2, Cslib.Circuits.Boolean.computableInPolyTime_csa4to2: uniform native constructors.

References

The underlying carry-save circuits are formalized in Boolean.CarrySave, following Chandra, Stockmeyer and Vishkin and Vollmer, Chapter 1.

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

The sum-bit formula instantiated at three raw input references.

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

A carry-bit formula, including the constant lowest carry and total raw-index behavior.

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

Generate the full three-to-two carry-save circuit code from its width.

theorem Cslib.Circuits.Boolean.csa3to2Code_eq_code (w : ℕ) : csa3to2Code w = (csa3to2 w).code

Generation preserves the exact existing circuit, including its unequal carry-bit blocks.

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

The actual three-to-two reducer has a uniform native generator on unary widths.

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

Generate the existing two-layer carry-save reducer, including all input wiring.

theorem Cslib.Circuits.Boolean.csa4to2Code_eq_code (w : ℕ) : csa4to2Code w = (csa4to2 w).code

The generated code is exactly the existing four-to-two circuit's code.

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

The actual four-to-two reducer has a uniform native generator on unary widths.