theory Ipc_DR

lemma handle_reply_cur_thread_idle_thread:
  "\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> Syscall_A.handle_reply
            \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s) \<rbrace>" apply (simp add:handle_reply_def) apply (wp do_ipc_transfer_cur_thread_idle_thread|wpc)+ apply (clarsimp simp:Ipc_A.do_reply_transfer_def) apply (wp set_thread_state_cur_thread_idle_thread dxo_wp_weak
                |wpc|simp add: trans_state_def)+ apply ((wps|wp cap_delete_one_it)+)[1] apply (wp do_ipc_transfer_cur_thread_idle_thread dxo_wp_weak)+ apply (clarsimp simp: trans_state_def) apply (case_tac xf) apply (simp | wp set_thread_state_cur_thread_idle_thread
                                    thread_set_cur_thread_idle_thread)+ apply ((wps | wp)+)[1] apply wp+ apply ((wps | wp cap_delete_one_it)+)[1] apply (rule hoare_drop_imp | rule hoare_conjI | rule hoare_allI | wp)+ apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> Syscall_A.handle_reply \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do thread <- gets cur_thread;
caller_cap <- CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3);
case caller_cap of cap.NullCap \<Rightarrow> return () | cap.ReplyCap caller True R \<Rightarrow> fail | cap.ReplyCap caller False R \<Rightarrow> Ipc_A.do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>thread caller_cap x51 x52 x53. \<lbrakk>caller_cap = cap.ReplyCap x51 x52 x53; x52 = False\<rbrakk> \<Longrightarrow> \<lbrace>?R91 thread caller_cap x51 x52 x53\<rbrace> Ipc_A.do_reply_transfer thread x51 (thread, tcb_cnode_index 3) (AllowGrant \<in> x53) \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 2. \<And>thread caller_cap x61 x62 x63. caller_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 thread caller_cap x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 3. \<And>thread caller_cap x7. caller_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 thread caller_cap x7\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 4. \<And>thread caller_cap. caller_cap = cap.DomainCap \<Longrightarrow> \<lbrace>?R59 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 5. \<And>thread caller_cap. caller_cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 6. \<And>thread caller_cap x10. caller_cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 thread caller_cap x10\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 7. \<And>thread caller_cap x111 x112 x113. caller_cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>?R62 thread caller_cap x111 x112 x113\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 8. \<And>thread caller_cap x12. caller_cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 thread caller_cap x12\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 9. \<And>thread. \<lbrace>?B1 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>caller_cap s. (caller_cap = cap.NullCap \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>x xa xb xc. caller_cap = cap.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = cap.EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = cap.NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = cap.ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> ?R91 thread caller_cap x xa xb s)) \<and> (\<forall>x xa xb. caller_cap = cap.CNodeCap x xa xb \<longrightarrow> ?R57 thread caller_cap x xa xb s) \<and> (\<forall>x. caller_cap = ThreadCap x \<longrightarrow> ?R58 thread caller_cap x s) \<and> (caller_cap = cap.DomainCap \<longrightarrow> ?R59 thread caller_cap s) \<and> (caller_cap = IRQControlCap \<longrightarrow> ?R60 thread caller_cap s) \<and> (\<forall>x. caller_cap = IRQHandlerCap x \<longrightarrow> ?R61 thread caller_cap x s) \<and> (\<forall>x xa xb. caller_cap = Zombie x xa xb \<longrightarrow> ?R62 thread caller_cap x xa xb s) \<and> (\<forall>x. caller_cap = ArchObjectCap x \<longrightarrow> ?R63 thread caller_cap x s)\<rbrace>
 10. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>thread x51 x52 x53. \<not> x52 \<Longrightarrow> \<lbrace>?R91 thread (cap.ReplyCap x51 False x53) x51 False x53\<rbrace> do state <- get_thread_state x51;
