1(* interactive use: 2 3quietdec := true; 4loadPath := (concat Globals.HOLDIR "/examples/dev/sw") :: !loadPath; 5 6app load ["pred_setSimps","pred_setTheory","whileTheory","finite_mapTheory","rich_listTheory","prim_recTheory", "wordsTheory", "wordsLib", "preARMTheory"]; 7 8quietdec := false; 9*) 10 11open HolKernel Parse boolLib bossLib numLib pred_setSimps pred_setTheory wordsLib 12 arithmeticTheory wordsTheory pairTheory listTheory whileTheory finite_mapTheory preARMTheory; 13 14val _ = new_theory "ARMComposition"; 15 16val _ = Globals.priming := NONE; 17 18(*------------------------------------------------------------------------------------------------------*) 19(* Additional theorems for finite maps *) 20(*------------------------------------------------------------------------------------------------------*) 21 22(* Sort in ascending order *) 23val FUPDATE_LT_COMMUTES = Q.store_thm ( 24 "FUPDATE_LT_COMMUTES", 25 ` !f a b c d. c < a ==> (f |+ (a:num, b) |+ (c,d) = f |+ (c,d) |+ (a,b))`, 26 RW_TAC arith_ss [FUPDATE_COMMUTES] 27 ); 28 29(* Sort in descending order *) 30val FUPDATE_GT_COMMUTES = Q.store_thm ( 31 "FUPDATE_GT_COMMUTES", 32 ` !f a b c d. c > a ==> (f |+ (a:ADDR,b) |+ (c,d) = f |+ (c,d) |+ (a,b))`, 33 RW_TAC arith_ss [FUPDATE_COMMUTES] 34 ); 35 36 37val fupdate_normalizer = 38 let val thm = SPEC_ALL FUPDATE_LT_COMMUTES 39 val pat = lhs(snd(dest_imp(concl thm))) 40 in 41 {name = "Finite map normalization", 42 trace = 2, 43 key = SOME([],pat), 44 conv = let fun reducer tm = 45 let val (theta,ty_theta) = match_term pat tm 46 val thm' = INST theta (INST_TYPE ty_theta thm) 47 val constraint = fst(dest_imp(concl thm')) 48 val cthm = EQT_ELIM(reduceLib.REDUCE_CONV constraint) 49 in MP thm' cthm 50 end 51 in 52 K (K reducer) 53 end} 54 end; 55 56val finmap_conv_frag = 57 simpLib.SSFRAG 58 {convs = [fupdate_normalizer], 59 rewrs = [], ac=[],filter=NONE,dprocs=[],congs=[]}; 60 61val finmap_ss = bossLib.std_ss ++ finmap_conv_frag 62 ++ rewrites [FUPDATE_EQ, FAPPLY_FUPDATE_THM]; 63 64val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss; 65 66(*---------------------------------------------------------------------------------*) 67(* termination *) 68(*---------------------------------------------------------------------------------*) 69 70val terminated = Define ` 71 terminated arm = 72 !(s:STATEPCS) iB. 73 stopAt (\s':STATEPCS. FST (FST s') = FST (FST s) + LENGTH arm) (step (upload arm iB (FST (FST s)))) s`; 74 75val TERMINATED_THM = Q.store_thm ( 76 "TERMINATED_THM", 77 `!arm. terminated arm ==> 78 !s iB. FST (FST (runTo (upload arm iB (FST (FST s))) (FST (FST s) + LENGTH arm) s)) = FST (FST s) + LENGTH arm`, 79 RW_TAC std_ss [terminated, UNROLL_RUNTO] THEN 80 METIS_TAC [Q.SPECL [`s:STATEPCS`, `\s':STATEPCS. FST (FST s') = FST (FST (s:STATEPCS)) + LENGTH arm`, 81 `step (upload arm iB (FST (FST (s:STATEPCS))))`] (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_STOP)] 82 ); 83 84(*---------------------------------------------------------------------------------*) 85(* Closed segment of codes *) 86(*---------------------------------------------------------------------------------*) 87 88val closed = Define ` 89 closed arm = 90 !s iB. (!x. x IN SND (runTo (upload arm iB (FST s)) (FST s + LENGTH arm) (s,({}))) ==> FST s <= x /\ x < FST s + LENGTH arm)`; 91 92val CLOSED_THM = Q.store_thm ( 93 "CLOSED_THM", 94 `!m arm s iB pos. closed arm ==> 95 stopAt (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step (upload arm iB (FST (FST s)))) s /\ 96 m < shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step (upload arm iB (FST (FST s)))) s 97 ==> 98 FST (FST s) <= FST (FST (FUNPOW (step (upload arm iB (FST (FST s)))) m s)) /\ 99 FST (FST (FUNPOW (step (upload arm iB (FST (FST s)))) m s)) < FST (FST s) + LENGTH arm 100 `, 101 REPEAT GEN_TAC THEN 102 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 103 ASM_REWRITE_TAC [] THEN 104 REWRITE_TAC [closed] THEN 105 NTAC 2 STRIP_TAC THEN 106 Q.PAT_ASSUM `!s iB x.p` (MP_TAC o Q.SPECL [`s0`, `iB`, `FST (FST (FUNPOW (step (upload arm iB (FST s0))) m (s0,pcS0)))`]) THEN 107 IMP_RES_TAC (Q.SPECL [`pcS0`, `{}`] STOPAT_ANY_PCS_2) THEN 108 IMP_RES_TAC UNROLL_RUNTO THEN 109 ASM_REWRITE_TAC [] THEN 110 NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 111 IMP_RES_TAC RUNTO_PCS_MEMBERS_2 THEN 112 `shortest (\s'. FST (FST s') = FST s0 + LENGTH arm) (step (upload arm iB (FST s0))) (s0,pcS0) = 113 shortest (\s'. FST (FST s') = FST s0 + LENGTH arm) (step (upload arm iB (FST s0))) (s0,{})` 114 by METIS_TAC [SIMP_RULE std_ss [] (Q.SPECL [`(s0,pcS0)`,`(s0,({}))`] SHORTEST_INDEPENDENT_OF_PCS)] THEN 115 STRIP_TAC THEN 116 METIS_TAC [] 117 ); 118 119 120(*---------------------------------------------------------------------------------*) 121(* Running of closed codes *) 122(*---------------------------------------------------------------------------------*) 123 124val CLOSED_MIDDLE_STEP_LEM = Q.store_thm ( 125 "CLOSED_MIDDLE_STEP_LEM", 126 `!arm arm' arm'' pos iB pos (s:STATEPCS). 127 (pos + LENGTH arm' <= FST (FST s)) /\ (FST (FST s) < pos + LENGTH arm' + LENGTH arm) ==> 128 (step (upload (arm' ++ arm ++ arm'') iB pos) s = step (upload arm iB (pos + LENGTH arm')) s)`, 129 RW_TAC std_ss [] THEN 130 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 131 FULL_SIMP_TAC std_ss [step_def] THEN 132 `?k. k < LENGTH arm /\ (FST s0 = pos + LENGTH arm' + k)` by (Q.EXISTS_TAC `FST s0 - pos - LENGTH arm'` THEN RW_TAC arith_ss []) THEN 133 RW_TAC std_ss [] THEN 134 `LENGTH arm' + k < LENGTH (arm' ++ arm ++ arm'')` by RW_TAC list_ss [] THEN 135 IMP_RES_TAC UPLOAD_LEM THEN 136 `EL (k + LENGTH arm') (arm' ++ arm ++ arm'') = EL k arm` by ALL_TAC THENL [ 137 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 138 Induct_on `arm'` THENL [ 139 RW_TAC list_ss [rich_listTheory.EL_APPEND1], 140 RW_TAC list_ss [] THEN 141 `k + SUC (LENGTH arm') = SUC (k + LENGTH arm')` by RW_TAC arith_ss [] THEN 142 RW_TAC list_ss [rich_listTheory.EL_APPEND1, APPEND_ASSOC] THEN 143 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 144 Induct_on `arm'` THENL [ 145 RW_TAC list_ss [], 146 `k + SUC (LENGTH arm') = SUC (k + LENGTH arm')` by RW_TAC arith_ss [] THEN 147 RW_TAC list_ss [rich_listTheory.EL_APPEND1] 148 ] 149 ], 150 RW_TAC std_ss [] THEN 151 METIS_TAC [ADD_ASSOC, ADD_SYM] 152 ] 153 ); 154 155 156val CLOSED_MIDDLE_LEM = Q.store_thm ( 157 "CLOSED_MIDDLE_LEM", 158 `!arm arm' arm'' pos iB (s:STATEPCS) s'. 159 closed arm /\ terminated arm /\ (pos + LENGTH arm' = FST (FST s)) /\ (instB = upload arm iB (FST (FST s))) /\ 160 (?m. (s' = FUNPOW (step instB) m (s)) /\ m <= shortest (\s1:STATEPCS. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s) 161 ==> 162 (runTo (upload (arm' ++ arm ++ arm'') iB pos) (FST (FST s) + LENGTH arm) s' = 163 runTo (upload arm iB (FST (FST s))) (FST (FST s) + LENGTH arm) s')`, 164 165 RW_TAC std_ss [] THEN 166 Q.ABBREV_TAC `instB = upload arm iB (FST (FST s))` THEN 167 Cases_on `m = shortest (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` THENL [ 168 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [STOPAT_THM, terminated] THEN 169 `FST (FST (FUNPOW (step instB) m s)) = FST (FST s) + LENGTH arm` by ( FULL_SIMP_TAC std_ss [stopAt_def, shortest_def] THEN 170 METIS_TAC [Q.SPEC `\n.FST (FST (FUNPOW (step instB) n s)) = FST (FST s) + LENGTH arm` LEAST_INTRO]) THEN 171 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE] THEN 172 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE], 173 174 `m < shortest (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 175 Q.PAT_ASSUM `~p` (K ALL_TAC) THEN 176 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) (FUNPOW (step instB) m s)` by METIS_TAC [STOPAT_THM, terminated] THEN 177 RW_TAC std_ss [UNROLL_RUNTO] THEN 178 Induct_on `shortest (\s1:STATEPCS. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) (FUNPOW (step instB) m s)` THENL [ 179 REWRITE_TAC [Once EQ_SYM_EQ] THEN 180 RW_TAC list_ss [FUNPOW] THEN 181 Q.ABBREV_TAC `s' = FUNPOW (step instB) m s` THEN 182 `FST (FST s') = FST (FST s) + LENGTH arm` by METIS_TAC [Q.SPECL [`s'`, `\s1. FST (FST s1) = FST (FST s) + LENGTH arm`] 183 (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_LEM)] THEN 184 `?s0 pcS0. s' = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 185 METIS_TAC [RUNTO_ADVANCE, FST, SND], 186 187 REWRITE_TAC [Once EQ_SYM_EQ] THEN 188 RW_TAC list_ss [FUNPOW] THEN 189 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 190 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [terminated] THEN 191 `SUC m <= shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 192 `v + SUC m = shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [FUNPOW_SUC, ADD_SYM, 193 (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_THM)] THEN 194 `step (upload (arm' ++ arm ++ arm'') iB pos) (FUNPOW (step instB) m s) = 195 step instB (FUNPOW (step instB) m s)` by (Q.UNABBREV_TAC `instB` THEN 196 METIS_TAC [CLOSED_THM, CLOSED_MIDDLE_STEP_LEM]) THEN 197 198 Cases_on `v` THENL [ 199 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE, FUNPOW] THENL [ 200 METIS_TAC [], 201 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE, FUNPOW] THEN 202 Q.ABBREV_TAC `s' = step instB (FUNPOW (step instB) m s)` THEN 203 `(FST (FST s') = FST (FST s) + LENGTH arm)` by METIS_TAC [Q.SPECL [`s'`, `\s1. FST (FST s1) = 204 FST (FST s) + LENGTH arm`] (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_LEM)] 205 ], 206 207 Q.PAT_ASSUM `!s.p` (ASSUME_TAC o SIMP_RULE std_ss [FUNPOW_SUC] o Q.SPECL [`s`,`arm`,`instB`,`SUC m`]) THEN 208 `SUC m < shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 209 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE] THEN 210 METIS_TAC [] 211 ] 212 ] 213 ] 214 ); 215 216 217val CLOSED_MIDDLE = Q.store_thm ( 218 "CLOSED_MIDDLE", 219 `!arm arm' arm'' pos iB (s:STATEPCS). 220 closed arm /\ terminated arm /\ (pos + LENGTH arm' = FST (FST s)) ==> 221 (runTo (upload (arm' ++ arm ++ arm'') iB pos) (FST (FST s) + LENGTH arm) s = 222 runTo (upload arm iB (FST (FST s))) (FST (FST s) + LENGTH arm) s)`, 223 REPEAT STRIP_TAC THEN 224 `(?m. (FUNPOW (step (upload arm iB (FST (FST s)))) 0 s = FUNPOW (step (upload arm iB (FST (FST s)))) m s) /\ 225 m <= shortest (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step (upload arm iB (FST (FST s)))) s) ==> 226 (runTo (upload (arm' ++ arm ++ arm'') iB pos) (FST (FST s) + LENGTH arm) (FUNPOW (step (upload arm iB (FST (FST s)))) 0 s) = 227 runTo (upload arm iB (FST (FST s))) (FST (FST s) + LENGTH arm) (FUNPOW (step (upload arm iB (FST (FST s)))) 0 s))` 228 by METIS_TAC [(SIMP_RULE std_ss [] o Q.SPECL [`arm`,`arm'`,`arm''`,`pos`,`iB`,`s`,`FUNPOW (step instB) 0 s`] o 229 SIMP_RULE std_ss []) CLOSED_MIDDLE_LEM] THEN 230 `0 <= shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step (upload arm iB (FST (FST s)))) s` by RW_TAC arith_ss [] THEN 231 RES_TAC THEN 232 METIS_TAC [FUNPOW] 233 ); 234 235 236val CLOSED_PREFIX = Q.store_thm ( 237 "CLOSED_PREFIX", 238 `!arm arm' pos iB (s:STATEPCS). 239 closed arm /\ terminated arm /\ (pos + LENGTH arm' = FST (FST s)) ==> 240 (runTo (upload (arm' ++ arm) iB pos) (FST (FST s) + LENGTH arm) s = 241 runTo (upload arm iB (FST (FST s))) (FST (FST s) + LENGTH arm) s)`, 242 REPEAT STRIP_TAC THEN 243 IMP_RES_TAC (Q.SPECL [`arm`,`arm'`,`[]`] CLOSED_MIDDLE) THEN 244 FULL_SIMP_TAC list_ss [] 245 ); 246 247 248val CLOSED_SUFFIX = Q.store_thm ( 249 "CLOSED_SUFFIX", 250 `!arm arm' iB instB (s:STATEPCS). 251 closed arm /\ terminated arm ==> 252 (runTo (upload (arm ++ arm') iB (FST (FST s))) (FST (FST s) + LENGTH arm) s = 253 runTo (upload arm iB (FST (FST s))) (FST (FST s) + LENGTH arm) s)`, 254 REPEAT STRIP_TAC THEN 255 IMP_RES_TAC (Q.SPECL [`arm`,`[]`,`arm'`] CLOSED_MIDDLE) THEN 256 FULL_SIMP_TAC list_ss [] 257 ); 258 259(*---------------------------------------------------------------------------------*) 260(* Terimination information of closed codes *) 261(*---------------------------------------------------------------------------------*) 262 263val TERMINATED_MIDDLE_LEM = Q.store_thm ( 264 "TERMINATED_MIDDLE_LEM", 265 `!arm arm' arm'' pos iB (s:STATEPCS) s'. 266 closed arm /\ terminated arm /\ (pos + LENGTH arm' = FST (FST s)) /\ (instB = upload arm iB (FST (FST s))) /\ 267 (?m. (s' = FUNPOW (step instB) m (s)) /\ m <= shortest (\s1:STATEPCS. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s) 268 ==> 269 terd (upload (arm' ++ arm ++ arm'') iB pos) (FST (FST s) + LENGTH arm) s'`, 270 271 RW_TAC std_ss [terd_def] THEN 272 Q.ABBREV_TAC `instB = upload arm iB (FST (FST s))` THEN 273 Cases_on `m = shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` THENL [ 274 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [STOPAT_THM, terminated] THEN 275 `FST (FST (FUNPOW (step instB) m s)) = FST (FST s) + LENGTH arm` by ( FULL_SIMP_TAC std_ss [stopAt_def, shortest_def] THEN 276 METIS_TAC [Q.SPEC `\n.FST (FST (FUNPOW (step instB) n s)) = FST (FST s) + LENGTH arm` LEAST_INTRO]) THEN 277 RW_TAC std_ss [stopAt_def] THEN 278 Q.EXISTS_TAC `0` THEN 279 RW_TAC std_ss [FUNPOW], 280 281 `m < shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 282 Q.PAT_ASSUM `~p` (K ALL_TAC) THEN 283 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) (FUNPOW (step instB) m s)` by METIS_TAC [STOPAT_THM, terminated] THEN 284 Induct_on `shortest (\s1:STATEPCS. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) (FUNPOW (step instB) m s)` THENL [ 285 REWRITE_TAC [Once EQ_SYM_EQ] THEN 286 RW_TAC list_ss [FUNPOW] THEN 287 Q.ABBREV_TAC `s' = FUNPOW (step instB) m s` THEN 288 `FST (FST s') = FST (FST s) + LENGTH arm` by METIS_TAC [Q.SPECL [`s'`, `\s1. FST (FST s1) = FST (FST s) + LENGTH arm`] 289 (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_LEM)] THEN 290 RW_TAC std_ss [stopAt_def] THEN 291 Q.EXISTS_TAC `0` THEN 292 RW_TAC std_ss [FUNPOW], 293 294 REWRITE_TAC [Once EQ_SYM_EQ] THEN 295 RW_TAC list_ss [FUNPOW] THEN 296 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 297 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [terminated] THEN 298 `SUC m <= shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 299 `v + SUC m = shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [FUNPOW_SUC, ADD_SYM, 300 (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_THM)] THEN 301 `step (upload (arm' ++ arm ++ arm'') iB pos) (FUNPOW (step instB) m s) = 302 step instB (FUNPOW (step instB) m s)` by (Q.UNABBREV_TAC `instB` THEN 303 METIS_TAC [CLOSED_THM, CLOSED_MIDDLE_STEP_LEM]) THEN 304 Cases_on `v` THENL [ 305 RW_TAC std_ss [stopAt_def] THEN 306 Q.ABBREV_TAC `s' = step instB (FUNPOW (step instB) m s)` THEN 307 `(FST (FST s') = FST (FST s) + LENGTH arm)` by METIS_TAC [Q.SPECL [`s'`, `\s1. FST (FST s1) = 308 FST (FST s) + LENGTH arm`] (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_LEM)] THEN 309 Q.EXISTS_TAC `SUC 0` THEN 310 RW_TAC std_ss [FUNPOW], 311 312 Q.PAT_ASSUM `!s.p` (ASSUME_TAC o SIMP_RULE std_ss [FUNPOW_SUC] o Q.SPECL [`s`,`arm`,`instB`,`SUC m`]) THEN 313 `SUC m < shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 314 RES_TAC THEN 315 FULL_SIMP_TAC std_ss [stopAt_def] THEN 316 Q.EXISTS_TAC `SUC n''''` THEN 317 RW_TAC std_ss [FUNPOW] 318 ] 319 ] 320 ] 321 ); 322 323val TERMINATED_MIDDLE = Q.store_thm ( 324 "TERMINATED_MIDDLE", 325 `!arm arm' arm'' pos iB instB (s:STATEPCS). 326 closed arm /\ terminated arm /\ (pos + LENGTH arm' = FST (FST s)) ==> 327 terd (upload (arm' ++ arm ++ arm'') iB pos) (FST (FST s) + LENGTH arm) s`, 328 329 REPEAT STRIP_TAC THEN 330 `(?m. (FUNPOW (step (upload arm iB (FST (FST s)))) 0 s = FUNPOW (step (upload arm iB (FST (FST s)))) m s) /\ 331 m <= shortest (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step (upload arm iB (FST (FST s)))) s) ==> 332 terd (upload (arm' ++ arm ++ arm'') iB pos) (FST (FST s) + LENGTH arm) (FUNPOW (step (upload arm iB (FST (FST s)))) 0 s)` 333 by METIS_TAC [(SIMP_RULE std_ss [] o Q.SPECL [`arm`,`arm'`,`arm''`,`pos`,`iB`,`s`,`FUNPOW (step (upload arm iB (FST (FST s)))) 0 s`] o 334 SIMP_RULE std_ss []) TERMINATED_MIDDLE_LEM] THEN 335 `0 <= shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step (upload arm iB (FST (FST s)))) s` by RW_TAC arith_ss [] THEN 336 RES_TAC THEN 337 METIS_TAC [FUNPOW] 338 ); 339 340(*---------------------------------------------------------------------------------*) 341(* Sequential Composition witin a context *) 342(* arm' and arm'' represent the context *) 343(*---------------------------------------------------------------------------------*) 344 345val CLOSED_SEQUENTIAL_COMPOSITION = Q.store_thm ( 346 "CLOSED_SEQUENTIAL_COMPOSITION", 347 `!arm1 arm2 arm' arm'' pos iB (s:STATEPCS). 348 closed arm1 /\ terminated arm1 /\ closed arm2 /\ terminated arm2 /\ 349 (pos + LENGTH arm' = FST (FST s)) /\ ~(FST (FST s) + LENGTH arm1 + LENGTH arm2 IN SND s) ==> 350 stopAt (\s'. FST (FST s') = FST (FST s) + LENGTH arm1 + LENGTH arm2) (step (upload (arm' ++ arm1 ++ arm2 ++ arm'') iB pos)) s 351 /\ 352 (runTo (upload (arm' ++ arm1 ++ arm2 ++ arm'') iB pos) (FST (FST s) + LENGTH arm1 + LENGTH arm2) s = 353 runTo (upload arm2 iB (FST (FST s) + LENGTH arm1)) (FST (FST s) + LENGTH arm1 + LENGTH arm2) 354 (runTo (upload arm1 iB (FST (FST s))) (FST (FST s) + LENGTH arm1) s))`, 355 356 NTAC 8 STRIP_TAC THEN 357 Cases_on `LENGTH arm2 = 0` THENL [ 358 IMP_RES_TAC LENGTH_NIL THEN 359 FULL_SIMP_TAC list_ss [CLOSED_MIDDLE] THEN 360 Q.ABBREV_TAC `s' = runTo (upload arm1 iB (FST (FST s))) (FST (FST s) + LENGTH arm1) s` THEN 361 `FST (FST s') = FST (FST s) + LENGTH arm1` by (Q.UNABBREV_TAC `s'` THEN METIS_TAC [TERMINATED_THM]) THEN 362 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE] THEN 363 METIS_TAC [TERMINATED_MIDDLE, terd_def], 364 365 Q.ABBREV_TAC `insts2 = arm2 ++ arm''` THEN 366 `~(LENGTH insts2 = 0) /\ (arm' ++ arm1 ++ arm2 ++ arm'' = arm' ++ arm1 ++ insts2)` by 367 (Q.UNABBREV_TAC `insts2` THEN RW_TAC list_ss [] THEN METIS_TAC [APPEND_ASSOC]) THEN 368 ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN 369 `?s1 pcS1. (s1,pcS1) = runTo (upload (arm' ++ arm1 ++ insts2) iB pos) (FST (FST s) + LENGTH arm1) s` by METIS_TAC [ABS_PAIR_THM] THEN 370 `~(FST (FST s) + LENGTH arm1 + LENGTH arm2 IN (FST (FST s) INSERT pcS1))` by ALL_TAC THENL [ 371 POP_ASSUM MP_TAC THEN 372 RW_TAC std_ss [SIMP_RULE std_ss [] (Q.SPECL [`arm1`,`arm'`,`insts2`,`pos`,`iB`, `s:STATEPCS`] CLOSED_MIDDLE)] THEN 373 `pcS1 = SND (runTo (upload arm1 iB (FST (FST (s:STATEPCS)))) (FST (FST s) + LENGTH arm1) ((FST s,{}):STATEPCS)) UNION SND s` by METIS_TAC 374 [terminated, Q.SPEC `(FST (s:STATEPCS),SND s)` (INST_TYPE [alpha |-> Type`:STATEPCS`] RUNTO_PCS_UNION), SND, FST, ABS_PAIR_THM] THEN 375 `!x. x IN SND (runTo (upload arm1 iB (FST (FST s))) (FST (FST s) + LENGTH arm1) (FST s,{})) ==> 376 FST (FST s) <= x /\ x < FST (FST s) + LENGTH arm1` by METIS_TAC [closed,FST] THEN 377 Q.UNABBREV_TAC `insts2` THEN 378 FULL_SIMP_TAC set_ss [] THEN FULL_SIMP_TAC arith_ss [] THEN 379 STRIP_TAC THEN RES_TAC THEN 380 FULL_SIMP_TAC arith_ss [], 381 382 `terd (upload (arm' ++ arm1 ++ insts2) iB pos) (FST (FST s) + LENGTH arm1) (FST s,SND s) /\ 383 ((s1,pcS1) = runTo (upload (arm' ++ arm1 ++ insts2) iB pos) (FST (FST s) + LENGTH arm1) (FST s,SND s))` 384 by METIS_TAC [FST, SND, TERMINATED_MIDDLE, ABS_PAIR_THM] THEN 385 IMP_RES_TAC RUNTO_COMPOSITION THEN 386 FULL_SIMP_TAC std_ss [] THEN STRIP_TAC THENL [ 387 RW_TAC std_ss [stopAt_def] THEN 388 Q.ABBREV_TAC `instB = upload (arm' ++ arm1 ++ insts2) iB pos` THEN 389 Q.EXISTS_TAC `shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm1 + LENGTH arm2) (step instB) (s1,pcS1) + 390 shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm1) (step instB) s` THEN 391 RW_TAC std_ss [GSYM FUNPOW_FUNPOW] THEN 392 FULL_SIMP_TAC std_ss [terd_def, 393 REWRITE_RULE [Once EQ_SYM_EQ] (Q.SPECL [`instB`,`FST (FST (s:STATEPCS)) + LENGTH arm1`, `s:STATEPCS`] (GSYM UNROLL_RUNTO))] THEN 394 Q.UNABBREV_TAC `instB` THEN 395 `runTo (upload arm1 iB (FST (FST s))) (FST (FST s) + LENGTH arm1) s = (s1,pcS1)` by 396 METIS_TAC [terd_def, FST, CLOSED_PAIR_EQ,CLOSED_MIDDLE] THEN 397 Q.PAT_ASSUM `(s1,pcS1) = x` (ASSUME_TAC o GSYM) THEN 398 FULL_SIMP_TAC std_ss [] THEN 399 Q.UNABBREV_TAC `insts2` THEN 400 REWRITE_TAC [APPEND_ASSOC, ADD_ASSOC] THEN 401 `pos + LENGTH (arm' ++ arm1) = FST (FST (s1,pcS1))` by METIS_TAC [TERMINATED_THM, FST, LENGTH_APPEND, ADD_ASSOC] THEN 402 `terd (upload (arm' ++ arm1 ++ arm2 ++ arm'') iB pos) (FST (FST s) + LENGTH arm1 + LENGTH arm2) (s1,pcS1)` 403 by METIS_TAC [FST, SND, TERMINATED_MIDDLE, ABS_PAIR_THM, LENGTH_APPEND, ADD_ASSOC] THEN 404 FULL_SIMP_TAC list_ss [terd_def, REWRITE_RULE [Once EQ_SYM_EQ] (Q.SPECL [`upload (arm' ++ arm1 ++ arm2 ++ arm'') iB pos`, 405 `FST (FST (s:STATEPCS)) + LENGTH arm1 + LENGTH arm2`, `(s1,pcS1):STATEPCS`] (GSYM UNROLL_RUNTO))] THEN 406 FULL_SIMP_TAC std_ss [ADD_ASSOC] THEN 407 `runTo (upload (arm' ++ arm1 ++ arm2 ++ arm'') iB pos) (FST (FST s) + LENGTH arm1 + LENGTH arm2) (s1,pcS1) = 408 runTo (upload arm2 iB (FST s1)) (FST s1 + LENGTH arm2) (s1,pcS1)` by METIS_TAC [FST, 409 (REWRITE_RULE [ADD_ASSOC] o SIMP_RULE list_ss []) 410 (Q.SPECL [`arm2`,`arm' ++ arm1`,`arm''`, `pos`,`iB`,`(s1,pcS1):STATEPCS`] CLOSED_MIDDLE)] THEN 411 METIS_TAC [TERMINATED_THM], 412 413 POP_ASSUM (K ALL_TAC) THEN 414 POP_ASSUM (ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC [] THEN 415 `runTo (upload arm1 iB (FST (FST s))) (FST (FST s) + LENGTH arm1) s = (s1,pcS1)` by METIS_TAC [FST, CLOSED_PAIR_EQ,CLOSED_MIDDLE] THEN 416 FULL_SIMP_TAC std_ss [] THEN 417 Q.UNABBREV_TAC `insts2` THEN 418 REWRITE_TAC [APPEND_ASSOC, ADD_ASSOC] THEN 419 `pos + LENGTH (arm' ++ arm1) = FST (FST (s1,pcS1))` by METIS_TAC [TERMINATED_THM, FST, LENGTH_APPEND, ADD_ASSOC] THEN 420 METIS_TAC [CLOSED_MIDDLE, FST, ADD_ASSOC, LENGTH_APPEND] 421 ] 422 ] 423 ] 424 ); 425 426(*---------------------------------------------------------------------------------*) 427(* pc- and cpsr-independent codes *) 428(* The result data excluding the cpsr and pc is independent of pc and cpsr *) 429(* of the source state *) 430(*---------------------------------------------------------------------------------*) 431 432val get_st = Define ` 433 get_st (s:STATEPCS) = 434 SND (SND (FST s))`; 435 436val status_independent = Define ` 437 status_independent arm = 438 !st pos0 pos1 cpsr0 cpsr1 iB. 439 get_st (runTo (upload arm iB pos0) (pos0 + LENGTH arm) ((pos0,cpsr0,st),({}))) = 440 get_st (runTo (upload arm iB pos1) (pos1 + LENGTH arm) ((pos1,cpsr1,st),({})))`; 441 442val _ = type_abbrev("DSTATE", Type`:(REGISTER |-> DATA) # (ADDR |-> DATA)`); 443 444 445val DSTATE_IRRELEVANT_PCS = Q.store_thm 446 ("DSTATE_IRRELEVANT_PCS", 447 `!arm pcS0 pcS1 iB s. 448 terminated arm ==> 449 (get_st (runTo (upload arm iB (FST s)) (FST s + LENGTH arm) (s,pcS0)) = 450 get_st (runTo (upload arm iB (FST s)) (FST s + LENGTH arm) (s,pcS1)))`, 451 RW_TAC std_ss [terminated, get_st] THEN 452 Cases_on `LENGTH arm` THENL [ 453 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE] THEN 454 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE], 455 METIS_TAC [FST, RUNTO_STATE_PCS_SEPERATE] 456 ] 457 ); 458 459val DSTATE_COMPOSITION = Q.store_thm ( 460 "DSTATE_COMPOSITION", 461 `!arm arm' pos0 pos1 pos2 cpsr0 cpsr1 cpsr2 iB (st:DSTATE). 462 closed arm /\ terminated arm /\ status_independent arm /\ 463 closed arm' /\ terminated arm' /\ status_independent arm' 464 ==> 465 (get_st (runTo (upload (arm ++ arm') iB pos0) (pos0 + LENGTH arm + LENGTH arm') ((pos0,cpsr0,st),({}))) = 466 get_st (runTo (upload arm' iB pos2) (pos2 + LENGTH arm') 467 ((pos2,cpsr2, get_st (runTo (upload arm iB pos1) (pos1 + LENGTH arm) ((pos1,cpsr1,st),({})))), ({}))))`, 468 469 RW_TAC std_ss [get_st] THEN 470 RW_TAC std_ss [(SIMP_RULE set_ss [ADD_ASSOC] o SIMP_RULE list_ss [] o 471 Q.SPECL [`arm`,`arm'`,`[]`,`[]`,`pos0`,`iB`,`((pos0,cpsr0,st),{}):STATEPCS`]) CLOSED_SEQUENTIAL_COMPOSITION] THEN 472 `?pos' cpsr' pcS'. runTo (upload arm iB pos0) (pos0 + LENGTH arm) ((pos0,cpsr0,st),{}) = 473 ((pos',cpsr',SND(SND(FST (runTo (upload arm iB pos0) (pos0 + LENGTH arm) ((pos0,cpsr0,st),{}))))),pcS')` by METIS_TAC [ABS_PAIR_THM, FST,SND] THEN 474 `pos' = pos0 + LENGTH arm` by METIS_TAC [TERMINATED_THM, FST] THEN 475 ONCE_ASM_REWRITE_TAC [] THEN 476 Q.PAT_ASSUM `runTo x y z = k` (K ALL_TAC) THEN 477 ASM_REWRITE_TAC [] THEN 478 `SND (SND (FST (runTo (upload arm iB pos0) (pos0 + LENGTH arm) (((pos0,cpsr0,st),({})):STATEPCS)))) = 479 SND (SND (FST (runTo (upload arm iB pos1) (pos1 + LENGTH arm) (((pos1,cpsr1,st),({})):STATEPCS))))` by METIS_TAC [status_independent,get_st] THEN 480 METIS_TAC [status_independent, FST, get_st, DSTATE_IRRELEVANT_PCS, SND] 481 ); 482 483(* 484val BASIC_CLOSED_POSIND_COMPOSITION = 485 SIMP_RULE std_ss [Once SWAP_FORALL_THM] (GEN_ALL (SIMP_RULE arith_ss [reset_st] (Q.SPECL [`arm`,`arm'`,`0`,`0`,`0`] CLOSED_POSIND_COMPOSITION))); 486*) 487 488(*---------------------------------------------------------------------------------*) 489(* Well formed codes *) 490(*---------------------------------------------------------------------------------*) 491 492val well_formed = Define ` 493 well_formed arm = 494 closed arm /\ terminated arm /\ status_independent arm`; 495 496 497(*---------------------------------------------------------------------------------*) 498(* Evaluation of flag codes *) 499(*---------------------------------------------------------------------------------*) 500 501val eval_fl = Define ` 502 eval_fl arm st = 503 get_st (runTo (uploadCode arm (\i.ARB)) (LENGTH arm) ((0,0w,st),({})))`; 504 505 506val SEQ_COMPOSITION_FLAT = Q.store_thm ( 507 "SEQ_COMPOSITION_FLAT", 508 `!arm arm'. 509 well_formed arm /\ well_formed arm' 510 ==> 511 (eval_fl (arm ++ arm') = eval_fl arm' o eval_fl arm)`, 512 RW_TAC std_ss [uploadCode_def, eval_fl, well_formed, FUN_EQ_THM] THEN 513 RW_TAC list_ss [SIMP_RULE arith_ss [] (Q.SPECL [`arm`,`arm'`,`0`,`0`,`0`,`0w`,`0w`,`0w`,`(\i. ARB)`,`x`] DSTATE_COMPOSITION)] 514 ); 515 516(*---------------------------------------------------------------------------------*) 517(* flat coce composition *) 518(*---------------------------------------------------------------------------------*) 519 520val mk_SC = Define ` 521 mk_SC arm1 arm2 = 522 arm1 ++ arm2`; 523 524val mk_CJ = Define ` 525 mk_CJ (v1,rop,v2) arm_t arm_f = 526 [((CMP,NONE,F),NONE,[v1;v2],NONE):INST] ++ 527 [((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))] ++ 528 arm_f ++ 529 [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ 530 arm_t`; 531 532 533val mk_TR = Define ` 534 mk_TR (v1,rop,v2) (arm:INST list) = 535 ((CMP,NONE,F),NONE,[v1;v2],NONE) :: 536 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2))) :: 537 arm ++ 538 [((B,SOME AL,F),NONE,[],SOME (NEG (LENGTH arm + 2)))]`; 539 540(*---------------------------------------------------------------------------------*) 541(* Well-formed Composition *) 542(*---------------------------------------------------------------------------------*) 543 544val SC_IS_WELL_FORMED = Q.store_thm ( 545 "SC_IS_WELL_FORMED", 546 `!arm1 arm2. well_formed arm1 /\ well_formed arm2 547 ==> well_formed (mk_SC arm1 arm2)`, 548 549 REPEAT STRIP_TAC THEN 550 FULL_SIMP_TAC std_ss [well_formed, mk_SC] THEN 551 ASSUME_TAC ((GEN (Term `s:STATE`) o GEN (Term `iB:num->INST`) o SIMP_RULE set_ss [] o SIMP_RULE list_ss [] o 552 Q.SPECL [`arm1`,`arm2`,`[]`,`[]`,`FST (s:STATE)`,`iB`,`(s,{}):STATEPCS`]) CLOSED_SEQUENTIAL_COMPOSITION) THEN 553 RW_TAC std_ss [terminated, status_independent] THENL [ 554 555 RES_TAC THEN 556 FULL_SIMP_TAC std_ss [ADD_ASSOC, LENGTH_APPEND, closed] THEN 557 REPEAT GEN_TAC THEN 558 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 559 `FST (FST (runTo (upload arm1 iB (FST s)) (FST s + LENGTH arm1) (s,{}))) = FST s + LENGTH arm1` by METIS_TAC [TERMINATED_THM,FST] THEN 560 `?s' pcS'. runTo (upload arm1 iB (FST s)) (FST s + LENGTH arm1) (s,{}) = (s',pcS')` by METIS_TAC [ABS_PAIR_THM] THEN 561 `SND (runTo (upload arm2 iB (FST s + LENGTH arm1)) (FST s + LENGTH arm1 + LENGTH arm2) (s',pcS')) = 562 SND (runTo (upload arm2 iB (FST s + LENGTH arm1)) (FST s + LENGTH arm1 + LENGTH arm2) (s',{})) UNION pcS'` 563 by METIS_TAC [terminated, RUNTO_PCS_UNION, ADD_ASSOC] THEN 564 FULL_SIMP_TAC set_ss [] THEN 565 STRIP_TAC THENL [ 566 Q.PAT_ASSUM `FST s' = FST s + LENGTH arm1` (ASSUME_TAC o GSYM) THEN 567 FULL_SIMP_TAC arith_ss [ADD_ASSOC] THEN 568 RES_TAC THEN FULL_SIMP_TAC arith_ss [], 569 `x IN SND (runTo (upload arm1 iB (FST s)) (FST s + LENGTH arm1) (s,{}))` by METIS_TAC [SND] THEN 570 RES_TAC THEN FULL_SIMP_TAC arith_ss [] 571 ], 572 573 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 574 ASM_REWRITE_TAC [ADD_ASSOC] THEN 575 MATCH_MP_TAC (Q.SPECL [`{}`,`pcS0`] STOPAT_ANY_PCS_2) THEN 576 METIS_TAC [LENGTH_APPEND], 577 578 RES_TAC THEN 579 FULL_SIMP_TAC std_ss [ADD_ASSOC, LENGTH_APPEND] THEN 580 FIRST_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPECL [`(pos0,cpsr0,st):STATE`,`iB`]) THEN 581 Q.PAT_ASSUM `!s.x` (ASSUME_TAC o SIMP_RULE std_ss [] o Q.SPECL [`(pos1,cpsr1,st):STATE`,`iB`]) THEN 582 FULL_SIMP_TAC std_ss [get_st, status_independent] THEN 583 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 584 Q.ABBREV_TAC `s' = runTo (upload arm1 iB pos0) (pos0 + LENGTH arm1) ((pos0,cpsr0,st),{})` THEN 585 `?pos' cpsr' pcS'. (s':STATEPCS = ((FST (FST (s')), FST (SND (FST s')), SND (SND (FST s'))),SND s')) /\ 586 (runTo (upload arm1 iB pos1) (pos1 + LENGTH arm1) ((pos1,cpsr1,st),{}) = 587 ((pos',cpsr',SND (SND (FST s'))),pcS'))` 588 by (Q.UNABBREV_TAC `s'` THEN METIS_TAC [ABS_PAIR_THM, FST, SND]) THEN 589 `(pos0 + LENGTH arm1 = FST (FST s')) /\ (pos1 + LENGTH arm1 = pos')` by 590 (Q.UNABBREV_TAC `s'` THEN METIS_TAC [TERMINATED_THM, terminated, FST]) THEN 591 ONCE_ASM_REWRITE_TAC [] THEN 592 NTAC 5 (POP_ASSUM (K ALL_TAC)) THEN 593 METIS_TAC [RUNTO_STATE_PCS_SEPERATE, terminated, FST] 594 ] 595 ); 596 597val UNCOND_JUMP_OVER_THM = Q.store_thm ( 598 "UNCOND_JUMP_OVER_THM", 599 `!arm. well_formed ([((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm + 1)))] ++ arm) /\ 600 !iB pos cpsr st pcS. get_st (runTo (upload ([((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm + 1)))] ++ arm) iB pos) 601 (pos + LENGTH arm + 1) ((pos,cpsr,st),pcS)) = st`, 602 603 STRIP_TAC THEN 604 `!s pcS iB. step (upload (((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm + 1)))::arm) iB (FST s)) (s,pcS) = 605 ((FST s + LENGTH arm + 1, SND s), FST s INSERT pcS)` by ALL_TAC THENL [ 606 REPEAT GEN_TAC THEN 607 `?pc cpsr st. s = (pc,cpsr,st)` by METIS_TAC [ABS_PAIR_THM] THEN 608 FULL_SIMP_TAC std_ss [step_def] THEN 609 `0 < LENGTH (((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm + 1)))::arm)` by RW_TAC list_ss [] THEN 610 IMP_RES_TAC UPLOAD_LEM THEN 611 FULL_SIMP_TAC arith_ss [EL, HD] THEN 612 RW_TAC list_ss [decode_cond_def, decode_cond_cpsr_def, decode_op_thm, setS_def, getS_def, goto_thm], 613 614 RW_TAC std_ss [well_formed, terminated, status_independent] THENL [ 615 SIMP_TAC std_ss [closed] THEN 616 REPEAT GEN_TAC THEN 617 SIMP_TAC list_ss [Once RUNTO_EXPAND_ONCE] THEN 618 ASM_REWRITE_TAC [] THEN 619 SIMP_TAC list_ss [Once RUNTO_EXPAND_ONCE] THEN 620 RW_TAC set_ss [] THEN 621 RW_TAC arith_ss [], 622 `?s0 pcS0. s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 623 RW_TAC list_ss [stopAt_def] THEN 624 Q.EXISTS_TAC `SUC 0` THEN 625 RW_TAC arith_ss [FUNPOW], 626 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, get_st] THEN 627 FIRST_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [] o (Q.SPECL [`(pos0,cpsr0,st)`])) THEN 628 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE] THEN 629 POP_ASSUM (K ALL_TAC) THEN 630 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [] o (Q.SPECL [`(pos1,cpsr1,st)`])) THEN 631 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE] THEN 632 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE], 633 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, get_st] THEN 634 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [] o (Q.SPECL [`(pos,cpsr,st)`])) THEN 635 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE] 636 ] 637 ] 638 ); 639 640 641(*---------------------------------------------------------------------------------*) 642(* Hoare Logic for sequential compositions of flat codes *) 643(*---------------------------------------------------------------------------------*) 644 645val _ = type_abbrev("P_DSTATE", Type`:DSTATE->bool`); 646 647val HOARE_SC_FLAT = Q.store_thm ( 648 "HOARE_SC_FLAT", 649 `!arm1 arm2 (P:P_DSTATE) (Q:P_DSTATE) (R:P_DSTATE) (T:P_DSTATE). 650 well_formed arm1 /\ well_formed arm2 /\ 651 (!st. P st ==> Q (eval_fl arm1 st)) /\ (!st. R st ==> T (eval_fl arm2 st)) /\ (!st. Q st ==> R st) 652 ==> 653 (!st. P st ==> T (eval_fl (mk_SC arm1 arm2) st))`, 654 RW_TAC std_ss [mk_SC, SEQ_COMPOSITION_FLAT] 655 ); 656 657 658(*---------------------------------------------------------------------------------*) 659(* Enumerate all possibilities of conditions *) 660(*---------------------------------------------------------------------------------*) 661val eval_cond_def = Define ` 662 (eval_cond (v1,EQ,v2) s = (read s v1 = read s v2)) /\ 663 (eval_cond (v1,CS,v2) s = (read s v1 >=+ read s v2)) /\ 664 (eval_cond (v1,MI,v2) s = (let (n,z,c,v) = nzcv (read s v1) (read s v2) in n)) /\ 665 (eval_cond (v1,VS,v2) s = (let (n,z,c,v) = nzcv (read s v1) (read s v2) in v)) /\ 666 (eval_cond (v1,HI,v2) s = (read s v1 >+ read s v2)) /\ 667 (eval_cond (v1,GE,v2) s = (read s v1 >= read s v2)) /\ 668 (eval_cond (v1,GT,v2) s = (read s v1 > read s v2)) /\ 669 (eval_cond (v1,AL,v2) s = T) /\ 670 671 (eval_cond (v1,NE,v2) s = ~(read s v1 = read s v2)) /\ 672 (eval_cond (v1,CC,v2) s = (read s v1 <+ read s v2)) /\ 673 (eval_cond (v1,PL,v2) s = (let (n,z,c,v) = nzcv (read s v1) (read s v2) in ~n)) /\ 674 (eval_cond (v1,VC,v2) s = (let (n,z,c,v) = nzcv (read s v1) (read s v2) in ~v)) /\ 675 (eval_cond (v1,LS,v2) s = (read s v1 <=+ read s v2)) /\ 676 (eval_cond (v1,LT,v2) s = (read s v1 < read s v2)) /\ 677 (eval_cond (v1,LE,v2) s = (read s v1 <= read s v2)) /\ 678 (eval_cond (v1,NV,v2) s = F)`; 679 680val WORD_HI_EQ = prove ( 681 ``!a b. a >+ b = b <+ a``, 682 SIMP_TAC arith_ss [WORD_HI, WORD_LO]) 683 684val WORD_GT_EQ = prove ( 685 ``!a b. word_gt a b = word_lt b a``, 686 SIMP_TAC arith_ss [WORD_GT, WORD_LT] THEN 687 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN 688 ASM_SIMP_TAC arith_ss []) 689 690val WORD_GE_EQ = prove ( 691 ``!a b. word_ge a b = word_le b a``, 692 SIMP_TAC arith_ss [WORD_GE, WORD_LE] THEN 693 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN 694 ASM_SIMP_TAC arith_ss []) 695 696val WORD_LT_NOT_EQ = prove ( 697 ``!a b. word_lt a b ==> ~(a = b)``, 698 SIMP_TAC arith_ss [WORD_LT]) 699 700val WORD_SUB_EQ_ZERO = prove ( 701 ``!a b. (a - b = 0w) = (a = b)``, 702 METIS_TAC[WORD_SUB_ADD, WORD_ADD_0, WORD_SUB_REFL]); 703 704 705val ENUMERATE_CJ = Q.store_thm ( 706 "ENUMERATE_CJ", 707 `!cond pc cpsr st offset. 708 (eval_cond cond st ==> 709 ?cpsr'. decode_cond (pc + 1, decode_op (pc,cpsr,st) (CMP,(NONE :EXP option),[FST cond; SND (SND cond)],(NONE:OFFSET option))) 710 ((B,SOME (FST (SND cond)),F),NONE,[],SOME offset) = 711 ((goto (pc+1,SOME offset)), cpsr', st)) /\ 712 (~(eval_cond cond) st ==> 713 ?cpsr'. decode_cond (pc + 1, decode_op (pc,cpsr,st) (CMP,(NONE :EXP option),[FST cond; SND (SND cond)],(NONE:OFFSET option))) 714 ((B,SOME (FST (SND cond)),F),NONE,[],SOME offset) = 715 (pc+2,cpsr',st))`, 716 717 REPEAT GEN_TAC THEN 718 `?v1 rop v2. cond = (v1,rop,v2)` by METIS_TAC [ABS_PAIR_THM] THEN 719 ASM_SIMP_TAC list_ss [decode_op_def, OPERATOR_case_def, decode_cond_def, LET_THM] THEN 720 `eval_cond (v1,rop,v2) st = decode_cond_cpsr 721 (setNZCV cpsr 722 (word_msb (read st v1 - read st v2),read st v1 = read st v2, 723 read st v2 <=+ read st v1, 724 ~(word_msb (read st v1) = word_msb (read st v2)) /\ 725 ~(word_msb (read st v1) = 726 word_msb (read st v1 - read st v2)))) rop` by ALL_TAC THENL [ 727 ALL_TAC, 728 ASM_SIMP_TAC std_ss [] 729 ] THEN 730 731 Cases_on `rop` THEN 732 FULL_SIMP_TAC std_ss [eval_cond_def, decode_cond_def , decode_op_thm, 733 decode_cond_cpsr_def, setNZCV_thm, LET_THM, 734 nzcv_def] THENL [ 735 736 737 REWRITE_TAC [WORD_HIGHER_EQ], 738 SIMP_TAC std_ss [GSYM word_add_def, word_sub_def], 739 SIMP_TAC std_ss [GSYM word_add_def, word_sub_def] THEN METIS_TAC[], 740 SIMP_TAC std_ss [WORD_HI_EQ, WORD_LOWER_OR_EQ] THEN METIS_TAC[WORD_LOWER_NOT_EQ], 741 742 SIMP_TAC std_ss [word_ge_def, nzcv_def, LET_THM, GSYM word_add_def, 743 GSYM word_sub_def] THEN METIS_TAC[], 744 745 SIMP_TAC std_ss [word_gt_def, nzcv_def, LET_THM, GSYM word_add_def, 746 GSYM word_sub_def, WORD_SUB_EQ_ZERO] THEN METIS_TAC[], 747 748 PROVE_TAC[WORD_LOWER_EQ_ANTISYM, WORD_LOWER_CASES], 749 SIMP_TAC std_ss [GSYM word_add_def, GSYM word_sub_def], 750 751 SIMP_TAC std_ss [GSYM word_add_def, GSYM word_sub_def] THEN METIS_TAC[], 752 753 SIMP_TAC std_ss [WORD_LOWER_OR_EQ] THEN 754 METIS_TAC[WORD_LOWER_LOWER_CASES, WORD_LOWER_ANTISYM], 755 756 SIMP_TAC std_ss [word_lt_def, nzcv_def, LET_THM, GSYM word_add_def, 757 GSYM word_sub_def, WORD_SUB_EQ_ZERO] THEN METIS_TAC[], 758 759 SIMP_TAC std_ss [word_le_def, nzcv_def, LET_THM, GSYM word_add_def, 760 GSYM word_sub_def, WORD_SUB_EQ_ZERO] THEN METIS_TAC[] 761 ] 762) 763 764(*---------------------------------------------------------------------------------*) 765(* Cnditional-jump compositions of flat codes *) 766(*---------------------------------------------------------------------------------*) 767 768(* The condition is true, execute the true block *) 769 770val CJ_COMPOSITION_LEM_1 = Q.store_thm ( 771 "CJ_COMPOSITION_LEM_1", 772 `!cond arm_t arm_f arm' s iB. 773 well_formed arm_t /\ well_formed arm_f /\ eval_cond cond (SND (SND s)) /\ (arm' = mk_CJ cond arm_t arm_f) 774 ==> ?cpsr' cpsr''. 775 (runTo (upload arm' iB (FST s)) (FST s + LENGTH arm') (s,{}) = 776 ((FST s + LENGTH arm', cpsr', get_st (runTo (uploadCode arm_t iB) (LENGTH arm_t) ((0,SND s),{}))), 777 SND (runTo (upload arm_t iB (FST s+ LENGTH arm_f + 3)) (FST s + LENGTH arm_f + 3 + LENGTH arm_t) 778 ((FST s + LENGTH arm_f + 3,cpsr'', SND (SND s)),{FST s + 1;FST s}))))`, 779 780 RW_TAC std_ss [well_formed] THEN 781 `(?v1 rop v2. cond = (v1,rop,v2)) /\ (?pc cpsr st. s = (pc,cpsr,st))` by METIS_TAC [ABS_PAIR_THM] THEN 782 RW_TAC list_ss [mk_CJ, SUC_ONE_ADD] THEN REWRITE_TAC [ADD_ASSOC, uploadCode_def] THEN 783 784 Q.ABBREV_TAC `insts = ((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: (arm_f ++ 785 [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t)` THEN 786 `0 < LENGTH insts` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss []) THEN 787 `((upload insts iB pc) pc = ((CMP,NONE,F),NONE,[v1; v2],NONE)) /\ ((upload insts iB pc) (pc+1) = 788 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))))` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss [UPLOAD_LEM] THEN 789 IMP_RES_TAC UPLOAD_LEM THEN FULL_SIMP_TAC list_ss []) THEN 790 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def, decode_cond_thm] THEN 791 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def] THEN 792 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`pc`,`cpsr:DATA`,`st`, `POS (LENGTH (arm_f:INST list) + 2)`] ENUMERATE_CJ)) THEN 793 POP_ASSUM (ASSUME_TAC o Q.SPECL [`pc`,`cpsr`,`arm_f`]) THEN 794 FULL_SIMP_TAC std_ss [] THEN 795 RW_TAC arith_ss [goto_def, uploadCode_def] THEN 796 Q.UNABBREV_TAC `insts` THEN 797 Q.ABBREV_TAC `insts = ((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))::arm_f ++ 798 [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))]` THEN 799 `(LENGTH arm_f + 3 = LENGTH insts) /\ 800 (((CMP,NONE,F),NONE,[v1; v2],NONE)::((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: 801 (arm_f ++ [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t) = 802 insts ++ arm_t)` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss []) THEN 803 `LENGTH arm_f + (LENGTH arm_t + 3) = LENGTH arm_f + 3 + LENGTH arm_t` by RW_TAC arith_ss [] THEN 804 ASM_REWRITE_TAC [] THEN 805 NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 806 RW_TAC arith_ss [get_st, SIMP_RULE arith_ss [] 807 (Q.SPECL [`arm_t:INST list`,`insts:INST list`,`pc`, `iB`, `((pc + LENGTH (insts:INST list),cpsr',st),{pc+1; pc})`] CLOSED_PREFIX)] THEN 808 `FST (FST (runTo (upload arm_t iB (pc + LENGTH insts)) (pc + LENGTH insts + LENGTH arm_t) ((pc+LENGTH insts,cpsr',st),{pc+1; pc}))) = 809 pc + LENGTH insts + LENGTH arm_t` by METIS_TAC [TERMINATED_THM, FST] THEN 810 Q.EXISTS_TAC `FST (SND (FST (runTo (upload arm_t iB (pc+LENGTH insts)) (pc+LENGTH arm_t+LENGTH insts) ((pc+LENGTH insts,cpsr',st),{pc+1;pc}))))` THEN 811 Q.EXISTS_TAC `cpsr'` THEN 812 `SND (SND (FST (runTo (upload arm_t iB 0) (LENGTH arm_t) ((0,cpsr,st),{})))) = SND (SND (FST (runTo (upload arm_t iB (pc+LENGTH insts)) 813 (pc + LENGTH insts + LENGTH arm_t) ((pc + LENGTH insts,cpsr',st),{pc+1;pc}))))` by METIS_TAC [get_st, DSTATE_IRRELEVANT_PCS, 814 status_independent, DECIDE (Term `!x.0 + x = x`), FST] THEN 815 REWRITE_TAC [ADD_ASSOC] THEN 816 ONCE_REWRITE_TAC [METIS_PROVE [ADD_SYM, ADD_ASSOC] (Term `pc + LENGTH arm_t + LENGTH insts = pc + LENGTH insts + LENGTH arm_t`)] THEN 817 FULL_SIMP_TAC std_ss [] THEN 818 METIS_TAC [ABS_PAIR_THM, ADD_SYM, FST, SND] 819 ); 820 821 822val CJ_TERMINATED_LEM_1 = Q.store_thm ( 823 "CJ_TERMINATED_LEM_1", 824 `!cond arm_t arm_f arm' s pcS iB. 825 well_formed arm_t /\ well_formed arm_f /\ eval_cond cond (SND (SND s)) /\ (arm' = mk_CJ cond arm_t arm_f) 826 ==> terd (upload arm' iB (FST s)) (FST s + LENGTH arm') (s,pcS)`, 827 828 RW_TAC std_ss [well_formed, terd_def, stopAt_def] THEN 829 `(?v1 rop v2. cond = (v1,rop,v2)) /\ (?pc cpsr st. s = (pc,cpsr,st))` by METIS_TAC [ABS_PAIR_THM] THEN 830 RW_TAC list_ss [mk_CJ, SUC_ONE_ADD] THEN REWRITE_TAC [ADD_ASSOC] THEN 831 Q.ABBREV_TAC `insts = ((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: (arm_f ++ 832 [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t)` THEN 833 `?cpsr' st' pcS'. FUNPOW (step (upload insts iB pc)) 2 ((pc,cpsr,st),pcS) = ((pc+3+LENGTH arm_f,cpsr',st'),pcS')` by ALL_TAC THENL [ 834 `0 < LENGTH insts` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss []) THEN 835 `((upload insts iB pc) pc = ((CMP,NONE,F),NONE,[v1; v2],NONE)) /\ ((upload insts iB pc) (pc+1) = 836 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))))` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss [UPLOAD_LEM] THEN 837 IMP_RES_TAC UPLOAD_LEM THEN FULL_SIMP_TAC list_ss []) THEN 838 REWRITE_TAC [DECIDE ``2 = SUC 1``] THEN 839 RW_TAC list_ss [FUNPOW, step_def, decode_cond_thm] THEN 840 REWRITE_TAC [DECIDE ``1 = SUC 0``] THEN 841 RW_TAC list_ss [FUNPOW, step_def] THEN 842 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`pc`,`cpsr:DATA`,`st`, `POS (LENGTH (arm_f:INST list) + 2)`] ENUMERATE_CJ)) THEN 843 POP_ASSUM (ASSUME_TAC o Q.SPECL [`pc`,`cpsr`,`arm_f`]) THEN 844 FULL_SIMP_TAC std_ss [] THEN RW_TAC arith_ss [goto_def], 845 846 Q.ABBREV_TAC `pc' = pc + 3 + LENGTH arm_f` THEN 847 Q.EXISTS_TAC `shortest (\s':STATEPCS.FST (FST s') = pc' + LENGTH arm_t) (step (upload insts iB pc)) ((pc',cpsr',st'),pcS') + 2` THEN 848 RW_TAC std_ss [GSYM FUNPOW_FUNPOW] THEN 849 Q.UNABBREV_TAC `insts` THEN 850 Q.ABBREV_TAC `insts = ((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))::arm_f ++ 851 [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))]` THEN 852 `(pc + 3 + LENGTH arm_f = pc + LENGTH insts) /\ 853 (((CMP,NONE,F),NONE,[v1; v2],NONE)::((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: 854 (arm_f ++ [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t) = 855 insts ++ arm_t)` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss [] THEN Q.UNABBREV_TAC `pc'` THEN RW_TAC arith_ss []) THEN 856 Q.UNABBREV_TAC `pc'` THEN ASM_REWRITE_TAC [] THEN 857 `stopAt (\s'. FST (FST s') = pc + LENGTH insts + LENGTH arm_t) (step (upload (insts ++ arm_t) iB pc)) 858 ((pc + LENGTH insts,cpsr',st'),pcS')` by METIS_TAC [SIMP_RULE list_ss [] (Q.SPECL [`arm_t`,`insts`,`[]`] TERMINATED_MIDDLE),FST,terd_def] THEN 859 IMP_RES_TAC UNROLL_RUNTO THEN POP_ASSUM (ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC [] THEN 860 NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 861 RW_TAC arith_ss [SIMP_RULE arith_ss [] (Q.SPECL [`arm_t:INST list`,`insts:INST list`,`pc`, `iB`, 862 `((pc + LENGTH (insts:INST list),cpsr',st'),pcS')`] CLOSED_PREFIX)] THEN 863 `FST (FST (runTo (upload arm_t iB (pc + LENGTH insts)) (pc + (LENGTH insts + LENGTH arm_t)) ((pc+LENGTH insts,cpsr',st'),pcS'))) = 864 pc + LENGTH insts + LENGTH arm_t` by METIS_TAC [TERMINATED_THM, FST, ADD_ASSOC] THEN 865 FULL_SIMP_TAC arith_ss [] 866 ] 867 ); 868 869 870(* The condition is false, execute the false block *) 871 872val CJ_COMPOSITION_LEM_2 = Q.store_thm ( 873 "CJ_COMPOSITION_LEM_2", 874 `!cond arm_t arm_f arm' s iB. 875 well_formed arm_t /\ well_formed arm_f /\ ~(eval_cond cond (SND (SND s))) /\ (arm' = mk_CJ cond arm_t arm_f) 876 ==> ?cpsr' cpsr''. 877 (runTo (upload arm' iB (FST s)) (FST s + LENGTH arm') (s,{}) = 878 ((FST s+LENGTH arm', cpsr', get_st (runTo (uploadCode arm_f iB) (LENGTH arm_f) ((0,SND s),{}))), 879 FST s + 2 + LENGTH arm_f INSERT SND (runTo (upload arm_f iB (FST s + 2)) (FST s + 2 + LENGTH arm_f) 880 ((FST s + 2,cpsr'',SND (SND s)),{FST s + 1;FST s}))))`, 881 882 RW_TAC std_ss [well_formed] THEN 883 `(?v1 rop v2. cond = (v1,rop,v2)) /\ (?pc cpsr st. s = (pc,cpsr,st))` by METIS_TAC [ABS_PAIR_THM] THEN 884 RW_TAC list_ss [mk_CJ, SUC_ONE_ADD] THEN REWRITE_TAC [ADD_ASSOC, uploadCode_def] THEN 885 886 Q.ABBREV_TAC `insts = ((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: (arm_f ++ 887 [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t)` THEN 888 `0 < LENGTH insts` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss []) THEN 889 `((upload insts iB pc) pc = ((CMP,NONE,F),NONE,[v1; v2],NONE)) /\ ((upload insts iB pc) (pc+1) = 890 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))))` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss [UPLOAD_LEM] THEN 891 IMP_RES_TAC UPLOAD_LEM THEN FULL_SIMP_TAC list_ss []) THEN 892 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def, decode_cond_thm] THEN 893 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def] THEN 894 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`pc`,`cpsr:DATA`,`st`, `POS (LENGTH (arm_f:INST list) + 2)`] ENUMERATE_CJ)) THEN 895 POP_ASSUM (ASSUME_TAC o Q.SPECL [`pc`,`cpsr`,`arm_f`]) THEN 896 FULL_SIMP_TAC std_ss [] THEN 897 RW_TAC arith_ss [goto_def, uploadCode_def] THEN 898 Q.UNABBREV_TAC `insts` THEN 899 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 900 Q.ABBREV_TAC `insts1 = (((CMP,NONE,F),NONE,[v1; v2],NONE):INST)::[((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))]` THEN 901 Q.ABBREV_TAC `insts2 = ((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1))) :: arm_t` THEN 902 `(LENGTH arm_t + 1 = LENGTH insts2) /\ (LENGTH insts1 = 2) /\ 903 ((((CMP,NONE,F),NONE,[v1; v2],NONE)::((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: 904 (arm_f ++ [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t)) = 905 (insts1 ++ (arm_f:INST list)) ++ insts2)` by (Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN RW_TAC list_ss [] THEN 906 METIS_TAC [ rich_listTheory.CONS_APPEND, APPEND_ASSOC]) THEN 907 ASM_REWRITE_TAC [] THEN 908 POP_ASSUM (K ALL_TAC) THEN 909 `pc + LENGTH insts1 = FST (FST ((pc + 2,cpsr',st),{pc+1; pc}))` by RW_TAC arith_ss [] THEN 910 `?s1 pcS1. (s1,pcS1) = runTo (upload (insts1 ++ arm_f ++ insts2) iB pc) (FST (FST ((pc+2,cpsr',st),{pc+1; pc})) + 911 LENGTH arm_f) ((pc + 2,cpsr',st),{pc+1; pc})` by METIS_TAC [ABS_PAIR_THM] THEN 912 `~(pc + LENGTH insts1 + LENGTH arm_f + LENGTH insts2 IN ((FST ((pc + 2,cpsr',st))) INSERT pcS1))` by ALL_TAC THENL [ 913 POP_ASSUM MP_TAC THEN 914 RW_TAC std_ss [SIMP_RULE std_ss [] (Q.SPECL [`arm_f`,`insts1`,`insts2`,`pc`,`iB`, `((pc+2,cpsr',st),{pc+1;pc}):STATEPCS`] CLOSED_MIDDLE)] THEN 915 `pcS1 = SND (runTo (upload arm_f iB (pc+2)) (pc + 2 + LENGTH arm_f) ((pc+2,cpsr',st),{})) UNION {pc+1;pc}` 916 by METIS_TAC [RUNTO_PCS_UNION, SND, FST, terminated] THEN 917 `!x. x IN SND (runTo (upload arm_f iB (pc+2)) (pc + 2 + LENGTH arm_f) ((pc + 2,cpsr',st),{})) ==> 918 pc + 2 <= x /\ x < pc + 2 + LENGTH arm_f` by METIS_TAC [closed,FST] THEN 919 Q.PAT_ASSUM `LENGTH arm_t + 1 = LENGTH insts2` (ASSUME_TAC o GSYM) THEN 920 FULL_SIMP_TAC set_ss [] THEN FULL_SIMP_TAC arith_ss [] THEN 921 STRIP_TAC THEN RES_TAC THEN 922 FULL_SIMP_TAC arith_ss [], 923 924 `terd (upload (insts1 ++ arm_f ++ insts2) iB pc) (FST (FST ((pc + 2,cpsr',st),{pc+1; pc})) + LENGTH arm_f) 925 ((pc+2,cpsr',st),{pc+1; pc})` by METIS_TAC [FST, TERMINATED_MIDDLE] THEN 926 `pc + (LENGTH arm_f + (LENGTH arm_t + 3)) = pc + LENGTH insts1 + LENGTH arm_f + LENGTH insts2` by RW_TAC arith_ss [] THEN 927 Q.PAT_ASSUM `LENGTH insts1 = 2` (K ALL_TAC) THEN 928 Q.PAT_ASSUM `pc + LENGTH insts1 = x` (K ALL_TAC) THEN 929 ASM_REWRITE_TAC [] THEN 930 IMP_RES_TAC RUNTO_COMPOSITION THEN ASM_REWRITE_TAC [] THEN 931 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 932 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [] o GSYM) THEN 933 `(LENGTH insts1 = 2) /\ (LENGTH insts2 = LENGTH arm_t + 1)` by (Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` 934 THEN RW_TAC list_ss []) THEN 935 `runTo (upload arm_f iB (pc+2)) (pc + 2 + LENGTH arm_f) ((pc+2,cpsr',st),{pc+1;pc})= (s1,pcS1)` by METIS_TAC [FST, CLOSED_PAIR_EQ, 936 DECIDE (Term `pc + (LENGTH arm_f + 2) = pc + 2 + LENGTH arm_f`), 937 SIMP_RULE std_ss [] (Q.SPECL [`arm_f`,`insts1`,`insts2`,`pc`,`iB`, `((pc+2,cpsr',st),{pc+1;pc}):STATEPCS`] CLOSED_MIDDLE)] THEN 938 FULL_SIMP_TAC std_ss [] THEN 939 `FST s1 = pc + 2 + LENGTH arm_f` by METIS_TAC [TERMINATED_THM,FST] THEN 940 `?cpsr1 st1. s1:STATE = (SUC (SUC (pc + LENGTH arm_f)), cpsr1,st1)` by (RW_TAC arith_ss [SUC_ONE_ADD] THEN 941 METIS_TAC [FST, ADD_SYM, ADD_ASSOC,ABS_PAIR_THM]) THEN 942 FULL_SIMP_TAC std_ss [] THEN 943 `(upload (insts1++arm_f++insts2) iB pc) (pc+(LENGTH arm_f+2)) = ((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))` by ALL_TAC THENL [ 944 Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN 945 `LENGTH arm_f + 2 < LENGTH ([((CMP,NONE,F),NONE,[v1; v2],NONE);((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))] ++ arm_f ++ 946 ((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))::arm_t)` by RW_TAC list_ss [] THEN 947 RW_TAC list_ss [UPLOAD_LEM] THEN 948 `LENGTH (((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))::arm_f) <= LENGTH arm_f + 2` 949 by RW_TAC list_ss [] THEN 950 IMP_RES_TAC rich_listTheory.EL_APPEND2 THEN 951 FULL_SIMP_TAC list_ss [SUC_ONE_ADD], 952 953 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def, decode_cond_thm, decode_op_thm,goto_thm] THEN 954 RW_TAC arith_ss [Once RUNTO_EXPAND_ONCE, SUC_ONE_ADD, ADD_SYM, get_st] THEN 955 Q.EXISTS_TAC `cpsr'` THEN STRIP_TAC THENL [ 956 `SND (SND (FST (runTo (upload arm_f iB 0) (LENGTH arm_f) ((0,cpsr,st),{})))) = SND (SND (FST (runTo (upload arm_f iB (pc + 2)) 957 (pc + 2 + LENGTH arm_f) ((pc + 2,cpsr',st),{pc+1; pc}))))` by METIS_TAC [get_st, DSTATE_IRRELEVANT_PCS, 958 status_independent, DECIDE (Term `!x.0 + x = x`), FST, ADD_SYM] THEN 959 METIS_TAC [ABS_PAIR_THM, ADD_SYM, FST, SND], 960 METIS_TAC [ABS_PAIR_THM, ADD_SYM, ADD_ASSOC,FST, SND] 961 ] 962 ] 963 ] 964 ); 965 966 967val CJ_TERMINATED_LEM_2 = Q.store_thm ( 968 "CJ_TERMINATED_LEM_2", 969 `!cond arm_t arm_f arm' s pcS iB. 970 well_formed arm_t /\ well_formed arm_f /\ ~(eval_cond cond (SND (SND s))) /\ (arm' = mk_CJ cond arm_t arm_f) 971 ==> terd (upload arm' iB (FST s)) (FST s + LENGTH arm') (s,pcS)`, 972 973 RW_TAC std_ss [well_formed, terd_def, stopAt_def] THEN 974 `(?v1 rop v2. cond = (v1,rop,v2)) /\ (?pc cpsr st. s = (pc,cpsr,st))` by METIS_TAC [ABS_PAIR_THM] THEN 975 RW_TAC list_ss [mk_CJ, SUC_ONE_ADD] THEN REWRITE_TAC [ADD_ASSOC] THEN 976 Q.ABBREV_TAC `insts = ((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: (arm_f ++ 977 [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t)` THEN 978 `?cpsr' st' pcS'. FUNPOW (step (upload insts iB pc)) 2 ((pc,cpsr,st),pcS) = ((pc+2,cpsr',st'),pcS')` by ALL_TAC THENL [ 979 `0 < LENGTH insts` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss []) THEN 980 `((upload insts iB pc) pc = ((CMP,NONE,F),NONE,[v1; v2],NONE)) /\ ((upload insts iB pc) (pc+1) = 981 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))))` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss [UPLOAD_LEM] THEN 982 IMP_RES_TAC UPLOAD_LEM THEN FULL_SIMP_TAC list_ss []) THEN 983 REWRITE_TAC [DECIDE ``2 = SUC 1``] THEN 984 RW_TAC list_ss [FUNPOW, step_def, decode_cond_thm] THEN 985 REWRITE_TAC [DECIDE ``1 = SUC 0``] THEN 986 RW_TAC list_ss [FUNPOW, step_def] THEN 987 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`pc`,`cpsr:DATA`,`st`, `POS (LENGTH (arm_f:INST list) + 2)`] ENUMERATE_CJ)) THEN 988 POP_ASSUM (ASSUME_TAC o Q.SPECL [`pc`,`cpsr`,`arm_f`]) THEN 989 FULL_SIMP_TAC std_ss [] THEN RW_TAC arith_ss [goto_def], 990 991 Q.EXISTS_TAC `1 + shortest (\s':STATEPCS.FST (FST s') = pc + 2 + LENGTH arm_f) (step (upload insts iB pc)) ((pc+2,cpsr',st'),pcS') + 2` THEN 992 RW_TAC std_ss [GSYM FUNPOW_FUNPOW] THEN 993 Q.UNABBREV_TAC `insts` THEN 994 Q.ABBREV_TAC `insts1 = (((CMP,NONE,F),NONE,[v1; v2],NONE):INST)::[((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))]` THEN 995 Q.ABBREV_TAC `insts2 = ((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1))) :: arm_t` THEN 996 `(LENGTH arm_t + 1 = LENGTH insts2) /\ (2 = LENGTH insts1) /\ 997 ((((CMP,NONE,F),NONE,[v1; v2],NONE)::((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: 998 (arm_f ++ [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t)) = 999 (insts1 ++ (arm_f:INST list)) ++ insts2)` by (Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN RW_TAC list_ss [] THEN 1000 METIS_TAC [ rich_listTheory.CONS_APPEND, APPEND_ASSOC]) THEN 1001 ASM_REWRITE_TAC [] THEN 1002 `stopAt (\s'. FST (FST s') = pc + LENGTH insts1 + LENGTH arm_f) (step (upload (insts1 ++ arm_f ++ insts2) iB pc)) ((pc + LENGTH insts1, 1003 cpsr',st'),pcS')` by METIS_TAC [SIMP_RULE list_ss [] (Q.SPECL [`arm_f`,`insts1`,`insts2`] TERMINATED_MIDDLE),FST,terd_def] THEN 1004 IMP_RES_TAC UNROLL_RUNTO THEN POP_ASSUM (ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC [] THEN 1005 NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1006 IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`arm_f`,`insts1:INST list`,`insts2`,`pc`,`iB`,`((pc + LENGTH (insts1:INST list),cpsr',st'),pcS')`] 1007 CLOSED_MIDDLE)) THEN 1008 RW_TAC std_ss [] THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 1009 `FST (FST (runTo (upload arm_f iB (pc+LENGTH insts1)) (pc + LENGTH insts1 + LENGTH arm_f) ((pc + LENGTH insts1,cpsr',st'),pcS'))) = 1010 pc + LENGTH insts1 + LENGTH arm_f` by METIS_TAC [TERMINATED_THM,FST] THEN 1011 `?cpsr1 st1 pcS1.runTo (upload arm_f iB (pc+LENGTH insts1)) (pc + LENGTH insts1 + LENGTH arm_f) ((pc + LENGTH insts1,cpsr',st'),pcS') = 1012 ((pc + LENGTH insts1 + LENGTH arm_f,cpsr1,st1),pcS1)` by METIS_TAC [FST,ABS_PAIR_THM] THEN 1013 ASM_REWRITE_TAC [] THEN REWRITE_TAC [DECIDE (Term`1 = SUC 0`)] THEN 1014 RW_TAC std_ss [FUNPOW] THEN 1015 `(upload (insts1++arm_f++insts2) iB pc) (pc+(LENGTH arm_f+2)) = ((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))` by ALL_TAC THENL [ 1016 Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN 1017 `LENGTH arm_f + 2 < LENGTH ([((CMP,NONE,F),NONE,[v1; v2],NONE);((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))] ++ arm_f ++ 1018 ((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))::arm_t)` by RW_TAC list_ss [] THEN 1019 RW_TAC list_ss [UPLOAD_LEM] THEN 1020 `LENGTH (((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))::arm_f) <= LENGTH arm_f + 2` 1021 by RW_TAC list_ss [] THEN 1022 IMP_RES_TAC rich_listTheory.EL_APPEND2 THEN 1023 FULL_SIMP_TAC list_ss [SUC_ONE_ADD], 1024 POP_ASSUM MP_TAC THEN 1025 FULL_SIMP_TAC arith_ss [] THEN 1026 RW_TAC list_ss [step_def, decode_cond_thm, goto_def] 1027 ] 1028 ] 1029 ); 1030 1031 1032val LENGTH_CJ = Q.store_thm ( 1033 "LENGTH_CJ", 1034 `!cond arm_t arm_f. LENGTH (mk_CJ cond arm_t arm_f) = LENGTH arm_f + 3 + LENGTH arm_t`, 1035 REPEAT STRIP_TAC THEN 1036 `?v1 rop v2. cond = (v1,rop,v2)` by METIS_TAC [ABS_PAIR_THM] THEN 1037 RW_TAC list_ss [mk_CJ] 1038 ); 1039 1040 1041val CJ_IS_WELL_FORMED = Q.store_thm ( 1042 "CJ_IS_WELL_FORMED", 1043 `!cond arm_t arm_f. well_formed arm_t /\ well_formed arm_f 1044 ==> well_formed (mk_CJ cond arm_t arm_f)`, 1045 1046 REPEAT STRIP_TAC THEN 1047 RW_TAC std_ss [well_formed, terminated, status_independent] THENL [ 1048 1049 SIMP_TAC std_ss [closed] THEN REPEAT GEN_TAC THEN Cases_on `eval_cond cond (SND (SND s))` THENL [ 1050 ASSUME_TAC ((Q.SPECL [`cond`,`arm_t`,`arm_f`,`s:STATE`,`iB:num->INST`]) (SIMP_RULE std_ss [] CJ_COMPOSITION_LEM_1)) THEN 1051 RES_TAC THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1052 FULL_SIMP_TAC set_ss [LENGTH_CJ] THEN 1053 Q.ABBREV_TAC `pc = FST s + LENGTH arm_f + 3` THEN 1054 `SND (runTo (upload arm_t iB pc) (pc + LENGTH arm_t) ((pc,cpsr'',SND(SND s)),{FST s + 1; FST s})) = 1055 SND (runTo (upload arm_t iB pc) (pc + LENGTH arm_t) ((pc,cpsr'',SND(SND s)),{})) UNION {FST s + 1; FST s}` 1056 by METIS_TAC [well_formed, terminated, RUNTO_PCS_UNION, FST] THEN 1057 FULL_SIMP_TAC set_ss [] THEN 1058 STRIP_TAC THEN FULL_SIMP_TAC arith_ss [] THEN 1059 `pc <= x /\ x< pc + LENGTH arm_t` by METIS_TAC [well_formed,closed,FST] THEN 1060 Q.UNABBREV_TAC `pc` THEN 1061 FULL_SIMP_TAC arith_ss [], 1062 ASSUME_TAC ((Q.SPECL [`cond`,`arm_t`,`arm_f`,`s:STATE`,`iB:num->INST`]) (SIMP_RULE std_ss [] CJ_COMPOSITION_LEM_2)) THEN 1063 RES_TAC THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1064 FULL_SIMP_TAC set_ss [LENGTH_CJ] THEN 1065 STRIP_TAC THEN 1066 FULL_SIMP_TAC arith_ss [] THEN 1067 `FST s + (LENGTH arm_f + 2) = FST s + 2 + LENGTH arm_f` by RW_TAC arith_ss [] THEN 1068 `SND (runTo (upload arm_f iB (FST s+2)) (FST s + (LENGTH arm_f + 2)) ((FST s+2,cpsr'',SND(SND s)),{FST s + 1; FST s})) = 1069 SND (runTo (upload arm_f iB (FST s+2)) (FST s + 2 + LENGTH arm_f) ((FST s+2,cpsr'',SND(SND s)),{})) UNION {FST s + 1; FST s}` 1070 by METIS_TAC [well_formed, terminated, RUNTO_PCS_UNION, FST] THEN 1071 Q.PAT_ASSUM `x IN k` MP_TAC THEN 1072 FULL_SIMP_TAC set_ss [] THEN 1073 STRIP_TAC THEN FULL_SIMP_TAC arith_ss [] THEN 1074 `FST s + 2 <= x /\ x< FST s + 2 + LENGTH arm_f` by METIS_TAC [well_formed,closed,FST, 1075 DECIDE (Term`FST s + (LENGTH arm_f + 2) = FST s + 2 + LENGTH arm_f`)] THEN 1076 FULL_SIMP_TAC arith_ss [] 1077 ], 1078 1079 `?s0 pcS0.s = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN ASM_REWRITE_TAC [] THEN Cases_on `eval_cond cond (SND (SND s0))` THENL [ 1080 METIS_TAC [CJ_TERMINATED_LEM_1,terd_def], 1081 METIS_TAC [CJ_TERMINATED_LEM_2,terd_def] 1082 ], 1083 1084 SIMP_TAC std_ss [closed] THEN REPEAT GEN_TAC THEN Cases_on `eval_cond cond st` THENL [ 1085 ASSUME_TAC ((SIMP_RULE std_ss [] o Q.SPECL [`cond`,`arm_t`,`arm_f`,`(pos0,cpsr0,st):STATE`,`iB:num->INST`]) 1086 (SIMP_RULE std_ss [] CJ_COMPOSITION_LEM_1)) THEN 1087 ASSUME_TAC ((SIMP_RULE std_ss [] o Q.SPECL [`cond`,`arm_t`,`arm_f`,`(pos1,cpsr1,st):STATE`,`iB:num->INST`]) 1088 (SIMP_RULE std_ss [] CJ_COMPOSITION_LEM_1)) THEN 1089 METIS_TAC [get_st,FST,SND,well_formed,status_independent, uploadCode_def, DECIDE (Term`!x.0+x=x`)], 1090 ASSUME_TAC ((SIMP_RULE std_ss [] o Q.SPECL [`cond`,`arm_t`,`arm_f`,`(pos0,cpsr0,st):STATE`,`iB:num->INST`]) 1091 (SIMP_RULE std_ss [] CJ_COMPOSITION_LEM_2)) THEN 1092 ASSUME_TAC ((SIMP_RULE std_ss [] o Q.SPECL [`cond`,`arm_t`,`arm_f`,`(pos1,cpsr1,st):STATE`,`iB:num->INST`]) 1093 (SIMP_RULE std_ss [] CJ_COMPOSITION_LEM_2)) THEN 1094 METIS_TAC [get_st,FST,SND,well_formed,status_independent, uploadCode_def, DECIDE (Term`!x.0+x=x`)] 1095 ] 1096 ] 1097 ); 1098 1099 1100val HOARE_CJ_FLAT_LEM_1 = Q.store_thm ( 1101 "HAORE_CJ_FLAT_LEM_1", 1102 `!cond arm_t arm_f (P:P_DSTATE) (Q:P_DSTATE) (R:P_DSTATE). 1103 well_formed arm_t /\ well_formed arm_f /\ 1104 (!st. P st ==> Q (eval_fl arm_t st)) /\ (!st. P st ==> R (eval_fl arm_f st)) 1105 ==> 1106 !st. (P st /\ eval_cond cond st ==> Q (eval_fl (mk_CJ cond arm_t arm_f) st))`, 1107 1108 RW_TAC std_ss [well_formed] THEN 1109 `?v1 rop v2. cond = (v1,rop,v2)` by METIS_TAC [ABS_PAIR_THM] THEN 1110 RW_TAC list_ss [mk_CJ, eval_fl, SUC_ONE_ADD] THEN 1111 1112 (* The condition is true, execute the true block *) 1113 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def, UPLOADCODE_LEM, decode_cond_thm] THEN 1114 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def, UPLOADCODE_LEM] THEN 1115 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`0`,`0w`,`st`, `POS (LENGTH (arm_f:INST list) + 2)`] ENUMERATE_CJ)) THEN 1116 POP_ASSUM (ASSUME_TAC o Q.SPEC `arm_f`) THEN 1117 FULL_SIMP_TAC std_ss [] THEN 1118 RW_TAC arith_ss [goto_def, uploadCode_def] THEN 1119 Q.ABBREV_TAC `insts = ((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))::arm_f ++ 1120 [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))]` THEN 1121 `(LENGTH arm_f + 3 = LENGTH insts) /\ 1122 (((CMP,NONE,F),NONE,[v1; v2],NONE)::((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: 1123 (arm_f ++ [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t) = 1124 insts ++ arm_t)` by (Q.UNABBREV_TAC `insts` THEN RW_TAC list_ss []) THEN 1125 `LENGTH arm_f + (LENGTH arm_t + 3) = LENGTH arm_f + 3 + LENGTH arm_t` by RW_TAC arith_ss [] THEN 1126 ASM_REWRITE_TAC [] THEN 1127 NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1128 RW_TAC arith_ss [SIMP_RULE arith_ss [] 1129 (Q.SPECL [`arm_t:INST list`,`insts:INST list`,`0`, `(\i. ARB)`, `((LENGTH insts,cpsr',st),{1; 0})`] CLOSED_PREFIX)] THEN 1130 FULL_SIMP_TAC std_ss [eval_fl, uploadCode_def] THEN 1131 `LENGTH insts = FST (LENGTH insts,cpsr',st)` by RW_TAC std_ss [] THEN 1132 METIS_TAC [status_independent, DECIDE (Term `!x.0 + x = x`), ADD_SYM, DSTATE_IRRELEVANT_PCS] 1133 ); 1134 1135 1136val HOARE_CJ_FLAT_LEM_2 = Q.store_thm ( 1137 "HAORE_CJ_FLAT_LEM_2", 1138 `!cond arm_t arm_f (P:P_DSTATE) (Q:P_DSTATE) (R:P_DSTATE). 1139 well_formed arm_t /\ well_formed arm_f /\ 1140 (!st. P st ==> Q (eval_fl arm_t st)) /\ (!st. P st ==> R (eval_fl arm_f st)) 1141 ==> 1142 !st. (P st /\ ~(eval_cond cond st) ==> R (eval_fl (mk_CJ cond arm_t arm_f) st))`, 1143 1144 RW_TAC std_ss [well_formed] THEN 1145 `?v1 rop v2. cond = (v1,rop,v2)` by METIS_TAC [ABS_PAIR_THM] THEN 1146 RW_TAC list_ss [mk_CJ, eval_fl, SUC_ONE_ADD] THEN 1147 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def, UPLOADCODE_LEM, decode_cond_thm] THEN 1148 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def, UPLOADCODE_LEM] THEN 1149 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`0`,`0w`,`st`, `POS (LENGTH (arm_f:INST list) + 2)`] ENUMERATE_CJ)) THEN 1150 POP_ASSUM (ASSUME_TAC o Q.SPEC `arm_f`) THEN 1151 FULL_SIMP_TAC std_ss [uploadCode_def] THEN 1152 POP_ASSUM (K ALL_TAC) THEN 1153 Q.ABBREV_TAC `insts1 = (((CMP,NONE,F),NONE,[v1; v2],NONE):INST)::[((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2)))]` THEN 1154 Q.ABBREV_TAC `insts2 = ((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1))) :: arm_t` THEN 1155 `(LENGTH arm_t + 1 = LENGTH insts2) /\ (LENGTH insts1 = 2) /\ 1156 ((((CMP,NONE,F),NONE,[v1; v2],NONE)::((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm_f + 2))):: 1157 (arm_f ++ [((B,SOME AL,F),NONE,[],SOME (POS (LENGTH arm_t + 1)))] ++ arm_t)) = 1158 (insts1 ++ (arm_f:INST list)) ++ insts2)` by (Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN RW_TAC list_ss [] THEN 1159 METIS_TAC [ rich_listTheory.CONS_APPEND, APPEND_ASSOC]) THEN 1160 ASM_REWRITE_TAC [] THEN 1161 POP_ASSUM (K ALL_TAC) THEN 1162 `0 + LENGTH insts1 = FST (FST ((2,cpsr',st),{1; 0}))` by RW_TAC arith_ss [] THEN 1163 `?s1 pcS1. (s1,pcS1) = runTo (upload (insts1 ++ arm_f ++ insts2) (\i. ARB) 0) (FST (FST ((2,cpsr',st),{1; 0})) + 1164 LENGTH arm_f) ((2,cpsr',st),{1; 0})` by METIS_TAC [ABS_PAIR_THM] THEN 1165 `~(LENGTH insts1 + LENGTH arm_f + LENGTH insts2 IN ((FST ((2,cpsr',st))) INSERT pcS1))` by ALL_TAC THENL [ 1166 POP_ASSUM MP_TAC THEN 1167 RW_TAC std_ss [SIMP_RULE std_ss [] (Q.SPECL [`arm_f`,`insts1`,`insts2`,`0`,`\i. ARB`, `((2,cpsr',st),{1; 0}):STATEPCS`] CLOSED_MIDDLE)] THEN 1168 `pcS1 = SND (runTo (upload arm_f (\i. ARB) 2) (2 + LENGTH arm_f) ((2,cpsr',st),{})) UNION {1;0}` 1169 by METIS_TAC [RUNTO_PCS_UNION, SND, FST, terminated] THEN 1170 `!x. x IN SND (runTo (upload arm_f (\i. ARB) 2) (2 + LENGTH arm_f) ((2,cpsr',st),{})) ==> 1171 2 <= x /\ x < 2 + LENGTH arm_f` by METIS_TAC [closed,FST] THEN 1172 Q.PAT_ASSUM `LENGTH arm_t + 1 = LENGTH insts2` (ASSUME_TAC o GSYM) THEN 1173 FULL_SIMP_TAC set_ss [] THEN FULL_SIMP_TAC arith_ss [] THEN 1174 STRIP_TAC THEN RES_TAC THEN 1175 FULL_SIMP_TAC arith_ss [], 1176 1177 `terd (upload (insts1 ++ arm_f ++ insts2) (\i. ARB) 0) (FST (FST ((2,cpsr',st),{1; 0})) + LENGTH arm_f) 1178 ((2,cpsr',st),{1; 0})` by METIS_TAC [FST, TERMINATED_MIDDLE] THEN 1179 `LENGTH arm_f + (LENGTH arm_t + 3) = LENGTH insts1 + LENGTH arm_f + LENGTH insts2` by RW_TAC arith_ss [] THEN 1180 Q.PAT_ASSUM `LENGTH insts1 = 2` (K ALL_TAC) THEN 1181 ASM_REWRITE_TAC [] THEN 1182 IMP_RES_TAC RUNTO_COMPOSITION THEN ASM_REWRITE_TAC [] THEN 1183 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 1184 POP_ASSUM (ASSUME_TAC o GSYM) THEN 1185 `LENGTH insts1 = 2` by (Q.UNABBREV_TAC `insts1` THEN RW_TAC list_ss []) THEN 1186 `runTo (upload arm_f (\i. ARB) 2) (2 + LENGTH arm_f) ((2,cpsr',st),{1; 0})= (s1,pcS1)` by METIS_TAC [FST, CLOSED_PAIR_EQ, 1187 SIMP_RULE std_ss [] (Q.SPECL [`arm_f`,`insts1`,`insts2`,`0`,`\i. ARB`, `((2,cpsr',st),{1; 0}):STATEPCS`] CLOSED_MIDDLE)] THEN 1188 FULL_SIMP_TAC std_ss [] THEN 1189 `?cpsr1 st1. s1:STATE = (SUC (SUC (LENGTH arm_f)), cpsr1,st1)` by (RW_TAC arith_ss [SUC_ONE_ADD] THEN 1190 METIS_TAC [TERMINATED_THM,FST, ADD_SYM, ABS_PAIR_THM]) THEN 1191 Q.PAT_ASSUM `LENGTH arm_t + 1 = LENGTH insts2` (ASSUME_TAC o GSYM) THEN 1192 FULL_SIMP_TAC std_ss [] THEN 1193 Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN 1194 1195 RW_TAC list_ss [Once RUNTO_EXPAND_ONCE, step_def, GSYM uploadCode_def, UPLOADCODE_LEM,rich_listTheory.EL_APPEND2, 1196 decode_cond_thm, decode_op_thm,goto_thm] THEN 1197 1198 RW_TAC arith_ss [Once RUNTO_EXPAND_ONCE, SUC_ONE_ADD, get_st] THEN 1199 FULL_SIMP_TAC arith_ss [SUC_ONE_ADD, eval_fl, uploadCode_def, get_st] THEN 1200 METIS_TAC [get_st, status_independent, DECIDE (Term `!x.0 + x = x`), DSTATE_IRRELEVANT_PCS, FST, SND, ADD_SYM] 1201 ] 1202 ); 1203 1204val HOARE_CJ_FLAT_1 = Q.store_thm ( 1205 "HOARE_CJ_FLAT_1", 1206 `!cond arm_t arm_f (P:P_DSTATE) (Q:P_DSTATE) (R:P_DSTATE). 1207 well_formed arm_t /\ well_formed arm_f /\ 1208 (!st. P st ==> Q (eval_fl arm_t st)) /\ (!st. P st ==> R (eval_fl arm_f st)) 1209 ==> 1210 !st. (P st /\ eval_cond cond st ==> Q (eval_fl (mk_CJ cond arm_t arm_f) st)) /\ 1211 (P st /\ ~(eval_cond cond st) ==> R (eval_fl (mk_CJ cond arm_t arm_f) st))`, 1212 RW_TAC std_ss [] THEN 1213 METIS_TAC [HOARE_CJ_FLAT_LEM_1,HOARE_CJ_FLAT_LEM_2] 1214 ); 1215 1216val HOARE_CJ_FLAT = Q.store_thm ( 1217 "HOARE_CJ_FLAT", 1218 `!cond arm_t arm_f (P:P_DSTATE) (Q:P_DSTATE) (R:P_DSTATE). 1219 well_formed arm_t /\ well_formed arm_f /\ 1220 (!st. P st ==> Q (eval_fl arm_t st)) /\ (!st. P st ==> R (eval_fl arm_f st)) 1221 ==> 1222 !st. (P st ==> if eval_cond cond st then Q (eval_fl (mk_CJ cond arm_t arm_f) st) 1223 else R (eval_fl (mk_CJ cond arm_t arm_f) st))`, 1224 RW_TAC std_ss [] THEN 1225 METIS_TAC [HOARE_CJ_FLAT_LEM_1,HOARE_CJ_FLAT_LEM_2] 1226 ); 1227 1228 1229(*---------------------------------------------------------------------------------*) 1230(* Tail Recursion Composition *) 1231(*---------------------------------------------------------------------------------*) 1232 1233(*---------------------------------------------------------------------------------*) 1234(* The well-founded behaviors of finite loops *) 1235(* There exsits a number identifing the minimal number of rounds for the loop *) 1236(* condition to hold, i.e. the number of rounds executed until the loop *) 1237(* terminates *) 1238(* The WF_Loop specifies a case where the loop would surely terminates, *) 1239(* it is built on a well-founded relation on states of consecutive rounds *) 1240(*---------------------------------------------------------------------------------*) 1241 1242val WF_Loop = Define ` 1243 WF_Loop (cond_f,g) = 1244 ?R. WF R /\ (!s. ~(cond_f s) ==> R (g s) s)`; 1245 1246val WF_LOOP_IMP_TER = Q.store_thm ( 1247 "WF_LOOP_IMP_TER", 1248 `!g cond_f. WF_Loop (cond_f,g) ==> 1249 !s. ?k. cond_f (FUNPOW g k s)`, 1250 RW_TAC std_ss [WF_Loop] THEN 1251 IMP_RES_TAC WHILE_INDUCTION THEN 1252 POP_ASSUM (ASSUME_TAC o Q.SPECL [`g`,`$~ o cond_f`]) THEN 1253 FULL_SIMP_TAC list_ss [] THEN 1254 RES_TAC THEN 1255 `!s.(~cond_f s ==> ?k. cond_f (FUNPOW g k (g s))) ==> ?k.cond_f(FUNPOW g k s)` by ALL_TAC THENL [ 1256 REPEAT STRIP_TAC THEN 1257 FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN 1258 Cases_on `cond_f s` THENL [ 1259 Q.EXISTS_TAC `0` THEN 1260 METIS_TAC [FUNPOW_THM_1], 1261 Q.EXISTS_TAC `k + 1` THEN 1262 METIS_TAC [GSYM FUNPOW, SUC_ONE_ADD, ADD_SYM] 1263 ], 1264 POP_ASSUM MP_TAC THEN 1265 POP_ASSUM (ASSUME_TAC o Q.SPEC `\v.?k.cond_f (FUNPOW g k v)`) THEN 1266 METIS_TAC [] 1267 ] 1268 ); 1269 1270val WF_LOOP_IMP_STOPAT = Q.store_thm ( 1271 "WF_LOOP_IMP_STOPAT", 1272 `!g cond_f s. WF_Loop (cond_f,g) ==> 1273 stopAt cond_f g x`, 1274 RW_TAC std_ss [stopAt_def] THEN 1275 METIS_TAC [WF_LOOP_IMP_TER] 1276 ); 1277 1278val LOOP_SHORTEST_LESS_LEAST = Q.store_thm ( 1279 "LOOP_SHORTEST_LESS_LEAST", 1280 `!i s g cond_f. 1281 (i < shortest cond_f g s ==> ~cond_f (FUNPOW g i s))`, 1282 RW_TAC list_ss [shortest_def] THEN 1283 METIS_TAC [Q.SPEC `\k. cond_f (FUNPOW f k s)` LESS_LEAST] 1284 ); 1285 1286val LOOP_SHORTEST_THM = Q.store_thm ( 1287 "LOOP_SHORTEST_THM", 1288 `!i s g cond_f. WF_Loop (cond_f,g) ==> 1289 (i <= shortest cond_f g s ==> (shortest cond_f g s = shortest cond_f g (FUNPOW g i s) + i))`, 1290 RW_TAC list_ss [] THEN 1291 IMP_RES_TAC WF_LOOP_IMP_TER THEN 1292 POP_ASSUM (ASSUME_TAC o (Q.SPEC `s`)) THEN 1293 FULL_SIMP_TAC list_ss [shortest_def] THEN 1294 IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPEC `\n.cond_f (FUNPOW g n s)` LEAST_ADD_LEM)) THEN 1295 RW_TAC arith_ss [SIMP_RULE std_ss [FUN_EQ_THM] FUNPOW_FUNPOW, ADD_SYM] 1296 ); 1297 1298val WF_LOOP_IMP_LEAST = Q.store_thm ( 1299 "WF_LOOP_IMP_LEAST", 1300 `!cond_f g. WF_Loop (cond_f,g) ==> 1301 !s. cond_f (FUNPOW g (shortest cond_f g s) s)`, 1302 RW_TAC list_ss [shortest_def] THEN 1303 IMP_RES_TAC WF_LOOP_IMP_TER THEN 1304 POP_ASSUM (ASSUME_TAC o Q.SPEC `s`) THEN 1305 METIS_TAC [Q.SPEC `\k. cond_f (FUNPOW g k s)` LEAST_INTRO] 1306 ); 1307 1308val UNROLL_LOOP = Q.store_thm ( 1309 "UNROLL_LOOP", 1310 `!P g x. WF_Loop (P,g) ==> 1311 (WHILE ($~ o P) g x = (FUNPOW g (shortest P g x) x))`, 1312 Induct_on `shortest P g x` THENL [ 1313 RW_TAC list_ss [] THEN 1314 IMP_RES_TAC WF_LOOP_IMP_LEAST THEN 1315 POP_ASSUM (ASSUME_TAC o Q.SPEC `x`) THEN 1316 PAT_ASSUM ``0 = x`` (ASSUME_TAC o GSYM) THEN 1317 FULL_SIMP_TAC arith_ss [Once WHILE,FUNPOW], 1318 REPEAT GEN_TAC THEN 1319 POP_ASSUM (ASSUME_TAC o Q.SPECL [`P`,`g`,`g (x:'a)`]) THEN 1320 STRIP_TAC THEN 1321 POP_ASSUM (ASSUME_TAC o GSYM) THEN 1322 STRIP_TAC THEN 1323 `SUC 0 <= shortest P g x` by RW_TAC arith_ss [] THEN 1324 IMP_RES_TAC LOOP_SHORTEST_THM THEN 1325 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [FUNPOW]) THEN 1326 `v = shortest P g (g x)` by RW_TAC arith_ss [] THEN 1327 `0 < shortest P g x` by RW_TAC arith_ss [] THEN 1328 IMP_RES_TAC LOOP_SHORTEST_LESS_LEAST THEN 1329 REWRITE_TAC [Once WHILE] THEN 1330 FULL_SIMP_TAC arith_ss [FUNPOW] THEN 1331 METIS_TAC [FUNPOW, DECIDE (Term`shortest P g (g x) + 1 = SUC (shortest P g (g x))`)] 1332 ] 1333 ); 1334 1335(*---------------------------------------------------------------------------------*) 1336(* Induction on the number of rounds, *) 1337(*---------------------------------------------------------------------------------*) 1338 1339val LENGTH_TR = Q.store_thm ( 1340 "LENGTH_TR", 1341 `!cond arm. LENGTH (mk_TR cond arm) = LENGTH arm + 3`, 1342 REPEAT STRIP_TAC THEN 1343 `?v1 rop v2. cond = (v1,rop,v2)` by METIS_TAC [ABS_PAIR_THM] THEN 1344 RW_TAC list_ss [mk_TR] 1345 ); 1346 1347 1348val WF_TR = Define ` 1349 WF_TR (cond,arm) = 1350 !iB. WF_Loop ((\s:STATEPCS.eval_cond cond (SND (SND (FST s)))), 1351 (\s:STATEPCS.runTo (upload arm iB (FST (FST s))) (FST (FST s) + LENGTH arm) s))`; 1352 1353val loopNum = Define ` 1354 loopNum cond arm iB = shortest (\s'.eval_cond cond (get_st s')) (\s'.runTo (upload arm iB (FST (FST s'))) (FST (FST s') + LENGTH arm) s')`; 1355 1356val LOOPNUM_BASIC = Q.store_thm ( 1357 "LOOPNUM_BASIC", 1358 `!n cond arm. WF_TR (cond,arm) /\ (loopNum cond arm iB s = 0) ==> 1359 eval_cond cond (get_st s)`, 1360 RW_TAC std_ss [WF_TR, loopNum] THEN 1361 Q.PAT_ASSUM `!iB.x` (ASSUME_TAC o Q.SPEC `iB`) THEN IMP_RES_TAC WF_LOOP_IMP_STOPAT THEN 1362 POP_ASSUM (ASSUME_TAC o Q.SPEC `s:STATEPCS`) THEN 1363 FULL_SIMP_TAC std_ss [GSYM get_st] THEN 1364 METIS_TAC [Q.SPECL [`s:STATEPCS`,`(\s. eval_cond cond (get_st s))`, `(\s'. runTo (upload arm iB (FST (FST s'))) (FST (FST s') + LENGTH arm) s')`] 1365 (INST_TYPE [alpha|->Type `:STATEPCS`] SHORTEST_LEM)] 1366 ); 1367 1368val LOOPNUM_INDUCTIVE = Q.store_thm ( 1369 "LOOPNUM_INDUCTIVE", 1370 `!n cond arm. WF_TR (cond,arm) /\ (loopNum cond arm iB s = SUC n) ==> 1371 ~eval_cond cond (get_st s) /\ (n = loopNum cond arm iB (runTo (upload arm iB (FST (FST s))) (FST (FST s) + LENGTH arm) s))`, 1372 REWRITE_TAC [WF_TR, loopNum] THEN NTAC 4 STRIP_TAC THEN 1373 Q.PAT_ASSUM `!iB.x` (ASSUME_TAC o Q.SPEC `iB`) THEN IMP_RES_TAC WF_LOOP_IMP_STOPAT THEN 1374 POP_ASSUM (ASSUME_TAC o Q.SPEC `s:STATEPCS`) THEN 1375 FULL_SIMP_TAC std_ss [GSYM get_st] THEN 1376 METIS_TAC [Q.SPECL [`(\s. eval_cond cond (get_st s))`, `(\s'. runTo (upload arm iB (FST (FST s'))) (FST (FST s') + LENGTH arm) s')`,`s:STATEPCS`] 1377 (INST_TYPE [alpha|->Type `:STATEPCS`] SHORTEST_INDUCTIVE)] 1378 ); 1379 1380 1381val LOOPNUM_INDEPENDENT_OF_CPSR_PCS = Q.store_thm ( 1382 "LOOPNUM_INDEPENDENT_OF_CPSR_PCS", 1383 `!cond arm iB pc0 pc1 cpsr0 cpsr1 st pcS0 pcS1. 1384 well_formed arm /\ WF_TR (cond,arm) ==> 1385 (loopNum cond arm iB ((pc0,cpsr0,st),pcS0) = loopNum cond arm iB ((pc1,cpsr1,st),pcS1))`, 1386 Induct_on `loopNum cond arm iB ((pc0,cpsr0,st),pcS0)` THENL [ 1387 RW_TAC std_ss [WF_TR] THEN 1388 POP_ASSUM (ASSUME_TAC o Q.SPEC `iB`) THEN IMP_RES_TAC WF_LOOP_IMP_STOPAT THEN 1389 FIRST_ASSUM (ASSUME_TAC o Q.SPEC `((pc0,cpsr0,st),pcS0):STATEPCS`) THEN 1390 FULL_SIMP_TAC std_ss [loopNum,get_st] THEN 1391 IMP_RES_TAC SHORTEST_LEM THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1392 `(\s. eval_cond cond (SND (SND (FST s)))) ((pc1,cpsr1,st),pcS1)` by METIS_TAC [SND,FST] THEN 1393 METIS_TAC [Q.SPECL [`((pc1,cpsr1,st),pcS):STATEPCS`,`(\s. eval_cond cond (SND (SND (FST s))))`] 1394 (INST_TYPE [alpha|->Type `:STATEPCS`] SHORTEST_LEM)], 1395 REWRITE_TAC [Once EQ_SYM_EQ] THEN FULL_SIMP_TAC std_ss [loopNum, get_st] THEN 1396 REPEAT STRIP_TAC THEN 1397 FIRST_ASSUM (ASSUME_TAC o Q.SPEC `iB` o REWRITE_RULE [WF_TR]) THEN 1398 IMP_RES_TAC WF_LOOP_IMP_STOPAT THEN 1399 FIRST_ASSUM (ASSUME_TAC o Q.SPEC `((pc0,cpsr0,st),pcS0):STATEPCS`) THEN 1400 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 1401 `?pc' cpsr' st' pcS'. runTo (upload arm iB pc0) (pc0 + LENGTH arm) ((pc0,cpsr0,st),pcS0) = ((pc',cpsr',st'),pcS')` 1402 by METIS_TAC [ABS_PAIR_THM] THEN 1403 Q.PAT_ASSUM `!cond arm iB pc cpsr0 st pcS0.x` (ASSUME_TAC o Q.SPECL [`cond`,`arm`,`iB`,`pc'`,`cpsr'`,`st'`,`pcS'`]) THEN 1404 `~(\s. eval_cond cond (SND (SND (FST s)))) (((pc1,cpsr1,st),pcS1):STATEPCS)` by METIS_TAC [SND,FST] THEN 1405 Q.PAT_ASSUM `!x.stopAT x y x` (ASSUME_TAC o Q.SPEC `((pc1,cpsr1,st),pcS1):STATEPCS`) THEN 1406 `1 <= shortest (\s'. eval_cond cond (SND (SND (FST s')))) (\s'.runTo (upload arm iB (FST (FST s'))) (FST (FST s') + LENGTH arm) 1407 s') ((pc1,cpsr1,st),pcS1)` by METIS_TAC [Q.SPECL [`((pc1,cpsr1,st),pcS):STATEPCS`,`(\s. eval_cond cond (SND (SND (FST s))))`] 1408 (INST_TYPE [alpha|->Type `:STATEPCS`] SHORTEST_LEM)] THEN 1409 IMP_RES_TAC SHORTEST_THM THEN ASM_REWRITE_TAC [DECIDE (Term `1 = SUC 0`), FUNPOW] THEN 1410 REWRITE_TAC [DECIDE (Term `!x.x + SUC 0 = SUC x`), prim_recTheory.INV_SUC_EQ] THEN 1411 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 1412 `?pc'' cpsr'' pcS''. runTo (upload arm iB pc1) (pc1 + LENGTH arm) ((pc1,cpsr1,st),pcS1) = ((pc'',cpsr'',st'),pcS'')` by ALL_TAC THENL [ 1413 `st' = SND (SND (FST (runTo (upload arm iB pc1) (pc1 + LENGTH arm) ((pc1,cpsr1,st),pcS1))))`by 1414 METIS_TAC [DSTATE_IRRELEVANT_PCS, status_independent, well_formed, FST, get_st,SND] THEN 1415 Q.EXISTS_TAC `FST (FST (runTo (upload arm iB pc1) (pc1 + LENGTH arm) ((pc1,cpsr1,st),pcS1)))` THEN 1416 Q.EXISTS_TAC `FST (SND (FST (runTo (upload arm iB pc1) (pc1 + LENGTH arm) ((pc1,cpsr1,st),pcS1))))` THEN 1417 Q.EXISTS_TAC `SND (runTo (upload arm iB pc1) (pc1 + LENGTH arm) ((pc1,cpsr1,st),pcS1))` THEN 1418 RW_TAC std_ss [], 1419 FULL_SIMP_TAC std_ss [] THEN RES_TAC 1420 ] 1421 ] 1422 ); 1423 1424 1425val TR_TERMINATED_LEM = Q.store_thm ( 1426 "TR_TERMINATED_LEM", 1427 `!cond arm s iB. 1428 well_formed arm /\ WF_TR (cond,arm) 1429 ==> terd (upload (mk_TR cond arm) iB (FST (FST s))) (FST(FST s) + LENGTH (mk_TR cond arm)) s`, 1430 REPEAT GEN_TAC THEN 1431 Induct_on `loopNum cond arm iB s` THENL [ 1432 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [terd_def, stopAt_def, LENGTH_TR] THEN 1433 IMP_RES_TAC LOOPNUM_BASIC THEN 1434 Q.EXISTS_TAC `SUC (SUC 0)` THEN 1435 `(?v1 rop v2. cond = (v1,rop,v2)) /\ (?pc cpsr st pcS. s = ((pc,cpsr,st),pcS))` by METIS_TAC [ABS_PAIR_THM] THEN 1436 `0 < LENGTH (mk_TR (v1,rop,v2) arm)` by (RW_TAC list_ss [LENGTH_TR]) THEN 1437 `((upload (mk_TR (v1,rop,v2) arm) iB pc) pc = ((CMP,NONE,F),NONE,[v1; v2],NONE)) /\ ((upload (mk_TR (v1,rop,v2) arm) iB pc) (pc+1) = 1438 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2))))` by (FULL_SIMP_TAC std_ss [mk_TR] THEN RW_TAC list_ss [UPLOAD_LEM] THEN 1439 IMP_RES_TAC UPLOAD_LEM THEN FULL_SIMP_TAC list_ss []) THEN 1440 RW_TAC list_ss [FUNPOW, step_def, decode_cond_thm] THEN 1441 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`pc`,`cpsr:DATA`,`st`, `POS (LENGTH (arm:INST list) + 2)`] ENUMERATE_CJ)) THEN 1442 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [get_st] o Q.SPECL [`pc`,`cpsr`,`arm`]) THEN 1443 FULL_SIMP_TAC std_ss [] THEN RW_TAC arith_ss [goto_def], 1444 1445 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [terd_def, stopAt_def, LENGTH_TR] THEN 1446 IMP_RES_TAC LOOPNUM_INDUCTIVE THEN 1447 `(?v1 rop v2. cond = (v1,rop,v2)) /\ (?pc cpsr st pcS. s = ((pc,cpsr,st),pcS))` by METIS_TAC [ABS_PAIR_THM] THEN 1448 FULL_SIMP_TAC std_ss [terd_def,stopAt_def] THEN 1449 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 1450 `?cpsr1. FUNPOW (step (upload (mk_TR (v1,rop,v2) arm) iB pc)) 2 ((pc,cpsr,st),pcS) = ((pc+2,cpsr1,st),pc+1 INSERT pc INSERT pcS)` 1451 by (`0 < LENGTH (mk_TR (v1,rop,v2) arm)` by RW_TAC list_ss [LENGTH_TR] THEN 1452 `((upload (mk_TR (v1,rop,v2) arm) iB pc) pc = ((CMP,NONE,F),NONE,[v1; v2],NONE)) /\ ((upload (mk_TR (v1,rop,v2) arm) iB pc) (pc+1) = 1453 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2))))` by (POP_ASSUM (ASSUME_TAC o REWRITE_RULE [mk_TR]) THEN 1454 RW_TAC list_ss [mk_TR, UPLOAD_LEM] THEN IMP_RES_TAC UPLOAD_LEM THEN FULL_SIMP_TAC list_ss []) THEN 1455 REWRITE_TAC [DECIDE ``2 = SUC 1``] THEN 1456 RW_TAC list_ss [FUNPOW, step_def, decode_cond_thm] THEN 1457 REWRITE_TAC [DECIDE ``1 = SUC 0``] THEN 1458 RW_TAC list_ss [FUNPOW, step_def] THEN 1459 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`pc`,`cpsr:DATA`,`st`, `POS (LENGTH (arm:INST list) + 2)`] ENUMERATE_CJ)) THEN 1460 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [get_st] o Q.SPECL [`pc`,`cpsr`,`arm`]) THEN 1461 FULL_SIMP_TAC std_ss []) THEN 1462 1463 `?cpsr' pcS'. FUNPOW (step (upload (mk_TR (v1,rop,v2) arm) iB pc)) (1 + shortest (\s':STATEPCS.FST (FST s') = pc + 2 + LENGTH arm) 1464 (step (upload (mk_TR (v1,rop,v2) arm) iB pc)) ((pc+2,cpsr1,st),pc + 1 INSERT pc INSERT pcS) + 2) ((pc,cpsr,st),pcS) = 1465 ((pc,cpsr',get_st(runTo (upload arm iB pc) (pc+LENGTH arm) ((pc,cpsr,st),pcS))),pcS')` by ALL_TAC THENL [ 1466 RW_TAC std_ss [GSYM FUNPOW_FUNPOW] THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 1467 Q.ABBREV_TAC `insts1 = (((CMP,NONE,F),NONE,[v1; v2],NONE):INST)::[((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2)))]` THEN 1468 Q.ABBREV_TAC `insts2 = [((B,SOME AL,F),NONE,[],SOME (NEG (LENGTH arm + 2))):INST]` THEN 1469 `(LENGTH insts2 = 1) /\ (2 = LENGTH insts1) /\ (mk_TR (v1,rop,v2) arm = insts1 ++ (arm:INST list) ++ insts2)` 1470 by (Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN RW_TAC list_ss [mk_TR] THEN 1471 METIS_TAC [ rich_listTheory.CONS_APPEND, APPEND_ASSOC]) THEN 1472 ASM_REWRITE_TAC [] THEN 1473 `stopAt (\s'. FST (FST s') = pc + LENGTH insts1 + LENGTH arm) (step (upload (insts1 ++ arm ++ insts2) iB pc)) ((pc + LENGTH insts1, 1474 cpsr1,st), pc + 1 INSERT pc INSERT pcS)` by METIS_TAC [SIMP_RULE list_ss [] 1475 (Q.SPECL [`arm`,`insts1`,`insts2`] TERMINATED_MIDDLE),FST,well_formed,terd_def] THEN 1476 IMP_RES_TAC UNROLL_RUNTO THEN POP_ASSUM (ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC [] THEN 1477 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN FULL_SIMP_TAC std_ss [well_formed] THEN 1478 IMP_RES_TAC (SIMP_RULE std_ss [] (Q.SPECL [`arm`,`insts1:INST list`,`insts2`,`pc`,`iB`, 1479 `((pc + LENGTH (insts1:INST list),cpsr1,st),pc + 1 INSERT pc INSERT pcS):STATEPCS`] CLOSED_MIDDLE)) THEN 1480 RW_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN 1481 Q.ABBREV_TAC `s10 = runTo (upload arm iB (pc+LENGTH insts1)) (pc + LENGTH insts1 + LENGTH arm) ((pc + LENGTH insts1,cpsr1,st), 1482 pc + 1 INSERT pc INSERT pcS)` THEN 1483 `SND (SND (FST s10)) = SND (SND (FST (runTo (upload arm iB pc) (pc+LENGTH arm) ((pc,cpsr,st),pcS))))` by 1484 (Q.UNABBREV_TAC `s10` THEN METIS_TAC [get_st, DSTATE_IRRELEVANT_PCS, status_independent, FST, ADD_SYM]) THEN 1485 `FST (FST s10) = pc + LENGTH insts1 + LENGTH arm` by (Q.UNABBREV_TAC `s10` THEN METIS_TAC [TERMINATED_THM,FST]) THEN 1486 `?cpsr2. s10 = ((FST (FST s10),cpsr2,SND (SND (FST s10))),SND s10)` by METIS_TAC [ABS_PAIR_THM,FST,SND] THEN 1487 ONCE_ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN REWRITE_TAC [DECIDE (Term`1 = SUC 0`)] THEN 1488 RW_TAC std_ss [FUNPOW] THEN 1489 `(upload (insts1++arm++insts2) iB pc) (pc+(LENGTH arm+LENGTH (insts1:INST list)))=((B,SOME AL,F),NONE,[],SOME (NEG (LENGTH arm+2)))` 1490 by ( 1491 Q.PAT_ASSUM `2 = x` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN 1492 Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN 1493 REPEAT (POP_ASSUM (K ALL_TAC)) THEN RW_TAC list_ss [] THEN 1494 `LENGTH (arm:INST list) + 2 < LENGTH (((CMP,NONE,F),NONE,[v1; v2],NONE)::((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2))) 1495 :: (arm ++ [((B,SOME AL,F),NONE,[],SOME (NEG (LENGTH arm + 2))):INST]))` by RW_TAC list_ss [] THEN 1496 RW_TAC list_ss [UPLOAD_LEM] THEN 1497 `LENGTH (((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2)))::arm) <= LENGTH arm + 2` 1498 by RW_TAC list_ss [] THEN 1499 IMP_RES_TAC rich_listTheory.EL_APPEND2 THEN 1500 FULL_SIMP_TAC list_ss [SUC_ONE_ADD] 1501 ) THEN 1502 RW_TAC list_ss [step_def, decode_cond_thm, decode_op_thm, goto_def, get_st], 1503 1504 Q.PAT_ASSUM `!cond1 arm1 iB1 s1.x` (ASSUME_TAC o SIMP_RULE std_ss [LENGTH_TR] o Q.SPECL [`(v1,rop,v2)`,`arm`,`iB`, 1505 `((pc,cpsr',get_st (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS))),pcS')`]) THEN 1506 `loopNum (v1,rop,v2) arm iB (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS)) = 1507 loopNum (v1,rop,v2) arm iB ((pc,cpsr', get_st (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS))),pcS')` by 1508 METIS_TAC [ABS_PAIR_THM, LOOPNUM_INDEPENDENT_OF_CPSR_PCS, get_st, FST, SND] THEN RES_TAC THEN 1509 POP_ASSUM MP_TAC THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN STRIP_TAC THEN 1510 Q.ABBREV_TAC `n'' = 1 + shortest (\s'. FST (FST s') = pc + 2 + LENGTH arm) (step (upload (mk_TR (v1,rop,v2) arm) iB pc)) 1511 ((pc + 2,cpsr1,st),pc + 1 INSERT pc INSERT pcS) + 2` THEN 1512 Q.EXISTS_TAC `n' + n''` THEN 1513 RW_TAC arith_ss [GSYM FUNPOW_FUNPOW] 1514 ] 1515 ] 1516 ); 1517 1518val FUNPOW_DSTATE = Q.store_thm ( 1519 "FUNPOW_DSTATE", 1520 `!n arm iB pc0 pc1 cpsr0 cpsr1 st pcS0 pcS1. 1521 well_formed arm ==> 1522 (get_st (FUNPOW (\s'. runTo (upload arm iB (FST (FST s'))) (FST (FST s') + LENGTH arm) s') n ((pc0,cpsr0,st),pcS0)) = 1523 get_st (FUNPOW (\s'. runTo (upload arm iB (FST (FST s'))) (FST (FST s') + LENGTH arm) s') n ((pc1,cpsr1,st),pcS1)))`, 1524 Induct_on `n` THENL [ 1525 RW_TAC std_ss [get_st, FUNPOW], 1526 RW_TAC std_ss [FUNPOW] THEN 1527 `get_st (runTo (upload arm iB pc0) (pc0 + LENGTH arm) ((pc0,cpsr0,st),pcS0)) = get_st (runTo (upload arm iB pc1) (pc1 + LENGTH arm) 1528 ((pc1,cpsr1,st),pcS1))` by METIS_TAC [DSTATE_IRRELEVANT_PCS, status_independent, well_formed, FST, get_st] THEN 1529 METIS_TAC [ABS_PAIR_THM, FST, SND, get_st] 1530 ] 1531 ); 1532 1533val _ = (Globals.priming := SOME ""); 1534 1535val UNROLL_TR_LEM = Q.store_thm ( 1536 "UNROLL_TR_LEM", 1537 `!cond arm iB s pcS. 1538 well_formed arm /\ WF_TR (cond,arm) /\ ~(FST s + LENGTH (mk_TR cond arm) IN pcS) ==> 1539 ?cpsr' pcS' cpsr''. (runTo (upload (mk_TR cond arm) iB (FST s)) (FST s + LENGTH (mk_TR cond arm)) (s,pcS) = 1540 ((FST s + LENGTH (mk_TR cond arm), cpsr', get_st (FUNPOW (\s'.runTo (upload arm iB (FST (FST s'))) 1541 (FST (FST s')+LENGTH arm) s') (loopNum cond arm iB (s,pcS)) (s,pcS))), pcS')) /\ 1542 !x. x IN pcS' DIFF pcS ==> FST s <= x /\ x < FST s + LENGTH (mk_TR cond arm)`, 1543 1544 REPEAT GEN_TAC THEN 1545 Induct_on `loopNum cond arm iB (s,pcS)` THENL [ 1546 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [LENGTH_TR, FUNPOW] THEN 1547 IMP_RES_TAC LOOPNUM_BASIC THEN 1548 `(?v1 rop v2. cond = (v1,rop,v2)) /\ (?pc cpsr st. s = (pc,cpsr,st))` by METIS_TAC [ABS_PAIR_THM] THEN 1549 `0 < LENGTH (mk_TR (v1,rop,v2) arm)` by (RW_TAC list_ss [LENGTH_TR]) THEN 1550 `((upload (mk_TR (v1,rop,v2) arm) iB pc) pc = ((CMP,NONE,F),NONE,[v1; v2],NONE)) /\ ((upload (mk_TR (v1,rop,v2) arm) iB pc) (pc+1) = 1551 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2))))` by (FULL_SIMP_TAC std_ss [mk_TR] THEN RW_TAC list_ss [UPLOAD_LEM] THEN 1552 IMP_RES_TAC UPLOAD_LEM THEN FULL_SIMP_TAC list_ss []) THEN 1553 RW_TAC list_ss [Once RUNTO_ADVANCE, step_def, decode_cond_thm] THEN 1554 RW_TAC list_ss [Once RUNTO_ADVANCE, step_def] THEN 1555 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`pc`,`cpsr:DATA`,`st`, `POS (LENGTH (arm:INST list) + 2)`] ENUMERATE_CJ)) THEN 1556 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [get_st] o Q.SPECL [`pc`,`cpsr`,`arm`]) THEN 1557 FULL_SIMP_TAC std_ss [] THEN RW_TAC arith_ss [goto_def] THEN 1558 RW_TAC set_ss [Once RUNTO_ADVANCE, get_st] THEN RW_TAC arith_ss [], 1559 1560 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [LENGTH_TR, FUNPOW] THEN 1561 IMP_RES_TAC LOOPNUM_INDUCTIVE THEN 1562 `(?v1 rop v2. cond = (v1,rop,v2)) /\ (?pc cpsr st pcS. s = (pc,cpsr,st))` by METIS_TAC [ABS_PAIR_THM] THEN 1563 FULL_SIMP_TAC std_ss [] THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 1564 `0 < LENGTH (mk_TR (v1,rop,v2) arm)` by (RW_TAC list_ss [LENGTH_TR]) THEN 1565 `((upload (mk_TR (v1,rop,v2) arm) iB pc) pc = ((CMP,NONE,F),NONE,[v1; v2],NONE)) /\ ((upload (mk_TR (v1,rop,v2) arm) iB pc) (pc+1) = 1566 ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2))))` by (FULL_SIMP_TAC std_ss [mk_TR] THEN RW_TAC list_ss [UPLOAD_LEM] THEN 1567 IMP_RES_TAC UPLOAD_LEM THEN FULL_SIMP_TAC list_ss []) THEN 1568 RW_TAC list_ss [Once RUNTO_ADVANCE, step_def, decode_cond_thm] THEN 1569 RW_TAC list_ss [Once RUNTO_ADVANCE, step_def] THEN 1570 IMP_RES_TAC (SIMP_RULE arith_ss [] (Q.SPECL [`(v1,rop,v2)`,`pc`,`cpsr:DATA`,`st`, `POS (LENGTH (arm:INST list) + 2)`] ENUMERATE_CJ)) THEN 1571 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [get_st] o Q.SPECL [`pc`,`cpsr`,`arm`]) THEN 1572 FULL_SIMP_TAC std_ss [] THEN NTAC 5 (POP_ASSUM (K ALL_TAC)) THEN 1573 1574 Q.ABBREV_TAC `insts1 = (((CMP,NONE,F),NONE,[v1; v2],NONE):INST)::[((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2)))]` THEN 1575 Q.ABBREV_TAC `insts2 = [((B,SOME AL,F),NONE,[],SOME (NEG (LENGTH arm + 2))):INST]` THEN 1576 `(LENGTH insts2 = 1) /\ (2 = LENGTH insts1) /\ (mk_TR (v1,rop,v2) arm = insts1 ++ (arm:INST list) ++ insts2)` 1577 by (Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN RW_TAC list_ss [mk_TR] THEN 1578 METIS_TAC [ rich_listTheory.CONS_APPEND, APPEND_ASSOC]) THEN 1579 ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN 1580 `?s1 pcS1. (s1,pcS1) = runTo (upload (insts1 ++ arm ++ insts2) iB pc) (pc + LENGTH (insts1:INST list) + LENGTH arm) 1581 ((pc + LENGTH (insts1:INST list),cpsr',st),pc + 1 INSERT pc INSERT pcS)` by METIS_TAC [ABS_PAIR_THM] THEN 1582 `~(pc + (LENGTH arm + 3) IN (FST ((pc + LENGTH insts1,cpsr',st)) INSERT pcS1))` by ( 1583 POP_ASSUM MP_TAC THEN FULL_SIMP_TAC std_ss [well_formed] THEN 1584 RW_TAC std_ss [SIMP_RULE std_ss [] (Q.SPECL [`arm`,`insts1`,`insts2`,`pc`,`iB`, `((pc + LENGTH (insts1:INST list),cpsr',st), 1585 pc + 1 INSERT pc INSERT pcS) :STATEPCS`] CLOSED_MIDDLE)] THEN 1586 `pcS1 = SND (runTo (upload arm iB (pc+2)) (pc + 2 + LENGTH arm) ((pc+2,cpsr',st),{})) UNION (pc+1 INSERT pc INSERT pcS)` 1587 by METIS_TAC [RUNTO_PCS_UNION, SND, FST, terminated] THEN 1588 `!x. x IN SND (runTo (upload arm iB (pc+2)) (pc + 2 + LENGTH arm) ((pc + 2,cpsr',st),{})) ==> 1589 pc + 2 <= x /\ x < pc + 2 + LENGTH arm` by METIS_TAC [closed,FST] THEN 1590 FULL_SIMP_TAC set_ss [] THEN FULL_SIMP_TAC arith_ss [] THEN 1591 STRIP_TAC THEN Q.PAT_ASSUM `2 = LENGTH insts1` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN 1592 RES_TAC THEN FULL_SIMP_TAC arith_ss [] 1593 ) THEN 1594 1595 `terd (upload (insts1 ++ arm ++ insts2) iB pc) (pc + LENGTH (insts1:INST list) + LENGTH arm) 1596 ((pc+LENGTH(insts1:INST list),cpsr',st),pc+1 INSERT pc INSERT pcS)` by METIS_TAC [FST, well_formed, TERMINATED_MIDDLE] THEN 1597 IMP_RES_TAC RUNTO_COMPOSITION THEN Q.PAT_ASSUM `(s1,pcS1) = x` (ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC [] THEN 1598 `(get_st (s1,pcS1) = get_st (runTo (upload arm iB pc) (pc+LENGTH arm) ((pc,cpsr,st),{}))) /\ 1599 (FST (FST (s1,pcS1)) = pc + LENGTH insts1 + LENGTH arm) /\ 1600 (pcS1 = SND (runTo (upload arm iB (pc+LENGTH (insts1:INST list))) (pc+LENGTH (insts1:INST list)+LENGTH arm) 1601 ((pc+LENGTH (insts1:INST list),cpsr',st),{})) UNION (pc+1 INSERT pc INSERT pcS))` by 1602 METIS_TAC [DSTATE_IRRELEVANT_PCS, status_independent, SIMP_RULE std_ss [] (Q.SPECL [`arm`,`insts1:INST list`,`insts2`,`pc`, 1603 `iB`,`((pc + LENGTH (insts1:INST list),cpsr',st), pc + 1 INSERT pc INSERT pcS):STATEPCS`] CLOSED_MIDDLE), 1604 well_formed, FST, TERMINATED_THM,RUNTO_PCS_UNION, terminated, SND] THEN 1605 `?cpsr2. s1 = (FST (FST (s1,pcS1)),cpsr2,get_st(s1,pcS1))` by METIS_TAC [ABS_PAIR_THM,FST,SND, get_st] THEN 1606 ONCE_ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN RW_TAC std_ss [] THEN NTAC 6 (POP_ASSUM (K ALL_TAC)) THEN 1607 1608 `(upload (insts1++arm++insts2) iB pc) (pc+(LENGTH arm+LENGTH (insts1:INST list)))=((B,SOME AL,F),NONE,[],SOME (NEG (LENGTH arm+2)))` by ( 1609 Q.PAT_ASSUM `2 = x` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN 1610 Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN 1611 REPEAT (POP_ASSUM (K ALL_TAC)) THEN RW_TAC list_ss [] THEN 1612 `LENGTH (arm:INST list) + 2 < LENGTH (((CMP,NONE,F),NONE,[v1; v2],NONE)::((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2))) 1613 :: (arm ++ [((B,SOME AL,F),NONE,[],SOME (NEG (LENGTH arm + 2))):INST]))` by RW_TAC list_ss [] THEN 1614 RW_TAC list_ss [UPLOAD_LEM] THEN 1615 `LENGTH (((CMP,NONE,F),NONE,[v1; v2],NONE):: ((B,SOME rop,F),NONE,[],SOME (POS (LENGTH arm + 2)))::arm) <= LENGTH arm + 2` 1616 by RW_TAC list_ss [] THEN 1617 IMP_RES_TAC rich_listTheory.EL_APPEND2 THEN 1618 FULL_SIMP_TAC list_ss [SUC_ONE_ADD] 1619 ) THEN 1620 RW_TAC list_ss [Once RUNTO_ADVANCE, step_def, decode_cond_thm, decode_op_thm, goto_def] THEN 1621 1622 Q.ABBREV_TAC `pcS10 = pc + (LENGTH arm + LENGTH insts1) INSERT SND (runTo (upload arm iB (pc + LENGTH insts1)) 1623 (pc + (LENGTH arm + LENGTH insts1)) ((pc + LENGTH insts1,cpsr',st),{})) UNION (pc + 1 INSERT pc INSERT pcS)` THEN 1624 Q.PAT_ASSUM `!cond1 arm1 iB1 s pcS1.x` (ASSUME_TAC o SIMP_RULE std_ss [LENGTH_TR] o Q.SPECL [`(v1,rop,v2)`,`arm`,`iB`, 1625 `(pc,cpsr2,get_st (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),{})))`, `pcS10`]) THEN 1626 `loopNum (v1,rop,v2) arm iB (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS)) = 1627 loopNum (v1,rop,v2) arm iB ((pc,cpsr2, get_st (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),{}))),pcS10)` by 1628 METIS_TAC [ABS_PAIR_THM, LOOPNUM_INDEPENDENT_OF_CPSR_PCS, get_st, FST, SND, DSTATE_IRRELEVANT_PCS, well_formed] THEN 1629 `~(pc + (LENGTH arm + 3) IN pcS10)` by ( 1630 Q.UNABBREV_TAC `pcS10` THEN 1631 FULL_SIMP_TAC set_ss [] THEN FULL_SIMP_TAC arith_ss [] THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1632 FULL_SIMP_TAC std_ss [well_formed, closed] THEN 1633 Q.PAT_ASSUM `!s iB x.k` (ASSUME_TAC o Q.SPECL [`(pc + LENGTH (insts1:INST list),cpsr',st)`,`iB`]) THEN 1634 `!x. x IN SND (runTo (upload arm iB (pc + LENGTH insts1)) (pc + (LENGTH arm + LENGTH insts1)) ((pc + LENGTH insts1,cpsr',st),{})) ==> 1635 pc + LENGTH insts1 <= x /\ x < pc + LENGTH insts1 + LENGTH arm` by METIS_TAC [ADD_SYM,ADD_ASSOC,FST] THEN 1636 STRIP_TAC THEN RES_TAC THEN 1637 FULL_SIMP_TAC arith_ss [] 1638 ) THEN 1639 1640 `insts1 ++ arm ++ insts2 = mk_TR (v1,rop,v2) arm` by (Q.UNABBREV_TAC `insts1` THEN Q.UNABBREV_TAC `insts2` THEN RW_TAC list_ss [mk_TR]) THEN 1641 RES_TAC THEN FULL_SIMP_TAC arith_ss [] THEN STRIP_TAC THENL [ 1642 NTAC 19 (POP_ASSUM (K ALL_TAC)) THEN 1643 `get_st (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS)) = 1644 get_st (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),{}))` by METIS_TAC [DSTATE_IRRELEVANT_PCS,FST,well_formed] THEN 1645 `?pc'' cpsr'' pc'' pcS''. runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),pcS) = 1646 ((pc'',cpsr'',get_st (runTo (upload arm iB pc) (pc + LENGTH arm) ((pc,cpsr,st),{}))),pcS'')` by 1647 METIS_TAC [get_st, FST, SND, ABS_PAIR_THM] THEN 1648 METIS_TAC [FUNPOW_DSTATE, ABS_PAIR_THM, FST, SND], 1649 1650 `pcS'3 = pcS'` by METIS_TAC [] THEN 1651 NTAC 2 (POP_ASSUM MP_TAC) THEN NTAC 11 (POP_ASSUM (K ALL_TAC)) THEN POP_ASSUM MP_TAC THEN 1652 Q.UNABBREV_TAC `pcS10` THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN Q.PAT_ASSUM `loopNum x y z p = q` (K ALL_TAC) THEN 1653 POP_ASSUM (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC set_ss [] THEN NTAC 5 STRIP_TAC THEN 1654 FULL_SIMP_TAC set_ss [] THEN Q.PAT_ASSUM `!x1.k` (ASSUME_TAC o Q.SPEC `x`) THEN 1655 FULL_SIMP_TAC arith_ss [] THEN 1656 Cases_on `(x = pc + 1) \/ (x = pc) \/ (x = pc + (LENGTH (arm:INST list) + LENGTH (insts1:INST list)))` THENL [ 1657 RW_TAC arith_ss [], 1658 FULL_SIMP_TAC arith_ss [] THEN 1659 Cases_on `x IN SND (runTo (upload arm iB (pc + LENGTH insts1)) (pc + (LENGTH (arm:INST list) + LENGTH (insts1:INST list))) 1660 ((pc + LENGTH (insts1:INST list),cpsr',st),{}))` THENL [ 1661 FULL_SIMP_TAC arith_ss [well_formed, closed] THEN 1662 Q.PAT_ASSUM `!s iB x.k` (ASSUME_TAC o Q.SPECL [`(pc + LENGTH (insts1:INST list),cpsr',st):STATE`,`iB`,`x`]) THEN 1663 `pc + 2 <= x /\ x < pc + 2 + LENGTH arm` by METIS_TAC [FST, ADD_SYM, ADD_ASSOC] THEN 1664 RW_TAC arith_ss [], 1665 FULL_SIMP_TAC arith_ss [] THEN METIS_TAC [] 1666 ] 1667 ] 1668 ] 1669 ] 1670 ); 1671 1672 1673val _ = (Globals.priming := NONE); 1674 1675val TR_IS_WELL_FORMED = Q.store_thm ( 1676 "TR_IS_WELL_FORMED", 1677 `!cond arm. well_formed arm /\ WF_TR (cond,arm) 1678 ==> well_formed (mk_TR cond arm)`, 1679 REPEAT STRIP_TAC THEN 1680 RW_TAC std_ss [well_formed, terminated, status_independent] THENL [ 1681 SIMP_TAC std_ss [closed] THEN REPEAT GEN_TAC THEN 1682 METIS_TAC [SND,SIMP_RULE set_ss [] (Q.SPECL [`cond`,`arm`,`iB`,`s:STATE`,`{}`] UNROLL_TR_LEM)], 1683 METIS_TAC [terd_def, TR_TERMINATED_LEM], 1684 IMP_RES_TAC (SIMP_RULE set_ss [] (Q.SPECL [`cond`,`arm`,`iB`,`(pos0,cpsr0,st):STATE`,`{}`] UNROLL_TR_LEM)) THEN 1685 METIS_TAC [SND,FST,get_st,FUNPOW_DSTATE, LOOPNUM_INDEPENDENT_OF_CPSR_PCS] 1686 ] 1687 ); 1688 1689 1690val HOARE_TR_FLAT = Q.store_thm ( 1691 "HOARE_TR_FLAT", 1692 `!cond arm_t (P:P_DSTATE). 1693 well_formed arm /\ WF_TR (cond,arm) /\ 1694 (!st. P st ==> P (eval_fl arm st)) ==> 1695 !st. P st ==> P (eval_fl (mk_TR cond arm) st) /\ (eval_cond cond (eval_fl (mk_TR cond arm) st))`, 1696 REPEAT GEN_TAC THEN SIMP_TAC std_ss [LENGTH_TR, eval_fl] THEN STRIP_TAC THEN GEN_TAC THEN 1697 IMP_RES_TAC (SIMP_RULE set_ss [] (Q.SPECL [`cond`,`arm`,`iB`,`s:STATE`,`{}`] UNROLL_TR_LEM)) THEN 1698 POP_ASSUM (ASSUME_TAC o Q.SPECL [`(0,0w,st):STATE`,`\i.ARB`]) THEN 1699 FULL_SIMP_TAC std_ss [LENGTH_TR, FUNPOW,get_st, uploadCode_def] THEN 1700 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 1701 Induct_on `loopNum cond arm (\i.ARB) ((0,0w,st),{})` THENL [ 1702 REWRITE_TAC [Once EQ_SYM_EQ] THEN REPEAT GEN_TAC THEN SIMP_TAC std_ss [FUNPOW,get_st] THEN 1703 NTAC 5 STRIP_TAC THEN 1704 METIS_TAC [LOOPNUM_BASIC, get_st, FST, SND], 1705 1706 REWRITE_TAC [Once EQ_SYM_EQ] THEN REPEAT GEN_TAC THEN SIMP_TAC std_ss [FUNPOW] THEN 1707 NTAC 5 STRIP_TAC THEN 1708 IMP_RES_TAC LOOPNUM_INDUCTIVE THEN 1709 `v = loopNum cond arm (\i.ARB) ((0,0w,SND (SND (FST (runTo (upload arm (\i.ARB) 0) (LENGTH arm) ((0,0w,st),{}))))),{})` by 1710 METIS_TAC [ABS_PAIR_THM,DECIDE (Term`!x.0+x=x`),LOOPNUM_INDEPENDENT_OF_CPSR_PCS, get_st, FST, SND, DSTATE_IRRELEVANT_PCS, well_formed] THEN 1711 RES_TAC THEN 1712 METIS_TAC [SND,FST,get_st,FUNPOW_DSTATE, ABS_PAIR_THM] 1713 ] 1714 ); 1715 1716(*---------------------------------------------------------------------------------*) 1717(* Well-formed program upon any instB *) 1718(*---------------------------------------------------------------------------------*) 1719 1720val WELL_FORMED_INSTB_LEM = Q.store_thm ( 1721 "WELL_FORMED_INSTB_LEM", 1722 `!arm iB0 iB1 (s:STATEPCS) s'. 1723 closed arm /\ terminated arm /\ (instB = upload arm iB0 (FST (FST s))) /\ 1724 (?m. (s' = FUNPOW (step instB) m s) /\ m <= shortest (\s1:STATEPCS. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s) 1725 ==> 1726 (runTo (upload arm iB0 (FST (FST s))) (FST (FST s) + LENGTH arm) s' = 1727 runTo (upload arm iB1 (FST (FST s))) (FST (FST s) + LENGTH arm) s')`, 1728 1729 RW_TAC std_ss [] THEN 1730 Q.ABBREV_TAC `instB = upload arm iB0 (FST (FST s))` THEN 1731 Cases_on `m = shortest (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` THENL [ 1732 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [STOPAT_THM, terminated] THEN 1733 `FST (FST (FUNPOW (step instB) m s)) = FST (FST s) + LENGTH arm` by ( FULL_SIMP_TAC std_ss [stopAt_def, shortest_def] THEN 1734 METIS_TAC [Q.SPEC `\n.FST (FST (FUNPOW (step instB) n s)) = FST (FST s) + LENGTH arm` LEAST_INTRO]) THEN 1735 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE] THEN 1736 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE], 1737 1738 `m < shortest (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 1739 Q.PAT_ASSUM `~p` (K ALL_TAC) THEN 1740 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) (FUNPOW (step instB) m s)` by METIS_TAC [STOPAT_THM, terminated] THEN 1741 RW_TAC std_ss [UNROLL_RUNTO] THEN 1742 Induct_on `shortest (\s1:STATEPCS. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) (FUNPOW (step instB) m s)` THENL [ 1743 REWRITE_TAC [Once EQ_SYM_EQ] THEN 1744 RW_TAC list_ss [FUNPOW] THEN 1745 Q.ABBREV_TAC `s' = FUNPOW (step instB) m s` THEN 1746 `FST (FST s') = FST (FST s) + LENGTH arm` by METIS_TAC [Q.SPECL [`s'`, `\s1. FST (FST s1) = FST (FST s) + LENGTH arm`] 1747 (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_LEM)] THEN 1748 `?s0 pcS0. s' = (s0,pcS0)` by METIS_TAC [ABS_PAIR_THM] THEN 1749 METIS_TAC [RUNTO_ADVANCE, FST, SND], 1750 1751 REWRITE_TAC [Once EQ_SYM_EQ] THEN 1752 RW_TAC list_ss [FUNPOW] THEN 1753 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 1754 `stopAt (\s1. FST (FST s1) = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [terminated] THEN 1755 `SUC m <= shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 1756 `v + SUC m = shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by METIS_TAC [FUNPOW_SUC, ADD_SYM, 1757 (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_THM)] THEN 1758 `step (upload arm iB1 (FST (FST s))) (FUNPOW (step instB) m s) = step instB (FUNPOW (step instB) m s)` by ( 1759 Q.UNABBREV_TAC `instB` THEN 1760 `FST (FST s) <= FST (FST (FUNPOW (step (upload arm iB0 (FST (FST s)))) m s))` by METIS_TAC [CLOSED_THM] THEN 1761 `?n. FST (FST (FUNPOW (step (upload arm iB0 (FST (FST s)))) m s)) = FST (FST s) + n` by RW_TAC arith_ss [LESS_EQUAL_ADD] THEN 1762 `n < LENGTH arm` by METIS_TAC [LESS_MONO_ADD_EQ, CLOSED_THM, ADD_SYM] THEN 1763 `?s' pcS'. FUNPOW (step (upload arm iB0 (FST (FST s)))) m s = (s',pcS')` by METIS_TAC [ABS_PAIR_THM] THEN 1764 FULL_SIMP_TAC std_ss [] THEN 1765 RW_TAC std_ss [step_def] THEN 1766 METIS_TAC [UPLOAD_LEM] 1767 ) THEN 1768 1769 Cases_on `v` THENL [ 1770 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE, FUNPOW] THENL [ 1771 METIS_TAC [], 1772 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE, FUNPOW] THEN 1773 Q.ABBREV_TAC `s' = step instB (FUNPOW (step instB) m s)` THEN 1774 `(FST (FST s') = FST (FST s) + LENGTH arm)` by METIS_TAC [Q.SPECL [`s'`, `\s1. FST (FST s1) = 1775 FST (FST s) + LENGTH arm`] (INST_TYPE [alpha |-> Type `:STATEPCS`] SHORTEST_LEM)] 1776 ], 1777 1778 Q.PAT_ASSUM `!s.p` (ASSUME_TAC o SIMP_RULE std_ss [FUNPOW_SUC] o Q.SPECL [`s`,`arm`,`instB`,`SUC m`]) THEN 1779 `SUC m < shortest (\s'. FST (FST s') = FST (FST s) + LENGTH arm) (step instB) s` by RW_TAC arith_ss [] THEN 1780 RW_TAC std_ss [Once RUNTO_EXPAND_ONCE] THEN 1781 METIS_TAC [] 1782 ] 1783 ] 1784 ] 1785 ); 1786 1787val WELL_FORMED_INSTB = Q.store_thm ( 1788 "WELL_FORMED_INSTB", 1789 `!arm iB0 iB1 (s:STATEPCS). 1790 well_formed arm ==> 1791 (runTo (upload arm iB0 (FST (FST s))) (FST (FST s) + LENGTH arm) s = 1792 runTo (upload arm iB1 (FST (FST s))) (FST (FST s) + LENGTH arm) s)`, 1793 RW_TAC std_ss [well_formed] THEN 1794 IMP_RES_TAC (SIMP_RULE arith_ss [GSYM RIGHT_EXISTS_IMP_THM] 1795 (Q.SPECL [`arm`,`iB0`,`iB1`, `s:STATEPCS`, `FUNPOW (step instB) 0 s`] WELL_FORMED_INSTB_LEM)) THEN 1796 NTAC 11 (POP_ASSUM (K ALL_TAC)) THEN FULL_SIMP_TAC std_ss [] THEN 1797 POP_ASSUM (ASSUME_TAC o Q.SPECL [`s`,`iB0`,`0`]) THEN 1798 FULL_SIMP_TAC arith_ss [FUNPOW] 1799 ); 1800 1801 1802val _ = export_theory(); 1803 1804