1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11(*<*) 12theory Library_CAMKES 13imports Types_CAMKES Wellformed_CAMKES 14begin 15(*>*) 16 17(*<*) 18(* Definitions of some built-in CAmkES entities. *) 19definition 20 seL4RPC :: connector 21where 22 "seL4RPC \<equiv> SyncConnector (Native RPC)" 23lemma[simp]: "wellformed_connector seL4RPC" 24 by (auto simp:wellformed_connector_def seL4RPC_def) 25 26definition 27 seL4Asynch :: connector 28where 29 "seL4Asynch \<equiv> AsyncConnector (Native AsynchronousEvent)" 30lemma[simp]: "wellformed_connector seL4Asynch" 31 by (auto simp:wellformed_connector_def seL4Asynch_def) 32 33definition 34 seL4SharedData :: connector 35where 36 "seL4SharedData \<equiv> MemoryConnector (Native SharedData)" 37lemma[simp]: "wellformed_connector seL4SharedData" 38 by (auto simp:wellformed_connector_def seL4SharedData_def) 39 40(* These connectors aren't literally identical, but for the purposes of the architectural model they 41 * are. 42 *) 43definition 44 seL4RPCSimple :: connector 45where 46 "seL4RPCSimple \<equiv> seL4RPC" 47lemma[simp]: "wellformed_connector seL4RPCSimple" 48 by (simp add:seL4RPCSimple_def) 49 50definition 51 seL4RPCCall :: connector 52where 53 "seL4RPCCall \<equiv> seL4RPC" 54lemma[simp]: "wellformed_connector seL4RPCCall" 55 by (simp add:seL4RPCCall_def) 56 57definition 58 seL4Notification :: connector 59where 60 "seL4Notification \<equiv> seL4Asynch" 61lemma[simp]: "wellformed_connector seL4Notification" 62 by (simp add:seL4Notification_def) 63 64lemmas connector_simps = 65 seL4SharedData_def 66 seL4RPC_def 67 seL4Asynch_def 68 seL4RPCSimple_def 69 seL4RPCCall_def 70 seL4Notification_def 71 72(*>*) 73 74(*<*)end(*>*) 75