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