I would like to share with you an experiment. Now that I am using AI for quite a few things I do not have time to do by hand, I got the idea to revisit the possibility of enabling the Colibri family of SMT solvers within SPARK/GNATprove.
For those of you who are a bit out of the loop, colibri used to be shipped with the GNAT made available by AdaCore. However, since it got discontinued, it no longer has been available in gnatprove.
Today I checked and there are fairly new releases of colibri v1 and colibri v2 (in beta/alpha). The changelog mentioned improvements to Why3 integration (the underlying system of gnatprove) so I decided to download them and see if they could work with the newer GNAT v16.
I gave all the information to the AI , I guided it with some issues and inputs and I told it to create a benchmark to see how of the commonly available SMT solvers used in GNATprove compared. The benchmark was focused on floating point arithmetic as that is where the Colibri family is supposed to excel.
I would personally be interested in @mgrojo and @streaksu’s opinions as I believe both of you still rely on Colibri for your projects and have reported substantial improvements with its use. I can also confirm that enabling Colibri v1 in GNATprove is very easy, it jus needs a shared library that may not be available in modern systems, but it can be faked easily with the new versions of the library. It is all explained in the README. Also, a word of caution, Colibri v1 marked a piece of code as OK (SATISFIED) but the other SMTs flagged it as incorrect and gave a counterexample. That is a major issue…
Well, that is all for today folks! Best regards,
Fer
Interesting.
I wonder though, how difficult would it be to make a [SPARK-proved] “unification engine” for using both SPARK and a DB? (SMT and DB-queries both operate off unification.) — Such a module would be very nice for having a unified, trusted way to interface either SMT or DB-queries. — Plus, if you export out [IIRC] SMT-LIB, you could have a SPARK-in-SPARK solver to use.
GNATprove uses Why3 as the underlying proving engine. GNATprove takes the Ada/SPARK code and feeds it to Why3 in a format it understand (very LISPy). Which it then generates the SMT code and passes it to the solvers. The generated proofs (VCs, aka, verification conditions) are… “named” in a way that they are traceable back to the code and between provers. Additionally, all provers use SMT-LIB as their underlying knowledge engine. GNATprove and Why3 basically unite all of this into a single, easy to use interface.
For example, if one prover fails to complete one VC, the same VC is fed to another prover. Why3 and GNATprove keep track of all of this and are able to report it back and make things traceable.
I hope this answers your question.
Regarding the DB aspect, afaik, it is all done via text, so no actual DB. However, I believe AdaCore or some of its partners do have some DBs with all the proofs, configurations, etc; and they are integrated into CI/CD pipelines.
Forcing text is a terrible idea: as you lose your [sub-]type information.
I was more thinking that the core of the proving engine could be “factored out”, and then (a) used in both SMT provers and DB-engines [both use unification], while (b) being itself SPARK-proved — you’ve then bootstraped a known-good component you can use in both SMT & DB, you then provide the interface with the other provers.
But yes, having the proofs in a DB w/ configs and all would be nice too. (And, if using the ‘factored out’ engine, you already have a known-good large piece of the DB’s query-engine. [There’s a couple other pieces you’d want to implement as quality-of-life improvements, obviously.])