At some point people worked on a verified SMT solver in Coq.
http://alt-ergo.lri.fr/
I'm trying to find the current status, but cannot find much in the last decade. Am I overlooking something?
I don't think anything was done in this direction since Stéphane Lescuyer's PhD (https://dblp.org/pid/66/3754.html)
But I really wish someone would take this up :)
It's not a verified solver, but Chantal Keller et al. have works on certified verifiers for SMT certificates that are of this decade: https://smtcoq.github.io/
With all the work that has been done on verifying imperative programs with expressive separation logics, I suppose it's no longer out of reach to verify all the crazy optimizations done in today's solvers.
Yes, smtcoq is nice too, but not up to date with the main branch IIRC.
I'm wondering about ocaml extraction of alt-ergo, and whether perhaps our rust extraction would work better.
I think the development was maintained for a little bit, but probably not past 8.5. Might not take too long to update though
@Théo Zimmermann would alt-ergo be a project to be maintained by the community ?
Matthieu Sozeau said:
With all the work that has been done on verifying imperative programs with expressive separation logics, I suppose it's no longer out of reach to verify all the crazy optimizations done in today's solvers.
Bas Spitters said:
Théo Zimmermann would alt-ergo be a project to be maintained by the community ?
AFAICT alt-ergo is maintained: https://alt-ergo.ocamlpro.com/ / https://github.com/OCamlPro/alt-ergo/
@Théo Zimmermann but those are not the coq sources...
Are the Coq sources available anywhere and under an open source license? If yes, then it would be in scope of coq-community to maintain them. However, they should probably need a new / modified name to distinguish them from the currently maintained alt-ergo project. And of course, this would be possible only if we find a volunteer, but you can begin by proposing the idea at https://github.com/coq-community/manifesto/issues/new/choose
There have never been any attempt to verify Alt-Ergo in Coq. What was verified by Stéphane Lescuyer was a minimal SMT solver with a toy theory for arithmetic and no support for quantifiers: https://github.com/coq-contribs/ergo
@Guillaume Melquiond Thanks! Is this up to date with master, and do you happen to know whether it extracts (to ocaml)?
The plugin is certainly not up-to-date to master, as it was never updated since 8.5. As for the Coq code, I don't think it was ever meant to be extracted. I don't quite remember.
Github has an 8.10 branch made by @Hugo Herbelin
Bas Spitters said:
Github has an 8.10 branch made by Hugo Herbelin
According to the log, the port to Coq 8.10 is incomplete (it was not so easy due to Coq changes in the treatment in the global proof state). Per se, it would not be so much work, so it depends on the demand.
I don't think there was extraction of code indeed (it is said to be a tactic). My memory is also that the certification proof was not complete. Stéphane had to stop without having completed it. But to know more, the best would be to ask him.
I think completeness was not finished, and he also had proofs about backjumping and conflict-driven clause learning.
But the core proof was about the same DPLL strategy as alt-ergo, at the time, IIUC
More precisely, it is a proof of CC(X), while Alt-Ergo used CC(X1,...,Xn). So, it goes a long way in guaranteeing that the algorithm of Alt-Ergo was sound, but not quite to the end. (And nowadays, Alt-Ergo uses AC(X1,...,Xn), so no longer the same algorithm.)
Not in Coq but https://twitter.com/MathiasFleury12/status/1413177141152337920 seems relevant
My verified SAT solver IsaSAT won the EDA challenge! #SAT2021 https://www.eda-ai.org/results/jfkainfiewr123890ansdifjiwu.php https://twitter.com/MathiasFleury12/status/1413177141152337920/photo/1
- Mathias Fleury (@MathiasFleury12)Note that this is a SAT solver, not an SMT solver, so not quite not the same.
Paolo Giarrusso said:
Not in Coq but https://twitter.com/MathiasFleury12/status/1413177141152337920 seems relevant
I think this is the same one that @Cody Roux has linked to.
Bas Spitters said:
Yes, smtcoq is nice too, but not up to date with the main branch IIRC.
Is that so? It does have an 8.13 branch and I guess 8.14 will be not that far away then.
Are you interested in verified SMT solvers or in verified a posteriori checks of SMT generated proofs or both?
Both actually, because integration with ATP has been a theme in ITP for so long.
Indeed. So can you please elaborate a bit on what issue you have with SMTCoq? I don't follow the argument that it is not maintained and actually was looking into including it in Coq Platform 2021.08.
@Chantal Keller : maybe you can comment.
Hi
I confirm that SMTCoq works for the last versions of Coq, even if not for trunk yet. For proof automation, I recommend the new tactic snipe
under active development https://github.com/smtcoq/sniper , available for Coq 8.11 to 8.13.
Very nice @Chantal Keller ! Thanks for the nice paper!
@Chantal Keller : I wonder what the outlook is for Coq 8.14 (which will be released soon) and generally what your opinion on the inclusion of SMTCoq into Coq Platform is. IMHO it definitely would make sense but Coq Platform has rather strict rules on maintenance (time from a Coq release to a working release of SMTCoq <= 2 months unless there have been very substantial changes to Coq). I don't know if this is long term doable for SMTCoq - I am not sure how much it depends on internals of Coq which change. I also plan to have an extended Coq Platform where the rules are more relaxed (say 6 months). Would you see SMTCoq more in the core Coq Platform or in the extension? Maybe we should discuss this in a SMTCoq centric forum ...
@Chantal Keller TIP is a format/tool collection that makes some similar transformations from a higher level language to SMTlib. Have you looked at it? Is it relevant?
https://tip-org.github.io/format.html
@Michael Soegtrop I'd like SMTCoq to be in the Coq community and CI in the short to mid term, then I think I can fulfill your requirements. Thanks for proposing!
@Bas Spitters I know this work. We are using very small transformations rather than a single pass, as explained in the paper. We also try to be directed by "common" Coq goals.
@Chantal Keller Thanks. Makes sense. So, perhaps at some point in the future something like TIP will already be done with small transformations (?)
@Chantal Keller : I will add it to Coq Platform and Coq CI and see what happens ...
@Chantal Keller I'm sure you're aware of the work, but I just stumbled upon some new work on reconstruction using veriT in isabelle.
https://link.springer.com/chapter/10.1007/978-3-030-79876-5_26
SMTCoq currently supports veriT ’s version 1 of the proof output which has different rules, does not support detailed skolemization rules, and is implemented in the 2016 version of veriT, which has worse performance...
@Michael Soegtrop @Chantal Keller There is also
https://github.com/fmlab-iis/coq-qfbv
https://link.springer.com/content/pdf/10.1007/978-3-030-81688-9_7.pdf
I'm not sure about the details of how it relates to smtcoq, but one could also consider addition to the platform. Perhaps, some kind of code sharing is possible?
@Bas Spitters thanks, interesting! I just wonder why it is Coq 8.11 when the paper is from 2021 and how GRAT work with Coq - it seems to be an Isabelle development.
Not sure about 8.11, I guess one should ask the authors. About GRAT, I think it includes a standalone tool as part of the development.
So GRAT can produce a Coq proof or something which can be efficiently converted to a Coq proof?
That's my (superficial) understanding.
Last updated: Nov 29 2023 at 19:01 UTC