Bas Spitters (Jul 12 2021 at 11:46): Bas Spitters (Jul 12 2021 at 11:46):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?
Matthieu Sozeau (Jul 12 2021 at 11:51):I don't think anything was done in this direction since Stéphane Lescuyer's PhD (https://dblp.org/pid/66/3754.html)
Matthieu Sozeau (Jul 12 2021 at 11:51):But I really wish someone would take this up :)
Yannick Zakowski (Jul 12 2021 at 11:53):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/
Matthieu Sozeau (Jul 12 2021 at 11:57):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 (Jul 12 2021 at 11:59):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.
Matthieu Sozeau (Jul 12 2021 at 12:03):I think the development was maintained for a little bit, but probably not past 8.5. Might not take too long to update though
Bas Spitters (Jul 12 2021 at 12:16):@Théo Zimmermann would alt-ergo be a project to be maintained by the community ?
Cody Roux (Jul 12 2021 at 12:54):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.
Théo Zimmermann (Jul 12 2021 at 13:09):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/
Bas Spitters (Jul 12 2021 at 13:15):@Théo Zimmermann but those are not the coq sources...
Théo Zimmermann (Jul 12 2021 at 13:19):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
Guillaume Melquiond (Jul 12 2021 at 13:20):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
Bas Spitters (Jul 12 2021 at 13:23):@Guillaume Melquiond Thanks! Is this up to date with master, and do you happen to know whether it extracts (to ocaml)?
Guillaume Melquiond (Jul 12 2021 at 13:24):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.
Bas Spitters (Jul 12 2021 at 13:29):Github has an 8.10 branch made by @Hugo Herbelin
Hugo Herbelin (Jul 12 2021 at 13:43):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.
Matthieu Sozeau (Jul 12 2021 at 13:49):I think completeness was not finished, and he also had proofs about backjumping and conflict-driven clause learning.
Matthieu Sozeau (Jul 12 2021 at 13:50):But the core proof was about the same DPLL strategy as alt-ergo, at the time, IIUC
Guillaume Melquiond (Jul 12 2021 at 13:53):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.)
Paolo Giarrusso (Jul 12 2021 at 14:15):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) Guillaume Melquiond (Jul 12 2021 at 14:19):Note that this is a SAT solver, not an SMT solver, so not quite not the same.
Alexander Gryzlov (Jul 12 2021 at 14:26):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.
Michael Soegtrop (Jul 13 2021 at 06:43):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?
Bas Spitters (Jul 13 2021 at 06:50):Both actually, because integration with ATP has been a theme in ITP for so long.
Michael Soegtrop (Jul 13 2021 at 09:47):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.
Chantal Keller (Jul 13 2021 at 11:56):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.
Bas Spitters (Jul 13 2021 at 12:14):Very nice @Chantal Keller ! Thanks for the nice paper!
Michael Soegtrop (Jul 13 2021 at 12:34):@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 ...
Bas Spitters (Jul 13 2021 at 14:13):@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
Chantal Keller (Jul 13 2021 at 16:34):@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!
Chantal Keller (Jul 13 2021 at 16:38):@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.
Bas Spitters (Jul 14 2021 at 06:31):@Chantal Keller Thanks. Makes sense. So, perhaps at some point in the future something like TIP will already be done with small transformations (?)
Michael Soegtrop (Jul 14 2021 at 07:27):@Chantal Keller : I will add it to Coq Platform and Coq CI and see what happens ...
Bas Spitters (Jul 17 2021 at 09:03):@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...
Bas Spitters (Aug 06 2021 at 08:36):@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?
Michael Soegtrop (Aug 06 2021 at 12:18):@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.
Bas Spitters (Aug 06 2021 at 12:38):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.
Michael Soegtrop (Aug 06 2021 at 13:02):So GRAT can produce a Coq proof or something which can be efficiently converted to a Coq proof?
Bas Spitters (Aug 06 2021 at 13:43):That's my (superficial) understanding.
Last updated: Jun 01 2023 at 13:01 UTC