Gate budgets of the scheduler

A phase with 2 ^ p ≤ 2 ^ D pending requests and a menu of r entries, where 2 ^ p * r ≤ 2 ^ D * (2 + 3 L) + 2 ^ (p + 1), costs at most 16384 * 2 ^ D * (s + 1) * (D + L + b + 2) ^ 4 gates when s < 2 ^ b (phaseCost_le). A sort of 2 ^ p records of width R by k key bits costs at most (p + 1) ^ 2 * 2 ^ p * (2 k + 2 R + 1) gates (size_bitonicSortCircuit_le). These count every gate, including constants; the factors are crude.

Main results

• Cslib.Circuits.Boolean.MassProduction.Scheduler.size_bitonicSortCircuit_le: sorting.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.phaseCost_le: the phase budget.

References

• Adapted from MassProduction/Nonuniform/BufferIterationCost.lean in S. Schlesinger, Boolean circuit mass production formalization, using the sorting network of K. E. Batcher, Sorting Networks and Their Applications.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.size_bitonicSortCircuit_le {k R : ℕ} (key : Fin k → Fin R) (p : ℕ) (ascending : Bool) : (bitonicSortCircuit key p ascending).size ≤ (p + 1) ^ 2 * 2 ^ p * (2 * k + 2 * R + 1)

A sort of 2 ^ p records of width R by k key bits uses at most (p + 1) ^ 2 * 2 ^ p * (2 * k + 2 * R + 1) gates.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.phaseCost_le {D L b s p a r : ℕ} (hk : a + BitonicSort.arity p = 2 ^ D) (hr : BitonicSort.arity p * r ≤ 2 ^ D * (2 + 3 * L) + 2 * BitonicSort.arity p) (hs : s < 2 ^ b) : phaseCost D L s p a r ≤ 16384 * 2 ^ D * (s + 1) * (D + L + b + 2) ^ 4

The phase budget. Under the menu-size bound and s < 2 ^ b, one phase costs at most 16384 * 2 ^ D * (s + 1) * (D + L + b + 2) ^ 4 gates, counting every gate.