Comparing and selecting words

Circuits over the De Morgan basis that compare words of w bits, read as numbers with the least significant bit first (BitString.equivFin), and select one of two words.

• The multiplexer muxCircuit w reads a control bit c and two words a and b, and outputs a when c is true and b otherwise. Bit i is (c ∧ a i) ∨ (¬c ∧ b i), with one negation of c shared by all bits: 3 w + 1 gates and depth at most 3.
• The comparator leCircuit w reads two words x and y and outputs whether x ≤ y. It scans the bits from the least significant: x ≤ y on the first k + 1 bits when x k < y k, or when x k = y k and x ≤ y on the first k bits; that is the majority of ¬x k, y k and the comparison of the first k bits. This costs five gates a bit and one for the comparison of empty words: 5 w + 1 gates and depth at most 4 w + 1.
• The minimum minCircuit w selects the smaller of two words, the first on ties: a comparator feeding a multiplexer, of 8 w + 2 gates. The keyed minimum keyedMinCircuit k p selects, of two records made of a key of k bits followed by a payload of p bits, the one with the smaller key, the first on ties, with 8 k + 3 p + 2 gates.

Zero-width words and keys are allowed; the comparator of empty words returns true. Pairwise keyed selection preserves the first payload on equal keys.

A balanced tree of keyed minimums selects a record with the least key among many (Cslib.Circuits.Boolean.tournamentCircuit).

Main definitions

• Cslib.Circuits.Boolean.muxCircuit, Cslib.Circuits.Boolean.leCircuit, Cslib.Circuits.Boolean.minCircuit, Cslib.Circuits.Boolean.keyedMinCircuit: the circuits.
• Cslib.BitString.recordKey, Cslib.BitString.keyedMinFn: the key of a record, and the record with the smaller key.

Main results

• Cslib.Circuits.Boolean.eval_muxCircuit, size_muxCircuit, depth_muxCircuit_le.
• Cslib.Circuits.Boolean.eval_leCircuit, size_leCircuit, depth_leCircuit_le.
• Cslib.Circuits.Boolean.eval_minCircuit, size_minCircuit, depth_minCircuit_le.
• Cslib.Circuits.Boolean.eval_keyedMinCircuit, size_keyedMinCircuit, depth_keyedMinCircuit_le.

References

Adapted from Samuel Schlesinger's earlier Complexitylib modules Circuits/{Multiplexer,BinaryComparison,BinaryMinimum,KeyedMinimum}.

The multiplexer

def Cslib.Circuits.Boolean.muxBit {w : ℕ} (i : Fin w) : Formula signature (1 + (w + w) + 1)

Bit i of the multiplexer, (c ∧ a i) ∨ (¬c ∧ b i), on the control c, the words a and b, and the negated control.

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

The multiplexer: reading a control bit c and words a and b, it outputs a when c is true and b otherwise.

@[simp]

theorem Cslib.Circuits.Boolean.eval_muxCircuit {w : ℕ} (c : Bool) (a b : BitString w) : (muxCircuit w).eval interpretation (Fin.append (fun (x : Fin 1) => c) (Fin.append a b)) = if c = true then a else b

@[simp]

theorem Cslib.Circuits.Boolean.size_muxCircuit (w : ℕ) : (muxCircuit w).size = 3 * w + 1

theorem Cslib.Circuits.Boolean.depth_muxCircuit_le (w : ℕ) : (muxCircuit w).depth ≤ 3

The comparator

def Cslib.Circuits.Boolean.leStepFormula : Formula signature (1 + 2 + 1)

One step of the comparator, on le, x k, y k and ¬x k: (¬x k ∧ y k) ∨ (le ∧ (¬x k ∨ y k)).

def Cslib.Circuits.Boolean.leStep : Circuit signature (1 + 2) 1

One step of the comparator: from whether x ≤ y on the bits below k, and from x k and y k, whether x ≤ y on the bits up to k.

