why3 issues
https://gitlab.inria.fr/why3/why3/-/issues
2019-03-01T13:37:02Z
https://gitlab.inria.fr/why3/why3/-/issues/278
Parsing on attributes in programs
2019-03-01T13:37:02Z
DAILLER Sylvain
Parsing on attributes in programs
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.
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.
https://gitlab.inria.fr/why3/why3/-/issues/246
Allow "use ghost Foo"
2019-05-21T13:37:41Z
Guillaume Melquiond
Allow "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/393
type invariant preservation question
2019-11-27T12:19:54Z
DAILLER Sylvain
type invariant preservation question
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
```
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/27
Sequence literals
2020-12-17T09:27:16Z
Guillaume Melquiond
Sequence literals
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.
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/519
When clauses
2021-01-29T06:27:18Z
Xavier Denis
When clauses
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.
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/531
Add a deriving framework for WhyML
2021-02-11T09:36:18Z
FranÃ§ois Bobot
Add a deriving framework for WhyML
Follow #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/493
turn lemma into lemma function automatically
2021-02-11T09:37:29Z
Jean-Christophe FilliÃ¢tre
turn lemma into lemma function automatically
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).
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 Pereira
MÃ¡rio Pereira
https://gitlab.inria.fr/why3/why3/-/issues/389
Add "final" specifier
2021-02-11T09:39:53Z
RaphaÃ«l Rieu-Helft
Add "final" specifier
It 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 Paskevich
Andrei Paskevich
https://gitlab.inria.fr/why3/why3/-/issues/552
RFC: binders for tuple components in function prototype
2021-02-11T09:43:19Z
Jean-Christophe FilliÃ¢tre
RFC: binders for tuple components in function prototype
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 }
```
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/547
Syntactic sugar for lemma functions
2021-04-09T06:27:17Z
LoÃ¯c Correnson
Syntactic sugar for lemma functions
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 â€¦]
```
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/505
Interface for Module
2021-09-06T11:23:30Z
FranÃ§ois Bobot
Interface for Module
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.
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 Bobot
FranÃ§ois Bobot