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 305 306val UNCHANGED_THM = store_thm ("UNCHANGED_THM", 307 308 ``!s ir. 309 UNCHANGED s ir = 310 EVERY (\r. !reg mem. (read (reg,mem) (toREG r) = read (run_ir ir (reg,mem)) (toREG r))) s``, 311 312 SIMP_TAC std_ss [EVERY_MEM, UNCHANGED_def, ELIM_PFORALL] THEN 313 METIS_TAC[pairTheory.PAIR]) 314 315(*---------------------------------------------------------------------------------*) 316(* Hoare Rules for IR *) 317(*---------------------------------------------------------------------------------*) 318 319val HOARE_SC_IR = Q.store_thm ( 320 "HOARE_SC_IR", 321 `!ir1 ir2 P Q R T. 322 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 323 (!st. P st ==> Q (run_ir ir1 st)) /\ 324 (!st. R st ==> T (run_ir ir2 st)) /\ (!st. Q st ==> R st) ==> 325 !st. P st ==> 326 T (run_ir (SC ir1 ir2) st)`, 327 RW_TAC std_ss [WELL_FORMED_SUB_thm, run_ir_def, translate_def, run_arm_def, eval_fl_def] THEN 328 IMP_RES_TAC (SIMP_RULE std_ss [eval_fl_def, uploadCode_def] HOARE_SC_FLAT) 329 ); 330 331val HOARE_CJ_IR = Q.store_thm ( 332 "HOARE_CJ_IR", 333 `!cond ir_t ir_f P Q R. 334 WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 335 (!st. P st ==> Q (run_ir ir_t st)) /\ 336 (!st. P st ==> R (run_ir ir_f st)) ==> 337 !st. P st ==> 338 if eval_il_cond cond st then Q (run_ir (CJ cond ir_t ir_f) st) 339 else R (run_ir (CJ cond ir_t ir_f) st)`, 340 RW_TAC std_ss [WELL_FORMED_SUB_thm, run_ir_def, translate_def, run_arm_def, eval_fl_def, eval_il_cond_def] THEN 341 IMP_RES_TAC (SIMP_RULE std_ss [eval_fl_def, uploadCode_def] HOARE_CJ_FLAT) THEN 342 METIS_TAC [] 343 ); 344 345val HOARE_TR_IR = Q.store_thm ( 346 "HOARE_TR_IR", 347 `!cond ir P. 348 WELL_FORMED ir /\ WF_TR (translate_condition cond, translate ir) /\ 349 (!st. P st ==> P (run_ir ir st)) ==> 350 !st. P st ==> P (run_ir (TR cond ir) st) /\ 351 eval_il_cond cond (run_ir (TR cond ir) st)`, 352 RW_TAC std_ss [WELL_FORMED_SUB_thm, run_ir_def, translate_def, run_arm_def, eval_fl_def, eval_il_cond_def] THEN 353 METIS_TAC [SIMP_RULE std_ss [eval_fl_def, uploadCode_def] HOARE_TR_FLAT] 354 ); 355 356(*---------------------------------------------------------------------------------*) 357(* Well-formedness of IR *) 358(*---------------------------------------------------------------------------------*) 359 360val UPLOAD_LEM_2 = Q.store_thm ( 361 "UPLOAD_LEM_2", 362 `!s stm iB. (upload [stm] iB (FST s)) (FST s) = stm`, 363 RW_TAC std_ss [] THEN 364 `0 < LENGTH [stm]` by RW_TAC list_ss [] THEN 365 METIS_TAC [UPLOAD_LEM, FST, DECIDE (Term`!x.x + 0 = x`), EL, HD] 366 ); 367 368val STATEMENT_IS_WELL_FORMED = Q.store_thm ( 369 "STATEMENT_IS_WELL_FORMED", 370 `!stm. well_formed [translate_assignment stm]`, 371 RW_TAC list_ss [FORALL_DSTATE, well_formed_def, terminated_def, stopAt_def, status_independent_def] THENL [ 372 Cases_on `stm` THEN 373 (fn g => 374 (SIMP_TAC list_ss [closed_def, Once RUNTO_ADVANCE, UPLOAD_LEM_2, TRANSLATE_ASSIGMENT_CORRECT_2, SUC_ONE_ADD] THEN 375 RW_TAC set_ss [Once RUNTO_ADVANCE]) g 376 ), 377 Cases_on `stm` THEN 378 Q.EXISTS_TAC `SUC 0` THEN 379 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 380 RW_TAC arith_ss [FUNPOW, UPLOAD_LEM_2, step_def, TRANSLATE_ASSIGMENT_CORRECT_2, SUC_ONE_ADD], 381 Cases_on `stm` THEN 382 (fn g => 383 (SIMP_TAC list_ss [get_st_def, Once RUNTO_ADVANCE, SIMP_RULE std_ss [] (Q.SPEC `(pos0,cpsr0,regs,mem):STATE` 384 (INST_TYPE [alpha |-> Type `:word32 # (word4 |-> word32) # (word30 |-> word32)`] UPLOAD_LEM_2)), 385 TRANSLATE_ASSIGMENT_CORRECT_2, SUC_ONE_ADD] THEN 386 RW_TAC std_ss [Once RUNTO_ADVANCE] THEN 387 SIMP_TAC list_ss [get_st_def, Once RUNTO_ADVANCE, SIMP_RULE std_ss [] (Q.SPEC `(pos1,cpsr1,regs,mem):STATE` 388 (INST_TYPE [alpha |-> Type `:word32 # (word4 |-> word32) # (word30 |-> word32)`] UPLOAD_LEM_2)), 389 TRANSLATE_ASSIGMENT_CORRECT_2, SUC_ONE_ADD] THEN 390 RW_TAC std_ss [Once RUNTO_ADVANCE]) g 391 ) 392 ] 393 ); 394 395 396val BLOCK_IS_WELL_FORMED = Q.store_thm ( 397 "BLOCK_IS_WELL_FORMED", 398 `!stmL. WELL_FORMED (BLK stmL)`, 399 Induct_on `stmL` THENL [ 400 RW_TAC list_ss [WELL_FORMED_def, well_formed_def, translate_def, closed_def, terminated_def, status_independent_def, stopAt_def] THENL [ 401 RW_TAC set_ss [Once RUNTO_ADVANCE], 402 Q.EXISTS_TAC `0` THEN RW_TAC std_ss [FUNPOW], 403 RW_TAC arith_ss [Once RUNTO_ADVANCE, get_st_def] THEN RW_TAC arith_ss [Once RUNTO_ADVANCE] 404 ], 405 GEN_TAC THEN `!h tl. h :: tl = [h:INST] ++ tl` by RW_TAC list_ss [] THEN 406 METIS_TAC [WELL_FORMED_def, translate_def, mk_SC_def, SC_IS_WELL_FORMED, STATEMENT_IS_WELL_FORMED] 407 ] 408); 409 410val IR_SC_IS_WELL_FORMED = Q.store_thm ( 411 "IR_SC_IS_WELL_FORMED", 412 `!ir1 ir2. WELL_FORMED ir1 /\ WELL_FORMED ir2 = WELL_FORMED (SC ir1 ir2)`, 413 RW_TAC std_ss [WELL_FORMED_SUB_thm, WELL_FORMED_SUB_def, translate_def] THEN 414 PROVE_TAC [SC_IS_WELL_FORMED] 415 ); 416 417val IR_CJ_IS_WELL_FORMED = Q.store_thm ( 418 "IR_CJ_IS_WELL_FORMED", 419 `!cond ir_t ir_f. WELL_FORMED ir_t /\ WELL_FORMED ir_f = 420 WELL_FORMED (CJ cond ir_t ir_f)`, 421 RW_TAC std_ss [WELL_FORMED_SUB_thm, WELL_FORMED_SUB_def, translate_def] THEN 422 PROVE_TAC [CJ_IS_WELL_FORMED] 423 ); 424 425val IR_TR_IS_WELL_FORMED = Q.store_thm ( 426 "IR_TR_IS_WELL_FORMED", 427 `!ir cond. WELL_FORMED ir /\ WF_TR (translate_condition cond, translate ir) = 428 WELL_FORMED (TR cond ir)`, 429 RW_TAC std_ss [WELL_FORMED_SUB_thm, WELL_FORMED_SUB_def, translate_def] THEN 430 PROVE_TAC [TR_IS_WELL_FORMED] 431 ); 432 433val WELL_FORMED_thm = store_thm ("WELL_FORMED_thm", 434 ``(WELL_FORMED (BLK stmL) = T) /\ 435 (WELL_FORMED (SC S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 436 (WELL_FORMED (CJ cond S1 S2) = WELL_FORMED S1 /\ WELL_FORMED S2) /\ 437 (WELL_FORMED (TR cond S1) = WELL_FORMED S1 /\ WF_TR (translate_condition cond, translate S1))``, 438 439 SIMP_TAC std_ss [BLOCK_IS_WELL_FORMED, IR_SC_IS_WELL_FORMED, IR_CJ_IS_WELL_FORMED, IR_TR_IS_WELL_FORMED]); 440 441 442(*---------------------------------------------------------------------------------*) 443(* Semantics of IR *) 444(*---------------------------------------------------------------------------------*) 445 446val IR_SEMANTICS_SC = Q.store_thm ( 447 "IR_SEMANTICS_SC", 448 `WELL_FORMED ir1 /\ WELL_FORMED ir2 ==> 449 (run_ir (SC ir1 ir2) st = 450 run_ir ir2 (run_ir ir1 st))`, 451 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`, 452 `\st'. st' = run_ir ir2 (run_ir ir1 st)`] HOARE_SC_IR)] 453 ); 454 455 456val IR_SEMANTICS_BLK = Q.store_thm ( 457 "IR_SEMANTICS_BLK", 458 `(run_ir (BLK (stm::stmL)) st = 459 run_ir (BLK stmL) (mdecode st stm)) /\ 460 (run_ir (BLK []) st = st)`, 461 462 REPEAT STRIP_TAC THENL [ 463 RW_TAC list_ss [run_ir_def, translate_def] THEN 464 `translate_assignment stm::translate (BLK stmL) = translate (SC (BLK [stm]) (BLK stmL))` by RW_TAC list_ss [translate_def,mk_SC_def] THEN 465 RW_TAC std_ss [GSYM run_ir_def] THEN 466 `run_ir (BLK [stm]) st = mdecode st stm` by ( 467 RW_TAC list_ss [run_ir_def, run_arm_def, translate_def, Once RUNTO_ADVANCE] THEN 468 RW_TAC list_ss [GSYM uploadCode_def, UPLOADCODE_LEM] THEN 469 RW_TAC list_ss [GSYM TRANSLATE_ASSIGMENT_CORRECT, get_st_def, Once RUNTO_ADVANCE] 470 ) THEN 471 `well_formed [translate_assignment stm] /\ well_formed (translate (BLK stmL))` by 472 METIS_TAC [WELL_FORMED_def, BLOCK_IS_WELL_FORMED, STATEMENT_IS_WELL_FORMED] THEN 473 FULL_SIMP_TAC list_ss [WELL_FORMED_def, IR_SEMANTICS_SC, translate_def], 474 RW_TAC list_ss [run_ir_def, run_arm_def, translate_def, Once RUNTO_ADVANCE, get_st_def] 475 ] 476 ); 477 478val IR_SEMANTICS_CJ = Q.store_thm ( 479 "IR_SEMANTICS_CJ", 480 ` WELL_FORMED ir_t /\ WELL_FORMED ir_f ==> 481 (run_ir (CJ cond ir_t ir_f) st = 482 if eval_il_cond cond st then run_ir ir_t st 483 else run_ir ir_f st)`, 484 RW_TAC std_ss [] THEN 485 METIS_TAC [SIMP_RULE std_ss [] (Q.SPECL [`cond`, `ir_t`, `ir_f`, `\st'. st' = st`, `\st'. st' = run_ir ir_t st`, 486 `\st'. st' = run_ir ir_f st`] HOARE_CJ_IR)] 487 ); 488 489 490val IR_SEMANTICS_TR = Q.store_thm ( 491 "IR_SEMANTICS_TR", 492 `WELL_FORMED ir /\ WF_TR (translate_condition cond,translate ir) ==> 493 (run_ir (TR cond ir) st = 494 WHILE (\st'.~eval_il_cond cond st') (run_ir ir) st)`, 495 496 RW_TAC std_ss [WELL_FORMED_SUB_thm, run_ir_def, run_arm_def, translate_def, eval_il_cond_def] THEN 497 Q.ABBREV_TAC `arm = translate ir` THEN 498 IMP_RES_TAC (SIMP_RULE set_ss [] (Q.SPECL [`translate_condition cond`,`arm`,`(\i. ARB)`,`(0,0w,st):STATE`,`{}`] UNROLL_TR_LEM)) THEN 499 POP_ASSUM (ASSUME_TAC o Q.SPEC `st`) THEN 500 FULL_SIMP_TAC std_ss [FUNPOW,get_st_def] THEN 501 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 502 Induct_on `loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,st),{})` THENL [ 503 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW,get_st_def] THEN 504 IMP_RES_TAC LOOPNUM_BASIC THEN 505 FULL_SIMP_TAC arith_ss [Once WHILE, get_st_def], 506 507 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW] THEN 508 IMP_RES_TAC LOOPNUM_INDUCTIVE THEN 509 `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 510 METIS_TAC [ABS_PAIR_THM,DECIDE (Term`!x.0+x=x`),LOOPNUM_INDEPENDENT_OF_CPSR_PCS, get_st_def, FST, SND, DSTATE_IRRELEVANT_PCS, 511 well_formed_def] THEN 512 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 513 Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN 514 Q.PAT_ASSUM `~x` (ASSUME_TAC o SIMP_RULE std_ss [get_st_def]) THEN 515 RW_TAC std_ss [Once WHILE] THEN 516 Q.UNABBREV_TAC `arm` THEN 517 `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 [ 518 get_st_def, run_ir_def, run_arm_def] THEN 519 METIS_TAC [SND,FST,get_st_def,FUNPOW_DSTATE, ABS_PAIR_THM] 520 ] 521 ); 522 523 524val IR_SEMANTICS_EMBEDDED_THM = Q.store_thm ( 525 "IR_SEMANTICS_EMBEDDED_THM", 526 `!ir s. well_formed (translate ir) ==> 527 (?pc cpsr pcS. 528 (run_arm (translate ir) s = ((pc, cpsr, run_ir ir (SND(SND(FST s)))), pcS)))`, 529 530 SIMP_TAC std_ss [run_ir_def, well_formed_def] THEN 531 REPEAT STRIP_TAC THEN 532 `?pc cpsr st pcS. (s = ((pc,cpsr,st),pcS))` by METIS_TAC[PAIR, FST, SND] THEN 533 ASM_REWRITE_TAC [run_arm_def] THEN 534 Q.ABBREV_TAC `arm = (translate ir)` THEN 535 `get_st (runTo (upload arm (\i. ARB) 0) (0 + LENGTH arm) ((0,0w,st),{})) = 536 get_st (runTo (upload arm (\i. ARB) pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS))` 537 by METIS_TAC[status_independent_def, DSTATE_IRRELEVANT_PCS, FST] THEN 538 ASM_SIMP_TAC std_ss [get_st_def] THEN 539 METIS_TAC[PAIR, FST, SND]); 540 541 542 543 544val WF_ir_TR_def = Define ` 545 WF_ir_TR (cond, ir) = 546 WF_Loop ((eval_il_cond cond), 547 (run_ir ir))`; 548 549 550val WF_ir_TR_thm = Q.store_thm ( 551 "WF_ir_TR_thm", 552 `!cond ir. WELL_FORMED ir ==> 553 (WF_ir_TR (cond, ir) = WF_TR (translate_condition cond, translate ir))`, 554 555SIMP_TAC std_ss [WF_ir_TR_def, WF_TR_def, WF_Loop_def, eval_il_cond_def, WELL_FORMED_SUB_thm] THEN 556REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 557 Q_TAC EXISTS_TAC `inv_image R get_st` THEN 558 ASM_SIMP_TAC std_ss [WF_inv_image] THEN 559 GEN_TAC THEN 560 `?pc' cpsr' pcS'. run_arm (translate ir) s = 561 ((pc',cpsr',run_ir ir (SND (SND (FST s)))),pcS')` by 562 METIS_TAC[IR_SEMANTICS_EMBEDDED_THM] THEN 563 `?pc cpsr st pcS. (s = ((pc,cpsr,st),pcS))` by METIS_TAC[PAIR, FST, SND] THEN 564 `runTo (upload (translate ir) iB pc) (pc + LENGTH (translate ir)) 565 ((pc,cpsr,st),pcS) = 566 run_arm (translate ir) ((pc,cpsr,st),pcS)` by ALL_TAC THEN1 ( 567 SIMP_TAC std_ss [run_arm_def] THEN 568 METIS_TAC[WELL_FORMED_INSTB, FST] 569 ) THEN 570 FULL_SIMP_TAC std_ss [relationTheory.inv_image_def, get_st_def], 571 572 573 574 FULL_SIMP_TAC std_ss [FORALL_PROD] THEN 575 `!iB pc cpsr st pcS. runTo (upload (translate ir) iB pc) (pc + LENGTH (translate ir)) 576 ((pc,cpsr,st),pcS) = 577 run_arm (translate ir) ((pc,cpsr,st),pcS)` by ALL_TAC THEN1 ( 578 SIMP_TAC std_ss [run_arm_def] THEN 579 METIS_TAC[WELL_FORMED_INSTB, FST] 580 ) THEN 581 FULL_SIMP_TAC std_ss [] THEN 582 POP_ASSUM (fn thm => ALL_TAC) THEN 583 584 `?Q. Q = \st st'. !s'. 585 let s = (run_arm (translate ir) s') in 586 (((get_st s' = st')) ==> ((get_st s = st) /\ 587 R s s'))` by METIS_TAC[] THEN 588 Q_TAC EXISTS_TAC `Q` THEN 589 REPEAT STRIP_TAC THENL [ 590 FULL_SIMP_TAC std_ss [WF_DEF, LET_THM] THEN 591 REPEAT STRIP_TAC THEN 592 `?B'. B' = (\s. B (get_st s))` by METIS_TAC[] THEN 593 Q.PAT_ASSUM `!B. (?w. B w) ==> X` (fn thm => Q_TAC 594 (fn t => (ASSUME_TAC (SPEC t thm))) `B'`) THEN 595 Q.PAT_UNDISCH_TAC `X` THEN 596 SIMP_TAC std_ss [GSYM LEFT_FORALL_IMP_THM, 597 GSYM LEFT_EXISTS_IMP_THM] THEN 598 599 `?w. B (get_st w)` by METIS_TAC[get_st_def, PAIR, FST, SND] THEN 600 Q_TAC EXISTS_TAC `w'` THEN 601 ASM_SIMP_TAC std_ss [] THEN 602 REPEAT STRIP_TAC THEN 603 Q_TAC EXISTS_TAC `get_st min` THEN 604 ASM_SIMP_TAC std_ss [] THEN 605 GEN_TAC THEN 606 Q_TAC EXISTS_TAC `min` THEN 607 SIMP_TAC std_ss [] THEN 608 METIS_TAC[], 609 610 611 FULL_SIMP_TAC std_ss [LET_THM, get_st_def, run_ir_def] THEN 612 GEN_TAC THEN 613 `?pc cpsr st pcS. (s' = ((pc,cpsr,st),pcS))` by METIS_TAC[PAIR, FST, SND] THEN 614 ASM_SIMP_TAC std_ss [] THEN 615 FULL_SIMP_TAC std_ss [GSYM get_st_def, run_arm_def, well_formed_def] THEN 616 617 `(LENGTH (translate ir)) = 0 + (LENGTH (translate ir))` by DECIDE_TAC THEN 618 METIS_TAC[status_independent_def, DSTATE_IRRELEVANT_PCS, FST] 619 ] 620]); 621 622 623 624val IR_SEMANTICS_TR___FUNPOW = Q.store_thm ( 625 "IR_SEMANTICS_TR___FUNPOW", 626 `WELL_FORMED ir /\ WF_TR (translate_condition cond,translate ir) ==> 627 (run_ir (TR cond ir) st = 628 FUNPOW (run_ir ir) (shortest (eval_il_cond cond) (run_ir ir) st) st)`, 629 630 631 SIMP_TAC std_ss [IR_SEMANTICS_TR] THEN 632 REPEAT STRIP_TAC THEN 633 `(\st'. ~eval_il_cond cond st') = $~ o (eval_il_cond cond)` by SIMP_TAC std_ss [combinTheory.o_DEF] THEN 634 ASM_SIMP_TAC std_ss [] THEN 635 MATCH_MP_TAC ARMCompositionTheory.UNROLL_LOOP THEN 636 METIS_TAC[WF_ir_TR_thm, WF_ir_TR_def]); 637 638 639 640 641val SEMANTICS_OF_IR = Q.store_thm ( 642 "SEMANTICS_OF_IR", 643 `(run_ir (BLK []) st = st) /\ 644 (run_ir (BLK (stm::stmL)) st = 645 run_ir (BLK stmL) (mdecode st stm)) /\ 646 ((WELL_FORMED ir1 /\ WELL_FORMED ir2) ==> 647 (run_ir (SC ir1 ir2) st = run_ir ir2 (run_ir ir1 st))) /\ 648 ((WELL_FORMED ir1 /\ WELL_FORMED ir2) ==> 649 (run_ir (CJ cond ir1 ir2) st = 650 (if eval_il_cond cond st then run_ir ir1 st else run_ir ir2 st))) /\ 651 (( WELL_FORMED ir1 /\ WF_TR (translate_condition cond,translate ir1)) ==> 652 (run_ir (TR cond ir1) st = 653 WHILE (\st'. ~eval_il_cond cond st') (run_ir ir1) st))`, 654 RW_TAC std_ss [IR_SEMANTICS_BLK, IR_SEMANTICS_CJ, IR_SEMANTICS_SC, IR_SEMANTICS_TR] 655 ); 656 657val _ = export_theory(); 658