1
2open HolKernel boolLib bossLib Parse;
3open wordsTheory pred_setTheory;
4
5open armTheory arm_stepTheory lpc_uartTheory;
6
7val _ = new_theory "lpc_devices";
8
9
10(* We define the type of a generic device *)
11
12val _ = type_abbrev ("device",``:
13   (* memory addresses that belong to this device, dependent on internal state of type 'a *)
14   ('a -> word32 set) #
15   (* if core executes a memory read, it sees the following data *)
16   ('a -> word32 -> word8) #
17   (* the next state relation for the devive  *)
18   (num -> memory_access list -> 'a -> 'a -> bool) #
19   (* an invariant that mst be true for this devie to make sense *)
20   (num # 'a -> bool)``);
21
22
23(* Devices can be composed *)
24
25val ACCESS_ADDRESS_def = Define `
26  (ACCESS_ADDRESS (MEM_READ w) = w) /\
27  (ACCESS_ADDRESS (MEM_WRITE w v) = w)`;
28
29val FILTER_ACCESSES_def = Define `
30  FILTER_ACCESSES d = FILTER (\x. (ACCESS_ADDRESS x) IN d)`;
31
32val COMPOSE_DEVICES_def = Define `
33  COMPOSE_DEVICES ((a1,m1,n1,i1):'a device) ((a2,m2,n2,i2):'b device) =
34     (* the combined addresses are the UNION of the two address sets *)
35    ((\(x,y). a1 x UNION a2 y),
36     (* memory reads are directed according to address ownership *)
37     (\(x,y) addr. if addr IN a1 x then m1 x addr else m2 y addr),
38     (* the combined next state relation filters memory accesses so that
39        respective devices only see relevant memoy accesses *)
40     (\t l (x1,y1) (x2,y2). n1 t (FILTER_ACCESSES (a1 x1) l) x1 x2 /\
41                            n2 t (FILTER_ACCESSES (a2 y1) l) y1 y2),
42     (* the invariant is the conjunction of part invariants and the condition
43        that the space used by these devices does not overlap. *)
44     (\(t,(x,y)). DISJOINT (a1 x) (a2 y) /\ i1 (t,x) /\ i2 (t,y))):('a # 'b) device`
45
46
47(* The most basic device: the EMPTY_DEVICE *)
48
49val EMPTY_DEVICE_def = Define `
50  (EMPTY_DEVICE:unit device) = ((\x. {}),(\x y. ARB),(\n l x y. T),(\x. T))`;
51
52
53(* RAM device *)
54
55val domain_def = Define `domain r = { a | ~(r a = NONE) }`;
56
57val UPDATE_RAM_def = Define `
58  (UPDATE_RAM [] ram = ram) /\
59  (UPDATE_RAM ((MEM_READ w)::xs) ram = UPDATE_RAM xs ram) /\
60  (UPDATE_RAM ((MEM_WRITE w v)::xs) ram = UPDATE_RAM xs (\a. if a = w then SOME v else ram a))`;
61
62val RAM_NEXT_def = Define `
63  RAM_NEXT (t:num) l (r1:word32 -> word8 option) r2 = (r2 = UPDATE_RAM l r1)`;
64
65val RAM_DEVICE_def = Define `
66  (RAM_DEVICE:(word32 -> word8 option) device) =
67    (domain, (\m addr. THE (m addr)), RAM_NEXT, (\x. T))`;
68
69
70(* ROM device - disallows write accesses *)
71
72val IS_WRITE_def = Define `
73  (IS_WRITE (MEM_READ w) = F) /\
74  (IS_WRITE (MEM_WRITE w v) = T)`;
75
76val ROM_NEXT_def = Define `
77  ROM_NEXT (t:num) l r1 r2 = (r2 = r1) /\ (FILTER IS_WRITE l = [])`;
78
79val ROM_DEVICE_def = Define `
80  (ROM_DEVICE:(word32 -> word8 option) device) =
81    (domain, (\m addr. THE (m addr)), ROM_NEXT, (\x. T))`;
82
83
84(* UART0 device *)
85
86val UART0_DEVICE_def = Define `
87  (UART0_DEVICE:uart0_state device) =
88    ((\x. UART0_addresses), UART0_read, UART0_NEXT, \(x,y). uart0_ok x y)`;
89
90
91(* The collection of all peripherals *)
92
93val ALL_PERIPHERALS_def = Define `
94  ALL_PERIPHERALS =
95   (COMPOSE_DEVICES (ROM_DEVICE)
96   (COMPOSE_DEVICES (RAM_DEVICE)
97   (COMPOSE_DEVICES (UART0_DEVICE)
98                    (EMPTY_DEVICE))))`;
99
100val PERIPHERALS_NEXT_def = Define `
101  PERIPHERALS_NEXT =
102    let (addresses,mem,next,inv) = ALL_PERIPHERALS in
103      \l (t1,x) (t2,y).
104        next t1 l x y /\ (t2 = t1 + 1) /\
105        (FILTER_ACCESSES (UNIV DIFF addresses x) l = [])`;
106
107val PERIPHERALS_OK_def = Define `
108  PERIPHERALS_OK =
109    let (addresses,mem,next,inv) = ALL_PERIPHERALS in inv`;
110
111val MEMORY_IMAGE_def = Define `
112  MEMORY_IMAGE (t:num,s) =
113    let (addresses,mem,next,inv) = ALL_PERIPHERALS in mem s`;
114
115val PENDING_INTERRUPT_def = Define `
116  PENDING_INTERRUPT p1 = NoInterrupt`;
117
118val peripherals_type =
119  ``PERIPHERALS_NEXT`` |> type_of |> dest_type |> snd |> el 2
120                                  |> dest_type |> snd |> el 1
121
122val _ = type_abbrev ("peripherals", peripherals_type)
123
124val PER_READ_ROM_def = Define `PER_READ_ROM ((t,x,y):peripherals) a = THE (x a)`;
125val PER_READ_RAM_def = Define `PER_READ_RAM ((t,x,y,z):peripherals) a = THE (y a)`;
126val PER_READ_UART_def = Define `PER_READ_UART ((t,x,y,u,z):peripherals) a = u`;
127
128
129(* The overall next-state relation *)
130
131val LOAD_IMAGE_def = Define `
132  LOAD_IMAGE (s:arm_state) m = s with <|memory := m; accesses := []|>`;
133
134val LPC_NEXT_def = Define `
135  LPC_NEXT (s1,p1) (s2,p2) =
136    (ARM_NEXT (PENDING_INTERRUPT p1)
137              (LOAD_IMAGE s1 (MEMORY_IMAGE p1)) = SOME s2) /\
138    PERIPHERALS_NEXT s2.accesses p1 p2`;
139
140
141(* Theorems *)
142
143val domain_UPDATE_RAM = prove(
144  ``!l p. (domain (UPDATE_RAM
145            (FILTER (\x. ACCESS_ADDRESS x IN domain p) l) p) = domain p)``,
146  SIMP_TAC std_ss [GSPECIFICATION] THEN Induct_on `l`
147  THEN SIMP_TAC std_ss [UPDATE_RAM_def,listTheory.FILTER]
148  THEN Cases_on `h` THEN SIMP_TAC std_ss [ACCESS_ADDRESS_def]
149  THEN REPEAT STRIP_TAC THEN Cases_on `c IN domain p` THEN ASM_SIMP_TAC std_ss []
150  THEN ASM_SIMP_TAC std_ss [UPDATE_RAM_def]
151  THEN `domain p = domain (\a. if a = c then SOME c0 else p a)` by
152   (FULL_SIMP_TAC std_ss [domain_def,GSPECIFICATION,EXTENSION]
153    THEN REPEAT STRIP_TAC THEN Cases_on `x = c` THEN ASM_SIMP_TAC std_ss [])
154  THEN ASM_SIMP_TAC std_ss []);
155
156val IMP_PERIPHERALS_OK = store_thm("IMP_PERIPHERALS_OK",
157  ``!p1 p2 l.
158      PERIPHERALS_OK p1 /\ PERIPHERALS_NEXT l p1 p2 ==>
159      PERIPHERALS_OK p2``,
160  SIMP_TAC std_ss [PERIPHERALS_OK_def,ALL_PERIPHERALS_def,UART0_DEVICE_def,
161    COMPOSE_DEVICES_def,ROM_DEVICE_def,RAM_DEVICE_def,EMPTY_DEVICE_def,
162    pairTheory.FORALL_PROD,LET_DEF,PERIPHERALS_NEXT_def,FILTER_ACCESSES_def,
163    listTheory.FILTER,ROM_NEXT_def,RAM_NEXT_def,UPDATE_RAM_def]
164  THEN SIMP_TAC std_ss [domain_UPDATE_RAM,UART0_NEXT_def]);
165
166val PERIPHERALS_NEXT_EXISTS = store_thm("PERIPHERALS_NEXT_EXISTS",
167  ``!p1. PERIPHERALS_OK p1 ==> ?p2. PERIPHERALS_NEXT [] p1 p2``,
168  SIMP_TAC std_ss [PERIPHERALS_OK_def,ALL_PERIPHERALS_def,UART0_DEVICE_def,
169    COMPOSE_DEVICES_def,ROM_DEVICE_def,RAM_DEVICE_def,EMPTY_DEVICE_def,
170    pairTheory.FORALL_PROD,LET_DEF,PERIPHERALS_NEXT_def,FILTER_ACCESSES_def,
171    listTheory.FILTER,ROM_NEXT_def,RAM_NEXT_def,UPDATE_RAM_def,
172    pairTheory.EXISTS_PROD] THEN METIS_TAC [UART0_NEXT_EXISTS]);
173
174
175val _ = export_theory();
176