theorem Cslib.Circuits.Boolean.eval_leStep (b c d : Bool) : leStep.eval interpretation (Fin.append (fun (x : Fin 1) => b) ![c, d]) = fun (x : Fin 1) => !c && d || b && (!c || d)

@[simp]

theorem Cslib.Circuits.Boolean.size_leStep : leStep.size = 5

theorem Cslib.Circuits.Boolean.depth_leStep_le : leStep.depth ≤ 4

def Cslib.Circuits.Boolean.lowBits (w : ℕ) : Fin (w + w) → Fin (w + 1 + (w + 1))

The first w bits of each of two words of w + 1 bits.

theorem Cslib.Circuits.Boolean.append_comp_lowBits {w : ℕ} (x y : BitString (w + 1)) : Fin.append x y ∘ lowBits w = Fin.append (Fin.init x) (Fin.init y)

def Cslib.Circuits.Boolean.topBits (w : ℕ) : Fin 2 → Fin (w + 1 + (w + 1))

The last bit of each of two words of w + 1 bits.

theorem Cslib.Circuits.Boolean.append_comp_topBits {w : ℕ} (x y : BitString (w + 1)) : Fin.append x y ∘ topBits w = ![x (Fin.last w), y (Fin.last w)]

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

The comparator: reading words x and y of w bits, it outputs whether x ≤ y as numbers with the least significant bit first.

@[simp]

theorem Cslib.Circuits.Boolean.eval_leCircuit {w : ℕ} (x y : BitString w) : (leCircuit w).eval interpretation (Fin.append x y) = fun (x_1 : Fin 1) => decide ((BitString.equivFin w) x ≤ (BitString.equivFin w) y)

@[simp]

theorem Cslib.Circuits.Boolean.size_leCircuit (w : ℕ) : (leCircuit w).size = 5 * w + 1

theorem Cslib.Circuits.Boolean.depth_leCircuit_le (w : ℕ) : (leCircuit w).depth ≤ 4 * w + 1

The minimum and the keyed minimum

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

The minimum: reading words x and y of w bits, it outputs the smaller, x on ties.

@[simp]

theorem Cslib.Circuits.Boolean.eval_minCircuit {w : ℕ} (x y : BitString w) : (minCircuit w).eval interpretation (Fin.append x y) = if (BitString.equivFin w) x ≤ (BitString.equivFin w) y then x else y

@[simp]

theorem Cslib.Circuits.Boolean.size_minCircuit (w : ℕ) : (minCircuit w).size = 8 * w + 2

theorem Cslib.Circuits.Boolean.depth_minCircuit_le (w : ℕ) : (minCircuit w).depth ≤ 4 * w + 4

def Cslib.Circuits.Boolean.keyBits (k p : ℕ) : Fin (k + k) → Fin (k + p + (k + p))

The keys of two records.

theorem Cslib.Circuits.Boolean.append_comp_keyBits {k p : ℕ} (r s : BitString (k + p)) : Fin.append r s ∘ keyBits k p = Fin.append r.recordKey s.recordKey

def Cslib.Circuits.Boolean.keyedMinCircuit (k p : ℕ) : Circuit signature (k + p + (k + p)) (k + p)

The keyed minimum: reading two records of a key of k bits followed by a payload of p bits, it outputs the one with the smaller key, the first on ties.

@[simp]

theorem Cslib.Circuits.Boolean.eval_keyedMinCircuit {k p : ℕ} (r s : BitString (k + p)) : (keyedMinCircuit k p).eval interpretation (Fin.append r s) = r.keyedMinFn s

@[simp]

theorem Cslib.Circuits.Boolean.size_keyedMinCircuit (k p : ℕ) : (keyedMinCircuit k p).size = 8 * k + 3 * p + 2

theorem Cslib.Circuits.Boolean.depth_keyedMinCircuit_le (k p : ℕ) : (keyedMinCircuit k p).depth ≤ 4 * k + 4