theory Detype_R

lemma createObject_pspace_no_overlap':
  "\<lbrace>\<lambda>s. pspace_no_overlap'
          (ptr + (of_nat n << APIType_capBits ty userSize)) sz s \<and>
        pspace_aligned' s \<and> pspace_distinct' s
        \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2)
        \<and> ptr \<noteq> 0\<rbrace>
   createObject ty (ptr + (of_nat n << APIType_capBits ty userSize)) userSize d
   \<lbrace>\<lambda>rv s. pspace_no_overlap'
             (ptr + (1 + of_nat n << APIType_capBits ty userSize)) sz s\<rbrace>" apply (rule hoare_pre) apply (clarsimp simp:createObject_def) apply wpc apply (wp ArchCreateObject_pspace_no_overlap') apply wpc apply wp apply (simp add:placeNewObject_def2) apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2
        | simp add: placeNewObject_def2 curDomain_def word_shiftl_add_distrib
        field_simps)+ apply (simp add:add.assoc[symmetric]) apply (wp createObjects'_pspace_no_overlap2
        [where n =0 and sz = sz,simplified]) apply (simp add:placeNewObject_def2) apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2
        | simp add: placeNewObject_def2 word_shiftl_add_distrib
        field_simps)+ apply (simp add:add.assoc[symmetric]) apply (wp createObjects'_pspace_no_overlap2
        [where n =0 and sz = sz,simplified]) apply (simp add:placeNewObject_def2) apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2
      | simp add: placeNewObject_def2 word_shiftl_add_distrib
      field_simps)+ apply (simp add:add.assoc[symmetric]) apply (wp createObjects'_pspace_no_overlap2
      [where n =0 and sz = sz,simplified]) apply (simp add:placeNewObject_def2) apply (wp doMachineOp_psp_no_overlap createObjects'_pspace_no_overlap2
     | simp add: placeNewObject_def2 word_shiftl_add_distrib
     field_simps)+ apply (simp add:add.assoc[symmetric]) apply (wp createObjects'_pspace_no_overlap2
     [where n =0 and sz = sz,simplified]) apply clarsimp apply (frule(1) range_cover_no_0[where p = n]) apply simp apply (frule pspace_no_overlap'_le2) apply (rule range_cover_compare_offset) apply simp+ apply (clarsimp simp:word_shiftl_add_distrib
              ,simp add:field_simps) apply (clarsimp simp:add.assoc[symmetric]) apply (rule range_cover_tail_mask[where n =0,simplified]) apply (drule range_cover_offset[rotated,where p = n]) apply simp apply (clarsimp simp:shiftl_t2n field_simps) apply (metis numeral_2_eq_2) apply (simp add:shiftl_t2n field_simps) apply (frule range_cover_offset[rotated,where p = n]) apply simp+ apply (auto simp: word_shiftl_add_distrib field_simps shiftl_t2n elim: range_cover_le,
    auto simp add: APIType_capBits_def fromAPIType_def objBits_def
        dest!: to_from_apiTypeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0\<rbrace> global.createObject ty (ptr + (word_of_nat n << APIType_capBits ty userSize)) userSize d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> global.createObject ty (ptr + (word_of_nat n << APIType_capBits ty userSize)) userSize d \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty (ptr + (word_of_nat n << APIType_capBits ty userSize)) userSize d;
return (capability.ArchObjectCap archCap)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)));
return $ capability.ThreadCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)))
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. toAPIType ty = None \<Longrightarrow> \<lbrace>?R18\<rbrace> do archCap <- Arch.createObject ty (ptr + (word_of_nat n << APIType_capBits ty userSize)) userSize d;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R19 x2\<rbrace> case x2 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)));
return $ capability.ThreadCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)))
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> ?R18 s) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R19 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x2. toAPIType ty = Some x2 \<Longrightarrow> \<lbrace>?R19 x2\<rbrace> case x2 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)));
return $ capability.ThreadCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)))
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> ?R19 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 d (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R36 x2\<rbrace> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)));
return $ capability.ThreadCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)))
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 x2\<rbrace> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<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 + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<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 + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 6. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<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 (5 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R36 x2\<rbrace> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)));
return $ capability.ThreadCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)))
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 x2\<rbrace> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 4. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 5. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz 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 (5 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.TCBObject; x2 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R36 ArchTypes_H.apiobject_type.TCBObject\<rbrace> do y <- createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOTCB makeObject) 0;
curdom <- curDomain;
y <- threadSet (tcbDomain_update (\<lambda>_. curdom)) (ptr + (word_of_nat n << APIType_capBits ty userSize));
return (capability.ThreadCap (ptr + (word_of_nat n << APIType_capBits ty userSize)))
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 x2\<rbrace> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 4. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 5. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz 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 (5 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.TCBObject; x2 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R36 (ds_id ArchTypes_H.apiobject_type.TCBObject)\<rbrace> createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOTCB makeObject) 0 \<lbrace>\<lambda>y. pspace_no_overlap' (ptr + ((word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 x2\<rbrace> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 4. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 5. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz 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 (5 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.TCBObject; x2 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R36 (ds_id ArchTypes_H.apiobject_type.TCBObject)\<rbrace> createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOTCB makeObject) 0 \<lbrace>\<lambda>y. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 x2\<rbrace> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 4. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 5. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz 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 (4 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 x2\<rbrace> do placeNewObject (ptr + (word_of_nat n << APIType_capBits ty userSize)) makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 4. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) 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 (4 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.EndpointObject; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 ArchTypes_H.apiobject_type.EndpointObject\<rbrace> do y <- createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOEndpoint makeObject) 0;
return (capability.EndpointCap (ptr + (word_of_nat n << APIType_capBits ty userSize)) 0 True True True True)
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 4. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) 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 (4 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.EndpointObject; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 (ds_id ArchTypes_H.apiobject_type.EndpointObject)\<rbrace> createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOEndpoint makeObject) 0 \<lbrace>\<lambda>y. pspace_no_overlap' (ptr + ((word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 4. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) 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 (4 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.EndpointObject; x2 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R35 (ds_id ArchTypes_H.apiobject_type.EndpointObject)\<rbrace> createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOEndpoint makeObject) 0 \<lbrace>\<lambda>y. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 4. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) 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 (3 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) 0 True True
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) 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 (3 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.NotificationObject; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 ArchTypes_H.apiobject_type.NotificationObject\<rbrace> do y <- createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KONotification makeObject) 0;
return (capability.NotificationCap (ptr + (word_of_nat n << APIType_capBits ty userSize)) 0 True True)
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) 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 (3 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.NotificationObject; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 (ds_id ArchTypes_H.apiobject_type.NotificationObject)\<rbrace> createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KONotification makeObject) 0 \<lbrace>\<lambda>y. pspace_no_overlap' (ptr + ((word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) 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 (3 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.NotificationObject; x2 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R34 (ds_id ArchTypes_H.apiobject_type.NotificationObject)\<rbrace> createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KONotification makeObject) 0 \<lbrace>\<lambda>y. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz\<rbrace>
 2. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 3. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) 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 (2 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some x2; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x2\<rbrace> do placeNewObject (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) makeObject userSize;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize)) then Just userSize else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr (ptr + (word_of_nat n << APIType_capBits ty userSize))) userSize 0 0
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KONotification makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R33 x s)) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.CapTableObject; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 ArchTypes_H.apiobject_type.CapTableObject\<rbrace> do y <- createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOCTE makeObject) userSize;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr + (word_of_nat n << APIType_capBits ty userSize) then Just userSize else gsCNodes ks y\<rparr>);
return (capability.CNodeCap (ptr + (word_of_nat n << APIType_capBits ty userSize)) userSize 0 0)
od \<lbrace>\<lambda>rv. pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KONotification makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R33 x s)) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.CapTableObject; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 (ds_id ArchTypes_H.apiobject_type.CapTableObject)\<rbrace> createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOCTE makeObject) userSize \<lbrace>\<lambda>y. pspace_no_overlap' (ptr + ((word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize)) sz\<rbrace>
 2. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KONotification makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R33 x s)) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>toAPIType ty = Some ArchTypes_H.apiobject_type.CapTableObject; x2 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R33 (ds_id ArchTypes_H.apiobject_type.CapTableObject)\<rbrace> createObjects' (ptr + (word_of_nat n << APIType_capBits ty userSize)) (Suc 0) (KOCTE makeObject) userSize \<lbrace>\<lambda>y. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz\<rbrace>
 2. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KONotification makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R33 x s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0 \<Longrightarrow> (toAPIType ty = None \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> range_cover ptr sz (APIType_capBits ty userSize) (n + 2) \<and> ptr \<noteq> 0) \<and> (\<forall>x. toAPIType ty = Some x \<longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KONotification makeObject) + 0) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> (pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz and (\<lambda>y. APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize) and (\<lambda>y. range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0)) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x\<rbrakk> \<Longrightarrow> n < Suc (Suc n)
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << APIType_capBits ty userSize) \<le> ?ptr'95 s x
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ?ptr'95 s x && ~~ mask sz = ptr + (word_of_nat n << APIType_capBits ty userSize) && ~~ mask sz
 3. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (?ptr'95 s x) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (5 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover ptr (?sz99 s x) (APIType_capBits ty userSize) (?t99 s x)
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> n + 1 < ?t99 s x
 3. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr \<noteq> 0
 4. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << APIType_capBits ty userSize) && ~~ mask sz = ptr + (word_of_nat n << APIType_capBits ty userSize) && ~~ mask sz
 5. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << APIType_capBits ty userSize) && ~~ mask sz = ptr + (word_of_nat n << APIType_capBits ty userSize) && ~~ mask sz
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + ((word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) && ~~ mask sz = ptr + (word_of_nat n << APIType_capBits ty userSize) && ~~ mask sz
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize && ~~ mask sz = ptr + (word_of_nat n << APIType_capBits ty userSize) && ~~ mask sz
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0))
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0
 3. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> n < Suc (Suc n)
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; range_cover (ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize) sz (APIType_capBits ty userSize) (Suc (Suc n) - n)\<rbrakk> \<Longrightarrow> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0))
 3. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0
 4. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; range_cover (ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize) sz (APIType_capBits ty userSize) (Suc (Suc n) - n)\<rbrakk> \<Longrightarrow> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0))
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0
 3. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize) sz s; pspace_aligned' s; pspace_distinct' s; ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; range_cover (ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize) sz (APIType_capBits ty userSize) 2\<rbrakk> \<Longrightarrow> range_cover (ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize) sz (APIType_capBits ty userSize) (Suc (Suc 0))
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0
 3. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s\<rbrakk> \<Longrightarrow> n < Suc (Suc n)
 2. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s; range_cover (ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize) sz (APIType_capBits ty userSize) (Suc (Suc n) - n)\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s) \<and> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz s; pspace_aligned' s; pspace_distinct' s; range_cover ptr sz (APIType_capBits ty userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType ty = Some x; ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize \<noteq> 0; pspace_no_overlap' (ptr + (1 + word_of_nat n << APIType_capBits ty userSize)) sz s; range_cover (ptr + word_of_nat n * 2 ^ APIType_capBits ty userSize) sz (APIType_capBits ty userSize) 2\<rbrakk> \<Longrightarrow> (x = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOTCB makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOEndpoint makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KONotification makeObject) \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) \<and> (x = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> pspace_no_overlap' (ptr + (word_of_nat n << APIType_capBits ty userSize) + 2 ^ APIType_capBits ty userSize) sz s \<and> APIType_capBits ty userSize = objBitsKO (KOCTE makeObject) + userSize \<and> range_cover (ptr + (word_of_nat n << APIType_capBits ty userSize)) sz (APIType_capBits ty userSize) (Suc (Suc 0)) \<and> ptr + (word_of_nat n << APIType_capBits ty userSize) \<noteq> 0) proof (prove)
goal:
No subgoals!