montgomery reduction proof -- would love some feedback!

Stream: mathlib4

[Jonathan Protzenko]

Hi all. Context: @Son Ho, @Aymeric Fromherz and I have been investigating Lean for proving facts about cryptographic algorithms (in the context of the Aeneas verification toolchain). Right now, we're looking at Kyber, a new post-quantum algorithm that uses a lot of linear algebra (this thesis has good background in §2.2 and §2.3: https://kannwischer.eu/thesis/phd-thesis-2023-01-03.pdf -- see also https://bwesterb.github.io/draft-schwabe-cfrg-kyber/draft-cfrg-schwabe-kyber.html). As a warm-up project, we've been proving algorithm 6 from the thesis above (page 42), namely a Montgomery reduction. (There's a lot more interesting stuff in Kyber, including NTT, and this has been going reasonably well so far, so I won't mention it here.)

The proof is 172 lines: https://gist.github.com/msprotz/54969de9c58106a22db3dcf50132d6ca (This should be an mwe! I can successfully copy/paste it into my editor, provided I have mathlib in scope.)

Our "ask": we would love to get a critique of the proof by some more experienced lean/mathlib users. Is there something that's abnormally tedious? Are we missing a library of lemmas somewhere? Is there some tactic that we could've used to make our lives easier? Is there a more common style of going about proof obligations? etc. etc. -- I've added some specific questions, but really, any thoughts by more experienced users would go a long way as we start fleshing out some proofs and evaluating Lean for reasoning about this flavor of algorithms. Thanks!

[Eric Wieser]

A quick remark: ZMod.inv q r should be (r : ZMod q)⁻¹ throughout. Perhaps we need a warning on the docstring of docs#ZMod.inv that it's an implementation detail

[Eric Wieser]

Your first sorry can be solved with by apply?, which finds Int.ediv_lt_of_lt_mul H H'

[Eric Wieser]

have := ZMod.inv_mul_of_unit (a : ZMod b) (ZMod.unitOfCoprime _ H_c).isUnit almost completely solves your first goal

[Jonathan Protzenko]

thanks, I'm getting unknown identifier 'apply?', do I need to import something?

[Jonathan Protzenko]

ah nevermind, just the editor that was slow to react

[Jonathan Protzenko]

ah excellent! this apply? thing is great

[Gabriel Ebner]

About div_lt_of_lt_mul. This is a victim of the still ongoing battle over the definition of integer division. Lean 4 started out with the rounding convention used in C, which is terrible for formalization. While mathlib wants (and redefines division to use!) another rounding convention (as in Python).

[Gabriel Ebner]

#eval (-1)/2 -- 0

[Gabriel Ebner]

import Mathlib
#eval (-1)/2 -- -1

[Gabriel Ebner]

Hopefully this will be resolved sometime in the future. Long story short, the theorem you're looking for is called ediv_lt_of_lt_mul for now.

[Gabriel Ebner]

My general impression is that people like Zmod more than ≡ [ZMOD] and that you'll find more lemmas there.

[Ruben Van de Velde]

Would that be ZMod?

[Michael Stoll]

ZMod n is a ring, which makes it easier to work in it, compared to congruences.

[Jonathan Protzenko]

We've found that the algorithm we were looking at was written with an "int" style in mind, rather than manipulating members of the zmod ring. I had an earlier version that tried to express everything within the group but since the algorithm juggles mod q and mod R, I didn't seem to go very far

[Jonathan Protzenko]

Maybe I started off in the wrong direction? but predicates like "this divides that mod something else" became hard to express, I thought, in the group setting

[Kevin Buzzard]

Can you give an explicit example of what you mean by "this divides that mod something else"? Right now I can't even typecheck that sentence.