theory DetSchedSchedule_AI

lemma handle_recv_valid_sched:
  "\<lbrace>valid_sched and invs and ct_active
      and ct_not_queued and scheduler_act_sane\<rbrace>
   handle_recv is_blocking \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: handle_recv_def Let_def ep_ntfn_cap_case_helper
              cong: if_cong) apply (wp get_simple_ko_wp handle_fault_valid_sched delete_caller_cap_not_queued
            receive_ipc_valid_sched receive_signal_valid_sched | simp)+ apply (rule hoare_vcg_E_elim) apply (wpsimp simp: lookup_cap_def lookup_slot_for_thread_def) apply (wp resolve_address_bits_valid_fault2)+ apply (simp add: valid_fault_def) apply (wp hoare_drop_imps hoare_vcg_all_lift_R) apply (wpsimp wp: delete_caller_cap_not_queued | strengthen invs_valid_tcb_ctable_strengthen)+ apply (auto simp: ct_in_state_def tcb_at_invs objs_valid_tcb_ctable invs_valid_objs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane\<rbrace> do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
if is_ep_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then liftE (do y <- delete_caller_cap thread;
receive_ipc thread ep_cap is_blocking
od) else throwError (MissingCapability 0) else if is_ntfn_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then doE ntfn <- liftE (get_notification (cap_ep_ptr ep_cap));
if ntfn_bound_tcb ntfn = Some thread \<or> ntfn_bound_tcb ntfn = None then liftE (receive_signal thread ep_cap is_blocking) else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) else throwError (MissingCapability 0)
odE) <catch> handle_fault thread
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'128 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> ct_active s \<and> not_queued thread s \<and> st_tcb_at active thread s \<and> valid_objs s \<and> scheduler_act_not thread s \<and> sym_refs (state_refs_of s) \<and> scheduler_act_not thread s \<and> invs s \<and> tcb_at thread s) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 2. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active or ct_idle) s \<and> scheduler_act_not thread s \<and> invs s \<and> ?P'128 thread ep_cptr s\<rbrace>
 3. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 4. \<And>s. (valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane) s \<Longrightarrow> ?Q12 s proof (prove)
goal (5 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P140 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr -, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 2. \<And>thread ep_cptr. \<lbrace>?P'140 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> ct_active s \<and> not_queued thread s \<and> st_tcb_at active thread s \<and> valid_objs s \<and> scheduler_act_not thread s \<and> sym_refs (state_refs_of s) \<and> scheduler_act_not thread s \<and> invs s \<and> tcb_at thread s) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, -
 3. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active or ct_idle) s \<and> scheduler_act_not thread s \<and> invs s \<and> ?P140 thread ep_cptr s \<and> ?P'140 thread ep_cptr s\<rbrace>
 4. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 5. \<And>s. (valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane) s \<Longrightarrow> ?Q12 s proof (prove)
goal (6 subgoals):
 1. \<And>thread ep_cptr tcb. \<lbrace>?B158 thread ep_cptr tcb\<rbrace> resolve_address_bits (tcb_ctable tcb, ep_cptr) \<lbrace>\<lambda>x s. True\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 2. \<And>thread ep_cptr. \<lbrace>?P140 thread ep_cptr\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>?B158 thread ep_cptr\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ep_cptr) True rv)\<rbrace>
 3. \<And>thread ep_cptr. \<lbrace>?P'140 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> ct_active s \<and> not_queued thread s \<and> st_tcb_at active thread s \<and> valid_objs s \<and> scheduler_act_not thread s \<and> sym_refs (state_refs_of s) \<and> scheduler_act_not thread s \<and> invs s \<and> tcb_at thread s) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, -
 4. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active or ct_idle) s \<and> scheduler_act_not thread s \<and> invs s \<and> ?P140 thread ep_cptr s \<and> ?P'140 thread ep_cptr s\<rbrace>
 5. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 6. \<And>s. (valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane) s \<Longrightarrow> ?Q12 s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'140 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> ct_active s \<and> not_queued thread s \<and> st_tcb_at active thread s \<and> valid_objs s \<and> scheduler_act_not thread s \<and> sym_refs (state_refs_of s) \<and> scheduler_act_not thread s \<and> invs s \<and> tcb_at thread s) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0)))) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s \<and> valid_fault (CapFault (of_bl ep_cptr) True (MissingCapability 0))))\<rbrace>, -
 2. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active or ct_idle) s \<and> scheduler_act_not thread s \<and> invs s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> (invs and valid_cap (fst (tcb_ctable (the (get_tcb thread s)), ep_cptr))) s \<and> True) \<and> ?P'140 thread ep_cptr s\<rbrace>
 3. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 4. \<And>s. (valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane) s \<Longrightarrow> ?Q12 s proof (prove)
