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.synthesis_candidate {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) : Synthesis interpretation src (Set.range fun (q : Fin r × Fin (BitonicSort.arity p) × Fin s × Fin (ℓ * b)) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => candidate hk bits scalar menu x q.1 q.2.1 q.2.2.1 q.2.2.2) (r * BitonicSort.arity p * s * (ℓ * b))

Stage 1: each candidate bit is an input bit or its negation.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.synthesis_occupied {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) (hcand : (Set.range fun (q : Fin r × Fin (BitonicSort.arity p) × Fin s × Fin (ℓ * b)) (x : BitString (2 ^ D * width D (ℓ * b) s)) => candidate hk bits scalar menu x q.1 q.2.1 q.2.2.1 q.2.2.2) ⊆ src) : Synthesis interpretation src (Set.range fun (q : Fin r × Fin (BitonicSort.arity p) × Fin s) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => occupied hk bits scalar menu x q.1 q.2.1 q.2.2) (48 * (r * BitonicSort.arity p * s + a * s + 1) * (Nat.clog 2 (r * BitonicSort.arity p * s + a * s) + 1) ^ 2 * (ℓ * b + 1 + 1))

Stage 2: occupancy by one shared OR lookup among the accepted line points.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.synthesis_duplicate {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))} (hcand : (Set.range fun (q : Fin r × Fin (BitonicSort.arity p) × Fin s × Fin (ℓ * b)) (x : BitString (2 ^ D * width D (ℓ * b) s)) => candidate hk bits scalar menu x q.1 q.2.1 q.2.2.1 q.2.2.2) ⊆ src) : Synthesis interpretation src (Set.range fun (q : Fin r × Fin (BitonicSort.arity p) × Fin s) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => duplicate hk bits scalar menu x q.1 q.2.1 q.2.2) (r * ((duplicateFlagsCircuit id (Nat.clog 2 (BitonicSort.arity p * s))).size + 2))

Stage 3: for each menu entry, duplicate flags among its candidates. Padding records carry a true tag bit, so they never repeat a candidate.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.synthesis_clean {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))} (hocc : (Set.range fun (q : Fin r × Fin (BitonicSort.arity p) × Fin s) (x : BitString (2 ^ D * width D (ℓ * b) s)) => occupied hk bits scalar menu x q.1 q.2.1 q.2.2) ⊆ src) (hdup : (Set.range fun (q : Fin r × Fin (BitonicSort.arity p) × Fin s) (x : BitString (2 ^ D * width D (ℓ * b) s)) => duplicate hk bits scalar menu x q.1 q.2.1 q.2.2) ⊆ src) : Synthesis interpretation src (Set.range fun (q : Fin r × Fin (BitonicSort.arity p)) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => clean hk bits scalar menu x q.1 q.2) (r * BitonicSort.arity p * (2 * s + 2))

Stage 4: a request is clean when no candidate is occupied or a duplicate.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.synthesis_success {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))} (hclean : (Set.range fun (q : Fin r × Fin (BitonicSort.arity p)) (x : BitString (2 ^ D * width D (ℓ * b) s)) => clean hk bits scalar menu x q.1 q.2) ⊆ src) : Synthesis interpretation src (Set.range fun (e : Fin r) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => success hk bits scalar menu x e) (r * (bitonicSortCircuit id p false).size)

Stage 5: an entry succeeds when its sorted clean flags are true at position ⌈2 ^ p / 2⌉ - 1.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.synthesis_chosen {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))} (hsucc : (Set.range fun (e : Fin r) (x : BitString (2 ^ D * width D (ℓ * b) s)) => success hk bits scalar menu x e) ⊆ src) : Synthesis interpretation src (Set.range fun (e : Fin r) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => chosen hk bits scalar menu x e) (3 * r)

Stage 6: the first successful entry, from shared prefix disjunctions.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.synthesis_flag {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))} (hchosen : (Set.range fun (e : Fin r) (x : BitString (2 ^ D * width D (ℓ * b) s)) => chosen hk bits scalar menu x e) ⊆ src) (hclean : (Set.range fun (q : Fin r × Fin (BitonicSort.arity p)) (x : BitString (2 ^ D * width D (ℓ * b) s)) => clean hk bits scalar menu x q.1 q.2) ⊆ src) : Synthesis interpretation src (Set.range fun (i : Fin (BitonicSort.arity p)) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => flag hk bits scalar menu x i) (BitonicSort.arity p * (2 * r + 1))

Stage 7: the clean flag of each request for the chosen entry.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.synthesis_newLine {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))} (hchosen : (Set.range fun (e : Fin r) (x : BitString (2 ^ D * width D (ℓ * b) s)) => chosen hk bits scalar menu x e) ⊆ src) (hcand : (Set.range fun (q : Fin r × Fin (BitonicSort.arity p) × Fin s × Fin (ℓ * b)) (x : BitString (2 ^ D * width D (ℓ * b) s)) => candidate hk bits scalar menu x q.1 q.2.1 q.2.2.1 q.2.2.2) ⊆ src) : Synthesis interpretation src (Set.range fun (q : Fin (BitonicSort.arity p) × Fin s × Fin (ℓ * b)) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => newLine hk bits scalar menu x q.1 q.2.1 q.2.2) (BitonicSort.arity p * s * (ℓ * b) * (2 * r + 1))

Stage 7: the candidate line of each request for the chosen entry.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.synthesis_sortedPending {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) (hflag : (Set.range fun (i : Fin (BitonicSort.arity p)) (x : BitString (2 ^ D * width D (ℓ * b) s)) => flag hk bits scalar menu x i) ⊆ src) (hnew : (Set.range fun (q : Fin (BitonicSort.arity p) × Fin s × Fin (ℓ * b)) (x : BitString (2 ^ D * width D (ℓ * b) s)) => newLine hk bits scalar menu x q.1 q.2.1 q.2.2) ⊆ src) : Synthesis interpretation src (Set.range fun (q : Fin (BitonicSort.arity p) × Fin (1 + width D (ℓ * b) s)) (x : Fin (2 ^ D * width D (ℓ * b) s) → Bool) => sortedPending hk bits scalar menu x q.1 q.2) (bitonicSortCircuit flagKey p false).size

Stage 8: the enriched pending records, sorted with clean records first.

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.