From b7bb3666f48bdd855140ea55878ebf8c81eba309 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Date: Mon, 13 Jul 2015 16:17:33 +1000
Subject: [PATCH] Update haskell for proving WCET annotations.

---
 spec/design/ArchVSpaceDecls_H.thy | 3 +++
 spec/design/ArchVSpace_H.thy      | 6 ++++++
 spec/design/TCB_H.thy             | 3 +++
 spec/design/skel/ArchVSpace_H.thy | 5 ++++-
 spec/design/skel/KernelInit_H.thy | 1 +
 spec/design/version               | 7 +++++--
 6 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/spec/design/ArchVSpaceDecls_H.thy b/spec/design/ArchVSpaceDecls_H.thy
index 86a344f0a..665b0638a 100644
--- a/spec/design/ArchVSpaceDecls_H.thy
+++ b/spec/design/ArchVSpaceDecls_H.thy
@@ -224,6 +224,9 @@ decodeARMPageFlush :: "machine_word \<Rightarrow> machine_word list \<Rightarrow
 consts
 checkVPAlignment :: "vmpage_size \<Rightarrow> vptr \<Rightarrow> ( syscall_error , unit ) kernel_f"
 
+consts
+validMappingSize :: "vmpage_size \<Rightarrow> kernel_state \<Rightarrow> bool"
+
 consts
 performARMMMUInvocation :: "ArchRetypeDecls_H.invocation \<Rightarrow> machine_word list kernel_p"
 
diff --git a/spec/design/ArchVSpace_H.thy b/spec/design/ArchVSpace_H.thy
index 29c2fa9f8..7debb48b4 100644
--- a/spec/design/ArchVSpace_H.thy
+++ b/spec/design/ArchVSpace_H.thy
@@ -1040,6 +1040,9 @@ defs decodeARMMMUInvocation_def:
             (case frameInfo of
                   None \<Rightarrow>   returnOk $ InvokePageDirectory PageDirectoryNothing
                 | Some frameInfo \<Rightarrow>   (doE
+                    withoutFailure $ stateAssert
+                        (validMappingSize (fst frameInfo))
+                        [];
                     baseStart \<leftarrow> returnOk ( pageBase (VPtr start) (fst frameInfo));
                     baseEnd \<leftarrow> returnOk ( pageBase (VPtr end - 1) (fst frameInfo));
                     whenE (baseStart \<noteq> baseEnd) $
@@ -1436,4 +1439,7 @@ defs storePTE_def:
 od)"
 
 
+defs validMappingSize_def:
+  "validMappingSize sz s == (2 ^ pageBitsForSize sz <= gsMaxObjectSize s)"
+
 end
diff --git a/spec/design/TCB_H.thy b/spec/design/TCB_H.thy
index 5f1c91ac0..b17db64a0 100644
--- a/spec/design/TCB_H.thy
+++ b/spec/design/TCB_H.thy
@@ -454,6 +454,9 @@ od)"
 defs deleteCallerCap_def:
 "deleteCallerCap receiver\<equiv> (do
     callerSlot \<leftarrow> getThreadCallerSlot receiver;
+    callerCap \<leftarrow> getSlotCap callerSlot;
+    haskell_assert (isReplyCap callerCap \<or> callerCap = NullCap)
+        [];
     cteDeleteOne callerSlot
 od)"
 
diff --git a/spec/design/skel/ArchVSpace_H.thy b/spec/design/skel/ArchVSpace_H.thy
index cb3b90460..be0179a78 100644
--- a/spec/design/skel/ArchVSpace_H.thy
+++ b/spec/design/skel/ArchVSpace_H.thy
@@ -19,6 +19,9 @@ imports
   ArchVSpaceDecls_H
 begin
 
-#INCLUDE_HASKELL SEL4/Kernel/VSpace/ARM.lhs bodies_only ArchInv=ArchRetypeDecls_H NOT checkPDAt checkPTAt checkPDASIDMapMembership
+#INCLUDE_HASKELL SEL4/Kernel/VSpace/ARM.lhs bodies_only ArchInv=ArchRetypeDecls_H NOT checkPDAt checkPTAt checkPDASIDMapMembership validMappingSize
+
+defs validMappingSize_def:
+  "validMappingSize sz s == (2 ^ pageBitsForSize sz <= gsMaxObjectSize s)"
 
 end
diff --git a/spec/design/skel/KernelInit_H.thy b/spec/design/skel/KernelInit_H.thy
index 130e9707e..1a6233121 100644
--- a/spec/design/skel/KernelInit_H.thy
+++ b/spec/design/skel/KernelInit_H.thy
@@ -50,6 +50,7 @@ where
         ksPSpace= newPSpace,
         gsUserPages= (\<lambda>x. None),
         gsCNodes= (\<lambda>x. None),
+        gsMaxObjectSize = card (UNIV :: machine_word set),
         ksDomScheduleIdx = newKSDomScheduleIdx,
         ksDomSchedule = newKSDomSchedule,
         ksCurDomain = newKSCurDomain,
diff --git a/spec/design/version b/spec/design/version
index 18b8449b6..0ff7edf1d 100644
--- a/spec/design/version
+++ b/spec/design/version
@@ -1,5 +1,8 @@
-Built from git repo at /Users/kleing/verification/seL4/haskell by kleing
+Built from git repo at /home/tsewell/dev/verification/seL4/haskell by tsewell
 
 Generated from changeset:
-cf53dfa removed setCurrentASID
+99efd6e Assertions to lean on abstract refinement.
 
+
+Warning - uncomitted changes used:
+?? ../rbuild/