A circuit for one scheduler phase

The phase function next is synthesized stage by stage, each stage reading wires built by the earlier ones:

1. candidate bits: the target bits plus fixed offsets, one negation per set offset bit;
2. occupancy: one shared OR lookup of all candidates among the accepted line points (batchOrCircuit);
3. duplicates: for each menu entry, duplicate flags among its candidates (duplicateFlagsCircuit), with padding records marked by a tag bit;
4. clean flags, a disjunction over the scalars per request;
5. success: the clean flags of each entry, sorted, read at position ⌈2 ^ p / 2⌉ - 1;
6. the first successful entry, from shared prefix disjunctions;
7. the chosen clean flags and candidate lines, disjunctions over the entries;
8. the enriched pending records, sorted with clean records first.

phaseCost is the exact sum of the stage budgets; it counts every gate, including constants. The construction is existential and does not certify the running time of any constructor.

Main definitions

• Cslib.Circuits.Boolean.MassProduction.Scheduler.phaseCost: the phase gate budget.

Main results

• Cslib.Circuits.Boolean.MassProduction.Scheduler.exists_next_circuit: a circuit computing next within phaseCost gates.

References

• Adapted from MassProduction/Nonuniform/BufferedPhaseCost.lean, MassProduction/Nonuniform/BufferOccupancy.lean, MassProduction/Nonuniform/CandidateSelection.lean, MassProduction/Nonuniform/ConstantTranslations.lean and MassProduction/Nonuniform/MaskedOr.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.next_mem {K : Type u_1} [Field K] {ℓ b s D p a r : ℕ} (hk : a + BitonicSort.arity p = 2 ^ D) (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (menu : Fin r → Fin (BitonicSort.arity p) → Fin ℓ → K) {src : Set (BooleanFunction (2 ^ D * width D (ℓ * b) s))} (hin : inputs (2 ^ D * width D (ℓ * b) s) ⊆ src) (hsort : (Set.range fun (q : Fin (BitonicSort.arity p) × Fin (1 + width D (ℓ * b) s)) (x : BitString (2 ^ D * width D (ℓ * b) s)) => sortedPending hk bits scalar menu x q.1 q.2) ⊆ src) (q : Fin (2 ^ D * width D (ℓ * b) s)) : (fun (x : BitString (2 ^ D * width D (ℓ * b) s)) => next hk bits scalar menu x q) ∈ src

The phase output is available once the sorted pending records are.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.phaseCost (D L s p a r : ℕ) : ℕ

The gate budget of one phase with 2 ^ p pending and a accepted records and a menu of r entries: the sum of the eight stage budgets. It counts every gate, including constants.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.exists_next_circuit {K : Type u_1} [Field K] {ℓ b s D p a r : ℕ} (hk : a + BitonicSort.arity p = 2 ^ D) (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (menu : Fin r → Fin (BitonicSort.arity p) → Fin ℓ → K) : ∃ (c : Circuit signature (2 ^ D * width D (ℓ * b) s) (2 ^ D * width D (ℓ * b) s)), c.Computes interpretation (next hk bits scalar menu) ∧ c.size ≤ phaseCost D (ℓ * b) s p a r

One scheduler phase. Some circuit computes next exactly, on every input, within phaseCost gates; the size counts every gate, including constants.