theory DetSchedSchedule_AI

lemma do_reply_transfer_add_assert:
  assumes a: "\<lbrace>st_tcb_at awaiting_reply receiver and P\<rbrace>
               do_reply_transfer sender receiver slot grant
              \<lbrace>\<lambda>_. Q\<rbrace>"
  shows "\<lbrace>P\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace>" apply (rule hoare_name_pre_state) apply (case_tac "st_tcb_at awaiting_reply receiver s") apply (rule hoare_pre) apply (wp a) apply simp apply (simp add: do_reply_transfer_def) apply (rule hoare_seq_ext) apply (rule hoare_seq_ext) prefer 2 apply (rule assert_false) apply simp apply (simp add: get_thread_state_def thread_get_def) apply wp apply (clarsimp simp: get_tcb_def pred_tcb_at_def obj_at_def
                  split: option.splits kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P s; st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>P s; st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>?Q3 s\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>s sa. \<lbrakk>P s; st_tcb_at awaiting_reply receiver s; s = sa\<rbrakk> \<Longrightarrow> ?Q3 s sa
 3. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>P s; st_tcb_at awaiting_reply receiver s; s = sa\<rbrakk> \<Longrightarrow> (st_tcb_at awaiting_reply receiver and P) sa
 2. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do state <- get_thread_state receiver;
y <- assert (awaiting_reply state);
thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od)
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s state. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>?B8 s state\<rbrace> do y <- assert (awaiting_reply state);
thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od)
od \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_thread_state receiver \<lbrace>?B8 s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s state y. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>?B11 s state y\<rbrace> thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od) \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>s state. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>?B8 s state\<rbrace> assert (awaiting_reply state) \<lbrace>?B11 s state\<rbrace>
 3. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_thread_state receiver \<lbrace>?B8 s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s state. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>?B8 s state\<rbrace> assert (awaiting_reply state) \<lbrace>?B11 s state\<rbrace>
 2. \<And>s state y. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>?B11 s state y\<rbrace> thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od) \<lbrace>\<lambda>_. Q\<rbrace>
 3. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_thread_state receiver \<lbrace>?B8 s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s state y. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. False\<rbrace> thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od) \<lbrace>\<lambda>_. Q\<rbrace>
 2. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_thread_state receiver \<lbrace>\<lambda>state s. state \<noteq> BlockedOnReply\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_thread_state receiver \<lbrace>\<lambda>state s. state \<noteq> BlockedOnReply\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do tcb <- gets_the (get_tcb receiver);
return (tcb_state tcb)
od \<lbrace>\<lambda>state s. state \<noteq> BlockedOnReply\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>P s; \<not> st_tcb_at awaiting_reply receiver s; s = sa\<rbrakk> \<Longrightarrow> get_tcb receiver sa \<noteq> None \<longrightarrow> tcb_state (the (get_tcb receiver sa)) \<noteq> BlockedOnReply proof (prove)
goal:
No subgoals!