Circuits returning complete visit schedules

For any finite map f : BitString n → BitString n and state pair (x, y), the set of times t at which f^[t] x = y is either empty or an arithmetic progression d + k * p where d < 2 ^ n is the first hitting time and p = Function.minimalPeriod f y is the minimal return period of y (with p = 0 when y is transient, encoding the singleton {d}).

Combining navigation_circuit (which computes the reachability bit and the (n + 1)-bit first hitting time d) with minimal_period_circuit (which computes the (n + 1)-bit minimal period p of y from cycle_label_circuit and periodicPts_circuit) yields a circuit of size O(powerBudget n c.size (2 ^ n) L) returning the complete visit schedule record (visit_schedule_circuit), and O(optimizedBudget n c.size (2 ^ n)) at the balanced checkpoint spacing (visit_schedule_optimized).

Main definitions

• Cslib.Circuits.Boolean.Iteration.visitScheduleWidth: bit width (1 + (n + 1)) + (n + 1) of a visit-schedule record.
• Cslib.Circuits.Boolean.Iteration.visitScheduleFirst: unpacks the (n + 1)-bit first visit time.
• Cslib.Circuits.Boolean.Iteration.visitSchedulePeriod: unpacks the (n + 1)-bit return period.
• Cslib.Circuits.Boolean.Iteration.visitScheduleContains: membership of a time t in the schedule encoded by a record.
• Cslib.Circuits.Boolean.Iteration.visitScheduleCount: number of visits up to a deadline T encoded by a record.

Main results

• Cslib.Circuits.Boolean.Iteration.minimal_period_circuit: computes Function.minimalPeriod f x in n + 1 bits within 110000 * powerBudget n c.size (2 ^ n) L gates.
• Cslib.Circuits.Boolean.Iteration.visitScheduleCount_spec: visitScheduleCount v T equals the cardinality of {t ≤ T | visitScheduleContains v t}.
• Cslib.Circuits.Boolean.Iteration.visit_schedule_circuit: computes the complete visit-schedule record within 5000000 * powerBudget n c.size (2 ^ n) L gates.
• Cslib.Circuits.Boolean.Iteration.visit_schedule_optimized: square-root-size circuit returning complete visit schedules and bounded visit counts.

References

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

theorem Cslib.Circuits.Boolean.Iteration.minimal_period_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature n (n + 1)), (∀ (x : Fin n → Bool), (word (out.eval interpretation x)).toNat = Function.minimalPeriod (c.eval interpretation) x) ∧ out.size ≤ 110000 * powerBudget n c.size (2 ^ n) L

Minimal return period, with zero denoting a transient state.

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Iteration.visitScheduleWidth (n : ℕ) : ℕ

One reachability bit, an (n + 1)-bit first visit time, and an (n + 1)-bit return period.

def Cslib.Circuits.Boolean.Iteration.visitScheduleFirst {n : ℕ} (v : BitString (visitScheduleWidth n)) : BitVec (n + 1)

The (n + 1)-bit first hitting time field of a visit-schedule record.

def Cslib.Circuits.Boolean.Iteration.visitSchedulePeriod {n : ℕ} (v : BitString (visitScheduleWidth n)) : BitVec (n + 1)

The (n + 1)-bit return period field of a visit-schedule record.

def Cslib.Circuits.Boolean.Iteration.visitScheduleContains {n : ℕ} (v : BitString (visitScheduleWidth n)) (t : ℕ) : Prop

Whether time t belongs to the arithmetic progression encoded by v.

def Cslib.Circuits.Boolean.Iteration.visitScheduleCount {n : ℕ} (v : BitString (visitScheduleWidth n)) (T : ℕ) : ℕ

An arithmetic interpretation of a schedule; no additional-input gate bound is asserted.

theorem Cslib.Circuits.Boolean.Iteration.visitScheduleCount_spec {n : ℕ} (v : BitString (visitScheduleWidth n)) (T : ℕ) : {t : ℕ | t ≤ T ∧ visitScheduleContains v t}.ncard = visitScheduleCount v T

theorem Cslib.Circuits.Boolean.Iteration.visit_schedule_circuit {n : ℕ} (c : Circuit signature n n) (L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) : ∃ (out : Circuit signature (n + n) (visitScheduleWidth n)), (∀ (z : BitString (n + n)) (t : ℕ), (c.eval interpretation)^[t] (inputLeft z) = inputRight z ↔ visitScheduleContains (out.eval interpretation z) t) ∧ out.size ≤ 5000000 * powerBudget n c.size (2 ^ n) L

Visit-schedule circuit at spacing L. The returned record describes every visit time, with period zero encoding a singleton visit to a transient target.

theorem Cslib.Circuits.Boolean.Iteration.visit_schedule_optimized {n : ℕ} (c : Circuit signature n n) : ∃ (out : Circuit signature (n + n) (visitScheduleWidth n)), (∀ (z : BitString (n + n)) (t : ℕ), (c.eval interpretation)^[t] (inputLeft z) = inputRight z ↔ visitScheduleContains (out.eval interpretation z) t) ∧ (∀ (z : BitString (n + n)) (T : ℕ), {t : ℕ | t ≤ T ∧ (c.eval interpretation)^[t] (inputLeft z) = inputRight z}.ncard = visitScheduleCount (out.eval interpretation z) T) ∧ ↑out.size ≤ 15000000 * optimizedBudget n c.size (2 ^ n)

Square-root visit-schedule circuit. Optimizing L gives a circuit of size at most 15000000 * optimizedBudget n c.size (2 ^ n) whose output record characterizes all visit times and determines the exact visit count up to any deadline T.