pgtable_lemmas.v 12.1 KB
Newer Older
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
From refinedc.typing Require Import typing.
Set Default Proof Using "Type".

(* S1 specific *)

Record Pte_S1_attr_lo := {
  attr_lo_s1_attridx : Z;
  attr_lo_s1_ap : Z;
  attr_lo_s1_sh : Z;
  attr_lo_s1_af : bool;
}.

Definition empty_Pte_S1_attr_lo := {|
  attr_lo_s1_attridx := 0;
  attr_lo_s1_ap := 0;
  attr_lo_s1_sh := 0;
  attr_lo_s1_af := false;
|}.

Definition Pte_S1_attr_lo_tm (r : Pte_S1_attr_lo) : tm :=
  bf_cons (range_of 2 3) (bf_val $ attr_lo_s1_attridx r) $
  bf_cons (range_of 6 2) (bf_val $ attr_lo_s1_ap r) $
  bf_cons (range_of 8 2) (bf_val $ attr_lo_s1_sh r) $
  bf_cons (range_of 10 1) (bf_val $ bool_to_Z $ attr_lo_s1_af r) $
  bf_nil.

Definition Pte_S1_attr_lo_wf (r : Pte_S1_attr_lo) : Prop :=
  0  attr_lo_s1_attridx r < 2^3 
  0  attr_lo_s1_ap r < 2^2 
  0  attr_lo_s1_sh r < 2^2 
  0  bool_to_Z $ attr_lo_s1_af r < 2^1 
  True.

Paul's avatar
Paul committed
34
35
Definition Pte_S1_attr_lo_sig :=
  sig_atom (range_of 2 3) $
Paul's avatar
Paul committed
36
  sig_atom (range_of 5 1) $ (* undef *)
Paul's avatar
Paul committed
37
38
39
  sig_atom (range_of 6 2) $
  sig_atom (range_of 8 2) $
  sig_atom (range_of 10 1) $
Paul's avatar
Paul committed
40
  sig_atom (range_of 11 1) $ (* undef *)
Paul's avatar
Paul committed
41
  sig_end.
Paul's avatar
Paul committed
42
Global Instance Pte_S1_attr_lo_sig_wf : SigWf Pte_S1_attr_lo_sig.
Paul's avatar
Paul committed
43
Proof. solve_sig_wf. Qed.
44

Paul's avatar
Paul committed
45
Global Instance Pte_S1_attr_lo_tm_value r :
Paul's avatar
Paul committed
46
47
  IsValue (Pte_S1_attr_lo_tm r).
Proof. repeat constructor. Qed.
Paul's avatar
Paul committed
48

Paul's avatar
Paul committed
49
Global Instance Pte_S1_attr_lo_tm_sort r `{!CanSolve (Pte_S1_attr_lo_wf r)} :
Paul's avatar
Paul committed
50
51
52
53
  HasSort (Pte_S1_attr_lo_tm r) Pte_S1_attr_lo_sig.
Proof.
  unfold HasSort; solve_goal.
Qed.
Paul's avatar
Paul committed
54

55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
Record Pte_S1_attr_hi := {
  attr_hi_s1_xn : bool;
}.

Definition empty_Pte_S1_attr_hi := {|
  attr_hi_s1_xn := false;
|}.

Definition Pte_S1_attr_hi_tm (r : Pte_S1_attr_hi) : tm :=
  bf_cons (range_of 54 1) (bf_val $ bool_to_Z $ attr_hi_s1_xn r) $
  bf_nil.

Definition Pte_S1_attr_hi_wf (r : Pte_S1_attr_hi) : Prop :=
  0  bool_to_Z $ attr_hi_s1_xn r < 2^1 
  True.

Paul's avatar
Paul committed
71
Definition Pte_S1_attr_hi_sig :=
Paul's avatar
Paul committed
72
73
74
75
  sig_atom (range_of 51 3) $ (* undef *)
  sig_atom (range_of 54 1) $
  sig_atom (range_of 55 9) $ (* undef *)
  sig_end.
Paul's avatar
Paul committed
76
Global Instance Pte_S1_attr_hi_sig_wf : SigWf Pte_S1_attr_hi_sig.
Paul's avatar
Paul committed
77
Proof. solve_sig_wf. Qed.
78

Paul's avatar
Paul committed
79
Global Instance Pte_S1_attr_hi_tm_value r :
Paul's avatar
Paul committed
80
81
  IsValue (Pte_S1_attr_hi_tm r).
Proof. repeat constructor. Qed.
Paul's avatar
Paul committed
82

Paul's avatar
Paul committed
83
Global Instance Pte_S1_attr_hi_tm_sort r `{!CanSolve (Pte_S1_attr_hi_wf r)} :
Paul's avatar
Paul committed
84
85
86
87
  HasSort (Pte_S1_attr_hi_tm r) Pte_S1_attr_hi_sig.
