theory CNodeInv_AI

lemma cap_swap_has_reply_cap_neg:
  "\<lbrace>\<lambda>s. \<not> has_reply_cap t s \<and>
    cte_wp_at (weak_derived c) p s \<and>
    cte_wp_at (weak_derived c') p' s \<and>
    p \<noteq> p'\<rbrace>
   cap_swap c p c' p' \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace>" apply (simp add: has_reply_cap_def is_reply_cap_to_def cte_wp_at_caps_of_state
              del: split_paired_All split_paired_Ex) apply (wp cap_swap_caps_of_state) apply (elim conjE exE) apply (drule(3) cap_swap_no_reply_caps[where cs="caps_of_state _"]) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> has_reply_cap t s \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at (weak_derived c') p' s \<and> p \<noteq> p'\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>rv s. \<not> has_reply_cap t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)) \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> weak_derived c cap) \<and> (\<exists>cap. caps_of_state s p' = Some cap \<and> weak_derived c' cap) \<and> p \<noteq> p'\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>rv s. \<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights)) \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> weak_derived c cap) \<and> (\<exists>cap. caps_of_state s p' = Some cap \<and> weak_derived c' cap) \<and> p \<noteq> p' \<Longrightarrow> \<forall>pa cap. ((caps_of_state s)(p \<mapsto> c', p' \<mapsto> c)) pa = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); p \<noteq> p'; caps_of_state s p = Some cap; weak_derived c cap; caps_of_state s p' = Some capa; weak_derived c' capa\<rbrakk> \<Longrightarrow> \<forall>pa cap. ((caps_of_state s)(p \<mapsto> c', p' \<mapsto> c)) pa = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights) proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa. \<lbrakk>\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); p \<noteq> p'; weak_derived c cap; caps_of_state s p' = Some capa; weak_derived c' capa\<rbrakk> \<Longrightarrow> \<forall>sl R. caps_of_state s sl \<noteq> Some (ReplyCap (?t10 s cap capa) False R)
 2. \<And>s cap capa. \<lbrakk>\<forall>p cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights); p \<noteq> p'; weak_derived c cap; caps_of_state s p' = Some capa; weak_derived c' capa; \<forall>sl R. ((caps_of_state s)(p \<mapsto> c', p' \<mapsto> c)) sl \<noteq> Some (ReplyCap (?t10 s cap capa) False R)\<rbrakk> \<Longrightarrow> \<forall>pa cap. ((caps_of_state s)(p \<mapsto> c', p' \<mapsto> c)) pa = Some cap \<longrightarrow> (\<forall>rights. cap \<noteq> ReplyCap t False rights) proof (prove)
goal:
No subgoals!