why3 issueshttps://gitlab.inria.fr/why3/why3/issues2019-10-09T09:01:52Zhttps://gitlab.inria.fr/why3/why3/issues/391Refining types by cloning ?2019-10-09T09:01:52ZDAILLER SylvainRefining types by cloning ?Hello,
After the GT of last week, I learned that it seemed to be possible to refine types by cloning. And, perhaps this issue is related to the one on "final" (and exactly why people want a final keyword ? I am not sure I understand).
Long story short, I was not satisfied by standard library's hashtbl (for my usage) because I wanted to have a hashtbl in which at most one element corresponds to each key. The hashtbl from standard library are àla Ocaml so they allow several addition for each key.
So, I start to refine the type as follows by adding an invariant to the type `t` stating that only list of length one are allowed:
```
module H
use int.Int
use map.Map
use list.ListRich
type key = int
type t 'a = { ghost mutable contents: map key (list 'a) }
invariant { forall k: key. length (contents k) <= 1 }
by { contents = (fun _ -> Nil) }
clone hashtbl.Hashtbl as H with
type key = key,
type t = t
```
What I would expect now is for the tool to make me prove somehow that this is compliant with the current signature of the hashtbl module ? But, instead, the definition is accepted and the following code can be proven:
```
let f (h: t int) (k: key) : unit
ensures { false }
=
H.add h k 3;
H.add h k 4
let invalid () : unit
ensures { false }
=
f (H.create 42) 1
end
```
I can use the `invalid` function like this:
```
module T
use H
let f (a: int) : int
ensures { result = 3 }
=
H.invalid ();
a
end
```
@paskevyc and others: Do you have any idea of what happens here ? Should I not be allowed to refine type `t`, should we generate new goals on the clone declaration (how?), or any other solution ?
I definitely don't want to be allowed to break the system like this (even if I did something wrong).Hello,
After the GT of last week, I learned that it seemed to be possible to refine types by cloning. And, perhaps this issue is related to the one on "final" (and exactly why people want a final keyword ? I am not sure I understand).
Long story short, I was not satisfied by standard library's hashtbl (for my usage) because I wanted to have a hashtbl in which at most one element corresponds to each key. The hashtbl from standard library are àla Ocaml so they allow several addition for each key.
So, I start to refine the type as follows by adding an invariant to the type `t` stating that only list of length one are allowed:
```
module H
use int.Int
use map.Map
use list.ListRich
type key = int
type t 'a = { ghost mutable contents: map key (list 'a) }
invariant { forall k: key. length (contents k) <= 1 }
by { contents = (fun _ -> Nil) }
clone hashtbl.Hashtbl as H with
type key = key,
type t = t
```
What I would expect now is for the tool to make me prove somehow that this is compliant with the current signature of the hashtbl module ? But, instead, the definition is accepted and the following code can be proven:
```
let f (h: t int) (k: key) : unit
ensures { false }
=
H.add h k 3;
H.add h k 4
let invalid () : unit
ensures { false }
=
f (H.create 42) 1
end
```
I can use the `invalid` function like this:
```
module T
use H
let f (a: int) : int
ensures { result = 3 }
=
H.invalid ();
a
end
```
@paskevyc and others: Do you have any idea of what happens here ? Should I not be allowed to refine type `t`, should we generate new goals on the clone declaration (how?), or any other solution ?
I definitely don't want to be allowed to break the system like this (even if I did something wrong).https://gitlab.inria.fr/why3/why3/issues/277Module Fset should be ghost2019-05-22T07:49:14ZGuillaume MelquiondModule Fset should be ghostEither that or it should be monomorphic with respect to equality. Indeed, as it stands, the following program is verifiable:
```
use set.Fset
type t = { ghost b : bool }
let f ()
ensures { result = 2 }
=
let s = singleton { b = false } in
let s = add { b = true } s in
cardinal s
```Either that or it should be monomorphic with respect to equality. Indeed, as it stands, the following program is verifiable:
```
use set.Fset
type t = { ghost b : bool }
let f ()
ensures { result = 2 }
=
let s = singleton { b = false } in
let s = add { b = true } s in
cardinal s
```1.3.0Jean-Christophe FilliâtreJean-Christophe Filliâtre