theory Syscall_DR

lemma perform_invocation_corres:
  "\<lbrakk>cdl_invocation_relation i i'\<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc)
         \<top> (invs and ct_active and valid_pdpt_objs and valid_etcbs
            and invocation_duplicates_valid i' and valid_invocation i')
      (Syscall_D.perform_invocation call block i)
      (Syscall_A.perform_invocation block call i')" apply (clarsimp simp: cdl_invocation_relation_def) apply (case_tac i') apply (simp_all add: translate_invocation_def split: Invocations_A.invocation.splits) subgoal  (* untyped *)
     apply (simp add: liftME_def[symmetric]) apply (rule corres_guard_imp, rule invoke_untyped_corres) apply clarsimp apply clarsimp done subgoal  (* send_ipc *)
     apply (clarsimp simp:invoke_endpoint_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cur_thread_corres]) apply (rule corres_dummy_return_l) apply (rule corres_split) apply (rule send_sync_ipc_corres; simp) apply (rule corres_trivial[OF corres_free_return]) apply (wp|clarsimp)+ apply (clarsimp simp: ct_in_state_def obj_at_def pred_tcb_at_def not_idle_thread_def
                          valid_state_def invs_def valid_idle_def) done subgoal  (* send_signal *)
     apply (clarsimp simp:invoke_notification_def liftE_bindE) apply (clarsimp simp:liftE_def bind_assoc returnOk_def) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule send_signal_corres; simp) apply (rule corres_trivial) apply (simp add:dc_def corres_free_return) apply (wp | clarsimp)+ done apply clarsimp subgoal for word a b c  (* invoke_reply *)
     apply (clarsimp simp:invoke_reply_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cur_thread_corres]) apply clarsimp apply (rule corres_dummy_return_l) apply (rule corres_split) apply (rule do_reply_transfer_corres, simp) apply (rule corres_trivial[OF  corres_free_return]) apply (wp|clarsimp)+ apply (simp add: ct_active_not_idle_etc) apply (rule conjI, fastforce)+ apply (subgoal_tac "valid_idle s \<and> valid_reply_caps s \<and> has_reply_cap word s") apply clarsimp apply (drule (1) valid_reply_capsD) apply (clarsimp simp: valid_idle_def not_idle_thread_def pred_tcb_at_def obj_at_def) apply (fastforce simp: has_reply_cap_def is_reply_cap_to_def) done subgoal  (* invoke_tcb *)
     apply (rule corres_guard_imp) apply (rule invoke_tcb_corres,simp+) done subgoal  (* invoke_domain *)
     apply (rule corres_guard_imp) apply (rule invoke_domain_corres,simp+) done subgoal  (* invoke_cnode *)
     apply (rule corres_guard_imp) apply (clarsimp simp:bindE_def returnOk_def lift_def bind_assoc) apply (rule corres_dummy_return_l) apply (rule corres_split[OF invoke_cnode_corres]) apply (clarsimp simp:lift_def,case_tac rv',simp add: throwError_def) apply (simp) apply (rule hoare_triv[of \<top>], rule hoare_post_taut)+ apply clarsimp+ done subgoal for irq_control_invocation  (* invoke_irq_control *)
     apply (simp add:liftE_def bindE_def) apply (case_tac irq_control_invocation) 
     (* generic *)
      apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (rule dcorres_invoke_irq_control) apply (rule_tac F = "\<exists>x. rv' = Inr x" in corres_gen_asm2) apply (rule corres_trivial) apply (clarsimp simp:lift_def returnOk_def) apply (rule hoare_triv[of \<top>], rule hoare_post_taut)+ apply ((wp|simp add: liftE_def)+) 
    (* arch *)
     apply (rename_tac arch_label) apply (case_tac arch_label) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (rule dcorres_arch_invoke_irq_control[simplified]) apply (rule_tac F = "\<exists>x. rv' = Inr x" in corres_gen_asm2) apply (rule corres_trivial) apply (clarsimp simp:lift_def returnOk_def) apply (rule hoare_triv[of \<top>], rule hoare_post_taut) apply ((wp|simp add: liftE_def)+) done subgoal  (* invoke_irq_handler *)
     apply (clarsimp simp:liftE_bindE,simp add:liftE_def returnOk_def) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule dcorres_invoke_irq_handler) apply (rule corres_trivial) apply clarsimp apply (wp|clarsimp)+ done subgoal  (* invoke_arch *)
     apply (rule corres_guard_imp[OF invoke_arch_corres],fastforce+) done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_invocation_relation i i' \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i') proof (prove)
goal (1 subgoal):
 1. case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i' \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i') proof (prove)
goal (10 subgoals):
 1. \<And>x1. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = invocation.InvokeUntyped x1\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 2. \<And>x21 x22 x23 x24. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = invocation.InvokeEndpoint x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 3. \<And>x31 x32. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = invocation.InvokeNotification x31 x32\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 4. \<And>x41 x42 x43. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = invocation.InvokeReply x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 5. \<And>x5. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = InvokeTCB x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 6. \<And>x61 x62. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = invocation.InvokeDomain x61 x62\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 7. \<And>x7. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 8. \<And>x8. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 9. \<And>x9. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i')
 10. \<And>x10. \<lbrakk>case i' of InvokeArchObject invo \<Rightarrow> arch_invocation_relation i invo | _ \<Rightarrow> i = translate_invocation i'; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid i' and valid_invocation i') (Syscall_D.perform_invocation call block i) (Syscall_A.perform_invocation block call i') proof (prove)
goal (10 subgoals):
 1. \<And>x1. \<lbrakk>i = cdl_invocation.InvokeUntyped (translate_untyped_invocation x1); i' = invocation.InvokeUntyped x1\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeUntyped x1) and valid_untyped_inv x1) (Untyped_D.invoke_untyped (translate_untyped_invocation x1)) (doE y <- Retype_A.invoke_untyped x1;
returnOk []
odE)
 2. \<And>x21 x22 x23 x24. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22 x23 x24 x21); i' = invocation.InvokeEndpoint x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21 x22 x23 x24) and (ep_at x21 and ex_nonz_cap_to x21)) (invoke_endpoint call block (SyncMessage x22 x23 x24 x21)) (do thread <- gets cur_thread;
