theory Arch_R

lemma decodeARMPageFlush_corres:
  "ARM_H.isPageFlushLabel (invocation_type (mi_label mi)) \<Longrightarrow>
   corres (ser \<oplus> archinv_relation)
           (invs and
            valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and
            cte_wp_at
             ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)))
             slot and
            (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s))
           (invs' and
            valid_cap'
             (capability.ArchObjectCap
               (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and
            (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and
            (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
           (if Suc 0 < length args
            then let start = args ! 0; end = args ! 1
                 in doE (asid, vaddr) \<leftarrow>
                        case option of
                        None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation
                        | Some x \<Rightarrow> returnOk x;
                        pd \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid;
                        whenE (end \<le> start) $
                        throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
                        page_size \<leftarrow> returnOk $ 1 << pageBitsForSize vmpage_size;
                        whenE (page_size \<le> start \<or> page_size < end) $
                        throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
                        returnOk $
                        arch_invocation.InvokePage $
                        ARM_A.page_invocation.PageFlush
                         (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr)
                         (end + vaddr - 1) (addrFromPPtr word + start) pd asid
                    odE
            else throwError ExceptionTypes_A.syscall_error.TruncatedMessage)
           (decodeARMPageFlush (mi_label mi) args
             (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))" apply (simp add: decodeARMPageFlush_def split del: if_split) apply (cases args, simp) apply (rename_tac a0 as) apply (case_tac as, simp) apply (rename_tac a1 as') apply (cases option, simp) apply (case_tac a) apply (rename_tac asid vref) apply clarsimp apply (rule corres_guard_imp) apply (rule corres_splitEE) apply (rule corres_lookup_error) apply (rule find_pd_for_asid_corres[OF refl]) apply (rule whenE_throwError_corres, simp) apply simp apply (rule whenE_throwError_corres, simp) apply simp apply (rule corres_trivial) apply (rule corres_returnOk) apply (clarsimp simp: archinv_relation_def page_invocation_map_def
                            label_to_flush_type_def labelToFlushType_def flush_type_map_def
                            ARM_H.isPageFlushLabel_def
                     split: flush_type.splits invocation_label.splits arch_invocation_label.splits) apply wp+ apply (fastforce simp: valid_cap_def mask_def
                          invs_vspace_objs[simplified]) apply (auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isPageFlushLabel (invocation_type (mi_label mi)) \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (decodeARMPageFlush (mi_label mi) args (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) proof (prove)
goal (1 subgoal):
 1. isPageFlushLabel (invocation_type (mi_label mi)) \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [start] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | start # end # xa \<Rightarrow> case option of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some (asid, vaddr) \<Rightarrow> doE pd <- lookupErrorOnFailure False $ findPDForASID asid;
whenE (end \<le> start) $ throw $ Fault_H.syscall_error.InvalidArgument 1;
pageSize <- returnOk (HaskellLib_H.bit (pageBitsForSize (capVPSize (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option));
whenE (pageSize \<le> start \<or> pageSize < end) $ throw $ Fault_H.syscall_error.InvalidArgument 0;
pstart <- returnOk (pageBase + id start);
start' <- returnOk (start + fromVPtr vaddr);
end' <- returnOk (end + fromVPtr vaddr);
returnOk $ invocation.InvokePage $ ARM_H.PageFlush (labelToFlushType (mi_label mi)) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a # list\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [start] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | start # end # xa \<Rightarrow> case option of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some (asid, vaddr) \<Rightarrow> doE pd <- lookupErrorOnFailure False $ findPDForASID asid;
whenE (end \<le> start) $ throw $ Fault_H.syscall_error.InvalidArgument 1;
pageSize <- returnOk (HaskellLib_H.bit (pageBitsForSize (capVPSize (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option));
whenE (pageSize \<le> start \<or> pageSize < end) $ throw $ Fault_H.syscall_error.InvalidArgument 0;
pstart <- returnOk (pageBase + id start);
start' <- returnOk (start + fromVPtr vaddr);
end' <- returnOk (end + fromVPtr vaddr);
returnOk $ invocation.InvokePage $ ARM_H.PageFlush (labelToFlushType (mi_label mi)) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a0 as. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # as\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [start] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | start # end # xa \<Rightarrow> case option of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some (asid, vaddr) \<Rightarrow> doE pd <- lookupErrorOnFailure False $ findPDForASID asid;
whenE (end \<le> start) $ throw $ Fault_H.syscall_error.InvalidArgument 1;
pageSize <- returnOk (HaskellLib_H.bit (pageBitsForSize (capVPSize (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option));
whenE (pageSize \<le> start \<or> pageSize < end) $ throw $ Fault_H.syscall_error.InvalidArgument 0;
pstart <- returnOk (pageBase + id start);
start' <- returnOk (start + fromVPtr vaddr);
end' <- returnOk (end + fromVPtr vaddr);
returnOk $ invocation.InvokePage $ ARM_H.PageFlush (labelToFlushType (mi_label mi)) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a0 as a list. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # as; as = a # list\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [start] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | start # end # xa \<Rightarrow> case option of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some (asid, vaddr) \<Rightarrow> doE pd <- lookupErrorOnFailure False $ findPDForASID asid;
whenE (end \<le> start) $ throw $ Fault_H.syscall_error.InvalidArgument 1;
pageSize <- returnOk (HaskellLib_H.bit (pageBitsForSize (capVPSize (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option));
whenE (pageSize \<le> start \<or> pageSize < end) $ throw $ Fault_H.syscall_error.InvalidArgument 0;
pstart <- returnOk (pageBase + id start);
start' <- returnOk (start + fromVPtr vaddr);
end' <- returnOk (end + fromVPtr vaddr);
returnOk $ invocation.InvokePage $ ARM_H.PageFlush (labelToFlushType (mi_label mi)) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a0 as a1 as'. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # as; as = a1 # as'\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [start] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | start # end # xa \<Rightarrow> case option of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some (asid, vaddr) \<Rightarrow> doE pd <- lookupErrorOnFailure False $ findPDForASID asid;
whenE (end \<le> start) $ throw $ Fault_H.syscall_error.InvalidArgument 1;
pageSize <- returnOk (HaskellLib_H.bit (pageBitsForSize (capVPSize (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option));
whenE (pageSize \<le> start \<or> pageSize < end) $ throw $ Fault_H.syscall_error.InvalidArgument 0;
pstart <- returnOk (pageBase + id start);
start' <- returnOk (start + fromVPtr vaddr);
end' <- returnOk (end + fromVPtr vaddr);
returnOk $ invocation.InvokePage $ ARM_H.PageFlush (labelToFlushType (mi_label mi)) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a0 as a1 as' a. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # as; as = a1 # as'; option = Some a\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [start] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | start # end # xa \<Rightarrow> case option of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some (asid, vaddr) \<Rightarrow> doE pd <- lookupErrorOnFailure False $ findPDForASID asid;
whenE (end \<le> start) $ throw $ Fault_H.syscall_error.InvalidArgument 1;
pageSize <- returnOk (HaskellLib_H.bit (pageBitsForSize (capVPSize (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option));
whenE (pageSize \<le> start \<or> pageSize < end) $ throw $ Fault_H.syscall_error.InvalidArgument 0;
pstart <- returnOk (pageBase + id start);
start' <- returnOk (start + fromVPtr vaddr);
end' <- returnOk (end + fromVPtr vaddr);
returnOk $ invocation.InvokePage $ ARM_H.PageFlush (labelToFlushType (mi_label mi)) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a0 as a1 as' a aa b. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # as; as = a1 # as'; option = Some a; a = (aa, b)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [start] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | start # end # xa \<Rightarrow> case option of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some (asid, vaddr) \<Rightarrow> doE pd <- lookupErrorOnFailure False $ findPDForASID asid;
whenE (end \<le> start) $ throw $ Fault_H.syscall_error.InvalidArgument 1;
pageSize <- returnOk (HaskellLib_H.bit (pageBitsForSize (capVPSize (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option));
whenE (pageSize \<le> start \<or> pageSize < end) $ throw $ Fault_H.syscall_error.InvalidArgument 0;
pstart <- returnOk (pageBase + id start);
start' <- returnOk (start + fromVPtr vaddr);
end' <- returnOk (end + fromVPtr vaddr);
returnOk $ invocation.InvokePage $ ARM_H.PageFlush (labelToFlushType (mi_label mi)) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a0 as a1 as' a asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # as; as = a1 # as'; option = Some a; a = (asid, vref)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option)) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size option))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option)) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (if Suc 0 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case option of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk x;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
returnOk $ arch_invocation.InvokePage $ ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (start + vaddr) (end + vaddr - 1) (addrFromPPtr word + start) pd asid
odE else throwError ExceptionTypes_A.syscall_error.TruncatedMessage) (case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | [start] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | start # end # xa \<Rightarrow> case option of None \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | Some (asid, vaddr) \<Rightarrow> doE pd <- lookupErrorOnFailure False $ findPDForASID asid;
whenE (end \<le> start) $ throw $ Fault_H.syscall_error.InvalidArgument 1;
pageSize <- returnOk (HaskellLib_H.bit (pageBitsForSize (capVPSize (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word (vmrights_map seta) vmpage_size option));
whenE (pageSize \<le> start \<or> pageSize < end) $ throw $ Fault_H.syscall_error.InvalidArgument 0;
pstart <- returnOk (pageBase + id start);
start' <- returnOk (start + fromVPtr vaddr);
end' <- returnOk (end + fromVPtr vaddr);
returnOk $ invocation.InvokePage $ ARM_H.PageFlush (labelToFlushType (mi_label mi)) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (doE pd <- lookup_error_on_failure False (find_pd_for_asid asid);
y <- whenE (a1 \<le> a0) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE) (doE pd <- lookupErrorOnFailure False (findPDForASID asid);
y <- whenE (a1 \<le> a0) (throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE) proof (prove)
goal (3 subgoals):
 1. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (?Q14 a0 a1 as' asid vref) (?Q'14 a0 a1 as' asid vref) (doE pd <- lookup_error_on_failure False (find_pd_for_asid asid);
y <- whenE (a1 \<le> a0) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE) (doE pd <- lookupErrorOnFailure False (findPDForASID asid);
y <- whenE (a1 \<le> a0) (throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE)
 2. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ?Q14 a0 a1 as' asid vref s
 3. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> ?Q'14 a0 a1 as' asid vref s proof (prove)
goal (6 subgoals):
 1. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> ?r'18 a0 a1 as' asid vref) (?P18 a0 a1 as' asid vref) (?P'18 a0 a1 as' asid vref) (lookup_error_on_failure False (find_pd_for_asid asid)) (lookupErrorOnFailure False (findPDForASID asid))
 2. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); ?r'18 a0 a1 as' asid vref pd pda\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (?R18 a0 a1 as' asid vref pd) (?R'18 a0 a1 as' asid vref pda) (doE y <- whenE (a1 \<le> a0) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE) (doE y <- whenE (a1 \<le> a0) (throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid))
odE)
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>?R18 a0 a1 as' asid vref\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>?R'18 a0 a1 as' asid vref\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> (?P18 a0 a1 as' asid vref and ?Q18 a0 a1 as' asid vref) s
 6. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (?P'18 a0 a1 as' asid vref and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (6 subgoals):
 1. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> corres (lfr \<oplus> ?r'18 a0 a1 as' asid vref) (?P18 a0 a1 as' asid vref) (?P'18 a0 a1 as' asid vref) (find_pd_for_asid asid) (findPDForASID asid)
 2. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); ?r'18 a0 a1 as' asid vref pd pda\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (?R18 a0 a1 as' asid vref pd) (?R'18 a0 a1 as' asid vref pda) (doE y <- whenE (a1 \<le> a0) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE) (doE y <- whenE (a1 \<le> a0) (throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid))
odE)
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>?R18 a0 a1 as' asid vref\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>?R'18 a0 a1 as' asid vref\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> (?P18 a0 a1 as' asid vref and ?Q18 a0 a1 as' asid vref) s
 6. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (?P'18 a0 a1 as' asid vref and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (5 subgoals):
 1. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (?R18 a0 a1 as' asid vref pd) (?R'18 a0 a1 as' asid vref pda) (doE y <- whenE (a1 \<le> a0) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE) (doE y <- whenE (a1 \<le> a0) (throwError (Fault_H.syscall_error.InvalidArgument (Suc 0)));
y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid))
odE)
 2. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>?R18 a0 a1 as' asid vref\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>?R'18 a0 a1 as' asid vref\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q18 a0 a1 as' asid vref) s
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (6 subgoals):
 1. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda\<rbrakk> \<Longrightarrow> (a1 \<le> a0) = (a1 \<le> a0)
 2. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda; \<not> a1 \<le> a0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (?Q29 a0 a1 as' asid vref pd) (?Q'31 a0 a1 as' asid vref pda) (doE y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE) (doE y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid))
odE)
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>\<lambda>pd s. \<not> a1 \<le> a0 \<longrightarrow> ?Q29 a0 a1 as' asid vref pd s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>\<lambda>pda s. \<not> a1 \<le> a0 \<longrightarrow> ?Q'31 a0 a1 as' asid vref pda s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q18 a0 a1 as' asid vref) s
 6. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (5 subgoals):
 1. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda; \<not> a1 \<le> a0\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (?Q29 a0 a1 as' asid vref pd) (?Q'31 a0 a1 as' asid vref pda) (doE y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (ExceptionTypes_A.syscall_error.InvalidArgument 0));
returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))
odE) (doE y <- whenE (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) (throwError (Fault_H.syscall_error.InvalidArgument 0));
returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid))
odE)
 2. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>\<lambda>pd s. \<not> a1 \<le> a0 \<longrightarrow> ?Q29 a0 a1 as' asid vref pd s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>\<lambda>pda s. \<not> a1 \<le> a0 \<longrightarrow> ?Q'31 a0 a1 as' asid vref pda s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q18 a0 a1 as' asid vref) s
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (6 subgoals):
 1. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda; \<not> a1 \<le> a0\<rbrakk> \<Longrightarrow> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) = (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1)
 2. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda; \<not> a1 \<le> a0; \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (?Q37 a0 a1 as' asid vref pd) (?Q'39 a0 a1 as' asid vref pda) (returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))) (returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid)))
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>\<lambda>pd s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> ?Q37 a0 a1 as' asid vref pd s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>\<lambda>pda s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> ?Q'39 a0 a1 as' asid vref pda s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q18 a0 a1 as' asid vref) s
 6. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (5 subgoals):
 1. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda; \<not> a1 \<le> a0; \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (?Q37 a0 a1 as' asid vref pd) (?Q'39 a0 a1 as' asid vref pda) (returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))) (returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid)))
 2. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>\<lambda>pd s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> ?Q37 a0 a1 as' asid vref pd s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>\<lambda>pda s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> ?Q'39 a0 a1 as' asid vref pda s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q18 a0 a1 as' asid vref) s
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (5 subgoals):
 1. \<And>a0 a1 as' asid vref pd pda. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda; \<not> a1 \<le> a0; \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> archinv_relation) (\<lambda>s. True) (\<lambda>s. True) (returnOk (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid))) (returnOk (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid)))
 2. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>\<lambda>pd s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>\<lambda>pda s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q18 a0 a1 as' asid vref) s
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (5 subgoals):
 1. \<And>a0 a1 as' asid vref pd pda s s'. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); pd = pda; \<not> a1 \<le> a0; \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1); (s, s') \<in> state_relation; True; True\<rbrakk> \<Longrightarrow> archinv_relation (arch_invocation.InvokePage (ARM_A.PageFlush (label_to_flush_type (invocation_type (mi_label mi))) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pd asid)) (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType (mi_label mi)) (a0 + vref) (a1 + vref - 1) (addrFromPPtr word + a0) pda asid))
 2. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>\<lambda>pd s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>\<lambda>pda s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q18 a0 a1 as' asid vref) s
 5. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (4 subgoals):
 1. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 a0 a1 as' asid vref\<rbrace> lookup_error_on_failure False (find_pd_for_asid asid) \<lbrace>\<lambda>pd s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>a0 a1 as' asid vref. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 a0 a1 as' asid vref\<rbrace> lookupErrorOnFailure False (findPDForASID asid) \<lbrace>\<lambda>pda s. \<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q18 a0 a1 as' asid vref) s
 4. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'18 a0 a1 as' asid vref) s proof (prove)
goal (2 subgoals):
 1. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref)))) and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageCap d word seta vmpage_size (Some (asid, vref))))) slot and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>_. True) (snd x) s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid (?pd25 a0 a1 as' asid vref) s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. True \<and> (\<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True))) s
 2. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> (\<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True))) s proof (prove)
goal (1 subgoal):
 1. \<And>a0 a1 as' asid vref s. \<lbrakk>isPageFlushLabel (invocation_type (mi_label mi)); args = a0 # a1 # as'; option = Some (asid, vref); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word (vmrights_map seta) vmpage_size (Some (asid, vref)))) and (\<lambda>s. \<forall>x\<in>set excaps'. valid_cap' (fst x) s \<and> cte_wp_at' (\<lambda>_. True) (snd x) s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> (\<not> a1 \<le> a0 \<longrightarrow> \<not> (2 ^ pageBitsForSize vmpage_size \<le> a0 \<or> 2 ^ pageBitsForSize vmpage_size < a1) \<longrightarrow> True))) s proof (prove)
goal:
No subgoals!