theory Ipc_AC

lemma cap_insert_pas_refined_transferable:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and
    K (is_transferable_cap new_cap \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \<and>
       abs_has_auth_to aag DeleteDerived (fst src_slot) (fst dest_slot))\<rbrace>
   cap_insert new_cap src_slot dest_slot
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: cap_insert_def) apply (rule hoare_pre) apply (wp set_cap_pas_refined set_cdt_pas_refined update_cdt_pas_refined hoare_vcg_imp_lift
            hoare_weak_lift_imp hoare_vcg_all_lift set_cap_caps_of_state2
            set_untyped_cap_as_full_cdt_is_original_cap get_cap_wp
            tcb_domain_map_wellformed_lift hoare_vcg_disj_lift
            set_untyped_cap_as_full_is_transferable'
         | simp split del: if_split del: split_paired_All fun_upd_apply
         | strengthen update_one_strg)+ by (fastforce split: if_split_asm
                 simp: cte_wp_at_caps_of_state pas_refined_refl valid_mdb_def2
                       mdb_cte_at_def Option.is_none_def
             simp del: split_paired_All
                 dest: aag_cdt_link_Control aag_cdt_link_DeleteDerived cap_auth_caps_of_state
                intro: aag_wellformed_delete_derived_trans[OF _ _ pas_refined_wellformed])

(* 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 K (is_transferable_cap new_cap \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \<and> (pasObjectAbs aag (fst src_slot), DeleteDerived, pasObjectAbs aag (fst dest_slot)) \<in> pasPolicy aag)\<rbrace> cap_insert new_cap src_slot dest_slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_transferable_cap new_cap \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \<and> (pasObjectAbs aag (fst src_slot), DeleteDerived, pasObjectAbs aag (fst dest_slot)) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb\<rbrace> cap_insert new_cap src_slot dest_slot \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_transferable_cap new_cap \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \<and> (pasObjectAbs aag (fst src_slot), DeleteDerived, pasObjectAbs aag (fst dest_slot)) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb\<rbrace> do src_cap <- get_cap src_slot;
old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap new_cap src_slot;
y <- set_cap new_cap dest_slot;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- update_cdt (\<lambda>cdt. cdt(dest_slot := if should_be_parent_of src_cap (is_original src_slot) new_cap (is_cap_revocable new_cap src_cap) then Some src_slot else cdt src_slot));
y <- cap_insert_ext (should_be_parent_of src_cap (is_original src_slot) new_cap (is_cap_revocable new_cap src_cap)) src_slot dest_slot src_p dest_p;
set_original dest_slot (is_cap_revocable new_cap src_cap)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_transferable_cap new_cap \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \<and> (pasObjectAbs aag (fst src_slot), DeleteDerived, pasObjectAbs aag (fst dest_slot)) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q2\<rbrace> do src_cap <- get_cap src_slot;
old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap new_cap src_slot;
y <- set_cap new_cap dest_slot;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src_slot);
dest_p <- gets (\<lambda>s. cdt s dest_slot);
y <- update_cdt (\<lambda>cdt. cdt(dest_slot := if should_be_parent_of src_cap (is_original src_slot) new_cap (is_cap_revocable new_cap src_cap) then Some src_slot else cdt src_slot));
y <- cap_insert_ext (should_be_parent_of src_cap (is_original src_slot) new_cap (is_cap_revocable new_cap src_cap)) src_slot dest_slot src_p dest_p;
set_original dest_slot (is_cap_revocable new_cap src_cap)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>is_transferable_cap new_cap \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \<and> (pasObjectAbs aag (fst src_slot), DeleteDerived, pasObjectAbs aag (fst dest_slot)) \<in> pasPolicy aag; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_transferable_cap new_cap \<and> aag_cap_auth aag (pasObjectAbs aag (fst dest_slot)) new_cap \<and> (pasObjectAbs aag (fst src_slot), DeleteDerived, pasObjectAbs aag (fst dest_slot)) \<in> pasPolicy aag; pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) src_slot s \<longrightarrow> (\<exists>cap. cte_wp_at ((=) cap) dest_slot s) \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) dest_slot s \<longrightarrow> cap \<noteq> NullCap) \<or> (is_transferable_in src_slot s \<and> \<not> Option.is_none (cdt s src_slot) \<longrightarrow> is_transferable_cap cap \<or> (pasObjectAbs aag (fst (the (cdt s src_slot))), Control, pasObjectAbs aag (fst src_slot)) \<in> pasPolicy aag) \<and> aag_cap_auth aag (pasObjectAbs aag (fst src_slot)) cap \<and> (\<forall>x xa. ((cdt s)(dest_slot := if should_be_parent_of cap (is_original_cap s src_slot) new_cap (is_cap_revocable new_cap cap) then Some src_slot else cdt s src_slot)) x = Some xa \<longrightarrow> cdt s x = Some xa \<or> (is_transferable (((caps_of_state s)(dest_slot \<mapsto> new_cap)) x) \<and> Some cap = caps_of_state s src_slot \<or> (pasObjectAbs aag (fst xa), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag) \<and> (pasObjectAbs aag (fst xa), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag)