Documentation

Complexity.Computability.Circuit.Boolean.Iteration.Batch

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).

If each trajectory's first L states lie in a finite set S, the same construction pays S.card / L for the shared checkpoint table (batched_fixed_power_on_prefixes). The trajectories may leave S later. In particular, an invariant set gives the tradeoff 100000 * batchBudget n s S.card r L (batched_fixed_power_on) and its balanced form (batched_fixed_power_on_optimized). No correctness is required outside the stated input domain.

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 #

Main results #

References #

source
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.

Instances For
    source
    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.

    Batched fixed powers #

    source
    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.

    source
    theorem Cslib.Circuits.Boolean.Iteration.batched_fixed_power_on_prefixes {n : ℕ} (c : Circuit signature n n) (S : Finset (BitString n)) (r T L : ℕ) (hrN : r ≤ 2 ^ n) (hL : 0 < L) (hLN : L ≤ 2 ^ n) :
    ∃ (out : Circuit signature (r * n) (r * n)), out.ComputesOn interpretation {x : Fin (r * n) → Bool | ∀ (member : Fin r) (i : Fin L), (c.eval interpretation)^[↑i] (directProductInput x member) ∈ S} (blockMap (c.eval interpretation)^[T] r) ∧ out.size ≤ 100000 * batchBudget n c.size S.card r L

    Batched powers on promised prefixes. If the first L states of each input trajectory lie in S, one shared checkpoint table costs S.card / L in the batched tradeoff. The set need not be invariant: later states may leave it. The circuit is only required to be correct on the displayed input domain. All gates are charged; the time to construct the circuit is not bounded.

    source
    theorem Cslib.Circuits.Boolean.Iteration.batched_fixed_power_on {n : ℕ} (c : Circuit signature n n) (S : Finset (BitString n)) (r T L : ℕ) (hS : ∀ x ∈ S, c.eval interpretation x ∈ S) (hrN : r ≤ 2 ^ n) (hL : 0 < L) (hLN : L ≤ 2 ^ n) :
    ∃ (out : Circuit signature (r * n) (r * n)), out.ComputesOn interpretation {x : Fin (r * n) → Bool | ∀ (member : Fin r), directProductInput x member ∈ S} (blockMap (c.eval interpretation)^[T] r) ∧ out.size ≤ 100000 * batchBudget n c.size S.card r L

    Batched powers on an invariant set. The checkpoint storage term S.card / L is shared by all r trajectories. The batch may have more members than S has states.

    source
    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.

    source
    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.

    Instances For
      source
      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.

      source
      theorem Cslib.Circuits.Boolean.Iteration.batched_fixed_power_on_optimized {n : ℕ} (c : Circuit signature n n) (S : Finset (BitString n)) (r T : ℕ) (hS : ∀ x ∈ S, c.eval interpretation x ∈ S) (hr : 0 < r) (hrN : r ≤ 2 ^ n) :
      ∃ (out : Circuit signature (r * n) (r * n)), out.ComputesOn interpretation {x : Fin (r * n) → Bool | ∀ (member : Fin r), directProductInput x member ∈ S} (blockMap (c.eval interpretation)^[T] r) ∧ ↑out.size ≤ 300000 * optimizedBatchBudget n c.size S.card r

      Square-root batched powers on an invariant set. The balanced shared-storage bound uses S.card rather than the size of the ambient state space.

      source
      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 #

      source
      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.

      source
      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.