why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2018-10-05T09:26:19Zhttps://gitlab.inria.fr/why3/why3/-/issues/195New split_vc sometimes crashes2018-10-05T09:26:19ZRaphaël Rieu-HelftNew split_vc sometimes crashesFollowing commit 22ab5177b, attempting to use split_vc on lemma `valuation_monotonous` in `examples/multiprecision/valuation.mlw` results in a failure (with the new popup!) due to an uncaught NoTerminationProof exception.Following commit 22ab5177b, attempting to use split_vc on lemma `valuation_monotonous` in `examples/multiprecision/valuation.mlw` results in a failure (with the new popup!) due to an uncaught NoTerminationProof exception.1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/188Modify split_vc to not use simplify_trivial_quantification2018-10-04T13:07:54ZRaphaël Rieu-HelftModify split_vc to not use simplify_trivial_quantification1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/128Transformation `split_vc` and term shapes2018-06-13T14:56:30ZGuillaume MelquiondTransformation `split_vc` and term shapesThe transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a single node of the proof tree. As a consequence, pairing gets completely confused as soon as the code is modified.
A solution would be to change the shape algorithm so that it also hashes the premises that have been marked by `introduce_premises`. This might considerably increase the size of the shapes, but that will also make the pairing algorithm more reliable.
I mark this issue as blocking, since `split_vc` is the recommended transformation for newcomers.The transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a single node of the proof tree. As a consequence, pairing gets completely confused as soon as the code is modified.
A solution would be to change the shape algorithm so that it also hashes the premises that have been marked by `introduce_premises`. This might considerably increase the size of the shapes, but that will also make the pairing algorithm more reliable.
I mark this issue as blocking, since `split_vc` is the recommended transformation for newcomers.1.0.0Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/120simplify_trivial_quantification kills some goals2018-05-22T14:47:51ZRaphaël Rieu-Helftsimplify_trivial_quantification kills some goalsOn the following program, after using split_vc twice (once on the function and once on the assertion), the subgoal `not true` is generated by simplify_trivial_quantification. My understanding is that the goal `not z = y` is used to replace `z` with `y` when attempting to eliminate the quantified variable `z`, but I hope I am wrong.
```
let f (l: list int) (y:int)
= assert { match l with Cons z _ -> not z = y | Nil -> false end }
```
I'm marking this as high priority because `split_vc` is intended as a default strategy for most users.On the following program, after using split_vc twice (once on the function and once on the assertion), the subgoal `not true` is generated by simplify_trivial_quantification. My understanding is that the goal `not z = y` is used to replace `z` with `y` when attempting to eliminate the quantified variable `z`, but I hope I am wrong.
```
let f (l: list int) (y:int)
= assert { match l with Cons z _ -> not z = y | Nil -> false end }
```
I'm marking this as high priority because `split_vc` is intended as a default strategy for most users.https://gitlab.inria.fr/why3/why3/-/issues/71Incorrect ident parsing in transformations2018-02-02T09:49:53ZRaphaël Rieu-HelftIncorrect ident parsing in transformationsIn each of the following examples, the output of `print (+)` is `function (+) real real: real` and (in M1) `cut (0 + 0 = 0)` fails with a typing error, when (+) should be the integer addition :
```
module M1
use import real.RealInfix
use import int.Int
constant x: int = 0 + 0
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M2
use import real.RealInfix
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
```
Maybe the `use import real.Real` declaration in `RealInfix` is treated as a `use export` ?In each of the following examples, the output of `print (+)` is `function (+) real real: real` and (in M1) `cut (0 + 0 = 0)` fails with a typing error, when (+) should be the integer addition :
```
module M1
use import real.RealInfix
use import int.Int
constant x: int = 0 + 0
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M2
use import real.RealInfix
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
```
Maybe the `use import real.Real` declaration in `RealInfix` is treated as a `use export` ?DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/19Apply with x2017-11-16T11:40:35ZDAILLER SylvainApply with xIt should be possible to give hint terms to apply (or rewrite). For example:
"apply h with x,y"
For example, it should allow to directly apply a lemma on transitivity:
"H : forall x y z, x < y -> y < z -> x < z
Goal: 0 < 2"
"apply H with 1" generates two new goals "0 < 1" and "1 < 2"It should be possible to give hint terms to apply (or rewrite). For example:
"apply h with x,y"
For example, it should allow to directly apply a lemma on transitivity:
"H : forall x y z, x < y -> y < z -> x < z
Goal: 0 < 2"
"apply H with 1" generates two new goals "0 < 1" and "1 < 2"2017-11-15DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/15destruct_alg improvement2017-11-15T15:25:17ZDAILLER Sylvaindestruct_alg improvementCurrently, "destruct_alg x" does not work on some cases: it should introduce the new destructed part at the right position in the task. When destructed components are used before their definition, the transformation fails.
Also, rewriting after applying this transformation should not be necessary. Add a boolean (or a new transformation name) so that subst is done right after destruct_alg.Currently, "destruct_alg x" does not work on some cases: it should introduce the new destructed part at the right position in the task. When destructed components are used before their definition, the transformation fails.
Also, rewriting after applying this transformation should not be necessary. Add a boolean (or a new transformation name) so that subst is done right after destruct_alg.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/18Case should add expl to its new subgoals2017-11-16T11:40:35ZDAILLER SylvainCase should add expl to its new subgoalsThe transformation "case" should add explanation labels to its subgoals (because these labels are visible in the proof tree). This is more clear for the user.
Transformations induction and others could also take benefits from this.The transformation "case" should add explanation labels to its subgoals (because these labels are visible in the proof tree). This is more clear for the user.
Transformations induction and others could also take benefits from this.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/16subst should remove declarations2018-05-16T14:14:22ZDAILLER Sylvainsubst should remove declarationsApplying "subst x" should remove the definition of x. This new behavior will be added as a new name or as a boolean parameter.Applying "subst x" should remove the definition of x. This new behavior will be added as a new name or as a boolean parameter.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/226Restricting behavior of rewrite_list2018-11-07T09:37:53ZDAILLER SylvainRestricting behavior of rewrite_listHello,
Currently `rewrite_list` uses the argument `with_terms` but I think it is difficult for the user to understand what these with_terms corresponds to with this transformation. This list of terms is supposed to be used by `apply/rewrite` after matching. For example,
```
module Rewrite
use int.Int
function f int : int
predicate p int
axiom A: forall a. f (a+1) = f 42
axiom B: forall a. f a = f (43 + 1)
goal g : 5 = f 42
end
```
`rewrite <- A with 43 (* To instantiate a *)`
`rewrite <- B with 43 (* To instantiate a *)`
To me, it makes less sense to try to do the same when rewriting several hypothesis at once:
`rewrite_list <- A,B with 43`
Also, I am not sure that it works when trying to instantiate with a different value for A and B. Should we remove this feature ?Hello,
Currently `rewrite_list` uses the argument `with_terms` but I think it is difficult for the user to understand what these with_terms corresponds to with this transformation. This list of terms is supposed to be used by `apply/rewrite` after matching. For example,
```
module Rewrite
use int.Int
function f int : int
predicate p int
axiom A: forall a. f (a+1) = f 42
axiom B: forall a. f a = f (43 + 1)
goal g : 5 = f 42
end
```
`rewrite <- A with 43 (* To instantiate a *)`
`rewrite <- B with 43 (* To instantiate a *)`
To me, it makes less sense to try to do the same when rewriting several hypothesis at once:
`rewrite_list <- A,B with 43`
Also, I am not sure that it works when trying to instantiate with a different value for A and B. Should we remove this feature ?Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/196Interaction of smt encoding with meta2021-03-12T23:53:06ZDAILLER SylvainInteraction of smt encoding with metaHello,
For the support of counterexamples, I am trying to add meta on a polymorphic functions but it seems that the transformation `encoding_smt_if_poly` breaks the meta I introduced when it monomorphizes the function. I would have expected the meta to be adapted (by the transformation) to the generated ident for the monomorphized function.
For example, the following task:
```
function length (array 'a) : int
(* meta my_meta function length *)
```
is translated to:
```
function length ty uni : uni
(* meta my_meta function length1 *)
```
Note that length1 seem to still refer to the first definition whereas it does not appear anymore in the task: its only apparition is in the meta declaration. Is there a way to keep the meta on my monomorphized function or should I find another solution ?Hello,
For the support of counterexamples, I am trying to add meta on a polymorphic functions but it seems that the transformation `encoding_smt_if_poly` breaks the meta I introduced when it monomorphizes the function. I would have expected the meta to be adapted (by the transformation) to the generated ident for the monomorphized function.
For example, the following task:
```
function length (array 'a) : int
(* meta my_meta function length *)
```
is translated to:
```
function length ty uni : uni
(* meta my_meta function length1 *)
```
Note that length1 seem to still refer to the first definition whereas it does not appear anymore in the task: its only apparition is in the meta declaration. Is there a way to keep the meta on my monomorphized function or should I find another solution ?Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/22induction_pr with arguments2019-03-27T14:42:06ZDAILLER Sylvaininduction_pr with argumentsMake a version of induction_pr with arguments.
"induction_pr H"
Same for "induction_ty_lex".Make a version of induction_pr with arguments.
"induction_pr H"
Same for "induction_ty_lex".DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/574Record transformation time2021-05-05T16:01:13ZQuentin GarcheryRecord transformation timeWhen developping in Why3, one might want to quickly know which part of the replay of a file takes time.
To this end, I think it would be useful if the transformations also recorded the time they spend. It could be stored in the `why3session.xml` with another attribute to the transformation, which would give something like `<transf name="split_vc" time="0.01" >`. It probably should be disabled by default, although it would mean that we should be able to handle session files that differ in this way.
As for prover calls, it could also be shown in the IDE. To not clutter the IDE, it could only be shown if the time goes beyond X seconds.
Would it even make sense to do this ? Is the time spent by transformations too volatile ?When developping in Why3, one might want to quickly know which part of the replay of a file takes time.
To this end, I think it would be useful if the transformations also recorded the time they spend. It could be stored in the `why3session.xml` with another attribute to the transformation, which would give something like `<transf name="split_vc" time="0.01" >`. It probably should be disabled by default, although it would mean that we should be able to handle session files that differ in this way.
As for prover calls, it could also be shown in the IDE. To not clutter the IDE, it could only be shown if the time goes beyond X seconds.
Would it even make sense to do this ? Is the time spent by transformations too volatile ?https://gitlab.inria.fr/why3/why3/-/issues/567wish: provide monomorphic, clonable modules for references and arrays2021-05-21T18:10:43ZMARCHE Claudewish: provide monomorphic, clonable modules for references and arraysPolymorphism is raising several issues. Currently the encoding from Spark to Why3 carefully avoids to produce any polymorphism in the WhyML generated, because provers CVC4 and Z3 are better when tasks have no polymorphism. The counterexample features are essentially broken in presence of polymorphism. In the current implementation of "jessie3" in collaboration with TIS, I had to suggest to avoid producing WhyML code involving polymorphism, both for proving efficiency and counterexamples. Recently, Quentin came up with the following trivial example
```
use int.Int
use array.Array
let update a i (v:int)
requires { 0 <= i < length a }
ensures { a[i] = v }
= a[i] <- v
```
which is easily solved by Alt-Ergo, but not by CVC4 nor Z3.
I suggest:
- to provide monomorphic clonable versions of ref.Ref and array.Array in the stdlib, which would allow to program without polymorphism unless needed elsewhere
- to review to current support of polymorphism in Why3: are the drivers appropriate? it seems that in Why3 0.xx, using modules ref.Ref or array.Array was *not* enforcing polymorphism in the generated tasks, but since Why3 1.0 tasks generated are always polymorphic because of type `ref'mk 'a` or `array'mk 'a`Polymorphism is raising several issues. Currently the encoding from Spark to Why3 carefully avoids to produce any polymorphism in the WhyML generated, because provers CVC4 and Z3 are better when tasks have no polymorphism. The counterexample features are essentially broken in presence of polymorphism. In the current implementation of "jessie3" in collaboration with TIS, I had to suggest to avoid producing WhyML code involving polymorphism, both for proving efficiency and counterexamples. Recently, Quentin came up with the following trivial example
```
use int.Int
use array.Array
let update a i (v:int)
requires { 0 <= i < length a }
ensures { a[i] = v }
= a[i] <- v
```
which is easily solved by Alt-Ergo, but not by CVC4 nor Z3.
I suggest:
- to provide monomorphic clonable versions of ref.Ref and array.Array in the stdlib, which would allow to program without polymorphism unless needed elsewhere
- to review to current support of polymorphism in Why3: are the drivers appropriate? it seems that in Why3 0.xx, using modules ref.Ref or array.Array was *not* enforcing polymorphism in the generated tasks, but since Why3 1.0 tasks generated are always polymorphic because of type `ref'mk 'a` or `array'mk 'a`1.5.0https://gitlab.inria.fr/why3/why3/-/issues/525destruct/case transformations incorrectly handle polymorphic formulas2021-07-13T14:40:01ZQuentin Garcherydestruct/case transformations incorrectly handle polymorphic formulasThe transformations `case` and `destruct` don't take into account the fact that the formula they are applied to can be implicitely quantified over a type variable.
This allows us to prove `false` in the following ways :
- apply `case (forall x y : 'a. x = y)` and pass the resulting tasks to Eprover
- first prove that `(forall x y : 'a. x = y) \/ (not forall x y : 'a. x = y)` (by calling CVC4 for example), apply `destruct` to this hypothesis and pass the resulting tasks to Eprover
**What's happening ?**
The formula `forall x y : 'a. x = y` should be understood as `forall 'a. forall x y : 'a. x = y`. When we apply `case` on this formula, the negation incorrectly goes under the type quantification in the second task.The transformations `case` and `destruct` don't take into account the fact that the formula they are applied to can be implicitely quantified over a type variable.
This allows us to prove `false` in the following ways :
- apply `case (forall x y : 'a. x = y)` and pass the resulting tasks to Eprover
- first prove that `(forall x y : 'a. x = y) \/ (not forall x y : 'a. x = y)` (by calling CVC4 for example), apply `destruct` to this hypothesis and pass the resulting tasks to Eprover
**What's happening ?**
The formula `forall x y : 'a. x = y` should be understood as `forall 'a. forall x y : 'a. x = y`. When we apply `case` on this formula, the negation incorrectly goes under the type quantification in the second task.1.4.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/405Hide does not work2019-11-04T12:43:00ZDAILLER SylvainHide does not workOn the following simple goal, `hide t 1` does not work. It should be investigated.
```
axiom h: 1 = 3
goal G: forall x. x = 1
```On the following simple goal, `hide t 1` does not work. It should be investigated.
```
axiom h: 1 = 3
goal G: forall x. x = 1
```DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/399`apply with` and `rewrite with` should give more details (e.g., quantifier na...2019-10-28T11:38:53ZGuillaume Melquiond`apply with` and `rewrite with` should give more details (e.g., quantifier names) when the number of arguments do not matchDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/380List transformation with arguments and documentation2019-11-22T15:21:38ZDAILLER SylvainList transformation with arguments and documentationDocument transformations with arguments with examples.
Investigate the possibility to have a more flexible parsing of list arguments in general (remove space constraint in particular `a, b, c`).Document transformations with arguments with examples.
Investigate the possibility to have a more flexible parsing of list arguments in general (remove space constraint in particular `a, b, c`).DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/377Why3 should not introduce spaces in identifiers2019-08-23T12:47:34ZDAILLER SylvainWhy3 should not introduce spaces in identifiersSpaces are introduced in identifiers in some cases. This makes it impossible for the user to use these identifiers in arguments of transformations.
An example with records is the following:
```
use int.Int
type r = {a : int; b : int}
let f (x y: r): bool
ensures {x.a = y.a}
=
true
```
To explicitly show the problem use the following transformations:
`introduce_premises`
`destruct_term x`
`assert (x2 = mk r x1 x)`
@marche suggest to use tick `'` instead of space because the user would still not be able to define those in .mlw file but they would be able to use them. Here, the result would be something along the lines of `r'mk`.
Note that spaces also appear in the names of goals: they could be removed in favor of `'` too. For example: `f'VC`.
On this issue, I will try to make a MR with the simple replacement of `mk ` with `'mk` to see if it could work. Note that I also expect to change accordingly any code that would recognize a record by looking if its name begins with `mk `.Spaces are introduced in identifiers in some cases. This makes it impossible for the user to use these identifiers in arguments of transformations.
An example with records is the following:
```
use int.Int
type r = {a : int; b : int}
let f (x y: r): bool
ensures {x.a = y.a}
=
true
```
To explicitly show the problem use the following transformations:
`introduce_premises`
`destruct_term x`
`assert (x2 = mk r x1 x)`
@marche suggest to use tick `'` instead of space because the user would still not be able to define those in .mlw file but they would be able to use them. Here, the result would be something along the lines of `r'mk`.
Note that spaces also appear in the names of goals: they could be removed in favor of `'` too. For example: `f'VC`.
On this issue, I will try to make a MR with the simple replacement of `mk ` with `'mk` to see if it could work. Note that I also expect to change accordingly any code that would recognize a record by looking if its name begins with `mk `.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/367Trivial goals are not user-friendly2019-12-04T12:24:11ZGuillaume MelquiondTrivial goals are not user-friendlyWhen doing `split_vc` on the weakest precondition of `bar`
```
let foo () requires { true } = ()
let bar () = foo (); foo ()
```
we get two subgoals `true` marked as unknown. At this point, the user can either apply `split_vc` or launch a prover, on each subgoal. In both cases, this is a waste of user time and processor cycles. This becomes especially noticeable after !207, as the number of trivial goals greatly increases.
Two possible solutions:
1. Automatically mark `true` goals as proved.
2. Prevent `split_vc` from generating them.When doing `split_vc` on the weakest precondition of `bar`
```
let foo () requires { true } = ()
let bar () = foo (); foo ()
```
we get two subgoals `true` marked as unknown. At this point, the user can either apply `split_vc` or launch a prover, on each subgoal. In both cases, this is a waste of user time and processor cycles. This becomes especially noticeable after !207, as the number of trivial goals greatly increases.
Two possible solutions:
1. Automatically mark `true` goals as proved.
2. Prevent `split_vc` from generating them.