Native generation of carry-save reductions

The generator preserves the complete half-split reducer, its zero fallback and the final adder. Input counts and references are binary, word widths unary, and all supplied leaf code is charged.

Main results

• Cslib.Circuits.Boolean.sumPairsCode_eq_code: exact reduction and final-adder code.
• Cslib.Circuits.Boolean.computableInPolyTime_sumPairsCode: uniform native generation.

def Cslib.Circuits.Boolean.pairWithZeroCode (n w : ℕ) (C : List (Op × List ℕ) × List ℕ) : List (Op × List ℕ) × List ℕ

Add the shared zero word to any supplied raw leaf code.

theorem Cslib.Circuits.Boolean.pairWithZeroCode_eq_code {n w : ℕ} (C : Circuit signature n w) : pairWithZeroCode n w C.code = (pairWithZero C).code

Exact carry-save representation of the original leaf.

def Cslib.Circuits.Boolean.sumPairsCode (n w : ℕ) (leaves : List (List (Op × List ℕ) × List ℕ)) : List (Op × List ℕ) × List ℕ

Generate the entire balanced sum and final carry-lookahead adder.

theorem Cslib.Circuits.Boolean.sumPairsCode_eq_code {n w : ℕ} (cs : List (Circuit signature n (w + w))) : sumPairsCode n w (List.map Circuit.code cs) = (sumPairs n w cs).code

The raw generator preserves every original gate, fallback and output selector.

theorem Cslib.Circuits.Boolean.computableInPolyTime_pairWithZeroCode {α : Type} {enc : α ↪ List Bool} {n w : α → ℕ} {C : α → List (Op × List ℕ) × List ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hw : Turing.MultiTapeTM.ComputableInPolyTime w enc Turing.MultiTapeTM.encUnary) (hC : Turing.MultiTapeTM.ComputableInPolyTime C enc encCode) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => pairWithZeroCode (n a) (w a) (C a)) enc encCode

Pair generation charges all supplied leaf code.

theorem Cslib.Circuits.Boolean.computableInPolyTime_sumPairsCode {α : Type} {enc : α ↪ List Bool} {n w : α → ℕ} {cs : α → List (List (Op × List ℕ) × List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n enc Turing.MultiTapeTM.encNat) (hw : Turing.MultiTapeTM.ComputableInPolyTime w enc Turing.MultiTapeTM.encUnary) (hcs : Turing.MultiTapeTM.ComputableInPolyTime cs enc (Turing.MultiTapeTM.encList encCode)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => sumPairsCode (n a) (w a) (cs a)) enc encCode

The native generator charges the complete leaf list and both reduction stages.