SPARK: Discharge verification conditions (VC) with Coq?

General
1

Hi all,

I intend to teach students how to discharge SPARK VCs with Coq.

The motivation is that sometimes, you need interactive theorem proving to prove the properties you’d like to prove.

I started with this from the SPARK User’s Guide:
https://docs.adacore.com/spark2014-docs/html/ug/en/source/manual_proof.html#manual-proof-using-coq

I then tried discharging all VCs with Coq in the SPARK Lab of this course:
https://www.inf.ed.ac.uk/teaching/courses/fv/spark/spark-lab.html

This was reasonably easy for swap.adb and search_arr_zero.adb , but got real ugly real fast for the other ones. While I am not very experienced with Coq (I did Vol. 1-2 of Software Foundations, but that was a long time ago), it seems to me that proving VCs in Coq does not scale; they get really hard to discharge in Coq.

Notably, the VCs in Coq make no sense to me. I know they are something that SPARK needs to finish a proof (and therefore, the VC does not need to make sense, provided we trust SPARK). But still; if the VC made more sense, then it would be easier to come up with a proof idea, to then implement in Coq.

I then looked around the Internet to see if anyone actually has used Coq to discharge VCs, and I did not find anyone who has done so. Even the VerifyThis! SPARK solution does not do so (thus leaving the challenges that need interactive proofs, unsolved).

Finally, I needed to install an older version of Coq to do this exercise (since this feature only worked for that version of Coq). Setting that up was (very doable, albeit) a bit painful.

Is this something that people just don’t do? Do people use other features in SPARK (e.g. ghost code), or just turn to other tools, when automated theorem proving fails? Is this ability to discharge SPARK VCs with Coq more of a “proof of concept” / “fun demo” / “in case anyone needs it”?

If this feature is really meant for proving properties of software in industry, then I would very much value any comments, hints, pointers, or reading, on how to do this. For instance, are there certain Coq libraries / tactics that makes discharging the VCs in Coq easier? Is there some rule-of-thumb / paradigm I should follow to make whatever SPARK cannot discharge automatically as small and simple as possible?

Kind regards,
Willard

2

For proof to be tractable in Coq, I recommend keeping it for lemmas that precisely express the properties that cannot be proven otherwise, i.e. with ghost code. That’s what we do for some lemmas of the SPARK library. This ensures that the VCs remain simple enough that you can handle them in Coq.

But it’s also true that we try in general to do all proofs with ghost code, which has the nice benefit of better evolving with the code to prove. This is what we recommend to all our users, in industry or otherwise.

So yes, you could say that, today, proving SPARK VCs in Coq is more a proof of concept than a real feature. I know only one team (the people from secunet) who have made an industrial use of manual proof (with Isabelle) on SPARK VCs.

Out of curiosity, did you try proving your properties with ghost code?

3 Likes
3

Hi Yannick, thank you for taking the time to reply here,

I haven’t tried proving my properties with ghost code; I’ll try that, and see how it goes.

What I read from your response, is that:

*) In general, ghost code is the go-to feature of SPARK for providing additional (human) insight to the verifier. This is sufficient in all but the most obscure circumstances.

*) In those obscure circumstances, if you must resort to discharging a VC in Coq, then it’s best to refactor [the part of the proof obligation that SPARK cannot discharge automatically], into a lemma, and then proving that lemma in Coq (which, presumably, will then be more readable in Coq).

(If I am mistaken in the above, then by all means correct me)

In this case, it seems that my initial motivation is incorrect; when proving properties of SPARK programs, you virtually never need interactive theorem proving. (I’m guessing this is in part because all data types are bounded, so quantifiers do not become (very) problematic).

Do you happen to know of kinds of properties that are difficult to prove in SPARK even if you resort to ghost code, for which you have to resort to interactive theorem proving? (I’m aware of hyperproperties, but I consider those out of scope here, since all program verifiers struggle with those since they aren’t even specifiable in the property specification languages).

4

You got it correctly regarding SPARK, ghost code and manually proved lemmas.

The reasoning about interactive theorem proving is a bit reversed: we tend to limit ourselves when using SPARK to properties which can be mostly automatically proved (that is, we can get fully automatic proof with enough ghost code). That’s what I presented this week at HIS 2022: Pushing the Boundary of Mostly… | High Integrity Software 2022

It would be nice sometimes to easily point to the lemma which the prover should instantiate to finish a proof, in particular when the context gets large and the prover gets lost doing something else. We’ve got a preview of what it would look like in SPARK already, but it’s not really ready for industrial usage: 7.1. How to Run GNATprove — SPARK User's Guide 24.0w

Then, sometimes even nudging provers is not enough, that’s when we have no other choice than to go to something like Coq. We currently only do this for some arithmetic lemmas that we provide in the SPARK library which can’t be proved automatically: 5.11. SPARK Libraries — SPARK User's Guide 24.0w That’s because they use non-linear arithmetic, or floating-point arithmetic, or a mix of arithmetic.

You could go after hyperproperties by composing the program with itself at source code level, and then using SPARK on the composed program.