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