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