theory Arch_R

lemma arch_decodeARMPageFlush_wf:
  "ARM_H.isPageFlushLabel (invocation_type label) \<Longrightarrow>
       \<lbrace>invs' and
        valid_cap'
         (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) and
        cte_wp_at'
         ((=) (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) \<circ>
          cteCap)
         slot and
        (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and
        sch_act_simple and
        (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
       decodeARMPageFlush label args (arch_capability.PageCap d word vmrights vmpage_size option)
       \<lbrace>valid_arch_inv'\<rbrace>, -" apply (simp add: decodeARMPageFlush_def) apply (rule hoare_pre) apply (wp throwE_R whenE_throwError_wp | wpc | clarsimp simp: if_apply_def2)+ apply (simp add: valid_arch_inv'_def valid_page_inv'_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isPageFlushLabel (invocation_type label) \<Longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) and cte_wp_at' ((=) (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) \<circ> cteCap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> decodeARMPageFlush label args (arch_capability.PageCap d word vmrights vmpage_size option) \<lbrace>valid_arch_inv'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. isPageFlushLabel (invocation_type label) \<Longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) and cte_wp_at' ((=) (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) \<circ> cteCap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> 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 vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word vmrights 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 label) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE \<lbrace>valid_arch_inv'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. isPageFlushLabel (invocation_type label) \<Longrightarrow> \<lbrace>?P'\<rbrace> 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 vmpage_size option))));
pageBase <- returnOk (addrFromPPtr $ capVPBasePtr (arch_capability.PageCap d word vmrights 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 label) (VPtr $ start') (VPtr $ end' - 1) pstart pd asid
odE \<lbrace>valid_arch_inv'\<rbrace>, -
 2. \<And>s. \<lbrakk>isPageFlushLabel (invocation_type label); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) and cte_wp_at' ((=) (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) \<circ> cteCap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<And>x21 x21a x22a x1 x2a. \<lbrakk>isPageFlushLabel (invocation_type label); args = x21 # x21a # x22a; option = Some (x1, x2a)\<rbrakk> \<Longrightarrow> \<lbrace>?P'86 x21 (x21a # x22a) x21a x22a (x1, x2a) x1 x2a\<rbrace> findPDForASID x1 \<lbrace>\<lambda>rv s. \<not> x21a \<le> x21 \<longrightarrow> \<not> 2 ^ pageBitsForSize vmpage_size \<le> x21 \<and> \<not> 2 ^ pageBitsForSize vmpage_size < x21a \<longrightarrow> valid_arch_inv' (invocation.InvokePage (ARM_H.PageFlush (labelToFlushType label) (x21 + x2a) (x21a + x2a - 1) (addrFromPPtr word + x21) rv x1)) s\<rbrace>, -
 2. \<And>s. \<lbrakk>isPageFlushLabel (invocation_type label); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) and cte_wp_at' ((=) (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) \<circ> cteCap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> (option = None \<longrightarrow> True) \<and> (\<forall>xd. option = Some xd \<longrightarrow> (\<forall>xe xf. xd = (xe, xf) \<longrightarrow> True \<and> True \<and> ?P'86 x xa xb xc xd xe xf s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>isPageFlushLabel (invocation_type label); (invs' and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) and cte_wp_at' ((=) (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size option)) \<circ> cteCap) slot and (\<lambda>s. \<forall>x\<in>set excaps. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s) and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> (option = None \<longrightarrow> True) \<and> (\<forall>xd. option = Some xd \<longrightarrow> (\<forall>xe xf. xd = (xe, xf) \<longrightarrow> True \<and> True \<and> ?P'86 x xa xb xc xd xe xf s)))) proof (prove)
goal:
No subgoals!