theory Syscall_AI

lemma hr_ct_active[wp]:
  "\<lbrace>invs and ct_active\<rbrace> handle_reply \<lbrace>\<lambda>rv. ct_active :: 'state_ext state \<Rightarrow> _\<rbrace>" apply (simp add: handle_reply_def) apply (rule hoare_seq_ext) apply (rule_tac t=thread in ct_in_state_decomp) apply ((wp hoare_drop_imps hoare_vcg_all_lift | wpc | simp)+)[1] apply (wp hoare_vcg_all_lift get_cap_wp do_reply_transfer_st_tcb_at_active
        | wpc | simp)+ apply (fastforce simp: ct_in_state_def cte_wp_at_caps_of_state is_reply_cap_to_def
                  dest: invs_valid_reply_caps
                  elim: valid_reply_caps_of_stateD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active\<rbrace> handle_reply \<lbrace>\<lambda>rv. ct_active\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active\<rbrace> do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. ct_active\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>?B thread\<rbrace> do caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. ct_active\<rbrace>
 2. \<lbrace>invs and ct_active\<rbrace> gets cur_thread \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>\<lambda>s. thread = cur_thread s\<rbrace> do caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. thread = cur_thread s\<rbrace>
 2. \<And>thread. \<lbrace>?Pre3 thread\<rbrace> do caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. st_tcb_at active thread\<rbrace>
 3. \<lbrace>invs and ct_active\<rbrace> gets cur_thread \<lbrace>\<lambda>thread s. ?Pre3 thread s \<and> thread = cur_thread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>?Pre3 thread\<rbrace> do caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv. st_tcb_at active thread\<rbrace>
 2. \<lbrace>invs and ct_active\<rbrace> gets cur_thread \<lbrace>\<lambda>thread s. ?Pre3 thread s \<and> thread = cur_thread s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> ct_active s \<Longrightarrow> \<forall>x. cte_wp_at ((=) x) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (x = NullCap \<longrightarrow> st_tcb_at active (cur_thread s) s) \<and> (\<forall>xa xb. (\<exists>xc. x = ReplyCap xa xb xc) \<longrightarrow> \<not> xb \<longrightarrow> valid_objs s \<and> st_tcb_at active (cur_thread s) s \<and> st_tcb_at awaiting_reply xa s \<and> cte_wp_at (is_reply_cap_to xa) (cur_thread s, tcb_cnode_index 3) s) proof (prove)
goal:
No subgoals!