Crypto

Stream: general

[Leonardo de Moura]

A colleague of mine is interested in proving the following result in Lean for a piece of crypto code. Here is the problem description he shared with me.

Hypotheses:

• Q = 3329
• 0 < A < Q
• 0 < B < Q

Given that, please prove that ((A * B) div Q) * Q != (A * B) where “div” is truncating integer division (rounding down towards zero).

[Johan Commelin]

Formal statement

import Mathlib.Data.Nat.Prime
import Mathlib.Tactic.NormNum

theorem challenge_aux (p a b : ℕ) (hp : p.Prime) (h0a : 0 < a) (ha: a < p) (h0b : 0 < b) (hb : b < p) :
    (a * b) / p * p ≠ a * b := by
  sorry

theorem challenge (q a b : ℕ) (hq : q = 3329) (h0a : 0 < a) (ha: a < q) (h0b : 0 < b) (hb : b < q) :
    (a * b) / q * q ≠ a * b := by
  apply challenge_aux _ _ _ _ h0a ha h0b hb
  rw [hq]
  show Nat.Prime 3329
  sorry

[Eric Wieser]

import Mathlib
example {Q : ℕ} (hQ : Q = 3329)
    (hA : 0 < A ∧ A < Q)
    (hB : 0 < B ∧ B < Q) :
    ((A * B) / Q) * Q ≠ (A * B) := by
  intro h
  have hP : Nat.Prime Q := by norm_num [hQ]
  have : Q ∣ (A * B) := dvd_of_mul_left_eq _ h
  apply hP.not_dvd_mul _ _ this
  · intro hAd
    exact hA.1.ne' <| Nat.eq_zero_of_dvd_of_lt hAd hA.2
  · intro hBd
    exact hB.1.ne' <| Nat.eq_zero_of_dvd_of_lt hBd hB.2

Last sorry should be easy

[Johan Commelin]

Which imports do you need for the norm_num proof?

[Johan Commelin]

Aha: import Mathlib.Data.Nat.PrimeNormNum

[Johan Commelin]

import Mathlib.Data.Nat.PrimeNormNum

theorem challenge_aux (p a b : ℕ) (hp : p.Prime) (h0a : 0 < a) (ha: a < p) (h0b : 0 < b) (hb : b < p) :
    (a * b) / p * p ≠ a * b := by
  intro h
  have : p ∣ a * b := dvd_of_mul_left_eq _ h
  apply hp.not_dvd_mul _ _ this <;>
    apply Nat.not_dvd_of_pos_of_lt <;> assumption

theorem challenge (q a b : ℕ) (hq : q = 3329) (h0a : 0 < a) (ha: a < q) (h0b : 0 < b) (hb : b < q) :
    (a * b) / q * q ≠ a * b := by
  apply challenge_aux _ _ _ _ h0a ha h0b hb
  rw [hq]
  norm_num

[Eric Wieser]

Nice, not_dvd_of_pos_of_lt was the one I couldn't find

[Johan Commelin]

apply? found it for me

[Johan Commelin]

@Leonardo de Moura voila: 2 solutions :up:

[Riccardo Brasca]

(n / m) * m = n ↔ m ∣ n deserves to be in mathlib!

[Kevin Buzzard]

Three:

import Mathlib

example (A B Q : ℕ) (hQ : Q = 3329) (hA : 0 < A ∧ A < Q)
    (hB : 0 < B ∧ B < Q) :
    ((A * B) / Q) * Q ≠ (A * B) := by
  -- assume the contrary
  intro h
  -- replace Q by 3329
  subst hQ
  -- key fact: 3329 is prime
  have h1 : Nat.Prime 3329 := by norm_num
  -- use our hypotheses about `A * B`
  have h2 : 3329 ∣ A * B := by
    use A * B / 3329
    nth_rw 1 [← h]
    ring
  -- mathlib has the key fact that p ∣ AB => p ∣ A or p ∣ B
  rw [Nat.Prime.dvd_mul h1] at h2
  -- do the two cases
  rcases h2 with (h | h)
  · -- now easy to get a contradiction in both cases
    have := Nat.eq_zero_of_dvd_of_lt h hA.2
    linarith
  · have := Nat.eq_zero_of_dvd_of_lt h hB.2
    linarith

[Riccardo Brasca]

Riccardo Brasca said:

(n / m) * m = n ↔ m ∣ n deserves to be in mathlib!

Ah. it's already there.

import Mathlib

theorem challenge (q a b : ℕ) (hq : q = 3329) (h0a : 0 < a) (ha: a < q) (h0b : 0 < b) (hb : b < q) :
    (a * b) / q * q ≠ a * b := by
  intro h
  rw [← Nat.dvd_iff_div_mul_eq] at h
  replace hq : Nat.Prime q := by rw [hq]; norm_num
  exact hq.not_dvd_mul (Nat.not_dvd_of_pos_of_lt ‹_› ‹_›) (Nat.not_dvd_of_pos_of_lt ‹_› ‹_›) h

[Johan Commelin]

Minigolf:

import Mathlib.Data.Nat.PrimeNormNum

