Sparse counter modifications with a live iteration count

Let r be the number of inputs where the permutation differs from the counter. Encoding and decoding cost O((n+1)*(r+1)) and are each performed once. The middle stage costs O((n+1)*(m+1)) for an m-bit time, giving additive dependence on edits and time width. The theorem constructs actual CSLib Boolean circuits from any permutation. The initial state occupies the first n inputs; the last m are the nonnegative iteration count in least-significant-bit-first order. Constants and selectors are charged. The chart is chosen nonuniformly; no bound on its construction runtime or on generating the output circuit is asserted.

Main definitions

• The input consists of an initial state followed by a binary iteration count.

Main results

• sparse_counter_variable_time: additive dependence on edits and time width.
• sparse_counter_labels: canonical coordinates at linear table cost.
• sparse_coordinate_variable_time: both coordinate conversions charged.

References

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

theorem Cslib.Circuits.Boolean.Iteration.CounterIntervalChart.variable_time {n R : ℕ} {f : BitVec n → BitVec n} (chart : CounterIntervalChart f R) (hf : Function.Injective f) (m : ℕ) : ∃ (out : Circuit signature (n + m) n), (out.Computes interpretation fun (z : Fin (n + m) → Bool) (i : Fin n) => (f^[(word fun (j : Fin m) => z (Fin.natAdd n j)).toNat] (word fun (j : Fin n) => z (Fin.castAdd m j))).getLsbD ↑i) ∧ out.size ≤ 1000 * (n + 3) * (R + m)

theorem Cslib.Circuits.Boolean.Iteration.sparse_counter_variable_time {n : ℕ} (f : Equiv.Perm (BitVec n)) (m : ℕ) : ∃ (out : Circuit signature (n + m) n), (out.Computes interpretation fun (z : Fin (n + m) → Bool) (i : Fin n) => ((⇑f)^[(word fun (j : Fin m) => z (Fin.natAdd n j)).toNat] (word fun (j : Fin n) => z (Fin.castAdd m j))).getLsbD ↑i) ∧ out.size ≤ 1000 * (n + 3) * ((FunctionalGraph.disagreement ⇑f fun (x : BitVec n) => x + 1).card + m + 1)

Every sparsely edited counter permutation has an additive live-time bound. Both the time and initial state are inputs; no edit-list or chart certificate is an input or hypothesis of the resulting Boolean circuit.

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

The same chart computes canonical cycle labels and phase in linear table cost.

theorem Cslib.Circuits.Boolean.Iteration.sparse_coordinate_variable_time {n : ℕ} (f g e : Equiv.Perm (BitVec n)) (hcycle : ∀ (x : BitVec n), e (g x) = e x + 1) (encode decode : Circuit signature n n) (he : encode.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => (e (word x)).getLsbD ↑i) (hd : decode.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => ((Equiv.symm e) (word x)).getLsbD ↑i) (m : ℕ) : ∃ (out : Circuit signature (n + m) n), (out.Computes interpretation fun (z : Fin (n + m) → Bool) (i : Fin n) => ((⇑f)^[(word fun (j : Fin m) => z (Fin.natAdd n j)).toNat] (word fun (j : Fin n) => z (Fin.castAdd m j))).getLsbD ↑i) ∧ out.size ≤ encode.size + decode.size + 1000 * (n + 3) * ((FunctionalGraph.disagreement ⇑f ⇑g).card + m + 1)

Charged coordinate changes preserve the additive live-time bound.