-
Notifications
You must be signed in to change notification settings - Fork 2
/
gset_map.fst
223 lines (193 loc) · 12.5 KB
/
gset_map.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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
module Gset_map
open FStar.List.Tot
#set-options "--query_stats"
open Library
module A = Alpha_map
module G = Gset
val pre_cond_merge_a : l:A.s G.s -> a:A.s G.s -> b:A.s G.s
-> Pure bool
(requires true)
(ensures (fun b1 -> (b1 = true <==> (forall e. A.mem_key_s e l ==> A.mem_key_s e a /\ A.mem_key_s e b) /\
(forall ch. A.mem_key_s ch a \/ A.mem_key_s ch b ==>
G.pre_cond_merge (A.get_val_s #G.s #G.op #G.rval ch l)
(A.get_val_s #G.s #G.op #G.rval ch a) (A.get_val_s #G.s #G.op #G.rval ch b)))))
let pre_cond_merge_a l a b = A.pre_cond_merge_a #G.s #G.op #G.rval l a b
val merge_a : l:A.s G.s
-> a:A.s G.s
-> b:A.s G.s
-> Pure (A.s G.s)
(requires pre_cond_merge_a l a b)
(ensures (fun r -> (forall ch. A.mem_key_s ch r <==> A.mem_key_s ch a \/ A.mem_key_s ch b) /\ A.unique_key r /\
(forall ch. A.mem_key_s ch a \/ A.mem_key_s ch b ==> (A.get_val_s #G.s #G.op #G.rval ch r) =
(G.merge (A.get_val_s #G.s #G.op #G.rval ch l) (A.get_val_s #G.s #G.op #G.rval ch a) (A.get_val_s #G.s #G.op #G.rval ch b)))))
let merge_a l a b = A.merge_a #G.s #G.op #G.rval l a b
val lemma2 : s1:A.s G.s
-> Lemma (requires true)
(ensures (forall e. mem e s1 ==> (A.get_val_s #G.s #G.op #G.rval (A.get_key_s e) s1 = A.get_val_s1 #G.s e)))
let rec lemma2 s1 =
match s1 with
|[] -> ()
|x::xs -> lemma2 xs
val lemma4 : tr:ae (A.op G.op) -> s1:A.s G.s
-> Lemma (requires A.sim_a #G.s #G.op #G.rval tr s1)
(ensures (forall i. (G.sim (A.project i tr) (A.get_val_s #G.s #G.op #G.rval i s1))))
let lemma4 tr s1 = ()
val lemma1 : tr:ae (A.op G.op)
-> st:A.s G.s
-> op1:(nat * (A.op G.op))
-> Lemma (requires (A.sim_a #G.s #G.op #G.rval tr st) /\ (not (mem_id (get_id op1) tr.l)) /\
(forall e. mem e tr.l ==> get_id e < get_id op1) /\ get_id op1 > 0 /\
G.pre_cond_do (A.get_val_s #G.s #G.op #G.rval (A.get_key op1) st) (A.project_op op1))
(ensures (forall i. A.mem_key_s i (get_st (A.do_a #G.s #G.op #G.rval st op1)) /\ i <> A.get_key op1 ==>
((forall e. mem e (A.project i (abs_do tr op1)).l <==> mem e (A.project i tr).l) /\
(forall e e1. mem e (A.project i (abs_do tr op1)).l /\ mem e1 (A.project i (abs_do tr op1)).l /\ get_id e <> get_id e1 /\
(A.project i (abs_do tr op1)).vis e e1 <==>
mem e (A.project i tr).l /\ mem e1 (A.project i tr).l /\ get_id e <> get_id e1 /\ (A.project i tr).vis e e1) /\
(A.get_val_s #G.s #G.op #G.rval i (get_st (A.do_a #G.s #G.op #G.rval st op1)) = (A.get_val_s #G.s #G.op #G.rval i st))) ==>
(G.sim (A.project i (abs_do tr op1)) (A.get_val_s #G.s #G.op #G.rval i (get_st (A.do_a #G.s #G.op #G.rval st op1))))))
#set-options "--z3rlimit 1000"
let lemma1 tr st op = ()
val lemma7 : tr:ae G.op -> s1:G.s -> tr1:ae G.op
-> Lemma (requires G.sim tr s1 /\ (forall e. mem e tr1.l <==> mem e tr.l) /\
(forall e e1. mem e tr1.l /\ mem e1 tr1.l /\ get_id e <> get_id e1 /\ tr1.vis e e1 <==>
mem e tr.l /\ mem e1 tr.l /\ get_id e <> get_id e1 /\ tr.vis e e1))
(ensures (G.sim tr1 s1))
#set-options "--z3rlimit 1000"
let lemma7 tr s1 tr1 = ()
val pre_cond_prop_merge_a : ltr:ae (A.op G.op)
-> l:A.s G.s
-> atr:ae (A.op G.op)
-> a:A.s G.s
-> btr:ae (A.op G.op)
-> b:A.s G.s
-> Tot (b1:bool {b1=true <==> (forall ch. A.mem_key_s ch a \/ A.mem_key_s ch b ==>
(G.pre_cond_prop_merge (A.project ch ltr) (A.get_val_s #G.s #G.op #G.rval ch l)
(A.project ch atr) (A.get_val_s #G.s #G.op #G.rval ch a)
(A.project ch btr) (A.get_val_s #G.s #G.op #G.rval ch b)) /\
(forall e. mem e (A.project ch ltr).l ==> not (mem_id (get_id e) (A.project ch atr).l)) /\
(forall e. mem e (A.project ch atr).l ==> not (mem_id (get_id e) (A.project ch btr).l)) /\
(forall e. mem e (A.project ch ltr).l ==> not (mem_id (get_id e) (A.project ch btr).l)) /\
(G.sim (A.project ch ltr) (A.get_val_s #G.s #G.op #G.rval ch l) /\
G.sim (union (A.project ch ltr) (A.project ch atr)) (A.get_val_s #G.s #G.op #G.rval ch a) /\
G.sim (union (A.project ch ltr) (A.project ch btr)) (A.get_val_s #G.s #G.op #G.rval ch b)))})
let pre_cond_prop_merge_a ltr l atr a btr b =
forallb (fun ch -> (G.pre_cond_prop_merge (A.project ch ltr) (A.get_val_s #G.s #G.op #G.rval ch l)
(A.project ch atr) (A.get_val_s #G.s #G.op #G.rval ch a)
(A.project ch btr) (A.get_val_s #G.s #G.op #G.rval ch b)) &&
forallb (fun e -> not (mem_id (get_id e) (A.project ch atr).l)) (A.project ch ltr).l &&
forallb (fun e -> not (mem_id (get_id e) (A.project ch btr).l)) (A.project ch atr).l &&
forallb (fun e -> not (mem_id (get_id e) (A.project ch btr).l)) (A.project ch ltr).l &&
G.sim (A.project ch ltr) (A.get_val_s #G.s #G.op #G.rval ch l) &&
G.sim (union (A.project ch ltr) (A.project ch atr)) (A.get_val_s #G.s #G.op #G.rval ch a) &&
G.sim (union (A.project ch ltr) (A.project ch btr)) (A.get_val_s #G.s #G.op #G.rval ch b)) (A.get_key_lst l a b)
instance _ : A.alpha_map G.s G.op G.rval G.gset = {
A.lemma1 = lemma1;
A.lemma4 = lemma4;
A.lemma2 = lemma2;
A.lemma7 = lemma7
}
val pre_cond_do_a : s1:(A.s G.s) -> op1:(nat * (A.op G.op))
-> Tot (b:bool {b = true <==>
G.pre_cond_do (A.get_val_s #G.s #G.op #G.rval (A.get_key op1) s1) (A.project_op op1)})
let pre_cond_do_a s1 op =
G.pre_cond_do (A.get_val_s #G.s #G.op #G.rval (A.get_key op) s1) (A.project_op op)
val pre_cond_prop_do_a : tr:ae (A.op G.op)
-> st:(A.s G.s)
-> op1:(nat * (A.op G.op))
-> Pure bool
(requires (not (mem_id (get_id op1) tr.l) /\
(forall e. mem e tr.l ==> get_id e < get_id op1) /\ get_id op1 > 0))
(ensures (fun b -> (b=true <==> (G.pre_cond_prop_do (A.project (A.get_key op1) tr)
(A.get_val_s #G.s #G.op #G.rval (A.get_key op1) st) (A.project_op op1)) /\
G.pre_cond_do (A.get_val_s #G.s #G.op #G.rval (A.get_key op1) st) (A.project_op op1) /\
(G.sim (A.project (A.get_key op1) (abs_do tr op1)) (A.get_val_s #G.s #G.op #G.rval (A.get_key op1) (get_st (A.do_a #G.s #G.op #G.rval st op1)))))))
let pre_cond_prop_do_a tr st op1 =
G.pre_cond_prop_do (A.project (A.get_key op1) tr)
(A.get_val_s #G.s #G.op #G.rval (A.get_key op1) st) (A.project_op op1) &&
G.pre_cond_do (A.get_val_s #G.s #G.op #G.rval (A.get_key op1) st) (A.project_op op1) &&
G.sim (A.project (A.get_key op1) (abs_do tr op1)) (A.get_val_s #G.s #G.op #G.rval (A.get_key op1)
(get_st (A.do_a #G.s #G.op #G.rval st op1)))
val prop_do_a : tr:ae (A.op G.op)
-> st:A.s G.s
-> op1:(nat * (A.op G.op))
-> Lemma (requires (A.sim_a #G.s #G.op #G.rval tr st) /\ (not (mem_id (get_id op1) tr.l)) /\
(forall e. mem e tr.l ==> get_id e < get_id op1) /\ get_id op1 > 0 /\
pre_cond_do_a st op1 /\ pre_cond_prop_do_a tr st op1)
(ensures (A.sim_a #G.s #G.op #G.rval (abs_do tr op1) (get_st (A.do_a #G.s #G.op #G.rval st op1))))
#set-options "--z3rlimit 1000"
let prop_do_a tr st op =
A.prop_do_a #G.s #G.op #G.rval #G.gset tr st op
val convergence_a : tr:ae (A.op G.op)
-> a:A.s G.s
-> b:A.s G.s
-> Lemma (requires (A.sim_a #G.s #G.op #G.rval tr a /\ A.sim_a #G.s #G.op #G.rval tr b))
(ensures (forall e. A.mem_key_s e a <==> A.mem_key_s e b) /\
(forall ch. A.mem_key_s ch a /\ A.mem_key_s ch b ==>
(forall e. mem e (A.get_val_s #G.s #G.op #G.rval ch a) <==> mem e (A.get_val_s #G.s #G.op #G.rval ch b))))
#set-options "--z3rlimit 1000"
let convergence_a tr a b =
A.convergence_a1 #G.s #G.op #G.rval tr a b
val prop_merge_a : ltr:ae (A.op G.op)
-> l:(A.s G.s)
-> atr:ae (A.op G.op)
-> a:(A.s G.s)
-> btr:ae (A.op G.op)
-> b:(A.s G.s)
-> Lemma (requires (forall e. mem e ltr.l ==> not (mem_id (get_id e) atr.l)) /\
(forall e. mem e atr.l ==> not (mem_id (get_id e) btr.l)) /\
(forall e. mem e ltr.l ==> not (mem_id (get_id e) btr.l)) /\
(A.sim_a #G.s #G.op #G.rval ltr l /\ A.sim_a #G.s #G.op #G.rval (union ltr atr) a /\ A.sim_a #G.s #G.op #G.rval (union ltr btr) b) /\
pre_cond_merge_a l a b /\
(forall ch. A.mem_key_s ch a \/ A.mem_key_s ch b ==>
(pre_cond_prop_merge #G.s #G.op #G.rval (A.project ch ltr) (A.get_val_s #G.s #G.op #G.rval ch l)
(A.project ch atr) (A.get_val_s #G.s #G.op #G.rval ch a)
(A.project ch btr) (A.get_val_s #G.s #G.op #G.rval ch b)) /\
(sim #G.s #G.op #G.rval (A.project ch ltr) (A.get_val_s #G.s #G.op #G.rval ch l) /\ sim #G.s #G.op #G.rval (union (A.project ch ltr) (A.project ch atr)) (A.get_val_s #G.s #G.op #G.rval ch a) /\ sim #G.s #G.op #G.rval (union (A.project ch ltr) (A.project ch btr)) (A.get_val_s #G.s #G.op #G.rval ch b))))
(ensures (A.sim_a #G.s #G.op #G.rval (abs_merge ltr atr btr) (merge_a l a b)))
#set-options "--z3rlimit 1000"
let prop_merge_a ltr l atr a btr b =
A.prop_merge_a #G.s #G.op #G.rval #G.gset ltr l atr a btr b
val extract : r:G.rval {r <> G.Bot} -> G.s
let extract (G.Val s) = s
val spec_a : o1:(nat * (A.op G.op))
-> tr:ae (A.op G.op)
-> Pure G.rval
(requires true)
(ensures (fun res -> A.opget o1 ==> (res = G.spec (A.project_op o1) (A.project (A.get_key o1) tr))))
let spec_a o1 tr = G.spec (A.project_op o1) (A.project (A.get_key o1) tr)
val prop_spec_a : tr:ae (A.op G.op)
-> st1:(A.s G.s)
-> op:(nat * (A.op G.op))
-> Lemma (requires (A.sim_a #G.s #G.op #G.rval tr st1) /\ (not (mem_id (get_id op) tr.l)) /\
(forall e. mem e tr.l ==> get_id e < get_id op) /\ get_id op > 0 /\
pre_cond_do_a st1 op)
(ensures (A.opget op ==>
((G.opa (A.project_op op) ==> (get_rval (A.do_a #G.s #G.op #G.rval st1 op)) =
((A.spec_a #G.s #G.op #G.rval) op tr)) /\
(not (G.opa (A.project_op op)) ==>
(forall e. mem e (extract (get_rval (A.do_a #G.s #G.op #G.rval st1 op))) <==>
mem e (extract ((A.spec_a #G.s #G.op #G.rval) op tr)))))))
#set-options "--z3rlimit 100000"
let prop_spec_a tr st op = ()
val sim_a : tr:ae (A.op G.op)
-> s1:(A.s G.s)
-> Tot (b:bool {(b = true) <==> (forall e1. mem e1 s1 ==> (exists e. mem e tr.l /\ A.get_key_s e1 = A.get_key e /\ A.opset e)) /\
(forall k. A.mem_key_s k s1 ==> G.sim (A.project k tr) (A.get_val_s #G.s #G.op #G.rval k s1)) /\
(forall e. mem e tr.l /\ A.opset e ==> (exists e1. mem e1 s1 /\ A.get_key e = A.get_key_s e1))})
let sim_a tr s1 =
A.sim_a #G.s #G.op #G.rval tr s1
instance gset_map : mrdt (A.s G.s) (A.op G.op) (G.rval) = {
Library.init = A.init_a;
Library.spec = spec_a;
Library.sim = sim_a;
Library.pre_cond_do = pre_cond_do_a;
Library.pre_cond_prop_do = pre_cond_prop_do_a;
Library.pre_cond_merge = pre_cond_merge_a;
Library.pre_cond_prop_merge = pre_cond_prop_merge_a;
Library.do = A.do_a;
Library.merge = merge_a;
Library.prop_do = prop_do_a;
Library.prop_merge = prop_merge_a;
Library.prop_spec = prop_spec_a;
Library.convergence = convergence_a
}