1 2(* 3quietdec := true; 4 5app load ["arithmeticTheory", "wordsTheory", "wordsLib", "pairTheory", "listTheory", "whileTheory", "finite_mapTheory", 6 "pred_setSimps", "pred_setTheory", "preARMTheory", "ARMCompositionTheory", "bigInstTheory", "funCallTheory", 7 "CFLTheory", "HSLTheory", "simplifier"]; 8 9open HolKernel Parse boolLib bossLib numLib arithmeticTheory wordsTheory wordsLib pairTheory listTheory whileTheory 10 pred_setSimps pred_setTheory finite_mapTheory preARMTheory bigInstTheory funCallTheory 11 CFLTheory HSLTheory simplifier; 12 13quietdec := false; 14*) 15 16open HolKernel Parse boolLib bossLib numLib arithmeticTheory wordsTheory wordsLib pairTheory listTheory whileTheory 17 pred_setSimps pred_setTheory finite_mapTheory preARMTheory bigInstTheory funCallTheory 18 CFLTheory HSLTheory simplifier; 19 20(*---------------------------------------------------------------------------------*) 21 22val _ = new_theory "HSL2CFL"; 23 24(*---------------------------------------------------------------------------------*) 25(* Translation from HSL to CFL *) 26(*---------------------------------------------------------------------------------*) 27 28val conv_roc_def = Define ` 29 (conv_roc (Rg r) = MR (conv_reg r)) /\ 30 (conv_roc (Cn v) = MC v) 31 `; 32 33val toLocn_def = Define ` 34 toLocn i = (fp, NEG (12 + i))`; 35 36val translate_assgn_def = Define ` 37 (translate_assgn (TLDR dst_reg src_mem) = MLDR (conv_reg dst_reg) (toLocn src_mem)) /\ 38 (translate_assgn (TSTR dst_mem src_reg) = MSTR (toLocn dst_mem) (conv_reg src_reg)) /\ 39 (translate_assgn (TMOV dst src) = MMOV (conv_reg dst) (conv_roc src)) /\ 40 41 (translate_assgn (TADD dst (Rg r) src) = MADD (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 42 (translate_assgn (TADD dst (Cn v) (Rg r)) = MADD (conv_reg dst) (conv_reg r) (MC v)) /\ 43 (translate_assgn (TADD dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1+v2))) /\ 44 (translate_assgn (TSUB dst (Rg r) src) = MSUB (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 45 (translate_assgn (TSUB dst (Cn v) (Rg r)) = MRSB (conv_reg dst) (conv_reg r) (MC v)) /\ 46 (translate_assgn (TSUB dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1-v2))) /\ 47 (translate_assgn (TRSB dst (Rg r) src) = MRSB (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 48 (translate_assgn (TRSB dst (Cn v) (Rg r)) = MSUB (conv_reg dst) (conv_reg r) (MC v)) /\ 49 (translate_assgn (TRSB dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v2-v1))) /\ 50 (translate_assgn (TMUL dst (Rg r) src) = MMUL (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 51 (translate_assgn (TMUL dst (Cn v) (Rg r)) = MMUL (conv_reg dst) (conv_reg r) (MC v)) /\ 52 (translate_assgn (TMUL dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1*v2))) /\ 53 (translate_assgn (TAND dst (Rg r) src) = MAND (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 54 (translate_assgn (TAND dst (Cn v) (Rg r)) = MAND (conv_reg dst) (conv_reg r) (MC v)) /\ 55 (translate_assgn (TAND dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1 && v2))) /\ 56 (translate_assgn (TORR dst (Rg r) src) = MORR (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 57 (translate_assgn (TORR dst (Cn v) (Rg r)) = MORR (conv_reg dst) (conv_reg r) (MC v)) /\ 58 (translate_assgn (TORR dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1 !! v2))) /\ 59 (translate_assgn (TEOR dst (Rg r) src) = MEOR (conv_reg dst) (conv_reg r) (conv_roc src)) /\ 60 (translate_assgn (TEOR dst (Cn v) (Rg r)) = MEOR (conv_reg dst) (conv_reg r) (MC v)) /\ 61 (translate_assgn (TEOR dst (Cn v1) (Cn v2)) = MMOV (conv_reg dst) (MC (v1 ?? v2))) /\ 62 63 (translate_assgn (TLSL dst (Rg r) src2_num) = MLSL (conv_reg dst) (conv_reg r) src2_num) /\ 64 (translate_assgn (TLSL dst (Cn v) src2_num) = MMOV (conv_reg dst) (MC (v << w2n src2_num))) /\ 65 (translate_assgn (TLSR dst (Rg r) src2_num) = MLSR (conv_reg dst) (conv_reg r) src2_num) /\ 66 (translate_assgn (TLSR dst (Cn v) src2_num) = MMOV (conv_reg dst) (MC (v >>> w2n src2_num))) /\ 67 (translate_assgn (TASR dst (Rg r) src2_num) = MASR (conv_reg dst) (conv_reg r) src2_num) /\ 68 (translate_assgn (TASR dst (Cn v) src2_num) = MMOV (conv_reg dst) (MC (v >> w2n src2_num))) /\ 69 (translate_assgn (TROR dst (Rg r) src2_num) = MROR (conv_reg dst) (conv_reg r) src2_num) /\ 70 (translate_assgn (TROR dst (Cn v) src2_num) = MMOV (conv_reg dst) (MC (v #>> w2n src2_num))) 71 `; 72 73val translate_TCND_def = Define ` 74 translate_TCND (r, c, e) = 75 (conv_reg r, c, conv_roc e)`; 76 77val translate_hsl_def = Define ` 78 (translate_hsl (Blk stmL) = BLK (MAP translate_assgn stmL)) /\ 79 (translate_hsl (Sc S1 S2) = 80 SC (translate_hsl S1) (translate_hsl S2)) /\ 81 (translate_hsl (Cj cond Strue Sfalse) = 82 CJ (translate_TCND cond) (translate_hsl Strue) (translate_hsl Sfalse)) /\ 83 (translate_hsl (Tr cond Sbody) = 84 TR (translate_TCND cond) (translate_hsl Sbody)) /\ 85 (translate_hsl (Fc (caller_i, callee_i) S_body (caller_o, callee_o) (m1,m2)) = 86 SC (SC (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) 87 (MAX (LENGTH caller_i) (LENGTH caller_o) - (LENGTH caller_i)) m2)) 88 (translate_hsl S_body)) 89 (BLK (post_call (MAP conv_exp caller_o, MAP conv_exp callee_o) m1)))`; 90 91(*---------------------------------------------------------------------------------*) 92(* Data registers are separate from pointer registers *) 93(*---------------------------------------------------------------------------------*) 94 95val data_reg_lem_1 = Q.store_thm ( 96 "data_reg_lem_1", 97 `!r. index_of_reg (conv_reg r) = data_reg_index r`, 98 Cases_on `r` THEN 99 100 RW_TAC std_ss [data_reg_index_def, conv_reg_def, index_of_reg_def, from_reg_index_def, index_of_reg_def] 101 ); 102 103val data_reg_lem_2 = Q.store_thm ( 104 "data_reg_lem_2", 105 `!r r''. (data_reg_index r = data_reg_index r'') = (r = r'')`, 106 Cases_on `r` THEN Cases_on `r''` THEN 107 RW_TAC std_ss [data_reg_index_def] 108 ); 109 110val data_reg_lem_3 = Q.store_thm ( 111 "data_reg_lem_3", 112 `!r. (data_reg_index r < 9) /\ ~(data_reg_index r = 10) /\ ~(data_reg_index r = 11) /\ 113 ~(data_reg_index r = 12) /\ ~(data_reg_index r = 13) /\ ~(data_reg_index r = 14)`, 114 Cases_on `r` THEN 115 RW_TAC arith_ss [data_reg_index_def] 116 ); 117 118val locate_ge_lem_3 = Q.store_thm ( 119 "locate_ge_lem_3", 120 `!x k. locate_ge x (12 + k) ==> 121 !i j. ~(i = j) /\ (i < k) /\ (j < k) ==> 122 ~(w2n x - (12 + i) = w2n x - (12 + j))`, 123 RW_TAC arith_ss [locate_ge_def] 124 ); 125 126(*---------------------------------------------------------------------------------*) 127(* Decode assignment statement *) 128(*---------------------------------------------------------------------------------*) 129 130val correspond_def = Define ` 131 correspond (rg,sk) st m = 132 (!r. rg ' (data_reg_index r) = read st (REG (data_reg_index r))) /\ 133 (!i. (i < m) ==> (sk ' i = read st (MEM (toLocn i)))) 134 `; 135 136val CORRESPOND_SAME_CONTENT = Q.store_thm ( 137 "CORRESPOND_SAME_CONTENT", 138 `correspond = same_content`, 139 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_TSTATE] THEN 140 REPEAT STRIP_TAC THEN EQ_TAC THEN 141 RW_TAC std_ss [correspond_def, same_content_def] THEN 142 FULL_SIMP_TAC std_ss [read_thm, data_reg_index_def, conv_exp_def, reade_def, toLocn_def] 143 ); 144 145(*---------------------------------------------------------------------------------*) 146(* Validation on the translation of single instructions *) 147(*---------------------------------------------------------------------------------*) 148 149val LDR_CORRESPOND_LEM = Q.store_thm ( 150 "LDR_CORRESPOND_LEM", 151 `!rg sk st T' T0 m. 152 valid_assgn (TLDR T' T0) m /\ correspond (rg,sk) st m ==> 153 correspond (tdecode (rg,sk) (TLDR T' T0)) (mdecode st (translate_assgn (TLDR T' T0))) m`, 154 155 SIMP_TAC std_ss [FORALL_DSTATE] THEN 156 FULL_SIMP_TAC std_ss [translate_assgn_def, toLocn_def, valid_assgn_def, within_bound_def] THEN 157 RW_TAC finmap_ss [correspond_def, fp_def, tdecode_def, twrite_def, tread_def, mdecode_def, toREG_def, 158 toMEM_def, write_thm, toEXP_def, toEXP_def, read_thm, toLocn_def, data_reg_lem_1, data_reg_lem_2] THEN 159 METIS_TAC [data_reg_lem_3] 160 ); 161 162val STR_CORRESPOND_LEM = Q.store_thm ( 163 "STR_CORRESPOND_LEM", 164 `!rg sk st T' T0 m. 165 valid_assgn (TSTR T' T0) m /\ locate_ge (read st FP) (12 + m) /\ 166 correspond (rg,sk) st m ==> 167 correspond (tdecode (rg,sk) (TSTR T' T0)) (mdecode st (translate_assgn (TSTR T' T0))) m`, 168 169 SIMP_TAC std_ss [FORALL_DSTATE] THEN 170 RW_TAC std_ss [translate_assgn_def, toLocn_def, valid_assgn_def, within_bound_def] THEN 171 FULL_SIMP_TAC finmap_ss [correspond_def, FP_def, fp_def, tdecode_def, twrite_def, tread_def, mdecode_def, 172 toREG_def, toMEM_def, write_thm, toEXP_def, toEXP_def, read_thm, toLocn_def, data_reg_lem_1] THEN 173 RW_TAC std_ss [] THEN 174 METIS_TAC [locate_ge_lem_3] 175 ); 176 177val ASSGN_CORRESPOND = Q.store_thm ( 178 "ASSGN_CORRESPOND", 179 `!rg sk st stm m. 180 valid_assgn stm m /\ locate_ge (read st FP) (12 + m) /\ 181 correspond (rg,sk) st m ==> 182 correspond (tdecode (rg,sk) stm) (mdecode st (translate_assgn stm)) m`, 183 184 let val tac1 = 185 FULL_SIMP_TAC finmap_ss [correspond_def, translate_assgn_def, tdecode_def, twrite_def, tread_def, mdecode_def, 186 toREG_def, toMEM_def, write_thm, toEXP_def, conv_roc_def, toEXP_def, read_thm, roc_2_exp_def, 187 data_reg_lem_1, data_reg_lem_2, toLocn_def] THEN 188 RW_TAC std_ss [data_reg_lem_3, fp_def] THEN 189 RW_TAC std_ss [WORD_ADD_COMM, WORD_MULT_COMM, WORD_AND_COMM, WORD_OR_COMM, WORD_XOR_COMM] 190 in 191 192 SIMP_TAC std_ss [FORALL_DSTATE] THEN 193 REPEAT STRIP_TAC THEN 194 Cases_on `stm` THENL [ 195 METIS_TAC [LDR_CORRESPOND_LEM], (* LDR *) 196 METIS_TAC [STR_CORRESPOND_LEM], (* STR *) 197 Cases_on `T0` THEN tac1, (* MOV *) 198 Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* ADD *) 199 Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* SUB *) 200 Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* RSB *) 201 Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* MUL *) 202 Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* AND *) 203 Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* ORR *) 204 Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* EOR *) 205 Cases_on `T0` THEN tac1, (* LSL *) 206 Cases_on `T0` THEN tac1, (* LSR *) 207 Cases_on `T0` THEN tac1, (* ASR *) 208 Cases_on `T0` THEN tac1 (* ROR *) 209 ] 210 end 211 ); 212 213(*---------------------------------------------------------------------------------*) 214(* All heap and stack operations in each instruction should be within the *) 215(* predefined domains *) 216(* The heap area and the stack area are separate *) 217(* Data registers include only r0-r8 *) 218(*---------------------------------------------------------------------------------*) 219 220val ASSGN_STATUS_INTACT = Q.store_thm ( 221 "ASSGN_STATUS_INTACT", 222 `!stm st. let st' = mdecode st (translate_assgn stm) in 223 status_intact st' st`, 224 225 let val tac1 = SIMP_TAC std_ss [FORALL_DSTATE, translate_assgn_def, mdecode_def, LET_THM] THEN 226 RW_TAC finmap_ss [valid_assgn_def, valid_TEXP_def, toREG_def, index_of_reg_def, read_thm, write_thm, 227 reade_def, toLocn_def, toMEM_def, IP_def, FP_def, SP_def, LR_def, data_reg_lem_1, data_reg_lem_3] 228 THEN FULL_SIMP_TAC arith_ss [fp_def] 229 in 230 SIMP_TAC std_ss [status_intact_def, same_fp_ip_sp_def] THEN 231 Cases_on `stm` THENL [ 232 Cases_on `T'` THEN tac1, (* LDR *) 233 Cases_on `T'` THEN tac1, (* STR *) 234 Cases_on `T'` THEN tac1, (* MOV *) 235 Cases_on `T'` THEN Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* ADD *) 236 Cases_on `T'` THEN Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* SUB *) 237 Cases_on `T'` THEN Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* RSB *) 238 Cases_on `T'` THEN Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* MUL *) 239 Cases_on `T'` THEN Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* AND *) 240 Cases_on `T'` THEN Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* ORR *) 241 Cases_on `T'` THEN Cases_on `T0` THEN Cases_on `T1` THEN tac1, (* EOR *) 242 Cases_on `T'` THEN Cases_on `T0` THEN tac1, (* LSL *) 243 Cases_on `T'` THEN Cases_on `T0` THEN tac1, (* LSR *) 244 Cases_on `T'` THEN Cases_on `T0` THEN tac1, (* ASR *) 245 Cases_on `T'` THEN Cases_on `T0` THEN tac1 (* ROR *) 246 ] 247 end 248 ); 249 250(*---------------------------------------------------------------------------------*) 251(* Correspondence for basic blocks *) 252(*---------------------------------------------------------------------------------*) 253 254val BLK_CORRESPONDENCE = Q.store_thm ( 255 "BLK_CORRESPONDENCE", 256 `!rg sk st stmL m. 257 valid_struct (Blk stmL) m /\ locate_ge (read st FP) (12 + m) /\ 258 correspond (rg,sk) st m ==> 259 correspond (run_hsl (Blk stmL) (rg,sk)) (run_cfl (translate_hsl (Blk stmL)) st) m`, 260 261 Induct_on `stmL` THENL [ 262 RW_TAC list_ss [correspond_def, run_hsl_def, translate_hsl_def, CFL_SEMANTICS_BLK], 263 RW_TAC list_ss [valid_struct_def, run_hsl_def, translate_hsl_def, CFL_SEMANTICS_BLK] THEN 264 `?rg' sk'. (rg',sk') = tdecode (rg,sk) h` by METIS_TAC [ABS_PAIR_THM] THEN 265 Q.PAT_ASSUM `!rg sk st m.x` (ASSUME_TAC o SIMP_RULE std_ss [valid_struct_def, translate_hsl_def] o 266 Q.SPECL [`rg'`,`sk'`,`mdecode st (translate_assgn h)`, `m`]) THEN 267 `read (mdecode st (translate_assgn h)) FP = read st FP` by 268 METIS_TAC [SIMP_RULE std_ss [LET_THM, status_intact_def, same_fp_ip_sp_def] ASSGN_STATUS_INTACT, w2n_11] THEN 269 METIS_TAC [ASSGN_CORRESPOND, ADD_SYM] 270 ] 271 ); 272 273val STATUS_INTACT_TRANS = Q.store_thm ( 274 "STATUS_INTACT_TRANS", 275 `!a b c. status_intact a b /\ status_intact b c ==> status_intact a c`, 276 RW_TAC list_ss [status_intact_def, same_fp_ip_sp_def] 277 ); 278 279val BLK_STATUS_INTACT = Q.store_thm ( 280 "BLK_STATUS_INTACT", 281 `!stmL st. let st' = run_cfl (translate_hsl (Blk stmL)) st in 282 status_intact st' st`, 283 284 Induct_on `stmL` THENL [ 285 RW_TAC list_ss [status_intact_def, same_fp_ip_sp_def, valid_struct_def, translate_hsl_def, CFL_SEMANTICS_BLK], 286 FULL_SIMP_TAC list_ss [LET_THM, valid_struct_def, translate_hsl_def, CFL_SEMANTICS_BLK] THEN 287 METIS_TAC [ASSGN_STATUS_INTACT, STATUS_INTACT_TRANS] 288 ] 289 ); 290 291(*---------------------------------------------------------------------------------*) 292(* Well formedness of HSL programs *) 293(*---------------------------------------------------------------------------------*) 294 295val Well_Formed_def = Define ` 296 Well_Formed S_hsl = 297 WELL_FORMED (translate_hsl S_hsl) 298 `; 299 300val Well_Formed_Blk = Q.store_thm ( 301 "Well_Formed_Blk", 302 `!stmL. Well_Formed (Blk stmL)`, 303 RW_TAC std_ss [Well_Formed_def, translate_hsl_def, WELL_FORMED_thm] 304 ); 305 306val Well_Formed_Sc = Q.store_thm ( 307 "Well_Formed_Sc", 308 `!S1 S2. Well_Formed (Sc S1 S2) = Well_Formed S1 /\ Well_Formed S2`, 309 RW_TAC std_ss [Well_Formed_def, translate_hsl_def, CFL_SC_IS_WELL_FORMED] 310 ); 311 312(*---------------------------------------------------------------------------------*) 313(* Semantics of a HSL program is preserved when it is translated to CFL *) 314(*---------------------------------------------------------------------------------*) 315 316val sem_spec_def = Define ` 317 sem_spec P S_hsl Q = 318 !s st m. P st /\ correspond s st m ==> 319 let st' = run_cfl (translate_hsl S_hsl) st in 320 correspond (run_hsl S_hsl s) st' m /\ Q st'`; 321 322(*---------------------------------------------------------------------------------*) 323(* Correspondence of Sc structures *) 324(*---------------------------------------------------------------------------------*) 325 326val SC_SEM_SPEC = Q.store_thm ( 327 "SC_SEM_SPEC", 328 `!S1 S2 m P Q R. 329 Well_Formed (Sc S1 S2) ==> 330 sem_spec P S1 Q /\ sem_spec Q S2 R ==> 331 sem_spec P (Sc S1 S2) R`, 332 333 RW_TAC std_ss [Well_Formed_def, WELL_FORMED_def, sem_spec_def, translate_hsl_def, LET_THM, 334 run_hsl_def, SEMANTICS_OF_CFL] THEN 335 METIS_TAC [] 336 ); 337 338(* 339val SC_STATUS_INTACT = Q.store_thm ( 340 "SC_STATUS_INTACT", 341 `!S1 S2 P Q. 342 Well_Formed (Sc S1 S2) ==> 343 (!st. P st ==> let st' = run_cfl (translate_hsl S1) st in 344 status_intact st' st /\ Q st') /\ 345 (!st. Q st ==> let st' = run_cfl (translate_hsl S2) st in 346 status_intact st' st) ==> 347 (!st. P st ==> let st' = run_cfl (translate_hsl (Sc S1 S2)) st in 348 status_intact st' st)`, 349 RW_TAC std_ss [Well_Formed_def, same_base_regs_def, run_hsl_def, translate_hsl_def, SEMANTICS_OF_CFL] THEN 350 METIS_TAC [] 351 ); 352*) 353 354(*---------------------------------------------------------------------------------*) 355(* Correspondence of Cj structures *) 356(*---------------------------------------------------------------------------------*) 357 358val conv_reg_lem_1 = Q.store_thm ( 359 "conv_reg_lem_1", 360 `!r. (toREG (conv_reg r) = REG (data_reg_index r))`, 361 Cases_on `r` THEN 362 RW_TAC std_ss [data_reg_index_def, conv_reg_thm, toREG_def, index_of_reg_def] 363 ); 364 365val EVAL_TCND_THM = Q.store_thm ( 366 "EVAL_TCND_THM", 367 `!cond s st m. correspond s st m ==> 368 (eval_TCND cond s = eval_il_cond (translate_TCND cond) st)`, 369 370 SIMP_TAC std_ss [FORALL_TSTATE, FORALL_DSTATE] THEN 371 RW_TAC std_ss [correspond_def] THEN 372 Cases_on `cond` THEN Cases_on `r` THEN 373 Cases_on `q'` THEN Cases_on `r'` THEN 374 RW_TAC std_ss [eval_TCND_def, translate_TCND_def, eval_il_cond_def, tread_def, translate_condition_def, 375 ARMCompositionTheory.eval_cond_def, roc_2_exp_def, conv_roc_def, toEXP_def, conv_reg_lem_1, read_thm] 376 ); 377 378val CJ_SEM_SPEC = Q.store_thm ( 379 "CJ_SEM_SPEC", 380 `!cond S1 S2. 381 Well_Formed (Cj cond S1 S2) ==> 382 sem_spec P S1 Q /\ sem_spec P S2 Q ==> 383 sem_spec P (Cj cond S1 S2) Q`, 384 385 RW_TAC std_ss [Well_Formed_def, WELL_FORMED_def, sem_spec_def, translate_hsl_def, LET_THM, 386 run_hsl_def, SEMANTICS_OF_CFL] THEN 387 METIS_TAC [EVAL_TCND_THM] 388 ); 389 390(*---------------------------------------------------------------------------------*) 391(* Correspondence of Tr structures *) 392(*---------------------------------------------------------------------------------*) 393 394(* 395val WF_TR_HSL_CFL = Q.store_thm ( 396 "WF_TR_HSL_CFL", 397 `!cond S_hsl. WF (\s1 s0. ~eval_TCND cond s0 /\ (s1 = run_hsl S_hsl s0)) /\ 398 WELL_FORMED (translate_hsl S_hsl) ==> 399 WF_TR (translate_condition (translate_TCND cond), translate (translate_hsl S_hsl))`, 400 RW_TAC std_ss [] THEN 401 MATCH_MP_TAC CFL_RulesTheory.WF_TR_LEM_1 THEN 402 MATCH_MP_TAC relationTheory.WF_SUBSET THEN 403 Q.EXISTS_TAC `\s1 s0. ~eval_TCND cond s0 /\ (s1 = run_hsl S_hsl s0)` THEN 404 RW_TAC std_ss [EVAL_TCND_THM] THEN 405 406 ); 407*) 408 409val WF_LOOP_LEM_1 = Q.store_thm ( 410 "WF_LOOP_LEM_1", 411 `!cond S_cfl. WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl S_cfl st0)) ==> 412 WF_Loop (eval_il_cond cond, run_cfl S_cfl)`, 413 RW_TAC std_ss [ARMCompositionTheory.WF_Loop_def] THEN 414 Q.EXISTS_TAC `\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl S_cfl st0)` THEN 415 RW_TAC std_ss [] 416 ); 417 418val UNROLL_WHILE_CFL = Q.store_thm ( 419 "UNROLL_WHILE_CFL", 420 `!cond S_cfl st. WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl S_cfl st0)) ==> 421 (WHILE (\st'. ~eval_il_cond cond st') (run_cfl S_cfl) st = 422 FUNPOW (run_cfl S_cfl) (shortest (\st'. eval_il_cond cond st') (run_cfl S_cfl) st) st)`, 423 RW_TAC std_ss [] THEN 424 IMP_RES_TAC WF_LOOP_LEM_1 THEN 425 METIS_TAC [ARMCompositionTheory.UNROLL_LOOP] 426 ); 427 428val TR_SEM_SPEC = Q.store_thm ( 429 "TR_SEM_SPEC", 430 `!S_hsl cond. Well_Formed S_hsl /\ 431 WF (\st1 st0. ~eval_il_cond (translate_TCND cond) st0 /\ (st1 = run_cfl (translate_hsl S_hsl) st0)) /\ 432 sem_spec P S_hsl P ==> 433 sem_spec P (Tr cond S_hsl) P`, 434 435 SIMP_TAC std_ss [Well_Formed_def, sem_spec_def, translate_hsl_def, LET_THM, run_hsl_def] THEN 436 REPEAT GEN_TAC THEN STRIP_TAC THEN 437 Q.ABBREV_TAC `cnd1 = translate_TCND cond` THEN 438 Q.ABBREV_TAC `S1 = translate_hsl S_hsl` THEN 439 `WF_TR (translate_condition cnd1, translate S1)` by METIS_TAC [CFL_RulesTheory.WF_TR_LEM_1] THEN 440 FULL_SIMP_TAC std_ss [CFL_SEMANTICS_TR, UNROLL_WHILE_CFL] THEN 441 IMP_RES_TAC WF_LOOP_LEM_1 THEN 442 IMP_RES_TAC ARMCompositionTheory.WF_LOOP_IMP_STOPAT THEN 443 Induct_on `shortest (\st'. eval_il_cond cnd1 st') (run_cfl S1) st` THENL [ 444 REWRITE_TAC [Once EQ_SYM_EQ] THEN 445 REPEAT GEN_TAC THEN NTAC 12 STRIP_TAC THEN 446 `eval_il_cond cnd1 st /\ eval_TCND cond s` by METIS_TAC [SHORTEST_LEM, EVAL_TCND_THM] THEN 447 FULL_SIMP_TAC arith_ss [Once WHILE, FUNPOW], 448 449 REWRITE_TAC [Once EQ_SYM_EQ] THEN 450 REPEAT GEN_TAC THEN NTAC 12 STRIP_TAC THEN 451 Q.PAT_ASSUM `!cnd1 S1 st. a ==> b ==> c ==> d` (ASSUME_TAC o Q.SPECL [`cnd1`,`S1`,`run_cfl S1 st`]) THEN 452 `(\st'. eval_il_cond cnd1 st') = eval_il_cond cnd1` by METIS_TAC [] THEN 453 FULL_SIMP_TAC std_ss [] THEN 454 POP_ASSUM (K ALL_TAC) THEN 455 `stopAt (eval_il_cond cnd1) (run_cfl S1) st` by METIS_TAC [] THEN 456 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 457 Q.ABBREV_TAC `k = shortest (eval_il_cond cnd1) (run_cfl S1) (run_cfl S1 st)` THEN 458 RES_TAC THEN RES_TAC THEN 459 `~eval_TCND cond s` by METIS_TAC [EVAL_TCND_THM] THEN 460 RW_TAC std_ss [Once WHILE, FUNPOW] 461 ] 462 ); 463 464(*---------------------------------------------------------------------------------*) 465(* Correspondence of Fc structures *) 466(*---------------------------------------------------------------------------------*) 467 468val proper_frames_def = Define ` 469 proper_frames st (m1,m2) (n1,n2) = 470 (w2n (read st SP) = w2n (read st FP) - (12 + m1)) /\ 471 locate_ge (read st SP) (MAX n1 n2 + 13 + m2)`; 472 473val MAP_LEM_4 = Q.store_thm ( 474 "MAP_LEM_4", 475 `!l1 l2 f g. (MAP f l1 = MAP g l2) ==> 476 (!i. (i < LENGTH l1) ==> (f (EL i l1) = g (EL i l2)))`, 477 Induct_on `l1` THEN Induct_on `l2` THEN 478 RW_TAC list_ss [] THEN 479 Induct_on `i` THEN 480 RW_TAC list_ss [] 481 ); 482 483(* 484val PRE_CALL_SAME_CONTENT = Q.store_thm ( 485 "PRE_CALL_SAME_CONTENT", 486 `!st m1 m2 caller_i callee_i caller_o callee_o. 487 VALID_FC_1 (caller_i,callee_i,callee_o,caller_o) (m1,m2) /\ 488 locate_ge (read st SP) (MAX (LENGTH caller_i) (LENGTH caller_o) + 13 + m2) /\ 489 (w2n (read st SP) = w2n (read st FP) - (12 + m1)) /\ 490 (MAX (LENGTH caller_i) (LENGTH caller_o) - (LENGTH caller_i) = k) /\ 491 same_content s st m1 ==> 492 same_content (transfer (empty_s,s) (callee_i,caller_i)) 493 (run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st) m2`, 494 495 REPEAT STRIP_TAC THEN 496 `standard_frame st m1 /\ locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2)` by 497 FULL_SIMP_TAC arith_ss [standard_frame_def, locate_ge_def, MAX_DEF] THEN 498 FULL_SIMP_TAC std_ss [same_content_thm] THEN 499 REPEAT STRIP_TAC THEN 500 FULL_SIMP_TAC std_ss [VALID_FC_1_def] THEN 501 Cases_on `MEM x callee_i` THENL [ 502 IMP_RES_TAC MEM_EL THEN 503 `run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i,MAP conv_exp callee_i) (MAX (LENGTH caller_i) 504 (LENGTH caller_o) - LENGTH caller_i) m2)) st '' conv_exp (EL n callee_i) = st '' conv_exp (EL n caller_i)` 505 by METIS_TAC [SIMP_RULE std_ss [rich_listTheory.EL_MAP] PRE_CALL_PASS_ARGUMENTS_THM_2] THEN 506 `MAP (tread (transfer (empty_s,s) (callee_i,caller_i))) callee_i = MAP (tread s) caller_i` 507 by METIS_TAC [TRANSFER_THM] THEN 508 FULL_SIMP_TAC std_ss [EVERY_EL] THEN 509 IMP_RES_TAC MAP_LEM_4 THEN 510 RW_TAC std_ss [] THEN METIS_TAC [], 511 512 FULL_SIMP_TAC std_ss [valid_arg_list_def, run_hsl_def, LET_THM] THEN 513 METIS_TAC [TRANSFER_INTACT] 514 ] 515 516*) 517 518(* 519val FC_SEM_SPEC = Q.store_thm ( 520 "FC_SEM_SPEC", 521 `!S_hsl cond. Well_Formed S_hsl /\ 522 VALID_FC_1 (caller_i,callee_i,callee_o,caller_o) (m1,m2) 523 ==> 524 sem_spec P S_hsl Q ==> 525 sem_spec (\st. P st /\ proper_frames st (m1,m2) (n1,n2) /\ 526 status_intact (run_cfl S_body st') st') 527 (Fc (caller_i, callee_i) S_hsl (caller_o, callee_o) (m1,m2)) Q`, 528 529 SIMP_TAC std_ss [Well_Formed_def, sem_spec_def, translate_hsl_def, LET_THM, run_hsl_def] THEN 530 REPEAT GEN_TAC THEN STRIP_TAC THEN 531 Q.ABBREV_TAC `cnd1 = translate_TCND cond` THEN 532 Q.ABBREV_TAC `S1 = translate_hsl S_hsl` THEN 533 `WF_TR (translate_condition cnd1, translate S1)` by METIS_TAC [CFL_RulesTheory.WF_TR_LEM_1] THEN 534 FULL_SIMP_TAC std_ss [CFL_SEMANTICS_TR, UNROLL_WHILE_CFL] THEN 535 IMP_RES_TAC WF_LOOP_LEM_1 THEN 536 IMP_RES_TAC WF_LOOP_IMP_STOPAT THEN 537 Induct_on `shortest (\st'. eval_il_cond cnd1 st') (run_cfl S1) st` THENL [ 538 REWRITE_TAC [Once EQ_SYM_EQ] THEN 539 REPEAT GEN_TAC THEN NTAC 12 STRIP_TAC THEN 540 `eval_il_cond cnd1 st /\ eval_TCND cond s` by METIS_TAC [SHORTEST_LEM, EVAL_TCND_THM] THEN 541 FULL_SIMP_TAC arith_ss [Once WHILE, FUNPOW], 542 543 REWRITE_TAC [Once EQ_SYM_EQ] THEN 544 REPEAT GEN_TAC THEN NTAC 12 STRIP_TAC THEN 545 Q.PAT_ASSUM `!cnd1 S1 st. a ==> b ==> c ==> d` (ASSUME_TAC o Q.SPECL [`cnd1`,`S1`,`run_cfl S1 st`]) THEN 546 `(\st'. eval_il_cond cnd1 st') = eval_il_cond cnd1` by METIS_TAC [] THEN 547 FULL_SIMP_TAC std_ss [] THEN 548 POP_ASSUM (K ALL_TAC) THEN 549 `stopAt (eval_il_cond cnd1) (run_cfl S1) st` by METIS_TAC [] THEN 550 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 551 Q.ABBREV_TAC `k = shortest (eval_il_cond cnd1) (run_cfl S1) (run_cfl S1 st)` THEN 552 RES_TAC THEN RES_TAC THEN 553 `~eval_TCND cond s` by METIS_TAC [EVAL_TCND_THM] THEN 554 RW_TAC std_ss [Once WHILE, FUNPOW] 555 ] 556 ); 557*) 558 559(*---------------------------------------------------------------------------------*) 560 561val _ = export_theory(); 562