why3 issueshttps://gitlab.inria.fr/why3/why3/issues2019-05-13T16:07:22Zhttps://gitlab.inria.fr/why3/why3/issues/55additional manually-written configuration files2019-05-13T16:07:22ZCLOCHARD Martinadditional manually-written configuration filesIt would be nice to have some additional configuration files on top of why3.conf, so that configuration is not entirely re-written by Why3 at each run. This would avoid the insertion of the "\n" in the user strategies, and prevent user data loss for unknown causes (this happened for some user strategies).It would be nice to have some additional configuration files on top of why3.conf, so that configuration is not entirely re-written by Why3 at each run. This would avoid the insertion of the "\n" in the user strategies, and prevent user data loss for unknown causes (this happened for some user strategies).François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/issues/298Migrate to Zarith2019-05-10T14:04:06ZFrançois BobotMigrate to ZarithPreviously we had to keep the num library for the why3 library because we compiled the coq-plugin. Could we now migrate to zarith?
From the [num](https://github.com/ocaml/num) website:
>This is a legacy library. It used to be part of the core OCaml distribution (in otherlibs/num) but is now distributed separately. New applications that need arbitrary-precision arithmetic should use the Zarith library (https://github.com/ocaml/Zarith) instead of the Num library, and older applications that already use Num are encouraged to switch to Zarith. Zarith delivers much better performance than Num and has a nicer API.Previously we had to keep the num library for the why3 library because we compiled the coq-plugin. Could we now migrate to zarith?
From the [num](https://github.com/ocaml/num) website:
>This is a legacy library. It used to be part of the core OCaml distribution (in otherlibs/num) but is now distributed separately. New applications that need arbitrary-precision arithmetic should use the Zarith library (https://github.com/ocaml/Zarith) instead of the Num library, and older applications that already use Num are encouraged to switch to Zarith. Zarith delivers much better performance than Num and has a nicer API.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/issues/313Why3 API backward compatibility2019-05-10T14:00:48ZFrançois BobotWhy3 API backward compatibilityWhich backward compatibility should provide the Why3 API?
Backward compatibility could mean two things:
- User of an old version of the API could use the new
- New user of the API can write code that works with the old and new API
The first one implies the second one, but the first one can be defeated just by adding an optional argument.
Recently two little modifications broke the backward compatibility of Why3. The API of Why3 is quite big now, so I think it is hard to not get such cases. What can we try to do to avoid that?
- Do we give no backward compatibility insurance
- Do we add a smaller API which would be backward compatible
- Do we try to check in some ways that all the API is backward compatible with the last why3 version?Which backward compatibility should provide the Why3 API?
Backward compatibility could mean two things:
- User of an old version of the API could use the new
- New user of the API can write code that works with the old and new API
The first one implies the second one, but the first one can be defeated just by adding an optional argument.
Recently two little modifications broke the backward compatibility of Why3. The API of Why3 is quite big now, so I think it is hard to not get such cases. What can we try to do to avoid that?
- Do we give no backward compatibility insurance
- Do we add a smaller API which would be backward compatible
- Do we try to check in some ways that all the API is backward compatible with the last why3 version?https://gitlab.inria.fr/why3/why3/issues/308Forall construction in code for ghost binding2019-05-10T14:00:38ZFrançois BobotForall construction in code for ghost bindingSometimes when we want to prove such functions:
```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
```
We need to prove with a ghost variable, for easing the proof
```
let f' x (ghost y) : result
requires { P(x,y) }
ensures { Q(x,y) }
```
However it is not possible to prove the first function using the second.
We propose to add a new construction which allows it.
```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
=
forall y requires { P(x,y) } in
f' x y
```
The semantic of this function is not completely clear:
* should a VC be generated to check that it exists such `y`
* what if the result contains a ghost
* what if there are ghost effectSometimes when we want to prove such functions:
```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
```
We need to prove with a ghost variable, for easing the proof
```
let f' x (ghost y) : result
requires { P(x,y) }
ensures { Q(x,y) }
```
However it is not possible to prove the first function using the second.
We propose to add a new construction which allows it.
```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
=
forall y requires { P(x,y) } in
f' x y
```
The semantic of this function is not completely clear:
* should a VC be generated to check that it exists such `y`
* what if the result contains a ghost
* what if there are ghost effecthttps://gitlab.inria.fr/why3/why3/issues/27Sequence literals2019-05-10T13:58:02ZGuillaume 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/312Missing hypothesis when splitting a formula with if-then-else and by2019-04-26T07:58:03ZGARCHERY QuentinMissing hypothesis when splitting a formula with if-then-else and byConsider the following code :
```
use int.Int
use seq.Seq
let function dirac (a b : int) =
if b = a then 1 else 0
let rec function count (x : int) (seq : seq int)
variant { Seq.length seq }
=
if Seq.length seq = 0
then 0
else dirac x seq[0] + count x seq[1..]
lemma count_case :
forall x h, t : seq int.
(if x = h
then (count x (cons h t) = count x t + 1
by dirac x h = 1)
else (count x (cons h t) = count x t
by dirac x h = 0))
by (cons h t)[1..] == t
```
When trying to prove the generated VCs (after split_vc) corresponding to the if-branches in the lemma,
the hypothesis `(cons h t)[1..] == t` is missing from the context. This makes the solvers fail to prove
the VCs directly (at least on my machine, giving them a reasonable delay).Consider the following code :
```
use int.Int
use seq.Seq
let function dirac (a b : int) =
if b = a then 1 else 0
let rec function count (x : int) (seq : seq int)
variant { Seq.length seq }
=
if Seq.length seq = 0
then 0
else dirac x seq[0] + count x seq[1..]
lemma count_case :
forall x h, t : seq int.
(if x = h
then (count x (cons h t) = count x t + 1
by dirac x h = 1)
else (count x (cons h t) = count x t
by dirac x h = 0))
by (cons h t)[1..] == t
```
When trying to prove the generated VCs (after split_vc) corresponding to the if-branches in the lemma,
the hypothesis `(cons h t)[1..] == t` is missing from the context. This makes the solvers fail to prove
the VCs directly (at least on my machine, giving them a reasonable delay).https://gitlab.inria.fr/why3/why3/issues/306Add program equality on Boolean type2019-04-20T06:55:02ZMARCHE ClaudeAdd program equality on Boolean typeTheory bool.Bool should provide (=) on Boolean type in programsTheory bool.Bool should provide (=) on Boolean type in programshttps://gitlab.inria.fr/why3/why3/issues/30Refresh does not reload source view, causing loss of work2019-04-15T12:08:50ZRaphaël Rieu-HelftRefresh does not reload source view, causing loss of workRefreshing the session with Ctrl-R does not reload the source view. I lost work from this with the following steps:
1) Open Why3 ide
2) Edit the source file in your favorite editor
3) Reload (source view does not change)
4) Edit the file from Why3 ide (in my case, inadvertently by pressing tab a few times in the ide), save file
5) You lose the work from 2)Refreshing the session with Ctrl-R does not reload the source view. I lost work from this with the following steps:
1) Open Why3 ide
2) Edit the source file in your favorite editor
3) Reload (source view does not change)
4) Edit the file from Why3 ide (in my case, inadvertently by pressing tab a few times in the ide), save file
5) You lose the work from 2)MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/issues/304improve ide window resizing2019-04-11T19:47:54ZLAWALL Juliaimprove ide window resizingWhen one resizes the IDE, the pane with the code in the upper right stays the same size, while the panes on the left and at the bottom get bigger. It is the code that one typically wants to see more of, so some effort is repetitively wasted to adjust the size of its pane. It would be fine if all the panes increased in size at the same rate, or if only the pane with the code got larger.When one resizes the IDE, the pane with the code in the upper right stays the same size, while the panes on the left and at the bottom get bigger. It is the code that one typically wants to see more of, so some effort is repetitively wasted to adjust the size of its pane. It would be fine if all the panes increased in size at the same rate, or if only the pane with the code got larger.https://gitlab.inria.fr/why3/why3/issues/294Why3 IDE - close a file/tab from the IDE directly2019-04-10T12:51:11ZDEMANGE DelphineWhy3 IDE - close a file/tab from the IDE directlySuppose I start a fresh why3 module in file1.mlw.
Then, suppose I want to either read, or reuse some definitions in another previous file, file2.mlw.
So I add file2.mlw to the current session to be able to read it in the IDE.
Now, suppose I'm done consulting file2.mlw, and that I don't want to see it appear in the source tabs,
or that I don't want to bother with the VCs in that file.
Currently, it doesn't seem to be possible to close the tab for file2.mlw from the IDE.
When I try to remove the "module proof node", the IDE tells me :
"Cannot remove attached proof nodes or theories, and proof_attempt that did not yet return"
So, I have to close the IDE, remove the directory corresponding to the session, and relaunch the IDE, and re-start all proofs related to file1.mlw.
Being able to remove a file (file2.mlw) from a session would be more convenient.Suppose I start a fresh why3 module in file1.mlw.
Then, suppose I want to either read, or reuse some definitions in another previous file, file2.mlw.
So I add file2.mlw to the current session to be able to read it in the IDE.
Now, suppose I'm done consulting file2.mlw, and that I don't want to see it appear in the source tabs,
or that I don't want to bother with the VCs in that file.
Currently, it doesn't seem to be possible to close the tab for file2.mlw from the IDE.
When I try to remove the "module proof node", the IDE tells me :
"Cannot remove attached proof nodes or theories, and proof_attempt that did not yet return"
So, I have to close the IDE, remove the directory corresponding to the session, and relaunch the IDE, and re-start all proofs related to file1.mlw.
Being able to remove a file (file2.mlw) from a session would be more convenient.https://gitlab.inria.fr/why3/why3/issues/300Add file from IDE is broken2019-04-08T08:19:20ZDAILLER SylvainAdd file from IDE is brokenHello,
When I have two files a.mlw and b.mlw in the same directory in the filesystem and the session for a.mlw in a/why3session.xml as usual. If I try to open why3ide on a.mlw and then add file b.mlw, I get an error in the "Messages" stating (cannot open a/../home/dailler/b.mlw). I think this is a problem with Sysutil.relativize_filename.Hello,
When I have two files a.mlw and b.mlw in the same directory in the filesystem and the session for a.mlw in a/why3session.xml as usual. If I try to open why3ide on a.mlw and then add file b.mlw, I get an error in the "Messages" stating (cannot open a/../home/dailler/b.mlw). I think this is a problem with Sysutil.relativize_filename.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/297smoke detection in ide2019-04-04T13:45:59ZDAILLER Sylvainsmoke detection in ideHello,
This issue is to record discussion about smoke detector on why3-club. smoke detector is a transformation that can be launched on any goal: using it may lead to an inconsistent state.
People want to keep usability of this transformation in the IDE. Several solutions exist to prevent errors:
- do nothing: the transformation is already described in the IDE
- allow using it only on proof nodes
- raise a warning when this transformation is called
- treat the smoke detector transformation in a specific way in the IDE/session so that smoke detected transformation do not make their parent goal appear proved. Adding an "inconsistent if reachable" value ?
[EDIT: Also make sure that the exact same smoke from why3replay can be used in IDE (or intentionally forbid it)? Hello,
This issue is to record discussion about smoke detector on why3-club. smoke detector is a transformation that can be launched on any goal: using it may lead to an inconsistent state.
People want to keep usability of this transformation in the IDE. Several solutions exist to prevent errors:
- do nothing: the transformation is already described in the IDE
- allow using it only on proof nodes
- raise a warning when this transformation is called
- treat the smoke detector transformation in a specific way in the IDE/session so that smoke detected transformation do not make their parent goal appear proved. Adding an "inconsistent if reachable" value ?
[EDIT: Also make sure that the exact same smoke from why3replay can be used in IDE (or intentionally forbid it)? https://gitlab.inria.fr/why3/why3/issues/291search in task view2019-04-02T07:45:09ZLAWALL Juliasearch in task viewIt would be nice to be able to search in the task view.It would be nice to be able to search in the task view.https://gitlab.inria.fr/why3/why3/issues/286Extend witness grammar for type invariant2019-03-26T16:35:06ZFrançois BobotExtend witness grammar for type invariantThe proposal is to extend the current grammar for the `by` construct.
Currently:
```
type t = { f1: ...; f2: ... } invariant { ... } by { f1 = ...; f2 = ...}
```
proposed:
```
type t = { ... } invariant { ... } by e
```
where all leaf of `e` in result position have the shape `{ f1 = ...; f2 = ...}`
The implementation:
- parsing e as an expression
- typing check that all the leaf define all the fields of the record, and translate the leaf into a tuple in the order of the field definition. So the witness is well-typed and doesn't use the defined type.
- check the properties on e
The properties on e checked, currently (not complete, nor correct?):
- no side effect
- pure
I don't see why we have these restrictions, we just want to prove that such element is buildable so any non-ghost computation should be acceptable.The proposal is to extend the current grammar for the `by` construct.
Currently:
```
type t = { f1: ...; f2: ... } invariant { ... } by { f1 = ...; f2 = ...}
```
proposed:
```
type t = { ... } invariant { ... } by e
```
where all leaf of `e` in result position have the shape `{ f1 = ...; f2 = ...}`
The implementation:
- parsing e as an expression
- typing check that all the leaf define all the fields of the record, and translate the leaf into a tuple in the order of the field definition. So the witness is well-typed and doesn't use the defined type.
- check the properties on e
The properties on e checked, currently (not complete, nor correct?):
- no side effect
- pure
I don't see why we have these restrictions, we just want to prove that such element is buildable so any non-ghost computation should be acceptable.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/issues/97range types should introduce an injectivity axiom2019-03-26T15:03:34ZMARCHE Clauderange types should introduce an injectivity axioma range type declaration
type t = range < a b >
generates a function `t'int` with an axiom
forall x:t. a <= t'int x <= b
but does NOT introduce any injectivity property such as
forall x y:t. t'int x = t'int y -> x = y (*1*)
Note that the form (1) is not easy to handle by solver. A potential interesting variant
is introducing a reverse function
function t'ofInt int : t
with axiom
forall x:t. t'ofInt (t'int x) = x (*2*)
This variant has the advantage of avoiding a potential quadratic number of instanciations,
as it is the case for (1)a range type declaration
type t = range < a b >
generates a function `t'int` with an axiom
forall x:t. a <= t'int x <= b
but does NOT introduce any injectivity property such as
forall x y:t. t'int x = t'int y -> x = y (*1*)
Note that the form (1) is not easy to handle by solver. A potential interesting variant
is introducing a reverse function
function t'ofInt int : t
with axiom
forall x:t. t'ofInt (t'int x) = x (*2*)
This variant has the advantage of avoiding a potential quadratic number of instanciations,
as it is the case for (1)https://gitlab.inria.fr/why3/why3/issues/285split_all_full raises out of memory on float theory2019-03-24T14:05:23ZDAILLER Sylvainsplit_all_full raises out of memory on float theoryHello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file [b.mlw](/uploads/777dac8832951acc1eacf6a489be58ba/b.mlw) ). Most likely, on the hypothesis fma_special, the negative monoid generated by split_core grows exponentially (which eventually eat all available memory).
I encountered this problem when launching the strategy "1" (problem which should be solved by #282).
Is it possible to optimize the generation of monoids during the transformation, stop the splitting done by the transformation when it grows to a critical size, or disallow part of the splitting ?Hello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file [b.mlw](/uploads/777dac8832951acc1eacf6a489be58ba/b.mlw) ). Most likely, on the hypothesis fma_special, the negative monoid generated by split_core grows exponentially (which eventually eat all available memory).
I encountered this problem when launching the strategy "1" (problem which should be solved by #282).
Is it possible to optimize the generation of monoids during the transformation, stop the splitting done by the transformation when it grows to a critical size, or disallow part of the splitting ?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.https://gitlab.inria.fr/why3/why3/issues/279Disappearance of keep_on_simp2019-03-01T10:09:10ZDAILLER SylvainDisappearance of keep_on_simpHello,
The attribute keep_on_simp disappeared from 0.88 to 1.0. Are there mechanisms to retrieve the behaviour it was used for ? Why was it dropped ?
I think it prevented simplifications of formulas under this attribute.Hello,
The attribute keep_on_simp disappeared from 0.88 to 1.0. Are there mechanisms to retrieve the behaviour it was used for ? Why was it dropped ?
I think it prevented simplifications of formulas under this attribute.https://gitlab.inria.fr/why3/why3/issues/272CVC4 for smtlib 2.62019-02-12T11:44:55ZDAILLER SylvainCVC4 for smtlib 2.6Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
> Yes, the semantics changed in version 2.6 [0]. `(bvurem s t)` returns `s` if `t` is zero (before, the value was a fresh constant). CVC4 automatically chooses the semantics that matches the SMT-LIB version. You can manually toggle the behavior with --(no-)bv-div-zero-const (enabling the flag corresponds to the 2.6 version, disabling to earlier versions). If your problems only use QF_BV, you can also improve performance by compiling CVC4 with support for CaDiCaL (run the `contrib/get-cadical` script, then configure with `--cadical`) and then using the flags `--bitblast=eager --bv-sat-solver=cadical` (eager bitblasting and using CaDiCaL as the SAT solver).
Is that possible that we now need to add the option "--(no-)bv-div-zero-const" to the smt-lib provers using 2.6 ? It seems to help SPARK users.
Additional question:
Will there be a problem with the following axiom because urem seems to be linked to bvurem by smt-lib drivers ? (axioms about "mod ?x 0" do not seem to exist so I guess it is ok unless mod is also mapped by a driver?)
```
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
```Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
> Yes, the semantics changed in version 2.6 [0]. `(bvurem s t)` returns `s` if `t` is zero (before, the value was a fresh constant). CVC4 automatically chooses the semantics that matches the SMT-LIB version. You can manually toggle the behavior with --(no-)bv-div-zero-const (enabling the flag corresponds to the 2.6 version, disabling to earlier versions). If your problems only use QF_BV, you can also improve performance by compiling CVC4 with support for CaDiCaL (run the `contrib/get-cadical` script, then configure with `--cadical`) and then using the flags `--bitblast=eager --bv-sat-solver=cadical` (eager bitblasting and using CaDiCaL as the SAT solver).
Is that possible that we now need to add the option "--(no-)bv-div-zero-const" to the smt-lib provers using 2.6 ? It seems to help SPARK users.
Additional question:
Will there be a problem with the following axiom because urem seems to be linked to bvurem by smt-lib drivers ? (axioms about "mod ?x 0" do not seem to exist so I guess it is ok unless mod is also mapped by a driver?)
```
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
```https://gitlab.inria.fr/why3/why3/issues/218IDE: should display the right source file in case of syntax or typing error2019-02-11T17:10:49ZMARCHE ClaudeIDE: should display the right source file in case of syntax or typing errorWhen an syntax or typing error occurs in another file than the one(s) currently in the session, such as a file imported, or a file coming from a front-end (C, Java, Python), then the source file in question should be added in a new tab a the cursor positioned on the errorWhen an syntax or typing error occurs in another file than the one(s) currently in the session, such as a file imported, or a file coming from a front-end (C, Java, Python), then the source file in question should be added in a new tab a the cursor positioned on the error1.3.0MARCHE ClaudeMARCHE Claude