1 2open HolKernel boolLib bossLib Parse; 3open wordsTheory pred_setTheory pairTheory; 4 5open x86_coretypesTheory x86_astTheory x86_seq_monadTheory; 6 7val _ = new_theory "x86_icache"; 8val _ = ParseExtras.temp_loose_equality() 9 10 11(* instruction cache definitions *) 12 13val X86_ICACHE_def = Define ` 14 X86_ICACHE ((r,e,s,m,i):x86_state) ((r2,e2,s2,m2,i2):x86_state) = 15 ?insert delete. 16 (r = r2) /\ (e = e2) /\ (s = s2) /\ (m = m2) /\ 17 (i2 = \addr. if addr IN insert then m addr else 18 if addr IN delete then NONE else i addr)`; 19 20val X86_ACCURATE_def = Define ` 21 X86_ACCURATE a ((r,e,s,m,i):x86_state) = (i a = NONE) \/ (i a = m a)`; 22 23val icache_def = Define ` 24 icache (insert,delete) m i addr = 25 if addr IN insert then m addr else if addr IN delete then NONE else i addr`; 26 27val X86_ICACHE_UPDATE_def = Define ` 28 X86_ICACHE_UPDATE x ((r1,e1,s1,m1,i1):x86_state) = (r1,e1,s1,m1,icache x m1 i1)`; 29 30 31(* theorems *) 32 33val X86_ICACHE_REFL = store_thm("X86_ICACHE_REFL", 34 ``!s. X86_ICACHE s s``, 35 STRIP_TAC THEN `?r e t m i. s = (r,e,t,m,i)` by METIS_TAC [PAIR] 36 THEN ASM_SIMP_TAC std_ss [X86_ICACHE_def] 37 THEN Q.EXISTS_TAC `{}` THEN Q.EXISTS_TAC `{}` 38 THEN ASM_SIMP_TAC std_ss [NOT_IN_EMPTY,FUN_EQ_THM]); 39 40val X86_ICACHE_TRANS = store_thm("X86_ICACHE_TRANS", 41 ``!s t u. X86_ICACHE s t /\ X86_ICACHE t u ==> X86_ICACHE s u``, 42 REPEAT STRIP_TAC 43 THEN `?r1 e1 t1 m1 i1. s = (r1,e1,t1,m1,i1)` by METIS_TAC [PAIR] 44 THEN `?r2 e2 t2 m2 i2. t = (r2,e2,t2,m2,i2)` by METIS_TAC [PAIR] 45 THEN `?r3 e3 t3 m3 i3. u = (r3,e3,t3,m3,i3)` by METIS_TAC [PAIR] 46 THEN FULL_SIMP_TAC std_ss [X86_ICACHE_def,FUN_EQ_THM] 47 THEN REPEAT (POP_ASSUM (K ALL_TAC)) 48 THEN Q.EXISTS_TAC `insert' UNION (insert DIFF delete')` 49 THEN Q.EXISTS_TAC `delete UNION delete'` 50 THEN SIMP_TAC std_ss [IN_DIFF,IN_INSERT,IN_UNION] THEN METIS_TAC []); 51 52val X86_ICACHE_THM = store_thm("X86_ICACHE_THM", 53 ``X86_ICACHE (r,e,s,m,i) (r2,e2,s2,m2,i2) = 54 ?update. 55 (r2,e2,s2,m2,i2) = (r,e,s,m,icache update m i)``, 56 SIMP_TAC std_ss [EXISTS_PROD,X86_ICACHE_def,icache_def,FUN_EQ_THM] 57 THEN METIS_TAC []); 58 59val XREAD_CLAUSES = store_thm("XREAD_CLAUSES", 60 ``!s. (XREAD_REG r (XWRITE_REG r2 w s) = if r2 = r then w else XREAD_REG r s) /\ 61 (XREAD_REG r (XWRITE_EIP e s) = XREAD_REG r s) /\ 62 (XREAD_REG r (XWRITE_EFLAG f b s) = XREAD_REG r s) /\ 63 (XREAD_REG r (XCLEAR_ICACHE s) = XREAD_REG r s) /\ 64 (XREAD_REG r (X86_ICACHE_UPDATE u s) = XREAD_REG r s) /\ 65 (XREAD_REG r (XWRITE_MEM2 a x s) = XREAD_REG r s) /\ 66 (XREAD_EIP (XWRITE_REG r2 w s) = XREAD_EIP s) /\ 67 (XREAD_EIP (XWRITE_EIP e s) = e) /\ 68 (XREAD_EIP (XWRITE_EFLAG f b s) = XREAD_EIP s) /\ 69 (XREAD_EIP (XCLEAR_ICACHE s) = XREAD_EIP s) /\ 70 (XREAD_EIP (X86_ICACHE_UPDATE u s) = XREAD_EIP s) /\ 71 (XREAD_EIP (XWRITE_MEM2 a x s) = XREAD_EIP s) /\ 72 (XREAD_EFLAG i (XWRITE_REG r2 w s) = XREAD_EFLAG i s) /\ 73 (XREAD_EFLAG i (XWRITE_EIP e s) = XREAD_EFLAG i s) /\ 74 (XREAD_EFLAG i (XWRITE_EFLAG f b s) = if f = i then b else XREAD_EFLAG i s) /\ 75 (XREAD_EFLAG i (XCLEAR_ICACHE s) = XREAD_EFLAG i s) /\ 76 (XREAD_EFLAG i (X86_ICACHE_UPDATE u s) = XREAD_EFLAG i s) /\ 77 (XREAD_EFLAG i (XWRITE_MEM2 a x s) = XREAD_EFLAG i s) /\ 78 (XREAD_MEM2 a (XWRITE_REG r2 w s) = XREAD_MEM2 a s) /\ 79 (XREAD_MEM2 a (XWRITE_EIP e s) = XREAD_MEM2 a s) /\ 80 (XREAD_MEM2 a (XWRITE_EFLAG f b s) = XREAD_MEM2 a s) /\ 81 (XREAD_MEM2 a (XCLEAR_ICACHE s) = XREAD_MEM2 a s) /\ 82 (XREAD_MEM2 a (X86_ICACHE_UPDATE u s) = XREAD_MEM2 a s) /\ 83 (XREAD_MEM2 a (XWRITE_MEM2 c x s) = if a = c then x else XREAD_MEM2 a s)``, 84 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR] 85 THEN Cases_on `u` 86 THEN ASM_SIMP_TAC std_ss [XREAD_REG_def,XREAD_EIP_def, 87 XREAD_EFLAG_def, XWRITE_REG_def, XWRITE_MEM2_def, XREAD_MEM2_def, 88 combinTheory.APPLY_UPDATE_THM, XWRITE_EIP_def,CAN_XREAD_MEM, 89 XWRITE_EFLAG_def,XCLEAR_ICACHE_def,CAN_XWRITE_MEM,X86_ICACHE_UPDATE_def] 90 THEN Cases_on `c = a` THEN ASM_SIMP_TAC std_ss []); 91 92 93val _ = export_theory (); 94