Carry lookahead by parallel prefix doubling

A carry summary (g, p) acts on a carry c by g || (p && c). Summaries are composed in significance order. Each round doubles the interval summarized by each cell; cells without a neighbour retain their summary. The initial carry is an additional cell, so width zero still has one output: that carry.

The construction uses the associative carry-transfer operation underlying parallel-prefix addition Ladner and Fischer, Section 4. OR-propagate summaries represent the same carry functions. It uses the simple doubling network, rather than their optimized linear-size prefix network. All gates, including constants and negations, count.

Main definitions

• Cslib.Circuits.Boolean.CarryLookahead.step: one prefix-doubling circuit.
• Cslib.Circuits.Boolean.CarryLookahead.scan: the prefix circuit after a specified number of rounds.
• Cslib.Circuits.Boolean.carryLookahead: full addition with carry-in and carry-out.
• Cslib.Circuits.Boolean.carryLookaheadAdd: modular addition of two unsigned words.
• Cslib.Circuits.Boolean.carryLookaheadFinish: finish a carry-save pair in logarithmic depth.

Main results

• Cslib.Circuits.Boolean.val_eval_carryLookahead: exact unsigned addition at every width.
• Cslib.Circuits.Boolean.depth_carryLookahead_le, size_carryLookahead: depth at most 7 + 2 * clog 2 (w + 1) and exactly 15*w + 2*(w+1) + 3*(w+1)*clog 2 (w+1) gates.
• Cslib.Circuits.Boolean.val_eval_carryLookaheadAdd: addition modulo 2^w.
• Cslib.Circuits.Boolean.pairVal_eval_carryLookaheadFinish_csa4to2_mod: a finishing client for the existing carry-save reduction.

Native polynomial-time generation of the complete codes is proved in CarryLookahead.PolyTime.

References

• R. E. Ladner, M. J. Fischer, Parallel Prefix Computation

def Cslib.Circuits.Boolean.CarryLookahead.combine (high low : Bool × Bool) : Bool × Bool

Compose the high-significance summary with the low-significance summary.

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.combine_unit_left (a : Bool × Bool) : combine (false, true) a = a

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.combine_unit_right (a : Bool × Bool) : combine a (false, true) = a

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.combine_self (a : Bool × Bool) : combine a a = a

def Cslib.Circuits.Boolean.CarryLookahead.rangeSummary (row : ℕ → Bool × Bool) (start : ℕ) : ℕ → Bool × Bool

Consecutive carry summaries, with the most significant one first.

def Cslib.Circuits.Boolean.CarryLookahead.readRow {k : ℕ} (row : BitString (k + k)) (i : ℕ) : Bool × Bool

Read one summary from two equal-width rows, using the identity after the row ends.

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

The neighbour at the given distance, or the cell itself if the neighbour is absent.

def Cslib.Circuits.Boolean.CarryLookahead.generateFormula (k distance : ℕ) (i : Fin k) : Formula signature (k + k)

The generate output of one prefix cell. Inactive cells use idempotence to retain their value, so the scalar circuit has exactly two gates in either branch.

def Cslib.Circuits.Boolean.CarryLookahead.propagateFormula (k distance : ℕ) (i : Fin k) : Formula signature (k + k)

The propagate output of one prefix cell.

def Cslib.Circuits.Boolean.CarryLookahead.step (k distance : ℕ) : Circuit signature (k + k) (k + k)

One round of parallel carry composition, with all generate bits before all propagate bits.

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.size_step (k distance : ℕ) : (step k distance).size = 3 * k

theorem Cslib.Circuits.Boolean.CarryLookahead.depth_step_le (k distance : ℕ) : (step k distance).depth ≤ 2

def Cslib.Circuits.Boolean.CarryLookahead.scan (k a✝ : ℕ) : Circuit signature (k + k) (k + k)

The doubling network on an existing row of carry summaries.

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.size_scan (k t : ℕ) : (scan k t).size = 3 * k * t

theorem Cslib.Circuits.Boolean.CarryLookahead.depth_scan_le (k t : ℕ) : (scan k t).depth ≤ 2 * t

theorem Cslib.Circuits.Boolean.CarryLookahead.readRow_scan {k : ℕ} (row : BitString (k + k)) (t i : ℕ) : readRow ((scan k t).eval interpretation row) i = rangeSummary (readRow row) i (2 ^ t)

After t rounds every cell summarizes the next 2^t original cells, with identity padding.

def Cslib.Circuits.Boolean.CarryLookahead.leftInput (w : ℕ) (i : Fin w) : Fin (w + w + 1)

Input bit i of the first word.

def Cslib.Circuits.Boolean.CarryLookahead.rightInput (w : ℕ) (i : Fin w) : Fin (w + w + 1)

