theory Detype_R

lemma createObject_cte_wp_at':
  "\<lbrace>\<lambda>s. Types_H.getObjectSize ty us < word_bits \<and>
        is_aligned ptr (Types_H.getObjectSize ty us) \<and>
        pspace_no_overlap' ptr (Types_H.getObjectSize ty us) s \<and>
        cte_wp_at' (\<lambda>c. P c) slot s \<and> pspace_aligned' s \<and>
        pspace_distinct' s\<rbrace>
   RetypeDecls_H.createObject ty ptr us d
   \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>c. P c) slot s \<rbrace>" apply (simp add:createObject_def) apply (rule hoare_pre) apply (wpc
        | wp createObjects_orig_cte_wp_at'[where sz = "(Types_H.getObjectSize ty us)"]
             threadSet_cte_wp_at'
        | simp add: ARM_H.createObject_def placeNewDataObject_def
                    unless_def placeNewObject_def2 objBits_simps range_cover_full
                    curDomain_def pageBits_def ptBits_def
                    pdBits_def getObjSize_simps archObjSize_def
                    apiGetObjectSize_def tcbBlockSizeBits_def
                    epSizeBits_def ntfnSizeBits_def
                    cteSizeBits_def pteBits_def pdeBits_def
        | intro conjI impI | clarsimp dest!: arch_toAPIType_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. getObjectSize ty us < word_bits \<and> is_aligned ptr (getObjectSize ty us) \<and> pspace_no_overlap' ptr (getObjectSize ty us) s \<and> cte_wp_at' P slot s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> global.createObject ty ptr us d \<lbrace>\<lambda>r. cte_wp_at' P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. getObjectSize ty us < word_bits \<and> is_aligned ptr (getObjectSize ty us) \<and> pspace_no_overlap' ptr (getObjectSize ty us) s \<and> cte_wp_at' P slot s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> 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 \<lbrace>\<lambda>r. cte_wp_at' P slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q7\<rbrace> 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 \<lbrace>\<lambda>r. cte_wp_at' P slot\<rbrace>
 2. \<And>s. getObjectSize ty us < word_bits \<and> is_aligned ptr (getObjectSize ty us) \<and> pspace_no_overlap' ptr (getObjectSize ty us) s \<and> cte_wp_at' P slot s \<and> pspace_aligned' s \<and> pspace_distinct' s \<Longrightarrow> ?Q7 s proof (prove)
goal:
No subgoals!