1 2open HolKernel boolLib bossLib Parse; 3open pred_setTheory res_quanTheory wordsTheory wordsLib bitTheory arithmeticTheory; 4open listTheory pairTheory combinTheory addressTheory; 5open finite_mapTheory; 6 7open set_sepTheory progTheory; 8open armTheory arm_coretypesTheory arm_stepTheory armLib; 9 10val _ = new_theory "prog_arm"; 11 12infix \\ 13val op \\ = op THEN; 14 15val RW = REWRITE_RULE; 16val RW1 = ONCE_REWRITE_RULE; 17 18 19(* ----------------------------------------------------------------------------- *) 20(* The ARM set *) 21(* ----------------------------------------------------------------------------- *) 22 23val _ = Hol_datatype ` 24 arm_el = aReg of word4 => word32 25 | aMem of word32 => word8 26 | aStatus of arm_bit => bool 27 | aCPSR_Reg of word32 28 | aUndef of bool`; 29 30val arm_el_11 = DB.fetch "-" "arm_el_11"; 31val arm_el_distinct = DB.fetch "-" "arm_el_distinct"; 32 33val _ = Parse.type_abbrev("arm_set",``:arm_el set``); 34 35 36(* ----------------------------------------------------------------------------- *) 37(* Converting from ARM-state record to arm_set *) 38(* ----------------------------------------------------------------------------- *) 39 40val ARM_OK_def = Define ` 41 ARM_OK state = 42 (ARM_ARCH state = ARMv6) /\ (ARM_EXTENSIONS state = {}) /\ 43 (ARM_UNALIGNED_SUPPORT state) /\ (ARM_READ_EVENT_REGISTER state) /\ 44 ~(ARM_READ_INTERRUPT_WAIT state) /\ ~(ARM_READ_SCTLR sctlrV state) /\ 45 (ARM_READ_SCTLR sctlrA state) /\ ~(ARM_READ_SCTLR sctlrU state) /\ 46 (ARM_READ_IT state = 0w) /\ ~(ARM_READ_STATUS psrJ state) /\ 47 ~(ARM_READ_STATUS psrT state) /\ ~(ARM_READ_STATUS psrE state) /\ 48 (ARM_MODE state = 16w)`; 49 50val ARM_READ_UNDEF_def = Define `ARM_READ_UNDEF s = ~(ARM_OK s)`; 51 52val ARM_READ_MASKED_CPSR_def = Define ` 53 ARM_READ_MASKED_CPSR s = (26 '' 0) (encode_psr (ARM_READ_CPSR s))`; 54 55val arm2set'_def = Define ` 56 arm2set' (rs,ms,st,cp,ud) (s:arm_state) = 57 IMAGE (\a. aReg a (ARM_READ_REG a s)) rs UNION 58 IMAGE (\a. aMem a (ARM_READ_MEM a s)) ms UNION 59 IMAGE (\a. aStatus a (ARM_READ_STATUS a s)) st UNION 60 (if cp then { aCPSR_Reg (ARM_READ_MASKED_CPSR s) } else {}) UNION 61 (if ud then { aUndef (ARM_READ_UNDEF s) } else {})`; 62 63val arm2set_def = Define `arm2set s = arm2set' (UNIV,UNIV,UNIV,T,T) s`; 64val arm2set''_def = Define `arm2set'' x s = arm2set s DIFF arm2set' x s`; 65 66(* theorems *) 67 68val arm2set'_SUBSET_arm2set = prove( 69 ``!y s. arm2set' y s SUBSET arm2set s``, 70 Cases_on `y` \\ Cases_on `r` \\ Cases_on `r'` \\ Cases_on `r` 71 \\ SIMP_TAC std_ss [SUBSET_DEF,arm2set'_def,arm2set_def,IN_IMAGE,IN_UNION,IN_UNIV] 72 \\ METIS_TAC [NOT_IN_EMPTY]); 73 74val SPLIT_arm2set = prove( 75 ``!x s. SPLIT (arm2set s) (arm2set' x s, arm2set'' x s)``, 76 REPEAT STRIP_TAC 77 \\ ASM_SIMP_TAC std_ss [SPLIT_def,EXTENSION,IN_UNION,IN_DIFF,arm2set''_def] 78 \\ `arm2set' x s SUBSET arm2set s` by METIS_TAC [arm2set'_SUBSET_arm2set] 79 \\ SIMP_TAC bool_ss [DISJOINT_DEF,EXTENSION,IN_INTER,NOT_IN_EMPTY,IN_DIFF] 80 \\ METIS_TAC [SUBSET_DEF]); 81 82val PUSH_IN_INTO_IF = METIS_PROVE [] 83 ``!g x y z. x IN (if g then y else z) = if g then x IN y else x IN z``; 84 85val SUBSET_arm2set = prove( 86 ``!u s. u SUBSET arm2set s = ?y. u = arm2set' y s``, 87 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 88 \\ ASM_REWRITE_TAC [arm2set'_SUBSET_arm2set] 89 \\ Q.EXISTS_TAC `({ a | a| ?x. aReg a x IN u }, 90 { a | a| ?x. aMem a x IN u },{ a | a| ?x. aStatus a x IN u }, 91 (?y. aCPSR_Reg y IN u),(?y. aUndef y IN u))` 92 \\ FULL_SIMP_TAC std_ss [arm2set'_def,arm2set_def,EXTENSION,SUBSET_DEF,IN_IMAGE, 93 IN_UNION,GSPECIFICATION,IN_INSERT,NOT_IN_EMPTY,IN_UNIV,PUSH_IN_INTO_IF] 94 \\ STRIP_TAC \\ ASM_REWRITE_TAC [] \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 METIS_TAC [] 95 \\ PAT_X_ASSUM ``!x:'a. b:bool`` (IMP_RES_TAC) \\ FULL_SIMP_TAC std_ss [arm_el_11,arm_el_distinct]); 96 97val SPLIT_arm2set_EXISTS = prove( 98 ``!s u v. SPLIT (arm2set s) (u,v) = ?y. (u = arm2set' y s) /\ (v = arm2set'' y s)``, 99 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_REWRITE_TAC [SPLIT_arm2set] 100 \\ FULL_SIMP_TAC bool_ss [SPLIT_def,arm2set'_def,arm2set''_def] 101 \\ `u SUBSET (arm2set s)` by 102 (FULL_SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_UNION] \\ METIS_TAC []) 103 \\ FULL_SIMP_TAC std_ss [SUBSET_arm2set] \\ Q.EXISTS_TAC `y` \\ REWRITE_TAC [] 104 \\ FULL_SIMP_TAC std_ss [EXTENSION,IN_DIFF,IN_UNION,DISJOINT_DEF,NOT_IN_EMPTY,IN_INTER] 105 \\ METIS_TAC []); 106 107val IN_arm2set = prove(`` 108 (!r x s. aReg r x IN (arm2set s) = (x = ARM_READ_REG r s)) /\ 109 (!r x s. aReg r x IN (arm2set' (rs,ms,st,cp,ud) s) = (x = ARM_READ_REG r s) /\ r IN rs) /\ 110 (!r x s. aReg r x IN (arm2set'' (rs,ms,st,cp,ud) s) = (x = ARM_READ_REG r s) /\ ~(r IN rs)) /\ 111 (!p x s. aMem p x IN (arm2set s) = (x = ARM_READ_MEM p s)) /\ 112 (!p x s. aMem p x IN (arm2set' (rs,ms,st,cp,ud) s) = (x = ARM_READ_MEM p s) /\ p IN ms) /\ 113 (!p x s. aMem p x IN (arm2set'' (rs,ms,st,cp,ud) s) = (x = ARM_READ_MEM p s) /\ ~(p IN ms)) /\ 114 (!a x s. aStatus a x IN (arm2set s) = (x = ARM_READ_STATUS a s)) /\ 115 (!a x s. aStatus a x IN (arm2set' (rs,ms,st,cp,ud) s) = (x = ARM_READ_STATUS a s) /\ a IN st) /\ 116 (!a x s. aStatus a x IN (arm2set'' (rs,ms,st,cp,ud) s) = (x = ARM_READ_STATUS a s) /\ ~(a IN st)) /\ 117 (!x s. aCPSR_Reg x IN (arm2set s) = (x = ARM_READ_MASKED_CPSR s)) /\ 118 (!x s. aCPSR_Reg x IN (arm2set' (rs,ms,st,cp,ud) s) = (x = ARM_READ_MASKED_CPSR s) /\ cp) /\ 119 (!x s. aCPSR_Reg x IN (arm2set'' (rs,ms,st,cp,ud) s) = (x = ARM_READ_MASKED_CPSR s) /\ ~cp) /\ 120 (!x s. aUndef x IN (arm2set s) = (x = ARM_READ_UNDEF s)) /\ 121 (!x s. aUndef x IN (arm2set' (rs,ms,st,cp,ud) s) = (x = ARM_READ_UNDEF s) /\ ud) /\ 122 (!x s. aUndef x IN (arm2set'' (rs,ms,st,cp,ud) s) = (x = ARM_READ_UNDEF s) /\ ~ud)``, 123 SRW_TAC [] [arm2set'_def,arm2set''_def,arm2set_def,IN_UNION, 124 IN_INSERT,NOT_IN_EMPTY,IN_DIFF,PUSH_IN_INTO_IF] \\ METIS_TAC []); 125 126val arm2set''_11 = prove( 127 ``!y y' s s'. (arm2set'' y' s' = arm2set'' y s) ==> (y = y')``, 128 REPEAT STRIP_TAC \\ CCONTR_TAC 129 \\ `?r m st cp ud. y = (r,m,st,cp,ud)` by METIS_TAC [PAIR] 130 \\ `?r' m' st' cp' ud'. y' = (r',m',st',cp',ud')` by METIS_TAC [PAIR] 131 \\ FULL_SIMP_TAC bool_ss [PAIR_EQ] THENL [ 132 `?a. ~(a IN r = a IN r')` by METIS_TAC [EXTENSION] 133 \\ sg `~((?x. aReg a x IN arm2set'' y s) = (?x. aReg a x IN arm2set'' y' s'))`, 134 `?a. ~(a IN m = a IN m')` by METIS_TAC [EXTENSION] 135 \\ sg `~((?x. aMem a x IN arm2set'' y s) = (?x. aMem a x IN arm2set'' y' s'))`, 136 `?a. ~(a IN st = a IN st')` by METIS_TAC [EXTENSION] 137 \\ sg `~((?x. aStatus a x IN arm2set'' y s) = (?x. aStatus a x IN arm2set'' y' s'))`, 138 sg `~((?x. aCPSR_Reg x IN arm2set'' y s) = (?x. aCPSR_Reg x IN arm2set'' y' s'))`, 139 sg `~((?x. aUndef x IN arm2set'' y s) = (?x. aUndef x IN arm2set'' y' s'))`] 140 \\ REPEAT (FULL_SIMP_TAC bool_ss [IN_arm2set] \\ METIS_TAC []) 141 \\ Q.PAT_X_ASSUM `arm2set'' _ _ = arm2set'' _ _` (K ALL_TAC) 142 \\ FULL_SIMP_TAC bool_ss [IN_arm2set] \\ METIS_TAC []); 143 144val DELETE_arm2set = prove(`` 145 (!a s. (arm2set' (rs,ms,st,cp,ud) s) DELETE aReg a (ARM_READ_REG a s) = 146 (arm2set' (rs DELETE a,ms,st,cp,ud) s)) /\ 147 (!b s. (arm2set' (rs,ms,st,cp,ud) s) DELETE aMem b (ARM_READ_MEM b s) = 148 (arm2set' (rs,ms DELETE b,st,cp,ud) s)) /\ 149 (!c s. (arm2set' (rs,ms,st,cp,ud) s) DELETE aStatus c (ARM_READ_STATUS c s) = 150 (arm2set' (rs,ms,st DELETE c,cp,ud) s)) /\ 151 (!s. (arm2set' (rs,ms,st,cp,ud) s) DELETE aCPSR_Reg (ARM_READ_MASKED_CPSR s) = 152 (arm2set' (rs,ms,st,F,ud) s)) /\ 153 (!s. (arm2set' (rs,ms,st,cp,ud) s) DELETE aUndef (ARM_READ_UNDEF s) = 154 (arm2set' (rs,ms,st,cp,F) s))``, 155 SRW_TAC [] [arm2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR, 156 EXISTS_OR_THM,IN_DELETE,IN_INSERT,NOT_IN_EMPTY,PUSH_IN_INTO_IF] 157 \\ Cases_on `x` \\ SRW_TAC [] [] \\ METIS_TAC []); 158 159val EMPTY_arm2set = prove(`` 160 (arm2set' (rs,ms,st,cp,ud) s = {}) = (rs = {}) /\ (ms = {}) /\ (st = {}) /\ ~cp /\ ~ud``, 161 Cases_on `ud` 162 \\ SRW_TAC [] [arm2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR, 163 EXISTS_OR_THM,IN_DELETE,IN_INSERT,NOT_IN_EMPTY,PUSH_IN_INTO_IF] 164 \\ METIS_TAC []); 165 166val ARM_READ_MASKED_CPSR_THM = 167 (SIMP_CONV std_ss [ARM_READ_MASKED_CPSR_def,encode_psr_def,word_slice_def] THENC 168 ONCE_REWRITE_CONV [METIS_PROVE [] ``p /\ q = p /\ (p ==> q)``] THENC 169 SIMP_CONV (std_ss++SIZES_ss) [fcpTheory.FCP_BETA,DECIDE ``(i<=31=i<32:num)/\(i<=26=i<27)``] THENC 170 ONCE_REWRITE_CONV [GSYM (METIS_PROVE [] ``p /\ q = p /\ (p ==> q)``)] THENC 171 SIMP_CONV std_ss [DECIDE ``i<27 /\ i<32 = i<27``]) 172 ``ARM_READ_MASKED_CPSR s`` 173 174 175(* ----------------------------------------------------------------------------- *) 176(* Defining the ARM_MODEL *) 177(* ----------------------------------------------------------------------------- *) 178 179val aR_def = Define `aR a x = SEP_EQ {aReg a x}`; 180val aM1_def = Define `aM1 a x = SEP_EQ {aMem a x}`; 181val aS1_def = Define `aS1 a x = SEP_EQ {aStatus a x}`; 182val aU1_def = Define `aU1 x = SEP_EQ {aUndef x}`; 183val aCPSR_def = Define `aCPSR x = SEP_EQ {aCPSR_Reg x}`; 184 185val aLR_def = Define `aLR lr = cond (ALIGNED lr) * aR 14w lr`; 186 187val aM_def = Define ` 188 aM a (w:word32) = 189 aM1 a ((7 >< 0) w) * 190 aM1 (a + 1w) ((7 >< 0) (w >> 8)) * 191 aM1 (a + 2w) ((7 >< 0) (w >> 16)) * 192 aM1 (a + 3w) ((7 >< 0) (w >> 24))`; 193 194val aPC_def = Define `aPC x = aR 15w x * aU1 F * cond (ALIGNED x)`; 195 196val aS_def = Define `aS (n,z,c,v) = aS1 psrN n * aS1 psrZ z * aS1 psrC c * aS1 psrV v`; 197 198val ARM_NEXT_REL_def = Define `ARM_NEXT_REL s s' = (ARM_NEXT NoInterrupt s = SOME s')`; 199 200val ARM_INSTR_def = Define `ARM_INSTR (a,w:word32) = 201 { aMem (a+3w) ((31 >< 24) w) ; 202 aMem (a+2w) ((23 >< 16) w) ; 203 aMem (a+1w) ((15 >< 8) w) ; 204 aMem (a+0w) (( 7 >< 0) w) }`; 205 206val ARM_MODEL_def = Define ` 207 ARM_MODEL = (arm2set, ARM_NEXT_REL, ARM_INSTR, (\x y. x = (y:arm_state)), 208 (K F):arm_state -> bool)`; 209 210val aST_LIST_def = Define ` 211 (aST_LIST a [] = emp) /\ 212 (aST_LIST a (x::xs) = aM a x * aST_LIST (a-4w) xs)`; 213 214val aST_def = Define `aST a xs = aR 13w a * aST_LIST a xs * cond (ALIGNED a)`; 215 216(* theorems *) 217 218val lemma = 219 METIS_PROVE [SPLIT_arm2set] 220 ``p (arm2set' y s) ==> (?u v. SPLIT (arm2set s) (u,v) /\ p u /\ (\v. v = arm2set'' y s) v)``; 221 222val ARM_SPEC_SEMANTICS = store_thm("ARM_SPEC_SEMANTICS", 223 ``SPEC ARM_MODEL p {} q = 224 !y s seq. p (arm2set' y s) /\ rel_sequence ARM_NEXT_REL seq s ==> 225 ?k. q (arm2set' y (seq k)) /\ (arm2set'' y s = arm2set'' y (seq k))``, 226 SIMP_TAC std_ss [GSYM RUN_EQ_SPEC,RUN_def,ARM_MODEL_def,STAR_def,SEP_REFINE_def] 227 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC 228 THEN1 (FULL_SIMP_TAC bool_ss [SPLIT_arm2set_EXISTS] \\ METIS_TAC []) 229 \\ Q.PAT_X_ASSUM `!s r. b` (STRIP_ASSUME_TAC o UNDISCH o SPEC_ALL o 230 (fn th => MATCH_MP th (UNDISCH lemma)) o Q.SPECL [`s`,`(\v. v = arm2set'' y s)`]) 231 \\ FULL_SIMP_TAC bool_ss [SPLIT_arm2set_EXISTS] 232 \\ IMP_RES_TAC arm2set''_11 \\ Q.EXISTS_TAC `i` \\ METIS_TAC []); 233 234 235(* ----------------------------------------------------------------------------- *) 236(* Theorems for construction of |- SPEC ARM_MODEL ... *) 237(* ----------------------------------------------------------------------------- *) 238 239val STAR_arm2set = store_thm("STAR_arm2set", 240 ``((aR a x * p) (arm2set' (rs,ms,st,cp,ud) s) = 241 (x = ARM_READ_REG a s) /\ a IN rs /\ p (arm2set' (rs DELETE a,ms,st,cp,ud) s)) /\ 242 ((aM1 b y * p) (arm2set' (rs,ms,st,cp,ud) s) = 243 (y = ARM_READ_MEM b s) /\ b IN ms /\ p (arm2set' (rs,ms DELETE b,st,cp,ud) s)) /\ 244 ((aS1 c z * p) (arm2set' (rs,ms,st,cp,ud) s) = 245 (z = ARM_READ_STATUS c s) /\ c IN st /\ p (arm2set' (rs,ms,st DELETE c,cp,ud) s)) /\ 246 ((aCPSR t * p) (arm2set' (rs,ms,st,cp,ud) s) = 247 (t = ARM_READ_MASKED_CPSR s) /\ cp /\ p (arm2set' (rs,ms,st,F,ud) s)) /\ 248 ((aU1 q * p) (arm2set' (rs,ms,st,cp,ud) s) = 249 (q = ARM_READ_UNDEF s) /\ ud /\ p (arm2set' (rs,ms,st,cp,F) s)) /\ 250 ((cond g * p) (arm2set' (rs,ms,st,cp,ud) s) = 251 g /\ p (arm2set' (rs,ms,st,cp,ud) s))``, 252 SIMP_TAC std_ss [aR_def,aS1_def,aM1_def,EQ_STAR,INSERT_SUBSET,cond_STAR,aU1_def, 253 aCPSR_def,EMPTY_SUBSET,IN_arm2set,GSYM DELETE_DEF] 254 \\ Cases_on `x = ARM_READ_REG a s` \\ ASM_SIMP_TAC bool_ss [DELETE_arm2set] 255 \\ Cases_on `y = ARM_READ_MEM b s` \\ ASM_SIMP_TAC bool_ss [DELETE_arm2set] 256 \\ Cases_on `z = ARM_READ_STATUS c s` \\ ASM_SIMP_TAC bool_ss [DELETE_arm2set] 257 \\ Cases_on `t = ARM_READ_MASKED_CPSR s` \\ ASM_SIMP_TAC bool_ss [DELETE_arm2set] 258 \\ Cases_on `q = ARM_READ_UNDEF s` \\ ASM_SIMP_TAC bool_ss [DELETE_arm2set] 259 \\ ASM_SIMP_TAC std_ss [AC CONJ_COMM CONJ_ASSOC]); 260 261val CODE_POOL_arm2set_LEMMA = prove( 262 ``!x y z. (x = z INSERT y) = (z INSERT y) SUBSET x /\ (x DIFF (z INSERT y) = {})``, 263 SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY,IN_DIFF] \\ METIS_TAC []); 264 265val CODE_POOL_arm2set_2 = prove( 266 ``CODE_POOL ARM_INSTR {(p,c);(q,d)} (arm2set' (rs,ms,st,cp,ud) s) = 267 ({p+3w;p+2w;p+1w;p;q+3w;q+2w;q+1w;q} = ms) /\ (rs = {}) /\ (st = {}) /\ ~cp /\ ~ud /\ 268 (ARM_READ_MEM (p + 0w) s = ( 7 >< 0) c) /\ 269 (ARM_READ_MEM (p + 1w) s = (15 >< 8) c) /\ 270 (ARM_READ_MEM (p + 2w) s = (23 >< 16) c) /\ 271 (ARM_READ_MEM (p + 3w) s = (31 >< 24) c) /\ 272 (ARM_READ_MEM (q + 0w) s = ( 7 >< 0) d) /\ 273 (ARM_READ_MEM (q + 1w) s = (15 >< 8) d) /\ 274 (ARM_READ_MEM (q + 2w) s = (23 >< 16) d) /\ 275 (ARM_READ_MEM (q + 3w) s = (31 >< 24) d)``, 276 SIMP_TAC bool_ss [CODE_POOL_def,IMAGE_INSERT,IMAGE_EMPTY,BIGUNION_INSERT, 277 BIGUNION_EMPTY,UNION_EMPTY,ARM_INSTR_def,CODE_POOL_arm2set_LEMMA, 278 GSYM DELETE_DEF, INSERT_SUBSET, EMPTY_SUBSET,IN_arm2set,INSERT_UNION_EQ] 279 \\ Cases_on `(31 >< 24) c = ARM_READ_MEM (p + 3w) s` \\ ASM_SIMP_TAC std_ss [] 280 \\ Cases_on `(23 >< 16) c = ARM_READ_MEM (p + 2w) s` \\ ASM_SIMP_TAC std_ss [] 281 \\ Cases_on `(15 >< 8) c = ARM_READ_MEM (p + 1w) s` \\ ASM_SIMP_TAC std_ss [] 282 \\ Cases_on `( 7 >< 0) c = ARM_READ_MEM (p + 0w) s` \\ ASM_SIMP_TAC std_ss [] 283 \\ Cases_on `(31 >< 24) d = ARM_READ_MEM (q + 3w) s` \\ ASM_SIMP_TAC std_ss [] 284 \\ Cases_on `(23 >< 16) d = ARM_READ_MEM (q + 2w) s` \\ ASM_SIMP_TAC std_ss [] 285 \\ Cases_on `(15 >< 8) d = ARM_READ_MEM (q + 1w) s` \\ ASM_SIMP_TAC std_ss [] 286 \\ Cases_on `( 7 >< 0) d = ARM_READ_MEM (q + 0w) s` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0] 287 \\ ASM_SIMP_TAC std_ss [DELETE_arm2set,EMPTY_arm2set,DIFF_INSERT] 288 \\ ASM_SIMP_TAC std_ss [AC CONJ_COMM CONJ_ASSOC,DIFF_EMPTY,EMPTY_arm2set]); 289 290val CODE_POOL_arm2set_1 = prove( 291 ``CODE_POOL ARM_INSTR {(p,c)} (arm2set' (rs,ms,st,cp,ud) s) = 292 ({p+3w;p+2w;p+1w;p} = ms) /\ (rs = {}) /\ (st = {}) /\ ~cp /\ ~ud /\ 293 (ARM_READ_MEM (p + 0w) s = ( 7 >< 0) c) /\ 294 (ARM_READ_MEM (p + 1w) s = (15 >< 8) c) /\ 295 (ARM_READ_MEM (p + 2w) s = (23 >< 16) c) /\ 296 (ARM_READ_MEM (p + 3w) s = (31 >< 24) c)``, 297 SIMP_TAC bool_ss [CODE_POOL_def,IMAGE_INSERT,IMAGE_EMPTY,BIGUNION_INSERT, 298 BIGUNION_EMPTY,UNION_EMPTY,ARM_INSTR_def,CODE_POOL_arm2set_LEMMA, 299 GSYM DELETE_DEF, INSERT_SUBSET, EMPTY_SUBSET,IN_arm2set] 300 \\ Cases_on `(31 >< 24) c = ARM_READ_MEM (p + 3w) s` \\ ASM_SIMP_TAC std_ss [] 301 \\ Cases_on `(23 >< 16) c = ARM_READ_MEM (p + 2w) s` \\ ASM_SIMP_TAC std_ss [] 302 \\ Cases_on `(15 >< 8) c = ARM_READ_MEM (p + 1w) s` \\ ASM_SIMP_TAC std_ss [] 303 \\ Cases_on `( 7 >< 0) c = ARM_READ_MEM (p + 0w) s` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0] 304 \\ ASM_SIMP_TAC std_ss [DELETE_arm2set,EMPTY_arm2set,DIFF_INSERT] 305 \\ ASM_SIMP_TAC std_ss [AC CONJ_COMM CONJ_ASSOC,DIFF_EMPTY,EMPTY_arm2set]); 306 307val CODE_POOL_arm2set = save_thm("CODE_POOL_arm2set", 308 CONJ CODE_POOL_arm2set_1 CODE_POOL_arm2set_2); 309 310val ARM_WRITE_STS_def = Define ` 311 ARM_WRITE_STS a x s = if a IN {psrN;psrZ;psrC;psrV;psrQ} then ARM_WRITE_STATUS a x s else s`; 312 313val ARM_WRITE_STS_INTRO = store_thm("ARM_WRITE_STS_INTRO", 314 ``(ARM_WRITE_STATUS psrN x s = ARM_WRITE_STS psrN x s) /\ 315 (ARM_WRITE_STATUS psrZ x s = ARM_WRITE_STS psrZ x s) /\ 316 (ARM_WRITE_STATUS psrC x s = ARM_WRITE_STS psrC x s) /\ 317 (ARM_WRITE_STATUS psrV x s = ARM_WRITE_STS psrV x s) /\ 318 (ARM_WRITE_STATUS psrQ x s = ARM_WRITE_STS psrQ x s)``, 319 SIMP_TAC std_ss [ARM_WRITE_STS_def,IN_INSERT]); 320 321val UNDEF_OF_UPDATES = prove( 322 ``(!a x. ARM_READ_UNDEF (ARM_WRITE_REG a x s) = ARM_READ_UNDEF s) /\ 323 (!a x. ARM_READ_UNDEF (ARM_WRITE_MEM a x s) = ARM_READ_UNDEF s) /\ 324 (!a x. ARM_READ_UNDEF (ARM_WRITE_STS a x s) = ARM_READ_UNDEF s) /\ 325 (!a x. ARM_READ_UNDEF (ARM_WRITE_MEM_WRITE a x s) = ARM_READ_UNDEF s) /\ 326 (!a. ARM_READ_UNDEF (ARM_WRITE_MEM_READ a s) = ARM_READ_UNDEF s) /\ 327 (!a x y. ARM_READ_UNDEF (CLEAR_EXCLUSIVE_BY_ADDRESS (x,y) s) = ARM_READ_UNDEF s)``, 328 SIMP_TAC std_ss [ARM_READ_UNDEF_def,ARM_OK_def] \\ REPEAT STRIP_TAC 329 \\ EVAL_TAC \\ SRW_TAC [] [] \\ EVAL_TAC); 330 331val MASKED_CPSR_OF_UPDATES = prove( 332 ``(!a x. ARM_READ_MASKED_CPSR (ARM_WRITE_STS a x s) = ARM_READ_MASKED_CPSR s) /\ 333 (!a x. ARM_READ_MASKED_CPSR (ARM_WRITE_REG a x s) = ARM_READ_MASKED_CPSR s) /\ 334 (!a x. ARM_READ_MASKED_CPSR (ARM_WRITE_MEM a x s) = ARM_READ_MASKED_CPSR s) /\ 335 (!a x. ARM_READ_MASKED_CPSR (ARM_WRITE_MEM_WRITE a x s) = ARM_READ_MASKED_CPSR s) /\ 336 (!a. ARM_READ_MASKED_CPSR (ARM_WRITE_MEM_READ a s) = ARM_READ_MASKED_CPSR s) /\ 337 (!a x y. ARM_READ_MASKED_CPSR (CLEAR_EXCLUSIVE_BY_ADDRESS (x,y) s) = ARM_READ_MASKED_CPSR s)``, 338 SIMP_TAC std_ss [ARM_READ_MASKED_CPSR_THM,ARM_OK_def] \\ REPEAT STRIP_TAC THEN1 339 (SIMP_TAC std_ss [ARM_WRITE_STS_def] 340 \\ Cases_on `a IN {psrN; psrZ; psrC; psrV; psrQ}` \\ ASM_SIMP_TAC std_ss [] 341 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (f x = f y)``) 342 \\ SIMP_TAC std_ss [FUN_EQ_THM] \\ REPEAT STRIP_TAC 343 \\ FULL_SIMP_TAC std_ss [IN_INSERT,NOT_IN_EMPTY] \\ EVAL_TAC) 344 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (f x = f y)``) 345 \\ SIMP_TAC std_ss [FUN_EQ_THM] \\ REPEAT STRIP_TAC \\ EVAL_TAC); 346 347val ARM_READ_WRITE = LIST_CONJ [REG_OF_UPDATES,MEM_OF_UPDATES,MASKED_CPSR_OF_UPDATES, 348 UNDEF_OF_UPDATES,CPSR_COMPONENTS_OF_UPDATES] 349val _ = save_thm("ARM_READ_WRITE",ARM_READ_WRITE); 350 351val ARM_OK_WRITE_GE = prove( 352 ``ARM_OK (ARM_WRITE_GE w4 s) = ARM_OK s``, 353 SIMP_TAC std_ss [ARM_OK_def] \\ EVAL_TAC); 354 355(* 356val UPDATE_arm2set''_GE = prove( 357 ``(!w4. arm2set'' (rs,ms,st,cp,ud) (ARM_WRITE_GE w4 s) = arm2set'' (rs,ms,st,cp,ud) s)``, 358 SIMP_TAC std_ss [arm2set_def,arm2set''_def,arm2set'_def,REG_OF_UPDATES, 359 MEM_OF_UPDATES,ARM_READ_WRITE,ARM_READ_UNDEF_def,ARM_OK_WRITE_GE] 360*) 361 362val UPDATE_arm2set'' = store_thm("UPDATE_arm2set''", 363 ``(!a x. a IN rs ==> (arm2set'' (rs,ms,st,cp,ud) (ARM_WRITE_REG a x s) = arm2set'' (rs,ms,st,cp,ud) s)) /\ 364 (!a x. a IN ms ==> (arm2set'' (rs,ms,st,cp,ud) (ARM_WRITE_MEM a x s) = arm2set'' (rs,ms,st,cp,ud) s)) /\ 365 (!b x. b IN st ==> (arm2set'' (rs,ms,st,cp,ud) (ARM_WRITE_STS b x s) = arm2set'' (rs,ms,st,cp,ud) s)) /\ 366 (!a x. arm2set'' (rs,ms,st,cp,ud) (ARM_WRITE_MEM_WRITE a x s) = arm2set'' (rs,ms,st,cp,ud) s) /\ 367 (!a. arm2set'' (rs,ms,st,cp,ud) (ARM_WRITE_MEM_READ a s) = arm2set'' (rs,ms,st,cp,ud) s) /\ 368 (!x y. arm2set'' (rs,ms,st,cp,ud) (CLEAR_EXCLUSIVE_BY_ADDRESS (x,y) s) = 369 arm2set'' (rs,ms,st,cp,ud) s)``, 370 SIMP_TAC std_ss [arm2set_def,arm2set''_def,arm2set'_def,EXTENSION,IN_UNION, 371 IN_IMAGE,IN_DIFF,IN_UNIV,NOT_IN_EMPTY,IN_INSERT,ARM_READ_WRITE,PUSH_IN_INTO_IF] 372 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 373 \\ Q.PAT_X_ASSUM `xx = yy` (fn th => FULL_SIMP_TAC std_ss [th]) 374 \\ FULL_SIMP_TAC std_ss [arm_el_distinct,arm_el_11] 375 \\ IMP_RES_TAC (METIS_PROVE [] ``x IN s /\ ~(y IN s) ==> ~(x = y:'a)``) 376 \\ ASM_SIMP_TAC std_ss [ARM_READ_WRITE,UNDEF_OF_UPDATES] 377 \\ SIMP_TAC std_ss [ARM_WRITE_STS_def] \\ TRY (Cases_on `b IN {psrN; psrZ; psrC; psrV; psrQ}`) 378 \\ FULL_SIMP_TAC std_ss [ARM_READ_WRITE,UNDEF_OF_UPDATES] 379 \\ METIS_TAC []); 380 381val ARM_SPEC_CODE = 382 SPEC_CODE |> ISPEC ``ARM_MODEL`` 383 |> SIMP_RULE std_ss [ARM_MODEL_def] 384 |> RW [GSYM ARM_MODEL_def]; 385 386val IMP_ARM_SPEC_LEMMA = prove( 387 ``!p q. 388 (!rs ms st cp ud s. ?s'. 389 (p (arm2set' (rs,ms,st,cp,ud) s) ==> 390 (ARM_NEXT NoInterrupt s = SOME s') /\ q (arm2set' (rs,ms,st,cp,ud) s') /\ 391 (arm2set'' (rs,ms,st,cp,ud) s = arm2set'' (rs,ms,st,cp,ud) s'))) ==> 392 SPEC ARM_MODEL p {} q``, 393 SIMP_TAC std_ss [RIGHT_EXISTS_IMP_THM] \\ REWRITE_TAC [ARM_SPEC_SEMANTICS] 394 \\ SIMP_TAC std_ss [FORALL_PROD] 395 \\ REPEAT STRIP_TAC \\ RES_TAC 396 \\ FULL_SIMP_TAC bool_ss [rel_sequence_def,ARM_NEXT_REL_def] 397 \\ Q.EXISTS_TAC `SUC 0` \\ METIS_TAC [PAIR,optionTheory.SOME_11]); 398 399val IMP_ARM_SPEC = save_thm("IMP_ARM_SPEC", 400 (RW1 [STAR_COMM] o RW [ARM_SPEC_CODE] o 401 SPECL [``CODE_POOL ARM_INSTR c * p'``, 402 ``CODE_POOL ARM_INSTR c * q'``]) IMP_ARM_SPEC_LEMMA); 403 404val aS_HIDE = store_thm("aS_HIDE", 405 ``~aS = ~aS1 psrN * ~aS1 psrZ * ~aS1 psrC * ~aS1 psrV``, 406 SIMP_TAC std_ss [SEP_HIDE_def,aS_def,SEP_CLAUSES,FUN_EQ_THM] 407 \\ SIMP_TAC std_ss [SEP_EXISTS] \\ METIS_TAC [aS_def,PAIR]); 408 409val _ = wordsLib.guess_lengths(); 410val BYTES_TO_WORD_LEMMA = store_thm("BYTES_TO_WORD_LEMMA", 411 ``!w. (31 >< 24) w @@ (23 >< 16) w @@ (15 >< 8) w @@ (7 >< 0) w = w``, 412 SRW_TAC [wordsLib.WORD_EXTRACT_ss] []); 413 414val aM_INTRO_LEMMA1 = prove( 415 ``!a x0 x1 x2 x3 p. 416 (p * aM1 a x0 * aM1 (a + 1w) x1 * aM1 (a + 2w) x2 * aM1 (a + 3w) x3 = 417 p * aM a (bytes2word [x0;x1;x2;x3]))``, 418 SRW_TAC [wordsLib.WORD_EXTRACT_ss] [bit_listTheory.bytes2word_def,aM_def,STAR_ASSOC]); 419 420val aM_INTRO_LEMMA2 = prove( 421 ``!a x0 x1 x2 x3 p. 422 (p * aM1 a x3 * aM1 (a - 1w) x2 * aM1 (a - 2w) x1 * aM1 (a - 3w) x0 = 423 p * aM (a - 3w) (bytes2word [x0; x1; x2; x3]))``, 424 SIMP_TAC std_ss [GSYM aM_INTRO_LEMMA1,word_arith_lemma3,WORD_ADD_0, 425 AC STAR_ASSOC STAR_COMM]); 426 427val aM_INTRO = save_thm("aM_INTRO", 428 GEN_ALL (CONJ (Q.SPEC `a` aM_INTRO_LEMMA1) 429 (Q.SPEC `a` aM_INTRO_LEMMA2))); 430 431 432(* ----------------------------------------------------------------------------- *) 433(* Byte-sized data memory *) 434(* ----------------------------------------------------------------------------- *) 435 436val aBYTE_MEMORY_SET_def = Define ` 437 aBYTE_MEMORY_SET df f = { aMem a (f a) | a | a IN df }`; 438 439val aBYTE_MEMORY_def = Define `aBYTE_MEMORY df f = SEP_EQ (aBYTE_MEMORY_SET df f)`; 440 441val IN_aBYTE_MEMORY_SET = prove( 442 ``a IN df ==> 443 (aBYTE_MEMORY_SET df g = (aMem a (g a)) INSERT aBYTE_MEMORY_SET (df DELETE a) g)``, 444 SIMP_TAC std_ss [EXTENSION,IN_INSERT,aBYTE_MEMORY_SET_def,GSPECIFICATION] 445 \\ REWRITE_TAC [IN_DELETE] \\ METIS_TAC []); 446 447val DELETE_aBYTE_MEMORY_SET = prove( 448 ``aBYTE_MEMORY_SET (df DELETE a) ((a =+ w) g) = 449 aBYTE_MEMORY_SET (df DELETE a) g``, 450 SIMP_TAC std_ss [EXTENSION,IN_INSERT,aBYTE_MEMORY_SET_def,GSPECIFICATION] 451 \\ REWRITE_TAC [IN_DELETE,APPLY_UPDATE_THM] \\ METIS_TAC []); 452 453val aBYTE_MEMORY_INSERT = store_thm("aBYTE_MEMORY_INSERT", 454 ``a IN df ==> 455 (aBYTE_MEMORY df ((a =+ w) g) = aM1 a w * aBYTE_MEMORY (df DELETE a) g)``, 456 SIMP_TAC std_ss [aBYTE_MEMORY_def,aM1_def,FUN_EQ_THM,EQ_STAR] 457 \\ SIMP_TAC std_ss [SEP_EQ_def] \\ REPEAT STRIP_TAC 458 \\ IMP_RES_TAC (GEN_ALL IN_aBYTE_MEMORY_SET) 459 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,DIFF_INSERT,DIFF_EMPTY] 460 \\ REWRITE_TAC [DELETE_aBYTE_MEMORY_SET,APPLY_UPDATE_THM] 461 \\ REWRITE_TAC [EXTENSION,IN_INSERT,IN_DELETE] 462 \\ `~(aMem a w IN aBYTE_MEMORY_SET (df DELETE a) g)` suffices_by METIS_TAC [] 463 \\ SIMP_TAC std_ss [aBYTE_MEMORY_SET_def,GSPECIFICATION,IN_DELETE,arm_el_11]); 464 465val aBYTE_MEMORY_INTRO = store_thm("aBYTE_MEMORY_INTRO", 466 ``SPEC m (aM1 a v * P) c (aM1 a w * Q) ==> 467 a IN df ==> 468 SPEC m (aBYTE_MEMORY df ((a =+ v) f) * P) c (aBYTE_MEMORY df ((a =+ w) f) * Q)``, 469 ONCE_REWRITE_TAC [STAR_COMM] 470 \\ SIMP_TAC std_ss [aBYTE_MEMORY_INSERT,STAR_ASSOC] 471 \\ METIS_TAC [SPEC_FRAME]); 472 473 474(* ----------------------------------------------------------------------------- *) 475(* Memory assertion based on finite maps *) 476(* ----------------------------------------------------------------------------- *) 477 478val aMEM_def = Define `aMEM m = aBYTE_MEMORY (FDOM m) (\x. m ' x)`; 479 480(* 481val _ = wordsLib.guess_lengths(); 482val READ32_def = Define ` 483 READ32 a (m:word32 |-> word8) = 484 (m ' (a + 3w) @@ m ' (a + 2w) @@ m ' (a + 1w) @@ m ' (a)):word32`; 485 486val WRITE32_def = Define ` 487 WRITE32 (a:word32) (w:word32) m = 488 m |+ (a + 0w, (( 7 >< 0) w):word8) 489 |+ (a + 1w, ((15 >< 8) w):word8) 490 |+ (a + 2w, ((23 >< 16) w):word8) 491 |+ (a + 3w, ((31 >< 24) w):word8)`; 492 493val WRITE32_THM = store_thm("WRITE32_THM", 494 ``!a w. 495 (((a + 3w =+ (31 >< 24) w) 496 ((a + 2w =+ (23 >< 16) w) 497 ((a + 1w =+ (15 >< 8) w) 498 ((a =+ (7 >< 0) w) (\x. m ' x))))) = 499 (\x. WRITE32 a w m ' x)) /\ 500 (((a =+ (7 >< 0) w) 501 ((a + 0x1w =+ (15 >< 8) w) 502 ((a + 0x2w =+ (23 >< 16) w) 503 ((a + 0x3w =+ (31 >< 24) w) (\x. m ' x))))) = 504 (\x. WRITE32 a w m ' x))``, 505 SIMP_TAC std_ss [WRITE32_def,FAPPLY_FUPDATE_THM,APPLY_UPDATE_THM,FUN_EQ_THM] 506 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_LCANCEL, 507 RW [WORD_ADD_0] (Q.SPECL [`w`,`0w`] WORD_EQ_ADD_LCANCEL), 508 RW [WORD_ADD_0] (Q.SPECL [`w`,`v`,`0w`] WORD_EQ_ADD_LCANCEL),n2w_11]); 509*) 510 511val aMEM_WRITE_BYTE = store_thm("aMEM_WRITE_BYTE", 512 ``!a:word32 w:word8. ((a =+ w) (\x. m ' x) = (\x. (m |+ (a,w)) ' x))``, 513 SIMP_TAC std_ss [FAPPLY_FUPDATE_THM,APPLY_UPDATE_THM,FUN_EQ_THM] \\ SRW_TAC [] []); 514 515 516(* ----------------------------------------------------------------------------- *) 517(* Word-sized data memory *) 518(* ----------------------------------------------------------------------------- *) 519 520val aMEMORY_WORD_def = Define ` 521 aMEMORY_WORD (a:word32) (w:word32) = 522 { aMem a (((7 >< 0) (w))) ; 523 aMem (a+1w) (((7 >< 0) (w >> 8))) ; 524 aMem (a+2w) (((7 >< 0) (w >> 16))) ; 525 aMem (a+3w) (((7 >< 0) (w >> 24))) }`; 526 527val aMEMORY_SET_def = Define ` 528 aMEMORY_SET df f = BIGUNION { aMEMORY_WORD a (f a) | a | a IN df /\ ALIGNED a }`; 529 530val aMEMORY_def = Define `aMEMORY df f = SEP_EQ (aMEMORY_SET df f)`; 531 532val aMEMORY_SET_SING = prove( 533 ``!a f. ALIGNED a ==> (aMEMORY_SET {a} f = aMEMORY_WORD a (f a))``, 534 ASM_SIMP_TAC std_ss [GSPECIFICATION,IN_INSERT,NOT_IN_EMPTY,APPLY_UPDATE_THM, 535 EXTENSION,aMEMORY_SET_def,IN_BIGUNION] \\ METIS_TAC [IN_INSERT]); 536 537val aMEMORY_ARITH_LEMMA = prove( 538 ``!a:word32. ~(a = a + 1w) /\ ~(a = a + 2w) /\ ~(a = a + 3w) /\ 539 ~(a + 1w = a + 2w) /\ ~(a + 1w = a + 3w) /\ ~(a + 2w = a + 3w)``, 540 SIMP_TAC (std_ss++wordsLib.SIZES_ss) [WORD_EQ_ADD_LCANCEL,n2w_11, 541 RW [WORD_ADD_0] (Q.SPECL [`x`,`0w`] WORD_EQ_ADD_LCANCEL)]); 542 543val aM_THM = store_thm("aM_THM", 544 ``!a f w. ALIGNED a ==> (aMEMORY {a} ((a =+ w) f) = aM a w)``, 545 SIMP_TAC std_ss [aMEMORY_def,aMEMORY_SET_SING,aM_def] \\ REPEAT STRIP_TAC 546 \\ ONCE_REWRITE_TAC [FUN_EQ_THM] 547 \\ SIMP_TAC std_ss [aM1_def,EQ_STAR,GSYM STAR_ASSOC,APPLY_UPDATE_THM] 548 \\ SIMP_TAC std_ss [SEP_EQ_def] 549 \\ STRIP_TAC \\ Cases_on `x = aMEMORY_WORD a w` \\ ASM_SIMP_TAC std_ss [] 550 \\ FULL_SIMP_TAC std_ss [aMEMORY_WORD_def,INSERT_SUBSET,IN_INSERT,NOT_IN_EMPTY, 551 GSYM DELETE_DEF,EMPTY_SUBSET,IN_DELETE,arm_el_11,EXTENSION] 552 THEN1 METIS_TAC [aMEMORY_ARITH_LEMMA,arm_el_11,arm_el_distinct] 553 \\ SIMP_TAC std_ss [aMEMORY_ARITH_LEMMA] 554 \\ Cases_on `aMem (a + 3w) (((7 >< 0) (w >> 24))) IN x` THEN1 METIS_TAC [] 555 \\ Cases_on `aMem (a + 2w) (((7 >< 0) (w >> 16))) IN x` THEN1 METIS_TAC [] 556 \\ Cases_on `aMem (a + 1w) (((7 >< 0) (w >> 8))) IN x` THEN1 METIS_TAC [] 557 \\ ASM_SIMP_TAC std_ss []); 558 559val aMEMORY_INSERT_LEMMA = prove( 560 ``!s. ALIGNED a /\ ~(a IN s) ==> 561 (aMEMORY {a} ((a =+ w) g) * aMEMORY s f = aMEMORY (a INSERT s) ((a =+ w) f))``, 562 STRIP_TAC 563 \\ SIMP_TAC bool_ss [FUN_EQ_THM,cond_STAR,aMEMORY_def,aMEMORY_SET_SING,APPLY_UPDATE_THM] 564 \\ SIMP_TAC std_ss [STAR_def,SEP_EQ_def,SPLIT_def] 565 \\ REPEAT STRIP_TAC 566 \\ `DISJOINT (aMEMORY_WORD a w) (aMEMORY_SET s f)` by 567 (SIMP_TAC std_ss [DISJOINT_DEF,EXTENSION,NOT_IN_EMPTY,IN_INTER, 568 aMEMORY_SET_def,IN_BIGUNION,GSPECIFICATION] 569 \\ REWRITE_TAC [GSYM IMP_DISJ_THM] \\ REPEAT STRIP_TAC 570 \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] 571 \\ Q.PAT_X_ASSUM `!x. b` (K ALL_TAC) 572 \\ `~(a = a')` by METIS_TAC [] 573 \\ NTAC 2 (FULL_SIMP_TAC bool_ss [aMEMORY_WORD_def,IN_INSERT, 574 NOT_IN_EMPTY,arm_el_11,WORD_EQ_ADD_RCANCEL]) 575 \\ FULL_SIMP_TAC std_ss [word_arith_lemma5,word_arith_lemma4] 576 \\ METIS_TAC [NOT_ALIGNED]) 577 \\ `aMEMORY_WORD a w UNION aMEMORY_SET s f = 578 aMEMORY_SET (a INSERT s) ((a =+ w) f)` by 579 (SIMP_TAC std_ss [IN_UNION,EXTENSION,NOT_IN_EMPTY,IN_INTER,IN_INSERT, 580 aMEMORY_SET_def,IN_BIGUNION,GSPECIFICATION] 581 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THENL [ 582 Q.EXISTS_TAC `aMEMORY_WORD a w` \\ ASM_SIMP_TAC std_ss [] 583 \\ Q.EXISTS_TAC `a` \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM], 584 Q.EXISTS_TAC `s'` \\ ASM_SIMP_TAC std_ss [] 585 \\ Q.EXISTS_TAC `a'` \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM] \\ METIS_TAC [], 586 FULL_SIMP_TAC bool_ss [APPLY_UPDATE_THM], 587 `~(a = a')` by METIS_TAC [] \\ FULL_SIMP_TAC bool_ss [APPLY_UPDATE_THM] 588 \\ METIS_TAC []]) 589 \\ ASM_SIMP_TAC bool_ss [] \\ METIS_TAC []); 590 591val aMEMORY_INSERT = save_thm("aMEMORY_INSERT", 592 SIMP_RULE std_ss [aM_THM] aMEMORY_INSERT_LEMMA); 593 594val aMEMORY_INTRO = store_thm("aMEMORY_INTRO", 595 ``SPEC ARM_MODEL (aM a v * P) c (aM a w * Q) ==> 596 ALIGNED a /\ a IN df ==> 597 SPEC ARM_MODEL (aMEMORY df ((a =+ v) f) * P) c (aMEMORY df ((a =+ w) f) * Q)``, 598 REPEAT STRIP_TAC 599 \\ (IMP_RES_TAC o GEN_ALL o REWRITE_RULE [AND_IMP_INTRO] o 600 SIMP_RULE std_ss [INSERT_DELETE,IN_DELETE] o 601 DISCH ``a:word32 IN df`` o Q.SPEC `df DELETE a` o GSYM) aMEMORY_INSERT_LEMMA 602 \\ ASM_REWRITE_TAC [] \\ ASM_SIMP_TAC bool_ss [aM_THM] 603 \\ ONCE_REWRITE_TAC [STAR_COMM] \\ REWRITE_TAC [STAR_ASSOC] 604 \\ MATCH_MP_TAC SPEC_FRAME 605 \\ FULL_SIMP_TAC bool_ss [AC STAR_COMM STAR_ASSOC]); 606 607 608(* ----------------------------------------------------------------------------- *) 609(* Extra *) 610(* ----------------------------------------------------------------------------- *) 611 612val aligned4_thm = store_thm("aligned4_thm", 613 ``!a. aligned (a,4) = ALIGNED a``, 614 Cases \\ ASM_SIMP_TAC std_ss [arm_coretypesTheory.aligned_def, 615 arm_coretypesTheory.align_def,w2n_n2w,ALIGNED_n2w,n2w_11] 616 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [] 617 \\ (STRIP_ASSUME_TAC o Q.SPEC `n` o GSYM o 618 RW1 [arithmeticTheory.MULT_COMM] o MATCH_MP arithmeticTheory.DIVISION) (DECIDE ``0 < 4:num``) 619 \\ Cases_on `n MOD 4 = 0` \\ FULL_SIMP_TAC std_ss [] 620 \\ `(4 * (n DIV 4)) < 4294967296` by DECIDE_TAC 621 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 622 623val aligned2_thm = store_thm("aligned2_thm", 624 ``!a:word32. aligned (a,2) = (a && 1w = 0w)``, 625 Cases \\ ASM_SIMP_TAC std_ss [arm_coretypesTheory.aligned_def, 626 arm_coretypesTheory.align_def,w2n_n2w,n2w_and_1,n2w_11] 627 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [] 628 \\ (STRIP_ASSUME_TAC o Q.SPEC `n` o GSYM o 629 RW1 [arithmeticTheory.MULT_COMM] o MATCH_MP arithmeticTheory.DIVISION) (DECIDE ``0 < 2:num``) 630 \\ Cases_on `n MOD 2 = 0` \\ FULL_SIMP_TAC std_ss [] 631 \\ `(2 * (n DIV 2)) < 4294967296` by DECIDE_TAC 632 \\ `0 < 2:num` by DECIDE_TAC 633 \\ `n MOD 2 < 2` by METIS_TAC [arithmeticTheory.MOD_LESS] 634 \\ `n MOD 2 < 4294967296` by DECIDE_TAC 635 \\ ASM_SIMP_TAC std_ss [] 636 \\ DECIDE_TAC); 637 638val ADD_WITH_CARRY_SUB_n2w = save_thm("ADD_WITH_CARRY_SUB_n2w", 639 ((RAND_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) 640 (ONCE_REWRITE_CONV [GSYM WORD_NOT_NOT] THENC 641 ONCE_REWRITE_CONV [word_1comp_n2w] THENC 642 SIMP_CONV (std_ss++wordsLib.SIZES_ss) []) THENC 643 REWRITE_CONV [ADD_WITH_CARRY_SUB]) 644 ``add_with_carry (x:word32,n2w n,T)``); 645 646val UPDATE_FCP = prove( 647 ``!k b f. (k :+ b) ((FCP i. f i):'a word) = (FCP i. if i = k then b else f i):'a word``, 648 SIMP_TAC std_ss [fcpTheory.CART_EQ,fcpTheory.FCP_BETA] 649 \\ ONCE_REWRITE_TAC [fcpTheory.FCP_APPLY_UPDATE_THM] 650 \\ SIMP_TAC std_ss [fcpTheory.CART_EQ,fcpTheory.FCP_BETA] \\ METIS_TAC []); 651 652val ARM_READ_MASKED_CPSR_INTRO = store_thm("ARM_READ_MASKED_CPSR_INTRO", 653 ``encode_psr (ARM_READ_CPSR s) = 654 (31 :+ ARM_READ_STATUS psrN s) 655 ((30 :+ ARM_READ_STATUS psrZ s) 656 ((29 :+ ARM_READ_STATUS psrC s) 657 ((28 :+ ARM_READ_STATUS psrV s) 658 ((27 :+ ARM_READ_STATUS psrQ s) (ARM_READ_MASKED_CPSR s)))))``, 659 SIMP_TAC std_ss [ARM_READ_CPSR_def,ARM_READ_MASKED_CPSR_THM,UPDATE_FCP,encode_psr_def] 660 \\ SIMP_TAC std_ss [fcpTheory.CART_EQ,fcpTheory.FCP_BETA] 661 \\ SIMP_TAC std_ss [ARM_READ_STATUS_def,ARM_READ_CPSR_def] 662 \\ SIMP_TAC (std_ss++SIZES_ss) [] \\ REPEAT STRIP_TAC 663 \\ Cases_on `i = 31` \\ ASM_SIMP_TAC std_ss [] 664 \\ Cases_on `i = 30` \\ ASM_SIMP_TAC std_ss [] 665 \\ Cases_on `i = 29` \\ ASM_SIMP_TAC std_ss [] 666 \\ Cases_on `i = 28` \\ ASM_SIMP_TAC std_ss [] 667 \\ Cases_on `i = 27` \\ ASM_SIMP_TAC std_ss [] 668 \\ Cases_on `i < 27` \\ ASM_SIMP_TAC std_ss [] 669 \\ `F` by DECIDE_TAC); 670 671val FCP_UPDATE_WORD_AND = store_thm("FCP_UPDATE_WORD_AND", 672 ``((j :+ b) w) && v = (j :+ v ' j /\ b) (w && ((j :+ F) v))``, 673 SIMP_TAC std_ss [fcpTheory.CART_EQ,fcpTheory.FCP_BETA,word_and_def] 674 \\ ONCE_REWRITE_TAC [fcpTheory.FCP_APPLY_UPDATE_THM] 675 \\ SIMP_TAC std_ss [fcpTheory.FCP_BETA] 676 \\ ONCE_REWRITE_TAC [fcpTheory.FCP_APPLY_UPDATE_THM] 677 \\ SIMP_TAC std_ss [fcpTheory.FCP_BETA] \\ METIS_TAC []); 678 679 680(* Stack --- sp points at top of stack, stack grows towards smaller addresses *) 681 682val SEP_HIDE_ARRAY_def = Define ` 683 SEP_HIDE_ARRAY p i a n = SEP_EXISTS xs. SEP_ARRAY p i a xs * cond (LENGTH xs = n)`; 684 685val aSTACK_def = Define ` 686 aSTACK bp n xs = 687 SEP_ARRAY aM 4w bp xs * cond (ALIGNED bp) * 688 SEP_HIDE_ARRAY aM (-4w) (bp - 4w) n`; 689 690val SEP_HIDE_ARRAY_SUC = prove( 691 ``SEP_HIDE_ARRAY aM w a (SUC n) = ~aM a * SEP_HIDE_ARRAY aM w (a + w) n``, 692 SIMP_TAC std_ss [SEP_HIDE_ARRAY_def,SEP_CLAUSES,FUN_EQ_THM,SEP_EXISTS_THM] 693 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 694 (Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,cond_STAR,SEP_ARRAY_def] 695 \\ Q.EXISTS_TAC `t` \\ FULL_SIMP_TAC std_ss [word_sub_def,SEP_CLAUSES] 696 \\ FULL_SIMP_TAC std_ss [SEP_HIDE_def,SEP_CLAUSES,SEP_EXISTS_THM] 697 \\ Q.EXISTS_TAC `h` \\ FULL_SIMP_TAC std_ss []) 698 \\ FULL_SIMP_TAC std_ss [SEP_HIDE_def,SEP_CLAUSES,SEP_EXISTS_THM,cond_STAR] 699 \\ Q.EXISTS_TAC `x'::xs` 700 \\ FULL_SIMP_TAC std_ss [LENGTH,SEP_ARRAY_def,cond_STAR,STAR_ASSOC]); 701 702val SEP_EXISTS_aSTACK = store_thm("SEP_EXISTS_aSTACK", 703 ``((SEP_EXISTS x. p x * q) = (SEP_EXISTS x. p x) * q) /\ 704 ((SEP_EXISTS x. q * p x) = q * (SEP_EXISTS x. p x)) /\ 705 ((SEP_EXISTS x. aSTACK a n (x::xs)) = aSTACK (a + 4w) (n + 1) xs)``, 706 SIMP_TAC std_ss [SEP_CLAUSES,aSTACK_def,GSYM ADD1,ALIGNED, 707 SEP_HIDE_ARRAY_SUC,SEP_ARRAY_def,WORD_ADD_SUB] 708 THEN SIMP_TAC std_ss [SEP_CLAUSES,SEP_HIDE_def,STAR_ASSOC,GSYM word_sub_def] 709 THEN SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM]); 710 711 712(* ----------------------------------------------------------------------------- *) 713(* Reading/writing chunks of memory *) 714(* ----------------------------------------------------------------------------- *) 715 716val READ8_def = Define ` 717 READ8 a (m:word32 -> word8) = m a`; 718 719val WRITE8_def = Define ` 720 WRITE8 (a:word32) (w:word8) m = (a =+ w:word8) m`; 721 722val _ = wordsLib.guess_lengths(); 723val READ32_def = zDefine ` 724 READ32 a (m:word32 -> word8) = 725 (m (a + 3w) @@ m (a + 2w) @@ m (a + 1w) @@ m (a)):word32`; 726 727val WRITE32_def = zDefine ` 728 WRITE32 (a:word32) (w:word32) m = 729 ((a + 0w =+ (w2w w):word8) 730 ((a + 1w =+ (w2w (w >>> 8)):word8) 731 ((a + 2w =+ (w2w (w >>> 16)):word8) 732 ((a + 3w =+ (w2w (w >>> 24)):word8) m))))`; 733 734val WRITE32_blast_lemma = blastLib.BBLAST_PROVE 735 ``((( 7 >< 0) (w:word32)) = (w2w w):word8) /\ 736 (((15 >< 8) (w:word32)) = (w2w (w >>> 8)):word8) /\ 737 (((23 >< 16) (w:word32)) = (w2w (w >>> 16)):word8) /\ 738 (((31 >< 24) (w:word32)) = (w2w (w >>> 24)):word8)`` 739 740val WRITE32_THM = store_thm("WRITE32_THM", 741 ``!a w. 742 (((a =+ (( 7 >< 0) w):word8) 743 ((a + 1w =+ ((15 >< 8) w):word8) 744 ((a + 2w =+ ((23 >< 16) w):word8) 745 ((a + 3w =+ ((31 >< 24) w):word8) m)))) = WRITE32 a w m) /\ 746 (((a + 3w =+ ((31 >< 24) w):word8) 747 ((a + 2w =+ ((23 >< 16) w):word8) 748 ((a + 1w =+ ((15 >< 8) w):word8) 749 ((a =+ (( 7 >< 0) w):word8) m)))) = WRITE32 a w m)``, 750 SIMP_TAC std_ss [GSYM WRITE32_blast_lemma,WRITE32_def,APPLY_UPDATE_THM,FUN_EQ_THM] 751 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_LCANCEL, 752 RW [WORD_ADD_0] (Q.SPECL [`w`,`0w`] WORD_EQ_ADD_LCANCEL), 753 RW [WORD_ADD_0] (Q.SPECL [`w`,`v`,`0w`] WORD_EQ_ADD_LCANCEL),n2w_11]); 754 755 756val _ = export_theory(); 757