Modular subtraction with carry lookahead

Subtract by complementing the second word and supplying an incoming carry of one. The output discards the final carry, so underflow wraps modulo 2 ^ w instead of truncated subtraction.

Main definitions

• Cslib.Circuits.Boolean.Modular.subtract: the modular subtraction circuit.

Main results

• Cslib.Circuits.Boolean.Modular.val_eval_subtract: exact modular subtraction on all words.
• Cslib.Circuits.Boolean.Modular.depth_subtract_le: depth at most 8 + 2 * clog 2 (w + 1).

References

Parallel-prefix finishing follows Ladner and Fischer.

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

Discard the carry-out after adding the first word, the second word's complement and one.

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

Modular subtraction, expressed without a truncated natural subtraction of the inputs.

theorem Cslib.Circuits.Boolean.Modular.depth_subtract_le (w : ℕ) : (subtract w).depth ≤ 8 + 2 * Nat.clog 2 (w + 1)

theorem Cslib.Circuits.Boolean.Modular.size_subtract_le (w : ℕ) : (subtract w).size ≤ 21 * (w + 1) ^ 2