theory Detype_R

lemma createNewCaps_not_nc:
  "\<lbrace>\<top>\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. (\<forall>cap\<in>set r. cap \<noteq> NullCap)\<rbrace>" unfolding createNewCaps_def Arch_createNewCaps_def by (wpsimp simp: Arch_createNewCaps_def split_del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> createNewCaps ty ptr (Suc (length as)) us d \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. cap \<noteq> capability.NullCap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> case toAPIType ty of None \<Rightarrow> do archCaps <- let pointerCast = PPtr \<circ> fromPPtr in case ty of APIObjectType apiObject \<Rightarrow> haskell_fail [] | SmallPageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr (Suc (length as)) Data 0;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSmallPage Nothing) addrs
od | LargePageObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr (Suc (length as)) Data 4;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMLargePage else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMLargePage Nothing) addrs
od | SectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr (Suc (length as)) Data 8;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSection Nothing) addrs
od | SuperSectionObject \<Rightarrow> let Data = if d then KOUserDataDevice else KOUserData in do addrs <- createObjects ptr (Suc (length as)) Data 12;
modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection else gsUserPages ks addr\<rparr>);
return $ map (\<lambda>n. arch_capability.PageCap d (PPtr (fromPPtr n)) VMReadWrite ARMSuperSection Nothing) addrs
od | PageTableObject \<Rightarrow> do tableSize <- return (ptBits - objBits makeObject);
addrs <- createObjects ptr (Suc (length as)) (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
return ();
return $ map (\<lambda>pt. arch_capability.PageTableCap pt Nothing) pts
od | PageDirectoryObject \<Rightarrow> do tableSize <- return (pdBits - objBits makeObject);
addrs <- createObjects ptr (Suc (length as)) (injectKOS makeObject) tableSize;
pts <- return (map (PPtr \<circ> fromPPtr) addrs);
do objSize <- return (1 `~shiftL~` pdBits);
mapM_x copyGlobalMappings pts;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + fromIntegral objSize - 1) (addrFromPPtr x)) pts
od;
return $ map (\<lambda>pt. arch_capability.PageDirectoryCap pt Nothing) pts
od;
return $ map capability.ArchObjectCap archCaps
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral (Suc (length as)) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc (length as)) (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr (Suc (length as)) (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr (Suc (length as)) (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr (Suc (length as)) (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>r s. \<forall>cap\<in>set r. cap \<noteq> capability.NullCap\<rbrace>