1192886Sedwin 2203019Sedwinopen HolKernel boolLib bossLib Parse; 3192886Sedwinopen pred_setTheory res_quanTheory wordsTheory wordsLib bitTheory arithmeticTheory; 4192886Sedwinopen listTheory pairTheory combinTheory addressTheory; 558787Sru 619874Swollmanopen set_sepTheory progTheory x86_Theory x86_seq_monadTheory x86_icacheTheory; 719874Swollman 8149514Swollmanval _ = new_theory "prog_x86"; 919874Swollman 1019874Swollman 1137998Sdesinfix \\ 1219874Swollmanval op \\ = op THEN; 1319874Swollman 1419874Swollmanval RW = REWRITE_RULE; 1519874Swollmanval RW1 = ONCE_REWRITE_RULE; 1619874Swollman 1719874Swollman 1886222Swollman(* ----------------------------------------------------------------------------- *) 1919874Swollman(* The x86 set *) 2019874Swollman(* ----------------------------------------------------------------------------- *) 2119874Swollman 2219874Swollmanval _ = Hol_datatype ` 2319874Swollman x86_el = xReg of Xreg => word32 2419874Swollman | xStatus of Xeflags => bool option 2519874Swollman | xEIP of word32 2619874Swollman | xMem of word32 => ((word8 # x86_permission set) option) => bool `; 2719874Swollman 2819874Swollmanval x86_el_11 = DB.fetch "-" "x86_el_11"; 2919874Swollmanval x86_el_distinct = DB.fetch "-" "x86_el_distinct"; 3019874Swollman 3119874Swollmanval _ = Parse.type_abbrev("x86_set",``:x86_el set``); 3219874Swollman 3319874Swollman 3419874Swollman(* ----------------------------------------------------------------------------- *) 3519874Swollman(* Converting from x86-state tuple to x86_set *) 3619874Swollman(* ----------------------------------------------------------------------------- *) 3719874Swollman 3819874Swollmanval x86_2set'_def = Define ` 39114173Swollman x86_2set' (rs,st,ep,ms) (r,e,s,m,i) = 4037998Sdes IMAGE (\a. xReg a (r a)) rs UNION 4137998Sdes IMAGE (\a. xStatus a (s a)) st UNION 4243014Swollman (if ep then {xEIP e} else {}) UNION 4319874Swollman IMAGE (\a. xMem a (m a) (X86_ACCURATE a (r,e,s,m,i))) ms`; 4475267Swollman 45171948Sedwinval x86_2set_def = Define `x86_2set s = x86_2set' (UNIV,UNIV,T,UNIV) s`; 4658787Sruval x86_2set''_def = Define `x86_2set'' x s = x86_2set s DIFF x86_2set' x s`; 47136638Swollman 48184406Sedwin(* theorems *) 49184406Sedwin 50136638Swollmanval x86_2set'_SUBSET_x86_2set = prove( 51163302Sru ``!y s. x86_2set' y s SUBSET x86_2set s``, 52149514Swollman STRIP_TAC \\ STRIP_TAC 53136638Swollman \\ `?rs st ep ms. y = (rs,st,ep,ms)` by METIS_TAC [PAIR] 54136638Swollman \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] 55136638Swollman \\ ASM_SIMP_TAC std_ss [] 56184406Sedwin \\ SIMP_TAC std_ss [SUBSET_DEF,x86_2set'_def,x86_2set_def,IN_IMAGE,IN_UNION,IN_UNIV] 57136638Swollman \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [NOT_IN_EMPTY]); 58136638Swollman 5919874Swollmanval SPLIT_x86_2set = prove( 6019874Swollman ``!x s. SPLIT (x86_2set s) (x86_2set' x s, x86_2set'' x s)``, 6119874Swollman REPEAT STRIP_TAC 62149514Swollman \\ ASM_SIMP_TAC std_ss [SPLIT_def,EXTENSION,IN_UNION,IN_DIFF,x86_2set''_def] 63149514Swollman \\ `x86_2set' x s SUBSET x86_2set s` by METIS_TAC [x86_2set'_SUBSET_x86_2set] 6419874Swollman \\ SIMP_TAC bool_ss [DISJOINT_DEF,EXTENSION,IN_INTER,NOT_IN_EMPTY,IN_DIFF] 6519874Swollman \\ METIS_TAC [SUBSET_DEF]); 6675267Swollman 6737998Sdesval PUSH_IN_INTO_IF = METIS_PROVE [] 6837998Sdes ``!g x y z. x IN (if g then y else z) = if g then x IN y else x IN z``; 6919874Swollman 7019874Swollmanval SUBSET_x86_2set = prove( 71169811Swollman ``!u s. u SUBSET x86_2set s = ?y. u = x86_2set' y s``, 72169811Swollman REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 73171948Sedwin \\ ASM_REWRITE_TAC [x86_2set'_SUBSET_x86_2set] 74136638Swollman \\ Q.EXISTS_TAC `({ a | a| ?x. xReg a x IN u },{ a | a| ?x. xStatus a x IN u }, 7519874Swollman (?x. xEIP x IN u),{ a | a| ?x y. xMem a x y IN u })` 7619874Swollman \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] 7719874Swollman \\ FULL_SIMP_TAC std_ss [x86_2set'_def,x86_2set_def,EXTENSION,SUBSET_DEF,IN_IMAGE, 7875267Swollman IN_UNION,GSPECIFICATION,IN_INSERT,NOT_IN_EMPTY,IN_UNIV] 7919874Swollman \\ STRIP_TAC \\ ASM_REWRITE_TAC [] \\ EQ_TAC \\ REPEAT STRIP_TAC 8019874Swollman \\ RES_TAC \\ FULL_SIMP_TAC std_ss [x86_el_11,x86_el_distinct] 8119874Swollman \\ FULL_SIMP_TAC std_ss [PUSH_IN_INTO_IF,NOT_IN_EMPTY,IN_INSERT] 8219874Swollman \\ RES_TAC \\ FULL_SIMP_TAC std_ss [x86_el_11,x86_el_distinct] 8319874Swollman \\ METIS_TAC []); 8419874Swollman 85174242Sedwinval SPLIT_x86_2set_EXISTS = prove( 8619874Swollman ``!s u v. SPLIT (x86_2set s) (u,v) = ?y. (u = x86_2set' y s) /\ (v = x86_2set'' y s)``, 8719874Swollman REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_REWRITE_TAC [SPLIT_x86_2set] 8819874Swollman \\ FULL_SIMP_TAC bool_ss [SPLIT_def,x86_2set'_def,x86_2set''_def] 8975267Swollman \\ `u SUBSET (x86_2set s)` by 9043543Swollman (FULL_SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_UNION] \\ METIS_TAC []) 91121098Swollman \\ FULL_SIMP_TAC std_ss [SUBSET_x86_2set] \\ Q.EXISTS_TAC `y` \\ REWRITE_TAC [] 9275267Swollman \\ FULL_SIMP_TAC std_ss [EXTENSION,IN_DIFF,IN_UNION,DISJOINT_DEF,NOT_IN_EMPTY,IN_INTER] 9343543Swollman \\ METIS_TAC []); 9443543Swollman 95121098Swollmanval X86_GET_MEMORY_def = Define `X86_GET_MEMORY (r,e,t,m,i) = m`; 96121098Swollman 97121098Swollmanval IN_x86_2set = prove(`` 98121098Swollman (!r x s. xReg r x IN (x86_2set s) = (x = XREAD_REG r s)) /\ 99181421Sedwin (!r x s. xReg r x IN (x86_2set' (rs,st,e,ms) s) = (x = XREAD_REG r s) /\ r IN rs) /\ 100181421Sedwin (!r x s. xReg r x IN (x86_2set'' (rs,st,e,ms) s) = (x = XREAD_REG r s) /\ ~(r IN rs)) /\ 10158787Sru (!a x s. xStatus a x IN (x86_2set s) = (x = XREAD_EFLAG a s)) /\ 10275267Swollman (!a x s. xStatus a x IN (x86_2set' (rs,st,e,ms) s) = (x = XREAD_EFLAG a s) /\ a IN st) /\ 10375267Swollman (!a x s. xStatus a x IN (x86_2set'' (rs,st,e,ms) s) = (x = XREAD_EFLAG a s) /\ ~(a IN st)) /\ 10475267Swollman (!x s. xEIP x IN (x86_2set s) = (x = XREAD_EIP s)) /\ 10519874Swollman (!x s. xEIP x IN (x86_2set' (rs,st,e,ms) s) = (x = XREAD_EIP s) /\ e) /\ 10667578Swollman (!x s. xEIP x IN (x86_2set'' (rs,st,e,ms) s) = (x = XREAD_EIP s) /\ ~e) /\ 107192886Sedwin (!p x y s. xMem p x y IN (x86_2set s) = (X86_GET_MEMORY s p = x) /\ (y = X86_ACCURATE p s)) /\ 10819874Swollman (!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) /\ 10919874Swollman (!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))``, 110163302Sru REPEAT STRIP_TAC 111163302Sru \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] \\ ASM_SIMP_TAC std_ss [] 11219874Swollman \\ SRW_TAC [] [x86_2set'_def,x86_2set''_def,x86_2set_def,IN_UNION, 113158421Swollman IN_INSERT,NOT_IN_EMPTY,IN_DIFF,PUSH_IN_INTO_IF,XREAD_REG_def, 114163302Sru XREAD_EIP_def,XREAD_EFLAG_def,X86_GET_MEMORY_def] 115163302Sru \\ METIS_TAC []); 116121098Swollman 117121098Swollmanval x86_2set''_11 = prove( 11819874Swollman ``!y y2 s s2. (x86_2set'' y2 s2 = x86_2set'' y s) ==> (y = y2)``, 11919874Swollman REPEAT STRIP_TAC \\ CCONTR_TAC 120169811Swollman \\ `?rs st ep m st. y = (rs,st,ep,m)` by METIS_TAC [PAIR] 121149514Swollman \\ `?rs2 st2 ep2 m2. y2 = (rs2,st2,ep2,m2)` by METIS_TAC [PAIR] 122187588Sedwin \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] 123163302Sru \\ `?r2 e2 t2 m2 i2. s2 = (r2,e2,t2,m2,i2)` by METIS_TAC [PAIR] 124163302Sru \\ FULL_SIMP_TAC bool_ss [PAIR_EQ,EXTENSION] 12519874Swollman THEN1 126163302Sru (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.SPEC `xReg xi yi`) 12719874Swollman \\ FULL_SIMP_TAC std_ss [IN_x86_2set] \\ METIS_TAC []) 12819874Swollman THEN1 12919874Swollman (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `xi` o Q.GEN `yi` o Q.SPEC `xStatus xi yi`) 130171948Sedwin \\ FULL_SIMP_TAC std_ss [IN_x86_2set] \\ METIS_TAC []) 13119874Swollman THEN1 132163302Sru (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.GEN `ei` o Q.SPEC `xEIP ei`) 13319874Swollman \\ FULL_SIMP_TAC std_ss [IN_x86_2set] \\ METIS_TAC []) 13419874Swollman THEN 13519874Swollman (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`) 13619874Swollman \\ FULL_SIMP_TAC std_ss [IN_x86_2set] \\ METIS_TAC [])); 13719874Swollman 13837998Sdesval DELETE_x86_2set = prove(`` 13937998Sdes (!a. (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) DELETE xReg a (r a) = 14019874Swollman (x86_2set' (rs DELETE a,st,ei,ms) (r,e,s,m,i))) /\ 14119874Swollman (!c. (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) DELETE xStatus c (s c) = 14219874Swollman (x86_2set' (rs,st DELETE c,ei,ms) (r,e,s,m,i))) /\ 14319874Swollman (!c. (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) DELETE xEIP e = 14419874Swollman (x86_2set' (rs,st,F,ms) (r,e,s,m,i))) /\ 14586222Swollman (!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)) = 146169811Swollman (x86_2set' (rs,st,ei,ms DELETE b) (r,e,s,m,i)))``, 14719874Swollman REPEAT STRIP_TAC 14893799Swollman \\ SRW_TAC [] [x86_2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR, 149163302Sru EXISTS_OR_THM,IN_DELETE,IN_INSERT,NOT_IN_EMPTY,PUSH_IN_INTO_IF, 150163302Sru XREAD_REG_def,XREAD_MEM_def,XREAD_EFLAG_def,XREAD_EIP_def] 151163302Sru \\ Cases_on `x` \\ SRW_TAC [] [] \\ METIS_TAC []); 152163302Sru 15319874Swollmanval EMPTY_x86_2set = prove(`` 15419874Swollman (x86_2set' (rs,st,e,ms) s = {}) = (rs = {}) /\ (ms = {}) /\ (st = {}) /\ ~e``, 15519874Swollman REPEAT STRIP_TAC 15619874Swollman \\ `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] \\ ASM_SIMP_TAC std_ss [] 15719874Swollman \\ SRW_TAC [] [x86_2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR, 15819874Swollman EXISTS_OR_THM,IN_DELETE,IN_INSERT,NOT_IN_EMPTY,PUSH_IN_INTO_IF] 15919874Swollman \\ SIMP_TAC std_ss [x86_el_distinct,x86_el_11] \\ METIS_TAC [PAIR,FST]); 16019874Swollman 16119874Swollman 16219874Swollman(* ----------------------------------------------------------------------------- *) 16319874Swollman(* Defining the X86_MODEL *) 16419874Swollman(* ----------------------------------------------------------------------------- *) 16519874Swollman 16619874Swollmanval xR_def = Define `xR a x = SEP_EQ {xReg a x}`; 16719874Swollmanval xM1_def = Define `xM1 a x b = SEP_EQ {xMem a x b}`; 16819874Swollmanval xS1_def = Define `xS1 a x = SEP_EQ {xStatus a x}`; 16919874Swollmanval xPC_def = Define `xPC x = SEP_EQ {xEIP x}`; 17019874Swollman 171169811Swollmanval xS_def = Define ` 17219874Swollman xS (x0,x1,x2,x3,x4,x5) = 17319874Swollman xS1 X_CF x0 * xS1 X_PF x1 * xS1 X_AF x2 * 17419874Swollman xS1 X_ZF x3 * xS1 X_SF x4 * xS1 X_OF x5`; 17519874Swollman 17619874Swollmanval X86_INSTR_PERM_def = Define ` 17719874Swollman X86_INSTR_PERM b = {Xread;Xexecute} UNION (if b then {Xwrite} else {})`; 17819874Swollman 179149514Swollmanval X86_INSTR_def = Define ` 18019874Swollman (X86_INSTR (a,([],b)) = {}) /\ 18119874Swollman (X86_INSTR (a,((c:word8)::cs,b)) = 182169811Swollman xMem a (SOME (c,X86_INSTR_PERM b)) T INSERT X86_INSTR (a+1w,(cs,b)))`; 18319874Swollman 18419874Swollmanval X86_MODEL_def = Define ` 185171948Sedwin X86_MODEL = (x86_2set, X86_NEXT_REL, X86_INSTR, X86_ICACHE, 18619874Swollman (K F):x86_state->bool)`; 18719874Swollman 18819874Swollmanval xCODE_def = Define `xCODE = CODE_POOL X86_INSTR`; 189163302Sru 19019874Swollmanval xM_def = Define ` 19119874Swollman xM a (w:word32) = 19286222Swollman ~xM1 a (SOME ((7 >< 0) w,{Xread;Xwrite})) * 19393799Swollman ~xM1 (a + 1w) (SOME ((7 >< 0) (w >> 8),{Xread;Xwrite})) * 194163302Sru ~xM1 (a + 2w) (SOME ((7 >< 0) (w >> 16),{Xread;Xwrite})) * 19593799Swollman ~xM1 (a + 3w) (SOME ((7 >< 0) (w >> 24),{Xread;Xwrite}))`; 19619874Swollman 19719874Swollman(* theorems *) 19819874Swollman 19919874Swollmanval lemma = 20019874Swollman METIS_PROVE [SPLIT_x86_2set] 20119874Swollman ``p (x86_2set' y s) ==> (?u v. SPLIT (x86_2set s) (u,v) /\ p u /\ (\v. v = x86_2set'' y s) v)``; 20219874Swollman 20319874Swollmanval X86_SPEC_SEMANTICS = store_thm("X86_SPEC_SEMANTICS", 20419874Swollman ``SPEC X86_MODEL p {} q = 20519874Swollman !y s t1 seq. 20658787Sru p (x86_2set' y t1) /\ X86_ICACHE t1 s /\ rel_sequence X86_NEXT_REL seq s ==> 20719874Swollman ?k t2. q (x86_2set' y t2) /\ X86_ICACHE t2 (seq k) /\ (x86_2set'' y t1 = x86_2set'' y t2)``, 20819874Swollman SIMP_TAC std_ss [GSYM RUN_EQ_SPEC,RUN_def,X86_MODEL_def,STAR_def,SEP_REFINE_def] 20919874Swollman \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC THENL [ 21019874Swollman FULL_SIMP_TAC bool_ss [SPLIT_x86_2set_EXISTS] 21119874Swollman \\ NTAC 3 (POP_ASSUM MP_TAC) \\ ASM_SIMP_TAC std_ss [] 21286222Swollman \\ REPEAT STRIP_TAC \\ RES_TAC 21393799Swollman \\ Q.EXISTS_TAC `k` \\ Q.EXISTS_TAC `t2` 21419874Swollman \\ ASM_SIMP_TAC std_ss [] \\ METIS_TAC [], 21519874Swollman FULL_SIMP_TAC std_ss [METIS_PROVE [] ``((?x. P x) ==> b) = !x. P x ==> b``, 21643014Swollman METIS_PROVE [] ``(b /\ (?x. P x)) = ?x. b /\ P x``] 217163302Sru \\ FULL_SIMP_TAC std_ss [GSYM AND_IMP_INTRO] 218177591Sedwin \\ IMP_RES_TAC lemma \\ RES_TAC 21919874Swollman \\ FULL_SIMP_TAC bool_ss [SPLIT_x86_2set_EXISTS] 22019874Swollman \\ IMP_RES_TAC x86_2set''_11 \\ METIS_TAC []]); 22119874Swollman 22219874Swollman 22319874Swollman(* ----------------------------------------------------------------------------- *) 224169811Swollman(* Theorems for construction of |- SPEC X86_MODEL ... *) 22519874Swollman(* ----------------------------------------------------------------------------- *) 22619874Swollman 22743543Swollmanval STAR_x86_2set = store_thm("STAR_x86_2set", 22819874Swollman ``((xR a x * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 22919874Swollman (x = r a) /\ a IN rs /\ p (x86_2set' (rs DELETE a,st,ei,ms) (r,e,s,m,i))) /\ 23019874Swollman ((xS1 c z * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 23119874Swollman (z = s c) /\ c IN st /\ p (x86_2set' (rs,st DELETE c,ei,ms) (r,e,s,m,i))) /\ 23219874Swollman ((xPC q * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 23319874Swollman (q = e) /\ ei /\ p (x86_2set' (rs,st,F,ms) (r,e,s,m,i))) /\ 23419874Swollman ((xM1 b y w * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 23519874Swollman (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))) /\ 23619874Swollman ((~(xM1 b y) * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 23719874Swollman (y = m b) /\ b IN ms /\ p (x86_2set' (rs,st,ei,ms DELETE b) (r,e,s,m,i))) /\ 23819874Swollman ((cond g * p) (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)) = 23919874Swollman g /\ p (x86_2set' (rs,st,ei,ms) (r,e,s,m,i)))``, 24093799Swollman REPEAT STRIP_TAC 24193799Swollman \\ SIMP_TAC std_ss [SEP_HIDE_def,SEP_CLAUSES] 24293799Swollman \\ SIMP_TAC std_ss [SEP_EXISTS] 24393799Swollman \\ SIMP_TAC std_ss [xR_def,xS1_def,xM1_def,EQ_STAR,INSERT_SUBSET,cond_STAR,xPC_def,XREAD_EIP_def, 24493799Swollman EMPTY_SUBSET,IN_x86_2set,XREAD_REG_def,XREAD_EFLAG_def,XREAD_MEM_def,GSYM DELETE_DEF,X86_GET_MEMORY_def] 24519874Swollman THEN1 METIS_TAC [DELETE_x86_2set] 24619874Swollman THEN1 METIS_TAC [DELETE_x86_2set] 24719874Swollman THEN1 METIS_TAC [DELETE_x86_2set] 24819874Swollman \\ Cases_on `y = m b` \\ ASM_SIMP_TAC std_ss [] 24919874Swollman \\ Cases_on `w = X86_ACCURATE b (r,e,s,m,i)` 25019874Swollman \\ ASM_SIMP_TAC std_ss [DELETE_x86_2set,AC CONJ_ASSOC CONJ_COMM]); 25119874Swollman 25219874Swollmanval CODE_POOL_x86_2set_AUX_LEMMA = prove( 25319874Swollman ``!x y z. ~(z IN y) ==> ((x = z INSERT y) = z IN x /\ (x DELETE z = y))``, 25419874Swollman SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY,IN_DELETE] \\ METIS_TAC []); 25519874Swollman 25619874Swollmanval address_list_def = Define ` 25719874Swollman (address_list a 0 = {}) /\ 25875267Swollman (address_list a (SUC n) = a INSERT address_list (a+1w) n)`; 259169811Swollman 260174242Sedwinval x86_pool_def = Define ` 26119874Swollman (x86_pool (r,s,e,m,i) p ([],d) = T) /\ 26219874Swollman (x86_pool (r,s,e,m,i) p ((c::cs),d) = 26319874Swollman (SOME (c:word8,X86_INSTR_PERM d) = m p) /\ X86_ACCURATE p (r,s,e,m,i) /\ 26419874Swollman x86_pool (r,s,e,m,i) (p+1w) (cs,d))`; 265149514Swollman 26619874Swollmanval LEMMA1 = prove( 26758787Sru ``!p q cs y b. xMem p y b IN X86_INSTR (q,(cs,d)) ==> ?k. k < LENGTH cs /\ (p = q + n2w k)``, 26886222Swollman Induct_on `cs` 26986222Swollman \\ ASM_SIMP_TAC std_ss [X86_INSTR_def,EMPTY_SUBSET,LENGTH,NOT_IN_EMPTY, 27093799Swollman address_list_def,IN_INSERT,x86_el_11,n2w_11] 27119874Swollman \\ REPEAT STRIP_TAC THEN1 (Q.EXISTS_TAC `0` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0]) 27219874Swollman \\ RES_TAC \\ Q.EXISTS_TAC `k + 1` 27319874Swollman \\ ASM_SIMP_TAC bool_ss [ADD1,GSYM word_add_n2w,WORD_ADD_ASSOC] 274158421Swollman \\ STRIP_TAC THEN1 DECIDE_TAC \\ METIS_TAC [WORD_ADD_ASSOC,WORD_ADD_COMM]); 27519874Swollman 27619874Swollmanval LEMMA2 = prove( 27719874Swollman ``!p q cs. p IN address_list q (LENGTH cs) ==> ?k. k < LENGTH cs /\ (p = q + n2w k)``, 27819874Swollman Induct_on `cs` 27958787Sru \\ ASM_SIMP_TAC std_ss [X86_INSTR_def,EMPTY_SUBSET,LENGTH,NOT_IN_EMPTY, 28058787Sru address_list_def,IN_INSERT,x86_el_11,n2w_11] 28164499Swollman \\ REPEAT STRIP_TAC THEN1 (Q.EXISTS_TAC `0` \\ ASM_SIMP_TAC std_ss [WORD_ADD_0]) 282203019Sedwin \\ RES_TAC \\ Q.EXISTS_TAC `k + 1` 283203019Sedwin \\ ASM_SIMP_TAC bool_ss [ADD1,GSYM word_add_n2w,WORD_ADD_ASSOC] 28458787Sru \\ STRIP_TAC THEN1 DECIDE_TAC \\ METIS_TAC [WORD_ADD_ASSOC,WORD_ADD_COMM]); 285203019Sedwin 286203019Sedwinval CODE_POOL_x86_2set_LEMMA = prove( 28758787Sru ``!cs p ms. 288203019Sedwin LENGTH cs < 5000 ==> 289203019Sedwin (xCODE {(p,(cs,d))} (x86_2set' (rs,st,ei,ms) (r,s,e,m,i)) = 29019874Swollman (ms = address_list p (LENGTH cs)) /\ (rs = {}) /\ (st = {}) /\ ~ei /\ 29119874Swollman x86_pool (r,s,e,m,i) p (cs,d))``, 29219874Swollman Induct 29319874Swollman \\ FULL_SIMP_TAC bool_ss [INSERT_SUBSET,GSYM DELETE_DEF, 294192886Sedwin LENGTH,x86_pool_def, EMPTY_SUBSET,xCODE_def, 29519874Swollman IN_DELETE, IMAGE_INSERT, CODE_POOL_def, IMAGE_EMPTY, 29619874Swollman XREAD_MEM_def, address_list_def, BIGUNION_INSERT, BIGUNION_EMPTY, 29719874Swollman UNION_EMPTY, X86_INSTR_def, IN_x86_2set, EMPTY_x86_2set] 29819874Swollman THEN1 METIS_TAC [] 29919874Swollman \\ REPEAT STRIP_TAC 30019874Swollman \\ `LENGTH cs < 5000` by DECIDE_TAC 301187588Sedwin \\ Cases_on `xMem p (SOME (h,X86_INSTR_PERM d)) T IN X86_INSTR (p + 1w,(cs,d))` 30219874Swollman THEN1 (IMP_RES_TAC LEMMA1 303183864Sedwin \\ FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [ 30419874Swollman REWRITE_RULE [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL), 305121098Swollman GSYM WORD_ADD_ASSOC,word_add_n2w,n2w_11] 30619874Swollman \\ `1 + k < 4294967296` by DECIDE_TAC 30719874Swollman \\ FULL_SIMP_TAC std_ss [LESS_MOD]) 30819874Swollman \\ Cases_on `p IN address_list (p + 1w) (LENGTH cs)` 30919874Swollman THEN1 (IMP_RES_TAC LEMMA2 31019874Swollman \\ FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) [ 31119874Swollman REWRITE_RULE [WORD_ADD_0] (Q.SPECL [`v`,`0w`] WORD_EQ_ADD_LCANCEL), 31219874Swollman GSYM WORD_ADD_ASSOC,word_add_n2w,n2w_11] 31319874Swollman \\ `1 + k < 4294967296` by DECIDE_TAC 31419874Swollman \\ FULL_SIMP_TAC std_ss [LESS_MOD]) 31519874Swollman \\ ASM_SIMP_TAC bool_ss [CODE_POOL_x86_2set_AUX_LEMMA,GSYM CONJ_ASSOC,IN_x86_2set,XREAD_MEM_def] 31619874Swollman \\ Cases_on `SOME (h,X86_INSTR_PERM d) = m p` \\ ASM_REWRITE_TAC [] 31719874Swollman \\ REWRITE_TAC [DIFF_INSERT,DELETE_x86_2set,X86_GET_MEMORY_def] 31819874Swollman \\ Cases_on `X86_ACCURATE p (r,s,e,m,i)` \\ ASM_SIMP_TAC std_ss [] 31943014Swollman \\ `xMem p (m p) T = xMem p (m p) (X86_ACCURATE p (r,s,e,m,i))` by 32019874Swollman FULL_SIMP_TAC std_ss [x86_el_11] 32119874Swollman \\ ONCE_ASM_REWRITE_TAC [] \\ NTAC 2 (POP_ASSUM (K ALL_TAC)) 32219874Swollman \\ REWRITE_TAC [DIFF_INSERT,DELETE_x86_2set,X86_GET_MEMORY_def] 32319874Swollman \\ Cases_on `p IN ms` \\ ASM_REWRITE_TAC [GSYM CONJ_ASSOC] 32419874Swollman \\ FULL_SIMP_TAC bool_ss []); 32519874Swollman 32619874Swollmanval CODE_POOL_x86_2set = store_thm("CODE_POOL_x86_2set", 32719874Swollman ``!cs p ms. 328163302Sru xCODE {(p,(cs,d))} (x86_2set' (rs,st,ei,ms) (r,s,e,m,i)) = 32937998Sdes if LENGTH cs < 5000 then 33019874Swollman (ms = address_list p (LENGTH cs)) /\ (rs = {}) /\ (st = {}) /\ ~ei /\ 331163302Sru x86_pool (r,s,e,m,i) p (cs,d) 332163302Sru else xCODE {(p,(cs,d))} (x86_2set' (rs,st,ei,ms) (r,s,e,m,i))``, 33319874Swollman METIS_TAC [CODE_POOL_x86_2set_LEMMA]); 33419874Swollman 33519874Swollmanval icache_revert_def = Define ` 336198825Sedwin icache_revert (m1:x86_memory,i1:x86_memory) (m2:x86_memory,i2:x86_memory) a = 33719874Swollman if m1 a = m2 a then i1 a else i2 a`; 33837998Sdes 33919874Swollmanval X86_ACCURATE_UPDATE = store_thm("X86_ACCURATE_UPDATE", 34037998Sdes ``(X86_ACCURATE a ((xr =+ yr) r,e,s,m,i) = X86_ACCURATE a (r,e,s,m,i)) /\ 34186222Swollman (X86_ACCURATE a (r,xe,s,m,i) = X86_ACCURATE a (r,e,s,m,i)) /\ 34286222Swollman (X86_ACCURATE a (r,e,(xs =+ ys) s,m,i) = X86_ACCURATE a (r,e,s,m,i)) /\ 34319874Swollman (~(xm = a) ==> (X86_ACCURATE a (r,e,s,(xm =+ ym) m,i) = X86_ACCURATE a (r,e,s,m,i))) /\ 34419874Swollman (~(a = b) ==> 34519874Swollman (X86_ACCURATE a (r,e,s,m,icache_revert (m,i) ((b =+ w) m2,i2)) = 34619874Swollman X86_ACCURATE a (r,e,s,m,icache_revert (m,i) (m2,i2))))``, 34719874Swollman SIMP_TAC std_ss [X86_ACCURATE_def,APPLY_UPDATE_THM,icache_revert_def]); 34819874Swollman 34919874Swollmanval icache_revert_ID = store_thm("icache_revert_ID", 35019874Swollman ``!m i y. icache_revert (m,i) (m,y) = i``, 35119874Swollman SIMP_TAC std_ss [FUN_EQ_THM,icache_revert_def]); 35219874Swollman 35319874Swollmanval icache_revert_update = prove( 354175034Sedwin ``b IN ms ==> 35519874Swollman (x86_2set'' (rs,st,ei,ms) (r,x,t,m, icache_revert (m,i) ((b =+ w) m2,j)) = 35619874Swollman x86_2set'' (rs,st,ei,ms) (r,x,t,m, icache_revert (m,i) (m2,j)))``, 35719874Swollman SIMP_TAC std_ss [EXTENSION] \\ STRIP_TAC \\ Cases 35819874Swollman \\ SIMP_TAC std_ss [IN_x86_2set,XREAD_REG_def,XREAD_EFLAG_def,APPLY_UPDATE_THM, 35919874Swollman XREAD_EIP_def,X86_GET_MEMORY_def,X86_ACCURATE_def,icache_revert_def] 36019874Swollman \\ METIS_TAC []); 36119874Swollman 36219874Swollmanval UPDATE_x86_2set'' = store_thm("UPDATE_x86_2set''", 36319874Swollman ``(!a x. a IN rs ==> 36419874Swollman (x86_2set'' (rs,st,ei,ms) ((a =+ x) r,e,s,m,i) = x86_2set'' (rs,st,ei,ms) (r,e,s,m,i))) /\ 36519874Swollman (!a x. a IN st ==> 36619874Swollman (x86_2set'' (rs,st,ei,ms) (r,e,(a =+ x) s,m,i) = x86_2set'' (rs,st,ei,ms) (r,e,s,m,i))) /\ 36737998Sdes (!a x y. 36819874Swollman ((x86_2set'' (rs,st,T,ms) (r,x,s,m,i) = x86_2set'' (rs,st,T,ms) (r,y,s,m,i)) = T)) /\ 36919874Swollman (!a x. a IN ms ==> 37019874Swollman (x86_2set'' (rs,st,ei,ms) (r,e,s,(a =+ x) m,i) = x86_2set'' (rs,st,ei,ms) (r,e,s,m,i))) /\ 37119874Swollman (!a x. a IN ms ==> 372105195Swollman (x86_2set'' (rs,st,ei,ms) (r,x,t,m, icache_revert (m,i) ((a =+ w) m2,j)) = 37367578Swollman x86_2set'' (rs,st,ei,ms) (r,x,t,m, icache_revert (m,i) (m2,j))))``, 37419874Swollman SIMP_TAC std_ss [x86_2set_def,x86_2set''_def,x86_2set'_def,EXTENSION,IN_UNION, 375192886Sedwin IN_INSERT,NOT_IN_EMPTY,IN_IMAGE,IN_DIFF,IN_UNIV,XREAD_REG_def,XREAD_MEM_def, 37619874Swollman XREAD_EFLAG_def,APPLY_UPDATE_THM,XREAD_EIP_def,icache_revert_update] 37719874Swollman \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 37819874Swollman \\ ASM_SIMP_TAC std_ss [] \\ SRW_TAC [] [X86_ACCURATE_UPDATE] 37919874Swollman \\ METIS_TAC [X86_ACCURATE_UPDATE]); 38019874Swollman 38119874Swollmanval X86_SPEC_CODE = save_thm("X86_SPEC_CODE", 38258787Sru RW [GSYM X86_MODEL_def,GSYM xCODE_def] 383171948Sedwin (SIMP_RULE std_ss [X86_MODEL_def] (Q.ISPEC `X86_MODEL` SPEC_CODE))); 38458787Sru 38519874Swollmanval IMP_X86_SPEC_LEMMA = prove( 386171948Sedwin ``!p q. 38719874Swollman (!y s t1. 38819874Swollman p (x86_2set' y t1) /\ X86_ICACHE t1 s ==> 38919874Swollman ?v t2. 39019874Swollman p (x86_2set' y s) /\ 391149514Swollman (X86_NEXT s = SOME v) /\ q (x86_2set' y t2) /\ X86_ICACHE t2 v /\ 39267578Swollman (x86_2set'' y t1 = x86_2set'' y t2)) ==> 393158421Swollman SPEC X86_MODEL p {} q``, 394171948Sedwin REWRITE_TAC [X86_SPEC_SEMANTICS] \\ REPEAT STRIP_TAC 395169811Swollman \\ `p (x86_2set' y s)` by METIS_TAC [] 396158421Swollman \\ `X86_NEXT_REL (seq 0) (seq (SUC 0))` by 397184406Sedwin (`?x. X86_NEXT_REL (seq 0) x` by 398158421Swollman (RES_TAC \\ Q.EXISTS_TAC `v'` 39919874Swollman \\ ASM_SIMP_TAC std_ss [X86_NEXT_REL_def] 400171948Sedwin \\ Q.EXISTS_TAC `seq 0` \\ ASM_SIMP_TAC std_ss [] 401184406Sedwin \\ FULL_SIMP_TAC bool_ss [rel_sequence_def,X86_ICACHE_REFL]) 402158421Swollman \\ METIS_TAC [rel_sequence_def]) 40386222Swollman \\ FULL_SIMP_TAC std_ss [X86_NEXT_REL_def] 404158421Swollman \\ `seq 0 = s` by FULL_SIMP_TAC std_ss [rel_sequence_def] 40519874Swollman \\ FULL_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `1` 40619874Swollman \\ `X86_ICACHE t1 u` by IMP_RES_TAC X86_ICACHE_TRANS 40719874Swollman \\ Q.PAT_ASSUM `!y s t1. bbb` (STRIP_ASSUME_TAC o UNDISCH_ALL o 40819874Swollman RW [GSYM AND_IMP_INTRO] o Q.SPECL [`y`,`u`,`t1`]) 40919874Swollman \\ Q.EXISTS_TAC `t2` 41019874Swollman \\ FULL_SIMP_TAC std_ss [optionTheory.SOME_11] \\ METIS_TAC []); 41119874Swollman 41219874Swollmanval X86_ICACHE_EXTRACT_def = Define ` 41319874Swollman X86_ICACHE_EXTRACT ((r1,e1,s1,m1,i1):x86_state) = i1`; 41419874Swollman 41519874Swollmanval X86_ICACHE_THM2 = prove( 41619874Swollman ``!s t. X86_ICACHE s t = ?z. t = X86_ICACHE_UPDATE z s``, 41743014Swollman REPEAT STRIP_TAC 41843014Swollman \\ `?r1 e1 s1 m1 i1. s = (r1,e1,s1,m1,i1)` by METIS_TAC [PAIR] 419192886Sedwin \\ `?r2 e2 s2 m2 i2. t = (r2,e2,s2,m2,i2)` by METIS_TAC [PAIR] 42019874Swollman \\ FULL_SIMP_TAC std_ss [X86_ICACHE_UPDATE_def,X86_ICACHE_THM]); 42119874Swollman 42219874Swollmanval X86_ICACHE_X86_ACCURATE = prove( 42319874Swollman ``X86_ICACHE (r1,e1,s1,m1,i1) (r1,e1,s1,m1,i2) = 424177591Sedwin !a. X86_ACCURATE a (r1,e1,s1,m1,i2) \/ (i1 a = i2 a)``, 42519874Swollman REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 42619874Swollman THEN1 (FULL_SIMP_TAC std_ss [X86_ACCURATE_def,X86_ICACHE_def,FUN_EQ_THM] 42719874Swollman \\ Cases_on `a IN insert` \\ ASM_SIMP_TAC std_ss [] 42819874Swollman \\ Cases_on `a IN delete` \\ ASM_SIMP_TAC std_ss []) 42919874Swollman \\ SIMP_TAC std_ss [X86_ICACHE_def,FUN_EQ_THM] 43019874Swollman \\ Q.EXISTS_TAC `{ a | X86_ACCURATE a (r1,e1,s1,m1,i2) /\ ~(i2 a = NONE) }` 43119874Swollman \\ Q.EXISTS_TAC `{ a | X86_ACCURATE a (r1,e1,s1,m1,i2) /\ (i2 a = NONE) }` 43219874Swollman \\ 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