theory Detype_R

lemma createObject_setCTE_commute:
  "monad_commute
     (cte_wp_at' (\<lambda>_. True) src and
        pspace_aligned' and pspace_distinct' and
        pspace_no_overlap' ptr (Types_H.getObjectSize ty us) and
        valid_arch_state' and K (ptr \<noteq> src) and
        K (is_aligned ptr (Types_H.getObjectSize ty us)) and
        K (Types_H.getObjectSize ty us < word_bits))
     (RetypeDecls_H.createObject ty ptr us d)
     (setCTE src cte)" apply (rule commute_grab_asm)+ apply (subgoal_tac "ptr && mask (Types_H.getObjectSize ty us) = 0") prefer 2 apply (clarsimp simp: range_cover_def is_aligned_mask) apply (clarsimp simp: createObject_def) apply (case_tac ty,
         simp_all add: ARM_H.toAPIType_def) apply (rename_tac apiobject_type) apply (case_tac apiobject_type) apply (simp_all add:
                       ARM_H.getObjectSize_def apiGetObjectSize_def
                       tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def
                       cteSizeBits_def)
            \<comment> \<open>Untyped\<close> apply (simp add: monad_commute_guard_imp[OF return_commute])
           \<comment> \<open>TCB, EP, NTFN\<close> apply (rule monad_commute_guard_imp[OF commute_commute]) apply (rule monad_commute_split[OF monad_commute_split]) apply (rule monad_commute_split[OF commute_commute[OF return_commute]]) apply (rule setCTE_modify_tcbDomain_commute) apply wp apply (rule curDomain_commute) apply wp+ apply (rule setCTE_placeNewObject_commute) apply (wp  placeNewObject_tcb_at' placeNewObject_cte_wp_at'
              placeNewObject_pspace_distinct'
              placeNewObject_pspace_aligned'
              | clarsimp simp: objBits_simps')+ apply (rule monad_commute_guard_imp[OF commute_commute]
            ,rule monad_commute_split[OF commute_commute[OF return_commute]]
            ,rule setCTE_placeNewObject_commute
            ,(wp|clarsimp simp: objBits_simps')+)+
        \<comment> \<open>CNode\<close> apply (rule monad_commute_guard_imp[OF commute_commute]) apply (rule monad_commute_split)+ apply (rule return_commute[THEN commute_commute]) apply (rule setCTE_modify_gsCNode_commute[of \<top>]) apply (rule hoare_triv[of \<top>]) apply wp apply (rule setCTE_placeNewObject_commute) apply (wp|clarsimp simp: objBits_simps')+
       \<comment> \<open>Arch Objects\<close> apply ((rule monad_commute_guard_imp[OF commute_commute]
              , rule monad_commute_split[OF commute_commute[OF return_commute]]
              , clarsimp simp: ARM_H.createObject_def
                               placeNewDataObject_def bind_assoc split
                          del: if_splits
              ,(rule monad_commute_split return_commute[THEN commute_commute]
                     setCTE_modify_gsUserPages_commute[of \<top>]
                     modify_wp[of "%_. \<top>"]
                     setCTE_doMachineOp_commute
                     setCTE_placeNewObject_commute
                     monad_commute_if_weak_r
                     copyGlobalMappings_setCTE_commute[THEN commute_commute]
                 | wp placeNewObject_pspace_distinct'
                      placeNewObject_pspace_aligned'
                      placeNewObject_cte_wp_at'
                      placeNewObject_valid_arch_state placeNewObject_pd_at'
                 | erule is_aligned_weaken
                 | simp add: objBits_simps pageBits_def ptBits_def pdBits_def
                             pdeBits_def pdBits_def pteBits_def
                             archObjSize_def split del: if_splits)+)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state' and K (ptr \<noteq> src) and K (is_aligned ptr (getObjectSize ty us)) and K (getObjectSize ty us < word_bits)) (global.createObject ty ptr us d) (setCTE src cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getObjectSize ty us < word_bits; is_aligned ptr (getObjectSize ty us); ptr \<noteq> src\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state') (global.createObject ty ptr us d) (setCTE src cte) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>getObjectSize ty us < word_bits; is_aligned ptr (getObjectSize ty us); ptr \<noteq> src; ptr && mask (getObjectSize ty us) = 0\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state') (global.createObject ty ptr us d) (setCTE src cte)
 2. \<lbrakk>getObjectSize ty us < word_bits; is_aligned ptr (getObjectSize ty us); ptr \<noteq> src\<rbrakk> \<Longrightarrow> ptr && mask (getObjectSize ty us) = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>getObjectSize ty us < word_bits; is_aligned ptr (getObjectSize ty us); ptr \<noteq> src\<rbrakk> \<Longrightarrow> ptr && mask (getObjectSize ty us) = 0
 2. \<lbrakk>getObjectSize ty us < word_bits; is_aligned ptr (getObjectSize ty us); ptr \<noteq> src; ptr && mask (getObjectSize ty us) = 0\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state') (global.createObject ty ptr us d) (setCTE src cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getObjectSize ty us < word_bits; is_aligned ptr (getObjectSize ty us); ptr \<noteq> src; ptr && mask (getObjectSize ty us) = 0\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state') (global.createObject ty ptr us d) (setCTE src cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getObjectSize ty us < word_bits; is_aligned ptr (getObjectSize ty us); ptr \<noteq> src; ptr && mask (getObjectSize ty us) = 0\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize ty us) and valid_arch_state') (case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us d;
return (capability.ArchObjectCap archCap)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od) (setCTE src cte) proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>getObjectSize (APIObjectType x1) us < word_bits; is_aligned ptr (getObjectSize (APIObjectType x1) us); ptr \<noteq> src; ptr && mask (getObjectSize (APIObjectType x1) us) = 0; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize (APIObjectType x1) us) and valid_arch_state') (case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od) (setCTE src cte)
 2. \<lbrakk>getObjectSize SmallPageObject us < word_bits; is_aligned ptr (getObjectSize SmallPageObject us); ptr \<noteq> src; ptr && mask (getObjectSize SmallPageObject us) = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SmallPageObject us) and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 3. \<lbrakk>getObjectSize LargePageObject us < word_bits; is_aligned ptr (getObjectSize LargePageObject us); ptr \<noteq> src; ptr && mask (getObjectSize LargePageObject us) = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize LargePageObject us) and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 4. \<lbrakk>getObjectSize SectionObject us < word_bits; is_aligned ptr (getObjectSize SectionObject us); ptr \<noteq> src; ptr && mask (getObjectSize SectionObject us) = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SectionObject us) and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 5. \<lbrakk>getObjectSize SuperSectionObject us < word_bits; is_aligned ptr (getObjectSize SuperSectionObject us); ptr \<noteq> src; ptr && mask (getObjectSize SuperSectionObject us) = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SuperSectionObject us) and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>getObjectSize PageTableObject us < word_bits; is_aligned ptr (getObjectSize PageTableObject us); ptr \<noteq> src; ptr && mask (getObjectSize PageTableObject us) = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize PageTableObject us) and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>getObjectSize PageDirectoryObject us < word_bits; is_aligned ptr (getObjectSize PageDirectoryObject us); ptr \<noteq> src; ptr && mask (getObjectSize PageDirectoryObject us) = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize PageDirectoryObject us) and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (7 subgoals):
 1. \<And>apiobject_type. \<lbrakk>getObjectSize (APIObjectType apiobject_type) us < word_bits; is_aligned ptr (getObjectSize (APIObjectType apiobject_type) us); ptr \<noteq> src; ptr && mask (getObjectSize (APIObjectType apiobject_type) us) = 0; ty = APIObjectType apiobject_type\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize (APIObjectType apiobject_type) us) and valid_arch_state') (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od) (setCTE src cte)
 2. \<lbrakk>getObjectSize SmallPageObject us < word_bits; is_aligned ptr (getObjectSize SmallPageObject us); ptr \<noteq> src; ptr && mask (getObjectSize SmallPageObject us) = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SmallPageObject us) and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 3. \<lbrakk>getObjectSize LargePageObject us < word_bits; is_aligned ptr (getObjectSize LargePageObject us); ptr \<noteq> src; ptr && mask (getObjectSize LargePageObject us) = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize LargePageObject us) and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 4. \<lbrakk>getObjectSize SectionObject us < word_bits; is_aligned ptr (getObjectSize SectionObject us); ptr \<noteq> src; ptr && mask (getObjectSize SectionObject us) = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SectionObject us) and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 5. \<lbrakk>getObjectSize SuperSectionObject us < word_bits; is_aligned ptr (getObjectSize SuperSectionObject us); ptr \<noteq> src; ptr && mask (getObjectSize SuperSectionObject us) = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SuperSectionObject us) and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>getObjectSize PageTableObject us < word_bits; is_aligned ptr (getObjectSize PageTableObject us); ptr \<noteq> src; ptr && mask (getObjectSize PageTableObject us) = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize PageTableObject us) and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>getObjectSize PageDirectoryObject us < word_bits; is_aligned ptr (getObjectSize PageDirectoryObject us); ptr \<noteq> src; ptr && mask (getObjectSize PageDirectoryObject us) = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize PageDirectoryObject us) and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type. \<lbrakk>getObjectSize (APIObjectType apiobject_type) us < word_bits; is_aligned ptr (getObjectSize (APIObjectType apiobject_type) us); ptr \<noteq> src; ptr && mask (getObjectSize (APIObjectType apiobject_type) us) = 0; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize (APIObjectType apiobject_type) us) and valid_arch_state') (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od) (setCTE src cte)
 2. \<And>apiobject_type. \<lbrakk>getObjectSize (APIObjectType apiobject_type) us < word_bits; is_aligned ptr (getObjectSize (APIObjectType apiobject_type) us); ptr \<noteq> src; ptr && mask (getObjectSize (APIObjectType apiobject_type) us) = 0; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize (APIObjectType apiobject_type) us) and valid_arch_state') (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od) (setCTE src cte)
 3. \<And>apiobject_type. \<lbrakk>getObjectSize (APIObjectType apiobject_type) us < word_bits; is_aligned ptr (getObjectSize (APIObjectType apiobject_type) us); ptr \<noteq> src; ptr && mask (getObjectSize (APIObjectType apiobject_type) us) = 0; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize (APIObjectType apiobject_type) us) and valid_arch_state') (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od) (setCTE src cte)
 4. \<And>apiobject_type. \<lbrakk>getObjectSize (APIObjectType apiobject_type) us < word_bits; is_aligned ptr (getObjectSize (APIObjectType apiobject_type) us); ptr \<noteq> src; ptr && mask (getObjectSize (APIObjectType apiobject_type) us) = 0; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize (APIObjectType apiobject_type) us) and valid_arch_state') (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od) (setCTE src cte)
 5. \<And>apiobject_type. \<lbrakk>getObjectSize (APIObjectType apiobject_type) us < word_bits; is_aligned ptr (getObjectSize (APIObjectType apiobject_type) us); ptr \<noteq> src; ptr && mask (getObjectSize (APIObjectType apiobject_type) us) = 0; ty = APIObjectType apiobject_type; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize (APIObjectType apiobject_type) us) and valid_arch_state') (case apiobject_type of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap d (PPtr $ fromPPtr ptr) us 0 | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od) (setCTE src cte)
 6. \<lbrakk>getObjectSize SmallPageObject us < word_bits; is_aligned ptr (getObjectSize SmallPageObject us); ptr \<noteq> src; ptr && mask (getObjectSize SmallPageObject us) = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SmallPageObject us) and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>getObjectSize LargePageObject us < word_bits; is_aligned ptr (getObjectSize LargePageObject us); ptr \<noteq> src; ptr && mask (getObjectSize LargePageObject us) = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize LargePageObject us) and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>getObjectSize SectionObject us < word_bits; is_aligned ptr (getObjectSize SectionObject us); ptr \<noteq> src; ptr && mask (getObjectSize SectionObject us) = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SectionObject us) and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>getObjectSize SuperSectionObject us < word_bits; is_aligned ptr (getObjectSize SuperSectionObject us); ptr \<noteq> src; ptr && mask (getObjectSize SuperSectionObject us) = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize SuperSectionObject us) and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>getObjectSize PageTableObject us < word_bits; is_aligned ptr (getObjectSize PageTableObject us); ptr \<noteq> src; ptr && mask (getObjectSize PageTableObject us) = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (getObjectSize PageTableObject us) and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type. \<lbrakk>us < word_bits; is_aligned ptr us; ptr \<noteq> src; ptr && mask us = 0; ty = APIObjectType ArchTypes_H.apiobject_type.Untyped; apiobject_type = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr us and valid_arch_state') (return (capability.UntypedCap d ptr us 0)) (setCTE src cte)
 2. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
