theory CNodeInv_AI

lemma cap_swap_valid_arch_caps[wp]:
  "\<And>c a c' b.
    \<lbrace>valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace>
      cap_swap c a c' b
    \<lbrace>\<lambda>rv. valid_arch_caps :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (simp add: cap_swap_def) apply (rule hoare_pre) apply (subst bind_assoc[symmetric],
          rule hoare_seq_ext [rotated],
          rule swap_of_caps_valid_arch_caps) apply (wp | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>c a c' b. \<lbrace>valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>c a c' b. \<lbrace>valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>c a c' b. \<lbrace>?Q c a c' b\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>
 2. \<And>c a c' b s. (valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q c a c' b s proof (prove)
goal (2 subgoals):
 1. \<And>c a c' b y. \<lbrace>valid_arch_caps\<rbrace> do slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>
 2. \<And>c a c' b s. (valid_arch_caps and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> (valid_arch_caps and cte_wp_at (weak_derived c') b and cte_wp_at (weak_derived c) a) s proof (prove)
goal:
No subgoals!