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.reconstruct: the state determined by a pair of records.

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

theorem Cslib.Circuits.Boolean.Iteration.repeatedValue_spec {n w : ℕ} (f : BitString n → BitString n) (T K i j : ℕ) (x : BitString n) (hij : i < j) (hj : j ≤ K) (hK : K < 2 ^ w) (hT : K ≤ T) (heq : f^[i] x = f^[j] x) : repeatedValue f T K x (BitVec.ofNat w i) (BitVec.ofNat w j) = 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

theorem Cslib.Circuits.Boolean.Iteration.synthesis_repeatedValue {n w : ℕ} (s : Set (BooleanFunction n)) (f : BitString n → BitString 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) (hp : prefixWires f K ⊆ s) (hc : ∀ (b : Bool), (fun (x : BitString n) => b) ∈ s) : Synthesis interpretation s (wires fun (x : BitString n) => repeatedValue f T K x (lo x) (hi x)) (200 * (K + 1) * (n + w + 1) ^ 2)

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)

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.