why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2021-02-24T09:54:37Zhttps://gitlab.inria.fr/why3/why3/-/issues/559Vanished invariant "expl" attribute2021-02-24T09:54:37ZDenis CousineauVanished invariant "expl" attributeHello all,
I searched a little bit in the list of issues but did not find any that is relative to my problem.
The problem is that, in some cases "expl" attributes on invariants terms are lost when seeing the associated verifications conditions in the IDE, or when getting them back from the API via `Termcode.goal_expl_task`.
For example, in the following code:
```whyml
module Pb_invariant_attribute
use export ref.Ref
use export bool.Bool
val a : ref bool
val b : ref bool
val c : ref bool
let test ()
diverges
=
while (true)
do
invariant { [@expl:foo] (!a) }
invariant { [@expl:bar] (not (!b)) }
invariant { [@expl:bla] (not (not (!c))) }
done
end
```
After a split, VCs concerning `a` are labelled "Loop invariant init" and "Loop invariant preservation", while the ones concerning `b` and `c` are respectively labelled "bar" and "bla".
![bug_label](/uploads/6aa13685211a32590f46903741d45d3a/bug_label.PNG)
[bug_label.mlw](/uploads/f3e23fff25044f42ed1727e4f8ec00b5/bug_label.mlw)Hello all,
I searched a little bit in the list of issues but did not find any that is relative to my problem.
The problem is that, in some cases "expl" attributes on invariants terms are lost when seeing the associated verifications conditions in the IDE, or when getting them back from the API via `Termcode.goal_expl_task`.
For example, in the following code:
```whyml
module Pb_invariant_attribute
use export ref.Ref
use export bool.Bool
val a : ref bool
val b : ref bool
val c : ref bool
let test ()
diverges
=
while (true)
do
invariant { [@expl:foo] (!a) }
invariant { [@expl:bar] (not (!b)) }
invariant { [@expl:bla] (not (not (!c))) }
done
end
```
After a split, VCs concerning `a` are labelled "Loop invariant init" and "Loop invariant preservation", while the ones concerning `b` and `c` are respectively labelled "bar" and "bla".
![bug_label](/uploads/6aa13685211a32590f46903741d45d3a/bug_label.PNG)
[bug_label.mlw](/uploads/f3e23fff25044f42ed1727e4f8ec00b5/bug_label.mlw)https://gitlab.inria.fr/why3/why3/-/issues/558Overzealous positivity checker?2021-02-23T14:32:22ZRaphaël Rieu-HelftOverzealous positivity checker?On the following example, Why3 complains about a non strictly positive occurrence of `t`, but I don't understand why it is problematic.
```
use int.Int
type t = { x : int }
with u = { y : t -> int; }
```
Obviously, in this simplified example, the recursive type definition is not needed, so there is an easy workaround. But in my general usecase (translating C programs to WhyML, including forward struct declarations and structs containing pointers to other structs), I will need recursive type definitions and this workaround will not apply. I don't understand the positivity criterion well enough to understand if what I'm doing is actually problematic or if the checker is being overzealous. @paskevyc maybe you can enlighten me?On the following example, Why3 complains about a non strictly positive occurrence of `t`, but I don't understand why it is problematic.
```
use int.Int
type t = { x : int }
with u = { y : t -> int; }
```
Obviously, in this simplified example, the recursive type definition is not needed, so there is an easy workaround. But in my general usecase (translating C programs to WhyML, including forward struct declarations and structs containing pointers to other structs), I will need recursive type definitions and this workaround will not apply. I don't understand the positivity criterion well enough to understand if what I'm doing is actually problematic or if the checker is being overzealous. @paskevyc maybe you can enlighten me?https://gitlab.inria.fr/why3/why3/-/issues/557Build a glossary of error messages2021-02-23T08:52:54ZMARCHE ClaudeBuild a glossary of error messagesThere are quite a lot of possible error messages from Why3, in particular from typing. It would help beginners, and indeed all users, if all these messages where explained in the manual, hopefully with examples.
Note: there should be at least one example exhibiting each error message anyway, in `bench/typing/bad'There are quite a lot of possible error messages from Why3, in particular from typing. It would help beginners, and indeed all users, if all these messages where explained in the manual, hopefully with examples.
Note: there should be at least one example exhibiting each error message anyway, in `bench/typing/bad'https://gitlab.inria.fr/why3/why3/-/issues/556Unused variable2021-02-23T14:47:33ZGuillaume CluzelUnused variableOn this small program
```ocaml
module Global_logic_declarations
use mach.int.Int32
use ref.Ref
type s = {
a_from_struct_S : Int32.int32
}
let rec f () : Int32.int32
ensures { result = 12 }
=
let x = (Ref.ref (any s) : Ref.ref s) in
Ref.(:=) x { (Ref.(!) x) with a_from_struct_S = 12 };
(Ref.(!) x).a_from_struct_S
end
```
Why3 tells me
```
warning: unused variable q
Ref.(:=) x { (Ref.(!) x) with a_from_struct_S = 12 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But, there is no variable `q` at all declared in my program, nor in `mach.int.Int32` or `Ref.ref`. Does this warning warn a real problem or can it be removed?On this small program
```ocaml
module Global_logic_declarations
use mach.int.Int32
use ref.Ref
type s = {
a_from_struct_S : Int32.int32
}
let rec f () : Int32.int32
ensures { result = 12 }
=
let x = (Ref.ref (any s) : Ref.ref s) in
Ref.(:=) x { (Ref.(!) x) with a_from_struct_S = 12 };
(Ref.(!) x).a_from_struct_S
end
```
Why3 tells me
```
warning: unused variable q
Ref.(:=) x { (Ref.(!) x) with a_from_struct_S = 12 };
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But, there is no variable `q` at all declared in my program, nor in `mach.int.Int32` or `Ref.ref`. Does this warning warn a real problem or can it be removed?https://gitlab.inria.fr/why3/why3/-/issues/555Add support for `string` type and module `io` in `why3 execute`2021-02-19T16:39:44ZMARCHE ClaudeAdd support for `string` type and module `io` in `why3 execute`Support for string and printing function in `why3 execute` could provide simple debugging features.
See also #554Support for string and printing function in `why3 execute` could provide simple debugging features.
See also #5541.5.0https://gitlab.inria.fr/why3/why3/-/issues/554Document the modulo `io`, document printing capabilities2021-02-19T16:25:10ZMARCHE ClaudeDocument the modulo `io`, document printing capabilitiesDocument, and export it to [Stdlib online doc](http://why3.lri.fr/stdlib/)
Also, document how to print in the manualDocument, and export it to [Stdlib online doc](http://why3.lri.fr/stdlib/)
Also, document how to print in the manual1.5.0https://gitlab.inria.fr/why3/why3/-/issues/553Broken uninstalled prover window2021-02-19T12:06:29ZRaphaël Rieu-HelftBroken uninstalled prover windowOn the most recent master (b6ed3c1b), I opened the IDE, made the goals obsolete with `o`, and attempted to replay the proof where one of the provers was uninstalled (examples/multiprecision/sqrt.mlw without Alt-Ergo 2.2.0). The uninstalled prover window was broken (screenshot below), and all choices except "remove these proofs from session" triggered a fatal assertion (line 1402 of `gconfig.ml`).
![uninstalled_prover](/uploads/8f66ee7c4877a715c2c02521ddd3c0dd/uninstalled_prover.png)On the most recent master (b6ed3c1b), I opened the IDE, made the goals obsolete with `o`, and attempted to replay the proof where one of the provers was uninstalled (examples/multiprecision/sqrt.mlw without Alt-Ergo 2.2.0). The uninstalled prover window was broken (screenshot below), and all choices except "remove these proofs from session" triggered a fatal assertion (line 1402 of `gconfig.ml`).
![uninstalled_prover](/uploads/8f66ee7c4877a715c2c02521ddd3c0dd/uninstalled_prover.png)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/551Module `mach.bv` should provide purely bitvector-based pre-conditions2021-02-12T13:38:09ZMARCHE ClaudeModule `mach.bv` should provide purely bitvector-based pre-conditionsAs a follow-up of issue #340, this issue calls for improvement in the pre-conditions of the function of the modules `mach.bv.*`. Usage of functions `to_int` and `to_uint` are not convenient for provers with built-in BV support, hence bit-vector style formulas should be used instead. The book Hacker's Delight should provide good solutions.As a follow-up of issue #340, this issue calls for improvement in the pre-conditions of the function of the modules `mach.bv.*`. Usage of functions `to_int` and `to_uint` are not convenient for provers with built-in BV support, hence bit-vector style formulas should be used instead. The book Hacker's Delight should provide good solutions.1.5.0https://gitlab.inria.fr/why3/why3/-/issues/550Add support for recent versions of Z32021-02-11T10:34:46ZMARCHE ClaudeAdd support for recent versions of Z3Add support for Z3 4.8.7 to 4.8.10 :
https://github.com/Z3Prover/z3/releasesAdd support for Z3 4.8.7 to 4.8.10 :
https://github.com/Z3Prover/z3/releases1.4.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/549z3 4.5.12021-02-07T17:04:55ZBas Spittersz3 4.5.1When installing easycrypt, I get:
why3 config --detect --full-config
....
Prover Z3 version 4.5.1 is not known to be supported.When installing easycrypt, I get:
why3 config --detect --full-config
....
Prover Z3 version 4.5.1 is not known to be supported.https://gitlab.inria.fr/why3/why3/-/issues/548Incorrect representation of float literal -12021-02-04T12:20:17ZGuillaume CluzelIncorrect representation of float literal -1Consider the program
```
use ieee_float.Float64
let rec f (a : Float64.t): Float64.t
ensures { result = (-1. : Float64.t) }
= a
```
The literal `(-1. : Float64.t)` is represented by `(fp #b1 #b00000000000 #b1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)` in the file generated for CVC4 and Z3.
You can notice that the fraction part contains 1045 numbers while it should contain only 52 bits.Consider the program
```
use ieee_float.Float64
let rec f (a : Float64.t): Float64.t
ensures { result = (-1. : Float64.t) }
= a
```
The literal `(-1. : Float64.t)` is represented by `(fp #b1 #b00000000000 #b1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)` in the file generated for CVC4 and Z3.
You can notice that the fraction part contains 1045 numbers while it should contain only 52 bits.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/547Syntactic sugar for lemma functions2021-02-11T09:34:39ZLoï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/546Inductive proofs on inductives2021-02-11T09:35:12ZLoïc CorrensonInductive proofs on inductivesThis is a proposal feature allowing inductive proofs over inductive predicates in why3.
Consider an inductive predicate `P` as follows:
```
inductive p xs = A: forall ys. hs -> p es | ...
```
The idea is to automatically generate the following items:
- `type p'witness = A ys | ...` witnessing the universally quantified variables obtained to build a proof of `p` with each constructor
- `val ghost function p'proof xs : p'witness` returns, under precondition `p xs`, a witness of its (minimal) proof.
- `val ghost function p'induction xs : int` returns a (decreasing) variant over the proof of `p xs`.
The post condition of `p'proof xs` introduces, for each witness constructor `A ys` the hypotheses `hs` and the associated unifications of `es` and `xs`, together with strictly decreasing variants of `p'induction` for any sub-proofs of `p` in `hs`.
A complete example of how this can be used in practice is provided here:
- [ind.mlw](/uploads/a336611a3844c6a68dcbc8debfa44960/ind.mlw): full example of use of the generated symbols
(including also why3/why3#547 although it is not necessary…).
- [ind_gen.mlw](/uploads/d42763ecbdab345676b472d7d8fecdb6/ind_gen.mlw): the full exemple together with the (axiomatized) generated symbols, that makes the lemma proof automatically discharged easily.
- [ind.v](/uploads/042c16623daa356c4ef5ef0b792d3e06/ind.v): a Coq realization of the generated symbols of the example using destruction of the inductive predicate in `Type` (we can not realize modules... yet, although it shall look like this).
- [ind_fol.mlw](/uploads/dbf0d183aa20786db2437064782ba440/ind_fol.mlw): a fully proven Why-3 reference implementation (without inductives) for all the generated symbols of the example.This is a proposal feature allowing inductive proofs over inductive predicates in why3.
Consider an inductive predicate `P` as follows:
```
inductive p xs = A: forall ys. hs -> p es | ...
```
The idea is to automatically generate the following items:
- `type p'witness = A ys | ...` witnessing the universally quantified variables obtained to build a proof of `p` with each constructor
- `val ghost function p'proof xs : p'witness` returns, under precondition `p xs`, a witness of its (minimal) proof.
- `val ghost function p'induction xs : int` returns a (decreasing) variant over the proof of `p xs`.
The post condition of `p'proof xs` introduces, for each witness constructor `A ys` the hypotheses `hs` and the associated unifications of `es` and `xs`, together with strictly decreasing variants of `p'induction` for any sub-proofs of `p` in `hs`.
A complete example of how this can be used in practice is provided here:
- [ind.mlw](/uploads/a336611a3844c6a68dcbc8debfa44960/ind.mlw): full example of use of the generated symbols
(including also why3/why3#547 although it is not necessary…).
- [ind_gen.mlw](/uploads/d42763ecbdab345676b472d7d8fecdb6/ind_gen.mlw): the full exemple together with the (axiomatized) generated symbols, that makes the lemma proof automatically discharged easily.
- [ind.v](/uploads/042c16623daa356c4ef5ef0b792d3e06/ind.v): a Coq realization of the generated symbols of the example using destruction of the inductive predicate in `Type` (we can not realize modules... yet, although it shall look like this).
- [ind_fol.mlw](/uploads/dbf0d183aa20786db2437064782ba440/ind_fol.mlw): a fully proven Why-3 reference implementation (without inductives) for all the generated symbols of the example.https://gitlab.inria.fr/why3/why3/-/issues/545why3 execute computes out of range values2021-02-11T10:18:47ZGuillaume Melquiondwhy3 execute computes out of range values```shell
> why3 execute foo.mlw --use mach.int.Int31 "10000000 * 100000000"
result: int31 = 1000000000000000
globals:
``````shell
> why3 execute foo.mlw --use mach.int.Int31 "10000000 * 100000000"
result: int31 = 1000000000000000
globals:
```1.4.0Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/544transformation `compute` is too permissive with respect to division2021-02-11T10:35:11ZMARCHE Claudetransformation `compute` is too permissive with respect to divisionWith the file
```
use int.Int
use int.ComputerDivision
goal g : div 1 0 = 0
```
the transformation `compute_in_goal` solves the goal, which is incorrect.
Probably the same mistake with `rem`, and with `EuclideanDivision` too.With the file
```
use int.Int
use int.ComputerDivision
goal g : div 1 0 = 0
```
the transformation `compute_in_goal` solves the goal, which is incorrect.
Probably the same mistake with `rem`, and with `EuclideanDivision` too.1.4.0Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/543why3 execute fails with "anomaly: Not_found"2021-02-11T09:29:56ZGuillaume Melquiondwhy3 execute fails with "anomaly: Not_found"```console
> why3 execute foo.mlw --use mach.int.UInt64 "0 - 1"
anomaly: Not_found
``````console
> why3 execute foo.mlw --use mach.int.UInt64 "0 - 1"
anomaly: Not_found
```Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/542Execution of "division by zero" succeeds2021-02-11T09:30:13ZGuillaume MelquiondExecution of "division by zero" succeeds```console
> why3 execute empty.mlw --use int.ComputerDivision "div 1 0"
result: int = 0
globals:
``````console
> why3 execute empty.mlw --use int.ComputerDivision "div 1 0"
result: int = 0
globals:
```https://gitlab.inria.fr/why3/why3/-/issues/541The execute button in TryWhy3 no longer works2021-02-02T21:20:07ZGuillaume MelquiondThe execute button in TryWhy3 no longer worksWhen pressing the "execute" button, TryWhy3 complains: "No main function found" (even when there is a `main` function), which makes the feature completely uselles. This is a regression with respect to TryWhy3 1.3.When pressing the "execute" button, TryWhy3 complains: "No main function found" (even when there is a `main` function), which makes the feature completely uselles. This is a regression with respect to TryWhy3 1.3.1.4.0https://gitlab.inria.fr/why3/why3/-/issues/540TryWhy3 crashes at startup: "caml_thread_initialize not implemented"2021-02-02T18:47:21ZGuillaume MelquiondTryWhy3 crashes at startup: "caml_thread_initialize not implemented"Since the `Unix` module is indirectly reachable from `trywhy3/why_worker.ml`, JavaScript chokes on the initialization code of this module, which includes a call to the unavailable function `caml_thread_initialize`.Since the `Unix` module is indirectly reachable from `trywhy3/why_worker.ml`, JavaScript chokes on the initialization code of this module, which includes a call to the unavailable function `caml_thread_initialize`.1.4.0