theory CNodeInv_AI

lemma cap_move_if_live[wp]:
  "\<lbrace>cte_wp_at ((=) cap.NullCap) ptr'
         and cte_wp_at (weak_derived cap) ptr
         and K (ptr \<noteq> ptr')
         and if_live_then_nonz_cap\<rbrace>
     cap_move cap ptr ptr'
   \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>" unfolding cap_move_def apply (rule hoare_pre) apply (wp|simp)+ apply (rule hoare_post_imp, simp only: if_live_then_nonz_cap_def) apply (simp only: ex_nonz_cap_to_def cte_wp_at_caps_of_state
                      imp_conv_disj) apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift)+ apply (clarsimp simp: if_live_then_nonz_cap_def
                        ex_nonz_cap_to_def cte_wp_at_caps_of_state
                   del: allI
              simp del: split_paired_Ex) apply (erule allEI, rule impI, drule(1) mp) apply (erule exfEI[where f="id (ptr := ptr', ptr' := ptr)"]) apply (clarsimp simp: weak_derived_obj_refs zobj_refs_to_obj_refs) apply (rule conjI) apply (clarsimp simp: weak_derived_is_zombie) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_live_then_nonz_cap\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_live_then_nonz_cap\<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);
set_cdt (\<lambda>r. if cdt' r = Some ptr then Some ptr' else cdt' r);
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. if_live_then_nonz_cap\<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);
set_cdt (\<lambda>r. if cdt' r = Some ptr then Some ptr' else cdt' r);
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. if_live_then_nonz_cap\<rbrace>
 2. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_live_then_nonz_cap) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B4 ()\<rbrace> set_cap NullCap ptr \<lbrace>\<lambda>xa. if_live_then_nonz_cap\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap cap ptr' \<lbrace>?B4\<rbrace>
 3. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_live_then_nonz_cap) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B4 ()\<rbrace> set_cap NullCap ptr \<lbrace>\<lambda>rv s. \<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap cap ptr' \<lbrace>?B4\<rbrace>
 3. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_live_then_nonz_cap) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B4 ()\<rbrace> set_cap NullCap ptr \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> obj_at live ptr s \<or> (\<exists>cref cap. caps_of_state s cref = Some cap \<and> ptr \<in> zobj_refs cap)\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap cap ptr' \<lbrace>?B4\<rbrace>
 3. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_live_then_nonz_cap) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_live_then_nonz_cap) s \<Longrightarrow> \<forall>x. \<not> obj_at live x s \<or> (\<exists>cref capa. ((caps_of_state s)(ptr' \<mapsto> cap, ptr \<mapsto> NullCap)) cref = Some capa \<and> x \<in> zobj_refs capa) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; \<forall>ptr. obj_at live ptr s \<longrightarrow> (\<exists>cref cap. caps_of_state s cref = Some cap \<and> ptr \<in> zobj_refs cap); caps_of_state s ptr = Some capa; weak_derived cap capa\<rbrakk> \<Longrightarrow> \<forall>x. obj_at live x s \<longrightarrow> (\<exists>cref. (cref = ptr' \<longrightarrow> x \<in> zobj_refs cap) \<and> (cref \<noteq> ptr' \<longrightarrow> cref \<noteq> ptr \<and> (cref \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> x \<in> zobj_refs cap)))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; obj_at live x s; \<exists>cref cap. caps_of_state s cref = Some cap \<and> x \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = ptr' \<longrightarrow> x \<in> zobj_refs cap) \<and> (cref \<noteq> ptr' \<longrightarrow> cref \<noteq> ptr \<and> (cref \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> x \<in> zobj_refs cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x cref. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; obj_at live x s; \<exists>cap. caps_of_state s cref = Some cap \<and> x \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> ((id(ptr := ptr', ptr' := ptr)) cref = ptr' \<longrightarrow> x \<in> zobj_refs cap) \<and> ((id(ptr := ptr', ptr' := ptr)) cref \<noteq> ptr' \<longrightarrow> (id(ptr := ptr', ptr' := ptr)) cref \<noteq> ptr \<and> ((id(ptr := ptr', ptr' := ptr)) cref \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s ((id(ptr := ptr', ptr' := ptr)) cref) = Some cap \<and> x \<in> zobj_refs cap))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa x a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; obj_at live x s; caps_of_state s (a, b) = Some capaa; x \<in> obj_refs capaa; \<not> is_zombie capaa\<rbrakk> \<Longrightarrow> ((a, b) = ptr \<longrightarrow> x \<in> obj_refs capa \<and> \<not> is_zombie cap) \<and> ((a, b) \<noteq> ptr \<longrightarrow> (a, b) \<noteq> ptr') proof (prove)
goal (2 subgoals):
 1. \<And>s capa x a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; obj_at live x s; caps_of_state s (a, b) = Some capaa; x \<in> obj_refs capaa; \<not> is_zombie capaa\<rbrakk> \<Longrightarrow> (a, b) = ptr \<longrightarrow> x \<in> obj_refs capa \<and> \<not> is_zombie cap
 2. \<And>s capa x a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; obj_at live x s; caps_of_state s (a, b) = Some capaa; x \<in> obj_refs capaa; \<not> is_zombie capaa\<rbrakk> \<Longrightarrow> (a, b) \<noteq> ptr \<longrightarrow> (a, b) \<noteq> ptr' proof (prove)
goal (1 subgoal):
 1. \<And>s capa x a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; obj_at live x s; caps_of_state s (a, b) = Some capaa; x \<in> obj_refs capaa; \<not> is_zombie capaa\<rbrakk> \<Longrightarrow> (a, b) \<noteq> ptr \<longrightarrow> (a, b) \<noteq> ptr' proof (prove)
goal:
No subgoals!