Advancing sparse orbit coordinates with one streamed input-time remainder

Main definitions

• advanceCycleLabel: advance a phase by an input bit-string time.

Main results

• advanceCycleLabel_spec: advancing the label agrees with iteration.
• synthesis_advanceCycleLabel: one streamed remainder, linear in time width.

References

• Adapted from lean/Proofs/CounterChartTime.lean at revision c4cfa198 of [S. Schlesinger, Square-root circuit bounds for iterated functions] [Sch26f].

def Cslib.Circuits.Boolean.Iteration.advanceCycleLabel {n m : ℕ} (r : BitString (n + (chartWidth n + chartWidth n))) (bits : Fin m → Bool) : BitString (n + (chartWidth n + chartWidth n))

Keep the cycle representative and length, advancing its phase by the input time.

theorem Cslib.Circuits.Boolean.Iteration.advanceCycleLabel_spec {n m : ℕ} (f : BitVec n → BitVec n) (x : BitVec n) (bits : Fin m → Bool) : advanceCycleLabel (wordCycleLabel f x) bits = wordCycleLabel f (f^[(word bits).toNat] x)

theorem Cslib.Circuits.Boolean.Iteration.synthesis_advanceCycleLabel {n m a : ℕ} (s : Set (BitString a → Bool)) (r : BitString a → BitString (n + (chartWidth n + chartWidth n))) (bits : BitString a → Fin m → Bool) (hr : wires r ⊆ s) (hb : ∀ (j : Fin m), (fun (z : BitString a) => bits z j) ∈ s) (hz : (fun (x : BitString a) => false) ∈ s) : Synthesis interpretation s (wires fun (z : BitString a) => advanceCycleLabel (r z) (bits z)) (200 * (n + 3) * (m + 1))

Streaming is performed once after the input's cycle length is selected.