theory Arch_DR

lemma invoke_arch_corres:
  "arch_invocation_relation invok arch_invok
   \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True)
   (invs and ct_active and valid_arch_inv arch_invok
         and invocation_duplicates_valid (Invocations_A.InvokeArchObject arch_invok)
         and valid_pdpt_objs and valid_etcbs)
   (Syscall_D.perform_invocation block call_m invok)
    (arch_perform_invocation arch_invok)" apply (clarsimp simp: arch_perform_invocation_def valid_arch_inv_def) apply (case_tac arch_invok) apply (simp_all add:arch_invocation_relation_def translate_arch_invocation_def) apply (clarsimp simp:liftE_def bind_assoc) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule invoke_page_table_corres; simp) apply (rule corres_trivial, simp) apply (wp | clarsimp)+ apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule invoke_page_directory_corres; simp) apply (rule corres_trivial[OF corres_free_return]) apply (wp | clarsimp)+ apply (rule corres_guard_imp) apply (rule invoke_page_corres) apply (wp | clarsimp simp:invocation_duplicates_valid_def)+ apply (clarsimp split: asid_control_invocation.split) apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule invoke_asid_control_corres) apply (simp add: arch_invocation_relation_def translate_arch_invocation_def) apply (rule corres_trivial, simp) apply (wp | simp)+ apply (clarsimp split: asid_pool_invocation.split) apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule invoke_asid_pool_corres) apply (simp add: arch_invocation_relation_def translate_arch_invocation_def) apply (rule corres_trivial[OF corres_free_return]) apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_invocation_relation invok arch_invok \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_arch_inv arch_invok and invocation_duplicates_valid (InvokeArchObject arch_invok) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (arch_perform_invocation arch_invok) proof (prove)
goal (1 subgoal):
 1. arch_invocation_relation invok arch_invok \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (case arch_invok of arch_invocation.InvokePageTable pti \<Rightarrow> valid_pti pti | arch_invocation.InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | arch_invocation.InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and invocation_duplicates_valid (InvokeArchObject arch_invok) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (case arch_invok of arch_invocation.InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | arch_invocation.InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | arch_invocation.InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od)) proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>arch_invocation_relation invok arch_invok; arch_invok = arch_invocation.InvokePageTable x1\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (case arch_invok of arch_invocation.InvokePageTable pti \<Rightarrow> valid_pti pti | arch_invocation.InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | arch_invocation.InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and invocation_duplicates_valid (InvokeArchObject arch_invok) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (case arch_invok of arch_invocation.InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | arch_invocation.InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | arch_invocation.InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od))
 2. \<And>x2. \<lbrakk>arch_invocation_relation invok arch_invok; arch_invok = arch_invocation.InvokePageDirectory x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (case arch_invok of arch_invocation.InvokePageTable pti \<Rightarrow> valid_pti pti | arch_invocation.InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | arch_invocation.InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and invocation_duplicates_valid (InvokeArchObject arch_invok) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (case arch_invok of arch_invocation.InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | arch_invocation.InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | arch_invocation.InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od))
 3. \<And>x3. \<lbrakk>arch_invocation_relation invok arch_invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (case arch_invok of arch_invocation.InvokePageTable pti \<Rightarrow> valid_pti pti | arch_invocation.InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | arch_invocation.InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and invocation_duplicates_valid (InvokeArchObject arch_invok) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (case arch_invok of arch_invocation.InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | arch_invocation.InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | arch_invocation.InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od))
 4. \<And>x4. \<lbrakk>arch_invocation_relation invok arch_invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (case arch_invok of arch_invocation.InvokePageTable pti \<Rightarrow> valid_pti pti | arch_invocation.InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | arch_invocation.InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and invocation_duplicates_valid (InvokeArchObject arch_invok) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (case arch_invok of arch_invocation.InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | arch_invocation.InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | arch_invocation.InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od))
 5. \<And>x5. \<lbrakk>arch_invocation_relation invok arch_invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and (case arch_invok of arch_invocation.InvokePageTable pti \<Rightarrow> valid_pti pti | arch_invocation.InvokePageDirectory pdi \<Rightarrow> valid_pdi pdi | arch_invocation.InvokePage pgi \<Rightarrow> valid_page_inv pgi | InvokeASIDControl aci \<Rightarrow> valid_aci aci | InvokeASIDPool ap \<Rightarrow> valid_apinv ap) and invocation_duplicates_valid (InvokeArchObject arch_invok) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (case arch_invok of arch_invocation.InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | arch_invocation.InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | arch_invocation.InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od)) proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>\<exists>z. transform_page_table_inv x1 = Some z \<and> cdl_invocation.InvokePageTable z = invok; arch_invok = arch_invocation.InvokePageTable x1\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_pti x1 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageTable x1)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_page_table_invocation x1;
