theory Retype_C

lemma createObject_cnodes_have_size:
  "\<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits newType userSize)
      \<and> cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s)\<rbrace>
    createObject newType ptr userSize dev
  \<lbrace>\<lambda>rv s. cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s)\<rbrace>" apply (simp add: createObject_def) apply (rule hoare_pre) apply (wp mapM_x_wp' | wpc | simp add: createObjects_def)+ apply (cases newType, simp_all add: ARM_H.toAPIType_def) apply (clarsimp simp: APIType_capBits_def objBits_simps'
                              cnodes_retype_have_size_def cte_level_bits_def
                       split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits newType userSize) \<and> cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s)\<rbrace> global.createObject newType ptr userSize dev \<lbrace>\<lambda>rv s. cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits newType userSize) \<and> cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s)\<rbrace> case toAPIType newType of None \<Rightarrow> do archCap <- Arch.createObject newType ptr userSize dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) userSize 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 userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) userSize 0 0
od \<lbrace>\<lambda>rv s. cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> case toAPIType newType of None \<Rightarrow> do archCap <- Arch.createObject newType ptr userSize dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) userSize 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 userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) userSize 0 0
od \<lbrace>\<lambda>rv s. cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s)\<rbrace>
 2. \<And>s. is_aligned ptr (APIType_capBits newType userSize) \<and> cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s) \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. is_aligned ptr (APIType_capBits newType userSize) \<and> cnodes_retype_have_size R (APIType_capBits newType userSize) (gsCNodes s) \<Longrightarrow> toAPIType newType = Some ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> cnodes_retype_have_size R (APIType_capBits newType userSize) (\<lambda>y. if y = ptr then Just userSize else gsCNodes s y) proof (prove)
goal (1 subgoal):
 1. \<And>s x1. \<lbrakk>is_aligned ptr (APIType_capBits (APIObjectType x1) userSize) \<and> cnodes_retype_have_size R (APIType_capBits (APIObjectType x1) userSize) (gsCNodes s); newType = APIObjectType x1\<rbrakk> \<Longrightarrow> x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> cnodes_retype_have_size R (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) userSize) (\<lambda>y. if y = ptr then Just userSize else gsCNodes s y) proof (prove)
goal:
No subgoals!