Arithmetic solver

Stream: lean4

[Joe Hendrix]

Are there any efforts to build a proof producing solver in Lean for discharging goals involving arithmetic constraints?
I started to work on some buffer manipulation code as part of some work to formalize crypto routines in Lean. I find myself spending a fair bit of time writing arithmetic lemmas by hand, and it seems like I should start working on automation rather than keep pushing through those lemmas.

[Huỳnh Trần Khanh]

oh? I don't know cryptography :joy: but could you post some examples of arithmetic constraints? the word sounds vague to me as a non expert, and I doubt that there are many cryptographers here

[Huỳnh Trần Khanh]

do you mean something like "this addition won't overflow"? or could you be more specific

[Huỳnh Trần Khanh]

or do you mean something like... if you do this kind of pointer arithmetic then a buffer overflow won't happen?

[Mario Carneiro]

Have you tried tactic#linarith? Of course it is not in lean 4 yet, but anything in lean 3 is slated for porting in the near term

[Joe Hendrix]

@Mario Carneiro I have not, but that looks like exactly what I am looking for. I'd be happy to help with the porting.

[Huỳnh Trần Khanh]

a fair warning: in lean 3 I've learned to avoid the linarith tactic because it makes proofs unreasonably slow. I'm not sure if linarith could run faster in lean 4 or not

[Kevin Buzzard]

The thing about linarith is that it loves the jobs you hate. It makes working with Lean more like the way an undergraduate mathematician would work on paper -- "obviously a+b+c>0 because this follows from the assumptions which I'm carrying around in my head". So for mathematicians it's a really important and useful tactic.

[Joe Hendrix]

It's super useful for computer scientists and programmers too (for array bound checks if nothing else). I think it's essential that Lean 4 have a fast linear arithmetic tactic (which some heuristics for limited non-linear).

[Patrick Massot]

Joe Hendrix said:

Mario Carneiro I have not, but that looks like exactly what I am looking for. I'd be happy to help with the porting.

@Rob Lewis did you see that?

[Rob Lewis]

Huỳnh Trần Khanh said:

a fair warning: in lean 3 I've learned to avoid the linarith tactic because it makes proofs unreasonably slow. I'm not sure if linarith could run faster in lean 4 or not

Linarith isn't inherently slow. On average I wouldn't expect it to slow down your proofs more than simp, although of course they scale differently -- simp scales with the number of imports, linarith scales with the numbers of inequalities in your context and the number of variables in those inequalities. There's a linarith only variant that's faster.

[Rob Lewis]

That said, I think there's more promise for an efficient implementation of the simplex algorithm in Lean 4, which will scale better than the current Fourier-Motzkin implementation

[Huỳnh Trần Khanh]

sounds interesting... but i have a counterexample! https://gist.github.com/huynhtrankhanh/18611b9372d420f1cbbac54f52a4ba77 linarith is extremely slow in this proof :joy:

[Huỳnh Trần Khanh]

so well, there is an escape hatch at the top of the file

[Huỳnh Trần Khanh]

(the :+1: is to acknowledge that i've read your message, not to say that i agree with you lol)

[Rob Lewis]

That's a monster proof that's slow, period. There are 40 linarith calls in it, many with fairly big contexts. It shouldn't be at all surprising that replacing them with sorry speeds up the proof.

[Rob Lewis]

In addition, a lot of them involve natural number inequalities that get lifted (again and again and again) to int. Half of linarith's execution time is spent in zify preprocessing.

[Mario Carneiro]

Yeah, linarith isn't what is pathological about that proof. Lemmas are your friends

[Joe Hendrix]

I expect the use case I have will just involve really small arithmetic problems. So far, I'm just addressing it by building up a collection of lemmas and doing the proofs manually.

I think that approach may run into problems once I start specifying the actual crypto algorithms though.