why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2021-05-05T16:01:13Zhttps://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.https://gitlab.inria.fr/why3/why3/-/issues/366Incorrect goal location after splitting.2019-07-16T13:01:08ZGuillaume MelquiondIncorrect goal location after splitting.Testcase:
```
val bar (x:int): unit requires { x <> 0 }
let foo (x:int) : unit = bar x; bar x
```
When clicking the initially unique goal in the IDE, both calls `bar x` are properly highlighted as being the preconditions to prove. After splitting the goal, both goals cause the IDE to highlight the first call `bar x`, while the second goal is meant to be the precondition of the second call.
Note that this happens quite often in practice. For example, the fast exponentiation algorithm (or its variant, the ancient Egyptian multiplication) contains both divisions and modulos, which all have the same precondition, so all the goals point to the same location of the code.Testcase:
```
val bar (x:int): unit requires { x <> 0 }
let foo (x:int) : unit = bar x; bar x
```
When clicking the initially unique goal in the IDE, both calls `bar x` are properly highlighted as being the preconditions to prove. After splitting the goal, both goals cause the IDE to highlight the first call `bar x`, while the second goal is meant to be the precondition of the second call.
Note that this happens quite often in practice. For example, the fast exponentiation algorithm (or its variant, the ancient Egyptian multiplication) contains both divisions and modulos, which all have the same precondition, so all the goals point to the same location of the code.https://gitlab.inria.fr/why3/why3/-/issues/330Use hypotheses when doing compile_match2020-10-28T13:07:52ZPARREIRA PEREIRA Mário JoséUse hypotheses when doing compile_matchFor the following example:
```
use list.List
constant l: list int = Cons 42 Nil
goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end
```
if I want to get a goal of the form `42 = 42`, I must do first `subst_all` and only then `compile_match` is able to give me `42 = 42`.
Would it be possible for `compile_match` to use hypotheses of the form `H: e = e'` to further simplify goals of the form `match e with e' -> ... end` ?For the following example:
```
use list.List
constant l: list int = Cons 42 Nil
goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end
```
if I want to get a goal of the form `42 = 42`, I must do first `subst_all` and only then `compile_match` is able to give me `42 = 42`.
Would it be possible for `compile_match` to use hypotheses of the form `H: e = e'` to further simplify goals of the form `match e with e' -> ... end` ?https://gitlab.inria.fr/why3/why3/-/issues/285split_all_full raises out of memory on float theory2021-01-22T14:44:34ZDAILLER 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 ?1.5.0https://gitlab.inria.fr/why3/why3/-/issues/280induction_ty_arg_lex expected behavior2019-03-26T13:59:30ZDAILLER Sylvaininduction_ty_arg_lex expected behaviorThis is to investigate the behavior of induction_ty_arg_lex that apparently does not do induction on the right elements.
It was reported by users that on this:
```
goal list_simpl_r :
forall l1:list 'a, l2:list 'a, l:list 'a. (l1 ++ l) = (l2 ++ l) -> l1 = l2
```
It was impossible to make a recursion on ``l1``.
This issue should also investigate what changed in induction_ty_lex between 0.88 and 1.00 (on this same goal): apparently, the transformation is less clever.This is to investigate the behavior of induction_ty_arg_lex that apparently does not do induction on the right elements.
It was reported by users that on this:
```
goal list_simpl_r :
forall l1:list 'a, l2:list 'a, l:list 'a. (l1 ++ l) = (l2 ++ l) -> l1 = l2
```
It was impossible to make a recursion on ``l1``.
This issue should also investigate what changed in induction_ty_lex between 0.88 and 1.00 (on this same goal): apparently, the transformation is less clever.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/269transformation replace should replace also under the conditions of `if`2019-02-12T12:55:05ZMARCHE Claudetransformation replace should replace also under the conditions of `if`Apparently `replace` does traverse the conditions of `if` termsApparently `replace` does traverse the conditions of `if` terms1.3.0DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/264destruct improvement with if then else2019-02-08T13:47:07ZDAILLER Sylvaindestruct improvement with if then elseThis issue to keep track of a suggestion by @bbecker to extend destruct to "if .. then .. else":
```
axiom H: if c1 then c2 else c3
```
destruct H would create two branches: one replacing `H` by `c1 `and `c2` and the other one replacing it with `~c1` and `c3`.
Note: Similar behavior can be done for `match`.This issue to keep track of a suggestion by @bbecker to extend destruct to "if .. then .. else":
```
axiom H: if c1 then c2 else c3
```
destruct H would create two branches: one replacing `H` by `c1 `and `c2` and the other one replacing it with `~c1` and `c3`.
Note: Similar behavior can be done for `match`.Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/263Removing Inline_trivial2019-02-12T16:55:13ZDAILLER SylvainRemoving Inline_trivialHello,
I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes `cvc4 1.5` fail on some files (`bench/ce/array_mono.mlw`).
Am I misunderstanding the use of this transformation ? I think there may be a bug in the rest of the transformations used for CVC4 if not.Hello,
I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes `cvc4 1.5` fail on some files (`bench/ce/array_mono.mlw`).
Am I misunderstanding the use of this transformation ? I think there may be a bug in the rest of the transformations used for CVC4 if not.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/259improve destruct_alg2019-01-31T16:26:45ZMARCHE Claudeimprove destruct_algFeature wishes for improvements:
* allow user to provide the introduced names, e.g `destruct_alg t as x1,x2`
* rename it into something better, e.g. `destruct_term`.Feature wishes for improvements:
* allow user to provide the introduced names, e.g `destruct_alg t as x1,x2`
* rename it into something better, e.g. `destruct_term`.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/238Improve case transformation2019-06-18T07:58:40ZDAILLER SylvainImprove case transformationIt is my feeling that VC generation/split often produces hypotheses containing implications with the same premises (or its negation) such as:
```
H: P -> A
H1: not P -> B
H2: P -> C
```
On these cases, I think the user would like `case P` to remove unsatisfiable hypothesis and premises. This would give two new context:
```
H: A
H2: C
H3: P
```
and
```
H1: B
H: not P
```It is my feeling that VC generation/split often produces hypotheses containing implications with the same premises (or its negation) such as:
```
H: P -> A
H1: not P -> B
H2: P -> C
```
On these cases, I think the user would like `case P` to remove unsatisfiable hypothesis and premises. This would give two new context:
```
H: A
H2: C
H3: P
```
and
```
H1: B
H: not P
```DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/235Avoid substituting to proxy symbols2018-11-16T09:02:53ZDAILLER SylvainAvoid substituting to proxy symbolsWhen using `subst_all` or `split_vc`, it is not rare to substitute variables to a proxy symbol:
```
H : r = (o [@mlw_proxy_symbol])
Goal : r + r = 5
```
With `subst_all` or `split_vc` would become:
`Goal: o + o = 5`
I think it is better to do the substitution from the other side.When using `subst_all` or `split_vc`, it is not rare to substitute variables to a proxy symbol:
```
H : r = (o [@mlw_proxy_symbol])
Goal : r + r = 5
```
With `subst_all` or `split_vc` would become:
`Goal: o + o = 5`
I think it is better to do the substitution from the other side.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/233Improve apply2018-11-07T10:08:46ZDAILLER SylvainImprove applyIn some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp H1`
To be investigated.In some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp H1`
To be investigated.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/232instantiate should be able to remove the general hypothesis2019-09-24T10:34:43ZDAILLER Sylvaininstantiate should be able to remove the general hypothesisAdd an optional argument so that on hypothesis:
`H : forall x. x = 0`
`instantiate H 1` generate the following hypotheses (name change and remove hypothesis):
`H : 1 = 0`
instead of
```
H : forall x. x = 0
H_inst : 1 = 0
```Add an optional argument so that on hypothesis:
`H : forall x. x = 0`
`instantiate H 1` generate the following hypotheses (name change and remove hypothesis):
`H : 1 = 0`
instead of
```
H : forall x. x = 0
H_inst : 1 = 0
```DAILLER SylvainDAILLER Sylvain