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