y <- assert (awaiting_reply state);
thread_get tcb_fault x51 >>= case_option (do y <- Ipc_A.do_ipc_transfer thread None 0 (AllowGrant \<in> x53) x51;
y <- cap_delete_one (thread, tcb_cnode_index 3);
y <- set_thread_state x51 Running;
do_extended_op (possible_switch_to x51)
od) (\<lambda>f. do y <- cap_delete_one (thread, tcb_cnode_index 3);
mi <- get_message_info thread;
buf <- lookup_ipc_buffer False thread;
mrs <- get_mrs thread buf mi;
restart <- handle_fault_reply f x51 (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) x51;
y <- set_thread_state x51 (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to x51))
od)
od \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 2. \<And>thread caller_cap x61 x62 x63. caller_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 thread caller_cap x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 3. \<And>thread caller_cap x7. caller_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 thread caller_cap x7\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 4. \<And>thread caller_cap. caller_cap = cap.DomainCap \<Longrightarrow> \<lbrace>?R59 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 5. \<And>thread caller_cap. caller_cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 6. \<And>thread caller_cap x10. caller_cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 thread caller_cap x10\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 7. \<And>thread caller_cap x111 x112 x113. caller_cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>?R62 thread caller_cap x111 x112 x113\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 8. \<And>thread caller_cap x12. caller_cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 thread caller_cap x12\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 9. \<And>thread. \<lbrace>?B1 thread\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 3) \<lbrace>\<lambda>caller_cap s. (caller_cap = cap.NullCap \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>x xa xb xc. caller_cap = cap.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = cap.EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = cap.NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. caller_cap = cap.ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> True) \<and> (xa = False \<longrightarrow> ?R91 thread caller_cap x xa xb s)) \<and> (\<forall>x xa xb. caller_cap = cap.CNodeCap x xa xb \<longrightarrow> ?R57 thread caller_cap x xa xb s) \<and> (\<forall>x. caller_cap = ThreadCap x \<longrightarrow> ?R58 thread caller_cap x s) \<and> (caller_cap = cap.DomainCap \<longrightarrow> ?R59 thread caller_cap s) \<and> (caller_cap = IRQControlCap \<longrightarrow> ?R60 thread caller_cap s) \<and> (\<forall>x. caller_cap = IRQHandlerCap x \<longrightarrow> ?R61 thread caller_cap x s) \<and> (\<forall>x xa xb. caller_cap = Zombie x xa xb \<longrightarrow> ?R62 thread caller_cap x xa xb s) \<and> (\<forall>x. caller_cap = ArchObjectCap x \<longrightarrow> ?R63 thread caller_cap x s)\<rbrace>
 10. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
A total of 11 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>thread x51 x52 x53 state xa. \<lbrakk>\<not> x52; xa = None\<rbrakk> \<Longrightarrow> \<lbrace>?B119 thread x51 False x53 state () None ()\<rbrace> cap_delete_one (thread, tcb_cnode_index 3) \<lbrace>\<lambda>xc s. P (cur_thread s) (idle_thread s)\<rbrace>
 2. \<And>thread x51 x52 x53 state x xa. \<lbrakk>\<not> x52; xa = None\<rbrakk> \<Longrightarrow> \<lbrace>?R115 thread x51 x52 x53 state x xa\<rbrace> Ipc_A.do_ipc_transfer thread None 0 (AllowGrant \<in> x53) x51 \<lbrace>?B119 thread x51 x52 x53 state x xa\<rbrace>
 3. \<And>thread x51 x52 x53 state x xa x2. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R116 thread x51 x52 x53 state x xa x2\<rbrace> do y <- cap_delete_one (thread, tcb_cnode_index 3);
