Modular-counter remainders, short-exponent circuits, and variable-time equivalence

Computing ModulusCounter.power T on 2 k bits is equivalent up to O(k) gates to computing the fixed-integer remainder x ↦ T % x on k-bit moduli (ModulusCounter.remainder_of_power, ModulusCounter.power_of_remainder, counter_powers_compute_remainders). Likewise, variable-time iteration of counterStep k for an m-bit input time is equivalent up to O(k) gates to m-bit division remainder (variable_time_counter_iff_remainder).

Hardwiring m numerator bits into the streaming remainder circuit of Remainder.lean shows that any exponent T < 2 ^ m has a power circuit of size at most 110 * (m + 1) * (k + 1) (ModulusCounter.short_power_circuit). Consequently, every hard power requires an exponent of binary length m = Ω(2 ^ k / k ^ 2) (ModulusCounter.hard_power_requires_long_exponent, ModulusCounter.hard_power_exponent_capacity).

Main definitions

• Cslib.Circuits.Boolean.Iteration.ModulusCounter.remainder: fixed-integer remainder on k-bit words.
• Cslib.Circuits.Boolean.Iteration.counterInput, Cslib.Circuits.Boolean.Iteration.counterOutput: input packing and state extraction for remainder reductions.
• Cslib.Circuits.Boolean.Iteration.inputTimeRemainder: two-input remainder on m numerator bits and k modulus bits.

Main results

• Cslib.Circuits.Boolean.Iteration.ModulusCounter.remainder_of_power, Cslib.Circuits.Boolean.Iteration.ModulusCounter.power_of_remainder, Cslib.Circuits.Boolean.Iteration.counter_powers_compute_remainders: equivalence between fixed-exponent counter powers and fixed-integer remainders.
• Cslib.Circuits.Boolean.Iteration.ModulusCounter.short_remainder_circuit, Cslib.Circuits.Boolean.Iteration.ModulusCounter.short_power_circuit: linear-in-m * k circuits for exponents T < 2 ^ m.
• Cslib.Circuits.Boolean.Iteration.ModulusCounter.hard_power_requires_long_exponent, Cslib.Circuits.Boolean.Iteration.ModulusCounter.hard_power_exponent_capacity: exponential lower bound on the binary length of hard exponents.
• Cslib.Circuits.Boolean.Iteration.variable_time_counter_iff_remainder: equivalence between variable-time counter iteration and two-input remainder.

References

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

Fixed-integer remainders and equivalence with counter powers

def Cslib.Circuits.Boolean.Iteration.ModulusCounter.remainder {k : ℕ} (T : ℕ) (x : BitString k) : BitString k

Fixed-integer remainder x ↦ T % x on k-bit words, with 0 on modulus 0.

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

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

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.remainder_of_power {k : ℕ} (T : ℕ) (c : Circuit signature (k + k) (k + k)) (hc : c.Computes interpretation (power T)) : ∃ (out : Circuit signature k k), out.Computes interpretation (remainder T) ∧ out.size ≤ c.size + 1

A circuit for power T yields a circuit for remainder T with at most one extra gate.

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.power_of_remainder {k : ℕ} (T : ℕ) (c : Circuit signature k k) (hc : c.Computes interpretation (remainder T)) : ∃ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (power T) ∧ out.size ≤ c.size + 100 * (k + 1)

A circuit for remainder T yields a circuit for power T with at most 100 * (k + 1) extra gates.

Short-exponent upper bounds and exponent-length lower bounds

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.short_remainder_circuit (k m T : ℕ) (hT : T < 2 ^ m) : ∃ (out : Circuit signature k k), out.Computes interpretation (remainder T) ∧ out.size ≤ m * (51 * (k + 1) + 4) + 10 * (k + 1)

Hardwiring m numerator bits into bounded_modulus_remainder and masking modulus zero gives a circuit for remainder T of size linear in m * (k + 1).

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.short_power_circuit (k m T : ℕ) (hT : T < 2 ^ m) : ∃ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (power T) ∧ out.size ≤ 110 * (m + 1) * (k + 1)

