why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-02-21T15:47:07+01:00https://gitlab.inria.fr/why3/why3/-/issues/623Check counterexamples classification benchmark2023-02-21T15:47:07+01:00MOREAU SoleneCheck counterexamples classification benchmarkThis is the list of example files for the classification of counterexamples using the giant-step approach, located in the folder `bench/check-ce` and listed in alphabetical order. For each file, we need to check that the counterexamples ...This is the list of example files for the classification of counterexamples using the giant-step approach, located in the folder `bench/check-ce` and listed in alphabetical order. For each file, we need to check that the counterexamples returned by the provers and their classification are correct.
See also [ce-stats.py](https://gitlab.inria.fr/why3/why3/-/blob/master/bench/ce-stats.py) to compute statistics about the bench for checking CE.
| test | CE classification | related issues |
| ---- | ----------------- | -------------- |
| 614.mlw | | |
| 615.mlw | | |
| 640_no_loc_failure.mlw | | |
| 657.mlw | | #657 |
| 668_projection.mlw | | |
| 703_reduce_term.mlw | INCOMPLETE cannot decide | |
| algebraic_types_mono.mlw | | #640 |
| algebraic_types_poly.mlw | | |
| anonymous1.mlw | | |
| anonymous2.mlw | | |
| anonymous3.mlw | | |
| anonymous4.mlw | | |
| anonymous5.mlw | INCOMPLETE many args for exec + cannot decide | |
| anonymous6.mlw | | |
| anonymous6_mono.mlw | | |
| array_mono.mlw | INCOMPLETE cannot decide | |
| array_poly.mlw | INCOMPLETE uncaught exception (Cannot instantiate a defined symbol sorted_sub) | |
| array_records_mono.mlw | INCOMPLETE cannot decide (only z3 prover) | |
| array_records_poly.mlw | INCOMPLETE cannot decide | polymorphism |
| attributes.mlw | | |
| attributes_mono.mlw | | |
| blackbox.mlw | | |
| bv32.mlw | INCOMPLETE cannot decide (only z3 prover) | #352 |
| bv32_mono.mlw | | |
| bv32_toBig.mlw | | #657 |
| call-val-function.mlw | | #734 |
| double_projection.mlw | | |
| falseCE.mlw | | |
| fide21.mlw | | |
| floats.mlw | INCOMPLETE cannot decide | !311 #640 |
| for.mlw | | |
| for_mono.mlw | | |
| for1.mlw | | |
| for1_mono.mlw | | |
| func_call1.mlw | | |
| func_call1_mono.mlw | | |
| func_call2.mlw | | |
| func_call3.mlw | | |
| func_call4.mlw | | |
| func_call4_mono.mlw | | |
| func_call5.mlw | INCOMPLETE missing return value | |
| func_call6.mlw | | |
| func_call6_mono.mlw | | |
| func_call.mlw | | |
| func_call_mono.mlw | | |
| global_logic_constant.mlw | | |
| if_assign.mlw | | #353 |
| if_decision_branch.mlw | | |
| int32.mlw | | |
| int32_mono.mlw | | |
| integers.mlw | | #640 #705 |
| int_overflow.mlw | INCOMPLETE cannot decide | special case with div by 0 |
| jlamp_array_mono.mlw | INCOMPLETE cannot decide |
| jlamp_array_poly.mlw | INCOMPLETE cannot decide | polymorphism |
| jlamp_projections.mlw | | #351 |
| jlamp0_mono.mlw | | |
| jlamp0_poly.mlw | | #348 |
| let_constant.mlw | | |
| let_function_logic.mlw | | #734 |
| let_function.mlw | | |
| lists.mlw | |
| logic_constant.mlw | | |
| logic_function.mlw | | |
| loop_ce.mlw | | |
| loop_ce_mono.mlw | | |
| loop_inv_int.mlw | | |
| loop_inv_int_mono.mlw | | |
| loop_inv_real.mlw | INCOMPLETE cannot decide | polymorphism |
| loop_inv_real_mono.mlw | INCOMPLETE cannot decide | |
| manual_map.mlw | | |
| maps_mono.mlw | | |
| maps_poly.mlw | INCOMPLETE cannot import | #354 #640 polymorphism |
| multifile1.mlw | | |
| multifile2.mlw | | |
| polymorphism.mlw | | |
| range_type_float.mlw | | |
| range_type_int.mlw | | |
| real_values.mlw | INCOMPLETE cannot decide | |
| record_map.mlw | INCOMPLETE undefined argument + cannot decide | #359 |
| record_nested_one_field.mlw | | |
| records_inv.mlw | | |
| records_label.mlw | | TO DISCUSS (#355?) |
| recursive_model.mlw | | #640 |
| ref1.mlw | | |
| ref1_mono.mlw | | |
| ref2.mlw | | |
| ref2_mono.mlw | | |
| ref_ex.mlw | | TO DISCUSS (in postcondition of `incr`, `!y` is interpreted as `old y`?) + see #355 |
| ref_ex_mono.mlw | | |
| ref_mono.mlw | | TO DISCUSS (in postcondition of `incr`, `!y` is interpreted as `old y`) + see #355 |
| result.mlw | | #353 |
| return_value_below_if_when_vc_sp.mlw | | |
| simple_array.mlw | INCOMPLETE cannot decide (only z3 prover) | #640 |
| strings.mlw | INCOMPLETE cannot decide | #640 + TO DISCUSS (values of strings seem strange?) |
| test_result_ce_value0.mlw | | |
| test_result_ce_value1.mlw | | |
| test_result_ce_value2.mlw | | |
| threshold.mlw | | |
| tuple1.mlw | INCOMPLETE missing return value (only z3 prover) | |
| tuple.mlw | | |
| underspec.mlw | | |
| val_function.mlw | INCOMPLETE cannot decide | #734 |
| var_clones.mlw | | |
| while1.mlw | | |
| while1_mono.mlw | | |
| while.mlw | | |
| while_mono.mlw | | |
Additional files in `bench/check-ce/petiot2018`.
| test | CE classification | related issues |
| ---- | ----------------- | -------------- |
| binary_search.mlw | | |
| isqrt.mlw | | |
| rgf.mlw | | |https://gitlab.inria.fr/why3/why3/-/issues/622Improve IDE for counterexamples2023-02-21T15:42:21+01:00MOREAU SoleneImprove IDE for counterexamples- [ ] Add a boolean in proofattempt result to indicate if counterexamples can be launched on proofattempt
- [ ] Change the status image in the ide to show that counterexamples can be queried- [ ] Add a boolean in proofattempt result to indicate if counterexamples can be launched on proofattempt
- [ ] Change the status image in the ide to show that counterexamples can be queriedhttps://gitlab.inria.fr/why3/why3/-/issues/616Extend Ptree helpers2023-09-06T13:47:12+02:00MARCHE ClaudeExtend Ptree helpersThere is a need to extend Ptree helpers. This meta-issue records a list of corresponding wishes
- [ ] allows specifying a diverging program. Either gives a Boolean option to `begin_let` or
an additional function to set the spec of the ...There is a need to extend Ptree helpers. This meta-issue records a list of corresponding wishes
- [ ] allows specifying a diverging program. Either gives a Boolean option to `begin_let` or
an additional function to set the spec of the function in question
- [ ] give a way to add global variable (thus hiding the Eany that is needed for that)
- [ ] provide a function to add a `writes` clause in a contract1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/608add a notion of label in MLCFG2022-01-05T15:58:02+01:00MARCHE Claudeadd a notion of label in MLCFGMLCFG should provide a notion of label without a scope, e.g.
```
let cfg f (...) =
var x : int;
{
label L;
goto B
B {
assert { x = (x at L) };
}
```
The translation by computation of dominators should support that, but not the general ...MLCFG should provide a notion of label without a scope, e.g.
```
let cfg f (...) =
var x : int;
{
label L;
goto B
B {
assert { x = (x at L) };
}
```
The translation by computation of dominators should support that, but not the general one with mutually recursive functions. Hence such labels would not be supported when the code is not well-structured enough.Xavier DenisXavier Denishttps://gitlab.inria.fr/why3/why3/-/issues/599Usage of `Map.const` triggers polymorphism2023-11-13T14:55:16+01:00MARCHE ClaudeUsage of `Map.const` triggers polymorphismThe SMT-LIB driver allows one to use higher-order and `map.Map`, both of them being mapped to SMT-LIB expressions without polymorphism.
It would be better to also map the `map.Const.const` to something not requiring the encoding of poly...The SMT-LIB driver allows one to use higher-order and `map.Map`, both of them being mapped to SMT-LIB expressions without polymorphism.
It would be better to also map the `map.Const.const` to something not requiring the encoding of polymorphism. Note that writing `(fun _ -> c)` instead of `const c` does *not* trigger encoding, so it must be doable.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/591Misleading "unbound function" error message2021-09-27T14:23:59+02:00Xavier DenisMisleading "unbound function" error messageI was recently caught by the error message:
`unbound function or predicate symbol 'UInt64.of_int'`
It took me a second to realize that the reason was being raised was that `of_int` is a `val` and not a `function` or `predicate`. I feel...I was recently caught by the error message:
`unbound function or predicate symbol 'UInt64.of_int'`
It took me a second to realize that the reason was being raised was that `of_int` is a `val` and not a `function` or `predicate`. I feel like the message could be improved when a program symbol with the same name appears, something like:
```
unbound function or predicate symbol 'UInt64.of_int', but a program symbol with the same name was found
```
Even this marginal improvement would make the error much more clear (imo).https://gitlab.inria.fr/why3/why3/-/issues/588Coercion with type variables2021-09-09T14:34:28+02:00François BobotCoercion with type variablesIt is currently not possible to add the following coercion
```
type t 'a = {
t_a : 'a;
}
meta coercion function t_a
```
Currently only from one type constructor to another is allowed. It seems that allows to compute the transitive c...It is currently not possible to add the following coercion
```
type t 'a = {
t_a : 'a;
}
meta coercion function t_a
```
Currently only from one type constructor to another is allowed. It seems that allows to compute the transitive closure when inserting new coercion and not during type checking. What would be the complexity to add that? Does it become similar to type-class inference?
EDIT: It could also help if one could define
```
function t_a_foo: (x:t foo) : foo = x.t_a
meta coercion function t_a_foo
function t_a_bar: (x:t bar) : bar = x.t_a
meta coercion function t_a_bar
```https://gitlab.inria.fr/why3/why3/-/issues/585New function for conversion from real to float2023-11-13T14:56:16+01:00Guillaume CluzelNew function for conversion from real to floatIt would be useful to have in the `ieee_float.Float_Gen` theory a function `of_real mode real : t` that correctly rounds a real to a float `t` according to the rounding mode given.It would be useful to have in the `ieee_float.Float_Gen` theory a function `of_real mode real : t` that correctly rounds a real to a float `t` according to the rounding mode given.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/581Mlw printer incorrect for Eoptexn2023-09-06T13:47:31+02:00MARCHE ClaudeMlw printer incorrect for EoptexnThe `Eoptexn` constructor of `Ptree.expr` is for special local exceptions involved in `break`, `continue` and `return`.
Since there is no concrete syntax for those, they should be printed as
declaration of a local exception with an exp...The `Eoptexn` constructor of `Ptree.expr` is for special local exceptions involved in `break`, `continue` and `return`.
Since there is no concrete syntax for those, they should be printed as
declaration of a local exception with an explicit `try ... with ... -> () end` around. The current printing is not parseable.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/579Extend sets with filter and cartesian product2021-06-27T18:44:04+02:00Quentin GarcheryExtend sets with filter and cartesian productLooking at the modules inside `set.mlw`, I'm wondering whether or not it is possible to extend some of them.
For the `filter` function defined in module `Fset`, can we also have it in `SetApp` ?
What about `Set` ? I understand that thes...Looking at the modules inside `set.mlw`, I'm wondering whether or not it is possible to extend some of them.
For the `filter` function defined in module `Fset`, can we also have it in `SetApp` ?
What about `Set` ? I understand that these are potentially infinite sets, is it an issue ?
Another operator on sets that I think would be nice to have is the cartesian product.
For the finite sets, this can be added by:
```
let rec ghost function cartesian_product (s1 : fset 'a) (s2 : fset 'b)
variant { cardinal s1 }
ensures { forall x y. mem (x, y) result <-> mem x s1 /\ mem y s2 }
=
if is_empty s1 then empty
else let x1 = pick s1 in
union (map (fun y -> (x1, y)) s2)
(cartesian_product (remove x1 s1) s2)
```
Could we also add a cartesian product for all kinds of sets ?Quentin GarcheryQuentin Garcheryhttps://gitlab.inria.fr/why3/why3/-/issues/574Record transformation time2021-05-05T18:01:13+02:00Quentin 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 `why3ses...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/573Opening scopes at top level2021-04-30T10:06:00+02:00Xavier DenisOpening scopes at top levelWhen targetting WhyML from other languages, we would like to use `scopes` to help manage the namespaces for the produced code. In particular, it is desirable to produce a forest of nested scopes which contain modules or other declaration...When targetting WhyML from other languages, we would like to use `scopes` to help manage the namespaces for the produced code. In particular, it is desirable to produce a forest of nested scopes which contain modules or other declarations at the leaves. Currently, this is not possible as `module`s must be the top-level constructs of a WhyML file (implicit or explicit).
This restriction which prevents scopes from being at the top-level and thus containing modules seems unnecessary.
As a concrete example of what I would like to do:
```
scope MyScope
module Mod1
type t
end
scope OtherScope
(* optional, allow implicit modules inside scopes *)
let x () : bool = body
end
end
```
This code currently raises an error stating "Trying to open a module inside a module" due to the _implicit_ module opened by Why3.https://gitlab.inria.fr/why3/why3/-/issues/570Functions that could be used as let-functions2021-04-16T11:35:50+02:00Loïc CorrensonFunctions that could be used as let-functions:warning: **Disclaimer** this report is _wrong_ : a let-function without a contract actually exposes its definition to callers.
**Original Report** (wrong)
A frequent pattern we face when writing why3 code for extraction, is a pure lo...:warning: **Disclaimer** this report is _wrong_ : a let-function without a contract actually exposes its definition to callers.
**Original Report** (wrong)
A frequent pattern we face when writing why3 code for extraction, is a pure logical function that _only makes use of extractible expressions_. We then have to write the following code, with full duplication of core function definition:
```
function f x… : r = e
let rec function f x… : r ensures { result = e } = e
```
For large definition `e` with pattern matching or mutual-recursion, this is annoying !
This is the dual situation of a `let function f … = e`, where `f` can be used in both code & logic except that (among others):
1. the definition `e` of `let function f … = e` is _not_ available to provers
2. when writing `function f … = e` there is _no_ preconditions to `f`, hence `f x = e` always holds
3. pure logic function `f` must be structurally recursive so `let function f` needs no variant
**Proposal:**
Add a keyword to `function` definitions in order to have the associated `let rec function ...` for free.
Alternatively, detect that function definition only contains extractible terms and allow to use it like a `let function` in code.https://gitlab.inria.fr/why3/why3/-/issues/569Use lemma function like « by » operator2021-04-09T08:37:35+02:00Loïc CorrensonUse lemma function like « by » operatorIn addition to #547, it would be very useful to call a lemma function for writing a formula (_aka_, its ensures) along with its proof (_aka_, its requires).
Hence, the semantics of `f a…` where `f` is a lemma function would be similar t...In addition to #547, it would be very useful to call a lemma function for writing a formula (_aka_, its ensures) along with its proof (_aka_, its requires).
Hence, the semantics of `f a…` where `f` is a lemma function would be similar to `(E a…) by (R a…)`, where `E` and `R` are the ensures & requires of `f`, although there is no need for side condition `(R a… -> E a…)` since the lemma has been already established.
The manual description would be (Cf. § 7.3.4):
« An occurrence of `f a...` where `f` is a lemma function generates no side condition, since the lemma has already been established. When `f a...` occurs as a premise, it is reduced to the conjunction of `E a...` for all ensures `E` of `f` (the conclusion of the lemma are exhibited). When `f a...` occurs as a goal, it is reduced to the conjunction of `R a...` (the premisses of the lemma are verified). »https://gitlab.inria.fr/why3/why3/-/issues/568unused variables2021-04-01T13:44:23+02:00Jean-Christophe Filliâtreunused variablesWhen function parameters are not used in spec/code, Why3 emits a warning, which is useful.
But it does not for unused variables in the function result.
For instance
```
val f (x: int) : (y:int, z: int)
ensures { true }
```
emits a warn...When function parameters are not used in spec/code, Why3 emits a warning, which is useful.
But it does not for unused variables in the function result.
For instance
```
val f (x: int) : (y:int, z: int)
ensures { true }
```
emits a warning about `x` being unused, but does not complain about `y` and `z` being ununsed.https://gitlab.inria.fr/why3/why3/-/issues/567wish: provide monomorphic, clonable modules for references and arrays2024-02-13T17:09:15+01:00MARCHE 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 counterexa...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`https://gitlab.inria.fr/why3/why3/-/issues/557Build a glossary of error messages2022-11-04T16:33:12+01:00MARCHE 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 a...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/552RFC: binders for tuple components in function prototype2021-02-11T10:43:19+01:00Jean-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 ...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/547Syntactic sugar for lemma functions2021-04-09T08:27:17+02:00Loï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...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-11T10:35:12+01:00Loï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 ...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.