1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Definition of access rights.
9*)
10
11chapter "Access Rights"
12
13theory CapRights_A
14imports Main
15begin
16
17text \<open>The possible access-control rights that exist in the system.
18        Note that some rights are synonyms for others.\<close>
19datatype rights = AllowRead | AllowWrite | AllowGrant | AllowGrantReply
20
21definition
22  "AllowSend \<equiv> AllowWrite"
23definition
24  "AllowRecv \<equiv> AllowRead"
25definition
26  "CanModify \<equiv> AllowWrite"
27
28text \<open>Cap rights are just a set of access rights\<close>
29type_synonym cap_rights = "rights set"
30
31text \<open>The set of all rights:\<close>
32definition
33  all_rights :: cap_rights
34where
35 "all_rights \<equiv> UNIV"
36
37end
38