mi <- get_message_info thread;
buf <- lookup_ipc_buffer False thread;
mrs <- get_mrs thread buf mi;
restart <- handle_fault_reply x2 x51 (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) x51;
y <- set_thread_state x51 (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to x51))
od \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 4. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R115 thread x51 x52 x53 state x xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R116 thread x51 x52 x53 state x xa xb s)\<rbrace>
 5. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
 6. \<And>thread x51 x52 x53. \<not> x52 \<Longrightarrow> \<lbrace>?R91 thread (cap.ReplyCap x51 False x53) x51 (ds_id False) x53\<rbrace> get_thread_state x51 \<lbrace>?B102 thread x51 x52 x53\<rbrace>
 7. \<And>thread caller_cap x61 x62 x63. caller_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 thread caller_cap x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 8. \<And>thread caller_cap x7. caller_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 thread caller_cap x7\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 9. \<And>thread caller_cap. caller_cap = cap.DomainCap \<Longrightarrow> \<lbrace>?R59 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 10. \<And>thread caller_cap. caller_cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>thread x51 x52 x53 state x xa. \<lbrakk>\<not> x52; xa = None\<rbrakk> \<Longrightarrow> \<lbrace>?R115 thread x51 x52 x53 state x xa\<rbrace> Ipc_A.do_ipc_transfer thread None 0 (AllowGrant \<in> x53) x51 \<lbrace>\<lambda>a b. P (cur_thread b) (idle_thread b)\<rbrace>
 2. \<And>thread x51 x52 x53 state x xa x2. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R116 thread x51 x52 x53 state x xa x2\<rbrace> do y <- cap_delete_one (thread, tcb_cnode_index 3);
mi <- get_message_info thread;
buf <- lookup_ipc_buffer False thread;
mrs <- get_mrs thread buf mi;
restart <- handle_fault_reply x2 x51 (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) x51;
y <- set_thread_state x51 (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to x51))
od \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 3. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R115 thread x51 x52 x53 state x xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R116 thread x51 x52 x53 state x xa xb s)\<rbrace>
 4. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
 5. \<And>thread x51 x52 x53. \<not> x52 \<Longrightarrow> \<lbrace>?R91 thread (cap.ReplyCap x51 False x53) x51 (ds_id False) x53\<rbrace> get_thread_state x51 \<lbrace>?B102 thread x51 x52 x53\<rbrace>
 6. \<And>thread caller_cap x61 x62 x63. caller_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 thread caller_cap x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 7. \<And>thread caller_cap x7. caller_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 thread caller_cap x7\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 8. \<And>thread caller_cap. caller_cap = cap.DomainCap \<Longrightarrow> \<lbrace>?R59 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 9. \<And>thread caller_cap. caller_cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 10. \<And>thread caller_cap x10. caller_cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 thread caller_cap x10\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
A total of 15 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg xh s f. \<lbrakk>\<not> x52; xa = Some x2; xf\<rbrakk> \<Longrightarrow> P (cur_thread (trans_state f s)) (idle_thread (trans_state f s)) = P (cur_thread s) (idle_thread s)
 2. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B146 thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg\<rbrace> set_thread_state x51 (if xf then Restart else Inactive) \<lbrace>\<lambda>xh. if xf then \<lambda>s. P (cur_thread s) (idle_thread s) else (\<lambda>s. P (cur_thread s) (idle_thread s))\<rbrace>
 3. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe xf. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B145 thread x51 x52 x53 state x xa x2 xb xc xd xe xf\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) x51 \<lbrace>?B146 thread x51 x52 x53 state x xa x2 xb xc xd xe xf\<rbrace>
 4. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B144 thread x51 x52 x53 state x xa x2 xb xc xd xe\<rbrace> handle_fault_reply x2 x51 (mi_label xc) xe \<lbrace>?B145 thread x51 x52 x53 state x xa x2 xb xc xd xe\<rbrace>
 5. \<And>thread x51 x52 x53 state x xa x2 xb xc xd. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace> get_mrs thread xd xc \<lbrace>?B144 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace>
 6. \<And>thread x51 x52 x53 state x xa x2 xb xc. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb xc\<rbrace> lookup_ipc_buffer False thread \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc\<rbrace>
 7. \<And>thread x51 x52 x53 state x xa x2 xb. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread x51 x52 x53 state x xa x2 xb\<rbrace> get_message_info thread \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb\<rbrace>
 8. \<And>thread x51 x52 x53 state x xa x2. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R116 thread x51 x52 x53 state x xa x2\<rbrace> cap_delete_one (thread, tcb_cnode_index 3) \<lbrace>?B141 thread x51 x52 x53 state x xa x2\<rbrace>
 9. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R116 thread x51 x52 x53 state x xa xb s)\<rbrace>
 10. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
