theory DetSchedSchedule_AI

lemma handle_invocation_valid_sched:
  "\<lbrace>invs and valid_sched and ct_active and
    (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace>
     handle_invocation a b
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: handle_invocation_def) apply (wp syscall_valid handle_fault_valid_sched | wpc)+ apply (wp set_thread_state_runnable_valid_sched)[1] apply wp+ apply (wp gts_wp hoare_vcg_all_lift) apply (rule_tac Q="\<lambda>_. valid_sched" and E="\<lambda>_. valid_sched" in hoare_post_impErr) apply wp apply ((clarsimp simp: st_tcb_at_def obj_at_def)+)[2] apply (wp ct_in_state_set set_thread_state_runnable_valid_sched
             | simp add: split_def if_apply_def2 split del: if_split)+ apply (simp add: validE_E_def) apply (rule hoare_post_impErr) apply (rule lookup_cap_and_slot_valid_fault) apply (wp | simp)+ apply (auto simp: ct_in_state_def valid_sched_def ct_not_in_q_def valid_queues_def not_queued_def runnable_eq_active elim: st_tcb_ex_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> handle_invocation a b \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE (cap, slot) <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE) (\<lambda>fault. when b (handle_fault thread fault)) (\<lambda>(slot, cap, extracaps, buffer). doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args ptr slot cap extracaps
odE) (\<lambda>err. when a (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation b a oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when a (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (16 subgoals):
 1. \<And>thread info ptr rv y reply x ya. x = Restart \<Longrightarrow> \<lbrace>?B52 thread info ptr rv y reply x ya\<rbrace> set_thread_state thread Running \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>thread info ptr rv y reply x. x = Restart \<Longrightarrow> \<lbrace>?R34 thread info ptr rv y reply x\<rbrace> when a (reply_from_kernel thread (0, reply)) \<lbrace>?B52 thread info ptr rv y reply x\<rbrace>
 3. \<And>thread info ptr rv y reply x x41 x42. x = BlockedOnReceive x41 x42 \<Longrightarrow> \<lbrace>?R33 thread info ptr rv y reply x x41 x42\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>thread info ptr rv y reply x x51 x52. x = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>?R30 thread info ptr rv y reply x x51 x52\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>thread info ptr rv y reply x. awaiting_reply x \<Longrightarrow> \<lbrace>?R27 thread info ptr rv y reply x\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>thread info ptr rv y reply x x7. x = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R26 thread info ptr rv y reply x x7\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>thread info ptr rv y reply x. idle x \<Longrightarrow> \<lbrace>?R24 thread info ptr rv y reply x\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>thread info ptr rv y reply. \<lbrace>?B11 thread info ptr rv y reply\<rbrace> get_thread_state thread \<lbrace>\<lambda>x s. (x = Running \<longrightarrow> valid_sched s) \<and> (inactive x \<longrightarrow> valid_sched s) \<and> (x = Restart \<longrightarrow> ?R34 thread info ptr rv y reply x s) \<and> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> ?R33 thread info ptr rv y reply x xa xb s) \<and> (\<forall>xa xb. x = BlockedOnSend xa xb \<longrightarrow> ?R30 thread info ptr rv y reply x xa xb s) \<and> (awaiting_reply x \<longrightarrow> ?R27 thread info ptr rv y reply x s) \<and> (\<forall>xa. x = BlockedOnNotification xa \<longrightarrow> ?R26 thread info ptr rv y reply x xa s) \<and> (idle x \<longrightarrow> ?R24 thread info ptr rv y reply x s)\<rbrace>
 9. \<And>thread info ptr rv y. \<lbrace>?B10 thread info ptr rv y\<rbrace> perform_invocation b a rv \<lbrace>?B11 thread info ptr rv y\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 10. \<And>thread info ptr rv. \<lbrace>?P_no_err5 thread info ptr rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B10 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>thread info ptr rv y reply x. x = Restart \<Longrightarrow> \<lbrace>?R34 thread info ptr rv y reply x\<rbrace> when a (reply_from_kernel thread (0, reply)) \<lbrace>\<lambda>ya. valid_sched and st_tcb_at runnable thread and (\<lambda>s. runnable Running)\<rbrace>
 2. \<And>thread info ptr rv y reply x x41 x42. x = BlockedOnReceive x41 x42 \<Longrightarrow> \<lbrace>?R33 thread info ptr rv y reply x x41 x42\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>thread info ptr rv y reply x x51 x52. x = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>?R30 thread info ptr rv y reply x x51 x52\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>thread info ptr rv y reply x. awaiting_reply x \<Longrightarrow> \<lbrace>?R27 thread info ptr rv y reply x\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>thread info ptr rv y reply x x7. x = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R26 thread info ptr rv y reply x x7\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>thread info ptr rv y reply x. idle x \<Longrightarrow> \<lbrace>?R24 thread info ptr rv y reply x\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>thread info ptr rv y reply. \<lbrace>?B11 thread info ptr rv y reply\<rbrace> get_thread_state thread \<lbrace>\<lambda>x s. (x = Running \<longrightarrow> valid_sched s) \<and> (inactive x \<longrightarrow> valid_sched s) \<and> (x = Restart \<longrightarrow> ?R34 thread info ptr rv y reply x s) \<and> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> ?R33 thread info ptr rv y reply x xa xb s) \<and> (\<forall>xa xb. x = BlockedOnSend xa xb \<longrightarrow> ?R30 thread info ptr rv y reply x xa xb s) \<and> (awaiting_reply x \<longrightarrow> ?R27 thread info ptr rv y reply x s) \<and> (\<forall>xa. x = BlockedOnNotification xa \<longrightarrow> ?R26 thread info ptr rv y reply x xa s) \<and> (idle x \<longrightarrow> ?R24 thread info ptr rv y reply x s)\<rbrace>
 8. \<And>thread info ptr rv y. \<lbrace>?B10 thread info ptr rv y\<rbrace> perform_invocation b a rv \<lbrace>?B11 thread info ptr rv y\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 9. \<And>thread info ptr rv. \<lbrace>?P_no_err5 thread info ptr rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B10 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 10. \<And>thread info ptr rv. \<lbrace>?P_no_flt5 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args ptr slot cap extracaps
odE \<lbrace>?P_no_err5 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if a then valid_sched else valid_sched\<rbrace>
A total of 15 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>thread info ptr rv y reply. \<lbrace>?B11 thread info ptr rv y reply\<rbrace> get_thread_state thread \<lbrace>\<lambda>x s. (x = Running \<longrightarrow> valid_sched s) \<and> (inactive x \<longrightarrow> valid_sched s) \<and> (x = Restart \<longrightarrow> (if a then \<lambda>s. valid_sched s \<and> st_tcb_at runnable thread s \<and> runnable Running else (\<lambda>s. valid_sched s \<and> st_tcb_at runnable thread s \<and> runnable Running)) s) \<and> (\<forall>xa xb. x = BlockedOnReceive xa xb \<longrightarrow> valid_sched s) \<and> (\<forall>xa xb. x = BlockedOnSend xa xb \<longrightarrow> valid_sched s) \<and> (awaiting_reply x \<longrightarrow> valid_sched s) \<and> (\<forall>xa. x = BlockedOnNotification xa \<longrightarrow> valid_sched s) \<and> (idle x \<longrightarrow> valid_sched s)\<rbrace>
 2. \<And>thread info ptr rv y. \<lbrace>?B10 thread info ptr rv y\<rbrace> perform_invocation b a rv \<lbrace>?B11 thread info ptr rv y\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_err5 thread info ptr rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B10 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_flt5 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args ptr slot cap extracaps
odE \<lbrace>?P_no_err5 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if a then valid_sched else valid_sched\<rbrace>
 5. \<And>thread info ptr. \<lbrace>?B4 thread info ptr\<rbrace> doE (cap, slot) <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt5 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if b then valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle) and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ft) else valid_sched\<rbrace>
 6. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 9. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>thread info ptr rv y. \<lbrace>?B10 thread info ptr rv y\<rbrace> perform_invocation b a rv \<lbrace>\<lambda>reply s. \<forall>st. st_tcb_at ((=) st) thread s \<longrightarrow> (st = Running \<longrightarrow> valid_sched s) \<and> (inactive st \<longrightarrow> valid_sched s) \<and> (st = Restart \<longrightarrow> (if a then \<lambda>s. valid_sched s \<and> st_tcb_at runnable thread s \<and> runnable Running else (\<lambda>s. valid_sched s \<and> st_tcb_at runnable thread s \<and> runnable Running)) s) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> valid_sched s) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> valid_sched s) \<and> (awaiting_reply st \<longrightarrow> valid_sched s) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> valid_sched s) \<and> (idle st \<longrightarrow> valid_sched s)\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>thread info ptr rv. \<lbrace>?P_no_err5 thread info ptr rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B10 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt5 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args ptr slot cap extracaps