Proof.
  unfold HasSort; solve_goal.
Qed.
Paul's avatar
Paul committed
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
(* S2 specific *)

Record Pte_S2_attr_lo := {
  attr_lo_s2_memattr : Z;
  attr_lo_s2_ap_r : bool;
  attr_lo_s2_ap_w : bool;
  attr_lo_s2_sh : Z;
  attr_lo_s2_af : bool;
}.

Definition empty_Pte_S2_attr_lo := {|
  attr_lo_s2_memattr := 0;
  attr_lo_s2_ap_r := false;
  attr_lo_s2_ap_w := false;
  attr_lo_s2_sh := 0;
  attr_lo_s2_af := false;
|}.

Definition Pte_S2_attr_lo_tm (r : Pte_S2_attr_lo) : tm :=
  bf_cons (range_of 2 3) (bf_val $ attr_lo_s2_memattr r) $
  bf_cons (range_of 6 1) (bf_val $ bool_to_Z $ attr_lo_s2_ap_r r) $
  bf_cons (range_of 7 1) (bf_val $ bool_to_Z $ attr_lo_s2_ap_w r) $
  bf_cons (range_of 8 2) (bf_val $ attr_lo_s2_sh r) $
  bf_cons (range_of 10 1) (bf_val $ bool_to_Z $ attr_lo_s2_af r) $
  bf_nil.

Definition Pte_S2_attr_lo_wf (r : Pte_S2_attr_lo) : Prop :=
  0  attr_lo_s2_memattr r < 2^3 
  0  bool_to_Z $ attr_lo_s2_ap_r r < 2^1 
  0  bool_to_Z $ attr_lo_s2_ap_w r < 2^1 
  0  attr_lo_s2_sh r < 2^2 
  0  bool_to_Z $ attr_lo_s2_af r < 2^1 
  True.

Paul's avatar
Paul committed
123
124
Definition Pte_S2_attr_lo_sig :=
  sig_atom (range_of 2 3) $
Paul's avatar
Paul committed
125
  sig_atom (range_of 5 1) $ (* undef *)
Paul's avatar
Paul committed
126
127
128
129
  sig_atom (range_of 6 1) $
  sig_atom (range_of 7 1) $
  sig_atom (range_of 8 2) $
  sig_atom (range_of 10 1) $
Paul's avatar
Paul committed
130
  sig_atom (range_of 11 1) $ (* undef *)
Paul's avatar
Paul committed
131
  sig_end.
Paul's avatar
Paul committed
132
Global Instance Pte_S2_attr_lo_sig_wf : SigWf Pte_S2_attr_lo_sig.
Paul's avatar
Paul committed
133
Proof. solve_sig_wf. Qed.
134

Paul's avatar
Paul committed
135
Global Instance Pte_S2_attr_lo_tm_value r :
Paul's avatar
Paul committed
136
137
  IsValue (Pte_S2_attr_lo_tm r).
Proof. repeat constructor. Qed.
Paul's avatar
Paul committed
138

