why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2021-09-06T11:23:30Zhttps://gitlab.inria.fr/why3/why3/-/issues/505Interface for Module2021-09-06T11:23:30ZFrançois BobotInterface for ModuleLe but est d'avoir un moyen de cacher une implémentation derrière une interface plus simple et plus approprié pour la preuve.
En résumé:
1. Verification avec un clone
- Seulement pour les fonctions de même nom:
- On ajoute toutes les post-conditions de l'interface
- On prend les préconditions de l'interface, s'il n'y en a pas
2. Barrière d'abstraction
Plan d'action:
1. Pas d'interface multiple
Si nécessaire encoder à la main les interfaces multiples avec clone (dans le cas où il n'y a pas les même fonctions)
2. Utiliser un nom généré, l'utilisateur écrit
```
module I type t = a end
module J : I type t = b end
```
Le code suivant est généré.
```
module J'impl type t = b ; clone I with type t = t end
module J clone I end
```
3. Lors de l'extraction et interprétation, copie les modules et applique une substitution (`use J` -> `use J'impl`)
4. `clone J with ...` is only allowed to instantiate symbols that are refinable both in `I` and `J`. During extraction/execution this is replaced with `clone J'impl with ...`. We should make an effort to check that the instantiation is valid for the implementation at an early stage, so that we never fail during the extraction.Le but est d'avoir un moyen de cacher une implémentation derrière une interface plus simple et plus approprié pour la preuve.
En résumé:
1. Verification avec un clone
- Seulement pour les fonctions de même nom:
- On ajoute toutes les post-conditions de l'interface
- On prend les préconditions de l'interface, s'il n'y en a pas
2. Barrière d'abstraction
Plan d'action:
1. Pas d'interface multiple
Si nécessaire encoder à la main les interfaces multiples avec clone (dans le cas où il n'y a pas les même fonctions)
2. Utiliser un nom généré, l'utilisateur écrit
```
module I type t = a end
module J : I type t = b end
```
Le code suivant est généré.
```
module J'impl type t = b ; clone I with type t = t end
module J clone I end
```
3. Lors de l'extraction et interprétation, copie les modules et applique une substitution (`use J` -> `use J'impl`)
4. `clone J with ...` is only allowed to instantiate symbols that are refinable both in `I` and `J`. During extraction/execution this is replaced with `clone J'impl with ...`. We should make an effort to check that the instantiation is valid for the implementation at an early stage, so that we never fail during the extraction.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/547Syntactic sugar for lemma functions2021-04-09T06:27:17ZLoïc CorrensonSyntactic sugar for lemma functionsThe following syntactic sugar for automatically introduce proof-based lemma functions:
```
lemma a: forall xs. hs -> p [variant { v }] [do t done] [with …]
```
This automatically generates:
```
let [rec] lemma a'apply xs requires { hs } ensures { p } [variant {v}] = begin t end
[with …]
```The following syntactic sugar for automatically introduce proof-based lemma functions:
```
lemma a: forall xs. hs -> p [variant { v }] [do t done] [with …]
```
This automatically generates:
```
let [rec] lemma a'apply xs requires { hs } ensures { p } [variant {v}] = begin t end
[with …]
```https://gitlab.inria.fr/why3/why3/-/issues/552RFC: binders for tuple components in function prototype2021-02-11T09:43:19ZJean-Christophe FilliâtreRFC: binders for tuple components in function prototypeIt would be useful if we could name tuple components in function prototypes e.g.
```
val f (x: int, y: int) : (r: int)
requires { x < 0 && y > 0 }
ensures { r = x + y }
```
Currently, we have to bind the tuple and then decompose it in every clause of the contract:
```
val f (p: (int, int)) : (r: int)
requires { let x, y = p in x < 0 && y > 0 }
ensures { let x, y = p in r = x + y }
```It would be useful if we could name tuple components in function prototypes e.g.
```
val f (x: int, y: int) : (r: int)
requires { x < 0 && y > 0 }
ensures { r = x + y }
```
Currently, we have to bind the tuple and then decompose it in every clause of the contract:
```
val f (p: (int, int)) : (r: int)
requires { let x, y = p in x < 0 && y > 0 }
ensures { let x, y = p in r = x + y }
```https://gitlab.inria.fr/why3/why3/-/issues/389Add "final" specifier2021-02-11T09:39:53ZRaphaël Rieu-HelftAdd "final" specifierIt could be used for private types that we do not want to be refinable.It could be used for private types that we do not want to be refinable.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/493turn lemma into lemma function automatically2021-02-11T09:37:29ZJean-Christophe Filliâtreturn lemma into lemma function automaticallyI propose we turn any lemma automatically into a lemma function.
(This way, we can instantiate it manually anywhere.)
Of course, there may be several ways of doing it. If for instance the lemma is
```lemma L: forall x. P -> Q```
then it could be either
```let lemma L (x) requires P ensures Q```
or
```let lemma L(x) ensures P->Q```
I suggest we choose the former, heuristically. If ever users want the latter, they can always
introduce a dedicated lemma function.
Such a change should not impact existing proofs, as we are only introducing
additional ghost functions.
We could imagine having a label to tag lemma we do not want to translate into lemma functions (if ever).I propose we turn any lemma automatically into a lemma function.
(This way, we can instantiate it manually anywhere.)
Of course, there may be several ways of doing it. If for instance the lemma is
```lemma L: forall x. P -> Q```
then it could be either
```let lemma L (x) requires P ensures Q```
or
```let lemma L(x) ensures P->Q```
I suggest we choose the former, heuristically. If ever users want the latter, they can always
introduce a dedicated lemma function.
Such a change should not impact existing proofs, as we are only introducing
additional ghost functions.
We could imagine having a label to tag lemma we do not want to translate into lemma functions (if ever).Mário PereiraMário Pereirahttps://gitlab.inria.fr/why3/why3/-/issues/531Add a deriving framework for WhyML2021-02-11T09:36:18ZFrançois BobotAdd a deriving framework for WhyMLFollow #306 and Guillaume proposition:
> generate equality for enumeration type.
Should we go too `[@ deriving eq]` ?Follow #306 and Guillaume proposition:
> generate equality for enumeration type.
Should we go too `[@ deriving eq]` ?https://gitlab.inria.fr/why3/why3/-/issues/519When clauses2021-01-29T06:27:18ZXavier DenisWhen clausesI promised Jean-Christophe I'd write this long ago.. 🙈.
----
In functional languages it's a common feature to be able to perform matches on constants. Since why3 doesn't support constant patterns, it complicates translations from languages with support for this functionality.
The challenge with adding this functionality to why3 is that patterns are desugared quite late in the compilation pipeline. Since we would like to desugar a constant pattern into an equality test, this is problematic as we must correctly resolve `=` for the type of the matched constant.
An alternative approach which is also more general would be to introduce `when` clauses. In this approach, match arms could be annotated with any boolean valued function. This function would have access to any binders created by the match arm's patterns. As this function would get typechecked with the rest of the AST, by the time we get to case-desugaring we should have no difficulty transforming it into a boolean test.
---
During a GT a few weeks ago we discussed this and several challenges and alternative solutions were proposed, unfortunately I didn't take notes at time and I no longer recall them.I promised Jean-Christophe I'd write this long ago.. 🙈.
----
In functional languages it's a common feature to be able to perform matches on constants. Since why3 doesn't support constant patterns, it complicates translations from languages with support for this functionality.
The challenge with adding this functionality to why3 is that patterns are desugared quite late in the compilation pipeline. Since we would like to desugar a constant pattern into an equality test, this is problematic as we must correctly resolve `=` for the type of the matched constant.
An alternative approach which is also more general would be to introduce `when` clauses. In this approach, match arms could be annotated with any boolean valued function. This function would have access to any binders created by the match arm's patterns. As this function would get typechecked with the rest of the AST, by the time we get to case-desugaring we should have no difficulty transforming it into a boolean test.
---
During a GT a few weeks ago we discussed this and several challenges and alternative solutions were proposed, unfortunately I didn't take notes at time and I no longer recall them.https://gitlab.inria.fr/why3/why3/-/issues/27Sequence literals2020-12-17T09:27:16ZGuillaume MelquiondSequence literalsCurrently, the only non-singleton data structure for which literal constants can be provided is the `list` type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data structures. So it would be worth having an input syntax for expressing literals for such structures and propagating these constants as far as possible in the system. A few questions to answer:
1. What is the syntax? The OCaml syntax `[| ... ; ... |]` might be fine.
2. What is the type of such a literal? Should it have a fixed type (e.g. `seq 'a`)? Or should its type depend on the context so that one can use this syntax to input program arrays?
3. How should it be translated to provers that do not support such literals? Using `epsilon s. length s = ... /\ s[0] = ... /\ ...` might be both effective and cheap implementation-wise.Currently, the only non-singleton data structure for which literal constants can be provided is the `list` type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data structures. So it would be worth having an input syntax for expressing literals for such structures and propagating these constants as far as possible in the system. A few questions to answer:
1. What is the syntax? The OCaml syntax `[| ... ; ... |]` might be fine.
2. What is the type of such a literal? Should it have a fixed type (e.g. `seq 'a`)? Or should its type depend on the context so that one can use this syntax to input program arrays?
3. How should it be translated to provers that do not support such literals? Using `epsilon s. length s = ... /\ s[0] = ... /\ ...` might be both effective and cheap implementation-wise.https://gitlab.inria.fr/why3/why3/-/issues/393type invariant preservation question2019-11-27T12:19:54ZDAILLER Sylvaintype invariant preservation questionI have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant to be ensured in the proof for `f`. Is there a way to tell the tool "at this point of program type invariants should hold" ?
```
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end
```I have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant to be ensured in the proof for `f`. Is there a way to tell the tool "at this point of program type invariants should hold" ?
```
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end
```https://gitlab.inria.fr/why3/why3/-/issues/246Allow "use ghost Foo"2019-05-21T13:37:41ZGuillaume MelquiondAllow "use ghost Foo"It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted programs.
It would be good to have a way in the surface language to express and enforce that such a module is not meant to be actually used. Proposed syntax: `use ghost int.Int`. This would also make the extraction a lot less adhoc with respect to these modules.
A possible implementation would be to flag the corresponding scopes as being restricted. Any symbol accessed through such a scope would be forbidden to occur in non-ghost code. The change in `Why3extract.use_fold` would be trivial.
Open questions:
- what if the user do both `use` and `use ghost`?
- what if the user do `use ghost` on a module with toplevel side effects?It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted programs.
It would be good to have a way in the surface language to express and enforce that such a module is not meant to be actually used. Proposed syntax: `use ghost int.Int`. This would also make the extraction a lot less adhoc with respect to these modules.
A possible implementation would be to flag the corresponding scopes as being restricted. Any symbol accessed through such a scope would be forbidden to occur in non-ghost code. The change in `Why3extract.use_fold` would be trivial.
Open questions:
- what if the user do both `use` and `use ghost`?
- what if the user do `use ghost` on a module with toplevel side effects?https://gitlab.inria.fr/why3/why3/-/issues/278Parsing on attributes in programs2019-03-01T13:37:02ZDAILLER SylvainParsing on attributes in programsHello,
This issue is to keep track of discussions.
The question is the following. On why3 0.88, it was possible to add attributes to the program in order to retrieve them later in goals. This behaviour disappeared: it seems to be needed by SPARK for tracability of goals (goals A contains stuff that originate from this and that part of the code).
```
module Test
use int.Int
type d = {mutable contents: int; mutable useless: int}
let f c
ensures { c.contents = 1 }
= (*[@vc_sp]*)
c.contents <- 2;
[@This disappears] (c.contents <- 3);
c.contents <- 4
end
```
Copying potentially interested persons: @paskevyc @marche
PS: If you think people from SPARK should be involved, I can ask them to comment on this.Hello,
This issue is to keep track of discussions.
The question is the following. On why3 0.88, it was possible to add attributes to the program in order to retrieve them later in goals. This behaviour disappeared: it seems to be needed by SPARK for tracability of goals (goals A contains stuff that originate from this and that part of the code).
```
module Test
use int.Int
type d = {mutable contents: int; mutable useless: int}
let f c
ensures { c.contents = 1 }
= (*[@vc_sp]*)
c.contents <- 2;
[@This disappears] (c.contents <- 3);
c.contents <- 4
end
```
Copying potentially interested persons: @paskevyc @marche
PS: If you think people from SPARK should be involved, I can ask them to comment on this.