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