Batched fixed powers with one shared dictionary

A circuit with r * n inputs and outputs applies f^[T] to each of r independent n-bit states (blockMap). All members share one checkpoint table: the orbit prefixes of all members are looked up in one batched dictionary, and each member finishes on its own. For r ≤ 2 ^ n and 0 < L ≤ 2 ^ n this costs at most 100000 * batchBudget n s (2 ^ n) r L gates (batched_fixed_power), where batchBudget n s M r L = r * L * s + (n + 1) ^ 3 * (r * L + M / L + 1); the storage term M / L is paid once rather than r times. Balancing L gives 300000 * (r * A + √((n + 1) ^ 3 * 2 ^ n * r * A)) with A = s + (n + 1) ^ 3 (batched_fixed_power_optimized).

With a separate m-bit time for each member, binary powering with the batched powers costs m * (100000 * batchBudget n s (2 ^ n) r L + 4 * r * n) (batched_variable_time), and m * (300000 * optimizedBatchBudget n s (2 ^ n) r + 4 * r * n) balanced (batched_variable_time_optimized). These input-time circuits specialize the shared binary-powering rule in Iteration.InputTime to the batched fixed-power circuits proved here.

The circuits are native De Morgan circuits: every NOT, AND and OR gate and every constant is charged, while wiring and fanout are free. The checkpoints are chosen nonconstructively, so the circuits exist for each parameter choice; nothing here bounds the time to construct them.

Main definitions

• Cslib.Circuits.Boolean.Iteration.batchBudget: the batched size tradeoff.
• Cslib.Circuits.Boolean.Iteration.optimizedBatchBudget: its balanced square-root form.

Main results

• Cslib.Circuits.Boolean.Iteration.synthesis_batched_power: the shared-dictionary construction.
• Cslib.Circuits.Boolean.Iteration.batched_fixed_power, Cslib.Circuits.Boolean.Iteration.batched_fixed_power_optimized: batched fixed powers.
• Cslib.Circuits.Boolean.Iteration.synthesis_batched_binary_powering: binary powering of batches, with one time per member.
• Cslib.Circuits.Boolean.Iteration.batched_variable_time, Cslib.Circuits.Boolean.Iteration.batched_variable_time_optimized: batched input times.

References

• Adapted from lean/Proofs/{BatchPowers,BatchVariableTime}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

def Cslib.Circuits.Boolean.Iteration.batchBudget (n s M r L : ℕ) : ℕ

The batched tradeoff r * L * s + (n + 1) ^ 3 * (r * L + M / L + 1) for r trajectories of n-bit states, a transition circuit of size s, M relevant states and parameter L.

theorem Cslib.Circuits.Boolean.Iteration.batchBudget_one (n s M L : ℕ) : batchBudget n s M 1 L = powerBudget n s M L

A single trajectory has the fixed-power tradeoff.

theorem Cslib.Circuits.Boolean.Iteration.exists_circuit_blockMap {n r k : ℕ} {g : BitString n → BitString k} {C : ℕ} (h : Synthesis interpretation (inputs (r * n)) (⋃ (member : Fin r), wires fun (x : BitString (r * n)) => g (directProductInput x member)) C) : ∃ (out : Circuit signature (r * n) (r * k)), out.Computes interpretation (blockMap g r) ∧ out.size ≤ C

A synthesis of every member's output block gives a circuit for the block map.

Batched fixed powers

