Finishing trajectories with a shared checkpoint dictionary

Several fixed-power computations can share their checkpoint table. One batched lookup answers, for every state of every orbit prefix, whether it is a checkpoint and which state the table stores with it (synthesis_lookupOr); the lookup sorts all queries together with the table once, using batchOrCircuit. Each trajectory then finishes on its own: the last flagged prefix time selects a payload, which is advanced by the remaining steps (finishHit, synthesis_finishHit), and a trajectory without a flagged time must repeat early, where the fixed-power circuit without checkpoints is correct (exists_repeat_power).

All gates of the native De Morgan basis, including constants, are charged; wiring and fanout are free.

Main definitions

• Cslib.Circuits.Boolean.Iteration.lookupOr: the OR of the values stored under a key.
• Cslib.Circuits.Boolean.Iteration.finishHit: the state reached from the last flagged hit.

Main results

• Cslib.Circuits.Boolean.Iteration.synthesis_lookupOr: one shared lookup for many queries.
• Cslib.Circuits.Boolean.Iteration.finishHit_correct, Cslib.Circuits.Boolean.Iteration.synthesis_finishHit: finishing one trajectory.
• Cslib.Circuits.Boolean.Iteration.exists_repeat_power: a fixed power on orbits that repeat early, with no checkpoints.

References

• Adapted from lean/Proofs/{BatchLookup,BatchFinish}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.
• The lookup is batchOrCircuit, after S. Schlesinger, Boolean circuit mass production formalization.

Shared lookup

def Cslib.Circuits.Boolean.Iteration.lookupOr {M k v : ℕ} (keys : Fin M → BitString k) (values : Fin M → BitString v) (key : BitString k) : BitString v

The bitwise OR of the values stored under key. With distinct keys this is the value stored under key, and all-false if key is absent (lookupOr_of_eq, lookupOr_of_forall_ne).

theorem Cslib.Circuits.Boolean.Iteration.lookupOr_of_eq {M k v : ℕ} {keys : Fin M → BitString k} (values : Fin M → BitString v) (hkeys : Function.Injective keys) {j : Fin M} {key : BitString k} (h : keys j = key) : lookupOr keys values key = values j

theorem Cslib.Circuits.Boolean.Iteration.lookupOr_of_forall_ne {M k v : ℕ} {keys : Fin M → BitString k} (values : Fin M → BitString v) {key : BitString k} (h : ∀ (j : Fin M), keys j ≠ key) : lookupOr keys values key = fun (x : Fin v) => false

theorem Cslib.Circuits.Boolean.Iteration.synthesis_lookupOr {a M k v Q : ℕ} (s : Set (BooleanFunction a)) (keys : Fin M → BitString k) (values : Fin M → BitString v) (queries : BitString a → Fin Q → BitString k) (hq : ∀ (q : Fin Q) (bit : Fin k), (fun (x : BitString a) => queries x q bit) ∈ s) : Synthesis interpretation s (⋃ (q : Fin Q), wires fun (x : BitString a) => lookupOr keys values (queries x q)) (48 * (Q + M + 1) * (Nat.clog 2 (Q + M) + 1) ^ 2 * (k + v + 1))

Shared lookup. Answering Q available queries against one hardwired table of M keys costs one batchOrCircuit: at most 48 * (Q + M + 1) * (⌈log₂ (Q + M)⌉ + 1) ^ 2 * (k + v + 1) gates, constants included.

Finishing one trajectory

def Cslib.Circuits.Boolean.Iteration.hitRecord {n w : ℕ} (index : ℕ) (payload : BitString n) : BitString (w + n + 1)

A hit at prefix time index with stored state payload: a set flag, then index in w bits, then the payload.

def Cslib.Circuits.Boolean.Iteration.hitIndex {n w : ℕ} (record : BitString (w + n + 1)) : BitVec w

The time field of a hit record.

def Cslib.Circuits.Boolean.Iteration.hitPayload {n w : ℕ} (record : BitString (w + n + 1)) : BitString n

The payload field of a hit record.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.hitRecord_zero {n w : ℕ} (index : ℕ) (payload : BitString n) : hitRecord index payload 0 = true

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.hitIndex_hitRecord {n w : ℕ} (index : ℕ) (payload : BitString n) : hitIndex (hitRecord index payload) = BitVec.ofNat w index

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.hitPayload_hitRecord {n w : ℕ} (index : ℕ) (payload : BitString n) : hitPayload (hitRecord index payload) = payload

def Cslib.Circuits.Boolean.Iteration.finishHit {n w : ℕ} (f : BitString n → BitString n) (K : ℕ) (flags : Fin (K + 1) → Bool) (payloads : Fin (K + 1) → BitString n) (fallback : BitString n) : BitString n

The state K - j steps after the payload at the last flagged prefix time j, or fallback if no time is flagged.

theorem Cslib.Circuits.Boolean.Iteration.finishHit_correct {n w : ℕ} (f : BitString n → BitString n) (T K : ℕ) (x : BitString n) (flags : Fin (K + 1) → Bool) (payloads : Fin (K + 1) → BitString n) (fallback : BitString n) (hK : K < 2 ^ w) (hT : K ≤ T) (hyes : ∀ (j : Fin (K + 1)), flags j = true → payloads j = f^[T - K] (f^[↑j] x)) (hno : (∀ (j : Fin (K + 1)), flags j = false) → fallback = f^[T] x) : finishHit f K flags payloads fallback = f^[T] x

If every flagged prefix time j carries f^[T - K] (f^[j] x), and the fallback is correct when no time is flagged, the finished state is f^[T] x.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_finishHit {n w a : ℕ} (c : Circuit signature n n) (s : Set (BooleanFunction a)) (K : ℕ) (flags : BitString a → Fin (K + 1) → Bool) (payloads : BitString a → Fin (K + 1) → BitString n) (fallback : BitString a → BitString n) (hf : ∀ (j : Fin (K + 1)), (fun (x : BitString a) => flags x j) ∈ s) (hp : ∀ (j : Fin (K + 1)) (bit : Fin n), (fun (x : BitString a) => payloads x j bit) ∈ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) {C : ℕ} (hfall : Synthesis interpretation s (wires fallback) C) : Synthesis interpretation s (wires fun (x : BitString a) => finishHit (c.eval interpretation) K (flags x) (payloads x) (fallback x)) ((K + 1) * (4 * (w + n + 1)) + K * c.size + 200 * (K + 1) * (n + w + 1) ^ 2 + C + 4 * n)

Finishing a trajectory: selecting the last hit, advancing its payload and choosing the fallback.

theorem Cslib.Circuits.Boolean.Iteration.exists_repeat_power {n : ℕ} (c : Circuit signature n n) (T L : ℕ) (hL : 0 < L) (hLN : L ≤ 2 ^ n) (hT : 2 * L ≤ T) : ∃ (out : Circuit signature n n), (∀ (x : Fin n → Bool), FunctionalGraph.Repeats (c.eval interpretation) x L → out.eval interpretation x = (c.eval interpretation)^[T] x) ∧ out.size ≤ 40000 * powerBudget n c.size 0 L

Fixed powers on early repeats. The fixed-power circuit without checkpoints computes f^[T] on every state whose orbit repeats among its first L states, for 2 L ≤ T.