theory Arch_DP

lemma decode_page_map_intent_rv_20_24:
  "\<lbrakk>n = 20 \<or> n = 24 \<rbrakk>
  \<Longrightarrow> \<lbrace>\<lambda>s. R (InvokePage (PageMap (FrameCap dev frame_ptr rights n Real (get_mapped_asid asid' vaddr))
         (FrameCap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n Fake None) ref [cdl_lookup_pd_slot ptr vaddr])) \<rbrace>
  decode_invocation (FrameCap dev frame_ptr rights n real_type asid) ref
  [(PageDirectoryCap ptr real' asid',pdref)]
  (PageIntent (PageMapIntent vaddr perms vmattr))
  \<lbrace>\<lambda>r s. R r\<rbrace>, -" apply (simp add: decode_invocation_def get_index_def get_page_intent_def throw_opt_def
                   cap_rights_def decode_page_invocation_def throw_on_none_def get_mapped_asid_def) apply (wp | wpc)+ apply (rule validE_validE_R) apply wp apply (simp add:cdl_page_mapping_entries_def split del:if_split | wp | wpc)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = 20 \<or> n = 24 \<Longrightarrow> \<lbrace>\<lambda>s. R (InvokePage (PageMap (FrameCap dev frame_ptr rights n Real (get_mapped_asid asid' vaddr)) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref [cdl_lookup_pd_slot ptr vaddr]))\<rbrace> decode_invocation (FrameCap dev frame_ptr rights n real_type asid) ref [(PageDirectoryCap ptr real' asid', pdref)] (PageIntent (PageMapIntent vaddr perms vmattr)) \<lbrace>\<lambda>r s. R r\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. n = 20 \<or> n = 24 \<Longrightarrow> \<lbrace>\<lambda>s. R (InvokePage (PageMap (FrameCap dev frame_ptr rights n Real (map_option (\<lambda>x. (x, vaddr)) asid')) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref [cdl_lookup_pd_slot ptr vaddr]))\<rbrace> liftME InvokePage (doE (pd_object_id, asid) <- case asid' of None \<Rightarrow> throw | Some asid \<Rightarrow> returnOk (ptr, asid);
target_slots <- cdl_page_mapping_entries vaddr n pd_object_id;
returnOk (PageMap (FrameCap dev frame_ptr rights n Real (Some (asid, vaddr))) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref target_slots)
odE \<sqinter> throw) \<lbrace>\<lambda>r s. R r\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>x x1 x2. \<lbrakk>n = 20 \<or> n = 24; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 x x1 x2\<rbrace> cdl_page_mapping_entries vaddr n x1 \<lbrace>\<lambda>target_slots. ((\<lambda>r s. R r) \<circ> InvokePage) (PageMap (FrameCap dev frame_ptr rights n Real (Some (x2, vaddr))) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref target_slots)\<rbrace>, -
 2. n = 20 \<or> n = 24 \<Longrightarrow> \<lbrace>?P'7\<rbrace> case asid' of None \<Rightarrow> throw | Some asid \<Rightarrow> returnOk (ptr, asid) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> True \<and> ?P'22 x xa xb s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. n = 20 \<or> n = 24 \<Longrightarrow> \<lbrace>?P'6\<rbrace> throw \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>n = 20 \<or> n = 24; R (InvokePage (PageMap (FrameCap dev frame_ptr rights n Real (map_option (\<lambda>x. (x, vaddr)) asid')) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref [cdl_lookup_pd_slot ptr vaddr]))\<rbrakk> \<Longrightarrow> ((\<lambda>s. True \<and> ?P'7 s) and ?P'6) s proof (prove)
goal (4 subgoals):
 1. \<And>x x1 x2. \<lbrakk>n = 20 \<or> n = 24; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 x x1 x2\<rbrace> cdl_page_mapping_entries vaddr n x1 \<lbrace>\<lambda>target_slots. ((\<lambda>r s. R r) \<circ> InvokePage) (PageMap (FrameCap dev frame_ptr rights n Real (Some (x2, vaddr))) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref target_slots)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. n = 20 \<or> n = 24 \<Longrightarrow> \<lbrace>?P'7\<rbrace> case asid' of None \<Rightarrow> throw | Some asid \<Rightarrow> returnOk (ptr, asid) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> True \<and> ?P'22 x xa xb s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. n = 20 \<or> n = 24 \<Longrightarrow> \<lbrace>?P'6\<rbrace> throw \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>n = 20 \<or> n = 24; R (InvokePage (PageMap (FrameCap dev frame_ptr rights n Real (map_option (\<lambda>x. (x, vaddr)) asid')) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref [cdl_lookup_pd_slot ptr vaddr]))\<rbrakk> \<Longrightarrow> ((\<lambda>s. True \<and> ?P'7 s) and ?P'6) s proof (prove)
goal (4 subgoals):
 1. \<And>x x1 x2. \<lbrakk>n = 20 \<or> n = 24; x = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?P'28 x x1 x2\<rbrace> cdl_page_mapping_entries vaddr n x1 \<lbrace>\<lambda>target_slots. ((\<lambda>r s. R r) \<circ> InvokePage) (PageMap (FrameCap dev frame_ptr rights n Real (Some (x2, vaddr))) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref target_slots)\<rbrace>, -
 2. n = 20 \<or> n = 24 \<Longrightarrow> \<lbrace>?P'7\<rbrace> case asid' of None \<Rightarrow> throw | Some asid \<Rightarrow> returnOk (ptr, asid) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> True \<and> True \<and> ?P'28 x xa xb s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. n = 20 \<or> n = 24 \<Longrightarrow> \<lbrace>?P'6\<rbrace> throw \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>n = 20 \<or> n = 24; R (InvokePage (PageMap (FrameCap dev frame_ptr rights n Real (map_option (\<lambda>x. (x, vaddr)) asid')) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref [cdl_lookup_pd_slot ptr vaddr]))\<rbrakk> \<Longrightarrow> ((\<lambda>s. True \<and> ?P'7 s) and ?P'6) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>n = 20 \<or> n = 24; R (InvokePage (PageMap (FrameCap dev frame_ptr rights n Real (map_option (\<lambda>x. (x, vaddr)) asid')) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) n) ref [cdl_lookup_pd_slot ptr vaddr]))\<rbrakk> \<Longrightarrow> \<forall>a b. asid' = Some (a, b) \<longrightarrow> (n = 12 \<longrightarrow> ?P'114 a b (ptr, a, b) ptr (a, b) s) \<and> (n \<noteq> 12 \<longrightarrow> (n = 16 \<longrightarrow> ?P'112 a b (ptr, a, b) ptr (a, b) s) \<and> (n \<noteq> 16 \<longrightarrow> (n = 20 \<longrightarrow> R (InvokePage (PageMap (FrameCap dev frame_ptr rights 20 Real (Some ((a, b), vaddr))) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) 20) ref [cdl_lookup_pd_slot ptr vaddr]))) \<and> (n \<noteq> 20 \<longrightarrow> n = 24 \<longrightarrow> R (InvokePage (PageMap (FrameCap dev frame_ptr rights 24 Real (Some ((a, b), vaddr))) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) 24) ref [cdl_lookup_pd_slot ptr vaddr]))))) proof (prove)
goal:
No subgoals!