theory CNode_AC

lemma cap_move_pas_refined[wp]:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot
                    and cte_wp_at ((=) NullCap) dest_slot
                    and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot)
                                                          \<and> pas_cap_cur_auth aag new_cap)\<rbrace>
   cap_move new_cap src_slot dest_slot
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: cap_move_def) apply (rule hoare_pre) apply (wpsimp wp: set_cap_caps_of_state2 set_cap_pas_refined set_cdt_pas_refined
                     tcb_domain_map_wellformed_lift) by (fastforce simp: is_transferable_weak_derived valid_mdb_def2 mdb_cte_at_def
                      Option.is_none_def cte_wp_at_caps_of_state
            simp del: split_paired_All
                elim: pas_refined_refl
                dest: invs_mdb pas_refined_mem[OF sta_cdt]
                      pas_refined_mem[OF sta_cdt_transferable])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot and cte_wp_at ((=) NullCap) dest_slot and K (is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)\<rbrace> cap_move new_cap src_slot dest_slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot and cte_wp_at ((=) NullCap) dest_slot and (\<lambda>y. is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)\<rbrace> do y <- set_cap new_cap dest_slot;
y <- set_cap NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = src_slot then None else if r = dest_slot then cdt src_slot else cdt r) = Some src_slot then Some dest_slot else if r = src_slot then None else if r = dest_slot then cdt src_slot else cdt r);
y <- cap_move_ext src_slot dest_slot src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original dest_slot (is_original src_slot);
set_original src_slot False
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q8\<rbrace> do y <- set_cap new_cap dest_slot;
y <- set_cap NullCap src_slot;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = src_slot then None else if r = dest_slot then cdt src_slot else cdt r) = Some src_slot then Some dest_slot else if r = src_slot then None else if r = dest_slot then cdt src_slot else cdt r);
y <- cap_move_ext src_slot dest_slot src_p dest_p;
is_original <- gets is_original_cap;
y <- set_original dest_slot (is_original src_slot);
set_original src_slot False
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot and cte_wp_at ((=) NullCap) dest_slot and (\<lambda>y. is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)) s \<Longrightarrow> ?Q8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and cte_wp_at (weak_derived new_cap) src_slot and cte_wp_at ((=) NullCap) dest_slot and (\<lambda>y. is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)) s \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_transferable_in dest_slot s \<and> \<not> Option.is_none (cdt s dest_slot) \<longrightarrow> is_transferable_cap new_cap \<or> (pasObjectAbs aag (fst $ the $ cdt s dest_slot), Control, pasObjectAbs aag (fst dest_slot)) \<in> pasPolicy aag) and K (aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (is_transferable (((caps_of_state s)(dest_slot \<mapsto> new_cap)) src_slot) \<and> \<not> Option.is_none (cdt s src_slot) \<longrightarrow> is_transferable_cap NullCap \<or> (pasObjectAbs aag (fst $ the $ cdt s src_slot), Control, pasObjectAbs aag (fst src_slot)) \<in> pasPolicy aag) \<and> K (aag_cap_auth aag (pasObjectAbs aag (fst src_slot)) NullCap) s \<and> (\<forall>a b. ((a, b) = dest_slot \<longrightarrow> dest_slot \<noteq> src_slot \<longrightarrow> (cdt s src_slot = Some src_slot \<longrightarrow> (\<forall>aa. (\<exists>b. dest_slot = (aa, b) \<and> cdt s dest_slot \<noteq> Some (aa, b)) \<longrightarrow> (is_transferable (((caps_of_state s)(dest_slot \<mapsto> new_cap, src_slot \<mapsto> NullCap)) dest_slot) \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag)) \<and> (cdt s src_slot \<noteq> Some src_slot \<longrightarrow> (\<forall>aa. (\<exists>b. cdt s src_slot = Some (aa, b) \<and> cdt s dest_slot \<noteq> Some (aa, b)) \<longrightarrow> (is_transferable (((caps_of_state s)(dest_slot \<mapsto> new_cap, src_slot \<mapsto> NullCap)) dest_slot) \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag))) \<and> ((a, b) \<noteq> dest_slot \<longrightarrow> (a, b) \<noteq> src_slot \<longrightarrow> cdt s (a, b) = Some src_slot \<longrightarrow> (\<forall>aa. (\<exists>b. dest_slot = (aa, b) \<and> src_slot \<noteq> (aa, b)) \<longrightarrow> (is_transferable (((caps_of_state s)(dest_slot \<mapsto> new_cap, src_slot \<mapsto> NullCap)) (a, b)) \<or> (pasObjectAbs aag aa, Control, pasObjectAbs aag a) \<in> pasPolicy aag) \<and> (pasObjectAbs aag aa, DeleteDerived, pasObjectAbs aag a) \<in> pasPolicy aag)))