Input bit i of the second word.

def Cslib.Circuits.Boolean.CarryLookahead.initialGenerate (w : ℕ) (i : Fin (w + 1)) : Circuit signature (w + w + 1) 1

Generate one reversed input summary; the final cell supplies the incoming carry.

def Cslib.Circuits.Boolean.CarryLookahead.initialPropagate (w : ℕ) (i : Fin (w + 1)) : Circuit signature (w + w + 1) 1

Propagate one reversed input summary; the incoming carry is a constant transfer.

def Cslib.Circuits.Boolean.CarryLookahead.initial (w : ℕ) : Circuit signature (w + w + 1) (w + 1 + (w + 1))

Carry summaries in descending significance, followed by the incoming carry.

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.size_initialGenerate (w : ℕ) (i : Fin (w + 1)) : (initialGenerate w i).size = 1

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.size_initialPropagate (w : ℕ) (i : Fin (w + 1)) : (initialPropagate w i).size = 1

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.size_initial (w : ℕ) : (initial w).size = 2 * (w + 1)

theorem Cslib.Circuits.Boolean.CarryLookahead.depth_initial_le (w : ℕ) : (initial w).depth ≤ 1

def Cslib.Circuits.Boolean.CarryLookahead.carries (w : ℕ) : Circuit signature (w + w + 1) (w + 1 + (w + 1))

The carry network; w - i is the generate-wire index of the carry into bit i.

def Cslib.Circuits.Boolean.CarryLookahead.sumFormula (w : ℕ) (i : Fin w) : Formula signature (w + w + 1 + (w + 1 + (w + 1)))

One sum bit, reading the original inputs followed by the carry network.

def Cslib.Circuits.Boolean.CarryLookahead.finish (w : ℕ) : Circuit signature (w + w + 1 + (w + 1 + (w + 1))) (w + 1)

Convert carry summaries to sum bits and retain the final carry as the last output.

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.size_sumFormula (w : ℕ) (i : Fin w) : (sumFormula w i).size = 15

@[simp]

theorem Cslib.Circuits.Boolean.CarryLookahead.size_finish (w : ℕ) : (finish w).size = 15 * w

theorem Cslib.Circuits.Boolean.CarryLookahead.depth_finish_le (w : ℕ) : (finish w).depth ≤ 6

def Cslib.Circuits.Boolean.CarryLookahead.inputCarry {w : ℕ} (u : BitString (w + w + 1)) (i : ℕ) : Bool

The arithmetic carry into bit i, used only as the specification.

theorem Cslib.Circuits.Boolean.CarryLookahead.eval_carries {w : ℕ} (u : BitString (w + w + 1)) (i : Fin (w + 1)) : (carries w).eval interpretation u ⟨w - ↑i, ⋯⟩ = inputCarry u ↑i

The generate output at reversed index w-i is exactly carry i, including both endpoints.

def Cslib.Circuits.Boolean.carryLookahead (w : ℕ) : Circuit signature (w + w + 1) (w + 1)

Add two unsigned words and an input carry. Inputs are the first word, the second word, then one carry bit. Outputs are the low w sum bits followed by the output carry.

theorem Cslib.Circuits.Boolean.size_carryLookahead (w : ℕ) : (carryLookahead w).size = 15 * w + 2 * (w + 1) + 3 * (w + 1) * Nat.clog 2 (w + 1)

The exact number of gates in the doubling adder.

theorem Cslib.Circuits.Boolean.depth_carryLookahead_le (w : ℕ) : (carryLookahead w).depth ≤ 7 + 2 * Nat.clog 2 (w + 1)

Every gate has fan-in at most two, and the adder has logarithmic depth.

theorem Cslib.Circuits.Boolean.depth_carryLookahead_le_log (w : ℕ) : (carryLookahead w).depth ≤ 7 * (Nat.clog 2 (w + 1) + 1)

An explicit absolute-constant logarithmic depth bound, including width zero.

theorem Cslib.Circuits.Boolean.size_carryLookahead_le (w : ℕ) : (carryLookahead w).size ≤ 20 * (w + 1) ^ 2

A coarse polynomial bound on the complete adder's number of gates.

theorem Cslib.Circuits.Boolean.eval_carryLookahead_sum {w : ℕ} (u : BitString (w + w + 1)) (i : Fin w) : (carryLookahead w).eval interpretation u i.castSucc = (word (u ∘ CarryLookahead.leftInput w) + word (u ∘ CarryLookahead.rightInput w) + BitVec.setWidth w (BitVec.ofBool (u (Fin.last (w + w))))).getLsbD ↑i

Each low output bit is the sum bit with the specified incoming carry.

