1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7chapter "Virtual-Memory Rights"
8
9theory VMRights_A
10imports CapRights_A
11begin
12
13text \<open>
14This theory provides architecture-specific definitions and datatypes for virtual-memory support.
15\<close>
16
17text \<open>Page access rights.\<close>
18
19type_synonym vm_rights = cap_rights
20
21definition vm_kernel_only :: vm_rights
22where
23  "vm_kernel_only \<equiv> {}"
24
25definition vm_read_only :: vm_rights
26where
27  "vm_read_only \<equiv> {AllowRead}"
28
29definition vm_read_write :: vm_rights
30where
31  "vm_read_write \<equiv> {AllowRead,AllowWrite}"
32
33text \<open>
34  Note that only the above combinations of virtual-memory rights are permitted.
35  We introduce the following definitions to reflect this fact:
36  The predicate @{text valid_vm_rights} holds iff a given set of rights is valid
37  (i.e., a permitted combination).
38  The function @{text validate_vm_rights} takes an arbitrary set of rights and
39  returns the largest permitted subset.
40\<close>
41definition valid_vm_rights :: "vm_rights set"
42where
43  "valid_vm_rights \<equiv> {vm_read_write, vm_read_only, vm_kernel_only}"
44
45definition validate_vm_rights :: "vm_rights \<Rightarrow> vm_rights"
46where
47  "validate_vm_rights rs \<equiv>
48     if AllowRead \<in> rs
49     then if AllowWrite \<in> rs then vm_read_write else vm_read_only
50     else vm_kernel_only"
51
52text \<open>On the abstract level, capability and VM rights share the same type.
53  Nevertheless, a simple set intersection might lead to an invalid value like
54  @{term "{AllowWrite}"}.  Hence, @{const validate_vm_rights}.\<close>
55definition mask_vm_rights :: "vm_rights \<Rightarrow> cap_rights \<Rightarrow> vm_rights"
56where
57  "mask_vm_rights V R \<equiv> validate_vm_rights (V \<inter> R)"
58
59end
60