1 2open HolKernel boolLib bossLib Parse; 3open pred_setTheory res_quanTheory wordsTheory wordsLib bitTheory arithmeticTheory; 4open listTheory pairTheory combinTheory addressTheory; 5 6open set_sepTheory progTheory x86_Theory x86_seq_monadTheory x86_icacheTheory; 7 8val _ = new_theory "prog_x86"; 9 10 11infix \\ 12val op \\ = op THEN; 13 14val RW = REWRITE_RULE; 15val RW1 = ONCE_REWRITE_RULE; 16 17 18(* ----------------------------------------------------------------------------- *) 19(* The x86 set *) 20(* ----------------------------------------------------------------------------- *) 21 22val _ = Hol_datatype ` 23 x86_el = xReg of Xreg => word32 24 | xStatus of Xeflags => bool option 25 | xEIP of word32 26 | xMem of word32 => ((word8 # x86_permission set) option) => bool `; 27 28val x86_el_11 = DB.fetch "-" "x86_el_11"; 29val x86_el_distinct = DB.fetch "-" "x86_el_distinct"; 30 31val _ = Parse.type_abbrev("x86_set",``:x86_el set``); 32 33 34(* ----------------------------------------------------------------------------- *) 35(* Converting from x86-state tuple to x86_set *) 36(* ----------------------------------------------------------------------------- *) 37 38val x86_2set'_def = Define ` 39 x86_2set' (rs,st,ep,ms) (r,e,s,m,i) = 40 IMAGE (\a. xReg a (r a)) rs UNION 41 IMAGE (\a. xStatus a (s a)) st UNION 42 (if ep then {xEIP e} else {}) UNION 43 IMAGE (\a. xMem a (m a) (X86_ACCURATE a (r,e,s,m,i))) ms`; 44 45val x86_2set_def = Define `x86_2set s = x86_2set' (UNIV,UNIV,T,UNIV) s`; 46val x86_2set''_def = Define `x86_2set'' x s = x86_2set s DIFF x86_2set' x s`; 47 48(* theorems *) 49 50val x86_2set'_SUBSET_x86_2set = prove( 51 ``!y s. x86_2set' y s SUBSET x86_2set s``, 52 STRIP_TAC \\ STRIP_TAC 53 \\ `?rs st ep ms. y = (rs,st,ep,ms)` by METIS_TAC [PAIR] 54 \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] 55 \\ ASM_SIMP_TAC std_ss [] 56 \\ SIMP_TAC std_ss [SUBSET_DEF,x86_2set'_def,x86_2set_def,IN_IMAGE,IN_UNION,IN_UNIV] 57 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [NOT_IN_EMPTY]); 58 59val SPLIT_x86_2set = prove( 60 ``!x s. SPLIT (x86_2set s) (x86_2set' x s, x86_2set'' x s)``, 61 REPEAT STRIP_TAC 62 \\ ASM_SIMP_TAC std_ss [SPLIT_def,EXTENSION,IN_UNION,IN_DIFF,x86_2set''_def] 63 \\ `x86_2set' x s SUBSET x86_2set s` by METIS_TAC [x86_2set'_SUBSET_x86_2set] 64 \\ SIMP_TAC bool_ss [DISJOINT_DEF,EXTENSION,IN_INTER,NOT_IN_EMPTY,IN_DIFF] 65 \\ METIS_TAC [SUBSET_DEF]); 66 67val PUSH_IN_INTO_IF = METIS_PROVE [] 68 ``!g x y z. x IN (if g then y else z) = if g then x IN y else x IN z``; 69 70val SUBSET_x86_2set = prove( 71 ``!u s. u SUBSET x86_2set s = ?y. u = x86_2set' y s``, 72 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 73 \\ ASM_REWRITE_TAC [x86_2set'_SUBSET_x86_2set] 74 \\ Q.EXISTS_TAC `({ a | a| ?x. xReg a x IN u },{ a | a| ?x. xStatus a x IN u }, 75 (?x. xEIP x IN u),{ a | a| ?x y. xMem a x y IN u })` 76 \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] 77 \\ FULL_SIMP_TAC std_ss [x86_2set'_def,x86_2set_def,EXTENSION,SUBSET_DEF,IN_IMAGE, 78 IN_UNION,GSPECIFICATION,IN_INSERT,NOT_IN_EMPTY,IN_UNIV] 79 \\ STRIP_TAC \\ ASM_REWRITE_TAC [] \\ EQ_TAC \\ REPEAT STRIP_TAC 80 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [x86_el_11,x86_el_distinct] 81 \\ FULL_SIMP_TAC std_ss [PUSH_IN_INTO_IF,NOT_IN_EMPTY,IN_INSERT] 82 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [x86_el_11,x86_el_distinct] 83 \\ METIS_TAC []); 84 85val SPLIT_x86_2set_EXISTS = prove( 86 ``!s u v. SPLIT (x86_2set s) (u,v) = ?y. (u = x86_2set' y s) /\ (v = x86_2set'' y s)``, 87 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_REWRITE_TAC [SPLIT_x86_2set] 88 \\ FULL_SIMP_TAC bool_ss [SPLIT_def,x86_2set'_def,x86_2set''_def] 89 \\ `u SUBSET (x86_2set s)` by 90 (FULL_SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_UNION] \\ METIS_TAC []) 91 \\ FULL_SIMP_TAC std_ss [SUBSET_x86_2set] \\ Q.EXISTS_TAC `y` \\ REWRITE_TAC [] 92 \\ FULL_SIMP_TAC std_ss [EXTENSION,IN_DIFF,IN_UNION,DISJOINT_DEF,NOT_IN_EMPTY,IN_INTER] 93 \\ METIS_TAC []); 94 95val X86_GET_MEMORY_def = Define `X86_GET_MEMORY (r,e,t,m,i) = m`; 96 97val IN_x86_2set = prove(`` 98 (!r x s. xReg r x IN (x86_2set s) = (x = XREAD_REG r s)) /\ 99 (!r x s. xReg r x IN (x86_2set' (rs,st,e,ms) s) = (x = XREAD_REG r s) /\ r IN rs) /\ 100 (!r x s. xReg r x IN (x86_2set'' (rs,st,e,ms) s) = (x = XREAD_REG r s) /\ ~(r IN rs)) /\ 101 (!a x s. xStatus a x IN (x86_2set s) = (x = XREAD_EFLAG a s)) /\ 102 (!a x s. xStatus a x IN (x86_2set' (rs,st,e,ms) s) = (x = XREAD_EFLAG a s) /\ a IN st) /\ 103 (!a x s. xStatus a x IN (x86_2set'' (rs,st,e,ms) s) = (x = XREAD_EFLAG a s) /\ ~(a IN st)) /\ 104 (!x s. xEIP x IN (x86_2set s) = (x = XREAD_EIP s)) /\ 105 (!x s. xEIP x IN (x86_2set' (rs,st,e,ms) s) = (x = XREAD_EIP s) /\ e) /\ 106 (!x s. xEIP x IN (x86_2set'' (rs,st,e,ms) s) = (x = XREAD_EIP s) /\ ~e) /\ 107 (!p x y s. xMem p x y IN (x86_2set s) = (X86_GET_MEMORY s p = x) /\ (y = X86_ACCURATE p s)) /\ 108 (!p x y s. xMem p x y IN (x86_2set' (rs,st,e,ms) s) = (X86_GET_MEMORY s p = x) /\ (y = X86_ACCURATE p s) /\ p IN ms) /\ 109 (!p x y s. xMem p x y IN (x86_2set'' (rs,st,e,ms) s) = (X86_GET_MEMORY s p = x) /\ (y = X86_ACCURATE p s) /\ ~(p IN ms))``, 110 REPEAT STRIP_TAC 111 \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] \\ ASM_SIMP_TAC std_ss [] 112 \\ SRW_TAC [] [x86_2set'_def,x86_2set''_def,x86_2set_def,IN_UNION, 113 IN_INSERT,NOT_IN_EMPTY,IN_DIFF,PUSH_IN_INTO_IF,XREAD_REG_def, 114 XREAD_EIP_def,XREAD_EFLAG_def,X86_GET_MEMORY_def] 115 \\ METIS_TAC []); 116 117val x86_2set''_11 = prove( 118 ``!y y2 s s2. (x86_2set'' y2 s2 = x86_2set'' y s) ==> (y = y2)``, 119 REPEAT STRIP_TAC \\ CCONTR_TAC 120 \\ `?rs st ep m st. y = (rs,st,ep,m)` by METIS_TAC [PAIR] 121 \\ `?rs2 st2 ep2 m2. y2 = (rs2,st2,ep2,m2)` by METIS_TAC [PAIR] 122 \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] 123 \\ `?r2 e2 t2 m2 i2. s2 = (r2,e2,t2,m2,i2)` by METIS_TAC [PAIR] 124 \\ FULL_SIMP_TAC bool_ss [PAIR_EQ,EXTENSION] 125 THEN1 126 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.SPEC `xReg xi yi`) 127 \\ FULL_SIMP_TAC std_ss [IN_x86_2set] \\ METIS_TAC []) 128 THEN1 129 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.SPEC `xStatus xi yi`) 130 \\ FULL_SIMP_TAC std_ss [IN_x86_2set] \\ METIS_TAC []) 131 THEN1 132 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `ei` o Q.SPEC `xEIP ei`) 133 \\ FULL_SIMP_TAC std_ss [IN_x86_2set] \\ METIS_TAC []) 134 THEN 135 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.GEN `zi` o Q.SPEC `xMem xi yi zi`) 136 \\ FULL_SIMP_TAC std_ss [IN_x86_2set] \\ METIS_TAC [])); 137 138val DELETE_x86_2set = prove(`` 139 (!a. (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) DELETE xReg a (r a) = 140 (x86_2set' (rs DELETE a,st,ei,ms) (r,e,s,m,i))) /\ 141 (!c. (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) DELETE xStatus c (s c) = 142 (x86_2set' (rs,st DELETE c,ei,ms) (r,e,s,m,i))) /\ 143 (!c. (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) DELETE xEIP e = 144 (x86_2set' (rs,st,F,ms) (r,e,s,m,i))) /\ 145 (!b. (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) DELETE xMem b (m b) (X86_ACCURATE b (r,e,s,m,i)) = 146 (x86_2set' (rs,st,ei,ms DELETE b) (r,e,s,m,i)))``, 147 REPEAT STRIP_TAC 148 \\ SRW_TAC [] [x86_2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR, 149 EXISTS_OR_THM,IN_DELETE,IN_INSERT,NOT_IN_EMPTY,PUSH_IN_INTO_IF, 150 XREAD_REG_def,XREAD_MEM_def,XREAD_EFLAG_def,XREAD_EIP_def] 151 \\ Cases_on `x` \\ SRW_TAC [] [] \\ METIS_TAC []); 152 153val EMPTY_x86_2set = prove(`` 154 (x86_2set' (rs,st,e,ms) s = {}) = (rs = {}) /\ (ms = {}) /\ (st = {}) /\ ~e``, 155 REPEAT STRIP_TAC 156 \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] \\ ASM_SIMP_TAC std_ss [] 157 \\ SRW_TAC [] [x86_2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR, 158 EXISTS_OR_THM,IN_DELETE,IN_INSERT,NOT_IN_EMPTY,PUSH_IN_INTO_IF] 159 \\ SIMP_TAC std_ss [x86_el_distinct,x86_el_11] \\ METIS_TAC [PAIR,FST]); 160 161 162(* ----------------------------------------------------------------------------- *) 163(* Defining the X86_MODEL *) 164(* ----------------------------------------------------------------------------- *) 165 166val xR_def = Define `xR a x = SEP_EQ {xReg a x}`; 167val xM1_def = Define `xM1 a x b = SEP_EQ {xMem a x b}`; 168val xS1_def = Define `xS1 a x = SEP_EQ {xStatus a x}`; 169val xPC_def = Define `xPC x = SEP_EQ {xEIP x}`; 170 171val xS_def = Define ` 172 xS (x0,x1,x2,x3,x4,x5) = 173 xS1 X_CF x0 * xS1 X_PF x1 * xS1 X_AF x2 * 174 xS1 X_ZF x3 * xS1 X_SF x4 * xS1 X_OF x5`; 175 176val X86_INSTR_PERM_def = Define ` 177 X86_INSTR_PERM b = {Xread;Xexecute} UNION (if b then {Xwrite} else {})`; 178 179val X86_INSTR_def = Define ` 180 (X86_INSTR (a,([],b)) = {}) /\ 181 (X86_INSTR (a,((c:word8)::cs,b)) = 182 xMem a (SOME (c,X86_INSTR_PERM b)) T INSERT X86_INSTR (a+1w,(cs,b)))`; 183 184val X86_MODEL_def = Define ` 185 X86_MODEL = (x86_2set, X86_NEXT_REL, X86_INSTR, X86_ICACHE, 186 (K F):x86_state->bool)`; 187 188val xCODE_def = Define `xCODE = CODE_POOL X86_INSTR`; 189 190val xM_def = Define ` 191 xM a (w:word32) = 192 ~xM1 a (SOME ((7 >< 0) w,{Xread;Xwrite})) * 193 ~xM1 (a + 1w) (SOME ((7 >< 0) (w >> 8),{Xread;Xwrite})) * 194 ~xM1 (a + 2w) (SOME ((7 >< 0) (w >> 16),{Xread;Xwrite})) * 195 ~xM1 (a + 3w) (SOME ((7 >< 0) (w >> 24),{Xread;Xwrite}))`; 196 197(* theorems *) 198 199val lemma = 200 METIS_PROVE [SPLIT_x86_2set] 201 ``p (x86_2set' y s) ==> (?u v. SPLIT (x86_2set s) (u,v) /\ p u /\ (\v. v = x86_2set'' y s) v)``; 202 203val X86_SPEC_SEMANTICS = store_thm("X86_SPEC_SEMANTICS", 204 ``SPEC X86_MODEL p {} q = 205 !y s t1 seq. 206 p (x86_2set' y t1) /\ X86_ICACHE t1 s /\ rel_sequence X86_NEXT_REL seq s ==> 207 ?k t2. q (x86_2set' y t2) /\ X86_ICACHE t2 (seq k) /\ (x86_2set'' y t1 = x86_2set'' y t2)``, 208 SIMP_TAC std_ss [GSYM RUN_EQ_SPEC,RUN_def,X86_MODEL_def,STAR_def,SEP_REFINE_def] 209 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC THENL [ 210 FULL_SIMP_TAC bool_ss [SPLIT_x86_2set_EXISTS] 211 \\ NTAC 3 (POP_ASSUM MP_TAC) \\ ASM_SIMP_TAC std_ss [] 212 \\ REPEAT STRIP_TAC \\ RES_TAC 213 \\ Q.EXISTS_TAC `k` \\ Q.EXISTS_TAC `t2` 214 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [], 215 FULL_SIMP_TAC std_ss [METIS_PROVE [] ``((?x. P x) ==> b) = !x. P x ==> b``, 216 METIS_PROVE [] ``(b /\ (?x. P x)) = ?x. b /\ P x``] 217 \\ FULL_SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 218 \\ IMP_RES_TAC lemma \\ RES_TAC 219 \\ FULL_SIMP_TAC bool_ss [SPLIT_x86_2set_EXISTS] 220 \\ IMP_RES_TAC x86_2set''_11 \\ METIS_TAC []]); 221 222 223(* ----------------------------------------------------------------------------- *) 224(* Theorems for construction of |- SPEC X86_MODEL ... *) 225(* ----------------------------------------------------------------------------- *) 226 227val STAR_x86_2set = store_thm("STAR_x86_2set", 228 ``((xR a x * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 229 (x = r a) /\ a IN rs /\ p (x86_2set' (rs DELETE a,st,ei,ms) (r,e,s,m,i))) /\ 230 ((xS1 c z * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 231 (z = s c) /\ c IN st /\ p (x86_2set' (rs,st DELETE c,ei,ms) (r,e,s,m,i))) /\ 232 ((xPC q * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 233 (q = e) /\ ei /\ p (x86_2set' (rs,st,F,ms) (r,e,s,m,i))) /\ 234 ((xM1 b y w * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 235 (y = m b) /\ (w = X86_ACCURATE b (r,e,s,m,i)) /\ b IN ms /\ p (x86_2set' (rs,st,ei,ms DELETE b) (r,e,s,m,i))) /\ 236 ((~(xM1 b y) * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 237 (y = m b) /\ b IN ms /\ p (x86_2set' (rs,st,ei,ms DELETE b) (r,e,s,m,i))) /\ 238 ((cond g * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 239 g /\ p (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)))``, 240 REPEAT STRIP_TAC 241 \\ SIMP_TAC std_ss [SEP_HIDE_def,SEP_CLAUSES] 242 \\ SIMP_TAC std_ss [SEP_EXISTS] 243 \\ SIMP_TAC std_ss [xR_def,xS1_def,xM1_def,EQ_STAR,INSERT_SUBSET,cond_STAR,xPC_def,XREAD_EIP_def, 244 EMPTY_SUBSET,IN_x86_2set,XREAD_REG_def,XREAD_EFLAG_def,XREAD_MEM_def,GSYM DELETE_DEF,X86_GET_MEMORY_def] 245 THEN1 METIS_TAC [DELETE_x86_2set] 246 THEN1 METIS_TAC [DELETE_x86_2set] 247 THEN1 METIS_TAC [DELETE_x86_2set] 248 \\ Cases_on `y = m b` \\ ASM_SIMP_TAC std_ss [] 249 \\ Cases_on `w = X86_ACCURATE b (r,e,s,m,i)` 250 \\ ASM_SIMP_TAC std_ss [DELETE_x86_2set,AC CONJ_ASSOC CONJ_COMM]); 251 252val CODE_POOL_x86_2set_AUX_LEMMA = prove( 253 ``!x y z. ~(z IN y) ==> ((x = z INSERT y) = z IN x /\ (x DELETE z = y))``, 254 SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY,IN_DELETE] \\ METIS_TAC []); 255 256val address_list_def = Define ` 257 (address_list a 0 = {}) /\ 258 (address_list a (SUC n) = a INSERT address_list (a+1w) n)`; 259 260val x86_pool_def = Define ` 261 (x86_pool (r,s,e,m,i) p ([],d) = T) /\ 262 (x86_pool (r,s,e,m,i) p ((c::cs),d) = 263 (SOME (c:word8,X86_INSTR_PERM d) = m p) /\ X86_ACCURATE p (r,s,e,m,i) /\ 264 x86_pool (r,s,e,m,i) (p+1w) (cs,d))`; 265 266val LEMMA1 = prove( 267 ``!p q cs y b. xMem p y b IN X86_INSTR (q,(cs,d)) ==> ?k. k < LENGTH cs /\ (p = q + n2w k)``, 268 Induct_on `cs` 269 \\ ASM_SIMP_TAC std_ss [X86_INSTR_def,EMPTY_SUBSET,LENGTH,NOT_IN_EMPTY, 270 address_list_def,IN_INSERT,x86_el_11,n2w_11] 271 \\ REPEAT STRIP_TAC THEN1 (Q.EXISTS_TAC `0` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0]) 272 \\ RES_TAC \\ Q.EXISTS_TAC `k + 1` 273 \\ ASM_SIMP_TAC bool_ss [ADD1,GSYM word_add_n2w,WORD_ADD_ASSOC] 274 \\ STRIP_TAC THEN1 DECIDE_TAC \\ METIS_TAC [WORD_ADD_ASSOC,WORD_ADD_COMM]); 275 276val LEMMA2 = prove( 277 ``!p q cs. p IN address_list q (LENGTH cs) ==> ?k. k < LENGTH cs /\ (p = q + n2w k)``, 278 Induct_on `cs` 279 \\ ASM_SIMP_TAC std_ss [X86_INSTR_def,EMPTY_SUBSET,LENGTH,NOT_IN_EMPTY, 280 address_list_def,IN_INSERT,x86_el_11,n2w_11] 281 \\ REPEAT STRIP_TAC THEN1 (Q.EXISTS_TAC `0` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0]) 282 \\ RES_TAC \\ Q.EXISTS_TAC `k + 1` 283 \\ ASM_SIMP_TAC bool_ss [ADD1,GSYM word_add_n2w,WORD_ADD_ASSOC] 284 \\ STRIP_TAC THEN1 DECIDE_TAC \\ METIS_TAC [WORD_ADD_ASSOC,WORD_ADD_COMM]); 285 286val CODE_POOL_x86_2set_LEMMA = prove( 287 ``!cs p ms. 288 LENGTH cs < 5000 ==> 289 (xCODE {(p,(cs,d))} (x86_2set' (rs,st,ei,ms) (r,s,e,m,i)) = 290 (ms = address_list p (LENGTH cs)) /\ (rs = {}) /\ (st = {}) /\ ~ei /\ 291 x86_pool (r,s,e,m,i) p (cs,d))``, 292 Induct 293 \\ FULL_SIMP_TAC bool_ss [INSERT_SUBSET,GSYM DELETE_DEF, 294 LENGTH,x86_pool_def, EMPTY_SUBSET,xCODE_def, 295 IN_DELETE, IMAGE_INSERT, CODE_POOL_def, IMAGE_EMPTY, 296 XREAD_MEM_def, address_list_def, BIGUNION_INSERT, BIGUNION_EMPTY, 297 UNION_EMPTY, X86_INSTR_def, IN_x86_2set, EMPTY_x86_2set] 298 THEN1 METIS_TAC [] 299 \\ REPEAT STRIP_TAC 300 \\ `LENGTH cs < 5000` by DECIDE_TAC 301 \\ Cases_on `xMem p (SOME (h,X86_INSTR_PERM d)) T IN X86_INSTR (p + 1w,(cs,d))` 302 THEN1 (IMP_RES_TAC LEMMA1 303 \\ FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [ 304 REWRITE_RULE [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL), 305 GSYM WORD_ADD_ASSOC,word_add_n2w,n2w_11] 306 \\ `1 + k < 4294967296` by DECIDE_TAC 307 \\ FULL_SIMP_TAC std_ss [LESS_MOD]) 308 \\ Cases_on `p IN address_list (p + 1w) (LENGTH cs)` 309 THEN1 (IMP_RES_TAC LEMMA2 310 \\ FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [ 311 REWRITE_RULE [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL), 312 GSYM WORD_ADD_ASSOC,word_add_n2w,n2w_11] 313 \\ `1 + k < 4294967296` by DECIDE_TAC 314 \\ FULL_SIMP_TAC std_ss [LESS_MOD]) 315 \\ ASM_SIMP_TAC bool_ss [CODE_POOL_x86_2set_AUX_LEMMA,GSYM CONJ_ASSOC,IN_x86_2set,XREAD_MEM_def] 316 \\ Cases_on `SOME (h,X86_INSTR_PERM d) = m p` \\ ASM_REWRITE_TAC [] 317 \\ REWRITE_TAC [DIFF_INSERT,DELETE_x86_2set,X86_GET_MEMORY_def] 318 \\ Cases_on `X86_ACCURATE p (r,s,e,m,i)` \\ ASM_SIMP_TAC std_ss [] 319 \\ `xMem p (m p) T = xMem p (m p) (X86_ACCURATE p (r,s,e,m,i))` by 320 FULL_SIMP_TAC std_ss [x86_el_11] 321 \\ ONCE_ASM_REWRITE_TAC [] \\ NTAC 2 (POP_ASSUM (K ALL_TAC)) 322 \\ REWRITE_TAC [DIFF_INSERT,DELETE_x86_2set,X86_GET_MEMORY_def] 323 \\ Cases_on `p IN ms` \\ ASM_REWRITE_TAC [GSYM CONJ_ASSOC] 324 \\ FULL_SIMP_TAC bool_ss []); 325 326val CODE_POOL_x86_2set = store_thm("CODE_POOL_x86_2set", 327 ``!cs p ms. 328 xCODE {(p,(cs,d))} (x86_2set' (rs,st,ei,ms) (r,s,e,m,i)) = 329 if LENGTH cs < 5000 then 330 (ms = address_list p (LENGTH cs)) /\ (rs = {}) /\ (st = {}) /\ ~ei /\ 331 x86_pool (r,s,e,m,i) p (cs,d) 332 else xCODE {(p,(cs,d))} (x86_2set' (rs,st,ei,ms) (r,s,e,m,i))``, 333 METIS_TAC [CODE_POOL_x86_2set_LEMMA]); 334 335val icache_revert_def = Define ` 336 icache_revert (m1:x86_memory,i1:x86_memory) (m2:x86_memory,i2:x86_memory) a = 337 if m1 a = m2 a then i1 a else i2 a`; 338 339val X86_ACCURATE_UPDATE = store_thm("X86_ACCURATE_UPDATE", 340 ``(X86_ACCURATE a ((xr =+ yr) r,e,s,m,i) = X86_ACCURATE a (r,e,s,m,i)) /\ 341 (X86_ACCURATE a (r,xe,s,m,i) = X86_ACCURATE a (r,e,s,m,i)) /\ 342 (X86_ACCURATE a (r,e,(xs =+ ys) s,m,i) = X86_ACCURATE a (r,e,s,m,i)) /\ 343 (~(xm = a) ==> (X86_ACCURATE a (r,e,s,(xm =+ ym) m,i) = X86_ACCURATE a (r,e,s,m,i))) /\ 344 (~(a = b) ==> 345 (X86_ACCURATE a (r,e,s,m,icache_revert (m,i) ((b =+ w) m2,i2)) = 346 X86_ACCURATE a (r,e,s,m,icache_revert (m,i) (m2,i2))))``, 347 SIMP_TAC std_ss [X86_ACCURATE_def,APPLY_UPDATE_THM,icache_revert_def]); 348 349val icache_revert_ID = store_thm("icache_revert_ID", 350 ``!m i y. icache_revert (m,i) (m,y) = i``, 351 SIMP_TAC std_ss [FUN_EQ_THM,icache_revert_def]); 352 353val icache_revert_update = prove( 354 ``b IN ms ==> 355 (x86_2set'' (rs,st,ei,ms) (r,x,t,m, icache_revert (m,i) ((b =+ w) m2,j)) = 356 x86_2set'' (rs,st,ei,ms) (r,x,t,m, icache_revert (m,i) (m2,j)))``, 357 SIMP_TAC std_ss [EXTENSION] \\ STRIP_TAC \\ Cases 358 \\ SIMP_TAC std_ss [IN_x86_2set,XREAD_REG_def,XREAD_EFLAG_def,APPLY_UPDATE_THM, 359 XREAD_EIP_def,X86_GET_MEMORY_def,X86_ACCURATE_def,icache_revert_def] 360 \\ METIS_TAC []); 361 362val UPDATE_x86_2set'' = store_thm("UPDATE_x86_2set''", 363 ``(!a x. a IN rs ==> 364 (x86_2set'' (rs,st,ei,ms) ((a =+ x) r,e,s,m,i) = x86_2set'' (rs,st,ei,ms) (r,e,s,m,i))) /\ 365 (!a x. a IN st ==> 366 (x86_2set'' (rs,st,ei,ms) (r,e,(a =+ x) s,m,i) = x86_2set'' (rs,st,ei,ms) (r,e,s,m,i))) /\ 367 (!a x y. 368 ((x86_2set'' (rs,st,T,ms) (r,x,s,m,i) = x86_2set'' (rs,st,T,ms) (r,y,s,m,i)) = T)) /\ 369 (!a x. a IN ms ==> 370 (x86_2set'' (rs,st,ei,ms) (r,e,s,(a =+ x) m,i) = x86_2set'' (rs,st,ei,ms) (r,e,s,m,i))) /\ 371 (!a x. a IN ms ==> 372 (x86_2set'' (rs,st,ei,ms) (r,x,t,m, icache_revert (m,i) ((a =+ w) m2,j)) = 373 x86_2set'' (rs,st,ei,ms) (r,x,t,m, icache_revert (m,i) (m2,j))))``, 374 SIMP_TAC std_ss [x86_2set_def,x86_2set''_def,x86_2set'_def,EXTENSION,IN_UNION, 375 IN_INSERT,NOT_IN_EMPTY,IN_IMAGE,IN_DIFF,IN_UNIV,XREAD_REG_def,XREAD_MEM_def, 376 XREAD_EFLAG_def,APPLY_UPDATE_THM,XREAD_EIP_def,icache_revert_update] 377 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 378 \\ ASM_SIMP_TAC std_ss [] \\ SRW_TAC [] [X86_ACCURATE_UPDATE] 379 \\ METIS_TAC [X86_ACCURATE_UPDATE]); 380 381val X86_SPEC_CODE = save_thm("X86_SPEC_CODE", 382 RW [GSYM X86_MODEL_def,GSYM xCODE_def] 383 (SIMP_RULE std_ss [X86_MODEL_def] (Q.ISPEC `X86_MODEL` SPEC_CODE))); 384 385val IMP_X86_SPEC_LEMMA = prove( 386 ``!p q. 387 (!y s t1. 388 p (x86_2set' y t1) /\ X86_ICACHE t1 s ==> 389 ?v t2. 390 p (x86_2set' y s) /\ 391 (X86_NEXT s = SOME v) /\ q (x86_2set' y t2) /\ X86_ICACHE t2 v /\ 392 (x86_2set'' y t1 = x86_2set'' y t2)) ==> 393 SPEC X86_MODEL p {} q``, 394 REWRITE_TAC [X86_SPEC_SEMANTICS] \\ REPEAT STRIP_TAC 395 \\ `p (x86_2set' y s)` by METIS_TAC [] 396 \\ `X86_NEXT_REL (seq 0) (seq (SUC 0))` by 397 (`?x. X86_NEXT_REL (seq 0) x` by 398 (RES_TAC \\ Q.EXISTS_TAC `v'` 399 \\ ASM_SIMP_TAC std_ss [X86_NEXT_REL_def] 400 \\ Q.EXISTS_TAC `seq 0` \\ ASM_SIMP_TAC std_ss [] 401 \\ FULL_SIMP_TAC bool_ss [rel_sequence_def,X86_ICACHE_REFL]) 402 \\ METIS_TAC [rel_sequence_def]) 403 \\ FULL_SIMP_TAC std_ss [X86_NEXT_REL_def] 404 \\ `seq 0 = s` by FULL_SIMP_TAC std_ss [rel_sequence_def] 405 \\ FULL_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `1` 406 \\ `X86_ICACHE t1 u` by IMP_RES_TAC X86_ICACHE_TRANS 407 \\ Q.PAT_ASSUM `!y s t1. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o 408 RW [GSYM AND_IMP_INTRO] o Q.SPECL [`y`,`u`,`t1`]) 409 \\ Q.EXISTS_TAC `t2` 410 \\ FULL_SIMP_TAC std_ss [optionTheory.SOME_11] \\ METIS_TAC []); 411 412val X86_ICACHE_EXTRACT_def = Define ` 413 X86_ICACHE_EXTRACT ((r1,e1,s1,m1,i1):x86_state) = i1`; 414 415val X86_ICACHE_THM2 = prove( 416 ``!s t. X86_ICACHE s t = ?z. t = X86_ICACHE_UPDATE z s``, 417 REPEAT STRIP_TAC 418 \\ `?r1 e1 s1 m1 i1. s = (r1,e1,s1,m1,i1)` by METIS_TAC [PAIR] 419 \\ `?r2 e2 s2 m2 i2. t = (r2,e2,s2,m2,i2)` by METIS_TAC [PAIR] 420 \\ FULL_SIMP_TAC std_ss [X86_ICACHE_UPDATE_def,X86_ICACHE_THM]); 421 422val X86_ICACHE_X86_ACCURATE = prove( 423 ``X86_ICACHE (r1,e1,s1,m1,i1) (r1,e1,s1,m1,i2) = 424 !a. X86_ACCURATE a (r1,e1,s1,m1,i2) \/ (i1 a = i2 a)``, 425 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 426 THEN1 (FULL_SIMP_TAC std_ss [X86_ACCURATE_def,X86_ICACHE_def,FUN_EQ_THM] 427 \\ Cases_on `a IN insert` \\ ASM_SIMP_TAC std_ss [] 428 \\ Cases_on `a IN delete` \\ ASM_SIMP_TAC std_ss []) 429 \\ SIMP_TAC std_ss [X86_ICACHE_def,FUN_EQ_THM] 430 \\ Q.EXISTS_TAC `{ a | X86_ACCURATE a (r1,e1,s1,m1,i2) /\ ~(i2 a = NONE) }` 431 \\ Q.EXISTS_TAC `{ a | X86_ACCURATE a (r1,e1,s1,m1,i2) /\ (i2 a = NONE) }` 432 \\ SIMP_TAC std_ss [GSPECIFICATION] 433 \\ REPEAT STRIP_TAC 434 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `addr`) 435 \\ Cases_on `X86_ACCURATE addr (r1,e1,s1,m1,i2)` 436 \\ FULL_SIMP_TAC std_ss [] 437 \\ FULL_SIMP_TAC std_ss [X86_ACCURATE_def] \\ METIS_TAC []); 438 439val X86_ICACHE_icache_revert = prove( 440 ``X86_ICACHE (r1,e1,s1,m1,i1) (r1,e1,s1,m1,i2) ==> 441 X86_ICACHE (r2,e2,s2,m2,icache_revert (m1,i1) (m2,i2)) (r2,e2,s2,m2,i2)``, 442 SIMP_TAC std_ss [X86_ICACHE_X86_ACCURATE] \\ REPEAT STRIP_TAC 443 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `a`) 444 \\ FULL_SIMP_TAC std_ss [X86_ACCURATE_def,icache_revert_def] 445 \\ Cases_on `m1 a = m2 a` \\ ASM_SIMP_TAC std_ss []); 446 447val X86_ICACHE_REVERT_def = Define ` 448 X86_ICACHE_REVERT (r2,e2,s2,m2,i2) (r1,e1,s1,m1,i1) = 449 (r2,e2,s2,m2,icache_revert (m1,i1) (m2,i2))`; 450 451val X86_ICACHE_X86_ICACHE_REVERT = store_thm("X86_ICACHE_X86_ICACHE_REVERT", 452 ``!s t u. X86_ICACHE s t /\ (X86_ICACHE_EXTRACT t = X86_ICACHE_EXTRACT u) ==> 453 X86_ICACHE (X86_ICACHE_REVERT u s) u``, 454 NTAC 3 STRIP_TAC 455 \\ `?r1 e1 s1 m1 i1. s = (r1,e1,s1,m1,i1)` by METIS_TAC [PAIR] 456 \\ `?r2 e2 s2 m2 i2. t = (r2,e2,s2,m2,i2)` by METIS_TAC [PAIR] 457 \\ `?r3 e3 s3 m3 i3. u = (r3,e3,s3,m3,i3)` by METIS_TAC [PAIR] 458 \\ FULL_SIMP_TAC std_ss [X86_ICACHE_REVERT_def,X86_ICACHE_EXTRACT_def] 459 \\ REPEAT STRIP_TAC 460 \\ `(r1,e1,s1,m1) = (r2,e2,s2,m2)` by FULL_SIMP_TAC std_ss [X86_ICACHE_def] 461 \\ FULL_SIMP_TAC std_ss [] 462 \\ METIS_TAC [X86_ICACHE_icache_revert]); 463 464val X86_ICACHE_EXTRACT_CLAUSES = store_thm("X86_ICACHE_EXTRACT_CLAUSES", 465 ``!s r w f fv. 466 (X86_ICACHE_EXTRACT (XWRITE_EIP w s) = X86_ICACHE_EXTRACT s) /\ 467 (X86_ICACHE_EXTRACT (XWRITE_REG r w s) = X86_ICACHE_EXTRACT s) /\ 468 (X86_ICACHE_EXTRACT (XWRITE_EFLAG f fv s) = X86_ICACHE_EXTRACT s)``, 469 REPEAT STRIP_TAC 470 THEN `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] 471 THEN ASM_SIMP_TAC std_ss [X86_ICACHE_EXTRACT_def,XWRITE_EIP_def, 472 XWRITE_REG_def,XWRITE_EFLAG_def]); 473 474val X86_ACCURATE_CLAUSES = store_thm("X86_ACCURATE_CLAUSES", 475 ``(X86_ACCURATE a ((r =+ w) x,e,s,m,i) = X86_ACCURATE a (x,e,s,m,i)) /\ 476 (X86_ACCURATE a (x,e,(f =+ fv) s,m,i) = X86_ACCURATE a (x,e,s,m,i)) /\ 477 (~(b = a) ==> (X86_ACCURATE a (x,e,s,(b =+ v) m,i) = X86_ACCURATE a (x,e,s,m,i)))``, 478 SIMP_TAC std_ss [X86_ACCURATE_def,APPLY_UPDATE_THM]); 479 480val X86_ACCURATE_IMP = store_thm("X86_ACCURATE_IMP", 481 ``X86_ACCURATE a (r,e2,t,m,i) ==> 482 X86_ACCURATE a (r,e1,t,m,icache_revert (m,i) (m,icache x m i)) /\ 483 X86_ACCURATE a (r,e1,t,m,icache x m i) /\ 484 X86_ACCURATE a (r,e1,t,m,i)``, 485 Cases_on `x` THEN SIMP_TAC std_ss [X86_ACCURATE_def,icache_revert_def,icache_def] 486 THEN METIS_TAC []); 487 488val XREAD_INSTR_IMP = store_thm("XREAD_INSTR_IMP", 489 ``!x r e t i m a w p. 490 (m a = SOME (w,X86_INSTR_PERM p)) /\ X86_ACCURATE a (r,e,t,m,i) ==> 491 (XREAD_INSTR a (r,e,t,m,icache x m i) = SOME w)``, 492 Cases THEN REPEAT STRIP_TAC 493 THEN FULL_SIMP_TAC std_ss [X86_ACCURATE_def,icache_def,XREAD_INSTR_def] 494 THEN Cases_on `a IN q` \\ ASM_SIMP_TAC std_ss [] 495 THEN Cases_on `a IN r` \\ ASM_SIMP_TAC (srw_ss()) [] 496 THEN Cases_on `p` \\ ASM_SIMP_TAC (srw_ss()) [X86_INSTR_PERM_def]); 497 498val X86_ICACHE_REVERT_EMPTY = prove( 499 ``(X86_ICACHE_EXTRACT v = X86_ICACHE_EMPTY) ==> 500 X86_ICACHE (X86_ICACHE_REVERT v (r,e,t,m,i)) v``, 501 REPEAT STRIP_TAC 502 \\ `?r1 e1 s1 m1 i1. v = (r1,e1,s1,m1,i1)` by METIS_TAC [PAIR] 503 \\ FULL_SIMP_TAC std_ss [X86_ICACHE_REVERT_def,X86_ICACHE_EXTRACT_def] 504 \\ FULL_SIMP_TAC std_ss [X86_ICACHE_def] 505 \\ Q.EXISTS_TAC `{}` \\ Q.EXISTS_TAC `UNIV` 506 \\ SIMP_TAC std_ss [NOT_IN_EMPTY,IN_UNIV,X86_ICACHE_EMPTY_def]); 507 508val IMP_X86_SPEC_LEMMA2 = prove( 509 ``!p q. 510 (!rs st ei ms x r e t m i. 511 p (x86_2set' (rs,st,ei,ms) (r,e,t,m,i)) ==> 512 ?v. 513 (X86_NEXT (X86_ICACHE_UPDATE x (r,e,t,m,i)) = SOME v) /\ 514 ((X86_ICACHE_EXTRACT v = X86_ICACHE_EMPTY) \/ 515 (X86_ICACHE_EXTRACT (X86_ICACHE_UPDATE x (r,e,t,m,i)) = X86_ICACHE_EXTRACT v)) /\ 516 p (x86_2set' (rs,st,ei,ms) (X86_ICACHE_UPDATE x (r,e,t,m,i))) /\ 517 q (x86_2set' (rs,st,ei,ms) (X86_ICACHE_REVERT v (r,e,t,m,i))) /\ 518 (x86_2set'' (rs,st,ei,ms) (r,e,t,m,i) = 519 x86_2set'' (rs,st,ei,ms) (X86_ICACHE_REVERT v (r,e,t,m,i)))) ==> 520 SPEC X86_MODEL p {} q``, 521 REPEAT STRIP_TAC \\ MATCH_MP_TAC IMP_X86_SPEC_LEMMA 522 \\ REPEAT STRIP_TAC 523 \\ IMP_RES_TAC X86_ICACHE_THM2 524 \\ ASM_SIMP_TAC std_ss [] 525 \\ `?rs st ei ms. y = (rs,st,ei,ms)` by METIS_TAC [PAIR] 526 \\ `?r e t m i. t1 = (r,e,t,m,i)` by METIS_TAC [PAIR] 527 \\ FULL_SIMP_TAC std_ss [] 528 \\ Q.PAT_ASSUM `!rs.bb` (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`rs`,`st`,`ei`,`ms`,`z`,`r`,`e`,`t`,`m`,`i`]) 529 \\ ASM_SIMP_TAC std_ss [] 530 \\ Q.EXISTS_TAC `(X86_ICACHE_REVERT v (r,e,t,m,i))` 531 \\ FULL_SIMP_TAC std_ss [] 532 THEN1 (METIS_TAC [X86_ICACHE_REVERT_EMPTY]) 533 \\ MATCH_MP_TAC X86_ICACHE_X86_ICACHE_REVERT 534 \\ Q.EXISTS_TAC `(X86_ICACHE_UPDATE z (r,e,t,m,i))` \\ ASM_SIMP_TAC std_ss []); 535 536val IMP_X86_SPEC = save_thm("IMP_X86_SPEC", 537 (RW1 [STAR_COMM] o RW [X86_SPEC_CODE,GSYM xCODE_def] o 538 SPECL [``CODE_POOL X86_INSTR {(eip,c)} * p``, 539 ``CODE_POOL X86_INSTR {(eip,c)} * q``]) IMP_X86_SPEC_LEMMA2); 540 541val xS_HIDE = store_thm("xS_HIDE", 542 ``~xS = ~xS1 X_CF * ~xS1 X_PF * ~xS1 X_AF * ~xS1 X_ZF * ~xS1 X_SF * ~xS1 X_OF``, 543 SIMP_TAC std_ss [SEP_HIDE_def,xS_def,SEP_CLAUSES,FUN_EQ_THM] 544 \\ SIMP_TAC std_ss [SEP_EXISTS] \\ METIS_TAC [xS_def,PAIR]); 545 546 547(* ----------------------------------------------------------------------------- *) 548(* Byte-sized data memory *) 549(* ----------------------------------------------------------------------------- *) 550 551val xDATA_PERM_def = Define ` 552 xDATA_PERM exec = if exec then {Xread;Xwrite;Xexecute} else {Xread;Xwrite}`; 553 554val xBYTE_MEMORY_ANY_SET_def = Define ` 555 xBYTE_MEMORY_ANY_SET df f exec c = 556 { xMem a (SOME (f a, xDATA_PERM exec)) (c a) | a | a IN df }`; 557 558val xBYTE_MEMORY_ANY_C_def = Define ` 559 xBYTE_MEMORY_ANY_C exec df f c = SEP_EQ (xBYTE_MEMORY_ANY_SET df f exec c)`; 560 561val xBYTE_MEMORY_ANY_def = Define ` 562 xBYTE_MEMORY_ANY exec df f = 563 SEP_EXISTS c. SEP_EQ (xBYTE_MEMORY_ANY_SET df f exec c)`; 564 565val xBYTE_MEMORY_def = Define `xBYTE_MEMORY = xBYTE_MEMORY_ANY F`; 566val xBYTE_MEMORY_X_def = Define `xBYTE_MEMORY_X = xBYTE_MEMORY_ANY T`; 567 568val IN_xDATA_PERM = store_thm("IN_xDATA_PERM", 569 ``(Xread IN xDATA_PERM exec) /\ 570 (Xwrite IN xDATA_PERM exec) /\ 571 (Xexecute IN xDATA_PERM exec = exec)``, 572 Cases_on `exec` \\ SRW_TAC [] [xDATA_PERM_def,IN_INSERT,NOT_IN_EMPTY]); 573 574val IN_xBYTE_MEMORY_ANY_SET = prove( 575 ``a IN df ==> 576 (xBYTE_MEMORY_ANY_SET df g exec c = 577 (xMem a (SOME (g a, xDATA_PERM exec))) (c a) INSERT 578 xBYTE_MEMORY_ANY_SET (df DELETE a) g exec c)``, 579 SIMP_TAC std_ss [EXTENSION,IN_INSERT,xBYTE_MEMORY_ANY_SET_def,GSPECIFICATION] 580 \\ REWRITE_TAC [IN_DELETE] \\ METIS_TAC []); 581 582val DELETE_xBYTE_MEMORY_ANY_SET = prove( 583 ``xBYTE_MEMORY_ANY_SET (df DELETE a) ((a =+ w) g) exec ((a =+ b) c) = 584 xBYTE_MEMORY_ANY_SET (df DELETE a) g exec c``, 585 SIMP_TAC std_ss [EXTENSION,IN_INSERT,xBYTE_MEMORY_ANY_SET_def,GSPECIFICATION] 586 \\ REWRITE_TAC [IN_DELETE,APPLY_UPDATE_THM] \\ METIS_TAC []); 587 588val xBYTE_MEMORY_ANY_C_INSERT = prove( 589 ``a IN df ==> 590 (xBYTE_MEMORY_ANY_C e df ((a =+ w) g) ((a =+ b) c) = 591 xM1 a (SOME (w,xDATA_PERM e)) b * xBYTE_MEMORY_ANY_C e (df DELETE a) g c)``, 592 SIMP_TAC std_ss [xM1_def,xBYTE_MEMORY_ANY_C_def,FUN_EQ_THM,EQ_STAR] 593 \\ SIMP_TAC std_ss [SEP_EQ_def] \\ REPEAT STRIP_TAC 594 \\ IMP_RES_TAC (GEN_ALL IN_xBYTE_MEMORY_ANY_SET) 595 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,DIFF_INSERT,DIFF_EMPTY] 596 \\ REWRITE_TAC [DELETE_xBYTE_MEMORY_ANY_SET,APPLY_UPDATE_THM] 597 \\ sg `~(xMem a (SOME (w,xDATA_PERM e)) b IN xBYTE_MEMORY_ANY_SET (df DELETE a) g e c)` 598 \\ SIMP_TAC std_ss [xBYTE_MEMORY_ANY_SET_def,GSPECIFICATION,IN_DELETE,x86_el_11] 599 \\ FULL_SIMP_TAC std_ss [xBYTE_MEMORY_ANY_SET_def,EXTENSION,GSPECIFICATION,IN_DELETE,IN_INSERT] 600 \\ METIS_TAC []); 601 602val xBYTE_MEMORY_ANY_INSERT = store_thm("xBYTE_MEMORY_ANY_INSERT", 603 ``a IN df ==> 604 (xBYTE_MEMORY_ANY e df ((a =+ w) g) = 605 ~xM1 a (SOME (w,xDATA_PERM e)) * xBYTE_MEMORY_ANY e (df DELETE a) g)``, 606 SIMP_TAC std_ss [FUN_EQ_THM] 607 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THENL [ 608 FULL_SIMP_TAC std_ss [xBYTE_MEMORY_ANY_def,SEP_CLAUSES] 609 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,GSYM xBYTE_MEMORY_ANY_C_def] 610 \\ `(y = (a =+ y a) y)` by SIMP_TAC std_ss [APPLY_UPDATE_THM,FUN_EQ_THM] 611 \\ Q.PAT_ASSUM `xBYTE_MEMORY_ANY_C e df ((a =+ w) g) y x` MP_TAC 612 \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [th]) 613 \\ ASM_SIMP_TAC std_ss [xBYTE_MEMORY_ANY_C_INSERT] 614 \\ REPEAT STRIP_TAC 615 \\ SIMP_TAC std_ss [SEP_HIDE_def,SEP_CLAUSES] 616 \\ SIMP_TAC std_ss [SEP_EXISTS] \\ METIS_TAC [], 617 FULL_SIMP_TAC std_ss [xBYTE_MEMORY_ANY_def,SEP_CLAUSES] 618 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS,GSYM xBYTE_MEMORY_ANY_C_def] 619 \\ FULL_SIMP_TAC std_ss [SEP_HIDE_def,SEP_CLAUSES] 620 \\ FULL_SIMP_TAC std_ss [SEP_EXISTS] 621 \\ Q.EXISTS_TAC `(a =+ y') y` 622 \\ ASM_SIMP_TAC std_ss [xBYTE_MEMORY_ANY_C_INSERT]]); 623 624val xBYTE_MEMORY_ANY_INSERT_SET = 625 SIMP_RULE std_ss [IN_INSERT,DELETE_INSERT,APPLY_UPDATE_ID] 626 (Q.INST [`df`|->`a INSERT df`,`w`|->`g a`] xBYTE_MEMORY_ANY_INSERT); 627 628val xBYTE_MEMORY_ANY_INTRO = store_thm("xBYTE_MEMORY_ANY_INTRO", 629 ``SPEC m (~xM1 a (SOME (v,xDATA_PERM e)) * P) c 630 (~xM1 a (SOME (w,xDATA_PERM e)) * Q) ==> 631 a IN df ==> 632 SPEC m (xBYTE_MEMORY_ANY e df ((a =+ v) f) * P) c 633 (xBYTE_MEMORY_ANY e df ((a =+ w) f) * Q)``, 634 ONCE_REWRITE_TAC [STAR_COMM] 635 \\ SIMP_TAC std_ss [xBYTE_MEMORY_ANY_INSERT,STAR_ASSOC] 636 \\ METIS_TAC [SPEC_FRAME]); 637 638 639(* ----------------------------------------------------------------------------- *) 640(* Word-sized data memory *) 641(* ----------------------------------------------------------------------------- *) 642 643val xMEMORY_DOMAIN_def = Define ` 644 xMEMORY_DOMAIN df = BIGUNION { {b;b+1w;b+2w;b+3w} | ALIGNED b /\ b IN df }`; 645 646val xMEMORY_FUNC_def = Define ` 647 xMEMORY_FUNC (f:word32->word32) a = 648 let w = f (ADDR32 (ADDR30 a)) in 649 if a && 3w = 0w then (7 >< 0) (w) else 650 if a && 3w = 1w then (7 >< 0) (w >> 8) else 651 if a && 3w = 2w then (7 >< 0) (w >> 16) else 652 if a && 3w = 3w then (7 >< 0) (w >> 24) else 0w:word8`; 653 654val xMEMORY_def = Define ` 655 xMEMORY df f = xBYTE_MEMORY (xMEMORY_DOMAIN df) (xMEMORY_FUNC f)`; 656 657val xM_LEMMA = prove( 658 ``!w a f. ALIGNED a ==> (xM a w = xMEMORY {a} ((a =+ w) f))``, 659 ONCE_REWRITE_TAC [EQ_SYM_EQ] 660 \\ SIMP_TAC std_ss [xM_def,xMEMORY_def,xBYTE_MEMORY_def] 661 \\ REPEAT STRIP_TAC 662 \\ `xMEMORY_DOMAIN {a} = {a;a+1w;a+2w;a+3w}` by 663 (SIMP_TAC std_ss [xMEMORY_DOMAIN_def,IN_INSERT,NOT_IN_EMPTY] 664 \\ `{{b; b + 1w; b + 2w; b + 3w} | ALIGNED b /\ (b = a)} = 665 {{a; a + 1w; a + 2w; a + 3w}}` by 666 (SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,IN_BIGUNION,IN_INSERT,NOT_IN_EMPTY] 667 \\ METIS_TAC []) 668 \\ ASM_SIMP_TAC std_ss [BIGUNION_INSERT,BIGUNION_EMPTY,UNION_EMPTY]) 669 \\ ASM_SIMP_TAC std_ss [] 670 \\ SIMP_TAC (std_ss++SIZES_ss) [xBYTE_MEMORY_ANY_INSERT_SET,DELETE_INSERT, 671 WORD_EQ_ADD_CANCEL,n2w_11,EMPTY_DELETE,STAR_ASSOC,xDATA_PERM_def] 672 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [xMEMORY_FUNC_def,LET_DEF,ALIGNED_add_3_and_3, 673 ALIGNED_add_2_and_3,ALIGNED_add_1_and_3,n2w_11,APPLY_UPDATE_THM] 674 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [ALIGNED_INTRO] 675 \\ IMP_RES_TAC (RW [ALIGNED_INTRO] EXISTS_ADDR30) 676 \\ FULL_SIMP_TAC std_ss [ADDR30_ADDR32] 677 \\ sg `!f. xBYTE_MEMORY_ANY F {} (xMEMORY_FUNC f) = emp` 678 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES,WORD_ADD_0] 679 \\ SIMP_TAC std_ss [xBYTE_MEMORY_ANY_def,SEP_EXISTS,SEP_EQ_def] 680 \\ SIMP_TAC std_ss [xBYTE_MEMORY_ANY_SET_def,NOT_IN_EMPTY,EXTENSION,GSPECIFICATION,emp_def]); 681 682val xM_THM = store_thm("xM_THM", 683 ``!a w f. ALIGNED a ==> (xMEMORY {a} ((a =+ w) f) = xM a w) /\ 684 (xMEMORY {a} (\x. w) = xM a w)``, 685 SIMP_TAC std_ss [GSYM xM_LEMMA,GSYM (RW [APPLY_UPDATE_ID] 686 (Q.SPECL [`(f:word32->word32) a`,`a`,`f`] xM_LEMMA))]); 687 688val xBYTE_MEMORY_ANY_SET_EQ = prove( 689 ``xBYTE_MEMORY_ANY_SET df f exec c = 690 {xMem d (SOME (f d,xDATA_PERM exec)) (c d) | d IN df}``, 691 METIS_TAC [xBYTE_MEMORY_ANY_SET_def]); 692 693val xMEMORY_INSERT = prove( 694 ``a IN df /\ ALIGNED a ==> 695 (xMEMORY df ((a =+ w) f) = xM a w * xMEMORY (df DELETE a) f)``, 696 REPEAT STRIP_TAC 697 \\ ASM_SIMP_TAC std_ss [xMEMORY_def,xBYTE_MEMORY_def,xM_def,GSYM STAR_ASSOC] 698 \\ `xMEMORY_DOMAIN df = a INSERT (a+1w) INSERT (a+2w) INSERT 699 (a+3w) INSERT xMEMORY_DOMAIN (df DELETE a)` by 700 (FULL_SIMP_TAC std_ss [xMEMORY_DOMAIN_def] 701 \\ `{{b; b + 1w; b + 2w; b + 3w} | ALIGNED b /\ b IN df} = 702 {a; a + 1w; a + 2w; a + 3w} INSERT 703 {{b; b + 1w; b + 2w; b + 3w} | ALIGNED b /\ b IN df DELETE a}` by 704 (SIMP_TAC std_ss [EXTENSION,IN_INSERT, 705 IN_BIGUNION,GSPECIFICATION,NOT_IN_EMPTY,IN_DELETE] 706 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 707 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [] 708 \\ METIS_TAC []) 709 \\ ASM_SIMP_TAC std_ss [BIGUNION_INSERT,INSERT_UNION_EQ,UNION_EMPTY]) 710 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [xBYTE_MEMORY_ANY_INSERT_SET,DELETE_INSERT, 711 WORD_EQ_ADD_CANCEL,n2w_11] 712 \\ SIMP_TAC std_ss [xMEMORY_FUNC_def,LET_DEF] 713 \\ IMP_RES_TAC (GSYM (RW [ALIGNED_INTRO] ADDR32_ADDR30)) 714 \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [th]) 715 \\ SIMP_TAC std_ss [ADDR30_ADDR32] 716 \\ IMP_RES_TAC ((RW [ALIGNED_INTRO] ADDR32_ADDR30)) 717 \\ ASM_SIMP_TAC std_ss [APPLY_UPDATE_THM] 718 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [ALIGNED_add_1_and_3,ALIGNED_add_2_and_3, 719 ALIGNED_add_3_and_3,n2w_11] 720 \\ ASM_SIMP_TAC std_ss [ALIGNED_INTRO,xDATA_PERM_def] 721 \\ SIMP_TAC std_ss [STAR_ASSOC] 722 \\ MATCH_MP_TAC (METIS_PROVE [] ``(q1 = q2) ==> ((p * q1) = (STAR p q2))``) 723 \\ `~(a IN xMEMORY_DOMAIN (df DELETE a)) /\ 724 ~(a+1w IN xMEMORY_DOMAIN (df DELETE a)) /\ 725 ~(a+2w IN xMEMORY_DOMAIN (df DELETE a)) /\ 726 ~(a+3w IN xMEMORY_DOMAIN (df DELETE a))` by 727 (SIMP_TAC std_ss [xMEMORY_DOMAIN_def,GSPECIFICATION,IN_BIGUNION, 728 IN_DELETE,EXTENSION,IN_INSERT,NOT_IN_EMPTY] 729 \\ IMP_RES_TAC NOT_ALIGNED 730 \\ SIMP_TAC std_ss [METIS_PROVE [] ``~b \/ c = b ==> c``] 731 \\ REPEAT STRIP_TAC \\ CCONTR_TAC 732 \\ FULL_SIMP_TAC std_ss [WORD_ADD_EQ_SUB,word_arith_lemma4] 733 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,ALIGNED_CLAUSES,WORD_EQ_ADD_CANCEL] 734 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,ALIGNED_CLAUSES, 735 word_arith_lemma3,WORD_ADD_0]) 736 \\ FULL_SIMP_TAC std_ss [DELETE_NON_ELEMENT] 737 \\ FULL_SIMP_TAC std_ss [GSYM DELETE_NON_ELEMENT] 738 \\ FULL_SIMP_TAC std_ss [xBYTE_MEMORY_ANY_def] 739 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (f x = f y)``) 740 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] 741 \\ REPEAT STRIP_TAC 742 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (f x z = f y z)``) 743 \\ SIMP_TAC std_ss [xBYTE_MEMORY_ANY_SET_EQ,EXTENSION,GSPECIFICATION] 744 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 745 \\ ASM_SIMP_TAC std_ss [x86_el_11] 746 \\ SIMP_TAC std_ss [xMEMORY_FUNC_def,LET_DEF] 747 \\ `?q. (d = ADDR32 q + 0w) \/ (d = ADDR32 q + 1w) \/ 748 (d = ADDR32 q + 2w) \/ (d = ADDR32 q + 3w)` by METIS_TAC [EXISTS_ADDR32] 749 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_ADD_0,RW [ALIGNED_def] ALIGNED_ADDR32, 750 ALIGNED_add_1_and_3,ALIGNED_add_2_and_3,ALIGNED_add_3_and_3, 751 ALIGNED_ADDR32,n2w_11] 752 \\ SIMP_TAC std_ss [ADDR30_ADDR32,APPLY_UPDATE_THM] 753 \\ METIS_TAC []); 754 755val xMEMORY_INTRO = store_thm("xMEMORY_INTRO", 756 ``SPEC m (xM a v * P) c (xM a w * Q) ==> 757 ALIGNED a /\ a IN df ==> 758 SPEC m (xMEMORY df ((a =+ v) f) * P) c (xMEMORY df ((a =+ w) f) * Q)``, 759 ONCE_REWRITE_TAC [STAR_COMM] 760 \\ SIMP_TAC std_ss [xMEMORY_INSERT,STAR_ASSOC] 761 \\ METIS_TAC [SPEC_FRAME]); 762 763 764(* ----------------------------------------------------------------------------- *) 765(* Conversions between code and data *) 766(* ----------------------------------------------------------------------------- *) 767 768val xCODE_SET_def = Define `xCODE_SET df f = { (a,[f a],T) | a IN df }`; 769 770val xCODE_IMP_BYTE_MEMORY = store_thm("xCODE_IMP_BYTE_MEMORY", 771 ``!df f. SEP_IMP (xCODE (xCODE_SET df f)) (xBYTE_MEMORY_X df f)``, 772 SIMP_TAC std_ss [SEP_IMP_def,xCODE_def,CODE_POOL_def,SEP_EQ_def, 773 xBYTE_MEMORY_X_def,xBYTE_MEMORY_ANY_def,SEP_EXISTS,xBYTE_MEMORY_ANY_SET_def] 774 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `\x.T` 775 \\ SIMP_TAC std_ss [xDATA_PERM_def,xCODE_SET_def,EXTENSION] 776 \\ SIMP_TAC std_ss [GSPECIFICATION,EXTENSION,IN_BIGUNION] 777 \\ ONCE_REWRITE_TAC [IN_IMAGE] 778 \\ `X86_INSTR_PERM T = {Xread; Xwrite; Xexecute}` by 779 (SIMP_TAC std_ss [X86_INSTR_PERM_def,EXTENSION,IN_INSERT, 780 NOT_IN_EMPTY,IN_UNION] \\ METIS_TAC []) 781 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 782 (NTAC 2 (FULL_SIMP_TAC std_ss [X86_INSTR_def,GSPECIFICATION,IN_INSERT,NOT_IN_EMPTY]) 783 \\ Q.EXISTS_TAC `a` \\ FULL_SIMP_TAC std_ss []) 784 \\ Q.EXISTS_TAC `X86_INSTR (a,[f a],T)` 785 \\ ASM_SIMP_TAC std_ss [X86_INSTR_def,IN_INSERT,X86_INSTR_PERM_def] 786 \\ Q.EXISTS_TAC `(a,[f a],T)` 787 \\ ASM_SIMP_TAC std_ss [X86_INSTR_def,IN_INSERT,X86_INSTR_PERM_def] 788 \\ ASM_SIMP_TAC std_ss [GSPECIFICATION]); 789 790val x86_2set_ICACHE_EMPTY = prove( 791 ``(x86_2set' (rs,st,ei,ms) (r,e2,t,m,(\a. if a IN ms then NONE else i a)) = 792 x86_2set' (rs,st,ei,ms) (r,e2,t,m,X86_ICACHE_EMPTY)) /\ 793 (x86_2set'' (rs,st,ei,ms) (r,e2,t,m,(\a. if a IN ms then NONE else i a)) = 794 x86_2set'' (rs,st,ei,ms) (r,e2,t,m,i))``, 795 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [EXTENSION] \\ Cases 796 \\ SIMP_TAC std_ss [IN_x86_2set,XREAD_REG_def,XREAD_EFLAG_def, 797 XREAD_EIP_def,X86_GET_MEMORY_def,X86_ACCURATE_def,X86_ICACHE_EMPTY_def] 798 \\ SRW_TAC [][]); 799 800val IMP_X86_SPEC_LEMMA3 = prove( 801 ``!p q. 802 (!rs st ei ms x r e t m i. 803 p (x86_2set' (rs,st,ei,ms) (r,e,t,m,i)) ==> 804 ?e2. 805 (X86_NEXT (r,e,t,m,icache x m i) = SOME (r,e2,t,m,X86_ICACHE_EMPTY)) /\ 806 p (x86_2set' (rs,st,ei,ms) (r,e,t,m,icache x m i)) /\ 807 q (x86_2set' (rs,st,ei,ms) (r,e2,t,m,X86_ICACHE_EMPTY)) /\ 808 (x86_2set'' (rs,st,ei,ms) (r,e,t,m,i) = 809 x86_2set'' (rs,st,ei,ms) (r,e2,t,m,i))) ==> 810 SPEC X86_MODEL p {} q``, 811 REPEAT STRIP_TAC \\ MATCH_MP_TAC IMP_X86_SPEC_LEMMA 812 \\ REPEAT STRIP_TAC 813 \\ IMP_RES_TAC X86_ICACHE_THM2 814 \\ ASM_SIMP_TAC std_ss [] 815 \\ `?rs st ei ms. y = (rs,st,ei,ms)` by METIS_TAC [PAIR] 816 \\ `?r e t m i. t1 = (r,e,t,m,i)` by METIS_TAC [PAIR] 817 \\ FULL_SIMP_TAC std_ss [] 818 \\ Q.PAT_ASSUM `!rs.bb` (STRIP_ASSUME_TAC o UNDISCH o Q.SPECL [`rs`,`st`,`ei`,`ms`,`z`,`r`,`e`,`t`,`m`,`i`]) 819 \\ ASM_SIMP_TAC std_ss [X86_ICACHE_UPDATE_def] 820 \\ Q.EXISTS_TAC `(r,e2,t,m,(\addr. if addr IN ms then NONE else i addr))` 821 \\ ASM_SIMP_TAC std_ss [x86_2set_ICACHE_EMPTY] 822 \\ SIMP_TAC std_ss [X86_ICACHE_EMPTY_def,X86_ICACHE_def,FUN_EQ_THM] 823 \\ Q.EXISTS_TAC `{}` \\ Q.EXISTS_TAC `UNIV` \\ SRW_TAC [] []); 824 825val IMP_X86_SPEC2 = save_thm("IMP_X86_SPEC2", 826 (RW1 [STAR_COMM] o RW [X86_SPEC_CODE,GSYM xCODE_def] o 827 SPECL [``CODE_POOL X86_INSTR c * p``, 828 ``CODE_POOL X86_INSTR c * q``]) IMP_X86_SPEC_LEMMA3); 829 830 831open x86_astTheory; 832open x86_coretypesTheory; 833open x86_Lib x86_encodeLib; 834 835val jmp_esi = let 836 val th = x86_step (x86_encode "jmp esi") 837 val th = Q.INST [`s`|->`X86_ICACHE_UPDATE x (r,e,t,m,i)`] th 838 val th = RW [XREAD_CLAUSES] th 839 val th = RW [XREAD_REG_def,X86_ICACHE_UPDATE_def,XWRITE_EIP_def,XCLEAR_ICACHE_def] th 840 in th end 841 842val WORD_FINITE = store_thm("WORD_FINITE", 843 ``!s:'a word set. FINITE s``, 844 STRIP_TAC 845 \\ MATCH_MP_TAC ((ONCE_REWRITE_RULE [CONJ_COMM] o 846 REWRITE_RULE [AND_IMP_INTRO] o GEN_ALL o DISCH_ALL o SPEC_ALL o 847 UNDISCH_ALL o SPEC_ALL) SUBSET_FINITE) 848 \\ Q.EXISTS_TAC `UNIV` 849 \\ ASM_SIMP_TAC std_ss [SUBSET_UNIV] 850 \\ MATCH_MP_TAC ((ONCE_REWRITE_RULE [CONJ_COMM] o 851 REWRITE_RULE [AND_IMP_INTRO] o GEN_ALL o DISCH_ALL o SPEC_ALL o 852 UNDISCH_ALL o SPEC_ALL) SUBSET_FINITE) 853 \\ Q.EXISTS_TAC `{ n2w n | n < dimword(:'a) }` 854 \\ STRIP_TAC THEN1 855 (SIMP_TAC std_ss [SUBSET_DEF,IN_UNIV,GSPECIFICATION] 856 \\ Cases_word \\ Q.EXISTS_TAC `n` \\ ASM_SIMP_TAC std_ss []) 857 \\ Q.SPEC_TAC (`dimword (:'a)`,`k`) 858 \\ Induct \\ sg `{n2w n | n < 0} = {}` 859 \\ ASM_SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,NOT_IN_EMPTY,FINITE_EMPTY] 860 \\ sg `{n2w n | n < SUC k} = n2w k INSERT {n2w n | n < k}` 861 \\ ASM_SIMP_TAC std_ss [FINITE_INSERT] 862 \\ ASM_SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,NOT_IN_EMPTY,IN_INSERT] 863 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 864 \\ FULL_SIMP_TAC std_ss [DECIDE ``n < SUC k = n < k \/ (n = k)``] 865 \\ METIS_TAC []); 866 867val WORD_SET_INDUCT = save_thm("WORD_SET_INDUCT", 868 REWRITE_RULE [WORD_FINITE] 869 (INST_TYPE [``:'a``|->``:'a word``] FINITE_INDUCT)); 870 871val xBYTE_MEMORY_X_x86_2set = prove( 872 ``!df ms. 873 (xBYTE_MEMORY_X df f * p) (x86_2set' (rs,st,ei,ms) (r,e,t,m,i)) = 874 p (x86_2set' (rs,st,ei,ms DIFF df) (r,e,t,m,i)) /\ df SUBSET ms /\ 875 !a. a IN df ==> (m a = SOME (f a, {Xread;Xwrite;Xexecute}))``, 876 HO_MATCH_MP_TAC WORD_SET_INDUCT \\ REPEAT STRIP_TAC THENL [ 877 SIMP_TAC std_ss [xBYTE_MEMORY_X_def,xBYTE_MEMORY_ANY_def,SEP_CLAUSES] 878 \\ SIMP_TAC std_ss [NOT_IN_EMPTY] 879 \\ `!c. xBYTE_MEMORY_ANY_SET {} f T c = {}` by 880 SIMP_TAC std_ss [xBYTE_MEMORY_ANY_SET_def,NOT_IN_EMPTY,EXTENSION,GSPECIFICATION] 881 \\ ASM_SIMP_TAC std_ss [GSYM emp_def,SEP_EQ_def,SEP_CLAUSES] 882 \\ SIMP_TAC std_ss [DIFF_EMPTY,EMPTY_SUBSET], 883 FULL_SIMP_TAC std_ss [xBYTE_MEMORY_X_def] 884 \\ SIMP_TAC std_ss [DIFF_INSERT,xBYTE_MEMORY_ANY_INSERT_SET] 885 \\ FULL_SIMP_TAC std_ss [GSYM STAR_ASSOC,STAR_x86_2set,DELETE_NON_ELEMENT] 886 \\ FULL_SIMP_TAC std_ss [IN_INSERT,GSYM DELETE_NON_ELEMENT] 887 \\ ASM_SIMP_TAC std_ss [xDATA_PERM_def,INSERT_SUBSET,SUBSET_DELETE] 888 \\ METIS_TAC []]); 889 890val xCODE_SET_INSERT = store_thm("xCODE_SET_INSERT", 891 ``~(e IN df) ==> 892 (xCODE (xCODE_SET (e INSERT df) f) = 893 xM1 e (SOME (f e, {Xread; Xwrite; Xexecute})) T * xCODE (xCODE_SET df f))``, 894 SIMP_TAC std_ss [xCODE_def,xCODE_SET_def,xM1_def,EQ_STAR,FUN_EQ_THM] \\ STRIP_TAC 895 \\ SIMP_TAC std_ss [CODE_POOL_def,INSERT_SUBSET,EMPTY_SUBSET] 896 \\ `~((e,[f e],T) IN {(a,[f a],T) | a IN df}) /\ 897 ({(a,[f a],T) | a IN e INSERT df} = (e,[f e],T) INSERT {(a,[f a],T) | a IN df})` by 898 (SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,IN_INSERT] \\ METIS_TAC []) 899 \\ ASM_SIMP_TAC std_ss [IMAGE_INSERT,BIGUNION_INSERT] 900 \\ SIMP_TAC std_ss [X86_INSTR_def,INSERT_UNION_EQ,UNION_EMPTY] 901 \\ `X86_INSTR_PERM T = {Xread; Xwrite; Xexecute}` by 902 (SIMP_TAC std_ss [X86_INSTR_PERM_def,EXTENSION,IN_INSERT, 903 IN_UNION,NOT_IN_EMPTY] \\ REPEAT STRIP_TAC \\ EQ_TAC 904 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss []) 905 \\ ASM_SIMP_TAC std_ss [DIFF_INSERT,DIFF_EMPTY] 906 \\ Q.ABBREV_TAC `a1 = xMem e (SOME (f e,{Xread; Xwrite; Xexecute})) T` 907 \\ Q.ABBREV_TAC `a2 = BIGUNION (IMAGE X86_INSTR {(a,[f a],T) | a IN df})` 908 \\ `~(a1 IN a2)` suffices_by 909 (STRIP_TAC THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE] \\ METIS_TAC []) 910 \\ Q.UNABBREV_TAC `a1` \\ Q.UNABBREV_TAC `a2` 911 \\ ASM_SIMP_TAC std_ss [IN_IMAGE,IN_BIGUNION] 912 \\ SIMP_TAC std_ss [METIS_PROVE [] ``e \/ b = ~e ==> b``,GSPECIFICATION] 913 \\ REPEAT STRIP_TAC 914 \\ FULL_SIMP_TAC std_ss [X86_INSTR_def,IN_INSERT,NOT_IN_EMPTY,x86_el_11]); 915 916val xCODE_SET_x86_2set = prove( 917 ``!df ms. 918 (xCODE (xCODE_SET df f) * p) (x86_2set' (rs,st,ei,ms) (r,e,t,m,i)) = 919 p (x86_2set' (rs,st,ei,ms DIFF df) (r,e,t,m,i)) /\ df SUBSET ms /\ 920 !a. a IN df ==> (m a = SOME (f a, {Xread;Xwrite;Xexecute})) /\ 921 X86_ACCURATE a (r,e,t,m,i)``, 922 HO_MATCH_MP_TAC WORD_SET_INDUCT \\ REPEAT STRIP_TAC THENL [ 923 SIMP_TAC std_ss [xCODE_SET_def,xCODE_def,SEP_CLAUSES] 924 \\ `{(a,[f a],T) | a IN {}} = {}` by 925 SIMP_TAC std_ss [NOT_IN_EMPTY,EXTENSION,GSPECIFICATION] 926 \\ ASM_SIMP_TAC std_ss [CODE_POOL_def,IMAGE_EMPTY,BIGUNION_EMPTY] 927 \\ SIMP_TAC std_ss [GSYM emp_def,SEP_CLAUSES,DIFF_EMPTY,EMPTY_SUBSET] 928 \\ SIMP_TAC std_ss [NOT_IN_EMPTY], 929 ASM_SIMP_TAC std_ss [GSYM STAR_ASSOC,xCODE_SET_INSERT] 930 \\ FULL_SIMP_TAC std_ss [GSYM STAR_ASSOC,STAR_x86_2set,DELETE_NON_ELEMENT] 931 \\ FULL_SIMP_TAC std_ss [IN_INSERT,GSYM DELETE_NON_ELEMENT] 932 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,SUBSET_DELETE,DIFF_INSERT] 933 \\ METIS_TAC []]); 934 935val xCODE_INTRO = store_thm("xCODE_INTRO", 936 ``SPEC X86_MODEL 937 (xR ESI esi * xPC eip * xBYTE_MEMORY_X df f) 938 {(eip,[0xFFw;0xE6w],T)} 939 (xR ESI esi * xPC esi * xCODE (xCODE_SET df f))``, 940 MATCH_MP_TAC IMP_X86_SPEC2 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `r ESI` 941 \\ STRIP_TAC THENL [MATCH_MP_TAC jmp_esi,ALL_TAC] 942 \\ REPEAT (POP_ASSUM MP_TAC) 943 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC, 944 STAR_x86_2set, IN_DELETE, APPLY_UPDATE_THM, Xreg_distinct, 945 GSYM ALIGNED_def, wordsTheory.n2w_11, Xeflags_distinct, 946 Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, INSERT_SUBSET, 947 EMPTY_SUBSET, SEP_CLAUSES,X86_ICACHE_UPDATE_def,XREAD_EIP_def, 948 X86_ICACHE_REVERT_def,xM_def,WORD_EQ_ADD_CANCEL,x86_address_lemma, 949 xCODE_SET_x86_2set,xBYTE_MEMORY_X_x86_2set] 950 \\ ONCE_REWRITE_TAC [CODE_POOL_x86_2set] 951 \\ REWRITE_TAC [listTheory.LENGTH,address_list_def] 952 \\ SIMP_TAC std_ss [arithmeticTheory.ADD1,X86_ICACHE_EXTRACT_def] 953 \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC, 954 STAR_x86_2set, IN_DELETE, APPLY_UPDATE_THM, Xreg_distinct, 955 GSYM ALIGNED_def, wordsTheory.n2w_11, Xeflags_distinct, 956 Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, INSERT_SUBSET, 957 EMPTY_SUBSET,x86_pool_def,X86_ACCURATE_CLAUSES, 958 xCODE_SET_x86_2set,xBYTE_MEMORY_X_x86_2set] 959 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN1 960 (REPEAT STRIP_TAC \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 961 \\ MATCH_MP_TAC XREAD_INSTR_IMP \\ Q.EXISTS_TAC `T` 962 \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC []) 963 \\ SIMP_TAC std_ss [UPDATE_x86_2set'',IN_INSERT] 964 \\ STRIP_TAC \\ IMP_RES_TAC X86_ACCURATE_IMP 965 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def] 966 \\ SIMP_TAC std_ss [X86_ACCURATE_def,X86_ICACHE_EMPTY_def]); 967 968val SPLIT_CODE_SEQ = prove( 969 ``SPEC X86_MODEL p ((a,x::xs,T) INSERT s) q = 970 SPEC X86_MODEL p ((a+1w,xs,T) INSERT (a,[x],T) INSERT s) q``, 971 SIMP_TAC std_ss [progTheory.SPEC_def,X86_MODEL_def] 972 \\ sg `CODE_POOL X86_INSTR ((a + 0x1w,xs,T) INSERT (a,[x],T) INSERT s) = 973 CODE_POOL X86_INSTR ((a,x::xs,T) INSERT s)` 974 \\ ASM_SIMP_TAC std_ss [] 975 \\ SIMP_TAC std_ss [progTheory.CODE_POOL_def] 976 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> ((\s. s = x) = (\s. s = y))``) 977 \\ SIMP_TAC std_ss [IMAGE_INSERT,BIGUNION_INSERT] 978 \\ SIMP_TAC std_ss [EXTENSION,IN_BIGUNION] 979 \\ SIMP_TAC std_ss [X86_INSTR_def] 980 \\ SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] 981 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 982 \\ ASM_SIMP_TAC std_ss []); 983 984val X86_SPEC_EXLPODE_CODE_LEMMA = prove( 985 ``!s. SPEC X86_MODEL p ((a,xs,T) INSERT s) q = 986 SPEC X86_MODEL p ({ (a + n2w n, [EL n xs], T) | n| n < LENGTH xs } UNION s) q``, 987 Q.SPEC_TAC (`a`,`a`) \\ Q.SPEC_TAC (`xs`,`xs`) \\ REVERSE Induct THEN1 988 (ASM_SIMP_TAC std_ss [SPLIT_CODE_SEQ] \\ REPEAT STRIP_TAC 989 \\ sg `{(a + n2w n,[EL n (h::xs)],T) | n | n < LENGTH (h::xs)} = 990 {(a + 0x1w + n2w n,[EL n xs],T) | n | n < LENGTH xs} UNION {(a,[h],T)}` 991 \\ ASM_SIMP_TAC std_ss [INSERT_UNION_EQ,UNION_EMPTY,GSYM UNION_ASSOC] 992 \\ SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] 993 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC THENL [ 994 Cases_on `n` \\ ASM_SIMP_TAC std_ss [EL,HD,WORD_ADD_0,TL,CONS_11] 995 \\ FULL_SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC,word_add_n2w,LENGTH] 996 \\ SIMP_TAC std_ss [DECIDE ``1+n = SUC n``] \\ METIS_TAC [], 997 Q.EXISTS_TAC `SUC n` 998 \\ SIMP_TAC std_ss [EL,GSYM word_add_n2w,RW1 [ADD_COMM] ADD1] 999 \\ ASM_SIMP_TAC std_ss [TL,WORD_ADD_ASSOC,LENGTH] \\ DECIDE_TAC, 1000 Q.EXISTS_TAC `0` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0,EL,LENGTH,HD]]) 1001 \\ REPEAT STRIP_TAC 1002 \\ `{(a + n2w n,[EL n ([]:word8 list)],T) | n| n < LENGTH ([]:word8 list)} = {}` by 1003 ASM_SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,NOT_IN_EMPTY,LENGTH] 1004 \\ ASM_SIMP_TAC std_ss [UNION_EMPTY] 1005 \\ SIMP_TAC std_ss [progTheory.SPEC_def,X86_MODEL_def] 1006 \\ sg `CODE_POOL X86_INSTR ((a,[],T) INSERT s) = 1007 CODE_POOL X86_INSTR (s)` 1008 \\ ASM_SIMP_TAC std_ss [] 1009 \\ SIMP_TAC std_ss [progTheory.CODE_POOL_def] 1010 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> ((\s. s = x) = (\s. s = y))``) 1011 \\ POP_ASSUM (K ALL_TAC) 1012 \\ ASM_SIMP_TAC std_ss [UNION_EMPTY,IMAGE_INSERT,X86_INSTR_def,BIGUNION_INSERT]); 1013 1014val X86_SPEC_EXLPODE_CODE = save_thm("X86_SPEC_EXLPODE_CODE", 1015 RW [UNION_EMPTY] (Q.SPEC `{}` X86_SPEC_EXLPODE_CODE_LEMMA)); 1016 1017(* Stack --- sp points at top of stack, stack grows towards smaller addresses *) 1018 1019val xSTACK_def = Define ` 1020 xSTACK bp xs = xR EBP bp * xR ESP (bp - n2w (4 * LENGTH xs)) * 1021 SEP_ARRAY xM (-4w) bp xs * cond (ALIGNED bp)`; 1022 1023val STAR6 = prove( 1024 ``p1 * p2 * p3 * p4 * p5 * p6 = (p1 * p2 * p5) * (STAR p3 p4 * p6)``, 1025 SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM]); 1026 1027val xSTACK_INTRO_EBX = store_thm("xSTACK_INTRO_EBX", 1028 ``(ALIGNED ebp ==> 1029 SPEC X86_MODEL (q1 * xR EBP ebp * xM (ebp - n2w n) x) c 1030 (q2 * xR EBP ebp * xM (ebp - n2w n) y)) ==> 1031 !xs ys. 1032 (4 * LENGTH xs = n) ==> 1033 SPEC X86_MODEL (q1 * xSTACK ebp (xs ++ [x] ++ ys)) 1034 c (q2 * xSTACK ebp (xs ++ [y] ++ ys))``, 1035 SIMP_TAC std_ss [xSTACK_def,SEP_ARRAY_APPEND,GSYM WORD_NEG_RMUL,STAR_ASSOC, 1036 RW1 [MULT_COMM] word_mul_n2w,GSYM word_sub_def,SEP_ARRAY_def,SEP_CLAUSES, 1037 LENGTH,LENGTH_APPEND,SPEC_MOVE_COND] \\ ONCE_REWRITE_TAC [STAR6] 1038 \\ METIS_TAC [SPEC_FRAME]); 1039 1040val _ = export_theory(); 1041