A fixed exponent T < 2 ^ m gives a circuit for power T of size at most 110 * (m + 1) * (k + 1).

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.hard_power_requires_long_exponent (k m T : ℕ) (hT : T < 2 ^ m) (hard : ∀ (c : Circuit signature (k + k) (k + k)), c.Computes interpretation (power T) → lowerBudget k < c.size) : lowerBudget k < 110 * (m + 1) * (k + 1)

Any exponent whose counter power requires more than lowerBudget k gates needs lowerBudget k < 110 * (m + 1) * (k + 1).

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.hard_power_exponent_capacity (k m T : ℕ) (hT : T < 2 ^ m) (hard : ∀ (c : Circuit signature (k + k) (k + k)), c.Computes interpretation (power T) → lowerBudget k < c.size) : 2 ^ k < 112640 * (m + 1) * (k + 1) ^ 2

Explicit exponential lower bound on the binary length m of any hard exponent T < 2 ^ m.

Remainder helpers and variable-time equivalence

def Cslib.Circuits.Boolean.Iteration.counterInput {k : ℕ} (x : BitString k) : BitString (k + k)

Pack a k-bit modulus x with initial counter state 0.

def Cslib.Circuits.Boolean.Iteration.counterOutput {k : ℕ} (y : BitString (k + k)) : BitString k

Extract the k-bit counter state from a 2 k-bit state.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.counterInput_modulus_toNat {k : ℕ} (x : BitString k) : (ModulusCounter.leftWord (counterInput x)).toNat = (word x).toNat

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.counterInput_state_toNat {k : ℕ} (x : BitString k) : (ModulusCounter.rightWord (counterInput x)).toNat = 0

theorem Cslib.Circuits.Boolean.Iteration.counterRemainder_spec {k : ℕ} (T : ℕ) (x : BitString k) : counterOutput ((counterStep k)^[T] (counterInput x)) = ModulusCounter.remainder T x

theorem Cslib.Circuits.Boolean.Iteration.counter_powers_compute_remainders (k T : ℕ) : (∀ (c : Circuit signature (k + k) (k + k)), c.Computes interpretation (ModulusCounter.power T) → ∃ (out : Circuit signature k k), out.Computes interpretation (ModulusCounter.remainder T) ∧ out.size ≤ c.size + 1) ∧ ∀ (c : Circuit signature k k), c.Computes interpretation (ModulusCounter.remainder T) → ∃ (out : Circuit signature (k + k) (k + k)), out.Computes interpretation (ModulusCounter.power T) ∧ out.size ≤ c.size + 100 * (k + 1)

Computing ModulusCounter.power T and computing ModulusCounter.remainder T are equivalent up to linear additive overhead.

def Cslib.Circuits.Boolean.Iteration.inputTimeRemainder (m k : ℕ) (x : BitString (m + k)) : BitString k

Two-input remainder function on m numerator bits followed by k modulus bits, returning 0 when the modulus is 0.

theorem Cslib.Circuits.Boolean.Iteration.variable_time_counter_iff_remainder (m k : ℕ) : (∀ (c : Circuit signature (k + k + m) (k + k)), c.Computes interpretation (inputTimeIterate (counterStep k) m) → ∃ (out : Circuit signature (m + k) k), out.Computes interpretation (inputTimeRemainder m k) ∧ out.size ≤ c.size + 1) ∧ ∀ (c : Circuit signature (m + k) k), c.Computes interpretation (inputTimeRemainder m k) → ∃ (out : Circuit signature (k + k + m) (k + k)), out.Computes interpretation (inputTimeIterate (counterStep k) m) ∧ out.size ≤ c.size + 100 * (k + 1)

Variable-time iteration of counterStep k for an m-bit input time is equivalent up to O(k) gates to computing the m-bit remainder inputTimeRemainder m k.