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/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/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/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/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