return []
od))
 2. \<And>x2. \<lbrakk>\<exists>z. transform_page_dir_inv x2 = Some z \<and> cdl_invocation.InvokePageDirectory z = invok; arch_invok = arch_invocation.InvokePageDirectory x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_page_directory_invocation x2;
return []
od))
 3. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 4. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 5. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (5 subgoals):
 1. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_pti x1 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageTable x1)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (do r <- invoke_page_table z;
return (Inr ())
od) (do y <- perform_page_table_invocation x1;
return (Inr [])
od)
 2. \<And>x2. \<lbrakk>\<exists>z. transform_page_dir_inv x2 = Some z \<and> cdl_invocation.InvokePageDirectory z = invok; arch_invok = arch_invocation.InvokePageDirectory x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_page_directory_invocation x2;
return []
od))
 3. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 4. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 5. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (7 subgoals):
 1. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q10 x1 z) (?Q'10 x1 z) (do r <- invoke_page_table z;
return (Inr ())
od) (do y <- perform_page_table_invocation x1;
return (Inr [])
od)
 2. \<And>x1 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; True\<rbrakk> \<Longrightarrow> ?Q10 x1 z s
 3. \<And>x1 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; (invs and ct_active and valid_pti x1 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageTable x1)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'10 x1 z s
 4. \<And>x2. \<lbrakk>\<exists>z. transform_page_dir_inv x2 = Some z \<and> cdl_invocation.InvokePageDirectory z = invok; arch_invok = arch_invocation.InvokePageDirectory x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_page_directory_invocation x2;
return []
od))
 5. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 6. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 7. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (10 subgoals):
 1. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> dcorres (?r'14 x1 z) (?P14 x1 z) (?P'14 x1 z) (invoke_page_table z) (perform_page_table_invocation x1)
 2. \<And>x1 z r y. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; ?r'14 x1 z r y\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R14 x1 z r) (?R'14 x1 z y) (return (Inr ())) (return (Inr []))
 3. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 x1 z\<rbrace> invoke_page_table z \<lbrace>?R14 x1 z\<rbrace>
 4. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 x1 z\<rbrace> perform_page_table_invocation x1 \<lbrace>?R'14 x1 z\<rbrace>
 5. \<And>x1 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; True\<rbrakk> \<Longrightarrow> (?P14 x1 z and ?Q14 x1 z) s
 6. \<And>x1 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; (invs and ct_active and valid_pti x1 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageTable x1)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'14 x1 z and ?Q'14 x1 z) s
 7. \<And>x2. \<lbrakk>\<exists>z. transform_page_dir_inv x2 = Some z \<and> cdl_invocation.InvokePageDirectory z = invok; arch_invok = arch_invocation.InvokePageDirectory x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_page_directory_invocation x2;
