The scheduled recovery circuit

One circuit answers t requests Fin.append a z to a packed function (see MassProduction.Pipeline.Packing), keeping every request in its input position:

1. a shared table maps every prefix a to its target point, copy and bit position (lookupStage, by batchLookupCircuit);
2. a scheduler lists the points of pairwise disjoint punctured lines through the targets (scheduleStage);
3. every incidence of a request with a point of its line sends the request's suffix to the slot of its copy and point (scatterCircuit); since the lines are disjoint, a slot receives the suffix of at most one request, and unused slots receive zeros;
4. every slot evaluates every resource of its copy and point on its suffix once (bankCircuit), from caller-supplied resource circuits;
5. every incidence reads back the resource bit of its request (gatherCircuit);
6. every request sums its gathered bits (lineSums, at four gates per bit by complexity_lineSums_le).

The sum of a request is the requested value (lineSums_eval_recoveryCircuit). Requests may repeat. Scatter and gather are shared OR lookups (batchOrCircuit) on keys made of a copy index, point bits and, for the gather, a bit index.

Sizes count every gate, constants included (size_recoveryCircuit); they do not certify the running time of the circuit constructors.

Main definitions

• Cslib.Circuits.Boolean.MassProduction.Pipeline.recoveryCircuit: stages one to five.
• Cslib.Circuits.Boolean.MassProduction.Pipeline.lineSums: stage six, as a function.
• Cslib.Circuits.Boolean.MassProduction.Pipeline.slotResource: the resource of a slot.

Main results

• Cslib.Circuits.Boolean.MassProduction.Pipeline.lineSums_eval_recoveryCircuit: correctness.
• Cslib.Circuits.Boolean.MassProduction.Pipeline.size_recoveryCircuit: the exact gate count.
• Cslib.Circuits.Boolean.MassProduction.Pipeline.complexity_lineSums_le: the cost of the sums.

References

• Adapted from MassProduction/HighRate/{ResourceLayout,PrefixMetadata}.lean and MassProduction/Nonuniform/{IncidenceEvaluation,MaskedScatter,ResourceBank,ResourceGather, ScheduledRecovery}.lean in S. Schlesinger, Boolean circuit mass production formalization.

Shared OR lookup with one matching value

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.directProductInput_eval_batchOrCircuit {input sources requests k v : ℕ} (sourceKeys : Fin sources → Fin k → Fin input ⊕ Bool) (sourceValues : Fin sources → Fin v → Fin input ⊕ Bool) (queryKeys : Fin requests → Fin k → Fin input ⊕ Bool) (x : BitString input) (request : Fin requests) {V : BitString v} (hex : ∃ (source : Fin sources), substitute (sourceKeys source) x = substitute (queryKeys request) x) (hall : ∀ (source : Fin sources), substitute (sourceKeys source) x = substitute (queryKeys request) x → substitute (sourceValues source) x = V) : directProductInput ((batchOrCircuit sourceKeys sourceValues queryKeys).eval interpretation x) request = V

If some source matches a query and every matching source carries the value V, the shared OR lookup returns V to that query.

Encodings

def Cslib.Circuits.Boolean.MassProduction.Pipeline.slotEquiv {ℓ b copies : ℕ} : Fin copies × BitString (ℓ * b) ≃ Fin (copies * 2 ^ (ℓ * b))

Slots are numbered by a copy and the bits of a point.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.slotKey {ℓ b copies : ℕ} (q : Fin (copies * 2 ^ (ℓ * b))) : BitString (Nat.clog 2 copies + ℓ * b)

The key of a slot: its copy index followed by its point bits.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.slotKey_slotEquiv {ℓ b copies : ℕ} (c : Fin copies) (y : BitString (ℓ * b)) : slotKey (slotEquiv (c, y)) = Fin.append (BitString.indexBits c) y

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.MassProduction.Pipeline.metaWidth (ℓ b copies : ℕ) : ℕ

The width of the metadata of a request: its target point, copy and bit position.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.MassProduction.Pipeline.stateWidth (t p w ℓ b s copies : ℕ) : ℕ

The width of the circuit state after scheduling: listed lines, metadata and the input.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.slotKey_injective {ℓ b copies : ℕ} : Function.Injective slotKey

The stages