theorem Cslib.Circuits.Boolean.eval_carryLookahead_carry {w : ℕ} (u : BitString (w + w + 1)) : (carryLookahead w).eval interpretation u (Fin.last w) = CarryLookahead.inputCarry u w

The last output is the final carry, also at width zero.

theorem Cslib.Circuits.Boolean.val_eval_carryLookahead {w : ℕ} (a b : BitString w) (c : Bool) : ↑((BitString.equivFin (w + 1)) ((carryLookahead w).eval interpretation (Fin.append (Fin.append a b) fun (x : Fin 1) => c))) = ↑((BitString.equivFin w) a) + ↑((BitString.equivFin w) b) + c.toNat

Exact unsigned addition, including the output carry.

def Cslib.Circuits.Boolean.carryLookaheadAdd (w : ℕ) : Circuit signature (w + w) w

Discard the final carry and hardwire a false incoming carry.

theorem Cslib.Circuits.Boolean.val_eval_carryLookaheadAdd {w : ℕ} (a b : BitString w) : ↑((BitString.equivFin w) ((carryLookaheadAdd w).eval interpretation (Fin.append a b))) = (↑((BitString.equivFin w) a) + ↑((BitString.equivFin w) b)) % 2 ^ w

The modular result used to collapse a carry-save pair.

@[simp]

theorem Cslib.Circuits.Boolean.size_carryLookaheadAdd (w : ℕ) : (carryLookaheadAdd w).size = (carryLookahead w).size + 1

theorem Cslib.Circuits.Boolean.depth_carryLookaheadAdd_le (w : ℕ) : (carryLookaheadAdd w).depth ≤ 8 + 2 * Nat.clog 2 (w + 1)

theorem Cslib.Circuits.Boolean.depth_carryLookaheadAdd_le_log (w : ℕ) : (carryLookaheadAdd w).depth ≤ 8 * (Nat.clog 2 (w + 1) + 1)

An explicit absolute-constant depth bound for modular addition.

theorem Cslib.Circuits.Boolean.size_carryLookaheadAdd_le (w : ℕ) : (carryLookaheadAdd w).size ≤ 21 * (w + 1) ^ 2

Polynomial size after fixing the incoming carry and selecting the modular result.

def Cslib.Circuits.Boolean.carryLookaheadFinish (w : ℕ) : Circuit signature (w + w) (w + w)

A drop-in carry-save finisher: the first word is the modular sum and the second is zero.

@[simp]

theorem Cslib.Circuits.Boolean.size_carryLookaheadFinish (w : ℕ) : (carryLookaheadFinish w).size = (carryLookaheadAdd w).size + 1

Only one extra constant gate is needed to clear the second carry-save word.

theorem Cslib.Circuits.Boolean.depth_carryLookaheadFinish_le (w : ℕ) : (carryLookaheadFinish w).depth ≤ 8 + 2 * Nat.clog 2 (w + 1)

The carry-save finisher has logarithmic depth in the word width.

theorem Cslib.Circuits.Boolean.size_carryLookaheadFinish_le (w : ℕ) : (carryLookaheadFinish w).size ≤ 22 * (w + 1) ^ 2

A polynomial gate bound for the drop-in carry-save finisher.

theorem Cslib.Circuits.Boolean.pairVal_eval_carryLookaheadFinish_mod {w : ℕ} (p : BitString (w + w)) : pairVal ((carryLookaheadFinish w).eval interpretation p) % 2 ^ w = pairVal p % 2 ^ w

The replacement finishing stage preserves every carry-save value modulo 2^w.

theorem Cslib.Circuits.Boolean.sndBits_eval_carryLookaheadFinish {w : ℕ} (p : BitString (w + w)) : BitString.sndBits ((carryLookaheadFinish w).eval interpretation p) = fun (x : Fin w) => false

Every bit of the second output word is false after the logarithmic-depth finisher.

theorem Cslib.Circuits.Boolean.pairVal_eval_carryLookaheadFinish_csa4to2_mod {w : ℕ} (p q : BitString (w + w)) : pairVal (((carryLookaheadFinish w).comp (csa4to2 w)).eval interpretation (Fin.append p q)) % 2 ^ w = (pairVal p + pairVal q) % 2 ^ w

A 4-to-2 carry-save reduction followed by the new finisher computes the same modular sum. The existing carry-save circuit is unchanged.

theorem Cslib.Circuits.Boolean.depth_carryLookaheadFinish_comp_csa4to2_le (w : ℕ) : ((carryLookaheadFinish w).comp (csa4to2 w)).depth ≤ 20 + 2 * Nat.clog 2 (w + 1)

Finishing a 4-to-2 reduction adds only a constant to the logarithmic depth bound.