y <- Ipc_A.send_ipc block call x22 x23 x24 thread x21;
return []
od)
 3. \<And>x31 x32. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32 x31); i' = invocation.InvokeNotification x31 x32\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31 x32) and (ntfn_at x31 and ex_nonz_cap_to x31)) (liftE (invoke_notification (Signal x32 x31))) (doE y <- liftE (Ipc_A.send_signal x31 x32);
returnOk []
odE)
 4. \<And>x41 x42 x43. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage x41 (transform_cslot_ptr x42) x43); i' = invocation.InvokeReply x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply x41 x42 x43) and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap x41 False R) x42)) (invoke_reply (ReplyMessage x41 (transform_cslot_ptr x42) x43)) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender x41 x42 x43;
return []
od)
 5. \<And>x5. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5); i' = InvokeTCB x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5) and tcb_inv_wf x5) (Tcb_D.invoke_tcb (translate_tcb_invocation x5)) (Tcb_A.invoke_tcb x5)
 6. \<And>x61 x62. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61 x62); i' = invocation.InvokeDomain x61 x62\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61 x62) and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61 x62)) (Tcb_A.invoke_domain x61 x62)
 7. \<And>x7. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7); i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7) and valid_cnode_inv x7) (CNode_D.invoke_cnode (translate_cnode_invocation x7)) (doE y <- CSpace_A.invoke_cnode x7;
returnOk []
odE)
 8. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 9. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 10. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeUntyped (translate_untyped_invocation x1_); i' = invocation.InvokeUntyped x1_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeUntyped x1_) and valid_untyped_inv x1_) (Untyped_D.invoke_untyped (translate_untyped_invocation x1_)) (doE y <- Retype_A.invoke_untyped x1_;
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeUntyped (translate_untyped_invocation x1_); i' = invocation.InvokeUntyped x1_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeUntyped x1_) and valid_untyped_inv x1_) (Untyped_D.invoke_untyped (translate_untyped_invocation x1_)) (doE y <- Retype_A.invoke_untyped x1_;
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeUntyped (translate_untyped_invocation x1_); i' = invocation.InvokeUntyped x1_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeUntyped x1_) and valid_untyped_inv x1_) (Untyped_D.invoke_untyped (translate_untyped_invocation x1_)) (Retype_A.invoke_untyped x1_) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeUntyped (translate_untyped_invocation x1_); i' = invocation.InvokeUntyped x1_; True\<rbrakk> \<Longrightarrow> True
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeUntyped (translate_untyped_invocation x1_); i' = invocation.InvokeUntyped x1_; (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeUntyped x1_) and valid_untyped_inv x1_) s\<rbrakk> \<Longrightarrow> (invs and ct_active and valid_untyped_inv x1_ and valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeUntyped (translate_untyped_invocation x1_); i' = invocation.InvokeUntyped x1_; (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeUntyped x1_) and valid_untyped_inv x1_) s\<rbrakk> \<Longrightarrow> (invs and ct_active and valid_untyped_inv x1_ and valid_etcbs) s proof (prove)
goal:
No subgoals! proof (prove)
goal (9 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22 x23 x24 x21); i' = invocation.InvokeEndpoint x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21 x22 x23 x24) and (ep_at x21 and ex_nonz_cap_to x21)) (invoke_endpoint call block (SyncMessage x22 x23 x24 x21)) (do thread <- gets cur_thread;
y <- Ipc_A.send_ipc block call x22 x23 x24 thread x21;
return []
od)
 2. \<And>x31 x32. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32 x31); i' = invocation.InvokeNotification x31 x32\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31 x32) and (ntfn_at x31 and ex_nonz_cap_to x31)) (liftE (invoke_notification (Signal x32 x31))) (doE y <- liftE (Ipc_A.send_signal x31 x32);
returnOk []
odE)
 3. \<And>x41 x42 x43. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage x41 (transform_cslot_ptr x42) x43); i' = invocation.InvokeReply x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply x41 x42 x43) and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap x41 False R) x42)) (invoke_reply (ReplyMessage x41 (transform_cslot_ptr x42) x43)) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender x41 x42 x43;
