theory DomainSepInv

lemma invoke_tcb_domain_sep_inv:
  "\<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace>
   invoke_tcb tinv
   \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>" apply (case_tac tinv) apply ((wp restart_domain_sep_inv hoare_vcg_if_lift mapM_x_wp[OF _ subset_refl]
                 | wpc | simp split del: if_split add: check_cap_at_def | clarsimp)+)[3] defer apply ((wp | simp)+)[2] 
    (* just NotificationControl and ThreadControl left *)
     apply (rename_tac option) apply (case_tac option) apply  ((wp | simp)+)[1] apply (simp add: split_def cong: option.case_cong) apply (wp checked_cap_insert_domain_sep_inv hoare_vcg_all_lift_R hoare_vcg_all_lift
              hoare_vcg_const_imp_lift_R cap_delete_domain_sep_inv cap_delete_deletes
              dxo_wp_weak cap_delete_valid_cap cap_delete_cte_at hoare_weak_lift_imp
           | wpc | strengthen
           | simp add: option_update_thread_def emptyable_def tcb_cap_cases_def
                       tcb_cap_valid_def tcb_at_st_tcb_at
                  del: set_priority_extended.dxo_eq)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. tinv = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x21 x22 x23 x24. tinv = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x31 x32 x33 x34 x35 x36 x37. tinv = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 6. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 7. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 8. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x5. tinv = Suspend x5 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x6. tinv = Resume x6 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 5. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 x72. tinv = NotificationControl x71 x72 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. tinv = NotificationControl x71 option \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x71 option. \<lbrakk>tinv = NotificationControl x71 option; option = None\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x71 option a. \<lbrakk>tinv = NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 option a. \<lbrakk>tinv = NotificationControl x71 option; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x71 option a. \<lbrakk>tinv = NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>domain_sep_inv irqs st 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>_. domain_sep_inv irqs st\<rbrace>
 2. \<And>x81 x82. tinv = SetTLSBase x81 x82 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. tinv = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> \<lbrace>domain_sep_inv irqs st and tcb_inv_wf tinv\<rbrace> invoke_tcb tinv \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal:
No subgoals!