theory ArchIpc_AI

lemma arch_derive_cap_is_derived:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap . cap_master_cap cap =
                          cap_master_cap (ArchObjectCap c') \<and>
                          cap_aligned cap \<and>
                          cap_asid cap = cap_asid (ArchObjectCap c') \<and>
                          vs_cap_ref cap = vs_cap_ref (ArchObjectCap c')) p s\<rbrace>
     arch_derive_cap c'
   \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, -" unfolding arch_derive_cap_def apply(cases c', simp_all add: is_cap_simps cap_master_cap_def) apply((wp throwError_validE_R
             | clarsimp simp: is_derived_def
                              is_cap_simps cap_master_cap_def
                              cap_aligned_def is_aligned_no_overflow is_pt_cap_def
                              cap_asid_def vs_cap_ref_def
             | erule cte_wp_at_weakenE
             | simp split: arch_cap.split_asm cap.split_asm option.splits
             | rule conjI)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ArchObjectCap c') \<and> cap_aligned cap \<and> cap_asid cap = cap_asid (ArchObjectCap c') \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap c')) p\<rbrace> arch_derive_cap c' \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ArchObjectCap c') \<and> cap_aligned cap \<and> cap_asid cap = cap_asid (ArchObjectCap c') \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap c')) p\<rbrace> case c' of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap c') | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap c') | _ \<Rightarrow> returnOk (ArchObjectCap c') \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. c' = ASIDPoolCap x11 x12 \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>cap. (case cap of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap ref \<Rightarrow> ThreadCap ref | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) | _ \<Rightarrow> cap) = ArchObjectCap (ASIDPoolCap x11 0) \<and> cap_aligned cap \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap (ASIDPoolCap x11 x12))) p\<rbrace> returnOk (ArchObjectCap (ASIDPoolCap x11 x12)) \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, -
 2. c' = ASIDControlCap \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>cap. (case cap of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap ref \<Rightarrow> ThreadCap ref | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) | _ \<Rightarrow> cap) = ArchObjectCap ASIDControlCap \<and> cap_aligned cap \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap ASIDControlCap)) p\<rbrace> returnOk (ArchObjectCap ASIDControlCap) \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, -
 3. \<And>x31 x32 x33 x34 x35. c' = PageCap x31 x32 x33 x34 x35 \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>cap. (case cap of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap ref \<Rightarrow> ThreadCap ref | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) | _ \<Rightarrow> cap) = ArchObjectCap (PageCap x31 x32 UNIV x34 None) \<and> cap_aligned cap \<and> cap_asid cap = cap_asid (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) p\<rbrace> returnOk (ArchObjectCap (PageCap x31 x32 x33 x34 None)) \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, -
 4. \<And>x41 x42. c' = PageTableCap x41 x42 \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>cap. (case cap of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap ref \<Rightarrow> ThreadCap ref | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) | _ \<Rightarrow> cap) = ArchObjectCap (PageTableCap x41 None) \<and> cap_aligned cap \<and> cap_asid cap = cap_asid (ArchObjectCap (PageTableCap x41 x42)) \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap (PageTableCap x41 x42))) p\<rbrace> case x42 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (PageTableCap x41 x42)) \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, -
 5. \<And>x51 x52. c' = PageDirectoryCap x51 x52 \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>cap. (case cap of UntypedCap dev ref n f \<Rightarrow> UntypedCap dev ref n 0 | EndpointCap ref bdg rghts \<Rightarrow> EndpointCap ref 0 UNIV | NotificationCap ref bdg rghts \<Rightarrow> NotificationCap ref 0 UNIV | ReplyCap ref master rghts \<Rightarrow> ReplyCap ref True UNIV | CNodeCap ref bits gd \<Rightarrow> CNodeCap ref bits [] | ThreadCap ref \<Rightarrow> ThreadCap ref | DomainCap \<Rightarrow> DomainCap | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of ASIDPoolCap pool asid \<Rightarrow> ASIDPoolCap pool 0 | ASIDControlCap \<Rightarrow> acap | PageCap dev ref rghts sz mapdata \<Rightarrow> PageCap dev ref UNIV sz None | PageTableCap ptr data \<Rightarrow> PageTableCap ptr None | PageDirectoryCap ptr data \<Rightarrow> PageDirectoryCap ptr None) | _ \<Rightarrow> cap) = ArchObjectCap (PageDirectoryCap x51 None) \<and> cap_aligned cap \<and> cap_asid cap = cap_asid (ArchObjectCap (PageDirectoryCap x51 x52)) \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap (PageDirectoryCap x51 x52))) p\<rbrace> case x52 of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk (ArchObjectCap (PageDirectoryCap x51 x52)) \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, - proof (prove)
goal:
No subgoals!