return []
od)
 4. \<And>x5. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5); i' = InvokeTCB x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5) and tcb_inv_wf x5) (Tcb_D.invoke_tcb (translate_tcb_invocation x5)) (Tcb_A.invoke_tcb x5)
 5. \<And>x61 x62. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61 x62); i' = invocation.InvokeDomain x61 x62\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61 x62) and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61 x62)) (Tcb_A.invoke_domain x61 x62)
 6. \<And>x7. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7); i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7) and valid_cnode_inv x7) (CNode_D.invoke_cnode (translate_cnode_invocation x7)) (doE y <- CSpace_A.invoke_cnode x7;
returnOk []
odE)
 7. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 8. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 9. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) (invoke_endpoint call block (SyncMessage x22_ x23_ x24_ x21_)) (do thread <- gets cur_thread;
y <- Ipc_A.send_ipc block call x22_ x23_ x24_ thread x21_;
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) (invoke_endpoint call block (SyncMessage x22_ x23_ x24_ x21_)) (do thread <- gets cur_thread;
y <- Ipc_A.send_ipc block call x22_ x23_ x24_ thread x21_;
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) (do thread <- gets_the cdl_current_thread;
Endpoint_D.send_ipc block call x22_ x23_ x24_ thread x21_
od) (do thread <- gets cur_thread;
y <- Ipc_A.send_ipc block call x22_ x23_ x24_ thread x21_;
return []
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> dcorres dc ?Q4 ?Q'4 (do thread <- gets_the cdl_current_thread;
Endpoint_D.send_ipc block call x22_ x23_ x24_ thread x21_
od) (do thread <- gets cur_thread;
y <- Ipc_A.send_ipc block call x22_ x23_ x24_ thread x21_;
return []
od)
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; True\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) s\<rbrakk> \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> dcorres dc (?R8 thread) (?R'8 threada) (Endpoint_D.send_ipc block call x22_ x23_ x24_ thread x21_) (do y <- Ipc_A.send_ipc block call x22_ x23_ x24_ threada x21_;
return []
od)
 2. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the cdl_current_thread \<lbrace>?R8\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> gets cur_thread \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> dcorres dc (?R8 thread) (?R'8 threada) (Endpoint_D.send_ipc block call x22_ x23_ x24_ thread x21_ >>= return) (do y <- Ipc_A.send_ipc block call x22_ x23_ x24_ threada x21_;
return []
od)
 2. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the cdl_current_thread \<lbrace>?R8\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> gets cur_thread \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> dcorres (?r'14 thread threada) (?P15 thread) (?P'17 threada) (Endpoint_D.send_ipc block call x22_ x23_ x24_ thread x21_) (Ipc_A.send_ipc block call x22_ x23_ x24_ threada x21_)
 2. \<And>thread threada x y. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada; ?r'14 thread threada x y\<rbrakk> \<Longrightarrow> dcorres dc (?R14 thread threada x) (?R'14 thread threada y) (return x) (return [])
 3. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 thread\<rbrace> Endpoint_D.send_ipc block call x22_ x23_ x24_ thread x21_ \<lbrace>?R14 thread threada\<rbrace>
 4. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 threada\<rbrace> Ipc_A.send_ipc block call x22_ x23_ x24_ threada x21_ \<lbrace>?R'14 thread threada\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. ?P15 thread and ?Q16 thread\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. ?P'17 threada and ?Q'18 threada\<rbrace>
 7. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 8. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>thread threada x y. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R14 thread threada x) (?R'14 thread threada y) (return x) (return [])
 2. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 thread\<rbrace> Endpoint_D.send_ipc block call x22_ x23_ x24_ thread x21_ \<lbrace>?R14 thread threada\<rbrace>
 3. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 threada\<rbrace> Ipc_A.send_ipc block call x22_ x23_ x24_ threada x21_ \<lbrace>?R'14 thread threada\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q16 thread\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. not_idle_thread threada and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active threada and valid_state and valid_etcbs and ?Q'18 threada\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 7. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 thread\<rbrace> Endpoint_D.send_ipc block call x22_ x23_ x24_ thread x21_ \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>thread threada. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; thread = threada\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 threada\<rbrace> Ipc_A.send_ipc block call x22_ x23_ x24_ threada x21_ \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and ?Q16 thread\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> gets cur_thread \<lbrace>\<lambda>threada. not_idle_thread threada and (\<lambda>s. not_idle_thread (cur_thread s) s) and st_tcb_at active threada and valid_state and valid_etcbs and ?Q'18 threada\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) and (ep_at x21_ and ex_nonz_cap_to x21_)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'8) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeEndpoint (SyncMessage x22_ x23_ x24_ x21_); i' = invocation.InvokeEndpoint x21_ x22_ x23_ x24_; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeEndpoint x21_ x22_ x23_ x24_) s; ep_at x21_ s; ex_nonz_cap_to x21_ s\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s \<and> st_tcb_at active (cur_thread s) s \<and> valid_state s proof (prove)
goal:
No subgoals! proof (prove)
goal (8 subgoals):
 1. \<And>x31 x32. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32 x31); i' = invocation.InvokeNotification x31 x32\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31 x32) and (ntfn_at x31 and ex_nonz_cap_to x31)) (liftE (invoke_notification (Signal x32 x31))) (doE y <- liftE (Ipc_A.send_signal x31 x32);
returnOk []
odE)
 2. \<And>x41 x42 x43. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage x41 (transform_cslot_ptr x42) x43); i' = invocation.InvokeReply x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply x41 x42 x43) and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap x41 False R) x42)) (invoke_reply (ReplyMessage x41 (transform_cslot_ptr x42) x43)) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender x41 x42 x43;
return []
od)
 3. \<And>x5. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5); i' = InvokeTCB x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5) and tcb_inv_wf x5) (Tcb_D.invoke_tcb (translate_tcb_invocation x5)) (Tcb_A.invoke_tcb x5)
 4. \<And>x61 x62. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61 x62); i' = invocation.InvokeDomain x61 x62\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61 x62) and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61 x62)) (Tcb_A.invoke_domain x61 x62)
 5. \<And>x7. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7); i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7) and valid_cnode_inv x7) (CNode_D.invoke_cnode (translate_cnode_invocation x7)) (doE y <- CSpace_A.invoke_cnode x7;
returnOk []
odE)
 6. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 7. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 8. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) (liftE (invoke_notification (Signal x32_ x31_))) (doE y <- liftE (Ipc_A.send_signal x31_ x32_);
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) (liftE (invoke_notification (Signal x32_ x31_))) (doE y <- liftE (Ipc_A.send_signal x31_ x32_);
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) (liftE (Endpoint_D.send_signal x31_)) (do y <- Ipc_A.send_signal x31_ x32_;
returnOk []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) (do r <- Endpoint_D.send_signal x31_;
return (Inr ())
od) (do y <- Ipc_A.send_signal x31_ x32_;
return (Inr [])
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ?Q ?Q' (do r <- Endpoint_D.send_signal x31_;
return (Inr ())
od) (do y <- Ipc_A.send_signal x31_ x32_;
return (Inr [])
od)
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> dcorres ?r'4 ?P4 ?P'4 (Endpoint_D.send_signal x31_) (Ipc_A.send_signal x31_ x32_)
 2. \<And>r y. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; ?r'4 r y\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R4 r) (?R'4 y) (return (Inr ())) (return (Inr []))
 3. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> Endpoint_D.send_signal x31_ \<lbrace>?R4\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> Ipc_A.send_signal x31_ x32_ \<lbrace>?R'4\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; True\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) s\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r y. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; dc r y\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R4 r) (?R'4 y) (return (Inr ())) (return (Inr []))
 2. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> Endpoint_D.send_signal x31_ \<lbrace>?R4\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> Ipc_A.send_signal x31_ x32_ \<lbrace>?R'4\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r y. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; dc r y\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (return (Inr ())) (return (Inr []))
 2. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> Endpoint_D.send_signal x31_ \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> Ipc_A.send_signal x31_ x32_ \<lbrace>\<lambda>y _. True\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> Endpoint_D.send_signal x31_ \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> Ipc_A.send_signal x31_ x32_ \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeNotification (Signal x32_ x31_); i' = invocation.InvokeNotification x31_ x32_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeNotification x31_ x32_) and (ntfn_at x31_ and ex_nonz_cap_to x31_)) s\<rbrakk> \<Longrightarrow> (invs and valid_etcbs and ?Q'4) s proof (prove)
