From 89815424cfc74d26f2c403df6f947d6d6313efcf Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Wed, 16 Mar 2022 11:27:51 +1100
Subject: [PATCH] aarch64 aspec/haskell: sync attribs_from_word

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 spec/abstract/AARCH64/ArchDecode_A.thy         | 5 ++---
 spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/spec/abstract/AARCH64/ArchDecode_A.thy b/spec/abstract/AARCH64/ArchDecode_A.thy
index 4b100b9af..b57133d7c 100644
--- a/spec/abstract/AARCH64/ArchDecode_A.thy
+++ b/spec/abstract/AARCH64/ArchDecode_A.thy
@@ -61,9 +61,8 @@ definition arch_decode_irq_control_invocation ::
       else throwError TruncatedMessage
     else throwError IllegalOperation)"
 
-definition attribs_from_word :: "machine_word \<Rightarrow> vm_attributes"
-  where
-  "attribs_from_word w \<equiv> if \<not> w!!0 then {Execute} else {}"
+definition attribs_from_word :: "machine_word \<Rightarrow> vm_attributes" where
+  "attribs_from_word w \<equiv> {attr.  \<not>w!!0 \<and> attr = Execute \<or> \<not>w !! 2 \<and> attr = Device}"
 
 (* FIXME AARCH64: only half updated *)
 definition make_user_pte :: "paddr \<Rightarrow> vm_attributes \<Rightarrow> vm_rights \<Rightarrow> pte" where
diff --git a/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs b/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
index cb7986ce4..5a3a68469 100644
--- a/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
+++ b/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
@@ -511,7 +511,7 @@ makeUserPTE baseAddr rights attrs vmSize =
         pteSmallPage = vmSize == ARMSmallPage,
         pteGlobal = False,
         pteExecuteNever = armExecuteNever attrs,
-        pteDevice = armPageCacheable attrs,
+        pteDevice = not (armPageCacheable attrs),
         pteRights = rights }
 
 checkVPAlignment :: VMPageSize -> VPtr -> KernelF SyscallError ()