-
Notifications
You must be signed in to change notification settings - Fork 0
/
Gen_Spec.v
288 lines (201 loc) · 9.33 KB
/
Gen_Spec.v
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
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
(* theories/Gen_Spec.v: generated lemma specifications from CN *)
Require Import ZArith Bool.
Require CN_Lemmas.CN_Lib.
Module Types.
(* no type definitions required *)
End Types.
Module Type Parameters.
Import Types.
Parameter order_aligned : Z -> Z -> bool.
Parameter page_size_of_order : Z -> Z.
Parameter page_aligned : Z -> Z -> bool.
Parameter pfn_buddy : Z -> Z -> Z.
Parameter order_align : Z -> Z -> Z.
End Parameters.
Module Defs (P : Parameters).
Import Types P.
Open Scope Z.
Definition get_range_start_1_4 {T_0 T_1 T_2 T_3: Type} (t : (T_0 * T_1 * T_2 * T_3)) :=
(let '(x_t_0,x_t_1,x_t_2,x_t_3) := (t : (T_0 * T_1 * T_2 * T_3)) in
x_t_1).
Definition get_order_1_3 {T_0 T_1 T_2: Type} (t : (T_0 * T_1 * T_2)) :=
(let '(x_t_0,x_t_1,x_t_2) := (t : (T_0 * T_1 * T_2)) in
x_t_1).
Definition hyp_no_order :=
255.
Definition page_group_ok (page_index : Z) (vmemmap : ((Z -> (Z * Z * Z)))) (pool : (((Z -> (CN_Lib.Loc * CN_Lib.Loc))) * Z * Z * Z)) :=
(let page := (vmemmap page_index) in (let start_i := ((get_range_start_1_4 pool) / 4096) in (((get_order_1_3 page) = (hyp_no_order)) \/
(forall (i : Z),
(((1 <= i) /\ (i <= 10)) ->
(~
(((((order_align page_index i) < page_index) /\ (start_i <= (order_align page_index i))) /\ (i <= (get_order_1_3 (vmemmap (order_align page_index i))))) /\
(~ ((get_order_1_3 (vmemmap (order_align page_index i))) = (hyp_no_order)))))))))).
Definition fun_upd {A B : Type} (eq : A -> A -> bool) (f : A -> B) x y z :=
if eq x z then y else f z.
Definition upd_order_1_3 {T_0 T_1 T_2: Type} (t : (T_0 * T_1 * T_2)) (x : T_1) :=
(let '(x_t_0,x_t_1,x_t_2) := (t : (T_0 * T_1 * T_2)) in
(x_t_0,(x : T_1),x_t_2)).
Definition get_range_end_2_4 {T_0 T_1 T_2 T_3: Type} (t : (T_0 * T_1 * T_2 * T_3)) :=
(let '(x_t_0,x_t_1,x_t_2,x_t_3) := (t : (T_0 * T_1 * T_2 * T_3)) in
x_t_2).
Definition page_size :=
4096.
Definition get_refcount_0_3 {T_0 T_1 T_2: Type} (t : (T_0 * T_1 * T_2)) :=
(let '(x_t_0,x_t_1,x_t_2) := (t : (T_0 * T_1 * T_2)) in
x_t_0).
Definition get_flags_2_3 {T_0 T_1 T_2: Type} (t : (T_0 * T_1 * T_2)) :=
(let '(x_t_0,x_t_1,x_t_2) := (t : (T_0 * T_1 * T_2)) in
x_t_2).
Definition struct_hyp_page_good (x : (Z * Z * Z)) :=
((((0 <= (get_refcount_0_3 x)) /\ ((get_refcount_0_3 x) <= 65535)) /\ ((0 <= (get_order_1_3 x)) /\ ((get_order_1_3 x) <= 255))) /\ ((0 <= (get_flags_2_3 x)) /\ ((get_flags_2_3 x) <= 255))).
Definition order_dec_inv_type : Prop :=
forall (pool_range_end : Z),
forall (pfn : Z),
forall (order1 : Z),
forall (order2 : Z),
(Is_true (order_aligned pfn order1)) ->
(((pfn * 4096) + (page_size_of_order order1)) <= pool_range_end) ->
(0 <= order2) ->
(order2 <= order1) ->
(Is_true (order_aligned pfn order2)) /\ (((pfn * 4096) + (page_size_of_order order2)) <= pool_range_end).
Definition lemma2_type : Prop :=
forall (p_i : Z),
forall (order : Z),
(0 <= order) ->
let p_phys := (p_i * 4096) in
let buddy_i := (pfn_buddy p_i order) in
let buddy_phys := (buddy_i * 4096) in
(Is_true (order_aligned p_i order)) ->
(Is_true (order_aligned buddy_i order)) ->
let min_i := (if (p_i <? buddy_i) then p_i else buddy_i) in
let min_i_phys := (min_i * 4096) in
(Is_true (order_aligned min_i (order + 1))) /\ (Is_true (page_aligned min_i_phys (order + 1))) /\ (((p_phys + (page_size_of_order order)) = buddy_phys) \/ ((p_phys - (page_size_of_order order)) = buddy_phys)).
Definition extract_l_type : Prop :=
forall (p_i : Z),
forall (order : Z),
(0 <= order) ->
let p_phys := (p_i * 4096) in
let buddy_i := (pfn_buddy p_i order) in
let buddy_phys := (buddy_i * 4096) in
(Is_true (order_aligned p_i (order + 1))) ->
((p_phys + (page_size_of_order order)) = buddy_phys) /\ (Is_true (page_aligned p_phys order)) /\ (Is_true (page_aligned buddy_phys order)).
Definition page_size_of_order_inc_type : Prop :=
forall (order : Z),
(0 <= order) ->
((page_size_of_order (order + 1)) = (2 * (page_size_of_order order))).
Definition lemma4_type : Prop :=
forall (p_i : Z),
forall (order : Z),
(1 <= order) ->
let p_phys := (p_i * 4096) in
(Is_true (order_aligned p_i order)) ->
let buddy_i := (pfn_buddy p_i (order - 1)) in
let buddy_phys := (buddy_i * 4096) in
(~ (Is_true (order_aligned buddy_i order))) /\ (buddy_phys = (p_phys + (page_size_of_order (order - 1)))) /\ (0 < (page_size_of_order order)) /\ (0 < (page_size_of_order (order - 1))) /\ (((page_size_of_order
(order - 1)) * 2) = (page_size_of_order order)) /\ ((order_align buddy_i order) = p_i).
Definition order_align_inv_loop_type : Prop :=
forall (__hypvmemmap : CN_Lib.Loc),
forall (V : ((Z -> (Z * Z * Z)))),
forall (pool : (((Z -> (CN_Lib.Loc * CN_Lib.Loc))) * Z * Z * Z)),
forall (p : CN_Lib.Loc),
let hypvmemmap := __hypvmemmap in
let p_i := ((p - __hypvmemmap) / 4) in
let start_i := ((get_range_start_1_4 pool) / 4096) in
let end_i := ((get_range_end_2_4 pool) / 4096) in
let p_order := (get_order_1_3 (V p_i)) in
(1 <= p_order) ->
(p_order < 11) ->
(Is_true (order_aligned p_i p_order)) ->
((((CN_Lib.array_shift hypvmemmap 1 (4 * start_i)) <= p) /\ (p < (CN_Lib.array_shift hypvmemmap 1 (4 * end_i)))) /\ (((p - hypvmemmap) mod 4) = 0)) ->
let buddy_i := (pfn_buddy p_i (p_order - 1)) in
(forall (i : Z),
(((start_i <= i) /\ (i < end_i)) -> (page_group_ok i V pool))) ->
let p_new_page := (upd_order_1_3 (V p_i) (p_order - 1)) in
let buddy_new_page := (upd_order_1_3 (V buddy_i) (p_order - 1)) in
(forall (i : Z),
(((start_i <= i) /\ (i < end_i)) -> (page_group_ok i (fun_upd Z.eqb (fun_upd Z.eqb V p_i p_new_page) buddy_i buddy_new_page) pool))).
Definition order_aligned_init_type : Prop :=
forall (i : Z),
(Is_true (order_aligned i 0)).
Definition page_size_of_order_type : Prop :=
((page_size_of_order 0) = (page_size)).
Definition attach_inc_loop_type : Prop :=
forall (V : ((Z -> (Z * Z * Z)))),
forall (__hypvmemmap : CN_Lib.Loc),
forall (pool : (((Z -> (CN_Lib.Loc * CN_Lib.Loc))) * Z * Z * Z)),
forall (p : CN_Lib.Loc),
forall (order : Z),
let hypvmemmap := __hypvmemmap in
let start_i := ((get_range_start_1_4 pool) / 4096) in
let end_i := ((get_range_end_2_4 pool) / 4096) in
((((CN_Lib.array_shift hypvmemmap 1 (4 * start_i)) <= p) /\ (p < (CN_Lib.array_shift hypvmemmap 1 (4 * end_i)))) /\ (((p - hypvmemmap) mod 4) = 0)) ->
let p_i := ((p - __hypvmemmap) / 4) in
let buddy_i := (pfn_buddy p_i order) in
let buddy_order := (get_order_1_3 (V buddy_i)) in
(start_i <= buddy_i) ->
(buddy_i < end_i) ->
(0 <= order) ->
((order + 1) < 11) ->
(buddy_order = order) ->
(Is_true (order_aligned p_i order)) ->
(Is_true (order_aligned buddy_i order)) ->
((get_order_1_3 (V p_i)) = (hyp_no_order)) ->
let p_page_tweaked := (upd_order_1_3 (V p_i) order) in
(forall (i : Z),
(((start_i <= i) /\ (i < end_i)) -> (page_group_ok i (fun_upd Z.eqb V p_i p_page_tweaked) pool))) ->
let min_i := (if (p_i <? buddy_i) then p_i else buddy_i) in
let min_page := (upd_order_1_3 (V min_i) (order + 1)) in
let buddy_page := (upd_order_1_3 (V buddy_i) (hyp_no_order)) in
(forall (i : Z),
(((start_i <= i) /\ (i < end_i)) -> (page_group_ok i (fun_upd Z.eqb (fun_upd Z.eqb V buddy_i buddy_page) min_i min_page) pool))).
Definition find_buddy_xor_type : Prop :=
forall (addr_i : Z),
forall (order : Z),
(Is_true (order_aligned addr_i order)) ->
(0 <= order) ->
(order < 11) ->
(0 <= addr_i) ->
((addr_i * 4096) < (2 ^ 64)) ->
(0 < (2 ^ order)) /\ ((2 ^ order) < (2 ^ 11)) /\ (0 <= (Z.lxor (addr_i * 4096) (4096 * (2 ^ order)))) /\ ((Z.lxor (addr_i * 4096) (4096 * (2 ^ order))) < (2 ^ 64)) /\ let buddy_addr := (Z.lxor
(addr_i * 4096) (4096 * (2 ^ order))) in
let buddy_i := (buddy_addr / 4096) in
(buddy_i = (pfn_buddy addr_i order)) /\ ((buddy_addr mod 4096) = 0) /\ (Is_true (order_aligned buddy_i order)) /\ (~ (addr_i = buddy_i)).
Definition page_size_of_order2_type : Prop :=
forall (order : Z),
(0 <= order) ->
(order < 11) ->
(0 < (2 ^ order)) /\ ((2 ^ order) < (2 ^ 11)) /\ let size := (4096 * (2 ^ order)) in
(size = (page_size_of_order order)).
Definition page_group_ok_easy_type : Prop :=
forall (__hypvmemmap : CN_Lib.Loc),
forall (pool : (((Z -> (CN_Lib.Loc * CN_Lib.Loc))) * Z * Z * Z)),
forall (V : ((Z -> (Z * Z * Z)))),
let hypvmemmap := __hypvmemmap in
(0 <= (get_range_start_1_4 pool)) ->
(0 <= (get_range_end_2_4 pool)) ->
let start_i := ((get_range_start_1_4 pool) / 4096) in
let end_i := ((get_range_end_2_4 pool) / 4096) in
(forall (i : Z),
(((start_i <= i) /\ (i < end_i)) -> (struct_hyp_page_good (V i)))) ->
(forall (i : Z),
(((start_i <= i) /\ (i < end_i)) -> ((get_order_1_3 (V i)) = 0))) ->
(forall (i : Z),
(((start_i <= i) /\ (i < end_i)) -> (struct_hyp_page_good (V i)))) /\ (forall (i : Z),
(((start_i <= i) /\ (i < end_i)) -> (page_group_ok i V pool))).
End Defs.
Module Type Lemma_Spec (P : Parameters).
Module D := Defs(P).
Import D.
Parameter order_dec_inv : order_dec_inv_type.
Parameter lemma2 : lemma2_type.
Parameter extract_l : extract_l_type.
Parameter page_size_of_order_inc : page_size_of_order_inc_type.
Parameter lemma4 : lemma4_type.
Parameter order_align_inv_loop : order_align_inv_loop_type.
Parameter order_aligned_init : order_aligned_init_type.
Parameter page_size_of_order : page_size_of_order_type.
Parameter attach_inc_loop : attach_inc_loop_type.
Parameter find_buddy_xor : find_buddy_xor_type.
Parameter page_size_of_order2 : page_size_of_order2_type.
Parameter page_group_ok_easy : page_group_ok_easy_type.
End Lemma_Spec.