why3 issueshttps://gitlab.inria.fr/why3/why3/issues2020-03-27T00:05:33Zhttps://gitlab.inria.fr/why3/why3/issues/468Clone problem when type has nested regions2020-03-27T00:05:33ZMá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 = {
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.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-27T12:19:54ZDAILLER 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 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
```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` clause2019-06-19T14:12:00ZDAILLER 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 : int)
=
while c <= 10 do
invariant Ic { inv c }
variant { c }
c <- c + 2
done
```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
```DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/344Lost location for function argument2019-06-26T08:44:49ZDAILLER 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 :
#"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.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-20T12:02:23ZFranç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 invariant2020-03-05T15:32:16ZFranç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 to add the property that `view` is injective, for example using `mk` its inverse:
```
forall x:t [view x]. mk (view x) = x
``````
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
```1.4.0François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/issues/286Extend witness grammar for type invariant2019-03-26T16:35:06ZFranç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 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.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-28T14:00:00ZFranç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
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.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 variables2018-11-07T08:44:13ZDAILLER 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 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.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.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/issues/136Make `any ... ensures` less error-prone2018-06-22T09:28:03ZGuillaume 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 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.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-13T14:56:30ZGuillaume 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 `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.```
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-14T12:19:19ZGuillaume 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 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.```
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-02T09:52:53ZGuillaume 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