why3 issueshttps://gitlab.inria.fr/why3/why3/issues2019-11-27T12:19:54Zhttps://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/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/287Add injectivity for type invariant2020-02-05T15:47:01ZFranç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
```Franç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/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 Paskevich