Stream: Miscellaneous

Topic: alt-ergo


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Matthieu Sozeau (Jul 12 2021 at 11:51):

But I really wish someone would take this up :)

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bas Spitters (Jul 12 2021 at 12:16):

@Théo Zimmermann would alt-ergo be a project to be maintained by the community ?

view this post on Zulip 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.

It sure isn't!

view this post on Zulip 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/

view this post on Zulip Bas Spitters (Jul 12 2021 at 13:15):

@Théo Zimmermann but those are not the coq sources...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Jul 12 2021 at 13:29):

Github has an 8.10 branch made by @Hugo Herbelin

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Bas Spitters (Jul 13 2021 at 06:50):

Both actually, because integration with ATP has been a theme in ITP for so long.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Jul 13 2021 at 12:14):

Very nice @Chantal Keller ! Thanks for the nice paper!

view this post on Zulip 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 ...

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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 (?)

view this post on Zulip Michael Soegtrop (Jul 14 2021 at 07:27):

@Chantal Keller : I will add it to Coq Platform and Coq CI and see what happens ...

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Bas Spitters (Aug 06 2021 at 13:43):

That's my (superficial) understanding.


Last updated: Aug 19 2022 at 21:02 UTC