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