theory Tcb_AC

lemma invoke_tcb_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action
                       and tcb_inv_wf ti and K (authorised_tcb_inv aag ti)\<rbrace>
   invoke_tcb ti
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (cases ti, simp_all add: hoare_conjD1 [OF invoke_tcb_tc_respects_aag [simplified simp_thms]]
                            del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps K_def) apply (safe intro!: hoare_gen_asm) by ((wp itr_wps mapM_x_wp' arch_post_modify_registers_respects
       | wpc | clarsimp simp: authorised_tcb_inv_def if_apply_def2
       | rule conjI | subst (asm) idle_no_ex_cap)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf ti and K (authorised_tcb_inv aag ti)\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (WriteRegisters x11 x12 x13 x14) and K (authorised_tcb_inv aag (WriteRegisters x11 x12 x13 x14))\<rbrace> invoke_tcb (WriteRegisters x11 x12 x13 x14) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (ReadRegisters x21 x22 x23 x24) and K (authorised_tcb_inv aag (ReadRegisters x21 x22 x23 x24))\<rbrace> invoke_tcb (ReadRegisters x21 x22 x23 x24) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (CopyRegisters x31 x32 x33 x34 x35 x36 x37) and K (authorised_tcb_inv aag (CopyRegisters x31 x32 x33 x34 x35 x36 x37))\<rbrace> invoke_tcb (CopyRegisters x31 x32 x33 x34 x35 x36 x37) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>x5. ti = Suspend x5 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (Suspend x5) and K (authorised_tcb_inv aag (Suspend x5))\<rbrace> invoke_tcb (Suspend x5) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>x6. ti = Resume x6 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (Resume x6) and K (authorised_tcb_inv aag (Resume x6))\<rbrace> invoke_tcb (Resume x6) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (NotificationControl x71 x72) and K (authorised_tcb_inv aag (NotificationControl x71 x72))\<rbrace> invoke_tcb (NotificationControl x71 x72) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (SetTLSBase x81 x82) and K (authorised_tcb_inv aag (SetTLSBase x81 x82))\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>ti = WriteRegisters x11 x12 x13 x14; authorised_tcb_inv aag (WriteRegisters x11 x12 x13 x14)\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (WriteRegisters x11 x12 x13 x14)\<rbrace> invoke_tcb (WriteRegisters x11 x12 x13 x14) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x21 x22 x23 x24. \<lbrakk>ti = ReadRegisters x21 x22 x23 x24; authorised_tcb_inv aag (ReadRegisters x21 x22 x23 x24)\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (ReadRegisters x21 x22 x23 x24)\<rbrace> invoke_tcb (ReadRegisters x21 x22 x23 x24) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. \<lbrakk>ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37; authorised_tcb_inv aag (CopyRegisters x31 x32 x33 x34 x35 x36 x37)\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (CopyRegisters x31 x32 x33 x34 x35 x36 x37)\<rbrace> invoke_tcb (CopyRegisters x31 x32 x33 x34 x35 x36 x37) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>x5. \<lbrakk>ti = Suspend x5; authorised_tcb_inv aag (Suspend x5)\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (Suspend x5)\<rbrace> invoke_tcb (Suspend x5) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>x6. \<lbrakk>ti = Resume x6; authorised_tcb_inv aag (Resume x6)\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (Resume x6)\<rbrace> invoke_tcb (Resume x6) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>x71 x72. \<lbrakk>ti = NotificationControl x71 x72; authorised_tcb_inv aag (NotificationControl x71 x72)\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (NotificationControl x71 x72)\<rbrace> invoke_tcb (NotificationControl x71 x72) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<And>x81 x82. \<lbrakk>ti = SetTLSBase x81 x82; authorised_tcb_inv aag (SetTLSBase x81 x82)\<rbrakk> \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and einvs and simple_sched_action and tcb_inv_wf (SetTLSBase x81 x82)\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>