odE \<lbrace>?P_no_err5 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if a then valid_sched else valid_sched\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B4 thread info ptr\<rbrace> doE (cap, slot) <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt5 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if b then valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle) and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ft) else valid_sched\<rbrace>
 5. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>thread info ptr rv y. \<lbrace>?B10 thread info ptr rv y\<rbrace> perform_invocation b a rv \<lbrace>\<lambda>_. valid_sched\<rbrace>, \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>thread info ptr rv y rva s. valid_sched s \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) thread s \<longrightarrow> (st = Running \<longrightarrow> valid_sched s) \<and> (inactive st \<longrightarrow> valid_sched s) \<and> (st = Restart \<longrightarrow> (if a then \<lambda>s. valid_sched s \<and> st_tcb_at runnable thread s \<and> runnable Running else (\<lambda>s. valid_sched s \<and> st_tcb_at runnable thread s \<and> runnable Running)) s) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> valid_sched s) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> valid_sched s) \<and> (awaiting_reply st \<longrightarrow> valid_sched s) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> valid_sched s) \<and> (idle st \<longrightarrow> valid_sched s)
 3. \<And>thread info ptr rv y e s. valid_sched s \<Longrightarrow> valid_sched s
 4. \<And>thread info ptr rv. \<lbrace>?P_no_err5 thread info ptr rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B10 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>thread info ptr rv. \<lbrace>?P_no_flt5 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args ptr slot cap extracaps
