theory CNode_AC

lemma cap_insert_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and
    (\<lambda>s. (is_transferable_in src_slot s \<and> (\<not> Option.is_none (cdt s src_slot)))
         \<longrightarrow> is_transferable_cap new_cap) 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_insert new_cap src_slot dest_slot
   \<lbrace>\<lambda>rv. 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 F[symmetric]
                       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)

(* 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 (\<lambda>s. is_transferable_in src_slot s \<and> \<not> Option.is_none (cdt s src_slot) \<longrightarrow> is_transferable_cap new_cap) 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_insert new_cap src_slot dest_slot \<lbrace>\<lambda>rv. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and (\<lambda>s. is_transferable_in src_slot s \<and> \<not> Option.is_none (cdt s src_slot) \<longrightarrow> is_transferable_cap new_cap)\<rbrace> cap_insert new_cap src_slot dest_slot \<lbrace>\<lambda>rv. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and (\<lambda>s. is_transferable_in src_slot s \<and> \<not> Option.is_none (cdt s src_slot) \<longrightarrow> is_transferable_cap new_cap)\<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>rv. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap \<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>rv. pas_refined aag\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and (\<lambda>s. is_transferable_in src_slot s \<and> \<not> Option.is_none (cdt s src_slot) \<longrightarrow> is_transferable_cap new_cap)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst dest_slot) \<and> is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap; pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (is_transferable_in src_slot s \<and> \<not> Option.is_none (cdt s src_slot) \<longrightarrow> is_transferable_cap new_cap)\<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, pasSubject aag) \<in> pasPolicy aag) \<and> pas_cap_cur_auth aag cap \<and> (is_transferable_in dest_slot s \<longrightarrow> Option.is_none (cdt s dest_slot) \<or> is_transferable_cap new_cap \<or> (pasObjectAbs aag (fst (the (cdt s dest_slot))), Control, pasSubject aag) \<in> pasPolicy aag) \<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)