theory ArchIpc_AI

lemma derive_cap_is_derived [Ipc_AI_assms]:
  "\<lbrace>\<lambda>s. c'\<noteq> cap.NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap c'
                     \<and> (cap_badge cap, cap_badge c') \<in> capBadge_ordering False
                     \<and> cap_asid cap = cap_asid c'
                     \<and> vs_cap_ref cap = vs_cap_ref c') slot s
       \<and> valid_objs s\<rbrace>
  derive_cap slot c'
  \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow>
          cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -" unfolding derive_cap_def apply (cases c', simp_all add: is_cap_simps) apply ((wp ensure_no_children_wp
                    | clarsimp simp: is_derived_def is_cap_simps
                                     cap_master_cap_def bits_of_def
                                     same_object_as_def is_pt_cap_def
                                     cap_asid_def
                    | fold validE_R_def
                    | erule cte_wp_at_weakenE
                    | simp split: cap.split_asm)+)[11] apply(wp hoare_drop_imps arch_derive_cap_is_derived) apply(clarify, drule cte_wp_at_norm, clarify) apply(frule(1) cte_wp_at_valid_objs_valid_cap) apply(erule cte_wp_at_weakenE) apply(clarsimp simp: valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. c' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap c' \<and> (cap_badge cap, cap_badge c') \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid c' \<and> vs_cap_ref cap = vs_cap_ref c') slot s \<and> valid_objs s\<rbrace> derive_cap slot c' \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. c' \<noteq> NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap c' \<and> (cap_badge cap, cap_badge c') \<in> capBadge_ordering False \<and> cap_asid cap = cap_asid c' \<and> vs_cap_ref cap = vs_cap_ref c') slot s \<and> valid_objs s\<rbrace> case c' of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk c'
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk c' \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, - proof (prove)
goal (12 subgoals):
 1. c' = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 2. \<And>x21 x22 x23 x24. c' = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (UntypedCap x21 x22 x23 x24) \<and> cap_badge cap = None \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (UntypedCap x21 x22 x23 x24)) slot s \<and> valid_objs s\<rbrace> doE y <- ensure_no_children slot;
returnOk (UntypedCap x21 x22 x23 x24)
odE \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 3. \<And>x31 x32 x33. c' = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (EndpointCap x31 x32 x33) \<and> (cap_badge cap, Some x32) \<in> capBadge_ordering False \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (EndpointCap x31 x32 x33)) slot s \<and> valid_objs s\<rbrace> returnOk (EndpointCap x31 x32 x33) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 4. \<And>x41 x42 x43. c' = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (NotificationCap x41 x42 x43) \<and> (cap_badge cap, Some x42) \<in> capBadge_ordering False \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (NotificationCap x41 x42 x43)) slot s \<and> valid_objs s\<rbrace> returnOk (NotificationCap x41 x42 x43) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 5. \<And>x51 x52 x53. c' = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ReplyCap x51 x52 x53) \<and> cap_badge cap = None \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (ReplyCap x51 x52 x53)) slot s \<and> valid_objs s\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 6. \<And>x61 x62 x63. c' = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (CNodeCap x61 x62 x63) \<and> cap_badge cap = None \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (CNodeCap x61 x62 x63)) slot s \<and> valid_objs s\<rbrace> returnOk (CNodeCap x61 x62 x63) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 7. \<And>x7. c' = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ThreadCap x7) \<and> cap_badge cap = None \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (ThreadCap x7)) slot s \<and> valid_objs s\<rbrace> returnOk (ThreadCap x7) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 8. c' = DomainCap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap DomainCap \<and> cap_badge cap = None \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref DomainCap) slot s \<and> valid_objs s\<rbrace> returnOk DomainCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 9. c' = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap IRQControlCap \<and> cap_badge cap = None \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref IRQControlCap) slot s \<and> valid_objs s\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
 10. \<And>x10. c' = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (IRQHandlerCap x10) \<and> cap_badge cap = None \<and> cap_asid cap = None \<and> vs_cap_ref cap = vs_cap_ref (IRQHandlerCap x10)) slot s \<and> valid_objs s\<rbrace> returnOk (IRQHandlerCap x10) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x12. c' = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ArchObjectCap x12) \<and> cap_badge cap = None \<and> cap_asid cap = cap_asid (ArchObjectCap x12) \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap x12)) slot s \<and> valid_objs s\<rbrace> arch_derive_cap x12 \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>x12 s. \<lbrakk>c' = ArchObjectCap x12; cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ArchObjectCap x12) \<and> cap_badge cap = None \<and> cap_asid cap = cap_asid (ArchObjectCap x12) \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap x12)) slot s \<and> valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ArchObjectCap x12) \<and> cap_aligned cap \<and> cap_asid cap = cap_asid (ArchObjectCap x12) \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap x12)) slot s proof (prove)
goal (1 subgoal):
 1. \<And>x12 s c. \<lbrakk>c' = ArchObjectCap x12; valid_objs s; cte_wp_at ((=) c) slot s; cap_master_cap c = cap_master_cap (ArchObjectCap x12); cap_badge c = None; cap_asid c = cap_asid (ArchObjectCap x12); vs_cap_ref c = vs_cap_ref (ArchObjectCap x12)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ArchObjectCap x12) \<and> cap_aligned cap \<and> cap_asid cap = cap_asid (ArchObjectCap x12) \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap x12)) slot s proof (prove)
goal (1 subgoal):
 1. \<And>x12 s c. \<lbrakk>c' = ArchObjectCap x12; valid_objs s; cte_wp_at ((=) c) slot s; cap_master_cap c = cap_master_cap (ArchObjectCap x12); cap_badge c = None; cap_asid c = cap_asid (ArchObjectCap x12); vs_cap_ref c = vs_cap_ref (ArchObjectCap x12); \<exists>cap. c = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap (ArchObjectCap x12) \<and> cap_aligned cap \<and> cap_asid cap = cap_asid (ArchObjectCap x12) \<and> vs_cap_ref cap = vs_cap_ref (ArchObjectCap x12)) slot s proof (prove)
goal (1 subgoal):
 1. \<And>x12 s c ca. \<lbrakk>c' = ArchObjectCap x12; valid_objs s; cap_master_cap c = cap_master_cap (ArchObjectCap x12); cap_badge c = None; cap_asid c = cap_asid (ArchObjectCap x12); vs_cap_ref c = vs_cap_ref (ArchObjectCap x12); \<exists>cap. c = cap \<and> s \<turnstile> cap; c = ca\<rbrakk> \<Longrightarrow> cap_master_cap ca = cap_master_cap (ArchObjectCap x12) \<and> cap_aligned ca \<and> cap_asid ca = cap_asid (ArchObjectCap x12) \<and> vs_cap_ref ca = vs_cap_ref (ArchObjectCap x12) proof (prove)
goal:
No subgoals!