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