1open HolKernel boolLib bossLib Parse; 2open MMU_SetupTheory MMUTheory arm_opsemTheory arm_seq_monadTheory arm_coretypesTheory arm_stepTheory; 3open tacticsLib; 4 5val _ = new_theory("inference_rules"); 6val _ = ParseExtras.temp_loose_equality() 7 8 9val let_ss = simpLib.mk_simpset [boolSimps.LET_ss] ; 10val comb_def = Define `comb invr1 invr2 invr3 = (!s. invr3 s = (invr1 s \/ invr2 s))`; 11val assert_mode_def = Define `assert_mode k s = (ARM_MODE s = k)`; 12 13 14(* ============= Untouched ==========================*) 15(* smc mode is not involved yet, also RName_LRmon,RName_SPmon*) 16 17val untouched_def = Define `untouched id state1 state2 = 18(state1.coprocessors = state2.coprocessors) 19 20/\ 21(state1.information = 22 state2.information) 23 24/\ 25 26 (! a. 27 (((id <> guest1) /\ (id<>guest2)) ==> 28 ((state1.memory a) = (state2.memory a))) 29 /\ 30 (((id = guest1) /\ ((a >+ (* UNSIGNED *) guest1_max_adr) \/ (a <+ (* UNSIGNED *) guest1_min_adr))) ==> 31((state1.memory a) = (state2.memory a))) 32 /\ 33 (((id = guest2) /\ ((a >+ (* UNSIGNED *) guest2_max_adr) \/ (a <+ (* UNSIGNED *) guest2_min_adr))) ==> 34((state1.memory a) = (state2.memory a)))) 35 36/\ 37 38((state1.psrs (0, CPSR)).F = (state2.psrs (0, CPSR)).F) 39 40/\ 41let user_regs = {RName_0usr; RName_1usr; RName_2usr; RName_3usr; RName_4usr; RName_5usr; 42 RName_6usr; RName_7usr; RName_8usr; RName_9usr; RName_10usr; RName_11usr; 43 RName_12usr; RName_SPusr; RName_LRusr; RName_PC} in 44let irq_regs = {RName_0usr; RName_1usr; RName_2usr; RName_3usr; RName_4usr; RName_5usr; 45 RName_6usr; RName_7usr; RName_8usr; RName_9usr; RName_10usr; RName_11usr; 46 RName_12usr; RName_SPusr; RName_LRusr; RName_PC; RName_SPirq; RName_LRirq} in 47let fiq_regs = {RName_0usr; RName_1usr; RName_2usr; RName_3usr; RName_4usr; RName_5usr; 48 RName_6usr; RName_7usr; RName_8usr; RName_9usr; RName_10usr; RName_11usr; 49 RName_12usr; RName_SPusr; RName_LRusr; RName_PC; RName_8fiq; RName_9fiq; 50 RName_10fiq; RName_11fiq; RName_12fiq; RName_SPfiq; RName_LRfiq} in 51let abort_regs = {RName_0usr; RName_1usr; RName_2usr; RName_3usr; RName_4usr; RName_5usr; 52 RName_6usr; RName_7usr; RName_8usr; RName_9usr; RName_10usr; RName_11usr; 53 RName_12usr; RName_SPusr; RName_LRusr; RName_PC; RName_SPabt; RName_LRabt} in 54let svc_regs = {RName_0usr; RName_1usr; RName_2usr; RName_3usr; RName_4usr; RName_5usr; 55 RName_6usr; RName_7usr; RName_8usr; RName_9usr; RName_10usr; RName_11usr; 56 RName_12usr; RName_SPusr; RName_LRusr; RName_PC; RName_SPsvc; RName_LRsvc} in 57let und_regs = {RName_0usr; RName_1usr; RName_2usr; RName_3usr; RName_4usr; RName_5usr; 58 RName_6usr; RName_7usr; RName_8usr; RName_9usr; RName_10usr; RName_11usr; 59 RName_12usr; RName_SPusr; RName_LRusr; RName_PC; RName_SPund; RName_LRund} in 60 61 62(((ARM_MODE state1 = 16w) /\ 63 (ARM_MODE state2 = 16w)) ==> 64 ((!reg . (reg NOTIN user_regs) 65 ==> (state1.registers (0, reg) = state2.registers (0, reg))) 66/\ 67(!psr . ((psr <> CPSR) ==> (state1.psrs (0, psr) = state2.psrs (0, psr)))) 68/\ 69((state1.psrs (0, CPSR)).I = (state2.psrs (0, CPSR)).I) 70)) 71 72/\ 73((((ARM_MODE state1 = 16w) /\ 74 (ARM_MODE state2 = 17w)) 75\/ 76((ARM_MODE state1 = 17w) /\ 77 (ARM_MODE state2 = 17w))) ==> 78 ((!reg . ((reg NOTIN user_regs) /\ (reg NOTIN fiq_regs)) 79 ==> (state1.registers (0, reg) = state2.registers (0, reg))) 80/\ 81(!psr . ((psr <> CPSR) /\ (psr <> SPSR_fiq)) ==> (state1.psrs (0, psr) = state2.psrs (0, psr)))) 82) 83 84/\ 85((((ARM_MODE state1 = 16w) /\ 86 (ARM_MODE state2 = 18w)) 87\/ 88((ARM_MODE state1 = 18w) /\ 89 (ARM_MODE state2 = 18w))) ==> 90 ((!reg . ((reg NOTIN user_regs) /\ (reg NOTIN irq_regs)) 91 ==> (state1.registers (0, reg) = state2.registers (0, reg))) 92/\ 93(!psr . ((psr <> CPSR) /\ (psr <> SPSR_irq)) ==> (state1.psrs (0, psr) = state2.psrs (0, psr))))) 94/\ 95 96(*this is also the mode of reset, check again*) 97((((ARM_MODE state1 = 16w) /\ 98 (ARM_MODE state2 = 19w)) 99\/ 100((ARM_MODE state1 = 19w) /\ 101 (ARM_MODE state2 = 19w))) ==> 102 ((!reg . ((reg NOTIN user_regs) /\ (reg NOTIN svc_regs)) 103 ==> (state1.registers (0, reg) = state2.registers (0, reg))) 104/\ 105(!psr . ((psr <> CPSR) /\ (psr <> SPSR_svc)) ==> (state1.psrs (0, psr) = state2.psrs (0, psr))))) 106/\ 107 108((((ARM_MODE state1 = 16w) /\ 109 (ARM_MODE state2 = 23w)) 110\/ 111((ARM_MODE state1 = 23w) /\ 112 (ARM_MODE state2 = 23w))) ==> 113 ((!reg . ((reg NOTIN user_regs) /\ (reg NOTIN abort_regs)) 114 ==> (state1.registers (0, reg) = state2.registers (0, reg))) 115/\ 116(!psr . ((psr <> CPSR) /\ (psr <> SPSR_abt)) ==> (state1.psrs (0, psr) = state2.psrs (0, psr))))) 117/\ 118 119((((ARM_MODE state1 = 16w) /\ 120 (ARM_MODE state2 = 27w)) 121\/ 122((ARM_MODE state1 = 27w) /\ 123 (ARM_MODE state2 = 27w))) ==> 124 ((!reg . ((reg NOTIN user_regs) /\ (reg NOTIN und_regs)) 125 ==> (state1.registers (0, reg) = state2.registers (0, reg))) 126/\ 127(!psr . ((psr <> CPSR) /\ (psr <> SPSR_und)) ==> (state1.psrs (0, psr) = state2.psrs (0, psr))))) 128`; 129 130(* only for arm_next 131val priv_mode_similar_def = 132 Define `priv_mode_similar (g:bool[32]) state1 state2 = 133 (ARM_MODE state2 <> 16w) ==> 134 (let (lr_reg,spsr) = case (ARM_MODE state2) of 135 17w -> (RName_LRfiq,SPSR_fiq) 136 || 18w -> (RName_LRirq,SPSR_irq) 137 || 19w -> (RName_LRsvc,SPSR_svc) 138 || 22w -> (RName_LRmon,SPSR_mon) 139 || 23w -> (RName_LRabt,SPSR_abt) 140 || 27w -> (RName_LRund,SPSR_und) 141 || _ -> (RName_LRusr,CPSR) 142 in 143 (state1.registers(0,lr_reg) = state2.registers(0,lr_reg)) 144 /\ 145 (state1.psrs(0,spsr) = state2.psrs(0,spsr))) 146 147 `;*) 148 149 150val get_spsr_by_mode_def = 151 Define `get_spsr_by_mode (mode:bool[5]) = 152 case (mode) of 153 17w => SPSR_fiq 154 | 18w => SPSR_irq 155 | 19w => SPSR_svc 156 | 22w => SPSR_mon 157 | 23w => SPSR_abt 158 | 27w => SPSR_und 159 | _ => CPSR`; 160 161val get_lr_by_mode_def = 162 Define `get_lr_by_mode (mode:bool[5]) = 163 case (mode) of 164 17w => RName_LRfiq 165 | 18w => RName_LRirq 166 | 19w => RName_LRsvc 167 | 22w => RName_LRmon 168 | 23w => RName_LRabt 169 | 27w => RName_LRund 170 | _ => RName_LRusr `; 171 172val priv_mode_similar_def = 173 Define `priv_mode_similar (g:bool[32]) state1 state2 = 174 (ARM_MODE state2 <> 16w) ==> 175 (let (lr_reg,spsr) = (get_lr_by_mode(ARM_MODE state2) , 176get_spsr_by_mode(ARM_MODE state2)) 177 in 178 (state1.registers(0,lr_reg) = state2.registers(0,lr_reg)) 179 /\ 180 (state1.psrs(0,spsr) = state2.psrs(0,spsr))) 181 182 `; 183 184 185val untouched_trans = store_thm ( 186 "untouched_trans", 187 ``!g st1 st2 st3 . 188 (untouched g st1 st2 ) ==> (untouched g st2 st3 ) 189 ==> ((ARM_MODE st3 = ARM_MODE st2) \/ 190 (ARM_MODE st1 = ARM_MODE st2)) ==> 191 (untouched g st1 st3 )``, 192 RW_TAC (srw_ss()) [untouched_def] 193 THEN FULL_SIMP_TAC (let_ss) [] 194 THEN RW_TAC (srw_ss()) [] 195); 196 197val untouched_memory_eq_lem = store_thm( 198 "untouched_memory_eq_lem", 199 ``!s1 s2 g . (untouched g s1 s2 ) ==> 200 (!addr. (addr <+ (*UNSIGNED*) guest1_min_adr (*ADR*)) ==> (s1.memory addr = s2.memory addr))``, 201 REPEAT STRIP_TAC 202 THEN Cases_on `(g<>guest1) /\ (g<>guest2)` 203 THENL [ALL_TAC, IMP_RES_TAC address_trans (*ADR*)] 204 THEN FULL_SIMP_TAC (let_ss) [untouched_def] 205 THEN FULL_SIMP_TAC (srw_ss()) [untouched_def]); 206 207 208val untouched_permissions_lem = store_thm( 209 "untouched_permissions_lem", 210 ``!s1 s2 g priv . 211 (mmu_requirements s1 g) ==> 212 (untouched g s1 s2 ) 213 ==> (!addr isw c1 c3. 214 (permitted_byte addr isw c1 s1.coprocessors.state.cp15.C2 c3 priv s1.memory 215 = permitted_byte addr isw c1 s1.coprocessors.state.cp15.C2 c3 priv s2.memory))``, 216 REPEAT STRIP_TAC 217 THEN IMP_RES_TAC untouched_memory_eq_lem 218 THEN FULL_SIMP_TAC (srw_ss()) [permitted_byte_def] 219 THEN UNDISCH_TAC ``mmu_requirements s1 g`` 220 THEN PURE_ONCE_REWRITE_TAC [mmu_requirements_def] 221 THEN STRIP_TAC 222 THEN Cases_on `permitted_byte addr F s1.coprocessors.state.cp15.C1 s1.coprocessors.state.cp15.C2 s1.coprocessors.state.cp15.C3 F s1.memory` 223 THEN Cases_on `r` 224 THEN PAT_X_ASSUM (``!A1 A2 A3 A4 A5. (B ==> C)``) (fn th => (MP_TAC (SPECL [``addr:word32``, ``F``,``q:bool``, ``q':bool``, ``r':string``] th))) 225 THEN RW_TAC (srw_ss()) [read_mem32_def] 226 THEN `content_of_sd = content_of_sd'` by 227 (UNABBREV_ALL_TAC 228 THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF, read_mem32_def] 229 THEN IMP_RES_TAC (blastLib.BBLAST_PROVE ``!(addr:word32). ((0xFFFFC000w && s2.coprocessors.state.cp15.C2) >=+ (*UNSIGNED*) 0w) ==> ((0xFFFFC000w && s2.coprocessors.state.cp15.C2) <+ (*UNSIGNED*) (guest1_min_adr:word32) (*ADR*)) ==> ((0xFFFFC000w && s2.coprocessors.state.cp15.C2) + 16383w <+ (*UNSIGNED*) guest1_min_adr (*ADR*)) ==> 230 (((0xFFFFC000w && s2.coprocessors.state.cp15.C2) + 4w *(addr >>> (*UNSIGNED*) 20) <+ (*UNSIGNED*) guest1_min_adr (*ADR*)) /\ 231 ((0xFFFFC000w && s2.coprocessors.state.cp15.C2) + 4w *(addr >>> (*UNSIGNED*) 20) + 1w <+ (*UNSIGNED*) guest1_min_adr (*ADR*)) /\ 232 ((0xFFFFC000w && s2.coprocessors.state.cp15.C2) + 4w *(addr >>> (*UNSIGNED*) 20) + 2w <+ (*UNSIGNED*)guest1_min_adr (*ADR*)) /\ 233 ((0xFFFFC000w && s2.coprocessors.state.cp15.C2) + 4w *(addr >>> (*UNSIGNED*) 20) + 3w <+ (*UNSIGNED*) guest1_min_adr (*ADR*)) )``) 234 THEN METIS_TAC []) 235 THEN UNABBREV_ALL_TAC 236 THEN METIS_TAC []); 237 238 239val untouched_permissions_lem2 = store_thm( 240 "untouched_permissions_lem2", 241 ``!s1 s2 g priv . 242 (mmu_requirements s1 g) ==> 243 (untouched g s1 s2 ) 244 ==> (!addr isw. 245 (permitted_byte addr isw s1.coprocessors.state.cp15.C1 s1.coprocessors.state.cp15.C2 s1.coprocessors.state.cp15.C3 priv s1.memory 246 = permitted_byte addr isw s2.coprocessors.state.cp15.C1 s2.coprocessors.state.cp15.C2 s2.coprocessors.state.cp15.C3 priv s2.memory))``, 247 REPEAT STRIP_TAC 248 THEN IMP_RES_TAC (SPECL [``s1:arm_state``, ``s2:arm_state``, ``g:word32``] untouched_permissions_lem) 249 THEN FULL_SIMP_TAC (srw_ss()) [untouched_def] 250 THEN METIS_TAC []); 251 252 253val untouched_mmu_setup_lem = store_thm( 254 "untouched_mmu_setup_lem", 255 ``!s1 s2 g . 256 (mmu_requirements s1 g) ==> 257 (untouched g s1 s2 ) 258 ==> 259 (mmu_requirements s2 g)``, 260 REPEAT STRIP_TAC 261 THEN IMP_RES_TAC (SPECL [``s1:arm_state``, ``s2:arm_state``, ``g:word32``] untouched_permissions_lem) 262 THEN UNDISCH_TAC ``mmu_requirements s1 g`` 263 THEN FULL_SIMP_TAC (srw_ss()) [untouched_def] 264 THEN PURE_ONCE_REWRITE_TAC [mmu_requirements_def] 265 THEN METIS_TAC []); 266 267 268val trivially_untouched_mmu_setup_lem = store_thm( 269 "trivially_untouched_mmu_setup_lem", 270 ``!s t gst. (s.coprocessors = t.coprocessors) ==> 271 (s.memory = t.memory) 272 ==> 273 (mmu_requirements s gst = mmu_requirements t gst)``, 274 RW_TAC (srw_ss()) [mmu_requirements_def]); 275 276 277val trivially_untouched_av_lem = store_thm( 278 "trivially_untouched_av_lem", 279 ``!s t gst. (mmu_requirements s gst) ==> 280 (s.coprocessors = t.coprocessors) ==> 281 (s.memory = t.memory) ==> 282 (s.accesses = t.accesses) 283 ==> (access_violation s = access_violation t)``, 284 REPEAT STRIP_TAC 285 THEN `mmu_requirements t gst` by IMP_RES_TAC trivially_untouched_mmu_setup_lem 286 THEN IMP_RES_TAC access_violation_req 287 THEN RW_TAC (srw_ss()) [access_violation_pure_def]); 288 289 290val trivially_untouched_mmu_setup_lem2 = store_thm( 291 "trivially_untouched_mmu_setup_lem2", 292 ``!s t gst. (s.coprocessors.state.cp15.C1 = t.coprocessors.state.cp15.C1) ==> 293 (s.coprocessors.state.cp15.C2 = t.coprocessors.state.cp15.C2) ==> 294 (s.coprocessors.state.cp15.C3 = t.coprocessors.state.cp15.C3) ==> 295 (s.memory = t.memory) 296 ==> 297 (mmu_requirements s gst = mmu_requirements t gst)``, 298 RW_TAC (srw_ss()) [mmu_requirements_def]); 299 300 301 302 303 304val trivially_untouched_av_lem2 = store_thm( 305 "trivially_untouched_av_lem2", 306 ``!s t gst. (mmu_requirements s gst) ==> 307 (s.coprocessors.state.cp15.C1 = t.coprocessors.state.cp15.C1) ==> 308 (s.coprocessors.state.cp15.C2 = t.coprocessors.state.cp15.C2) ==> 309 (s.coprocessors.state.cp15.C3 = t.coprocessors.state.cp15.C3) ==> 310 (s.memory = t.memory) ==> 311 (s.accesses = t.accesses) 312 ==> (access_violation s = access_violation t)``, 313 REPEAT STRIP_TAC 314 THEN `mmu_requirements t gst` by IMP_RES_TAC trivially_untouched_mmu_setup_lem2 315 THEN IMP_RES_TAC access_violation_req 316 THEN RW_TAC (srw_ss()) [access_violation_pure_def]); 317 318 319 320(* ============= Similar ==========================*) 321 322val equal_user_register_def = Define `equal_user_register s t = 323(! reg. reg IN {RName_0usr; RName_1usr; RName_2usr; RName_3usr; RName_4usr; RName_5usr; 324 RName_6usr; RName_7usr; RName_8usr; RName_9usr; RName_10usr; RName_11usr; 325 RName_12usr; RName_SPusr; RName_LRusr; RName_PC} 326 ==> (s.registers (0, reg) = t.registers (0, reg)))`; 327 328 329 330val similar_def = Define `similar gst s1 s2 = 331(! addr. 332 (((addr <=+ (*UNSIGNED*) guest1_max_adr) /\ (addr >=+ (*UNSIGNED*) guest1_min_adr) /\ (gst = guest1)) ==> 333 ((s1.memory addr) = (s2.memory addr))) 334 /\ 335 (((addr <=+ (*UNSIGNED*) guest2_max_adr) /\ (addr >=+ (*UNSIGNED*) guest2_min_adr) /\ (gst = guest2)) ==> 336 ((s1.memory addr) = (s2.memory addr)))) /\ 337((s1.psrs (0,CPSR)= s2.psrs (0,CPSR))) /\ 338(equal_user_register s1 s2) /\ 339(s1.coprocessors.state = s2.coprocessors.state) /\ 340 341(s1.interrupt_wait 0 = s2.interrupt_wait 0) /\ 342 343(access_violation s1 = access_violation s2) /\ 344(s1.information = s2.information) /\ 345 346(* to be checked*) 347(s1.monitors = s2.monitors) 348 /\ 349(s1.event_register = s2.event_register) 350 351`; 352 353 354val similar_refl = store_thm( 355 "similar_refl", 356 ``!gst s . similar gst s s``, 357 RW_TAC (srw_ss()) [similar_def, equal_user_register_def]); 358 359 360(*********************** preserve ****************************) 361 362val trans_fun_def = Define `trans_fun uf = 363!g st1 st2 st3 . 364 (uf g st1 st2) ==> 365 (uf g st2 st3) 366 ==> (uf g st1 st3)`; 367 368 369val preserve_relation_mmu_def = 370Define `preserve_relation_mmu comp invr1 invr2 f y = 371 !g s1 s2 . 372 mmu_requirements s1 g ==> 373 mmu_requirements s2 g ==> 374 similar g s1 s2 ==> 375 (y g s1 s2) ==> 376 invr1 s1 ==> 377 invr1 s2 ==> 378 ((?a s1' s2'.((comp s1 = ValueState a s1') /\ (comp s2 = ValueState a s2') /\ 379 (untouched g s1 s1' ) /\ 380 (untouched g s2 s2' ) /\ 381 (f g s1 s1') /\ 382 (f g s2 s2') /\ 383 (y g s1' s2') /\ 384 (invr2 s1') /\ 385 (invr2 s2') /\ 386 (similar g s1' s2'))) 387\/ (? e. (comp s1 = Error e) /\ (comp s2 = Error e)))`; 388 389 390 391val preserve_relation_mmu_abs_def = Define `preserve_relation_mmu_abs comp invr1 invr2 f y = 392 !c g s1 s2 . 393 mmu_requirements s1 g ==> 394 mmu_requirements s2 g ==> 395 similar g s1 s2 ==> 396 (y g s1 s2) ==> 397 invr1 s1 ==> 398 invr1 s2 ==> 399 ((?a s1' s2'.((comp c s1 = ValueState a s1') /\ (comp c s2 = ValueState a s2') /\ 400 (untouched g s1 s1' ) /\ 401 (untouched g s2 s2' ) /\ 402 (f g s1 s1') /\ 403 (f g s2 s2') /\ 404 (y g s1' s2') /\ 405 (invr2 s1') /\ 406 (invr2 s2') /\ 407 (similar g s1' s2'))) 408\/ (? e. (comp c s1 = Error e) /\ (comp c s2 = Error e)))`; 409 410val comb_rel_lem = store_thm ( 411 "comb_rel_lem", 412 ``!i1 i2 i3 s. (comb i1 i2 i3) 413 ==> ((i1 s) ==> (i3 s)) /\ ((i2 s) ==> (i3 s))``, 414 RW_TAC (srw_ss()) [comb_def]); 415 416val seqT_preserves_relation_up_proof = 417 (RW_TAC (srw_ss()) [arm_seq_monadTheory.seqT_def,arm_seq_monadTheory.constT_def,preserve_relation_mmu_def,preserve_relation_mmu_abs_def,trans_fun_def]) 418 THEN (UNDISCH_ALL_TAC 419 THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) [])) 420 THENL [UNDISCH_ALL_TAC 421 THEN RW_TAC (srw_ss()) [] 422 THEN FULL_SIMP_TAC (srw_ss()) [] 423THEN RES_TAC 424THEN IMP_RES_TAC untouched_trans 425 THEN FULL_SIMP_TAC (srw_ss()) [] 426THEN METIS_TAC [untouched_trans, comb_rel_lem], 427RW_TAC (srw_ss()) [] 428THEN RES_TAC 429 THEN RW_TAC (srw_ss()) [] 430 THEN FULL_SIMP_TAC (srw_ss()) [] 431 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 432 THEN FULL_SIMP_TAC (srw_ss()) [], 433RW_TAC (srw_ss()) [] 434THEN Cases_on `assert_mode k s2` 435THEN RES_TAC 436THEN FULL_SIMP_TAC (srw_ss()) [] 437THEN FULL_SIMP_TAC (srw_ss()) [] 438THEN FULL_SIMP_TAC (srw_ss()) [], 439RW_TAC (srw_ss()) [] 440THEN RES_TAC 441 THEN RW_TAC (srw_ss()) [] 442 THEN FULL_SIMP_TAC (srw_ss()) [] 443 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 444 THEN FULL_SIMP_TAC (srw_ss()) [], 445RW_TAC (srw_ss()) [] THEN FULL_SIMP_TAC (srw_ss()) [assert_mode_def,comb_def] 446THEN Cases_on `f2 a b` 447THEN Cases_on `f2 a' b'` 448(* THEN *) 449(* SPEC_ASSUM_TAC (``���(c:'a) (s1:arm_state) (s2:arm_state) (x:'b). X ==> Y``, [``a:'a``]) *) 450THEN (NTAC 2 (RES_TAC 451THEN IMP_RES_TAC untouched_trans 452 THEN FULL_SIMP_TAC (srw_ss()) [] 453THEN IMP_RES_TAC untouched_mmu_setup_lem 454THEN 455TRY (PAT_X_ASSUM ``!c g' s1'' s2''. X`` (fn th => ASSUME_TAC (SPECL [``a:'a``, ``g:bool[32]``, ``b:arm_state``, ``b':arm_state``] th))) 456THEN 457(TRY (PAT_X_ASSUM `` ���g st1 st2 st3. X`` (fn th => ASSUME_TAC (SPECL [ ``g:bool[32]``, ``s1:arm_state``, ``b:arm_state``, ``b'':arm_state``] th) THEN ASSUME_TAC (SPECL [ ``g:bool[32]``, ``s2:arm_state``, ``b':arm_state``, ``b''':arm_state``] th)))) 458 THEN UNDISCH_ALL_TAC 459 THEN RW_TAC (srw_ss()) [] 460 THEN FULL_SIMP_TAC (srw_ss()) [])) 461THEN METIS_TAC [], 462RW_TAC (srw_ss()) [] 463THEN RES_TAC 464THEN FULL_SIMP_TAC (srw_ss()) [] 465THEN FULL_SIMP_TAC (srw_ss()) [], 466RW_TAC (srw_ss()) [] 467THEN Cases_on `assert_mode k s2` 468THEN RES_TAC 469THEN FULL_SIMP_TAC (srw_ss()) [] 470THEN FULL_SIMP_TAC (srw_ss()) [] 471THEN FULL_SIMP_TAC (srw_ss()) [], 472RW_TAC (srw_ss()) [] 473THEN RES_TAC 474THEN FULL_SIMP_TAC (srw_ss()) [] 475THEN FULL_SIMP_TAC (srw_ss()) [], 476RW_TAC (srw_ss()) [] 477THEN RES_TAC 478THEN FULL_SIMP_TAC (srw_ss()) [] 479THEN FULL_SIMP_TAC (srw_ss()) []]; 480 481val seqT_preserves_relation_up1_thm = 482 store_thm ("seqT_preserves_relation_up1_thm", 483 ``! f1 f2 k k' invr23 uf uy. 484 (comb (assert_mode k) (assert_mode k') invr23) ==> 485 (trans_fun uf) ==> 486 (preserve_relation_mmu f1 (assert_mode k) (assert_mode k) uf uy) ==> 487 (preserve_relation_mmu_abs f2 (assert_mode k) (assert_mode k') uf uy) ==> 488 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) invr23 uf uy) 489``, 490 seqT_preserves_relation_up_proof); 491 492 493 494val seqT_preserves_relation_up2_thm = 495 store_thm ("seqT_preserves_relation_up2_thm", 496 ``! f1 f2 k k' uf uy. 497 (trans_fun uf) ==> 498 (preserve_relation_mmu f1 (assert_mode k) (assert_mode k') uf uy) ==> 499 (preserve_relation_mmu_abs f2 (assert_mode k') (assert_mode k') uf uy) ==> 500 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) (assert_mode k') uf uy) 501``, 502seqT_preserves_relation_up_proof ); 503 504 505val seqT_preserves_relation_uc_thm = 506 store_thm ("seqT_preserves_relation_uc_thm", 507 ``! f1 f2 k k' comb_inv uf uy. 508 (comb (assert_mode k) (assert_mode k') comb_inv) ==> 509 (trans_fun uf) ==> 510 (preserve_relation_mmu f1 (assert_mode k) (assert_mode k) uf uy) ==> 511 (preserve_relation_mmu_abs f2 (assert_mode k) (comb_inv) uf uy) ==> 512 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) comb_inv uf uy) 513``, 514 (RW_TAC (srw_ss()) [arm_seq_monadTheory.seqT_def,arm_seq_monadTheory.constT_def,preserve_relation_mmu_def,preserve_relation_mmu_abs_def,trans_fun_def]) 515 THEN (UNDISCH_ALL_TAC 516 THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) [])) 517 THENL [UNDISCH_ALL_TAC 518 THEN RW_TAC (srw_ss()) [] 519 THEN FULL_SIMP_TAC (srw_ss()) [] 520THEN RES_TAC 521THEN IMP_RES_TAC untouched_trans 522 THEN FULL_SIMP_TAC (srw_ss()) [] 523THEN METIS_TAC [untouched_trans, comb_rel_lem], 524RW_TAC (srw_ss()) [] 525THEN RES_TAC 526 THEN RW_TAC (srw_ss()) [] 527 THEN FULL_SIMP_TAC (srw_ss()) [] 528 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 529 THEN FULL_SIMP_TAC (srw_ss()) [], 530RW_TAC (srw_ss()) [] 531THEN Cases_on `assert_mode k s2` 532THEN RES_TAC 533THEN FULL_SIMP_TAC (srw_ss()) [] 534THEN FULL_SIMP_TAC (srw_ss()) [] 535THEN FULL_SIMP_TAC (srw_ss()) [], 536RW_TAC (srw_ss()) [] 537THEN RES_TAC 538 THEN RW_TAC (srw_ss()) [] 539 THEN FULL_SIMP_TAC (srw_ss()) [] 540 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 541 THEN FULL_SIMP_TAC (srw_ss()) [], 542RW_TAC (srw_ss()) [] THEN FULL_SIMP_TAC (srw_ss()) [assert_mode_def,comb_def] 543THEN Cases_on `f2 a b` 544THEN Cases_on `f2 a' b'` 545THEN (NTAC 2 (RES_TAC 546THEN IMP_RES_TAC untouched_trans 547 THEN FULL_SIMP_TAC (srw_ss()) [] 548THEN IMP_RES_TAC untouched_mmu_setup_lem 549THEN 550TRY (PAT_X_ASSUM ``!c g' s1'' s2''. X`` (fn th => ASSUME_TAC (SPECL [``a:'a``, ``g:bool[32]``, ``b:arm_state``, ``b':arm_state``] th))) 551THEN 552(TRY (PAT_X_ASSUM `` ���g st1 st2 st3. X`` (fn th => ASSUME_TAC (SPECL [ ``g:bool[32]``, ``s1:arm_state``, ``b:arm_state``, ``b'':arm_state``] th) THEN ASSUME_TAC (SPECL [ ``g:bool[32]``, ``s2:arm_state``, ``b':arm_state``, ``b''':arm_state``] th)))) 553 THEN UNDISCH_ALL_TAC 554 THEN RW_TAC (srw_ss()) [] 555 THEN FULL_SIMP_TAC (srw_ss()) [])), 556RW_TAC (srw_ss()) [] 557THEN RES_TAC 558THEN FULL_SIMP_TAC (srw_ss()) [] 559THEN FULL_SIMP_TAC (srw_ss()) [], 560RW_TAC (srw_ss()) [] 561THEN Cases_on `assert_mode k s2` 562THEN RES_TAC 563THEN FULL_SIMP_TAC (srw_ss()) [] 564THEN FULL_SIMP_TAC (srw_ss()) [] 565THEN FULL_SIMP_TAC (srw_ss()) [], 566RW_TAC (srw_ss()) [] 567THEN RES_TAC 568THEN FULL_SIMP_TAC (srw_ss()) [] 569THEN FULL_SIMP_TAC (srw_ss()) [], 570RW_TAC (srw_ss()) [] 571THEN RES_TAC 572THEN FULL_SIMP_TAC (srw_ss()) [] 573THEN FULL_SIMP_TAC (srw_ss()) []]); 574 575 576val seqT_preserves_relation_uu_thm = 577 store_thm ("seqT_preserves_relation_uu_thm", 578 ``! f1 f2 k uf uy. 579 (trans_fun uf) ==> 580 (preserve_relation_mmu f1 (assert_mode k) (assert_mode k) uf uy) ==> 581 (preserve_relation_mmu_abs f2 (assert_mode k) (assert_mode k) uf uy) ==> 582 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) (assert_mode k) uf uy) 583``, 584 (RW_TAC (srw_ss()) [arm_seq_monadTheory.seqT_def,arm_seq_monadTheory.constT_def,preserve_relation_mmu_def,preserve_relation_mmu_abs_def,trans_fun_def]) 585 THEN (UNDISCH_ALL_TAC 586 THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) [])) 587 THENL [UNDISCH_ALL_TAC 588 THEN RW_TAC (srw_ss()) [] 589 THEN FULL_SIMP_TAC (srw_ss()) [] 590 THEN RES_TAC 591 THEN IMP_RES_TAC untouched_trans 592 THEN FULL_SIMP_TAC (srw_ss()) [] 593 THEN METIS_TAC [untouched_trans, comb_rel_lem], 594 RW_TAC (srw_ss()) [] 595 THEN RES_TAC 596 THEN RW_TAC (srw_ss()) [] 597 THEN FULL_SIMP_TAC (srw_ss()) [] 598 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 599 THEN FULL_SIMP_TAC (srw_ss()) [], 600 RW_TAC (srw_ss()) [] 601 THEN Cases_on `assert_mode k s2` 602 THEN RES_TAC 603 THEN FULL_SIMP_TAC (srw_ss()) [] 604 THEN FULL_SIMP_TAC (srw_ss()) [] 605 THEN FULL_SIMP_TAC (srw_ss()) [], 606 RW_TAC (srw_ss()) [] 607 THEN RES_TAC 608 THEN RW_TAC (srw_ss()) [] 609 THEN FULL_SIMP_TAC (srw_ss()) [] 610 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 611 THEN FULL_SIMP_TAC (srw_ss()) [], 612RW_TAC (srw_ss()) [] THEN FULL_SIMP_TAC (srw_ss()) [assert_mode_def,comb_def,trans_fun_def] 613THEN Cases_on `f2 a b` 614THEN Cases_on `f2 a' b'` 615THEN 616SPEC_ASSUM_TAC (``���(c:'a) (s1:arm_state) (s2:arm_state) (x:'b). X ==> Y``, [``a:'a``]) 617THEN (NTAC 2 (RES_TAC 618THEN IMP_RES_TAC untouched_trans 619 THEN FULL_SIMP_TAC (srw_ss()) [] 620THEN IMP_RES_TAC untouched_mmu_setup_lem 621THEN 622TRY (PAT_X_ASSUM ``!c g' s1'' s2''. X`` (fn th => ASSUME_TAC (SPECL [``a:'a``, ``g:bool[32]``, ``b:arm_state``, ``b':arm_state``] th))) 623 THEN UNDISCH_ALL_TAC 624 THEN RW_TAC (srw_ss()) [] 625 THEN FULL_SIMP_TAC (srw_ss()) [])), 626RW_TAC (srw_ss()) [] 627THEN RES_TAC 628THEN FULL_SIMP_TAC (srw_ss()) [] 629THEN FULL_SIMP_TAC (srw_ss()) [], 630RW_TAC (srw_ss()) [] 631THEN Cases_on `assert_mode k s2` 632THEN RES_TAC 633THEN FULL_SIMP_TAC (srw_ss()) [] 634THEN FULL_SIMP_TAC (srw_ss()) [] 635THEN FULL_SIMP_TAC (srw_ss()) [], 636RW_TAC (srw_ss()) [] 637THEN RES_TAC 638THEN FULL_SIMP_TAC (srw_ss()) [] 639THEN FULL_SIMP_TAC (srw_ss()) [], 640RW_TAC (srw_ss()) [] 641THEN RES_TAC 642THEN FULL_SIMP_TAC (srw_ss()) [] 643THEN FULL_SIMP_TAC (srw_ss()) []]); 644 645 646val reflexive_comp_def = Define `reflexive_comp f invr = 647 ! s g. (invr s) ==> f g s s`; 648 649 650val condT_preserves_relation_thm = store_thm("condT_preserves_relation_thm", 651``! b f invr1:(arm_state -> bool) uf uy. 652 (reflexive_comp uf invr1) ==> 653 (preserve_relation_mmu f invr1 invr1 uf uy) ==> 654 (preserve_relation_mmu (condT b f ) invr1 invr1 uf uy)``, 655(RW_TAC (srw_ss()) [preserve_relation_mmu_def,condT_def,similar_def,constT_def,untouched_def,reflexive_comp_def] ) 656THEN (RW_TAC (srw_ss()) [] )); 657 658val first_abs_lemma = store_thm ("first_abs_lemma", 659``(!f g i1 i2 uf uy. (f=g) ==> ((preserve_relation_mmu f i1 i2 uf uy) = 660 (preserve_relation_mmu g i1 i2 uf uy)))``, 661 RW_TAC (srw_ss()) []); 662 663 664val second_abs_lemma = store_thm ("second_abs_lemma", 665``! f i1 i2 uf uy. (! y. preserve_relation_mmu (f y) i1 i2 uf uy) = 666 preserve_relation_mmu_abs f i1 i2 uf uy``, 667 RW_TAC (srw_ss()) [preserve_relation_mmu_def,preserve_relation_mmu_abs_def]); 668 669 670val constT_preserves_relation_thm = store_thm( 671 "constT_preserves_relation_thm", 672 ``!invr:(arm_state->bool) x uf uy. (reflexive_comp uf invr) ==> 673 preserve_relation_mmu (constT x) invr invr uf uy``, 674 RW_TAC (srw_ss()) [constT_def, preserve_relation_mmu_def, untouched_def, similar_def,reflexive_comp_def] THEN 675RW_TAC (srw_ss()) [] ); 676 677 678val parT_alternative_thm = store_thm( 679 "parT_alternative_thm", 680 ``!(f1:'a M) (f2:'b M) s. ((f1 ||| f2) s ) = (case f1 s of ValueState x t => 681 if access_violation t then ValueState (ARB:'a#'b) t else (f2 >>= (\y. constT (x,y))) t | Error e => Error e)``, 682 RW_TAC (srw_ss()) [arm_seq_monadTheory.parT_def, arm_seq_monadTheory.constT_def, arm_seq_monadTheory.seqT_def]); 683 684val parT_latter_part_hlem = store_thm ( 685 "parT_latter_part_hlem", 686 ``!f2 i2 i3 (x:'a) uf uy. (preserve_relation_mmu f2 i2 i3 uf uy) ==> 687 preserve_relation_mmu (f2 >>= (��y. constT (x,y))) i2 i3 uf uy``, 688 REPEAT STRIP_TAC 689 THEN ASSUME_TAC (SPEC ``i3:arm_state->bool`` constT_preserves_relation_thm) 690 THEN UNDISCH_ALL_TAC 691 THEN RW_TAC (srw_ss()) [seqT_def,constT_def,preserve_relation_mmu_def,preserve_relation_mmu_abs_def] 692 THEN (UNDISCH_ALL_TAC THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) [])) 693 THEN FIRST_PROVE [ 694 RW_TAC (srw_ss()) [] 695 THEN Cases_on `i2 s2` 696 THEN RES_TAC 697 THEN (NTAC 3 (FULL_SIMP_TAC (srw_ss()) [])), 698 RW_TAC (srw_ss()) [] 699 THEN RES_TAC 700 THEN RW_TAC (srw_ss()) [] 701 THEN FULL_SIMP_TAC (srw_ss()) [] 702 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 703 THEN FULL_SIMP_TAC (srw_ss()) [], 704 RW_TAC (srw_ss()) [] 705 THEN FULL_SIMP_TAC (srw_ss()) [] 706 THEN Cases_on `f2 s1` 707 THEN Cases_on `f2 s2` 708 THEN (NTAC 2 (RES_TAC 709 THEN IMP_RES_TAC untouched_trans 710 THEN FULL_SIMP_TAC (srw_ss()) [] 711 THEN IMP_RES_TAC untouched_mmu_setup_lem 712 THEN UNDISCH_ALL_TAC 713 THEN RW_TAC (srw_ss()) [] 714 THEN FULL_SIMP_TAC (srw_ss()) [])) 715 THEN METIS_TAC []]); 716 717val parT_preserves_relation_up_thm = store_thm("parT_preserves_relation_up_thm", 718 `` ! f1 f2 k k' invr23 uf uy. 719 (trans_fun uf) ==> (comb (assert_mode k) (assert_mode k') invr23) ==> 720 (preserve_relation_mmu f1 (assert_mode k) (assert_mode k) uf uy) ==> 721 (preserve_relation_mmu f2 (assert_mode k) (assert_mode k') uf uy) ==> 722 (preserve_relation_mmu (parT f1 f2) (assert_mode k) invr23 uf uy) ``, 723 REPEAT STRIP_TAC 724 THEN IMP_RES_TAC parT_latter_part_hlem 725 THEN WEAKEN_TAC is_forall 726 THEN THROW_ONE_AWAY_TAC ``preserve_relation_mmu (*II*) f2 (assert_mode k) (assert_mode k') uf uy`` 727 THEN UNDISCH_ALL_TAC 728 THEN RW_TAC (srw_ss()) [parT_alternative_thm, preserve_relation_mmu_def,trans_fun_def] 729 THEN UNDISCH_ALL_TAC 730 THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) [comb_def]) 731 THEN FIRST_PROVE [ 732 RW_TAC (srw_ss()) [] 733 THEN Cases_on `(assert_mode k) s2` 734 THEN RES_TAC 735 THEN (NTAC 3 (FULL_SIMP_TAC (srw_ss()) [])), 736 RW_TAC (srw_ss()) [] 737 THEN RES_TAC 738 THEN RW_TAC (srw_ss()) [] 739 THEN FULL_SIMP_TAC (srw_ss()) [] 740 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 741 THEN FULL_SIMP_TAC (srw_ss()) [], 742 ASSERT_ASSUM_TAC ``access_violation b`` 743 THEN UNDISCH_ALL_TAC 744 THEN RW_TAC (srw_ss()) [] 745 THEN FULL_SIMP_TAC (srw_ss()) [] 746 THEN RES_TAC 747 THEN IMP_RES_TAC untouched_trans 748 THEN FULL_SIMP_TAC (srw_ss()) [] 749 THEN METIS_TAC [untouched_trans, comb_rel_lem], 750 RW_TAC (srw_ss()) [assert_mode_def] 751 THEN Cases_on `(f2 >>= (��y. constT (a,y))) b` 752 THEN Cases_on `(f2 >>= (��y. constT (a,y))) b'` 753 THEN SPEC_ASSUM_TAC (``���x (g:word32) (s1:arm_state) (s2:arm_state). X``, [``a:'a``, ``g:word32``, ``b:arm_state``, ``b':arm_state``]) 754 THEN (NTAC 2 (RES_TAC 755 THEN IMP_RES_TAC untouched_trans 756 THEN FULL_SIMP_TAC (srw_ss()) [] 757 THEN IMP_RES_TAC untouched_mmu_setup_lem 758 THEN TRY (PAT_X_ASSUM ``!c g' s1'' s2''. X`` (fn th => ASSUME_TAC (SPECL [``a:'a``, ``g:bool[32]``, ``b:arm_state``, ``b':arm_state``] th))) 759 THEN UNDISCH_ALL_TAC 760 THEN RW_TAC (srw_ss()) [] 761 THEN FULL_SIMP_TAC (srw_ss()) [])) 762 THEN METIS_TAC [comb_rel_lem]]); 763 764 765val parT_preserves_relation_uu_thm = store_thm("parT_preserves_relation_uu_thm", 766 `` ! f1 f2 k uf uy. 767 (trans_fun uf) ==> 768 (preserve_relation_mmu f1 (assert_mode k) (assert_mode k) uf uy) ==> 769 (preserve_relation_mmu f2 (assert_mode k) (assert_mode k) uf uy) ==> 770 (preserve_relation_mmu (parT f1 f2) (assert_mode k) (assert_mode k) uf uy) ``, 771 REPEAT STRIP_TAC 772 THEN IMP_RES_TAC parT_latter_part_hlem 773 THEN WEAKEN_TAC is_forall 774 THEN THROW_ONE_AWAY_TAC ``preserve_relation_mmu (*II*) f2 (assert_mode k) (assert_mode k) uf uy`` 775 THEN UNDISCH_ALL_TAC 776 THEN RW_TAC (srw_ss()) [parT_alternative_thm, preserve_relation_mmu_def,trans_fun_def] 777 THEN UNDISCH_ALL_TAC 778 THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) []) 779 THEN FIRST_PROVE [ 780 RW_TAC (srw_ss()) [] 781 THEN Cases_on `(assert_mode k) s2` 782 THEN RES_TAC 783 THEN (NTAC 3 (FULL_SIMP_TAC (srw_ss()) [])), 784 RW_TAC (srw_ss()) [] 785 THEN RES_TAC 786 THEN RW_TAC (srw_ss()) [] 787 THEN FULL_SIMP_TAC (srw_ss()) [] 788 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 789 THEN FULL_SIMP_TAC (srw_ss()) [], 790 ASSERT_ASSUM_TAC ``access_violation b`` 791 THEN UNDISCH_ALL_TAC 792 THEN RW_TAC (srw_ss()) [] 793 THEN FULL_SIMP_TAC (srw_ss()) [] 794 THEN RES_TAC 795 THEN IMP_RES_TAC untouched_trans 796 THEN FULL_SIMP_TAC (srw_ss()) [] 797 THEN METIS_TAC [untouched_trans, comb_rel_lem], 798 RW_TAC (srw_ss()) [assert_mode_def] 799 THEN Cases_on `(f2 >>= (��y. constT (a,y))) b` 800 THEN Cases_on `(f2 >>= (��y. constT (a,y))) b'` 801 THEN SPEC_ASSUM_TAC (``���x (g:word32) (s1':arm_state) (s2':arm_state). X``, [``a:'a``, ``g:word32``, ``b:arm_state``, ``b':arm_state``]) 802 THEN (NTAC 2 (RES_TAC 803 THEN IMP_RES_TAC untouched_trans 804 THEN FULL_SIMP_TAC (srw_ss()) [] 805 THEN IMP_RES_TAC untouched_mmu_setup_lem 806 THEN TRY (PAT_X_ASSUM ``!c g' s1'' s2''. X`` (fn th => ASSUME_TAC (SPECL [``a:'a``, ``g:bool[32]``, ``b:arm_state``, ``b':arm_state``] th))) 807 THEN UNDISCH_ALL_TAC 808 THEN RW_TAC (srw_ss()) [] 809 THEN FULL_SIMP_TAC (srw_ss()) [])) 810 THEN METIS_TAC [comb_rel_lem]]); 811 812val comb_monot_thm = store_thm("comb_monot_thm", 813 ``!a:(arm_state -> bool). comb a a a``, 814 RW_TAC (srw_ss()) [comb_def]); 815 816 817 818val preserve_relation_comb_thm1 = 819 store_thm ("preserve_relation_comb_thm1", 820 ``! a b c d f uf uy. 821 preserve_relation_mmu f d a uf uy 822 ==> 823 comb a b c ==> 824 preserve_relation_mmu f d c uf uy``, 825 RW_TAC (srw_ss()) [preserve_relation_mmu_def,comb_def] 826 THEN PAT_X_ASSUM ``���g s1 s2. X`` 827 (fn thm => ASSUME_TAC (SPECL [``g:bool[32]``, 828 ``s1:arm_state``, ``s2:arm_state``] thm)) 829 THEN RES_TAC 830 THEN RW_TAC (srw_ss()) []); 831 832val preserve_relation_comb_v2_thm = 833 store_thm ("preserve_relation_comb_v2_thm", 834 ``! a b c d f uf uy. 835 preserve_relation_mmu f d a uf uy 836 ==> 837 comb a b c ==> 838 preserve_relation_mmu f d c uf uy``, 839 RW_TAC (srw_ss()) [preserve_relation_mmu_def,comb_def] 840 THEN PAT_X_ASSUM ``���g s1 s2. X`` 841 (fn thm => ASSUME_TAC (SPECL [``g:bool[32]``, 842 ``s1:arm_state``, ``s2:arm_state``] thm)) 843 THEN RES_TAC 844 THEN RW_TAC (srw_ss()) []); 845 846val preserve_relation_comb_abs_thm = 847 store_thm ("preserve_relation_comb_abs_thm", 848 ``! a b c d f uf uy. preserve_relation_mmu_abs f d b uf uy 849 ==> comb a b c ==> 850 preserve_relation_mmu_abs f d c uf uy``, 851 RW_TAC (srw_ss()) [preserve_relation_mmu_abs_def,comb_def] 852 THEN PAT_X_ASSUM ``��� c g s1 s2. X`` 853 (fn thm => ASSUME_TAC (SPECL [``c':'a``,``g:bool[32]``, 854 ``s1:arm_state``, ``s2:arm_state``] thm)) 855 THEN RES_TAC 856 THEN RW_TAC (srw_ss()) []); 857 858 859val comb_mode_def = Define `comb_mode m n k s = (assert_mode m s \/ assert_mode n s \/ assert_mode k s)`; 860 861val comb_mode_def = Define `comb_mode m n s = (assert_mode m s \/ assert_mode n s)`; 862 863val comb_mode_thm = 864 store_thm ("comb_mode_thm", 865``! m n. comb (assert_mode m) (assert_mode n) (comb_mode m n)``, 866RW_TAC (srw_ss()) [ assert_mode_def,comb_mode_def,comb_def]); 867 868 869 870(********* 3-parts-lem *********) 871 872val keep_mode_relation_def = Define `keep_mode_relation comp i1 i2 = 873 (!g s s' x. (mmu_requirements s g) ==> (i1 s) ==> (comp s = ValueState x s') ==> (i2 s'))`; 874 875val keep_similar_relation_def = Define `keep_similar_relation comp invr1 y = 876 !g s1 s2. 877 mmu_requirements s1 g ==> 878 mmu_requirements s2 g ==> 879 similar g s1 s2 ==> 880 (y g s1 s2) ==> 881 invr1 s1 ==> 882 invr1 s2 ==> 883 ((?a s1' s2'.((comp s1 = ValueState a s1') /\ (comp s2 = ValueState a s2') /\ 884 (y g s1' s2') /\ (similar g s1' s2'))) 885\/ (? e. (comp s1 = Error e) /\ (comp s2 = Error e)))`; 886 887val keep_untouched_relation_def = Define `keep_untouched_relation comp invr1 f = 888 !g s s' a. (mmu_requirements s g) ==> (invr1 s) ==> (comp s = ValueState a s') ==> ((untouched g s s') /\ (f g s s'))`; 889 890val three_parts_thm = store_thm( 891 "three_parts_thm", 892 ``!comp i1 i2 f y. (keep_mode_relation comp i1 i2) ==> (keep_similar_relation comp i1 y) ==> (keep_untouched_relation comp i1 f) ==> (preserve_relation_mmu comp i1 i2 f y)``, 893 RW_TAC (srw_ss()) [preserve_relation_mmu_def, keep_mode_relation_def, keep_similar_relation_def, keep_untouched_relation_def] THEN METIS_TAC []); 894 895val refl_rel_def = Define `refl_rel y = (!gg ss. y gg ss ss)`; 896 897 898 899val downgrade_thm = store_thm ( 900 "downgrade_thm", 901 ``!comp i1 i2 f y. (preserve_relation_mmu comp i1 i2 f y) ==> (refl_rel y) 902 ==> (keep_mode_relation comp i1 i2 /\ keep_similar_relation comp i1 y /\ keep_untouched_relation comp i1 f)``, 903 RW_TAC (srw_ss()) [refl_rel_def, preserve_relation_mmu_def, keep_mode_relation_def, keep_similar_relation_def, keep_untouched_relation_def] 904 THEN RES_TAC 905 THEN FULL_SIMP_TAC (srw_ss()) [] 906 THEN (TRY (METIS_TAC [])) 907 THEN ASSUME_TAC (SPECL [``g:word32``, ``s:arm_state``] similar_refl) 908 THEN SPEC_ASSUM_TAC (``!gg ss. y gg ss``, [``g:word32``, ``s:arm_state``]) 909 THEN RES_TAC 910 THEN FULL_SIMP_TAC (srw_ss()) [] 911 THEN METIS_TAC []); 912 913 914 915 916 917 918 919 920(****** handling forT loops *******) 921 922 923val comb_gen_lem = store_thm( 924 "comb_gen_lem", 925 ``!comp i1 i2 i3 i23 f y. (comb i2 i3 i23 \/ comb i3 i2 i23) ==> (preserve_relation_mmu comp i1 i2 f y) ==> (preserve_relation_mmu comp i1 i23 f y)``, 926 RW_TAC (srw_ss()) [preserve_relation_mmu_def, comb_def] 927 THEN METIS_TAC[]); 928 929 930 931val constT_unit_preserving_lem = store_thm( 932 "constT_unit_preserving_lem", 933 ``!invr:(arm_state->bool) uf uy. (reflexive_comp uf invr) ==> 934 preserve_relation_mmu (constT ()) invr invr uf uy``, 935 RW_TAC (srw_ss()) [constT_def, preserve_relation_mmu_def, untouched_def, similar_def,reflexive_comp_def] THEN 936(RW_TAC (srw_ss()) [] )); 937 938 939 940val SEQT_UNTOUCHED_TAC = 941 UNDISCH_ALL_TAC 942 THEN RW_TAC (srw_ss()) [seqT_def, keep_untouched_relation_def, trans_fun_def] 943 THEN UNDISCH_ALL_TAC 944 THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) []) 945 THEN UNDISCH_ALL_TAC 946 THEN RW_TAC (srw_ss()) [] 947 THEN FULL_SIMP_TAC (srw_ss()) [] 948 THEN IMP_RES_TAC untouched_mmu_setup_lem 949 THEN RES_TAC 950 THEN IMP_RES_TAC untouched_trans 951 THEN FULL_SIMP_TAC (srw_ss()) []; 952 953 954 955 956val forT_untouching_thm = store_thm( 957 "forT_untouching_thm", 958 ``!f k uf uy. 959 (trans_fun uf) 960 ==> (reflexive_comp uf (assert_mode k)) 961 ==> (!a. keep_untouched_relation (f a) (assert_mode k) uf) 962 ==> (!a. keep_mode_relation (f a) (assert_mode k) (assert_mode k)) 963 ==> (!l h. keep_untouched_relation (forT l h f) (assert_mode k) uf)``, 964 REPEAT STRIP_TAC 965 THEN Induct_on `h - l` 966 THENL [FULL_SIMP_TAC (srw_ss()) [] 967 THEN REPEAT STRIP_TAC 968 THEN NTAC 2 (PURE_ONCE_REWRITE_TAC [forT_def, LET_DEF]) 969 THEN RW_TAC arith_ss [keep_untouched_relation_def, constT_def, seqT_def] 970 THEN (REPEAT (PAT_X_ASSUM (``!(l:num). X``) (fn th => (ASSUME_TAC (SPEC ``l:num`` th))))) 971 THEN REPEAT STRIP_TAC 972 THEN SEQT_UNTOUCHED_TAC 973 THEN FULL_SIMP_TAC (srw_ss()) [untouched_def, reflexive_comp_def] 974 THEN RW_TAC (srw_ss()) [LET_DEF], 975 FULL_SIMP_TAC (srw_ss()) [] 976 THEN REPEAT STRIP_TAC 977 THEN PURE_ONCE_REWRITE_TAC [forT_def, LET_DEF] 978 THEN UNDISCH_ALL_TAC 979 THEN RW_TAC arith_ss [constT_def] 980 THEN `v = h - (l+1)` by FULL_SIMP_TAC arith_ss [] 981 THEN PAT_X_ASSUM ``!(h:num) (l:num). (X:bool) ==> Y`` (fn th => IMP_RES_TAC (SPECL [``h:num``, ``(l+1):num``] th)) 982 THEN REPEAT (PAT_X_ASSUM (``!(l:num). X``) (fn th => (ASSUME_TAC (SPEC ``l:num`` th)))) 983 THEN FULL_SIMP_TAC (srw_ss()) [keep_mode_relation_def] 984 THEN REPEAT STRIP_TAC 985 THEN SEQT_UNTOUCHED_TAC 986 THEN METIS_TAC [assert_mode_def]]); 987 988 989val SEQT_PRESERVE_TAC = fn F1 => 990 (RW_TAC (srw_ss()) [seqT_def,constT_def,keep_similar_relation_def,keep_untouched_relation_def, keep_mode_relation_def] 991 THEN Cases_on [QUOTE (F1^" s1")] 992 THEN Cases_on [QUOTE (F1^" s2")] 993 THEN RES_TAC 994 THEN RW_TAC (srw_ss()) [] 995 THEN FULL_SIMP_TAC (srw_ss()) [] 996 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 997 THEN FULL_SIMP_TAC (srw_ss()) [] 998 THEN RW_TAC (srw_ss()) [] 999 THEN `mmu_requirements b g` by METIS_TAC [untouched_mmu_setup_lem] 1000 THEN `mmu_requirements b' g` by METIS_TAC [untouched_mmu_setup_lem] 1001 THEN METIS_TAC []); 1002 1003 1004val SEQT_PRESERVE_BEGIN_TAC = fn F1 => 1005 (RW_TAC (srw_ss()) [seqT_def,constT_def,keep_similar_relation_def,keep_untouched_relation_def, keep_mode_relation_def] 1006 THEN Cases_on [QUOTE (F1^" s1")] 1007 THEN Cases_on [QUOTE (F1^" s2")] 1008 THEN RES_TAC 1009 THEN RW_TAC (srw_ss()) [] 1010 THEN FULL_SIMP_TAC (srw_ss()) [] 1011 THEN (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 1012 THEN FULL_SIMP_TAC (srw_ss()) [] 1013 THEN RW_TAC (srw_ss()) [] 1014 THEN `mmu_requirements b g` by METIS_TAC [untouched_mmu_setup_lem] 1015 THEN `mmu_requirements b' g` by METIS_TAC [untouched_mmu_setup_lem]); 1016 1017val forT_similar_thm = store_thm( 1018 "forT_similar_thm", 1019 ``!f k uf uy. 1020 (!a. keep_untouched_relation (f a) (assert_mode k) uf) 1021 ==> (!a. keep_mode_relation (f a) (assert_mode k) (assert_mode k)) 1022 ==> (!a. keep_similar_relation (f a) (assert_mode k) uy) 1023 ==> (!l h. keep_similar_relation (forT l h f) (assert_mode k) uy)``, 1024 REPEAT STRIP_TAC 1025 THEN IMP_RES_TAC forT_untouching_thm 1026 THEN Induct_on `h - l` 1027 THENL [FULL_SIMP_TAC (srw_ss()) [] 1028 THEN (REPEAT STRIP_TAC) 1029 THEN (NTAC 2 (PURE_ONCE_REWRITE_TAC [forT_def, LET_DEF])) 1030 THEN RW_TAC arith_ss [keep_similar_relation_def, constT_def, seqT_def] 1031 THEN (REPEAT (PAT_X_ASSUM (``!(l:num). X``) (fn th => (ASSUME_TAC (SPEC ``l:num`` th))))) 1032 THEN (REPEAT STRIP_TAC) 1033 THEN UNDISCH_ALL_TAC 1034 THEN SEQT_PRESERVE_TAC "f l", 1035 1036 1037 FULL_SIMP_TAC (srw_ss()) [] 1038 THEN REPEAT STRIP_TAC 1039 THEN PURE_ONCE_REWRITE_TAC [forT_def, LET_DEF] 1040 THEN UNDISCH_ALL_TAC 1041 THEN RW_TAC arith_ss [] 1042 THEN `v = h - (l+1)` by FULL_SIMP_TAC arith_ss [] 1043 THEN PAT_X_ASSUM ``!h l. X ==> Y`` (fn th => IMP_RES_TAC (SPECL [``h:num``, ``(l+1):num``] th)) 1044 THEN REPEAT (PAT_X_ASSUM ``!(a:num). Z (x)`` (fn th => ASSUME_TAC (SPEC ``l:num`` th))) 1045 THEN REPEAT STRIP_TAC 1046 THEN UNDISCH_ALL_TAC 1047 THEN SEQT_PRESERVE_BEGIN_TAC "f l" 1048 THEN Cases_on `forT (l + 1) h f b` 1049 THEN Cases_on `forT (l + 1) h f b'` 1050 THEN FULL_SIMP_TAC (srw_ss()) [] 1051 THEN PAT_X_ASSUM ``���g s1 s2. mmu_requirements s1 g ��� 1052 mmu_requirements s2 g ��� 1053 similar g s1 s2 ��� 1054 uy g s1 s2 ==> 1055 (invr s1) ==> 1056 (invr s2) ==> 1057 (���a s1' s2'. 1058 (forT (l + 1) h f s1 = ValueState a s1') ��� 1059 (forT (l + 1) h f s2 = ValueState a s2') ��� (uy g s1' s2') /\ similar g s1' s2') ��� 1060 ���e. 1061 (forT (l + 1) h f s1 = Error e) ��� 1062 (forT (l + 1) h f s2 = Error e)`` 1063 (fn th => ASSUME_TAC (SPECL [``g:word32``, ``b:arm_state``, ``b':arm_state``] th)) 1064 THEN RES_TAC 1065 THEN FULL_SIMP_TAC (srw_ss()) [] 1066 THEN REPEAT IF_CASES_TAC THEN RW_TAC (srw_ss()) [] 1067 THEN (`access_violation b'' = access_violation b'''` by METIS_TAC [similar_def]) 1068 THEN FULL_SIMP_TAC (srw_ss()) []]); 1069 1070 1071val forT_mode_thm = store_thm( 1072 "forT_mode_thm", 1073 ``!f k uf. 1074 (!a. keep_untouched_relation (f a) (assert_mode k) uf) 1075 ==> (!a. keep_mode_relation (f a) (assert_mode k) (assert_mode k)) 1076 ==> (!l h. keep_mode_relation (forT l h f) (assert_mode k) (assert_mode k))``, 1077 REPEAT STRIP_TAC 1078 THEN Induct_on `h - l` 1079 THENL [FULL_SIMP_TAC (srw_ss()) [] 1080 THEN REPEAT STRIP_TAC 1081 THEN NTAC 2 (PURE_ONCE_REWRITE_TAC [forT_def, LET_DEF]) 1082 THEN RW_TAC arith_ss [keep_untouched_relation_def, constT_def, seqT_def] 1083 THEN (REPEAT (PAT_X_ASSUM (``!(l:num). X``) (fn th => (ASSUME_TAC (SPEC ``l:num`` th))))) 1084 THEN REPEAT STRIP_TAC 1085 THEN UNDISCH_ALL_TAC 1086 THEN RW_TAC (srw_ss()) [seqT_def, keep_mode_relation_def] 1087 THEN UNDISCH_ALL_TAC 1088 THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) []) 1089 THEN UNDISCH_ALL_TAC 1090 THEN RW_TAC (srw_ss()) [] 1091 THEN FULL_SIMP_TAC (srw_ss()) [] 1092 THEN RES_TAC 1093 THEN FULL_SIMP_TAC (srw_ss()) [], 1094 FULL_SIMP_TAC (srw_ss()) [] 1095 THEN REPEAT STRIP_TAC 1096 THEN PURE_ONCE_REWRITE_TAC [forT_def, LET_DEF] 1097 THEN UNDISCH_ALL_TAC 1098 THEN RW_TAC arith_ss [constT_def] 1099 THEN `v = h - (l+1)` by FULL_SIMP_TAC arith_ss [] 1100 THEN PAT_X_ASSUM ``!h l. X ==> Y`` (fn th => IMP_RES_TAC (SPECL [``h:num``, ``(l+1):num``] th)) 1101 THEN REPEAT (PAT_X_ASSUM (``!(l:num). X``) (fn th => (ASSUME_TAC (SPEC ``l:num`` th)))) 1102 THEN UNDISCH_ALL_TAC 1103 THEN RW_TAC (srw_ss()) [seqT_def, keep_mode_relation_def] 1104 THEN UNDISCH_ALL_TAC 1105 THEN REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) []) 1106 THEN UNDISCH_ALL_TAC 1107 THEN RW_TAC (srw_ss()) [] 1108 THEN RES_TAC 1109 THEN FULL_SIMP_TAC (srw_ss()) [keep_untouched_relation_def] 1110 THEN RES_TAC 1111 THEN IMP_RES_TAC untouched_mmu_setup_lem 1112 THEN RES_TAC]); 1113 1114 1115 1116val forT_preserves_user_relation_thm = store_thm( 1117 "forT_preserves_user_relation_thm", 1118 ``!f k uf uy. 1119 (trans_fun uf) 1120 ==> (refl_rel uy) 1121 ==> (reflexive_comp uf (assert_mode k)) 1122 ==> (!a. preserve_relation_mmu (f a) (assert_mode k) (assert_mode k) uf uy) 1123 ==> (!l h. preserve_relation_mmu (forT l h f) (assert_mode k) (assert_mode k) uf uy)``, 1124 METIS_TAC [forT_similar_thm, forT_mode_thm, forT_untouching_thm, three_parts_thm, downgrade_thm]); 1125 1126 1127val forT_preserving_thm = store_thm( 1128 "forT_preserving_thm", 1129 ``!f k uf uy. 1130 (trans_fun uf) 1131 ==> (refl_rel uy) 1132 ==> (reflexive_comp uf (assert_mode k)) 1133 ==> (preserve_relation_mmu_abs f (assert_mode k) (assert_mode k) uf uy) 1134 ==> (!l h. preserve_relation_mmu (forT l h f) (assert_mode k) (assert_mode k) uf uy)``, 1135 RW_TAC (srw_ss()) [] THEN METIS_TAC [forT_preserves_user_relation_thm, second_abs_lemma]); 1136 1137 1138(********* errorT *********) 1139 1140 1141val errorT_thm = 1142 store_thm("errorT_thm", 1143 ``! inv s uf1 uy1. preserve_relation_mmu (errorT s) inv inv uf1 uy1 ``, 1144 (RW_TAC (srw_ss()) [preserve_relation_mmu_def,similar_def, 1145 assert_mode_def,errorT_def,untouched_def])); 1146 1147val errorT_comb_thm = 1148 store_thm("errorT_comb_thm", 1149 ``! inv1 inv2 s uf1 uy1. preserve_relation_mmu (errorT s) inv1 inv2 uf1 uy1 ``, 1150 (RW_TAC (srw_ss()) [preserve_relation_mmu_def,similar_def, 1151 assert_mode_def,errorT_def,untouched_def])); 1152 1153 1154 1155val _ = export_theory(); 1156