Adopt dolmen10

[rod-chapman]

PR to adopt dolmen v0.10

In particular, this adds option --ext=bvconv that will allow the LibMLKEM benchmarks to be adopted.

[hansjoergschurr]

Thanks for the pull request!
The last few years we retired the submission repository after the submission process, and created a new repository for the upcoming year. I would used this as an opportunity to update Dolmen and to fix other problems with the CI tooling.

However, I would not adapt --ext=bvconv in the CI script, since this extension is not yet part of the SMT-LIB standard.
This also mean we can't yet include the benchmarks in the main release either. I contacted the SMT-LIB standard maintainers to see whats the current plan around this extension, and to discuss options for presenting such benchmarks.

[rod-chapman]

OK... let's upgrade the infrastructure to have dolmen0.10 using this PR, then we can return to getting bvconv put into the SMT-LIB standard.

[rod-chapman]

Does anyone know when we might see an update of the SMT-LIB standard to include the bv2nat stuff?
(Version 2.7 perhaps?)

With my "customer/user" hat on, the bv2nat stuff is as "standard" as anything else, since:

1. It is generated by widely-used VC generators, particularly the Why3 toolset.
2. It is accepted and processed by all provers that I care about and use (e.g. Z3, CVC4 and CVC5)
3. I use it and rely on it to verify real industrial programs every day.

Sounds to me like the standard needs to catch up with industrial practice.

[rod-chapman]

Does anyone know when we might see an update of the SMT-LIB standard to include the bv2nat stuff?
(Version 2.7 perhaps?)

With my "customer/user" hat on, the bv2nat stuff is as "standard" as anything else, since:

1. It is generated by widely-used VC generators, particularly the Why3 toolset.
2. It is accepted and processed by all provers that I care about and use (e.g. Z3, CVC4 and CVC5)
3. I use it and rely on it to verify real industrial programs every day.

Sounds to me like the standard needs to catch up with industrial practice.

[hansjoergschurr]

I think a good place to bring this up is the SMT-LIB Google Group. The group is also read by the people who maintain the standard itself (Clark, Pascal, and Cesare).

[barrettcw]

No need to bring this up in the SMT-LIB group. This is on my radar and on my to do list. Let me see if I can prioritize it for 2.7.

…

-Clark

On Thu, Jun 20, 2024 at 7:11 AM Hans-Jörg ***@***.***> wrote: I think a good place to bring this up is the SMT-LIB Google Group <https://groups.google.com/g/smt-lib>. The group is also read by the people who maintain the standard itself (Clark <https://theory.stanford.edu/~barrett/>, Pascal <https://people.montefiore.uliege.be/pfontain/>, and Cesare <https://homepage.cs.uiowa.edu/~tinelli/>). — Reply to this email directly, view it on GitHub <#20 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAWV5I3KON66OMFSBJV5FWTZILIIPAVCNFSM6AAAAABJOIKEQKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCOBQGY2DQOBYGE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[rod-chapman]

Thanks.