One scheduler phase

A phase starts from a state whose first a records are accepted and whose last 2 ^ p records are pending, and tests a fixed menu of direction tuples for the pending requests. For every menu entry e, pending request i and scalar index c, the candidate point is the target of i plus scalar c • menu e i; its bits are the target bits plus a fixed offset. A candidate is occupied when it lies on an accepted line, and a duplicate when another request's candidate for the same entry is the same point. A request is clean for an entry when none of its candidates is occupied or a duplicate; this is exactly LineCode.IsClean (clean_iff). An entry succeeds when at least half of the requests are clean, and the first successful entry is chosen. The pending records, with their candidate lines for the chosen entry and their clean flags, are sorted with clean records first; the first ⌈2 ^ p / 2⌉ of them are accepted (next).

For a universal menu some entry succeeds, so every accepted record is clean, which keeps the state good (good_next).

Main definitions

• Cslib.Circuits.Boolean.MassProduction.Scheduler.candidate: the bits of a candidate point.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.clean: the clean flags.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.chosen: the first successful entry.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.next: the state after the phase.

Main results

• Cslib.Circuits.Boolean.MassProduction.Scheduler.clean_iff: clean flags are IsClean.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.good_next: a phase keeps the state good.

References

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

def Cslib.Circuits.Boolean.MassProduction.Scheduler.pending {D p a : ℕ} (hk : a + BitonicSort.arity p = 2 ^ D) (i : Fin (BitonicSort.arity p)) : Fin (2 ^ D)

The position of pending request i.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.accepted {D p a : ℕ} (hk : a + BitonicSort.arity p = 2 ^ D) (m : Fin a) : Fin (2 ^ D)

The position of accepted request m.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (e : Fin r) (i : Fin (BitonicSort.arity p)) (c : Fin s) : BitString (ℓ * b)

The bits of candidate point c of request i for menu entry e: the target bits plus the fixed bits of scalar c • menu e i.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (e : Fin r) (i : Fin (BitonicSort.arity p)) (c : Fin s) : Bool

A candidate lies on an accepted line.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (e : Fin r) (i : Fin (BitonicSort.arity p)) (c : Fin s) : Bool

Another candidate of the same menu entry is the same point.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (e : Fin r) (i : Fin (BitonicSort.arity p)) : Bool

No candidate of request i for entry e is occupied or a duplicate.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (e : Fin r) : Bool

At least half of the pending requests are clean for entry e.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (e : Fin r) : Bool

Entry e is the first successful entry.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (i : Fin (BitonicSort.arity p)) : Bool

Request i is clean for the chosen entry.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (i : Fin (BitonicSort.arity p)) (c : Fin s) (β : Fin (ℓ * b)) : Bool

Bit β of candidate point c of request i for the chosen entry.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.enriched {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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (i : Fin (BitonicSort.arity p)) : BitString (1 + width D (ℓ * b) s)

A pending record with its clean flag in front and its candidate line for the chosen entry.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.flagKey {ℓ b s D : ℕ} : Fin 1 → Fin (1 + width D (ℓ * b) s)

The flag key of an enriched record.

noncomputable def Cslib.Circuits.Boolean.MassProduction.Scheduler.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) (x : BitString (2 ^ D * width D (ℓ * b) s)) : Fin (BitonicSort.arity p) → BitString (1 + width D (ℓ * b) s)

The enriched pending records, sorted with clean records first.

noncomputable def Cslib.Circuits.Boolean.MassProduction.Scheduler.next {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) (x : BitString (2 ^ D * width D (ℓ * b) s)) : BitString (2 ^ D * width D (ℓ * b) s)

The state after the phase: accepted records stay, and the sorted enriched pending records follow without their flags.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.val_pending {D p a : ℕ} {hk : a + BitonicSort.arity p = 2 ^ D} (i : Fin (BitonicSort.arity p)) : ↑(pending hk i) = a + ↑i

Pending request i sits i positions after the accepted block.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.val_accepted {D p a : ℕ} {hk : a + BitonicSort.arity p = 2 ^ D} (m : Fin a) : ↑(accepted hk m) = ↑m

