1(* ========================================================================= *) 2(* FILE : correctScript.sml *) 3(* DESCRIPTION : Formal verification of the ARM6 *) 4(* *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2001 - 2005 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["my_listTheory", "io_onestepTheory", "armTheory", "coreTheory", 11 "lemmasTheory", "coprocessorTheory", "multTheory", "blockTheory", 12 "wordsLib", "iclass_compLib", "armLib", "pred_setSimps"]; 13*) 14 15open HolKernel boolLib bossLib; 16open Q arithmeticTheory rich_listTheory my_listTheory wordsLib wordsTheory; 17open onestepTheory io_onestepTheory iclass_compLib armLib; 18open armTheory coreTheory lemmasTheory coprocessorTheory; 19open multTheory blockTheory interruptsTheory; 20 21val _ = new_theory "correct"; 22 23(* ------------------------------------------------------------------------- *) 24 25val () = Feedback.set_trace "PAT_ABBREV_TAC: match var/const" 0 26 27infix \\ << >> 28 29val op \\ = op THEN; 30val op << = op THENL; 31val op >> = op THEN1; 32 33val Abbr = BasicProvers.Abbr; 34val PRED_SET_ss = pred_setSimps.PRED_SET_ss; 35 36val FST_COND_RAND = ISPEC `FST` COND_RAND; 37val SND_COND_RAND = ISPEC `SND` COND_RAND; 38 39val booli_ss = bool_ss ++ ICLASS_ss ++ rewrites [iseq_distinct]; 40val std_ss = std_ss ++ boolSimps.LET_ss; 41val arith_ss = arith_ss ++ boolSimps.LET_ss; 42val stdi_ss = armLib.stdi_ss++rewrites[FST_COND_RAND,SND_COND_RAND]; 43 44val SUC2NUM = CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV; 45 46val GENLISTn = SUC2NUM GENLIST; 47val numeral_funpow = numeralTheory.numeral_funpow; 48 49val POP_LAST_TAC = POP_ASSUM (K ALL_TAC); 50fun POP_LASTN_TAC n = NTAC n POP_LAST_TAC; 51 52val tt = set_trace "types"; 53val fvs = set_trace "goalstack fvs"; 54 55(* ------------------------------------------------------------------------- *) 56 57val IS_MEMOP2_def = Define `IS_MEMOP2 (nmrq2,nopc1,nrw,nbw,areg) = nopc1`; 58 59val arm6out_nchotomy = 60 armLib.tupleCases 61 ``(dout:word32, mrq2:bool, nopc1:bool, nrw:bool, nbw:bool, areg:word32)``; 62 63val IS_MEMOP2 = prove( 64 `IS_MEMOP = IS_MEMOP2 o SND`, 65 REWRITE_TAC [FUN_EQ_THM] 66 \\ STRIP_TAC \\ SPEC_THEN `x` STRUCT_CASES_TAC arm6out_nchotomy 67 \\ SIMP_TAC std_ss [IS_MEMOP2_def,IS_MEMOP_def]); 68 69val LET_FILTER = prove( 70 `(!P. FILTER P [] = []) /\ 71 !P h t. FILTER P (h::t) = let l = FILTER P t in (if P h then h::l else l)`, 72 SIMP_TAC (list_ss++boolSimps.LET_ss) []); 73 74(* ------------------------------------------------------------------------- *) 75 76local 77 val SIMP_SPEC_0 = SIMP_RULE list_ss [] o SPEC `0` 78in 79 val HD_SNOC = SIMP_SPEC_0 EL_SNOC 80 val HD_MAP = SIMP_SPEC_0 EL_MAP 81 val HD_APPEND = SIMP_SPEC_0 EL_APPEND1 82end; 83 84val HD_GENLIST = 85 (GEN_ALL o REWRITE_RULE [EL] o INST [`x` |-> `0`] o SPEC_ALL) EL_GENLIST; 86 87val HD_APPEND2 = prove( 88 `!n f l. HD (GENLIST f n ++ l) = if n = 0 then HD l else f 0`, 89 Cases \\ SIMP_TAC list_ss [GENLIST,SNOC,HD_APPEND] 90 \\ Cases_on `n'` 91 \\ SIMP_TAC list_ss [LENGTH_SNOC,LENGTH_GENLIST,HD_SNOC, 92 HD_APPEND,HD_GENLIST] \\ SIMP_TAC list_ss [GENLIST,SNOC]); 93 94val FILTER_SND = prove( 95 `!P a h b. ~NULL a ==> 96 (FILTER (P o SND) (ZIP (a,h::b)) = 97 let t = FILTER (P o SND) (ZIP (TL a,b)) in 98 if P h then (HD a,h)::t else t)`, 99 Cases_on `a` \\ RW_TAC (list_ss++boolSimps.LET_ss) []); 100 101val CONS_SNOC = prove( 102 `!l a b. a::(SNOC b l) = SNOC b (a::l)`, 103 Cases \\ SIMP_TAC list_ss [SNOC]); 104 105val GENLIST_CONS = prove( 106 `!n f. GENLIST (\t. f t) (SUC n) = f 0::(GENLIST (\t. f (SUC t)) n)`, 107 Induct \\ SIMP_TAC list_ss [GENLIST,SNOC] 108 \\ REWRITE_TAC [CONS_SNOC] 109 \\ POP_ASSUM (fn th => SIMP_TAC bool_ss [GSYM th,GENLIST])); 110 111val MOVE_DOUT_INV = 112 (GEN_ALL o SIMP_RULE std_ss [] o DISCH `~NULL l` o GSYM o SPEC_ALL) 113 MOVE_DOUT_def; 114 115val NULL_GENLIST = prove(`!n f. NULL (GENLIST f n) = (n = 0)`, 116 Cases \\ SIMP_TAC list_ss [GENLIST,NULL_SNOC]); 117 118val NULL_MAP = prove(`!l f. NULL (MAP f l) = NULL l`, 119 Cases \\ SIMP_TAC list_ss []); 120 121val NULL_APPEND_RIGHT = prove(`!a b. ~NULL b ==> ~NULL (a ++ b)`, 122 RW_TAC list_ss [NULL_EQ_NIL]); 123 124val NULL_APPEND_LEFT = prove(`!a b. ~NULL a ==> ~NULL (a ++ b)`, 125 RW_TAC list_ss [NULL_EQ_NIL]); 126 127val LENGTH_NULL = (GSYM o REWRITE_RULE [GSYM NULL_EQ_NIL]) LENGTH_NIL; 128 129val LENGTH_NOT_NULL = prove(`0 < LENGTH l = ~NULL l`, 130 SIMP_TAC arith_ss [LENGTH_NULL]); 131 132val FILTER_MEMOP_ONE = (GEN_ALL o 133 SIMP_RULE list_ss [GSYM IS_MEMOP2,MOVE_DOUT_INV,TL_SNOC,NULL_MAP, 134 HD_SNOC,LENGTH_NOT_NULL,HD_MAP] o 135 DISCH `~NULL t` o 136 SIMP_CONV list_ss [MOVE_DOUT_def,IS_MEMOP2,FILTER_SND,NULL_SNOC]) 137 ``FILTER IS_MEMOP (MOVE_DOUT x (h::t))``; 138 139val FILTER_MEMOP_SINGLETON = 140 (SIMP_CONV list_ss [MOVE_DOUT_def,IS_MEMOP2,FILTER_SND,NULL_SNOC,SNOC]) 141 ``FILTER IS_MEMOP (MOVE_DOUT x [h])``; 142 143val LENGTH_MAPS = prove( 144 `!l x f g. ~(l = []) ==> (LENGTH (SNOC x (TL (MAP g l))) = LENGTH (MAP f l))`, 145 Induct \\ ASM_SIMP_TAC list_ss [SNOC,rich_listTheory.LENGTH_SNOC]); 146 147val LENGTH_MOVE_DOUT = prove( 148 `!l x. LENGTH (MOVE_DOUT x l) = LENGTH l`, 149 RW_TAC list_ss [MOVE_DOUT_def,LENGTH_ZIP,LENGTH_MAPS,NULL_EQ_NIL,LENGTH_SNOC, 150 REWRITE_RULE [LENGTH_NOT_NULL,NULL_EQ_NIL] LENGTH_TL] 151 \\ FULL_SIMP_TAC arith_ss [GSYM NULL_EQ_NIL,GSYM LENGTH_NOT_NULL]); 152 153val FILTER_MOVE_DOUT = prove( 154 `!l x. (FILTER IS_MEMOP (MOVE_DOUT x l) = []) = (FILTER IS_MEMOP l = [])`, 155 Induct >> SIMP_TAC list_ss [MOVE_DOUT_def] 156 \\ RW_TAC (list_ss++boolSimps.LET_ss) 157 [TL_SNOC,NULL_EQ_NIL,MOVE_DOUT_def,NULL_SNOC,FILTER_SND,IS_MEMOP2] 158 \\ FULL_SIMP_TAC std_ss [MOVE_DOUT_def,NULL_EQ_NIL,IS_MEMOP2]); 159 160val IS_MEM_MOVE_DOUT = prove( 161 `!l n x. n < LENGTH l ==> 162 (IS_MEMOP (EL n (MOVE_DOUT x l)) = IS_MEMOP (EL n l))`, 163 RW_TAC list_ss [IS_MEMOP2,MOVE_DOUT_def,NULL_EQ_NIL] 164 \\ METIS_TAC [listTheory.EL_ZIP,LENGTH_MAPS,LENGTH_MAP, 165 EL_MAP,pairTheory.SND]); 166 167val FILTER_MEMOP_ALL = prove( 168 `!f d x. (!t. t < d ==> ~IS_MEMOP (f t)) ==> 169 (FILTER IS_MEMOP (MOVE_DOUT x (GENLIST (\t. f t) d)) = [])`, 170 METIS_TAC [FILTER_ALL,IS_MEM_MOVE_DOUT,LENGTH_GENLIST, 171 LENGTH_MOVE_DOUT,EL_GENLIST]); 172 173val FILTER_MEMOP_NONE = prove( 174 `!f d x. (!t. t < d ==> IS_MEMOP (f t)) ==> 175 (FILTER IS_MEMOP (MOVE_DOUT x (GENLIST (\t. f t) d)) = 176 MOVE_DOUT x (GENLIST (\t. f t) d))`, 177 METIS_TAC [FILTER_NONE,IS_MEM_MOVE_DOUT,LENGTH_GENLIST, 178 LENGTH_MOVE_DOUT,EL_GENLIST]); 179 180val TL_EQ_BUTFIRSTN_1 = prove( 181 `!l. ~(l = []) ==> (BUTFIRSTN 1 l = TL l)`, 182 Cases \\ SIMP_TAC list_ss [SUC2NUM BUTFIRSTN]); 183 184val NOT_NIL_GTEQ_1 = 185 (REWRITE_RULE [DECIDE ``!n. ~(n = 0) = (1 <= n)``] o 186 ONCE_REWRITE_RULE [DECIDE ``!a:bool b. (a = b) = (~a = ~b)``]) LENGTH_NIL; 187 188val TL_APPEND = 189 (SIMP_RULE std_ss [REWRITE_RULE [NULL_EQ_NIL] NULL_APPEND_LEFT, 190 NOT_NIL_GTEQ_1,TL_EQ_BUTFIRSTN_1] o 191 SPEC `1`) BUTFIRSTN_APPEND1; 192 193val LENGTH_MAPS2 = prove( 194 `!l x y f g. LENGTH (SNOC x (MAP f l)) = LENGTH (y::MAP g l)`, 195 SIMP_TAC bool_ss [LENGTH_SNOC,LENGTH_MAP,LENGTH]); 196 197val MOVE_DOUT_APPEND = prove( 198 `!b a x. ~NULL b ==> 199 (MOVE_DOUT x (a ++ b) = MOVE_DOUT (FST (HD b)) a ++ MOVE_DOUT x b)`, 200 Induct \\ RW_TAC list_ss [MOVE_DOUT_def,NULL_EQ_NIL,ZIP_APPEND, 201 LENGTH_MAPS,LENGTH_MAPS2] 202 \\ SIMP_TAC list_ss [SNOC_APPEND] 203 \\ ONCE_REWRITE_TAC [CONS_APPEND] 204 \\ SIMP_TAC list_ss [] 205 \\ METIS_TAC [APPEND_ASSOC,TL_APPEND,REWRITE_RULE [NULL_EQ_NIL] NULL_MAP]); 206 207val MAP_CONG2 = prove( 208 `!a b f g. (LENGTH a = LENGTH b) /\ 209 (!n. n < LENGTH a ==> (f (EL n a) = g (EL n b))) ==> 210 (MAP f a = MAP g b)`, 211 METIS_TAC [LIST_EQ,EL_MAP,LENGTH_MAP]); 212 213val LENGTH_MAPS3 = prove( 214 `!l x f g. ~NULL l ==> (LENGTH (SNOC x (TL l)) = LENGTH l)`, 215 Cases THEN simp[]); 216 217val MAP_LDM_MEMOP = prove( 218 `!y n. MAP MEMOP (MOVE_DOUT y (GENLIST (\t. (f t,b1,b2,F,b3,g t)) n)) = 219 GENLIST (\t. MemRead (g t)) n`, 220 Induct_on `n` >> SIMP_TAC list_ss [GENLIST,MOVE_DOUT_def] 221 \\ RW_TAC list_ss [GENLIST,MOVE_DOUT_def,NULL_SNOC,MAP_SNOC,MAP_GENLIST, 222 TL_SNOC,NULL_GENLIST,MEMOP_def,ZIP_SNOC,LENGTH_GENLIST,LENGTH_MAPS3] 223 \\ FULL_SIMP_TAC std_ss [MOVE_DOUT_def,MAP_GENLIST,NULL_GENLIST]); 224 225val MAP_LDM_MEMOP = GEN_ALL MAP_LDM_MEMOP; 226 227val lem = prove( 228 `!f g n x. x < n ==> 229 ((\t. MemWrite b (g t) (if t + 1 = n then f n else f (t + 1))) x = 230 (\t. MemWrite b (g t) (if t + 1 = SUC n then y else f (t + 1))) x)`, 231 RW_TAC arith_ss [ADD1]); 232 233val MAP_STM_MEMOP = prove( 234 `!y n. 235 MAP MEMOP (MOVE_DOUT y (GENLIST (\t. (f t,b1,b2,T,b3,g t)) n)) = 236 GENLIST (\t. MemWrite (~b3) (g t) (if t + 1 = n then y else f (t + 1))) n`, 237 Induct_on `n` >> SIMP_TAC list_ss [GENLIST,MOVE_DOUT_def] 238 \\ RW_TAC list_ss [GENLIST,MOVE_DOUT_def,NULL_SNOC,MAP_SNOC,MAP_GENLIST, 239 TL_SNOC,NULL_GENLIST,MEMOP_def,ZIP_SNOC,LENGTH_GENLIST,LENGTH_MAPS3] 240 \\ FULL_SIMP_TAC std_ss [MOVE_DOUT_def,MAP_GENLIST,NULL_GENLIST] 241 \\ METIS_TAC [GEN_ALL (MATCH_MP (SPEC_ALL GENLIST_FUN_EQ) 242 (SPECL [`f`,`g`,`n`] lem))]); 243 244val MAP_STM_MEMOP = GEN_ALL MAP_STM_MEMOP; 245 246(* ------------------------------------------------------------------------- *) 247 248val DUR_IC = 249 (SIMP_RULE bossLib.bool_ss [GSYM RIGHT_AND_OVER_OR,GSYM LEFT_AND_OVER_OR] o 250 SIMP_RULE (stdi_ss++PBETA_ss++boolSimps.CONJ_ss++boolSimps.DNF_ss) 251 [RWA_def,PCCHANGE_def,FST_COND_RAND,SND_COND_RAND]) DUR_IC_def; 252 253val DUR_X2 = CONJ (GSYM IMP_DISJ_THM) ((SIMP_RULE (srw_ss()++boolSimps.LET_ss) 254 [ABORTINST_def,IC_def,IFLAGS_def,DECODE_PSR_def] o 255 INST [`iregval` |-> `T`,`onewinst` |-> `T`,`ointstart` |-> `F`]) DUR_X); 256 257val arm6state_inp = ``<|state := ARM6 (DP reg psr areg din alua alub dout) 258 (CTRL pipea pipeaval pipeb pipebval ireg iregval ointstart onewinst endinst 259 obaselatch opipebll nxtic nxtis nopc1 oorst resetlatch onfq ooonfq 260 oniq oooniq pipeaabt pipebabt iregabt2 dataabt2 aregn2 mrq2 nbw nrw 261 sctrlreg psrfb oareg mask orp oorp mul mul2 borrow2 mshift); 262 inp := (inp : num -> bool # bool # bool # bool # word32 # bool # bool) |>``; 263 264val arm6state = (snd o hd o snd o TypeBase.dest_record) arm6state_inp; 265 266val INIT_ARM6 = SIMP_RULE std_ss [ABORTINST_def,NXTIC_def] INIT_ARM6_def; 267 268val INIT_INIT = prove( 269 `!x. Abbrev (x = ^arm6state_inp) /\ Abbrev (x0 = SINIT INIT_ARM6 x) ==> 270 (SINIT INIT_ARM6 x0 = x0) /\ (PROJ_IREG x0.state = ireg) /\ 271 (ABS_ARM6 x0.state = ABS_ARM6 x.state)`, 272 REPEAT STRIP_TAC 273 \\ SIMP_TAC (srw_ss()) [Abbr`x`,Abbr`x0`,SINIT_def,PROJ_IREG_def,NXTIC_def, 274 ABS_ARM6_def,INIT_ARM6,MASK_MASK,num2exception_exception2num]); 275 276val IS_ABORT_LEM = prove( 277 `!i t. IS_ABORT i t = FST (SND (i t))`, 278 NTAC 2 STRIP_TAC 279 \\ REWRITE_TAC [IS_ABORT_def] 280 \\ Cases_on_arm6inp `i (t:num)` 281 \\ SIMP_TAC std_ss [PROJ_ABORT_def]); 282 283val IS_ABORT = CONJ 284 ((GEN_ALL o fst o EQ_IMP_RULE o SPEC_ALL) IS_ABORT_LEM) 285 ((GEN_ALL o fst o EQ_IMP_RULE o SPEC_ALL o 286 ONCE_REWRITE_RULE [DECIDE ``!a b. (a = b) = (~a = ~b)``]) IS_ABORT_LEM); 287 288val SWI_LEM = SIMP_CONV (stdi_ss++SWI_EX_ss) [] ``MASK swi_ex t3 x y``; 289 290val LEM = prove( 291 `!a x y z. a \/ ~((if ~a then x else y) = z) = a \/ ~(x = z)`, 292 Cases \\ REWRITE_TAC []); 293 294val LEM = CONJ (CONJ (CONJ LEM 295 ((GEN_ALL o SIMP_RULE std_ss [] o SPEC `a \/ b`) LEM)) 296 ((GEN_ALL o SIMP_RULE std_ss [] o SPEC `a /\ ~b`) LEM)) 297 ((GEN_ALL o SIMP_RULE std_ss [] o SPEC `~a`) LEM); 298 299val LEM2 = prove( 300 `!a x y z. (a /\ ((if a then x else y) = z)) /\ c = 301 a /\ ((x = z) /\ c)`, Cases \\ REWRITE_TAC []); 302 303val finish_rws = 304 [INIT_ARM6_def,DECODE_PSR_def,NXTIC_def,MASK_MASK, 305 SWI_LEM,AREGN1_THM,AREGN1_BIJ,TO_WRITE_READ6, 306 REG_READ_WRITE,REG_READ_WRITE_PC,REG_WRITE_WRITE]; 307 308val REG_WRITE_COMMUTE_PC = (GEN_ALL o 309 SIMP_RULE std_ss [] o DISCH `~(n = 15w)` o SPEC_ALL) REG_WRITE_WRITE_PC; 310 311val WORD_NEQS = 312 LIST_CONJ [(EQF_ELIM o EVAL) ``14w = 15w:word4``, 313 (EQF_ELIM o EVAL) ``2w = 0w:word3``, 314 (EQF_ELIM o EVAL) ``2w = 7w:word3``]; 315 316val finish_rws2 = 317 [TO_WRITE_READ6,READ_TO_READ6,REG_WRITE_WRITE,REG_READ_WRITE_NEQ, 318 (GEN_ALL o REWRITE_RULE [] o INST [`n2` |-> `n1`] o 319 SPEC_ALL o CONJUNCT1) REG_READ_WRITE,CONJUNCT2 REG_READ_WRITE, 320 REG_WRITE_COMMUTE_PC,CONJUNCT1 exception_BIJ,CPSR_WRITE_READ,CPSR_READ_WRITE, 321 GSYM WORD_ADD_SUB_SYM,WORD_ADD_SUB,WORD_ADD_0,ADD4_ADD4,WORD_NEQS]; 322 323val REMOVE_STUFF = REPEAT (WEAKEN_TAC (fn th => 324 not (can (match_term ``~(x = 15w:word4)``) th) andalso 325 not (can (match_term ``~(x:word3 IN X)``) th) andalso 326 not (can (match_term ``a \/ ~(x = 15w:word4)``) th))); 327 328val FINISH_OFF = 329 REMOVE_STUFF \\ RW_TAC std_ss finish_rws 330 \\ FULL_SIMP_TAC std_ss [MASK_MASK,REG_READ_WRITE,REG_READ_WRITE_PC, 331 EVAL ``14w = 15w:word4``]; 332 333val REGVAL_lem = prove( 334 `!P a:bool ** 'a. 335 ((a = b) ==> P) ==> (P \/ ~((if P then x else a) = b))`, 336 RW_TAC std_ss []); 337 338val REGVAL_lem2 = prove( 339 `!P a:bool ** 'a. 340 (~P \/ ~((if P then 14w:word4 else b) = 15w))`, 341 RW_TAC std_ss [WORD_NEQS]); 342 343val LT_RESET_TAC = POP_ASSUM MP_TAC 344 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss++boolSimps.LIFT_COND_ss) 345 [Abbr`w`,Abbr`x`,Abbr`x0`,SINIT_def,INIT_ARM6,DUR_X2] 346 \\ ASM_SIMP_TAC stdi_ss [AC ADD_ASSOC ADD_COMM,ADD1,DUR_IC] 347 \\ PROVE_TAC []; 348 349val NOT_RESET2b = (GEN_ALL o REWRITE_RULE [] o SPECL [`x`,`T`]) NOT_RESET2; 350 351val PROJ_IF_COND = GEN_ALL(prove( 352 `PROJ_IF_FLAGS (if a then ARM reg1 psr else ARM reg2 psr) = 353 let (nzcv,i,f,m) = DECODE_PSR (CPSR_READ psr) in (i,f)`, 354 RW_TAC std_ss [PROJ_IF_FLAGS_def])); 355 356val PROJ_IF_COND2 = GEN_ALL(prove( 357 `PROJ_IF_FLAGS (if a then ARM reg (CPSR_WRITE psr 358 (SET_NZCV (NZCV d) (CPSR_READ psr))) else ARM reg2 psr) = 359 let (nzcv,i,f,m) = DECODE_PSR (CPSR_READ psr) in (i,f)`, 360 RW_TAC std_ss [PROJ_IF_FLAGS_def,NZCV_def,DECODE_IFMODE_SET_NZCV, 361 DECODE_PSR_def,CPSR_WRITE_READ])); 362 363val PROJ_IF_COND3 = GEN_ALL(prove( 364 `PROJ_IF_FLAGS ( 365 if a then 366 ARM reg psr 367 else 368 ARM reg2 (if b then CPSR_WRITE psr (SET_NZCV d (CPSR_READ psr)) 369 else psr)) = 370 let (nzcv,i,f,m) = DECODE_PSR (CPSR_READ psr) in (i,f)`, 371 RW_TAC std_ss [PROJ_IF_FLAGS_def,DECODE_IFMODE_SET_NZCV, 372 DECODE_PSR_def,CPSR_WRITE_READ])); 373 374val PROJ_IF_COND4 = GEN_ALL(prove( 375 `PROJ_IF_FLAGS ( 376 ARM reg (if a then 377 CPSR_WRITE psr 378 (if b then SPSR_READ psr m 379 else if c then SET_NZCV d (CPSR_READ psr) 380 else SET_NZCV e (CPSR_READ psr)) 381 else psr)) = 382 (if a /\ b then 383 let (nzcv,i,f,m) = DECODE_PSR (SPSR_READ psr m) in (i,f) 384 else 385 let (nzcv,i,f,m) = DECODE_PSR (CPSR_READ psr) in (i,f))`, 386 RW_TAC std_ss [PROJ_IF_FLAGS_def,DECODE_IFMODE_SET_NZCV, 387 DECODE_PSR_def,CPSR_WRITE_READ] \\ FULL_SIMP_TAC std_ss [])); 388 389val CP_NOT = prove( 390 `!ic. ic IN {cdp_und; mrc; mcr; stc; ldc} ==> 391 ~(ic = swp) /\ ~(ic = mrs_msr) /\ ~(ic = data_proc) /\ ~(ic = reg_shift) /\ 392 ~(ic = mla_mul) /\ ~(ic = ldr) /\ ~(ic = str) /\ ~(ic = ldm) /\ 393 ~(ic = stm) /\ ~(ic = br) /\ ~(ic = swi_ex) /\ ~(ic = unexec)`, 394 RW_TAC (std_ss++PRED_SET_ss) []); 395 396val CP_NOT2 = prove( 397 `!ic w x. ic IN {cdp_und; mrc} ==> 398 (ic IN {cdp_und; mrc; mcr; stc; ldc} /\ 399 ~(ic = mcr) /\ ~(ic = ldc) /\ ~(ic = stc)) /\ 400 ((if (ic = cdp_und) \/ ic IN {mcr; mrc; ldc; stc} /\ a /\ b then 401 w 402 else if ic = mrc then w + 2 else x) = 403 (if (ic = cdp_und) \/ a /\ b then 0 else 2) + w)`, 404 RW_TAC (arith_ss++PRED_SET_ss) []); 405 406val CP_NOT3 = prove( 407 `!ic w x. ic IN {cdp_und; mrc} ==> (~(ic = cdp_und) ==> (ic = mrc))`, 408 RW_TAC (arith_ss++PRED_SET_ss) []); 409 410val STC_LDC_NOT = prove( 411 `(!ic. ic IN {stc; ldc} ==> ~(ic = cdp_und) /\ ~(ic = mrc) /\ ~(ic = mcr) /\ 412 ((ic = ldc) \/ (ic = stc))) /\ 413 (!ic. ~(ic IN {stc; ldc}) ==> ~(ic = stc) /\ ~(ic = ldc))`, 414 RW_TAC (std_ss++PRED_SET_ss) []); 415 416val EXTRACT_UNDEFINED = prove( 417 `~(ic IN {0w; 1w; 2w; 5w}) ==> ~(ic IN {0w; 2w; 5w})`, 418 RW_TAC (std_ss++PRED_SET_ss) []); 419 420val SIMP_interrupt2exception5_mrs_msr = 421 (GEN_ALL o SIMP_RULE std_ss [] o 422 INST [`i'` |-> `FST (x:bool # bool)`,`f'` |-> `SND (x:bool#bool)`] o 423 DISCH `DECODE_INST ireg = mrs_msr` o SPEC_ALL) SIMP_interrupt2exception5; 424 425val DATA_PROCESSING = 426 (SIMP_RULE std_ss [COND_RATOR,SET_NZC_def] o PairRules.PBETA_RULE o 427 SIMP_RULE std_ss [ARITHMETIC_THM,TEST_OR_COMP_THM,DECODE_DATAP_def]) 428 DATA_PROCESSING_def; 429 430val word2_software = prove(`num2exception (w2n (2w:word3)) = software`, 431 EVAL_TAC \\ PROVE_TAC [num2exception_thm]); 432 433val finish_rws3 = 434 [ABS_ARM6_def,NEXT_ARM_def,state_arm_ex_case_def,EXEC_INST_def,DECODE_PSR_def, 435 STC_LDC_NOT,CP_NOT,LDC_STC_def,DECODE_LDC_STC_def,ADDR_MODE5_def,MRC_def, 436 MLA_MUL_def,DECODE_MLA_MUL_def,LDM_STM_def,DECODE_LDM_STM_def,ADDR_MODE4_def, 437 EXCEPTION_def,MRS_def,DECODE_MRS_def,MSR_def,DECODE_MSR_def, 438 DATA_PROCESSING,ADDR_MODE1_def,BRANCH_def,DECODE_BRANCH_def, 439 SWP_def,DECODE_SWP_def,LDR_STR_def,DECODE_LDR_STR_def,ADDR_MODE2_def, 440 SIMP_interrupt2exception,SIMP_interrupt2exception2,SIMP_interrupt2exception3, 441 SIMP_interrupt2exception4,SIMP_interrupt2exception5, 442 SIMP_interrupt2exception5_mrs_msr,SIMP_IS_Dabort,word2_software, 443 PROJ_IF_FLAGS_def,PROJ_IF_COND,PROJ_IF_COND2,PROJ_IF_COND3,PROJ_IF_COND4, 444 PROJ_DATA_def,CPSR_WRITE_READ, 445 NOT_RESET,NOT_RESET2,NOT_RESET2b,LSL_ZERO,EXTRACT_UNDEFINED]; 446 447fun mk_pat t1 t2 n = 448 [QUOTE (t1 ^ " = " ^ t2 ^ " " ^ 449 String.concat (List.tabulate(n - 1, (fn i => "v"^(Int.toString i)^" "))) ^ 450 "v" ^ (Int.toString (n - 1)))]; 451 452val PAT_TAC = 453 MAP_EVERY (fn n => PAT_ABBREV_TAC (mk_pat "z" n 17) \\ POP_LAST_TAC) 454 ["ointstart'","obaselatch'","onfq'","ooonfq'","oniq'","oooniq'", 455 "pipeaabt'","pipebabt'","iregabt'","dataabt'"]; 456 457(* ------------------------------------------------------------------------- *) 458 459val _ = print "*\nVerifying output: mul\n*\n"; (*============================*) 460 461val MEM_MLA_MUL = Count.apply prove( 462 `!t x. Abbrev (x = ^arm6state_inp) /\ 463 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 464 (DECODE_INST ireg = mla_mul) /\ (aregn2 = 2w) /\ 465 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 466 ~FST (DUR_X x0) ==> (!t. t < DUR_ARM6 x0 ==> 467 ~IS_MEMOP (OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t x0).state)))`, 468 REWRITE_TAC [markerTheory.Abbrev_def] \\ NTAC 2 STRIP_TAC 469 \\ ABBREV_TAC `pc = REG_READ6 reg usr 15w` 470 \\ ABBREV_TAC `cpsr = CPSR_READ psr` 471 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) cpsr)` 472 \\ ABBREV_TAC `w = MLA_MUL_DUR (REG_READ6 reg nbs ((11 >< 8) ireg))` 473 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) [DUR_X2,DUR_ARM6_def,DUR_IC_def, 474 INIT_ARM6,SINIT_def] 475 \\ STRIP_TAC 476 \\ RULE_ASSUM_TAC (ONCE_REWRITE_RULE [ADD_COMM]) 477 \\ `~IS_RESET inp 0` by ASM_SIMP_TAC arith_ss [] 478 \\ IMP_RES_TAC NOT_RESET_EXISTS 479 \\ STRIP_TAC 480 \\ Cases_on `t` 481 >> SIMP_TAC (std_ss++STATE_INP_ss) [FUNPOW,OUT_ARM6_def,IS_MEMOP_def] 482 \\ STRIP_TAC 483 \\ POP_ASSUM (fn th => ASSUME_TAC 484 (MATCH_MP (DECIDE ``!a b. SUC a < 1 + b ==> a <= b``) th)) 485 \\ ASM_SIMP_TAC bool_ss [SNEXT,FUNPOW] 486 \\ MLA_MUL_TAC 487 \\ ASM_SIMP_TAC (stdi_ss++ARITH_ss++PBETA_ss) [MULT_ALU6_ZERO,LSL_ZERO, 488 w2w_0,WORD_MULT_CLAUSES,WORD_ADD_0,REGVAL_lem] 489 \\ REWRITE_TAC [IF_NEG,DECIDE ``~a /\ ~b = ~(a \/ b)``] 490 \\ SIMP_TAC std_ss [] 491 \\ RES_MP_TAC [`i` |-> `inp`] MLA_MUL_INVARIANT 492 \\ POP_ASSUM (STRIP_ASSUME_TAC o 493 (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV (SKOLEM_CONV))))) 494 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss) [OUT_ARM6_def,IS_MEMOP_def]); 495 496val _ = print "*\nVerifying time-consistency and correctess: mul\n*\n"; (* * *) 497 498val MLA_MUL = Count.apply prove( 499 `!x. Abbrev (x = ^arm6state_inp) /\ inp IN STRM_ARM6 /\ 500 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 501 (DECODE_INST ireg = mla_mul) /\ (aregn2 = 2w) /\ 502 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 503 ~FST (DUR_X x0) ==> 504 (let s = (FUNPOW (SNEXT NEXT_ARM6) (DUR_ARM6 x0) x0).state in 505 (INIT_ARM6 s = s) /\ 506 (STATE_ARM 1 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 507 ABS_ARM6 s))`, 508 NTAC 2 STRIP_TAC \\ FULL_SIMP_TAC stdi_ss [DUR_ARM6_def] 509 \\ ABBREV_TAC `pc = REG_READ6 reg usr 15w` 510 \\ ABBREV_TAC `cpsr = CPSR_READ psr` 511 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) cpsr)` 512 \\ ABBREV_TAC `w = MLA_MUL_DUR (REG_READ6 reg nbs ((11 >< 8) ireg))` 513 \\ sg `(x.inp = inp) /\ (x.state = ^arm6state) /\ 514 (<|state := x0.state; inp := inp|> = x0)` 515 THENL [ 516 SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,Abbr`x0`,SINIT_def], 517 ALL_TAC 518 ] 519 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++SIZES_ss) [num2exception_thm, 520 SUC2NUM STATE_ARM_def,ABS_ARM6_def,SMPL_ARM6_def,PACK_def,IMM_LEN_def, 521 SUC2NUM IMM_ARM6_def,MAP_STRM_def,COMBINE_def,SMPL_EXC_ARM6_def, 522 SMPL_DATA_ARM6_def,IFLAGS_def,STATE_ARM6_COR,FUNPOW,ADVANCE_ZERO, 523 DECODE_PSR_def] 524 \\ POP_LASTN_TAC 3 525 \\ STRIP_TAC 526 \\ `(!t. t < w + 1 ==> ~IS_RESET inp t) /\ (SND (DUR_X x0) = SUC w)` 527 by LT_RESET_TAC 528 \\ ASM_SIMP_TAC std_ss [DUR_ARM6_def,FUNPOW] 529 \\ ABBREV_TAC `s = SNEXT NEXT_ARM6 x0` \\ POP_ASSUM MP_TAC 530 \\ `~IS_RESET inp 0` by ASM_SIMP_TAC arith_ss [] 531 \\ IMP_RES_TAC NOT_RESET_EXISTS 532 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) 533 [Abbr`x0`,Abbr`x`,SNEXT,SINIT_def,INIT_ARM6_def] 534 \\ MLA_MUL_TAC 535 \\ ASM_SIMP_TAC (arith_ss++ICLASS_ss++PBETA_ss) 536 [FST_COND_RAND,SND_COND_RAND,IF_NEG,LSL_ZERO,MULT_ALU6_ZERO,REGVAL_lem, 537 TO_WRITE_READ6,w2w_0, WORD_MULT_CLAUSES,WORD_ADD_0] 538 \\ REWRITE_TAC [GSYM DE_MORGAN_THM,IF_NEG] 539 \\ STRIP_TAC \\ UNABBREV_TAC `s` 540 \\ PAT_ABBREV_TAC `s = FUNPOW (SNEXT NEXT_ARM6) w q` 541 \\ POP_ASSUM MP_TAC 542 \\ RES_MP_TAC [`i` |-> `inp`] MLA_MUL_TN 543 \\ POP_ASSUM (STRIP_ASSUME_TAC o 544 (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV (SKOLEM_CONV))))) 545 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) [] 546 \\ POP_ASSUM (ASSUME_TAC o GEN_ALL o 547 (MATCH_MP (DECIDE ``a /\ b /\ c /\ d ==> a /\ b /\ c``)) o SPEC_ALL) 548 \\ STRIP_TAC \\ UNABBREV_TAC `s` \\ CONJ_TAC 549 << [ 550 RULE_ASSUM_TAC (SIMP_RULE (std_ss++PRED_SET_ss) []) 551 \\ RW_TAC std_ss finish_rws 552 \\ METIS_TAC [], 553 ASM_SIMP_TAC (std_ss++STATE_INP_ss) [ABS_ARM6_def] 554 \\ PAT_ABBREV_TAC (mk_pat "aregn" "aregn'" 17) 555 \\ `~(aregn IN {0w; 1w; 2w; 5w}) /\ 556 ((aregn = 7w) ==> ~(cpsr %% 6)) /\ 557 ((aregn = 6w) ==> ~(cpsr %% 7))` 558 by METIS_TAC [] 559 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) ([Abbr`cpsr`,ALU_multiply_def, 560 MLA_MUL_CARRY_def,MSHIFT_def,SET_NZC_def] @ finish_rws3) 561 \\ RW_TAC std_ss ([Abbr`pc`,WORD_ADD_0,CARRY_LEM] @ finish_rws2) 562 \\ FULL_SIMP_TAC std_ss []]); 563 564(* ------------------------------------------------------------------------- *) 565 566val ALU_ABBREV_TAC = with_flag (priming,SOME "") 567 (PAT_ABBREV_TAC `alu = ALU6 ic is xireg xborrow2 xmul xdataabt xalua xalub xc`); 568 569val PSR_ABBREV_TAC = with_flag (priming,SOME "") 570 (PAT_ABBREV_TAC `psr = xpsr:psr`); 571 572val lem = prove( 573 `!ic. ic IN {cdp_und; mrc; mcr; stc; ldc} ==> 574 ((ic = cdp_und) \/ ic IN {mcr; mrc; ldc; stc} /\ b /\ c = 575 (ic = cdp_und) \/ b /\ c)`, 576 RW_TAC (std_ss++PRED_SET_ss) []); 577 578val lem2 = prove( 579 `!ic w a x y z. ic IN {cdp_und; mrc; mcr; stc; ldc} /\ 580 ~(ic IN {stc; ldc}) ==> 581 ((if (ic = cdp_und) \/ a then (w:num) 582 else if ic = mcr then w + x 583 else if ic = mrc then w + y 584 else z) = 585 (if (ic = cdp_und) \/ a then 0 586 else if ic = mcr then x else y) + w)`, 587 RW_TAC (arith_ss++PRED_SET_ss) []); 588 589val LT_RESET_TAC = POP_ASSUM MP_TAC 590 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss++boolSimps.LIFT_COND_ss) 591 [Abbr`w`,Abbr`x`,Abbr`x0`,SINIT_def,INIT_ARM6,DUR_X2] 592 \\ ASM_SIMP_TAC std_ss [CP_NOT,CP_NOT2,STC_LDC_NOT,DUR_IC]; 593 594val lem3 = prove( 595 `(!inp w. inp IN STRM_ARM6 /\ (!t. t < 1 + w ==> ~IS_RESET inp t) ==> 596 ?ABORT NFQ NIQ DATA CPA CPB. 597 (inp w = (T,ABORT,NFQ,NIQ,DATA,CPA,CPB)) /\ (CPA ==> CPB)) /\ 598 (!inp w. inp IN STRM_ARM6 /\ (!t. t < 2 + w ==> ~IS_RESET inp t) ==> 599 (?ABORT NFQ NIQ DATA CPA CPB. 600 (inp w = (T,ABORT,NFQ,NIQ,DATA,CPA,CPB)) /\ (CPA ==> CPB)) /\ 601 (?ABORT NFQ NIQ DATA CPA CPB. 602 (inp (w + 1) = (T,ABORT,NFQ,NIQ,DATA,CPA,CPB)) /\ (CPA ==> CPB)))`, 603 RW_TAC std_ss [IN_DEF,STRM_ARM6_def,IS_RESET_def,IS_ABSENT_def,IS_BUSY_def] 604 \\ PAT_X_ASSUM `!t. PROJ_CPA (inp t) ==> PROJ_CPB (inp t)` 605 (fn th => ASSUME_TAC (SPEC `w` th) \\ ASSUME_TAC (SPEC `w + 1` th)) 606 \\ `w < 1 + w /\ w < 2 + w /\ w + 1 < 2 + w` by DECIDE_TAC \\ RES_TAC 607 \\ Cases_on_arm6inp `inp (w:num)` 608 \\ Cases_on_arm6inp `inp (w + 1)` 609 \\ FULL_SIMP_TAC std_ss [PROJ_NRESET_def,PROJ_CPA_def,PROJ_CPB_def]); 610 611val _ = print "*\nVerifying output: cdp_und, mrc\n*\n"; (*===================*) 612 613val CP_MEMOPS = Count.apply prove( 614 `!x y. Abbrev (x = ^arm6state_inp) /\ inp IN STRM_ARM6 /\ 615 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 616 (DECODE_INST ireg IN {cdp_und; mrc}) /\ (aregn2 = 2w) /\ 617 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 618 ~FST (DUR_X x0) ==> (!t. t < DUR_ARM6 x0 ==> 619 ~IS_MEMOP (OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t x0).state)))`, 620 NTAC 3 STRIP_TAC \\ FULL_SIMP_TAC stdi_ss [DUR_ARM6_def,FILTER_MOVE_DOUT] 621 \\ ABBREV_TAC `i = CPSR_READ psr %% 7` 622 \\ ABBREV_TAC `f = CPSR_READ psr %% 6` 623 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 624 \\ ABBREV_TAC `b = BUSY_WAIT (onfq,ooonfq,oniq,oooniq,f,i,pipebabt) inp` 625 \\ ABBREV_TAC `w = 1 + b` 626 \\ STRIP_TAC 627 \\ `!t. t < w ==> ~IS_RESET inp t` by (LT_RESET_TAC \\ RW_TAC arith_ss []) 628 \\ RES_MP1_TAC [] COPROC_BUSY_WAIT >> METIS_TAC [CP_NOT2] 629 \\ RES_MP1_TAC [] COPROC_BUSY_WAIT2 >> (POP_LAST_TAC \\ METIS_TAC [CP_NOT2]) 630 \\ PAT_X_ASSUM `~FST (DUR_X x0)` MP_TAC 631 \\ FULL_SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,SINIT_def,INIT_ARM6] 632 \\ UNABBREV_TAC `x0` \\ ASM_SIMP_TAC stdi_ss [DUR_X2] 633 \\ PAT_ABBREV_TAC `d = DUR_IC ic ireg rs iflags inp` \\ POP_ASSUM MP_TAC 634 \\ ASM_SIMP_TAC stdi_ss [CP_NOT,CP_NOT2,DUR_IC] 635 \\ STRIP_TAC \\ UNABBREV_TAC `d` 636 \\ COND_CASES_TAC \\ ASM_SIMP_TAC std_ss [ADD,GSYM IMP_DISJ_THM] 637 \\ NTAC 2 STRIP_TAC 638 << [ 639 PAT_X_ASSUM `!t. t < w ==> P` IMP_RES_TAC 640 \\ POP_ASSUM SUBST1_TAC 641 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss++PRED_SET_ss) 642 [OUT_ARM6_def,IS_MEMOP_def,CP_NOT2], 643 STRIP_TAC 644 \\ `t < w \/ ((t = w) \/ (t = 1 + w))` by DECIDE_TAC 645 << [ 646 PAT_X_ASSUM `!t. t < w ==> P` IMP_RES_TAC 647 \\ POP_ASSUM SUBST1_TAC 648 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss++PRED_SET_ss) 649 [OUT_ARM6_def,IS_MEMOP_def,CP_NOT2], 650 ASM_SIMP_TAC (std_ss++STATE_INP_ss++PRED_SET_ss) 651 [OUT_ARM6_def,IS_MEMOP_def,CP_NOT2], 652 IMP_RES_TAC lem3 \\ POP_LASTN_TAC 6 653 \\ ASM_SIMP_TAC (std_ss++PRED_SET_ss) [FUNPOW_COMP,CP_NOT2] 654 \\ FULL_SIMP_TAC std_ss [IS_BUSY_def,CP_NOT3] 655 \\ ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 656 [SNEXT_def,ADVANCE_def,numeral_funpow,ADD_0] 657 \\ ASM_SIMP_TAC (stdi_ss++MRC_ss++PBETA_ss) 658 [SND_COND_RAND,FST_COND_RAND,OUT_ARM6_def,IS_MEMOP_def]]]); 659 660val ELL_1_TL_GENLIST = prove( 661 `!inp w. 0 < w ==> 662 (ELL 1 (TL (GENLIST (\s. PROJ_DATA (inp s)) (2 + w))) = 663 PROJ_DATA (inp w))`, 664 RW_TAC list_ss [DECIDE ``2 + w = SUC (SUC w)``,GENLIST,TL_SNOC, 665 NULL_SNOC,SUC2NUM ELL,LAST,BUTLAST] 666 \\ METIS_TAC [LENGTH_NOT_NULL,LENGTH_GENLIST]); 667 668val ALU2_ss = rewrites 669 [GSYM ONE_COMP_THREE_ADD,LSL_ZERO,LSL_TWO, 670 ALUOUT_ALU_logic,ALUOUT_ADD,ALUOUT_SUB]; 671 672val _ = print "*\nVerifying time-consistency \ 673 \and correctness: cdp_und, mrc, mcr, stc, ldc\n*\n"; (*========*) 674 675val CP_TC = Count.apply prove( 676 `!x. Abbrev (x = ^arm6state_inp) /\ inp IN STRM_ARM6 /\ 677 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 678 (DECODE_INST ireg IN {cdp_und; mrc; mcr; stc; ldc}) /\ (aregn2 = 2w) /\ 679 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 680 ~FST (DUR_X x0) ==> 681 (let s = (FUNPOW (SNEXT NEXT_ARM6) (DUR_ARM6 x0) x0).state in 682 (INIT_ARM6 s = s) /\ 683 (STATE_ARM 1 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 684 ABS_ARM6 s))`, 685 NTAC 2 STRIP_TAC \\ FULL_SIMP_TAC stdi_ss [DUR_ARM6_def] 686 \\ ABBREV_TAC `i = CPSR_READ psr %% 7` 687 \\ ABBREV_TAC `f = CPSR_READ psr %% 6` 688 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 689 \\ ABBREV_TAC `b = BUSY_WAIT (onfq,ooonfq,oniq,oooniq,f,i,pipebabt) inp` 690 \\ `(x.inp = inp) /\ (x.state = ^arm6state) /\ 691 (<|state := x0.state; inp := inp|> = x0) /\ 692 (IFLAGS x0.state = (onfq,ooonfq,oniq,oooniq,f,i,pipebabt))` 693 by ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++STATE_INP_ss) 694 [Abbr`x`,Abbr`x0`,SINIT_def,IFLAGS_def,INIT_ARM6_def,DECODE_PSR_def] 695 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++SIZES_ss) [num2exception_thm, 696 SUC2NUM STATE_ARM_def,ABS_ARM6_def,SMPL_ARM6_def,PACK_def,IMM_LEN_def, 697 SUC2NUM IMM_ARM6_def,MAP_STRM_def,COMBINE_def,SMPL_EXC_ARM6_def, 698 SMPL_DATA_ARM6_def,STATE_ARM6_COR,FUNPOW,ADVANCE_ZERO,DECODE_PSR_def] 699 \\ POP_LASTN_TAC 3 700 \\ Cases_on `DECODE_INST ireg IN {stc; ldc} /\ ~IS_BUSY inp b` 701 << [ 702 ABBREV_TAC `w = 1 + b + LEAST n. IS_BUSY (ADVANCE b inp) n` 703 \\ STRIP_TAC 704 \\ `(!t. t < w ==> ~IS_RESET inp t) /\ (SND (DUR_X x0) = w)` 705 by (LT_RESET_TAC \\ PROVE_TAC []) 706 \\ RES_MP_TAC [] LDC_STC_THM2 707 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss) [DUR_ARM6_def] 708 \\ CONJ_TAC 709 << [ 710 FINISH_OFF \\ FULL_SIMP_TAC (std_ss++PRED_SET_ss++SIZES_ss) [n2w_11], 711 POP_LAST_TAC \\ ASM_SIMP_TAC stdi_ss finish_rws3 712 \\ RW_TAC (std_ss++SIZES_ss) 713 ([UP_DOWN_def,w2w_extract] @ finish_rws2) 714 ], 715 ABBREV_TAC `w = 1 + b` \\ STRIP_TAC 716 \\ `!t. t < w ==> ~IS_RESET inp t` 717 by (LT_RESET_TAC \\ RW_TAC arith_ss [] \\ 718 FULL_SIMP_TAC (std_ss++PRED_SET_ss) []) 719 \\ PAT_X_ASSUM `~FST (DUR_X x0)` MP_TAC 720 \\ RES_MP_TAC [] COPROC_BUSY_WAIT2 721 \\ FULL_SIMP_TAC (std_ss++STATE_INP_ss) 722 [Abbr`x`,SINIT_def,INIT_ARM6,DUR_ARM6_def] 723 \\ UNABBREV_TAC `x0` \\ ASM_SIMP_TAC stdi_ss [DUR_X2] 724 \\ PAT_ABBREV_TAC `d = DUR_IC ic ireg rs iflags inp` 725 \\ POP_ASSUM MP_TAC 726 \\ ASM_SIMP_TAC stdi_ss [CP_NOT,DUR_IC,STC_LDC_NOT,lem] 727 << [ 728 ASM_SIMP_TAC std_ss [lem2] 729 \\ STRIP_TAC \\ UNABBREV_TAC `d` 730 \\ ASM_SIMP_TAC std_ss [FUNPOW_COMP,IS_BUSY_def] 731 \\ PAT_X_ASSUM `FUNPOW z w q = r` (K ALL_TAC) 732 \\ Cases_on `(DECODE_INST ireg = cdp_und) \/ PROJ_CPB (inp b) /\ 733 CP_INTERRUPT (onfq,ooonfq,oniq,oooniq,f,i,pipebabt) inp b` 734 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss) [FUNPOW] 735 << [ 736 POP_ASSUM (fn th => ASSUME_TAC th \\ ASSUME_TAC 737 (MATCH_MP (DECIDE ``!a b c. a \/ b /\ c ==> 738 (~a /\ (~b \/ ~c) = F)``) th)) 739 \\ POP_ASSUM SUBST1_TAC 740 \\ STRIP_TAC 741 << [ 742 POP_LASTN_TAC 2 \\ FINISH_OFF \\ POP_ASSUM MP_TAC 743 \\ FULL_SIMP_TAC (std_ss++PRED_SET_ss++SIZES_ss) [n2w_11], 744 FULL_SIMP_TAC std_ss [] \\ ASM_SIMP_TAC stdi_ss finish_rws3 745 \\ RW_TAC std_ss finish_rws2 746 ], 747 STRIP_TAC 748 \\ PAT_ABBREV_TAC `s = FUNPOW fx nx 749 (xx: (state_arm6, bool # bool # bool # bool # 750 word32 # bool # bool) state_inp)` 751 \\ NTAC 2 (POP_ASSUM MP_TAC) 752 \\ POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss []) 753 \\ ASM_SIMP_TAC std_ss [] 754 \\ Cases_on `DECODE_INST ireg = mcr` 755 \\ ASM_SIMP_TAC std_ss [] 756 \\ STRIP_TAC \\ IMP_RES_TAC lem3 757 \\ POP_LASTN_TAC 4 758 << (let 759 val tac = ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 760 [SNEXT_def,ADVANCE_def,numeral_funpow,ADD_0] 761 \\ ASM_SIMP_TAC (stdi_ss++MCR_ss++MRC_ss++PBETA_ss) 762 [SND_COND_RAND,FST_COND_RAND,IF_NEG,REGVAL_lem] 763 \\ STRIP_TAC \\ UNABBREV_TAC `s` 764 \\ CONJ_TAC 765 val tac2 = ASM_SIMP_TAC (std_ss++STATE_INP_ss) 766 ([state_arm6_11,dp_11,ctrl_11] @ finish_rws) 767 \\ ASM_SIMP_TAC (std_ss++boolSimps.CONJ_ss) 768 [AC DISJ_ASSOC DISJ_COMM,MASK_MASK] 769 in [ (* MCR *) tac >> tac2 770 \\ SIMP_TAC (std_ss++STATE_INP_ss) [] 771 \\ ASM_SIMP_TAC stdi_ss finish_rws3 772 \\ RW_TAC std_ss finish_rws2, 773 (* MRC *) 774 `(DECODE_INST ireg = mrc) /\ 0 < w` 775 by FULL_SIMP_TAC (arith_ss++PRED_SET_ss) [Abbr`w`] 776 \\ tac >> (tac2 \\ FINISH_OFF) 777 \\ `~PROJ_CPB (inp b)` 778 by (IMP_RES_TAC EXISTS_BUSY_WAIT_IMP_BUSY_WAIT_DONE \\ 779 FULL_SIMP_TAC stdi_ss [BUSY_WAIT_DONE_def,IS_BUSY_def] 780 \\ METIS_TAC []) 781 \\ IMP_RES_TAC ELL_1_TL_GENLIST 782 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss++ALU_ss++ALU2_ss) 783 finish_rws3 784 \\ RW_TAC std_ss finish_rws2 785 ] end) 786 ], (* BUSY ==> INTERRUPT *) 787 `CP_INTERRUPT (onfq,ooonfq,oniq,oooniq,f,i,pipebabt) inp b` 788 by (POP_LAST_TAC \\ IMP_RES_TAC EXISTS_BUSY_WAIT_IMP_BUSY_WAIT_DONE 789 \\ METIS_TAC [BUSY_WAIT_DONE_def]) 790 \\ ASM_SIMP_TAC std_ss [] 791 \\ STRIP_TAC \\ UNABBREV_TAC `d` 792 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss) [] 793 \\ PAT_X_ASSUM `FUNPOW z w q = r` (K ALL_TAC) 794 \\ CONJ_TAC 795 << [ 796 FULL_SIMP_TAC std_ss [IS_BUSY_def] \\ FINISH_OFF 797 \\ FULL_SIMP_TAC (std_ss++PRED_SET_ss++SIZES_ss) [n2w_11], 798 ASM_SIMP_TAC stdi_ss finish_rws3 799 \\ FULL_SIMP_TAC std_ss [IS_BUSY_def]]]]); 800 801(* ------------------------------------------------------------------------- *) 802 803val RESET_THM = prove( 804 `!x i. (!t. t < SUC x ==> ~IS_RESET i t) = 805 (if x = 0 then ~IS_RESET i x 806 else (!t. t < x ==> ~IS_RESET i t) /\ ~IS_RESET i x)`, 807 REPEAT STRIP_TAC \\ EQ_TAC \\ RW_TAC arith_ss [] 808 \\ FULL_SIMP_TAC arith_ss [DECIDE ``t < 1 ==> (t = 0)``] 809 \\ Cases_on `t = x` \\ FULL_SIMP_TAC arith_ss []); 810 811(* 812val CONCAT_MSR = 813 (SIMP_RULE std_ss [WORD_SLICE_ZERO_THM,WORD_BITS_HB_0] o 814 SIMP_RULE arith_ss [WORD_SLICE_COMP_RWT,GSYM WORD_SLICE_ZERO_THM] o 815 SPECL [`a`,`a`] o CONJUNCT1) CONCAT_MSR_THM; 816*) 817 818val CPSR_WRITE_READ_COND = GEN_ALL(prove( 819 `CPSR_READ 820 (if a then 821 CPSR_WRITE psr 822 (if USER nbs then CPSR_READ psr else SPSR_READ psr nbs) 823 else 824 psr) = 825 CPSR_READ (if a then CPSR_WRITE psr (SPSR_READ psr nbs) else psr)`, 826 RW_TAC std_ss [SPSR_READ_THM2] 827)); 828 829val CPSR_WRITE_READ_COND2 = GEN_ALL(prove( 830 `(n = 7) \/ (n = 6) ==> 831 (CPSR_READ 832 (if a then 833 CPSR_WRITE psr 834 (if b then SET_NZCV c (CPSR_READ psr) else SET_NZCV d (CPSR_READ psr)) 835 else 836 psr) %% n = 837 CPSR_READ psr %% n)`, 838 RW_TAC std_ss [CPSR_WRITE_READ] \\ SIMP_TAC std_ss [DECODE_IFMODE_SET_NZCV])); 839 840val _ = print "*\nVerifying: mrs_msr, data_proc, \ 841 \reg_shift, br, swi_ex, unexec\n*\n"; (*======================*) 842 843val NON_MEMOPS = Count.apply prove( 844 `!x y. 845 Abbrev (x = ^arm6state_inp) /\ 846 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 847 (DECODE_INST ireg IN {mrs_msr; data_proc; reg_shift; br; swi_ex; unexec}) /\ 848 (aregn2 = 2w) /\ CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 849 ~FST (DUR_X x0) ==> 850 (let s = (FUNPOW (SNEXT NEXT_ARM6) (DUR_ARM6 x0) x0).state in 851 (INIT_ARM6 s = s) /\ 852 (STATE_ARM 1 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 853 ABS_ARM6 s)) /\ 854 (FILTER IS_MEMOP (MOVE_DOUT y 855 (GENLIST (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t x0).state)) 856 (DUR_ARM6 x0))) = [])`, 857 NTAC 3 STRIP_TAC 858 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 859 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++SIZES_ss) [num2exception_thm, 860 Abbr`x`,DUR_ARM6_def,FILTER_MOVE_DOUT,SUC2NUM STATE_ARM_def, 861 ABS_ARM6_def,SMPL_ARM6_def,SMPL_DATA_ARM6_def,IFLAGS_def,ADVANCE_ZERO, 862 DECODE_PSR_def,PACK_def,IMM_LEN_def,SUC2NUM IMM_ARM6_def,MAP_STRM_def, 863 COMBINE_def,SMPL_EXC_ARM6_def,STATE_ARM6_COR,FUNPOW] 864 \\ FULL_SIMP_TAC (std_ss++STATE_INP_ss++PRED_SET_ss) 865 [SINIT_def,DECODE_INST_NOT_UNEXEC,INIT_ARM6] 866 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) [Abbr`x0`,DUR_X2] 867 \\ PAT_ABBREV_TAC `d = DUR_IC ic ireg rs iflags inp` \\ POP_ASSUM MP_TAC 868 \\ ASM_SIMP_TAC stdi_ss [DUR_IC] \\ STRIP_TAC \\ UNABBREV_TAC `d` 869 \\ TRY COND_CASES_TAC \\ SIMP_TAC std_ss [SUC2NUM RESET_THM] 870 \\ STRIP_TAC \\ IMP_RES_TAC NOT_RESET_EXISTS 871 \\ ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 872 [OUT_ARM6_def,IS_MEMOP2,IS_MEMOP2_def,LET_FILTER,SNOC,GENLISTn, 873 SNEXT_def,ADVANCE_def,PROJ_DATA_def,TL,numeral_funpow] 874 \\ REPEAT (PAT_ABBREV_TAC `s = NEXT_ARM6 a b`) 875 \\ RULE_ASSUM_TAC (REWRITE_RULE [DECIDE ``~(a /\ b) = ~a \/ ~b``]) 876 \\ REPEAT (PAT_X_ASSUM `Abbrev (q = NEXT_ARM6 (ARM6 dp ctrl) input)` MP_TAC 877 \\ ASM_SIMP_TAC (booli_ss++pairSimps.PAIR_ss++MRS_MSR_ss++BR_ss++ 878 DATA_PROC_ss++REG_SHIFT_ss++SWI_EX_ss++UNEXEC_ss++PBETA_ss) 879 [SND_COND_RAND,FST_COND_RAND,REGVAL_lem2,WORD_NEQS] 880 \\ TRY ALU_ABBREV_TAC \\ TRY PSR_ABBREV_TAC 881 \\ ASM_SIMP_TAC bossLib.old_arith_ss [markerTheory.Abbrev_def,LEM] 882 \\ DISCH_THEN SUBST_ALL_TAC 883 \\ SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 884 [OUT_ARM6_def,IS_MEMOP2_def]) 885 \\ ASM_SIMP_TAC (stdi_ss++UNEXEC_ss++SWI_EX_ss) [] 886 \\ (CONJ_TAC >> FINISH_OFF 887 \\ RULE_ASSUM_TAC (SIMP_RULE (stdi_ss++PBETA_ss++ALU_ss++ALU2_ss) 888 [GSYM IMMEDIATE_THM,IMMEDIATE_THM2]) 889 \\ TRY (UNABBREV_TAC `psr1`) \\ TRY (UNABBREV_TAC `psr2`) 890 \\ FULL_SIMP_TAC (stdi_ss++STATE_INP_ss) 891 ([CPSR_WRITE_READ_COND,CPSR_WRITE_READ_COND2,PSR_WRITE_COMM, 892 DECODE_MODE_mode_num,DECODE_IFMODE_SET_IFMODE, 893 exception_distinct,state_arm_ex_11] @ finish_rws3) 894 \\ TRY (UNABBREV_TAC `alu`) \\ TRY (UNABBREV_TAC `alu1`) 895 \\ TRY (UNABBREV_TAC `alu2`) 896 \\ RW_TAC (stdi_ss++ALU2_ss) ([SET_NZC_def,SPSR_READ_WRITE,CONCAT_MSR, 897 SHIFT_IMMEDIATE_THM2,IMMEDIATE_THM2,SHIFT_REGISTER_THM2, 898 SOFTWARE_ADDRESS] @ finish_rws2) 899 \\ NTAC 2 (FULL_SIMP_TAC std_ss []) 900 \\ TRY (METIS_TAC [DATA_PROC_IMP_NOT_BIT4,REG_SHIFT_IMP_BITS]))); 901 902(* ------------------------------------------------------------------------- *) 903 904val _ = print "*\nVerifying: exception entry, unexecuted\n*\n"; (*===========*) 905 906val NON_MEMOPS_UNEXEC = Count.apply prove( 907 `!x y. Abbrev (x = ^arm6state_inp) /\ 908 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 909 ((aregn2 = 2w) ==> 910 ~CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg) ==> 911 ~FST (DUR_X x0) ==> 912 (let s = (FUNPOW (SNEXT NEXT_ARM6) (DUR_ARM6 x0) x0).state in 913 (INIT_ARM6 s = s) /\ 914 (STATE_ARM 1 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 915 ABS_ARM6 s)) /\ 916 (FILTER IS_MEMOP (MOVE_DOUT y 917 (GENLIST (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t x0).state)) 918 (DUR_ARM6 x0))) = [])`, 919 NTAC 3 STRIP_TAC 920 \\ FULL_SIMP_TAC (srw_ss()++boolSimps.LET_ss++PRED_SET_ss++SIZES_ss) 921 [num2exception_thm,Abbr`x`,Abbr`x0`,SUC2NUM STATE_ARM_def,ABS_ARM6_def, 922 SMPL_ARM6_def,SMPL_DATA_ARM6_def,IFLAGS_def,ADVANCE_ZERO, 923 DECODE_PSR_def,PACK_def,IMM_LEN_def,SUC2NUM IMM_ARM6_def,MAP_STRM_def, 924 SMPL_EXC_ARM6_def,IC_def,ABORTINST_def,NXTIC_def,DUR_X,DUR_ARM6_def, 925 DUR_IC,FILTER_MOVE_DOUT,IFLAGS_def,SINIT_def,SUC2NUM RESET_THM, 926 DECIDE ``!x y b. (x = y) ==> b = ~(x = y) \/ (x = y) /\ b``, 927 INIT_ARM6_def,num2exception_exception2num,COMBINE_def, 928 FST_COND_RAND,SND_COND_RAND,STATE_ARM6_COR,FUNPOW] 929 \\ STRIP_TAC 930 \\ ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 931 [OUT_ARM6_def,IS_MEMOP2,IS_MEMOP2_def,LET_FILTER,SNOC,GENLISTn, 932 SNEXT_def,ADVANCE_def,numeral_funpow] 933 \\ REPEAT (PAT_ABBREV_TAC `s = NEXT_ARM6 a b`) 934 \\ IMP_RES_TAC NOT_RESET_EXISTS 935 \\ REPEAT (PAT_X_ASSUM `Abbrev (q = NEXT_ARM6 (ARM6 dp ctrl) input)` MP_TAC 936 \\ ASM_SIMP_TAC (booli_ss++SWI_EX_ss++UNEXEC_ss++pairSimps.PAIR_ss++ 937 PBETA_ss) [SND_COND_RAND,FST_COND_RAND,WORD_NEQS] 938 \\ TRY ALU_ABBREV_TAC \\ TRY PSR_ABBREV_TAC \\ STRIP_TAC 939 \\ POP_ASSUM (fn th => FULL_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 940 [OUT_ARM6_def,IS_MEMOP2_def, 941 REWRITE_RULE [markerTheory.Abbrev_def] th])) 942 \\ SIMP_TAC (stdi_ss++SWI_EX_ss) [] 943 \\ (CONJ_TAC >> FINISH_OFF 944 \\ RULE_ASSUM_TAC (SIMP_RULE (stdi_ss++ALU_ss) []) 945 \\ TRY (UNABBREV_TAC `psr1` \\ UNABBREV_TAC `psr2`) 946 \\ FULL_SIMP_TAC (stdi_ss++STATE_INP_ss) 947 ([PSR_WRITE_COMM,DECODE_MODE_mode_num,num2exception_word3, 948 DECODE_IFMODE_SET_IFMODE] @ finish_rws3) 949 \\ TRY (UNABBREV_TAC `alu1` \\ UNABBREV_TAC `alu2`) 950 \\ RW_TAC (stdi_ss++ALU2_ss) ([INTERRUPT_ADDRESS] @ finish_rws2))); 951 952(* ------------------------------------------------------------------------- *) 953 954val SINIT_ARM6 = (GSYM o SIMP_CONV std_ss [SINIT_def]) ``SINIT INIT_ARM6 x``; 955 956val IS_SOME_COND = GEN_ALL(prove( 957 `IS_SOME (if b then SOME a else NONE) = b`, 958 RW_TAC (std_ss++optionSimps.OPTION_ss) [])); 959 960val _ = print "*\nVerifying: swp, ldr, str\n*\n"; (*=========================*) 961 962val BASIC_MEMOPS = Count.apply prove( 963 `!x. Abbrev (x = ^arm6state_inp) /\ 964 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 965 (DECODE_INST ireg IN {swp; ldr; str}) /\ (aregn2 = 2w) /\ 966 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 967 ~FST (DUR_X x0) ==> 968 (let s = (FUNPOW (SNEXT NEXT_ARM6) (DUR_ARM6 x0) x0).state in 969 (INIT_ARM6 s = s) /\ 970 (STATE_ARM 1 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 971 ABS_ARM6 s)) /\ 972 (OUT_ARM (ABS_ARM6 x.state) = 973 OSMPL_ARM6 x0 (GENLIST 974 (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t x0).state)) (DUR_ARM6 x0)))`, 975 NTAC 2 STRIP_TAC \\ IMP_RES_TAC INIT_INIT 976 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++SIZES_ss) [num2exception_thm, 977 Abbr`x`,DUR_ARM6_def,SUC2NUM STATE_ARM_def,ABS_ARM6_def,SMPL_ARM6_def, 978 SMPL_DATA_ARM6_def,IFLAGS_def,OSMPL_ARM6_def,ADVANCE_ZERO, 979 DECODE_PSR_def,PACK_def,IMM_LEN_def,SUC2NUM IMM_ARM6_def,MAP_STRM_def, 980 COMBINE_def,SMPL_EXC_ARM6_def,STATE_ARM6_COR,FUNPOW] 981 \\ POP_LASTN_TAC 3 982 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 983 \\ FULL_SIMP_TAC (stdi_ss++STATE_INP_ss++PRED_SET_ss) 984 [SINIT_def,DECODE_INST_NOT_UNEXEC,INIT_ARM6] 985 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) [Abbr`x0`,DUR_X2] 986 \\ PAT_ABBREV_TAC `d = DUR_IC ic ireg rs iflags inp` \\ POP_ASSUM MP_TAC 987 \\ ASM_SIMP_TAC stdi_ss [DUR_IC] \\ STRIP_TAC \\ UNABBREV_TAC `d` 988 \\ TRY COND_CASES_TAC \\ SIMP_TAC std_ss [SUC2NUM RESET_THM] 989 \\ STRIP_TAC \\ IMP_RES_TAC NOT_RESET_EXISTS 990 \\ ASM_SIMP_TAC (list_ss++STATE_INP_ss) 991 [OUT_ARM6_def,IS_MEMOP2,IS_MEMOP2_def,LET_FILTER,SNOC,GENLISTn, 992 PROJ_DATA_def,MOVE_DOUT_def,SNEXT_def,ADVANCE_def,numeral_funpow] 993 \\ REPEAT (PAT_ABBREV_TAC `s = NEXT_ARM6 a b`) 994 \\ FULL_SIMP_TAC bossLib.std_ss [] 995 \\ REPEAT (PAT_X_ASSUM `Abbrev (q = NEXT_ARM6 (ARM6 dp ctrl) input)` MP_TAC 996 \\ ASM_SIMP_TAC (booli_ss++pairSimps.PAIR_ss++SWP_ss++LDR_ss++ 997 STR_ss++ARITH_ss++UNEXEC_ss++PBETA_ss) 998 [SND_COND_RAND,FST_COND_RAND] 999 \\ TRY ALU_ABBREV_TAC 1000 \\ ASM_SIMP_TAC bossLib.old_arith_ss [markerTheory.Abbrev_def,LEM,LEM2] 1001 \\ DISCH_THEN SUBST_ALL_TAC 1002 \\ SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 1003 [OUT_ARM6_def,IS_MEMOP2_def]) 1004 \\ (CONJ_TAC 1005 << [ 1006 CONJ_TAC >> (ASM_SIMP_TAC bossLib.std_ss [LEM] \\ FINISH_OFF) 1007 \\ RULE_ASSUM_TAC (SIMP_RULE (stdi_ss++ALU_ss++ALU2_ss) []) 1008 \\ FULL_SIMP_TAC (stdi_ss++STATE_INP_ss) 1009 ([IS_SOME_COND,HD,LDR_IMP_BITS,STR_IMP_BITS] @ finish_rws3) 1010 \\ TRY (UNABBREV_TAC `alu`) \\ TRY (UNABBREV_TAC `alu1`) 1011 \\ TRY (UNABBREV_TAC `alu2`) \\ TRY (UNABBREV_TAC `alu3`) 1012 \\ RW_TAC (stdi_ss++ALU2_ss++SIZES_ss) ([UP_DOWN_def,BW_READ_def, 1013 SLICE_ROR_THM,SHIFT_IMMEDIATE_THM2,IMMEDIATE_THM2,SND_ROR, 1014 SHIFT_ALIGN,w2w_extract] @ finish_rws2) 1015 \\ NTAC 2 (FULL_SIMP_TAC std_ss finish_rws2) 1016 \\ Cases_on `(19 >< 16) ireg = 15w:word4` 1017 \\ FULL_SIMP_TAC std_ss finish_rws2, 1018 TRY (UNABBREV_TAC `alu1`) 1019 \\ ASM_SIMP_TAC (stdi_ss++listSimps.LIST_ss++ALU_ss++ALU2_ss++SIZES_ss) 1020 ([Abbr`alu`,SWP_def,LDR_STR_def,DECODE_SWP_def,DECODE_LDR_STR_def, 1021 ADDR_MODE2_def,DECODE_PSR_def,OUT_ARM_def,MEMOP_def,SNOC, 1022 LDR_IMP_BITS,STR_IMP_BITS,IF_NEG,UP_DOWN_THM,SHIFT_IMMEDIATE_THM2, 1023 num2exception_word3,w2w_extract] @ finish_rws2)]) 1024); 1025 1026(* ------------------------------------------------------------------------- *) 1027 1028val NOT_ABORT = METIS_PROVE [] 1029 ``(!s. ~(s < SUC n) \/ ~IS_ABORT i (s + 1)) ==> 1030 ~(?s. s < SUC n /\ IS_ABORT i (s + 1))``; 1031 1032val IN_LDM_STM = 1033 SIMP_CONV (std_ss++pred_setSimps.PRED_SET_ss) [] ``ic IN {ldm; stm}``; 1034 1035val MASKN_1 = (REWRITE_RULE [MASKN_ZERO] o SPEC `0`) MASKN_SUC; 1036val MASKN_2 = (SIMP_RULE arith_ss [] o SPEC `1`) MASKN_SUC; 1037 1038val LDM_PENCZ_ZERO = 1039 (GEN_ALL o REWRITE_RULE [MASKN_ZERO] o INST [`x` |-> `0`] o SPEC_ALL o 1040 CONJUNCT1 o SIMP_RULE (std_ss++PRED_SET_ss) [] o SPEC `ldm`) PENCZ_THM; 1041 1042val PENCZ_ONE = prove( 1043 `!list. 0 < LENGTH (REGISTER_LIST list) ==> 1044 (PENCZ ldm list (MASKN 1 list) = (LENGTH (REGISTER_LIST list) = 1))`, 1045 REPEAT STRIP_TAC \\ `ldm IN {ldm; stm}` by SIMP_TAC (std_ss++PRED_SET_ss) [] 1046 \\ Cases_on `LENGTH (REGISTER_LIST list) = 1` 1047 \\ ASM_SIMP_TAC arith_ss [PENCZ_THM] 1048 \\ PROVE_TAC [PENCZ_THM]); 1049 1050val NOT_T3 = prove( 1051 `!b. ~((if b then tm else tn) = t3)`, RW_TAC stdi_ss []); 1052 1053val next_7tuple = (GEN_ALL o ONCE_REWRITE_CONV [form_7tuple]) ``NEXT_ARM6 x i``; 1054 1055val LDM_INIT = 1056 (SIMP_RULE (std_ss++boolSimps.CONJ_ss++ICLASS_ss) 1057 [NOT_T3,IN_LDM_STM,PENCZ_THM3,MASKN_SUC,MASKN_1,LSL_ZERO] o 1058 SIMP_RULE (bossLib.bool_ss++LDM_ss++PBETA_ss) 1059 [IS_ABORT,SND_COND_RAND,FST_COND_RAND] o 1060 SIMP_RULE (bossLib.bool_ss++LDM_ss) [IS_ABORT,SND_COND_RAND,FST_COND_RAND] o 1061 CONV_RULE (RAND_CONV (RHS_CONV (LAND_CONV 1062 (ONCE_REWRITE_CONV [next_7tuple])))) o 1063 CONV_RULE (RAND_CONV (RHS_CONV (ONCE_REWRITE_CONV [next_7tuple]))) o 1064 SIMP_RULE stdi_ss [IC_def,ABORTINST_def,NXTIC_def,DECODE_PSR_def] o 1065 DISCH `(DECODE_INST ireg = ldm) /\ (aregn2 = 2w) /\ 1066 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg` o 1067 SIMP_CONV bossLib.bool_ss [INIT_ARM6_def]) 1068 ``NEXT_ARM6 (NEXT_ARM6 (INIT_ARM6 (ARM6 (DP reg psr areg din alua alub dout) 1069 (CTRL pipea pipeaval pipeb pipebval ireg iregval ointstart onewinst 1070 endinst obaselatch opipebll nxtic nxtis nopc1 oorst resetlatch 1071 onfq ooonfq oniq oooniq pipeaabt pipebabt iregabt2 dataabt2 aregn2 1072 mrq2 nbw nrw sctrlreg psrfb oareg mask orp oorp mul mul2 borrow2 1073 mshift))) i0) i1``; 1074 1075val LDM_INIT2 = prove( 1076 `!x. Abbrev (x = ^arm6state_inp) /\ 1077 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1078 (DECODE_INST ireg = ldm) /\ (aregn2 = 2w) /\ 1079 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg /\ 1080 Abbrev (w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) ==> 1081 ~FST (DUR_X x0) ==> 1082 (!t. t < SUC (SUC w) ==> ~IS_RESET inp t) /\ 1083 (DUR_ARM6 x0 = (if ireg %% 15 /\ ~?s. s < w /\ IS_ABORT inp (s + 1) 1084 then 2 else 0) + 1 + (w - 1) + 2)`, 1085 NTAC 2 STRIP_TAC 1086 \\ FULL_SIMP_TAC (stdi_ss++STATE_INP_ss) 1087 [Abbr`x`,SINIT_def,IC_def,ABORTINST_def,NXTIC_def,INIT_ARM6, 1088 DECODE_PSR_def] 1089 \\ UNABBREV_TAC `x0` 1090 \\ ASM_SIMP_TAC stdi_ss [IC_def,ABORTINST_def,NXTIC_def,DUR_X,DUR_ARM6_def, 1091 DUR_IC,SINIT_def,DECODE_PSR_def,GSYM IMP_DISJ_THM] 1092 \\ STRIP_TAC \\ IMP_RES_TAC IS_RESET_THM2 1093 \\ POP_ASSUM (SPEC_THEN `SUC (SUC w)` (ASSUME_TAC o REWRITE_RULE 1094 [DECIDE ``!x y. SUC (SUC x) <= 2 + (x - 1) + 1 + y``])) 1095 \\ ASM_SIMP_TAC (std_ss++numSimps.ARITH_AC_ss) []); 1096 1097val LDM_f = 1098 `\t. ((f t reg psr (inp:num->bool#bool#bool#bool#word32#bool#bool)):word32, 1099 F,T,F,T, 1100 FIRST_ADDRESS (ireg %% 24) (ireg:word32 %% 23) 1101 (REG_READ6 reg (DECODE_MODE ((4 >< 0) (CPSR_READ psr))) 1102 ((19 >< 16) ireg)) 1103 (WB_ADDRESS (ireg %% 23) 1104 (REG_READ6 reg (DECODE_MODE ((4 >< 0) (CPSR_READ psr))) 1105 ((19 >< 16) ireg)) 1106 (LENGTH (REGISTER_LIST ((15 >< 0) ireg)))) + n2w (SUC t) * 4w)`; 1107 1108val SNEXT2 = (BETA_RULE o REWRITE_RULE [FUN_EQ_THM]) SNEXT_def; 1109 1110val LDM_GENLIST_MEMOP_EQ = prove( 1111 `!x. Abbrev (x = ^arm6state_inp) /\ 1112 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1113 (DECODE_INST ireg = ldm) /\ (aregn2 = 2w) /\ 1114 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg /\ 1115 Abbrev (SUC n = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) ==> 1116 ~FST (DUR_X x0) ==> 1117 (?f. GENLIST (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t 1118 (FUNPOW (SNEXT NEXT_ARM6) 2 x0)).state)) n = 1119 GENLIST (^(Parse.Term LDM_f)) n)`, 1120 REPEAT STRIP_TAC 1121 \\ EXISTS_TAC `\t reg psr inp. if t = 0 then 1122 REG_READ6 (REG_WRITE reg usr 15w (REG_READ6 reg usr 15w + 4w)) 1123 (DECODE_MODE ((4 >< 0) (CPSR_READ psr))) ARB else PROJ_DATA (inp t)` 1124 \\ MATCH_MP_TAC GENLIST_FUN_EQ 1125 \\ REPEAT STRIP_TAC 1126 \\ MAP_EVERY IMP_RES_TAC [LDM_INIT2,LDM_INIT] 1127 \\ `~IS_RESET inp 0 /\ ~IS_RESET inp 1` by ASM_SIMP_TAC arith_ss [] 1128 \\ IMP_RES_TAC NOT_RESET_EXISTS 1129 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) [Abbr`x`,Abbr`x0`,SINIT_def, 1130 PENCZ_ONE,numeral_funpow,SNEXT2,ADVANCE_def,GSYM ADVANCE_COMP, 1131 LDM_PENCZ_ZERO] 1132 \\ PAT_X_ASSUM `!sctrlreg resetlatch. P` (K ALL_TAC) 1133 \\ REPEAT ALU_ABBREV_TAC 1134 \\ `SUC n = LENGTH (REGISTER_LIST ((15 >< 0) ireg))` by METIS_TAC [] 1135 \\ `0 < SUC n /\ x' <= SUC n - 1 /\ ~(SUC n = 1)` by DECIDE_TAC 1136 \\ IMP_RES_TAC NEXT_CORE_LDM_TN_X 1137 \\ PAT_X_ASSUM `~(SUC n = 1)` (fn th => 1138 FULL_SIMP_TAC std_ss [th,WORD_MULT_CLAUSES,IS_ABORT_def]) 1139 \\ PAT_X_ASSUM `inp 1 = q` SUBST_ALL_TAC 1140 \\ FULL_SIMP_TAC std_ss [PROJ_DATA_def,PROJ_ABORT_def] 1141 \\ POP_ASSUM (STRIP_ASSUME_TAC o 1142 (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV (SKOLEM_CONV))))) 1143 \\ UNABBREV_TAC `alu1` 1144 \\ ASM_SIMP_TAC (arith_ss++ICLASS_ss++STATE_INP_ss) [PROJ_DATA_def, 1145 OUT_ARM6_def,IN_LDM_STM,GSYM FIRST_ADDRESS,TO_WRITE_READ6]); 1146 1147val FILTER_LDM_MEMOPS_X = prove( 1148 `!y x. Abbrev (x = ^arm6state_inp) /\ 1149 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1150 (DECODE_INST ireg = ldm) /\ (aregn2 = 2w) /\ 1151 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg /\ 1152 Abbrev (SUC n = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) /\ 1153 ~FST (DUR_X x0) ==> 1154 (let l = MOVE_DOUT y (GENLIST 1155 (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t 1156 (FUNPOW (SNEXT NEXT_ARM6) 2 x0)).state)) n) in 1157 FILTER IS_MEMOP l = l)`, 1158 SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1159 \\ IMP_RES_TAC LDM_GENLIST_MEMOP_EQ \\ NTAC 15 (POP_LAST_TAC) 1160 \\ POP_ASSUM SUBST1_TAC 1161 \\ MATCH_MP_TAC ((GEN_ALL o BETA_RULE o ISPEC LDM_f) FILTER_MEMOP_NONE) 1162 \\ RW_TAC bossLib.std_ss [IS_MEMOP_def]); 1163 1164fun PAT_TAC (asl, w) = 1165 let val g = (snd o strip_comb o snd o dest_comb o snd o hd o snd o 1166 TypeBase.dest_record o rhs o snd o dest_comb o fst o dest_imp) w 1167 in 1168 (MAP_EVERY (fn x => let val t = List.nth(g,x) 1169 val g = genvar (type_of t) in 1170 (ABBREV_TAC `^g = ^t` \\ POP_LAST_TAC) end) 1171 [6,16,17,18,19,20,21,34,35,36,37]) (asl, w) 1172 end; 1173 1174val PROJ_IREG_COR = GEN_ALL (prove( 1175 `Abbrev (x = ^arm6state_inp) /\ Abbrev (x0 = SINIT INIT_ARM6 x) ==> 1176 (PROJ_IREG x0.state = ireg)`, 1177 STRIP_TAC \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss) 1178 [Abbr`x`,Abbr`x0`,SINIT_def,INIT_ARM6_def,PROJ_IREG_def])); 1179 1180val state_inp_simp = 1181 simpLib.SIMP_PROVE (srw_ss()) [state_inp_component_equality] 1182 ``<| state := x.state; inp := x.inp |> = x``; 1183 1184local 1185 fun tac ss = PAT_X_ASSUM `Abbrev (q = NEXT_ARM6 (ARM6 dp ctrl) input)` MP_TAC 1186 \\ ASM_SIMP_TAC (booli_ss++pairSimps.PAIR_ss++ss++PBETA_ss) 1187 [NOT_ABORT,SND_COND_RAND,FST_COND_RAND] 1188 \\ TRY ALU_ABBREV_TAC \\ STRIP_TAC 1189 \\ POP_ASSUM (fn th => FULL_SIMP_TAC (bossLib.std_ss++boolSimps.CONJ_ss) 1190 [OUT_ARM6_def,IS_MEMOP2_def,REWRITE_RULE [markerTheory.Abbrev_def] th]) 1191in 1192 val LDM_TAC = tac LDM_ss 1193 val UNEXEC_TAC = tac UNEXEC_ss 1194end; 1195 1196val _ = print "*\nVerifying output: ldm\n*\n"; (*============================*) 1197 1198val LDM_MEMOPS = Count.apply prove( 1199 `!x. Abbrev (x = ^arm6state_inp) /\ 1200 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1201 (DECODE_INST ireg = ldm) /\ (aregn2 = 2w) /\ 1202 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 1203 ~FST (DUR_X x0) ==> 1204 (OUT_ARM (ABS_ARM6 x.state) = 1205 OSMPL_ARM6 x0 (GENLIST 1206 (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t x0).state)) 1207 (DUR_ARM6 x0)))`, 1208 REPEAT STRIP_TAC 1209 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 1210 \\ ABBREV_TAC `w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))` 1211 \\ Cases_on `w` 1212 \\ MAP_EVERY IMP_RES_TAC [LDM_INIT2,INIT_INIT,PROJ_IREG_COR] 1213 \\ ASM_SIMP_TAC (std_ss++ICLASS_ss) 1214 [FUNPOW,ADVANCE_ZERO,STATE_ARM6_COR, 1215 OSMPL_ARM6_def,SINIT_def,SUC2NUM IMM_ARM6_def,state_inp_simp] 1216 \\ POP_LASTN_TAC 4 1217 << [ 1218 `~(ireg %% 15)` by METIS_TAC [PENCZ_THM2,WORD_BITS_150_ZERO] 1219 \\ `!mask. PENCZ ldm ((15 >< 0) ireg) mask` 1220 by METIS_TAC [PENCZ_THM2,PENCZ_THM3,IN_LDM_STM] 1221 \\ ASM_SIMP_TAC (list_ss++boolSimps.LET_ss++STATE_INP_ss) 1222 [Abbr`x`,Abbr`x0`,SINIT_def,numeral_funpow,SNOC,HD_GENLIST, 1223 IS_MEMOP2_def,NULL_GENLIST,NULL_APPEND_RIGHT,ADVANCE_def, 1224 INIT_ARM6_def,ABS_ARM6_def,SNEXT2,GENLISTn,FILTER_MEMOP_ONE, 1225 FILTER_MEMOP_SINGLETON,OUT_ARM6_def] 1226 \\ REPEAT (PAT_ABBREV_TAC `q = NEXT_ARM6 a b`) 1227 \\ `~IS_RESET inp 0 /\ ~IS_RESET inp 1` by ASM_SIMP_TAC arith_ss [] 1228 \\ IMP_RES_TAC NOT_RESET_EXISTS 1229 \\ NTAC 2 LDM_TAC 1230 \\ ASM_SIMP_TAC stdi_ss [OUT_ARM_def,DECODE_PSR_def,LDM_STM_def, 1231 DECODE_LDM_STM_def,ADDR_MODE4_def,DECODE_INST_LDM,ADDRESS_LIST_def, 1232 GENLIST,MAP], 1233 IMP_RES_TAC FILTER_LDM_MEMOPS_X 1234 \\ FULL_SIMP_TAC stdi_ss [STATE_ARM6_COR,OSMPL_ARM6_def] 1235 \\ MAP_EVERY (fn th => ONCE_REWRITE_TAC [th]) 1236 [FUNPOW_COMP,GENLIST_APPEND,GENLIST_APPEND] 1237 \\ BETA_TAC \\ REWRITE_TAC 1238 [(GEN_ALL o INST [`b` |-> `2`] o SPEC_ALL) FUNPOW_COMP] 1239 \\ COND_CASES_TAC 1240 << [ 1241 `~((15 >< 0) ireg = 0w:word16)` by METIS_TAC [WORD_BITS_150_ZERO] 1242 \\ `RP ldm ((15 >< 0) ireg) (MASKN n ((15 >< 0) ireg)) = 15w` 1243 by METIS_TAC [RP_LAST_15,WORD_BITS_150_ZERO, 1244 DECIDE ``0 < SUC n /\ (!m n. (m = SUC n) ==> (n = (m - 1)))``], 1245 PAT_X_ASSUM `~(a /\ b)` (K ALL_TAC) 1246 ] 1247 \\ ASM_SIMP_TAC list_ss [FILTER_MEMOP_ONE,FILTER_MEMOP_SINGLETON, 1248 NULL_GENLIST,NULL_APPEND_RIGHT,GENLISTn,SNOC,HD_GENLIST, 1249 HD_APPEND2,IS_MEMOP2_def,CONJUNCT1 FUNPOW] 1250 \\ ASM_SIMP_TAC list_ss [FILTER_APPEND,FILTER_MEMOP_ONE, 1251 FILTER_MEMOP_SINGLETON,MOVE_DOUT_APPEND] 1252 \\ PAT_X_ASSUM `!y. FILTER f l = l` (K ALL_TAC) 1253 \\ RES_MP_TAC [] LDM_GENLIST_MEMOP_EQ \\ POP_ASSUM IMP_RES_TAC 1254 \\ PAT_X_ASSUM `Abbrev (x0 = SINIT INIT_ARM6 x)` MP_TAC 1255 \\ ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) [Abbr`x`,SINIT_def, 1256 IC_def,ABORTINST_def,NXTIC_def,DECODE_PSR_def,SNEXT2,ADVANCE_def, 1257 INIT_ARM6,numeral_funpow] 1258 \\ POP_LAST_TAC \\ STRIP_TAC 1259 \\ SIMP_TAC (bossLib.std_ss++STATE_INP_ss) [Abbr`x0`,OUT_ARM6_def, 1260 IS_MEMOP2_def,GSYM ADVANCE_COMP] 1261 \\ SIMP_TAC bossLib.std_ss [ONCE_REWRITE_RULE [ADD_COMM] FUNPOW_COMP] 1262 \\ REPEAT (PAT_ABBREV_TAC `q = NEXT_ARM6 a b`) 1263 \\ ABBREV_TAC `sn = FUNPOW (SNEXT NEXT_ARM6) n 1264 <| state := q'; inp := ADVANCE 2 inp|>` 1265 \\ `~IS_RESET inp 0 /\ ~IS_RESET inp 1` by ASM_SIMP_TAC arith_ss [] 1266 \\ IMP_RES_TAC NOT_RESET_EXISTS2 1267 \\ NTAC 2 LDM_TAC 1268 \\ PAT_X_ASSUM `Abbrev (sn = FUNPOW fn n state)` MP_TAC 1269 \\ `0 < SUC n` by DECIDE_TAC \\ IMP_RES_TAC NEXT_CORE_LDM_TN_W1 1270 \\ POP_ASSUM MP_TAC 1271 \\ ASM_SIMP_TAC (bossLib.old_arith_ss++STATE_INP_ss) [GSYM ADVANCE_COMP, 1272 LDM_PENCZ_ZERO,NOT_T3,PROJ_DATA_def,PROJ_ABORT_def,PENCZ_ONE, 1273 MASKN_1,MASKN_SUC,SPECL [`i`,`1`] IS_ABORT_def,PENCZ_THM3,LSL_ZERO] 1274 \\ DISCH_THEN (STRIP_ASSUME_TAC o 1275 (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV (SKOLEM_CONV))))) 1276 \\ ASM_SIMP_TAC (bossLib.old_arith_ss++STATE_INP_ss) 1277 [numeral_funpow,SNEXT2,ADVANCE_def] 1278 \\ POP_LAST_TAC \\ PAT_TAC 1279 \\ REPEAT (PAT_ABBREV_TAC `q = NEXT_ARM6 a b`) 1280 \\ STRIP_TAC \\ UNABBREV_TAC `sn` 1281 \\ RULE_ASSUM_TAC (SIMP_RULE (bossLib.old_arith_ss++STATE_INP_ss) 1282 [ADVANCE_def,PROJ_DATA_def]) 1283 \\ ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 1284 [OUT_ARM6_def,IS_MEMOP2_def] 1285 << [ 1286 `~IS_RESET inp (SUC n + 1)` by ASM_SIMP_TAC arith_ss [] 1287 \\ IMP_RES_TAC NOT_RESET_EXISTS \\ POP_LASTN_TAC 2 1288 \\ LDM_TAC \\ Cases_on_arm6inp `inp (SUC n + 2)` 1289 \\ UNEXEC_TAC \\ POP_LASTN_TAC 4, ALL_TAC ] 1290 \\ ASM_SIMP_TAC (stdi_ss++listSimps.LIST_ss++ARITH_ss) 1291 ([Abbr`alu`,combinTheory.o_ABS_R,GSYM FIRST_ADDRESS,LSL_ZERO, 1292 num2exception_word3,ABS_ARM6_def,MEMOP_def,MAP_LDM_MEMOP, 1293 OUT_ARM_def,DECODE_PSR_def,LDM_STM_def,DECODE_LDM_STM_def, 1294 ADDR_MODE4_def,DECODE_INST_LDM,ADDRESS_LIST_def,word_mul_n2w, 1295 MAP_GENLIST,GENLIST_CONS,WORD_ADD_0,IN_LDM_STM] @ finish_rws2)]); 1296 1297val REV_ADD4 = DECIDE ``a + b + c + d = d + c + b + a:num``; 1298 1299val LDM_LEM = prove( 1300 `!ireg:word32 base abort. 1301 Abbrev (w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) /\ 0 < w ==> 1302 ((abort /\ (base = 15w) \/ 1303 ~((if abort then 1304 base 1305 else 1306 RP ldm ((15 >< 0) ireg) (MASKN (w - 1) ((15 >< 0) ireg))) = 15w)) = 1307 (abort \/ ~(ireg %% 15)))`, 1308 REPEAT STRIP_TAC 1309 \\ Cases_on `base = 15w` \\ ASM_SIMP_TAC std_ss [Abbr`w`,LEM,RP_LAST_15] 1310 \\ Cases_on `abort` \\ ASM_SIMP_TAC std_ss [RP_LAST_15,WORD_BITS_150_ZERO]); 1311 1312val REG_WRITE_READ_NEQ_15 = 1313 (GEN_ALL o CONV_RULE (LAND_CONV (ONCE_DEPTH_CONV SYM_CONV)) o 1314 SIMP_RULE arith_ss [TO_WRITE_READ6] o 1315 INST [`n1` |-> `15w`] o SPEC_ALL) REG_READ_WRITE_NEQ; 1316 1317val ABBREV_RP_LAST_15 = 1318 (GEN_ALL o REWRITE_RULE [DECIDE ``a ==> b ==> c = a /\ b ==> c``] o 1319 SIMP_RULE std_ss [] o 1320 DISCH `Abbrev (w = LENGTH (REGISTER_LIST list))` o 1321 SPEC_ALL) RP_LAST_15; 1322 1323val IF_COND = prove( 1324 `~(~USER nbs /\ ireg %% 22) ==> 1325 (CPSR_READ (if ireg %% 22 then 1326 CPSR_WRITE (psr:psrs -> word32) (SPSR_READ psr nbs) 1327 else 1328 psr) = CPSR_READ psr)`, 1329 RW_TAC std_ss [USER_usr,CPSR_READ_WRITE]); 1330 1331val REG_WRITEN_SUC = (GEN_ALL o SIMP_RULE arith_ss [] o 1332 DISCH `0 < n` o INST [`n` |-> `n - 1`] o SPEC_ALL) REG_WRITEN_SUC; 1333 1334local val spec_list_rule = 1335 (GEN_ALL o SIMP_RULE arith_ss [GSYM WORD_BITS_150_ZERO,ADVANCE_def] o 1336 DISCH `0 < LENGTH (REGISTER_LIST ((15 >< 0) ireg))` o 1337 INST [`list` |-> `(15 >< 0) (ireg:word32)`,`i` |-> `ADVANCE 1 i`] o SPEC_ALL) 1338in 1339 val REG_WRITEN_WRITE_PC3 = spec_list_rule REG_WRITEN_WRITE_PC 1340 val REG_WRITEN_WRITE_PC4 = spec_list_rule REG_WRITEN_WRITE_PC2 1341end; 1342 1343fun PAT_TAC n = 1344 MAP_EVERY (fn s => PAT_ABBREV_TAC (mk_pat "z" s n) \\ POP_LAST_TAC) 1345 ["ointstart'","onfq'","ooonfq'","oniq'","oooniq'", 1346 "pipeaabt'","pipebabt'","borrow2'"] 1347 \\ MAP_EVERY (fn s => PAT_ABBREV_TAC (mk_pat "q" s n) \\ POP_LAST_TAC) 1348 ["oareg'","mul'"] 1349 \\ PAT_ABBREV_TAC (mk_pat "qq:word32" "mul2'" n) \\ POP_LAST_TAC 1350 \\ PAT_ABBREV_TAC (mk_pat "qqq:word5" "mshift'" n) \\ POP_LAST_TAC 1351 \\ PAT_ABBREV_TAC (mk_pat "aregn" "aregn'" n); 1352 1353val _ = print "*\nVerifying time-consistency and correctness: ldm\n*\n"; (*==*) 1354 1355val LDM = Count.apply prove( 1356 `!x. Abbrev (x = ^arm6state_inp) /\ inp IN STRM_ARM6 /\ 1357 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1358 (DECODE_INST ireg = ldm) /\ (aregn2 = 2w) /\ 1359 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 1360 ~FST (DUR_X x0) ==> 1361 (let s = (FUNPOW (SNEXT NEXT_ARM6) (DUR_ARM6 x0) x0).state in 1362 (INIT_ARM6 s = s) /\ 1363 (STATE_ARM 1 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 1364 ABS_ARM6 s))`, 1365 REPEAT STRIP_TAC 1366 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 1367 \\ ABBREV_TAC `w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))` 1368 \\ MAP_EVERY IMP_RES_TAC [LDM_INIT2,INIT_INIT,PROJ_IREG_COR] 1369 \\ `(x.inp = inp) /\ (x.state = ^arm6state) /\ 1370 (<|state := x0.state; inp := inp|> = x0)` 1371 by SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,Abbr`x0`,SINIT_def] 1372 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++SIZES_ss) [num2exception_thm, 1373 SUC2NUM STATE_ARM_def,ABS_ARM6_def,SMPL_ARM6_def,SMPL_DATA_ARM6_def, 1374 IFLAGS_def,ADVANCE_ZERO,DECODE_PSR_def,PACK_def,IMM_LEN_def, 1375 SUC2NUM IMM_ARM6_def,MAP_STRM_def,COMBINE_def,SMPL_EXC_ARM6_def, 1376 STATE_ARM6_COR,FUNPOW,ADVANCE_ZERO,OSMPL_ARM6_def,SINIT_def, 1377 SUC2NUM IMM_ARM6_def,state_inp_simp] 1378 \\ POP_LASTN_TAC 7 1379 \\ PAT_ABBREV_TAC `s = (FUNPOW (SNEXT NEXT_ARM6) d x0).state` 1380 \\ POP_ASSUM MP_TAC 1381 \\ REWRITE_TAC [FUNPOW_COMP] 1382 \\ PAT_X_ASSUM `~FST (DUR_X x0)` MP_TAC 1383 \\ ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 1384 [Abbr`x`,Abbr`x0`,ADVANCE_def,SINIT_def,SNEXT,numeral_funpow] 1385 \\ `~IS_RESET inp 0 /\ ~IS_RESET inp 1` by ASM_SIMP_TAC arith_ss [] 1386 \\ MAP_EVERY IMP_RES_TAC [NOT_RESET_EXISTS2,LDM_INIT] 1387 \\ ASM_SIMP_TAC stdi_ss [DUR_X2,DUR_IC_def,INIT_ARM6] \\ POP_LAST_TAC 1388 \\ STRIP_TAC \\ REPEAT ALU_ABBREV_TAC 1389 \\ Cases_on `(15 >< 0) ireg = 0w:word16` 1390 \\ ASM_SIMP_TAC stdi_ss [PENCZ_THM3,IN_LDM_STM] 1391 << [ 1392 MAP_EVERY IMP_RES_TAC [PENCZ_THM2,CONJUNCT1 WORD_BITS_150_ZERO] 1393 \\ ASM_SIMP_TAC std_ss [Abbr`w`,SUB_0,FUNPOW] 1394 \\ `~IS_RESET inp 2` by ASM_SIMP_TAC arith_ss [] 1395 \\ IMP_RES_TAC NOT_RESET_EXISTS2 \\ POP_LASTN_TAC 2 1396 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss) [SNEXT_def,ADVANCE_def] 1397 \\ iclass_compLib.LDM_TAC 1398 \\ FULL_SIMP_TAC (stdi_ss++STATE_INP_ss) [] 1399 \\ STRIP_TAC \\ UNABBREV_TAC `s` \\ CONJ_TAC 1400 << [ 1401 RW_TAC std_ss finish_rws \\ FULL_SIMP_TAC std_ss [], 1402 IMP_RES_TAC DECODE_INST_LDM 1403 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss++SIZES_ss) 1404 (word_0::finish_rws3) 1405 \\ RW_TAC stdi_ss ([Abbr`alu`,FIRSTN,WB_ADDRESS_ZERO,IN_LDM_STM, 1406 (REWRITE_RULE [] o SPEC `0w`) PENCZ_THM2,LDM_LIST_EMPTY, 1407 USER_usr] @ finish_rws2) 1408 ], 1409 `0 < w` by FULL_SIMP_TAC arith_ss [Abbr`w`,PENCZ_THM2] 1410 \\ ABBREV_TAC `abort = ?s. s < w /\ IS_ABORT inp (s + 1)` 1411 \\ `Abbrev (~abort = !s. s < w ==> ~IS_ABORT inp (s + 1))` 1412 by SIMP_TAC std_ss [Abbr`abort`,IS_ABORT_def,IMP_DISJ_THM, 1413 markerTheory.Abbrev_def] 1414 \\ FULL_SIMP_TAC std_ss [] 1415 \\ IMP_RES_TAC NEXT_CORE_LDM_TN_W1 1416 \\ POP_ASSUM (STRIP_ASSUME_TAC o 1417 (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV (SKOLEM_CONV))))) 1418 \\ PAT_X_ASSUM `inp 1 = (T,ABORT1,NFQ1,NIQ1,DATA1,CPA1,CPB1)` 1419 (fn th => RULE_ASSUM_TAC (SIMP_RULE std_ss 1420 [SPECL [`x`,`1`] IS_ABORT_def,PROJ_ABORT_def,PROJ_DATA_def,th])) 1421 \\ ASM_SIMP_TAC (stdi_ss++ARITH_ss) [PENCZ_ONE, 1422 GSYM ADVANCE_COMP,LDM_PENCZ_ZERO] 1423 \\ PAT_X_ASSUM `!sctrlreg reg psrfb. P` (ASSUME_TAC o GEN_ALL o 1424 (MATCH_MP (DECIDE ``a /\ b /\ c /\ d ==> a /\ b /\ c``)) o SPEC_ALL) 1425 \\ PAT_TAC 23 1426 \\ `~(aregn IN {0w; 1w; 2w; 5w}) /\ 1427 ((aregn = 7w) ==> ~(CPSR_READ psr %% 6)) /\ 1428 ((aregn = 6w) ==> ~(CPSR_READ psr %% 7))` 1429 by METIS_TAC [Abbr`aregn`] 1430 \\ markerLib.RM_ABBREV_TAC "aregn" 1431 \\ PAT_X_ASSUM `!sctrlreg reg psrfb. P` (K ALL_TAC) 1432 \\ `~IS_RESET inp (w + 1)` 1433 by METIS_TAC [DECIDE ``!w. 0 < w ==> w + 1 < 2 + (w - 1) + 1 + x``] 1434 \\ IMP_RES_TAC NOT_RESET_EXISTS2 1435 \\ ASM_SIMP_TAC arith_ss [SNEXT,numeral_funpow,ADVANCE_def] 1436 \\ iclass_compLib.LDM_TAC 1437 \\ RES_MP_TAC [`base` |-> `(19 >< 16) ireg`] LDM_LEM 1438 \\ ASM_SIMP_TAC (stdi_ss++ARITH_ss++boolSimps.CONJ_ss++PBETA_ss) 1439 [ALUOUT_ALU_logic,LSL_ZERO,DECIDE ``a /\ b \/ ~a = a ==> b``] 1440 \\ POP_LAST_TAC 1441 \\ Cases_on `~abort /\ ireg %% 15` 1442 \\ ASM_SIMP_TAC std_ss [FUNPOW] 1443 << [ 1444 REPEAT (PAT_X_ASSUM `~IS_RESET inp x` (K ALL_TAC)) 1445 \\ `~IS_RESET inp (w + 2) /\ ~IS_RESET inp (w + 3)` 1446 by FULL_SIMP_TAC arith_ss [] 1447 \\ IMP_RES_TAC NOT_RESET_EXISTS2 1448 \\ RES_MP_TAC [`list` |-> `(15 >< 0) (ireg:word32)`] 1449 ABBREV_RP_LAST_15 1450 \\ ASM_SIMP_TAC arith_ss [REG_WRITEN_def,SNEXT, 1451 numeral_funpow,ADVANCE_def] 1452 \\ POP_LAST_TAC 1453 \\ iclass_compLib.UNEXEC_TAC 1454 \\ SIMP_TAC (stdi_ss++STATE_INP_ss) [] 1455 \\ STRIP_TAC \\ UNABBREV_TAC `s` \\ CONJ_TAC 1456 << [ 1457 POP_ASSUM_LIST (K ALL_TAC) \\ RW_TAC std_ss finish_rws 1458 \\ FULL_SIMP_TAC std_ss [], 1459 IMP_RES_TAC DECODE_INST_LDM 1460 \\ `w <= LENGTH (REGISTER_LIST ((15 >< 0) ireg)) /\ 1461 LENGTH (REGISTER_LIST ((15 >< 0) ireg)) <= w + 3` 1462 by SIMP_TAC arith_ss [Abbr`w`] 1463 \\ Cases_on `~USER nbs /\ ireg %% 22` 1464 \\ IMP_RES_TAC IF_COND 1465 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) 1466 ([REG_WRITEN_SUC,GSYM WORD_BITS_150_ZERO] @ finish_rws3) 1467 \\ RW_TAC stdi_ss ([Abbr`w`,Abbr`alu`, 1468 (SIMP_RULE arith_ss [FST_ADDR_MODE4] o INST [`n` |-> 1469 `LENGTH (REGISTER_LIST ((15 >< 0) ireg)) + 3`] o 1470 SPEC_ALL) REGISTER_LIST_LDM_THM,GSYM WORD_BITS_150_ZERO, 1471 SND_ADDR_MODE4,REG_WRITEN_WRITE_PC4,GSYM FIRST_ADDRESS, 1472 ALUOUT_ALU_logic,LENGTH_ADDR_MODE4,GSYM WB_ADDRESS, 1473 REG_READ_WRITEN_PC,ADVANCE_def,LSL_ZERO,IN_LDM_STM, 1474 REG_WRITE_WRITEN_PC,REG_WRITEN_WRITE_PC3] @ finish_rws2) 1475 \\ FULL_SIMP_TAC std_ss [CPSR_READ_WRITE] 1476 ], 1477 STRIP_TAC \\ UNABBREV_TAC `s` 1478 \\ FULL_SIMP_TAC (std_ss++STATE_INP_ss) [FUNPOW] 1479 << [ALL_TAC, 1480 `~(RP ldm ((15 >< 0) ireg) (MASKN (w - 1) ((15 >< 0) ireg)) = 15w)` 1481 by METIS_TAC [RP_LAST_15,CONJUNCT2 WORD_BITS_150_ZERO] 1482 \\ `w - 1 < w` by DECIDE_TAC] 1483 \\ (CONJ_TAC 1484 << [ 1485 RW_TAC std_ss finish_rws \\ FULL_SIMP_TAC std_ss [], 1486 IMP_RES_TAC DECODE_INST_LDM 1487 \\ `abort ==> ((LEAST s. IS_ABORT inp (s + 1)) < w) /\ 1488 ((LEAST s. s < w /\ IS_ABORT inp (s + 1)) = 1489 (LEAST s. IS_ABORT inp (s + 1))) /\ 1490 ((w = 1) ==> 1491 ((LEAST s. s < 1 /\ IS_ABORT inp (s + 1)) = 1492 (LEAST s. IS_ABORT inp (s + 1))))` 1493 by (SIMP_TAC std_ss [Abbr`abort`,GSYM IS_ABORT_def, 1494 LEAST_ABORT_LT2,LEAST_ABORT_ISA] \\ 1495 METIS_TAC [LEAST_ABORT_ISA]) 1496 \\ Cases_on `abort` \\ FULL_SIMP_TAC std_ss [] 1497 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) 1498 ([SIMP_PROJ_Dabort,REG_WRITEN_SUC, 1499 GSYM WORD_BITS_150_ZERO] @ finish_rws3) 1500 \\ RW_TAC arith_ss ([Abbr`w`,Abbr`alu`, 1501 (SIMP_RULE arith_ss [FST_ADDR_MODE4] o 1502 INST [`n` |-> `LENGTH (REGISTER_LIST ireg) + 1`] o 1503 SPEC_ALL) REGISTER_LIST_LDM_THM,GSYM WORD_BITS_150_ZERO, 1504 SND_ADDR_MODE4,REG_WRITEN_WRITE_PC4,GSYM FIRST_ADDRESS, 1505 REG_WRITEN_COMMUTE_PC,ALUOUT_ALU_logic,LENGTH_ADDR_MODE4, 1506 GSYM WB_ADDRESS,REG_READ_WRITEN_PC,REG_WRITEN_COMMUTES, 1507 REG_READ_WRITEN_PC2,ADVANCE_def,LSL_ZERO,IN_LDM_STM, 1508 REG_WRITE_WRITEN_PC,REG_WRITEN_WRITE_PC3] @ finish_rws2) 1509 \\ `(LEAST s. IS_ABORT inp (s + 1)) = 0` by DECIDE_TAC 1510 \\ ASM_SIMP_TAC std_ss ((CONJUNCT1 REG_WRITEN_def)::finish_rws2) 1511 ])]]); 1512 1513(* ------------------------------------------------------------------------- *) 1514 1515val LENGTH_ONE = prove( 1516 `!l. (LENGTH l = 1) ==> (l = [HD l])`, 1517 Cases \\ SIMP_TAC list_ss [LENGTH_NIL]); 1518 1519val HD_TL = prove( 1520 `!l. (0 < LENGTH l) ==> (l = ((HD l)::TL l))`, 1521 Cases \\ SIMP_TAC list_ss [LENGTH_NIL]); 1522 1523val STM_PENCZ_ZERO = 1524 (GEN_ALL o REWRITE_RULE [MASKN_ZERO] o INST [`x` |-> `0`] o SPEC_ALL o 1525 CONJUNCT1 o SIMP_RULE std_ss [IN_LDM_STM] o SPEC `stm`) PENCZ_THM; 1526 1527val STM_PENCZ_ONE = 1528 (GEN_ALL o REWRITE_RULE [] o INST [`x` |-> `1`] o SPEC_ALL o 1529 CONJUNCT1 o SIMP_RULE std_ss [IN_LDM_STM] o SPEC `stm`) PENCZ_THM; 1530 1531val STM_INIT = 1532 (SIMP_RULE (stdi_ss++boolSimps.CONJ_ss++ARITH_ss) 1533 [MASK_def,STM_PENCZ_ZERO,STM_PENCZ_ONE,IN_LDM_STM,MASKN_2,LSL_ZERO] o 1534 SIMP_RULE (booli_ss++STM_ss++PBETA_ss) 1535 [IS_ABORT,SND_COND_RAND,FST_COND_RAND,IN_LDM_STM,MASKN_1] o 1536 CONV_RULE (RAND_CONV (RHS_CONV 1537 (LAND_CONV (ONCE_REWRITE_CONV [next_7tuple])))) o 1538 CONV_RULE (RAND_CONV (RHS_CONV (ONCE_REWRITE_CONV [next_7tuple]))) o 1539 SIMP_RULE stdi_ss [IC_def,ABORTINST_def,NXTIC_def,DECODE_PSR_def] o 1540 DISCH `1 < LENGTH (REGISTER_LIST ((15 >< 0) ireg)) /\ 1541 (DECODE_INST ireg = stm) /\ (aregn2 = 2w) /\ 1542 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg` o 1543 SIMP_CONV bossLib.bool_ss [INIT_ARM6_def]) 1544 ``NEXT_ARM6 (NEXT_ARM6 (INIT_ARM6 (ARM6 (DP reg psr areg din alua alub dout) 1545 (CTRL pipea pipeaval pipeb pipebval ireg iregval ointstart onewinst 1546 endinst obaselatch opipebll nxtic nxtis nopc1 oorst resetlatch 1547 onfq ooonfq oniq oooniq pipeaabt pipebabt iregabt2 dataabt2 aregn2 1548 mrq2 nbw nrw sctrlreg psrfb oareg mask orp oorp mul mul2 borrow2 1549 mshift))) i0) i1``; 1550 1551val STM_INIT2 = prove( 1552 `!x. Abbrev (x = ^arm6state_inp) /\ 1553 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1554 (DECODE_INST ireg = stm) /\ (aregn2 = 2w) /\ 1555 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg /\ 1556 Abbrev (l = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) ==> 1557 ~FST (DUR_X x0) ==> 1558 (!t. t < SUC l ==> ~IS_RESET inp t) /\ (DUR_ARM6 x0 = (2 + (l - 1)))`, 1559 NTAC 2 STRIP_TAC 1560 \\ FULL_SIMP_TAC (stdi_ss++STATE_INP_ss) [Abbr`x`,Abbr`x0`,SINIT_def, 1561 IC_def,ABORTINST_def,NXTIC_def,INIT_ARM6_def,DECODE_PSR_def,IC_def, 1562 ABORTINST_def,NXTIC_def,DUR_X,DUR_ARM6_def,DUR_IC,SINIT_def, 1563 GSYM IMP_DISJ_THM] 1564 \\ STRIP_TAC \\ IMP_RES_TAC IS_RESET_THM2 1565 \\ POP_ASSUM (SPEC_THEN `SUC l` (STRIP_ASSUME_TAC o 1566 REWRITE_RULE [DECIDE ``!x y. SUC x <= 2 + (x - 1)``]))); 1567 1568val STM_f = 1569 `\t. (if t = 0 then 1570 REG_READ6 (REG_WRITE reg usr 15w 1571 (REG_READ6 reg usr 15w + 4w)) nbs (RP stm ((15 >< 0) ireg) UINT_MAXw) 1572 else 1573 REG_READ6 1574 (if ireg %% 21 /\ ~((19 >< 16) ireg = 15w:word4) then 1575 REG_WRITE (REG_WRITE reg usr 15w 1576 (REG_READ6 reg usr 15w + 4w)) nbs ((19 >< 16) ireg) 1577 (WB_ADDRESS (ireg %% 23) 1578 (REG_READ6 reg (DECODE_MODE ((4 >< 0) (CPSR_READ psr))) 1579 ((19 >< 16) (ireg:word32))) 1580 (LENGTH (REGISTER_LIST ((15 >< 0) ireg)))) 1581 else 1582 REG_WRITE reg usr 15w (REG_READ6 reg usr 15w + 4w)) nbs 1583 (RP stm ((15 >< 0) ireg) (MASKN t ((15 >< 0) ireg))),F,T,T,T, 1584 FIRST_ADDRESS (ireg %% 24) (ireg %% 23) 1585 (REG_READ6 reg (DECODE_MODE ((4 >< 0) (CPSR_READ psr))) 1586 ((19 >< 16) ireg)) 1587 (WB_ADDRESS (ireg %% 23) 1588 (REG_READ6 reg (DECODE_MODE ((4 >< 0) (CPSR_READ psr))) 1589 ((19 >< 16) ireg)) 1590 (LENGTH (REGISTER_LIST ((15 >< 0) ireg)))) + n2w (SUC t) * 4w)`; 1591 1592val STM_GENLIST_MEMOP_EQ = prove( 1593 `!x. Abbrev (x = ^arm6state_inp) /\ 1594 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1595 Abbrev (nbs = if ireg %% 22 then usr 1596 else DECODE_MODE ((4 >< 0) (CPSR_READ psr))) /\ 1597 (DECODE_INST ireg = stm) /\ (aregn2 = 2w) /\ 1598 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg /\ 1599 Abbrev (SUC n = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) ==> 1600 ~FST (DUR_X x0) ==> 1601 (GENLIST (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t 1602 (FUNPOW (SNEXT NEXT_ARM6) 2 x0)).state)) n = 1603 GENLIST (^(Parse.Term STM_f)) n)`, 1604 REPEAT STRIP_TAC 1605 \\ MATCH_MP_TAC GENLIST_FUN_EQ 1606 \\ MAP_EVERY IMP_RES_TAC [STM_INIT2,STM_INIT] 1607 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) [Abbr`x`,Abbr`x0`,SINIT_def, 1608 numeral_funpow,SNEXT,ADVANCE_def,GSYM ADVANCE_COMP, 1609 STM_PENCZ_ZERO,PENCZ_ONE] 1610 \\ POP_LAST_TAC 1611 \\ REPEAT ALU_ABBREV_TAC 1612 \\ REPEAT STRIP_TAC 1613 \\ `~IS_RESET inp 0 /\ ~IS_RESET inp 1` 1614 by METIS_TAC [DECIDE ``0 < SUC (SUC n) /\ 1 < SUC (SUC n)``] 1615 \\ IMP_RES_TAC NOT_RESET_EXISTS2 1616 \\ `1 < SUC n /\ x <= SUC n - 2 /\ ~(SUC n = 1)` by DECIDE_TAC 1617 \\ `SUC n = LENGTH (REGISTER_LIST ((15 >< 0) ireg))` by METIS_TAC [] 1618 \\ IMP_RES_TAC NEXT_CORE_STM_TN_X 1619 \\ PAT_X_ASSUM `~(SUC n = 1)` 1620 (fn th => FULL_SIMP_TAC std_ss [th,WORD_MULT_CLAUSES]) 1621 \\ POP_ASSUM (STRIP_ASSUME_TAC o 1622 (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV (SKOLEM_CONV))))) 1623 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) [Abbr`alu`,Abbr`alu1`, 1624 IS_ABORT_def,PROJ_ABORT_def,ADVANCE_def,OUT_ARM6_def,GSYM WB_ADDRESS, 1625 GSYM FIRST_ADDRESS,TO_WRITE_READ6,IN_LDM_STM]); 1626 1627val FILTER_STM_MEMOPS_X = prove( 1628 `!x. Abbrev (x = ^arm6state_inp) /\ 1629 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1630 (DECODE_INST ireg = stm) /\ (aregn2 = 2w) /\ 1631 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg /\ 1632 Abbrev (SUC n = LENGTH (REGISTER_LIST ((15 >< 0) ireg))) /\ 1633 ~FST (DUR_X x0) ==> 1634 (let l = MOVE_DOUT y (GENLIST (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t 1635 (FUNPOW (SNEXT NEXT_ARM6) 2 x0)).state)) n) in 1636 FILTER IS_MEMOP l = l)`, 1637 SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1638 \\ ABBREV_TAC `nbs = if ireg %% 22 then usr 1639 else DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 1640 \\ IMP_RES_TAC STM_GENLIST_MEMOP_EQ 1641 \\ POP_ASSUM SUBST1_TAC 1642 \\ MATCH_MP_TAC ((GEN_ALL o BETA_RULE o ISPEC STM_f) FILTER_MEMOP_NONE) 1643 \\ RW_TAC bossLib.std_ss [IS_MEMOP_def]); 1644 1645val FILTER_STM_MEMOPS_X = 1646 SIMP_RULE (bool_ss++boolSimps.LET_ss) [] FILTER_STM_MEMOPS_X; 1647 1648val STM_TAC = 1649 PAT_X_ASSUM `Abbrev (q = NEXT_ARM6 (ARM6 dp ctrl) input)` MP_TAC 1650 \\ ASM_SIMP_TAC (booli_ss++pairSimps.PAIR_ss++STM_ss++PBETA_ss) 1651 [SND_COND_RAND,FST_COND_RAND] 1652 \\ TRY ALU_ABBREV_TAC \\ STRIP_TAC 1653 \\ POP_ASSUM (fn th => FULL_SIMP_TAC (bossLib.std_ss++boolSimps.CONJ_ss) 1654 [OUT_ARM6_def,IS_MEMOP2_def,REWRITE_RULE [markerTheory.Abbrev_def] th]); 1655 1656val _ = print "*\nVerifying output: stm\n*\n"; (*============================*) 1657 1658val STM_MEMOPS = Count.apply prove( 1659 `!x. Abbrev (x = ^arm6state_inp) /\ Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1660 (DECODE_INST ireg = stm) /\ (aregn2 = 2w) /\ 1661 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 1662 ~FST (DUR_X x0) ==> 1663 (OUT_ARM (ABS_ARM6 x.state) = 1664 OSMPL_ARM6 x0 (GENLIST 1665 (\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t x0).state)) (DUR_ARM6 x0)))`, 1666 REPEAT STRIP_TAC 1667 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 1668 \\ ABBREV_TAC `w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))` 1669 \\ MAP_EVERY IMP_RES_TAC [STM_INIT2,INIT_INIT,PROJ_IREG_COR] 1670 \\ ASM_SIMP_TAC (arith_ss++ICLASS_ss) 1671 [FUNPOW,ADVANCE_ZERO,STATE_ARM6_COR,OSMPL_ARM6_def,SINIT_def, 1672 SUC2NUM IMM_ARM6_def,state_inp_simp] 1673 \\ POP_LASTN_TAC 4 1674 \\ `~IS_RESET inp 0` by ASM_SIMP_TAC arith_ss [] 1675 \\ IMP_RES_TAC NOT_RESET_EXISTS2 1676 \\ Cases_on `w` 1677 << [ 1678 FULL_SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,SINIT_def,INIT_ARM6_def, 1679 IC_def,ABORTINST_def,NXTIC_def, DECODE_PSR_def] 1680 \\ SIMP_TAC (list_ss++STATE_INP_ss) [Abbr`x0`,GENLISTn,OUT_ARM6_def, 1681 IS_MEMOP2_def,FILTER_MEMOP_ONE,FILTER_MEMOP_SINGLETON,ADVANCE_def, 1682 SNEXT,numeral_funpow,SNOC,ABS_ARM6_def] 1683 \\ REPEAT (PAT_ABBREV_TAC `q = NEXT_ARM6 a b`) 1684 \\ `!mask. PENCZ stm ((15 >< 0) ireg) mask` 1685 by METIS_TAC [PENCZ_THM2,PENCZ_THM3,IN_LDM_STM] 1686 \\ STM_TAC 1687 \\ `REGISTER_LIST ((15 >< 0) ireg) = []` by METIS_TAC [LENGTH_NIL] 1688 \\ ASM_SIMP_TAC (stdi_ss++listSimps.LIST_ss) [OUT_ARM_def, 1689 DECODE_PSR_def,LDM_STM_def,STM_LIST_def,DECODE_LDM_STM_def, 1690 ADDR_MODE4_def,DECODE_INST_STM,ADDRESS_LIST_def, 1691 GENLIST,ZIP,MAP], 1692 Cases_on `n` 1693 << [ 1694 FULL_SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,SINIT_def, 1695 INIT_ARM6_def,IC_def,ABORTINST_def,NXTIC_def,DECODE_PSR_def] 1696 \\ `~IS_RESET inp 1` by ASM_SIMP_TAC arith_ss [] 1697 \\ IMP_RES_TAC NOT_RESET_EXISTS2 1698 \\ SIMP_TAC (list_ss++STATE_INP_ss) [Abbr`x0`,GENLISTn, 1699 OUT_ARM6_def,IS_MEMOP2_def,FILTER_MEMOP_ONE, 1700 FILTER_MEMOP_SINGLETON,ADVANCE_def,SNEXT,numeral_funpow, 1701 SNOC,ABS_ARM6_def] 1702 \\ REPEAT (PAT_ABBREV_TAC `q = NEXT_ARM6 a b`) 1703 \\ NTAC 2 STM_TAC 1704 \\ `LENGTH (FST (ADDR_MODE4 (ireg %% 24) (ireg %% 23) 1705 (REG_READ6 reg nbs ((19 >< 16) ireg)) ((15 >< 0) ireg))) = 1` 1706 by METIS_TAC [LENGTH_ADDR_MODE4] 1707 \\ POP_ASSUM (ASSUME_TAC o (MATCH_MP LENGTH_ONE)) 1708 \\ ASM_SIMP_TAC (stdi_ss++ARITH_ss++PBETA_ss) 1709 ([Abbr`alu`,STM_PENCZ_ZERO,FILTER_MEMOP_SINGLETON, 1710 IS_MEMOP2_def,OUT_ARM_def,DECODE_PSR_def,LDM_STM_def, 1711 STM_LIST_def,LSL_ZERO,DECODE_LDM_STM_def,DECODE_INST_STM, 1712 ADDRESS_LIST_def,MAP,MEMOP_def,GENLISTn,SNOC,IN_LDM_STM, 1713 SND_ADDR_MODE4,MASKN_ZERO,GSYM WB_ADDRESS,GSYM FIRST_ADDRESS, 1714 ALUOUT_ALU_logic,WORD_MULT_CLAUSES,num2exception_word3, 1715 FST_HD_FST_ADDR_MODE4,LENGTH_ONE] @ finish_rws2) 1716 \\ POP_ASSUM SUBST1_TAC 1717 \\ ASM_SIMP_TAC arith_ss [ZIP,MAP,FST_HD_FST_ADDR_MODE4] 1718 \\ RW_TAC arith_ss finish_rws2 1719 \\ Cases_on `RP stm ((15 >< 0) ireg) UINT_MAXw = 15w` 1720 \\ RW_TAC arith_ss ([REG_READ_WRITE_NEQ,REG_WRITE_READ_NEQ_15] @ 1721 finish_rws2), 1722 IMP_RES_TAC FILTER_STM_MEMOPS_X 1723 \\ ASM_SIMP_TAC list_ss [NULL_GENLIST,GENLISTn,FILTER_MEMOP_ONE, 1724 ONCE_REWRITE_RULE [ADD_COMM] GENLIST_APPEND, 1725 (GEN_ALL o INST [`b` |-> `2`] o SPEC_ALL) FUNPOW_COMP, 1726 FILTER_MEMOP_SINGLETON,SNOC,HD_GENLIST,CONJUNCT1 FUNPOW] 1727 \\ POP_LAST_TAC \\ UNABBREV_TAC `nbs` 1728 \\ ABBREV_TAC `nbs = if ireg %% 22 then usr 1729 else DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 1730 \\ IMP_RES_TAC STM_GENLIST_MEMOP_EQ 1731 \\ POP_ASSUM SUBST1_TAC 1732 \\ SIMP_TAC (bossLib.old_arith_ss++STATE_INP_ss) 1733 [Abbr`x0`,Abbr`x`,SINIT_def,SNEXT,numeral_funpow] 1734 \\ REPEAT (PAT_ABBREV_TAC `q = NEXT_ARM6 a b`) 1735 \\ FULL_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) [INIT_ARM6,IC_def, 1736 ABORTINST_def,NXTIC_def,DECODE_PSR_def] 1737 \\ FULL_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 1738 [ADVANCE_def,OUT_ARM6_def,IS_MEMOP2_def,ABS_ARM6_def] 1739 \\ `~IS_RESET inp 1` by ASM_SIMP_TAC arith_ss [] 1740 \\ IMP_RES_TAC NOT_RESET_EXISTS2 \\ POP_LAST_TAC 1741 \\ NTAC 2 STM_TAC 1742 \\ ASM_SIMP_TAC (bossLib.old_arith_ss++STATE_INP_ss) [MASK_def, 1743 STM_PENCZ_ZERO,STM_PENCZ_ONE,LSL_ZERO,MASKN_1,MASKN_2, 1744 GSYM ADVANCE_COMP,iseq_distinct] 1745 \\ UNABBREV_TAC `nbs` 1746 \\ ABBREV_TAC `cpsr = CPSR_READ psr` 1747 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) cpsr)` 1748 \\ `1 < SUC (SUC n')` by DECIDE_TAC 1749 \\ `!t. t < SUC (SUC n') ==> ~IS_RESET inp t` 1750 by ASM_SIMP_TAC arith_ss [] 1751 \\ IMP_RES_TAC NEXT_CORE_STM_TN_W1 1752 \\ POP_ASSUM (STRIP_ASSUME_TAC o 1753 (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV (SKOLEM_CONV))))) 1754 \\ `SUC n' = SUC (SUC n') - 1` by DECIDE_TAC 1755 \\ POP_ASSUM SUBST1_TAC 1756 \\ ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) [OUT_ARM6_def] 1757 \\ POP_LAST_TAC 1758 \\ `LENGTH (FST (ADDR_MODE4 (ireg %% 24) (ireg %% 23) 1759 (REG_READ6 reg nbs ((19 >< 16) ireg)) ((15 >< 0) ireg))) = 1760 SUC (SUC n')` 1761 by PROVE_TAC [LENGTH_ADDR_MODE4] 1762 \\ ASM_SIMP_TAC (stdi_ss++PBETA_ss++listSimps.LIST_ss++ARITH_ss) 1763 ([Abbr`alu`,Abbr`alu1`,combinTheory.o_ABS_R,word_mul_n2w, 1764 LSL_ZERO,ABS_ARM6_def,MEMOP_def,MAP_STM_MEMOP,OUT_ARM_def, 1765 DECODE_PSR_def,LDM_STM_def,DECODE_LDM_STM_def,IN_LDM_STM, 1766 SND_ADDR_MODE4,DECODE_INST_STM,ADDRESS_LIST_def,MAP_GENLIST, 1767 WORD_ADD_0,STM_LIST_def,SND_ADDR_MODE4,GSYM WB_ADDRESS, 1768 GSYM FIRST_ADDRESS,FST_HD_FST_ADDR_MODE4,ZIP_GENLIST, 1769 LENGTH_GENLIST,num2exception_word3] @ finish_rws2) 1770 \\ ASM_SIMP_TAC list_ss [(GEN_ALL o SPEC `SUC n`) GENLIST_CONS, 1771 FST_HD_FST_ADDR_MODE4,WORD_ADD_0] 1772 \\ CONJ_TAC 1773 << [ 1774 RW_TAC arith_ss finish_rws2 1775 \\ Cases_on `RP stm ((15 >< 0) ireg) UINT_MAXw = 15w` 1776 \\ RW_TAC arith_ss 1777 ([REG_READ_WRITE_NEQ,REG_WRITE_READ_NEQ_15] @ finish_rws2), 1778 MATCH_MP_TAC GENLIST_FUN_EQ 1779 \\ SIMP_TAC arith_ss [GSYM ADD1] 1780 \\ `SUC n' < LENGTH (REGISTER_LIST ((15 >< 0) ireg))` 1781 by ASM_SIMP_TAC arith_ss [LENGTH_ADDR_MODE4] 1782 \\ RW_TAC arith_ss ([REG_READ_WRITE_NEQ,REG_WRITE_READ_NEQ_15, 1783 (GSYM o CONJUNCT2) EL,GSYM REGISTER_LIST_STM_THM] @ 1784 finish_rws2) 1785 \\ PAT_X_ASSUM `q = (19 >< 16) ireg` (SUBST1_TAC o SYM) 1786 << (let fun tac x = Cases_on `RP stm ((15 >< 0) ireg) 1787 (MASKN (SUC (^x)) ((15 >< 0) ireg)) = 15w` \\ 1788 RW_TAC arith_ss ([REG_READ_WRITE_NEQ,RP_NOT_EQUAL_ZERO, 1789 REG_WRITE_READ_NEQ_15] @ finish_rws2) in 1790 [tac ``n':num``, tac ``x:num``, tac ``n':num``, tac ``x:num``] 1791 end)]]]); 1792 1793val _ = print "*\nVerifying time-consistency and correctness: stm\n*\n"; (*==*) 1794 1795val STM = Count.apply prove( 1796 `!x. Abbrev (x = ^arm6state_inp) /\ inp IN STRM_ARM6 /\ 1797 Abbrev (x0 = SINIT INIT_ARM6 x) /\ 1798 (DECODE_INST ireg = stm) /\ (aregn2 = 2w) /\ 1799 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 1800 ~FST (DUR_X x0) ==> 1801 (let s = (FUNPOW (SNEXT NEXT_ARM6) (DUR_ARM6 x0) x0).state in 1802 (INIT_ARM6 s = s) /\ 1803 (STATE_ARM 1 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 1804 ABS_ARM6 s))`, 1805 REPEAT STRIP_TAC 1806 \\ ABBREV_TAC `nbs = DECODE_MODE ((4 >< 0) (CPSR_READ psr))` 1807 \\ ABBREV_TAC `w = LENGTH (REGISTER_LIST ((15 >< 0) ireg))` 1808 \\ MAP_EVERY IMP_RES_TAC [STM_INIT2,INIT_INIT,PROJ_IREG_COR] 1809 \\ `(x.inp = inp) /\ (x.state = ^arm6state) /\ 1810 (<|state := x0.state; inp := inp|> = x0)` 1811 by SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,Abbr`x0`,SINIT_def] 1812 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++SIZES_ss) [num2exception_thm, 1813 SUC2NUM STATE_ARM_def,ABS_ARM6_def,SMPL_ARM6_def,SMPL_DATA_ARM6_def, 1814 IFLAGS_def,ADVANCE_ZERO,DECODE_PSR_def,PACK_def,IMM_LEN_def, 1815 SUC2NUM IMM_ARM6_def,MAP_STRM_def,COMBINE_def,SMPL_EXC_ARM6_def, 1816 STATE_ARM6_COR,FUNPOW,ADVANCE_ZERO,OSMPL_ARM6_def,SINIT_def, 1817 SUC2NUM IMM_ARM6_def,state_inp_simp] 1818 \\ POP_LASTN_TAC 7 1819 \\ PAT_ABBREV_TAC `s = (FUNPOW (SNEXT NEXT_ARM6) d x0).state` 1820 \\ POP_ASSUM MP_TAC 1821 \\ ONCE_REWRITE_TAC [ADD_COMM] \\ REWRITE_TAC [FUNPOW_COMP] 1822 \\ PAT_X_ASSUM `~FST (DUR_X x0)` MP_TAC 1823 \\ ASM_SIMP_TAC (bossLib.std_ss++STATE_INP_ss) 1824 [Abbr`x`,Abbr`x0`,ADVANCE_def,SINIT_def,SNEXT,numeral_funpow] 1825 \\ ASM_SIMP_TAC stdi_ss [DUR_X2,DUR_IC_def,INIT_ARM6] \\ POP_LAST_TAC 1826 \\ STRIP_TAC 1827 \\ `~IS_RESET inp 0 /\ ~IS_RESET inp 1` by ASM_SIMP_TAC arith_ss [] 1828 \\ IMP_RES_TAC NOT_RESET_EXISTS2 1829 \\ iclass_compLib.STM_TAC \\ ALU_ABBREV_TAC 1830 \\ SIMP_TAC (stdi_ss++boolSimps.CONJ_ss++PBETA_ss) 1831 [FST_COND_RAND,SND_COND_RAND,LSL_ZERO,MASKN_1] 1832 \\ Cases_on `(15 >< 0) ireg = 0w:word16` 1833 \\ ASM_SIMP_TAC stdi_ss [PENCZ_THM3,IN_LDM_STM] 1834 << [ 1835 IMP_RES_TAC PENCZ_THM2 1836 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) [Abbr`w`,FUNPOW] 1837 \\ STRIP_TAC \\ UNABBREV_TAC `s` \\ CONJ_TAC >> FINISH_OFF 1838 \\ IMP_RES_TAC DECODE_INST_STM 1839 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) 1840 ([Abbr`alu`,LSL_ZERO,ALUOUT_ALU_logic,WB_ADDRESS_ZERO,IN_LDM_STM, 1841 (REWRITE_RULE [] o SPEC `0w`) PENCZ_THM2] @ finish_rws3) 1842 \\ RW_TAC std_ss finish_rws2, 1843 `~PENCZ stm ((15 >< 0) ireg) UINT_MAXw` 1844 by (FULL_SIMP_TAC std_ss [PENCZ_THM2] \\ 1845 METIS_TAC [STM_PENCZ_ZERO,NOT_ZERO_LT_ZERO]) 1846 \\ Cases_on `w = 1` 1847 << [ 1848 `PENCZ stm ((15 >< 0) ireg) (MASKN 1 ((15 >< 0) ireg))` 1849 by PROVE_TAC [PENCZ_THM,IN_LDM_STM] 1850 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) [Abbr`w`,FUNPOW] 1851 \\ STRIP_TAC \\ UNABBREV_TAC `s` \\ CONJ_TAC >> FINISH_OFF 1852 \\ IMP_RES_TAC DECODE_INST_STM 1853 \\ ASM_SIMP_TAC (stdi_ss++ARITH_ss++STATE_INP_ss) 1854 ([Abbr`alu`,LSL_ZERO,ALUOUT_ALU_logic,GSYM WB_ADDRESS, 1855 IN_LDM_STM] @ finish_rws3) 1856 \\ RW_TAC std_ss finish_rws2, 1857 `1 < w` by FULL_SIMP_TAC arith_ss [Abbr`w`,PENCZ_THM2] 1858 \\ `~(PENCZ stm ((15 >< 0) ireg) (MASKN 1 ((15 >< 0) ireg)))` 1859 by PROVE_TAC [PENCZ_THM,IN_LDM_STM] 1860 \\ ASM_SIMP_TAC stdi_ss [LSL_ZERO,MASK_def,GSYM ADVANCE_COMP] 1861 \\ IMP_RES_TAC (simpLib.SIMP_PROVE arith_ss [] 1862 ``!w. 1 < w ==> (!t. t < 2 + (w - 1) ==> ~IS_RESET i t) ==> 1863 (!t. t < SUC w ==> ~IS_RESET i t)``) 1864 \\ ABBREV_TAC `cpsr = CPSR_READ psr` 1865 \\ IMP_RES_TAC NEXT_CORE_STM_TN_W1 1866 \\ POP_ASSUM (STRIP_ASSUME_TAC o 1867 (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV (SKOLEM_CONV))))) 1868 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) [MASKN_2] 1869 \\ POP_ASSUM (ASSUME_TAC o GEN_ALL o (MATCH_MP 1870 (DECIDE ``a /\ b /\ c /\ d ==> a /\ b /\ c``)) o SPEC_ALL) 1871 \\ PAT_TAC 25 1872 \\ `~(aregn IN {0w; 1w; 2w; 5w}) /\ 1873 ((aregn = 7w) ==> ~(CPSR_READ psr %% 6)) /\ 1874 ((aregn = 6w) ==> ~(CPSR_READ psr %% 7))` 1875 by METIS_TAC [] 1876 \\ markerLib.RM_ABBREV_TAC "aregn" 1877 \\ PAT_X_ASSUM `!sctrlreg reg psrfb. P` (K ALL_TAC) 1878 \\ STRIP_TAC \\ UNABBREV_TAC `s` \\ CONJ_TAC 1879 << [ 1880 FINISH_OFF 1881 \\ FULL_SIMP_TAC (std_ss++PRED_SET_ss++SIZES_ss) [n2w_11], 1882 IMP_RES_TAC DECODE_INST_STM 1883 \\ ASM_SIMP_TAC (stdi_ss++ARITH_ss++STATE_INP_ss) 1884 ([Abbr`alu`,Abbr`cpsr`,LSL_ZERO,ALUOUT_ALU_logic, 1885 GSYM WB_ADDRESS,IN_LDM_STM] @ finish_rws3) 1886 \\ RW_TAC std_ss finish_rws2]]]); 1887 1888(* ------------------------------------------------------------------------- *) 1889 1890val lem = (GEN_ALL o BETA_RULE o 1891 ISPEC `\t. OUT_ARM6 ((FUNPOW (SNEXT NEXT_ARM6) t x).state)`) FILTER_MEMOP_ALL; 1892 1893val _ = print "*\nVerifying output\n*\n"; (*=================================*) 1894 1895val ARM6_OUT_THM = prove( 1896 `!x. (x = ^arm6state_inp) ==> inp IN STRM_ARM6 ==> 1897 (OUTPUT ARM_SPEC <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> 0 = 1898 OSMPL OSMPL_ARM6 ARM6_SPEC IMM_ARM6 (x,OUTPUT ARM6_SPEC x) 0)`, 1899 RW_TAC std_ss [] 1900 \\ SIMP_TAC (srw_ss()++boolSimps.LET_ss) [OUTPUT_def,ARM_SPEC_def, 1901 ARM6_SPEC_def,STATE_ARM6_COR,STATE_ARM_def,FUNPOW,ADVANCE_ZERO, 1902 IMM_LEN_def,OSMPL_def,SINIT_def,SUC2NUM IMM_ARM6_def,MAP_STRM_def, 1903 PACK_def] 1904 \\ ABBREV_TAC `x = ^arm6state_inp` \\ ABBREV_TAC `x0 = SINIT INIT_ARM6 x` 1905 \\ `(<|state := INIT_ARM6 (^arm6state); inp := inp|> = x0)` 1906 by RW_TAC std_ss [Abbr`x`,Abbr`x0`,SINIT_def] 1907 \\ POP_ASSUM SUBST1_TAC 1908 \\ `^arm6state = x.state` by RW_TAC std_ss [Abbr`x`] 1909 \\ POP_ASSUM SUBST1_TAC 1910 \\ IMP_RES_TAC INIT_INIT 1911 \\ Cases_on `FST (DUR_X x0) \/ (DECODE_INST ireg = mcr) \/ 1912 (DECODE_INST ireg = ldc) \/ (DECODE_INST ireg = stc)` 1913 << [ (* reset *) 1914 ASM_SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,ABS_ARM6_def,OSMPL_ARM6_def], 1915 FULL_SIMP_TAC std_ss [] 1916 \\ Cases_on `(aregn2 = 2w:word3) ==> 1917 ~CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg` 1918 << [ (* exception or not executed *) 1919 IMP_RES_TAC NON_MEMOPS_UNEXEC 1920 \\ FULL_SIMP_TAC stdi_ss [IMP_DISJ_THM,OSMPL_ARM6_def,MAP] 1921 \\ ASM_SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,ABS_ARM6_def, 1922 OUT_ARM_def,DECODE_PSR_def,num2exception_word3], 1923 FULL_SIMP_TAC bool_ss [] 1924 \\ `2w:word3 = 2w` by SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 1925 \\ Cases_on `DECODE_INST ireg = ldm` >> IMP_RES_TAC LDM_MEMOPS 1926 \\ Cases_on `DECODE_INST ireg = stm` >> IMP_RES_TAC STM_MEMOPS 1927 \\ Cases_on `DECODE_INST ireg IN {swp; ldr; str}` 1928 >> IMP_RES_TAC BASIC_MEMOPS 1929 \\ Cases_on `DECODE_INST ireg IN {mrs_msr; data_proc; 1930 reg_shift; br; swi_ex; unexec}` 1931 << [ 1932 IMP_RES_TAC NON_MEMOPS \\ POP_LASTN_TAC 2 1933 \\ FULL_SIMP_TAC (stdi_ss++PRED_SET_ss++STATE_INP_ss) 1934 [Abbr`x`,OSMPL_ARM6_def,ABS_ARM6_def,OUT_ARM_def, 1935 DECODE_PSR_def,MAP], 1936 Cases_on `DECODE_INST ireg IN {cdp_und; mrc}` 1937 << [ 1938 IMP_RES_TAC CP_MEMOPS \\ POP_LAST_TAC \\ IMP_RES_TAC lem 1939 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) [Abbr`x`, 1940 OSMPL_ARM6_def,ABS_ARM6_def,OUT_ARM_def, 1941 DECODE_PSR_def,MAP,CP_NOT,CP_NOT2], 1942 `DECODE_INST ireg = mla_mul` 1943 by (Cases_on `DECODE_INST ireg` \\ 1944 FULL_SIMP_TAC (bossLib.bool_ss++PRED_SET_ss) []) 1945 \\ IMP_RES_TAC MEM_MLA_MUL \\ POP_LAST_TAC 1946 \\ IMP_RES_TAC lem 1947 \\ ASM_SIMP_TAC (stdi_ss++STATE_INP_ss) 1948 [Abbr`x`,OSMPL_ARM6_def,ABS_ARM6_def,OUT_ARM_def, 1949 DECODE_PSR_def,MAP]]]]]); 1950 1951val ARM6_OUT_THM = GEN_ALL (SIMP_RULE (srw_ss()) [] ARM6_OUT_THM); 1952 1953(* ------------------------------------------------------------------------- *) 1954 1955val FST_DUR_X = prove( 1956 `!x. FST (DUR_X x) ==> 1957 (?t. IS_RESET x.inp t) /\ 1958 (DUR_ARM6 x = 1959 (LEAST t. IS_RESET x.inp t /\ ~IS_RESET x.inp (t + 1) /\ 1960 ~IS_RESET x.inp (t + 2)) + 3)`, 1961 Cases \\ Cases_on_arm6 `a` 1962 \\ RW_TAC std_ss [DUR_X_def,DECODE_PSR_def,DUR_ARM6_def] 1963 \\ METIS_TAC []); 1964 1965val _ = print "*\nVerifying time-consistency\n*\n"; (*=======================*) 1966 1967val ARM6_TCON_LEM1 = prove( 1968 `!x. (x = ^arm6state_inp) ==> inp IN STRM_ARM6 ==> 1969 (INIT_ARM6 (STATE_ARM6 (IMM_ARM6 x 1) x) = STATE_ARM6 (IMM_ARM6 x 1) x)`, 1970 RW_TAC bool_ss [] 1971 \\ SIMP_TAC (srw_ss()++boolSimps.LET_ss) [ARM6_SPEC_def,STATE_ARM6_COR, 1972 FUNPOW,ADVANCE_ZERO,SINIT_def,SUC2NUM IMM_ARM6_def] 1973 \\ ABBREV_TAC `x = ^arm6state_inp` \\ ABBREV_TAC `x0 = SINIT INIT_ARM6 x` 1974 \\ `(<|state := INIT_ARM6 (^arm6state); inp := inp|> = x0)` 1975 by RW_TAC std_ss [Abbr`x`,Abbr`x0`,SINIT_def] 1976 \\ POP_ASSUM SUBST1_TAC 1977 \\ Cases_on `FST (DUR_X x0)` 1978 << [ (* reset *) 1979 PAT_X_ASSUM `inp IN STRM_ARM6` (fn th => `x0.inp IN STRM_ARM6` 1980 by ASM_SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x0`,Abbr`x`,SINIT_def,th]) 1981 \\ MAP_EVERY IMP_RES_TAC [FST_DUR_X,LEAST_NOT_RESET] 1982 \\ PAT_X_ASSUM `IS_RESET x0.inp t` (K ALL_TAC) 1983 \\ MAP_EVERY IMP_RES_TAC [LEAST_RESET_GT_TWO,PREVIOUS_THREE_RESET] 1984 \\ REPEAT (PAT_X_ASSUM `~a ==> b` (K ALL_TAC)) 1985 \\ IMP_RES_TAC (DECIDE ``!n. (2 < n) ==> (n = n - 3 + 3)``) 1986 \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [th] \\ 1987 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [th])) 1988 \\ ASM_REWRITE_TAC [DECIDE ``!a. a + 3 + 3 = 6 + a``] 1989 \\ REWRITE_TAC [FUNPOW_COMP] 1990 \\ PAT_ABBREV_TAC `y = FUNPOW (SNEXT NEXT_ARM6) xt x0` 1991 \\ RULE_ASSUM_TAC (ONCE_REWRITE_RULE [GSYM STATE_FUNPOW_INIT2]) 1992 \\ UNABBREV_TAC `y` 1993 \\ PAT_ABBREV_TAC `y = (FUNPOW (SNEXT NEXT_ARM6) xt x0).state` 1994 \\ IMP_RES_TAC SPEC_AFTER_NRESET2 1995 \\ POP_ASSUM (SPEC_THEN `y` ASSUME_TAC) 1996 \\ FULL_SIMP_TAC (arith_ss++STATE_INP_ss) [AFTER_NRESET2_THM3], 1997 Cases_on `(aregn2 = 2w) ==> ~CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg` 1998 >> IMP_RES_TAC (SIMP_RULE std_ss [] NON_MEMOPS_UNEXEC) 1999 \\ FULL_SIMP_TAC bool_ss [] 2000 \\ `2w:word3 = 2w` by SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 2001 \\ `DECODE_INST ireg IN {cdp_und; mrc; mcr; stc; ldc} \/ 2002 DECODE_INST ireg IN {mrs_msr; data_proc; reg_shift; 2003 br; swi_ex; unexec} \/ 2004 DECODE_INST ireg IN {swp; ldr; str} \/ 2005 (DECODE_INST ireg = mla_mul) \/ 2006 (DECODE_INST ireg = ldm) \/ 2007 (DECODE_INST ireg = stm)` 2008 by (SIMP_TAC (std_ss++PRED_SET_ss) [] \\ 2009 Cases_on `DECODE_INST ireg` \\ ASM_REWRITE_TAC []) 2010 << (map (IMP_RES_TAC o (SIMP_RULE std_ss [])) 2011 [CP_TC,NON_MEMOPS,BASIC_MEMOPS,MLA_MUL,LDM,STM]) 2012 ] (* reset *) 2013); 2014 2015val ARM6_TCON_ONE = GEN_ALL (SIMP_RULE bool_ss [] ARM6_TCON_LEM1); 2016 2017val _ = print "*\nVerifying correctness\n*\n"; (*============================*) 2018 2019val ARM6_COR_LEM1 = prove( 2020 `!x. (x = ^arm6state_inp) ==> inp IN STRM_ARM6 ==> 2021 (STATE_ARM 1 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 2022 ABS_ARM6 (STATE_ARM6 (IMM_ARM6 x 1) x))`, 2023 RW_TAC bool_ss [] 2024 \\ SIMP_TAC (srw_ss()++boolSimps.LET_ss) [ARM6_SPEC_def,STATE_ARM6_COR, 2025 FUNPOW,ADVANCE_ZERO,SINIT_def,SUC2NUM IMM_ARM6_def] 2026 \\ ABBREV_TAC `x = ^arm6state_inp` \\ ABBREV_TAC `x0 = SINIT INIT_ARM6 x` 2027 \\ `^arm6state = x.state` by RW_TAC std_ss [Abbr`x`] 2028 \\ `(<|state := INIT_ARM6 (^arm6state); inp := inp|> = x0)` 2029 by RW_TAC std_ss [Abbr`x`,Abbr`x0`,SINIT_def] 2030 \\ NTAC 2 (POP_ASSUM SUBST1_TAC) 2031 \\ Cases_on `FST (DUR_X x0)` 2032 << [ 2033 PAT_X_ASSUM `inp IN STRM_ARM6` (fn th => `x0.inp IN STRM_ARM6` 2034 by ASM_SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x0`,Abbr`x`,SINIT_def,th]) 2035 \\ MAP_EVERY IMP_RES_TAC [FST_DUR_X,LEAST_NOT_RESET] 2036 \\ `<|state := x0.state; inp := x.inp|> = x0` 2037 by SIMP_TAC (std_ss++STATE_INP_ss) [Abbr`x`,Abbr`x0`,SINIT_def] 2038 \\ ASM_SIMP_TAC (arith_ss++STATE_INP_ss) 2039 [SUC2NUM STATE_ARM_def,SMPL_ARM6_def,COMBINE_def,SMPL_EXC_ARM6_def, 2040 SMPL_DATA_ARM6_def,SUC2NUM IMM_ARM6_def,SUC2NUM STATE_ARM6_COR, 2041 MAP_STRM_def,FUNPOW,ADVANCE_ZERO,NEXT_ARM_def] 2042 \\ POP_LAST_TAC 2043 \\ PAT_X_ASSUM `IS_RESET x0.inp t` (K ALL_TAC) 2044 \\ MAP_EVERY IMP_RES_TAC [LEAST_RESET_GT_TWO,PREVIOUS_THREE_RESET] 2045 \\ REPEAT (PAT_X_ASSUM `~a ==> b` (K ALL_TAC)) 2046 \\ IMP_RES_TAC (DECIDE ``!n. (2 < n) ==> (n = n - 3 + 3)``) 2047 \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [th] \\ 2048 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [th])) 2049 \\ ASM_REWRITE_TAC [DECIDE ``!a. a + 3 + 3 = 6 + a``] 2050 \\ REWRITE_TAC [FUNPOW_COMP] 2051 \\ PAT_ABBREV_TAC `y = FUNPOW (SNEXT NEXT_ARM6) xt x0` 2052 \\ RULE_ASSUM_TAC (ONCE_REWRITE_RULE [GSYM STATE_FUNPOW_INIT2]) 2053 \\ UNABBREV_TAC `y` 2054 \\ PAT_ABBREV_TAC `y = (FUNPOW (SNEXT NEXT_ARM6) xt x0).state` 2055 \\ IMP_RES_TAC SPEC_AFTER_NRESET2 2056 \\ POP_ASSUM (SPEC_THEN `y` ASSUME_TAC) 2057 \\ POP_ASSUM_LIST (fn thl => ASSUME_TAC (hd thl)) 2058 \\ FULL_SIMP_TAC arith_ss [AFTER_NRESET2_THM4], 2059 Cases_on `(aregn2 = 2w) ==> ~CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg` 2060 >> IMP_RES_TAC (SIMP_RULE std_ss [] NON_MEMOPS_UNEXEC) 2061 \\ FULL_SIMP_TAC bool_ss [] 2062 \\ `2w:word3 = 2w` by SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 2063 \\ `DECODE_INST ireg IN {cdp_und; mrc; mcr; stc; ldc} \/ 2064 DECODE_INST ireg IN {mrs_msr; data_proc; reg_shift; 2065 br; swi_ex; unexec} \/ 2066 DECODE_INST ireg IN {swp; ldr; str} \/ 2067 (DECODE_INST ireg = mla_mul) \/ 2068 (DECODE_INST ireg = ldm) \/ 2069 (DECODE_INST ireg = stm)` 2070 by (SIMP_TAC (std_ss++PRED_SET_ss) [] \\ 2071 Cases_on `DECODE_INST ireg` \\ ASM_REWRITE_TAC []) 2072 << (map (IMP_RES_TAC o (SIMP_RULE std_ss [])) 2073 [CP_TC,NON_MEMOPS,BASIC_MEMOPS,MLA_MUL,LDM,STM]) 2074 ] (* reset *) 2075); 2076 2077val ARM6_COR_ONE = GEN_ALL (SIMP_RULE (std_ss++STATE_INP_ss) [] ARM6_COR_LEM1); 2078 2079(* ------------------------------------------------------------------------- *) 2080 2081val DUR_IC_WELL = prove( 2082 `!ic ireg rs iflags inp. 0 < DUR_IC ic ireg rs iflags inp`, 2083 RW_TAC arith_ss [DUR_IC_def]); 2084 2085val DUR_ARM6_WELL = store_thm("DUR_ARM6_WELL", 2086 `!x. 0 < DUR_ARM6 x`, 2087 Cases \\ Cases_on_arm6 `a` 2088 \\ RW_TAC arith_ss [DECODE_PSR_def,DUR_ARM6_def,DUR_X_def,DUR_IC_WELL]); 2089 2090val IMM_ARM6_THM = store_thm("IMM_ARM6_THM", 2091 `UIMMERSION IMM_ARM6 ARM6_SPEC DUR_ARM6`, 2092 RW_TAC stdi_ss [UIMMERSION_def,DUR_ARM6_WELL,IMM_ARM6_def,ARM6_SPEC_def]); 2093 2094val IMM_ARM6_UNIFORM = store_thm("IMM_ARM6_UNIFORM", 2095 `UNIFORM IMM_ARM6 ARM6_SPEC`, 2096 REWRITE_TAC [UNIFORM_def] 2097 \\ EXISTS_TAC `DUR_ARM6` 2098 \\ REWRITE_TAC [IMM_ARM6_THM]); 2099 2100val IMM_ARM6_ONE = 2101 MATCH_MP UIMMERSION_ONE (CONJ STATE_ARM6_IMAP_INIT IMM_ARM6_THM); 2102 2103(* ------------------------------------------------------------------------- *) 2104 2105val ARM6_DATA_ABSTRACTION = store_thm("ARM6_DATA_ABSTRACTION", 2106 `DATA_ABSTRACTION ABS_ARM6 2107 (state_out_state o ARM6_SPEC 0) (state_out_state o ARM_SPEC 0)`, 2108 RW_TAC bool_ss [MATCH_MP DATA_ABSTRACTION_I 2109 (CONJ STATE_ARM_THM3 STATE_ARM6_IMAP_INIT)] 2110 \\ Cases_on `a` 2111 \\ Q.MATCH_ABBREV_TAC `?b. ABS_ARM6 (INIT_ARM6 b) = ARM_EX s c e` 2112 \\ markerLib.RM_ALL_ABBREVS_TAC \\ Cases_on `s` 2113 \\ EXISTS_TAC `ARM6 (DP (ADD8_PC f) f0 areg din alua alub dout) 2114 (CTRL pipea pipeaval pipeb pipebval c iregval ointstart onewinst endinst 2115 obaselatch opipebll nxtic nxtis nopc1 oorst resetlatch onfq ooonfq 2116 oniq oooniq pipeaabt pipebabt iregabt2 dataabt2 (n2w (exception2num e)) 2117 mrq2 nbw nrw sctrlreg psrfb oareg mask orp oorp mul mul2 borrow2 mshift)` 2118 \\ SIMP_TAC std_ss [ABS_ARM6_def,SUB8_INV,INIT_ARM6_def] 2119 \\ Cases_on `e` \\ SIMP_TAC (std_ss++SIZES_ss) 2120 [exception2num_thm,num2exception_thm,w2n_n2w]); 2121 2122(* ------------------------------------------------------------------------- *) 2123 2124val STRM_ARM6_LEM = prove( 2125 `!x. (x = ^arm6state_inp) ==> 2126 inp IN STRM_ARM6 ==> PROJ_NRESET (inp (IMM_ARM6 x 1 - 1))`, 2127 REPEAT STRIP_TAC 2128 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss++STATE_INP_ss) [IFLAGS_def, 2129 IMM_ARM6_ONE,INIT_ARM6_def,DUR_ARM6_def,DUR_X,DECODE_PSR_def] 2130 \\ COND_CASES_TAC 2131 << [ 2132 POP_ASSUM MP_TAC \\ PAT_ABBREV_TAC `d = DUR_IC xic xireg xrs xiflags xi` 2133 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2134 \\ POP_ASSUM (SPEC_THEN `d - 1` ASSUME_TAC) 2135 \\ UNABBREV_TAC `d` 2136 \\ FULL_SIMP_TAC arith_ss [IS_RESET_def,DUR_IC_WELL], 2137 FULL_SIMP_TAC std_ss [(REWRITE_RULE [PROVE [] ``(~a = b) = (a = ~b)``] o 2138 GSYM) IS_RESET_def] 2139 \\ IMP_RES_TAC LEAST_NOT_RESET 2140 \\ ASM_SIMP_TAC arith_ss []]); 2141 2142val lem = simpLib.SIMP_PROVE (srw_ss()) 2143 [io_onestepTheory.state_inp_component_equality] 2144 ``state_inp a b = <|state:= a; inp := b|>``; 2145 2146val STRM_ARM6_LEMb = prove( 2147 `!x. x.inp IN STRM_ARM6 ==> ~IS_RESET x.inp (IMM_ARM6 x 1 - 1)`, 2148 Cases \\ Cases_on_arm6 `a` \\ SIMP_TAC (std_ss++STATE_INP_ss) 2149 [lem,IS_RESET_def,GEN_ALL (SIMP_RULE bool_ss [] STRM_ARM6_LEM)]); 2150 2151val STRM_ARM6_THM = store_thm("STRM_ARM6_THM", 2152 `!x t. x.inp IN STRM_ARM6 ==> (ADVANCE (IMM_ARM6 x 1) x.inp) IN STRM_ARM6`, 2153 REPEAT STRIP_TAC \\ IMP_RES_TAC STRM_ARM6_LEMb 2154 \\ FULL_SIMP_TAC bool_ss [IN_DEF,STRM_ARM6_def,ADVANCE_def,IS_RESET_def, 2155 IS_BUSY_def,IS_ABSENT_def] 2156 \\ REPEAT STRIP_TAC 2157 << [ 2158 PAT_X_ASSUM `!t. ~PROJ_NRESET (x.inp t) ==> b` 2159 (SPEC_THEN `IMM_ARM6 x 1 + t` IMP_RES_TAC) 2160 \\ Cases_on `t` 2161 \\ FULL_SIMP_TAC arith_ss [ADD1], 2162 PAT_X_ASSUM `!t. ?t2. t < t2 /\ PROJ_NRESET (x.inp t2) /\ b` 2163 (SPEC_THEN `IMM_ARM6 x 1 + t` STRIP_ASSUME_TAC), 2164 PAT_X_ASSUM `!t. ?t2. P` 2165 (SPEC_THEN `IMM_ARM6 x 1 + t` STRIP_ASSUME_TAC), 2166 PAT_X_ASSUM `!t. ~PROJ_CPB (x.inp t) ==> p` 2167 (SPEC_THEN `IMM_ARM6 x 1 + t` IMP_RES_TAC)] 2168 \\ EXISTS_TAC `t2 - IMM_ARM6 x 1` 2169 \\ ASM_SIMP_TAC arith_ss []); 2170 2171val ARM6_STREAM_ABSTRACTION = store_thm("ARM6_STREAM_ABSTRACTION", 2172 `STREAM_ABSTRACTION SMPL_ARM6 UNIV STRM_ARM6`, 2173 RW_TAC std_ss [STREAM_ABSTRACTION_def,pred_setTheory.IN_UNIV] 2174 \\ EXISTS_TAC `\t. (T,T,F,F,word_0,T,T)` 2175 \\ SIMP_TAC std_ss [IN_DEF,STRM_ARM6_def,IS_RESET_def,IS_ABSENT_def, 2176 IS_BUSY_def,PROJ_NRESET_def,PROJ_CPA_def,PROJ_CPB_def] 2177 \\ STRIP_TAC \\ EXISTS_TAC `t + 1` \\ DECIDE_TAC); 2178 2179(* ------------------------------------------------------------------------- *) 2180 2181val ARM6_TCON_LEM0 = store_thm("ARM6_TCON_LEM0", 2182 `!x. (x = ^arm6state_inp) ==> 2183 (INIT_ARM6 (STATE_ARM6 (IMM_ARM6 x 0) x) = STATE_ARM6 (IMM_ARM6 x 0) x)`, 2184 RW_TAC bool_ss [] 2185 \\ SIMP_TAC (std_ss++STATE_INP_ss) 2186 [STATE_ARM6_def,IMM_ARM6_def,INIT_ARM6_def,NXTIC_def,MASK_def]); 2187 2188val ARM6_TCON_ZERO = GEN_ALL (SIMP_RULE bool_ss [] ARM6_TCON_LEM0); 2189 2190val INIT = REWRITE_RULE [GSYM FUN_EQ_THM] (CONJUNCT1 STATE_ARM6_def); 2191 2192val ARM6_TIME_CON_IMM = store_thm("ARM6_TIME_CON_IMM", 2193 `TCON_IMMERSION ARM6_SPEC IMM_ARM6 STRM_ARM6`, 2194 SIMP_TAC bool_ss [STRM_ARM6_THM,MATCH_MP TCON_IMMERSION_ONE_STEP_THM 2195 (CONJ STATE_ARM6_IMAP_INIT IMM_ARM6_UNIFORM)] 2196 \\ REPEAT STRIP_TAC 2197 \\ Cases_on `x` \\ Cases_on_arm6 `a` 2198 \\ FULL_SIMP_TAC (std_ss++STATE_INP_ss) [lem,ARM6_SPEC_STATE,INIT, 2199 ARM6_TCON_ZERO,ARM6_TCON_ONE]); 2200 2201(* ------------------------------------------------------------------------- *) 2202 2203val lem2 = prove( 2204 `(!t1 t2 i. IS_ABORT (ADVANCE t1 i) t2 = IS_ABORT i (t1 + t2)) /\ 2205 !t1 t2 i. IS_BUSY (ADVANCE t1 i) t2 = IS_BUSY i (t1 + t2)`, 2206 REPEAT STRIP_TAC 2207 \\ REWRITE_TAC [FUN_EQ_THM] 2208 \\ SIMP_TAC arith_ss [IS_ABORT_def,IS_BUSY_def,ADVANCE_def]); 2209 2210val TCON_SMPL_ARM6 = prove( 2211 `TCON_SMPL SMPL_ARM6 IMM_ARM6 ARM6_SPEC STRM_ARM6`, 2212 RW_TAC std_ss [TCON_SMPL_def] 2213 \\ REWRITE_TAC [FUN_EQ_THM] 2214 \\ MAP_EVERY ASSUME_TAC [STATE_ARM6_IMAP,IMM_ARM6_UNIFORM,ARM6_TIME_CON_IMM] 2215 \\ IMP_RES_TAC (GSYM TCON_IMMERSION_COR) 2216 \\ X_GEN_TAC `t2` \\ Cases_on `x` 2217 \\ ABBREV_TAC `inp = f` \\ markerLib.RM_ABBREV_TAC "inp" 2218 \\ `state_inp a inp = <| state:= a; inp := inp |>` 2219 by (SIMP_TAC (srw_ss()) [state_inp_component_equality]) 2220 \\ FULL_SIMP_TAC (arith_ss++STATE_INP_ss) [GSYM ARM6_SPEC_STATE, 2221 COMBINE_def,SMPL_ARM6_def,ADVANCE_def,GSYM ADVANCE_COMP,lem2, 2222 SMPL_EXC_ARM6_def,SMPL_DATA_ARM6_def,MAP_STRM_def,PACK_def, 2223 IMM_LEN_def,ADVANCE_def, 2224 (GSYM o SIMP_RULE (srw_ss()) [] o GEN_ALL o 2225 INST [`x` |-> `<| state:= a; inp := inp |>`] o SPEC_ALL o 2226 SIMP_RULE std_ss [TCON_IMMERSION_def]) ARM6_TIME_CON_IMM] 2227 \\ POP_ASSUM (K ALL_TAC) 2228 \\ POP_ASSUM (fn th => REWRITE_TAC [(GSYM o SPECL [`t2 + 1`,`t`]) th, 2229 (GSYM o SPECL [`t2`,`t`]) th] \\ ASSUME_TAC th) 2230 \\ SIMP_TAC arith_ss []); 2231 2232(* ------------------------------------------------------------------------- *) 2233 2234val ARM6_COR_LEM0 = store_thm("ARM6_COR_LEM0", 2235 `!x. (x = ^arm6state_inp) ==> 2236 (STATE_ARM 0 <|state := ABS_ARM6 x.state; inp := SMPL_ARM6 x|> = 2237 ABS_ARM6 (STATE_ARM6 (IMM_ARM6 x 0) x))`, 2238 RW_TAC bool_ss [] 2239 \\ SIMP_TAC (std_ss++STATE_INP_ss) [STATE_ARM_def,STATE_ARM6_def, 2240 IMM_ARM6_def,INIT_ARM6_def,ABS_ARM6_def]); 2241 2242val ARM6_COR_ZERO = GEN_ALL (SIMP_RULE (srw_ss()) [] ARM6_COR_LEM0); 2243 2244(* ------------------------------------------------------------------------- *) 2245 2246val CORRECT_ARM6 = store_thm("CORRECT_ARM6", 2247 `CORRECT ARM_SPEC ARM6_SPEC IMM_ARM6 ABS_ARM6 2248 (OSMPL OSMPL_ARM6 ARM6_SPEC IMM_ARM6) SMPL_ARM6 UNIV STRM_ARM6`, 2249 MATCH_MP_TAC ONE_STEP_THM 2250 \\ EXISTS_TAC `OSMPL_ARM6` 2251 \\ SIMP_TAC std_ss [STATE_ARM_THM2,STATE_ARM6_IMAP,IMM_ARM6_UNIFORM, 2252 ARM6_DATA_ABSTRACTION,ARM6_STREAM_ABSTRACTION, 2253 REWRITE_RULE [TCONa_def] (MATCH_MP TCON_I_THMa STATE_ARM_THM3), 2254 ARM6_TIME_CON_IMM,TCON_SMPL_ARM6] 2255 \\ REPEAT STRIP_TAC 2256 \\ Cases_on `x` \\ Cases_on_arm6 `a` 2257 \\ FULL_SIMP_TAC (std_ss++STATE_INP_ss) 2258 [lem,ARM6_SPEC_STATE,ARM_SPEC_STATE,ARM6_COR_ZERO,ARM6_COR_ONE, 2259 ARM6_OUT_THM]); 2260 2261(* ------------------------------------------------------------------------- *) 2262 2263val _ = export_theory(); 2264