Long input times at additive cost

Binary powering iterates for an m-bit input time with m fixed-power circuits (variable_time). For long times this is wasteful: the state after T steps is the state after a time below 2 * 2 ^ n, namely T itself or 2 ^ n plus T - 2 ^ n modulo the cycle length (FunctionalGraph.iterate_normalizedTime). The cycle length is part of the canonical label, the reduction streams through the time bits at O(n) gates per bit, and only n + 3 time bits remain for binary powering (compressedTime). This gives a circuit of size at most 200000 * (n + 1) * powerBudget n s (2 ^ n) L + 80 * m * (n + 1), additive in the time width (variable_time_additive), and 600000 * (n + 1) * optimizedBudget n s (2 ^ n) + 80 * m * (n + 1) balanced (variable_time_additive_optimized). Together with variable_time_optimized this gives the minimum of the two bounds.

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 and L; nothing here bounds the time to construct them.

Main definitions

• Cslib.Circuits.Boolean.Iteration.compressedTime: a short time with the same state.

Main results

• Cslib.Circuits.Boolean.Iteration.toNat_compressedTime: it is the normalized time.
• Cslib.Circuits.Boolean.Iteration.variable_time_additive, Cslib.Circuits.Boolean.Iteration.variable_time_additive_optimized: long input times.

References

• Adapted from lean/Proofs/LongTime.lean in S. Schlesinger, Square-root circuit bounds for iterated functions, whose bound is 33000000 * (n + 1) * optimizedBudget n s (2 ^ n) + 200 * m * (n + 1).

def Cslib.Circuits.Boolean.Iteration.compressedTime {m : ℕ} (n : ℕ) (ell : BitVec (n + 3)) (bits : BitString m) : BitVec (n + 3)

For a time given by m bits and a cycle length ell, the time itself if it is below 2 ^ n, and otherwise 2 ^ n plus the excess modulo ell, in n + 3 bits.

theorem Cslib.Circuits.Boolean.Iteration.toNat_compressedTime {n m : ℕ} (f : BitString n → BitString n) (x : BitString n) (bits : BitString m) (hnm : n < m) : (compressedTime n (BitVec.ofNat (n + 3) (FunctionalGraph.cycleLength f x)) bits).toNat = FunctionalGraph.normalizedTime f x (word bits).toNat

With the cycle length of x, the compressed time is the normalized time.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_compressedTime {n m a : ℕ} (s : Set (BooleanFunction a)) (ell : BitString a → BitVec (n + 3)) (bits : BitString a → BitString m) (hl : wordWires ell ⊆ s) (hb : ∀ (j : Fin m), (fun (x : BitString a) => bits x j) ∈ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) : Synthesis interpretation s (wordWires fun (x : BitString a) => compressedTime n (ell x) (bits x)) (m * (22 * (n + 3) + 3) + 50 * (n + 4) ^ 2 + 16 * (n + 3) + 1 + (5 * m + 2))

Compressing an available time with an available cycle length: one streaming remainder over the time bits, one modular difference, one addition, one comparison and one selection.

def Cslib.Circuits.Boolean.Iteration.longTimeBudget (n s m L : ℕ) : ℕ

The gate count of the long-time construction: constants, the label circuit, the time compression and binary powering over n + 3 time bits.

theorem Cslib.Circuits.Boolean.Iteration.long_time_circuit {n : ℕ} (c : Circuit signature n n) (m L : ℕ) (hnm : n < m) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature (n + m) n), out.Computes interpretation (inputTimeIterate (c.eval interpretation) m) ∧ out.size ≤ longTimeBudget n c.size m L

Long input times, for times wider than the state: some circuit of size at most longTimeBudget n c.size m L iterates c for a number of steps given by m > n input bits.

theorem Cslib.Circuits.Boolean.Iteration.longTimeBudget_le (n s m L : ℕ) : longTimeBudget n s m L ≤ 200000 * (n + 1) * powerBudget n s (2 ^ n) L + 80 * m * (n + 1)

theorem Cslib.Circuits.Boolean.Iteration.variable_time_additive {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 ≤ 200000 * (n + 1) * powerBudget n c.size (2 ^ n) L + 80 * m * (n + 1)

Long input times. For every 0 < L ≤ 2 ^ n, some circuit of size at most 200000 * (n + 1) * powerBudget n c.size (2 ^ n) L + 80 * m * (n + 1) iterates c for a number of steps given by m input bits. The cost of the time bits is additive.

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

Square-root long input times. Some circuit of size at most 600000 * (n + 1) * optimizedBudget n c.size (2 ^ n) + 80 * m * (n + 1) iterates c for a number of steps given by m input bits.