Documentation

Complexity.Computability.Circuit.Boolean.Iteration.InputTime

Iterating for a number of steps given as input #

A circuit with n + m inputs reads a state from its first n inputs and a number of steps from its last m inputs, in binary with the least significant bit first, and returns that iterate of f (inputTimeIterate). Binary powering builds it from fixed powers: stage j applies a circuit for f^[2 ^ j] to the current state, and bit j of the time selects its result or the current state, at four gates per state bit (synthesis_binary_powering). With the fixed-power circuits of size 40000 * powerBudget n s (2 ^ n) L, an m-bit time costs at most m * (40000 * powerBudget n s (2 ^ n) L + 4 * n) (variable_time), and m * (120000 * optimizedBudget n s (2 ^ n) + 4 * n) with the balanced parameter (variable_time_optimized). The cost is linear in m; a bound additive in m, which first reduces the time modulo the cycle length, is variable_time_additive in Iteration.LongTime.

The shared rule synthesis_batched_binary_powering processes r states with independent m-bit times using one batched power circuit of size at most C per stage, for a total of m * (C + 4 * (r * n)) gates. Scalar binary powering is its singleton specialization; Circuit.replicate 1 supplies the batched power circuits without increasing their size.

The circuits are native De Morgan circuits: every NOT, AND and OR gate and every constant is charged, while wiring and fanout are free. They exist for each m, because the fixed-power circuits do; nothing here bounds the time to construct them.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.Iteration.inputTimeIterate {n : ℕ} (f : BitString n → BitString n) (m : ℕ) (y : BitString (n + m)) :
BitString n

The state after T steps of f, where the first n of the n + m input bits are the state and the last m bits are T in binary, least significant bit first.

Instances For
    source
    theorem Cslib.Circuits.Boolean.Iteration.inputTimeIterate_zero {n : ℕ} (f : BitString n → BitString n) (y : BitString (n + 0)) :
    inputTimeIterate f 0 y = fun (i : Fin n) => y (Fin.castAdd 0 i)

    Without time bits the state is returned unchanged.

    source
    theorem Cslib.Circuits.Boolean.Iteration.toNat_word_mod_two_pow_succ {m : ℕ} (bits : BitString m) {j : ℕ} (hj : j < m) :
    (word bits).toNat % 2 ^ (j + 1) = (word bits).toNat % 2 ^ j + if bits ⟨j, hj⟩ = true then 2 ^ j else 0

    Reading one more bit of a binary time adds that bit's power of two.

    source
    theorem Cslib.Circuits.Boolean.Iteration.iterate_toNat_word_mod_two_pow_succ {m : ℕ} {α : Type u_1} (f : α → α) (bits : BitString m) {j : ℕ} (hj : j < m) (y : α) :
    f^[(word bits).toNat % 2 ^ (j + 1)] y = if bits ⟨j, hj⟩ = true then f^[2 ^ j] (f^[(word bits).toNat % 2 ^ j] y) else f^[(word bits).toNat % 2 ^ j] y

    Applying f^[2 ^ j] exactly when bit j is set extends the time read so far by that bit.

    source
    theorem Cslib.Circuits.Boolean.Iteration.synthesis_batched_binary_powering {n m r a : ℕ} (f : BitString n → BitString n) (C : ℕ) (hpowers : ∀ j < m, ∃ (c : Circuit signature (r * n) (r * n)), c.Computes interpretation (blockMap f^[2 ^ j] r) ∧ c.size ≤ C) (s : Set (BooleanFunction a)) (init : BitString a → Fin r → BitString n) (bits : BitString a → Fin r → BitString m) (hi : ∀ (member : Fin r) (bit : Fin n), (fun (x : BitString a) => init x member bit) ∈ s) (hb : ∀ (member : Fin r) (j : Fin m), (fun (x : BitString a) => bits x member j) ∈ s) :
    Synthesis interpretation s (⋃ (member : Fin r), wires fun (x : BitString a) => f^[(word (bits x member)).toNat] (init x member)) (m * (C + 4 * (r * n)))

    Batched binary powering. If every batched power f^[2 ^ j] with j < m has a circuit of size at most C, then r available states, each with its own time given by m available bits, cost at most m * (C + 4 * r * n) gates.

    source
    theorem Cslib.Circuits.Boolean.Iteration.synthesis_binary_powering {n m a : ℕ} (f : BitString n → BitString n) (C : ℕ) (hpowers : ∀ j < m, ∃ (c : Circuit signature n n), c.Computes interpretation f^[2 ^ j] ∧ c.size ≤ C) (s : Set (BooleanFunction a)) (init : BitString a → BitString n) (bits : BitString a → BitString m) (hi : wires init ⊆ s) (hb : wires bits ⊆ s) :
    Synthesis interpretation s (wires fun (x : BitString a) => f^[(word (bits x)).toNat] (init x)) (m * (C + 4 * n))

    Binary powering. If every power f^[2 ^ j] with j < m has a circuit of size at most C, then T steps of f from an available state, with T given by m available bits, cost at most m * (C + 4 * n) gates: one power circuit and one multiplexer per bit.

    source
    theorem Cslib.Circuits.Boolean.Iteration.binary_powering {n : ℕ} (f : BitString n → BitString n) (m C : ℕ) (hpowers : ∀ j < m, ∃ (c : Circuit signature n n), c.Computes interpretation f^[2 ^ j] ∧ c.size ≤ C) :
    ∃ (out : Circuit signature (n + m) n), out.Computes interpretation (inputTimeIterate f m) ∧ out.size ≤ m * (C + 4 * n)

    Binary powering, as a circuit on n + m inputs.

    source
    theorem Cslib.Circuits.Boolean.Iteration.variable_time {n : ℕ} (c : Circuit signature n n) (m L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) :
    ∃ (out : Circuit signature (n + m) n), out.Computes interpretation (inputTimeIterate (c.eval interpretation) m) ∧ out.size ≤ m * (40000 * powerBudget n c.size (2 ^ n) L + 4 * n)

    Input times. For every 0 < L ≤ 2 ^ n, some circuit of size at most m * (40000 * powerBudget n c.size (2 ^ n) L + 4 * n) iterates c for a number of steps given by m input bits.

    source
    theorem Cslib.Circuits.Boolean.Iteration.variable_time_optimized {n : ℕ} (c : Circuit signature n n) (m : ℕ) :
    ∃ (out : Circuit signature (n + m) n), out.Computes interpretation (inputTimeIterate (c.eval interpretation) m) ∧ ↑out.size ≤ ↑m * (120000 * optimizedBudget n c.size (2 ^ n) + 4 * ↑n)

    Square-root input times.