why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2020-06-23T18:50:33+02:00https://gitlab.inria.fr/why3/why3/-/issues/490Function symbol not found in a block of mutually recursive definitions2020-06-23T18:50:33+02:00Mário PereiraFunction symbol not found in a block of mutually recursive definitionsConsider the following example:
```
let rec function f (x: int)
ensures { result = g x }
=
g x
with function g (x: int) =
f x
```
Why3 complains with an unbound function error for the postcondition of `f`. Is this the expected beh...Consider the following example:
```
let rec function f (x: int)
ensures { result = g x }
=
g x
with function g (x: int) =
f x
```
Why3 complains with an unbound function error for the postcondition of `f`. Is this the expected behavior? Since `g` is defined using `with function`, I supposed it would be bound also for the contract of `f`.https://gitlab.inria.fr/why3/why3/-/issues/468Clone problem when type has nested regions2020-03-27T01:05:33+01:00Mário PereiraClone problem when type has nested regionsConsider the following example:
```
module A
use seq.Seq, int.Int
type t = private { ghost mutable view: seq int }
val set (a: t) : unit
writes { a.view }
end
module B
use array.Array, int.Int, seq.Seq
type t = {
...Consider the following example:
```
module A
use seq.Seq, int.Int
type t = private { ghost mutable view: seq int }
val set (a: t) : unit
writes { a.view }
end
module B
use array.Array, int.Int, seq.Seq
type t = {
mutable data: A.array int;
ghost mutable view: seq int;
}
let set (a: t) : unit
= a.data[0] <- 42; a.view <- empty
end
module C
use B
clone A with type t, val set
end
```
I get an
```
Illegal instantiation for program function set:
unreferenced write effects in variables: a
```
error message because of the `clone` in module `C`.
I believe this is due to the fact that I am changing the elements of `data`, hence touching the region of the array. In fact, if I change `data` directly
```
let set (a: t) : unit
= a.data <- make 0 42; a.view <- empty
```
Why3 is happy.
Apparently, the problem is being detected at line 1179 of `pmodule.ml`.
Given the recent updates on Why3 `clone` mechanism, am I missing something here? Is there a proper way to specify the effect of `set` in module `A` in order to to pass this `clone`, even when touching an inner region?
Note: this is a simplified example taken from the VOCaL library (cf, https://github.com/vocal-project/vocal/blob/master/vocal/proofs/why3/Vector_impl.mlw). Before merge request !347 we were able to clone function `set` as is.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/393type invariant preservation question2019-11-27T13:19:54+01:00DAILLER Sylvaintype invariant preservation questionI have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant t...I have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant to be ensured in the proof for `f`. Is there a way to tell the tool "at this point of program type invariants should hold" ?
```
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end
```https://gitlab.inria.fr/why3/why3/-/issues/348Location of `variant` clause2022-08-01T16:51:33+02:00DAILLER SylvainLocation of `variant` clauseThe location of `variant` clauses is at the enclosing loop. It should be at the clause itself (like invariants). In the example below, the loop variant should be at line 9 not 7.
```
use int.Int
predicate inv (x : int)
let p2 (ref c :...The location of `variant` clauses is at the enclosing loop. It should be at the clause itself (like invariants). In the example below, the loop variant should be at line 9 not 7.
```
use int.Int
predicate inv (x : int)
let p2 (ref c : int)
=
while c <= 10 do
invariant Ic { inv c }
variant { c }
c <- c + 2
done
```https://gitlab.inria.fr/why3/why3/-/issues/344Lost location for function argument2022-03-14T11:27:57+01:00DAILLER SylvainLost location for function argumentIn the following example:
```
type t = { mutable f : int }
let set (x : t) (v : int) ensures { x.f = v} =
x.f <- v
let g (a : t) =
set a 42;
assert { a.f = 43}
```
The following task is generated:
```
[...]
axiom H :
#"benc...In the following example:
```
type t = { mutable f : int }
let set (x : t) (v : int) ensures { x.f = v} =
x.f <- v
let g (a : t) =
set a 42;
assert { a.f = 43}
```
The following task is generated:
```
[...]
axiom H :
#"bench/ce/bug/../bug.mlw" 8 2 10#
(#"bench/ce/bug/../bug.mlw" 4 36 37# a)
= (#"bench/ce/bug/../bug.mlw" 8 8 10# 42)
[...]
```
The second location apparently refers to the declaration of field `f`. It should not appear here. Only the first location (on line 8), should be kept.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/307Add `(e at label)` as acceptable ghost code2019-04-20T14:02:23+02:00François BobotAdd `(e at label)` as acceptable ghost codeThe `at` construction could be generalized from logic expression to ghost code. It would remove some need of `let ghost` construction which have their own restriction.The `at` construction could be generalized from logic expression to ghost code. It would remove some need of `let ghost` construction which have their own restriction.https://gitlab.inria.fr/why3/why3/-/issues/287Add injectivity for type invariant2024-01-31T14:02:14+01:00François BobotAdd injectivity for type invariant```
type t = {
v: int;
} invariant { 0 <= v }
```
It is currently not possible to prove that:
```
forall x1 x2:t. x1.v = x2.v -> x1 = x2
```
Which is compiled to:
```
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
```
We need...```
type t = {
v: int;
} invariant { 0 <= v }
```
It is currently not possible to prove that:
```
forall x1 x2:t. x1.v = x2.v -> x1 = x2
```
Which is compiled to:
```
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
```
We need to add the property that `view` is injective, for example using `mk` its inverse:
```
forall x:t [view x]. mk (view x) = x
```
# Decision #
> So, we agreed that adding `t'mk` for constructing a non-private type `t` from its fields is a good idea.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/286Extend witness grammar for type invariant2021-04-24T22:17:58+02:00François BobotExtend witness grammar for type invariantThe proposal is to extend the current grammar for the `by` construct.
Currently:
```
type t = { f1: ...; f2: ... } invariant { ... } by { f1 = ...; f2 = ...}
```
proposed:
```
type t = { ... } invariant { ... } by e
```
where all leaf...The proposal is to extend the current grammar for the `by` construct.
Currently:
```
type t = { f1: ...; f2: ... } invariant { ... } by { f1 = ...; f2 = ...}
```
proposed:
```
type t = { ... } invariant { ... } by e
```
where all leaf of `e` in result position have the shape `{ f1 = ...; f2 = ...}`
The implementation:
- parsing e as an expression
- typing check that all the leaf define all the fields of the record, and translate the leaf into a tuple in the order of the field definition. So the witness is well-typed and doesn't use the defined type.
- check the properties on e
The properties on e checked, currently (not complete, nor correct?):
- no side effect
- pure
I don't see why we have these restrictions, we just want to prove that such element is buildable so any non-ghost computation should be acceptable.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/258Cloning part of mutable structure2019-01-28T15:00:00+01:00François BobotCloning part of mutable structureSimilar attempt than in #51, but here the question is more what would be the right way to use.
The important points to try to keep are:
* the field minimum is not mutable
* there is an invariant
```
module T
use int.Int
...Similar attempt than in #51, but here the question is more what would be the right way to use.
The important points to try to keep are:
* the field minimum is not mutable
* there is an invariant
```
module T
use int.Int
type t_mutable = mutable { }
type t = {
ghost minimum: int;
t_mutable: t_mutable;
}
val create (ghost i:int) : t
ensures { result.minimum = i }
val set (x:t) (i:int) : unit
requires { x.minimum <= i }
writes { x.t_mutable }
exception Unset
val get (x:t) (i:int) : int
ensures { x.minimum <= result }
raises { Unset -> true }
end
module T2
use int.Int
type t_mutable = {
mutable v: int;
mutable set': bool;
}
type t = {
ghost minimum: int;
t_mutable : t_mutable;
}
invariant { t_mutable.set' -> minimum <= t_mutable.v }
let set (x:t) (i:int) : unit
requires { x.minimum <= i }
=
x.t_mutable.v <- i;
x.t_mutable.set' <- true
let create (ghost i:int) : t
ensures { result.minimum = i } =
{ minimum = i;
t_mutable = { set' = false; v = 0 }
}
exception Unset
let get (x:t) (i:int) : int
ensures { x.minimum <= result }
raises { Unset -> true }
=
if not x.t_mutable.set' then raise Unset;
x.t_mutable.v
clone T with
type t_mutable = t_mutable,
val create = create,
val set = set,
exception Unset = Unset,
val get = get
end
```
Currently the message is that the two t types are not the same. The substitution of `type t = t`, can't be currently added in the clone stanza because t is defined in T.https://gitlab.inria.fr/why3/why3/-/issues/229Adding location to SP generated variables2022-07-11T17:38:34+02:00DAILLER SylvainAdding location to SP generated variablesHello,
I don't know if I already opened an issue for this but there should be locations for ident generated by the sp_expr function in vc.ml. In this part of the code, I would like the None locations to be replaced by the appropriate lo...Hello,
I don't know if I already opened an issue for this but there should be locations for ident generated by the sp_expr function in vc.ml. In this part of the code, I would like the None locations to be replaced by the appropriate locations:
```
let fresh_wr2 v _ = clone_pv None v in
let fresh_rd2 v _ = if v.pv_ity.ity_pure then None
else Some (clone_pv None v) in
```
This is apparently possible to do by adding a location to constructor Kseq and then propagating it.
A test for checking that it works is simply to create several assignments in a function and look at the generated task. If the constants of the generated task don't have locations, it does not work.MOREAU SoleneMOREAU Solenehttps://gitlab.inria.fr/why3/why3/-/issues/136Make `any ... ensures` less error-prone2018-06-22T11:28:03+02:00Guillaume MelquiondMake `any ... ensures` less error-proneI didn't know that `any ... ensures` introduces an axiom. And I was not the only developer to get it wrong. We really should limit the number of language constructions that introduce axioms.
There are only three occurrences of this cons...I didn't know that `any ... ensures` introduces an axiom. And I was not the only developer to get it wrong. We really should limit the number of language constructions that introduce axioms.
There are only three occurrences of this construction in the gallery:
- `unraveling_a_card_trick`: `any int ensures { 0 <= result <= n*m }`
- `white_and_black_balls`: `any (x: int, y: int) ensures { 0 <= x && 0 <= y && x + y = 2 && x <= !b && y <= !w }`
- `vstte12_bfs`: `any B.t ensures { !!result = succ v }`
The first two occurrences are actually provable, so I am not sure their authors intended them to generate axioms. The last one is an actual axiom, but it should ideally have been `val`, so that the user could instantiate it to obtain an effective algorithm.
Thus, I suggest that this construction be repurposed so that it generates a verification condition.1.0.0https://gitlab.inria.fr/why3/why3/-/issues/57Variants and soundness guarantees2018-06-13T16:56:30+02:00Guillaume MelquiondVariants and soundness guarantees```
predicate p (x y : unit) = true
let rec function foo (x : unit) : unit
variant { x with p } ensures { false } = foo x
goal g : false
```
As far as I understand it, the rule of thumb has always been that, in absence of `axiom` or `...```
predicate p (x y : unit) = true
let rec function foo (x : unit) : unit
variant { x with p } ensures { false } = foo x
goal g : false
```
As far as I understand it, the rule of thumb has always been that, in absence of `axiom` or `val`, the system should be sound. So either this rule should also exclude the use of custom `variant`, or Why3 should generate a proof obligation for the wellfoundedness of such relations.https://gitlab.inria.fr/why3/why3/-/issues/56No default order for range types2018-09-14T14:19:19+02:00Guillaume MelquiondNo default order for range types```
use import mach.int.Int63
let rec foo (x: int63): int63
variant { x }
= foo (x - 1)
```
```
File "foo.mlw", line 4, characters 2-13:
no default order for o
```
It would be good if range types were usable as variants without havin...```
use import mach.int.Int63
let rec foo (x: int63): int63
variant { x }
= foo (x - 1)
```
```
File "foo.mlw", line 4, characters 2-13:
no default order for o
```
It would be good if range types were usable as variants without having to use `of_int`. In fact, the ordering relation is much simpler than in the `int` case, since we do not even have to choose an arbitrary lower bound.
Note also that the error message is rather poor since it mentions an automatically generated binder.https://gitlab.inria.fr/why3/why3/-/issues/29Machine integers and range types2018-02-02T10:52:53+01:00Guillaume MelquiondMachine integers and range typesNow that range types are available, we should investigate moving away types such as `int31` from abstract types. We should also see whether it helps expressing `for` loops on machine integers (hopefully yes).Now that range types are available, we should investigate moving away types such as `int31` from abstract types. We should also see whether it helps expressing `for` loops on machine integers (hopefully yes).1.0.0Guillaume MelquiondGuillaume Melquiond