theory Syscall_AI

lemma do_reply_transfer_st_tcb_at_active:
  "\<lbrace>valid_objs and st_tcb_at active t and st_tcb_at awaiting_reply t' and
    cte_wp_at (is_reply_cap_to t') sl\<rbrace>
    do_reply_transfer t t' sl grant
   \<lbrace>\<lambda>rv. st_tcb_at active t :: 'state_ext state \<Rightarrow> _\<rbrace>" apply (simp add: do_reply_transfer_def is_reply_cap_to_def) apply (wp drop_when_dxo_wp sts_st_tcb_at' sts_st_tcb_at_neq cap_delete_one_reply_st_tcb_at
            hoare_drop_imps thread_set_no_change_tcb_state
            do_ipc_transfer_non_null_cte_wp_at2
       | wpc | clarsimp simp: is_reply_cap_to_def)+ apply (wp hoare_allI hoare_drop_imp)+ apply (fastforce simp add: st_tcb_def2 is_reply_cap_to_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and st_tcb_at active t and st_tcb_at awaiting_reply t' and cte_wp_at (is_reply_cap_to t') sl\<rbrace> do_reply_transfer t t' sl grant \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and st_tcb_at active t and st_tcb_at awaiting_reply t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t' False rights) sl\<rbrace> do state <- get_thread_state t';
y <- assert (awaiting_reply state);
thread_get tcb_fault t' >>= case_option (do y <- do_ipc_transfer t None 0 grant t';
y <- cap_delete_one sl;
y <- set_thread_state t' Running;
do_extended_op (possible_switch_to t')
od) (\<lambda>f. do y <- cap_delete_one sl;
mi <- get_message_info t;
buf <- lookup_ipc_buffer False t;
mrs <- get_mrs t buf mi;
restart <- handle_fault_reply f t' (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) t';
y <- set_thread_state t' (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to t'))
od)
od \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>state. \<lbrace>?P'99 state ()\<rbrace> thread_get tcb_fault t' \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> st_tcb_at active t s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'95 state () (Some x) x) False rights) sl s \<and> t \<noteq> t'\<rbrace>
 2. \<And>state. \<lbrace>?B5 state\<rbrace> assert (awaiting_reply state) \<lbrace>\<lambda>y s. (st_tcb_at active t s \<and> (valid_objs and cte_wp_at (is_reply_cap_to (?t'102 state y)) sl) s \<and> K (t \<noteq> t') s) \<and> ?P'99 state y s\<rbrace>
 3. \<lbrace>?Q4\<rbrace> get_thread_state t' \<lbrace>?B5\<rbrace>
 4. \<And>s. (valid_objs and st_tcb_at active t and st_tcb_at awaiting_reply t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t' False rights) sl) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and st_tcb_at active t and st_tcb_at awaiting_reply t' and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t' False rights) sl) s \<Longrightarrow> (st_tcb_at active t s \<and> (valid_objs and cte_wp_at (is_reply_cap_to (?t'130 ())) sl) s \<and> K (t \<noteq> t') s) \<and> st_tcb_at active t s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'128 ()) False rights) sl s \<and> t \<noteq> t'
flex-flex pairs:
?t'128 () \<equiv>\<^sup>? ?t'132 () proof (prove)
goal:
No subgoals!