theory CSpaceInv_AI

lemma set_cap_valid_pspace:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (\<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s)
                        \<and> (\<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'.
                              p \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s
                                \<longrightarrow> (cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap))) p s
     \<and> valid_cap cap s \<and> tcb_cap_valid cap p s \<and> valid_pspace s\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. valid_pspace\<rbrace>" apply (simp add: valid_pspace_def) apply (wp set_cap_valid_objs set_cap_iflive set_cap_zombies) apply (clarsimp elim!: cte_wp_at_weakenE | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (\<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) \<and> (\<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap)) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<and> valid_pspace s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap'. (\<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) \<and> (\<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>a b. p \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>cap'. (\<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) \<and> (\<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>a b. p \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie cap)) p s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap p s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<Longrightarrow> (valid_objs and valid_cap cap and tcb_cap_valid cap p) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (cte_wp_at (\<lambda>cap'. \<forall>p'\<in>zobj_refs cap' - zobj_refs cap. obj_at (Not \<circ> live) p' s) p s \<and> if_live_then_nonz_cap s) \<and> (zombies_final s \<and> cte_wp_at (\<lambda>cap'. \<forall>r\<in>ex_zombie_refs (cap, cap'). \<forall>p'. p \<noteq> p' \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie cap) p s) \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) proof (prove)
goal:
No subgoals!