arch_split: checkpoint for namespacing haskell

lib/Qualify.thy

@@ -106,7 +106,7 @@ fun get_new_types old_thy types =
 
 fun add_qualified qual nm =
   let
-    val nm' = Long_Name.explode nm |> rev |> tl |> hd;
+    val nm' = Long_Name.explode nm |> tl |> hd;
   in if qual = nm' then cons nm else I end
   handle List.Empty => I
 
@@ -125,13 +125,16 @@ fun set_global_qualify (args : qualify_args) thy =
 
   in if #deep args then
   let
+    val lthy = Named_Target.begin (str, Position.none) thy';
 
     val facts = 
       Facts.fold_static (fn (nm, _) => add_qualified str nm) (Global_Theory.facts_of thy) []
       |> map (`make_bind_local)
 
+    val const_space = #const_space (Consts.dest (Proof_Context.consts_of lthy));
+
     val consts = fold (fn (nm, _) => add_qualified str nm) (#constants (Consts.dest (Sign.consts_of thy))) []
-      |> map (`make_bind_local)                                                
+      |> map (`(make_bind const_space thy'))                                                
 
     val types = 
       Name_Space.fold_table (fn (nm, _) => add_qualified str nm) (#types (Type.rep_tsig (Sign.tsig_of thy))) []

spec/design/ARM/ArchInterruptDecls_H.thy

@@ -12,14 +12,15 @@ theory ArchInterruptDecls_H
 imports "../RetypeDecls_H" "../CNode_H" 
 begin
 
+qualify ARM
+
 consts
 decodeIRQControlInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> machine_word \<Rightarrow> capability list \<Rightarrow> ( syscall_error , ArchRetypeDecls_H.irqcontrol_invocation ) kernel_f"
 
 consts
 performIRQControl :: "ArchRetypeDecls_H.irqcontrol_invocation \<Rightarrow> unit kernel_p"
 
-consts
-checkIRQ :: "machine_word \<Rightarrow> ( syscall_error , unit ) kernel_f"
 
+end_qualify
 
 end

spec/design/ARM/ArchInterrupt_H.thy

@@ -12,14 +12,15 @@ theory ArchInterrupt_H
 imports "../RetypeDecls_H" "../CNode_H" "../InterruptDecls_H" ArchInterruptDecls_H
 begin
 
+qualify ARM
+
 defs decodeIRQControlInvocation_def:
 "decodeIRQControlInvocation arg1 arg2 arg3 arg4 \<equiv> throw IllegalOperation"
 
 defs performIRQControl_def:
 "performIRQControl arg1 \<equiv> haskell_fail []"
 
-defs checkIRQ_def:
-"checkIRQ irq\<equiv> rangeCheck irq (fromEnum minIRQ) (fromEnum maxIRQ)"
 
+end_qualify
 
 end

spec/design/ARM/ArchObjInsts_H.thy

@@ -20,6 +20,7 @@ imports
   "../PSpaceStorable_H"
   "../ObjectInstances_H"
 begin
+qualify ARM
 
 instantiation pde :: pre_storable
 begin
@@ -181,4 +182,5 @@ instance
 
 end
 
+end_qualify
 end

spec/design/ARM/ArchRetypeDecls_H.thy

@@ -19,6 +19,7 @@ imports
   "../PSpaceFuns_H"
   ArchObjInsts_H
 begin
+qualify ARM
 
 datatype page_table_invocation =
     PageTableUnmap arch_capability machine_word
@@ -659,4 +660,5 @@ consts
 capUntypedSize :: "arch_capability \<Rightarrow> machine_word"
 
 
+end_qualify
 end

spec/design/ARM/ArchRetype_H.thy

@@ -17,6 +17,7 @@ imports
   Hardware_H
   "../KI_Decls_H"
 begin
+qualify ARM
 
 defs deriveCap_def:
 "deriveCap x0 x1\<equiv> (let c = x1 in
@@ -294,4 +295,5 @@ defs capUntypedSize_def:
   )"
 
 
+end_qualify
 end

spec/design/ARM/ArchStateData_H.thy

@@ -20,6 +20,7 @@ imports
   ArchTypes_H
   ArchStructures_H
 begin
+qualify ARM
 
 datatype kernel_state =
     ARMKernelState machine_word "asid \<Rightarrow> ((machine_word) option)" "hardware_asid \<Rightarrow> (asid option)" hardware_asid "asid \<Rightarrow> ((hardware_asid * machine_word) option)" machine_word "machine_word list" "machine_word \<Rightarrow> arm_vspace_region_use"
@@ -396,4 +397,5 @@ where
                                    (state, frames)"
 
 
+end_qualify
 end

spec/design/ARM/ArchStructures_H.thy

@@ -14,6 +14,7 @@ imports
   "../Types_H"
   Hardware_H
 begin
+qualify ARM
 
 type_synonym asid = "word32"
 
@@ -245,4 +246,5 @@ where
 | "archTypeOf (KOPTE e) = PTET"
 | "archTypeOf (KOASIDPool e) = ASIDPoolT"
 
+end_qualify
 end

spec/design/ARM/ArchTCB_H.thy

@@ -11,6 +11,7 @@
 theory ArchTCB_H
 imports "../TCBDecls_H"
 begin
+qualify ARM
 
 definition
 decodeTransfer :: "word8 \<Rightarrow> ( syscall_error , copy_register_sets ) kernel_f"
@@ -23,4 +24,5 @@ where
 "performTransfer arg1 arg2 arg3 \<equiv> return ()"
 
 
+end_qualify
 end

spec/design/ARM/ArchThreadDecls_H.thy

@@ -20,6 +20,7 @@ imports
   "../FaultMonad_H"
   "../KernelInitMonad_H"
 begin
+qualify ARM
 
 consts
 switchToThread :: "machine_word \<Rightarrow> unit kernel"
@@ -34,4 +35,5 @@ consts
 activateIdleThread :: "machine_word \<Rightarrow> unit kernel"
 
 
+end_qualify
 end

spec/design/ARM/ArchThread_H.thy

@@ -16,6 +16,7 @@ imports
   "../TCBDecls_H"
   ArchVSpaceDecls_H
 begin
+qualify ARM
 
 defs switchToThread_def:
 "switchToThread tcb\<equiv> (do
@@ -44,5 +45,5 @@ defs activateIdleThread_def:
 "activateIdleThread arg1 \<equiv> return ()"
 
 
-
+end_qualify
 end

spec/design/ARM/ArchTypes_H.thy

@@ -19,33 +19,72 @@ imports
   State_H
   Hardware_H
   "../../../lib/Lib"
+  keywords "instantiation'" :: thy_decl
 begin
 
-datatype apiobject_type =
+ML
-    Untyped
+  \<open>val _ =
-  | TCBObject
+  Outer_Syntax.command @{command_keyword instantiation2'} "instantiate and prove type arity"
-  | EndpointObject
+   (Parse.opt_target -- Parse.multi_arity --| Parse.begin
-  | NotificationObject
+     >> (fn (opt_target, arities) => 
-  | CapTableObject
+          Toplevel.local_theory NONE opt_target (fn lthy =>
+            let
+              val thy = Proof_Context.theory_of lthy;
+              val lthy' = Class.instantiation_cmd arities thy;
+            in
+              lthy'
+            end)));
+\<close>
+
+ML \<open>
+val _ =
+  Outer_Syntax.command @{command_keyword instantiation'} "instantiate and prove type arity"
+   (Parse.opt_target -- Parse.multi_arity --| Parse.begin
+     >> (fn (opt_target, arities) => 
+            Toplevel.generic_theory (
+              (fn (Context.Theory thy) =>
+                    let
+                      val lthy = Class.instantiation_cmd arities thy;
+                      val gthy = Context.Proof lthy;
+                      val _ =
+                        (case Local_Theory.pretty lthy of
+                          [] => ()
+                        | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
+                    in gthy end
+              | (Context.Proof lthy) =>
+                     let
+                       val thy = Proof_Context.theory_of lthy;
+                       val lthy' = Class.instantiation_cmd arities thy;
+                       val gthy = Context.Proof lthy';
+                       val _ =
+                        (case Local_Theory.pretty lthy' of
+                          [] => ()
+                        | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
+                      in gthy end))));
+\<close>
+
+ML \<open>Local_Theory.init\<close>
+context ARM begin
+
+datatype apiobject_type = Foo
+
 (* apiobject_type instance proofs *)
 (*<*)
-instantiation apiobject_type :: enum begin
+instantiation' ARM.apiobject_type :: enum begin
+interpretation ARM .
+
 definition
   enum_apiobject_type: "enum_class.enum \<equiv> 
     [ 
-      Untyped,
+      Foo
-      TCBObject,
-      EndpointObject,
-      NotificationObject,
-      CapTableObject
     ]"
 
 
 definition
-  "enum_class.enum_all (P :: apiobject_type \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
+  "enum_class.enum_all (P :: ARM.apiobject_type \<Rightarrow> bool) \<longleftrightarrow> Ball UNIV P"
 
 definition
-  "enum_class.enum_ex (P :: apiobject_type \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
+  "enum_class.enum_ex (P :: ARM.apiobject_type \<Rightarrow> bool) \<longleftrightarrow> Bex UNIV P"
 
   instance
   apply intro_classes
@@ -71,37 +110,9 @@ end
 (*>*)
 
 
-definition
+end
-tcbBlockSizeBits :: "nat"
-where
-"tcbBlockSizeBits \<equiv> 9"
-
-definition
-epSizeBits :: "nat"
-where
-"epSizeBits \<equiv> 4"
-
-definition
-ntfnSizeBits :: "nat"
-where
-"ntfnSizeBits \<equiv> 4"
-
-definition
-cteSizeBits :: "nat"
-where
-"cteSizeBits \<equiv> 4"
-
-definition
-apiGetObjectSize :: "apiobject_type \<Rightarrow> nat \<Rightarrow> nat"
-where
-"apiGetObjectSize x0 magnitude\<equiv> (case x0 of
-    Untyped \<Rightarrow>    magnitude
-  | TCBObject \<Rightarrow>    tcbBlockSizeBits
-  | EndpointObject \<Rightarrow>    epSizeBits
-  | NotificationObject \<Rightarrow>    ntfnSizeBits
-  | CapTableObject \<Rightarrow>    cteSizeBits + magnitude
-  )"
 
+qualify ARM
 
 datatype object_type =
     APIObjectType apiobject_type
@@ -138,11 +149,14 @@ where
   )"
 
 
+end_qualify
 
 text {* object\_type instance proofs *}
 
 instantiation object_type :: enum
 begin
+interpretation ARM .
+
 definition
   enum_object_type: "enum_class.enum \<equiv> 
     map APIObjectType (enum_class.enum :: apiobject_type list) @ 
@@ -184,4 +198,5 @@ begin
 instance by (intro_classes, simp add: enum_alt_object_type)
 end
 
+end_qualify
 end

spec/design/ARM/ArchVSpaceDecls_H.thy

@@ -13,6 +13,10 @@ chapter "Retyping Objects"
 theory ArchVSpaceDecls_H
 imports ArchRetypeDecls_H "../InvocationLabels_H"
 begin
+qualify ARM
+
+consts
+kernelBase :: "vptr"
 
 consts
 globalsBase :: "vptr"
@@ -63,10 +67,7 @@ consts
 createITFrameCap :: "machine_word \<Rightarrow> vptr \<Rightarrow> asid option \<Rightarrow> bool \<Rightarrow> capability kernel_init"
 
 consts
-vptrFromPPtr :: "machine_word \<Rightarrow> vptr kernel_init"
+createFramesOfRegion :: "capability \<Rightarrow> region \<Rightarrow> bool \<Rightarrow> vptr \<Rightarrow> unit kernel_init"
-
-consts
-createFramesOfRegion :: "capability \<Rightarrow> region \<Rightarrow> bool \<Rightarrow> unit kernel_init"
 
 consts
 mapGlobalsFrame :: "unit kernel"
@@ -258,4 +259,5 @@ consts
 storePTE :: "machine_word \<Rightarrow> pte \<Rightarrow> unit kernel"
 
 
+end_qualify
 end

spec/design/ARM/ArchVSpace_H.thy

@@ -22,6 +22,9 @@ begin
 defs vptrFromPPtr_def:
 "vptrFromPPtr ptr \<equiv> returnOk $ ptr + 0x20000000"
 
+defs kernelBase_def:
+"kernelBase \<equiv> VPtr 0xf0000000"
+
 defs globalsBase_def:
 "globalsBase \<equiv> VPtr 0xffffc000"
 
@@ -31,24 +34,26 @@ defs idleThreadStart_def:
 defs idleThreadCode_def:
 "idleThreadCode \<equiv>
     [ 0xe3a00000
+    , 0xee070f9a
+    , 0xee070f90
     , 0xeafffffc
     ]"
 
 defs mapKernelWindow_def:
 "mapKernelWindow\<equiv> (do
-    baseoffset \<leftarrow> return ( kernelBase `~shiftR~` pageBitsForSize (ARMSection));
+    vbase \<leftarrow> return ( kernelBase `~shiftR~` pageBitsForSize (ARMSection));
     pdeBits \<leftarrow> return ( objBits (undefined ::pde));
     pteBits \<leftarrow> return ( objBits (undefined ::pte));
     ptSize \<leftarrow> return ( ptBits - pteBits);
     pdSize \<leftarrow> return ( pdBits - pdeBits);
     globalPD \<leftarrow> gets $ armKSGlobalPD \<circ> ksArchState;
     globalPTs \<leftarrow> gets $ armKSGlobalPTs \<circ> ksArchState;
-    startentry \<leftarrow> return $ (PPtr (fromPPtr globalPD ));
+    deleteObjects (PPtr $ fromPPtr globalPD) pdBits;
-    deleteObjects (startentry) pdBits;
+    placeNewObject (PPtr $ fromPPtr globalPD) (makeObject ::pde) pdSize;
-    placeNewObject (startentry) (makeObject ::pde) pdSize;
+    forM_x [vbase, vbase+16  .e.  (bit pdSize) - 16 - 1] $ createSectionPDE;
-    forM_x [baseoffset, baseoffset+16  .e.  (bit pdSize) - 16 - 1] $ createSectionPDE;
+    forM_x [(bit pdSize) - 16, (bit pdSize) - 2] (\<lambda> v. (do
-    forM_x [(bit pdSize) - 16, (bit pdSize) - 2] (\<lambda> offset. (do
+          offset \<leftarrow> return ( fromVPtr v);
-          virt \<leftarrow> return ( offset `~shiftL~` pageBitsForSize (ARMSection));
+          virt \<leftarrow> return ( v `~shiftL~` pageBitsForSize (ARMSection));
           phys \<leftarrow> return ( addrFromPPtr $ PPtr $ fromVPtr virt);
           pde \<leftarrow> return ( SectionPDE_ \<lparr>
                   pdeFrame= phys,
@@ -58,7 +63,7 @@ defs mapKernelWindow_def:
                   pdeGlobal= True,
                   pdeExecuteNever= False,
                   pdeRights= VMKernelOnly \<rparr>);
-          slot \<leftarrow> return ( globalPD + PPtr ((fromVPtr offset) `~shiftL~` pdeBits));
+          slot \<leftarrow> return ( globalPD + PPtr (offset `~shiftL~` pdeBits));
           storePDE slot pde
     od));
     paddr \<leftarrow> return ( addrFromPPtr $ PPtr $ fromPPtr $ head globalPTs);
@@ -73,13 +78,14 @@ defs mapKernelWindow_def:
 od)"
 
 defs createSectionPDE_def:
-"createSectionPDE offset\<equiv> (do
+"createSectionPDE v\<equiv> (do
+    vbase \<leftarrow> return ( kernelBase `~shiftR~` pageBitsForSize (ARMSection));
     pdeBits \<leftarrow> return ( objBits (undefined ::pde));
     pteBits \<leftarrow> return ( objBits (undefined ::pte));
     globalPD \<leftarrow> gets $ armKSGlobalPD \<circ> ksArchState;
-    virt \<leftarrow> return ( fromVPtr $ offset `~shiftL~` pageBitsForSize (ARMSection));
+    offset \<leftarrow> return ( fromVPtr v);
-    phys \<leftarrow> return ( addrFromPPtr $ PPtr virt);
+    virt \<leftarrow> return ( (v - vbase) `~shiftL~` (pageBitsForSize (ARMSuperSection) - 4));
-    base \<leftarrow> return ( fromVPtr offset);
+    phys \<leftarrow> return ( addrFromPPtr $ PPtr $ fromVPtr virt);
     pde \<leftarrow> return ( SuperSectionPDE_ \<lparr>
             pdeFrame= phys,
             pdeParity= True,
@@ -88,7 +94,7 @@ defs createSectionPDE_def:
             pdeExecuteNever= False,
             pdeRights= VMKernelOnly \<rparr>);
     slots \<leftarrow> return ( map (\<lambda> n. globalPD + PPtr (n `~shiftL~` pdeBits))
-            [base  .e.  base + 15]);
+            [offset  .e.  offset + 15]);
     (flip $ mapM_x ) slots (\<lambda> slot.  storePDE slot pde)
 od)"
 
@@ -129,7 +135,7 @@ defs createITPDPTs_def:
     odE));
     slotAfter \<leftarrow> noInitFailure $ gets initSlotPosCur;
     bootInfo \<leftarrow> noInitFailure $ gets initBootInfo;
-    bootInfo' \<leftarrow> returnOk ( bootInfo \<lparr>bifUIPDCaps := [slotBefore - 1  .e.  slotBefore - 1], bifUIPTCaps := [slotBefore  .e.  slotAfter - 1] \<rparr>);
+    bootInfo' \<leftarrow> returnOk ( bootInfo \<lparr> bifUIPTCaps := [slotBefore  .e.  slotAfter - 1] \<rparr>);
     noInitFailure $ modify (\<lambda> s. s \<lparr> initBootInfo := bootInfo' \<rparr>);
     returnOk pdCap
 odE)"
@@ -302,13 +308,13 @@ defs createITFrameCap_def:
 odE)"
 
 defs createFramesOfRegion_def:
-"createFramesOfRegion rootCNCap region doMap\<equiv> (doE
+"createFramesOfRegion rootCNCap region doMap pvOffset\<equiv> (doE
     curSlotPos \<leftarrow> noInitFailure $ gets initSlotPosCur;
     (startPPtr, endPPtr) \<leftarrow> returnOk $ fromRegion region;
     forME_x [startPPtr,startPPtr + (bit pageBits)  .e.  endPPtr] (\<lambda> ptr. (doE
-        vptr \<leftarrow> vptrFromPPtr $ ptr;
+        paddr \<leftarrow> returnOk ( fromPAddr $ addrFromPPtr ptr);
         frameCap \<leftarrow> if doMap then
-                    createITFrameCap ptr vptr (Just itASID) False
+                    createITFrameCap ptr ((VPtr paddr) + pvOffset ) (Just itASID) False
                     else createITFrameCap ptr 0 Nothing False;
         provideCap rootCNCap frameCap
     odE));
@@ -1101,7 +1107,6 @@ defs decodeARMMMUInvocation_def:
         )
   else if isPageCap cap
   then  
- (
     (case (invocationType label, args, extraCaps) of
           (ArchInvocationLabel ARMPageMap, vaddr#rightsMask#attr#_, (pdCap,_)#_) \<Rightarrow>   (doE
             whenE (isJust $ capVPMappedAddress cap) $
@@ -1162,7 +1167,6 @@ defs decodeARMMMUInvocation_def:
         | (ArchInvocationLabel ARMPageGetAddress, _, _) \<Rightarrow>   returnOk $ InvokePage $ PageGetAddr (capVPBasePtr cap)
         | _ \<Rightarrow>   throw IllegalOperation
         )
- )
   else if isASIDControlCap cap
   then  
     (case (invocationType label, args, extraCaps) of

spec/design/ARM/Arch_Structs_B.thy

@@ -13,8 +13,9 @@
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports "~~/src/HOL/Main"
+imports "~~/src/HOL/Main" "../../../spec/machine/$L4V_ARCH/Setup_Locale"
 begin
+qualify ARM
 
 datatype arm_vspace_region_use =
     ArmVSpaceUserRegion
@@ -23,4 +24,5 @@ datatype arm_vspace_region_use =
   | ArmVSpaceDeviceWindow
 
 
+end_qualify
 end

spec/design/ARM/Hardware_H.thy

@@ -13,10 +13,11 @@ imports
   "../../machine/ARM/MachineOps"
   State_H
 begin
+context ARM begin
 
-type_synonym irq = "Platform.irq"
+type_synonym irq = "Platform.ARM.irq"
 
-type_synonym paddr = "Platform.paddr"
+type_synonym paddr = "Platform.ARM.paddr"
 
 datatype vmrights =
     VMNoAccess
@@ -342,12 +343,17 @@ lemma armPageCacheable_armPageCacheable_update [simp]:
 definition
 fromPAddr :: "paddr \<Rightarrow> machine_word"
 where
-"fromPAddr \<equiv> Platform.fromPAddr"
+"fromPAddr \<equiv> Platform.ARM.fromPAddr"
 
 definition
 pageColourBits :: "nat"
 where
-"pageColourBits \<equiv> Platform.pageColourBits"
+"pageColourBits \<equiv> Platform.ARM.pageColourBits"
+
+definition
+setInterruptMode :: "irq \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> unit machine_monad"
+where
+"setInterruptMode arg1 arg2 arg3 \<equiv> return ()"
 
 definition
 clearExMonitor :: "unit machine_monad"
@@ -364,16 +370,13 @@ ptBits :: "nat"
 where
 "ptBits \<equiv> pageBits - 2"
 
-definition
-physBase :: "paddr"
-where
-"physBase \<equiv> toPAddr Platform.physBase"
 
-definition
+end
-kernelBase :: "vptr"
-where
-"kernelBase \<equiv> Platform.kernelBase"
 
+qualify ARM (deep)
+
+declare ARM.vmrights.exhaust[cases type: ARM.vmrights]
+ Hardware_H.ARM.vmrights.simps[simp]
 
 (* vmrights instance proofs *)
 (*<*)
@@ -418,6 +421,13 @@ end
 (*>*)
 
 
+end_qualify
+
+declare ARM.vmrights.exhaust[cases del]
+ Hardware_H.ARM.vmrights.simps[simp del]
+
+context ARM begin
+
 definition
 wordFromPDE :: "pde \<Rightarrow> machine_word"
 where
@@ -466,3 +476,4 @@ where
 
 
 end
+end

spec/design/ARM/RegisterSet_H.thy

@@ -15,6 +15,7 @@ imports
   "../../../lib/HaskellLib_H"
   "../../machine/ARM/MachineTypes"
 begin
+context ARM begin
 
 definition
   newContext :: "register => machine_word"
@@ -22,3 +23,4 @@ where
  "newContext \<equiv> (K 0) aLU initContext"
 
 end
+end

spec/design/ARM/State_H.thy

@@ -20,6 +20,7 @@ imports
   RegisterSet_H
   "../../machine/ARM/MachineOps"
 begin
+qualify ARM (deep)
 
 definition
   Word :: "machine_word \<Rightarrow> machine_word"
@@ -122,5 +123,5 @@ definition
 where
  "nullPointer \<equiv> 0"
 
-
+end_qualify
 end

spec/design/Delete_H.thy

@@ -251,7 +251,7 @@ od))
         state \<leftarrow> getThreadState tptr;
         (case state of
               BlockedOnSend _ _ _ _ \<Rightarrow>   blockedIPCCancel state
-            | BlockedOnReceive _ \<Rightarrow>   blockedIPCCancel state
+            | BlockedOnReceive _ _ \<Rightarrow>   blockedIPCCancel state
             | BlockedOnNotification _ \<Rightarrow>   cancelSignal tptr (waitingOnNotification state)
             | BlockedOnReply  \<Rightarrow>   replyIPCCancel
             | _ \<Rightarrow>   return ()

spec/design/Endpoint_H.thy

@@ -50,12 +50,13 @@ defs sendIPC_def:
                 recvState \<leftarrow> getThreadState dest;
                 haskell_assert (isReceive recvState)
                        [];
+                diminish \<leftarrow> return ( blockingIPCDiminishCaps recvState);
                 doIPCTransfer thread (Just epptr) badge canGrant
-                    dest;
+                    dest diminish;
                 setThreadState Running dest;
                 attemptSwitchTo dest;
                 fault \<leftarrow> threadGet tcbFault thread;
-                (case (call, fault, canGrant) of
+                (case (call, fault, canGrant \<and> Not diminish) of
                       (False, None, _) \<Rightarrow>   return ()
                     | (_, _, True) \<Rightarrow>   setupCallerCap thread dest
                     | _ \<Rightarrow>   setThreadState Inactive thread
@@ -78,6 +79,7 @@ defs receiveIPC_def:
   then   (do
         epptr \<leftarrow> return ( capEPPtr cap);
         ep \<leftarrow> getEndpoint epptr;
+        diminish \<leftarrow> return ( Not $ capEPCanSend cap);
         ntfnPtr \<leftarrow> getBoundNotification thread;
         ntfn \<leftarrow> maybe (return $ NTFN IdleNtfn Nothing) (getNotification) ntfnPtr;
         if (isJust ntfnPtr \<and> isActive ntfn)
@@ -86,7 +88,8 @@ defs receiveIPC_def:
               IdleEP \<Rightarrow>   (case isBlocking of
                 True \<Rightarrow>   (do
                   setThreadState (BlockedOnReceive_ \<lparr>
-                      blockingObject= epptr \<rparr>) thread;
+                      blockingObject= epptr,
+                      blockingIPCDiminishCaps= diminish \<rparr>) thread;
                   setEndpoint epptr $ RecvEP [thread]
                 od)
               | False \<Rightarrow>   doNBRecvFailedTransfer thread
@@ -94,7 +97,8 @@ defs receiveIPC_def:
             | RecvEP queue \<Rightarrow>   (case isBlocking of
                 True \<Rightarrow>   (do
                   setThreadState (BlockedOnReceive_ \<lparr>
-                      blockingObject= epptr \<rparr>) thread;
+                      blockingObject= epptr,
+                      blockingIPCDiminishCaps= diminish \<rparr>) thread;
                   setEndpoint epptr $ RecvEP $ queue @ [thread]
                 od)
               | False \<Rightarrow>   doNBRecvFailedTransfer thread
@@ -110,10 +114,10 @@ defs receiveIPC_def:
                 badge \<leftarrow> return ( blockingIPCBadge senderState);
                 canGrant \<leftarrow> return ( blockingIPCCanGrant senderState);
                 doIPCTransfer sender (Just epptr) badge canGrant
-                    thread;
+                    thread diminish;
                 call \<leftarrow> return ( blockingIPCIsCall senderState);
                 fault \<leftarrow> threadGet tcbFault sender;
-                (case (call, fault, canGrant) of
+                (case (call, fault, canGrant \<and> Not diminish) of
                       (False, None, _) \<Rightarrow>   (do
                         setThreadState Running sender;
                         switchIfRequiredTo sender
@@ -179,7 +183,7 @@ defs cancelIPC_def:
         state \<leftarrow> getThreadState tptr;
         (case state of
               BlockedOnSend _ _ _ _ \<Rightarrow>   blockedIPCCancel state
-            | BlockedOnReceive _ \<Rightarrow>   blockedIPCCancel state
+            | BlockedOnReceive _ _ \<Rightarrow>   blockedIPCCancel state
             | BlockedOnNotification _ \<Rightarrow>   cancelSignal tptr (waitingOnNotification state)
             | BlockedOnReply  \<Rightarrow>   replyIPCCancel
             | _ \<Rightarrow>   return ()

spec/design/Event_H.thy

@@ -21,12 +21,12 @@ text {*
 *}
 
 datatype syscall =
-    SysCall
+    SysSend
-  | SysReplyRecv
-  | SysSend
   | SysNBSend
+  | SysCall
   | SysRecv
   | SysReply
+  | SysReplyRecv
   | SysYield
   | SysNBRecv
 

spec/design/Fault_H.thy

@@ -262,7 +262,7 @@ where
   | _ \<Rightarrow> False"
 
 datatype init_failure =
-    IFailure
+    InitFailure
 
 datatype syscall_error =
     IllegalOperation

spec/design/InterruptDecls_H.thy

@@ -23,7 +23,7 @@ consts
 performIRQControl :: "irqcontrol_invocation \<Rightarrow> unit kernel_p"
 
 consts
-decodeIRQHandlerInvocation :: "machine_word \<Rightarrow> irq \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , irqhandler_invocation ) kernel_f"
+decodeIRQHandlerInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> irq \<Rightarrow> (capability * machine_word) list \<Rightarrow> ( syscall_error , irqhandler_invocation ) kernel_f"
 
 consts
 toBool :: "machine_word \<Rightarrow> bool"

spec/design/Interrupt_H.thy

@@ -38,8 +38,8 @@ defs decodeIRQControlInvocation_def:
 "decodeIRQControlInvocation label args srcSlot extraCaps \<equiv>
     (case (invocationType label, args, extraCaps) of
           (IRQIssueIRQHandler, irqW#index#depth#_, cnode#_) \<Rightarrow>   (doE
-            ArchInterruptDecls_H.checkIRQ (irqW && mask 16);
+            rangeCheck irqW (fromEnum minIRQ) (fromEnum maxIRQ);
-            irq \<leftarrow> returnOk ( toEnum (fromIntegral (irqW && mask 16)) ::irq);
+            irq \<leftarrow> returnOk ( toEnum (fromIntegral irqW) ::irq);
             irqActive \<leftarrow> withoutFailure $ isIRQActive irq;
             whenE irqActive $ throw RevokeFirst;
             destSlot \<leftarrow> lookupTargetSlot cnode
@@ -63,7 +63,7 @@ defs performIRQControl_def:
   )"
 
 defs decodeIRQHandlerInvocation_def:
-"decodeIRQHandlerInvocation label irq extraCaps \<equiv>
+"decodeIRQHandlerInvocation label args irq extraCaps \<equiv>
     (case (invocationType label,extraCaps) of
           (IRQAckIRQ,_) \<Rightarrow>   returnOk $ AckIRQ irq
         | (IRQSetIRQHandler,(cap,slot)#_) \<Rightarrow>   (case cap of
@@ -73,6 +73,10 @@ defs decodeIRQHandlerInvocation_def:
                 )
         | (IRQSetIRQHandler,_) \<Rightarrow>   throw TruncatedMessage
         | (IRQClearIRQHandler,_) \<Rightarrow>   returnOk $ ClearIRQHandler irq
+        | (IRQSetMode,_) \<Rightarrow>   (case args of
+                  trig#pol#_ \<Rightarrow>   returnOk $ SetMode irq (toBool trig) (toBool pol)
+                | _ \<Rightarrow>   throw TruncatedMessage
+                )
         | _ \<Rightarrow>   throw IllegalOperation
         )"
 
@@ -92,6 +96,8 @@ defs invokeIRQHandler_def:
     irqSlot \<leftarrow> getIRQSlot irq;
     cteDeleteOne irqSlot
   od)
+  | (SetMode irq trig pol) \<Rightarrow>   
+    doMachineOp $ setInterruptMode irq trig pol
   )"
 
 defs deletingIRQHandler_def:

spec/design/InvocationLabels_H.thy

@@ -48,6 +48,7 @@ datatype invocation_label =
   | IRQAckIRQ
   | IRQSetIRQHandler
   | IRQClearIRQHandler
+  | IRQSetMode
   | DomainSetSet
   | ArchInvocationLabel ArchInvocationLabels_H.ARM.arch_invocation_label
 
@@ -83,6 +84,7 @@ definition
       IRQAckIRQ,
       IRQSetIRQHandler,
       IRQClearIRQHandler,
+      IRQSetMode,
       DomainSetSet
     ]
     @ (map ArchInvocationLabel enum)"

spec/design/Invocations_H.thy

@@ -830,8 +830,19 @@ where
 datatype irqhandler_invocation =
     AckIRQ irq
   | ClearIRQHandler irq
+  | SetMode irq bool bool
   | SetIRQHandler irq capability machine_word
 
+primrec
+  modeIRQ :: "irqhandler_invocation \<Rightarrow> irq"
+where
+  "modeIRQ (SetMode v0 v1 v2) = v0"
+
+primrec
+  modeTrigger :: "irqhandler_invocation \<Rightarrow> bool"
+where
+  "modeTrigger (SetMode v0 v1 v2) = v1"
+
 primrec
   irqHandlerIRQ :: "irqhandler_invocation \<Rightarrow> irq"
 where
@@ -844,11 +855,26 @@ primrec
 where
   "setIRQHandlerCap (SetIRQHandler v0 v1 v2) = v1"
 
+primrec
+  modePolarity :: "irqhandler_invocation \<Rightarrow> bool"
+where
+  "modePolarity (SetMode v0 v1 v2) = v2"
+
 primrec
   setIRQHandlerSlot :: "irqhandler_invocation \<Rightarrow> machine_word"
 where
   "setIRQHandlerSlot (SetIRQHandler v0 v1 v2) = v2"
 
+primrec
+  modeIRQ_update :: "(irq \<Rightarrow> irq) \<Rightarrow> irqhandler_invocation \<Rightarrow> irqhandler_invocation"
+where
+  "modeIRQ_update f (SetMode v0 v1 v2) = SetMode (f v0) v1 v2"
+
+primrec
+  modeTrigger_update :: "(bool \<Rightarrow> bool) \<Rightarrow> irqhandler_invocation \<Rightarrow> irqhandler_invocation"
+where
+  "modeTrigger_update f (SetMode v0 v1 v2) = SetMode v0 (f v1) v2"
+
 primrec
   irqHandlerIRQ_update :: "(irq \<Rightarrow> irq) \<Rightarrow> irqhandler_invocation \<Rightarrow> irqhandler_invocation"
 where
@@ -861,6 +887,11 @@ primrec
 where
   "setIRQHandlerCap_update f (SetIRQHandler v0 v1 v2) = SetIRQHandler v0 (f v1) v2"
 
+primrec
+  modePolarity_update :: "(bool \<Rightarrow> bool) \<Rightarrow> irqhandler_invocation \<Rightarrow> irqhandler_invocation"
+where
+  "modePolarity_update f (SetMode v0 v1 v2) = SetMode v0 v1 (f v2)"
+
 primrec
   setIRQHandlerSlot_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> irqhandler_invocation \<Rightarrow> irqhandler_invocation"
 where
@@ -876,6 +907,11 @@ abbreviation (input)
 where
   "ClearIRQHandler_ \<lparr> irqHandlerIRQ= v0 \<rparr> == ClearIRQHandler v0"
 
+abbreviation (input)
+  SetMode_trans :: "(irq) \<Rightarrow> (bool) \<Rightarrow> (bool) \<Rightarrow> irqhandler_invocation" ("SetMode'_ \<lparr> modeIRQ= _, modeTrigger= _, modePolarity= _ \<rparr>")
+where
+  "SetMode_ \<lparr> modeIRQ= v0, modeTrigger= v1, modePolarity= v2 \<rparr> == SetMode v0 v1 v2"
+
 abbreviation (input)
   SetIRQHandler_trans :: "(irq) \<Rightarrow> (capability) \<Rightarrow> (machine_word) \<Rightarrow> irqhandler_invocation" ("SetIRQHandler'_ \<lparr> irqHandlerIRQ= _, setIRQHandlerCap= _, setIRQHandlerSlot= _ \<rparr>")
 where
@@ -895,6 +931,13 @@ where
     ClearIRQHandler v0 \<Rightarrow> True
   | _ \<Rightarrow> False"
 
+definition
+  isSetMode :: "irqhandler_invocation \<Rightarrow> bool"
+where
+ "isSetMode v \<equiv> case v of
+    SetMode v0 v1 v2 \<Rightarrow> True
+  | _ \<Rightarrow> False"
+
 definition
   isSetIRQHandler :: "irqhandler_invocation \<Rightarrow> bool"
 where

spec/design/KI_Decls_H.thy

@@ -35,7 +35,7 @@ consts
 allocRegion :: "nat \<Rightarrow> paddr kernel_init"
 
 consts
-initKernel :: "vptr \<Rightarrow> vptr \<Rightarrow> paddr list \<Rightarrow> paddr list \<Rightarrow> paddr list \<Rightarrow> unit kernel"
+initKernel :: "vptr \<Rightarrow> paddr list \<Rightarrow> vptr \<Rightarrow> paddr list \<Rightarrow> paddr list \<Rightarrow> unit kernel"
 
 consts
 finaliseBIFrame :: "unit kernel_init"

spec/design/KernelInit_H.thy

@@ -109,11 +109,14 @@ defs allocRegion_def:
                           odE)"
 
 defs initKernel_def:
-"initKernel entry initOffset initFrames kernelFrames bootFrames\<equiv> (do
+"initKernel entry initFrames initOffset kernelFrames bootFrames\<equiv> (do
         uiRegion \<leftarrow> return ( coverOf $ map (\<lambda> x. Region (ptrFromPAddr x, (ptrFromPAddr x) + bit (pageBits))) initFrames);
+        kernelRegion \<leftarrow> return ( coverOf $ map (\<lambda> x. Region (ptrFromPAddr x, (ptrFromPAddr x) + bit (pageBits))) kernelFrames);
         kePPtr \<leftarrow> return ( fst $ fromRegion $ uiRegion);
         kfEndPAddr \<leftarrow> return ( addrFromPPtr kePPtr);
         (startPPtr,endPPtr) \<leftarrow> return $ fromRegion uiRegion;
+        vptrStart \<leftarrow> return ( (VPtr (fromPAddr $ addrFromPPtr $ startPPtr )) + initOffset);
+        vptrEnd \<leftarrow> return ( (VPtr (fromPAddr $ addrFromPPtr $ endPPtr )) + initOffset);
         allMemory \<leftarrow> doMachineOp getMemoryRegions;
         initPSpace $ map (\<lambda> (s, e). (ptrFromPAddr s, ptrFromPAddr e))
                          allMemory;
@@ -121,9 +124,7 @@ defs initKernel_def:
         initKernelVM;
         initCPU;
         initPlatform;
-        runInit initOffset $ (doE
+        runInit $ (doE
-                vptrStart \<leftarrow> vptrFromPPtr startPPtr;
-                vptrEnd \<leftarrow> vptrFromPPtr endPPtr;
                 initFreemem kfEndPAddr uiRegion;
                 rootCNCap \<leftarrow> makeRootCNode;
                 initInterruptController rootCNCap biCapIRQControl;
@@ -131,7 +132,7 @@ defs initKernel_def:
                 ipcBufferCap \<leftarrow> createIPCBufferFrame rootCNCap ipcBufferVPtr;
                 biFrameVPtr \<leftarrow> returnOk ( vptrEnd + (1 `~shiftL~` pageBits));
                 createBIFrame rootCNCap biFrameVPtr 0 1;
-                createFramesOfRegion rootCNCap uiRegion True;
+                createFramesOfRegion rootCNCap uiRegion True initOffset;
                 itPDCap \<leftarrow> createITPDPTs rootCNCap vptrStart biFrameVPtr;
                 writeITPDPTs rootCNCap itPDCap;
                 itAPCap \<leftarrow> createITASIDPool rootCNCap;
@@ -158,7 +159,7 @@ defs createInitialThread_def:
       tcb' \<leftarrow> allocRegion tcbBits;
       tcbPPtr \<leftarrow> returnOk ( ptrFromPAddr tcb');
       doKernelOp $ (do
-         placeNewObject tcbPPtr initTCB 0;
+         placeNewObject tcbPPtr (makeObject::tcb) 0;
          srcSlot \<leftarrow> locateSlotCap rootCNCap biCapITCNode;
          destSlot \<leftarrow> getThreadCSpaceRoot tcbPPtr;
          cteInsert rootCNCap srcSlot destSlot;
@@ -209,7 +210,7 @@ defs createUntypedObject_def:
     freemem \<leftarrow> noInitFailure $ gets initFreeMemory;
     (flip mapME) (take maxNumFreememRegions freemem)
         (\<lambda> reg. (
-            (\<lambda> f. foldME f reg [4  .e.  (finiteBitSize (undefined::machine_word)) - 2])
+            (\<lambda> f. mapME (f reg) [4  .e.  wordBits - 2])
                 (\<lambda> reg bits. (doE
                     reg' \<leftarrow> (if Not (isAligned (regStartPAddr reg) (bits + 1))
                                 \<and> (regEndPAddr reg) - (regStartPAddr reg) \<ge> bit bits
@@ -260,7 +261,7 @@ defs provideCap_def:
 "provideCap rootCNodeCap cap\<equiv> (doE
     currSlot \<leftarrow> noInitFailure $ gets initSlotPosCur;
     maxSlot \<leftarrow> noInitFailure $ gets initSlotPosMax;
-    whenE (currSlot \<ge> maxSlot) $ throwError $ IFailure;
+    whenE (currSlot \<ge> maxSlot) $ throwError InitFailure;
     slot \<leftarrow> doKernelOp $ locateSlotCap rootCNodeCap currSlot;
     doKernelOp $ insertInitCap slot cap;
     noInitFailure $ modify (\<lambda> st. st \<lparr> initSlotPosCur := currSlot + 1 \<rparr>)

spec/design/Notification_H.thy

@@ -20,7 +20,7 @@ begin
 
 defs receiveBlocked_def:
 "receiveBlocked st\<equiv> (case st of
-      BlockedOnReceive v1 \<Rightarrow>   True
+      BlockedOnReceive v1 v2 \<Rightarrow>   True
     | _ \<Rightarrow>   False
     )"
 

spec/design/PSpaceFuns_H.thy

@@ -142,7 +142,9 @@ defs deleteObjects_def:
         doMachineOp $ freeMemory (PPtr (fromPPtr ptr)) bits;
         ps \<leftarrow> gets ksPSpace;
         inRange \<leftarrow> return ( (\<lambda> x. x && ((- mask bits) - 1) = fromPPtr ptr));
-        map' \<leftarrow> return ( deleteRange (psMap ps) (fromPPtr ptr) bits);
+        map' \<leftarrow> return ( data_map_filterWithKey
+                        (\<lambda> x _. Not (inRange x))
+                        (psMap ps));
         ps' \<leftarrow> return ( ps \<lparr> psMap := map' \<rparr>);
         modify (\<lambda> ks. ks \<lparr> ksPSpace := ps'\<rparr>);
         modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> x. if inRange x

spec/design/Retype_H.thy

@@ -376,7 +376,7 @@ defs decodeInvocation_def:
   then let irq = capIRQ cap
   in  
     liftME InvokeIRQHandler $
-        decodeIRQHandlerInvocation label irq extraCaps
+        decodeIRQHandlerInvocation label args irq extraCaps
   else if isArchObjectCap cap
   then let cap = capCap cap
   in  

spec/design/Structures_H.thy

@@ -736,7 +736,7 @@ lemma cteMDBNode_cteMDBNode_update [simp]:
   by (cases v) simp
 
 datatype thread_state =
-    BlockedOnReceive machine_word
+    BlockedOnReceive machine_word bool
   | BlockedOnReply
   | BlockedOnNotification machine_word
   | Running
@@ -750,57 +750,67 @@ primrec
 where
   "blockingIPCIsCall (BlockedOnSend v0 v1 v2 v3) = v3"
 
-primrec
-  blockingObject :: "thread_state \<Rightarrow> machine_word"
-where
-  "blockingObject (BlockedOnReceive v0) = v0"
-| "blockingObject (BlockedOnSend v0 v1 v2 v3) = v0"
-
-primrec
-  blockingIPCBadge :: "thread_state \<Rightarrow> machine_word"
-where
-  "blockingIPCBadge (BlockedOnSend v0 v1 v2 v3) = v1"
-
 primrec
   waitingOnNotification :: "thread_state \<Rightarrow> machine_word"
 where
   "waitingOnNotification (BlockedOnNotification v0) = v0"
 
+primrec
+  blockingObject :: "thread_state \<Rightarrow> machine_word"
+where
+  "blockingObject (BlockedOnReceive v0 v1) = v0"
+| "blockingObject (BlockedOnSend v0 v1 v2 v3) = v0"
+
 primrec
   blockingIPCCanGrant :: "thread_state \<Rightarrow> bool"
 where
   "blockingIPCCanGrant (BlockedOnSend v0 v1 v2 v3) = v2"
 
+primrec
+  blockingIPCDiminishCaps :: "thread_state \<Rightarrow> bool"
+where
+  "blockingIPCDiminishCaps (BlockedOnReceive v0 v1) = v1"
+
+primrec
+  blockingIPCBadge :: "thread_state \<Rightarrow> machine_word"
+where
+  "blockingIPCBadge (BlockedOnSend v0 v1 v2 v3) = v1"
+
 primrec
   blockingIPCIsCall_update :: "(bool \<Rightarrow> bool) \<Rightarrow> thread_state \<Rightarrow> thread_state"
 where
   "blockingIPCIsCall_update f (BlockedOnSend v0 v1 v2 v3) = BlockedOnSend v0 v1 v2 (f v3)"
 
-primrec
-  blockingObject_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> thread_state \<Rightarrow> thread_state"
-where
-  "blockingObject_update f (BlockedOnReceive v0) = BlockedOnReceive (f v0)"
-| "blockingObject_update f (BlockedOnSend v0 v1 v2 v3) = BlockedOnSend (f v0) v1 v2 v3"
-
-primrec
-  blockingIPCBadge_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> thread_state \<Rightarrow> thread_state"
-where
-  "blockingIPCBadge_update f (BlockedOnSend v0 v1 v2 v3) = BlockedOnSend v0 (f v1) v2 v3"
-
 primrec
   waitingOnNotification_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> thread_state \<Rightarrow> thread_state"
 where
   "waitingOnNotification_update f (BlockedOnNotification v0) = BlockedOnNotification (f v0)"
 
+primrec
+  blockingObject_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> thread_state \<Rightarrow> thread_state"
+where
+  "blockingObject_update f (BlockedOnReceive v0 v1) = BlockedOnReceive (f v0) v1"
+| "blockingObject_update f (BlockedOnSend v0 v1 v2 v3) = BlockedOnSend (f v0) v1 v2 v3"
+
 primrec
   blockingIPCCanGrant_update :: "(bool \<Rightarrow> bool) \<Rightarrow> thread_state \<Rightarrow> thread_state"
 where
   "blockingIPCCanGrant_update f (BlockedOnSend v0 v1 v2 v3) = BlockedOnSend v0 v1 (f v2) v3"
 
-abbreviation (input)
+primrec
-  BlockedOnReceive_trans :: "(machine_word) \<Rightarrow> thread_state" ("BlockedOnReceive'_ \<lparr> blockingObject= _ \<rparr>")
+  blockingIPCDiminishCaps_update :: "(bool \<Rightarrow> bool) \<Rightarrow> thread_state \<Rightarrow> thread_state"
 where
-  "BlockedOnReceive_ \<lparr> blockingObject= v0 \<rparr> == BlockedOnReceive v0"
+  "blockingIPCDiminishCaps_update f (BlockedOnReceive v0 v1) = BlockedOnReceive v0 (f v1)"
+
+primrec
+  blockingIPCBadge_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> thread_state \<Rightarrow> thread_state"
+where
+  "blockingIPCBadge_update f (BlockedOnSend v0 v1 v2 v3) = BlockedOnSend v0 (f v1) v2 v3"
+
+abbreviation (input)
+  BlockedOnReceive_trans :: "(machine_word) \<Rightarrow> (bool) \<Rightarrow> thread_state" ("BlockedOnReceive'_ \<lparr> blockingObject= _, blockingIPCDiminishCaps= _ \<rparr>")
+where
+  "BlockedOnReceive_ \<lparr> blockingObject= v0, blockingIPCDiminishCaps= v1 \<rparr> == BlockedOnReceive v0 v1"
 
 abbreviation (input)
   BlockedOnNotification_trans :: "(machine_word) \<Rightarrow> thread_state" ("BlockedOnNotification'_ \<lparr> waitingOnNotification= _ \<rparr>")
@@ -816,7 +826,7 @@ definition
   isBlockedOnReceive :: "thread_state \<Rightarrow> bool"
 where
  "isBlockedOnReceive v \<equiv> case v of
-    BlockedOnReceive v0 \<Rightarrow> True
+    BlockedOnReceive v0 v1 \<Rightarrow> True
   | _ \<Rightarrow> False"
 
 definition
@@ -2116,7 +2126,7 @@ defs wordSizeCase_def:
 
 defs isReceive_def:
 "isReceive x0\<equiv> (case x0 of
-    (BlockedOnReceive _) \<Rightarrow>    True
+    (BlockedOnReceive _ _) \<Rightarrow>    True
   | _ \<Rightarrow>    False
   )"
 

spec/design/TCB_H.thy

@@ -122,7 +122,7 @@ defs decodeSetPriority_def:
         throw IllegalOperation;
     returnOk $ ThreadControl_ \<lparr>
         tcThread= capTCBPtr cap,
-        tcThreadCapSlot= 0,
+        tcThreadCapSlot= error [],
         tcNewFaultEP= Nothing,
         tcNewPriority= Just $ fromIntegral newPrio,
         tcNewCRoot= Nothing,

spec/design/ThreadDecls_H.thy

@@ -40,19 +40,19 @@ consts
 restart :: "machine_word \<Rightarrow> unit kernel"
 
 consts
-doIPCTransfer :: "machine_word \<Rightarrow> (machine_word) option \<Rightarrow> machine_word \<Rightarrow> bool \<Rightarrow> machine_word \<Rightarrow> unit kernel"
+doIPCTransfer :: "machine_word \<Rightarrow> (machine_word) option \<Rightarrow> machine_word \<Rightarrow> bool \<Rightarrow> machine_word \<Rightarrow> bool \<Rightarrow> unit kernel"
 
 consts
 doReplyTransfer :: "machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> unit kernel"
 
 consts
-doNormalTransfer :: "machine_word \<Rightarrow> (machine_word) option \<Rightarrow> (machine_word) option \<Rightarrow> machine_word \<Rightarrow> bool \<Rightarrow> machine_word \<Rightarrow> (machine_word) option \<Rightarrow> unit kernel"
+doNormalTransfer :: "machine_word \<Rightarrow> (machine_word) option \<Rightarrow> (machine_word) option \<Rightarrow> machine_word \<Rightarrow> bool \<Rightarrow> machine_word \<Rightarrow> (machine_word) option \<Rightarrow> bool \<Rightarrow> unit kernel"
 
 consts
 doFaultTransfer :: "machine_word \<Rightarrow> machine_word \<Rightarrow> machine_word \<Rightarrow> (machine_word) option \<Rightarrow> unit kernel"
 
 consts
-transferCaps :: "message_info \<Rightarrow> (capability * machine_word) list \<Rightarrow> (machine_word) option \<Rightarrow> machine_word \<Rightarrow> (machine_word) option \<Rightarrow> message_info kernel"
+transferCaps :: "message_info \<Rightarrow> (capability * machine_word) list \<Rightarrow> (machine_word) option \<Rightarrow> machine_word \<Rightarrow> (machine_word) option \<Rightarrow> bool \<Rightarrow> message_info kernel"
 
 consts
 schedule :: "unit kernel"

spec/design/Thread_H.thy

@@ -60,7 +60,7 @@ defs isBlocked_def:
         state \<leftarrow> getThreadState thread;
         return $ (case state of
               Inactive \<Rightarrow>   True
-            | BlockedOnReceive _ \<Rightarrow>   True
+            | BlockedOnReceive _ _ \<Rightarrow>   True
             | BlockedOnSend _ _ _ _ \<Rightarrow>   True
             | BlockedOnNotification _ \<Rightarrow>   True
             | BlockedOnReply \<Rightarrow>   True
@@ -369,18 +369,15 @@ defs timerTick_def:
   od)
 od)"
 
-definition
-"initTCB\<equiv> (makeObject::tcb)\<lparr> tcbPriority:=maxBound \<rparr>"
-
 
 primrec
-transferCapsToSlots :: "(machine_word) option \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> (capability * machine_word) list \<Rightarrow> machine_word list \<Rightarrow> message_info \<Rightarrow> message_info kernel"
+transferCapsToSlots :: "(machine_word) option \<Rightarrow> bool \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> (capability * machine_word) list \<Rightarrow> machine_word list \<Rightarrow> message_info \<Rightarrow> message_info kernel"
 where
-  "transferCapsToSlots arg1 arg2 n [] arg5 mi = (
+  "transferCapsToSlots arg1 arg2 arg3 n [] arg6 mi = (
     return $ mi \<lparr> msgExtraCaps := fromIntegral n \<rparr>)"
-| "transferCapsToSlots ep rcvBuffer n (arg#caps) slots mi = (
+| "transferCapsToSlots ep diminish rcvBuffer n (arg#caps) slots mi = (
     let
-       transferAgain = transferCapsToSlots ep rcvBuffer (n + 1) caps;
+       transferAgain = transferCapsToSlots ep diminish rcvBuffer (n + 1) caps;
        miCapUnfolded = mi \<lparr> msgCapsUnwrapped := msgCapsUnwrapped mi || bit n\<rparr>;
        (cap, srcSlot) = arg
     in
@@ -395,7 +392,10 @@ where
             odE)
             else (case v5 of
             destSlot # slots' \<Rightarrow>  (doE
-                cap' \<leftarrow> unifyFailure $ deriveCap srcSlot $ cap;
+                cap' \<leftarrow> unifyFailure $ deriveCap srcSlot $ if diminish
+                        then allRights \<lparr> capAllowWrite := False \<rparr>
+                            `~maskCapRights~` cap
+                        else cap;
                 whenE (isNullCap cap') $ throw undefined;
                 withoutFailure $ cteInsert cap' srcSlot destSlot;
                 withoutFailure $ transferAgain slots' mi
@@ -407,7 +407,7 @@ where
 
 
 defs doIPCTransfer_def:
-"doIPCTransfer sender endpoint badge grant receiver\<equiv> (do
+"doIPCTransfer sender endpoint badge grant receiver diminish\<equiv> (do
         receiveBuffer \<leftarrow> lookupIPCBuffer True receiver;
         fault \<leftarrow> threadGet tcbFault sender;
         (case fault of
@@ -415,7 +415,7 @@ defs doIPCTransfer_def:
                 sendBuffer \<leftarrow> lookupIPCBuffer False sender;
                 doNormalTransfer
                     sender sendBuffer endpoint badge grant
-                    receiver receiveBuffer
+                    receiver receiveBuffer diminish
               od)
             | Some v1 \<Rightarrow>   (
                 doFaultTransfer badge sender receiver receiveBuffer
@@ -438,7 +438,7 @@ defs doReplyTransfer_def:
     fault \<leftarrow> threadGet tcbFault receiver;
     (case fault of
           None \<Rightarrow>   (do
-            doIPCTransfer sender Nothing 0 True receiver;
+            doIPCTransfer sender Nothing 0 True receiver False;
             cteDeleteOne slot;
             setThreadState Running receiver;
             attemptSwitchTo receiver
@@ -461,7 +461,7 @@ defs doReplyTransfer_def:
 od)"
 
 defs doNormalTransfer_def:
-"doNormalTransfer sender sendBuffer endpoint badge canGrant receiver receiveBuffer\<equiv> (do
+"doNormalTransfer sender sendBuffer endpoint badge canGrant receiver receiveBuffer diminish\<equiv> (do
         tag \<leftarrow> getMessageInfo sender;
         caps \<leftarrow> if canGrant
             then lookupExtraCaps sender sendBuffer tag
@@ -469,20 +469,20 @@ defs doNormalTransfer_def:
             else return [];
         msgTransferred \<leftarrow> copyMRs sender sendBuffer receiver receiveBuffer $
                                   msgLength tag;
-        tag' \<leftarrow> transferCaps tag caps endpoint receiver receiveBuffer;
+        tag' \<leftarrow> transferCaps tag caps endpoint receiver receiveBuffer diminish;
         tag'' \<leftarrow> return ( tag' \<lparr> msgLength := msgTransferred \<rparr>);
         setMessageInfo receiver tag'';
         asUser receiver $ setRegister badgeRegister badge
 od)"
 
 defs transferCaps_def:
-"transferCaps info caps endpoint receiver receiveBuffer\<equiv> (do
+"transferCaps info caps endpoint receiver receiveBuffer diminish\<equiv> (do
     destSlots \<leftarrow> getReceiveSlots receiver receiveBuffer;
     info' \<leftarrow> return ( info \<lparr> msgExtraCaps := 0, msgCapsUnwrapped := 0 \<rparr>);
     (case receiveBuffer of
           None \<Rightarrow>   return info'
         | Some rcvBuffer \<Rightarrow>   (
-            transferCapsToSlots endpoint rcvBuffer 0
+            transferCapsToSlots endpoint diminish rcvBuffer 0
                 caps destSlots info'
         )
         )

spec/design/Types_H.thy

@@ -415,162 +415,152 @@ lemma bidrBasePAddr_bidrBasePAddr_update [simp]:
   by (cases v) simp
 
 datatype biframe_data =
-    BIFrameData word32 word32 word32 vptr "machine_word list" "machine_word list" "machine_word list" "machine_word list" "machine_word list" "machine_word list" "paddr list" "word8 list" word8 word32 "bidevice_region list"
+    BIFrameData word32 word32 word32 vptr "machine_word list" "machine_word list" "machine_word list" "machine_word list" "machine_word list" "paddr list" "word8 list" word8 word32 "bidevice_region list"
 
 primrec
   bifNumIOPTLevels :: "biframe_data \<Rightarrow> word32"
 where
-  "bifNumIOPTLevels (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v2"
+  "bifNumIOPTLevels (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v2"
 
 primrec
   bifNullCaps :: "biframe_data \<Rightarrow> machine_word list"
 where
-  "bifNullCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v4"
+  "bifNullCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v4"
 
 primrec
   bifIPCBufVPtr :: "biframe_data \<Rightarrow> vptr"
 where
-  "bifIPCBufVPtr (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v3"
+  "bifIPCBufVPtr (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v3"
 
 primrec
   bifUIPTCaps :: "biframe_data \<Rightarrow> machine_word list"
 where
-  "bifUIPTCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v8"
+  "bifUIPTCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v7"
 
 primrec
   bifUIFrameCaps :: "biframe_data \<Rightarrow> machine_word list"
 where
-  "bifUIFrameCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v6"
+  "bifUIFrameCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v6"
 
 primrec
   bifUntypedObjSizeBits :: "biframe_data \<Rightarrow> word8 list"
 where
-  "bifUntypedObjSizeBits (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v11"
+  "bifUntypedObjSizeBits (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v10"
 
 primrec
   bifNodeID :: "biframe_data \<Rightarrow> word32"
 where
-  "bifNodeID (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v0"
+  "bifNodeID (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v0"
 
 primrec
   bifNumDeviceRegions :: "biframe_data \<Rightarrow> word32"
 where
-  "bifNumDeviceRegions (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v13"
+  "bifNumDeviceRegions (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v12"
 
 primrec
   bifSharedFrameCaps :: "biframe_data \<Rightarrow> machine_word list"
 where
-  "bifSharedFrameCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v5"
+  "bifSharedFrameCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v5"
 
 primrec
   bifDeviceRegions :: "biframe_data \<Rightarrow> bidevice_region list"
 where
-  "bifDeviceRegions (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v14"
+  "bifDeviceRegions (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v13"
 
 primrec
   bifUntypedObjPAddrs :: "biframe_data \<Rightarrow> paddr list"
 where
-  "bifUntypedObjPAddrs (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v10"
+  "bifUntypedObjPAddrs (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v9"
 
 primrec
   bifNumNodes :: "biframe_data \<Rightarrow> word32"
 where
-  "bifNumNodes (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v1"
+  "bifNumNodes (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v1"
-
-primrec
-  bifUIPDCaps :: "biframe_data \<Rightarrow> machine_word list"
-where
-  "bifUIPDCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v7"
 
 primrec
   bifUntypedObjCaps :: "biframe_data \<Rightarrow> machine_word list"
 where
-  "bifUntypedObjCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v9"
+  "bifUntypedObjCaps (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v8"
 
 primrec
   bifITCNodeSizeBits :: "biframe_data \<Rightarrow> word8"
 where
-  "bifITCNodeSizeBits (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = v12"
+  "bifITCNodeSizeBits (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = v11"
 
 primrec
   bifNumIOPTLevels_update :: "(word32 \<Rightarrow> word32) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifNumIOPTLevels_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 (f v2) v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14"
+  "bifNumIOPTLevels_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 (f v2) v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13"
 
 primrec
   bifNullCaps_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifNullCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 (f v4) v5 v6 v7 v8 v9 v10 v11 v12 v13 v14"
+  "bifNullCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 (f v4) v5 v6 v7 v8 v9 v10 v11 v12 v13"
 
 primrec
   bifIPCBufVPtr_update :: "(vptr \<Rightarrow> vptr) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifIPCBufVPtr_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 (f v3) v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14"
+  "bifIPCBufVPtr_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 (f v3) v4 v5 v6 v7 v8 v9 v10 v11 v12 v13"
 
 primrec
   bifUIPTCaps_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifUIPTCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 (f v8) v9 v10 v11 v12 v13 v14"
+  "bifUIPTCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 v5 v6 (f v7) v8 v9 v10 v11 v12 v13"
 
 primrec
   bifUIFrameCaps_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifUIFrameCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 (f v6) v7 v8 v9 v10 v11 v12 v13 v14"
+  "bifUIFrameCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 v5 (f v6) v7 v8 v9 v10 v11 v12 v13"
 
 primrec
   bifUntypedObjSizeBits_update :: "((word8 list) \<Rightarrow> (word8 list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifUntypedObjSizeBits_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 (f v11) v12 v13 v14"
+  "bifUntypedObjSizeBits_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 (f v10) v11 v12 v13"
 
 primrec
   bifNodeID_update :: "(word32 \<Rightarrow> word32) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifNodeID_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData (f v0) v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14"
+  "bifNodeID_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData (f v0) v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13"
 
 primrec
   bifNumDeviceRegions_update :: "(word32 \<Rightarrow> word32) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifNumDeviceRegions_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 (f v13) v14"
+  "bifNumDeviceRegions_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 (f v12) v13"
 
 primrec
   bifSharedFrameCaps_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifSharedFrameCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 (f v5) v6 v7 v8 v9 v10 v11 v12 v13 v14"
+  "bifSharedFrameCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 (f v5) v6 v7 v8 v9 v10 v11 v12 v13"
 
 primrec
   bifDeviceRegions_update :: "((bidevice_region list) \<Rightarrow> (bidevice_region list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifDeviceRegions_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 (f v14)"
+  "bifDeviceRegions_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 (f v13)"
 
 primrec
   bifUntypedObjPAddrs_update :: "((paddr list) \<Rightarrow> (paddr list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifUntypedObjPAddrs_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 (f v10) v11 v12 v13 v14"
+  "bifUntypedObjPAddrs_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 (f v9) v10 v11 v12 v13"
 
 primrec
   bifNumNodes_update :: "(word32 \<Rightarrow> word32) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifNumNodes_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 (f v1) v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14"
+  "bifNumNodes_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 (f v1) v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13"
-
-primrec
-  bifUIPDCaps_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
-where
-  "bifUIPDCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 v6 (f v7) v8 v9 v10 v11 v12 v13 v14"
 
 primrec
   bifUntypedObjCaps_update :: "((machine_word list) \<Rightarrow> (machine_word list)) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifUntypedObjCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 (f v9) v10 v11 v12 v13 v14"
+  "bifUntypedObjCaps_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 (f v8) v9 v10 v11 v12 v13"
 
 primrec
   bifITCNodeSizeBits_update :: "(word8 \<Rightarrow> word8) \<Rightarrow> biframe_data \<Rightarrow> biframe_data"
 where
-  "bifITCNodeSizeBits_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 (f v12) v13 v14"
+  "bifITCNodeSizeBits_update f (BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13) = BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 (f v11) v12 v13"
 
 abbreviation (input)
-  BIFrameData_trans :: "(word32) \<Rightarrow> (word32) \<Rightarrow> (word32) \<Rightarrow> (vptr) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (paddr list) \<Rightarrow> (word8 list) \<Rightarrow> (word8) \<Rightarrow> (word32) \<Rightarrow> (bidevice_region list) \<Rightarrow> biframe_data" ("BIFrameData'_ \<lparr> bifNodeID= _, bifNumNodes= _, bifNumIOPTLevels= _, bifIPCBufVPtr= _, bifNullCaps= _, bifSharedFrameCaps= _, bifUIFrameCaps= _, bifUIPDCaps= _, bifUIPTCaps= _, bifUntypedObjCaps= _, bifUntypedObjPAddrs= _, bifUntypedObjSizeBits= _, bifITCNodeSizeBits= _, bifNumDeviceRegions= _, bifDeviceRegions= _ \<rparr>")
+  BIFrameData_trans :: "(word32) \<Rightarrow> (word32) \<Rightarrow> (word32) \<Rightarrow> (vptr) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (machine_word list) \<Rightarrow> (paddr list) \<Rightarrow> (word8 list) \<Rightarrow> (word8) \<Rightarrow> (word32) \<Rightarrow> (bidevice_region list) \<Rightarrow> biframe_data" ("BIFrameData'_ \<lparr> bifNodeID= _, bifNumNodes= _, bifNumIOPTLevels= _, bifIPCBufVPtr= _, bifNullCaps= _, bifSharedFrameCaps= _, bifUIFrameCaps= _, bifUIPTCaps= _, bifUntypedObjCaps= _, bifUntypedObjPAddrs= _, bifUntypedObjSizeBits= _, bifITCNodeSizeBits= _, bifNumDeviceRegions= _, bifDeviceRegions= _ \<rparr>")
 where
-  "BIFrameData_ \<lparr> bifNodeID= v0, bifNumNodes= v1, bifNumIOPTLevels= v2, bifIPCBufVPtr= v3, bifNullCaps= v4, bifSharedFrameCaps= v5, bifUIFrameCaps= v6, bifUIPDCaps= v7, bifUIPTCaps= v8, bifUntypedObjCaps= v9, bifUntypedObjPAddrs= v10, bifUntypedObjSizeBits= v11, bifITCNodeSizeBits= v12, bifNumDeviceRegions= v13, bifDeviceRegions= v14 \<rparr> == BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14"
+  "BIFrameData_ \<lparr> bifNodeID= v0, bifNumNodes= v1, bifNumIOPTLevels= v2, bifIPCBufVPtr= v3, bifNullCaps= v4, bifSharedFrameCaps= v5, bifUIFrameCaps= v6, bifUIPTCaps= v7, bifUntypedObjCaps= v8, bifUntypedObjPAddrs= v9, bifUntypedObjSizeBits= v10, bifITCNodeSizeBits= v11, bifNumDeviceRegions= v12, bifDeviceRegions= v13 \<rparr> == BIFrameData v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13"
 
 lemma bifNumIOPTLevels_bifNumIOPTLevels_update [simp]:
   "bifNumIOPTLevels (bifNumIOPTLevels_update f v) = f (bifNumIOPTLevels v)"
@@ -620,10 +610,6 @@ lemma bifNumIOPTLevels_bifNumNodes_update [simp]:
   "bifNumIOPTLevels (bifNumNodes_update f v) = bifNumIOPTLevels v"
   by (cases v) simp
 
-lemma bifNumIOPTLevels_bifUIPDCaps_update [simp]:
-  "bifNumIOPTLevels (bifUIPDCaps_update f v) = bifNumIOPTLevels v"
-  by (cases v) simp
-
 lemma bifNumIOPTLevels_bifUntypedObjCaps_update [simp]:
   "bifNumIOPTLevels (bifUntypedObjCaps_update f v) = bifNumIOPTLevels v"
   by (cases v) simp
@@ -680,10 +666,6 @@ lemma bifNullCaps_bifNumNodes_update [simp]:
   "bifNullCaps (bifNumNodes_update f v) = bifNullCaps v"
   by (cases v) simp
 
-lemma bifNullCaps_bifUIPDCaps_update [simp]:
-  "bifNullCaps (bifUIPDCaps_update f v) = bifNullCaps v"
-  by (cases v) simp
-
 lemma bifNullCaps_bifUntypedObjCaps_update [simp]:
   "bifNullCaps (bifUntypedObjCaps_update f v) = bifNullCaps v"
   by (cases v) simp
@@ -740,10 +722,6 @@ lemma bifIPCBufVPtr_bifNumNodes_update [simp]:
   "bifIPCBufVPtr (bifNumNodes_update f v) = bifIPCBufVPtr v"
   by (cases v) simp
 
-lemma bifIPCBufVPtr_bifUIPDCaps_update [simp]:
-  "bifIPCBufVPtr (bifUIPDCaps_update f v) = bifIPCBufVPtr v"
-  by (cases v) simp
-
 lemma bifIPCBufVPtr_bifUntypedObjCaps_update [simp]:
   "bifIPCBufVPtr (bifUntypedObjCaps_update f v) = bifIPCBufVPtr v"
   by (cases v) simp
@@ -800,10 +778,6 @@ lemma bifUIPTCaps_bifNumNodes_update [simp]:
   "bifUIPTCaps (bifNumNodes_update f v) = bifUIPTCaps v"
   by (cases v) simp
 
-lemma bifUIPTCaps_bifUIPDCaps_update [simp]:
-  "bifUIPTCaps (bifUIPDCaps_update f v) = bifUIPTCaps v"
-  by (cases v) simp
-
 lemma bifUIPTCaps_bifUntypedObjCaps_update [simp]:
   "bifUIPTCaps (bifUntypedObjCaps_update f v) = bifUIPTCaps v"
   by (cases v) simp
@@ -860,10 +834,6 @@ lemma bifUIFrameCaps_bifNumNodes_update [simp]:
   "bifUIFrameCaps (bifNumNodes_update f v) = bifUIFrameCaps v"
   by (cases v) simp
 
-lemma bifUIFrameCaps_bifUIPDCaps_update [simp]:
-  "bifUIFrameCaps (bifUIPDCaps_update f v) = bifUIFrameCaps v"
-  by (cases v) simp
-
 lemma bifUIFrameCaps_bifUntypedObjCaps_update [simp]:
   "bifUIFrameCaps (bifUntypedObjCaps_update f v) = bifUIFrameCaps v"
   by (cases v) simp
@@ -920,10 +890,6 @@ lemma bifUntypedObjSizeBits_bifNumNodes_update [simp]:
   "bifUntypedObjSizeBits (bifNumNodes_update f v) = bifUntypedObjSizeBits v"
   by (cases v) simp
 
-lemma bifUntypedObjSizeBits_bifUIPDCaps_update [simp]:
-  "bifUntypedObjSizeBits (bifUIPDCaps_update f v) = bifUntypedObjSizeBits v"
-  by (cases v) simp
-
 lemma bifUntypedObjSizeBits_bifUntypedObjCaps_update [simp]:
   "bifUntypedObjSizeBits (bifUntypedObjCaps_update f v) = bifUntypedObjSizeBits v"
   by (cases v) simp
@@ -980,10 +946,6 @@ lemma bifNodeID_bifNumNodes_update [simp]:
   "bifNodeID (bifNumNodes_update f v) = bifNodeID v"
   by (cases v) simp
 
-lemma bifNodeID_bifUIPDCaps_update [simp]:
-  "bifNodeID (bifUIPDCaps_update f v) = bifNodeID v"
-  by (cases v) simp
-
 lemma bifNodeID_bifUntypedObjCaps_update [simp]:
   "bifNodeID (bifUntypedObjCaps_update f v) = bifNodeID v"
   by (cases v) simp
@@ -1040,10 +1002,6 @@ lemma bifNumDeviceRegions_bifNumNodes_update [simp]:
   "bifNumDeviceRegions (bifNumNodes_update f v) = bifNumDeviceRegions v"
   by (cases v) simp
 
-lemma bifNumDeviceRegions_bifUIPDCaps_update [simp]:
-  "bifNumDeviceRegions (bifUIPDCaps_update f v) = bifNumDeviceRegions v"
-  by (cases v) simp
-
 lemma bifNumDeviceRegions_bifUntypedObjCaps_update [simp]:
   "bifNumDeviceRegions (bifUntypedObjCaps_update f v) = bifNumDeviceRegions v"
   by (cases v) simp
@@ -1100,10 +1058,6 @@ lemma bifSharedFrameCaps_bifNumNodes_update [simp]:
   "bifSharedFrameCaps (bifNumNodes_update f v) = bifSharedFrameCaps v"
   by (cases v) simp
 
-lemma bifSharedFrameCaps_bifUIPDCaps_update [simp]:
-  "bifSharedFrameCaps (bifUIPDCaps_update f v) = bifSharedFrameCaps v"
-  by (cases v) simp
-
 lemma bifSharedFrameCaps_bifUntypedObjCaps_update [simp]:
   "bifSharedFrameCaps (bifUntypedObjCaps_update f v) = bifSharedFrameCaps v"
   by (cases v) simp
@@ -1160,10 +1114,6 @@ lemma bifDeviceRegions_bifNumNodes_update [simp]:
   "bifDeviceRegions (bifNumNodes_update f v) = bifDeviceRegions v"
   by (cases v) simp
 
-lemma bifDeviceRegions_bifUIPDCaps_update [simp]:
-  "bifDeviceRegions (bifUIPDCaps_update f v) = bifDeviceRegions v"
-  by (cases v) simp
-
 lemma bifDeviceRegions_bifUntypedObjCaps_update [simp]:
   "bifDeviceRegions (bifUntypedObjCaps_update f v) = bifDeviceRegions v"
   by (cases v) simp
@@ -1220,10 +1170,6 @@ lemma bifUntypedObjPAddrs_bifNumNodes_update [simp]:
   "bifUntypedObjPAddrs (bifNumNodes_update f v) = bifUntypedObjPAddrs v"
   by (cases v) simp
 
-lemma bifUntypedObjPAddrs_bifUIPDCaps_update [simp]:
-  "bifUntypedObjPAddrs (bifUIPDCaps_update f v) = bifUntypedObjPAddrs v"
-  by (cases v) simp
-
 lemma bifUntypedObjPAddrs_bifUntypedObjCaps_update [simp]:
   "bifUntypedObjPAddrs (bifUntypedObjCaps_update f v) = bifUntypedObjPAddrs v"
   by (cases v) simp
@@ -1280,10 +1226,6 @@ lemma bifNumNodes_bifNumNodes_update [simp]:
   "bifNumNodes (bifNumNodes_update f v) = f (bifNumNodes v)"
   by (cases v) simp
 
-lemma bifNumNodes_bifUIPDCaps_update [simp]:
-  "bifNumNodes (bifUIPDCaps_update f v) = bifNumNodes v"
-  by (cases v) simp
-
 lemma bifNumNodes_bifUntypedObjCaps_update [simp]:
   "bifNumNodes (bifUntypedObjCaps_update f v) = bifNumNodes v"
   by (cases v) simp
@@ -1292,66 +1234,6 @@ lemma bifNumNodes_bifITCNodeSizeBits_update [simp]:
   "bifNumNodes (bifITCNodeSizeBits_update f v) = bifNumNodes v"
   by (cases v) simp
 
-lemma bifUIPDCaps_bifNumIOPTLevels_update [simp]:
-  "bifUIPDCaps (bifNumIOPTLevels_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifNullCaps_update [simp]:
-  "bifUIPDCaps (bifNullCaps_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifIPCBufVPtr_update [simp]:
-  "bifUIPDCaps (bifIPCBufVPtr_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifUIPTCaps_update [simp]:
-  "bifUIPDCaps (bifUIPTCaps_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifUIFrameCaps_update [simp]:
-  "bifUIPDCaps (bifUIFrameCaps_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifUntypedObjSizeBits_update [simp]:
-  "bifUIPDCaps (bifUntypedObjSizeBits_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifNodeID_update [simp]:
-  "bifUIPDCaps (bifNodeID_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifNumDeviceRegions_update [simp]:
-  "bifUIPDCaps (bifNumDeviceRegions_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifSharedFrameCaps_update [simp]:
-  "bifUIPDCaps (bifSharedFrameCaps_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifDeviceRegions_update [simp]:
-  "bifUIPDCaps (bifDeviceRegions_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifUntypedObjPAddrs_update [simp]:
-  "bifUIPDCaps (bifUntypedObjPAddrs_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifNumNodes_update [simp]:
-  "bifUIPDCaps (bifNumNodes_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifUIPDCaps_update [simp]:
-  "bifUIPDCaps (bifUIPDCaps_update f v) = f (bifUIPDCaps v)"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifUntypedObjCaps_update [simp]:
-  "bifUIPDCaps (bifUntypedObjCaps_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
-lemma bifUIPDCaps_bifITCNodeSizeBits_update [simp]:
-  "bifUIPDCaps (bifITCNodeSizeBits_update f v) = bifUIPDCaps v"
-  by (cases v) simp
-
 lemma bifUntypedObjCaps_bifNumIOPTLevels_update [simp]:
   "bifUntypedObjCaps (bifNumIOPTLevels_update f v) = bifUntypedObjCaps v"
   by (cases v) simp
@@ -1400,10 +1282,6 @@ lemma bifUntypedObjCaps_bifNumNodes_update [simp]:
   "bifUntypedObjCaps (bifNumNodes_update f v) = bifUntypedObjCaps v"
   by (cases v) simp
 
-lemma bifUntypedObjCaps_bifUIPDCaps_update [simp]:
-  "bifUntypedObjCaps (bifUIPDCaps_update f v) = bifUntypedObjCaps v"
-  by (cases v) simp
-
 lemma bifUntypedObjCaps_bifUntypedObjCaps_update [simp]:
   "bifUntypedObjCaps (bifUntypedObjCaps_update f v) = f (bifUntypedObjCaps v)"
   by (cases v) simp
@@ -1460,10 +1338,6 @@ lemma bifITCNodeSizeBits_bifNumNodes_update [simp]:
   "bifITCNodeSizeBits (bifNumNodes_update f v) = bifITCNodeSizeBits v"
   by (cases v) simp
 
-lemma bifITCNodeSizeBits_bifUIPDCaps_update [simp]:
-  "bifITCNodeSizeBits (bifUIPDCaps_update f v) = bifITCNodeSizeBits v"
-  by (cases v) simp
-
 lemma bifITCNodeSizeBits_bifUntypedObjCaps_update [simp]:
   "bifITCNodeSizeBits (bifUntypedObjCaps_update f v) = bifITCNodeSizeBits v"
   by (cases v) simp
@@ -1473,217 +1347,163 @@ lemma bifITCNodeSizeBits_bifITCNodeSizeBits_update [simp]:
   by (cases v) simp
 
 datatype init_data =
-    InitData "region list" machine_word machine_word biframe_data vptr paddr
+    InitData "region list" machine_word machine_word biframe_data paddr
 
 primrec
   initSlotPosMax :: "init_data \<Rightarrow> machine_word"
 where
-  "initSlotPosMax (InitData v0 v1 v2 v3 v4 v5) = v2"
+  "initSlotPosMax (InitData v0 v1 v2 v3 v4) = v2"
-
-primrec
-  initSlotPosCur :: "init_data \<Rightarrow> machine_word"
-where
-  "initSlotPosCur (InitData v0 v1 v2 v3 v4 v5) = v1"
-
-primrec
-  initFreeMemory :: "init_data \<Rightarrow> region list"
-where
-  "initFreeMemory (InitData v0 v1 v2 v3 v4 v5) = v0"
-
-primrec
-  initVPtrOffset :: "init_data \<Rightarrow> vptr"
-where
-  "initVPtrOffset (InitData v0 v1 v2 v3 v4 v5) = v4"
 
 primrec
   initBootInfoFrame :: "init_data \<Rightarrow> paddr"
 where
-  "initBootInfoFrame (InitData v0 v1 v2 v3 v4 v5) = v5"
+  "initBootInfoFrame (InitData v0 v1 v2 v3 v4) = v4"
+
+primrec
+  initSlotPosCur :: "init_data \<Rightarrow> machine_word"
+where
+  "initSlotPosCur (InitData v0 v1 v2 v3 v4) = v1"
 
 primrec
   initBootInfo :: "init_data \<Rightarrow> biframe_data"
 where
-  "initBootInfo (InitData v0 v1 v2 v3 v4 v5) = v3"
+  "initBootInfo (InitData v0 v1 v2 v3 v4) = v3"
+
+primrec
+  initFreeMemory :: "init_data \<Rightarrow> region list"
+where
+  "initFreeMemory (InitData v0 v1 v2 v3 v4) = v0"
 
 primrec
   initSlotPosMax_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> init_data \<Rightarrow> init_data"
 where
-  "initSlotPosMax_update f (InitData v0 v1 v2 v3 v4 v5) = InitData v0 v1 (f v2) v3 v4 v5"
+  "initSlotPosMax_update f (InitData v0 v1 v2 v3 v4) = InitData v0 v1 (f v2) v3 v4"
-
-primrec
-  initSlotPosCur_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> init_data \<Rightarrow> init_data"
-where
-  "initSlotPosCur_update f (InitData v0 v1 v2 v3 v4 v5) = InitData v0 (f v1) v2 v3 v4 v5"
-
-primrec
-  initFreeMemory_update :: "((region list) \<Rightarrow> (region list)) \<Rightarrow> init_data \<Rightarrow> init_data"
-where
-  "initFreeMemory_update f (InitData v0 v1 v2 v3 v4 v5) = InitData (f v0) v1 v2 v3 v4 v5"
-
-primrec
-  initVPtrOffset_update :: "(vptr \<Rightarrow> vptr) \<Rightarrow> init_data \<Rightarrow> init_data"
-where
-  "initVPtrOffset_update f (InitData v0 v1 v2 v3 v4 v5) = InitData v0 v1 v2 v3 (f v4) v5"
 
 primrec
   initBootInfoFrame_update :: "(paddr \<Rightarrow> paddr) \<Rightarrow> init_data \<Rightarrow> init_data"
 where
-  "initBootInfoFrame_update f (InitData v0 v1 v2 v3 v4 v5) = InitData v0 v1 v2 v3 v4 (f v5)"
+  "initBootInfoFrame_update f (InitData v0 v1 v2 v3 v4) = InitData v0 v1 v2 v3 (f v4)"
+
+primrec
+  initSlotPosCur_update :: "(machine_word \<Rightarrow> machine_word) \<Rightarrow> init_data \<Rightarrow> init_data"
+where
+  "initSlotPosCur_update f (InitData v0 v1 v2 v3 v4) = InitData v0 (f v1) v2 v3 v4"
 
 primrec
   initBootInfo_update :: "(biframe_data \<Rightarrow> biframe_data) \<Rightarrow> init_data \<Rightarrow> init_data"
 where
-  "initBootInfo_update f (InitData v0 v1 v2 v3 v4 v5) = InitData v0 v1 v2 (f v3) v4 v5"
+  "initBootInfo_update f (InitData v0 v1 v2 v3 v4) = InitData v0 v1 v2 (f v3) v4"
+
+primrec
+  initFreeMemory_update :: "((region list) \<Rightarrow> (region list)) \<Rightarrow> init_data \<Rightarrow> init_data"
+where
+  "initFreeMemory_update f (InitData v0 v1 v2 v3 v4) = InitData (f v0) v1 v2 v3 v4"
 
 abbreviation (input)
-  InitData_trans :: "(region list) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (biframe_data) \<Rightarrow> (vptr) \<Rightarrow> (paddr) \<Rightarrow> init_data" ("InitData'_ \<lparr> initFreeMemory= _, initSlotPosCur= _, initSlotPosMax= _, initBootInfo= _, initVPtrOffset= _, initBootInfoFrame= _ \<rparr>")
+  InitData_trans :: "(region list) \<Rightarrow> (machine_word) \<Rightarrow> (machine_word) \<Rightarrow> (biframe_data) \<Rightarrow> (paddr) \<Rightarrow> init_data" ("InitData'_ \<lparr> initFreeMemory= _, initSlotPosCur= _, initSlotPosMax= _, initBootInfo= _, initBootInfoFrame= _ \<rparr>")
 where
-  "InitData_ \<lparr> initFreeMemory= v0, initSlotPosCur= v1, initSlotPosMax= v2, initBootInfo= v3, initVPtrOffset= v4, initBootInfoFrame= v5 \<rparr> == InitData v0 v1 v2 v3 v4 v5"
+  "InitData_ \<lparr> initFreeMemory= v0, initSlotPosCur= v1, initSlotPosMax= v2, initBootInfo= v3, initBootInfoFrame= v4 \<rparr> == InitData v0 v1 v2 v3 v4"
 
 lemma initSlotPosMax_initSlotPosMax_update [simp]:
   "initSlotPosMax (initSlotPosMax_update f v) = f (initSlotPosMax v)"
   by (cases v) simp
 
-lemma initSlotPosMax_initSlotPosCur_update [simp]:
-  "initSlotPosMax (initSlotPosCur_update f v) = initSlotPosMax v"
-  by (cases v) simp
-
-lemma initSlotPosMax_initFreeMemory_update [simp]:
-  "initSlotPosMax (initFreeMemory_update f v) = initSlotPosMax v"
-  by (cases v) simp
-
-lemma initSlotPosMax_initVPtrOffset_update [simp]:
-  "initSlotPosMax (initVPtrOffset_update f v) = initSlotPosMax v"
-  by (cases v) simp
-
 lemma initSlotPosMax_initBootInfoFrame_update [simp]:
   "initSlotPosMax (initBootInfoFrame_update f v) = initSlotPosMax v"
   by (cases v) simp
 
+lemma initSlotPosMax_initSlotPosCur_update [simp]:
+  "initSlotPosMax (initSlotPosCur_update f v) = initSlotPosMax v"
+  by (cases v) simp
+
 lemma initSlotPosMax_initBootInfo_update [simp]:
   "initSlotPosMax (initBootInfo_update f v) = initSlotPosMax v"
   by (cases v) simp
 
-lemma initSlotPosCur_initSlotPosMax_update [simp]:
+lemma initSlotPosMax_initFreeMemory_update [simp]:
-  "initSlotPosCur (initSlotPosMax_update f v) = initSlotPosCur v"
+  "initSlotPosMax (initFreeMemory_update f v) = initSlotPosMax v"
-  by (cases v) simp
-
-lemma initSlotPosCur_initSlotPosCur_update [simp]:
-  "initSlotPosCur (initSlotPosCur_update f v) = f (initSlotPosCur v)"
-  by (cases v) simp
-
-lemma initSlotPosCur_initFreeMemory_update [simp]:
-  "initSlotPosCur (initFreeMemory_update f v) = initSlotPosCur v"
-  by (cases v) simp
-
-lemma initSlotPosCur_initVPtrOffset_update [simp]:
-  "initSlotPosCur (initVPtrOffset_update f v) = initSlotPosCur v"
-  by (cases v) simp
-
-lemma initSlotPosCur_initBootInfoFrame_update [simp]:
-  "initSlotPosCur (initBootInfoFrame_update f v) = initSlotPosCur v"
-  by (cases v) simp
-
-lemma initSlotPosCur_initBootInfo_update [simp]:
-  "initSlotPosCur (initBootInfo_update f v) = initSlotPosCur v"
-  by (cases v) simp
-
-lemma initFreeMemory_initSlotPosMax_update [simp]:
-  "initFreeMemory (initSlotPosMax_update f v) = initFreeMemory v"
-  by (cases v) simp
-
-lemma initFreeMemory_initSlotPosCur_update [simp]:
-  "initFreeMemory (initSlotPosCur_update f v) = initFreeMemory v"
-  by (cases v) simp
-
-lemma initFreeMemory_initFreeMemory_update [simp]:
-  "initFreeMemory (initFreeMemory_update f v) = f (initFreeMemory v)"
-  by (cases v) simp
-
-lemma initFreeMemory_initVPtrOffset_update [simp]:
-  "initFreeMemory (initVPtrOffset_update f v) = initFreeMemory v"
-  by (cases v) simp
-
-lemma initFreeMemory_initBootInfoFrame_update [simp]:
-  "initFreeMemory (initBootInfoFrame_update f v) = initFreeMemory v"
-  by (cases v) simp
-
-lemma initFreeMemory_initBootInfo_update [simp]:
-  "initFreeMemory (initBootInfo_update f v) = initFreeMemory v"
-  by (cases v) simp
-
-lemma initVPtrOffset_initSlotPosMax_update [simp]:
-  "initVPtrOffset (initSlotPosMax_update f v) = initVPtrOffset v"
-  by (cases v) simp
-
-lemma initVPtrOffset_initSlotPosCur_update [simp]:
-  "initVPtrOffset (initSlotPosCur_update f v) = initVPtrOffset v"
-  by (cases v) simp
-
-lemma initVPtrOffset_initFreeMemory_update [simp]:
-  "initVPtrOffset (initFreeMemory_update f v) = initVPtrOffset v"
-  by (cases v) simp
-
-lemma initVPtrOffset_initVPtrOffset_update [simp]:
-  "initVPtrOffset (initVPtrOffset_update f v) = f (initVPtrOffset v)"
-  by (cases v) simp
-
-lemma initVPtrOffset_initBootInfoFrame_update [simp]:
-  "initVPtrOffset (initBootInfoFrame_update f v) = initVPtrOffset v"
-  by (cases v) simp
-
-lemma initVPtrOffset_initBootInfo_update [simp]:
-  "initVPtrOffset (initBootInfo_update f v) = initVPtrOffset v"
   by (cases v) simp
 
 lemma initBootInfoFrame_initSlotPosMax_update [simp]:
   "initBootInfoFrame (initSlotPosMax_update f v) = initBootInfoFrame v"
   by (cases v) simp
 
-lemma initBootInfoFrame_initSlotPosCur_update [simp]:
-  "initBootInfoFrame (initSlotPosCur_update f v) = initBootInfoFrame v"
-  by (cases v) simp
-
-lemma initBootInfoFrame_initFreeMemory_update [simp]:
-  "initBootInfoFrame (initFreeMemory_update f v) = initBootInfoFrame v"
-  by (cases v) simp
-
-lemma initBootInfoFrame_initVPtrOffset_update [simp]:
-  "initBootInfoFrame (initVPtrOffset_update f v) = initBootInfoFrame v"
-  by (cases v) simp
-
 lemma initBootInfoFrame_initBootInfoFrame_update [simp]:
   "initBootInfoFrame (initBootInfoFrame_update f v) = f (initBootInfoFrame v)"
   by (cases v) simp
 
+lemma initBootInfoFrame_initSlotPosCur_update [simp]:
+  "initBootInfoFrame (initSlotPosCur_update f v) = initBootInfoFrame v"
+  by (cases v) simp
+
 lemma initBootInfoFrame_initBootInfo_update [simp]:
   "initBootInfoFrame (initBootInfo_update f v) = initBootInfoFrame v"
   by (cases v) simp
 
+lemma initBootInfoFrame_initFreeMemory_update [simp]:
+  "initBootInfoFrame (initFreeMemory_update f v) = initBootInfoFrame v"
+  by (cases v) simp
+
+lemma initSlotPosCur_initSlotPosMax_update [simp]:
+  "initSlotPosCur (initSlotPosMax_update f v) = initSlotPosCur v"
+  by (cases v) simp
+
+lemma initSlotPosCur_initBootInfoFrame_update [simp]:
+  "initSlotPosCur (initBootInfoFrame_update f v) = initSlotPosCur v"
+  by (cases v) simp
+
+lemma initSlotPosCur_initSlotPosCur_update [simp]:
+  "initSlotPosCur (initSlotPosCur_update f v) = f (initSlotPosCur v)"
+  by (cases v) simp
+
+lemma initSlotPosCur_initBootInfo_update [simp]:
+  "initSlotPosCur (initBootInfo_update f v) = initSlotPosCur v"
+  by (cases v) simp
+
+lemma initSlotPosCur_initFreeMemory_update [simp]:
+  "initSlotPosCur (initFreeMemory_update f v) = initSlotPosCur v"
+  by (cases v) simp
+
 lemma initBootInfo_initSlotPosMax_update [simp]:
   "initBootInfo (initSlotPosMax_update f v) = initBootInfo v"
   by (cases v) simp
 
-lemma initBootInfo_initSlotPosCur_update [simp]:
-  "initBootInfo (initSlotPosCur_update f v) = initBootInfo v"
-  by (cases v) simp
-
-lemma initBootInfo_initFreeMemory_update [simp]:
-  "initBootInfo (initFreeMemory_update f v) = initBootInfo v"
-  by (cases v) simp
-
-lemma initBootInfo_initVPtrOffset_update [simp]:
-  "initBootInfo (initVPtrOffset_update f v) = initBootInfo v"
-  by (cases v) simp
-
 lemma initBootInfo_initBootInfoFrame_update [simp]:
   "initBootInfo (initBootInfoFrame_update f v) = initBootInfo v"
   by (cases v) simp
 
+lemma initBootInfo_initSlotPosCur_update [simp]:
+  "initBootInfo (initSlotPosCur_update f v) = initBootInfo v"
+  by (cases v) simp
+
 lemma initBootInfo_initBootInfo_update [simp]:
   "initBootInfo (initBootInfo_update f v) = f (initBootInfo v)"
   by (cases v) simp
 
+lemma initBootInfo_initFreeMemory_update [simp]:
+  "initBootInfo (initFreeMemory_update f v) = initBootInfo v"
+  by (cases v) simp
+
+lemma initFreeMemory_initSlotPosMax_update [simp]:
+  "initFreeMemory (initSlotPosMax_update f v) = initFreeMemory v"
+  by (cases v) simp
+
+lemma initFreeMemory_initBootInfoFrame_update [simp]:
+  "initFreeMemory (initBootInfoFrame_update f v) = initFreeMemory v"
+  by (cases v) simp
+
+lemma initFreeMemory_initSlotPosCur_update [simp]:
+  "initFreeMemory (initSlotPosCur_update f v) = initFreeMemory v"
+  by (cases v) simp
+
+lemma initFreeMemory_initBootInfo_update [simp]:
+  "initFreeMemory (initBootInfo_update f v) = initFreeMemory v"
+  by (cases v) simp
+
+lemma initFreeMemory_initFreeMemory_update [simp]:
+  "initFreeMemory (initFreeMemory_update f v) = f (initFreeMemory v)"
+  by (cases v) simp
+
 definition
 getObjectSize :: "object_type \<Rightarrow> nat \<Rightarrow> nat"
 where

spec/design/VSpace_H.thy

@@ -28,7 +28,6 @@ definition
 initPlatform :: "unit kernel"
 where
 "initPlatform\<equiv> (do
-  doMachineOp $ initIRQController;
   doMachineOp $ configureTimer;
   doMachineOp $ initL2Cache
 od)"
@@ -49,7 +48,7 @@ where
 "createBIFrame  \<equiv> ArchVSpaceDecls_H.createBIFrame"
 
 definition
-createFramesOfRegion :: "capability \<Rightarrow> region \<Rightarrow> bool \<Rightarrow> unit kernel_init"
+createFramesOfRegion :: "capability \<Rightarrow> region \<Rightarrow> bool \<Rightarrow> vptr \<Rightarrow> unit kernel_init"
 where
 "createFramesOfRegion \<equiv> ArchVSpaceDecls_H.createFramesOfRegion"
 
@@ -98,10 +97,5 @@ lookupIPCBuffer :: "bool \<Rightarrow> machine_word \<Rightarrow> ((machine_word
 where
 "lookupIPCBuffer \<equiv> ArchVSpaceDecls_H.lookupIPCBuffer"
 
-definition
-vptrFromPPtr :: "machine_word \<Rightarrow> vptr kernel_init"
-where
-"vptrFromPPtr \<equiv> ArchVSpaceDecls_H.vptrFromPPtr"
-
 
 end

spec/design/skel/ARM/ArchInterruptDecls_H.thy

@@ -12,6 +12,10 @@ theory ArchInterruptDecls_H
 imports "../RetypeDecls_H" "../CNode_H" 
 begin
 
+qualify ARM
+
 #INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs decls_only ArchInv=ArchRetypeDecls_H
 
+end_qualify
+
 end

spec/design/skel/ARM/ArchInterrupt_H.thy

@@ -12,6 +12,10 @@ theory ArchInterrupt_H
 imports "../RetypeDecls_H" "../CNode_H" "../InterruptDecls_H" ArchInterruptDecls_H
 begin
 
+qualify ARM
+
 #INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs bodies_only ArchInv=ArchRetypeDecls_H
 
+end_qualify
+
 end

spec/design/skel/ARM/ArchObjInsts_H.thy

@@ -20,6 +20,7 @@ imports
   "../PSpaceStorable_H"
   "../ObjectInstances_H"
 begin
+qualify ARM
 
 instantiation pde :: pre_storable
 begin
@@ -153,4 +154,5 @@ instance
 
 end
 
+end_qualify
 end

spec/design/skel/ARM/ArchRetypeDecls_H.thy

@@ -19,8 +19,10 @@ imports
   "../PSpaceFuns_H"
   ArchObjInsts_H
 begin
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs decls_only NOT isPageFlushLabel isPDFlushLabel
 #INCLUDE_HASKELL SEL4/Object/ObjectType/ARM.lhs Arch.Types=ArchTypes_H ArchInv=ArchRetypeDecls_H decls_only
 
+end_qualify
 end

spec/design/skel/ARM/ArchRetype_H.thy

@@ -17,8 +17,10 @@ imports
   Hardware_H
   "../KI_Decls_H"
 begin
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/Object/ObjectType/ARM.lhs Arch.Types=ArchTypes_H ArchInv=ArchRetypeDecls_H bodies_only
 #INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs bodies_only NOT isPDFlushLabel isPageFlushLabel
 
+end_qualify
 end

spec/design/skel/ARM/ArchStateData_H.thy

@@ -20,7 +20,9 @@ imports
   ArchTypes_H
   ArchStructures_H
 begin
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs NOT ArmVSpaceRegionUse
 
+end_qualify
 end

spec/design/skel/ARM/ArchStructures_H.thy

@@ -14,6 +14,7 @@ imports
   "../Types_H"
   Hardware_H
 begin
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs decls_only
 #INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs instanceproofs
@@ -31,4 +32,5 @@ where
 | "archTypeOf (KOPTE e) = PTET"
 | "archTypeOf (KOASIDPool e) = ASIDPoolT"
 
+end_qualify
 end

spec/design/skel/ARM/ArchTCB_H.thy

@@ -11,7 +11,9 @@
 theory ArchTCB_H
 imports "../TCBDecls_H"
 begin
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/Object/TCB/ARM.lhs
 
+end_qualify
 end

spec/design/skel/ARM/ArchThreadDecls_H.thy

@@ -20,7 +20,9 @@ imports
   "../FaultMonad_H"
   "../KernelInitMonad_H"
 begin
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/Kernel/Thread/ARM.lhs decls_only
 
+end_qualify
 end

spec/design/skel/ARM/ArchThread_H.thy

@@ -16,8 +16,9 @@ imports
   "../TCBDecls_H"
   ArchVSpaceDecls_H
 begin
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/Kernel/Thread/ARM.lhs ARMHardware=MachineOps bodies_only
 
-
+end_qualify
 end

spec/design/skel/ARM/ArchTypes_H.thy

@@ -20,16 +20,24 @@ imports
   Hardware_H
   "../../../lib/Lib"
 begin
+context ARM begin
 
-#INCLUDE_HASKELL SEL4/API/Types/Universal.lhs all_bits
+#INCLUDE_HASKELL SEL4/API/Types/Universal.lhs NOT instanceproofs
+
+end
+
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/API/Types/ARM.lhs 
 
+end_qualify
 
 text {* object\_type instance proofs *}
 
 instantiation object_type :: enum
 begin
+interpretation ARM .
+
 definition
   enum_object_type: "enum_class.enum \<equiv> 
     map APIObjectType (enum_class.enum :: apiobject_type list) @ 
@@ -71,4 +79,5 @@ begin
 instance by (intro_classes, simp add: enum_alt_object_type)
 end
 
+end_qualify
 end

spec/design/skel/ARM/ArchVSpaceDecls_H.thy

@@ -13,8 +13,10 @@ chapter "Retyping Objects"
 theory ArchVSpaceDecls_H
 imports ArchRetypeDecls_H "../InvocationLabels_H"
 begin
+qualify ARM
 
 #INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures.lhs
 #INCLUDE_HASKELL SEL4/Kernel/VSpace/ARM.lhs decls_only ArchInv=ArchRetypeDecls_H ArchLabels=ArchInvocationLabels_H
 
+end_qualify
 end

spec/design/skel/ARM/Arch_Structs_B.thy

@@ -13,9 +13,11 @@
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports "~~/src/HOL/Main"
+imports "~~/src/HOL/Main" "../../../spec/machine/$L4V_ARCH/Setup_Locale"
 begin
+qualify ARM
 
 #INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs ONLY ArmVSpaceRegionUse
 
+end_qualify
 end

spec/design/skel/ARM/Hardware_H.thy

@@ -13,11 +13,27 @@ imports
   "../../machine/ARM/MachineOps"
   State_H
 begin
+context ARM begin
 
-#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory writeTTBR0 setCurrentPD setGlobalPD  setTTBCR setHardwareASID invalidateTLB invalidateTLB_ASID invalidateTLB_VAASID cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidate_D_PoU cleanInvalidateL2Range invalidateL2Range cleanL2Range isb dsb dmb getIFSR getDFSR getFAR HardwareASID wordFromPDE wordFromPTE VMFaultType VMPageSize pageBits pageBitsForSize toPAddr cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr initIRQController MachineData
+#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs Platform=Platform.ARM NOT getMemoryRegions getDeviceRegions getKernelDevices loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory clearMemoryVM initMemory freeMemory writeTTBR0 setCurrentPD setGlobalPD  setTTBCR setHardwareASID invalidateTLB invalidateTLB_ASID invalidateTLB_VAASID cleanByVA cleanByVA_PoU invalidateByVA invalidateByVA_I invalidate_I_PoU cleanInvalByVA branchFlush clean_D_PoU cleanInvalidate_D_PoC cleanInvalidate_D_PoU cleanInvalidateL2Range invalidateL2Range cleanL2Range isb dsb dmb getIFSR getDFSR getFAR HardwareASID wordFromPDE wordFromPTE VMFaultType VMPageSize pageBits pageBitsForSize toPAddr cacheLineBits cacheLine lineStart cacheRangeOp cleanCacheRange_PoC cleanInvalidateCacheRange_RAM cleanCacheRange_RAM cleanCacheRange_PoU invalidateCacheRange_RAM invalidateCacheRange_I branchFlushRange cleanCaches_PoU cleanInvalidateL1Caches addrFromPPtr ptrFromPAddr initIRQController MachineData
+
+end
+
+qualify ARM (deep)
+
+declare ARM.vmrights.exhaust[cases type: ARM.vmrights]
+ Hardware_H.ARM.vmrights.simps[simp]
 
 #INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs instanceproofs NOT HardwareASID VMFaultType VMPageSize
 
+end_qualify
+
+declare ARM.vmrights.exhaust[cases del]
+ Hardware_H.ARM.vmrights.simps[simp del]
+
+context ARM begin
+
 #INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs ONLY wordFromPDE wordFromPTE
 
 end
+end

spec/design/skel/ARM/RegisterSet_H.thy

@@ -15,6 +15,7 @@ imports
   "../../../lib/HaskellLib_H"
   "../../machine/ARM/MachineTypes"
 begin
+context ARM begin
 
 definition
   newContext :: "register => machine_word"
@@ -22,3 +23,4 @@ where
  "newContext \<equiv> (K 0) aLU initContext"
 
 end
+end

spec/design/skel/ARM/State_H.thy

@@ -20,6 +20,7 @@ imports
   RegisterSet_H
   "../../machine/ARM/MachineOps"
 begin
+qualify ARM (deep)
 
 definition
   Word :: "machine_word \<Rightarrow> machine_word"
@@ -46,5 +47,5 @@ definition
 where
  "nullPointer \<equiv> 0"
 
-
+end_qualify
 end

spec/design/version

@@ -1,5 +1,5 @@
-Built from git repo at /home/matthewb/verification/arch_split/seL4/haskell by matthewb
+Built from git repo at /Users/dmatichuk/verification-archsplit/seL4/haskell by dmatichuk
 
 Generated from changeset:
-603484f SELFOUR-114: trivial - add missing types to x86
+e35adcb remove mentions of ARM from arch-independent invocation labels