why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2020-10-28T14:11:17+01:00https://gitlab.inria.fr/why3/why3/-/issues/97range types should introduce an injectivity axiom2020-10-28T14:11:17+01:00MARCHE Clauderange types should introduce an injectivity axioma range type declaration
type t = range < a b >
generates a function `t'int` with an axiom
forall x:t. a <= t'int x <= b
but does NOT introduce any injectivity property such as
forall x y:t. t'int x = t'int y -> x = y (*...a range type declaration
type t = range < a b >
generates a function `t'int` with an axiom
forall x:t. a <= t'int x <= b
but does NOT introduce any injectivity property such as
forall x y:t. t'int x = t'int y -> x = y (*1*)
Note that the form (1) is not easy to handle by solver. A potential interesting variant
is introducing a reverse function
function t'ofInt int : t
with axiom
forall x:t. t'ofInt (t'int x) = x (*2*)
This variant has the advantage of avoiding a potential quadratic number of instanciations,
as it is the case for (1)https://gitlab.inria.fr/why3/why3/-/issues/193usage of array.Array should not enforce polymorphic VCs2021-02-11T10:42:47+01:00MARCHE Claudeusage of array.Array should not enforce polymorphic VCsIn Why3 0.88, for a program importing `array.Array` but wasn't using any other polymorphic types, the resulting tasks were not polymorphic and were consequently easier to discharge by SMT solvers.
Would it be possible to ignore the pol...In Why3 0.88, for a program importing `array.Array` but wasn't using any other polymorphic types, the resulting tasks were not polymorphic and were consequently easier to discharge by SMT solvers.
Would it be possible to ignore the polymorphism of the new array type in Why3 1.0 ?https://gitlab.inria.fr/why3/why3/-/issues/306Add program equality on Boolean type2023-08-28T16:11:06+02:00MARCHE ClaudeAdd program equality on Boolean typeTheory bool.Bool should provide (=) on Boolean type in programsTheory bool.Bool should provide (=) on Boolean type in programs1.8.0https://gitlab.inria.fr/why3/why3/-/issues/337Module `Cursor` should be documented2021-09-22T10:42:56+02:00MARCHE ClaudeModule `Cursor` should be documentedPlease add documentation as why3doc comments in `stdlib/cursor.mlw`Please add documentation as why3doc comments in `stdlib/cursor.mlw`PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/-/issues/500Simplify bitvector module `Bv`2023-09-06T13:47:44+02:00Benedikt BeckerSimplify bitvector module `Bv`The module `Bv` for bitvectors, specifically its axiomatization, should be simplified using recent features of Why3, see
https://gitlab.inria.fr/why3/why3/-/merge_requests/393#note_378246,
https://gitlab.inria.fr/why3/why3/-/merge_reque...The module `Bv` for bitvectors, specifically its axiomatization, should be simplified using recent features of Why3, see
https://gitlab.inria.fr/why3/why3/-/merge_requests/393#note_378246,
https://gitlab.inria.fr/why3/why3/-/merge_requests/393#note_3782471.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/504list functions to move from "function" to "let function"2020-10-23T17:17:08+02:00Jean-Christophe Filliâtrelist functions to move from "function" to "let function"Functions in modules `list.Map`, `list.FoldLeft`, and `list.FoldRight` are currently defined as `function` but could be `let function` (to be used in non-ghost programs).Functions in modules `list.Map`, `list.FoldLeft`, and `list.FoldRight` are currently defined as `function` but could be `let function` (to be used in non-ghost programs).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/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/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/637provide axioms for sdiv and smod in theory bitvector theory2023-09-06T13:47:01+02:00MARCHE Claudeprovide axioms for sdiv and smod in theory bitvector theorySuch axioms exist but are commented out. They should be uncommented and realizedSuch axioms exist but are commented out. They should be uncommented and realized1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/659The infix operators for reals are awkward2024-01-12T13:37:01+01:00Raphaël Rieu-HelftThe infix operators for reals are awkwardThe `real.Real` module defines infix binary operators on reals that have the same names as the integer ones. In case the user wishes to use both integer and real binary operators, `(+.)` and so on are defined in a second module `RealInfi...The `real.Real` module defines infix binary operators on reals that have the same names as the integer ones. In case the user wishes to use both integer and real binary operators, `(+.)` and so on are defined in a second module `RealInfix`. But I feel this introduces more issues than it solves. The lemmas in other real theories (such as `real.Square`, `real.PowerReal` and so on use the `real.Real` operators. But in most nontrivial programs, the user really will use both `Int` and `Real`, so their lemmas will use the `RealInfix` operators. This mismatch causes some lemma instantiation issues.
My impression is that few programs will manage to use `real.Real` operators (that is, not import int.Int at all or namespace it), and that we'd be better off always having points in the binary operators rather than having two separate sets of operators.https://gitlab.inria.fr/why3/why3/-/issues/669Wish: provide a better lemma for rounding error on add and sub for floats2022-11-16T13:33:29+01:00MARCHE ClaudeWish: provide a better lemma for rounding error on add and sub for floatsThe lemmas `round_bound` `ieee_float.Float32` and `ieee_float.Float64` are providing bounds on rounding arbitrary real number. Lemmas `round_bound_ne` are a bit more precise for the NE rounding mode.
Better lemmas should be provided in ...The lemmas `round_bound` `ieee_float.Float32` and `ieee_float.Float64` are providing bounds on rounding arbitrary real number. Lemmas `round_bound_ne` are a bit more precise for the NE rounding mode.
Better lemmas should be provided in the case the operand is the addition or subtraction of two floats. In such a case the `eta` constant, either `0x1p-149` for 32-bits or `0x1p-1074` for 64-bits, could be made equal to 0.
The proof is already present in Flocq so the realization of such addition lemmas should be easy.https://gitlab.inria.fr/why3/why3/-/issues/681Support unicode strings2022-11-16T13:33:44+01:00Xavier DenisSupport unicode stringsIt seems like the grammar of strings in Why3 is limited to ascii strings, but the corresponding SMT theory specifically supports unicode strings.
We don't even need to support parsing utf-8 strings so long as we allow longer escape seq...It seems like the grammar of strings in Why3 is limited to ascii strings, but the corresponding SMT theory specifically supports unicode strings.
We don't even need to support parsing utf-8 strings so long as we allow longer escape sequences for individual characters up to `0x2FFFF`. However, since currently `char` is mapped to OCaml's `char` type this introduces a conflict.