goal:
No subgoals! proof (prove)
goal (7 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage x41 (transform_cslot_ptr x42) x43); i' = invocation.InvokeReply x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply x41 x42 x43) and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap x41 False R) x42)) (invoke_reply (ReplyMessage x41 (transform_cslot_ptr x42) x43)) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender x41 x42 x43;
return []
od)
 2. \<And>x5. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5); i' = InvokeTCB x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5) and tcb_inv_wf x5) (Tcb_D.invoke_tcb (translate_tcb_invocation x5)) (Tcb_A.invoke_tcb x5)
 3. \<And>x61 x62. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61 x62); i' = invocation.InvokeDomain x61 x62\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61 x62) and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61 x62)) (Tcb_A.invoke_domain x61 x62)
 4. \<And>x7. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7); i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7) and valid_cnode_inv x7) (CNode_D.invoke_cnode (translate_cnode_invocation x7)) (doE y <- CSpace_A.invoke_cnode x7;
returnOk []
odE)
 5. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 6. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 7. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (7 subgoals):
 1. \<And>x41 a b x43. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage x41 (transform_cslot_ptr (a, b)) x43); i' = invocation.InvokeReply x41 (a, b) x43\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply x41 (a, b) x43) and (tcb_at x41 and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap x41 False R) (a, b))) (invoke_reply (ReplyMessage x41 (transform_cslot_ptr (a, b)) x43)) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender x41 (a, b) x43;
