The modular-counter permutation: state, period, and linear-size step circuit

On 2 k bits split into a k-bit modulus a (leftWord) and a k-bit state b (rightWord), ModulusCounter.power T advances b to (b + T) % a whenever 0 < a and b < a, and fixes all other states (advance). For T = 1, this defines a permutation counterStep k = ModulusCounter.power 1 computed by a native De Morgan circuit of linear size at most 50 * k + 20 (counterStep_circuit, ModulusCounter.exists_linear_circuit).

Every active modulus 1 ≤ a ≤ 2 ^ k - 1 divides ModulusCounter.period k = lcm(1, …, 2 ^ k - 1), and distinct exponents below ModulusCounter.period k give distinct Boolean functions (ModulusCounter.powers_injective, counter_power_ne).

Main definitions

• Cslib.Circuits.Boolean.Iteration.ModulusCounter.advance: advance b by T modulo a when 0 < a and b < a.
• Cslib.Circuits.Boolean.Iteration.ModulusCounter.leftWord, Cslib.Circuits.Boolean.Iteration.ModulusCounter.rightWord, Cslib.Circuits.Boolean.Iteration.ModulusCounter.pack: split and pack k-bit modulus and state words in BitString (k + k).
• Cslib.Circuits.Boolean.Iteration.ModulusCounter.power: T-step modular counter map on BitString (k + k).
• Cslib.Circuits.Boolean.Iteration.ModulusCounter.period: Nat.lcmUpto (2 ^ k - 1).
• Cslib.Circuits.Boolean.Iteration.ModulusCounter.stepValue: next counter word after one step.
• Cslib.Circuits.Boolean.Iteration.counterModulus, Cslib.Circuits.Boolean.Iteration.counterStepValue, Cslib.Circuits.Boolean.Iteration.counterStep, Cslib.Circuits.Boolean.Iteration.counterNextBits: top-level single-step modular counter permutation and helpers.

Main results

• Cslib.Circuits.Boolean.Iteration.ModulusCounter.power_bijective: the single-step counter map is a bijection.
• Cslib.Circuits.Boolean.Iteration.ModulusCounter.powers_injective: powers below period k are pairwise distinct.
• Cslib.Circuits.Boolean.Iteration.ModulusCounter.exists_linear_circuit, Cslib.Circuits.Boolean.Iteration.counterStep_circuit: counterStep k has a De Morgan circuit of size at most 50 * k + 20.

References

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

Modular counter semantics and period

def Cslib.Circuits.Boolean.Iteration.ModulusCounter.advance (a b T : ℕ) : ℕ

Advance b by T modulo a when 0 < a and b < a; inactive pairs are fixed.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.advance_zero (a b : ℕ) : advance a b 0 = b

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.advance_lt {a b U T : ℕ} (ha : a < U) (hb : b < U) : advance a b T < U

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.advance_add (a b S T : ℕ) : advance a (advance a b S) T = advance a b (S + T)

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

The k-bit modulus word in the first k coordinates.

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

The k-bit counter state word in the last k coordinates.

def Cslib.Circuits.Boolean.Iteration.ModulusCounter.pack {k : ℕ} (a b : BitVec k) : BitString (k + k)

Pack a k-bit modulus word and a k-bit counter state word into BitString (k + k).

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.leftWord_pack {k : ℕ} (a b : BitVec k) : leftWord (pack a b) = a

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.rightWord_pack {k : ℕ} (a b : BitVec k) : rightWord (pack a b) = b

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.pack_words {k : ℕ} (x : BitString (k + k)) : pack (leftWord x) (rightWord x) = x

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

The T-step modular counter map on BitString (k + k).

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.power_zero {k : ℕ} (x : BitString (k + k)) : power 0 x = x

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.power_add {k : ℕ} (S T : ℕ) (x : BitString (k + k)) : power T (power S x) = power (S + T) x

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.iterate_power {k : ℕ} (T : ℕ) : (power 1)^[T] = power T

def Cslib.Circuits.Boolean.Iteration.ModulusCounter.period (k : ℕ) : ℕ

The order lcm(1, …, 2 ^ k - 1) common to every active k-bit modular counter.

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.modulus_dvd_period {k a : ℕ} (ha : 0 < a) (haU : a < 2 ^ k) : a ∣ period k

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.power_period {k : ℕ} (x : BitString (k + k)) : power (period k) x = x

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.power_bijective {k : ℕ} : Function.Bijective (power 1)

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.powers_injective {k : ℕ} : Function.Injective fun (T : Fin (period k)) => power ↑T

