Remainder-power equivalence and batched powers of the modular counter

Computing the T-th power of the 2 k-bit modular counter (counterStep k) is equivalent up to linear additive overhead to computing the fixed-integer remainder x ↦ T % x on k-bit moduli (counterRemainder_of_power, counterPower_of_remainder).

On a batch of r independent 2 k-bit modular counters (counterBatchPower), all r members can share a single hardwired lookup dictionary a ↦ T % a over the 2 ^ k - 1 positive k-bit moduli (residueKeys, residueValues). Each member then needs only the linear carry-safe residue addition (addResidue), giving a circuit of size at most 40000 * (k + 1) ^ 3 * (2 ^ k + r) for every r ≤ 2 ^ (k + k) (batched_counter_power). Conversely, one block of a batched circuit computes the single power with no extra gates (counterPower_of_batched), and whenever the power is not the identity every block requires its own output gate (counterBatch_size_ge_of_ne_id). Together with the counting lower bound for counterStep k, this yields matching Ω(2 ^ k / k + r) and O(k ^ 3 * (2 ^ k + r)) bounds for batched modular-counter powers (batched_hard_counter_power).

Main definitions

• Cslib.Circuits.Boolean.Iteration.counterRemainder: fixed-integer remainder x ↦ T % x on k-bit words (zero on modulus zero).
• Cslib.Circuits.Boolean.Iteration.counterBlock: block member of an r-way batched 2 k-bit state.
• Cslib.Circuits.Boolean.Iteration.counterBatchPower: the T-step modular counter applied independently to each of r blocks.
• Cslib.Circuits.Boolean.Iteration.residueKeys, Cslib.Circuits.Boolean.Iteration.residueValues: shared dictionary keys 1, …, 2 ^ k - 1 and payloads T % a.

Main results

• Cslib.Circuits.Boolean.Iteration.counterRemainder_of_power, Cslib.Circuits.Boolean.Iteration.counterPower_of_remainder: circuit equivalence between (counterStep k)^[T] and counterRemainder T.
• Cslib.Circuits.Boolean.Iteration.batched_counter_power: shared-dictionary upper bound 40000 * (k + 1) ^ 3 * (2 ^ k + r) for r ≤ 2 ^ (k + k).
• Cslib.Circuits.Boolean.Iteration.counterPower_of_batched, Cslib.Circuits.Boolean.Iteration.counterBatch_size_ge_of_ne_id, Cslib.Circuits.Boolean.Iteration.counterBatch_lower_bounds: single-block and per-block output lower bounds.
• Cslib.Circuits.Boolean.Iteration.batched_hard_counter_power: combined upper and lower bounds for hard exponents at k ≥ 64.

References

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

Remainder-power equivalence for counterStep

@[reducible, inline]

abbrev Cslib.Circuits.Boolean.Iteration.counterRemainder {k : ℕ} (T : ℕ) (x : BitString k) : BitString k

Fixed-integer remainder x ↦ T % x on k-bit words, returning 0 when the modulus is 0.

theorem Cslib.Circuits.Boolean.Iteration.word_counterRemainder {k : ℕ} (T : ℕ) (x : BitString k) : word (counterRemainder T x) = BitVec.ofNat k (if (word x).toNat = 0 then 0 else T % (word x).toNat)

theorem Cslib.Circuits.Boolean.Iteration.addResidue_eq_addWrapSpec {k : ℕ} (a b r : BitVec k) (T : ℕ) (hr : 0 < a.toNat → r.toNat = T % a.toNat) : addResidue a b r = BitVec.ofNat k (ModulusCounter.advance a.toNat b.toNat T)

Carry-safe modular addition addResidue a b r computes ModulusCounter.advance a.toNat b.toNat T whenever r.toNat = T % a.toNat on positive moduli.

theorem Cslib.Circuits.Boolean.Iteration.counterRemainder_of_power {k : ℕ} (T : ℕ) (c : Circuit signature (k + k) (k + k)) (hc : c.Computes interpretation (counterStep k)^[T]) : ∃ (out : Circuit signature k k), out.Computes interpretation (counterRemainder T) ∧ out.size ≤ c.size + 1

A circuit for (counterStep k)^[T] yields a circuit for counterRemainder T with at most one extra gate.

theorem Cslib.Circuits.Boolean.Iteration.counterPower_of_remainder {k : ℕ} (T : ℕ) (c : Circuit signature k k) (hc : c.Computes interpretation (counterRemainder T)) : ∃ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (counterStep k)^[T] ∧ out.size ≤ c.size + 100 * (k + 1)

A circuit for counterRemainder T yields a circuit for (counterStep k)^[T] with at most 100 * (k + 1) extra gates.

Batched modular-counter states and dictionary

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.divNat_finProdFinEquiv {m n : ℕ} (a : Fin m) (b : Fin n) : (finProdFinEquiv (a, b)).divNat = a

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.modNat_finProdFinEquiv {m n : ℕ} (a : Fin m) (b : Fin n) : (finProdFinEquiv (a, b)).modNat = b

def Cslib.Circuits.Boolean.Iteration.counterBlock {k r : ℕ} (x : BitString (r * (k + k))) (member : Fin r) : BitString (k + k)

Block member of a batched r * (k + k)-bit state.

def Cslib.Circuits.Boolean.Iteration.counterBatchPower {k r : ℕ} (T : ℕ) (x : BitString (r * (k + k))) : BitString (r * (k + k))

