Linear scans for a least state and a first flagged position

A linear scan keeps the least of a sequence of values (scanMin). For bit strings ordered lexicographically with coordinate zero most significant (lexOrder), each step compares the next state with the current minimum once and selects one of them, at 10 * n + 1 gates for n-bit states (synthesis_scanMin). Scanning the records in reverse order selects the first flagged one (chooseFirst), and the first flagged position, written in binary, costs four gates per position and bit (synthesis_firstIndex).

All gates of the native De Morgan basis, including constants, are charged; wiring and fanout are free.

Main definitions

• Cslib.Circuits.Boolean.Iteration.lexOrder: the lexicographic order on bit strings.
• Cslib.Circuits.Boolean.Iteration.scanMin: the least of the first values and a fallback.
• Cslib.Circuits.Boolean.Iteration.chooseFirst: the first flagged record.
• Cslib.Circuits.Boolean.Iteration.firstIndex: the first flagged position as a word.

Main results

• Cslib.Circuits.Boolean.Iteration.scanMin_spec: the scan is a least value.
• Cslib.Circuits.Boolean.Iteration.chooseFirst_spec, firstIndex_spec: the first flagged record and position.
• Cslib.Circuits.Boolean.Iteration.synthesis_scanMin, Cslib.Circuits.Boolean.Iteration.synthesis_firstIndex: their gate counts.

References

• Adapted from lean/Proofs/ScanSelection.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

@[reducible, inline]

noncomputable abbrev Cslib.Circuits.Boolean.Iteration.lexOrder (n : ℕ) : LinearOrder (BitString n)

The lexicographic order on bit strings, with coordinate zero most significant and false below true.

Least values

def Cslib.Circuits.Boolean.Iteration.scanMin {α : Type u_1} [LinearOrder α] {R : ℕ} (values : Fin R → α) (fallback : α) : ℕ → α

The least of the values at positions below t and the fallback.

theorem Cslib.Circuits.Boolean.Iteration.scanMin_spec {α : Type u_1} [LinearOrder α] {R : ℕ} (values : Fin R → α) (fallback : α) (t : ℕ) : (scanMin values fallback t = fallback ∨ ∃ (j : Fin R), ↑j < t ∧ scanMin values fallback t = values j) ∧ scanMin values fallback t ≤ fallback ∧ ∀ (j : Fin R), ↑j < t → scanMin values fallback t ≤ values j

The scan is the fallback or one of the scanned values, and below all of them.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_lexLt {n a : ℕ} (s : Set (BooleanFunction a)) (x y : BitString a → BitString n) (hx : wires x ⊆ s) (hy : wires y ⊆ s) : Synthesis interpretation s {fun (z : BitString a) => decide (toLex (x z) < toLex (y z))} (6 * n + 1)

Lexicographic comparison of two available bit strings, by the native comparison formula.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_scanMin {n a R : ℕ} (s : Set (BooleanFunction a)) (values : BitString a → Fin R → BitString n) (fallback : BitString a → BitString n) (hv : ∀ (j : Fin R) (bit : Fin n), (fun (x : BitString a) => values x j bit) ∈ s) (hf : ∀ (bit : Fin n), (fun (x : BitString a) => fallback x bit) ∈ s) : Synthesis interpretation s (wires fun (x : BitString a) => scanMin (values x) (fallback x) R) (R * (10 * n + 1))

Minimum scan. The lexicographically least of R available states and a fallback costs one comparison and one selection per state.

First flagged positions

theorem Cslib.Circuits.Boolean.Iteration.chooseRecord_eq_of_last {R : ℕ} {α : Type u_1} (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) (j : Fin R) (hj : flags j = true) (t : ℕ) (hjt : ↑j < t) (hlast : ∀ (i : Fin R), ↑j < ↑i → ↑i < t → flags i = false) : chooseRecord flags records fallback t = records j

If position j is flagged and no later position below t is, the scan returns its record.

def Cslib.Circuits.Boolean.Iteration.chooseFirst {R : ℕ} {α : Type u_1} (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) : α

The first flagged record, or the fallback if none is flagged: the last flagged record in reverse order.

theorem Cslib.Circuits.Boolean.Iteration.chooseFirst_spec {R : ℕ} {α : Type u_1} (flags : Fin R → Bool) (records : Fin R → α) (fallback : α) (j : Fin R) (hj : flags j = true) (hfirst : ∀ (i : Fin R), ↑i < ↑j → flags i = false) : chooseFirst flags records fallback = records j

def Cslib.Circuits.Boolean.Iteration.firstIndex {R w : ℕ} (flags : Fin R → Bool) : BitVec w

The first flagged position in w bits, or zero if none is flagged.

theorem Cslib.Circuits.Boolean.Iteration.firstIndex_spec {R w : ℕ} (flags : Fin R → Bool) (j : Fin R) (hj : flags j = true) (hfirst : ∀ (i : Fin R), ↑i < ↑j → flags i = false) : firstIndex flags = BitVec.ofNat w ↑j

theorem Cslib.Circuits.Boolean.Iteration.synthesis_firstIndex {a R w : ℕ} (s : Set (BooleanFunction a)) (flags : BitString a → Fin R → Bool) (hf : ∀ (j : Fin R), (fun (x : BitString a) => flags x j) ∈ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) : Synthesis interpretation s (wordWires fun (x : BitString a) => firstIndex (flags x)) (R * (4 * w))

The first flagged position among R available flags costs four gates per position and bit.