1 2open HolKernel boolLib bossLib Parse; 3open wordsTheory pred_setTheory pairTheory; 4 5open x64_coretypesTheory x64_astTheory x64_seq_monadTheory; 6 7val _ = new_theory "x64_icache"; 8val _ = ParseExtras.temp_loose_equality() 9 10 11(* instruction cache definitions *) 12 13val X64_ICACHE_def = Define ` 14 X64_ICACHE ((r,e,s,m,i):x64_state) ((r2,e2,s2,m2,i2):x64_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 X64_ACCURATE_def = Define ` 21 X64_ACCURATE a ((r,e,s,m,i):x64_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 X64_ICACHE_UPDATE_def = Define ` 28 X64_ICACHE_UPDATE x ((r1,e1,s1,m1,i1):x64_state) = (r1,e1,s1,m1,icache x m1 i1)`; 29 30 31(* theorems *) 32 33val X64_ICACHE_REFL = store_thm("X64_ICACHE_REFL", 34 ``!s. X64_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 [X64_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 X64_ICACHE_TRANS = store_thm("X64_ICACHE_TRANS", 41 ``!s t u. X64_ICACHE s t /\ X64_ICACHE t u ==> X64_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 [X64_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 X64_ICACHE_THM = store_thm("X64_ICACHE_THM", 53 ``X64_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,X64_ICACHE_def,icache_def,FUN_EQ_THM] 57 THEN METIS_TAC []); 58 59val ZREAD_CLAUSES = store_thm("ZREAD_CLAUSES", 60 ``!s. (ZREAD_REG r (ZWRITE_REG r2 w s) = if r2 = r then w else ZREAD_REG r s) /\ 61 (ZREAD_REG r (ZWRITE_RIP e s) = ZREAD_REG r s) /\ 62 (ZREAD_REG r (ZWRITE_EFLAG f b s) = ZREAD_REG r s) /\ 63 (ZREAD_REG r (ZCLEAR_ICACHE s) = ZREAD_REG r s) /\ 64 (ZREAD_REG r (X64_ICACHE_UPDATE u s) = ZREAD_REG r s) /\ 65 (ZREAD_REG r (ZWRITE_MEM2 a x s) = ZREAD_REG r s) /\ 66 (ZREAD_RIP (ZWRITE_REG r2 w s) = ZREAD_RIP s) /\ 67 (ZREAD_RIP (ZWRITE_RIP e s) = e) /\ 68 (ZREAD_RIP (ZWRITE_EFLAG f b s) = ZREAD_RIP s) /\ 69 (ZREAD_RIP (ZCLEAR_ICACHE s) = ZREAD_RIP s) /\ 70 (ZREAD_RIP (X64_ICACHE_UPDATE u s) = ZREAD_RIP s) /\ 71 (ZREAD_RIP (ZWRITE_MEM2 a x s) = ZREAD_RIP s) /\ 72 (ZREAD_EFLAG i (ZWRITE_REG r2 w s) = ZREAD_EFLAG i s) /\ 73 (ZREAD_EFLAG i (ZWRITE_RIP e s) = ZREAD_EFLAG i s) /\ 74 (ZREAD_EFLAG i (ZWRITE_EFLAG f b s) = if f = i then b else ZREAD_EFLAG i s) /\ 75 (ZREAD_EFLAG i (ZCLEAR_ICACHE s) = ZREAD_EFLAG i s) /\ 76 (ZREAD_EFLAG i (X64_ICACHE_UPDATE u s) = ZREAD_EFLAG i s) /\ 77 (ZREAD_EFLAG i (ZWRITE_MEM2 a x s) = ZREAD_EFLAG i s) /\ 78 (ZREAD_MEM2 a (ZWRITE_REG r2 w s) = ZREAD_MEM2 a s) /\ 79 (ZREAD_MEM2 a (ZWRITE_RIP e s) = ZREAD_MEM2 a s) /\ 80 (ZREAD_MEM2 a (ZWRITE_EFLAG f b s) = ZREAD_MEM2 a s) /\ 81 (ZREAD_MEM2 a (ZCLEAR_ICACHE s) = ZREAD_MEM2 a s) /\ 82 (ZREAD_MEM2 a (X64_ICACHE_UPDATE u s) = ZREAD_MEM2 a s) /\ 83 (ZREAD_MEM2 a (ZWRITE_MEM2 c x s) = if a = c then x else ZREAD_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 [ZREAD_REG_def,ZREAD_RIP_def, 87 ZREAD_EFLAG_def, ZWRITE_REG_def, ZWRITE_MEM2_def, ZREAD_MEM2_def, 88 combinTheory.APPLY_UPDATE_THM, ZWRITE_RIP_def,CAN_ZREAD_MEM, 89 ZWRITE_EFLAG_def,ZCLEAR_ICACHE_def,CAN_ZWRITE_MEM,X64_ICACHE_UPDATE_def] 90 THEN Cases_on `c = a` THEN ASM_SIMP_TAC std_ss []); 91 92 93val _ = export_theory (); 94