Moving a residue into a repeated interval

If an orbit repeats with f^[i] x = f^[j] x for i < j, the state at any time T ≥ i is the state at the unique time in [i, j) congruent to T modulo j - i. A circuit finds that time without division: it looks up T % (j - i) in a table indexed by the period, which depends on the fixed exponent T only through its residues, and then adds the period while the value is below i. At most K additions suffice when i ≤ K (liftResidue_reconstructs).

Main definitions

• Cslib.Circuits.Boolean.Iteration.liftResidue, Cslib.Circuits.Boolean.Iteration.liftWord: one bounded correction of a residue, on natural numbers and on words.
• Cslib.Circuits.Boolean.Iteration.residueWord: table lookup of the residue of T modulo a period word.
• Cslib.Circuits.Boolean.Iteration.repeatWordIndex: the word computation of the time in the repeated interval.

Main results

• Cslib.Circuits.Boolean.Iteration.liftResidue_reconstructs: the corrected residue gives the state at time T.
• Cslib.Circuits.Boolean.Iteration.repeatWordIndex_spec: the same for the word computation.
• Cslib.Circuits.Boolean.Iteration.synthesis_repeatWordIndex: its gate count does not depend on T.

References

• Adapted from lean/Proofs/Residues.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

def Cslib.Circuits.Boolean.Iteration.liftResidue (lower period r : ℕ) : ℕ

One bounded correction of a residue: add the period once if below the interval.

theorem Cslib.Circuits.Boolean.Iteration.liftResidue_reconstructs {α : Type u_1} {f : α → α} {x : α} {i j T K : ℕ} (hij : i < j) (heq : f^[i] x = f^[j] x) (hK : i ≤ K) (hT : i ≤ T) : have r := (liftResidue i (j - i))^[K] (T % (j - i)); i ≤ r ∧ r < j ∧ f^[r] x = f^[T] x

The corrected residue lies in the repeated interval and gives the state at time T.

def Cslib.Circuits.Boolean.Iteration.liftWord {w : ℕ} (lower period r : BitVec w) : BitVec w

The word form of liftResidue.

def Cslib.Circuits.Boolean.Iteration.residueWord {w : ℕ} (T K : ℕ) (period : BitVec w) : BitVec w

The residues of T modulo every period up to K, selected by the period.

def Cslib.Circuits.Boolean.Iteration.repeatWordIndex {w : ℕ} (T K : ℕ) (lo hi : BitVec w) : BitVec w

The time in the repeated interval [lo, hi) that is congruent to T.

theorem Cslib.Circuits.Boolean.Iteration.repeatWordIndex_spec {α : Type u_1} {f : α → α} {x : α} {w T K : ℕ} (lo hi : BitVec w) (hlt : lo.toNat < hi.toNat) (hhi : hi.toNat ≤ K) (hK : K < 2 ^ w) (hT : K ≤ T) (heq : f^[lo.toNat] x = f^[hi.toNat] x) : have r := (repeatWordIndex T K lo hi).toNat; lo.toNat ≤ r ∧ r < hi.toNat ∧ f^[r] x = f^[T] x

The word computation lies in the repeated interval and selects the state at time T.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_repeatWordIndex {n w : ℕ} (s : Set (BooleanFunction n)) (T K : ℕ) (lo hi : BitString n → BitVec w) (hlo : ∀ (i : Fin w), (fun (x : BitString n) => (lo x).getLsbD ↑i) ∈ s) (hhi : ∀ (i : Fin w), (fun (x : BitString n) => (hi x).getLsbD ↑i) ∈ s) (hconst : ∀ (b : Bool), (fun (x : BitString n) => b) ∈ s) : Synthesis interpretation s (wordWires fun (x : BitString n) => repeatWordIndex T K (lo x) (hi x)) (100 * (K + 1) * (w + 1) ^ 2)

The repeated-interval index circuit has no dependence on the bit length of T.