goal (4 subgoals):
 1. \<And>thread ep_cptr. \<lbrace>?P'140 thread ep_cptr\<rbrace> lookup_cap thread ep_cptr \<lbrace>\<lambda>ep_cap s. (is_ep_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> ct_active s \<and> not_queued thread s \<and> st_tcb_at active thread s \<and> valid_objs s \<and> scheduler_act_not thread s \<and> sym_refs (state_refs_of s) \<and> scheduler_act_not thread s \<and> invs s \<and> tcb_at thread s) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s)) \<and> (\<not> is_ep_cap ep_cap \<longrightarrow> (is_ntfn_cap ep_cap \<longrightarrow> (AllowRecv \<in> cap_rights ep_cap \<longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) (cap_ep_ptr ep_cap) s \<longrightarrow> (ntfn_bound_tcb ntfn = Some thread \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn = None \<longrightarrow> valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (ntfn_bound_tcb ntfn \<noteq> Some thread \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s))) \<and> (AllowRecv \<notin> cap_rights ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s)) \<and> (\<not> is_ntfn_cap ep_cap \<longrightarrow> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s))\<rbrace>, -
 2. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active or ct_idle) s \<and> scheduler_act_not thread s \<and> invs s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> (invs and valid_cap (fst (tcb_ctable (the (get_tcb thread s)), ep_cptr))) s \<and> True) \<and> ?P'140 thread ep_cptr s\<rbrace>
 3. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 4. \<And>s. (valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane) s \<Longrightarrow> ?Q12 s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B13 thread\<rbrace> liftM to_bl (as_user thread (getRegister cap_register)) \<lbrace>\<lambda>ep_cptr s. valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active or ct_idle) s \<and> scheduler_act_not thread s \<and> invs s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> (invs and valid_cap (fst (tcb_ctable (the (get_tcb thread s)), ep_cptr))) s \<and> True) \<and> ((valid_sched s \<and> st_tcb_at active thread s \<and> ct_active s \<and> not_queued thread s \<and> st_tcb_at active thread s \<and> valid_objs s \<and> scheduler_act_not thread s \<and> sym_refs (state_refs_of s) \<and> scheduler_act_not thread s \<and> invs s \<and> tcb_at thread s) \<and> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s) \<and> ((\<forall>x. (valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> (valid_sched s \<and> scheduler_act_not thread s \<and> not_queued thread s) \<and> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s) \<and> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s) \<and> valid_sched s \<and> st_tcb_at active thread s \<and> not_queued thread s \<and> (ct_active s \<or> ct_idle s) \<and> scheduler_act_not thread s \<and> invs s\<rbrace>
 2. \<lbrace>?Q12\<rbrace> gets cur_thread \<lbrace>?B13\<rbrace>
 3. \<And>s. (valid_sched and invs and ct_active and ct_not_queued and scheduler_act_sane) s \<Longrightarrow> ?Q12 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_sched s; invs s; ct_active s; ct_not_queued s; scheduler_act_sane s\<rbrakk> \<Longrightarrow> st_tcb_at active (cur_thread s) s \<and> ((\<exists>y. get_tcb (cur_thread s) s = Some y) \<longrightarrow> s \<turnstile> tcb_ctable (the (get_tcb (cur_thread s) s))) \<and> st_tcb_at active (cur_thread s) s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> tcb_at (cur_thread s) s \<and> st_tcb_at active (cur_thread s) s proof (prove)
goal:
No subgoals!