theory Tcb_AI

lemma (in Tcb_AI) tcbinv_invs:
  "\<lbrace>(invs::('state_ext::state_ext) state\<Rightarrow>bool) and tcb_inv_wf ti\<rbrace>
     invoke_tcb ti
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (case_tac ti, simp_all only:) apply ((wp writereg_invs readreg_invs copyreg_invs tc_invs
              | simp
              | clarsimp simp: invs_def valid_state_def valid_pspace_def
                        dest!: idle_no_ex_cap
                        split: option.split
              | rule conjI)+)[6] apply (rename_tac option) apply (case_tac option, simp_all) apply (rule hoare_pre) apply ((wp unbind_notification_invs get_simple_ko_wp | simp)+)[2] apply (wp bind_notification_invs) apply clarsimp apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_inv_wf ti\<rbrace> invoke_tcb ti \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (WriteRegisters x11 x12 x13 x14)\<rbrace> invoke_tcb (WriteRegisters x11 x12 x13 x14) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (ReadRegisters x21 x22 x23 x24)\<rbrace> invoke_tcb (ReadRegisters x21 x22 x23 x24) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> \<lbrace>invs 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>rv. invs\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48)\<rbrace> invoke_tcb (ThreadControl x41 x42 x43 x44 x45 x46 x47 x48) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x5. ti = Suspend x5 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (Suspend x5)\<rbrace> invoke_tcb (Suspend x5) \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. ti = Resume x6 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (Resume x6)\<rbrace> invoke_tcb (Resume x6) \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (NotificationControl x71 x72)\<rbrace> invoke_tcb (NotificationControl x71 x72) \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (SetTLSBase x81 x82)\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (NotificationControl x71 x72)\<rbrace> invoke_tcb (NotificationControl x71 x72) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (SetTLSBase x81 x82)\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x71 option. ti = NotificationControl x71 option \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (NotificationControl x71 option)\<rbrace> invoke_tcb (NotificationControl x71 option) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf (SetTLSBase x81 x82)\<rbrace> invoke_tcb (SetTLSBase x81 x82) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. \<lbrakk>ti = NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> \<lbrace>invs and (tcb_at x71 and ex_nonz_cap_to x71)\<rbrace> liftE (do y <- unbind_notification x71;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x71 option a. \<lbrakk>ti = NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))\<rbrace> liftE (do y <- bind_notification x71 a;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and (tcb_at x81 and ex_nonz_cap_to x81)\<rbrace> liftE (do y <- as_user x81 (setRegister tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) (do_extended_op reschedule_required);
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x71 option. \<lbrakk>ti = NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q288 x71 option\<rbrace> liftE (do y <- unbind_notification x71;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x71 option s. \<lbrakk>ti = NotificationControl x71 None; option = None; (invs and (tcb_at x71 and ex_nonz_cap_to x71)) s\<rbrakk> \<Longrightarrow> ?Q288 x71 option s
 3. \<And>x71 option a. \<lbrakk>ti = NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))\<rbrace> liftE (do y <- bind_notification x71 a;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and (tcb_at x81 and ex_nonz_cap_to x81)\<rbrace> liftE (do y <- as_user x81 (setRegister tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) (do_extended_op reschedule_required);
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x71 option a. \<lbrakk>ti = NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>invs and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))\<rbrace> liftE (do y <- bind_notification x71 a;
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and (tcb_at x81 and ex_nonz_cap_to x81)\<rbrace> liftE (do y <- as_user x81 (setRegister tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) (do_extended_op reschedule_required);
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x71 option a s. \<lbrakk>ti = NotificationControl x71 (Some a); option = Some a; (invs and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71))) s\<rbrakk> \<Longrightarrow> (bound_tcb_at ((=) None) x71 and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) a and invs and ex_nonz_cap_to a and ex_nonz_cap_to x71) s
 2. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and (tcb_at x81 and ex_nonz_cap_to x81)\<rbrace> liftE (do y <- as_user x81 (setRegister tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) (do_extended_op reschedule_required);
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>invs and (tcb_at x81 and ex_nonz_cap_to x81)\<rbrace> liftE (do y <- as_user x81 (setRegister tlsBaseRegister x82);
cur <- gets cur_thread;
y <- when (x81 = cur) (do_extended_op reschedule_required);
return []
od) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!