odE \<lbrace>?P_no_err5 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if a then valid_sched else valid_sched\<rbrace>
 6. \<And>thread info ptr. \<lbrace>?B4 thread info ptr\<rbrace> doE (cap, slot) <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt5 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if b then valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle) and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ft) else valid_sched\<rbrace>
 7. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 9. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 10. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>thread info ptr rv y rva s. valid_sched s \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) thread s \<longrightarrow> (st = Running \<longrightarrow> valid_sched s) \<and> (inactive st \<longrightarrow> valid_sched s) \<and> (st = Restart \<longrightarrow> (if a then \<lambda>s. valid_sched s \<and> st_tcb_at runnable thread s \<and> runnable Running else (\<lambda>s. valid_sched s \<and> st_tcb_at runnable thread s \<and> runnable Running)) s) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> valid_sched s) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> valid_sched s) \<and> (awaiting_reply st \<longrightarrow> valid_sched s) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> valid_sched s) \<and> (idle st \<longrightarrow> valid_sched s)
 2. \<And>thread info ptr rv y e s. valid_sched s \<Longrightarrow> valid_sched s
 3. \<And>thread info ptr rv. \<lbrace>?P_no_err5 thread info ptr rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>\<lambda>y s. (invs and valid_invocation rv and ct_active and simple_sched_action and valid_sched and ct_not_queued) s \<and> (invs and valid_invocation rv and ct_active and simple_sched_action and valid_sched and ct_not_queued) s\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_flt5 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args ptr slot cap extracaps
odE \<lbrace>?P_no_err5 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if a then valid_sched else valid_sched\<rbrace>
 5. \<And>thread info ptr. \<lbrace>?B4 thread info ptr\<rbrace> doE (cap, slot) <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt5 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if b then valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle) and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ft) else valid_sched\<rbrace>
 6. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 9. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>thread info ptr rv. \<lbrace>?P_no_err5 thread info ptr rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>\<lambda>y s. (invs and valid_invocation rv and ct_active and simple_sched_action and valid_sched and ct_not_queued) s \<and> (invs and valid_invocation rv and ct_active and simple_sched_action and valid_sched and ct_not_queued) s\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>thread info ptr rv. \<lbrace>?P_no_flt5 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args ptr slot cap extracaps