A total of 21 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B146 thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg\<rbrace> set_thread_state x51 (if xf then Restart else Inactive) \<lbrace>\<lambda>xh. if xf then \<lambda>s. P (cur_thread s) (idle_thread s) else (\<lambda>s. P (cur_thread s) (idle_thread s))\<rbrace>
 2. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe xf. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B145 thread x51 x52 x53 state x xa x2 xb xc xd xe xf\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) x51 \<lbrace>?B146 thread x51 x52 x53 state x xa x2 xb xc xd xe xf\<rbrace>
 3. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B144 thread x51 x52 x53 state x xa x2 xb xc xd xe\<rbrace> handle_fault_reply x2 x51 (mi_label xc) xe \<lbrace>?B145 thread x51 x52 x53 state x xa x2 xb xc xd xe\<rbrace>
 4. \<And>thread x51 x52 x53 state x xa x2 xb xc xd. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace> get_mrs thread xd xc \<lbrace>?B144 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace>
 5. \<And>thread x51 x52 x53 state x xa x2 xb xc. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb xc\<rbrace> lookup_ipc_buffer False thread \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc\<rbrace>
 6. \<And>thread x51 x52 x53 state x xa x2 xb. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread x51 x52 x53 state x xa x2 xb\<rbrace> get_message_info thread \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb\<rbrace>
 7. \<And>thread x51 x52 x53 state x xa x2. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R116 thread x51 x52 x53 state x xa x2\<rbrace> cap_delete_one (thread, tcb_cnode_index 3) \<lbrace>?B141 thread x51 x52 x53 state x xa x2\<rbrace>
 8. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R116 thread x51 x52 x53 state x xa xb s)\<rbrace>
 9. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
 10. \<And>thread x51 x52 x53. \<not> x52 \<Longrightarrow> \<lbrace>?R91 thread (cap.ReplyCap x51 False x53) x51 (ds_id False) x53\<rbrace> get_thread_state x51 \<lbrace>?B102 thread x51 x52 x53\<rbrace>
A total of 20 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg. \<lbrakk>\<not> x52; xa = Some x2; xf\<rbrakk> \<Longrightarrow> \<lbrace>?B146 thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg\<rbrace> set_thread_state x51 (if xf then Restart else Inactive) \<lbrace>\<lambda>xh. if xf then \<lambda>s. P (cur_thread s) (idle_thread s) else (\<lambda>s. P (cur_thread s) (idle_thread s))\<rbrace>
 2. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg. \<lbrakk>\<not> x52; xa = Some x2; \<not> xf\<rbrakk> \<Longrightarrow> \<lbrace>?B146 thread x51 x52 x53 state x xa x2 xb xc xd xe xf xg\<rbrace> set_thread_state x51 (if xf then Restart else Inactive) \<lbrace>\<lambda>xh. if xf then \<lambda>s. P (cur_thread s) (idle_thread s) else (\<lambda>s. P (cur_thread s) (idle_thread s))\<rbrace>
 3. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe xf. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B145 thread x51 x52 x53 state x xa x2 xb xc xd xe xf\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) x51 \<lbrace>?B146 thread x51 x52 x53 state x xa x2 xb xc xd xe xf\<rbrace>
 4. \<And>thread x51 x52 x53 state x xa x2 xb xc xd xe. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B144 thread x51 x52 x53 state x xa x2 xb xc xd xe\<rbrace> handle_fault_reply x2 x51 (mi_label xc) xe \<lbrace>?B145 thread x51 x52 x53 state x xa x2 xb xc xd xe\<rbrace>
 5. \<And>thread x51 x52 x53 state x xa x2 xb xc xd. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace> get_mrs thread xd xc \<lbrace>?B144 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace>
 6. \<And>thread x51 x52 x53 state x xa x2 xb xc. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb xc\<rbrace> lookup_ipc_buffer False thread \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc\<rbrace>
 7. \<And>thread x51 x52 x53 state x xa x2 xb. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread x51 x52 x53 state x xa x2 xb\<rbrace> get_message_info thread \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb\<rbrace>
 8. \<And>thread x51 x52 x53 state x xa x2. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R116 thread x51 x52 x53 state x xa x2\<rbrace> cap_delete_one (thread, tcb_cnode_index 3) \<lbrace>?B141 thread x51 x52 x53 state x xa x2\<rbrace>
 9. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R116 thread x51 x52 x53 state x xa xb s)\<rbrace>
 10. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
