theory CNodeInv_AI

lemma cap_move_ex_cap_cte:
  "\<lbrace>ex_cte_cap_wp_to P ptr and
    cte_wp_at (weak_derived cap) p and
    cte_wp_at ((=) cap.NullCap) p' and
    K (p \<noteq> p') and K (\<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap')\<rbrace>
  cap_move cap p p'
  \<lbrace>\<lambda>_. ex_cte_cap_wp_to P ptr\<rbrace>" unfolding cap_move_def ex_cte_cap_wp_to_def cte_wp_at_caps_of_state set_cdt_def apply (rule hoare_pre) apply wp apply (simp del: split_paired_Ex) apply (wp set_cap_caps_of_state | simp del: split_paired_Ex add: cte_wp_at_caps_of_state)+ apply (elim conjE exE) apply (case_tac "cref = p") apply (rule_tac x=p' in exI) apply clarsimp apply (drule weak_derived_cte_refs_abs) apply simp apply (rule_tac x=cref in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P ptr and cte_wp_at (weak_derived cap) p and cte_wp_at ((=) NullCap) p' and K (p \<noteq> p') and K (\<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap')\<rbrace> cap_move cap p p' \<lbrace>\<lambda>_. ex_cte_cap_wp_to P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)) and (\<lambda>s. \<exists>capa. caps_of_state s p = Some capa \<and> weak_derived cap capa) and (\<lambda>s. \<exists>cap. caps_of_state s p' = Some cap \<and> NullCap = cap) and K (p \<noteq> p') and K (\<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap')\<rbrace> do set_cap cap p';
set_cap NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
parent <- return $ cdt p;
cdt' <- return $ cdt(p' := parent, p := None);
do s <- get;
put $ s\<lparr>cdt := \<lambda>r. if cdt' r = Some p then Some p' else cdt' r\<rparr>
od;
do_extended_op (cap_move_ext p p' src_p dest_p);
is_original <- gets is_original_cap;
set_original p' (is_original p);
set_original p False
od \<lbrace>\<lambda>_ s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do set_cap cap p';
set_cap NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
parent <- return $ cdt p;
cdt' <- return $ cdt(p' := parent, p := None);
do s <- get;
put $ s\<lparr>cdt := \<lambda>r. if cdt' r = Some p then Some p' else cdt' r\<rparr>
od;
do_extended_op (cap_move_ext p p' src_p dest_p);
is_original <- gets is_original_cap;
set_original p' (is_original p);
set_original p False
od \<lbrace>\<lambda>_ s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)) and (\<lambda>s. \<exists>capa. caps_of_state s p = Some capa \<and> weak_derived cap capa) and (\<lambda>s. \<exists>cap. caps_of_state s p' = Some cap \<and> NullCap = cap) and K (p \<noteq> p') and K (\<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap')) s \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>x xa src_p dest_p cdt parent cdt' xb s f. (\<exists>cref cap. caps_of_state (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(p' := is_original_cap (trans_state f s) p), is_original_cap := (is_original_cap (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(p' := is_original_cap (trans_state f s) p)\<rparr>))(p := False)\<rparr>) cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(p' := is_original_cap (trans_state f s) p), is_original_cap := (is_original_cap (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(p' := is_original_cap (trans_state f s) p)\<rparr>))(p := False)\<rparr>))) = (\<exists>cref cap. caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p)\<rparr>))(p := False)\<rparr>) cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p)\<rparr>))(p := False)\<rparr>)))
 2. \<And>x xa src_p dest_p cdt parent cdt'. \<lbrace>?B12 x xa src_p dest_p cdt parent cdt'\<rbrace> do s <- get;
