Synthesis tools for the scheduler circuit

The scheduler uses the shared circuit synthesis rule (Synthesis.circuit), shared prefix disjunctions (Synthesis.prefixOr), and two facts about sorted arrays: a permuted finite array is a reindexing (List.Perm.exists_equiv_ofFn), and in an array of flags sorted with true flags first, a position holds a true flag exactly when it precedes the number of true flags (eq_true_iff_lt_card_of_sorted).

Gate counts are synthesis budgets: they count every gate, including constants, and do not certify the running time of any construction.

Main results

• Cslib.Circuits.Synthesis.prefixOr: all prefix disjunctions of r available functions.
• List.Perm.exists_equiv_ofFn: permuted finite arrays differ by a permutation of positions.
• Cslib.Circuits.Boolean.eq_true_iff_lt_card_of_sorted: positions of true sorted flags.
• Cslib.Circuits.Boolean.apply_zero_le_of_toLex_le: lexicographic order on one bit.
• Cslib.Circuits.Boolean.sort_flag_eq_true_iff: positions of true keys after sorting.

References

• Adapted from MassProduction/Nonuniform/FlagSelection.lean and MassProduction/Nonuniform/OrderedPermutation.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem List.Perm.exists_equiv_ofFn {α : Type u_1} {n : ℕ} {f g : Fin n → α} (h : (ofFn f).Perm (ofFn g)) : ∃ (σ : Equiv.Perm (Fin n)), ∀ (i : Fin n), f i = g (σ i)

Permuted finite arrays differ by a permutation of their positions.

theorem Cslib.Circuits.Boolean.eq_true_iff_lt_card_of_sorted {k : ℕ} (g : Fin k → Bool) (sorted : ∀ (i j : Fin k), i ≤ j → g i = false → g j = false) (j : Fin k) : g j = true ↔ ↑j < {i : Fin k | g i = true}.card

Every flag is false after a false flag; flags are sorted with true flags first.

theorem Cslib.Circuits.Boolean.apply_zero_le_of_toLex_le {x y : Fin 1 → Bool} (h : toLex x ≤ toLex y) : x 0 ≤ y 0

On one coordinate, lexicographic order is the order of the bit.

theorem Cslib.Circuits.Boolean.sort_flag_eq_true_iff {α : Type u_1} (φ : α → Fin 1 → Bool) (p : ℕ) (input : Fin (BitonicSort.arity p) → α) (j : Fin (BitonicSort.arity p)) : φ (BitonicSort.sort (fun (r : α) => toLex (φ r)) p false input j) 0 = true ↔ ↑j < {i : Fin (BitonicSort.arity p) | φ (input i) 0 = true}.card

Sorting records by a one-bit key with true keys first puts a true key at position j exactly when j is less than the number of true keys.

def Cslib.Circuits.Boolean.prefixOr {n r : ℕ} (F : Fin r → BooleanFunction n) (j : ℕ) : BooleanFunction n

The disjunction of the first j + 1 of r functions.

theorem Cslib.Circuits.Synthesis.prefixOr {n r : ℕ} {s : Set (BooleanFunction n)} (F : Fin r → BooleanFunction n) (hF : ∀ (e : Fin r), F e ∈ s) : Synthesis Boolean.interpretation s (Set.range fun (e : Fin r) => Boolean.prefixOr F ↑e) r

All prefix disjunctions of r available functions, sharing each prefix with the next: one OR gate per function after the first.