1(* interactive use: 2 3quietdec := true; 4loadPath := (concat Globals.HOLDIR "/examples/dev/sw") :: !loadPath; 5 6app load ["pred_setSimps", "pred_setTheory", 7 "arithmeticTheory", "wordsTheory", "wordsLib", "pairTheory", "listTheory", "whileTheory", "finite_mapTheory", "preARMTheory", "ARMCompositionTheory", 8 "relationTheory"]; 9 10quietdec := false; 11*) 12 13 14open HolKernel Parse boolLib bossLib numLib pred_setSimps pred_setTheory 15 arithmeticTheory wordsTheory wordsLib pairTheory listTheory whileTheory finite_mapTheory preARMTheory ARMCompositionTheory relationTheory; 16 17val _ = hide "B"; 18(*---------------------------------------------------------------------------------*) 19(*---------------------------------------------------------------------------------*) 20 21val _ = new_theory "IL"; 22 23val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss; 24 25(*---------------------------------------------------------------------------------*) 26(* Registers and memory data in IL *) 27(*---------------------------------------------------------------------------------*) 28 29val _ = Hol_datatype ` 30 MREG = R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 | R13 | R14`; 31 32val _ = type_abbrev("MMEM", Type`:MREG # OFFSET`); (* memory in ir *) 33 34val _ = Hol_datatype ` 35 MEXP = MR of MREG (* registers *) 36 | MC of word4 => word8 (* constants *) 37 `; 38 39val index_of_reg = Define ` 40 (index_of_reg R0 = 0) /\ 41 (index_of_reg R1 = 1) /\ 42 (index_of_reg R2 = 2) /\ 43 (index_of_reg R3 = 3) /\ 44 (index_of_reg R4 = 4) /\ 45 (index_of_reg R5 = 5) /\ 46 (index_of_reg R6 = 6) /\ 47 (index_of_reg R7 = 7) /\ 48 (index_of_reg R8 = 8) /\ 49 (index_of_reg R9 = 9) /\ 50 (index_of_reg R10 = 10) /\ 51 (index_of_reg R11 = 11) /\ 52 (index_of_reg R12 = 12) /\ 53 (index_of_reg R13 = 13) /\ 54 (index_of_reg R14 = 14)`; 55 56val from_reg_index_def = Define ` 57 from_reg_index i = 58 if i = 0 then R0 59 else if i = 1 then R1 60 else if i = 2 then R2 61 else if i = 3 then R3 62 else if i = 4 then R4 63 else if i = 5 then R5 64 else if i = 6 then R6 65 else if i = 7 then R7 66 else if i = 8 then R8 67 else if i = 9 then R9 68 else if i = 10 then R10 69 else if i = 11 then R11 70 else if i = 12 then R12 71 else if i = 13 then R13 72 else R14`; 73 74val from_reg_index_thm = Q.store_thm 75 ("from_reg_index_thm", 76 `(from_reg_index 0 = R0) /\ 77 (from_reg_index 1 = R1) /\ 78 (from_reg_index 2 = R2) /\ 79 (from_reg_index 3 = R3) /\ 80 (from_reg_index 4 = R4) /\ 81 (from_reg_index 5 = R5) /\ 82 (from_reg_index 6 = R6) /\ 83 (from_reg_index 7 = R7) /\ 84 (from_reg_index 8 = R8) /\ 85 (from_reg_index 9 = R9) /\ 86 (from_reg_index 10 = R10) /\ 87 (from_reg_index 11 = R11) /\ 88 (from_reg_index 12 = R12) /\ 89 (from_reg_index 13 = R13) /\ 90 (from_reg_index 14 = R14)`, 91 RW_TAC std_ss [from_reg_index_def] 92 ); 93 94val toREG_def = Define ` 95 toREG r = 96 REG (index_of_reg r)`; 97 98val toMEM_def = Define ` 99 toMEM ((base,offset):MMEM) = 100 preARM$MEM (index_of_reg base,offset)`; (* [base + offset] *) 101 102val toEXP_def = Define ` 103 (toEXP (MR r) = toREG r) /\ 104 (toEXP (MC shift c) = WCONST ((w2w c):word32 #>> (2*w2n shift)))`; 105 106(*---------------------------------------------------------------------------------*) 107(* Semantics of the intermediate language *) 108(*---------------------------------------------------------------------------------*) 109 110val _ = Hol_datatype ` 111 DOPER = MLDR of MREG => MMEM | 112 MSTR of MMEM => MREG | 113 MMOV of MREG => MEXP | 114 MADD of MREG => MREG => MEXP | 115 MSUB of MREG => MREG => MEXP | 116 MRSB of MREG => MREG => MEXP | 117 MMUL of MREG => MREG => MREG | 118 MAND of MREG => MREG => MEXP | 119 MORR of MREG => MREG => MEXP | 120 MEOR of MREG => MREG => MEXP | 121 MLSL of MREG => MREG => word5 | 122 MLSR of MREG => MREG => word5 | 123 MASR of MREG => MREG => word5 | 124 MROR of MREG => MREG => word5 | 125 MPUSH of num => num list | 126 MPOP of num => num list`; 127 128val _ = type_abbrev("CEXP", Type`:MREG # COND # MEXP`); 129 130val _ = Hol_datatype `CTL_STRUCTURE = 131 BLK of DOPER list | 132 SC of CTL_STRUCTURE => CTL_STRUCTURE | 133 CJ of CEXP => CTL_STRUCTURE => CTL_STRUCTURE | 134 TR of CEXP => CTL_STRUCTURE 135 `; 136 137(*---------------------------------------------------------------------------------*) 138(* Macro machine *) 139(* Stack Operations *) 140(* Since a negative integeter minus 0 results in 0, we assume the stack goes *) 141(* up to avoid this problem *) 142(*---------------------------------------------------------------------------------*) 143 144(* Push into the stack from multiple registers with writing-back to the sp *) 145 146val pushL_def = 147 Define `pushL st baseR regL = 148 write (FST (FOLDL (\(st1,i) reg. (write st1 (MEM(baseR,NEG i)) (read st reg), i+1)) (st,0) (REVERSE (MAP REG regL)))) 149 (REG baseR) (read st (REG baseR) - n2w (4*LENGTH regL))`; 150 151(* Pop into multiple registers from the stack with writing-back to the sp *) 152 153val popL_def = 154 Define `popL st baseR regL = 155 write (FST (FOLDL (\(st1,i) reg. (write st1 reg (read st (MEM(baseR, POS(i+1)))), i+1)) (st,0) (MAP REG regL))) 156 (REG baseR) (read st (REG baseR) + n2w (4*LENGTH regL))`; 157 158(*---------------------------------------------------------------------------------*) 159(* Decode assignment statement *) 160(*---------------------------------------------------------------------------------*) 161 162val mdecode_def = Define ` 163 (!dst src.mdecode st (MLDR dst src) = 164 write st (toREG dst) (read st (toMEM src))) /\ 165 (!dst src.mdecode st (MSTR dst src) = 166 write st (toMEM dst) (read st (toREG src))) /\ 167 (mdecode st (MMOV dst src) = 168 write st (toREG dst) (read st (toEXP src))) /\ 169 (mdecode st (MADD dst src1 src2) = 170 write st (toREG dst) (read st (toREG src1) + read st (toEXP src2))) /\ 171 (mdecode st (MSUB dst src1 src2) = 172 write st (toREG dst) (read st (toREG src1) - read st (toEXP src2))) /\ 173 (mdecode st (MRSB dst src1 src2) = 174 write st (toREG dst) (read st (toEXP src2) - read st (toREG src1))) /\ 175 (mdecode st (MMUL dst src1 src2_reg) = 176 write st (toREG dst) (read st (toREG src1) * read st (toREG src2_reg))) /\ 177 (mdecode st (MAND dst src1 src2) = 178 write st (toREG dst) (read st (toREG src1) && read st (toEXP src2))) /\ 179 (mdecode st (MORR dst src1 src2) = 180 write st (toREG dst) (read st (toREG src1) !! read st (toEXP src2))) /\ 181 (mdecode st (MEOR dst src1 src2) = 182 write st (toREG dst) (read st (toREG src1) ?? read st (toEXP src2))) /\ 183 (mdecode st (MLSL dst src2_reg src2_num) = 184 write st (toREG dst) (read st (toREG src2_reg) << w2n src2_num)) /\ 185 (mdecode st (MLSR dst src2_reg src2_num) = 186 write st (toREG dst) (read st (toREG src2_reg) >>> w2n src2_num)) /\ 187 (mdecode st (MASR dst src2_reg src2_num) = 188 write st (toREG dst) (read st (toREG src2_reg) >> w2n src2_num)) /\ 189 (mdecode st (MROR dst src2_reg src2_num) = 190 write st (toREG dst) (read st (toREG src2_reg) #>> w2n src2_num)) /\ 191 (mdecode st (MPUSH dst' srcL) = 192 pushL st dst' srcL) /\ 193 (mdecode st (MPOP dst' srcL) = 194 popL st dst' srcL) 195 `; 196 197val translate_assignment_def = Define ` 198 (translate_assignment (MMOV dst src) = ((MOV,NONE,F),SOME (toREG dst), [toEXP src], NONE):INST) /\ 199 (translate_assignment (MADD dst src1 src2) = ((ADD,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\ 200 (translate_assignment (MSUB dst src1 src2) = ((SUB,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\ 201 (translate_assignment (MRSB dst src1 src2) = ((RSB,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\ 202 (translate_assignment (MMUL dst src1 src2_reg) = ((MUL,NONE,F),SOME (toREG dst), [toREG src1; toREG src2_reg], NONE):INST) /\ 203 (translate_assignment (MAND dst src1 src2) = ((AND,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\ 204 (translate_assignment (MORR dst src1 src2) = ((ORR,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\ 205 (translate_assignment (MEOR dst src1 src2) = ((EOR,NONE,F),SOME (toREG dst), [toREG src1; toEXP src2], NONE):INST) /\ 206 (translate_assignment (MLSL dst src2_reg src2_num) = ((LSL,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\ 207 (translate_assignment (MLSR dst src2_reg src2_num) = ((LSR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\ 208 (translate_assignment (MASR dst src2_reg src2_num) = ((ASR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\ 209 (translate_assignment (MROR dst src2_reg src2_num) = ((ROR,NONE,F),SOME (toREG dst), [toREG src2_reg; WCONST (w2w src2_num)], NONE):INST) /\ 210 (!dst src.translate_assignment (MLDR dst src) = ((LDR,NONE,F),SOME (toREG dst), [toMEM src], NONE):INST) /\ 211 (!dst src.translate_assignment (MSTR dst src) = ((STR,NONE,F),SOME (toREG src), [toMEM dst], NONE):INST) /\ 212 (!dst srcL.translate_assignment (MPUSH dst srcL) = ((STMFD,NONE,F),SOME (WREG dst), MAP REG srcL, NONE):INST) /\ 213 (!dst srcL.translate_assignment (MPOP dst srcL) = ((LDMFD,NONE,F),SOME (WREG dst), MAP REG srcL, NONE):INST) 214 `; 215 216val translate_condition_def = Define ` 217 translate_condition (r, c, e) = 218 (toREG r, c, toEXP e)` 219 220val eval_il_cond_def = Define ` 221 eval_il_cond cond = eval_cond (translate_condition cond)`; 222 223 224val TRANSLATE_ASSIGMENT_CORRECT = Q.store_thm 225 ("TRANSLATE_ASSIGMENT_CORRECT", 226 `!(stm:DOPER) pc cpsr st. 227 (SUC pc,cpsr,mdecode st stm) = decode_cond (pc,cpsr,st) (translate_assignment stm)`, 228 SIMP_TAC std_ss [FORALL_DSTATE] THEN 229 Cases_on `stm` THEN 230 RW_TAC list_ss [translate_assignment_def, decode_cond_thm, decode_op_thm, write_thm, mdecode_def] THEN 231 RW_TAC list_ss [pushL_def, popL_def, read_thm, w2n_w2w, dimindex_5, dimindex_32] 232 ); 233 234val TRANSLATE_ASSIGMENT_CORRECT_2 = Q.store_thm 235 ("TRANSLATE_ASSIGMENT_CORRECT_2", 236 `!(stm:DOPER) s. 237 decode_cond s (translate_assignment stm) = (SUC (FST s),FST (SND s),mdecode (SND (SND s)) stm)`, 238 RW_TAC std_ss [] THEN 239 METIS_TAC [ABS_PAIR_THM,FST,SND,TRANSLATE_ASSIGMENT_CORRECT] 240 ); 241 242 243(*---------------------------------------------------------------------------------*) 244(* Decode from intermedia language to low level language *) 245(*---------------------------------------------------------------------------------*) 246 247val translate_def = Define ` 248 (translate (BLK (stm::stmL)) = translate_assignment stm :: translate (BLK stmL)) /\ 249 (translate (BLK []) = []) /\ 250 (translate (SC S1 S2) = 251 mk_SC (translate S1) (translate S2)) /\ 252 (translate (CJ cond Strue Sfalse) = 253 mk_CJ (translate_condition cond) (translate Strue) (translate Sfalse)) /\ 254 (translate (TR cond Sbody) = 255 mk_TR (translate_condition cond) (translate Sbody)) 256 `; 257 258(*---------------------------------------------------------------------------------*) 259(* Intermediate Representation *) 260(* Definition of run_ir *) 261(*---------------------------------------------------------------------------------*) 262 263val run_arm_def = Define ` 264 run_arm arm ((pc,cpsr,st),pcS) = runTo (upload arm (\i.ARB) pc) (pc+LENGTH arm) ((pc,cpsr,st),pcS)`; 265 266val run_ir_def = Define ` 267 run_ir ir st = get_st (run_arm (translate ir) ((0,0w,st),{}))`; 268 269 270val WELL_FORMED_def = Define ` 271 (WELL_FORMED (BLK stmL) = well_formed (translate (BLK stmL))) /\ 272 (WELL_FORMED (SC S1 S2) = well_formed (translate (SC S1 S2)) /\ 273 WELL_FORMED S1 /\ WELL_FORMED S2) /\ 274 (WELL_FORMED (CJ cond S1 S2) = well_formed (translate (CJ cond S1 S2)) /\ 275 WELL_FORMED S1 /\ WELL_FORMED S2) /\ 276 (WELL_FORMED (TR cond S1) = well_formed (translate (TR cond S1)) /\ 277 WELL_FORMED S1 /\ 278 WF_TR (translate_condition cond, translate S1))`; 279 280 281val WELL_FORMED_SUB_def = Define ` 282 (WELL_FORMED_SUB (BLK stmL) = T) /\ 283 (WELL_FORMED_SUB (SC S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 284 (WELL_FORMED_SUB (CJ cond S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 285 (WELL_FORMED_SUB (TR cond S1) = WELL_FORMED S1 /\ WF_TR (translate_condition cond, translate S1))`; 286 287val WELL_FORMED_SUB_thm = store_thm ("WELL_FORMED_SUB_thm", 288 ``!ir. WELL_FORMED ir = (WELL_FORMED_SUB ir /\ well_formed (translate ir))``, 289 290 Cases_on `ir` THEN 291 REWRITE_TAC [WELL_FORMED_def, WELL_FORMED_SUB_def] THEN 292 PROVE_TAC[]); 293 294 295val CHANGED_def = Define `CHANGED s ir = 296 !st st'. (st' = run_ir ir st) ==> ( 297 !r. ~(MEM r s) ==> (read st (toREG r) = read st' (toREG r)) 298 )` 299 300val UNCHANGED_def = Define `UNCHANGED s ir = 301 !st st'. (st' = run_ir ir st) ==> ( 302 !r. (MEM r s) ==> (read st (toREG r) = read st' (toREG r)) 303 )` 304 305val LIST_COUNT_def = Define ` 306 (LIST_COUNT 0 = []) /\ 307 (LIST_COUNT (SUC n) = n::(LIST_COUNT n))` 308 309val MEM_LIST_COUNT = store_thm ("MEM_LIST_COUNT", 310 ``!n m. MEM n (LIST_COUNT m) = (n < m)``, 311 312 Induct_on `m` THENL [ 313 SIMP_TAC list_ss [LIST_COUNT_def], 314 ASM_SIMP_TAC list_ss [LIST_COUNT_def] 315 ]) 316 317 318val USED_STACK_def = Define `USED_STACK size ir = 319 !r m r' m' base. (((r', m') = run_ir ir (r, m)) /\ 320 (base = preARM$MEM_ADDR (read (r,m) (REG 13))) 321 ) ==> ( 322 (!l. (MEM l (MAP (\off. base - n2w off) (LIST_COUNT size))) \/ (m ' l = m' ' l)) 323 )`; 324 325val USED_STACK_THM = 326 store_thm ("USED_STACK_THM", 327 ``USED_STACK size ir = 328 !r m r' m'. ((r', m') = run_ir ir (r, m)) ==> ( 329 (!l. ~(MEM l (MAP (\off. preARM$MEM_ADDR (r ' 13w) - n2w off) (LIST_COUNT size))) ==> (m ' l = m' ' l)) 330 )``, 331 332 SIMP_TAC std_ss [USED_STACK_def, read_thm, IMP_DISJ_THM]) 333 334 335val USED_STACK_ENLARGE = 336 store_thm ("USED_STACK_ENLARGE", 337 ``!ir size1 size2. 338 ((size1 <= size2) /\ USED_STACK size1 ir) ==> 339 USED_STACK size2 ir``, 340 341 SIMP_TAC std_ss [USED_STACK_def, MEM_MAP, MEM_LIST_COUNT] THEN 342 REPEAT STRIP_TAC THEN 343 `!off. (off < size1) ==> (off < size2)` by DECIDE_TAC THEN 344 METIS_TAC[]) 345 346 347val UNCHANGED_STACK_def = Define `UNCHANGED_STACK reglist stack_size ir = UNCHANGED reglist ir /\ USED_STACK stack_size ir`; 348 349 350val UNCHANGED_THM = store_thm ("UNCHANGED_THM", 351 352 ``!s ir. 353 UNCHANGED s ir = 354 EVERY (\r. !reg mem. (read (run_ir ir (reg,mem)) (toREG r) = 355 read (reg,mem) (toREG r))) s``, 356 357 SIMP_TAC std_ss [EVERY_MEM, UNCHANGED_def, ELIM_PFORALL] THEN 358 METIS_TAC[pairTheory.PAIR]) 359 360(*---------------------------------------------------------------------------------*) 361(* Hoare Rules for IR *) 362(*---------------------------------------------------------------------------------*) 363 364val HOARE_SC_IR = Q.store_thm ( 365 "HOARE_SC_IR", 366 `!ir1 ir2 P Q R T. 367 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 368 (!st. P st ==> Q (run_ir ir1 st)) /\ 369 (!st. R st ==> T (run_ir ir2 st)) /\ (!st. Q st ==> R st) ==> 370 !st. P st ==> 371 T (run_ir (SC ir1 ir2) st)`, 372 RW_TAC std_ss [WELL_FORMED_SUB_thm, run_ir_def, translate_def, run_arm_def, eval_fl_def] THEN 373 IMP_RES_TAC (SIMP_RULE std_ss [eval_fl_def, uploadCode_def] HOARE_SC_FLAT) 374 ); 375 376val HOARE_CJ_IR = Q.store_thm ( 377 "HOARE_CJ_IR", 378 `!cond ir_t ir_f P Q R. 379 WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 380 (!st. P st ==> Q (run_ir ir_t st)) /\ 381 (!st. P st ==> R (run_ir ir_f st)) ==> 382 !st. P st ==> 383 if eval_il_cond cond st then Q (run_ir (CJ cond ir_t ir_f) st) 384 else R (run_ir (CJ cond ir_t ir_f) st)`, 385 RW_TAC std_ss [WELL_FORMED_SUB_thm, run_ir_def, translate_def, run_arm_def, eval_fl_def, eval_il_cond_def] THEN 386 IMP_RES_TAC (SIMP_RULE std_ss [eval_fl_def, uploadCode_def] HOARE_CJ_FLAT) THEN 387 METIS_TAC [] 388 ); 389 390val HOARE_TR_IR = Q.store_thm ( 391 "HOARE_TR_IR", 392 `!cond ir P. 393 WELL_FORMED ir /\ WF_TR (translate_condition cond, translate ir) /\ 394 (!st. P st ==> P (run_ir ir st)) ==> 395 !st. P st ==> P (run_ir (TR cond ir) st) /\ 396 eval_il_cond cond (run_ir (TR cond ir) st)`, 397 RW_TAC std_ss [WELL_FORMED_SUB_thm, run_ir_def, translate_def, run_arm_def, eval_fl_def, eval_il_cond_def] THEN 398 METIS_TAC [SIMP_RULE std_ss [eval_fl_def, uploadCode_def] HOARE_TR_FLAT] 399 ); 400 401(*---------------------------------------------------------------------------------*) 402(* Well-formedness of IR *) 403(*---------------------------------------------------------------------------------*) 404 405val UPLOAD_LEM_2 = Q.store_thm ( 406 "UPLOAD_LEM_2", 407 `!s stm iB. (upload [stm] iB (FST s)) (FST s) = stm`, 408 RW_TAC std_ss [] THEN 409 `0 < LENGTH [stm]` by RW_TAC list_ss [] THEN 410 METIS_TAC [UPLOAD_LEM, FST, DECIDE (Term`!x.x + 0 = x`), EL, HD] 411 ); 412 413val STATEMENT_IS_WELL_FORMED = Q.store_thm ( 414 "STATEMENT_IS_WELL_FORMED", 415 `!stm. well_formed [translate_assignment stm]`, 416 RW_TAC list_ss [FORALL_DSTATE, well_formed_def, terminated_def, stopAt_def, status_independent_def] THENL [ 417 Cases_on `stm` THEN 418 (fn g => 419 (SIMP_TAC list_ss [closed_def, Once RUNTO_ADVANCE, UPLOAD_LEM_2, TRANSLATE_ASSIGMENT_CORRECT_2, SUC_ONE_ADD] THEN 420 RW_TAC set_ss [Once RUNTO_ADVANCE]) g 421 ), 422 Cases_on `stm` THEN 423 Q.EXISTS_TAC `SUC 0` THEN 424 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 425 RW_TAC arith_ss [FUNPOW, UPLOAD_LEM_2, step_def, TRANSLATE_ASSIGMENT_CORRECT_2, SUC_ONE_ADD], 426 Cases_on `stm` THEN 427 (fn g => 428 (SIMP_TAC list_ss [get_st_def, Once RUNTO_ADVANCE, SIMP_RULE std_ss [] (Q.SPEC `(pos0,cpsr0,regs,mem):STATE` 429 (INST_TYPE [alpha |-> Type `:word32 # (word4 |-> word32) # (word30 |-> word32)`] UPLOAD_LEM_2)), 430 TRANSLATE_ASSIGMENT_CORRECT_2, SUC_ONE_ADD] THEN 431 RW_TAC std_ss [Once RUNTO_ADVANCE] THEN 432 SIMP_TAC list_ss [get_st_def, Once RUNTO_ADVANCE, SIMP_RULE std_ss [] (Q.SPEC `(pos1,cpsr1,regs,mem):STATE` 433 (INST_TYPE [alpha |-> Type `:word32 # (word4 |-> word32) # (word30 |-> word32)`] UPLOAD_LEM_2)), 434 TRANSLATE_ASSIGMENT_CORRECT_2, SUC_ONE_ADD] THEN 435 RW_TAC std_ss [Once RUNTO_ADVANCE]) g 436 ) 437 ] 438 ); 439 440 441val BLOCK_IS_WELL_FORMED = Q.store_thm ( 442 "BLOCK_IS_WELL_FORMED", 443 `!stmL. WELL_FORMED (BLK stmL)`, 444 Induct_on `stmL` THENL [ 445 RW_TAC list_ss [WELL_FORMED_def, well_formed_def, translate_def, closed_def, terminated_def, status_independent_def, stopAt_def] THENL [ 446 RW_TAC set_ss [Once RUNTO_ADVANCE], 447 Q.EXISTS_TAC `0` THEN RW_TAC std_ss [FUNPOW], 448 RW_TAC arith_ss [Once RUNTO_ADVANCE, get_st_def] THEN RW_TAC arith_ss [Once RUNTO_ADVANCE] 449 ], 450 GEN_TAC THEN `!h tl. h :: tl = [h:INST] ++ tl` by RW_TAC list_ss [] THEN 451 METIS_TAC [WELL_FORMED_def, translate_def, mk_SC_def, SC_IS_WELL_FORMED, STATEMENT_IS_WELL_FORMED] 452 ] 453); 454 455val IR_SC_IS_WELL_FORMED = Q.store_thm ( 456 "IR_SC_IS_WELL_FORMED", 457 `!ir1 ir2. WELL_FORMED ir1 /\ WELL_FORMED ir2 = WELL_FORMED (SC ir1 ir2)`, 458 RW_TAC std_ss [WELL_FORMED_SUB_thm, WELL_FORMED_SUB_def, translate_def] THEN 459 PROVE_TAC [SC_IS_WELL_FORMED] 460 ); 461 462val IR_CJ_IS_WELL_FORMED = Q.store_thm ( 463 "IR_CJ_IS_WELL_FORMED", 464 `!cond ir_t ir_f. WELL_FORMED ir_t /\ WELL_FORMED ir_f = 465 WELL_FORMED (CJ cond ir_t ir_f)`, 466 RW_TAC std_ss [WELL_FORMED_SUB_thm, WELL_FORMED_SUB_def, translate_def] THEN 467 PROVE_TAC [CJ_IS_WELL_FORMED] 468 ); 469 470val IR_TR_IS_WELL_FORMED = Q.store_thm ( 471 "IR_TR_IS_WELL_FORMED", 472 `!ir cond. WELL_FORMED ir /\ WF_TR (translate_condition cond, translate ir) = 473 WELL_FORMED (TR cond ir)`, 474 RW_TAC std_ss [WELL_FORMED_SUB_thm, WELL_FORMED_SUB_def, translate_def] THEN 475 PROVE_TAC [TR_IS_WELL_FORMED] 476 ); 477 478val WELL_FORMED_thm = store_thm ("WELL_FORMED_thm", 479 ``(WELL_FORMED (BLK stmL) = T) /\ 480 (WELL_FORMED (SC S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 481 (WELL_FORMED (CJ cond S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 482 (WELL_FORMED (TR cond S1) = WELL_FORMED S1 /\ WF_TR (translate_condition cond, translate S1))``, 483 484 SIMP_TAC std_ss [BLOCK_IS_WELL_FORMED, IR_SC_IS_WELL_FORMED, IR_CJ_IS_WELL_FORMED, IR_TR_IS_WELL_FORMED]); 485 486 487(*---------------------------------------------------------------------------------*) 488(* Semantics of IR *) 489(*---------------------------------------------------------------------------------*) 490 491val IR_SEMANTICS_SC = Q.store_thm ( 492 "IR_SEMANTICS_SC", 493 `WELL_FORMED ir1 /\ WELL_FORMED ir2 ==> 494 (run_ir (SC ir1 ir2) st = 495 run_ir ir2 (run_ir ir1 st))`, 496 METIS_TAC [SIMP_RULE std_ss [] (Q.SPECL [`ir1`,`ir2`, `\st'. st' = st`, `\st'. st' = run_ir ir1 st`, `\st'. st' = run_ir ir1 st`, 497 `\st'. st' = run_ir ir2 (run_ir ir1 st)`] HOARE_SC_IR)] 498 ); 499 500 501val IR_SEMANTICS_BLK = Q.store_thm ( 502 "IR_SEMANTICS_BLK", 503 `(run_ir (BLK (stm::stmL)) st = 504 run_ir (BLK stmL) (mdecode st stm)) /\ 505 (run_ir (BLK []) st = st)`, 506 507 REPEAT STRIP_TAC THENL [ 508 RW_TAC list_ss [run_ir_def, translate_def] THEN 509 `translate_assignment stm::translate (BLK stmL) = translate (SC (BLK [stm]) (BLK stmL))` by RW_TAC list_ss [translate_def,mk_SC_def] THEN 510 RW_TAC std_ss [GSYM run_ir_def] THEN 511 `run_ir (BLK [stm]) st = mdecode st stm` by ( 512 RW_TAC list_ss [run_ir_def, run_arm_def, translate_def, Once RUNTO_ADVANCE] THEN 513 RW_TAC list_ss [GSYM uploadCode_def, UPLOADCODE_LEM] THEN 514 RW_TAC list_ss [GSYM TRANSLATE_ASSIGMENT_CORRECT, get_st_def, Once RUNTO_ADVANCE] 515 ) THEN 516 `well_formed [translate_assignment stm] /\ well_formed (translate (BLK stmL))` by 517 METIS_TAC [WELL_FORMED_def, BLOCK_IS_WELL_FORMED, STATEMENT_IS_WELL_FORMED] THEN 518 FULL_SIMP_TAC list_ss [WELL_FORMED_def, IR_SEMANTICS_SC, translate_def], 519 RW_TAC list_ss [run_ir_def, run_arm_def, translate_def, Once RUNTO_ADVANCE, get_st_def] 520 ] 521 ); 522 523val IR_SEMANTICS_CJ = Q.store_thm ( 524 "IR_SEMANTICS_CJ", 525 ` WELL_FORMED ir_t /\ WELL_FORMED ir_f ==> 526 (run_ir (CJ cond ir_t ir_f) st = 527 if eval_il_cond cond st then run_ir ir_t st 528 else run_ir ir_f st)`, 529 RW_TAC std_ss [] THEN 530 METIS_TAC [SIMP_RULE std_ss [] (Q.SPECL [`cond`, `ir_t`, `ir_f`, `\st'. st' = st`, `\st'. st' = run_ir ir_t st`, 531 `\st'. st' = run_ir ir_f st`] HOARE_CJ_IR)] 532 ); 533 534 535val IR_SEMANTICS_TR = Q.store_thm ( 536 "IR_SEMANTICS_TR", 537 `WELL_FORMED ir /\ WF_TR (translate_condition cond,translate ir) ==> 538 (run_ir (TR cond ir) st = 539 WHILE (\st'.~eval_il_cond cond st') (run_ir ir) st)`, 540 541 RW_TAC std_ss [WELL_FORMED_SUB_thm, run_ir_def, run_arm_def, translate_def, eval_il_cond_def] THEN 542 Q.ABBREV_TAC `arm = translate ir` THEN 543 IMP_RES_TAC (SIMP_RULE set_ss [] (Q.SPECL [`translate_condition cond`,`arm`,`(\i. ARB)`,`(0,0w,st):STATE`,`{}`] UNROLL_TR_LEM)) THEN 544 POP_ASSUM (ASSUME_TAC o Q.SPEC `st`) THEN 545 FULL_SIMP_TAC std_ss [FUNPOW,get_st_def] THEN 546 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 547 Induct_on `loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,st),{})` THENL [ 548 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW,get_st_def] THEN 549 IMP_RES_TAC LOOPNUM_BASIC THEN 550 FULL_SIMP_TAC arith_ss [Once WHILE, get_st_def], 551 552 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW] THEN 553 IMP_RES_TAC LOOPNUM_INDUCTIVE THEN 554 `v = loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,SND (SND (FST (runTo (upload arm (\i.ARB) 0) (LENGTH arm) ((0,0w,st),{}))))),{})` by 555 METIS_TAC [ABS_PAIR_THM,DECIDE (Term`!x.0+x=x`),LOOPNUM_INDEPENDENT_OF_CPSR_PCS, get_st_def, FST, SND, DSTATE_IRRELEVANT_PCS, 556 well_formed_def] THEN 557 RES_TAC THEN Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN 558 Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN 559 Q.PAT_ASSUM `~x` (ASSUME_TAC o SIMP_RULE std_ss [get_st_def]) THEN 560 RW_TAC std_ss [Once WHILE] THEN 561 Q.UNABBREV_TAC `arm` THEN 562 `run_ir ir st = SND (SND (FST (runTo (upload (translate ir) (\i. ARB) 0) (LENGTH (translate ir)) ((0,0w,st),{}))))` by RW_TAC arith_ss [ 563 get_st_def, run_ir_def, run_arm_def] THEN 564 METIS_TAC [SND,FST,get_st_def,FUNPOW_DSTATE, ABS_PAIR_THM] 565 ] 566 ); 567 568 569val IR_SEMANTICS_EMBEDDED_THM = Q.store_thm ( 570 "IR_SEMANTICS_EMBEDDED_THM", 571 `!ir s. well_formed (translate ir) ==> 572 (?pc cpsr pcS. 573 (run_arm (translate ir) s = ((pc, cpsr, run_ir ir (SND(SND(FST s)))), pcS)))`, 574 575 SIMP_TAC std_ss [run_ir_def, well_formed_def] THEN 576 REPEAT STRIP_TAC THEN 577 `?pc cpsr st pcS. (s = ((pc,cpsr,st),pcS))` by METIS_TAC[PAIR, FST, SND] THEN 578 ASM_REWRITE_TAC [run_arm_def] THEN 579 Q.ABBREV_TAC `arm = (translate ir)` THEN 580 `get_st (runTo (upload arm (\i. ARB) 0) (0 + LENGTH arm) ((0,0w,st),{})) = 581 get_st (runTo (upload arm (\i. ARB) pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS))` 582 by METIS_TAC[status_independent_def, DSTATE_IRRELEVANT_PCS, FST] THEN 583 ASM_SIMP_TAC std_ss [get_st_def] THEN 584 METIS_TAC[PAIR, FST, SND]); 585 586 587 588 589val WF_ir_TR_def = Define ` 590 WF_ir_TR (cond, ir) = 591 WF_Loop ((eval_il_cond cond), 592 (run_ir ir))`; 593 594 595val WF_ir_TR_thm = Q.store_thm ( 596 "WF_ir_TR_thm", 597 `!cond ir. WELL_FORMED ir ==> 598 (WF_ir_TR (cond, ir) = WF_TR (translate_condition cond, translate ir))`, 599 600SIMP_TAC std_ss [WF_ir_TR_def, WF_TR_def, WF_Loop_def, eval_il_cond_def, WELL_FORMED_SUB_thm] THEN 601REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 602 Q_TAC EXISTS_TAC `inv_image R get_st` THEN 603 ASM_SIMP_TAC std_ss [WF_inv_image] THEN 604 GEN_TAC THEN 605 `?pc' cpsr' pcS'. run_arm (translate ir) s = 606 ((pc',cpsr',run_ir ir (SND (SND (FST s)))),pcS')` by 607 METIS_TAC[IR_SEMANTICS_EMBEDDED_THM] THEN 608 `?pc cpsr st pcS. (s = ((pc,cpsr,st),pcS))` by METIS_TAC[PAIR, FST, SND] THEN 609 `runTo (upload (translate ir) iB pc) (pc + LENGTH (translate ir)) 610 ((pc,cpsr,st),pcS) = 611 run_arm (translate ir) ((pc,cpsr,st),pcS)` by ALL_TAC THEN1 ( 612 SIMP_TAC std_ss [run_arm_def] THEN 613 METIS_TAC[WELL_FORMED_INSTB, FST] 614 ) THEN 615 FULL_SIMP_TAC std_ss [relationTheory.inv_image_def, get_st_def], 616 617 618 619 FULL_SIMP_TAC std_ss [FORALL_PROD] THEN 620 `!iB pc cpsr st pcS. runTo (upload (translate ir) iB pc) (pc + LENGTH (translate ir)) 621 ((pc,cpsr,st),pcS) = 622 run_arm (translate ir) ((pc,cpsr,st),pcS)` by ALL_TAC THEN1 ( 623 SIMP_TAC std_ss [run_arm_def] THEN 624 METIS_TAC[WELL_FORMED_INSTB, FST] 625 ) THEN 626 FULL_SIMP_TAC std_ss [] THEN 627 POP_ASSUM (fn thm => ALL_TAC) THEN 628 629 `?Q. Q = \st st'. !s'. 630 let s = (run_arm (translate ir) s') in 631 (((get_st s' = st')) ==> ((get_st s = st) /\ 632 R s s'))` by METIS_TAC[] THEN 633 Q_TAC EXISTS_TAC `Q` THEN 634 REPEAT STRIP_TAC THENL [ 635 FULL_SIMP_TAC std_ss [WF_DEF, LET_THM] THEN 636 REPEAT STRIP_TAC THEN 637 `?B'. B' = (\s. B (get_st s))` by METIS_TAC[] THEN 638 Q.PAT_ASSUM `!B. (?w. B w) ==> X` (fn thm => Q_TAC 639 (fn t => (ASSUME_TAC (SPEC t thm))) `B'`) THEN 640 Q.PAT_UNDISCH_TAC `X` THEN 641 SIMP_TAC std_ss [GSYM LEFT_FORALL_IMP_THM, 642 GSYM LEFT_EXISTS_IMP_THM] THEN 643 644 `?w. B (get_st w)` by METIS_TAC[get_st_def, PAIR, FST, SND] THEN 645 Q_TAC EXISTS_TAC `w'` THEN 646 ASM_SIMP_TAC std_ss [] THEN 647 REPEAT STRIP_TAC THEN 648 Q_TAC EXISTS_TAC `get_st min` THEN 649 ASM_SIMP_TAC std_ss [] THEN 650 GEN_TAC THEN 651 Q_TAC EXISTS_TAC `min` THEN 652 SIMP_TAC std_ss [] THEN 653 METIS_TAC[], 654 655 656 FULL_SIMP_TAC std_ss [LET_THM, get_st_def, run_ir_def] THEN 657 GEN_TAC THEN 658 `?pc cpsr st pcS. (s' = ((pc,cpsr,st),pcS))` by METIS_TAC[PAIR, FST, SND] THEN 659 ASM_SIMP_TAC std_ss [] THEN 660 FULL_SIMP_TAC std_ss [GSYM get_st_def, run_arm_def, well_formed_def] THEN 661 662 `(LENGTH (translate ir)) = 0 + (LENGTH (translate ir))` by DECIDE_TAC THEN 663 METIS_TAC[status_independent_def, DSTATE_IRRELEVANT_PCS, FST] 664 ] 665]); 666 667 668 669val IR_SEMANTICS_TR___FUNPOW = Q.store_thm ( 670 "IR_SEMANTICS_TR___FUNPOW", 671 `WELL_FORMED ir /\ WF_TR (translate_condition cond,translate ir) ==> 672 (run_ir (TR cond ir) st = 673 FUNPOW (run_ir ir) (shortest (eval_il_cond cond) (run_ir ir) st) st)`, 674 675 676 SIMP_TAC std_ss [IR_SEMANTICS_TR] THEN 677 REPEAT STRIP_TAC THEN 678 `(\st'. ~eval_il_cond cond st') = $~ o (eval_il_cond cond)` by SIMP_TAC std_ss [combinTheory.o_DEF] THEN 679 ASM_SIMP_TAC std_ss [] THEN 680 MATCH_MP_TAC ARMCompositionTheory.UNROLL_LOOP THEN 681 METIS_TAC[WF_ir_TR_thm, WF_ir_TR_def]); 682 683 684 685 686val SEMANTICS_OF_IR = Q.store_thm ( 687 "SEMANTICS_OF_IR", 688 `(run_ir (BLK []) st = st) /\ 689 (run_ir (BLK (stm::stmL)) st = 690 run_ir (BLK stmL) (mdecode st stm)) /\ 691 ((WELL_FORMED ir1 /\ WELL_FORMED ir2) ==> 692 (run_ir (SC ir1 ir2) st = run_ir ir2 (run_ir ir1 st))) /\ 693 ((WELL_FORMED ir1 /\ WELL_FORMED ir2) ==> 694 (run_ir (CJ cond ir1 ir2) st = 695 (if eval_il_cond cond st then run_ir ir1 st else run_ir ir2 st))) /\ 696 (( WELL_FORMED ir1 /\ WF_TR (translate_condition cond,translate ir1)) ==> 697 (run_ir (TR cond ir1) st = 698 WHILE (\st'. ~eval_il_cond cond st') (run_ir ir1) st))`, 699 RW_TAC std_ss [IR_SEMANTICS_BLK, IR_SEMANTICS_CJ, IR_SEMANTICS_SC, IR_SEMANTICS_TR] 700 ); 701 702val _ = export_theory(); 703