Sequential squaring modulo a fixed squarefree modulus

For a squarefree modulus M, write λ(M) for the Carmichael exponent, here the exponent of the unit group (ZMod M)ˣ (carmichael). Every residue, unit or not, satisfies x ^ (λ(M) + 1) = x (pow_carmichael_succ), so two positive exponents that agree modulo λ(M) give the same power map (pow_eq_pow_of_modEq). Consequently T sequential squarings are the single power x ↦ x ^ e with e = 1 + (2 ^ T - 1) % λ(M) (reducedExponent, iterate_square_reduced), for every T, including T = 0, and every residue.

Main definitions

• Cslib.Circuits.Boolean.Iteration.SequentialSquaring.carmichael: the Carmichael exponent λ(M) of ZMod M, defined as Monoid.exponent (ZMod M)ˣ.
• Cslib.Circuits.Boolean.Iteration.SequentialSquaring.reducedExponent: the reduced exponent 1 + (2 ^ T - 1) % λ(M) of T sequential squarings.

Main results

• Cslib.Circuits.Boolean.Iteration.SequentialSquaring.pow_carmichael_succ: for squarefree M, every x : ZMod M satisfies x ^ (carmichael M + 1) = x.
• Cslib.Circuits.Boolean.Iteration.SequentialSquaring.pow_eq_pow_of_modEq: positive exponents congruent modulo carmichael M induce identical power maps on ZMod M.
• Cslib.Circuits.Boolean.Iteration.SequentialSquaring.iterate_square_reduced: T sequential squarings modulo squarefree M equal x ^ reducedExponent M T.
• Cslib.Circuits.Boolean.Iteration.SequentialSquaring.crypto_table_entries: parameter table values for n = 512, 256, 128 and T = 2 ^ 40.

References

• Adapted from lean/Proofs/SequentialSquaring.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

@[reducible, inline]

noncomputable abbrev Cslib.Circuits.Boolean.Iteration.SequentialSquaring.carmichael (M : ℕ) : ℕ

The Carmichael exponent λ(M): the exponent of the unit group of ZMod M.

theorem Cslib.Circuits.Boolean.Iteration.SequentialSquaring.carmichael_pos (M : ℕ) : 0 < carmichael M

The Carmichael exponent of any modulus is positive.

theorem Cslib.Circuits.Boolean.Iteration.SequentialSquaring.pow_carmichael_succ_prime {M p : ℕ} [NeZero M] (hp : Nat.Prime p) (hpM : p ∣ M) (y : ZMod p) : y ^ (carmichael M + 1) = y

Modulo a prime divisor p of M, every residue satisfies y ^ (λ(M) + 1) = y.

theorem Cslib.Circuits.Boolean.Iteration.SequentialSquaring.pow_carmichael_succ {M : ℕ} (hM : Squarefree M) (x : ZMod M) : x ^ (carmichael M + 1) = x

For squarefree M, every residue modulo M, unit or not, satisfies x ^ (λ(M) + 1) = x.

theorem Cslib.Circuits.Boolean.Iteration.SequentialSquaring.pow_add_mul_carmichael {M : ℕ} (hM : Squarefree M) (x : ZMod M) {a : ℕ} (ha : 1 ≤ a) (k : ℕ) : x ^ (a + carmichael M * k) = x ^ a

Adding a multiple of λ(M) to a positive exponent does not change the power map.

theorem Cslib.Circuits.Boolean.Iteration.SequentialSquaring.pow_eq_pow_of_modEq {M : ℕ} (hM : Squarefree M) (x : ZMod M) {a b : ℕ} (ha : 1 ≤ a) (hb : 1 ≤ b) (h : a ≡ b [MOD carmichael M]) : x ^ a = x ^ b

For squarefree M, positive exponents congruent modulo λ(M) give the same power of every residue, including non-units.

noncomputable def Cslib.Circuits.Boolean.Iteration.SequentialSquaring.reducedExponent (M T : ℕ) : ℕ

The reduced exponent 1 + (2 ^ T - 1) % λ(M) of T squarings.

theorem Cslib.Circuits.Boolean.Iteration.SequentialSquaring.reducedExponent_le (M T : ℕ) : 1 ≤ reducedExponent M T ∧ reducedExponent M T ≤ carmichael M

The reduced exponent is positive and at most λ(M).

theorem Cslib.Circuits.Boolean.Iteration.SequentialSquaring.iterate_square_reduced {M : ℕ} (hM : Squarefree M) (T : ℕ) (x : ZMod M) : (fun (y : ZMod M) => y ^ 2)^[T] x = x ^ reducedExponent M T

Sequential squaring modulo a fixed squarefree M: for every T and every residue x, including non-units, T squarings equal the single power x ^ (1 + (2 ^ T - 1) % λ(M)).

theorem Cslib.Circuits.Boolean.Iteration.SequentialSquaring.crypto_table_entries : 512 ^ 3 * 2 ^ 512 / 2 ^ 40 = 2 ^ 499 ∧ 256 ^ 3 * 2 ^ 256 / 2 ^ 40 = 2 ^ 240 ∧ 128 ^ 3 * 2 ^ 128 / 2 ^ 40 = 2 ^ 109 ∧ (2 ^ 512).sqrt = 2 ^ 256 ∧ (2 ^ 256).sqrt = 2 ^ 128 ∧ (2 ^ 128).sqrt = 2 ^ 64

The entries of the parameter table in the cryptographic section, without the omitted constant and polynomial factors. For state lengths n = 512, 256, 128 and T = 2 ^ 40, the dictionary size n ^ 3 * 2 ^ n / T of a constant-factor speed-up is 2 ^ 499, 2 ^ 240, and 2 ^ 109, and sqrt (2 ^ n) is 2 ^ 256, 2 ^ 128, and 2 ^ 64.