Circuits for transient depths

Let c be a circuit of size s computing f on n-bit states. Some circuit of size at most 50000 * powerBudget n s (2 ^ n) L computes the transient depth of every state, in n + 2 bits (checkpoint_depth_circuit), for every 0 < L ≤ 2 ^ n; with the balanced parameter the size is at most 150000 * optimizedBudget n s (2 ^ n) (checkpoint_depth_optimized).

The construction compares the first 2 L + 1 states of the orbit of x with those of its cycle projection f^[(2 ^ n)!] x, computed by a fixed-power circuit. The two orbits agree exactly from the transient depth on (FunctionalGraph.iterate_eq_projection_iff). If they agree at the end of the prefix, the first agreement is the depth (shortDepth_eq). Otherwise the transient is long, so the prefix cannot repeat and meets a checkpoint, all of whose prefix states are transient: the depth is the hardwired depth of the checkpoint plus its time in the prefix. One shared dictionary answers all prefix states.

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

Main definitions

• Cslib.Circuits.Boolean.Iteration.shortDepth: the first agreement with the projected orbit.
• Cslib.Circuits.Boolean.Iteration.depthCost: the gate count of the checkpoint construction.

Main results

• Cslib.Circuits.Boolean.Iteration.depth_from_checkpoints: depths from given checkpoints.
• Cslib.Circuits.Boolean.Iteration.checkpoint_depth_circuit, Cslib.Circuits.Boolean.Iteration.checkpoint_depth_optimized: transient depths.

References

• Adapted from lean/Proofs/CheckpointDepth.lean in S. Schlesinger, Square-root circuit bounds for iterated functions, whose bounds have the constants 1000000 and 3000000. The dictionary here is the library's batchOrCircuit lookup.

def Cslib.Circuits.Boolean.Iteration.shortDepth {n : ℕ} (f : BitString n → BitString n) (K : ℕ) (x : BitString n) : BitVec (n + 2)

The first time up to K at which the orbit of x agrees with the orbit of its cycle projection, in n + 2 bits.

theorem Cslib.Circuits.Boolean.Iteration.shortDepth_eq {n : ℕ} (f : BitString n → BitString n) (K : ℕ) (x : BitString n) (hK : FunctionalGraph.transientDepth f x ≤ K) : shortDepth f K x = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth f x)

A transient of length at most K is found by the first agreement.

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

The gate count of the depth construction from M checkpoints with parameter L: constants, the projection, both orbit prefixes, the shared dictionary, and per prefix state an equality test, an addition and two selection steps, then the final selection.

theorem Cslib.Circuits.Boolean.Iteration.depth_from_checkpoints {n M : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (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) : ∃ (out : Circuit signature n (n + 2)), (∀ (x : Fin n → Bool), word (out.eval interpretation x) = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth (c.eval interpretation) x)) ∧ out.size ≤ depthCost n c.size M L

Depths from checkpoints. 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. Then some circuit of size at most depthCost n c.size M L computes the transient depth of every state in n + 2 bits.

theorem Cslib.Circuits.Boolean.Iteration.depthCost_le (n s M L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (hM : M ≤ 2 ^ n / L) : depthCost n s M L ≤ 50000 * powerBudget n s (2 ^ n) L

The depth construction is within 50000 times the fixed-power tradeoff.

theorem Cslib.Circuits.Boolean.Iteration.checkpoint_depth_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n (n + 2)), (∀ (x : Fin n → Bool), word (out.eval interpretation x) = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth (c.eval interpretation) x)) ∧ out.size ≤ 50000 * powerBudget n c.size (2 ^ n) L

Transient depths. For every 0 < L ≤ 2 ^ n, some circuit of size at most 50000 * powerBudget n c.size (2 ^ n) L computes the transient depth of every state in n + 2 bits.

theorem Cslib.Circuits.Boolean.Iteration.checkpoint_depth_optimized {n : ℕ} (c : Circuit signature n n) : ∃ (out : Circuit signature n (n + 2)), (∀ (x : Fin n → Bool), word (out.eval interpretation x) = BitVec.ofNat (n + 2) (FunctionalGraph.transientDepth (c.eval interpretation) x)) ∧ ↑out.size ≤ 150000 * optimizedBudget n c.size (2 ^ n)

Square-root transient depths. Some circuit of size at most 150000 * optimizedBudget n c.size (2 ^ n) computes the transient depth of every state in n + 2 bits.