Update haskell for proving WCET annotations.

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"
 

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

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)"
 

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

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,

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/