return []
od)
 2. \<And>x5. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5); i' = InvokeTCB x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5) and tcb_inv_wf x5) (Tcb_D.invoke_tcb (translate_tcb_invocation x5)) (Tcb_A.invoke_tcb x5)
 3. \<And>x61 x62. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61 x62); i' = invocation.InvokeDomain x61 x62\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61 x62) and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61 x62)) (Tcb_A.invoke_domain x61 x62)
 4. \<And>x7. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7); i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7) and valid_cnode_inv x7) (CNode_D.invoke_cnode (translate_cnode_invocation x7)) (doE y <- CSpace_A.invoke_cnode x7;
returnOk []
odE)
 5. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 6. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 7. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) (invoke_reply (ReplyMessage word (transform_cslot_ptr (a, b)) c)) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender word (a, b) c;
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) (invoke_reply (ReplyMessage word (transform_cslot_ptr (a, b)) c)) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender word (a, b) c;
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) (do send <- gets_the cdl_current_thread;
Endpoint_D.do_reply_transfer send word (transform_cslot_ptr (a, b)) c
od) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender word (a, b) c;
return []
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> dcorres dc ?Q ?Q' (do send <- gets_the cdl_current_thread;
Endpoint_D.do_reply_transfer send word (transform_cslot_ptr (a, b)) c
od) (do sender <- gets cur_thread;
y <- Ipc_A.do_reply_transfer sender word (a, b) c;
return []
od)
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>send sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; send = sender\<rbrakk> \<Longrightarrow> dcorres dc (?R4 send) (?R'4 sender) (Endpoint_D.do_reply_transfer send word (transform_cslot_ptr (a, b)) c) (do y <- Ipc_A.do_reply_transfer sender word (a, b) c;
return []
od)
 2. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>?R4\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>?R'4\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> dcorres dc (?R4 sender) (?R'4 sender) (Endpoint_D.do_reply_transfer sender word (transform_cslot_ptr (a, b)) c) (do y <- Ipc_A.do_reply_transfer sender word (a, b) c;
return []
od)
 2. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>?R4\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>?R'4\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> dcorres dc (?R4 sender) (?R'4 sender) (Endpoint_D.do_reply_transfer sender word (transform_cslot_ptr (a, b)) c >>= return) (do y <- Ipc_A.do_reply_transfer sender word (a, b) c;
return []
od)
 2. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>?R4\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>?R'4\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> dcorres (?r'13 sender) (?P13 sender) (?P'13 sender) (Endpoint_D.do_reply_transfer sender word (transform_cslot_ptr (a, b)) c) (Ipc_A.do_reply_transfer sender word (a, b) c)
 2. \<And>sender x y. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; ?r'13 sender x y\<rbrakk> \<Longrightarrow> dcorres dc (?R13 sender x) (?R'13 sender y) (return x) (return [])
 3. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 sender\<rbrace> Endpoint_D.do_reply_transfer sender word (transform_cslot_ptr (a, b)) c \<lbrace>?R13 sender\<rbrace>
 4. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 sender\<rbrace> Ipc_A.do_reply_transfer sender word (a, b) c \<lbrace>?R'13 sender\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>sender. ?P13 sender and ?Q13 sender\<rbrace>
 6. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>sender. ?P'13 sender and ?Q'13 sender\<rbrace>
 7. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>sender x y. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R13 sender x) (?R'13 sender y) (return x) (return [])
 2. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 sender\<rbrace> Endpoint_D.do_reply_transfer sender word (transform_cslot_ptr (a, b)) c \<lbrace>?R13 sender\<rbrace>
 3. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 sender\<rbrace> Ipc_A.do_reply_transfer sender word (a, b) c \<lbrace>?R'13 sender\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>sender. (\<lambda>_. True) and ?Q13 sender\<rbrace>
 5. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>sender. invs and tcb_at word and tcb_at sender and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread word and not_idle_thread sender and valid_etcbs and ?Q'13 sender\<rbrace>
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 sender\<rbrace> Endpoint_D.do_reply_transfer sender word (transform_cslot_ptr (a, b)) c \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>sender. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'13 sender\<rbrace> Ipc_A.do_reply_transfer sender word (a, b) c \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> gets_the cdl_current_thread \<lbrace>\<lambda>sender. (\<lambda>_. True) and ?Q13 sender\<rbrace>
 4. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> gets cur_thread \<lbrace>\<lambda>sender. invs and tcb_at word and tcb_at sender and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) and (\<lambda>s. not_idle_thread (cur_thread s) s) and not_idle_thread word and not_idle_thread sender and valid_etcbs and ?Q'13 sender\<rbrace>
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) and (tcb_at word and cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b))) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. not_idle_thread (cur_thread s) s) and ?Q'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s\<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s \<and> tcb_at (cur_thread s) s \<and> not_idle_thread (cur_thread s) s \<and> not_idle_thread word s \<and> not_idle_thread (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s\<rbrakk> \<Longrightarrow> tcb_at (cur_thread s) s \<and> not_idle_thread word s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s\<rbrakk> \<Longrightarrow> not_idle_thread word s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s; valid_idle s \<and> valid_reply_caps s \<and> has_reply_cap word s\<rbrakk> \<Longrightarrow> not_idle_thread word s
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s\<rbrakk> \<Longrightarrow> valid_idle s \<and> valid_reply_caps s \<and> has_reply_cap word s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s; valid_idle s; valid_reply_caps s; has_reply_cap word s\<rbrakk> \<Longrightarrow> not_idle_thread word s
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s\<rbrakk> \<Longrightarrow> valid_idle s \<and> valid_reply_caps s \<and> has_reply_cap word s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s; valid_idle s; valid_reply_caps s; st_tcb_at awaiting_reply word s\<rbrakk> \<Longrightarrow> not_idle_thread word s
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s\<rbrakk> \<Longrightarrow> valid_idle s \<and> valid_reply_caps s \<and> has_reply_cap word s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeReply (ReplyMessage word (transform_cslot_ptr (a, b)) c); i' = invocation.InvokeReply word (a, b) c; invs s; ct_active s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; invocation_duplicates_valid (invocation.InvokeReply word (a, b) c) s; tcb_at word s; cte_wp_at (\<lambda>cap. \<exists>R. cap = cap.ReplyCap word False R) (a, b) s\<rbrakk> \<Longrightarrow> valid_idle s \<and> valid_reply_caps s \<and> has_reply_cap word s proof (prove)
goal:
No subgoals! proof (prove)
goal (6 subgoals):
 1. \<And>x5. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5); i' = InvokeTCB x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5) and tcb_inv_wf x5) (Tcb_D.invoke_tcb (translate_tcb_invocation x5)) (Tcb_A.invoke_tcb x5)
 2. \<And>x61 x62. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61 x62); i' = invocation.InvokeDomain x61 x62\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61 x62) and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61 x62)) (Tcb_A.invoke_domain x61 x62)
 3. \<And>x7. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7); i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7) and valid_cnode_inv x7) (CNode_D.invoke_cnode (translate_cnode_invocation x7)) (doE y <- CSpace_A.invoke_cnode x7;
returnOk []
odE)
 4. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 5. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 6. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5_); i' = InvokeTCB x5_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5_) and tcb_inv_wf x5_) (Tcb_D.invoke_tcb (translate_tcb_invocation x5_)) (Tcb_A.invoke_tcb x5_) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5_); i' = InvokeTCB x5_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5_) and tcb_inv_wf x5_) (Tcb_D.invoke_tcb (translate_tcb_invocation x5_)) (Tcb_A.invoke_tcb x5_) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5_); i' = InvokeTCB x5_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ?Q ?Q' (Tcb_D.invoke_tcb (translate_tcb_invocation x5_)) (Tcb_A.invoke_tcb x5_)
 2. \<And>s. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5_); i' = InvokeTCB x5_; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>i = InvokeTcb (translate_tcb_invocation x5_); i' = InvokeTCB x5_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeTCB x5_) and tcb_inv_wf x5_) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal:
No subgoals! proof (prove)
goal (5 subgoals):
 1. \<And>x61 x62. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61 x62); i' = invocation.InvokeDomain x61 x62\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61 x62) and (tcb_at x61 and (\<lambda>s. x61 \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61 x62)) (Tcb_A.invoke_domain x61 x62)
 2. \<And>x7. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7); i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7) and valid_cnode_inv x7) (CNode_D.invoke_cnode (translate_cnode_invocation x7)) (doE y <- CSpace_A.invoke_cnode x7;
returnOk []
odE)
 3. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 4. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 5. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61_ x62_); i' = invocation.InvokeDomain x61_ x62_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61_ x62_) and (tcb_at x61_ and (\<lambda>s. x61_ \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61_ x62_)) (Tcb_A.invoke_domain x61_ x62_) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61_ x62_); i' = invocation.InvokeDomain x61_ x62_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61_ x62_) and (tcb_at x61_ and (\<lambda>s. x61_ \<noteq> idle_thread s))) (Tcb_D.invoke_domain (SetDomain x61_ x62_)) (Tcb_A.invoke_domain x61_ x62_) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61_ x62_); i' = invocation.InvokeDomain x61_ x62_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ?Q ?Q' (Tcb_D.invoke_domain (SetDomain x61_ x62_)) (Tcb_A.invoke_domain x61_ x62_)
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61_ x62_); i' = invocation.InvokeDomain x61_ x62_; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeDomain (SetDomain x61_ x62_); i' = invocation.InvokeDomain x61_ x62_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeDomain x61_ x62_) and (tcb_at x61_ and (\<lambda>s. x61_ \<noteq> idle_thread s))) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal:
No subgoals! proof (prove)
goal (4 subgoals):
 1. \<And>x7. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7); i' = invocation.InvokeCNode x7\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7) and valid_cnode_inv x7) (CNode_D.invoke_cnode (translate_cnode_invocation x7)) (doE y <- CSpace_A.invoke_cnode x7;
