1(*  Oliver *)
2
3open HolKernel boolLib bossLib Parse;
4open MMUTheory;
5open Cond_rewrite blastLib;
6
7val _ = new_theory "MMU_Setup";
8
9(* === MMU requirements  === *)
10val guest1_min_adr_def = Define `guest1_min_adr = 0x100000w:word32`;
11val guest1_max_adr_def = Define `guest1_max_adr= 0x3FFFFFw:word32`;
12val guest2_min_adr_def = Define `guest2_min_adr = 0x400000w:word32`;
13val guest2_max_adr_def = Define `guest2_max_adr = 0x6FFFFFw:word32`;
14
15val _ = new_constant ("guest1", ``:word32``);
16val _ = new_constant ("guest2", ``:word32``);
17
18val you_and_me_axiom = new_axiom("you_and_me_axiom", ``guest1 <> guest2``);
19val you_and_me_thm = store_thm("you_and_me_thm", ``guest1 <> guest2``, FULL_SIMP_TAC (srw_ss()) [you_and_me_axiom]);
20
21val inequal_by_inequalities_gt_lem = blastLib.BBLAST_PROVE ``!(x:word32) (a:word32) (b:word32). (a > x) /\  (b <= x) ==> (a <> b)``;
22
23val inequal_by_inequalities_lt_lem = blastLib.BBLAST_PROVE ``!(x:word32) (a:word32) (b:word32). (a < x) /\  (b >= x) ==> (a <> b)``;
24
25val inequal_by_inequalities_gtu_lem = blastLib.BBLAST_PROVE ``!(x:word32) (a:word32) (b:word32). (a >+ x) /\  (b <=+ x) ==> (a <> b)``;
26
27val inequal_by_inequalities_ltu_lem = blastLib.BBLAST_PROVE ``!(x:word32) (a:word32) (b:word32). (a <+ x) /\  (b >=+ x) ==> (a <> b)``;
28
29
30
31val inequal_by_inequalities = save_thm(
32   "inequal_by_inequalities",
33(CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_gtu_lem)
34(CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_gtu_lem)
35(CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_ltu_lem)
36(CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_ltu_lem)
37(CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_gtu_lem)
38(CONJ (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_gtu_lem)
39(CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_ltu_lem)
40(CONJ (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_ltu_lem)
41(CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_gt_lem)
42(CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_gt_lem)
43(CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_lt_lem)
44(CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_lt_lem)
45(CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_gt_lem)
46(CONJ (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_gt_lem)
47(CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_lt_lem)
48      (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_lt_lem)))))))))))))))));
49
50
51val negated_inequalities_lem = blastLib.BBLAST_PROVE  ``!(x:word32) (y:word32).
52                         ((~(y <= x)) ==> (y >  x))
53                     /\  ((~(y <  x)) ==> (y >= x))
54                     /\  ((~(y >  x)) ==> (y <= x))
55                     /\  ((~(y >= x)) ==> (y <  x)) ``;
56
57val negated_inequalities_unsigned_lem = blastLib.BBLAST_PROVE  ``!(x:word32) (y:word32).
58                         ((~(y <=+ x)) ==> (y >+  x))
59                     /\  ((~(y <+  x)) ==> (y >=+ x))
60                     /\  ((~(y >+  x)) ==> (y <=+ x))
61                     /\  ((~(y >=+ x)) ==> (y <+  x)) ``;
62
63
64val negated_inequalities = save_thm("negated_inequalities",
65 (CONJ (SPEC ``guest1_min_adr:word32`` negated_inequalities_unsigned_lem)
66 (CONJ (SPEC ``guest1_max_adr:word32`` negated_inequalities_unsigned_lem)
67 (CONJ (SPEC ``guest2_min_adr:word32`` negated_inequalities_unsigned_lem)
68 (CONJ (SPEC ``guest2_max_adr:word32`` negated_inequalities_unsigned_lem)
69 (CONJ (SPEC ``guest1_min_adr:word32`` negated_inequalities_lem)
70 (CONJ (SPEC ``guest1_max_adr:word32`` negated_inequalities_lem)
71 (CONJ (SPEC ``guest2_min_adr:word32`` negated_inequalities_lem)
72       (SPEC ``guest2_max_adr:word32`` negated_inequalities_lem)))))))));
73
74
75val address_cases = save_thm(
76    "address_cases", blastLib.BBLAST_PROVE ``!(b:word32) (a:word32) (X:bool) (Y:bool).
77(((a <= b) ==> X)  ==> (((a > b) \/ Y) ==> X)  ==> X) /\
78(((a >= b) ==> X)  ==> ((Y \/ (a < b)) ==> X)  ==> X) /\
79(((a <=+ b) ==> X)  ==> (((a >+ b) \/ Y) ==> X)  ==> X) /\
80(((a >=+ b) ==> X)  ==> ((Y \/ (a <+ b)) ==> X)  ==> X)``);
81
82
83
84val negated_and_or =  save_thm(
85    "negated_and_or",
86    blastLib.BBLAST_PROVE
87``!(a:word32).
88((~(a > guest2_max_adr ��� a < guest2_min_adr))  =  (a <= guest2_max_adr /\ a >= guest2_min_adr)) /\
89((~(a ��� guest1_max_adr ��� a ��� guest1_min_adr))  =  (a >  guest1_max_adr \/ a <  guest1_min_adr)) /\
90((~(a > guest1_max_adr ��� a < guest1_min_adr))  =  (a <= guest1_max_adr /\ a >= guest1_min_adr)) /\
91((~(a ��� guest2_max_adr ��� a ��� guest2_min_adr))  =  (a >  guest2_max_adr \/ a <  guest2_min_adr)) /\
92((~(a > guest2_max_adr ��� a < guest1_min_adr))  =  (a <= guest2_max_adr /\ a >= guest1_min_adr)) /\
93((~(a >+ guest2_max_adr ��� a <+ guest2_min_adr))  =  (a <=+ guest2_max_adr /\ a >=+ guest2_min_adr)) /\
94((~(a <=+ guest1_max_adr ��� a >=+ guest1_min_adr))  =  (a >+  guest1_max_adr \/ a <+  guest1_min_adr)) /\
95((~(a >+ guest1_max_adr ��� a <+ guest1_min_adr))  =  (a <=+ guest1_max_adr /\ a >=+ guest1_min_adr)) /\
96((~(a <=+ guest2_max_adr ��� a >=+ guest2_min_adr))  =  (a >+  guest2_max_adr \/ a <+  guest2_min_adr)) /\
97((~(a >+ guest2_max_adr ��� a <+ guest1_min_adr))  =  (a <=+ guest2_max_adr /\ a >=+ guest1_min_adr)) /\
98((~(a > 0x2FFFFFw ��� a < 0x200000w))  =  (a <= 0x2FFFFFw /\ a >= 0x200000w)) /\
99((~(a ��� 0x1FFFFFw ��� a ��� 0x100000w))  =  (a >  0x1FFFFFw \/ a <  0x100000w)) /\
100((~(a > 0x1FFFFFw ��� a < 0x100000w))  =  (a <= 0x1FFFFFw /\ a >= 0x100000w)) /\
101((~(a ��� 0x2FFFFFw ��� a ��� 0x200000w))  =  (a >  0x2FFFFFw \/ a <  0x200000w)) /\
102((~(a > 0x2FFFFFw ��� a < 0x100000w))  =  (a <= 0x2FFFFFw /\ a >= 0x100000w))``);
103
104
105
106(* address border *)
107
108val address_border_concrete = save_thm(
109    "address_border_concrete", blastLib.BBLAST_PROVE ``!(a:word32). (a ��� 0x1FFFFFw \/ a ��� 0x200000w) /\ (a ��� 0x3FFFFFw \/ a ��� 0x400000w) /\ (a <=+ 0x3FFFFFw \/ a >=+ 0x400000w)``);
110
111val address_border = store_thm(
112    "address_border",
113    ``!(a:word32). (a <=+ guest1_max_adr \/ a >=+ guest2_min_adr)``,
114    FULL_SIMP_TAC (srw_ss()) [address_border_concrete, guest1_max_adr_def, guest2_min_adr_def]);
115
116
117(* transitivity for all <, <=, >, >= *)
118val address_trans = store_thm(
119    "address_trans",
120    ``!(x:word32).
121((x <+  guest1_min_adr) ==> (x <=+ guest1_min_adr)) /\
122((x <+  guest1_min_adr) ==> (x <+  guest1_max_adr)) /\
123((x <+  guest1_min_adr) ==> (x <=+ guest1_max_adr)) /\
124((x <+  guest1_min_adr) ==> (x <+  guest2_min_adr)) /\
125((x <+  guest1_min_adr) ==> (x <=+ guest2_min_adr)) /\
126((x <+  guest1_min_adr) ==> (x <+  guest2_max_adr)) /\
127((x <+  guest1_min_adr) ==> (x <=+ guest2_max_adr)) /\
128((x <=+ guest1_min_adr) ==> (x <+  guest1_max_adr)) /\
129((x <=+ guest1_min_adr) ==> (x <=+ guest1_max_adr)) /\
130((x <=+ guest1_min_adr) ==> (x <+  guest2_min_adr)) /\
131((x <=+ guest1_min_adr) ==> (x <=+ guest2_min_adr)) /\
132((x <=+ guest1_min_adr) ==> (x <+  guest2_max_adr)) /\
133((x <=+ guest1_min_adr) ==> (x <=+ guest2_max_adr)) /\
134((x <+  guest1_max_adr) ==> (x <=+ guest1_max_adr)) /\
135((x <+  guest1_max_adr) ==> (x <+  guest2_min_adr)) /\
136((x <+  guest1_max_adr) ==> (x <=+ guest2_min_adr)) /\
137((x <+  guest1_max_adr) ==> (x <+  guest2_max_adr)) /\
138((x <+  guest1_max_adr) ==> (x <=+ guest2_max_adr)) /\
139((x <=+ guest1_max_adr) ==> (x <+  guest2_min_adr)) /\
140((x <=+ guest1_max_adr) ==> (x <=+ guest2_min_adr)) /\
141((x <=+ guest1_max_adr) ==> (x <+  guest2_max_adr)) /\
142((x <=+ guest1_max_adr) ==> (x <=+ guest2_max_adr)) /\
143((x <+  guest2_min_adr) ==> (x <=+ guest1_max_adr)) /\
144((x <+  guest2_min_adr) ==> (x <=+ guest2_min_adr)) /\
145((x <+  guest2_min_adr) ==> (x <+  guest2_max_adr)) /\
146((x <+  guest2_min_adr) ==> (x <=+ guest2_max_adr)) /\
147((x <=+ guest2_min_adr) ==> (x <+  guest2_max_adr)) /\
148((x <=+ guest2_min_adr) ==> (x <=+ guest2_max_adr)) /\
149((x <+  guest2_max_adr) ==> (x <=+ guest2_max_adr)) /\
150((x >+  guest2_max_adr) ==> (x >=+ guest2_max_adr)) /\
151((x >+  guest2_max_adr) ==> (x >+  guest2_min_adr)) /\
152((x >+  guest2_max_adr) ==> (x >=+ guest2_min_adr)) /\
153((x >+  guest2_max_adr) ==> (x >+  guest1_max_adr)) /\
154((x >+  guest2_max_adr) ==> (x >=+ guest1_max_adr)) /\
155((x >+  guest2_max_adr) ==> (x >+  guest1_min_adr)) /\
156((x >+  guest2_max_adr) ==> (x >=+ guest1_min_adr)) /\
157((x >=+ guest2_max_adr) ==> (x >+  guest2_min_adr)) /\
158((x >=+ guest2_max_adr) ==> (x >=+ guest2_min_adr)) /\
159((x >=+ guest2_max_adr) ==> (x >+  guest1_max_adr)) /\
160((x >=+ guest2_max_adr) ==> (x >=+ guest1_max_adr)) /\
161((x >=+ guest2_max_adr) ==> (x >+  guest1_min_adr)) /\
162((x >=+ guest2_max_adr) ==> (x >=+ guest1_min_adr)) /\
163((x >+  guest2_min_adr) ==> (x >=+ guest2_min_adr)) /\
164((x >+  guest2_min_adr) ==> (x >+  guest1_max_adr)) /\
165((x >+  guest2_min_adr) ==> (x >=+ guest1_max_adr)) /\
166((x >+  guest2_min_adr) ==> (x >+  guest1_min_adr)) /\
167((x >+  guest2_min_adr) ==> (x >=+ guest1_min_adr)) /\
168((x >=+ guest2_min_adr) ==> (x >+  guest1_max_adr)) /\
169((x >=+ guest2_min_adr) ==> (x >=+ guest1_max_adr)) /\
170((x >=+ guest2_min_adr) ==> (x >+  guest1_min_adr)) /\
171((x >=+ guest2_min_adr) ==> (x >=+ guest1_min_adr)) /\
172((x >+  guest1_max_adr) ==> (x >=+ guest1_max_adr)) /\
173((x >+  guest1_max_adr) ==> (x >+  guest1_min_adr)) /\
174((x >+  guest1_max_adr) ==> (x >=+ guest1_min_adr)) /\
175((x >=+ guest1_max_adr) ==> (x >+  guest1_min_adr)) /\
176((x >=+ guest1_max_adr) ==> (x >=+ guest1_min_adr)) /\
177((x >+  guest1_min_adr) ==> (x >=+ guest1_min_adr))``,
178FULL_SIMP_TAC (srw_ss()) [guest1_min_adr_def, guest1_max_adr_def, guest2_min_adr_def, guest2_max_adr_def] THEN blastLib.BBLAST_TAC);
179
180
181val address_complete = store_thm(
182    "address_complete",
183    ``!(add1:word32). (add1 <=+ guest1_max_adr ��� add1 >=+ guest1_min_adr) \/
184                     (add1 <=+ guest2_max_adr ��� add1 >=+ guest2_min_adr) \/
185                     (add1 >+ guest2_max_adr ��� add1 <+ guest1_min_adr)``,
186    FULL_SIMP_TAC (srw_ss()) [guest1_min_adr_def, guest1_max_adr_def, guest2_min_adr_def, guest2_max_adr_def] THEN blastLib.BBLAST_TAC);
187
188
189(* what we assume when guests are running *)
190val mmu_requirements_def = Define `mmu_requirements state id =
191!add1 is_write u p m.
192  ((u,p,m) = permitted_byte add1
193                            is_write
194                            state.coprocessors.state.cp15.C1
195                            state.coprocessors.state.cp15.C2
196                            state.coprocessors.state.cp15.C3
197                            F
198                            state.memory)
199==>
200    u
201/\  ( ((add1 <=+ guest1_max_adr) /\ (add1 >=+  guest1_min_adr))   ==>    (p = (id=guest1)) )
202/\  ( ((add1 <=+ guest2_max_adr) /\ (add1 >=+  guest2_min_adr))   ==>    (p = (id=guest2)) )
203/\  ( ((add1 >+  guest2_max_adr) \/ (add1 <+   guest1_min_adr))   ==>    (~p) )
204/\  ((state.coprocessors.state.cp15.C2  && (0xFFFFC000w:bool[32])) >=+  0w)
205/\  ((state.coprocessors.state.cp15.C2  && (0xFFFFC000w:bool[32])) <+  guest1_min_adr)
206/\  (((state.coprocessors.state.cp15.C2  && (0xFFFFC000w:bool[32])) + 4w * 4095w + 3w) <+   guest1_min_adr)`;
207
208
209(* some consequences from the above for permitted_byte_pure *)
210val mmu_requirements_pure_def = Define `mmu_requirements_pure state id =
211!add1 is_write.
212( ((add1 <=+ guest1_max_adr) /\ (add1 >=+ guest1_min_adr))   ==>
213  ((id=guest1) = permitted_byte_pure add1
214                                is_write
215                                state.coprocessors.state.cp15.C1
216                                state.coprocessors.state.cp15.C2
217                                state.coprocessors.state.cp15.C3
218                                F
219                                state.memory))  /\
220( ((add1 <=+ guest2_max_adr ) /\ (add1 >=+ guest2_min_adr))   ==>
221  ((id=guest2) = permitted_byte_pure add1
222                                is_write
223                                state.coprocessors.state.cp15.C1
224                                state.coprocessors.state.cp15.C2
225                                state.coprocessors.state.cp15.C3
226                                F
227                                state.memory))  /\
228( ((add1 >+ guest2_max_adr ) \/ (add1 <+  guest1_min_adr))   ==>
229  (~ permitted_byte_pure add1
230                                is_write
231                                state.coprocessors.state.cp15.C1
232                                state.coprocessors.state.cp15.C2
233                                state.coprocessors.state.cp15.C3
234                                F
235                                state.memory))`;
236
237
238(* lemma: mmu_requirements_pure follows from mmu_requirements *)
239val mmu_requirements_simp = store_thm(
240    "mmu_requirements_simp",
241    ``!s g. mmu_requirements s g ==> mmu_requirements_pure s g``,
242    PURE_ONCE_REWRITE_TAC [mmu_requirements_pure_def]
243      THEN NTAC 5 STRIP_TAC
244      THEN Cases_on `permitted_byte add1 is_write s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory`
245      THEN pairLib.PairCases_on `r`
246      THEN NTAC 2 STRIP_TAC
247      THEN TRY DISCH_TAC
248      THENL[`q /\ (r0 = (g=guest1))` by METIS_TAC [mmu_requirements_def]
249              THEN METIS_TAC [permitted_byte_simp],
250           `q /\ (r0 = (g=guest2))` by METIS_TAC [mmu_requirements_def]
251              THEN METIS_TAC [permitted_byte_simp],
252           `q /\ ~r0` by METIS_TAC [mmu_requirements_def]
253              THEN METIS_TAC [permitted_byte_simp]
254           ]
255);
256
257
258(* lemma: mmu_requirements don't change by access list update *)
259
260val mmu_requirement_accesses_update_lem = store_thm(
261    "mmu_requirement_accesses_update_lem",
262    ``!add1 x s g.
263      ((mmu_requirements s g) = (mmu_requirements (s with accesses updated_by CONS (MEM_READ add1)) g))
264   /\ ((mmu_requirements s g) = (mmu_requirements (s with accesses updated_by CONS (MEM_WRITE add1 x)) g))``,
265    FULL_SIMP_TAC (srw_ss()) [mmu_requirements_def]);
266
267val mmu_requirement_accesses_update_lem2 = store_thm(
268    "mmu_requirement_accesses_update_lem2",
269    ``!add1 x s g.
270      ((mmu_requirements s g) = (mmu_requirements (s with accesses updated_by CONS (MEM_READ add1) o other) g))
271   /\ ((mmu_requirements s g) = (mmu_requirements (s with accesses updated_by CONS (MEM_WRITE add1 x) o other) g))``,
272    FULL_SIMP_TAC (srw_ss()) [mmu_requirements_def]);
273
274
275
276(* lemma: same setup -->  same access rights *)
277
278val same_setup_same_rights_lem = store_thm(
279    "same_setup_same_rights_lem",
280    ``! s1 s2 g add1 is_write.
281      mmu_requirements_pure s1 g ==>
282      mmu_requirements_pure s2 g
283    ==>
284      (permitted_byte_pure add1 is_write s1.coprocessors.state.cp15.C1
285                                        s1.coprocessors.state.cp15.C2
286                                        s1.coprocessors.state.cp15.C3
287                                        F s1.memory
288      = permitted_byte_pure add1 is_write s2.coprocessors.state.cp15.C1
289                                         s2.coprocessors.state.cp15.C2
290                                         s2.coprocessors.state.cp15.C3
291                                         F s2.memory)``,
292    REPEAT STRIP_TAC
293       THEN MP_TAC (SPEC ``add1:word32`` negated_and_or)
294       THEN MP_TAC (SPEC ``add1:word32`` address_border)
295       THEN FULL_SIMP_TAC (srw_ss()) [mmu_requirements_pure_def]
296       THEN METIS_TAC []);
297
298
299val same_setup_same_check_accesses_lem = store_thm(
300    "same_setup_same_check_accesses_lem",
301    ``! s1 s2 g accesses.
302      mmu_requirements_pure s1 g ==>
303      mmu_requirements_pure s2 g
304    ==>
305      (check_accesses_pure accesses s1.coprocessors.state.cp15.C1
306                                    s1.coprocessors.state.cp15.C2
307                                    s1.coprocessors.state.cp15.C3 F s1.memory
308      =check_accesses_pure accesses s2.coprocessors.state.cp15.C1
309                                    s2.coprocessors.state.cp15.C2
310                                    s2.coprocessors.state.cp15.C3 F s2.memory)``,
311    REPEAT STRIP_TAC
312       THEN Induct_on `accesses`
313       THEN PURE_ONCE_REWRITE_TAC [check_accesses_pure_def]
314       THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF]
315       THEN STRIP_TAC
316       THEN CASE_TAC
317       THEN ASSUME_TAC (SPECL [``s1:arm_state``, ``s2:arm_state``, ``g:word32``, ``c:word32``] same_setup_same_rights_lem)
318       THEN FULL_SIMP_TAC (srw_ss()) []);
319
320
321val same_setup_same_av_pure_lem = store_thm(
322    "same_setup_same_av_pure_lem",
323    ``! s1 s2 g.
324      mmu_requirements_pure s1 g ==>
325      mmu_requirements_pure s2 g ==>
326      (s1.accesses = s2.accesses)
327    ==>
328      (access_violation_pure s1 = access_violation_pure s2)``,
329    REPEAT STRIP_TAC
330       THEN RW_TAC (srw_ss()) [access_violation_pure_def]
331       THEN METIS_TAC [same_setup_same_check_accesses_lem]);
332
333
334
335(* === well-defined MMU setup allows (simpler) computation of access violation === *)
336
337val access_violation_req = store_thm (
338    "access_violation_req",
339    ``!s id. (mmu_requirements s id)
340      ==> (access_violation s = access_violation_pure s)``,
341    REPEAT STRIP_TAC
342      THEN Cond_rewrite.COND_REWRITE1_TAC (SPEC ``s:arm_state`` access_violation_simp_FST)
343      THEN FULL_SIMP_TAC (srw_ss()) [access_violation_full_def]
344      THEN  `!add1 is_write.
345            ((u,p,m) = (permitted_byte add1 is_write s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory))
346            ==> u` by METIS_TAC [mmu_requirements_def]
347     THEN  `!add1 is_write.
348            FST (permitted_byte add1 is_write s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory)`
349            by (RW_TAC (srw_ss()) []
350                  THEN Cases_on `permitted_byte add1 is_write s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory`
351                  THEN pairLib.PairCases_on `r`
352                  THEN FULL_SIMP_TAC (srw_ss()) []
353                  THEN METIS_TAC[mmu_requirements_def]
354                )
355     THEN METIS_TAC [ check_accesses_understand]);
356
357
358
359
360val same_setup_same_av_lem = store_thm(
361    "same_setup_same_av_lem",
362    ``! s1 s2 g.
363      mmu_requirements s1 g ==>
364      mmu_requirements s2 g ==>
365      (s1.accesses = s2.accesses)
366    ==>
367      (access_violation s1 = access_violation s2)``,
368    REPEAT STRIP_TAC
369       THEN IMP_RES_TAC access_violation_req
370       THEN IMP_RES_TAC mmu_requirements_simp
371       THEN ASSUME_TAC same_setup_same_av_pure_lem
372       THEN METIS_TAC []);
373
374(* malicious_read and malicious_write  *)
375
376val malicious_read = store_thm (
377    "malicious_read",
378    ``!s t address. (t = s with accesses updated_by CONS (MEM_READ address)) ==>
379                 (~ permitted_byte_pure address F s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory  \/
380                  ~ permitted_byte_pure address F t.coprocessors.state.cp15.C1 t.coprocessors.state.cp15.C2 t.coprocessors.state.cp15.C3 F t.memory)
381            ==>   access_violation_pure t``,
382    REPEAT STRIP_TAC
383      THEN `?restlist. t.accesses = (MEM_READ address)::restlist` by (EXISTS_TAC ``s.accesses`` THEN FULL_SIMP_TAC (srw_ss()) [])
384      THEN `t.memory = s.memory` by FULL_SIMP_TAC (srw_ss()) []
385      THEN `t.coprocessors = s.coprocessors` by FULL_SIMP_TAC (srw_ss()) []
386      THEN PURE_ONCE_REWRITE_TAC [access_violation_pure_def]
387      THEN PURE_ONCE_REWRITE_TAC [check_accesses_pure_def]
388      THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF]
389);
390
391
392val malicious_read2 = store_thm (
393    "malicious_read2",
394    ``!s t address. (t = s with accesses updated_by CONS (MEM_READ address) o other) ==>
395                 (~ permitted_byte_pure address F s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory  \/
396                  ~ permitted_byte_pure address F t.coprocessors.state.cp15.C1 t.coprocessors.state.cp15.C2 t.coprocessors.state.cp15.C3 F t.memory)
397            ==>   access_violation_pure t``,
398    REPEAT STRIP_TAC
399      THEN `?restlist. t.accesses = (MEM_READ address)::restlist` by (EXISTS_TAC ``(other (s.accesses)):(memory_access list)`` THEN FULL_SIMP_TAC (srw_ss()) [])
400      THEN `t.memory = s.memory` by FULL_SIMP_TAC (srw_ss()) []
401      THEN `t.coprocessors = s.coprocessors` by FULL_SIMP_TAC (srw_ss()) []
402      THEN PURE_ONCE_REWRITE_TAC [access_violation_pure_def]
403      THEN PURE_ONCE_REWRITE_TAC [check_accesses_pure_def]
404      THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF]);
405
406
407val malicious_write = store_thm (
408    "malicious_write",
409    ``!s t address value. (t = s with accesses updated_by CONS (MEM_WRITE address value)) ==>
410                 (~ permitted_byte_pure address T s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory  \/
411                  ~ permitted_byte_pure address T t.coprocessors.state.cp15.C1 t.coprocessors.state.cp15.C2 t.coprocessors.state.cp15.C3 F t.memory)
412            ==>   access_violation_pure t``,
413    REPEAT STRIP_TAC
414      THEN `?restlist. t.accesses = (MEM_WRITE address value)::restlist` by (EXISTS_TAC ``s.accesses`` THEN FULL_SIMP_TAC (srw_ss()) [])
415      THEN `t.memory = s.memory` by FULL_SIMP_TAC (srw_ss()) []
416      THEN `t.coprocessors = s.coprocessors` by FULL_SIMP_TAC (srw_ss()) []
417      THEN PURE_ONCE_REWRITE_TAC [access_violation_pure_def]
418      THEN PURE_ONCE_REWRITE_TAC [check_accesses_pure_def]
419      THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF]
420);
421
422
423
424(* predicate "word aligned around address add is readable" *)
425
426
427val aligned_word_readable_def = Define `aligned_word_readable s is_thumb add1 =
428 (  permitted_byte_pure (add1) F s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory
429       /\ (is_thumb ==> (  permitted_byte_pure (align(add1,2)) F s.coprocessors.state.cp15.C1
430                                                        s.coprocessors.state.cp15.C2
431                                                         s.coprocessors.state.cp15.C3 F s.memory
432                               /\ permitted_byte_pure (align (add1,2) + 1w) F s.coprocessors.state.cp15.C1
433                                                              s.coprocessors.state.cp15.C2
434                                                              s.coprocessors.state.cp15.C3 F s.memory))
435
436       /\ (~is_thumb ==> (  permitted_byte_pure (align(add1,4)) F s.coprocessors.state.cp15.C1
437                                                        s.coprocessors.state.cp15.C2
438                                                         s.coprocessors.state.cp15.C3 F s.memory
439                               /\ permitted_byte_pure (align (add1,4) + 1w) F s.coprocessors.state.cp15.C1
440                                                              s.coprocessors.state.cp15.C2
441                                                              s.coprocessors.state.cp15.C3 F s.memory
442                               /\ permitted_byte_pure (align (add1,4) + 2w) F s.coprocessors.state.cp15.C1
443                                                              s.coprocessors.state.cp15.C2
444                                                              s.coprocessors.state.cp15.C3 F s.memory
445                               /\ permitted_byte_pure (align (add1,4) + 3w) F s.coprocessors.state.cp15.C1
446                                                              s.coprocessors.state.cp15.C2
447                                                              s.coprocessors.state.cp15.C3 F s.memory)))`;
448
449
450val _ = export_theory();
451