Recovery schedules

A scheduler circuit reads t target points and writes, for every request in its original position, the points of a punctured line through that request's target, such that the lines of distinct requests are disjoint (IsScheduler). Targets may repeat, and t may be zero. The directions are existential; only the listed points are outputs.

Main definitions

• Cslib.Circuits.Boolean.MassProduction.IsScheduler: the scheduler specification.

References

• Adapted from the scheduler contracts of MassProduction/Nonuniform/SchedulerCircuit.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.Circuits.Boolean.MassProduction.IsScheduler {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ b s t : ℕ} (bits : K ≃+ BitString b) (scalar : Fin s ≃ { c : K // c ≠ 0 }) (c : Circuit signature (t * (ℓ * b)) (t * (s * (ℓ * b)))) : Prop

A scheduler maps every batch of t targets to listed punctured lines through them, with nonzero directions and pairwise disjoint lines, keeping every request in its original position. The lines are listed in the order of the bijection scalar onto the nonzero scalars.