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