why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-09-06T13:46:11+02:00https://gitlab.inria.fr/why3/why3/-/issues/720Support for ADT in Alt-Ergo2023-09-06T13:46:11+02:00BONNOT PaulSupport for ADT in Alt-ErgoNow that Alt-ergo supports ADTs, it is needed to modify the driver and the printer to use this feature.Now that Alt-ergo supports ADTs, it is needed to modify the driver and the printer to use this feature.1.8.0BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/719`Split_vc` takes a lot of time when used in huge context2023-11-13T14:55:01+01:00François Bobot`Split_vc` takes a lot of time when used in huge context`Split_vc` uses substitution which have a bad behavior with huge context.
```
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered ~subst_proxy:false subst_filter)
let split_vc =
Trans.compo...`Split_vc` uses substitution which have a bad behavior with huge context.
```
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered ~subst_proxy:false subst_filter)
let split_vc =
Trans.compose_l
(*** do test:
(Trans.compose Simplify_formula.simplify_trivial_wp_quantification
*)
(Trans.compose generalize_intro Split_goal.split_goal_right)
(Trans.singleton simplify_intros)
```
We are trying to create a toy example, but in any case it seems strange that `split_vc` looks at all the task. What is the goal os this substitution?
The lot of time is that a reload in the IDE can take 14min.1.8.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/716micro-Python: add slice assignment2023-07-17T15:44:03+02:00Jean-Christophe Filliâtremicro-Python: add slice assignmentAdd support for slice assignment, that is,
```
e1[e2:e3] = e4
```Add support for slice assignment, that is,
```
e1[e2:e3] = e4
```Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/715improve transformation used by dreal driver2023-09-06T13:46:27+02:00MARCHE Claudeimprove transformation used by dreal driverThe driver for dreal uses a dedicated transformation `keep_only_arithmetic`. The code for this transformation could be made more elegant, more compact, and could support more cases.
For example, this transformation would completely remo...The driver for dreal uses a dedicated transformation `keep_only_arithmetic`. The code for this transformation could be made more elegant, more compact, and could support more cases.
For example, this transformation would completely remove an hypothesis of the form
```
H: not (arith_fact \/ non_arith_fact)
```
whereas it could keep
```
H: not arith_fact
```BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/714recursive logical definitions in micro-Python2022-11-17T15:40:41+01:00Jean-Christophe Filliâtrerecursive logical definitions in micro-PythonCurrently, there is no support for recursive logical functions and predicates in micro-Python,
though a syntax for variants is provided.
An example would be
```
#@ function factorial(n: int) -> int variant { n } = if n <= 1 then 1 else ...Currently, there is no support for recursive logical functions and predicates in micro-Python,
though a syntax for variants is provided.
An example would be
```
#@ function factorial(n: int) -> int variant { n } = if n <= 1 then 1 else n*factorial(n-1)
```Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/711Recursion under quantifier inside of `let function`2022-11-16T13:41:38+01:00Xavier DenisRecursion under quantifier inside of `let function`I know that we discussed this back in october, but I cannot find any trace of our discussions.
Currently if you define a `let rec function` and perform a recursive call under a quantifier, you get an `unbound predicate or function` err...I know that we discussed this back in october, but I cannot find any trace of our discussions.
Currently if you define a `let rec function` and perform a recursive call under a quantifier, you get an `unbound predicate or function` error for namespace reasons.
We had discussed several solutions, but I forget what the tradeoffs were.
cc @x-DEwert who independently stumbled on this.https://gitlab.inria.fr/why3/why3/-/issues/710Rose Tree Mutual Recursion Termination2022-11-14T20:59:54+01:00David EwertRose Tree Mutual Recursion TerminationWhen trying implement a [Rose Tree](https://en.wikipedia.org/wiki/Rose_tree) type data structure:
```
type node 't =
| Leaf 't
| Internal (List.list Int.int) (Seq.seq (node 't))
```
gives the error "Constructor Internal2 contains...When trying implement a [Rose Tree](https://en.wikipedia.org/wiki/Rose_tree) type data structure:
```
type node 't =
| Leaf 't
| Internal (List.list Int.int) (Seq.seq (node 't))
```
gives the error "Constructor Internal2 contains a non strictly positive occurrence of type node2 't", which seems to be cause by `Seq.seq 't` being an opaque type which is assumed invariant over `'t`. I think it should be sound for `seq.Seq` to be covariant as it could be implemented with a `List.list 't` or a `(int, (int -> 't))` both of which are covariant.
Even if `Seq.seq` was covariant it would still be difficult/(maybe impossible) to prove termination for functions using this definition as Why3 functions don't seem to have a way of ensuring that there result is less than there input in the structural well founded order. For example:
```
type node 't =
| Leaf 't
| Internal (List.list (node 't))
let rec function node_sum (self : node Int.int) : Int.int =
match (self) with
| Leaf x -> x
| Internal nodes -> list_sum nodes
end
with function list_sum (nodes : List.list (node Int.int)) : Int.int =
match (nodes) with
| Nil -> 0
| Cons first rest -> (node_sum first) + (list_sum rest)
end
```
```
use list.Length
use list.Nth
use option.Option
type node 't =
| Leaf 't
| Internal (List.list (node 't))
let rec function node_last (self : node 't) : Option.option 't =
match (self) with
| Leaf x -> Option.Some x
| Internal nodes -> list_last nodes
end
with function list_last (nodes : List.list (node 't)) : Option.option 't =
match(Nth.nth ((Length.length nodes) - 1) nodes) with
| Option.Some x -> node_last x
| Option.None -> Option.None
end
```
in the first example Why3 is able prove termination, but the second example it isn't since `Nth.nth` isn't known to return a structural sub-part of the list.
This also makes it difficult to prove termination for map based rose-trees, eg. Why3 also can't prove termination for:
```
let rec function node_sum (self : node Int.int) : Int.int =
match (self) with
| Leaf x -> x
| Internal keys nodes -> list_sum keys nodes
end
with function list_sum (keys : List.list Int.int) (nodes : Map.map Int.int (node Int.int)) : Int.int =
match (keys) with
| Nil -> 0
| Cons first rest -> (node_sum (Map.get nodes first)) + (list_sum rest nodes)
end
```Xavier DenisXavier Denishttps://gitlab.inria.fr/why3/why3/-/issues/708Consider not removing all props in `smt-lib-floats.gen`2022-11-16T13:41:56+01:00MARCHE ClaudeConsider not removing all props in `smt-lib-floats.gen`Currently the `smt-lib-floats.gen` removes all props. Probably it aims at using exclusively the built-in support for floats in SMT solvers. Yet, there are properties that are removed that are not known by solvers, so it might be better t...Currently the `smt-lib-floats.gen` removes all props. Probably it aims at using exclusively the built-in support for floats in SMT solvers. Yet, there are properties that are removed that are not known by solvers, so it might be better to remove less props.
An example are the lemma `max_int_def` and `max_real_def` which are removed, thus the counterexample exhibit values 0 and 0.0 for them, which is clearly incorrect.https://gitlab.inria.fr/why3/why3/-/issues/707Consider making the FPA alternative of Alt-Ergo the default2022-11-16T13:29:47+01:00MARCHE ClaudeConsider making the FPA alternative of Alt-Ergo the defaultA recent commit added the alternative FPA to Alt-Ergo, supporting dedicated reasoning on real numbers and floats.
It should be investigated if it could be made the default, in other words if the FPA does not prevent other proofs.A recent commit added the alternative FPA to Alt-Ergo, supporting dedicated reasoning on real numbers and floats.
It should be investigated if it could be made the default, in other words if the FPA does not prevent other proofs.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/706Issues with error locations2023-01-11T13:58:50+01:00Guillaume MelquiondIssues with error locationsPrompted by !760, I have tried to understand better how tools are supposed to report error locations.
Here are Emacs' expectations:
1. The first character of a line is at position 1 (even if Emacs itself counts column starting from zer...Prompted by !760, I have tried to understand better how tools are supposed to report error locations.
Here are Emacs' expectations:
1. The first character of a line is at position 1 (even if Emacs itself counts column starting from zero). A buffer setting makes it so that they are at position 0.
2. Tabulation characters count for as many positions as needed to reach the next multiple of eight. A buffer setting makes it so that they count for one.
3. Unicode characters count for one position.
Here are Vim's expectations:
1. The first character of a line is at position 1.
2. Tabulation characters count either for one position, or for as many positions as needed to reach the next multiple of eight, depending on the error format.
3. Unicode characters count for one position.
Here are Gedit's expectations (`+l:c` on command line):
1. The first character of a line is at position 1.
2. Tabulations characters count for one position.
3. Unicode characters count for one position.
Here are Why3 IDE's current expectations:
1. The first character of a line is at position 0. (Trivial to change.)
2. Tabulations characters count for one. (Moderately easy to change.)
3. Unicode characters count for one position. (Almost impossible to change.)
Here is a small example that exhibits the three cases:
```
let f ()
ensures { result = 0 }
(* next is a tab *) ensures { result = 0 }
(* éééé *) ensures { [@ ééé ] result = 0 }
= 0
```
Just select the goal in the IDE and see whether the postconditions are correctly highlighted. If you want to experiment with error messages instead, just change `result` into `risult`.
As it stands (!763, !766), Why3 accommodates these expectations as follows:
1. Not satisfied for Vim (and Gedit, but that is less relevant).
2. Satisfied.
3. Almost satisfied, e.g., in the absence of combining marks.
For completeness, here is GCC's behavior:
1. The first character of a line is at position 1.
2. Tabulation characters count for as many positions as needed to reach the next multiple of eight.
3. Unicode characters count for one.
Here is Clang's behavior:
1. The first character of a line is at position 1.
2. Tabulation characters count for one position for column. They count for multiple positions for caret.
3. Unicode characters count for their number of bytes for column. They count for one position for caret.
Here is OCaml's behavior:
1. The first character of a line is at position 0.
2. Tabulation characters count for one. (Hence a broken caret.)
3. Unicode characters count for their number of bytes. (Hence a broken caret.)
Here is the LSP protocol's specification:
1. The first character of a line is at position 0.
2. Tabulation characters count for one.
3. Unicode characters count for the number of words needed to represent them in UTF-16. (Since May 2022, client and server can negotiate to count in bytes or in unicode.)https://gitlab.inria.fr/why3/why3/-/issues/704Soundness issue with Colibri2 prover2023-09-29T10:11:04+02:00BONNOT PaulSoundness issue with Colibri2 proverTest Why3 support for new versions of the [Colibri2](https://colibri.frama-c.com/) prover and add tests.Test Why3 support for new versions of the [Colibri2](https://colibri.frama-c.com/) prover and add tests.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/701Failure in why3_open when using Isabelle2022-10-17T14:52:01+02:00Guillaume MelquiondFailure in why3_open when using IsabelleReported by Grzegorz Fabiański: "In the code attached below, the filterExtendesSpec vc extracts correctly in the Isabelle, although using Isabelle on any goal after it results in an error on Isabelle's side during "why3_open"."
```whyml...Reported by Grzegorz Fabiański: "In the code attached below, the filterExtendesSpec vc extracts correctly in the Isabelle, although using Isabelle on any goal after it results in an error on Isabelle's side during "why3_open"."
```whyml
module BugInIsabelleExtraction
use list.List
use list.NumOcc
let rec function filter (p : 'a -> bool) (l : list 'a) : list 'a =
match l with
| Nil -> Nil
| Cons hd tl ->
let filteredRest = filter p tl in
if p hd then
Cons hd filteredRest
else
filteredRest
end
(*vc's of this are extracted correctly *)
let rec lemma filterExtendesSpec (x : 'a) (p : 'a -> bool) (l : list 'a) =
variant {l }
ensures { p x -> num_occ x (filter p l) = num_occ x l }
ensures { not p x -> num_occ x (filter p l) = 0 }
match l with
| Nil -> ()
| Cons hd tl ->
filterExtendesSpec x p tl
end
(* but any goal after this fail "why3_open" in Isabelle, even the simplest ones *)
goal test : 4=4
end
```https://gitlab.inria.fr/why3/why3/-/issues/693Location warning due to overly long argument due to proof bisection2022-10-03T10:23:29+02:00Guillaume MelquiondLocation warning due to overly long argument due to proof bisectionProof bisection introduces a "remove" transformation in the proof session. It has an argument that lists all the useless symbols. This list can contain hundreds of symbols and thus exceeds 4096 characters. In turn, this causes Why3 to sp...Proof bisection introduces a "remove" transformation in the proof session. It has an argument that lists all the useless symbols. This list can contain hundreds of symbols and thus exceeds 4096 characters. In turn, this causes Why3 to spew warnings in the IDE or when replaying sessions, e.g.,
```console
$ bin/why3 replay --merging-only -L examples/multiprecision/ examples/multiprecision/mpz_set_str
Warning: Loc.user_position: end char number `4098` overflows on next line
```
We should not warn about things that are out of the control of the user.https://gitlab.inria.fr/why3/why3/-/issues/692rac prover should be executed on a task before transformation compute2023-07-17T15:48:23+02:00MARCHE Clauderac prover should be executed on a task before transformation computeThe RAC prover is executed on the task obtained after `compute_in_goal`, this is not good since for example definition like `BV32.sle` are expanded, whereas the prover has a mapping for it in the driverThe RAC prover is executed on the task obtained after `compute_in_goal`, this is not good since for example definition like `BV32.sle` are expanded, whereas the prover has a mapping for it in the driverMARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/687Map the library of sequences of Why3 to the SMTLIB theory of sequences2023-07-17T15:49:31+02:00MARCHE ClaudeMap the library of sequences of Why3 to the SMTLIB theory of sequencesThis mapping should follow the same guidelines as the mapping for functional mappings, or for bitvectors, or for character strings.
Caution must be taken for functions which are declared total in SMTLIB: the one for extracting a sub-seq...This mapping should follow the same guidelines as the mapping for functional mappings, or for bitvectors, or for character strings.
Caution must be taken for functions which are declared total in SMTLIB: the one for extracting a sub-sequence returns the empty sequence when the parameters are out of bounds, and the one for updating, which returns the sequence unchanged when out-of-bounds.Jacques-Henri JourdanJacques-Henri Jourdanhttps://gitlab.inria.fr/why3/why3/-/issues/685Automatically add triggers to function definition/specification axioms2022-11-16T13:42:40+01:00David EwertAutomatically add triggers to function definition/specification axiomsI think it would be helpful to add triggers to the definitions/specifications of functions/predicates (possibly via a transformation or meta/attribute). One possible strategy would be:
For non-recursive functions/predicates: add `resul...I think it would be helpful to add triggers to the definitions/specifications of functions/predicates (possibly via a transformation or meta/attribute). One possible strategy would be:
For non-recursive functions/predicates: add `result`/(the function being defined) as the trigger for both the definition and specification axioms.
```ocaml
module Add1
use int.Int
let function add1 (arg: int) : int
ensures { result > arg }
=
arg + 1
goal test: add1 0 = 1
end
module Add1Trigger
use int.Int
function add1 (arg:int) : int
axiom add1_def : forall arg:int [add1 arg]. add1 arg = arg + 1
axiom add1_spec : forall arg:int [add1 arg]. add1 arg > arg
goal test: add1 0 = 1
end
```
For recursive functions/predicates: create a new "limited" function with the same arguments as the function being defined. Create a new axiom stating that it's equivalent to the original function. In the definition axiom replace that the recursive calls with the "limited" function and trigger on the original.
In the specification axiom using "limited" function in place of 'result' and as the trigger, ends up being slightly stronger as it means the prover can learn it even after unfolding the definition.
```ocaml
module Id
use int.Int
let rec function id (arg: int) : int
requires { arg >= 0}
variant {arg}
ensures { arg = 0 -> result = 0 }
=
if arg = 0 then 0 else id(arg - 1) + 1
goal test0: id 0 = 0
goal test1: id 1 = 1
goal test2: id 2 = 2
goal test20: id 20 = 20 (*Takes >5000 steps with Alt-ergo on https://why3.lri.fr/try/*)
end
module IdTrigger
use int.Int
function id_lim int : int
function id int : int
axiom id_def :
forall arg:int [id arg].
arg >= 0 ->
(if arg = 0 then id arg = 0 else id arg = (id_lim (arg - 1) + 1))
axiom id_spec : forall arg:int [id_lim arg]. arg >= 0 -> arg = 0 -> id_lim arg = 0
axiom id_lim_spec : forall arg:int [id arg]. id arg = id_lim arg
goal test0: id 0 = 0
goal test1: id 1 = 1 (*Succeeds only because we used the limited function in the spec axiom*)
goal test2: id 2 = 2 (*Fails*)
goal test20: id 20 = 20 (*Fails*)
end
```
One other issue I found is, when verifying and recursive item (function/predicate/lemma) which calls a recursive function/predicate under a quantifier in a post-condition (maybe also pre-condition), the task might fail even when it intuitively only requires a single unfolding. This is because the prover might use the not-"limited" in the trigger for the quantifier when expanding the recursive call, so the quantifier won't apply at all to the unfolded definition.
One solution would be to duplicate the post-condition, where the second version uses the "limited" function instead (in all places). A slight improvement would be to only modify the VC task and duplicate the post-condition in the assumption from the recursive call, the goal wouldn't need to be changed since the original version function can always be proved if the other one can. A similar trick could also be used for quantifiers in loop-invariants.
```ocaml
module IdLemma
use int.Int
use Id
let rec lemma idLemma(arg: int)
requires {arg >= 0}
variant {arg}
ensures {forall i:int. 0 <= i < arg -> id i = i}
= if arg <> 0 then idLemma (arg - 1)
end
module IdLemmaBroken
use int.Int
use IdTrigger
let rec lemma idLemma(arg: int)
requires {arg >= 0}
variant {arg}
ensures {forall i:int. 0 <= i < arg -> id i = i} (*Fails*)
= if arg <> 0 then idLemma (arg - 1)
end
module IdLemmaFix
use int.Int
use IdTrigger
let rec lemma idLemma(arg: int)
requires {arg >= 0}
variant {arg}
ensures {forall i:int. 0 <= i < arg -> id i = i}
ensures {forall i:int. 0 <= i < arg -> id_lim i = i}
= if arg <> 0 then idLemma (arg - 1)
end
module IdLemmaFix2
use int.Int
use IdTrigger
goal idLemma_vc :
forall arg:int.
arg >= 0 ->
(let (=)_result_unused_unused = (if arg = 0 then True else False) in
(not arg = 0 -> (let o = arg - 1 in (0 <= arg /\ o < arg) /\ o >= 0)) /\
(arg = 0 \/
(let o = arg - 1 in
(forall i:int. 0 <= i /\ i < o -> id i = i) /\
(forall i:int. 0 <= i /\ i < o -> id_lim i = i)) ->
(forall i:int. 0 <= i /\ i < arg -> id i = i)))
end
```https://gitlab.inria.fr/why3/why3/-/issues/684Python plugin: add extensional definition of lists in the logic2022-09-08T14:43:35+02:00Jean-Christophe FilliâtrePython plugin: add extensional definition of lists in the logicCurrently, the micro Python input format has syntax for extensional definition of lists in Python code (`[e1, e2, ..., en]`) but not in logical annotations.
In code, an extensional list `[e1, e2, ..., en]` is translated to WhyML as foll...Currently, the micro Python input format has syntax for extensional definition of lists in Python code (`[e1, e2, ..., en]`) but not in logical annotations.
In code, an extensional list `[e1, e2, ..., en]` is translated to WhyML as follows:
```
let s = make n e1 in
s[1] <- e2;
...
s[n-1] <- en;
s
```
This is related to having array/sequence literals in Why3.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.https://gitlab.inria.fr/why3/why3/-/issues/680Exploit the accessors for ADTs in SMTLIB2022-09-06T14:12:06+02:00MARCHE ClaudeExploit the accessors for ADTs in SMTLIBThe ADTs in SMTLIB allow the declaration of accessors. WhyML allows it too, with a syntax like
```
type list 'a = Nil | Cons (hd : 'a) (tl : list 'a)
```
The above is not accepted by Why3 though, because an accessor must occur in all con...The ADTs in SMTLIB allow the declaration of accessors. WhyML allows it too, with a syntax like
```
type list 'a = Nil | Cons (hd : 'a) (tl : list 'a)
```
The above is not accepted by Why3 though, because an accessor must occur in all constructor (i.e. with the same name and type).
Allowing partially defined accessors in WhyML would opne the possibility to exploit SMTLIB accessors as well.
The problem though is how to interpret accessors in solvers where they are not supported. A declaration like
```
function hd : list 'a -> 'a
axiom hd_spec : forall x y. hd (Cons x y) = x
```
seems dangerous because `hd Nil` may be interpreted differently by provers (clarification needed)https://gitlab.inria.fr/why3/why3/-/issues/677Cannot run eliminate_symbol after discriminate2022-11-16T13:34:19+01:00Xavier DenisCannot run eliminate_symbol after discriminateIm forwarding an issue from David Ewert which I received over mail:
> I have been trying to get Why3 to completely monomorphise all of the polymorphic logic functions and propositions, in order to avoid the "encoding_smt" transformation...Im forwarding an issue from David Ewert which I received over mail:
> I have been trying to get Why3 to completely monomorphise all of the polymorphic logic functions and propositions, in order to avoid the "encoding_smt" transformation. I've found that the "discriminate" transformation pretty much does what I want (especially when setting meta "select_inst_default" "all", meta "select_lskept_default" "all"). Unfortunately, it still keeps the polymorphic functions and propositions (which I don't want) after introducing the monomorphic ones. I also tried running "eliminate_symbol" after "discriminate" setting "ls:eliminate" for some of the sequence functions hoping this would eliminate the polymorphic versions, but this gave the error: "Failure in transformation eliminate_symbol Ident map is not yet declared". I think that it would be useful for Why3 to have a transformation that runs "discriminate" and then eliminates all polymorphic symbols or at least to allow "eliminate_symbol" to work after "discriminate" (although this seems like more of a hack)
**Note:** He is working with Creusot, so his immediate concern may be solved by !680, but this still seems like a valid bug report.