theory Finalise_AC

lemma invoke_cnode_pas_refined:
  "\<lbrace>pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action
                    and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s))
                    and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci\<rbrace>
   invoke_cnode ci
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp add:cap_insert_pas_refined cap_delete_pas_refined cap_revoke_pas_refined
             get_cap_wp cap_move_empty_src_slot
             | wpc
             | simp split del: if_split
             | wp (once) cap_move_cte_wp_at_separation)+ by (cases ci;
      simp add: authorised_cnode_inv_def
                cnode_inv_auth_derivations_def integrity_def;
      (clarsimp simp: cte_wp_at_caps_of_state pas_refined_refl cap_links_irq_def
                      real_cte_emptyable_strg
       | drule auth_derived_caps_of_state_impls
       | fastforce intro: cap_cur_auth_caps_of_state dest: is_derived_is_transferable)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> valid_cnode_inv ci s \<and> is_subject aag (cur_thread s) \<and> cnode_inv_auth_derivations ci s \<and> authorised_cnode_inv aag ci s \<Longrightarrow> (\<forall>x a b aa. (\<exists>ba. ci = InsertCall x (a, b) (aa, ba)) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> (is_transferable_in (a, b) s \<and> \<not> Option.is_none (cdt s (a, b)) \<longrightarrow> is_transferable_cap x) \<and> is_subject aag aa \<and> is_subject aag a \<and> pas_cap_cur_auth aag x) \<and> (\<forall>x a b aa ba. ci = MoveCall x (a, b) (aa, ba) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> cte_wp_at (weak_derived x) (a, b) s \<and> cte_wp_at ((=) NullCap) (aa, ba) s \<and> is_subject aag aa \<and> is_subject aag a \<and> pas_cap_cur_auth aag x) \<and> (\<forall>a. (\<exists>b. ci = RevokeCall (a, b)) \<longrightarrow> is_subject aag a) \<and> (\<forall>a b. ci = DeleteCall (a, b) \<longrightarrow> cdt_change_allowed' aag (a, b) s \<and> emptyable (a, b) s) \<and> (\<forall>x xa a b aa ba ab bb. ci = RotateCall x xa (a, b) (aa, ba) (ab, bb) \<longrightarrow> (a = ab \<and> b = bb \<longrightarrow> cte_wp_at (weak_derived x) (ab, bb) s \<and> cte_wp_at (weak_derived xa) (aa, ba) s \<and> is_subject aag ab \<and> is_subject aag aa \<and> pas_cap_cur_auth aag x \<and> pas_cap_cur_auth aag xa) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> cte_wp_at (weak_derived xa) (aa, ba) s \<and> cte_wp_at ((=) NullCap) (ab, bb) s \<and> is_subject aag ab \<and> is_subject aag aa \<and> pas_cap_cur_auth aag xa \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> cte_wp_at ((=) NullCap) (ab, bb) s \<and> cte_wp_at (\<lambda>c. weak_derived xa c \<and> c \<noteq> NullCap) (aa, ba) s \<and> cte_wp_at (weak_derived x) (a, b) s \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<and> (aa = ab \<longrightarrow> ba \<noteq> bb) \<and> is_subject aag aa \<and> is_subject aag a \<and> pas_cap_cur_auth aag x)) \<and> (\<forall>a b. ci = SaveCall (a, b) \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> cte_wp_at (weak_derived (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s \<and> cte_wp_at ((=) NullCap) (a, b) s \<and> is_subject aag a \<and> pas_cap_cur_auth aag (ReplyCap x False xb)))) \<and> (\<forall>x. ci = CancelBadgedSendsCall x \<longrightarrow> (\<forall>xa xb. (\<exists>xc. x = EndpointCap xa xb xc) \<longrightarrow> (if xb \<noteq> 0 then \<lambda>a. pas_refined aag a \<and> pspace_aligned a \<and> valid_vspace_objs a \<and> valid_arch_state a else pas_refined aag) s))