Paul's avatar
Paul committed
139
Global Instance Pte_S2_attr_lo_tm_sort r `{!CanSolve (Pte_S2_attr_lo_wf r)} :
Paul's avatar
Paul committed
140
141
142
143
  HasSort (Pte_S2_attr_lo_tm r) Pte_S2_attr_lo_sig.
Proof.
  unfold HasSort; solve_goal.
Qed.
Paul's avatar
Paul committed
144

145
146
147
148
149
150
151
152
153
Record Pte_S2_attr_hi := {
  attr_hi_s2_xn : bool;
}.

Definition empty_Pte_S2_attr_hi := {|
  attr_hi_s2_xn := false;
|}.

Definition Pte_S2_attr_hi_tm (r : Pte_S2_attr_hi) : tm :=
Paul's avatar
Paul committed
154
  bf_cons (range_of 54 1) (bf_val $ bool_to_Z $ attr_hi_s2_xn r) $
155
156
157
158
159
160
  bf_nil.

Definition Pte_S2_attr_hi_wf (r : Pte_S2_attr_hi) : Prop :=
  0  bool_to_Z $ attr_hi_s2_xn r < 2^1 
  True.

Paul's avatar
Paul committed
161
162
163
164
165
Definition Pte_S2_attr_hi_sig :=
  sig_atom (range_of 51 3) $ (* undef *)
  sig_atom (range_of 54 1) $
  sig_atom (range_of 55 9) $ (* undef *)
  sig_end.
Paul's avatar
Paul committed
166
Global Instance Pte_S2_attr_hi_sig_wf : SigWf Pte_S2_attr_hi_sig.
Paul's avatar
Paul committed
167
Proof. solve_sig_wf. Qed.
168

Paul's avatar
Paul committed
169
Global Instance Pte_S2_attr_hi_tm_value r :
Paul's avatar
Paul committed
170
171
  IsValue (Pte_S2_attr_hi_tm r).
Proof. repeat constructor. Qed.
Paul's avatar
Paul committed
172

Paul's avatar
Paul committed
173
Global Instance Pte_S2_attr_hi_tm_sort r `{!CanSolve (Pte_S2_attr_hi_wf r)} :
Paul's avatar
Paul committed
174
175
176
177
  HasSort (Pte_S2_attr_hi_tm r) Pte_S2_attr_hi_sig.
Proof.
  unfold HasSort; solve_goal.
Qed.
Paul's avatar
Paul committed
178

179
180
181
182
183
(* Pte *)

Record Pte := mk_pte {
  pte_valid : bool;
  pte_type : Z;
184
  pte_leaf_attr_lo : Pte_S1_attr_lo + Pte_S2_attr_lo;
185
186
  pte_addr : Z;
  pte_undef : Z;
187
  pte_leaf_attr_hi : Pte_S1_attr_hi + Pte_S2_attr_hi;
188
189
}.

190
191
192
Inductive stage : Type := S1 | S2.

Definition empty_Pte (s : stage) := {|
193
194
  pte_valid := false;
  pte_type := 0;
195
196
197
198
199
  pte_leaf_attr_lo :=
    match s with
    | S1 => inl empty_Pte_S1_attr_lo
    | S2 => inr empty_Pte_S2_attr_lo
    end;
200
201
  pte_addr := 0;
  pte_undef := 0;
202
203
204
205
206
  pte_leaf_attr_hi :=
    match s with
    | S1 => inl empty_Pte_S1_attr_hi
    | S2 => inr empty_Pte_S2_attr_hi
    end;
207
208
209
210
211
212
213
214
215
|}.

Global Instance Pte_settable : Settable _ := settable! mk_pte
  <pte_valid; pte_type; pte_leaf_attr_lo; pte_addr; pte_undef; pte_leaf_attr_hi>.

Definition Pte_repr (r : Pte) : tm :=
  bf_cons (range_of 0 1) (bf_val $ bool_to_Z $ pte_valid r) $
  bf_cons (range_of 1 1) (bf_val $ pte_type r) $
  bf_cons (range_of 2 10) (bf_nested (range_of 2 10)
216
    (sum_elim (pte_leaf_attr_lo r) Pte_S1_attr_lo_tm Pte_S2_attr_lo_tm)) $
217
218
219
  bf_cons (range_of 12 36) (bf_val $ pte_addr r) $
  bf_cons (range_of 48 3) (bf_val $ pte_undef r) $
  bf_cons (range_of 51 13) (bf_nested (range_of 51 13)
220
    (sum_elim (pte_leaf_attr_hi r) Pte_S1_attr_hi_tm Pte_S2_attr_hi_tm)) $
221
222
223
  bf_nil.
Arguments Pte_repr _/.

Paul's avatar
Paul committed
224
225
226
Definition pte_wf (r : Pte) : Prop :=
  0  bool_to_Z $ pte_valid r < 2^1 
  0  pte_type r < 2^1 
Paul's avatar
Paul committed
227
  sum_elim (pte_leaf_attr_lo r) Pte_S1_attr_lo_wf Pte_S2_attr_lo_wf 
Paul's avatar
Paul committed
228
229
  0  pte_addr r < 2^36 
  0  pte_undef r < 2^3 
Paul's avatar
Paul committed
230
  sum_elim (pte_leaf_attr_hi r) Pte_S1_attr_hi_wf Pte_S2_attr_hi_wf 
