theory Tcb_AC

lemma invoke_tcb_pas_refined:
  "\<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action
                    and K (authorised_tcb_inv aag ti)\<rbrace>
   invoke_tcb ti
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (cases "\<exists>t sl ep mcp priority croot vroot buf.
                ti = tcb_invocation.ThreadControl t sl ep mcp priority croot vroot buf") apply safe apply (rule hoare_chain, rule_tac Q'="\<lambda>_. pas_refined aag" and st1="\<lambda>x. x" in
                                     hoare_st_refl[OF invoke_tcb_tc_respects_aag]) apply force apply fastforce apply assumption apply (rule hoare_gen_asm) apply (cases ti, simp_all add: authorised_tcb_inv_def) apply (wp ita_wps hoare_drop_imps
                  hoare_strengthen_post[where Q="\<lambda>_. pas_refined aag and pspace_aligned
                                                                     and valid_vspace_objs
                                                                     and valid_arch_state",
                                        OF mapM_x_wp']
              | simp add: emptyable_def if_apply_def2 authorised_tcb_inv_def
              | rule ball_tcb_cap_casesI
              | wpc
              | fastforce intro: notE[rotated,OF idle_no_ex_cap,simplified]
                           simp: invs_valid_global_refs invs_valid_objs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<exists>t sl ep mcp priority croot vroot buf. ti = ThreadControl t sl ep mcp priority croot vroot buf \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<nexists>t sl ep mcp priority croot vroot buf. ti = ThreadControl t sl ep mcp priority croot vroot buf \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t a b ep mcp priority croot vroot buf. ti = ThreadControl t (a, b) ep mcp priority croot vroot buf \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf (ThreadControl t (a, b) ep mcp priority croot vroot buf) and einvs and simple_sched_action and K (authorised_tcb_inv aag (ThreadControl t (a, b) ep mcp priority croot vroot buf))\<rbrace> invoke_tcb (ThreadControl t (a, b) ep mcp priority croot vroot buf) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<nexists>t sl ep mcp priority croot vroot buf. ti = ThreadControl t sl ep mcp priority croot vroot buf \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>t a b ep mcp priority croot vroot buf r s st. \<lbrakk>ti = ThreadControl t (a, b) ep mcp priority croot vroot buf; (integrity aag (?X16 t a b ep mcp priority croot vroot buf st) st and pas_refined aag) s\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>t a b ep mcp priority croot vroot buf s. \<lbrakk>ti = ThreadControl t (a, b) ep mcp priority croot vroot buf; (pas_refined aag and tcb_inv_wf (ThreadControl t (a, b) ep mcp priority croot vroot buf) and einvs and simple_sched_action and K (authorised_tcb_inv aag (ThreadControl t (a, b) ep mcp priority croot vroot buf))) s\<rbrakk> \<Longrightarrow> (integrity aag (?X16 t a b ep mcp priority croot vroot buf s) s and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (ThreadControl t (a, b) ep mcp priority croot vroot buf) and K (authorised_tcb_inv aag (ThreadControl t (a, b) ep mcp priority croot vroot buf))) s
 3. \<And>t a b ep mcp priority croot vroot buf rv s. \<lbrakk>ti = ThreadControl t (a, b) ep mcp priority croot vroot buf; pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<nexists>t sl ep mcp priority croot vroot buf. ti = ThreadControl t sl ep mcp priority croot vroot buf \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t a b ep mcp priority croot vroot buf s. \<lbrakk>ti = ThreadControl t (a, b) ep mcp priority croot vroot buf; (pas_refined aag and tcb_inv_wf (ThreadControl t (a, b) ep mcp priority croot vroot buf) and einvs and simple_sched_action and K (authorised_tcb_inv aag (ThreadControl t (a, b) ep mcp priority croot vroot buf))) s\<rbrakk> \<Longrightarrow> (integrity aag (?X16 t a b ep mcp priority croot vroot buf s) s and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (ThreadControl t (a, b) ep mcp priority croot vroot buf) and K (authorised_tcb_inv aag (ThreadControl t (a, b) ep mcp priority croot vroot buf))) s
 2. \<And>t a b ep mcp priority croot vroot buf rv s. \<lbrakk>ti = ThreadControl t (a, b) ep mcp priority croot vroot buf; pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<nexists>t sl ep mcp priority croot vroot buf. ti = ThreadControl t sl ep mcp priority croot vroot buf \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t a b ep mcp priority croot vroot buf rv s. \<lbrakk>ti = ThreadControl t (a, b) ep mcp priority croot vroot buf; pas_refined aag s\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<nexists>t sl ep mcp priority croot vroot buf. ti = ThreadControl t sl ep mcp priority croot vroot buf \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<nexists>t sl ep mcp priority croot vroot buf. ti = ThreadControl t sl ep mcp priority croot vroot buf \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nexists>t sl ep mcp priority croot vroot buf. ti = ThreadControl t sl ep mcp priority croot vroot buf; authorised_tcb_inv aag ti\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>is_subject aag x11; ti = WriteRegisters x11 x12 x13 x14\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and (tcb_at x11 and ex_nonz_cap_to x11) and einvs and simple_sched_action\<rbrace> liftE (do self <- gets cur_thread;
b <- arch_get_sanitise_register_info x11;
y <- as_user x11 (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register b r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od);
y <- arch_post_modify_registers self x11;
y <- when x12 (restart x11);
y <- when (x11 = self) reschedule_required;
return []
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x21 x22 x23 x24. \<lbrakk>is_subject aag x21; ti = ReadRegisters x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and (tcb_at x21 and ex_nonz_cap_to x21) and einvs and simple_sched_action\<rbrace> liftE (do y <- when x22 (suspend x21);
self <- gets cur_thread;
as_user x21 (mapM getRegister (take (unat x23) frame_registers @ take (unat x23 - length frame_registers) gp_registers))
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>is_subject aag x32 \<and> is_subject aag x31; ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and (tcb_at x31 and tcb_at x32 and ex_nonz_cap_to x32 and ex_nonz_cap_to x31) and einvs and simple_sched_action\<rbrace> liftE (do y <- when x33 (suspend x32);
y <- when x34 (restart x31);
y <- when x35 (do y <- mapM_x (\<lambda>r. do v <- as_user x32 (getRegister r);
as_user x31 (setRegister r v)
od) frame_registers;
pc <- as_user x31 getRestartPC;
as_user x31 (setNextPC pc)
od);
y <- when x36 (mapM_x (\<lambda>r. do v <- as_user x32 (getRegister r);
as_user x31 (setRegister r v)
od) gpRegisters);
cur <- gets cur_thread;
y <- arch_post_modify_registers cur x31;
y <- when (x31 = cur) reschedule_required;
return []
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>x5. \<lbrakk>is_subject aag x5; ti = Suspend x5\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and (tcb_at x5 and ex_nonz_cap_to x5) and einvs and simple_sched_action\<rbrace> liftE (do y <- suspend x5;
return []
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<And>x6. \<lbrakk>is_subject aag x6; ti = Resume x6\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and (tcb_at x6 and ex_nonz_cap_to x6) and einvs and simple_sched_action\<rbrace> liftE (do y <- restart x6;
return []
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 6. \<And>x71 x72. \<lbrakk>is_subject aag x71 \<and> (case x72 of None \<Rightarrow> True | Some a \<Rightarrow> (pasSubject aag, Receive, pasObjectAbs aag a) \<in> pasPolicy aag \<and> (pasSubject aag, Reset, pasObjectAbs aag a) \<in> pasPolicy aag); ti = NotificationControl x71 x72\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and (tcb_at x71 and ex_nonz_cap_to x71 and (case x72 of None \<Rightarrow> \<lambda>_. True | Some ntfnptr \<Rightarrow> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr and ex_nonz_cap_to ntfnptr and bound_tcb_at ((=) None) x71)) and einvs and simple_sched_action\<rbrace> invoke_tcb (NotificationControl x71 x72) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 7. \<And>x81 x82. \<lbrakk>is_subject aag x81; ti = SetTLSBase x81 x82\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and (tcb_at x81 and ex_nonz_cap_to x81) and einvs and simple_sched_action\<rbrace> liftE (do y <- as_user x81 (setRegister tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) reschedule_required;
return []
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal:
No subgoals!