frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2020-10-02T11:00:15Zhttps://git.frama-c.com/pub/frama-c/-/issues/30Wanted features related to Why3-Coq2020-10-02T11:00:15ZAllan BlanchardWanted features related to Why3-CoqThis 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):
1. drivers that are only applied to Coq (or any prover), an that can be verified,
2. 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:
```c
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
```c
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:
```c
/*@
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.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):
1. drivers that are only applied to Coq (or any prover), an that can be verified,
2. 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:
```c
lemma Foo: // ...
lemma To_Prove: // uses Foo
```
```c
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:
```c
/*@
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.Allan BlanchardAllan Blanchard