return []
od))
 8. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 9. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 10. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (9 subgoals):
 1. \<And>x1 z r y. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; dc r y\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?R14 x1 z r) (?R'14 x1 z y) (return (Inr ())) (return (Inr []))
 2. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 x1 z\<rbrace> invoke_page_table z \<lbrace>?R14 x1 z\<rbrace>
 3. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 x1 z\<rbrace> perform_page_table_invocation x1 \<lbrace>?R'14 x1 z\<rbrace>
 4. \<And>x1 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q14 x1 z) s
 5. \<And>x1 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; (invs and ct_active and valid_pti x1 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageTable x1)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_pti x1 and invs and valid_etcbs and ?Q'14 x1 z) s
 6. \<And>x2. \<lbrakk>\<exists>z. transform_page_dir_inv x2 = Some z \<and> cdl_invocation.InvokePageDirectory z = invok; arch_invok = arch_invocation.InvokePageDirectory x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_page_directory_invocation x2;
return []
od))
 7. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 8. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 9. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (8 subgoals):
 1. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 x1 z\<rbrace> invoke_page_table z \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>x1 z. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 x1 z\<rbrace> perform_page_table_invocation x1 \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>x1 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q14 x1 z) s
 4. \<And>x1 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageTable x1; transform_page_table_inv x1 = Some z; invok = cdl_invocation.InvokePageTable z; (invs and ct_active and valid_pti x1 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageTable x1)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_pti x1 and invs and valid_etcbs and ?Q'14 x1 z) s
 5. \<And>x2. \<lbrakk>\<exists>z. transform_page_dir_inv x2 = Some z \<and> cdl_invocation.InvokePageDirectory z = invok; arch_invok = arch_invocation.InvokePageDirectory x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_page_directory_invocation x2;