odE \<lbrace>?P_no_err5 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if a then valid_sched else valid_sched\<rbrace>
 3. \<And>thread info ptr. \<lbrace>?B4 thread info ptr\<rbrace> doE (cap, slot) <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt5 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if b then valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle) and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ft) else valid_sched\<rbrace>
 4. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>thread info ptr. b \<Longrightarrow> \<lbrace>?P'355 thread info ptr\<rbrace> lookup_cap_and_slot thread ptr -, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ptr) False rv)\<rbrace>
 2. \<And>thread info ptr. \<lbrace>?P'343 thread info ptr\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>\<lambda>x s. (b \<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> b \<longrightarrow> valid_sched s) \<and> valid_sched s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> s \<turnstile> fst x \<and> invs s \<and> cte_wp_at ((=) (fst x)) (snd x) s \<and> real_cte_at (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> cur_thread s = thread \<and> simple_sched_action s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> ct_not_queued s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> s \<turnstile> fst x \<and> invs s \<and> cte_wp_at ((=) (fst x)) (snd x) s \<and> real_cte_at (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> cur_thread s = thread \<and> simple_sched_action s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> ct_not_queued s\<rbrace>, \<lbrace>\<lambda>rv s. \<not> b \<longrightarrow> valid_sched s\<rbrace>
 3. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>\<lambda>ptr s. (b \<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> ?P'355 thread info ptr s) \<and> ?P'343 thread info ptr s\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>thread info ptr. b \<Longrightarrow> \<lbrace>?P'355 thread info ptr\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault (CapFault (of_bl ptr) False rv)\<rbrace>
 2. \<And>thread info ptr. \<lbrace>?P'343 thread info ptr\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>\<lambda>x s. (b \<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> b \<longrightarrow> valid_sched s) \<and> valid_sched s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> s \<turnstile> fst x \<and> invs s \<and> cte_wp_at ((=) (fst x)) (snd x) s \<and> real_cte_at (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> cur_thread s = thread \<and> simple_sched_action s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> ct_not_queued s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> s \<turnstile> fst x \<and> invs s \<and> cte_wp_at ((=) (fst x)) (snd x) s \<and> real_cte_at (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> cur_thread s = thread \<and> simple_sched_action s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> ct_not_queued s\<rbrace>, \<lbrace>\<lambda>rv s. \<not> b \<longrightarrow> valid_sched s\<rbrace>
 3. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>\<lambda>ptr s. (b \<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> ?P'355 thread info ptr s) \<and> ?P'343 thread info ptr s\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>thread info ptr. b \<Longrightarrow> \<lbrace>?P'355 thread info ptr\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>?Q358 thread info ptr\<rbrace>, \<lbrace>?E358 thread info ptr\<rbrace>
 2. \<And>thread info ptr rv s. \<lbrakk>b; ?Q358 thread info ptr rv s\<rbrakk> \<Longrightarrow> True
 3. \<And>thread info ptr e s. \<lbrakk>b; ?E358 thread info ptr e s\<rbrakk> \<Longrightarrow> valid_fault (CapFault (of_bl ptr) False e)
 4. \<And>thread info ptr. \<lbrace>?P'343 thread info ptr\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>\<lambda>x s. (b \<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> b \<longrightarrow> valid_sched s) \<and> valid_sched s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> s \<turnstile> fst x \<and> invs s \<and> cte_wp_at ((=) (fst x)) (snd x) s \<and> real_cte_at (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> cur_thread s = thread \<and> simple_sched_action s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> ct_not_queued s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> s \<turnstile> fst x \<and> invs s \<and> cte_wp_at ((=) (fst x)) (snd x) s \<and> real_cte_at (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> cur_thread s = thread \<and> simple_sched_action s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> ct_not_queued s\<rbrace>, \<lbrace>\<lambda>rv s. \<not> b \<longrightarrow> valid_sched s\<rbrace>
 5. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>\<lambda>ptr s. (b \<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> ?P'355 thread info ptr s) \<and> ?P'343 thread info ptr s\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>thread info ptr rv s. \<lbrakk>b; valid_objs s\<rbrakk> \<Longrightarrow> True
 2. \<And>thread info ptr e s. \<lbrakk>b; valid_fault (CapFault (of_bl ptr) (?rp362 thread info ptr) e)\<rbrakk> \<Longrightarrow> valid_fault (CapFault (of_bl ptr) False e)
 3. \<And>thread info ptr. \<lbrace>?P'343 thread info ptr\<rbrace> lookup_cap_and_slot thread ptr \<lbrace>\<lambda>x s. (b \<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> b \<longrightarrow> valid_sched s) \<and> valid_sched s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> s \<turnstile> fst x \<and> invs s \<and> cte_wp_at ((=) (fst x)) (snd x) s \<and> real_cte_at (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> cur_thread s = thread \<and> simple_sched_action s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> ct_not_queued s \<and> st_tcb_at active thread s \<and> invs s \<and> ex_nonz_cap_to thread s \<and> s \<turnstile> fst x \<and> invs s \<and> cte_wp_at ((=) (fst x)) (snd x) s \<and> real_cte_at (snd x) s \<and> ex_cte_cap_wp_to (\<lambda>_. True) (snd x) s \<and> (\<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) \<and> (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s) \<and> invs s \<and> valid_objs s \<and> invs s \<and> cur_thread s = thread \<and> simple_sched_action s \<and> valid_sched s \<and> st_tcb_at runnable thread s \<and> ct_not_queued s\<rbrace>, \<lbrace>\<lambda>rv s. \<not> b \<longrightarrow> valid_sched s\<rbrace>
 4. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>\<lambda>ptr s. (b \<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_objs s) \<and> ?P'343 thread info ptr s\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>s. (invs and valid_sched and ct_active and (\<lambda>s. scheduler_action s = resume_cur_thread)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> valid_sched s \<and> ct_active s \<and> scheduler_action s = resume_cur_thread \<Longrightarrow> (b \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> st_tcb_at active (cur_thread s) s \<and> ct_not_queued s \<and> valid_objs s) \<and> (\<not> b \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) \<and> (b \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> st_tcb_at active (cur_thread s) s \<and> ct_not_queued s) \<and> (\<not> b \<longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s)) \<and> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_queued s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> valid_sched_2 (ready_queues s) (ekheap s) resume_cur_thread (cur_domain s) (kheap s) (cur_thread s) (idle_thread s) \<and> st_tcb_at runnable (cur_thread s) s \<and> ct_not_queued s proof (prove)
goal:
No subgoals!