theory Retype_C

lemma createObject_capRange:
shows "\<lbrace>P\<rbrace>createObject ty ptr us dev \<lbrace>\<lambda>m s. capRange m = {ptr.. ptr + 2 ^ (APIType_capBits ty us) - 1}\<rbrace>" apply (simp add:createObject_def) apply (case_tac "ty") apply (simp_all add:toAPIType_def ARM_H.toAPIType_def) apply (rule hoare_pre) apply wpc apply wp apply (simp add:split untypedRange.simps objBits_simps capRange_def APIType_capBits_def | wp)+ apply (simp add:ARM_H.createObject_def capRange_def APIType_capBits_def
         acapClass.simps | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x1. ty = APIObjectType x1 \<Longrightarrow> \<lbrace>P\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace>
 2. ty = object_type.SmallPageObject \<Longrightarrow> \<lbrace>P\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace>
 3. ty = object_type.LargePageObject \<Longrightarrow> \<lbrace>P\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace>
 4. ty = object_type.SectionObject \<Longrightarrow> \<lbrace>P\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace>
 5. ty = object_type.SuperSectionObject \<Longrightarrow> \<lbrace>P\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace>
 6. ty = object_type.PageTableObject \<Longrightarrow> \<lbrace>P\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace>
 7. ty = object_type.PageDirectoryObject \<Longrightarrow> \<lbrace>P\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits ty us - 1}\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x1. ty = APIObjectType x1 \<Longrightarrow> \<lbrace>P\<rbrace> case x1 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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 2. ty = object_type.SmallPageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SmallPageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SmallPageObject us - 1}\<rbrace>
 3. ty = object_type.LargePageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.LargePageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.LargePageObject us - 1}\<rbrace>
 4. ty = object_type.SectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SectionObject us - 1}\<rbrace>
 5. ty = object_type.SuperSectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SuperSectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SuperSectionObject us - 1}\<rbrace>
 6. ty = object_type.PageTableObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.PageTableObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.PageTableObject us - 1}\<rbrace>
 7. ty = object_type.PageDirectoryObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.PageDirectoryObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.PageDirectoryObject us - 1}\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x1. ty = APIObjectType x1 \<Longrightarrow> \<lbrace>?Q3 x1\<rbrace> case x1 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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 2. \<And>x1 s. \<lbrakk>ty = APIObjectType x1; P s\<rbrakk> \<Longrightarrow> ?Q3 x1 s
 3. ty = object_type.SmallPageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SmallPageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SmallPageObject us - 1}\<rbrace>
 4. ty = object_type.LargePageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.LargePageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.LargePageObject us - 1}\<rbrace>
 5. ty = object_type.SectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SectionObject us - 1}\<rbrace>
 6. ty = object_type.SuperSectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SuperSectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SuperSectionObject us - 1}\<rbrace>
 7. ty = object_type.PageTableObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.PageTableObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.PageTableObject us - 1}\<rbrace>
 8. ty = object_type.PageDirectoryObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.PageDirectoryObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.PageDirectoryObject us - 1}\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R17 x1\<rbrace> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 2. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R16 x1\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 3. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R15 x1\<rbrace> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 4. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R14 x1\<rbrace> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 5. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R13 x1\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 6. \<And>x1 s. \<lbrakk>ty = APIObjectType x1; P s\<rbrakk> \<Longrightarrow> (x1 = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> ?R17 x1 s) \<and> (x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> ?R16 x1 s) \<and> (x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> ?R15 x1 s) \<and> (x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> ?R14 x1 s) \<and> (x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R13 x1 s)
 7. ty = object_type.SmallPageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SmallPageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SmallPageObject us - 1}\<rbrace>
 8. ty = object_type.LargePageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.LargePageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.LargePageObject us - 1}\<rbrace>
 9. ty = object_type.SectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SectionObject us - 1}\<rbrace>
 10. ty = object_type.SuperSectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SuperSectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SuperSectionObject us - 1}\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R16 x1\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 2. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R15 x1\<rbrace> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 3. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R14 x1\<rbrace> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 4. \<And>x1. \<lbrakk>ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R13 x1\<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>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}\<rbrace>
 5. \<And>x1 s. \<lbrakk>ty = APIObjectType x1; P s\<rbrakk> \<Longrightarrow> (x1 = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> capRange (capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0) = {ptr..ptr + 2 ^ APIType_capBits (APIObjectType x1) us - 1}) \<and> (x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> ?R16 x1 s) \<and> (x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> ?R15 x1 s) \<and> (x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> ?R14 x1 s) \<and> (x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R13 x1 s)
 6. ty = object_type.SmallPageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SmallPageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SmallPageObject us - 1}\<rbrace>
 7. ty = object_type.LargePageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.LargePageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.LargePageObject us - 1}\<rbrace>
 8. ty = object_type.SectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SectionObject us - 1}\<rbrace>
 9. ty = object_type.SuperSectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SuperSectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SuperSectionObject us - 1}\<rbrace>
 10. ty = object_type.PageTableObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.PageTableObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.PageTableObject us - 1}\<rbrace>
A total of 11 subgoals... proof (prove)
goal (7 subgoals):
 1. ty = object_type.SmallPageObject \<Longrightarrow> \<lbrace>?Q58\<rbrace> Arch.createObject object_type.SmallPageObject ptr us dev \<lbrace>\<lambda>archCap a. (if acapClass archCap \<noteq> PhysicalClass then {} else {global.capUntypedPtr (capability.ArchObjectCap archCap)..global.capUntypedPtr (capability.ArchObjectCap archCap) + 2 ^ capBits (capability.ArchObjectCap archCap) - 1}) = {ptr..0xFFF + ptr}\<rbrace>
 2. \<And>s. \<lbrakk>ty = object_type.SmallPageObject; P s\<rbrakk> \<Longrightarrow> ?Q58 s
 3. ty = object_type.LargePageObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.LargePageObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.LargePageObject us - 1}\<rbrace>
 4. ty = object_type.SectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SectionObject us - 1}\<rbrace>
 5. ty = object_type.SuperSectionObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.SuperSectionObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.SuperSectionObject us - 1}\<rbrace>
 6. ty = object_type.PageTableObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.PageTableObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.PageTableObject us - 1}\<rbrace>
 7. ty = object_type.PageDirectoryObject \<Longrightarrow> \<lbrace>P\<rbrace> do archCap <- Arch.createObject object_type.PageDirectoryObject ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m s. capRange m = {ptr..ptr + 2 ^ APIType_capBits object_type.PageDirectoryObject us - 1}\<rbrace> proof (prove)
goal:
No subgoals!