theory CSpacePre_AI

lemma set_untyped_cap_as_full_cte_wp_at_neg:
  "\<lbrace>\<lambda>s. (dest \<noteq> src \<and> \<not> (cte_wp_at P dest s) \<or>
         dest = src \<and> \<not> cte_wp_at (\<lambda>a. P (masked_as_full a cap)) src s) \<and>
        cte_wp_at ((=) src_cap) src s\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>ya s. \<not> cte_wp_at P dest s\<rbrace>" apply (clarsimp simp:set_untyped_cap_as_full_def | rule conjI |wp set_cap_cte_wp_at_neg)+ apply (clarsimp simp:cte_wp_at_caps_of_state masked_as_full_def)+ apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (dest \<noteq> src \<and> \<not> cte_wp_at P dest s \<or> dest = src \<and> \<not> cte_wp_at (\<lambda>a. P (masked_as_full a cap)) src s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>ya s. \<not> cte_wp_at P dest s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; \<not> cte_wp_at (\<lambda>a. P (masked_as_full a cap)) src s; cte_wp_at ((=) src_cap) src s; dest = src\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) src s
 2. \<And>s. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; \<not> cte_wp_at (\<lambda>a. P (masked_as_full a cap)) src s; cte_wp_at ((=) src_cap) src s; dest = src\<rbrakk> \<Longrightarrow> \<not> P (max_free_index_update src_cap)
 3. \<And>s. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; dest \<noteq> src \<and> \<not> cte_wp_at P dest s \<or> dest = src \<and> \<not> cte_wp_at (\<lambda>a. P (masked_as_full a cap)) src s; cte_wp_at ((=) src_cap) src s\<rbrakk> \<Longrightarrow> dest \<noteq> src \<longrightarrow> cte_wp_at (\<lambda>_. True) src s \<and> \<not> cte_wp_at P dest s
 4. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. (dest \<noteq> src \<and> \<not> cte_wp_at P dest s \<or> dest = src \<and> \<not> cte_wp_at (\<lambda>a. P (masked_as_full a cap)) src s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>ya s. \<not> cte_wp_at P dest s\<rbrace> proof (prove)
goal (1 subgoal):
 1. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. (dest \<noteq> src \<and> (\<forall>cap. caps_of_state s dest = Some cap \<longrightarrow> \<not> P cap) \<or> dest = src \<and> (\<forall>capa. (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> caps_of_state s src = Some capa \<longrightarrow> \<not> P (max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> caps_of_state s src = Some capa \<longrightarrow> \<not> P capa))) \<and> caps_of_state s src = Some src_cap\<rbrace> return () \<lbrace>\<lambda>ya s. \<forall>cap. caps_of_state s dest = Some cap \<longrightarrow> \<not> P cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; (dest \<noteq> src \<and> (\<forall>cap. caps_of_state s dest = Some cap \<longrightarrow> \<not> P cap) \<or> dest = src \<and> (\<forall>capa. (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> caps_of_state s src = Some capa \<longrightarrow> \<not> P (max_free_index_update capa)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> caps_of_state s src = Some capa \<longrightarrow> \<not> P capa))) \<and> caps_of_state s src = Some src_cap\<rbrakk> \<Longrightarrow> \<forall>cap. caps_of_state s dest = Some cap \<longrightarrow> \<not> P cap proof (prove)
goal:
No subgoals!