theory Ipc_AC

lemma do_reply_transfer_respects:
  "\<lbrace>pas_refined aag and integrity aag X st and einvs \<comment> \<open>cap_delete_one\<close> and tcb_at sender
                    and cte_wp_at (is_reply_cap_to receiver) slot
                    and K (is_subject aag sender)
                    and K (aag_has_auth_to aag Reply receiver)
                    and K (is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver))\<rbrace>
   do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm)+ apply (simp add: do_reply_transfer_def thread_get_def get_thread_state_def) apply (rule hoare_seq_ext[OF _ assert_get_tcb_sp];force?) apply (rule hoare_seq_ext[OF _ assert_sp]) apply (rule hoare_seq_ext[OF _ assert_get_tcb_sp];force?) apply wpc
    \<comment> \<open>No fault case\<close> apply (rule hoare_vcg_if_split[where P= "is_subject aag receiver" and f=f and g=f for f,
                                   simplified if_cancel])
     \<comment> \<open>receiver is a subject\<close> apply ((wp set_thread_state_integrity_autarch thread_set_integrity_autarch
                handle_fault_reply_respects do_ipc_transfer_integrity_autarch
                do_ipc_transfer_pas_refined
             | simp
             | intro conjI impI)+)[1]
    \<comment> \<open>receiver is not a subject\<close> apply (rule use_spec') \<comment> \<open>Name initial state\<close> apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close> apply (rule_tac Q="\<lambda>_ s'. integrity aag X st s \<and>
                              integrity_tcb_in_ipc aag X receiver _ TRFinal s s'" in hoare_post_imp) apply (fastforce dest!: integrity_tcb_in_ipc_final elim!: integrity_trans) apply ((wp possible_switch_to_respects_in_ipc_autarch
               set_thread_state_running_respects_in_ipc_reply
               cte_delete_one_respects_in_ipc_autharch cap_delete_one_reply_st_tcb_at
               do_ipc_transfer_pred_tcb do_ipc_transfer_respects_in_ipc
               do_ipc_transfer_non_null_cte_wp_at2
           | simp add: is_cap_simps is_reply_cap_to_def
           | clarsimp)+)[1]
   \<comment> \<open>fault case\<close> apply (rule hoare_vcg_if_split[where P= "is_subject aag receiver" and f=f and g=f for f,
                                  simplified if_cancel])
    \<comment> \<open>receiver is a subject\<close> apply ((wp set_thread_state_integrity_autarch thread_set_integrity_autarch
               handle_fault_reply_respects
           | simp
           | intro conjI impI)+)[1]
    \<comment> \<open>receiver is not a subject\<close> apply (rule hoare_seq_ext, simp) apply (rule use_spec') \<comment> \<open>Name initial state\<close> apply (simp add: spec_valid_def) \<comment> \<open>no imp rule?\<close> apply wp apply (rule_tac Q="\<lambda>_ s'. integrity aag X st s \<and>
                                      integrity_tcb_in_fault_reply aag X receiver TRFFinal s s'"
                       in hoare_post_imp) apply (fastforce dest!: integrity_tcb_in_fault_reply_final elim!: integrity_trans) apply (wp set_thread_state_respects_in_fault_reply
                    thread_set_no_fault_respects_in_fault_reply
                    handle_fault_reply_respects_in_fault_reply
                 | simp)+ apply (strengthen integrity_tcb_in_fault_reply_refl)+ apply (wp cap_delete_one_reply_st_tcb_at)
  \<comment> \<open>the end\<close> by (force simp: st_tcb_at_tcb_states_of_state cte_wp_at_caps_of_state is_cap_simps
                  is_reply_cap_to_def
           dest!: tcb_states_of_state_kheapD get_tcb_SomeD tcb_atD ko_atD
           intro: tcb_atI fault_tcb_atI emptyable_not_master
          intro!: integrity_tcb_in_ipc_refl tcb_states_of_state_kheapI
           elim!: fault_tcb_atE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and K (is_subject aag sender) and K ((pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag) and K (is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver))\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot\<rbrace> do tcb <- gets_the (get_tcb receiver);
y <- assert (awaiting_reply (tcb_state tcb));
tcb <- gets_the (get_tcb receiver);
case tcb_fault tcb of None \<Rightarrow> 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 | Some f \<Rightarrow> 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>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb\<rbrace> do y <- assert (awaiting_reply (tcb_state tcb));
tcb <- gets_the (get_tcb receiver);
case tcb_fault tcb of None \<Rightarrow> 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 | Some f \<Rightarrow> 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>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb y. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)\<rbrace> do tcb <- gets_the (get_tcb receiver);
case tcb_fault tcb of None \<Rightarrow> 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 | Some f \<Rightarrow> 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>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb y tcba. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba\<rbrace> case tcb_fault tcba of None \<Rightarrow> 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 | Some f \<Rightarrow> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb y tcba. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None\<rbrakk> \<Longrightarrow> \<lbrace>?R60 tcb y tcba\<rbrace> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R61 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> ?R60 tcb y tcba s) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> ?R61 tcb y tcba x s) proof (prove)
goal (4 subgoals):
 1. \<And>tcb y tcba. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None; is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>?Q63 tcb y tcba\<rbrace> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R63 tcb y tcba\<rbrace> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R61 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> ?Q63 tcb y tcba s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R63 tcb y tcba s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> ?R61 tcb y tcba x s) proof (prove)
