theory DetSchedSchedule_AI

lemma tc_valid_sched[wp]:
  "\<lbrace>valid_sched and simple_sched_action and (\<lambda>s. a \<noteq> idle_thread s)\<rbrace>
      invoke_tcb (ThreadControl a sl b mcp pr e f g)
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply clarsimp apply wp apply wpsimp apply wpc apply (clarsimp simp: if_apply_def2 eq_commute[where a=a] option_update_thread_def
               | wpsimp wp: hoare_drop_imps reschedule_preserves_valid_sched
                                  hoare_lift_Pf [where f= "cur_thread" and P="\<lambda>x s. x \<noteq> idle_thread s"]
                                  check_cap_inv cap_insert_valid_sched thread_set_not_state_valid_sched
                      cong: conj_cong imp_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and simple_sched_action and (\<lambda>s. a \<noteq> idle_thread s)\<rbrace> invoke_tcb (ThreadControl a sl b mcp pr e f g) \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and simple_sched_action and (\<lambda>s. a \<noteq> idle_thread s)\<rbrace> doE y <- liftE (option_update_thread a (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) b);
y <- liftE (case mcp of None \<Rightarrow> return () | Some (newmcp, x) \<Rightarrow> set_mcpriority a newmcp);
y <- case e of None \<Rightarrow> returnOk () | Some (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index 0))))
odE;
y <- case f of None \<Rightarrow> returnOk () | Some (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index (Suc 0));
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index (Suc 0)))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some (ptr, frame) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. ptr)) a);
y <- liftE (case frame of None \<Rightarrow> return () | Some (new_cap, src_slot) \<Rightarrow> check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (a = cur) reschedule_required)
odE;
y <- liftE (case pr of None \<Rightarrow> return () | Some (prio, x) \<Rightarrow> set_priority a prio);
returnOk []
odE \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc yd. \<lbrace>?B30 y ya yb yc yd\<rbrace> case pr of None \<Rightarrow> return () | Some (prio, x) \<Rightarrow> set_priority a prio \<lbrace>\<lambda>ye. valid_sched\<rbrace>
 2. \<And>y ya yb yc. \<lbrace>?B29 y ya yb yc\<rbrace> case g of None \<Rightarrow> returnOk () | Some (ptr, frame) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. ptr)) a);
y <- liftE (case frame of None \<Rightarrow> return () | Some (new_cap, src_slot) \<Rightarrow> check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (a = cur) reschedule_required)
odE \<lbrace>?B30 y ya yb yc\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>y ya yb. \<lbrace>?B28 y ya yb\<rbrace> case f of None \<Rightarrow> returnOk () | Some (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index (Suc 0));
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index (Suc 0)))))
odE \<lbrace>?B29 y ya yb\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>y ya. \<lbrace>?B27 y ya\<rbrace> case e of None \<Rightarrow> returnOk () | Some (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index 0))))
odE \<lbrace>?B28 y ya\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>y. \<lbrace>?B26 y\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some (newmcp, x) \<Rightarrow> set_mcpriority a newmcp) \<lbrace>?B27 y\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<lbrace>?Q24\<rbrace> liftE (option_update_thread a (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) b) \<lbrace>?B26\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>s. (valid_sched and simple_sched_action and (\<lambda>s. a \<noteq> idle_thread s)) s \<Longrightarrow> ?Q24 s proof (prove)
goal (6 subgoals):
 1. \<And>y ya yb yc. \<lbrace>?B29 y ya yb yc\<rbrace> case g of None \<Rightarrow> returnOk () | Some (ptr, frame) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. ptr)) a);
y <- liftE (case frame of None \<Rightarrow> return () | Some (new_cap, src_slot) \<Rightarrow> check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (a = cur) reschedule_required)
odE \<lbrace>\<lambda>yd s. (pr = None \<longrightarrow> valid_sched s) \<and> (\<forall>x. pr = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (valid_sched and (\<lambda>s. a \<noteq> idle_thread s)) s))\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>y ya yb. \<lbrace>?B28 y ya yb\<rbrace> case f of None \<Rightarrow> returnOk () | Some (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index (Suc 0));
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index (Suc 0)))))
odE \<lbrace>?B29 y ya yb\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>y ya. \<lbrace>?B27 y ya\<rbrace> case e of None \<Rightarrow> returnOk () | Some (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index 0))))
odE \<lbrace>?B28 y ya\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>y. \<lbrace>?B26 y\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some (newmcp, x) \<Rightarrow> set_mcpriority a newmcp) \<lbrace>?B27 y\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<lbrace>?Q24\<rbrace> liftE (option_update_thread a (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) b) \<lbrace>?B26\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<And>s. (valid_sched and simple_sched_action and (\<lambda>s. a \<noteq> idle_thread s)) s \<Longrightarrow> ?Q24 s proof (prove)
goal (7 subgoals):
 1. \<And>y ya yb yc. g = None \<Longrightarrow> \<lbrace>?R67 y ya yb yc\<rbrace> returnOk () \<lbrace>\<lambda>yd s. (pr = None \<longrightarrow> valid_sched s) \<and> (\<forall>x. pr = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (valid_sched and (\<lambda>s. a \<noteq> idle_thread s)) s))\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 2. \<And>y ya yb yc x2. g = Some x2 \<Longrightarrow> \<lbrace>?R68 y ya yb yc x2\<rbrace> case x2 of (ptr, frame) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 4);
y <- liftE (thread_set (tcb_ipc_buffer_update (\<lambda>_. ptr)) a);
y <- liftE (case frame of None \<Rightarrow> return () | Some (new_cap, src_slot) \<Rightarrow> check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index 4))));
cur <- liftE (gets cur_thread);
liftE (when (a = cur) reschedule_required)
odE \<lbrace>\<lambda>yd s. (pr = None \<longrightarrow> valid_sched s) \<and> (\<forall>x. pr = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (valid_sched and (\<lambda>s. a \<noteq> idle_thread s)) s))\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 3. \<And>y ya yb. \<lbrace>?B28 y ya yb\<rbrace> case f of None \<Rightarrow> returnOk () | Some (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index (Suc 0));
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index (Suc 0)))))
odE \<lbrace>\<lambda>yc s. (g = None \<longrightarrow> ?R67 y ya yb yc s) \<and> (\<forall>x. g = Some x \<longrightarrow> ?R68 y ya yb yc x s)\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 4. \<And>y ya. \<lbrace>?B27 y ya\<rbrace> case e of None \<Rightarrow> returnOk () | Some (new_cap, src_slot) \<Rightarrow> doE y <- cap_delete (a, tcb_cnode_index 0);
liftE (check_cap_at new_cap src_slot (check_cap_at (ThreadCap a) sl (cap_insert new_cap src_slot (a, tcb_cnode_index 0))))
odE \<lbrace>?B28 y ya\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 5. \<And>y. \<lbrace>?B26 y\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some (newmcp, x) \<Rightarrow> set_mcpriority a newmcp) \<lbrace>?B27 y\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 6. \<lbrace>?Q24\<rbrace> liftE (option_update_thread a (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) b) \<lbrace>?B26\<rbrace>, \<lbrace>\<lambda>rv. valid_sched\<rbrace>
 7. \<And>s. (valid_sched and simple_sched_action and (\<lambda>s. a \<noteq> idle_thread s)) s \<Longrightarrow> ?Q24 s proof (prove)
goal:
No subgoals!