theorem Cslib.Circuits.Boolean.Iteration.synthesis_batched_power {n r a M : ℕ} (c : Circuit signature n n) (s : Set (BooleanFunction a)) (init : BitString a → Fin r → BitString n) (hi : ∀ (member : Fin r) (bit : Fin n), (fun (x : BitString a) => init x member bit) ∈ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) (T L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (hT : 2 * L ≤ T) (cp : Fin M → BitString n) (hcp : Function.Injective cp) (hcover : ∀ (x : Fin n → Bool), FunctionalGraph.Repeats (c.eval interpretation) x L ∨ ∃ t < 2 * L, ∃ (j : Fin M), (c.eval interpretation)^[t] x = cp j) : Synthesis interpretation s (⋃ (member : Fin r), wires fun (x : BitString a) => (c.eval interpretation)^[T] (init x member)) (r * (2 * L * c.size) + 48 * (r * (2 * L + 1) + M + 1) * (Nat.clog 2 (r * (2 * L + 1) + M) + 1) ^ 2 * (n + (n + 1) + 1) + r * ((2 * L + 1) * (4 * (n + 2 + n + 1)) + 2 * L * c.size + 200 * (2 * L + 1) * (n + (n + 2) + 1) ^ 2 + 40000 * powerBudget n c.size 0 L + 4 * n))

Shared-dictionary powers. Let cp be injective checkpoints such that every orbit repeats among its first L states or reaches a checkpoint in fewer than 2 L steps, and let 2 L ≤ T. Then f^[T] of r available states costs one orbit prefix of 2 L steps per member, one shared lookup of all prefix states against the M checkpoints, and one finishing step and one checkpoint-free fixed-power circuit per member.

theorem Cslib.Circuits.Boolean.Iteration.batch_construction_cost (n s M r L : ℕ) (hrN : r ≤ 2 ^ n) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (hM : M ≤ 2 ^ n / L) : 2 + (r * (2 * L * s) + 48 * (r * (2 * L + 1) + M + 1) * (Nat.clog 2 (r * (2 * L + 1) + M) + 1) ^ 2 * (n + (n + 1) + 1) + r * ((2 * L + 1) * (4 * (n + 2 + n + 1)) + 2 * L * s + 200 * (2 * L + 1) * (n + (n + 2) + 1) ^ 2 + 40000 * powerBudget n s 0 L + 4 * n)) ≤ 100000 * batchBudget n s (2 ^ n) r L

The construction cost is within 100000 times the batched tradeoff.

theorem Cslib.Circuits.Boolean.Iteration.batched_fixed_power {n : ℕ} (c : Circuit signature n n) (r T L : ℕ) (hrN : r ≤ 2 ^ n) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature (r * n) (r * n)), out.Computes interpretation (blockMap (c.eval interpretation)^[T] r) ∧ out.size ≤ 100000 * batchBudget n c.size (2 ^ n) r L

Batched fixed powers. For r ≤ 2 ^ n and 0 < L ≤ 2 ^ n, some circuit of size at most 100000 * batchBudget n c.size (2 ^ n) r L applies T steps of c to each of r independent states.

noncomputable def Cslib.Circuits.Boolean.Iteration.optimizedBatchBudget (n s M r : ℕ) : ℝ

The balanced batched budget r * A + √((n + 1) ^ 3 * M * r * A) with A = s + (n + 1) ^ 3.

theorem Cslib.Circuits.Boolean.Iteration.optimizedBatchBudget_one (n s M : ℕ) : optimizedBatchBudget n s M 1 = optimizedBudget n s M

A single trajectory has the balanced fixed-power budget.

theorem Cslib.Circuits.Boolean.Iteration.exists_batchBudget_le_optimizedBatchBudget (n s M r : ℕ) (hr : 0 < r) (hM : M ≤ 2 ^ n) : ∃ (L : ℕ), 0 < L ∧ L ≤ 2 ^ n ∧ ↑(batchBudget n s M r L) ≤ 3 * optimizedBatchBudget n s M r

theorem Cslib.Circuits.Boolean.Iteration.batched_fixed_power_optimized {n : ℕ} (c : Circuit signature n n) (r T : ℕ) (hr : 0 < r) (hrN : r ≤ 2 ^ n) : ∃ (out : Circuit signature (r * n) (r * n)), out.Computes interpretation (blockMap (c.eval interpretation)^[T] r) ∧ ↑out.size ≤ 300000 * optimizedBatchBudget n c.size (2 ^ n) r

Square-root batched fixed powers.

Batched input times

theorem Cslib.Circuits.Boolean.Iteration.batched_variable_time {n : ℕ} (c : Circuit signature n n) (r m L : ℕ) (hrN : r ≤ 2 ^ n) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature (r * (n + m)) (r * n)), out.Computes interpretation (blockMap (inputTimeIterate (c.eval interpretation) m) r) ∧ out.size ≤ m * (100000 * batchBudget n c.size (2 ^ n) r L + 4 * (r * n))

Batched input times. For r ≤ 2 ^ n and 0 < L ≤ 2 ^ n, some circuit of size at most m * (100000 * batchBudget n c.size (2 ^ n) r L + 4 * (r * n)) iterates c on each of r independent states for that member's own number of steps, given by m input bits.

theorem Cslib.Circuits.Boolean.Iteration.batched_variable_time_optimized {n : ℕ} (c : Circuit signature n n) (r m : ℕ) (hr : 0 < r) (hrN : r ≤ 2 ^ n) : ∃ (out : Circuit signature (r * (n + m)) (r * n)), out.Computes interpretation (blockMap (inputTimeIterate (c.eval interpretation) m) r) ∧ ↑out.size ≤ ↑m * (300000 * optimizedBatchBudget n c.size (2 ^ n) r + 4 * (↑r * ↑n))

Square-root batched input times.