theory Ipc_AC

lemma do_reply_transfer_pas_refined:
  "\<lbrace>pas_refined aag and invs and K (is_subject aag sender)
                    and K ((grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))\<rbrace>
   do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: do_reply_transfer_def) apply (rule hoare_pre) apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined
            thread_set_pas_refined K_valid
         | wpc | simp add: thread_get_def split del: if_split)+ 
  (* otherwise simp does too much *)
   apply (rule hoare_strengthen_post, rule gts_inv) apply (rule impI) apply assumption apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and K (is_subject aag sender) and K ((grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and (\<lambda>y. is_subject aag sender) and (\<lambda>y. (grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))\<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;
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 (possible_switch_to receiver)
od)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<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;
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 (possible_switch_to receiver)
od)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>s. (pas_refined aag and invs and (\<lambda>y. is_subject aag sender) and (\<lambda>y. (grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>\<lambda>state s. awaiting_reply state \<longrightarrow> (\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> (tcb_fault (the (get_tcb receiver s)) = None \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (grant \<longrightarrow> is_subject aag sender) \<and> (grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. tcb_fault (the (get_tcb receiver s)) = Some x) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)\<rbrace>
 2. \<And>s. (pas_refined aag and invs and (\<lambda>y. is_subject aag sender) and (\<lambda>y. (grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_thread_state receiver \<lbrace>\<lambda>state s. awaiting_reply state \<longrightarrow> (\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> (tcb_fault (the (get_tcb receiver s)) = None \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (grant \<longrightarrow> is_subject aag sender) \<and> (grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. tcb_fault (the (get_tcb receiver s)) = Some x) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)\<rbrace>
 2. \<And>s. (pas_refined aag and invs and (\<lambda>y. is_subject aag sender) and (\<lambda>y. (grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q4 s \<Longrightarrow> awaiting_reply rv \<longrightarrow> (\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> (tcb_fault (the (get_tcb receiver s)) = None \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (grant \<longrightarrow> is_subject aag sender) \<and> (grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. tcb_fault (the (get_tcb receiver s)) = Some x) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)
 2. \<And>s. (pas_refined aag and invs and (\<lambda>y. is_subject aag sender) and (\<lambda>y. (grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>?Q4 s; awaiting_reply rv\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> (tcb_fault (the (get_tcb receiver s)) = None \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (grant \<longrightarrow> is_subject aag sender) \<and> (grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. tcb_fault (the (get_tcb receiver s)) = Some x) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)
 2. \<And>s. (pas_refined aag and invs and (\<lambda>y. is_subject aag sender) and (\<lambda>y. (grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and invs and (\<lambda>y. is_subject aag sender) and (\<lambda>y. (grant \<longrightarrow> is_subject aag receiver) \<and> is_subject aag (fst slot))) s \<Longrightarrow> (\<exists>y. get_tcb receiver s = Some y) \<longrightarrow> (tcb_fault (the (get_tcb receiver s)) = None \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_mdb s \<and> (grant \<longrightarrow> is_subject aag sender) \<and> (grant \<longrightarrow> is_subject aag receiver) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) \<and> ((\<exists>x. tcb_fault (the (get_tcb receiver s)) = Some x) \<longrightarrow> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (fst slot) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s) proof (prove)
goal:
No subgoals!