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