Wanted features related to Why3-Coq
This is a follow up on frama-c/frama-c#956 and discussion we had with Jens on the ACSL by Example GitLab about Coq via Why3 in Frama-C.
At least two features could be added to make it easier to use (in particular for ACSL by Example):
- drivers that are only applied to Coq (or any prover), an that can be verified,
- user defined (restricted) context for the proof of lemmas in Coq.
Drivers
This shall be the job of the driver. We probably need to a way to refine the why3 context per prover. Then, it is easy to enrich the Task generated by ProverWhy3
, which is already « prepared » in a specific way for each prover.
Currently, the supported import directives for WP drivers are:
why3.file="mydir/foo.why"
why3.file="mydir/foo.why:Bar"
why3.file="mydir/foo.why:Bar:T"
why3.import="foo.Bar"
why3.import="foo.Bar:T"
@lcorrenson suggests to reformulate all of them into something fully understandable from why3 users:
[for "myProver",...] loadpath "path/to/dir";
[for "myProver",...] import foo.Bar [as T];
This is indeed more flexible than using our custom meta
directives.
Restricted context
If we have two files like:
lemma Foo: // ...
lemma To_Prove: // uses Foo
lemma Bar: // ...
lemma Foo: // ...
lemma To_Prove: // uses Foo
The two files generate different proof contexts for lemmas, because even if To_Prove
only needs Foo
, WP collects all lemmas that appear before To_Prove
. This is why I suggest to provide the user with a way to specify precisely the proof context so that it can remain the same from a file to another.
I think we could create an ACSL extension like:
/*@
lemma Foo: ...
lemma Bar: ...
lemma Proved_with_Coq: ...
lemma_dependencies Proved_with_Coq: Foo ;
*/
So that the user can restrict the proof context of the lemma can be as simple and predictable as possible. Note that we should check that it compatible with the RefUsage
analysis.