returnOk []
odE)
 2. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 3. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 4. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) (CNode_D.invoke_cnode (translate_cnode_invocation x7_)) (doE y <- CSpace_A.invoke_cnode x7_;
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) (CNode_D.invoke_cnode (translate_cnode_invocation x7_)) (doE y <- CSpace_A.invoke_cnode x7_;
returnOk []
odE) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ?Q ?Q' (CNode_D.invoke_cnode (translate_cnode_invocation x7_)) (doE y <- CSpace_A.invoke_cnode x7_;
returnOk []
odE)
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ?Q ?Q' (CNode_D.invoke_cnode (translate_cnode_invocation x7_)) (CSpace_A.invoke_cnode x7_ >>= lift (\<lambda>y. return (Inr [])))
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ?Q ?Q' (CNode_D.invoke_cnode (translate_cnode_invocation x7_) >>= return) (CSpace_A.invoke_cnode x7_ >>= lift (\<lambda>y. return (Inr [])))
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>x rv'. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (dc \<oplus> dc) x rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R8 x) (?R'8 rv') (return x) (lift (\<lambda>y. return (Inr [])) rv')
 2. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> CNode_D.invoke_cnode (translate_cnode_invocation x7_) \<lbrace>?R8\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> CSpace_A.invoke_cnode x7_ \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) s\<rbrakk> \<Longrightarrow> (valid_cnode_inv x7_ and invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>x rv' b. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (dc \<oplus> dc) x rv'; rv' = Inr b\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R8 x) (?R'8 rv') (return x) (case rv' of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> return (Inr []))
 2. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> CNode_D.invoke_cnode (translate_cnode_invocation x7_) \<lbrace>?R8\<rbrace>
 3. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> CSpace_A.invoke_cnode x7_ \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) s\<rbrakk> \<Longrightarrow> (valid_cnode_inv x7_ and invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and ?Q'8) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> CNode_D.invoke_cnode (translate_cnode_invocation x7_) \<lbrace>?R8\<rbrace>
 2. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> CSpace_A.invoke_cnode x7_ \<lbrace>?R'8\<rbrace>
 3. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 4. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) s\<rbrakk> \<Longrightarrow> (valid_cnode_inv x7_ and invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 2. \<And>s. \<lbrakk>i = cdl_invocation.InvokeCNode (translate_cnode_invocation x7_); i' = invocation.InvokeCNode x7_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (invocation.InvokeCNode x7_) and valid_cnode_inv x7_) s\<rbrakk> \<Longrightarrow> (valid_cnode_inv x7_ and invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals! proof (prove)
goal (3 subgoals):
 1. \<And>x8. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation x8); i' = InvokeIRQControl x8\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl x8) and irq_control_inv_valid x8) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation x8))) (doE y <- Interrupt_A.invoke_irq_control x8;
returnOk []
odE)
 2. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 3. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation))) (doE y <- Interrupt_A.invoke_irq_control irq_control_invocation;
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (liftE (Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation))) (doE y <- Interrupt_A.invoke_irq_control irq_control_invocation;
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk []))
 2. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk []))
 2. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q1 x11 x12 x13) (?Q'1 x11 x12 x13) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk []))
 2. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; True\<rbrakk> \<Longrightarrow> ?Q1 x11 x12 x13 s
 3. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) s\<rbrakk> \<Longrightarrow> ?Q'1 x11 x12 x13 s
 4. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> dcorres dc (?P5 x11 x12 x13) (?P'5 x11 x12 x13) (Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation)) (Interrupt_A.invoke_irq_control irq_control_invocation)
 2. \<And>x11 x12 x13 r rv'. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; dc r rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R5 x11 x12 x13 r) (?R'5 x11 x12 x13 rv') (return (Inr ())) (lift (\<lambda>y. returnOk []) rv')
 3. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 x11 x12 x13\<rbrace> Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation) \<lbrace>?R5 x11 x12 x13\<rbrace>
 4. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5 x11 x12 x13\<rbrace> Interrupt_A.invoke_irq_control irq_control_invocation \<lbrace>?R'5 x11 x12 x13\<rbrace>
 5. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; True\<rbrakk> \<Longrightarrow> (?P5 x11 x12 x13 and ?Q5 x11 x12 x13) s
 6. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) s\<rbrakk> \<Longrightarrow> (?P'5 x11 x12 x13 and ?Q'5 x11 x12 x13) s
 7. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12 x13 r rv'. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; dc r rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R5 x11 x12 x13 r) (?R'5 x11 x12 x13 rv') (return (Inr ())) (lift (\<lambda>y. returnOk []) rv')
 2. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 x11 x12 x13\<rbrace> Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation) \<lbrace>?R5 x11 x12 x13\<rbrace>
 3. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5 x11 x12 x13\<rbrace> Interrupt_A.invoke_irq_control irq_control_invocation \<lbrace>?R'5 x11 x12 x13\<rbrace>
 4. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5 x11 x12 x13) s
 5. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) s\<rbrakk> \<Longrightarrow> (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs and ?Q'5 x11 x12 x13) s
 6. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12 x13 r rv'. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; dc r rv'; \<exists>x. rv' = Inr x\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R5 x11 x12 x13 r) (?P'12 x11 x12 x13 rv') (return (Inr ())) (lift (\<lambda>y. returnOk []) rv')
 2. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 x11 x12 x13\<rbrace> Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation) \<lbrace>?R5 x11 x12 x13\<rbrace>
 3. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5 x11 x12 x13\<rbrace> Interrupt_A.invoke_irq_control irq_control_invocation \<lbrace>\<lambda>rv'. ?P'12 x11 x12 x13 rv' and (\<lambda>s. \<exists>x. rv' = Inr x)\<rbrace>
 4. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5 x11 x12 x13) s
 5. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) s\<rbrakk> \<Longrightarrow> (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs and ?Q'5 x11 x12 x13) s
 6. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12 x13 r rv'. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; dc r rv'; \<exists>x. rv' = Inr x\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (return (Inr ())) (lift (\<lambda>y. returnOk []) rv')
 2. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 x11 x12 x13\<rbrace> Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation) \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5 x11 x12 x13\<rbrace> Interrupt_A.invoke_irq_control irq_control_invocation \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. \<exists>x. rv' = Inr x)\<rbrace>
 4. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5 x11 x12 x13) s
 5. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) s\<rbrakk> \<Longrightarrow> (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs and ?Q'5 x11 x12 x13) s
 6. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 x11 x12 x13\<rbrace> Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5 x11 x12 x13\<rbrace> Interrupt_A.invoke_irq_control irq_control_invocation \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. \<exists>x. rv' = Inr x)\<rbrace>
 3. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5 x11 x12 x13) s
 4. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) s\<rbrakk> \<Longrightarrow> (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs and ?Q'5 x11 x12 x13) s
 5. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5 x11 x12 x13\<rbrace> Interrupt_A.invoke_irq_control irq_control_invocation \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. \<exists>x. rv' = Inr x)\<rbrace>
 2. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 3. \<And>x11 x12 x13 s. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = IRQControl x11 x12 x13; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) s\<rbrakk> \<Longrightarrow> (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs and ?Q'5 x11 x12 x13) s
 4. \<And>x2. \<lbrakk>i = InvokeIrqControl (translate_irq_control_invocation irq_control_invocation); i' = InvokeIRQControl irq_control_invocation; irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl irq_control_invocation) and irq_control_inv_valid irq_control_invocation) (do r <- Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation);
return (Inr ())
od) (Interrupt_A.invoke_irq_control irq_control_invocation >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>i = InvokeIrqControl (case x2 of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl x2); irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl x2)) and arch_irq_control_inv_valid x2) (do r <- Interrupt_D.invoke_irq_control (case x2 of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p));
return (Inr ())
od) (local.arch_invoke_irq_control x2 >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>i = InvokeIrqControl (case x2 of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl x2); irq_control_invocation = ArchIRQControl x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl x2)) and arch_irq_control_inv_valid x2) (do r <- Interrupt_D.invoke_irq_control (case x2 of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p));
return (Inr ())
od) (local.arch_invoke_irq_control x2 >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (1 subgoal):
 1. \<And>arch_label. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) (do r <- Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p));
