From 3a2bfe5a9372fc155253ddf8ba80478b51f87932 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Date: Sat, 11 Apr 2020 01:55:29 +1000
Subject: [PATCH] riscv crefine: sync frame PTE rights with C updates

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
---
 proof/crefine/RISCV64/StateRelation_C.thy | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/proof/crefine/RISCV64/StateRelation_C.thy b/proof/crefine/RISCV64/StateRelation_C.thy
index 6b3a7b21d..5c2ad4add 100644
--- a/proof/crefine/RISCV64/StateRelation_C.thy
+++ b/proof/crefine/RISCV64/StateRelation_C.thy
@@ -392,7 +392,13 @@ definition
 
 definition
   "writable_from_vm_rights R \<equiv> case R of
-    VMReadOnly \<Rightarrow> 0
+    VMReadWrite \<Rightarrow> 1
+  | _ \<Rightarrow> 0"
+
+(* kernel-only conveys no  *)
+definition
+  "readable_from_vm_rights R \<equiv> case R of
+    VMKernelOnly \<Rightarrow> 0
   | _ \<Rightarrow> 1"
 
 (* if RWX are all 0, then the pte is a pointer to the next level page table *)
@@ -421,10 +427,10 @@ where
         pte_CL.dirty_CL = 1,
         pte_CL.accessed_CL = 1,
         pte_CL.global_CL = of_bool global,
-        pte_CL.user_CL = user_from_vm_rights rights, \<comment> \<open>FIXME RISCV user seems redundant for page ptes\<close>
+        pte_CL.user_CL = user_from_vm_rights rights,
         pte_CL.execute_CL = of_bool execute,
         pte_CL.write_CL = writable_from_vm_rights rights,
-        pte_CL.read_CL = undefined,
+        pte_CL.read_CL = readable_from_vm_rights rights,
         pte_CL.valid_CL = 1 \<rparr>
   | PageTablePTE ppn global user \<Rightarrow>
       cpte' =  \<lparr>