theory Retype_C

lemma createNewCaps_1_gsCNodes_p:
  "\<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> createNewCaps newType ptr 1 n dev\<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>" apply (simp add: createNewCaps_def) apply (rule hoare_pre) apply (wp mapM_x_wp' | wpc | simp add: createObjects_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> createNewCaps newType ptr 1 n dev \<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> case toAPIType newType of None \<Rightarrow> do archCaps <- Arch_createNewCaps newType ptr (Suc 0) n dev;
return $ map capability.ArchObjectCap archCaps
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>na. capability.UntypedCap dev (ptr + na * 2 ^ fromIntegral n) n 0) [0 .e. fromIntegral (Suc 0) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 0) (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 0) (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 0) (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 0) (injectKOS makeObject) n;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just n else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr n 0 0) addrs
od \<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> case toAPIType newType of None \<Rightarrow> do archCaps <- Arch_createNewCaps newType ptr (Suc 0) n dev;
return $ map capability.ArchObjectCap archCaps
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>na. capability.UntypedCap dev (ptr + na * 2 ^ fromIntegral n) n 0) [0 .e. fromIntegral (Suc 0) - 1] | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr (Suc 0) (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 0) (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 0) (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 0) (injectKOS makeObject) n;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just n else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr n 0 0) addrs
od \<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>
 2. \<And>s. P (gsCNodes s p) \<and> p \<noteq> ptr \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!