theory CNodeInv_AI

lemma cap_swap_fd_invs[wp]:
  "\<And>a b.
  \<lbrace>invs and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) a
        and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) b
        and (\<lambda>s. \<forall>c. tcb_cap_valid c a s)
        and (\<lambda>s. \<forall>c. tcb_cap_valid c b s)
        and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) a
        and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) b\<rbrace>
   cap_swap_for_delete a b \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp get_cap_wp) apply (clarsimp) apply (strengthen cap_irqs_appropriate_strengthen, simp) apply (rule conjI, fastforce dest: cte_wp_at_valid_objs_valid_cap) apply (rule conjI, fastforce dest: cte_wp_at_valid_objs_valid_cap) apply (clarsimp simp: cte_wp_at_caps_of_state weak_derived_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrace>invs and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) a and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) b and (\<lambda>s. \<forall>c. tcb_cap_valid c a s) and (\<lambda>s. \<forall>c. tcb_cap_valid c b s) and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) a and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) b\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrace>invs and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) a and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) b and (\<lambda>s. \<forall>c. tcb_cap_valid c a s) and (\<lambda>s. \<forall>c. tcb_cap_valid c b s) and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) a and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) b\<rbrace> when (a \<noteq> b) (do cap1 <- get_cap a;
cap2 <- get_cap b;
cap_swap cap1 a cap2 b
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b s. (invs and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) a and ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) b and (\<lambda>s. \<forall>c. tcb_cap_valid c a s) and (\<lambda>s. \<forall>c. tcb_cap_valid c b s) and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) a and cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) b) s \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> (invs and ex_cte_cap_wp_to (appropriate_cte_cap capa) a and ex_cte_cap_wp_to (appropriate_cte_cap cap) b and valid_cap cap and valid_cap capa and tcb_cap_valid cap b and tcb_cap_valid capa a and cte_wp_at (weak_derived cap) a and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = cap) a and cte_wp_at (weak_derived capa) b and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = capa) b and K (a \<noteq> b \<and> \<not> is_master_reply_cap cap \<and> \<not> is_master_reply_cap capa)) s) else invs) s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s cap capa. \<lbrakk>invs s; ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (a, b) s; ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (aa, ba) s; \<forall>c. tcb_cap_valid c (a, b) s; \<forall>c. tcb_cap_valid c (aa, ba) s; cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (a, b) s; cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (aa, ba) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at ((=) cap) (a, b) s; cte_wp_at ((=) capa) (aa, ba) s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap capa) (a, b) s \<and> ex_cte_cap_wp_to (appropriate_cte_cap cap) (aa, ba) s \<and> s \<turnstile> cap \<and> s \<turnstile> capa \<and> cte_wp_at (weak_derived cap) (a, b) s \<and> cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = cap) (a, b) s \<and> cte_wp_at (weak_derived capa) (aa, ba) s \<and> cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = capa) (aa, ba) s \<and> \<not> is_master_reply_cap cap \<and> \<not> is_master_reply_cap capa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s cap capa. \<lbrakk>invs s; ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (a, b) s; ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (aa, ba) s; \<forall>c. tcb_cap_valid c (a, b) s; \<forall>c. tcb_cap_valid c (aa, ba) s; cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (a, b) s; cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (aa, ba) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at ((=) cap) (a, b) s; cte_wp_at ((=) capa) (aa, ba) s\<rbrakk> \<Longrightarrow> s \<turnstile> cap \<and> s \<turnstile> capa \<and> cte_wp_at (weak_derived cap) (a, b) s \<and> cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = cap) (a, b) s \<and> cte_wp_at (weak_derived capa) (aa, ba) s \<and> cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = capa) (aa, ba) s \<and> \<not> is_master_reply_cap cap \<and> \<not> is_master_reply_cap capa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s cap capa. \<lbrakk>invs s; ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (a, b) s; ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (aa, ba) s; \<forall>c. tcb_cap_valid c (a, b) s; \<forall>c. tcb_cap_valid c (aa, ba) s; cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (a, b) s; cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (aa, ba) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at ((=) cap) (a, b) s; cte_wp_at ((=) capa) (aa, ba) s\<rbrakk> \<Longrightarrow> s \<turnstile> capa \<and> cte_wp_at (weak_derived cap) (a, b) s \<and> cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = cap) (a, b) s \<and> cte_wp_at (weak_derived capa) (aa, ba) s \<and> cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = capa) (aa, ba) s \<and> \<not> is_master_reply_cap cap \<and> \<not> is_master_reply_cap capa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba s cap capa. \<lbrakk>invs s; ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (a, b) s; ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (aa, ba) s; \<forall>c. tcb_cap_valid c (a, b) s; \<forall>c. tcb_cap_valid c (aa, ba) s; cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (a, b) s; cte_wp_at (\<lambda>c. \<not> is_master_reply_cap c) (aa, ba) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at ((=) cap) (a, b) s; cte_wp_at ((=) capa) (aa, ba) s\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived cap) (a, b) s \<and> cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = cap) (a, b) s \<and> cte_wp_at (weak_derived capa) (aa, ba) s \<and> cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = capa) (aa, ba) s \<and> \<not> is_master_reply_cap cap \<and> \<not> is_master_reply_cap capa proof (prove)
goal:
No subgoals!