return (Inr ())
od) (local.arch_invoke_irq_control arch_label >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (1 subgoal):
 1. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) (do r <- Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p));
return (Inr ())
od) (local.arch_invoke_irq_control arch_label >>= lift (\<lambda>y. returnOk [])) proof (prove)
goal (3 subgoals):
 1. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q31 arch_label x1 x2 x3 x4) (?Q'31 arch_label x1 x2 x3 x4) (do r <- Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p));
return (Inr ())
od) (local.arch_invoke_irq_control arch_label >>= lift (\<lambda>y. returnOk []))
 2. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; True\<rbrakk> \<Longrightarrow> ?Q31 arch_label x1 x2 x3 x4 s
 3. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) s\<rbrakk> \<Longrightarrow> ?Q'31 arch_label x1 x2 x3 x4 s proof (prove)
goal (6 subgoals):
 1. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> dcorres dc (?P35 arch_label x1 x2 x3 x4) (?P'35 arch_label x1 x2 x3 x4) (Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p))) (local.arch_invoke_irq_control arch_label)
 2. \<And>arch_label x1 x2 x3 x4 r rv'. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; dc r rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R35 arch_label x1 x2 x3 x4 r) (?R'35 arch_label x1 x2 x3 x4 rv') (return (Inr ())) (lift (\<lambda>y. returnOk []) rv')
 3. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 arch_label x1 x2 x3 x4\<rbrace> Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)) \<lbrace>?R35 arch_label x1 x2 x3 x4\<rbrace>
 4. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'35 arch_label x1 x2 x3 x4\<rbrace> local.arch_invoke_irq_control arch_label \<lbrace>?R'35 arch_label x1 x2 x3 x4\<rbrace>
 5. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; True\<rbrakk> \<Longrightarrow> (?P35 arch_label x1 x2 x3 x4 and ?Q35 arch_label x1 x2 x3 x4) s
 6. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) s\<rbrakk> \<Longrightarrow> (?P'35 arch_label x1 x2 x3 x4 and ?Q'35 arch_label x1 x2 x3 x4) s proof (prove)