return []
od))
 6. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 7. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 8. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (4 subgoals):
 1. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (invoke_page_directory z) (do y <- perform_page_directory_invocation x2;
return []
od)
 2. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 3. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 4. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (4 subgoals):
 1. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (invoke_page_directory z >>= return) (do y <- perform_page_directory_invocation x2;
return []
od)
 2. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 3. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 4. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (6 subgoals):
 1. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> dcorres dc (?Q42 x2 z) (?Q'42 x2 z) (invoke_page_directory z >>= return) (do y <- perform_page_directory_invocation x2;
return []
od)
 2. \<And>x2 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; True\<rbrakk> \<Longrightarrow> ?Q42 x2 z s
 3. \<And>x2 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'42 x2 z s
 4. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 5. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 6. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (9 subgoals):
 1. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> dcorres (?r'46 x2 z) (?P46 x2 z) (?P'46 x2 z) (invoke_page_directory z) (perform_page_directory_invocation x2)
 2. \<And>x2 z x y. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; ?r'46 x2 z x y\<rbrakk> \<Longrightarrow> dcorres dc (?R46 x2 z x) (?R'46 x2 z y) (return x) (return [])
 3. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 x2 z\<rbrace> invoke_page_directory z \<lbrace>?R46 x2 z\<rbrace>
 4. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 x2 z\<rbrace> perform_page_directory_invocation x2 \<lbrace>?R'46 x2 z\<rbrace>
 5. \<And>x2 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; True\<rbrakk> \<Longrightarrow> (?P46 x2 z and ?Q46 x2 z) s
 6. \<And>x2 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'46 x2 z and ?Q'46 x2 z) s
 7. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 8. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 9. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (8 subgoals):
 1. \<And>x2 z x y. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R46 x2 z x) (?R'46 x2 z y) (return x) (return [])
 2. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 x2 z\<rbrace> invoke_page_directory z \<lbrace>?R46 x2 z\<rbrace>
 3. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 x2 z\<rbrace> perform_page_directory_invocation x2 \<lbrace>?R'46 x2 z\<rbrace>
 4. \<And>x2 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q46 x2 z) s
 5. \<And>x2 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and ?Q'46 x2 z) s
 6. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 7. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 8. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (7 subgoals):
 1. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 x2 z\<rbrace> invoke_page_directory z \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>x2 z. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 x2 z\<rbrace> perform_page_directory_invocation x2 \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>x2 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q46 x2 z) s
 4. \<And>x2 z s. \<lbrakk>arch_invok = arch_invocation.InvokePageDirectory x2; transform_page_dir_inv x2 = Some z; invok = cdl_invocation.InvokePageDirectory z; (invs and ct_active and valid_pdi x2 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePageDirectory x2)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and ?Q'46 x2 z) s
 5. \<And>x3. \<lbrakk>\<exists>z. transform_page_inv x3 = Some z \<and> cdl_invocation.InvokePage z = invok; arch_invok = arch_invocation.InvokePage x3\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (perform_page_invocation x3))
 6. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 7. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (3 subgoals):
 1. \<And>x3 z. \<lbrakk>arch_invok = arch_invocation.InvokePage x3; transform_page_inv x3 = Some z; invok = cdl_invocation.InvokePage z\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (invoke_page z) (perform_page_invocation x3)
 2. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 3. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (5 subgoals):
 1. \<And>x3 z. \<lbrakk>arch_invok = arch_invocation.InvokePage x3; transform_page_inv x3 = Some z; invok = cdl_invocation.InvokePage z\<rbrakk> \<Longrightarrow> dcorres dc (?Q72 x3 z) (?Q'72 x3 z) (invoke_page z) (perform_page_invocation x3)
 2. \<And>x3 z s. \<lbrakk>arch_invok = arch_invocation.InvokePage x3; transform_page_inv x3 = Some z; invok = cdl_invocation.InvokePage z; True\<rbrakk> \<Longrightarrow> ?Q72 x3 z s
 3. \<And>x3 z s. \<lbrakk>arch_invok = arch_invocation.InvokePage x3; transform_page_inv x3 = Some z; invok = cdl_invocation.InvokePage z; (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'72 x3 z s
 4. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 5. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (5 subgoals):
 1. \<And>x3 z. \<lbrakk>arch_invok = arch_invocation.InvokePage x3; transform_page_inv x3 = Some z; invok = cdl_invocation.InvokePage z\<rbrakk> \<Longrightarrow> transform_page_inv x3 = Some z
 2. \<And>x3 z s. \<lbrakk>arch_invok = arch_invocation.InvokePage x3; transform_page_inv x3 = Some z; invok = cdl_invocation.InvokePage z; True\<rbrakk> \<Longrightarrow> True
 3. \<And>x3 z s. \<lbrakk>arch_invok = arch_invocation.InvokePage x3; transform_page_inv x3 = Some z; invok = cdl_invocation.InvokePage z; (invs and ct_active and valid_page_inv x3 and invocation_duplicates_valid (InvokeArchObject (arch_invocation.InvokePage x3)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_page_inv x3 and invs and page_inv_duplicates_valid x3 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs and ct_active) s
 4. \<And>x4. \<lbrakk>(case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base))) = invok; arch_invok = InvokeASIDControl x4\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDControl x4)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 5. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>arch_invok = InvokeASIDControl x4; invok = (case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base)))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_aci x4 and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m (case x4 of asid_control_invocation.MakePool frame slot parent base \<Rightarrow> InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {frame..frame + 2 ^ pageBits - 1} {}) (transform_cslot_ptr parent) {frame..frame + 2 ^ pageBits - 1} (transform_cslot_ptr slot) (fst $ transform_asid base)))) (liftE (do y <- perform_asid_control_invocation x4;
return []
od))
 2. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (invoke_asid_control (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))) (do y <- perform_asid_control_invocation (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a);
return []
od)
 2. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (invoke_asid_control (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))) >>= return) (do y <- perform_asid_control_invocation (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a);
return []
od)
 2. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (4 subgoals):
 1. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> dcorres dc (?Q101 x1 a b aa ba x4a) (?Q'101 x1 a b aa ba x4a) (invoke_asid_control (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))) >>= return) (do y <- perform_asid_control_invocation (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a);
return []
od)
 2. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); True\<rbrakk> \<Longrightarrow> ?Q101 x1 a b aa ba x4a s
 3. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'101 x1 a b aa ba x4a s
 4. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (7 subgoals):
 1. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> dcorres (?r'105 x1 a b aa ba x4a) (?P105 x1 a b aa ba x4a) (?P'105 x1 a b aa ba x4a) (invoke_asid_control (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))) (perform_asid_control_invocation (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a))
 2. \<And>x1 a b aa ba x4a x y. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); ?r'105 x1 a b aa ba x4a x y\<rbrakk> \<Longrightarrow> dcorres dc (?R105 x1 a b aa ba x4a x) (?R'105 x1 a b aa ba x4a y) (return x) (return [])
 3. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q105 x1 a b aa ba x4a\<rbrace> invoke_asid_control (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))) \<lbrace>?R105 x1 a b aa ba x4a\<rbrace>
 4. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'105 x1 a b aa ba x4a\<rbrace> perform_asid_control_invocation (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) \<lbrace>?R'105 x1 a b aa ba x4a\<rbrace>
 5. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); True\<rbrakk> \<Longrightarrow> (?P105 x1 a b aa ba x4a and ?Q105 x1 a b aa ba x4a) s
 6. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'105 x1 a b aa ba x4a and ?Q'105 x1 a b aa ba x4a) s
 7. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (7 subgoals):
 1. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> arch_invocation_relation (InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))) (InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a))
 2. \<And>x1 a b aa ba x4a x y. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R105 x1 a b aa ba x4a x) (?R'105 x1 a b aa ba x4a y) (return x) (return [])
 3. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q105 x1 a b aa ba x4a\<rbrace> invoke_asid_control (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))) \<lbrace>?R105 x1 a b aa ba x4a\<rbrace>
 4. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'105 x1 a b aa ba x4a\<rbrace> perform_asid_control_invocation (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) \<lbrace>?R'105 x1 a b aa ba x4a\<rbrace>
 5. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q105 x1 a b aa ba x4a) s
 6. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and valid_etcbs and ?Q'105 x1 a b aa ba x4a) s
 7. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (6 subgoals):
 1. \<And>x1 a b aa ba x4a x y. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R105 x1 a b aa ba x4a x) (?R'105 x1 a b aa ba x4a y) (return x) (return [])
 2. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q105 x1 a b aa ba x4a\<rbrace> invoke_asid_control (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))) \<lbrace>?R105 x1 a b aa ba x4a\<rbrace>
 3. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'105 x1 a b aa ba x4a\<rbrace> perform_asid_control_invocation (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) \<lbrace>?R'105 x1 a b aa ba x4a\<rbrace>
 4. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q105 x1 a b aa ba x4a) s
 5. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and valid_etcbs and ?Q'105 x1 a b aa ba x4a) s
 6. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (5 subgoals):
 1. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q105 x1 a b aa ba x4a\<rbrace> invoke_asid_control (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>x1 a b aa ba x4a. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'105 x1 a b aa ba x4a\<rbrace> perform_asid_control_invocation (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q105 x1 a b aa ba x4a) s
 4. \<And>x1 a b aa ba x4a s. \<lbrakk>arch_invok = InvokeASIDControl (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a); invok = InvokeAsidControl (cdl_asid_control_invocation.MakePool (cdl_cap.UntypedCap False {x1..x1 + 2 ^ pageBits - 1} {}) (transform_cslot_ptr (aa, ba)) {x1..x1 + 2 ^ pageBits - 1} (transform_cslot_ptr (a, b)) (fst (transform_asid x4a))); (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and ct_active and valid_aci (asid_control_invocation.MakePool x1 (a, b) (aa, ba) x4a) and valid_etcbs and ?Q'105 x1 a b aa ba x4a) s
 5. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>(case x5 of asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid asid) (transform_cslot_ptr ct_slot) (pool_ptr, snd (transform_asid asid)))) = invok; arch_invok = InvokeASIDPool x5\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and ct_active and valid_apinv x5 and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool x5)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (Syscall_D.perform_invocation block call_m invok) (liftE (do y <- perform_asid_pool_invocation x5;
return []
od)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)))) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (invoke_asid_pool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))) (do y <- perform_asid_pool_invocation (asid_pool_invocation.Assign x1 x2 (a, b));
return []
od) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and ct_active and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)))) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (invoke_asid_pool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))) >>= return) (do y <- perform_asid_pool_invocation (asid_pool_invocation.Assign x1 x2 (a, b));
return []
od) proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> dcorres dc (?Q135 x1 x2 a b) (?Q'135 x1 x2 a b) (invoke_asid_pool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))) >>= return) (do y <- perform_asid_pool_invocation (asid_pool_invocation.Assign x1 x2 (a, b));
return []
od)
 2. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); True\<rbrakk> \<Longrightarrow> ?Q135 x1 x2 a b s
 3. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); (invs and ct_active and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)))) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'135 x1 x2 a b s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> dcorres (?r'139 x1 x2 a b) (?P139 x1 x2 a b) (?P'139 x1 x2 a b) (invoke_asid_pool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))) (perform_asid_pool_invocation (asid_pool_invocation.Assign x1 x2 (a, b)))
 2. \<And>x1 x2 a b x y. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); ?r'139 x1 x2 a b x y\<rbrakk> \<Longrightarrow> dcorres dc (?R139 x1 x2 a b x) (?R'139 x1 x2 a b y) (return x) (return [])
 3. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q139 x1 x2 a b\<rbrace> invoke_asid_pool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))) \<lbrace>?R139 x1 x2 a b\<rbrace>
 4. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 x1 x2 a b\<rbrace> perform_asid_pool_invocation (asid_pool_invocation.Assign x1 x2 (a, b)) \<lbrace>?R'139 x1 x2 a b\<rbrace>
 5. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); True\<rbrakk> \<Longrightarrow> (?P139 x1 x2 a b and ?Q139 x1 x2 a b) s
 6. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); (invs and ct_active and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)))) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'139 x1 x2 a b and ?Q'139 x1 x2 a b) s proof (prove)