goal (3 subgoals):
 1. \<And>tcb y tcba. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R63 tcb y tcba\<rbrace> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R61 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R63 tcb y tcba s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> ?R61 tcb y tcba x s) proof (prove)
goal (3 subgoals):
 1. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>?R63 tcb y tcba\<rbrace> 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R61 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R63 tcb y tcba s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> ?R61 tcb y tcba x s) proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcba s. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> ?R63 tcb () tcba sa\<rbrace> do y <- do_ipc_transfer sender None 0 False receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
possible_switch_to receiver
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R61 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R63 tcb y tcba s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> ?R61 tcb y tcba x s) proof (prove)
goal (4 subgoals):
 1. \<And>tcb tcba s rv sa. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None; pasObjectAbs aag receiver \<noteq> pasSubject aag; integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu106 tcb tcba s) TRFinal s sa\<rbrakk> \<Longrightarrow> integrity aag X st sa
 2. \<And>tcb tcba s. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> ?R63 tcb () tcba sa\<rbrace> do y <- do_ipc_transfer sender None 0 False receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
possible_switch_to receiver
od \<lbrace>\<lambda>_ s'. integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu106 tcb tcba s) TRFinal s s'\<rbrace>
 3. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R61 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R63 tcb y tcba s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> ?R61 tcb y tcba x s) proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcba s. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = None; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> ?R63 tcb () tcba sa\<rbrace> do y <- do_ipc_transfer sender None 0 False receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
possible_switch_to receiver
od \<lbrace>\<lambda>_ s'. integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu106 tcb tcba s) TRFinal s s'\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R61 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R63 tcb y tcba s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> ?R61 tcb y tcba x s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R61 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> ?R61 tcb y tcba x s) proof (prove)
goal (3 subgoals):
 1. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; is_subject aag receiver\<rbrakk> \<Longrightarrow> \<lbrace>?Q278 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R278 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> ?Q278 tcb y tcba x s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R278 tcb y tcba x s)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R278 tcb y tcba x2\<rbrace> 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 x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R278 tcb y tcba x s)) proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B341 tcb () tcba x2 ()\<rbrace> do mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R278 tcb y tcba x2\<rbrace> cap_delete_one slot \<lbrace>?B341 tcb y tcba x2\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R278 tcb y tcba x s)) proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcba x2 s. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>?B341 tcb () tcba x2 ()\<rbrace> do mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R278 tcb y tcba x2\<rbrace> cap_delete_one slot \<lbrace>?B341 tcb y tcba x2\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R278 tcb y tcba x s)) proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcba x2 s. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> ?B341 tcb () tcba x2 () sa\<rbrace> do mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 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 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R278 tcb y tcba x2\<rbrace> cap_delete_one slot \<lbrace>?B341 tcb y tcba x2\<rbrace>
 3. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R278 tcb y tcba x s)) proof (prove)