The batched modular-counter power: ModulusCounter.power T applied independently to each of r blocks.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.counterBatchPower_apply {k r : ℕ} (T : ℕ) (x : BitString (r * (k + k))) (member : Fin r) (bit : Fin (k + k)) : counterBatchPower T x (finProdFinEquiv (member, bit)) = ModulusCounter.power T (counterBlock x member) bit

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.counterBlock_counterBatchPower {k r : ℕ} (T : ℕ) (x : BitString (r * (k + k))) (member : Fin r) : counterBlock (counterBatchPower T x) member = ModulusCounter.power T (counterBlock x member)

theorem Cslib.Circuits.Boolean.Iteration.iterate_counterBatchPower {k r : ℕ} (T : ℕ) : (counterBatchPower 1)^[T] = counterBatchPower T

The batched power is the T-th iterate of the single-step batched update.

theorem Cslib.Circuits.Boolean.Iteration.counterStep_iterate_left {k : ℕ} (T : ℕ) (y : BitString (k + k)) (i : Fin k) : ModulusCounter.power T y (Fin.castAdd k i) = y (Fin.castAdd k i)

The left half (the modulus) of every state is preserved by ModulusCounter.power T.

theorem Cslib.Circuits.Boolean.Iteration.counterStep_iterate_joinState_zero {k : ℕ} (T : ℕ) (b : BitVec k) : ModulusCounter.power T (ModulusCounter.pack 0 b) = ModulusCounter.pack 0 b

States with modulus zero are fixed by ModulusCounter.power T.

theorem Cslib.Circuits.Boolean.Iteration.joinState_zero_zero {k : ℕ} : ModulusCounter.pack 0 0 = fun (x : Fin (k + k)) => false

def Cslib.Circuits.Boolean.Iteration.residueKeys (k : ℕ) (j : Fin (2 ^ k - 1)) : BitString k

Dictionary keys: the positive k-bit moduli 1, …, 2 ^ k - 1.

def Cslib.Circuits.Boolean.Iteration.residueValues (k T : ℕ) (j : Fin (2 ^ k - 1)) : BitString k

Dictionary payloads: T % a for the key a = j.val + 1.

theorem Cslib.Circuits.Boolean.Iteration.residueKeys_injective (k : ℕ) : Function.Injective (residueKeys k)

theorem Cslib.Circuits.Boolean.Iteration.clog_two_pow_add_le {k r : ℕ} (hr : r ≤ 2 ^ (k + k)) : Nat.clog 2 (r + (2 ^ k - 1)) ≤ 2 * k + 1

theorem Cslib.Circuits.Boolean.Iteration.batched_counter_power {k : ℕ} (T r : ℕ) (hr : r ≤ 2 ^ (k + k)) : ∃ (out : Circuit signature (r * (k + k)) (r * (k + k))), out.Computes interpretation (counterBatchPower T) ∧ out.size ≤ 40000 * (k + 1) ^ 3 * (2 ^ k + r)

Batched modular-counter upper bound. Using one shared residue dictionary, r independent 2 k-bit modular counters can be advanced by T steps in size at most 40000 * (k + 1) ^ 3 * (2 ^ k + r) for every r ≤ 2 ^ (k + k).

theorem Cslib.Circuits.Boolean.Iteration.counterPower_of_batched {k r : ℕ} (T : ℕ) (member : Fin r) (c : Circuit signature (r * (k + k)) (r * (k + k))) (hc : c.Computes interpretation (counterBatchPower T)) : ∃ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (ModulusCounter.power T) ∧ out.size ≤ c.size

One block of a batched circuit computes the single power with no extra gates: feed the same state to every block.

theorem Cslib.Circuits.Boolean.Iteration.counterBatch_size_ge_of_ne_id {k r : ℕ} (T : ℕ) (hT : ModulusCounter.power T ≠ id) (c : Circuit signature (r * (k + k)) (r * (k + k))) (hc : c.Computes interpretation (counterBatchPower T)) : r ≤ c.size

If ModulusCounter.power T is not the identity, every block needs its own output gate.

theorem Cslib.Circuits.Boolean.Iteration.counterBatch_lower_bounds {k r : ℕ} (T : ℕ) (hr : 0 < r) (c : Circuit signature (r * (k + k)) (r * (k + k))) (hc : c.Computes interpretation (counterBatchPower T)) : (∃ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (ModulusCounter.power T) ∧ out.size ≤ c.size) ∧ (ModulusCounter.power T ≠ id → r ≤ c.size)

Both lower bounds: a batched circuit is at least as large as any circuit for the single power, and, unless the power is the identity, has size at least r.

theorem Cslib.Circuits.Boolean.Iteration.batched_hard_counter_power (k : ℕ) (hk : 64 ≤ k) : ∃ T < ModulusCounter.period k, ∀ (r : ℕ), 0 < r → r ≤ 2 ^ (k + k) → (∃ (out : Circuit signature (r * (k + k)) (r * (k + k))), out.Computes interpretation (counterBatchPower T) ∧ out.size ≤ 40000 * (k + 1) ^ 3 * (2 ^ k + r)) ∧ ∀ (c : Circuit signature (r * (k + k)) (r * (k + k))), c.Computes interpretation (counterBatchPower T) → lowerBudget k < c.size ∧ r ≤ c.size

Batched hard modular-counter powers. For k ≥ 64, there exists an exponent T < ModulusCounter.period k such that for every 0 < r ≤ 2 ^ (k + k), counterBatchPower T has a circuit of size at most 40000 * (k + 1) ^ 3 * (2 ^ k + r) and every circuit computing it has size greater than lowerBudget k and at least r.