curdom <- curDomain;
y <- threadSet (tcbDomain_update (\<lambda>_. curdom)) ptr;
return (capability.ThreadCap ptr)
od) (setCTE src cte)
 3. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 4. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 5. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 6. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
curdom <- curDomain;
y <- threadSet (tcbDomain_update (\<lambda>_. curdom)) ptr;
return (capability.ThreadCap ptr)
od) (setCTE src cte)
 2. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 3. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 4. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 5. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P9 apiobject_type) (setCTE src cte) (do y <- placeNewObject ptr makeObject 0;
curdom <- curDomain;
y <- threadSet (tcbDomain_update (\<lambda>_. curdom)) ptr;
return (capability.ThreadCap ptr)
od)
 2. \<And>apiobject_type s. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') s\<rbrakk> \<Longrightarrow> ?P9 apiobject_type s
 3. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 4. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 5. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 6. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 11 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>apiobject_type y ra. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?Q14 apiobject_type y ra) (setCTE src cte) (do y <- threadSet (tcbDomain_update (\<lambda>_. ra)) ptr;
return (capability.ThreadCap ptr)
od)
 2. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P14 apiobject_type y) (setCTE src cte) curDomain
 3. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 apiobject_type y\<rbrace> curDomain \<lbrace>?Q14 apiobject_type y\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P13 apiobject_type) (setCTE src cte) (placeNewObject ptr makeObject 0)
 5. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 apiobject_type\<rbrace> placeNewObject ptr makeObject 0 \<lbrace>\<lambda>y. ?P14 apiobject_type y and ?P'14 apiobject_type y\<rbrace>
 6. \<And>apiobject_type s. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P13 apiobject_type and ?P'13 apiobject_type) s
 7. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 8. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 9. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 10. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 15 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>apiobject_type y ra. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P20 apiobject_type y ra) (setCTE src cte) (threadSet (tcbDomain_update (\<lambda>_. ra)) ptr)
 2. \<And>apiobject_type y ra. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'20 apiobject_type y ra\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P14 apiobject_type y) (setCTE src cte) curDomain
 4. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 apiobject_type y\<rbrace> curDomain \<lbrace>\<lambda>ya. ?P20 apiobject_type y ya and ?P'20 apiobject_type y ya\<rbrace>
 5. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P13 apiobject_type) (setCTE src cte) (placeNewObject ptr makeObject 0)
 6. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 apiobject_type\<rbrace> placeNewObject ptr makeObject 0 \<lbrace>\<lambda>y. ?P14 apiobject_type y and ?P'14 apiobject_type y\<rbrace>
 7. \<And>apiobject_type s. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P13 apiobject_type and ?P'13 apiobject_type) s
 8. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 9. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 10. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>apiobject_type y ra. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'20 apiobject_type y ra\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ra)) ptr \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P14 apiobject_type y) (setCTE src cte) curDomain
 3. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 apiobject_type y\<rbrace> curDomain \<lbrace>\<lambda>ya. tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and ?P'20 apiobject_type y ya\<rbrace>
 4. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P13 apiobject_type) (setCTE src cte) (placeNewObject ptr makeObject 0)
 5. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 apiobject_type\<rbrace> placeNewObject ptr makeObject 0 \<lbrace>\<lambda>y. ?P14 apiobject_type y and ?P'14 apiobject_type y\<rbrace>
 6. \<And>apiobject_type s. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P13 apiobject_type and ?P'13 apiobject_type) s
 7. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 8. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 9. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 10. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P14 apiobject_type y) (setCTE src cte) curDomain
 2. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 apiobject_type y\<rbrace> curDomain \<lbrace>\<lambda>y. tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and (\<lambda>s. True)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P13 apiobject_type) (setCTE src cte) (placeNewObject ptr makeObject 0)
 4. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 apiobject_type\<rbrace> placeNewObject ptr makeObject 0 \<lbrace>\<lambda>y. ?P14 apiobject_type y and ?P'14 apiobject_type y\<rbrace>
 5. \<And>apiobject_type s. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P13 apiobject_type and ?P'13 apiobject_type) s
 6. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 7. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 8. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 9. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>apiobject_type y P. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setCTE src cte \<lbrace>\<lambda>r s. P (ksCurDomain s)\<rbrace>
 2. \<And>apiobject_type y. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'14 apiobject_type y\<rbrace> curDomain \<lbrace>\<lambda>y. tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and (\<lambda>s. True)\<rbrace>
 3. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P13 apiobject_type) (setCTE src cte) (placeNewObject ptr makeObject 0)
 4. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 apiobject_type\<rbrace> placeNewObject ptr makeObject 0 \<lbrace>\<lambda>y. (\<lambda>_. True) and ?P'14 apiobject_type y\<rbrace>
 5. \<And>apiobject_type s. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P13 apiobject_type and ?P'13 apiobject_type) s
 6. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 7. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 8. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 9. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 14 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> monad_commute (?P13 apiobject_type) (setCTE src cte) (placeNewObject ptr makeObject 0)
 2. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 apiobject_type\<rbrace> placeNewObject ptr makeObject 0 \<lbrace>\<lambda>y. (\<lambda>_. True) and (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and (\<lambda>s. True))\<rbrace>
 3. \<And>apiobject_type s. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P13 apiobject_type and ?P'13 apiobject_type) s
 4. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 5. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 6. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 7. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>apiobject_type. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'13 apiobject_type\<rbrace> placeNewObject ptr makeObject 0 \<lbrace>\<lambda>y. (\<lambda>_. True) and (tcb_at' ptr and cte_wp_at' (\<lambda>_. True) src and pspace_distinct' and pspace_aligned' and (\<lambda>s. True))\<rbrace>
 2. \<And>apiobject_type s. \<lbrakk>9 < word_bits; is_aligned ptr 9; ptr \<noteq> src; ptr && mask 9 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject; apiobject_type = ArchTypes_H.apiobject_type.TCBObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 9 and valid_arch_state') s\<rbrakk> \<Longrightarrow> (K (is_aligned ptr (objBitsKO (injectKOS makeObject) + 0) \<and> objBitsKO (injectKOS makeObject) + 0 < word_bits) and K (ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS makeObject) + 0) and ?P'13 apiobject_type) s
 3. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject; apiobject_type = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 4. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 5. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 6. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (setCTE src cte)
 2. \<And>apiobject_type. \<lbrakk>4 < word_bits; is_aligned ptr 4; ptr \<noteq> src; ptr && mask 4 = 0; ty = APIObjectType ArchTypes_H.apiobject_type.NotificationObject; apiobject_type = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 4 and valid_arch_state') (do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od) (setCTE src cte)
 3. \<And>apiobject_type. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; apiobject_type = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 4. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 5. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (setCTE src cte)
 2. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 3. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 4. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 5. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute ?P93 (setCTE src cte) (do y <- placeNewObject ptr makeObject us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od)
 2. \<And>s. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') s\<rbrakk> \<Longrightarrow> ?P93 s
 3. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 4. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 5. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (12 subgoals):
 1. \<And>r ra. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (?Q101 r ra) (setCTE src cte) (return (capability.CNodeCap ptr us 0 0))
 2. \<And>r. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (?P101 r) (setCTE src cte) (modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>))
 3. \<And>r. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'101 r\<rbrace> modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>) \<lbrace>?Q101 r\<rbrace>
 4. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute ?P97 (setCTE src cte) (placeNewObject ptr makeObject us)
 5. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'97\<rbrace> placeNewObject ptr makeObject us \<lbrace>\<lambda>r. ?P101 r and ?P'101 r\<rbrace>
 6. \<And>s. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P97 and ?P'97) s
 7. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>r. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute (?P101 r) (setCTE src cte) (modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>))
 2. \<And>r. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'101 r\<rbrace> modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute ?P97 (setCTE src cte) (placeNewObject ptr makeObject us)
 4. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'97\<rbrace> placeNewObject ptr makeObject us \<lbrace>\<lambda>r. ?P101 r and ?P'101 r\<rbrace>
 5. \<And>s. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P97 and ?P'97) s
 6. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>r. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'101 r\<rbrace> modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute ?P97 (setCTE src cte) (placeNewObject ptr makeObject us)
 3. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'97\<rbrace> placeNewObject ptr makeObject us \<lbrace>\<lambda>r. (\<lambda>_. True) and ?P'101 r\<rbrace>
 4. \<And>s. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P97 and ?P'97) s
 5. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (10 subgoals):
 1. \<And>r. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute ?P97 (setCTE src cte) (placeNewObject ptr makeObject us)
 3. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'97\<rbrace> placeNewObject ptr makeObject us \<lbrace>\<lambda>r. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 4. \<And>s. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P97 and ?P'97) s
 5. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 10. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> monad_commute ?P97 (setCTE src cte) (placeNewObject ptr makeObject us)
 2. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'97\<rbrace> placeNewObject ptr makeObject us \<lbrace>\<lambda>r. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 3. \<And>s. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') s\<rbrakk> \<Longrightarrow> (?P97 and ?P'97) s
 4. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 5. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 9. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?P'97\<rbrace> placeNewObject ptr makeObject us \<lbrace>\<lambda>r. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 2. \<And>s. \<lbrakk>4 + us < word_bits; is_aligned ptr (4 + us); ptr \<noteq> src; ptr && mask (4 + us) = 0; ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (4 + us) and valid_arch_state') s\<rbrakk> \<Longrightarrow> (K (is_aligned ptr (objBitsKO (injectKOS makeObject) + us) \<and> objBitsKO (injectKOS makeObject) + us < word_bits) and K (ptr \<noteq> src) and cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBitsKO (injectKOS makeObject) + us) and ?P'97) s
 3. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 4. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 5. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 7. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 8. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>12 < word_bits; is_aligned ptr 12; ptr \<noteq> src; ptr && mask 12 = 0; ty = SmallPageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 12 and valid_arch_state') (do archCap <- Arch.createObject SmallPageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 2. \<lbrakk>16 < word_bits; is_aligned ptr 16; ptr \<noteq> src; ptr && mask 16 = 0; ty = LargePageObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 16 and valid_arch_state') (do archCap <- Arch.createObject LargePageObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 3. \<lbrakk>20 < word_bits; is_aligned ptr 20; ptr \<noteq> src; ptr && mask 20 = 0; ty = SectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 20 and valid_arch_state') (do archCap <- Arch.createObject SectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 4. \<lbrakk>24 < word_bits; is_aligned ptr 24; ptr \<noteq> src; ptr && mask 24 = 0; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr 24 and valid_arch_state') (do archCap <- Arch.createObject SuperSectionObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 5. \<lbrakk>ptBits < word_bits; is_aligned ptr ptBits; ptr \<noteq> src; ptr && mask ptBits = 0; ty = PageTableObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr ptBits and valid_arch_state') (do archCap <- Arch.createObject PageTableObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte)
 6. \<lbrakk>pdBits < word_bits; is_aligned ptr pdBits; ptr \<noteq> src; ptr && mask pdBits = 0; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> monad_commute (cte_wp_at' (\<lambda>_. True) src and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr pdBits and valid_arch_state') (do archCap <- Arch.createObject PageDirectoryObject ptr us d;
return (capability.ArchObjectCap archCap)
od) (setCTE src cte) proof (prove)
goal:
No subgoals!