Accepted request m sits at position m.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.accepted_or_pending {D p a : ℕ} {hk : a + BitonicSort.arity p = 2 ^ D} (m : Fin (2 ^ D)) : (∃ (m' : Fin a), m = accepted hk m') ∨ ∃ (i : Fin (BitonicSort.arity p)), m = pending hk i

Every position is accepted or pending.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.next_accepted {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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (m : Fin a) (f : Fin (width D (ℓ * b) s)) : next hk bits scalar menu x (finProdFinEquiv (accepted hk m, f)) = x (finProdFinEquiv (accepted hk m, f))

A phase keeps the accepted records.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.next_pending {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) (x : BitString (2 ^ D * width D (ℓ * b) s)) (j : Fin (BitonicSort.arity p)) (f : Fin (width D (ℓ * b) s)) : next hk bits scalar menu x (finProdFinEquiv (pending hk j, f)) = sortedPending hk bits scalar menu x j (Fin.natAdd 1 f)

After a phase, the pending block holds the sorted enriched records without their flags.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.acceptedLines {K : Type u_1} {ℓ D : ℕ} (a : ℕ) (T dirs : Fin (2 ^ D) → Fin ℓ → K) : Fin (2 ^ D) → Option ((Fin ℓ → K) × (Fin ℓ → K))

The accepted lines of a state, padded by unused slots.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.mem_occupiedPoints_acceptedLines {K : Type u_1} [Field K] {ℓ D a : ℕ} [Fintype K] [DecidableEq K] {T dirs : Fin (2 ^ D) → Fin ℓ → K} {w : Fin ℓ → K} : w ∈ LineCode.occupiedPoints (acceptedLines a T dirs) ↔ ∃ (m : Fin (2 ^ D)), ↑m < a ∧ w ∈ LineCode.puncturedLine (T m) (dirs m)

The occupied points are the points of the accepted lines.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.candidate_eq {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) {x : BitString (2 ^ D * width D (ℓ * b) s)} {T : Fin (2 ^ D) → Fin ℓ → K} (htarget : ∀ (m : Fin (2 ^ D)), target x m = BitString.pointBits bits (T m)) (e : Fin r) (i : Fin (BitonicSort.arity p)) (c : Fin s) : candidate hk bits scalar menu x e i c = BitString.pointBits bits (T (pending hk i) + ↑(scalar c) • menu e i)

A candidate lists the bits of its point.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.occupied_iff {K : Type u_1} [Field K] {ℓ b s D p a r : ℕ} {hk : a + BitonicSort.arity p = 2 ^ D} [Fintype K] [DecidableEq K] (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (menu : Fin r → Fin (BitonicSort.arity p) → Fin ℓ → K) {x : BitString (2 ^ D * width D (ℓ * b) s)} {T dirs : Fin (2 ^ D) → Fin ℓ → K} (htarget : ∀ (m : Fin (2 ^ D)), target x m = BitString.pointBits bits (T m)) (hline : ∀ (m : Fin (2 ^ D)), ↑m < a → dirs m ≠ 0 ∧ ∀ (c : Fin s), line x m c = BitString.pointBits bits (T m + ↑(scalar c) • dirs m)) (e : Fin r) (i : Fin (BitonicSort.arity p)) (c : Fin s) : occupied hk bits scalar menu x e i c = true ↔ T (pending hk i) + ↑(scalar c) • menu e i ∈ LineCode.occupiedPoints (acceptedLines a T dirs)

A candidate is occupied exactly when its point lies on an accepted line.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.duplicate_iff {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) {x : BitString (2 ^ D * width D (ℓ * b) s)} {T : Fin (2 ^ D) → Fin ℓ → K} (htarget : ∀ (m : Fin (2 ^ D)), target x m = BitString.pointBits bits (T m)) (e : Fin r) (i : Fin (BitonicSort.arity p)) (c : Fin s) : duplicate hk bits scalar menu x e i c = true ↔ ∃ (i' : Fin (BitonicSort.arity p)) (c' : Fin s), (i', c') ≠ (i, c) ∧ T (pending hk i') + ↑(scalar c') • menu e i' = T (pending hk i) + ↑(scalar c) • menu e i

A candidate is a duplicate exactly when another candidate of its entry is the same point.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.clean_iff {K : Type u_1} [Field K] {ℓ b s D p a r : ℕ} {hk : a + BitonicSort.arity p = 2 ^ D} [Fintype K] [DecidableEq K] (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (menu : Fin r → Fin (BitonicSort.arity p) → Fin ℓ → K) {x : BitString (2 ^ D * width D (ℓ * b) s)} {T dirs : Fin (2 ^ D) → Fin ℓ → K} (htarget : ∀ (m : Fin (2 ^ D)), target x m = BitString.pointBits bits (T m)) (hline : ∀ (m : Fin (2 ^ D)), ↑m < a → dirs m ≠ 0 ∧ ∀ (c : Fin s), line x m c = BitString.pointBits bits (T m + ↑(scalar c) • dirs m)) (hmenu : ∀ (e : Fin r) (i : Fin (BitonicSort.arity p)), menu e i ≠ 0) (e : Fin r) (i : Fin (BitonicSort.arity p)) : clean hk bits scalar menu x e i = true ↔ LineCode.IsClean (LineCode.occupiedPoints (acceptedLines a T dirs)) (fun (i : Fin (BitonicSort.arity p)) => T (pending hk i)) (menu e) i

The clean flags are exactly the clean requests of LineCode.IsClean, for nonzero menu directions.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.good_next {K : Type u_1} [Field K] {ℓ b s D p a r : ℕ} {hk : a + BitonicSort.arity p = 2 ^ D} [Fintype K] [DecidableEq K] (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (menu : Fin r → Fin (BitonicSort.arity p) → Fin ℓ → K) (hmenu : LineCode.IsUniversalMenu (2 ^ D) menu) {targets : Fin (2 ^ D) → Fin ℓ → K} {x : BitString (2 ^ D * width D (ℓ * b) s)} (hx : Good bits scalar targets a x) : Good bits scalar targets (a + (BitonicSort.arity p + 1) / 2) (next hk bits scalar menu x)

A phase with a universal menu keeps the state good and accepts ⌈2 ^ p / 2⌉ more requests.