A near-linear nonuniform scheduler circuit

For 2 ^ D requests, a fixed De Morgan circuit maps the bits of arbitrary target points of K ^ ℓ, which may repeat, to listed punctured lines through them with nonzero directions and pairwise disjoint lines, in the original request order (IsScheduler). Universal menus of direction tuples are a hypothesis: for every 0 < k ≤ 2 ^ D pending requests some menu of r entries with k * r ≤ 2 ^ D * (2 + 3 ℓ b) + 2 k serves every state with 2 ^ D occupied lines.

The circuit labels every request with its position, then runs D + 1 phases with 2 ^ D, 2 ^ (D - 1), …, 1 pending requests. Each phase tests its menu and accepts the clean half of the pending requests (Scheduler.next), keeping the state good (Scheduler.good_next). Finally the records are sorted by label, which returns every request's line to its original position (Scheduler.finalOutput_eq_lineBits).

The size counts every gate, including constants, and is at most 524288 * 2 ^ D * (s + 1) * (D + ℓ * b + 2) ^ 5 (schedulerBound). The circuit is obtained existentially from synthesis bounds; its size does not certify the running time of any constructor.

Main definitions

• Cslib.Circuits.Boolean.MassProduction.schedulerBound: the gate bound.

Main results

• Cslib.Circuits.Boolean.MassProduction.exists_isScheduler: a scheduler circuit within schedulerBound gates.

References

• Adapted from MassProduction/Nonuniform/SchedulerCircuit.lean, MassProduction/Nonuniform/BufferIteration.lean and 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.exists_finalOutput_circuit (D L s : ℕ) : ∃ (c : Circuit signature (2 ^ D * width D L s) (2 ^ D * (s * L))), c.Computes interpretation finalOutput ∧ c.size ≤ (D + 1) ^ 2 * 2 ^ D * (2 * D + 2 * width D L s + 1)

Some circuit computes finalOutput exactly, by sorting the records by label and reading every request's line from the rank of its label, within the displayed number of gates.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.exists_phases_circuit {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b s D : ℕ} (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (hmenu : ∀ (k : ℕ), 0 < k → k ≤ 2 ^ D → ∃ (r : ℕ), k * r ≤ 2 ^ D * (2 + 3 * (ℓ * b)) + 2 * k ∧ ∃ (menu : Fin r → Fin k → Fin ℓ → K), LineCode.IsUniversalMenu (2 ^ D) menu) (hs : s < 2 ^ b) (p : ℕ) (hp : p ≤ D) : ∃ (c : Circuit signature (2 ^ D * width D (ℓ * b) s) (2 ^ D * width D (ℓ * b) s)), (∀ (targets : Fin (2 ^ D) → Fin ℓ → K) (x : BitString (2 ^ D * width D (ℓ * b) s)), Good bits scalar targets (2 ^ D - BitonicSort.arity p) x → Good bits scalar targets (2 ^ D) (c.eval interpretation x)) ∧ c.size ≤ (p + 1) * (16384 * 2 ^ D * (s + 1) * (D + ℓ * b + b + 2) ^ 4)

The phases with 2 ^ p, 2 ^ (p - 1), …, 1 pending requests accept every remaining request: some circuit maps every good state with 2 ^ D - 2 ^ p accepted records to a good state with all records accepted, within p + 1 phase budgets.

def Cslib.Circuits.Boolean.MassProduction.schedulerBound (D ℓ b s : ℕ) : ℕ

The gate bound of the scheduler: 524288 * 2 ^ D * (s + 1) * (D + ℓ * b + 2) ^ 5.

theorem Cslib.Circuits.Boolean.MassProduction.exists_isScheduler {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b s D : ℕ} (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (hmenu : ∀ (k : ℕ), 0 < k → k ≤ 2 ^ D → ∃ (r : ℕ), k * r ≤ 2 ^ D * (2 + 3 * (ℓ * b)) + 2 * k ∧ ∃ (menu : Fin r → Fin k → Fin ℓ → K), LineCode.IsUniversalMenu (2 ^ D) menu) : ∃ (c : Circuit signature (2 ^ D * (ℓ * b)) (2 ^ D * (s * (ℓ * b)))), IsScheduler bits scalar c ∧ c.size ≤ schedulerBound D ℓ b s

A near-linear scheduler circuit. Given universal menus for every number 0 < k ≤ 2 ^ D of pending requests, of r entries with k * r ≤ 2 ^ D * (2 + 3 ℓ b) + 2 k, some De Morgan circuit schedules 2 ^ D requests: for all targets, repeated or not, it outputs in the original order listed punctured lines through them with nonzero directions and pairwise disjoint lines. Its size, counting every gate including constants, is at most schedulerBound D ℓ b s.