goal (5 subgoals):
 1. \<And>arch_label x1 x2 x3 x4 r rv'. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; dc r rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R35 arch_label x1 x2 x3 x4 r) (?R'35 arch_label x1 x2 x3 x4 rv') (return (Inr ())) (lift (\<lambda>y. returnOk []) rv')
 2. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 arch_label x1 x2 x3 x4\<rbrace> Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)) \<lbrace>?R35 arch_label x1 x2 x3 x4\<rbrace>
 3. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'35 arch_label x1 x2 x3 x4\<rbrace> local.arch_invoke_irq_control arch_label \<lbrace>?R'35 arch_label x1 x2 x3 x4\<rbrace>
 4. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q35 arch_label x1 x2 x3 x4) s
 5. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) s\<rbrakk> \<Longrightarrow> (invs and arch_irq_control_inv_valid arch_label and valid_etcbs and ?Q'35 arch_label x1 x2 x3 x4) s proof (prove)
goal (5 subgoals):
 1. \<And>arch_label x1 x2 x3 x4 r rv'. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; dc r rv'; \<exists>x. rv' = Inr x\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R35 arch_label x1 x2 x3 x4 r) (?P'42 arch_label x1 x2 x3 x4 rv') (return (Inr ())) (lift (\<lambda>y. returnOk []) rv')
 2. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 arch_label x1 x2 x3 x4\<rbrace> Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)) \<lbrace>?R35 arch_label x1 x2 x3 x4\<rbrace>
 3. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'35 arch_label x1 x2 x3 x4\<rbrace> local.arch_invoke_irq_control arch_label \<lbrace>\<lambda>rv'. ?P'42 arch_label x1 x2 x3 x4 rv' and (\<lambda>s. \<exists>x. rv' = Inr x)\<rbrace>
 4. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q35 arch_label x1 x2 x3 x4) s
 5. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) s\<rbrakk> \<Longrightarrow> (invs and arch_irq_control_inv_valid arch_label and valid_etcbs and ?Q'35 arch_label x1 x2 x3 x4) s proof (prove)
goal (5 subgoals):
 1. \<And>arch_label x1 x2 x3 x4 r rv'. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; dc r rv'; \<exists>x. rv' = Inr x\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (return (Inr ())) (lift (\<lambda>y. returnOk []) rv')
 2. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 arch_label x1 x2 x3 x4\<rbrace> Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)) \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'35 arch_label x1 x2 x3 x4\<rbrace> local.arch_invoke_irq_control arch_label \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. \<exists>x. rv' = Inr x)\<rbrace>
 4. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q35 arch_label x1 x2 x3 x4) s
 5. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) s\<rbrakk> \<Longrightarrow> (invs and arch_irq_control_inv_valid arch_label and valid_etcbs and ?Q'35 arch_label x1 x2 x3 x4) s proof (prove)
goal (4 subgoals):
 1. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q35 arch_label x1 x2 x3 x4\<rbrace> Interrupt_D.invoke_irq_control (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'35 arch_label x1 x2 x3 x4\<rbrace> local.arch_invoke_irq_control arch_label \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. \<exists>x. rv' = Inr x)\<rbrace>
 3. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q35 arch_label x1 x2 x3 x4) s
 4. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) s\<rbrakk> \<Longrightarrow> (invs and arch_irq_control_inv_valid arch_label and valid_etcbs and ?Q'35 arch_label x1 x2 x3 x4) s proof (prove)
goal (3 subgoals):
 1. \<And>arch_label x1 x2 x3 x4. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>?Q'35 arch_label x1 x2 x3 x4\<rbrace> local.arch_invoke_irq_control arch_label \<lbrace>\<lambda>rv'. (\<lambda>_. True) and (\<lambda>s. \<exists>x. rv' = Inr x)\<rbrace>
 2. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>_. True)) s
 3. \<And>arch_label x1 x2 x3 x4 s. \<lbrakk>i = InvokeIrqControl (case arch_label of ArchIRQControlIssue irq p slot t \<Rightarrow> IssueIrqHandler irq (transform_cslot_ptr slot) (transform_cslot_ptr p)); i' = InvokeIRQControl (ArchIRQControl arch_label); irq_control_invocation = ArchIRQControl arch_label; arch_label = ArchIRQControlIssue x1 x2 x3 x4; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQControl (ArchIRQControl arch_label)) and arch_irq_control_inv_valid arch_label) s\<rbrakk> \<Longrightarrow> (invs and arch_irq_control_inv_valid arch_label and valid_etcbs and ?Q'35 arch_label x1 x2 x3 x4) s proof (prove)
goal:
No subgoals! proof (prove)
goal (2 subgoals):
 1. \<And>x9. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9); i' = InvokeIRQHandler x9\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9) and irq_handler_inv_valid x9) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9);
returnOk []
odE)
 2. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9_) and irq_handler_inv_valid x9_) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9_);
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9_) and irq_handler_inv_valid x9_) (liftE (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_))) (doE y <- liftE (Interrupt_A.invoke_irq_handler x9_);
returnOk []
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9_) and irq_handler_inv_valid x9_) (do r <- Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_);
return (Inr ())
od) (do y <- Interrupt_A.invoke_irq_handler x9_;
return (Inr [])
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ?Q ?Q' (do r <- Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_);
return (Inr ())
od) (do y <- Interrupt_A.invoke_irq_handler x9_;
return (Inr [])
od)
 2. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9_) and irq_handler_inv_valid x9_) s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> dcorres ?r'4 ?P4 ?P'4 (Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_)) (Interrupt_A.invoke_irq_handler x9_)
 2. \<And>r y. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; ?r'4 r y\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R4 r) (?R'4 y) (return (Inr ())) (return (Inr []))
 3. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_) \<lbrace>?R4\<rbrace>
 4. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> Interrupt_A.invoke_irq_handler x9_ \<lbrace>?R'4\<rbrace>
 5. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; True\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9_) and irq_handler_inv_valid x9_) s\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r y. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; dc r y\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R4 r) (?R'4 y) (return (Inr ())) (return (Inr []))
 2. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_) \<lbrace>?R4\<rbrace>
 3. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> Interrupt_A.invoke_irq_handler x9_ \<lbrace>?R'4\<rbrace>
 4. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9_) and irq_handler_inv_valid x9_) s\<rbrakk> \<Longrightarrow> (invs and irq_handler_inv_valid x9_ and valid_etcbs and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r y. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; dc r y\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (return (Inr ())) (return (Inr []))
 2. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_) \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> Interrupt_A.invoke_irq_handler x9_ \<lbrace>\<lambda>y _. True\<rbrace>
 4. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9_) and irq_handler_inv_valid x9_) s\<rbrakk> \<Longrightarrow> (invs and irq_handler_inv_valid x9_ and valid_etcbs and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> Interrupt_D.invoke_irq_handler (translate_irq_handler_invocation x9_) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> Interrupt_A.invoke_irq_handler x9_ \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. \<lbrakk>i = InvokeIrqHandler (translate_irq_handler_invocation x9_); i' = InvokeIRQHandler x9_; (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeIRQHandler x9_) and irq_handler_inv_valid x9_) s\<rbrakk> \<Longrightarrow> (invs and irq_handler_inv_valid x9_ and valid_etcbs and ?Q'4) s proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>x10. \<lbrakk>arch_invocation_relation i x10; i' = InvokeArchObject x10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10) and valid_arch_inv x10) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_invocation_relation i x10_; i' = InvokeArchObject x10_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10_) and valid_arch_inv x10_) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10_) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_invocation_relation i x10_; i' = InvokeArchObject x10_\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and invocation_duplicates_valid (InvokeArchObject x10_) and valid_arch_inv x10_) (Syscall_D.perform_invocation call block i) (arch_perform_invocation x10_) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!