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