Scheduler states

The scheduler keeps 2 ^ D records in fixed positions. A record holds the D-bit label of its original request, the bits of that request's target point, and s listed points of a line. The first a positions hold accepted requests. Good targets a x says that the records are a permutation of the labelled requests, that every accepted record lists the punctured line through its target with some nonzero direction, and that accepted lines are pairwise disjoint.

The initial state lists every request in its original position, with no accepted line. When all records are accepted, sorting by label restores the original order: each label has a fixed rank (rank), so a final wiring reads every request's line from its sorted position (finalOutput).

Main definitions

• Cslib.Circuits.Boolean.MassProduction.Scheduler.width: the record width.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.Good: the scheduler invariant.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.initialSubstitution: the initial records.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.finalOutput: lines in original order.

Main results

• Cslib.Circuits.Boolean.MassProduction.Scheduler.good_initial: the initial state is good.
• Cslib.Circuits.Boolean.MassProduction.Scheduler.finalOutput_eq_lineBits: a fully accepted good state yields a valid schedule.

References

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

Points

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.mem_puncturedLine_iff {K : Type u_1} [Field K] {ℓ s : ℕ} [Fintype K] [DecidableEq K] (scalar : Fin s ≃ { c : K // c ≠ 0 }) {u v w : Fin ℓ → K} : w ∈ LineCode.puncturedLine u v ↔ ∃ (c : Fin s), u + ↑(scalar c) • v = w

The punctured line lists the points u + scalar c • v.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.add_smul_injective {K : Type u_1} [Field K] {ℓ s : ℕ} (scalar : Fin s ≃ { c : K // c ≠ 0 }) {u v : Fin ℓ → K} (hv : v ≠ 0) : Function.Injective fun (c : Fin s) => u + ↑(scalar c) • v

A line with a nonzero direction lists distinct points.

Records

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.MassProduction.Scheduler.width (D L s : ℕ) : ℕ

A record: D label bits, a target point of L bits, and s listed points.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.labelBit {s D L : ℕ} (j : Fin D) : Fin (width D L s)

The position of a label bit in a record.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.targetBit {s D L : ℕ} (β : Fin L) : Fin (width D L s)

The position of a target bit in a record.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.lineBit {s D L : ℕ} (c : Fin s) (β : Fin L) : Fin (width D L s)

The position of a bit of a listed point in a record.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.label {s D t L : ℕ} (x : BitString (t * width D L s)) (m : Fin t) : BitString D

The label bits of record m.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.target {s D t L : ℕ} (x : BitString (t * width D L s)) (m : Fin t) : BitString L

The target bits of record m.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.line {s D t L : ℕ} (x : BitString (t * width D L s)) (m : Fin t) (c : Fin s) : BitString L

The bits of listed point c of record m.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.encode (D : ℕ) (i : Fin (2 ^ D)) : BitString D

The label of an original request: its binary numbering.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.encode_injective {D : ℕ} : Function.Injective (encode D)

Distinct requests have distinct labels.

def Cslib.Circuits.Boolean.MassProduction.Scheduler.Good {K : Type u_1} [Field K] {ℓ b s D : ℕ} [Fintype K] [DecidableEq K] (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (targets : Fin (2 ^ D) → Fin ℓ → K) (a : ℕ) (x : BitString (2 ^ D * width D (ℓ * b) s)) : Prop

The state invariant after a acceptances: the records are a permutation π of the labelled requests, every accepted record lists the punctured line through its target with a nonzero direction, and accepted lines are pairwise disjoint.

The initial state

def Cslib.Circuits.Boolean.MassProduction.Scheduler.initialSubstitution (D L s : ℕ) : Fin (2 ^ D * width D L s) → Fin (2 ^ D * L) ⊕ Bool

The initial records: each request in its original position, labelled by its position, with its target bits and an empty line.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.good_initial {K : Type u_1} [Field K] {ℓ b s D : ℕ} [Fintype K] [DecidableEq K] (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (targets : Fin (2 ^ D) → Fin ℓ → K) : Good bits scalar targets 0 (substitute (initialSubstitution D (ℓ * b) s) (BitString.targetBits bits targets))

The initial state is good with no accepted requests.

Restoring the original order

noncomputable def Cslib.Circuits.Boolean.MassProduction.Scheduler.rank {D : ℕ} (i : Fin (2 ^ D)) : Fin (2 ^ D)

The sorted position of a label: the number of smaller labels.

noncomputable def Cslib.Circuits.Boolean.MassProduction.Scheduler.sortedByLabel {s D L : ℕ} (x : BitString (2 ^ D * width D L s)) : Fin (BitonicSort.arity D) → BitString (width D L s)

Records sorted by label.

noncomputable def Cslib.Circuits.Boolean.MassProduction.Scheduler.finalOutput {s D L : ℕ} (x : BitString (2 ^ D * width D L s)) : BitString (2 ^ D * (s * L))

Every request's listed line, read from its label's sorted position.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.sortedByLabel_rank {s D L : ℕ} {x : BitString (2 ^ D * width D L s)} (π : Equiv.Perm (Fin (2 ^ D))) (hlabel : ∀ (m : Fin (2 ^ D)), label x m = encode D (π m)) (i : Fin (2 ^ D)) : sortedByLabel x (Fin.cast ⋯ (rank i)) = fun (f : Fin (width D L s)) => x (finProdFinEquiv ((Equiv.symm π) i, f))

Sorting by distinct labels places the record of request i at its rank.

theorem Cslib.Circuits.Boolean.MassProduction.Scheduler.finalOutput_eq_lineBits {K : Type u_1} [Field K] {ℓ b s D : ℕ} [Fintype K] [DecidableEq K] (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) {targets : Fin (2 ^ D) → Fin ℓ → K} {x : BitString (2 ^ D * width D (ℓ * b) s)} (hx : Good bits scalar targets (2 ^ D) x) : ∃ (directions : Fin (2 ^ D) → Fin ℓ → K), (∀ (i : Fin (2 ^ D)), directions i ≠ 0) ∧ (∀ (i j : Fin (2 ^ D)), i ≠ j → Disjoint (LineCode.puncturedLine (targets i) (directions i)) (LineCode.puncturedLine (targets j) (directions j))) ∧ finalOutput x = BitString.lineBits bits (fun (c : Fin s) => ↑(scalar c)) targets directions

When every record is accepted, the final output lists, for every request in its original position, a punctured line through its target; the lines have nonzero directions and are pairwise disjoint.