theory Retype_C

lemma createObject_notZombie[wp]:
  "\<lbrace>\<top>\<rbrace>createObject ty ptr us dev \<lbrace>\<lambda>r s. \<not> isZombie r\<rbrace>" apply (rule hoare_pre) apply (simp add:createObject_def) apply wpc apply (wp| clarsimp simp add:isCap_simps)+ apply wpc apply (wp| clarsimp simp add:isCap_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>r s. \<not> isZombie r\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>r s. \<not> isZombie r\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 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 us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>r s. \<not> isZombie r\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. toAPIType ty = None \<Longrightarrow> \<lbrace>?R11\<rbrace> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od \<lbrace>\<lambda>r s. \<not> isZombie r\<rbrace>
 2. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R12 x2\<rbrace> case x2 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | 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 | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>r s. \<not> isZombie r\<rbrace>
 3. \<And>s. True \<Longrightarrow> (toAPIType ty = None \<longrightarrow> ?R11 s) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R12 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R12 x2\<rbrace> case x2 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | 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 | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>r s. \<forall>v0 v1 v2. r \<noteq> capability.Zombie v0 v1 v2\<rbrace>
 2. \<And>s. True \<Longrightarrow> (toAPIType ty = None \<longrightarrow> True) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R12 x s) proof (prove)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R37 x2\<rbrace> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 \<lbrace>\<lambda>r s. \<forall>v0 v1 v2. r \<noteq> capability.Zombie v0 v1 v2\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R36 x2\<rbrace> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od \<lbrace>\<lambda>r s. \<forall>v0 v1 v2. r \<noteq> capability.Zombie v0 v1 v2\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 x2\<rbrace> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od \<lbrace>\<lambda>r s. \<forall>v0 v1 v2. r \<noteq> capability.Zombie v0 v1 v2\<rbrace>
 4. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od \<lbrace>\<lambda>r s. \<forall>v0 v1 v2. r \<noteq> capability.Zombie v0 v1 v2\<rbrace>
 5. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>r s. \<forall>v0 v1 v2. r \<noteq> capability.Zombie v0 v1 v2\<rbrace>
 6. \<And>s. True \<Longrightarrow> (toAPIType ty = None \<longrightarrow> True) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> ?R37 x s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> ?R36 x s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> ?R35 x s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> ?R34 x s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R33 x s)) proof (prove)
goal:
No subgoals!