Different residues modulo period k give different Boolean functions.

Linear-size step circuit

def Cslib.Circuits.Boolean.Iteration.ModulusCounter.stepValue {k : ℕ} (a b : BitVec k) : BitVec k

Next counter word after one step: increment b modulo a when b < a.

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.stepValue_spec {k : ℕ} (a b : BitVec k) : stepValue a b = BitVec.ofNat k (advance a.toNat b.toNat 1)

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.synthesis_word_eq {k n : ℕ} (s : Set (BooleanFunction n)) (a b : BitString n → BitVec k) (ha : ∀ (i : Fin k), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin k), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) : Synthesis interpretation s {fun (x : BitString n) => decide (a x = b x)} (6 * k + 1)

Equality of two available k-bit words costs at most 6 * k + 1 gates.

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.synthesis_stepValue {k n : ℕ} (src : Set (BooleanFunction n)) (a b : BitString n → BitVec k) (ha : ∀ (i : Fin k), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ src) (hb : ∀ (i : Fin k), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ src) (hc : ∀ (v : Bool), (fun (x : BitString n) => v) ∈ src) : Synthesis interpretation src (wordWires fun (x : BitString n) => stepValue (a x) (b x)) (50 * k + 18)

Synthesizing stepValue (a x) (b x) from available words and constants costs at most 50 * k + 18 gates.

theorem Cslib.Circuits.Boolean.Iteration.ModulusCounter.exists_linear_circuit (k : ℕ) : ∃ (c : Circuit signature (k + k) (k + k)), c.Computes interpretation (power 1) ∧ c.size ≤ 50 * k + 20

The single-step modular counter power 1 has a De Morgan circuit of size at most 50 * k + 20.

Top-level counter definitions

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

The modulus as a natural number.

def Cslib.Circuits.Boolean.Iteration.counterStepValue (a b : ℕ) : ℕ

Single-step modular counter transition on natural numbers.

def Cslib.Circuits.Boolean.Iteration.counterStep (k : ℕ) : BitString (k + k) → BitString (k + k)

Single-step modular counter permutation on BitString (k + k).

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

Coordinate bits of ModulusCounter.stepValue (ModulusCounter.leftWord x) (ModulusCounter.rightWord x).

theorem Cslib.Circuits.Boolean.Iteration.counterModulus_eq_of_eq {k : ℕ} {x y : BitString (k + k)} (h : (fun (i : Fin k) => x (Fin.castAdd k i)) = fun (i : Fin k) => y (Fin.castAdd k i)) : counterModulus x = counterModulus y

theorem Cslib.Circuits.Boolean.Iteration.counterStep_preserve_modulus {k : ℕ} (x : BitString (k + k)) : counterModulus (counterStep k x) = counterModulus x

theorem Cslib.Circuits.Boolean.Iteration.counterStepValue_iterate (a b T : ℕ) : (counterStepValue a)^[T] b = ModulusCounter.advance a b T

theorem Cslib.Circuits.Boolean.Iteration.counterStep_iterate_toNat {k : ℕ} (T : ℕ) (x : BitString (k + k)) : (ModulusCounter.rightWord ((counterStep k)^[T] x)).toNat = ModulusCounter.advance (ModulusCounter.leftWord x).toNat (ModulusCounter.rightWord x).toNat T

theorem Cslib.Circuits.Boolean.Iteration.counter_power_ne {k S T : ℕ} (hS : S < ModulusCounter.period k) (hT : T < ModulusCounter.period k) (hne : S ≠ T) : (counterStep k)^[S] ≠ (counterStep k)^[T]

Distinct exponents below ModulusCounter.period k produce distinct counter powers.

theorem Cslib.Circuits.Boolean.Iteration.counter_family_card (k : ℕ) : (Finset.image (fun (T : Fin (ModulusCounter.period k)) => ModulusCounter.power ↑T) Finset.univ).card = ModulusCounter.period k

theorem Cslib.Circuits.Boolean.Iteration.counterStep_circuit (k : ℕ) : ∃ (c : Circuit signature (k + k) (k + k)), c.Computes interpretation (counterStep k) ∧ c.size ≤ 50 * k + 20

The single-step modular counter counterStep k has a De Morgan circuit of size at most 50 * k + 20.