goal (9 subgoals):
 1. \<And>tcb tcba x2 s mi buf mrs restart y. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B353 tcb tcba x2 s mi buf mrs restart y\<rbrace> set_thread_state receiver (if restart then Restart else Inactive) \<lbrace>\<lambda>ya. if restart then integrity aag X st else integrity aag X st\<rbrace>
 2. \<And>tcb tcba x2 s mi buf mrs restart. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B352 tcb tcba x2 s mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>?B353 tcb tcba x2 s mi buf mrs restart\<rbrace>
 3. \<And>tcb tcba x2 s mi buf mrs. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B351 tcb tcba x2 s mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B352 tcb tcba x2 s mi buf mrs\<rbrace>
 4. \<And>tcb tcba x2 s mi buf. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B350 tcb tcba x2 s mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B351 tcb tcba x2 s mi buf\<rbrace>
 5. \<And>tcb tcba x2 s mi. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B349 tcb tcba x2 s mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B350 tcb tcba x2 s mi\<rbrace>
 6. \<And>tcb tcba x2 s. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q348 tcb tcba x2 s\<rbrace> get_message_info sender \<lbrace>?B349 tcb tcba x2 s\<rbrace>
 7. \<And>tcb tcba x2 s sa. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag; sa = s \<and> ?B341 tcb () tcba x2 () sa\<rbrakk> \<Longrightarrow> ?Q348 tcb tcba x2 s sa
 8. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R278 tcb y tcba x2\<rbrace> cap_delete_one slot \<lbrace>?B341 tcb y tcba x2\<rbrace>
 9. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R278 tcb y tcba x s)) proof (prove)
goal (10 subgoals):
 1. \<And>tcb tcba x2 s mi buf mrs restart y rv sa. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag; integrity aag X st s \<and> integrity_tcb_in_fault_reply aag X receiver TRFFinal s sa\<rbrakk> \<Longrightarrow> (if restart then integrity aag X st else integrity aag X st) sa
 2. \<And>tcb tcba x2 s mi buf mrs restart y. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B353 tcb tcba x2 s mi buf mrs restart y\<rbrace> set_thread_state receiver (if restart then Restart else Inactive) \<lbrace>\<lambda>_ s'. integrity aag X st s \<and> integrity_tcb_in_fault_reply aag X receiver TRFFinal s s'\<rbrace>
 3. \<And>tcb tcba x2 s mi buf mrs restart. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B352 tcb tcba x2 s mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>?B353 tcb tcba x2 s mi buf mrs restart\<rbrace>
 4. \<And>tcb tcba x2 s mi buf mrs. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B351 tcb tcba x2 s mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B352 tcb tcba x2 s mi buf mrs\<rbrace>
 5. \<And>tcb tcba x2 s mi buf. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B350 tcb tcba x2 s mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B351 tcb tcba x2 s mi buf\<rbrace>
 6. \<And>tcb tcba x2 s mi. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B349 tcb tcba x2 s mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B350 tcb tcba x2 s mi\<rbrace>
 7. \<And>tcb tcba x2 s. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q348 tcb tcba x2 s\<rbrace> get_message_info sender \<lbrace>?B349 tcb tcba x2 s\<rbrace>
 8. \<And>tcb tcba x2 s sa. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag; sa = s \<and> ?B341 tcb () tcba x2 () sa\<rbrakk> \<Longrightarrow> ?Q348 tcb tcba x2 s sa
 9. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R278 tcb y tcba x2\<rbrace> cap_delete_one slot \<lbrace>?B341 tcb y tcba x2\<rbrace>
 10. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R278 tcb y tcba x s)) proof (prove)
