theory DetSchedSchedule_AI

lemma perform_invocation_valid_sched[wp]:
  "\<lbrace>invs and valid_invocation i and ct_active and simple_sched_action and valid_sched
         and (\<lambda>s. not_queued (cur_thread s) s)\<rbrace>
     perform_invocation calling blocking i
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (cases i, simp_all) apply (wp invoke_untyped_valid_sched send_ipc_valid_sched | clarsimp)+ apply (clarsimp simp: ct_in_state_def) apply (wp invoke_cnode_valid_sched send_ipc_valid_sched invoke_domain_valid_sched
             | simp add: invs_valid_objs idle_not_reply_cap invs_valid_idle invs_valid_reply_caps
                         is_reply_cap_to_def
             | clarsimp simp: ct_in_state_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_invocation i and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> perform_invocation calling blocking i \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. i = InvokeUntyped x1 \<Longrightarrow> \<lbrace>invs and valid_untyped_inv x1 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- invoke_untyped x1;
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x21 x22 x23 x24. i = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs and (ep_at x21 and ex_nonz_cap_to x21) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> liftE (do thread <- gets cur_thread;
y <- send_ipc calling blocking x22 x23 x24 thread x21;
return []
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>x31 x32. i = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>invs and (ntfn_at x31 and ex_nonz_cap_to x31) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- liftE (send_signal x31 x32);
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>x41 x42 x43. i = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>invs and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41 False R) x42) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> liftE (do sender <- gets cur_thread;
y <- do_reply_transfer sender x41 x42 x43;
return []
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>x5. i = InvokeTCB x5 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf x5 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> invoke_tcb x5 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>x61 x62. i = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>invs and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s)) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> invoke_domain x61 x62 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>x7. i = InvokeCNode x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv x7 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- invoke_cnode x7;
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>invs and irq_control_inv_valid x8 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- invoke_irq_control x8;
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 9. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>invs and irq_handler_inv_valid x9 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 10. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>invs and valid_arch_inv x10 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> arch_perform_invocation x10 \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>x21 x22 x23 x24 s. \<lbrakk>i = InvokeEndpoint x21 x22 x23 x24; invs s; ep_at x21 s; ex_nonz_cap_to x21 s; ct_active s; simple_sched_action s; valid_sched s; ct_not_queued s\<rbrakk> \<Longrightarrow> st_tcb_at active (cur_thread s) s
 2. \<And>x31 x32. i = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>invs and (ntfn_at x31 and ex_nonz_cap_to x31) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- liftE (send_signal x31 x32);
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>x41 x42 x43. i = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>invs and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41 False R) x42) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> liftE (do sender <- gets cur_thread;
y <- do_reply_transfer sender x41 x42 x43;
return []
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>x5. i = InvokeTCB x5 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf x5 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> invoke_tcb x5 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>x61 x62. i = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>invs and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s)) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> invoke_domain x61 x62 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>x7. i = InvokeCNode x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv x7 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- invoke_cnode x7;
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>invs and irq_control_inv_valid x8 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- invoke_irq_control x8;
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>invs and irq_handler_inv_valid x9 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 9. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>invs and valid_arch_inv x10 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> arch_perform_invocation x10 \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x31 x32. i = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>invs and (ntfn_at x31 and ex_nonz_cap_to x31) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- liftE (send_signal x31 x32);
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>x41 x42 x43. i = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>invs and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = ReplyCap x41 False R) x42) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> liftE (do sender <- gets cur_thread;
y <- do_reply_transfer sender x41 x42 x43;
return []
od) \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>x5. i = InvokeTCB x5 \<Longrightarrow> \<lbrace>invs and tcb_inv_wf x5 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> invoke_tcb x5 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>x61 x62. i = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>invs and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s)) and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> invoke_domain x61 x62 \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>x7. i = InvokeCNode x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv x7 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- invoke_cnode x7;
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>invs and irq_control_inv_valid x8 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- invoke_irq_control x8;
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>invs and irq_handler_inv_valid x9 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> doE y <- liftE (invoke_irq_handler x9);
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 8. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>invs and valid_arch_inv x10 and ct_active and simple_sched_action and valid_sched and ct_not_queued\<rbrace> arch_perform_invocation x10 \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!