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: one bounded correction of a residue.
• 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_invariant (lower period r t : ℕ) (hp : 0 < period) (hr : r < period) : have v := (liftResidue lower period)^[t] r; (lower ≤ v ∨ t ≤ v) ∧ v < lower + period ∧ v % period = r

Repeated correction preserves the residue and never passes the interval.

theorem Cslib.Circuits.Boolean.Iteration.liftResidue_spec (lower period T K : ℕ) (hp : 0 < period) (hK : lower ≤ K) : have v := (liftResidue lower period)^[K] (T % period); lower ≤ v ∧ v < lower + period ∧ v % period = T % period

Enough corrections place the residue in 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.

theorem Cslib.Circuits.Boolean.Iteration.liftWord_toNat {w : ℕ} (lower period r : BitVec w) (hfit : lower.toNat + period.toNat ≤ 2 ^ w) : (liftWord lower period r).toNat = liftResidue lower.toNat period.toNat r.toNat

The word correction agrees with the natural-number one when the interval fits.

theorem Cslib.Circuits.Boolean.Iteration.liftWord_iterate_toNat {w : ℕ} (lower period r : BitVec w) (hfit : lower.toNat + period.toNat ≤ 2 ^ w) (K : ℕ) : ((liftWord lower period)^[K] r).toNat = (liftResidue lower.toNat period.toNat)^[K] r.toNat

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.

theorem Cslib.Circuits.Boolean.Iteration.residueWord_toNat {w T K : ℕ} (period : BitVec w) (hK : K < 2 ^ w) (hp : 0 < period.toNat) (hpK : period.toNat ≤ K) : (residueWord T K period).toNat = T % period.toNat

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_liftWord {n w : ℕ} (s : Set (BooleanFunction n)) (lower period r : BitString n → BitVec w) (hl : ∀ (i : Fin w), (fun (x : BitString n) => (lower x).getLsbD ↑i) ∈ s) (hp : ∀ (i : Fin w), (fun (x : BitString n) => (period x).getLsbD ↑i) ∈ s) (hr : ∀ (i : Fin w), (fun (x : BitString n) => (r x).getLsbD ↑i) ∈ s) : Synthesis interpretation s (wordWires fun (x : BitString n) => liftWord (lower x) (period x) (r x)) (21 * w + 3)

One word correction: an addition, a comparison and a multiplexer.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_liftWord_iterate {n w : ℕ} (s : Set (BooleanFunction n)) (lower period init : BitString n → BitVec w) (hl : ∀ (i : Fin w), (fun (x : BitString n) => (lower x).getLsbD ↑i) ∈ s) (hp : ∀ (i : Fin w), (fun (x : BitString n) => (period x).getLsbD ↑i) ∈ s) (hinit : ∀ (i : Fin w), (fun (x : BitString n) => (init x).getLsbD ↑i) ∈ s) (K : ℕ) : Synthesis interpretation s (wordWires fun (x : BitString n) => (liftWord (lower x) (period x))^[K] (init x)) (K * (21 * w + 3))

Iterated word corrections, sharing all intermediate words.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_residueWord {n w : ℕ} (s : Set (BooleanFunction n)) (T K : ℕ) (period : BitString n → BitVec w) (hp : ∀ (i : Fin w), (fun (x : BitString n) => (period x).getLsbD ↑i) ∈ s) (hconst : ∀ (b : Bool), (fun (x : BitString n) => b) ∈ s) : Synthesis interpretation s (wordWires fun (x : BitString n) => residueWord T K (period x)) (w * ((K + 1) * (2 * w + 3) + 1))

A residue table costs only its word width and entry count, whatever T is.

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.