A total of 21 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>thread x51 x52 x53 state xa x2 xc xd xe. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B144 thread x51 False x53 state () (Some x2) x2 () xc xd xe\<rbrace> handle_fault_reply x2 x51 (mi_label xc) xe \<lbrace>\<lambda>a b. P (cur_thread b) (idle_thread b)\<rbrace>
 2. \<And>thread x51 x52 x53 state x xa x2 xb xc xd. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace> get_mrs thread xd xc \<lbrace>?B144 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace>
 3. \<And>thread x51 x52 x53 state x xa x2 xb xc. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb xc\<rbrace> lookup_ipc_buffer False thread \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc\<rbrace>
 4. \<And>thread x51 x52 x53 state x xa x2 xb. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread x51 x52 x53 state x xa x2 xb\<rbrace> get_message_info thread \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb\<rbrace>
 5. \<And>thread x51 x52 x53 state x xa x2. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R116 thread x51 x52 x53 state x xa x2\<rbrace> cap_delete_one (thread, tcb_cnode_index 3) \<lbrace>?B141 thread x51 x52 x53 state x xa x2\<rbrace>
 6. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R116 thread x51 x52 x53 state x xa xb s)\<rbrace>
 7. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
 8. \<And>thread x51 x52 x53. \<not> x52 \<Longrightarrow> \<lbrace>?R91 thread (cap.ReplyCap x51 False x53) x51 (ds_id False) x53\<rbrace> get_thread_state x51 \<lbrace>?B102 thread x51 x52 x53\<rbrace>
 9. \<And>thread caller_cap x61 x62 x63. caller_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 thread caller_cap x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 10. \<And>thread caller_cap x7. caller_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 thread caller_cap x7\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>thread x51 x52 x53 state x xa x2 xb xc xd. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc xd\<rbrace> get_mrs thread xd xc \<lbrace>\<lambda>a b. P (cur_thread b) (idle_thread b)\<rbrace>
 2. \<And>thread x51 x52 x53 state x xa x2 xb xc. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb xc\<rbrace> lookup_ipc_buffer False thread \<lbrace>?B143 thread x51 x52 x53 state x xa x2 xb xc\<rbrace>
 3. \<And>thread x51 x52 x53 state x xa x2 xb. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?B141 thread x51 x52 x53 state x xa x2 xb\<rbrace> get_message_info thread \<lbrace>?B142 thread x51 x52 x53 state x xa x2 xb\<rbrace>
 4. \<And>thread x51 x52 x53 state x xa x2. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R116 thread x51 x52 x53 state x xa x2\<rbrace> cap_delete_one (thread, tcb_cnode_index 3) \<lbrace>?B141 thread x51 x52 x53 state x xa x2\<rbrace>
 5. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R116 thread x51 x52 x53 state x xa xb s)\<rbrace>
 6. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
 7. \<And>thread x51 x52 x53. \<not> x52 \<Longrightarrow> \<lbrace>?R91 thread (cap.ReplyCap x51 False x53) x51 (ds_id False) x53\<rbrace> get_thread_state x51 \<lbrace>?B102 thread x51 x52 x53\<rbrace>
 8. \<And>thread caller_cap x61 x62 x63. caller_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 thread caller_cap x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 9. \<And>thread caller_cap x7. caller_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 thread caller_cap x7\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 10. \<And>thread caller_cap. caller_cap = cap.DomainCap \<Longrightarrow> \<lbrace>?R59 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
