## 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.