goal (9 subgoals):
 1. \<And>tcb tcba x2 s mi buf mrs restart y. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B353 tcb tcba x2 s mi buf mrs restart y\<rbrace> set_thread_state receiver (if restart then Restart else Inactive) \<lbrace>\<lambda>_ s'. integrity aag X st s \<and> integrity_tcb_in_fault_reply aag X receiver TRFFinal s s'\<rbrace>
 2. \<And>tcb tcba x2 s mi buf mrs restart. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B352 tcb tcba x2 s mi buf mrs restart\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) receiver \<lbrace>?B353 tcb tcba x2 s mi buf mrs restart\<rbrace>
 3. \<And>tcb tcba x2 s mi buf mrs. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B351 tcb tcba x2 s mi buf mrs\<rbrace> handle_fault_reply x2 receiver (mi_label mi) mrs \<lbrace>?B352 tcb tcba x2 s mi buf mrs\<rbrace>
 4. \<And>tcb tcba x2 s mi buf. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B350 tcb tcba x2 s mi buf\<rbrace> get_mrs sender buf mi \<lbrace>?B351 tcb tcba x2 s mi buf\<rbrace>
 5. \<And>tcb tcba x2 s mi. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?B349 tcb tcba x2 s mi\<rbrace> lookup_ipc_buffer False sender \<lbrace>?B350 tcb tcba x2 s mi\<rbrace>
 6. \<And>tcb tcba x2 s. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q348 tcb tcba x2 s\<rbrace> get_message_info sender \<lbrace>?B349 tcb tcba x2 s\<rbrace>
 7. \<And>tcb tcba x2 s sa. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag; sa = s \<and> ?B341 tcb () tcba x2 () sa\<rbrakk> \<Longrightarrow> ?Q348 tcb tcba x2 s sa
 8. \<And>tcb y tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?R278 tcb y tcba x2\<rbrace> cap_delete_one slot \<lbrace>?B341 tcb y tcba x2\<rbrace>
 9. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> ?R278 tcb y tcba x s)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?P'395 tcb () tcba x2\<rbrace> cap_delete_one slot \<lbrace>\<lambda>rv s. integrity_tcb_in_fault_reply aag X receiver TRFContext s s\<rbrace>
 2. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> ?P'395 tcb y tcba x s)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb tcba x2. \<lbrakk>is_subject aag (fst slot) \<and> \<not> grant; (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; tcb_fault tcba = Some x2; pasObjectAbs aag receiver \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> \<lbrace>?P'395 tcb () tcba x2\<rbrace> cap_delete_one slot \<lbrace>\<lambda>r s. st_tcb_at awaiting_reply receiver s \<and> fault_tcb_at (swp (\<noteq>) None) receiver s \<and> (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag \<and> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag s\<rbrace>
 2. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> ?P'395 tcb y tcba x s)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb y tcba s. \<lbrakk>is_subject aag (fst slot) \<and> (grant \<longrightarrow> is_subject aag receiver); (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag; is_subject aag sender; ((\<lambda>s. (pas_refined aag and integrity aag X st and einvs and tcb_at sender and cte_wp_at (is_reply_cap_to receiver) slot and ko_at (TCB tcb) receiver and valid_tcb receiver tcb) s \<and> awaiting_reply (tcb_state tcb)) and ko_at (TCB tcba) receiver and valid_tcb receiver tcba) s\<rbrakk> \<Longrightarrow> (tcb_fault tcba = None \<longrightarrow> (is_subject aag receiver \<longrightarrow> (pas_refined aag and integrity aag X st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (is_subject aag receiver \<and> (grant \<longrightarrow> is_subject aag sender))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and K (grant \<longrightarrow> is_subject aag sender) and K (grant \<longrightarrow> is_subject aag receiver)) s \<and> (invs and tcb_at receiver and tcb_at sender) s \<and> valid_list s \<and> valid_sched s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> integrity aag X st s \<and> integrity_tcb_in_ipc aag X receiver (?uu274 tcb y tcba s) TRContext s s \<and> 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> st_tcb_at can_receive_ipc receiver s \<and> valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_list s \<and> valid_objs s \<and> cte_wp_at is_reply_cap slot s \<and> st_tcb_at awaiting_reply receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'276 tcb y tcba s) False rights) slot s \<and> fault_tcb_at ((=) None) receiver s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap (?t'275 tcb y tcba s) False rights) slot s)) \<and> (\<forall>x. tcb_fault tcba = Some x \<longrightarrow> (is_subject aag receiver \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s \<and> K (is_subject aag receiver) s) \<and> (pasObjectAbs aag receiver \<noteq> pasSubject aag \<longrightarrow> (integrity aag X st and pas_refined aag and einvs and K (is_subject aag (fst slot))) s \<and> (st_tcb_at awaiting_reply receiver and cte_wp_at (is_reply_cap_to (?t'409 tcb y tcba x)) slot) s \<and> (fault_tcb_at (swp (\<noteq>) None) receiver and cte_wp_at (is_reply_cap_to (?t'415 tcb y tcba x)) slot) s \<and> (pasSubject aag, Reply, pasObjectAbs aag receiver) \<in> pasPolicy aag \<and> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (valid_mdb and K (is_subject aag (fst slot)))) s))