theory CNodeInv_AI

lemma cap_move_zombies_final[wp]:
  "\<lbrace>zombies_final and cte_wp_at ((=) cap.NullCap) ptr'
         and cte_wp_at (weak_derived cap) ptr
         and K (ptr \<noteq> ptr')\<rbrace>
     cap_move cap ptr ptr'
   \<lbrace>\<lambda>rv. zombies_final\<rbrace>" unfolding cap_move_def zombies_final_caps_of_state o_def set_cdt_def apply (rule hoare_pre) apply (wp|simp)+ apply (simp add: cte_wp_at_caps_of_state zombies_final_caps_def del: split_paired_All) apply (elim conjE exE) apply (intro impI allI) apply (simp add: weak_derived_obj_refs weak_derived_is_zombie del: split_paired_All) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr')\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>x. zombies_final_caps (caps_of_state x)) and cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr')\<rbrace> do set_cap cap ptr';
set_cap NullCap ptr;
src_p <- gets (\<lambda>s. cdt s ptr);
dest_p <- gets (\<lambda>s. cdt s ptr');
cdt <- gets cdt;
parent <- return $ cdt ptr;
cdt' <- return $ cdt(ptr' := parent, ptr := None);
do s <- get;
put $ s\<lparr>cdt := \<lambda>r. if cdt' r = Some ptr then Some ptr' else cdt' r\<rparr>
od;
do_extended_op (cap_move_ext ptr ptr' src_p dest_p);
is_original <- gets is_original_cap;
set_original ptr' (is_original ptr);
set_original ptr False
od \<lbrace>\<lambda>rv x. zombies_final_caps (caps_of_state x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do set_cap cap ptr';
set_cap NullCap ptr;
src_p <- gets (\<lambda>s. cdt s ptr);
dest_p <- gets (\<lambda>s. cdt s ptr');
cdt <- gets cdt;
parent <- return $ cdt ptr;
cdt' <- return $ cdt(ptr' := parent, ptr := None);
do s <- get;
put $ s\<lparr>cdt := \<lambda>r. if cdt' r = Some ptr then Some ptr' else cdt' r\<rparr>
od;
do_extended_op (cap_move_ext ptr ptr' src_p dest_p);
is_original <- gets is_original_cap;
set_original ptr' (is_original ptr);
set_original ptr False
od \<lbrace>\<lambda>rv x. zombies_final_caps (caps_of_state x)\<rbrace>
 2. \<And>s. ((\<lambda>x. zombies_final_caps (caps_of_state x)) and cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr')) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final_caps (caps_of_state s) \<and> cte_wp_at ((=) NullCap) ptr' s \<and> cte_wp_at (weak_derived cap) ptr s \<and> ptr \<noteq> ptr' \<Longrightarrow> zombies_final_caps (\<lambda>a. if a = ptr then Some NullCap else if a = ptr' then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap') \<and> caps_of_state s ptr' = Some NullCap \<and> (\<exists>capa. caps_of_state s ptr = Some capa \<and> weak_derived cap capa) \<and> ptr \<noteq> ptr' \<Longrightarrow> \<forall>p. (p = ptr' \<longrightarrow> ptr' \<noteq> ptr \<longrightarrow> (\<forall>p'. p' \<noteq> ptr' \<longrightarrow> p' \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'))) \<and> (p \<noteq> ptr' \<longrightarrow> p \<noteq> ptr \<longrightarrow> ptr' \<noteq> ptr \<longrightarrow> (\<forall>capa. caps_of_state s p = Some capa \<and> obj_refs capa \<inter> obj_refs cap \<noteq> {} \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa\<rbrakk> \<Longrightarrow> \<forall>p. (p = ptr' \<longrightarrow> ptr' \<noteq> ptr \<longrightarrow> (\<forall>p'. p' \<noteq> ptr' \<longrightarrow> p' \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'))) \<and> (p \<noteq> ptr' \<longrightarrow> p \<noteq> ptr \<longrightarrow> ptr' \<noteq> ptr \<longrightarrow> (\<forall>capa. caps_of_state s p = Some capa \<and> obj_refs capa \<inter> obj_refs cap \<noteq> {} \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa p. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa\<rbrakk> \<Longrightarrow> (p = ptr' \<longrightarrow> ptr' \<noteq> ptr \<longrightarrow> (\<forall>p'. p' \<noteq> ptr' \<longrightarrow> p' \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'))) \<and> (p \<noteq> ptr' \<longrightarrow> p \<noteq> ptr \<longrightarrow> ptr' \<noteq> ptr \<longrightarrow> (\<forall>capa. caps_of_state s p = Some capa \<and> obj_refs capa \<inter> obj_refs cap \<noteq> {} \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa p. \<lbrakk>\<forall>p p' cap cap'. caps_of_state s p = Some cap \<and> caps_of_state s p' = Some cap' \<and> obj_refs cap \<inter> obj_refs cap' \<noteq> {} \<and> p \<noteq> p' \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie cap'; caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa\<rbrakk> \<Longrightarrow> (p = ptr' \<longrightarrow> (\<forall>p'. p' \<noteq> ptr' \<longrightarrow> p' \<noteq> ptr \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<and> obj_refs capa \<inter> obj_refs cap' \<noteq> {} \<longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie cap'))) \<and> (p \<noteq> ptr' \<longrightarrow> p \<noteq> ptr \<longrightarrow> (\<forall>cap. caps_of_state s p = Some cap \<and> obj_refs cap \<inter> obj_refs capa \<noteq> {} \<longrightarrow> \<not> is_zombie cap \<and> \<not> is_zombie capa)) proof (prove)
goal:
No subgoals!