theory Finalise_AC

lemma invoke_cnode_respects:
  "\<lbrace>integrity aag X st and authorised_cnode_inv aag ci and (\<lambda>s. is_subject aag (cur_thread s))
                       and pas_refined aag and einvs and simple_sched_action
                       and valid_cnode_inv ci and cnode_inv_auth_derivations ci\<rbrace>
   invoke_cnode ci
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: invoke_cnode_def authorised_cnode_inv_def split: cnode_invocation.split, safe) apply (wpsimp wp: get_cap_wp cap_insert_integrity_autarch
                    cap_revoke_respects cap_delete_respects
              simp: real_cte_emptyable_strg is_transferable_weak_derived
         | clarsimp simp: cte_wp_at_caps_of_state invs_valid_objs invs_sym_refs
                          cnode_inv_auth_derivations_def
         | drule(2) auth_derived_caps_of_state_impls
         | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
         | rule hoare_pre | rule cca_direct)+ apply (auto simp: cap_auth_conferred_def cap_rights_to_auth_def aag_cap_auth_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and authorised_cnode_inv aag ci and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and cnode_inv_auth_derivations ci\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>x11 a b aa ba. ci = InsertCall x11 (a, b) (aa, ba) \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag a \<and> is_subject aag aa) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and (valid_cap x11 and cap_table_at (length b) a and cap_table_at (length ba) aa and (\<lambda>s. cte_wp_at (is_derived (cdt s) (a, b) x11) (a, b) s) and cte_wp_at (\<lambda>c. c = NullCap) (aa, ba) and ex_cte_cap_wp_to is_cnode_cap (aa, ba) and (\<lambda>y. a = aa \<longrightarrow> b \<noteq> ba) and (\<lambda>s. \<forall>r\<in>obj_refs x11. \<forall>a b. (aa = a \<longrightarrow> ba \<noteq> b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)) and cnode_inv_auth_derivations (InsertCall x11 (a, b) (aa, ba))\<rbrace> liftE (cap_insert x11 (a, b) (aa, ba)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x21 a b aa ba. ci = MoveCall x21 (a, b) (aa, ba) \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag a \<and> is_subject aag aa) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and (valid_cap x21 and cte_wp_at ((=) NullCap) (aa, ba) and cte_wp_at ((\<noteq>) NullCap) (a, b) and cte_wp_at (weak_derived x21) (a, b) and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x21) (a, b) and ex_cte_cap_wp_to is_cnode_cap (aa, ba) and cap_table_at (length b) a and cap_table_at (length ba) aa) and cnode_inv_auth_derivations (MoveCall x21 (a, b) (aa, ba))\<rbrace> liftE (cap_move x21 (a, b) (aa, ba)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>a b. ci = RevokeCall (a, b) \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag a) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and cte_wp_at (\<lambda>_. True) (a, b) and cnode_inv_auth_derivations (RevokeCall (a, b))\<rbrace> cap_revoke (a, b) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>a b. ci = DeleteCall (a, b) \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag a) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and cap_table_at (length b) a and cnode_inv_auth_derivations (DeleteCall (a, b))\<rbrace> cap_delete (a, b) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>x51 x52 a b aa ba ab bb. ci = RotateCall x51 x52 (ab, bb) (aa, ba) (ab, bb) \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag ab \<and> is_subject aag aa \<and> is_subject aag ab) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and (valid_cap x51 and valid_cap x52 and cap_table_at (length bb) ab and cap_table_at (length ba) aa and cte_wp_at (weak_derived x51) (ab, bb) and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) (ab, bb) and cte_wp_at ((\<noteq>) NullCap) (ab, bb) and cte_wp_at (weak_derived x52) (aa, ba) and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) (aa, ba) and cte_wp_at ((\<noteq>) NullCap) (aa, ba) and (\<lambda>y. (ab = aa \<longrightarrow> bb \<noteq> ba) \<and> (aa = ab \<longrightarrow> ba \<noteq> bb)) and ex_cte_cap_wp_to is_cnode_cap (aa, ba) and ex_cte_cap_wp_to is_cnode_cap (ab, bb)) and cnode_inv_auth_derivations (RotateCall x51 x52 (ab, bb) (aa, ba) (ab, bb))\<rbrace> liftE (cap_swap x51 (ab, bb) x52 (aa, ba)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>x51 x52 a b aa ba ab bb. \<lbrakk>ci = RotateCall x51 x52 (a, b) (aa, ba) (ab, bb); a \<noteq> ab\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag a \<and> is_subject aag aa \<and> is_subject aag ab) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and (valid_cap x51 and valid_cap x52 and cap_table_at (length b) a and cap_table_at (length bb) ab and cap_table_at (length ba) aa and cte_wp_at (weak_derived x51) (a, b) and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) (a, b) and cte_wp_at ((\<noteq>) NullCap) (a, b) and cte_wp_at (weak_derived x52) (aa, ba) and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) (aa, ba) and cte_wp_at ((\<noteq>) NullCap) (aa, ba) and (\<lambda>y. (a = aa \<longrightarrow> b \<noteq> ba) \<and> (aa = ab \<longrightarrow> ba \<noteq> bb)) and cte_wp_at (\<lambda>c. c = NullCap) (ab, bb) and ex_cte_cap_wp_to is_cnode_cap (aa, ba) and ex_cte_cap_wp_to is_cnode_cap (ab, bb)) and cnode_inv_auth_derivations (RotateCall x51 x52 (a, b) (aa, ba) (ab, bb))\<rbrace> liftE (do y <- cap_move x52 (aa, ba) (ab, bb);
cap_move x51 (a, b) (aa, ba)
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>x51 x52 a b aa ba ab bb. \<lbrakk>ci = RotateCall x51 x52 (a, b) (aa, ba) (ab, bb); b \<noteq> bb\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag a \<and> is_subject aag aa \<and> is_subject aag ab) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and (valid_cap x51 and valid_cap x52 and cap_table_at (length b) a and cap_table_at (length bb) ab and cap_table_at (length ba) aa and cte_wp_at (weak_derived x51) (a, b) and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) (a, b) and cte_wp_at ((\<noteq>) NullCap) (a, b) and cte_wp_at (weak_derived x52) (aa, ba) and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) (aa, ba) and cte_wp_at ((\<noteq>) NullCap) (aa, ba) and (\<lambda>y. (a = aa \<longrightarrow> b \<noteq> ba) \<and> (aa = ab \<longrightarrow> ba \<noteq> bb)) and cte_wp_at (\<lambda>c. c = NullCap) (ab, bb) and ex_cte_cap_wp_to is_cnode_cap (aa, ba) and ex_cte_cap_wp_to is_cnode_cap (ab, bb)) and cnode_inv_auth_derivations (RotateCall x51 x52 (a, b) (aa, ba) (ab, bb))\<rbrace> liftE (do y <- cap_move x52 (aa, ba) (ab, bb);
cap_move x51 (a, b) (aa, ba)
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 8. \<And>a b. ci = SaveCall (a, b) \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag a) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and (ex_cte_cap_wp_to is_cnode_cap (a, b) and cte_wp_at (\<lambda>c. c = NullCap) (a, b) and cap_table_at (length b) a) and cnode_inv_auth_derivations (SaveCall (a, b))\<rbrace> liftE (do thread <- gets cur_thread;
cap <- get_cap (thread, tcb_cnode_index 3);
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap (thread, tcb_cnode_index 3) (a, b) | _ \<Rightarrow> fail
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 9. \<And>x7. ci = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. pas_cap_cur_auth aag x7) and (\<lambda>s. is_subject aag (cur_thread s)) and pas_refined aag and einvs and simple_sched_action and (valid_cap x7 and (\<lambda>y. has_cancel_send_rights x7)) and cnode_inv_auth_derivations (CancelBadgedSendsCall x7)\<rbrace> case x7 of EndpointCap ep b R \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | _ \<Rightarrow> fail \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>ci = CancelBadgedSendsCall (EndpointCap x xa xb); integrity aag X st s; pas_cap_cur_auth aag (EndpointCap x xa xb); is_subject aag (cur_thread s); pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; s \<turnstile> EndpointCap x xa xb; has_cancel_send_rights (EndpointCap x xa xb); xa \<noteq> 0\<rbrakk> \<Longrightarrow> (pasSubject aag, Reset, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!