theory CNodeInv_AI

lemma cap_move_valid_arch_caps[wp]:
  "\<And>cap ptr.
    \<lbrace>valid_arch_caps
          and cte_wp_at (weak_derived cap) ptr
          and cte_wp_at ((=) cap.NullCap) ptr'\<rbrace>
      cap_move cap ptr ptr'
    \<lbrace>\<lambda>rv. valid_arch_caps :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (simp add: cap_move_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)+ apply (clarsimp elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap ptr. \<lbrace>valid_arch_caps and cte_wp_at (weak_derived cap) ptr and cte_wp_at ((=) NullCap) ptr'\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap ptr. \<lbrace>valid_arch_caps and cte_wp_at (weak_derived cap) ptr and cte_wp_at ((=) NullCap) ptr'\<rbrace> do y <- set_cap cap ptr';
y <- set_cap NullCap ptr;
src_p <- gets (\<lambda>s. cdt s ptr);
dest_p <- gets (\<lambda>s. cdt s ptr');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = ptr then None else if r = ptr' then cdt ptr else cdt r) = Some ptr then Some ptr' else if r = ptr then None else if r = ptr' then cdt ptr else cdt r);
y <- do_extended_op (cap_move_ext ptr ptr' src_p dest_p);
is_original <- gets is_original_cap;
y <- set_original ptr' (is_original ptr);
set_original ptr False
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cap ptr. \<lbrace>?Q8 cap ptr\<rbrace> do y <- set_cap cap ptr';
y <- set_cap NullCap ptr;
src_p <- gets (\<lambda>s. cdt s ptr);
dest_p <- gets (\<lambda>s. cdt s ptr');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = ptr then None else if r = ptr' then cdt ptr else cdt r) = Some ptr then Some ptr' else if r = ptr then None else if r = ptr' then cdt ptr else cdt r);
y <- do_extended_op (cap_move_ext ptr ptr' src_p dest_p);
is_original <- gets is_original_cap;
y <- set_original ptr' (is_original ptr);
set_original ptr False
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>
 2. \<And>cap ptr s. (valid_arch_caps and cte_wp_at (weak_derived cap) ptr and cte_wp_at ((=) NullCap) ptr') s \<Longrightarrow> ?Q8 cap ptr s proof (prove)
goal (2 subgoals):
 1. \<And>cap ptr y. \<lbrace>valid_arch_caps\<rbrace> do src_p <- gets (\<lambda>s. cdt s ptr);
dest_p <- gets (\<lambda>s. cdt s ptr');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = ptr then None else if r = ptr' then cdt ptr else cdt r) = Some ptr then Some ptr' else if r = ptr then None else if r = ptr' then cdt ptr else cdt r);
y <- do_extended_op (cap_move_ext ptr ptr' src_p dest_p);
is_original <- gets is_original_cap;
y <- set_original ptr' (is_original ptr);
set_original ptr False
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>
 2. \<And>cap ptr s. (valid_arch_caps and cte_wp_at (weak_derived cap) ptr and cte_wp_at ((=) NullCap) ptr') s \<Longrightarrow> (valid_arch_caps and cte_wp_at (weak_derived cap) ptr and cte_wp_at (weak_derived NullCap) ptr') s proof (prove)
goal (1 subgoal):
 1. \<And>cap ptr s. valid_arch_caps s \<and> cte_wp_at (weak_derived cap) ptr s \<and> cte_wp_at ((=) NullCap) ptr' s \<Longrightarrow> cte_wp_at (\<lambda>a. a = NullCap) ptr' s proof (prove)
goal:
No subgoals!