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