Paul's avatar
Paul committed
231
  True.
232

Paul's avatar
Paul committed
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
Definition Pte_sig (s : stage) :=
  sig_atom (range_of 0 1) $
  sig_atom (range_of 1 1) $
  sig_nested (range_of 2 10) (match s with
    | S1 => Pte_S1_attr_lo_sig
    | S2 => Pte_S2_attr_lo_sig
  end) $
  sig_atom (range_of 12 36) $
  sig_atom (range_of 48 3) $
  sig_nested (range_of 51 13) (match s with
    | S1 => Pte_S1_attr_hi_sig
    | S2 => Pte_S2_attr_hi_sig
  end) $
  sig_end.

Paul's avatar
Paul committed
248
Global Instance Pte_sig_wf s : SigWf (Pte_sig s).
Paul's avatar
Paul committed
249
Proof. destruct s; solve_sig_wf. Qed.
Paul's avatar
Paul committed
250

Paul's avatar
Paul committed
251
252
Definition Pte_constraints (s : stage) (r : Pte) :=
  match s with
253
254
  | S1 => ( a, pte_leaf_attr_lo r = inl a)  ( a, pte_leaf_attr_hi r = inl a)
  | S2 => ( a, pte_leaf_attr_lo r = inr a)  ( a, pte_leaf_attr_hi r = inr a)
Paul's avatar
Paul committed
255
256
  end.

257
258
259
Global Program Instance Pte_bd : BitfieldDesc Pte := {|
  bitfield_it := u64;
  bitfield_args := stage;
260
  bitfield_constraints := Pte_constraints;
Paul's avatar
Paul committed
261
  bitfield_wf   := pte_wf;
262
  bitfield_repr := Pte_repr;
Paul's avatar
Paul committed
263
  bitfield_sig  := Pte_sig;
264
|}.
Paul's avatar
Paul committed
265
266

Global Instance Pte_attr_lo_tm_value r :
Paul's avatar
Paul committed
267
268
269
270
271
272
273
274
275
276
277
278
279
  IsValue (sum_elim r Pte_S1_attr_lo_tm Pte_S2_attr_lo_tm).
Proof.
  destruct r; typeclasses eauto.
Qed.

Global Instance Pte_attr_lo_tm_sort r s
  `{!CanSolve (sum_elim r Pte_S1_attr_lo_wf Pte_S2_attr_lo_wf)}
  `{!CanSolve (match s with
                | S1 => ( a, r = inl a)
                | S2 => ( a, r = inr a)
               end)}:
  HasSort (sum_elim r Pte_S1_attr_lo_tm Pte_S2_attr_lo_tm)
    (match s with
Paul's avatar
Paul committed
280
281
    | S1 => Pte_S1_attr_lo_sig
    | S2 => Pte_S2_attr_lo_sig
Paul's avatar
Paul committed
282
283
284
285
    end).
Proof.
  unfold CanSolve in *; case_match; destruct CanSolve1; subst; typeclasses eauto.
Qed.
Paul's avatar
Paul committed
286

Paul's avatar
Paul committed
287
Global Instance Pte_attr_hi_tm_value r :
Paul's avatar
Paul committed
288
289
290
291
292
293
294
295
296
297
298
299
300
  IsValue (sum_elim r Pte_S1_attr_hi_tm Pte_S2_attr_hi_tm).
Proof.
  destruct r; typeclasses eauto.
Qed.

Global Instance Pte_attr_hi_tm_sort r s
  `{!CanSolve (sum_elim r Pte_S1_attr_hi_wf Pte_S2_attr_hi_wf)}
  `{!CanSolve (match s with
                | S1 => ( a, r = inl a)
                | S2 => ( a, r = inr a)
               end)} :
  HasSort (sum_elim r Pte_S1_attr_hi_tm Pte_S2_attr_hi_tm)
    (match s with
Paul's avatar
Paul committed
301
302
    | S1 => Pte_S1_attr_hi_sig
    | S2 => Pte_S2_attr_hi_sig
Paul's avatar
Paul committed
303
304
305
306
    end).
Proof.
  unfold CanSolve in *; case_match; destruct CanSolve1; subst; typeclasses eauto.
Qed.
Paul's avatar
Paul committed
307

