Algorithm correctness

Stream: Is there code for X?

[Bjørn Kjos-Hanssen]

Do you know any examples of formalized results on implementation of algorithms together with a proof of the algorithm's correctness in Lean or other proof assistants?
In other words,
def f_algorithm := ...
followed by
example : f 17 = 4 := by decide (which should run reasonably fast) and
theorem (x : Nat): f_algorithm x = well_known_function x
I can give an example if it helps.

[Adam Topaz]

I think some sorting algorithms are proven correct in Std4?

[Adam Topaz]

I’m sure there are other more interesting examples

[Adam Topaz]

This isn't quite what you have in mind, and it's not anywhere public (it was for a project for my class last term), but @Isaac Hernando used quadratic reciprocity to write an algorithm for computing Legendre symbols, and proved that it agrees with docs#legendreSym with a lemma tagged with csimp. I think that's really nice, and I wish we had more stuff like this in mathlib.

[Adam Topaz]

Looking around now I see that there is a norm_num extension for Legendre symbols. Does this actually use quadratic reciprocity in any way?

[Adam Topaz]

Oh, and now I also remember @Matthew Ballard doing something similar for the 2-adic valuation. Did that ever make it to mathlib?

[Adam Topaz]

Adam Topaz said:

Looking around now I see that there is a norm_num extension for Legendre symbols. Does this actually use quadratic reciprocity in any way?

Indeed it does :) https://github.com/leanprover-community/mathlib4/blob/b8ea7cb7072a51dd9c80dcc72153af0d07e7a64b/Mathlib/Tactic/NormNum/LegendreSymbol.lean#L252

[Kyle Miller]

norm_num extensions aren't themselves proved correct though -- all they do is create a proof that some function evaluates to something, and then that proof is checked.

[Adam Topaz]

I'm just glad that quadratic reciprocity is used in some algorithm in mathlib :)

[Bjørn Kjos-Hanssen]

How about the Euclidean algorithm (to take something with the word 'algorithm' in the name)?

[Kyle Miller]

That's docs#Nat.xgcd for the extended Euclidean algorithm with proofs of correctness like docs#Nat.gcd_eq_gcd_ab (Bézout's identity) connecting it to docs#Nat.gcd (which is defined using the Euclidean algorithm). Key results of correctness are docs#Nat.gcd_dvd and docs#Nat.dvd_gcd

[Heather Macbeth]

Are you aware of the Coq Software Foundations book? For example, here's the page doing implementation and correctness-proof of mergesort.
https://softwarefoundations.cis.upenn.edu/vfa-current/Merge.html

[Heather Macbeth]

A small example in Lean: @Matej Penciak came to speak to my undergraduate class and taught them about fast exponentiation (exponentiation by squaring). Here's his code giving the algorithm and proof of correctness:
https://github.com/mpenciak/FordhamSp2023/blob/main/Fordham/ProofDemos.lean

[Jason Rute]

Other theorem provers have been used a lot for such work. For example, I don't know how much is published but John Harrison verified Intel's floating point Pentium chip algorithms in HOL-Light. He even was able to reduce the number of instructions in one of those.

[Jason Rute]

There is an entire C compiler verified in Coq: https://compcert.org/

[Jason Rute]

However, I should clarify that both of those projects are verifying the correctness of code written in another language separate from the formal proof assistant.

[Bjørn Kjos-Hanssen]

Heather Macbeth said:

Are you aware of the Coq Software Foundations book? For example, here's the page doing implementation and correctness-proof of mergesort.
https://softwarefoundations.cis.upenn.edu/vfa-current/Merge.html

Nice, thanks. I was particularly looking for depth-first search but that seems to be missing.

[Jason Rute]

I think you are looking for more basic stuff, but here are some more examples of big projects done in Coq: https://coq.discourse.group/t/high-assurance-high-code-complexity-use-of-coq/209

[Bjørn Kjos-Hanssen]

Jason Rute said:

Other theorem provers have been used a lot for such work. For example, I don't know how much is published but John Harrison verified Intel's floating point Pentium chip algorithms in HOL-Light. He even was able to reduce the number of instructions in one of those.

Oh right, I recall he gave an invited talk at an ASL meeting in 2010 (although not about that work).

[Siddhartha Gadgil]

I have experimented with such things at different scales:

• My first Lean project SATurn is a DPLL SAT solver in Lean with proved algorithms.
• In a course I taught, I had a few small examples: solving a linear Diaphontine equation in two variables, finding the minimum in a List and then insertion sort as a homework.

[Eric Rodriguez]

Jason Rute said:

Other theorem provers have been used a lot for such work. For example, I don't know how much is published but John Harrison verified Intel's floating point Pentium chip algorithms in HOL-Light. He even was able to reduce the number of instructions in one of those.

There was recently someone in the Zulip who wanted a proof of a theorem in order to get rid of two instructions from his cryptography routine, iirc

[Matthew Ballard]

Adam Topaz said:

Oh, and now I also remember Matthew Ballard doing something similar for the 2-adic valuation. Did that ever make it to mathlib?

docs#Nat.maxPowDiv and docs#padicValNat.padicValNat_eq_maxPowDiv

[Matthew Ballard]

Grepping reveals three uses of csimp in mathlib-proper

[Andrew Carter]

I've implemented and proved equivalent Karatsuba on my warpath towards proving algorithmic complexities:
https://github.com/calcu16/lean_complexity/blob/main/Karatsuba.lean

search for

theorem Nat.karatsuba_eq_mul: karatsuba = Nat.mul :=

in general any funext proof would seem to be a proof of "algorithmic correctness" right?