goal (6 subgoals):
 1. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> arch_invocation_relation (InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))) (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)))
 2. \<And>x1 x2 a b x y. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R139 x1 x2 a b x) (?R'139 x1 x2 a b y) (return x) (return [])
 3. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q139 x1 x2 a b\<rbrace> invoke_asid_pool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))) \<lbrace>?R139 x1 x2 a b\<rbrace>
 4. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 x1 x2 a b\<rbrace> perform_asid_pool_invocation (asid_pool_invocation.Assign x1 x2 (a, b)) \<lbrace>?R'139 x1 x2 a b\<rbrace>
 5. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q139 x1 x2 a b) s
 6. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); (invs and ct_active and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)))) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and valid_etcbs and ?Q'139 x1 x2 a b) s proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 a b x y. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R139 x1 x2 a b x) (?R'139 x1 x2 a b y) (return x) (return [])
 2. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q139 x1 x2 a b\<rbrace> invoke_asid_pool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))) \<lbrace>?R139 x1 x2 a b\<rbrace>
 3. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 x1 x2 a b\<rbrace> perform_asid_pool_invocation (asid_pool_invocation.Assign x1 x2 (a, b)) \<lbrace>?R'139 x1 x2 a b\<rbrace>
 4. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q139 x1 x2 a b) s
 5. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); (invs and ct_active and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)))) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and valid_etcbs and ?Q'139 x1 x2 a b) s proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q139 x1 x2 a b\<rbrace> invoke_asid_pool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>x1 x2 a b. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1)))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'139 x1 x2 a b\<rbrace> perform_asid_pool_invocation (asid_pool_invocation.Assign x1 x2 (a, b)) \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q139 x1 x2 a b) s
 4. \<And>x1 x2 a b s. \<lbrakk>arch_invok = InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)); invok = InvokeAsidPool (cdl_asid_pool_invocation.Assign (transform_asid x1) (transform_cslot_ptr (a, b)) (x2, snd (transform_asid x1))); (invs and ct_active and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and invocation_duplicates_valid (InvokeArchObject (InvokeASIDPool (asid_pool_invocation.Assign x1 x2 (a, b)))) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (invs and valid_apinv (asid_pool_invocation.Assign x1 x2 (a, b)) and valid_etcbs and ?Q'139 x1 x2 a b) s proof (prove)
goal:
No subgoals!