Reconstructing the fixed power from a detected pair

A detected pair of records determines f^[T] x (reconstruct_spec). If the prefix state at time d is a checkpoint, the checkpoint's payload is f^[T - K] of it, and K - d further steps of the payload give f^[T] x; the circuit computes all of the payload's first K steps and selects one (hitValue). If the prefix repeats between times i < j, the state at the time in [i, j) congruent to T is selected from the prefix (repeatedValue). All branches are total, also on pairs that a detector never produces.

Main definitions

• Cslib.Circuits.Boolean.Iteration.hitValue: the state after (BitVec.ofNat w K - index).toNat steps from a checkpoint payload (using the selector's out-of-range fallback above K).
• Cslib.Circuits.Boolean.Iteration.repeatedValue: the prefix state at the time in [lo, hi) congruent to T.
• Cslib.Circuits.Boolean.Iteration.reconstruct: the state determined by a pair of records.
• Cslib.Circuits.Boolean.Iteration.prefixWires: the wire functions of the prefix states up to time K.

Main results

• Cslib.Circuits.Boolean.Iteration.reconstruct_spec: a witness pair determines f^[T] x.
• Cslib.Circuits.Boolean.Iteration.synthesis_reconstruct: its gate count.

References

• Adapted from lean/Proofs/{Decoder,DecoderCircuits,Reconstruction}.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

def Cslib.Circuits.Boolean.Iteration.hitValue {n w : ℕ} (f : BitString n → BitString n) (K : ℕ) (index : BitVec w) (payload : BitString n) : BitString n

The state K - index steps after payload.

def Cslib.Circuits.Boolean.Iteration.repeatedValue {n w : ℕ} (f : BitString n → BitString n) (T K : ℕ) (x : BitString n) (lo hi : BitVec w) : BitString n

The prefix state at the time in [lo, hi) congruent to T.

def Cslib.Circuits.Boolean.Iteration.reconstruct {n w : ℕ} (f : BitString n → BitString n) (T K : ℕ) (x : BitString n) (a b : Record n w) : BitString n

The state determined by a pair of records: by a checkpoint's payload if either is one, and otherwise by the repeat between the two query times.

theorem Cslib.Circuits.Boolean.Iteration.hitValue_spec {n w : ℕ} (f : BitString n → BitString n) (T K d : ℕ) (x : BitString n) (hd : d ≤ K) (hK : K < 2 ^ w) (hT : K ≤ T) : hitValue f K (BitVec.ofNat w d) (f^[T - K] (f^[d] x)) = f^[T] x

Stepping K - d times from the checkpoint payload f^[T - K] (f^[d] x) recovers f^[T] x.

theorem Cslib.Circuits.Boolean.Iteration.reconstruct_spec {n w M : ℕ} (f : BitString n → BitString n) (T K : ℕ) (checkpoints : Fin M → BitString n) (x : BitString n) (a b : Record n w) (hK : K < 2 ^ w) (hT : K ≤ T) (h : Record.Witness f T K checkpoints x a b) : reconstruct f T K x a b = f^[T] x

A witness pair determines the state at time T.

Gate counts

def Cslib.Circuits.Boolean.Iteration.prefixWires {n : ℕ} (f : BitString n → BitString n) (K : ℕ) : Set (BooleanFunction n)

The prefix states up to time K.

theorem Cslib.Circuits.Boolean.Iteration.prefix_mem {n : ℕ} (f : BitString n → BitString n) {K j : ℕ} (hj : j ≤ K) (bit : Fin n) : (fun (x : BitString n) => f^[j] x bit) ∈ prefixWires f K

Every bit wire of f^[j] for j ≤ K belongs to prefixWires f K.

theorem Cslib.Circuits.Boolean.Iteration.synthesis_hitValue {n w a : ℕ} (s : Set (BooleanFunction a)) (c : Circuit signature n n) (K : ℕ) (index : BitString a → BitVec w) (payload : BitString a → BitString n) (hi : ∀ (i : Fin w), (fun (x : BitString a) => (index x).getLsbD ↑i) ∈ s) (hp : wires payload ⊆ s) (hc : ∀ (b : Bool), (fun (x : BitString a) => b) ∈ s) : Synthesis interpretation s (wires fun (x : BitString a) => hitValue (c.eval interpretation) K (index x) (payload x)) (K * c.size + 200 * (K + 1) * (n + w + 1) ^ 2)

Synthesizes hitValue by unfolding K steps of c from payload and selecting the step at the unsigned value of BitVec.ofNat w K - index x (with the selector's out-of-range fallback).

theorem Cslib.Circuits.Boolean.Iteration.synthesis_reconstruct {n w : ℕ} (s : Set (BooleanFunction n)) (c : Circuit signature n n) (T K : ℕ) (a b : BitString n → Record n w) (ha : Record.wireSet a ⊆ s) (hb : Record.wireSet b ⊆ s) (hp : prefixWires (c.eval interpretation) K ⊆ s) (hc : ∀ (b : Bool), (fun (x : BitString n) => b) ∈ s) : Synthesis interpretation s (wires fun (x : BitString n) => reconstruct (c.eval interpretation) T K x (a x) (b x)) (4 * K * c.size + 1000 * (K + 1) * (n + w + 1) ^ 2)

The reconstruction circuit: two payload orbits, two residue branches and their selection.