theorem challenge_aux (p a b : ℕ) (hp : p.Prime) (h0a : 0 < a) (ha: a < p) (h0b : 0 < b) (hb : b < p) :
    (a * b) / p * p ≠ a * b := by
  rw [Ne.def, ← Nat.dvd_iff_div_mul_eq]
  apply_rules [Nat.Prime.not_dvd_mul, Nat.not_dvd_of_pos_of_lt]

theorem challenge (q a b : ℕ) (hq : q = 3329) (h0a : 0 < a) (ha: a < q) (h0b : 0 < b) (hb : b < q) :
    (a * b) / q * q ≠ a * b := by
  apply challenge_aux _ _ _ _ h0a ha h0b hb
  rw [hq]; norm_num

[Roderick Chapman]

Thanks for the help everyone. For context, this proof allow me to shave 2 machine code instructions off the Montgomery-style reduction of (A * B) mod 3329 in the Kyber PQC algorithm.

[Roderick Chapman]

I like Kevin's version because it has comments that I can understand... :-)

[Patrick Massot]

We are sorry about the delay, everybody was busy watching Lean Together talks.

[Joachim Breitner]

(deleted)

[Miguel Marco]

Roderick Chapman said:

Thanks for the help everyone. For context, this proof allow me to shave 2 machine code instructions off the Montgomery-style reduction of (A * B) mod 3329 in the Kyber PQC algorithm.

Just out of curiosity: you need the formalized proof because you want to formally prove that your implementation is correct? Or just wanted to be totally sure of the fact before using it?

Also, 3329 looks like a strange prime to use in cryptography (too small to be a "big prime", too big to be a "small prime". Why that choice? Is there some delicate balance between the size of the set where you sample, the variance of the distribution and the number of samples or something like that?

[Roderick Chapman]

I can't comment on the choice of 3329 - this is "Module Lattice" math that I frankly do not understand. Google for "FIPS-203" for the details.

[Roderick Chapman]

As for the proof... I'm basically trying to compute (A * B) mod 3329, where both A and B lie in 0 .. 3328, but do it as fast as possible, and avoid using a "divide" instruction, which leak info via a timing side-channel. The standard way to compute
"mod" is to do
R = A mod 3329 = A - (A div 3329) * 3329
but you do the "div" using a multiply and shift sequence, using (2**37 / 3329) as the multiplier which is close enough to being an integer to get the right answer if A and B are both in 0 .. 3328.

Without the proof above I can prove that the answer I get lies in 0 .. 3329, so I have to do one additional constant-time reduction step:

R := Boolean'Pos (R /= 3329) * R;

On ARM64 with optimization enabled, that costs an extra 2 instructions.

With the proof above, I can prove that I get answer in 0 .. 3328, so that final reduction step is not required.

Does that make sense?

[Riccardo Brasca]

The choice of p = 3329 seems related to the fact that $X^d - 1$ splits completely over $\mathbb{F}_p$, where d is some power of 2 (indeed 3329 = 2^8 * 13 + 1), but I don't know.

[Miguel Marco]

So, (2**37/3329) is treated as a floating point number? or you mean the quotient of that division with remainder?

[Mauricio Collares]

Miguel Marco said:

So, (2**37/3329) is treated as a floating point number? or you mean the quotient of that division with remainder?

The / stands for truncating division, probably. Compilers often optimize division by a constant D by finding a "magic number" (that's the technical term) M and a shift S such that A*M>>S equals A/D for every (32-bit, say) integer, and this is an example of a magic number for dividing by 3329. You can read more about it in chapter 10 of Hacker's Delight.

[Miguel Marco]

I see. So in this particular case, just an exhaustive check argument in 3329 cases would be ok too?

[Miguel Marco]

BTW, is that actually faster than looking up in a precomputed table?

[Mauricio Collares]

A 3329^2 lookup table would probably not fit in cache or be evicted often

[Wrenna Robson]

Roderick Chapman said:

Thanks for the help everyone. For context, this proof allow me to shave 2 machine code instructions off the Montgomery-style reduction of (A * B) mod 3329 in the Kyber PQC algorithm.

Oh hey Rod. I thought this sounded oddly like your kind of thing.

[Alok Singh]

Wrenna Robson said:

Roderick Chapman said:

Thanks for the help everyone. For context, this proof allow me to shave 2 machine code instructions off the Montgomery-style reduction of (A * B) mod 3329 in the Kyber PQC algorithm.

Oh hey Rod. I thought this sounded oddly like your kind of thing.

smol world

[Wrenna Robson]

Well, I work in Rod's approximate field (he is big smart and every time I have the chance to talk to him it's awesome). We were on a panel together relatively recently!

[Roderick Chapman]

I'm pleased to say that my colleague John Harrison has also supplied a proof of that Lemma in HOL-Lite, so at least I now have a comforting feeling of redundancy... :-)

[Julian Berman]

Some additional higher level context from this morning: https://words.filippo.io/dispatches/mlkem768/

exhaustively test every input combination for base field arithmetic operations (addition, subtraction, and multiplication modulo 3329) against expected values computed trivially with variable-time operations;

[Roderick Chapman]

I'm pleased to say that my code that needed this lemma is now freely available. In particular that lemma drops into the proof of "*" (mod Q) here: https://github.com/awslabs/LibMLKEM/blob/c8a6f6ac0c421847c9c33d6c22c5a7b7dad6f35b/spark_ada/src/mlkem.adb#L169