theory CNodeInv_AI

lemma cap_swap_not_recursive:
  "\<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n
     \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s
                      \<and> p1 \<in> fst_cte_ptrs cap) p2 s
     \<and> cte_wp_at ((=) c1) p1 s
     \<and> cte_wp_at ((=) c2) p2 s
     \<and> p1 \<noteq> p2\<rbrace>
     cap_swap c1 p1 c2 p2
   \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace>" apply (cases "p1 = p2", simp_all) apply (simp add: cap_swap_def set_cdt_def when_def) apply (rule hoare_vcg_precond_imp) apply (wp | simp)+ apply (rule not_recursive_set_cap_doesn't_grow) apply (wp not_recursive_set_cap_shrinks set_cap_cte_wp_at' get_cap_wp hoare_vcg_disj_lift) apply (clarsimp simp: cte_wp_at_def) apply (frule(3) final_cap_duplicate_cte_ptr) apply simp apply (case_tac c2, simp_all add: fst_cte_ptrs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> cte_wp_at ((=) c1) p1 s \<and> cte_wp_at ((=) c2) p2 s \<and> p1 \<noteq> p2\<rbrace> cap_swap c1 p1 c2 p2 \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace> proof (prove)
goal (1 subgoal):
 1. p1 \<noteq> p2 \<Longrightarrow> \<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> cte_wp_at ((=) c1) p1 s \<and> cte_wp_at ((=) c2) p2 s\<rbrace> cap_swap c1 p1 c2 p2 \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace> proof (prove)
goal (1 subgoal):
 1. p1 \<noteq> p2 \<Longrightarrow> \<lbrace>\<lambda>s. card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> cte_wp_at ((=) c1) p1 s \<and> cte_wp_at ((=) c2) p2 s\<rbrace> do y <- set_cap c2 p1;
y <- set_cap c1 p2;
slot1_p <- gets (\<lambda>s. cdt s p1);
slot2_p <- gets (\<lambda>s. cdt s p2);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := (\<lambda>n. if cdt n = Some p1 then Some p2 else if cdt n = Some p2 then Some p1 else cdt n)(p1 := if cdt p2 = Some p1 then Some p2 else if cdt p2 = Some p2 then Some p1 else cdt p2, p2 := if cdt p1 = Some p1 then Some p2 else if cdt p1 = Some p2 then Some p1 else cdt p1)\<rparr>)
od;
y <- do_extended_op (cap_swap_ext p1 p2 slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original p1 (is_original p2);
set_original p2 (is_original p1)
od \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace> proof (prove)
goal (2 subgoals):
 1. p1 \<noteq> p2 \<Longrightarrow> \<lbrace>?Q2\<rbrace> do y <- set_cap c2 p1;
y <- set_cap c1 p2;
slot1_p <- gets (\<lambda>s. cdt s p1);
slot2_p <- gets (\<lambda>s. cdt s p2);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := (\<lambda>n. if cdt n = Some p1 then Some p2 else if cdt n = Some p2 then Some p1 else cdt n)(p1 := if cdt p2 = Some p1 then Some p2 else if cdt p2 = Some p2 then Some p1 else cdt p2, p2 := if cdt p1 = Some p1 then Some p2 else if cdt p1 = Some p2 then Some p1 else cdt p1)\<rparr>)
od;
y <- do_extended_op (cap_swap_ext p1 p2 slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original p1 (is_original p2);
set_original p2 (is_original p1)
od \<lbrace>\<lambda>rv s. card (not_recursive_cspaces s) < n\<rbrace>
 2. \<And>s. \<lbrakk>p1 \<noteq> p2; card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> cte_wp_at ((=) c1) p1 s \<and> cte_wp_at ((=) c2) p2 s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. p1 \<noteq> p2 \<Longrightarrow> \<lbrace>?B6 ()\<rbrace> set_cap c1 p2 \<lbrace>\<lambda>ya s. card (not_recursive_cspaces s) < n\<rbrace>
 2. p1 \<noteq> p2 \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap c2 p1 \<lbrace>?B6\<rbrace>
 3. \<And>s. \<lbrakk>p1 \<noteq> p2; card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> cte_wp_at ((=) c1) p1 s \<and> cte_wp_at ((=) c2) p2 s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. p1 \<noteq> p2 \<Longrightarrow> \<lbrace>?Q2\<rbrace> set_cap c2 p1 \<lbrace>\<lambda>a b. card (not_recursive_cspaces b) < n \<and> cte_wp_at (\<lambda>cap. p2 \<notin> fst_cte_ptrs cap) p2 b\<rbrace>
 2. \<And>s. \<lbrakk>p1 \<noteq> p2; card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> cte_wp_at ((=) c1) p1 s \<and> cte_wp_at ((=) c2) p2 s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p1 \<noteq> p2; card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. is_final_cap' cap s \<and> p1 \<in> fst_cte_ptrs cap) p2 s \<and> cte_wp_at ((=) c1) p1 s \<and> cte_wp_at ((=) c2) p2 s\<rbrakk> \<Longrightarrow> (card (not_recursive_cspaces s) \<le> n \<and> cte_wp_at (\<lambda>cap. p1 \<notin> fst_cte_ptrs cap) p1 s \<and> p1 \<in> fst_cte_ptrs c2) \<and> (if p2 = p1 then p2 \<notin> fst_cte_ptrs c2 \<and> cte_wp_at (\<lambda>_. True) p1 s else cte_wp_at (\<lambda>cap. p2 \<notin> fst_cte_ptrs cap) p2 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p1 \<noteq> p2; card (not_recursive_cspaces s) \<le> n; fst (get_cap p1 s) = {(c1, s)}; fst (get_cap p2 s) = {(c2, s)}; is_final_cap' c2 s; p1 \<in> fst_cte_ptrs c2\<rbrakk> \<Longrightarrow> p1 \<notin> fst_cte_ptrs c1 \<and> p2 \<notin> fst_cte_ptrs c2 proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p1 \<noteq> p2; card (not_recursive_cspaces s) \<le> n; fst (get_cap p1 s) = {(c1, s)}; fst (get_cap p2 s) = {(c2, s)}; is_final_cap' c2 s; p1 \<in> fst_cte_ptrs c2\<rbrakk> \<Longrightarrow> p2 \<noteq> p1
 2. \<And>s. \<lbrakk>p1 \<noteq> p2; card (not_recursive_cspaces s) \<le> n; fst (get_cap p1 s) = {(c1, s)}; fst (get_cap p2 s) = {(c2, s)}; is_final_cap' c2 s; p1 \<in> fst_cte_ptrs c2; p1 \<notin> fst_cte_ptrs c1\<rbrakk> \<Longrightarrow> p1 \<notin> fst_cte_ptrs c1 \<and> p2 \<notin> fst_cte_ptrs c2 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p1 \<noteq> p2; card (not_recursive_cspaces s) \<le> n; fst (get_cap p1 s) = {(c1, s)}; fst (get_cap p2 s) = {(c2, s)}; is_final_cap' c2 s; p1 \<in> fst_cte_ptrs c2; p1 \<notin> fst_cte_ptrs c1\<rbrakk> \<Longrightarrow> p1 \<notin> fst_cte_ptrs c1 \<and> p2 \<notin> fst_cte_ptrs c2 proof (prove)
goal:
No subgoals!