Sparse-counter reachability, first hitting times, and visit schedules

Two cycle labels suffice for every pair query (x, y) on a permutation. Because both phases are already reduced modulo the cycle length, modular subtraction costs only linearly many gates (subtractResidues), so full visit-schedule records and first hitting times for sparsely edited counter permutations have circuits of size O((n + 1) * (r + 1)).

Main definitions

• cycleLabelDistance, cycleLabelVisits: phase distance and visit schedule from two cycle labels.

Main results

• cycleLabelVisits_spec, synthesis_cycleLabelVisits: correctness and linear gate bound for combining two cycle labels into a visit schedule.
• cycle_label_visit_circuit: visit-schedule circuit from any cycle-label circuit.
• sparse_counter_visit_circuit, sparse_counter_visit_schedule, sparse_counter_hitting_time: O((n + 1) * (r + 1)) circuits for visit-schedule records and first hitting times.
• sparse_coordinate_visit_schedule: coordinate transfer charging only two forward encodings.

References

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

def Cslib.Circuits.Boolean.Iteration.cycleLabelDistance {n : ℕ} (x y : BitString (n + (chartWidth n + chartWidth n))) : BitVec (chartWidth n)

Phase difference from label x to label y modulo the cycle length of x.

def Cslib.Circuits.Boolean.Iteration.cycleLabelVisits {n : ℕ} (x y : BitString (n + (chartWidth n + chartWidth n))) : BitString (visitScheduleWidth n)

A flag, first time, and return period in the visit-schedule format.

theorem Cslib.Circuits.Boolean.Iteration.cycleLabelVisits_flag {n : ℕ} (f : BitVec n → BitVec n) (hf : Function.Injective f) (x y : BitVec n) : cycleLabelVisits (wordCycleLabel f x) (wordCycleLabel f y) (Fin.castAdd (n + 1) 0) = true ↔ ∃ (t : ℕ), f^[t] x = y

theorem Cslib.Circuits.Boolean.Iteration.cycleLabelDistance_toNat {n : ℕ} (f : BitVec n → BitVec n) (hf : Function.Injective f) (x y : BitVec n) (hc : FunctionalGraph.canonicalCycle f x = FunctionalGraph.canonicalCycle f y) : (cycleLabelDistance (wordCycleLabel f x) (wordCycleLabel f y)).toNat = FunctionalGraph.cyclicDistance f x y

theorem Cslib.Circuits.Boolean.Iteration.cycleLabelVisits_first {n : ℕ} (f : BitVec n → BitVec n) (hf : Function.Injective f) (x y : BitVec n) (hr : ∃ (t : ℕ), f^[t] x = y) : have d := (visitScheduleFirst (cycleLabelVisits (wordCycleLabel f x) (wordCycleLabel f y))).toNat; f^[d] x = y ∧ (∀ j < d, f^[j] x ≠ y) ∧ d < 2 ^ n

theorem Cslib.Circuits.Boolean.Iteration.cycleLabelVisits_period {n : ℕ} (f : BitVec n → BitVec n) (hf : Function.Injective f) (x y : BitVec n) : (visitSchedulePeriod (cycleLabelVisits (wordCycleLabel f x) (wordCycleLabel f y))).toNat = Function.minimalPeriod f y

theorem Cslib.Circuits.Boolean.Iteration.cycleLabelVisits_spec {n : ℕ} (f : BitVec n → BitVec n) (hf : Function.Injective f) (x y : BitVec n) (t : ℕ) : f^[t] x = y ↔ visitScheduleContains (cycleLabelVisits (wordCycleLabel f x) (wordCycleLabel f y)) t

theorem Cslib.Circuits.Boolean.Iteration.synthesis_cycleLabelVisits {n a : ℕ} (s : Set (BitString a → Bool)) (x y : BitString a → BitString (n + (chartWidth n + chartWidth n))) (hx : wires x ⊆ s) (hy : wires y ⊆ s) : Synthesis interpretation s (wires fun (z : BitString a) => cycleLabelVisits (x z) (y z)) (200 * (n + 3))

Querying two already computed labels uses only linear arithmetic and wiring.