put $ s\<lparr>cdt := \<lambda>r. if cdt' r = Some p then Some p' else cdt' r\<rparr>
od \<lbrace>\<lambda>xb s. \<exists>cref cap. caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p)\<rparr>))(p := False)\<rparr>) cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p)\<rparr>))(p := False)\<rparr>))\<rbrace>
 3. \<And>x xa src_p dest_p cdt parent. \<lbrace>?B11 x xa src_p dest_p cdt parent\<rbrace> return $ cdt(p' := parent, p := None) \<lbrace>?B12 x xa src_p dest_p cdt parent\<rbrace>
 4. \<And>x xa src_p dest_p cdt. \<lbrace>?B10 x xa src_p dest_p cdt\<rbrace> return $ cdt p \<lbrace>?B11 x xa src_p dest_p cdt\<rbrace>
 5. \<And>x xa src_p dest_p. \<lbrace>?B9 x xa src_p dest_p\<rbrace> gets cdt \<lbrace>?B10 x xa src_p dest_p\<rbrace>
 6. \<And>x xa src_p. \<lbrace>?B8 x xa src_p\<rbrace> gets (\<lambda>s. cdt s p') \<lbrace>?B9 x xa src_p\<rbrace>
 7. \<And>x xa. \<lbrace>?B6 x xa\<rbrace> gets (\<lambda>s. cdt s p) \<lbrace>?B8 x xa\<rbrace>
 8. \<And>x. \<lbrace>?B4 x\<rbrace> set_cap NullCap p \<lbrace>?B6 x\<rbrace>
 9. \<lbrace>?Q\<rbrace> set_cap cap p' \<lbrace>?B4\<rbrace>
 10. \<And>s. ((\<lambda>s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)) and (\<lambda>s. \<exists>capa. caps_of_state s p = Some capa \<and> weak_derived cap capa) and (\<lambda>s. \<exists>cap. caps_of_state s p' = Some cap \<and> NullCap = cap) and K (p \<noteq> p') and K (\<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap')) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>x xa src_p dest_p cdt parent cdt'. \<lbrace>?B12 x xa src_p dest_p cdt parent cdt'\<rbrace> do s <- get;
put $ s\<lparr>cdt := \<lambda>r. if cdt' r = Some p then Some p' else cdt' r\<rparr>
od \<lbrace>\<lambda>xb s. \<exists>cref cap. caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p)\<rparr>))(p := False)\<rparr>) cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p), is_original_cap := (is_original_cap (s\<lparr>is_original_cap := (is_original_cap s)(p' := is_original_cap s p)\<rparr>))(p := False)\<rparr>))\<rbrace>
 2. \<And>x xa src_p dest_p cdt parent. \<lbrace>?B11 x xa src_p dest_p cdt parent\<rbrace> return $ cdt(p' := parent, p := None) \<lbrace>?B12 x xa src_p dest_p cdt parent\<rbrace>
 3. \<And>x xa src_p dest_p cdt. \<lbrace>?B10 x xa src_p dest_p cdt\<rbrace> return $ cdt p \<lbrace>?B11 x xa src_p dest_p cdt\<rbrace>
 4. \<And>x xa src_p dest_p. \<lbrace>?B9 x xa src_p dest_p\<rbrace> gets cdt \<lbrace>?B10 x xa src_p dest_p\<rbrace>
 5. \<And>x xa src_p. \<lbrace>?B8 x xa src_p\<rbrace> gets (\<lambda>s. cdt s p') \<lbrace>?B9 x xa src_p\<rbrace>
 6. \<And>x xa. \<lbrace>?B6 x xa\<rbrace> gets (\<lambda>s. cdt s p) \<lbrace>?B8 x xa\<rbrace>
 7. \<And>x. \<lbrace>?B4 x\<rbrace> set_cap NullCap p \<lbrace>?B6 x\<rbrace>
 8. \<lbrace>?Q\<rbrace> set_cap cap p' \<lbrace>?B4\<rbrace>
 9. \<And>s. ((\<lambda>s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)) and (\<lambda>s. \<exists>capa. caps_of_state s p = Some capa \<and> weak_derived cap capa) and (\<lambda>s. \<exists>cap. caps_of_state s p' = Some cap \<and> NullCap = cap) and K (p \<noteq> p') and K (\<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap')) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)) \<and> (\<exists>capa. caps_of_state s p = Some capa \<and> weak_derived cap capa) \<and> caps_of_state s p' = Some NullCap \<and> p \<noteq> p' \<and> (\<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap') \<Longrightarrow> \<exists>cref. (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s); cref = p\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))))
 2. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s); cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s); cref = p\<rbrakk> \<Longrightarrow> (p' = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (p' \<noteq> p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))))
 2. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s); cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s a b capa. \<lbrakk>caps_of_state s p' = Some NullCap; (a, b) \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s (a, b) = Some capa; weak_derived cap capa; P capa; ptr \<in> cte_refs capa (interrupt_irq_node s); p = (a, b)\<rbrakk> \<Longrightarrow> ptr \<in> cte_refs cap (interrupt_irq_node s)
 2. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s); cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s a b capa. \<lbrakk>caps_of_state s p' = Some NullCap; (a, b) \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s (a, b) = Some capa; P capa; ptr \<in> cte_refs capa (interrupt_irq_node s); p = (a, b); cte_refs capa = cte_refs cap\<rbrakk> \<Longrightarrow> ptr \<in> cte_refs cap (interrupt_irq_node s)
 2. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s); cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s); cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref capa capaa. \<lbrakk>caps_of_state s p' = Some NullCap; p \<noteq> p'; \<forall>cap'. weak_derived cap cap' \<longrightarrow> P cap = P cap'; caps_of_state s p = Some capa; weak_derived cap capa; caps_of_state s cref = Some capaa; P capaa; ptr \<in> cte_refs capaa (interrupt_irq_node s); cref \<noteq> p\<rbrakk> \<Longrightarrow> (cref = p' \<longrightarrow> p' \<noteq> p \<and> (p' \<noteq> p \<longrightarrow> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s))) \<and> (cref \<noteq> p' \<longrightarrow> cref \<noteq> p \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> ptr \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal:
No subgoals!