A total of 17 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>thread x51 x52 x53 state x xa x2. \<lbrakk>\<not> x52; xa = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?R116 thread x51 x52 x53 state x xa x2\<rbrace> cap_delete_one (thread, tcb_cnode_index 3) \<lbrace>\<lambda>xb a. P (cur_thread a) (idle_thread a)\<rbrace>
 2. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R116 thread x51 x52 x53 state x xa xb s)\<rbrace>
 3. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
 4. \<And>thread x51 x52 x53. \<not> x52 \<Longrightarrow> \<lbrace>?R91 thread (cap.ReplyCap x51 False x53) x51 (ds_id False) x53\<rbrace> get_thread_state x51 \<lbrace>?B102 thread x51 x52 x53\<rbrace>
 5. \<And>thread caller_cap x61 x62 x63. caller_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 thread caller_cap x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 6. \<And>thread caller_cap x7. caller_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 thread caller_cap x7\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 7. \<And>thread caller_cap. caller_cap = cap.DomainCap \<Longrightarrow> \<lbrace>?R59 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 8. \<And>thread caller_cap. caller_cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 9. \<And>thread caller_cap x10. caller_cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 thread caller_cap x10\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 10. \<And>thread caller_cap x111 x112 x113. caller_cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>?R62 thread caller_cap x111 x112 x113\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>thread x51 x52 x53 state x. \<not> x52 \<Longrightarrow> \<lbrace>?B104 thread x51 x52 x53 state x\<rbrace> thread_get tcb_fault x51 \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> P (cur_thread s) (idle_thread s)) \<and> (\<forall>x. xa = Some x \<longrightarrow> P (cur_thread s) (idle_thread s))\<rbrace>
 2. \<And>thread x51 x52 x53 state. \<not> x52 \<Longrightarrow> \<lbrace>?B102 thread x51 x52 x53 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B104 thread x51 x52 x53 state\<rbrace>
 3. \<And>thread x51 x52 x53. \<not> x52 \<Longrightarrow> \<lbrace>?R91 thread (cap.ReplyCap x51 False x53) x51 (ds_id False) x53\<rbrace> get_thread_state x51 \<lbrace>?B102 thread x51 x52 x53\<rbrace>
 4. \<And>thread caller_cap x61 x62 x63. caller_cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>?R57 thread caller_cap x61 x62 x63\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 5. \<And>thread caller_cap x7. caller_cap = ThreadCap x7 \<Longrightarrow> \<lbrace>?R58 thread caller_cap x7\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 6. \<And>thread caller_cap. caller_cap = cap.DomainCap \<Longrightarrow> \<lbrace>?R59 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 7. \<And>thread caller_cap. caller_cap = IRQControlCap \<Longrightarrow> \<lbrace>?R60 thread caller_cap\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 8. \<And>thread caller_cap x10. caller_cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?R61 thread caller_cap x10\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 9. \<And>thread caller_cap x111 x112 x113. caller_cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>?R62 thread caller_cap x111 x112 x113\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
 10. \<And>thread caller_cap x12. caller_cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>?R63 thread caller_cap x12\<rbrace> fail \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cur_thread s) (idle_thread s) \<Longrightarrow> P (cur_thread s) (idle_thread s) proof (prove)
goal:
No subgoals!