308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
Global Instance simple_protected_Pte_constraints p `{!IsProtected p} x r `{!CanSolve (Pte_constraints x r)} :
  SimplAndUnsafe true (Pte_constraints p r) (λ T, p = x  T).
Proof. split; naive_solver. Qed.
Global Instance Pte_constraints_S1 valid type leaf_attr_lo addr undef leaf_attr_hi :
  SimplAnd (Pte_constraints S1 {|
    pte_valid := valid;
    pte_type := type;
    pte_leaf_attr_lo := inl leaf_attr_lo;
    pte_addr := addr;
    pte_undef := undef;
    pte_leaf_attr_hi := inl leaf_attr_hi;
  |}) (λ T, T).
Proof. split; naive_solver. Qed.
Global Instance Pte_constraints_S2 valid type leaf_attr_lo addr undef leaf_attr_hi :
  SimplAnd (Pte_constraints S2 {|
    pte_valid := valid;
    pte_type := type;
    pte_leaf_attr_lo := inr leaf_attr_lo;
    pte_addr := addr;
    pte_undef := undef;
    pte_leaf_attr_hi := inr leaf_attr_hi;
  |}) (λ T, T).
Proof. split; naive_solver. Qed.

332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
Global Instance simpl_exist_Pte P : SimplExist Pte P
  ( valid type leaf_attr_lo addr undef leaf_attr_hi,
    P {|
      pte_valid := valid;
      pte_type := type;
      pte_leaf_attr_lo := leaf_attr_lo;
      pte_addr := addr;
      pte_undef := undef;
      pte_leaf_attr_hi := leaf_attr_hi;
    |}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_Pte P : SimplForall Pte 6 P
  ( valid type leaf_attr_lo addr undef leaf_attr_hi,
    P {|
      pte_valid := valid;
      pte_type := type;
      pte_leaf_attr_lo := leaf_attr_lo;
      pte_addr := addr;
      pte_undef := undef;
      pte_leaf_attr_hi := leaf_attr_hi;
    |}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.

(* pte prot *)

Record Prot := {
  prot_x : bool;
  prot_w : bool;
  prot_r : bool;
  prot_device : bool;
}.

Definition prot_repr (p : Prot) : tm :=
  bf_cons (range_of 0 1) (bf_val $ bool_to_Z $ prot_x p) $
  bf_cons (range_of 1 1) (bf_val $ bool_to_Z $ prot_w p) $
  bf_cons (range_of 2 1) (bf_val $ bool_to_Z $ prot_r p) $
  bf_cons (range_of 3 1) (bf_val $ bool_to_Z $ prot_device p) $
  bf_nil.

Arguments prot_repr _/.

Definition prot_wf (p : Prot) : Prop :=
  0  bool_to_Z $ prot_x p < 2^1 
  0  bool_to_Z $ prot_w p < 2^1 
  0  bool_to_Z $ prot_r p < 2^1 
  0  bool_to_Z $ prot_device p < 2^1.

Global Program Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
  bitfield_it := u64;
  bitfield_args := ();
382
  bitfield_constraints := λ _ _, True;
383
384
  bitfield_repr := prot_repr;
  bitfield_wf := prot_wf;
Paul's avatar
Paul committed
385
386
387
388
389
390
  bitfield_sig  := λ _,
    sig_atom (range_of 0 1) $
    sig_atom (range_of 1 1) $
    sig_atom (range_of 2 1) $
    sig_atom (range_of 3 1) $
    sig_end
391
|}.
Paul's avatar
Paul committed
392
Next Obligation. destruct 1; solve_sig_wf. Qed.
393
394
395
396
397
398
399
400
401
402

Global Instance simpl_exist_Prot P : SimplExist Prot P ( x w r device,
  P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_Prot P : SimplForall Prot 4 P ( x w r device,
  P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.

(* struct, const *)

403
404
Definition pte_from_addr (s : stage) (pa : Pte) : Pte :=
  empty_Pte s <| pte_addr := pte_addr pa |>.
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419

Record mm_callbacks := {
  virt_to_phys : Z  Pte;
}.

Definition max_level : Z := 4.
Definition mtype_device : Z := 5.
Definition mtype_normal : Z := 0.
Definition pte_type_block : Z := 0.
Definition pte_type_page : Z := 1.
Definition pte_type_table : Z := 1.
Definition ap_rw : Z := 1.
Definition ap_ro : Z := 3.
Definition sh_is : Z := 3.
Definition err_code : Z := 22.