theory Retype_C

lemma createObject_gsCNodes_p:
  "\<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> createObject t ptr sz dev\<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>" apply (simp add: createObject_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> global.createObject t ptr sz 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 t of None \<Rightarrow> do archCap <- Arch.createObject t ptr sz dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) sz 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr 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 placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject sz;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just sz else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) sz 0 0
od \<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> case toAPIType t of None \<Rightarrow> do archCap <- Arch.createObject t ptr sz dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) sz 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr 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 placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject sz;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just sz else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) sz 0 0
od \<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>
 2. \<And>s. P (gsCNodes s p) \<and> p \<noteq> ptr \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!