theory Orphanage

lemma createObject_no_orphans:
  "\<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and
    cte_wp_at' (\<lambda>cte. cteCap cte = (capability.UntypedCap d ptr sz idx)) cref and
    K (range_cover ptr sz (APIType_capBits tp us) (Suc 0)) and no_orphans\<rbrace>
   RetypeDecls_H.createObject tp ptr us d
   \<lbrace>\<lambda>xa. no_orphans\<rbrace>" apply (simp only: createObject_def ARM_H.createObject_def placeNewObject_def2) apply (wpsimp wp: createObjects'_wp_subst threadSet_no_orphans
                  createObjects_no_orphans[where sz = sz]
    simp: placeNewObject_def2 placeNewDataObject_def
                       projectKO_opt_tcb cte_wp_at_ctes_of projectKO_opt_ep
                       is_active_thread_state_def makeObject_tcb pageBits_def unless_def
                       projectKO_opt_tcb isRunning_def isRestart_def
                       APIType_capBits_def objBits_simps
    split_del: if_split) apply (clarsimp simp: toAPIType_def APIType_capBits_def objBits_simps
                        archObjSize_def pteBits_def ptBits_def
                        pdeBits_def pdBits_def
      split: object_type.split_asm apiobject_type.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr sz idx) cref and K (range_cover ptr sz (APIType_capBits tp us) (Suc 0)) and no_orphans\<rbrace> global.createObject tp ptr us d \<lbrace>\<lambda>xa. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' ptr sz and pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr sz idx) cref and K (range_cover ptr sz (APIType_capBits tp us) (Suc 0)) and no_orphans\<rbrace> let funupd = \<lambda>f x v y. if y = x then v else f y in case toAPIType tp of None \<Rightarrow> do archCap <- let funupd = \<lambda>f x v y. if y = x then v else f y; pointerCast = PPtr \<circ> fromPPtr; mkPageCap = \<lambda>sz. arch_capability.PageCap d (pointerCast ptr) VMReadWrite sz Nothing in case tp of APIObjectType v2 \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> do placeNewDataObject ptr 0 d;
modify (\<lambda>ks. ks\<lparr>gsUserPages := funupd (gsUserPages ks) (fromPPtr ptr) (Just ARMSmallPage)\<rparr>);
return $ mkPageCap ARMSmallPage
od | LargePageObject \<Rightarrow> do placeNewDataObject ptr 4 d;
modify (\<lambda>ks. ks\<lparr>gsUserPages := funupd (gsUserPages ks) (fromPPtr ptr) (Just ARMLargePage)\<rparr>);
return $ mkPageCap ARMLargePage
od | SectionObject \<Rightarrow> do placeNewDataObject ptr 8 d;
modify (\<lambda>ks. ks\<lparr>gsUserPages := funupd (gsUserPages ks) (fromPPtr ptr) (Just ARMSection)\<rparr>);
return $ mkPageCap ARMSection
od | SuperSectionObject \<Rightarrow> do placeNewDataObject ptr 12 d;
modify (\<lambda>ks. ks\<lparr>gsUserPages := funupd (gsUserPages ks) (fromPPtr ptr) (Just ARMSuperSection)\<rparr>);
return $ mkPageCap ARMSuperSection
od | PageTableObject \<Rightarrow> do ptSize <- return (ptBits - objBits makeObject);
createObjects' ptr 1 (injectKOS makeObject) ptSize;
return $ arch_capability.PageTableCap (pointerCast ptr) Nothing
od | PageDirectoryObject \<Rightarrow> do pdSize <- return (pdBits - objBits makeObject);
regionSize <- return (1 `~shiftL~` pdBits);
createObjects' ptr 1 (injectKOS makeObject) pdSize;
copyGlobalMappings (pointerCast ptr);
doMachineOp $ cleanCacheRange_PoU (VPtr $ fromPPtr ptr) (VPtr $ fromPPtr ptr + regionSize - 1) (addrFromPPtr ptr);
return $ arch_capability.PageDirectoryCap (pointerCast ptr) Nothing
od;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do createObjects' ptr 1 (injectKOS makeObject) 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do createObjects' ptr 1 (injectKOS makeObject) 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do createObjects' (PPtr $ fromPPtr ptr) 1 (injectKOS makeObject) 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do createObjects' (PPtr $ fromPPtr ptr) 1 (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := funupd (gsCNodes ks) (fromPPtr ptr) (Just us)\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>xa. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>pspace_no_overlap' ptr sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (case tp of APIObjectType ArchTypes_H.apiobject_type.Untyped \<Rightarrow> us | APIObjectType ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> objBits makeObject | APIObjectType ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> objBits makeObject | APIObjectType ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> objBits makeObject | APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> objBits makeObject + us | SmallPageObject \<Rightarrow> pageBitsForSize ARMSmallPage | LargePageObject \<Rightarrow> pageBitsForSize ARMLargePage | SectionObject \<Rightarrow> pageBitsForSize ARMSection | SuperSectionObject \<Rightarrow> pageBitsForSize ARMSuperSection | PageTableObject \<Rightarrow> 10 | PageDirectoryObject \<Rightarrow> 14) (Suc 0); no_orphans s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr sz idx\<rbrakk> \<Longrightarrow> (toAPIType tp = None \<longrightarrow> (tp = SmallPageObject \<longrightarrow> range_cover ptr sz 12 (Suc 0)) \<and> (tp = LargePageObject \<longrightarrow> range_cover ptr sz 16 (Suc 0)) \<and> (tp = SectionObject \<longrightarrow> range_cover ptr sz 20 (Suc 0)) \<and> (tp = SuperSectionObject \<longrightarrow> range_cover ptr sz 24 (Suc 0)) \<and> (tp = PageTableObject \<longrightarrow> range_cover ptr sz (archObjSize (KOPTE makeObject) + (ptBits - archObjSize (KOPTE makeObject))) (Suc 0)) \<and> (tp = PageDirectoryObject \<longrightarrow> range_cover ptr sz (archObjSize (KOPDE makeObject) + (pdBits - archObjSize (KOPDE makeObject))) (Suc 0))) \<and> (\<forall>x. toAPIType tp = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> range_cover ptr sz tcbBlockSizeBits (Suc 0)) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> range_cover ptr sz epSizeBits (Suc 0)) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> range_cover ptr sz ntfnSizeBits (Suc 0)) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> range_cover ptr sz (cteSizeBits + us) (Suc 0))) proof (prove)
goal:
No subgoals!