theorem Cslib.Circuits.Boolean.Iteration.cycle_label_visit_circuit {n : ℕ} (f : BitVec n → BitVec n) (labels : Circuit signature n (n + (chartWidth n + chartWidth n))) (hl : labels.Computes interpretation fun (x : Fin n → Bool) => wordCycleLabel f (word x)) : ∃ (out : Circuit signature (n + n) (visitScheduleWidth n)), (out.Computes interpretation fun (z : Fin (n + n) → Bool) => cycleLabelVisits (wordCycleLabel f (word (inputLeft z))) (wordCycleLabel f (word (inputRight z)))) ∧ out.size ≤ 2 * labels.size + 200 * (n + 3)

Any cheap cycle-label circuit for a permutation gives cheap navigation.

theorem Cslib.Circuits.Boolean.Iteration.sparse_counter_visit_circuit {n : ℕ} (f : Equiv.Perm (BitVec n)) : ∃ (out : Circuit signature (n + n) (visitScheduleWidth n)), (out.Computes interpretation fun (z : Fin (n + n) → Bool) => cycleLabelVisits (wordCycleLabel (⇑f) (word (inputLeft z))) (wordCycleLabel (⇑f) (word (inputRight z)))) ∧ out.size ≤ 1200 * (n + 3) * ((FunctionalGraph.disagreement ⇑f fun (x : BitVec n) => x + 1).card + 1)

theorem Cslib.Circuits.Boolean.Iteration.sparse_counter_visit_schedule {n : ℕ} (f : Equiv.Perm (BitVec n)) : ∃ (out : Circuit signature (n + n) (visitScheduleWidth n)), (∀ (z : BitString (n + n)) (t : ℕ), (⇑f)^[t] (word (inputLeft z)) = word (inputRight z) ↔ visitScheduleContains (out.eval interpretation z) t) ∧ (∀ (z : BitString (n + n)) (T : ℕ), {t : ℕ | t ≤ T ∧ (⇑f)^[t] (word (inputLeft z)) = word (inputRight z)}.ncard = visitScheduleCount (out.eval interpretation z) T) ∧ out.size ≤ 1200 * (n + 3) * ((FunctionalGraph.disagreement ⇑f fun (x : BitVec n) => x + 1).card + 1)

The sparse bound covers the complete visit set and its bounded-count interpretation.

theorem Cslib.Circuits.Boolean.Iteration.sparse_counter_hitting_time {n : ℕ} (f : Equiv.Perm (BitVec n)) : ∃ (out : Circuit signature (n + n) (1 + (n + 1))), (∀ (z : Fin (n + n) → Bool), out.eval interpretation z 0 = true ↔ ∃ (t : ℕ), (⇑f)^[t] (word (inputLeft z)) = word (inputRight z)) ∧ (∀ (z : Fin (n + n) → Bool), out.eval interpretation z 0 = true → have t := (word fun (i : Fin (n + 1)) => out.eval interpretation z (Fin.natAdd 1 i)).toNat; (⇑f)^[t] (word (inputLeft z)) = word (inputRight z) ∧ (∀ j < t, (⇑f)^[j] (word (inputLeft z)) ≠ word (inputRight z)) ∧ t < 2 ^ n) ∧ out.size ≤ 1200 * (n + 3) * ((FunctionalGraph.disagreement ⇑f fun (x : BitVec n) => x + 1).card + 1)

The existence flag and first hitting time have the same sparse circuit bound.

theorem Cslib.Circuits.Boolean.Iteration.sparse_coordinate_visit_schedule {n : ℕ} (f g e : Equiv.Perm (BitVec n)) (hcycle : ∀ (x : BitVec n), e (g x) = e x + 1) (encode : Circuit signature n n) (he : encode.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => (e (word x)).getLsbD ↑i) : ∃ (out : Circuit signature (n + n) (visitScheduleWidth n)), (∀ (z : BitString (n + n)) (t : ℕ), (⇑f)^[t] (word (inputLeft z)) = word (inputRight z) ↔ visitScheduleContains (out.eval interpretation z) t) ∧ (∀ (z : BitString (n + n)) (T : ℕ), {t : ℕ | t ≤ T ∧ (⇑f)^[t] (word (inputLeft z)) = word (inputRight z)}.ncard = visitScheduleCount (out.eval interpretation z) T) ∧ out.size ≤ 2 * encode.size + 1200 * (n + 3) * ((FunctionalGraph.disagreement ⇑f ⇑g).card + 1)

Pair queries need the forward coordinate map twice, but no inverse circuit.