-
Notifications
You must be signed in to change notification settings - Fork 2
/
InitFreezeMST.fst
73 lines (61 loc) · 2.17 KB
/
InitFreezeMST.fst
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
module InitFreezeMST
open FStar.Preorder
open FStar.Heap
open FStar.ST
open FStar.MRef
type rstate (a:Type) =
| Empty : rstate a
| Mutable : v:a -> rstate a
| Frozen : v:a -> rstate a
let evolve_broken' (a:Type) = fun r1 r2 ->
match r1, r2 with
| Empty, Mutable _
| Mutable _, Mutable _ -> True
| Mutable v1, Frozen v2 -> v1 == v2
| _, _ -> False
[@expect_failure]
let evolve_broken (a:Type) : Tot (preorder (rstate a)) = evolve_broken' a
let evolve' (a:Type) = fun r1 r2 ->
match r1, r2 with
| Empty, _
| Mutable _, Mutable _
| Mutable _, Frozen _ -> True
| Frozen v1, Frozen v2 -> v1 == v2
| _, _ -> False
let evolve (a:Type) : Tot (preorder (rstate a)) = evolve' a
let eref (a:Type) : Type = mref (rstate a) (evolve a)
let alloc (a:Type) : ST (eref a) (requires (fun _ -> True))
(ensures (fun _ r h -> Empty? (sel h r)))
= alloc #_ #(evolve a) Empty
let read (#a:Type) (r:eref a) : ST a (requires (fun h -> ~(Empty? (sel h r))))
(ensures (fun h v h' -> h == h' /\
(sel h r == Mutable v \/ sel h r == Frozen v)))
= match (!r) with | Mutable v | Frozen v -> v
let write (#a:Type) (r:eref a) (v:a) :
ST unit (requires (fun h -> ~(Frozen? (sel h r))))
(ensures (fun _ _ h -> sel h r == Mutable v))
= r := Mutable v
let freeze (#a:Type) (r:eref a) :
ST unit (requires (fun h0 -> Mutable? (sel h0 r)))
(ensures (fun h0 _ h1 -> Frozen? (sel h1 r) /\
Mutable?.v (sel h0 r) == Frozen?.v (sel h1 r)))
= r := Frozen (Mutable?.v !r)
assume val complex_procedure (r:eref int) : St unit
let main() : St unit =
let r = alloc int in
(* ignore (read r) -- fails like it should *)
write r 42;
ignore (read r);
write r 0;
witness_token r (fun rs -> ~(Empty? rs));
freeze r;
(* write r 7; -- fails like it should *)
ignore (read r);
witness_token r (fun rs -> rs == Frozen 0);
complex_procedure r;
(* ignore (read r); -- fails like it should *)
recall_token r (fun rs -> ~(Empty? rs));
let x = read r in
(* assert (x == 0) -- fails like it should *)
recall_token r (fun rs -> rs == Frozen 0);
assert (x == 0)