1(* ========================================================================= *) 2(* FILE : blockScript.sml *) 3(* DESCRIPTION : A collection of lemmas used to verify the Block Data *) 4(* Transfer (ldm, stm) instruction class *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2003 - 2005 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["pred_setSimps", "wordsTheory", "wordsLib", "armLib", 11 "iclass_compLib", "io_onestepTheory", "my_listTheory", "armTheory", 12 "coreTheory", "lemmasTheory", "interruptsTheory"]; 13*) 14 15open HolKernel boolLib bossLib; 16open Q arithmeticTheory whileTheory rich_listTheory; 17open bitTheory sum_numTheory wordsLib wordsTheory; 18open armLib iclass_compLib io_onestepTheory my_listTheory; 19open armTheory coreTheory lemmasTheory interruptsTheory; 20 21val _ = new_theory "block"; 22val _ = ParseExtras.temp_loose_equality() 23(* ------------------------------------------------------------------------- *) 24 25infix \\ << >> 26 27val op \\ = op THEN; 28val op << = op THENL; 29val op >> = op THEN1; 30 31val std_ss = std_ss ++ boolSimps.LET_ss; 32val arith_ss = arith_ss ++ boolSimps.LET_ss; 33 34val WL = ``dimindex (:'a)``; 35 36val tt = set_trace "types"; 37 38(* ------------------------------------------------------------------------- *) 39 40val GEN_REG_LIST_def = Define` 41 GEN_REG_LIST wl n = (MAP SND o FILTER FST) (GENLIST (\b. (BIT b n,b)) wl)`; 42 43val MASK_BIT_def = Define` 44 MASK_BIT (list:bool ** 'a) mask = 45 CLEARBIT ((LEASTBIT (list && mask)) MOD ^WL) mask`; 46 47val MASKN_def = Define `MASKN n list = FUNPOW (MASK_BIT list) n UINT_MAXw`; 48 49val REG_WRITE_RP_def = Define` 50 REG_WRITE_RP n reg mode list data = 51 REG_WRITE reg mode (RP ldm list (MASKN n list)) data`; 52 53val REG_WRITEN_def = Define` 54 (REG_WRITEN 0 reg mode list i = reg) /\ 55 (REG_WRITEN (SUC n) reg mode list i = 56 REG_WRITE_RP n (REG_WRITEN n reg mode list i) mode list 57 (PROJ_DATA (i n)))`; 58 59(* ------------------------------------------------------------------------- *) 60 61val BITV_THM2 = prove( 62 `!n. BITV n = \b. SBIT (BIT b n) 0`, 63 REWRITE_TAC [FUN_EQ_THM] \\ SIMP_TAC std_ss [BITV_THM]); 64 65val CLEARBIT_THM = prove( 66 `!a w:bool ** 'a. a < ^WL ==> ~((CLEARBIT a w) %% a)`, 67 RW_TAC fcp_ss [CLEARBIT_def,word_modify_def]); 68 69val CLEARBIT_THM2 = prove( 70 `!a b w:bool ** 'a. ~(a = b) /\ (a < ^WL) ==> 71 ((CLEARBIT b w) %% a = w %% a)`, 72 RW_TAC fcp_ss [CLEARBIT_def,word_modify_def]); 73 74val GEN_REG_LIST_ZERO = prove( 75 `!n. GEN_REG_LIST 0 n = []`, 76 SIMP_TAC list_ss [GENLIST,FILTER,MAP,GEN_REG_LIST_def]); 77 78val GEN_REG_LIST_THM = prove( 79 `!wl n. GEN_REG_LIST (SUC wl) n = 80 if BIT wl n then SNOC wl (GEN_REG_LIST wl n) 81 else GEN_REG_LIST wl n`, 82 RW_TAC std_ss [GEN_REG_LIST_def,GENLIST,FILTER_SNOC,MAP_SNOC]); 83 84val LENGTH_GEN_REG_LIST = prove( 85 `!wl n. LENGTH (GEN_REG_LIST wl n) = SUM wl (BITV n)`, 86 Induct >> REWRITE_TAC [GEN_REG_LIST_ZERO,LENGTH,SUM_def] 87 \\ RW_TAC arith_ss [SUM_def,GEN_REG_LIST_THM,BITV_THM2,SBIT_def, 88 LENGTH_SNOC,ADD1]); 89 90(* ------------------------------------------------------------------------- *) 91 92val BIT_w2n = prove( 93 `!i w:bool ** 'a. i < ^WL ==> (BIT i (w2n w) = w %% i)`, 94 STRIP_TAC \\ Cases \\ STRIP_ASSUME_TAC EXISTS_HB 95 \\ ASM_SIMP_TAC (fcp_ss++ARITH_ss) 96 [w2n_n2w,dimword_def,BIT_def,MIN_DEF,BITS_COMP_THM2,GSYM BITS_ZERO3] 97 \\ ASM_SIMP_TAC fcp_ss [BIT_def,n2w_def]); 98 99val MASKN_ZERO = store_thm("MASKN_ZERO", 100 `!ireg. MASKN 0 list = UINT_MAXw`, 101 REWRITE_TAC [MASKN_def,FUNPOW]); 102 103val MASKN_SUC = prove( 104 `!n list. MASKN (SUC n) list = MASK_BIT list (MASKN n list)`, 105 REWRITE_TAC [MASKN_def,FUNPOW_SUC]); 106 107val lem = (SPEC `p` o SIMP_RULE bool_ss [] o INST [`P` |-> 108 `\b. (list && (MASKN 109 (SUM p (\b. (if BIT b ireg then 1 else 0))) list)) %% b`]) LEAST_THM; 110 111val MASKN_THM = prove( 112 `!p list:bool ** 'a. 113 (!x. p <= x /\ x < ^WL ==> 114 (MASKN (SUM p (BITV (w2n list))) list) %% x) /\ 115 (!x. x < p /\ p <= ^WL ==> 116 ~((list && (MASKN (SUM p (BITV (w2n list))) list)) %% x))`, 117 REWRITE_TAC [BITV_THM2] 118 \\ Induct 119 >> SIMP_TAC bool_ss [prim_recTheory.NOT_LESS_0,SUM_def,MASKN_def, 120 FUNPOW,word_T] 121 \\ STRIP_TAC 122 \\ POP_ASSUM (SPEC_THEN `list` (STRIP_ASSUME_TAC o 123 SIMP_RULE arith_ss [SBIT_def])) 124 \\ RW_TAC arith_ss [SUM_def,SBIT_def,GSYM ADD1,BIT_w2n] 125 \\ REWRITE_TAC [MASKN_SUC,MASK_BIT_def,LEASTBIT_def] 126 << [ 127 `(list && (MASKN 128 (SUM p (\b. (if BIT b (w2n list) then 1 else 0))) list)) %% p` 129 by ASM_SIMP_TAC (fcp_ss++ARITH_ss) [word_and_def] 130 \\ IMP_RES_TAC lem 131 \\ ASM_SIMP_TAC arith_ss [CLEARBIT_THM2], 132 `(list && (MASKN 133 (SUM p (\b. (if BIT b (w2n list) then 1 else 0))) list)) %% p` 134 by ASM_SIMP_TAC (fcp_ss++ARITH_ss) [word_and_def] 135 \\ IMP_RES_TAC lem 136 \\ Cases_on `x < p` 137 >> FULL_SIMP_TAC (fcp_ss++ARITH_ss) [CLEARBIT_THM2,word_and_def] 138 \\ `x = p` by DECIDE_TAC 139 \\ FULL_SIMP_TAC (fcp_ss++ARITH_ss) [CLEARBIT_THM,word_and_def], 140 Cases_on `x < p` >> ASM_SIMP_TAC arith_ss [] 141 \\ `x = p` by DECIDE_TAC 142 \\ ASM_SIMP_TAC (fcp_ss++ARITH_ss) [word_and_def]]); 143 144(* ------------------------------------------------------------------------- *) 145 146val SUM_BITS = prove( 147 `!p n. SUM (SUC p) (BITV n) = 148 if BIT p n then 149 SUC (SUM p (BITV n)) 150 else 151 SUM p (BITV n)`, 152 RW_TAC arith_ss [SUM_def,BITV_THM2,SBIT_def]); 153 154val SUM_BITS2 = prove( 155 `!p n. BIT p n ==> (SUM (SUC p) (BITV n) = SUC (SUM p (BITV n)))`, 156 RW_TAC bool_ss [SUM_BITS]); 157 158val SUM_BITS3 = prove( 159 `!p n. BIT p n ==> 160 (!q. q < p ==> ~(SUM (SUC q) (BITV n) = SUM (SUC p) (BITV n)))`, 161 REPEAT STRIP_TAC 162 \\ `~(BITV n p = 0)` 163 by ASM_SIMP_TAC arith_ss [GSYM BIT_def,NOT_BITS,BITV_def] 164 \\ IMP_RES_TAC ((GEN_ALL o REWRITE_RULE [GSYM LESS_EQ] o 165 SPEC `SUC m`) SUM_MONO) 166 \\ DECIDE_TAC); 167 168val EL_GEN_REG_LIST = prove( 169 `!x wl n. x < LENGTH (GEN_REG_LIST wl n) ==> 170 (EL x (GEN_REG_LIST wl n) = $LEAST (\p. SUM (SUC p) (BITV n) = SUC x))`, 171 Induct_on `wl` 172 >> REWRITE_TAC [prim_recTheory.NOT_LESS_0,GEN_REG_LIST_ZERO,LENGTH] 173 \\ RW_TAC arith_ss [GEN_REG_LIST_THM,LENGTH_SNOC] 174 \\ Cases_on `x < LENGTH (GEN_REG_LIST wl n)` 175 >> ASM_SIMP_TAC bool_ss [EL_SNOC] 176 \\ `x = LENGTH (GEN_REG_LIST wl n)` by DECIDE_TAC 177 \\ ASM_SIMP_TAC bool_ss [EL_LENGTH_SNOC] 178 \\ ASM_SIMP_TAC bool_ss [LENGTH_GEN_REG_LIST,GSYM SUM_BITS2] 179 \\ IMP_RES_TAC SUM_BITS3 180 \\ IMP_RES_TAC ((SIMP_RULE bool_ss [] o SPEC `wl` o INST [`P` |-> 181 `\x. SUM (SUC x) (BITV n) = SUM (SUC wl) (BITV n)`]) LEAST_THM) 182 \\ ASM_REWRITE_TAC []); 183 184val EXISTS_SUM_BITS = prove( 185 `!x wl n. x < LENGTH (GEN_REG_LIST wl n) ==> 186 ?p. p < wl /\ (x = SUM p (BITV n))`, 187 Induct_on `wl` 188 >> REWRITE_TAC [prim_recTheory.NOT_LESS_0,GEN_REG_LIST_ZERO,LENGTH] 189 \\ RW_TAC arith_ss [GEN_REG_LIST_THM,LENGTH_SNOC] 190 << [ 191 Cases_on `x < LENGTH (GEN_REG_LIST wl n)` 192 << [ 193 PAT_X_ASSUM `!x n. P` IMP_RES_TAC 194 \\ `p < SUC wl` by DECIDE_TAC \\ PROVE_TAC [], 195 `x = LENGTH (GEN_REG_LIST wl n)` by DECIDE_TAC 196 \\ FULL_SIMP_TAC bool_ss [LENGTH_GEN_REG_LIST] 197 \\ EXISTS_TAC `wl` \\ SIMP_TAC arith_ss [] 198 ], 199 PAT_X_ASSUM `!x n. P` IMP_RES_TAC 200 \\ `p < SUC wl` by DECIDE_TAC \\ PROVE_TAC []]); 201 202val SUM_LT = prove( 203 `!p list:bool ** 'a. 204 SUM p (BITV (w2n list)) < SUM ^WL (BITV (w2n list)) ==> 205 ?y. p <= y /\ y < ^WL /\ 206 ((list && (MASKN (SUM p (BITV (w2n list))) list)) %% y) /\ 207 (!q. q < y ==> 208 ~((list && (MASKN (SUM p (BITV (w2n list))) list)) %% q))`, 209 REPEAT STRIP_TAC 210 \\ POP_ASSUM (ASSUME_TAC o 211 (MATCH_MP ((GEN_ALL o snd o EQ_IMP_RULE o SPEC_ALL) SUM_LESS))) 212 \\ RULE_ASSUM_TAC (SIMP_RULE arith_ss 213 [BITV_THM,SBIT_def,METIS_PROVE [DECIDE ``~(1 = 0)``] 214 ``!a. ((if a then 1 else 0) = 0) = ~a``]) 215 \\ RULE_ASSUM_TAC (REWRITE_RULE [(SIMP_RULE std_ss [] o 216 SPEC `\y. p <= y /\ y < m /\ BIT y n`) LEAST_EXISTS]) 217 \\ ABBREV_TAC `z = LEAST y. p <= y /\ y < ^WL /\ BIT y (w2n list)` 218 \\ POP_ASSUM (K ALL_TAC) \\ EXISTS_TAC `z` 219 \\ RW_TAC arith_ss [] 220 >> (ASM_SIMP_TAC fcp_ss [MASKN_THM,word_and_def] \\ PROVE_TAC [BIT_w2n]) 221 \\ PAT_X_ASSUM `!n. P` (IMP_RES_TAC o SPEC `q`) 222 \\ FULL_SIMP_TAC arith_ss [] 223 >> (`q < p /\ p <= ^WL` by DECIDE_TAC \\ ASM_SIMP_TAC bool_ss [MASKN_THM]) 224 \\ ASM_SIMP_TAC (fcp_ss++ARITH_ss) [word_and_def] 225 \\ `q < ^WL` by DECIDE_TAC \\ PROVE_TAC [BIT_w2n]); 226 227val lem3a = prove( 228 `!y p list:bool ** 'a. p <= y /\ y < ^WL /\ 229 (list && (MASKN (SUM p (BITV (w2n list))) list)) %% y /\ 230 (!q. q < y ==> 231 ~((list && (MASKN (SUM p (BITV (w2n list))) list)) %% q)) ==> 232 (p <= y /\ y < ^WL /\ list %% y /\ (!q. q < y ==> ~(p <= q /\ list %% q)))`, 233 RW_TAC bool_ss [] 234 >> PAT_X_ASSUM `y < ^WL` (fn th => FULL_SIMP_TAC fcp_ss [word_and_def,th]) 235 \\ SPOSE_NOT_THEN STRIP_ASSUME_TAC 236 \\ PAT_X_ASSUM `!q. P` (SPEC_THEN `q` IMP_RES_TAC) 237 \\ `q < ^WL` by DECIDE_TAC 238 \\ POP_ASSUM (fn th => FULL_SIMP_TAC (fcp_ss++ARITH_ss) [word_and_def,th] 239 \\ ASSUME_TAC th) 240 \\ PROVE_TAC [MASKN_THM]); 241 242val SPEC_SUM_EQUAL2 = 243 (GEN_ALL o SIMP_RULE std_ss [BITV_def,GSYM NOT_BIT] o 244 SPECL [`p`,`y`,`BITV (w2n list)`]) SUM_EQUAL; 245 246val SPEC_SUM_EQUAL3 = PROVE [SUM_EQUAL] 247 ``!m n f. m <= n /\ (!q. m <= q /\ q < n ==> (f q = 0)) ==> 248 (SUM m f = SUM n f)``; 249 250val SPEC_SUM_EQUAL4 = 251 (GEN_ALL o SIMP_RULE std_ss [BITV_def,GSYM NOT_BIT] o 252 SPECL [`p`,`y`,`BITV (w2n list)`]) SPEC_SUM_EQUAL3; 253 254val lem3b = prove( 255 `!y p list:bool ** 'a. 256 (p <= y /\ y < ^WL /\ list %% y /\ 257 (!q. q < y ==> ~(p <= q /\ list %% q))) ==> 258 ((SUM (SUC y) (BITV (w2n list)) = SUC (SUM p (BITV (w2n list)))) /\ 259 (!q. q < y ==> 260 ~(SUM (SUC q) (BITV (w2n list)) = SUC (SUM p (BITV (w2n list))))))`, 261 RW_TAC arith_ss [SUM_def,BITV_THM,SBIT_def,GSYM ADD1,BIT_w2n] 262 \\ RULE_ASSUM_TAC (REWRITE_RULE [DECIDE 263 ``!a b c. (a ==> ~b \/ c) = (b /\ a ==> c)``]) 264 << [ 265 Cases_on `p = y` >> PROVE_TAC [] 266 \\ `p < y /\ !q. q < y ==> q < ^WL` by DECIDE_TAC 267 \\ PROVE_TAC [SPEC_SUM_EQUAL2,BIT_w2n], 268 RW_TAC arith_ss [GSYM ADD1,SPEC_SUM_EQUAL2] 269 << [ 270 Cases_on `~(q <= p)` >> PROVE_TAC [] 271 \\ FULL_SIMP_TAC arith_ss [] 272 \\ Cases_on `q < p` 273 >> (EXISTS_TAC `q` \\ ASM_SIMP_TAC arith_ss [BIT_w2n]) 274 \\ `p <= q` by DECIDE_TAC \\ PROVE_TAC [], 275 Cases_on `~(p < q)` >> PROVE_TAC [] 276 \\ FULL_SIMP_TAC arith_ss [] 277 \\ `p <= q` by DECIDE_TAC 278 \\ PROVE_TAC [], 279 `SUM p (BITV (w2n list)) = SUM y (BITV (w2n list))` 280 by (MATCH_MP_TAC SPEC_SUM_EQUAL4 \\ 281 ASM_SIMP_TAC arith_ss [BIT_w2n]) 282 \\ ASM_SIMP_TAC arith_ss [] 283 \\ `SUC (SUM y (BITV (w2n list))) = SUM (SUC y) (BITV (w2n list))` 284 by FULL_SIMP_TAC arith_ss 285 [BITV_def,SBIT_def,SUM_def,ADD1,GSYM BIT_def,BIT_w2n] 286 \\ POP_ASSUM SUBST1_TAC 287 \\ `q <= y` by DECIDE_TAC 288 \\ METIS_TAC [(GEN_ALL o SIMP_RULE arith_ss 289 [BITV_def,GSYM NOT_BIT] o 290 SPECL [`q`,`y`,`BITV (w2n list)`]) SUM_MONO, 291 DECIDE ``a < b ==> ~(a = b:num)``,BIT_w2n]]]); 292 293val lem3 = GEN_ALL (IMP_TRANS (SPEC_ALL lem3a) (SPEC_ALL lem3b)); 294 295val IN_LDM_STM = 296 SIMP_CONV (std_ss++pred_setSimps.PRED_SET_ss) [] ``ic IN {ldm; stm}``; 297 298val INST_16 = 299 SIMP_RULE (bool_ss++SIZES_ss) [] o Thm.INST_TYPE [alpha |-> ``:16``]; 300 301val REGISTER_LIST_LEM = prove( 302 `!ic x list:word16. 303 (ic IN {ldm; stm}) /\ 304 x < LENGTH (GEN_REG_LIST 16 (w2n list)) ==> 305 (n2w (EL x (GEN_REG_LIST 16 (w2n list))) = RP ic list (MASKN x list))`, 306 RW_TAC bool_ss [EL_GEN_REG_LIST] 307 \\ IMP_RES_TAC EXISTS_SUM_BITS 308 \\ FULL_SIMP_TAC bool_ss [GSYM IN_LDM_STM,RP_def,LEASTBIT_def, 309 LENGTH_GEN_REG_LIST] 310 \\ IMP_RES_TAC (INST_16 SUM_LT) 311 \\ IMP_RES_TAC ((SIMP_RULE bool_ss [] o SPEC `y` o 312 INST [`P` |-> `\b. (list:word16 && (MASKN 313 (SUM p (BITV (w2n list))) list)) %% b`]) LEAST_THM) 314 \\ IMP_RES_TAC (INST_16 lem3) 315 \\ NTAC 4 (POP_ASSUM (K ALL_TAC)) 316 \\ IMP_RES_TAC ((SIMP_RULE bool_ss [] o SPEC `y` o 317 INST [`P` |-> `\p'. SUM (SUC p') (BITV n) = 318 SUC (SUM p (BITV n))`]) LEAST_THM) 319 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w,LESS_MOD]); 320 321(* ------------------------------------------------------------------------- *) 322 323val MUST_BE_EQUAL = DECIDE ``!x y. x < SUC y /\ ~(x < y) ==> (x = y)``; 324 325val EL_GEN_REG_LIST_LT_WL = prove( 326 `!wl x n. x < LENGTH (GEN_REG_LIST wl n) ==> (EL x (GEN_REG_LIST wl n) < wl)`, 327 Induct >> SIMP_TAC list_ss [GEN_REG_LIST_ZERO] 328 \\ RW_TAC std_ss [GEN_REG_LIST_def,GENLIST,FILTER_SNOC,MAP_SNOC,LENGTH_SNOC] 329 \\ FULL_SIMP_TAC arith_ss [(GSYM o SIMP_RULE std_ss []) GEN_REG_LIST_def, 330 EL_SNOC,(GSYM o CONJUNCT1) EL,prim_recTheory.LESS_SUC] 331 \\ Cases_on `x < LENGTH (GEN_REG_LIST wl n)` 332 >> ASM_SIMP_TAC arith_ss [EL_SNOC,prim_recTheory.LESS_SUC] 333 \\ IMP_RES_TAC MUST_BE_EQUAL 334 \\ ASM_SIMP_TAC arith_ss [EL_LENGTH_SNOC]); 335 336(* ------------------------------------------------------------------------- *) 337 338val EL_FILTER = prove( 339 `!f g h j k l. 340 (!x. x < LENGTH k ==> 341 (f (EL x k) = g (EL x l)) /\ 342 (h (EL x k) = j (EL x l))) /\ 343 (LENGTH k = LENGTH l) ==> 344 (!x. x < LENGTH (FILTER f k) ==> 345 (h (EL x (FILTER f k)) = j (EL x (FILTER g l))))`, 346 Induct_on `k` \\ Induct_on `l` \\ RW_TAC list_ss [] 347 >> (Cases_on `x` \\ ASM_SIMP_TAC list_ss [EL_CONS,prim_recTheory.PRE] \\ 348 METIS_TAC [EL,HD,TL,LESS_MONO_EQ,prim_recTheory.LESS_0]) 349 \\ METIS_TAC [EL,HD,TL,LESS_MONO_EQ,prim_recTheory.LESS_0]); 350 351val LENGTH_FILTER = prove( 352 `!f g k l. (!x. x < LENGTH k ==> (f (EL x k) = g (EL x l))) /\ 353 (LENGTH k = LENGTH l) ==> 354 (LENGTH (FILTER f k) = LENGTH (FILTER g l))`, 355 Induct_on `k` \\ Induct_on `l` \\ RW_TAC list_ss [] 356 \\ METIS_TAC [EL,HD,TL,LESS_MONO_EQ,prim_recTheory.LESS_0]); 357 358val REGISTER_LIST_GEN_REG_LIST = prove( 359 `!list. GEN_REG_LIST 16 (w2n list) = MAP w2n (REGISTER_LIST list)`, 360 STRIP_TAC \\ MATCH_MP_TAC LIST_EQ \\ REWRITE_TAC [REGISTER_LIST_def] 361 \\ Q.ABBREV_TAC `sz = 16` 362 \\ SIMP_TAC list_ss [GEN_REG_LIST_def,REGISTER_LIST_def] 363 \\ `LENGTH (FILTER FST (GENLIST (\b. (BIT b (w2n list),b)) sz)) = 364 LENGTH (FILTER FST (GENLIST (\i. (list %% i,(n2w i):word4)) sz))` 365 by (MATCH_MP_TAC LENGTH_FILTER \\ 366 SIMP_TAC std_ss [LENGTH_GENLIST,EL_GENLIST,INST_16 BIT_w2n, Abbr`sz`]) 367 \\ RW_TAC list_ss [EL_MAP] 368 \\ `!z:bool # word4. w2n (SND z) = (w2n o SND) z` 369 by SIMP_TAC std_ss [] 370 \\ POP_ASSUM (fn th => REWRITE_TAC [th]) \\ POP_ASSUM MP_TAC 371 \\ CONV_TAC (ONCE_DEPTH_CONV SYM_CONV) \\ MATCH_MP_TAC EL_FILTER 372 \\ SIMP_TAC (list_ss++SIZES_ss) 373 [EL_GENLIST,LENGTH_GENLIST,w2n_n2w,BIT_w2n] 374 \\ SIMP_TAC (list_ss ++ SIZES_ss) [Abbr`sz`, BIT_w2n]); 375 376val EL_GEN_REG_LIST_EQUAL = prove( 377 `!wl x y n. 378 x < LENGTH (GEN_REG_LIST wl n) /\ 379 y < LENGTH (GEN_REG_LIST wl n) ==> 380 ((EL x (GEN_REG_LIST wl n) = EL y (GEN_REG_LIST wl n)) = (x = y))`, 381 Induct >> SIMP_TAC list_ss [GEN_REG_LIST_ZERO] 382 \\ RW_TAC std_ss [GEN_REG_LIST_def,GENLIST,FILTER_SNOC,MAP_SNOC,LENGTH_SNOC] 383 \\ FULL_SIMP_TAC arith_ss [(GSYM o SIMP_RULE std_ss []) GEN_REG_LIST_def, 384 EL_SNOC,(GSYM o CONJUNCT1) EL] 385 \\ Cases_on `x < LENGTH (GEN_REG_LIST wl n)` 386 \\ Cases_on `y < LENGTH (GEN_REG_LIST wl n)` 387 \\ ASM_SIMP_TAC arith_ss [EL_SNOC] 388 \\ IMP_RES_TAC EL_GEN_REG_LIST_LT_WL 389 \\ IMP_RES_TAC MUST_BE_EQUAL 390 \\ ASM_SIMP_TAC arith_ss [EL_LENGTH_SNOC]); 391 392val RP_NOT_EQUAL_ZERO = prove( 393 `!x list. 0 < x /\ 394 x < LENGTH (GEN_REG_LIST 16 (w2n list)) ==> 395 ~(RP stm list (MASKN x list) = RP stm list (MASKN 0 list))`, 396 SIMP_TAC (arith_ss++SIZES_ss) [GSYM REGISTER_LIST_LEM,EL_GEN_REG_LIST_LT_WL, 397 EL_GEN_REG_LIST_EQUAL,IN_LDM_STM,n2w_11]); 398 399val RP_NOT_EQUAL_ZERO = save_thm("RP_NOT_EQUAL_ZERO", 400 (REWRITE_RULE [MASKN_ZERO,LENGTH_MAP,REGISTER_LIST_GEN_REG_LIST]) 401 RP_NOT_EQUAL_ZERO); 402 403(* ------------------------------------------------------------------------- *) 404 405val REGISTER_LIST_THM = store_thm("REGISTER_LIST_THM", 406 `!ic x list. ic IN {ldm; stm} /\ x < LENGTH (REGISTER_LIST list) ==> 407 (EL x (REGISTER_LIST list) = RP ic list (MASKN x list))`, 408 REPEAT STRIP_TAC 409 \\ IMP_RES_TAC ((SIMP_RULE std_ss 410 [LENGTH_MAP,REGISTER_LIST_GEN_REG_LIST] o GSYM) REGISTER_LIST_LEM) 411 \\ IMP_RES_TAC (Thm.INST_TYPE 412 [alpha |-> ``:word4``, beta |-> ``:num``] EL_MAP) 413 \\ POP_ASSUM (SPEC_THEN `w2n` ASSUME_TAC) 414 \\ ASM_SIMP_TAC std_ss [n2w_w2n]); 415 416val RP_LT_16 = store_thm("RP_LT_16", 417 `!x ic list mask. w2n (RP ic list mask) < 16`, 418 PROVE_TAC [(SIMP_RULE (std_ss++SIZES_ss) [] o 419 Thm.INST_TYPE [alpha |-> ``:4``]) w2n_lt]); 420 421val LENGTH_TL_GENLIST = prove( 422 `!n f. LENGTH (TL (GENLIST f (n + 1))) = n`, 423 METIS_TAC [LENGTH_GENLIST,LENGTH_TL, 424 DECIDE ``!n. 0 < n + 1 /\ (n + 1 - 1 = n)``]); 425 426val SPEC_FOLDL_SNOC = (GEN_ALL o GSYM o SIMP_RULE std_ss [] o 427 ISPECL [`(\(reg':reg) (rp:word4,rd:word32). REG_WRITE reg' mode rp rd)`, 428 `reg:reg`,`(r:word4,a:word32)`]) 429 FOLDL_SNOC; 430 431val PROJ_DATA_EL = store_thm("PROJ_DATA_EL", 432 `!x n i. SUC x <= n ==> 433 (PROJ_DATA (ADVANCE 1 i x) = 434 EL x (TL (GENLIST (\s. PROJ_DATA (i s)) (n + 1))))`, 435 RW_TAC arith_ss [GSYM EL,EL_GENLIST,ADVANCE_def,ADD1]); 436 437val REGISTER_LIST_LDM_THM = store_thm("REGISTER_LIST_LDM_THM", 438 `!n x list reg mode inp. 439 x <= LENGTH (REGISTER_LIST list) /\ 440 LENGTH (REGISTER_LIST list) <= n ==> 441 (LDM_LIST reg mode (FIRSTN x (FST (ADDR_MODE4 P U base list))) 442 (FIRSTN x (TL (GENLIST (\s. PROJ_DATA (inp s)) (n + 1)))) = 443 REG_WRITEN x reg mode list (ADVANCE 1 inp))`, 444 Induct_on `x` \\ REPEAT STRIP_TAC 445 >> SIMP_TAC list_ss [FIRSTN,LDM_LIST_def,REG_WRITEN_def] 446 \\ `x <= LENGTH (REGISTER_LIST list)` by DECIDE_TAC 447 \\ PAT_X_ASSUM `!n list reg mode inp. _` (IMP_RES_TAC o GSYM) 448 \\ ASM_SIMP_TAC arith_ss [REG_WRITEN_def,ADDR_MODE4_def,REG_WRITE_RP_def, 449 (REWRITE_RULE [IN_LDM_STM] o GSYM) REGISTER_LIST_THM] 450 \\ `SUC x <= n` by DECIDE_TAC 451 \\ IMP_RES_TAC PROJ_DATA_EL \\ POP_ASSUM (K ALL_TAC) 452 \\ POP_ASSUM (ISPEC_THEN `inp` SUBST1_TAC) 453 \\ `LENGTH (REGISTER_LIST list) <= 454 LENGTH (TL (GENLIST (\s. PROJ_DATA (inp s)) (n + 1)))` 455 by ASM_SIMP_TAC arith_ss [LENGTH_TL_GENLIST] 456 \\ `EL x (TL (GENLIST (\s. PROJ_DATA (inp s)) (n + 1))) = 457 EL x (FIRSTN (LENGTH (REGISTER_LIST list)) 458 (TL (GENLIST (\s. PROJ_DATA (inp s)) (n + 1))))` 459 by ASM_SIMP_TAC arith_ss [GSYM EL_FIRSTN] 460 \\ ASM_SIMP_TAC list_ss [LENGTH_TL_GENLIST,PROJ_DATA_EL, 461 GSYM listTheory.EL_ZIP,SPEC_FOLDL_SNOC,LENGTH_FIRSTN,SNOC_EL_FIRSTN, 462 LENGTH_ZIP,LDM_LIST_def,ZIP_FIRSTN_LEQ]); 463 464val FST_ADDR_MODE4 = save_thm("FST_ADDR_MODE4", 465 (GEN_ALL o SIMP_CONV std_ss [ADDR_MODE4_def]) 466 ``FST (ADDR_MODE4 P U base n)``); 467 468val SND_ADDR_MODE4 = save_thm("SND_ADDR_MODE4", 469 SIMP_CONV std_ss [ADDR_MODE4_def] ``SND (ADDR_MODE4 P U base n)``); 470 471val LENGTH_ADDR_MODE4 = save_thm("LENGTH_ADDR_MODE4", 472 (GEN_ALL o REWRITE_CONV [FST_ADDR_MODE4]) 473 ``LENGTH (FST (ADDR_MODE4 P U base n))``); 474 475val REGISTER_LIST_STM_THM = save_thm("REGISTER_LIST_STM_THM", 476 (GSYM o REWRITE_RULE [IN_LDM_STM,GSYM FST_ADDR_MODE4] o 477 SPEC `stm`) REGISTER_LIST_THM); 478 479val LENGTH_ADDRESS_LIST = 480 (GEN_ALL o REWRITE_CONV [LENGTH_GENLIST,ADDRESS_LIST_def]) 481 ``LENGTH (ADDRESS_LIST base n)``; 482 483val FST_HD_FST_ADDR_MODE4 = store_thm("FST_HD_FST_ADDR_MODE4", 484 `!P U base n. 0 < LENGTH (REGISTER_LIST n) ==> 485 (HD (FST (ADDR_MODE4 P U base n)) = RP stm n UINT_MAXw)`, 486 METIS_TAC [FST_ADDR_MODE4,(GSYM o CONJUNCT1) EL,MASKN_ZERO, 487 LENGTH_ADDRESS_LIST,REGISTER_LIST_THM,IN_LDM_STM]); 488 489(* ------------------------------------------------------------------------- *) 490 491val lift_gen_reg_list = 492 (GEN_ALL o SIMP_RULE arith_ss 493 [(GEN_ALL o SIMP_RULE (std_ss++SIZES_ss) [w2n_n2w] o 494 ISPECL [`v:word4`,`15w:word4`]) w2n_11, 495 EL_MAP,LENGTH_MAP,REGISTER_LIST_GEN_REG_LIST] o 496 ISPECL [`15`,`w2n (list:word16)`]); 497 498val GEN_REG_LIST_NOT_LAST = prove( 499 `!x n y. y < LENGTH (GEN_REG_LIST (SUC x) n) - 1 ==> 500 ~(EL y (GEN_REG_LIST (SUC x) n) = x)`, 501 RW_TAC arith_ss [LENGTH_SNOC,GEN_REG_LIST_THM,EL_SNOC] 502 >> (IMP_RES_TAC EL_GEN_REG_LIST_LT_WL \\ ASM_SIMP_TAC arith_ss []) 503 \\ `y < LENGTH (GEN_REG_LIST x n)` by DECIDE_TAC 504 \\ IMP_RES_TAC EL_GEN_REG_LIST_LT_WL 505 \\ ASM_SIMP_TAC arith_ss []); 506 507val REGISTER_LIST_NOT_LAST = lift_gen_reg_list GEN_REG_LIST_NOT_LAST; 508 509val RP_NOT_15 = store_thm("RP_NOT_15", 510 `!ic y n. ic IN {ldm; stm} /\ y < LENGTH (REGISTER_LIST n) - 1 ==> 511 ~(RP ic n (MASKN y n) = 15w)`, 512 SIMP_TAC arith_ss [REGISTER_LIST_NOT_LAST,EL_MAP,n2w_w2n, 513 (GSYM o SIMP_RULE std_ss [LENGTH_MAP,REGISTER_LIST_GEN_REG_LIST]) 514 REGISTER_LIST_LEM]); 515 516val lem = DECIDE ``!x. 0 < x ==> (x - 1 < x) /\ (x = SUC (x - 1))``; 517 518val GEN_RP_LAST = prove( 519 `!x n. 0 < LENGTH (GEN_REG_LIST (SUC x) n) ==> 520 ((EL (LENGTH (GEN_REG_LIST (SUC x) n) - 1) (GEN_REG_LIST (SUC x) n) = x) = 521 BIT x n)`, 522 RW_TAC arith_ss [LENGTH_SNOC,GEN_REG_LIST_THM,EL_SNOC,EL_LENGTH_SNOC] 523 \\ PROVE_TAC [lem,prim_recTheory.LESS_NOT_EQ,EL_GEN_REG_LIST_LT_WL]); 524 525val lift_gen_reg_list = 526 (SIMP_RULE (std_ss++SIZES_ss) [BIT_w2n] o lift_gen_reg_list); 527 528val REGISTER_LIST_LAST = lift_gen_reg_list GEN_RP_LAST; 529 530val RP_LAST_15 = store_thm("RP_LAST_15", 531 `!list. 0 < LENGTH (REGISTER_LIST list) ==> 532 ((RP ldm list (MASKN (LENGTH (REGISTER_LIST list) - 1) list) = 15w) = 533 list %% 15)`, 534 SIMP_TAC arith_ss [IN_LDM_STM,GSYM REGISTER_LIST_THM,REGISTER_LIST_LAST]); 535 536val REG_WRITEN_COMMUTES = store_thm("REG_WRITEN_COMMUTES", 537 `!n ireg reg m1 m2 i. 538 n < LENGTH (REGISTER_LIST ireg) ==> 539 (REG_WRITEN n (REG_WRITE reg m1 15w d) m2 ireg i = 540 REG_WRITE (REG_WRITEN n reg m2 ireg i) m1 15w d)`, 541 Induct \\ RW_TAC bool_ss [REG_WRITEN_def,TO_WRITE_READ6,REG_WRITE_RP_def] 542 \\ ASM_SIMP_TAC arith_ss [REG_WRITE_RP_def,RP_LT_16,RP_NOT_15,IN_LDM_STM, 543 REG_WRITE_WRITE_PC]); 544 545val LENGTH_GEN_REG_LIST_NOT_ZERO = prove( 546 `!wl ireg. BIT wl ireg ==> 0 < LENGTH (GEN_REG_LIST (SUC wl) ireg)`, 547 RW_TAC arith_ss [LENGTH_GEN_REG_LIST,SUM_def,BITV_THM,SBIT_def]); 548 549val LENGTH_REGISTER_LIST_NOT_ZERO = 550 lift_gen_reg_list LENGTH_GEN_REG_LIST_NOT_ZERO; 551 552(* --- *) 553 554val writen_pc_tac = REPEAT STRIP_TAC 555 \\ IMP_RES_TAC LENGTH_REGISTER_LIST_NOT_ZERO 556 \\ IMP_RES_TAC lem \\ POP_ASSUM SUBST1_TAC 557 \\ FULL_SIMP_TAC bool_ss [GSYM RP_LAST_15] 558 \\ ASM_SIMP_TAC arith_ss [REG_WRITEN_def,REG_WRITE_RP_def, 559 REG_WRITEN_COMMUTES,TO_WRITE_READ6,REG_WRITE_WRITE,REG_READ_WRITE]; 560 561val REG_WRITE_WRITEN_PC = store_thm("REG_WRITE_WRITEN_PC", 562 `!list reg mode i. list %% 15 ==> 563 (REG_WRITEN (LENGTH (REGISTER_LIST list)) 564 (REG_WRITE reg usr 15w d) mode list i = 565 REG_WRITEN (LENGTH (REGISTER_LIST list)) reg mode list i)`, 566 writen_pc_tac); 567 568val REG_WRITEN_WRITE_PC = store_thm("REG_WRITEN_WRITE_PC", 569 `!list reg mode i. list %% 15 ==> 570 (REG_WRITE (REG_WRITEN 571 (LENGTH (REGISTER_LIST list)) reg mode list i) usr 15w 572 (PROJ_DATA (i (LENGTH (REGISTER_LIST list) - 1))) = 573 REG_WRITEN (LENGTH (REGISTER_LIST list)) reg mode list i)`, 574 writen_pc_tac); 575 576val REG_WRITEN_WRITE_PC2 = store_thm("REG_WRITEN_WRITE_PC2", 577 `!list reg mode i. list %% 15 ==> 578 (REG_WRITE (REG_WRITEN 579 (LENGTH (REGISTER_LIST list) - 1) reg mode list i) usr 15w 580 (PROJ_DATA (i (LENGTH (REGISTER_LIST list) - 1))) = 581 REG_WRITEN (LENGTH (REGISTER_LIST list)) reg mode list i)`, 582 writen_pc_tac); 583 584val REG_READ_WRITEN_PC = store_thm("REG_READ_WRITEN_PC", 585 `!list reg mode i. list %% 15 ==> 586 (REG_READ6 (REG_WRITEN 587 (LENGTH (REGISTER_LIST list)) reg mode list i) usr 15w = 588 (PROJ_DATA (i (LENGTH (REGISTER_LIST list) - 1))))`, 589 writen_pc_tac); 590 591val REG_WRITEN_COMMUTE_PC = store_thm("REG_WRITEN_COMMUTE_PC", 592 `!list reg mode i. ~(list %% 15) /\ 0 < LENGTH (REGISTER_LIST list) ==> 593 (REG_WRITEN (LENGTH (REGISTER_LIST list)) 594 (REG_WRITE reg usr 15w d) mode list i = 595 REG_WRITE (REG_WRITEN 596 (LENGTH (REGISTER_LIST list)) reg mode list i) usr 15w d)`, 597 writen_pc_tac \\ ASM_SIMP_TAC arith_ss [REG_WRITE_WRITE_PC]); 598 599val REG_READ_WRITEN_PC2 = store_thm("REG_READ_WRITEN_PC2", 600 `!list reg mode i. x < LENGTH (REGISTER_LIST list) ==> 601 (REG_READ6 (REG_WRITEN x reg mode list i) usr 15w = 602 REG_READ6 reg usr 15w)`, 603 REPEAT STRIP_TAC \\ Induct_on `x` 604 \\ REWRITE_TAC [REG_WRITEN_def] 605 \\ STRIP_TAC \\ IMP_RES_TAC prim_recTheory.SUC_LESS 606 \\ ASM_SIMP_TAC arith_ss [IN_LDM_STM,REG_WRITE_RP_def,RP_NOT_15, 607 REG_READ_WRITE_PC]); 608 609(* ------------------------------------------------------------------------- *) 610 611val LENGTH_REGISTER_LIST = save_thm("LENGTH_REGISTER_LIST", 612 (GEN_ALL o REWRITE_RULE [LENGTH_MAP,REGISTER_LIST_GEN_REG_LIST] o 613 SPECL [`16`,`w2n (list:word16)`]) LENGTH_GEN_REG_LIST); 614 615val REGISTER_LIST_LENGTH = GSYM LENGTH_REGISTER_LIST; 616 617val PENCZ1 = prove( 618 `!list:word16 x. x < LENGTH (GEN_REG_LIST 16 (w2n list)) ==> 619 ~(list && (MASKN x list) = 0w)`, 620 REPEAT STRIP_TAC \\ IMP_RES_TAC EXISTS_SUM_BITS 621 \\ POP_ASSUM SUBST_ALL_TAC 622 \\ FULL_SIMP_TAC bool_ss [LENGTH_GEN_REG_LIST] 623 \\ IMP_RES_TAC (INST_16 SUM_LT) 624 \\ PAT_X_ASSUM `list && (MASKN (SUM p (BITV (w2n list))) list) = 0w` 625 SUBST_ALL_TAC 626 \\ PROVE_TAC [INST_16 word_0]); 627 628val PENCZ1 = REWRITE_RULE [LENGTH_GEN_REG_LIST,REGISTER_LIST_LENGTH] PENCZ1; 629 630val PENCZ2 = prove( 631 `!list. list && (MASKN (LENGTH (REGISTER_LIST list)) list) = 0w`, 632 SIMP_TAC (arith_ss++SIZES_ss) [GSYM WORD_EQ,word_bit_def,word_0, 633 LENGTH_REGISTER_LIST,MASKN_THM]); 634 635val PENCZ_THM = store_thm("PENCZ_THM", 636 `!ic. ic IN {ldm; stm} ==> 637 (!list x. x < LENGTH (REGISTER_LIST list) ==> 638 ~PENCZ ic list (MASKN x list)) /\ 639 !list. PENCZ ic list (MASKN (LENGTH (REGISTER_LIST list)) list)`, 640 RW_TAC bool_ss [IN_LDM_STM,PENCZ_def,PENCZ2,PENCZ1]); 641 642val PENCZ_THM2 = store_thm("PENCZ_THM2", 643 `!list. (list = 0w) = (LENGTH (REGISTER_LIST list) = 0)`, 644 Cases \\ SIMP_TAC bool_ss 645 [LENGTH_REGISTER_LIST,BITV_def,GSYM SUM_ZERO,BITS_COMP_THM2,w2n_n2w, 646 MOD_DIMINDEX,GSYM WORD_EQ,word_bit_n2w,BIT_def,BITS_ZERO2,dimindex_16] 647 \\ SIMP_TAC arith_ss [MIN_DEF,NOT_BITS2]); 648 649val PENCZ_THM3 = store_thm("PENCZ_THM3", 650 `!list mask. (list = 0w) /\ ic IN {ldm; stm} ==> PENCZ ic list mask`, 651 SIMP_TAC std_ss [PENCZ_def,WORD_AND_CLAUSES,IN_LDM_STM]); 652 653(* ------------------------------------------------------------------------- *) 654 655val ADD_THREE_ONE = prove( 656 `!a. 3w + a + 1w = a + 4w`, 657 SIMP_TAC arith_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,word_add_n2w]); 658 659val NOT_ADD = prove( 660 `!a b. ~a + b = b - (a + 1w)`, 661 REWRITE_TAC [WORD_NOT,GSYM WORD_ADD_SUB_SYM,WORD_SUB_PLUS, 662 WORD_LCANCEL_SUB,WORD_SUB]); 663 664val NOT_ADD_1 = prove( 665 `!a b. ~a + b + 1w = b - a`, 666 REWRITE_TAC [WORD_NOT,GSYM WORD_ADD_SUB_SYM,WORD_ADD_SUB,WORD_SUB]); 667 668val FIRST_ADDRESS = store_thm("FIRST_ADDRESS", 669 `!ireg ic base c borrow2 mul. 670 1 <= LENGTH (REGISTER_LIST ((15 >< 0) ireg)) /\ ic IN {ldm; stm} ==> 671 (FIRST_ADDRESS (ireg %% 24) (ireg %% 23) base 672 (WB_ADDRESS (ireg %% 23) base (LENGTH (REGISTER_LIST ((15 >< 0) ireg)))) = 673 SND (ALU6 ic t3 ireg borrow2 mul F 674 (OFFSET ic t3 ireg ((15 >< 0) ireg)) base c))`, 675 RW_TAC std_ss [FIRST_ADDRESS_def,WB_ADDRESS_def,ALU6_def,OFFSET_def, 676 ALUOUT_ADD_CARRY,ALUOUT_ADD,ALUOUT_ALU_logic,UP_DOWN_def, 677 REGISTER_LIST_LENGTH,IN_LDM_STM,ADD_THREE_ONE,NOT_ADD,NOT_ADD_1, 678 word_mul_n2w,WORD_EQ_ADD_LCANCEL,WORD_ADD_SUB_SYM,WORD_SUB_SUB] 679 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,WORD_SUB_ADD, 680 EVAL ``3w + 1w:word32``]); 681 682val WB_ADDRESS = store_thm("WB_ADDRESS", 683 `!ireg ic base c borrow2 mul. ic IN {ldm; stm} ==> 684 (WB_ADDRESS (ireg %% 23) base (LENGTH (REGISTER_LIST ((15 >< 0) ireg))) = 685 SND (ALU6 ic t4 ireg borrow2 mul F 686 (OFFSET ic t4 ireg ((15 >< 0) ireg)) base c))`, 687 RW_TAC std_ss [FIRST_ADDRESS_def,WB_ADDRESS_def,ALU6_def,OFFSET_def, 688 ALUOUT_ADD_CARRY,ALUOUT_ADD,ALUOUT_ALU_logic,UP_DOWN_def, 689 REGISTER_LIST_LENGTH,IN_LDM_STM,ADD_THREE_ONE,NOT_ADD,NOT_ADD_1, 690 word_mul_n2w,WORD_EQ_ADD_LCANCEL,WORD_ADD_SUB_SYM,WORD_SUB_SUB, 691 PENCZ_THM2,WORD_ADD_0,WORD_SUB_RZERO] 692 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,WORD_EQ_ADD_LCANCEL] 693 \\ SIMP_TAC std_ss [WORD_ADD_ASSOC,EVAL ``1w + 3w:word32``,WORD_SUB_ADD2]); 694 695val WB_ADDRESS_ZERO = save_thm("WB_ADDRESS_ZERO", 696 (GEN_ALL o 697 SIMP_RULE bool_ss [(GEN_ALL o snd o EQ_IMP_RULE o SPEC_ALL) PENCZ_THM2] o 698 DISCH `LENGTH (REGISTER_LIST ((15 >< 0) ireg)) = 0` o 699 GSYM o SPEC_ALL) WB_ADDRESS); 700 701(* ------------------------------------------------------------------------- *) 702 703val MASKN_SUC = store_thm("MASKN_SUC", 704 `!n ic list. ((ic = ldm) \/ (ic = stm)) ==> 705 (CLEARBIT (w2n (RP ic list (MASKN n list))) (MASKN n list) = 706 MASKN (SUC n) list)`, 707 SIMP_TAC (arith_ss++SIZES_ss) [MASKN_SUC,MASK_BIT_def,RP_def,w2n_n2w]); 708 709val LDM_LIST_EMPTY = store_thm("LDM_LIST_EMPTY", 710 `!reg mode. LDM_LIST reg mode [] [] = reg`, 711 SIMP_TAC list_ss [LDM_LIST_def]); 712 713val WORD_BITS_150_ZERO = store_thm("WORD_BITS_150_ZERO", 714 `(!i:word32. (((15 >< 0) i = 0w:word16) ==> ~(i %% 15))) /\ 715 !i:word32. (i %% 15 = ((15 >< 0) i):word16 %% 15)`, 716 STRIP_TAC \\ REWRITE_TAC [GSYM WORD_EQ] 717 \\ RW_TAC (fcp_ss++ARITH_ss++SIZES_ss) [word_bit_def,word_0, 718 word_extract_def,word_bits_def,w2w]); 719 720(* ------------------------------------------------------------------------- *) 721 722val IS_ABORT_ZERO = prove( 723 `(?s. s < 1 /\ IS_ABORT i (s + 1)) = IS_ABORT i 1`, 724 EQ_TAC \\ REPEAT STRIP_TAC 725 >> (`s = 0` by DECIDE_TAC \\ FULL_SIMP_TAC arith_ss []) 726 \\ EXISTS_TAC `0` \\ ASM_SIMP_TAC arith_ss []); 727 728val LEAST_ABORT_ZERO = prove( 729 `!w i. 0 < w /\ IS_ABORT i 1 ==> 730 ((LEAST s. s < w /\ IS_ABORT i (s + 1)) = 0)`, 731 RW_TAC arith_ss [LEAST_DEF,Once WHILE]); 732 733val LEAST_ABORT_ZERO_ISA = store_thm("LEAST_ABORT_ZERO_ISA", 734 `!i. IS_ABORT i 1 ==> ((LEAST s. IS_ABORT i (s + 1)) = 0)`, 735 RW_TAC arith_ss [LEAST_DEF,Ntimes WHILE 2]); 736 737val lem = prove( 738 `(!m. m < n ==> ~(m < w /\ IS_ABORT i (m + 1))) /\ 739 n < w /\ IS_ABORT i (n + 1) ==> 740 (n = LEAST s. IS_ABORT i (s + 1))`, 741 RW_TAC std_ss [] 742 \\ `!m. m < n ==> m < w` by METIS_TAC [LESS_TRANS] 743 \\ FULL_SIMP_TAC std_ss [(BETA_RULE o 744 INST [`P` |-> `\s. IS_ABORT i (s + 1)`]) LEAST_THM]); 745 746val LEAST_ABORT_ISA = store_thm("LEAST_ABORT_ISA", 747 `(?s. s < w /\ IS_ABORT i (s + 1)) ==> 748 ((LEAST s. s < w /\ IS_ABORT i (s + 1)) = (LEAST s. IS_ABORT i (s + 1)))`, 749 RW_TAC std_ss [] 750 \\ IMP_RES_TAC ((GEN_ALL o BETA_RULE o 751 SPECL [`\l. l = LEAST s. IS_ABORT i (s + 1)`, 752 `\s. s < w /\ IS_ABORT i (s + 1)`]) LEAST_ELIM) 753 \\ METIS_TAC [lem]); 754 755val LEAST_ABORT_LT2 = store_thm("LEAST_ABORT_LT2", 756 `(?s. s < w /\ IS_ABORT i (s + 1)) ==> (LEAST s. IS_ABORT i (s + 1)) < w`, 757 REPEAT STRIP_TAC \\ IMP_RES_TAC (GSYM LEAST_ABORT_ISA) 758 \\ POP_ASSUM SUBST1_TAC 759 \\ METIS_TAC [lem,(GEN_ALL o SIMP_RULE bool_ss [] o 760 BETA_RULE o SPECL [`\l. l < w`, 761 `\s. s < w /\ IS_ABORT i (s + 1)`]) LEAST_ELIM]); 762 763(* ------------------------------------------------------------------------- *) 764 765val NEW_ABORT_SUC = prove( 766 `!x. (?s. s < x + 1 /\ IS_ABORT i (s + 1)) \/ IS_ABORT i (x + 2) = 767 ?s. s < x + 2 /\ IS_ABORT i (s + 1)`, 768 STRIP_TAC \\ EQ_TAC \\ RW_TAC arith_ss [] 769 >> METIS_TAC [DECIDE ``!s x. s < x + 1 ==> s < x + 2``] 770 >> (EXISTS_TAC `x + 1` \\ ASM_SIMP_TAC arith_ss []) 771 \\ Cases_on `s = x + 1` >> FULL_SIMP_TAC arith_ss [] 772 \\ DISJ1_TAC \\ EXISTS_TAC `s` 773 \\ ASM_SIMP_TAC arith_ss []); 774 775val lem = prove( 776 `!w x i. SUC x <= w - 1 /\ (!s. s < x + 1 ==> 777 ~IS_ABORT i (s + 1)) /\ s < x + 2 /\ IS_ABORT i (s + 1) ==> 778 (!n. (!m. m < n ==> m < w ==> ~IS_ABORT i (m + 1)) /\ 779 n < w /\ IS_ABORT i (n + 1) ==> (n = x + 1))`, 780 RW_TAC std_ss [] \\ Cases_on `n < x + 1` 781 >> PAT_X_ASSUM `!s. s < _ ==> ~IS_ABORT i (s + 1)` 782 (SPEC_THEN `n` IMP_RES_TAC) 783 \\ Tactical.REVERSE (Cases_on `x + 1 < n`) >> DECIDE_TAC 784 \\ `s < n /\ s < w` by DECIDE_TAC 785 \\ PAT_X_ASSUM `!m. m < n ==> m < w ==> ~IS_ABORT i (m + 1)` 786 (SPEC_THEN `s` IMP_RES_TAC)); 787 788val NEW_LEAST_ABORT_SUC = prove( 789 `!x w i s. SUC x <= w - 1 /\ 790 (!s. s < x + 1 ==> ~IS_ABORT i (s + 1)) /\ 791 s < x + 2 /\ IS_ABORT i (s + 1) ==> 792 ((LEAST s. s < w /\ IS_ABORT i (s + 1)) = x + 1)`, 793 REPEAT STRIP_TAC 794 \\ IMP_RES_TAC lem 795 \\ `s < w` by DECIDE_TAC 796 \\ IMP_RES_TAC ((GEN_ALL o 797 REWRITE_RULE [DECIDE ``!a b c. a /\ b ==> c = (a ==> b ==> c)``, 798 DECIDE ``!a b. ~(a /\ b) = (a ==> ~b)``] o 799 BETA_RULE o SPECL [`\l. l = x + 1`,`\s. s < w /\ IS_ABORT i (s + 1)`]) 800 LEAST_ELIM)); 801 802val NEW_LEAST_ABORT_ZERO = prove( 803 `!w i. 0 < w /\ (?s. s < 1 /\ IS_ABORT i (s + 1)) ==> 804 ((LEAST s. s < w /\ IS_ABORT i (s + 1)) = 0)`, 805 REPEAT STRIP_TAC \\ `s = 0 ` by DECIDE_TAC 806 \\ FULL_SIMP_TAC arith_ss [LEAST_DEF,Once WHILE]); 807 808val lem = prove( 809 `!w x i. 1 < w /\ x < w - 1 /\ IS_ABORT i (x + 1) ==> 810 (!n. (!m. m < n ==> m < w ==> ~IS_ABORT i (m + 1)) /\ 811 n < w /\ IS_ABORT i (n + 1) ==> (n < w))`, 812 RW_TAC arith_ss []); 813 814val NEW_LEAST_ABORT_LT = prove( 815 `!x w i. 1 < w /\ x < w - 1 /\ IS_ABORT i (x + 1) ==> 816 ((LEAST s. s < w /\ IS_ABORT i (s + 1)) < w)`, 817 METIS_TAC [lem,DECIDE ``x < w - 1 ==> x < w``, 818 (GEN_ALL o REWRITE_RULE [DECIDE ``!a b. ~(a /\ b) = (a ==> ~b)``] o 819 BETA_RULE o SPECL [`\l. l < w`,`\s. s < w /\ IS_ABORT i (s + 1)`]) 820 LEAST_ELIM]); 821 822val NEW_LEAST_ABORT_LT2 = prove( 823 `!x w i. 1 < w /\ x < w - 1 /\ IS_ABORT i (x + 1) ==> 824 ((LEAST s. s < w /\ IS_ABORT i (s + 1)) - 1 < w)`, 825 REPEAT STRIP_TAC \\ IMP_RES_TAC NEW_LEAST_ABORT_LT \\ DECIDE_TAC); 826 827val lem = prove( 828 `!w x i. 1 < w /\ x < w /\ IS_ABORT i (x + 1) ==> 829 (!n. (!m. m < n ==> m < w ==> ~IS_ABORT i (m + 1)) /\ 830 n < w /\ IS_ABORT i (n + 1) ==> (n - 1 < w))`, 831 RW_TAC arith_ss []); 832 833val NEW_LEAST_ABORT_LT3 = prove( 834 `!x w i. 1 < w /\ x < w /\ IS_ABORT i (x + 1) ==> 835 ((LEAST s. s < w /\ IS_ABORT i (s + 1)) - 1 < w)`, 836 REPEAT STRIP_TAC 837 \\ IMP_RES_TAC lem 838 \\ METIS_TAC [(GEN_ALL o 839 REWRITE_RULE [DECIDE ``!a b. ~(a /\ b) = (a ==> ~b)``] o 840 BETA_RULE o SPECL [`\l. l - 1 < w`,`\s. s < w /\ IS_ABORT i (s + 1)`]) 841 LEAST_ELIM]); 842 843(* ------------------------------------------------------------------------- *) 844 845val MULT_ADD_FOUR = prove( 846 `!a x. a + n2w x * 4w + 4w = a + n2w (x + 1) * 4w`, 847 REWRITE_TAC [RIGHT_ADD_DISTRIB,GSYM WORD_ADD_ASSOC,MULT_LEFT_1, 848 word_add_n2w,word_mul_n2w]); 849 850fun SIMP_ASSUM a = (SIMP_RULE (stdi_ss++ARITH_ss) 851 [COND_PAIR,MASKN_SUC,PENCZ_THM3,IN_LDM_STM] o DISCH a); 852 853val REG_WRITEN_SUC = save_thm("REG_WRITEN_SUC", 854 (GEN_ALL o SIMP_RULE arith_ss [ADD1,ADVANCE_def] o 855 INST [`i` |-> `ADVANCE 1 i`] o SPEC_ALL o 856 REWRITE_RULE [REG_WRITE_RP_def] o GSYM o CONJUNCT2) REG_WRITEN_def); 857 858val lem = prove( 859 `!b. ~((if b then tm else tn) = t3)`, PROVE_TAC [iseq_distinct]); 860 861val NEXT_CORE_LDM_TN1 = (GEN_ALL o 862 SIMP_ASSUM `~((15 >< 0) ireg = 0w:word16)` o 863 GEN_REWRITE_RULE (RAND_CONV o DEPTH_CONV) empty_rewrites 864 [MULT_ADD_FOUR,ALUOUT_ALU_logic,LSL_ZERO,lem] o LDM_ITER_CONV) 865 ``NEXT_ARM6 (ARM6 (DP (REG_WRITEN y reg 866 (if ireg %% 22 /\ ~(ireg %% 15) then usr else 867 DECODE_MODE ((4 >< 0) (CPSR_READ psr))) ((15 >< 0) ireg) din) 868 psr (base + n2w (x + 1) * 4w) din2 alua alub dout) 869 (CTRL pipea T pipeb T ireg T ointstart F F obaselatch F ldm tn 870 T F F onfq ooonfq oniq oooniq pipeaabt pipebabt pipebabt dataabt2 871 aregn2 T T F sctrlreg psrfb oareg (MASKN (x + 2) ((15 >< 0) ireg)) 872 (RP ldm ((15 >< 0) ireg) (MASKN (x + 1) ((15 >< 0) ireg))) 873 (RP ldm ((15 >< 0) ireg) (MASKN x ((15 >< 0) ireg))) 874 mul mul2 borrow2 mshift)) (NRESET,ABORT,NFQ,NIQ,DATA,CPA,CPB)``; 875 876val LDM_PENCZ_THM = 877 (GEN_ALL o SIMP_RULE std_ss [] o 878 DISCH `LENGTH (REGISTER_LIST list) = x` o 879 SPEC `list` o CONJUNCT2 o SIMP_RULE stdi_ss [IN_LDM_STM] o 880 SPEC `ldm`) PENCZ_THM; 881 882val LDM_PENCZ_LEM = prove( 883 `!list x. SUC x <= LENGTH (REGISTER_LIST list) - 1 ==> 884 (PENCZ ldm list (MASKN (x + 2) list) = 885 (x + 1 = LENGTH (REGISTER_LIST list) - 1))`, 886 RW_TAC std_ss [GSYM ADD1] 887 \\ Cases_on `SUC x = LENGTH (REGISTER_LIST list) - 1` 888 >> (`LENGTH (REGISTER_LIST list) = x + 2` by DECIDE_TAC \\ 889 ASM_SIMP_TAC arith_ss [LDM_PENCZ_THM]) 890 \\ ASM_SIMP_TAC arith_ss [PENCZ_THM,IN_LDM_STM]); 891 892val NEXT_CORE_LDM_TN_X = store_thm("NEXT_CORE_LDM_TN_X", 893 `!x w reg ireg alub alua din dout i. 894 (w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) ==> 895 0 < w ==> 896 x <= w - 1 ==> 897 (!t. t < SUC (SUC w) ==> ~IS_RESET i t) ==> 898 ?ointstart' onfq' ooonfq' oniq' oooniq' pipeaabt' pipebabt' 899 aregn' oareg' mul' mul2' borrow2' mshift'. 900 ~(aregn' IN {0w; 1w; 2w; 5w}) /\ 901 ((aregn' = 7w) ==> ~((CPSR_READ psr) %% 6)) /\ 902 ((aregn' = 6w) ==> ~((CPSR_READ psr) %% 7)) /\ 903 (FUNPOW (SNEXT NEXT_ARM6) x <|state := ARM6 904 (DP reg psr (if w = 1 then din else base + 1w * 4w) 905 (PROJ_DATA (i 1)) alua alub dout) 906 (CTRL pipea T pipeb T ireg T ointstart F F T F ldm 907 (if w = 1 then tm else tn) (~(w = 1)) F F onfq ooonfq oniq oooniq 908 pipeaabt pipebabt pipebabt (IS_ABORT i 1) aregn2 (~(w = 1)) T F 909 sctrlreg psrfb oareg (MASKN 2 ((15 >< 0) ireg)) 910 (RP ldm ((15 >< 0) ireg) (MASKN 1 ((15 >< 0) ireg))) 911 (RP ldm ((15 >< 0) ireg) UINT_MAXw) mul mul2 borrow2 mshift); 912 inp := ADVANCE 2 i|> = 913 (let dataabt2 = ?s. (s < x + 1) /\ IS_ABORT i (s + 1) in 914 let y = if dataabt2 then LEAST s. (s < w) /\ IS_ABORT i (s + 1) else x 915 and nbs = if ireg %% 22 /\ ~(ireg %% 15) then usr 916 else DECODE_MODE ((4 >< 0) (CPSR_READ psr)) in 917 <| state := ARM6 918 (DP (REG_WRITEN y reg nbs ((15 >< 0) ireg) (ADVANCE 1 i)) 919 psr (if (x = w - 1) /\ ~(w = 1) then 920 REG_READ6 (REG_WRITEN (y - 1) reg nbs ((15 >< 0) ireg) 921 (ADVANCE 1 i)) usr 15w 922 else if w = 1 then din else base + n2w (SUC x) * 4w) 923 (PROJ_DATA (i (x + 1))) 924 (if x = 0 then alua else REG_READ6 reg nbs ((19 >< 16) ireg)) 925 (if x = 0 then alub else PROJ_DATA (i x)) 926 (if x = 0 then dout else PROJ_DATA (i x))) 927 (CTRL pipea T pipeb T ireg T ointstart' F F (x = 0) F ldm 928 (if x = w - 1 then tm else tn) (~(x = w - 1)) F F onfq' ooonfq' 929 oniq' oooniq' pipeaabt' pipebabt' pipebabt' dataabt2 930 (if x = 0 then aregn2 else 931 if ointstart' then (if dataabt2 then 4w else aregn') else 2w) 932 (~(x = w - 1)) T F sctrlreg 933 (if x = 0 then psrfb else SPSR_READ psr nbs) 934 (if x = 0 then oareg else oareg') 935 (MASKN (SUC (SUC x)) ((15 >< 0) ireg)) 936 (RP ldm ((15 >< 0) ireg) (MASKN (SUC x) ((15 >< 0) ireg))) 937 (RP ldm ((15 >< 0) ireg) (MASKN x ((15 >< 0) ireg))) 938 mul' mul2' borrow2' mshift'); inp := ADVANCE x (ADVANCE 2 i)|>))`, 939 Induct 940 >> (RW_TAC arith_ss [FUNPOW,REG_WRITEN_def,MASKN_ZERO,ADVANCE_ZERO, 941 IS_ABORT_ZERO,LEAST_ABORT_ZERO] \\ 942 FULL_SIMP_TAC arith_ss [interrupt_exists]) 943 \\ REPEAT STRIP_TAC 944 \\ `1 < w /\ x <= w - 1` by DECIDE_TAC 945 \\ PAT_X_ASSUM `!w reg ireg alub alua din dout i. X` IMP_RES_TAC 946 \\ POP_ASSUM (SPECL_THEN [`reg`,`dout`,`din`,`alub`,`alua`] 947 STRIP_ASSUME_TAC) 948 \\ FULL_SIMP_TAC arith_ss [FUNPOW_SUC] 949 \\ POP_ASSUM (K ALL_TAC) 950 \\ `~((15 >< 0) ireg = 0w:word16)` by ASM_SIMP_TAC arith_ss [PENCZ_THM2] 951 \\ `~IS_RESET i (x + 2)` by ASM_SIMP_TAC arith_ss [] 952 \\ IMP_RES_TAC NOT_RESET_EXISTS 953 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) [SNEXT,NEXT_CORE_LDM_TN1, 954 PROJ_DATA_def,state_arm6_11,dp_11,ctrl_11,ADD1,NEW_ABORT_SUC, 955 ADVANCE_def,GSYM ADVANCE_COMP,LDM_PENCZ_LEM, 956 DECIDE ``!a b. (~a \/ b) = (a ==> b)``, 957 NEW_LEAST_ABORT_ZERO,CONJUNCT1 REG_WRITEN_def] 958 \\ SIMP_TAC (bool_ss++boolSimps.CONJ_ss) [REG_WRITEN_SUC] 959 \\ ONCE_REWRITE_TAC [DECIDE ``a /\ b /\ c /\ d /\ e /\ f /\ g = 960 (a /\ b /\ c /\ g) /\ (d /\ e /\ f)``] 961 \\ CONV_TAC EXISTS_AND_CONV 962 \\ CONJ_TAC 963 << [ 964 ASM_SIMP_TAC std_ss [NEW_ABORT_SUC, 965 DECIDE ``a \/ b \/ c \/ d \/ e = (b \/ a) \/ c \/ d \/ e``] 966 \\ RW_TAC (arith_ss++SIZES_ss) [AREGN1_def,n2w_11, 967 pred_setTheory.IN_INSERT,pred_setTheory.NOT_IN_EMPTY] 968 \\ EXISTS_TAC `3w` \\ SIMP_TAC (std_ss++SIZES_ss) [n2w_11], 969 CONJ_TAC 970 << [ 971 RW_TAC std_ss [ADD1] 972 \\ FULL_SIMP_TAC arith_ss [DECIDE ``!a b. (~a \/ b) = (a ==> b)``] 973 \\ TRY (METIS_TAC [DECIDE ``!s. s < x + 1 ==> s < x + 2``, 974 NEW_LEAST_ABORT_SUC]), 975 CONJ_TAC 976 >> RW_TAC arith_ss [NEW_LEAST_ABORT_LT,NEW_LEAST_ABORT_LT2, 977 NEW_LEAST_ABORT_LT3,REG_READ_WRITEN_PC2] 978 \\ RW_TAC arith_ss [RP_NOT_15,IN_LDM_STM] \\ METIS_TAC []]]); 979 980val NEXT_CORE_LDM_TN_W1 = save_thm("NEXT_CORE_LDM_TN_W1", 981 (GEN_ALL o SIMP_RULE std_ss [] o 982 DISCH `Abbrev (w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) /\ 983 Abbrev (nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr)))` o 984 SIMP_RULE arith_ss [WORD_MULT_CLAUSES,GSYM ADVANCE_COMP,WORD_ADD_0, 985 DECIDE ``!x. 0 < x ==> (SUC (x - 1) = x)``, 986 DECIDE ``!w. 0 < w ==> (w <= 1 = (w = 1))``] o 987 INST [`w` |-> `LENGTH (REGISTER_LIST ((15 >< 0) ireg))`] o 988 SPEC_ALL o SPECL [`w - 1`,`w`]) NEXT_CORE_LDM_TN_X); 989 990(* ------------------------------------------------------------------------- *) 991 992val NEXT_CORE_STM_TN1 = (GEN_ALL o SIMP_RULE (stdi_ss++ARITH_ss) [COND_PAIR] o 993 GEN_REWRITE_RULE (RAND_CONV o DEPTH_CONV) empty_rewrites [MULT_ADD_FOUR] o 994 STM_ITER_CONV) 995 ``NEXT_ARM6 (ARM6 996 (DP reg psr (base + n2w (SUC x) * 4w) din alua alub dout) 997 (CTRL pipea T pipeb T ireg T ointstart F F obaselatch F stm tn 998 T F F onfq ooonfq oniq oooniq pipeaabt pipebabt pipebabt dataabt2 999 aregn2 T T T sctrlreg psrfb oareg 1000 (MASKN (SUC (SUC x)) ((15 >< 0) ireg)) 1001 (RP stm ((15 >< 0) ireg) (MASKN (SUC x) ((15 >< 0) ireg))) 1002 (RP stm ((15 >< 0) ireg) (MASKN x ((15 >< 0) ireg))) 1003 mul mul2 borrow2 mshift)) (NRESET,ABORT,NFQ,NIQ,DATA,CPA,CPB)``; 1004 1005val NEXT_CORE_STM_TN_X = store_thm("NEXT_CORE_STM_TN_X", 1006 `!x w y reg ireg alub alua dout i. 1007 (w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) ==> 1008 1 < w ==> 1009 x <= w - 2 ==> 1010 (!t. t < SUC w ==> ~IS_RESET i t) ==> 1011 ?ointstart' obaselatch' onfq' ooonfq' oniq' oooniq' pipeaabt' pipebabt' 1012 dataabt2' aregn' oareg' mul' mul2' borrow2' mshift'. 1013 ~(aregn' IN {0w; 1w; 2w; 5w}) /\ 1014 ((aregn' = 7w) ==> ~((CPSR_READ psr) %% 6)) /\ 1015 ((aregn' = 6w) ==> ~((CPSR_READ psr) %% 7)) /\ 1016 (FUNPOW (SNEXT NEXT_ARM6) x <|state := 1017 ARM6 (DP reg psr (base + 1w * 4w) din alua alub dout) 1018 (CTRL pipea T pipeb T ireg T ointstart F F obaselatch F stm tn 1019 T F F onfq ooonfq oniq oooniq pipeaabt pipebabt pipebabt dataabt2 1020 aregn2 T T T sctrlreg psrfb oareg (MASKN 2 ((15 >< 0) ireg)) 1021 (RP stm ((15 >< 0) (ireg)) (MASKN 1 ((15 >< 0) ireg))) 1022 (RP stm ((15 >< 0) (ireg)) UINT_MAXw) mul mul2 borrow2 mshift); 1023 inp := ADVANCE 2 i|> = 1024 (let nbs = if ireg %% 22 then usr else 1025 DECODE_MODE ((4 >< 0) (CPSR_READ psr)) in 1026 <|state := ARM6 (DP reg psr (base + n2w (SUC x) * 4w) 1027 (if x = 0 then din else ireg) alua alub 1028 (if x = 0 then dout else 1029 REG_READ6 reg nbs 1030 (RP stm ((15 >< 0) ireg) (MASKN x ((15 >< 0) ireg))))) 1031 (CTRL pipea T pipeb T ireg T ointstart' F F obaselatch' F stm tn 1032 T F F onfq' ooonfq' oniq' oooniq' pipeaabt' pipebabt' pipebabt' 1033 dataabt2' (if x = 0 then aregn2 else 1034 if ointstart' then aregn' else 2w) T T T sctrlreg 1035 (if x = 0 then psrfb else SPSR_READ psr nbs) 1036 (if x = 0 then oareg else oareg') 1037 (MASKN (SUC (SUC x)) ((15 >< 0) ireg)) 1038 (RP stm ((15 >< 0) ireg) (MASKN (SUC x) ((15 >< 0) ireg))) 1039 (RP stm ((15 >< 0) ireg) (MASKN x ((15 >< 0) ireg))) 1040 mul' mul2' borrow2' mshift'); inp := ADVANCE x (ADVANCE 2 i)|>))`, 1041 Induct 1042 >> (RW_TAC arith_ss [FUNPOW,MASKN_ZERO,GSYM ADVANCE_COMP] \\ 1043 METIS_TAC [interrupt_exists]) 1044 \\ REPEAT STRIP_TAC 1045 \\ `x <= w - 2` by DECIDE_TAC 1046 \\ PAT_X_ASSUM `!w y reg ireg alub alua dout i. X` IMP_RES_TAC 1047 \\ POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL) 1048 \\ FULL_SIMP_TAC std_ss [FUNPOW_SUC] 1049 \\ POP_ASSUM (K ALL_TAC) 1050 \\ `SUC (SUC x) < LENGTH (REGISTER_LIST ((15 >< 0) ireg))` by DECIDE_TAC 1051 \\ `~((15 >< 0) ireg = 0w:word16)` by ASM_SIMP_TAC arith_ss [PENCZ_THM2] 1052 \\ ABBREV_TAC `nbs = if ireg %% 22 then usr else 1053 DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 1054 \\ `~IS_RESET i (x + 2)` by ASM_SIMP_TAC arith_ss [] 1055 \\ IMP_RES_TAC NOT_RESET_EXISTS 1056 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) [SNEXT,NEXT_CORE_STM_TN1, 1057 GSYM ADVANCE_COMP,ADVANCE_def,IN_LDM_STM,PENCZ_THM, 1058 DECIDE ``!x. x + 3 = SUC x + 2``] 1059 \\ RW_TAC (arith_ss++SIZES_ss) [MASK_def,MASKN_SUC,ADVANCE_def,AREGN1_def, 1060 pred_setTheory.IN_INSERT,pred_setTheory.NOT_IN_EMPTY,n2w_11] 1061 \\ FULL_SIMP_TAC (arith_ss++SIZES_ss) [ADD1,n2w_11] 1062 \\ EXISTS_TAC `3w` \\ SIMP_TAC (arith_ss++SIZES_ss) [n2w_11]); 1063 1064val NEXT_CORE_STM_TN_W2 = 1065 (GEN_ALL o SIMP_RULE arith_ss [] o 1066 INST [`w` |-> `LENGTH (REGISTER_LIST ((15 >< 0) ireg))`] o 1067 SPEC_ALL o SPECL [`w - 2`,`w`]) NEXT_CORE_STM_TN_X; 1068 1069val SUC_SUC_SUB2 = 1070 DECIDE ``!x. 1 < x ==> (1 + (x - 2) + 2 = x + 1) /\ (2 + (x - 2 + 0) = x)``; 1071 1072val SUC_SUC_SUB2b = DECIDE ``!x. 1 < x ==> (SUC (SUC (x - 2)) = x)``; 1073 1074val NEXT_CORE_STM_TN_W1 = prove( 1075 `!w y reg ireg alub alua. 1076 (w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) ==> 1077 1 < w ==> 1078 (!t. t < SUC w ==> ~IS_RESET i t) ==> 1079 ?ointstart' obaselatch' onfq' ooonfq' oniq' oooniq' pipeaabt' pipebabt' 1080 dataabt2' aregn' oareg' mul' mul2' borrow2' mshift'. 1081 ~(aregn' IN {0w; 1w; 2w; 5w}) /\ 1082 ((aregn' = 7w) ==> ~((CPSR_READ psr) %% 6)) /\ 1083 ((aregn' = 6w) ==> ~((CPSR_READ psr) %% 7)) /\ 1084 (FUNPOW (SNEXT NEXT_ARM6) (w - 1) <|state := ARM6 1085 (DP reg psr (base + 1w * 4w) din alua alub dout) 1086 (CTRL pipea T pipeb T ireg T ointstart F F obaselatch F stm tn 1087 T F F onfq ooonfq oniq oooniq pipeaabt pipebabt pipebabt dataabt2 1088 aregn2 T T T sctrlreg psrfb oareg (MASKN 2 ((15 >< 0) ireg)) 1089 (RP stm ((15 >< 0) (ireg)) (MASKN 1 ((15 >< 0) ireg))) 1090 (RP stm ((15 >< 0) (ireg)) UINT_MAXw) mul mul2 borrow2 mshift); 1091 inp := ADVANCE 2 i|> = 1092 (let nbs = if ireg %% 22 then usr else 1093 DECODE_MODE ((4 >< 0) (CPSR_READ psr)) in 1094 <|state := ARM6 (DP reg psr (REG_READ6 reg usr 15w) pipeb alua alub 1095 (REG_READ6 reg nbs 1096 (RP stm ((15 >< 0) ireg) (MASKN (w - 1) ((15 >< 0) ireg))))) 1097 (CTRL pipea T pipea T pipeb T ointstart' T T obaselatch' T 1098 (if ointstart' then swi_ex else DECODE_INST pipeb) t3 1099 F F F onfq' ooonfq' oniq' oooniq' pipeaabt' pipeaabt' pipebabt' 1100 dataabt2' (if ointstart' then aregn' else 2w) T T F sctrlreg 1101 (SPSR_READ psr nbs) oareg' 1102 (MASK (if ointstart' then swi_ex else DECODE_INST pipeb) t3 ARB ARB) 1103 (RP stm ((15 >< 0) ireg) (MASKN w ((15 >< 0) ireg))) 1104 (RP stm ((15 >< 0) ireg) (MASKN (w - 1) ((15 >< 0) ireg))) 1105 mul' mul2' borrow2' mshift'); inp := ADVANCE (w + 1) i|>))`, 1106 REPEAT STRIP_TAC 1107 \\ `~((15 >< 0) ireg = 0w:word16)` by ASM_SIMP_TAC arith_ss [PENCZ_THM2] 1108 \\ PAT_X_ASSUM `w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))` SUBST_ALL_TAC 1109 \\ IMP_RES_TAC NEXT_CORE_STM_TN_W2 1110 \\ POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL) 1111 \\ ASM_SIMP_TAC std_ss [FUNPOW_SUC, 1112 DECIDE ``!x. 1 < x ==> (x - 1 = SUC (x - 2))``] 1113 \\ POP_ASSUM (K ALL_TAC) 1114 \\ `~IS_RESET i (LENGTH (REGISTER_LIST ((15 >< 0) ireg)))` 1115 by ASM_SIMP_TAC arith_ss [] 1116 \\ IMP_RES_TAC NOT_RESET_EXISTS 1117 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) [SNEXT,NEXT_CORE_STM_TN1, 1118 SUC_SUC_SUB2,GSYM ADVANCE_COMP,ADVANCE_def] 1119 \\ ASM_SIMP_TAC stdi_ss [MASK_def,PENCZ_THM,SUC_SUC_SUB2b] 1120 \\ ABBREV_TAC `nbs = if ireg %% 22 then usr else 1121 DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 1122 \\ POP_ASSUM (K ALL_TAC) 1123 \\ RW_TAC (arith_ss++SIZES_ss) [MASK_def,PENCZ_THM,ADVANCE_def,AREGN1_def, 1124 pred_setTheory.IN_INSERT,pred_setTheory.NOT_IN_EMPTY,n2w_11] 1125 \\ FULL_SIMP_TAC (arith_ss++SIZES_ss) [ADD1,n2w_11] 1126 \\ EXISTS_TAC `3w` \\ SIMP_TAC (arith_ss++SIZES_ss) [n2w_11]); 1127 1128val NEXT_CORE_STM_TN_W1 = save_thm("NEXT_CORE_STM_TN_W1", 1129 (GEN_ALL o SIMP_RULE bool_ss [] o 1130 DISCH `Abbrev (w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) /\ 1131 Abbrev (nbs = DECODE_MODE ((4 >< 0) cpsr)) /\ 1132 Abbrev (cpsr = CPSR_READ psr)` o SPEC_ALL o 1133 SIMP_RULE std_ss [WORD_ADD_0,WORD_MULT_CLAUSES]) NEXT_CORE_STM_TN_W1); 1134 1135(* ------------------------------------------------------------------------- *) 1136 1137val _ = export_theory(); 1138