why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2024-01-31T14:02:14+01:00https://gitlab.inria.fr/why3/why3/-/issues/287Add injectivity for type invariant2024-01-31T14:02:14+01:00François BobotAdd injectivity for type invariant```
type t = {
v: int;
} invariant { 0 <= v }
```
It is currently not possible to prove that:
```
forall x1 x2:t. x1.v = x2.v -> x1 = x2
```
Which is compiled to:
```
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
```
We need...```
type t = {
v: int;
} invariant { 0 <= v }
```
It is currently not possible to prove that:
```
forall x1 x2:t. x1.v = x2.v -> x1 = x2
```
Which is compiled to:
```
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
```
We need to add the property that `view` is injective, for example using `mk` its inverse:
```
forall x:t [view x]. mk (view x) = x
```
# Decision #
> So, we agreed that adding `t'mk` for constructing a non-private type `t` from its fields is a good idea.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/625Allow running prover in parallel in strategies2023-09-12T15:46:20+02:00MARCHE ClaudeAllow running prover in parallel in strategiesThe strategies should provide a way to run provers in parallel, so that when one of such prover succeed, the others are interrupted as soon as possibleThe strategies should provide a way to run provers in parallel, so that when one of such prover succeed, the others are interrupted as soon as possible1.7.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/742Attributes before a `let` in a formula are lost2023-04-30T11:09:27+02:00Guillaume CluzelAttributes before a `let` in a formula are lostConsidering the following program
```
let f (ref x : int) : unit
ensures { [@xxxx] [@expl:foo] let a = x in a = 0 }
= x <- 0
```
I would expect to see the attribute `[@expl:foo]` and `[@xxxx]` in the VC that correspond to the goal fo...Considering the following program
```
let f (ref x : int) : unit
ensures { [@xxxx] [@expl:foo] let a = x in a = 0 }
= x <- 0
```
I would expect to see the attribute `[@expl:foo]` and `[@xxxx]` in the VC that correspond to the goal for the ensures. But only the attribute `[@expl:foo]` is kept, the other is lost during the generation of VC as show by the verbatim:
```
goal f'vc [@expl:VC for f] : [@hyp_name:Ensures] [@expl:foo] x = 0
```
It would be better to treat those attributes as the expl ones.https://gitlab.inria.fr/why3/why3/-/issues/667strategies should always use most recent versions of provers2022-11-15T13:36:31+01:00MARCHE Claudestrategies should always use most recent versions of proversOn my laptop the strategy 0, as shown by `why3 config show` uses Alt-Ergo 2.4.0, CVC4 1.7 and Z3 4.8.6. Yet, I have Alt-Ergo 2.4.1, CVC4 1.8 and Z3 4.8.10, and these are correctly detected and shown by `why3 config list-provers`.
I beli...On my laptop the strategy 0, as shown by `why3 config show` uses Alt-Ergo 2.4.0, CVC4 1.7 and Z3 4.8.6. Yet, I have Alt-Ergo 2.4.1, CVC4 1.8 and Z3 4.8.10, and these are correctly detected and shown by `why3 config list-provers`.
I believe the most recent version should be used in strategies.1.6.0https://gitlab.inria.fr/why3/why3/-/issues/690CVC4 driver does not escape `is`2022-11-15T12:40:03+01:00Xavier DenisCVC4 driver does not escape `is`It seems like if you have a variable called `is` then CVC4 will not properly escape it and crash.
Attached is the generated SMT showing the issue.
[05_map-C05Map_Impl0_Next-nextqtvc_1.smt2](/uploads/eba1b6d81ae26399ee63c9c68c06be49/05_...It seems like if you have a variable called `is` then CVC4 will not properly escape it and crash.
Attached is the generated SMT showing the issue.
[05_map-C05Map_Impl0_Next-nextqtvc_1.smt2](/uploads/eba1b6d81ae26399ee63c9c68c06be49/05_map-C05Map_Impl0_Next-nextqtvc_1.smt2)MOREAU SoleneMOREAU Solenehttps://gitlab.inria.fr/why3/why3/-/issues/387Cloning: please improve syntax and error messages2021-03-12T18:45:52+01:00MARCHE ClaudeCloning: please improve syntax and error messagesSee the following example file.
1. in the first case, the error message should be much more explicit on why the instantiation is illegal
2. in the second case: the syntax `val function` seems not supported though it should be natural
3. ...See the following example file.
1. in the first case, the error message should be much more explicit on why the instantiation is illegal
2. in the second case: the syntax `val function` seems not supported though it should be natural
3. in the third case it works but: one would expect that only the program symbol would be substituted. the goal afterwards is proved (e.g by Alt-Ergo) and so the logic symbol is also substituted, which is just unexpected
```
module M
type t
val function f t : t
end
module N
use int.Int
function g (x:int) : int = x+1
(* give `Illegal instantiation for symbol f`
clone M
with type t = int, function f = g
*)
let function h (x:int) : int = x+1
(* give ` syntax error` (on lexeme `function`)
clone M
with type t = int, val function f = h
*)
clone M
with type t = int, val f = h
goal test: g 41 = 42
end
```1.4.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/392Allow changing foreground color in source on error2021-02-15T16:54:26+01:00DAILLER SylvainAllow changing foreground color in source on errorCurrently, its not possible to do this change AFAIK. And, the gconfig.error_color parameter is used both for the error message (bottom right corner) and for the source coloring.Currently, its not possible to do this change AFAIK. And, the gconfig.error_color parameter is used both for the error message (bottom right corner) and for the source coloring.1.3.0https://gitlab.inria.fr/why3/why3/-/issues/325Extraction of partial applications2020-06-02T10:57:16+02:00Raphaël Rieu-HelftExtraction of partial applicationsExtraction of partial applications fails at least in the following case
```
let f (ghost x1 : int) (x2:int) (x3:int) = 53
let main () =
let g = f 1 in
let h = g 2 in
h 3
```
We should also add constructors to Mltree to dif...Extraction of partial applications fails at least in the following case
```
let f (ghost x1 : int) (x2:int) (x3:int) = 53
let main () =
let g = f 1 in
let h = g 2 in
h 3
```
We should also add constructors to Mltree to differentiate between total and partial application.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/42Invalid_argument('Expr.let_rec") in clone declarations2020-03-17T01:18:27+01:00Raphaël Rieu-HelftInvalid_argument('Expr.let_rec") in clone declarationsIn a large clone declaration containing `val x = y` where `x` is a `val constant` and y is a `let ghost constant` , I received the error `Invalid_argument("Expr.let_rec")`. My attempts to reproduce on smaller examples were not rejected a...In a large clone declaration containing `val x = y` where `x` is a `val constant` and y is a `let ghost constant` , I received the error `Invalid_argument("Expr.let_rec")`. My attempts to reproduce on smaller examples were not rejected at all.1.3.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/168Cloning function with bad ghost status raises Invalid_argument("Expr.let_rec")2020-03-17T01:18:26+01:00PARREIRA PEREIRA Mário JoséCloning function with bad ghost status raises Invalid_argument("Expr.let_rec")The following fails with anomaly: Invalid_argument("Expr.let_rec")
```
module A
type t
val f (ghost x: t) : t
let rec ff (ghost x: t) = f x
end
module B
let f (x: int) = 42
clone A with val f, type t = int
end
```
The...The following fails with anomaly: Invalid_argument("Expr.let_rec")
```
module A
type t
val f (ghost x: t) : t
let rec ff (ghost x: t) = f x
end
module B
let f (x: int) = 42
clone A with val f, type t = int
end
```
The error message points to the `clone` line. Removing the `rec` keyword from the definition of `ff`, or stating the argument `x`, of function `f` in module B, as ghost removes the problem.
The error message is a little cryptic, and I don't fully understand why this only happens when we call `f` inside a `let rec` definition.1.3.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/420The behavior of Ctrl-Down is not user-friendly2020-03-06T13:22:18+01:00Raphaël Rieu-HelftThe behavior of Ctrl-Down is not user-friendlyOn the following file, apply `split_vc` on main and on subgoal 0, and prove subgoal 1 by calling a prover.
```
use int.Int
let f () : unit requires { 1 + 1 = 2 /\ 2 + 2 = 4 } = ()
let main () = f(); f(); f()
```
Assume that we want t...On the following file, apply `split_vc` on main and on subgoal 0, and prove subgoal 1 by calling a prover.
```
use int.Int
let f () : unit requires { 1 + 1 = 2 /\ 2 + 2 = 4 } = ()
let main () = f(); f(); f()
```
Assume that we want to save the proof of subgoal 0 for later. The navigation between goals with Ctrl-Up/Down becomes very painful. We can observe two issues:
- When selecting a subgoal of goal 0, pressing Ctrl-Down only cycles between subgoals 0.0 and 0.1, never reaching subgoal 2.
- When selecting subgoal 1, pressing Ctrl-Down jumps back up to 0.0 instead of going to 2.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/452Update gallery2020-03-04T16:56:19+01:00Guillaume MelquiondUpdate gallerySee at the bottom of `misc/release.md` for instructions about gallery generation.
:warning: Never commit all the modified files of the generated gallery. Only commit the few examples that you have just added to `examples.rc`.
Examples ...See at the bottom of `misc/release.md` for instructions about gallery generation.
:warning: Never commit all the modified files of the generated gallery. Only commit the few examples that you have just added to `examples.rc`.
Examples that are not yet part of the gallery:
- [x] `array_most_frequent`
- [x] `bignum` (too simple)
- [x] `coincidence_count_list`
- [x] `cubic_root`
- [x] `cursor_examples`
- [x] `equality_up_to_spaces`
- [x] `huffman_with_two_queues`
- [x] (Claude) `isqrt_von_neumann`
- [x] `leftist_heap`
- [x] `list_removal`
- [x] `min_max`
- [x] (Claude) `nistonacci`
- [x] `pairing_heap`
- [x] `pairing_heap_bin`
- [x] `queue_two_lists`
- [x] `simple_queue` (renamed `ring_buffer`)
- [x] `string_base64_encoding`
- [x] `string_hex_encoding`
- [x] `string_search` (to be completed first)
- [x] `subsequence`
- [x] (Claude) `sumrange`
- [x] `white_and_black_balls`
- [x] `word_common_factor`
Multi-file examples that are not yet part of the gallery:
- [x] (outdated) `bitvectors`
- [x] (outdated) `foveoos11-cm`
Multi-file examples that need updating:
- [x] `multiprecision`
Multi-file examples that seem up-to-date but use an antediluvian documentation:
- [x] (Claude) `double_wp`
- [x] (Claude) `verifythis_2016_matrix_multiplication`1.3.0Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/450Wrong smtlib file generation for ieee_float.FloatXX.in_range (at least) for CVC42020-03-04T10:36:51+01:00Ghost UserWrong smtlib file generation for ieee_float.FloatXX.in_range (at least) for CVC4On the following example:
```why3
module Cvc4Bug
use ieee_float.Float32
goal G: in_range 0.0
end
```
The following command fails:
```
$ why3 prove cvc4_bug.mlw -P cvc4
cvc4_bug.mlw Cvc4Bug G: HighFailure (0.03s, 36 steps)
Prover e...On the following example:
```why3
module Cvc4Bug
use ieee_float.Float32
goal G: in_range 0.0
end
```
The following command fails:
```
$ why3 prove cvc4_bug.mlw -P cvc4
cvc4_bug.mlw Cvc4Bug G: HighFailure (0.03s, 36 steps)
Prover exit status: exited with status 1
Prover output:
(error "expecting an integer subterm")
...
```
Apparently, `in_range` is transformed into `abs 0.0` which requires an int. Note that on Why3 1.2.1, the file contains a definition `abs1` for real numbers, but the generated goal uses `abs` (leading to the same error). If `in_range` is used in a lemma or an axiom, the same bug happens.1.3.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/401set logic to ALL_SUPPORTED for CVC42020-02-13T12:00:44+01:00MARCHE Claudeset logic to ALL_SUPPORTED for CVC4replace the hardcoded logic AUFBVDTFPNIRA by ALL_SUPPORTED
this requires:
* fix the driver for the built-in sqrt function on real numbers
* decide from which version of CVC4 this is accepted. Maybe only from version 1.7replace the hardcoded logic AUFBVDTFPNIRA by ALL_SUPPORTED
this requires:
* fix the driver for the built-in sqrt function on real numbers
* decide from which version of CVC4 this is accepted. Maybe only from version 1.71.3.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/374eliminate_if transformation explodes2019-12-10T12:59:00+01:00Johannes Kanigeliminate_if transformation explodes[lexer__read_token.mlw](/uploads/1401f6eea89f1d461211f6cb8e6b6e8e/lexer__read_token.mlw)
On the attached file, eliminate_if creates a huge formula (20M nodes??) starting from a very small one (less than 200 nodes).
This should reproduce...[lexer__read_token.mlw](/uploads/1401f6eea89f1d461211f6cb8e6b6e8e/lexer__read_token.mlw)
On the attached file, eliminate_if creates a huge formula (20M nodes??) starting from a very small one (less than 200 nodes).
This should reproduce on master using this command: `why3 prove lexer__read_token.mlw -P alt-ergo`Quentin GarcheryQuentin Garcheryhttps://gitlab.inria.fr/why3/why3/-/issues/300Add file from IDE is broken2019-11-20T08:57:04+01:00DAILLER 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" st...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.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/381Make sure that Str is not used in places that trywhy3 uses2019-11-14T12:31:49+01:00Raphaël Rieu-HelftMake sure that Str is not used in places that trywhy3 uses`js_of_ocaml` does not support `Str`, which is used in Why3 in several places. We should:
- check that `Str` is still not used in places that `trywhy3` actually uses
- try to find a way to prevent future misuses of `Str`, ideally at comp...`js_of_ocaml` does not support `Str`, which is used in Why3 in several places. We should:
- check that `Str` is still not used in places that `trywhy3` actually uses
- try to find a way to prevent future misuses of `Str`, ideally at compile time or as part of the CI process.Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/222syntax function in extraction drivers2019-11-13T11:06:25+01:00Jean-Christophe Filliâtresyntax function in extraction driversSince 1.0.0, it makes no sense to use "syntax function" in extraction drivers. It should be "syntax val" instead.Since 1.0.0, it makes no sense to use "syntax function" in extraction drivers. It should be "syntax val" instead.Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/283module appmap.AppMap should propose *finite domain* maps2019-11-12T15:06:51+01:00MARCHE Claudemodule appmap.AppMap should propose *finite domain* mapsthe module appmap.AppMap is an interface for maps without domain. It should be an interface for maps of finite domain only.
Moreover, it should take the equality on the type of keys as parameterthe module appmap.AppMap is an interface for maps without domain. It should be an interface for maps of finite domain only.
Moreover, it should take the equality on the type of keys as parameter1.3.0Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/384Named results shadow parameter names2019-11-12T14:27:22+01:00Raphaël Rieu-HelftNamed results shadow parameter namesIf the result of a function is named with the same name as a parameter of the function, it becomes impossible to refer to this parameter in the ensures. I think it should be forbidden to give the result the same name as a parameter.
```...If the result of a function is named with the same name as a parameter of the function, it becomes impossible to refer to this parameter in the ensures. I think it should be forbidden to give the result the same name as a parameter.
```
let samename (x:uint64) : (x:uint64)
requires { x = 1 }
ensures { x = 3 }
= 3
```DIVERIO DiegoDIVERIO Diego