def Cslib.Circuits.Boolean.MassProduction.Pipeline.metadata {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {p ℓ b copies : ℕ} (bits : K ≃+ BitString b) (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (a : BitString p) : BitString (metaWidth ℓ b copies)

The metadata of a prefix: the bits of its information point, its copy and its bit index.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.prefixWires (t p w : ℕ) (y : Fin (t * p)) : Fin (t * (p + w))

The input wires of the prefixes of the requests, as t consecutive blocks.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.lookupStage {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {p ℓ b copies : ℕ} (bits : K ≃+ BitString b) (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (t w : ℕ) : Circuit signature (t * (p + w)) (t * metaWidth ℓ b copies + t * (p + w))

Stage one: look up the metadata of every prefix in one shared table, keeping the input.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.scheduleStage {t ℓ b s : ℕ} (sched : Circuit signature (t * (ℓ * b)) (t * (s * (ℓ * b)))) (p w copies : ℕ) : Circuit signature (t * metaWidth ℓ b copies + t * (p + w)) (stateWidth t p w ℓ b s copies)

Stage two: list the lines of the scheduler through the target points, keeping the state.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.incidenceKey (t p w ℓ b s copies : ℕ) (y : Fin (t * s)) : Fin (Nat.clog 2 copies + ℓ * b) → Fin (stateWidth t p w ℓ b s copies)

The state wires of the key of incidence (i, j): the copy index of request i, then point j of its line.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.scatterCircuit (t p w ℓ b s copies : ℕ) : Circuit signature (stateWidth t p w ℓ b s copies) (copies * 2 ^ (ℓ * b) * w)

Stage three: every incidence sends the suffix of its request to the slot of its key.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.bankCircuit {w ℓ b copies : ℕ} (members : Fin (copies * 2 ^ (ℓ * b)) → Fin b → Circuit signature w 1) : Circuit signature (copies * 2 ^ (ℓ * b) * w) (copies * 2 ^ (ℓ * b) * b)

Stage four: every slot runs one circuit per bit position on its suffix.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.gatherCircuit (t p w ℓ b s copies : ℕ) : Circuit signature (copies * 2 ^ (ℓ * b) * b + stateWidth t p w ℓ b s copies) (t * s * 1)

Stage five: every incidence reads the bank output at the slot of its key and the bit position of its request.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.recoveryCircuit {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {t p w ℓ b s copies : ℕ} (bits : K ≃+ BitString b) (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (sched : Circuit signature (t * (ℓ * b)) (t * (s * (ℓ * b)))) (members : Fin (copies * 2 ^ (ℓ * b)) → Fin b → Circuit signature w 1) : Circuit signature (t * (p + w)) (t * s * 1)

The scheduled recovery circuit. Output (i, j) is the resource bit of request i at point j of its line.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.size_recoveryCircuit {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {t p w ℓ b s copies : ℕ} {bits : K ≃+ BitString b} {C : LineCode K ℓ} {place : BitString p ↪ Fin copies × ↥C.info × Fin b} (sched : Circuit signature (t * (ℓ * b)) (t * (s * (ℓ * b)))) (members : Fin (copies * 2 ^ (ℓ * b)) → Fin b → Circuit signature w 1) : (recoveryCircuit bits C place sched members).size = (batchLookupCircuit (metadata bits C place) t).size + sched.size + (scatterCircuit t p w ℓ b s copies).size + ∑ q : Fin (copies * 2 ^ (ℓ * b)), ∑ r : Fin b, (members q r).size + (gatherCircuit t p w ℓ b s copies).size

Every gate is counted, including the constants of the lookups.

def Cslib.Circuits.Boolean.MassProduction.Pipeline.lineSums (t s : ℕ) (y : BitString (t * s * 1)) (i : Fin t) : Bool

Stage six, as a function: request i sums its s gathered bits.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.complexity_lineSums_le {t s : ℕ} : complexity interpretation (lineSums t s) ≤ t * (4 * s + 1)

Summing the gathered bits costs four gates per bit and one constant per request.

Correctness

def Cslib.Circuits.Boolean.MassProduction.Pipeline.slotResource {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {p w ℓ b copies : ℕ} (bits : K ≃+ BitString b) (C : LineCode K ℓ) (place : BitString p ↪ Fin copies × ↥C.info × Fin b) (f : BooleanFunction (p + w)) (q : Fin (copies * 2 ^ (ℓ * b))) (r : Fin b) : BooleanFunction w

The resource of slot q and bit position r.

theorem Cslib.Circuits.Boolean.MassProduction.Pipeline.lineSums_eval_recoveryCircuit {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {t p w ℓ b s copies : ℕ} {bits : K ≃+ BitString b} {C : LineCode K ℓ} {place : BitString p ↪ Fin copies × ↥C.info × Fin b} (scalar : Fin s ≃ { c : K // c ≠ 0 }) {sched : Circuit signature (t * (ℓ * b)) (t * (s * (ℓ * b)))} (hsched : IsScheduler bits scalar sched) {f : BooleanFunction (p + w)} {members : Fin (copies * 2 ^ (ℓ * b)) → Fin b → Circuit signature w 1} (hmembers : ∀ (q : Fin (copies * 2 ^ (ℓ * b))) (r : Fin b), (members q r).Computes interpretation (single (slotResource bits C place f q r))) (x : BitString (t * (p + w))) : lineSums t s ((recoveryCircuit bits C place sched members).eval interpretation x) = directProduct f t x

Correctness of scheduled recovery. Given a scheduler and circuits for the slot resources, the outputs of every request along its line sum to f at its input block.