theory Arch_DP

lemma decode_page_map_intent_rv_16_12:
  "\<lbrakk>n = 12 \<or> n = 16 \<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
         [(p, unat ((vaddr >> 12) && 0xFF))]))
  \<and> <(ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)> s\<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 apply (rule validE_validE_R) apply wp apply (simp add:cdl_page_mapping_entries_def) apply (wp cdl_lookup_pt_slot_rv | wpc | simp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = 12 \<or> n = 16 \<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 [(p, unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<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 = 12 \<or> n = 16 \<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 [(p, unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<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. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?B9 x\<rbrace> case x of (pd_object_id, asid) \<Rightarrow> doE 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 \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, -
 2. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'7\<rbrace> case asid' of None \<Rightarrow> throw | Some asid \<Rightarrow> returnOk (ptr, asid) \<lbrace>?B9\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'6\<rbrace> throw \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>n = 12 \<or> n = 16; 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 [(p, unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. True \<and> ?P'7 s) and ?P'6) s proof (prove)
goal (4 subgoals):
 1. \<And>x. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?B9 x\<rbrace> case x of (pd_object_id, asid) \<Rightarrow> doE 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 \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'7\<rbrace> case asid' of None \<Rightarrow> throw | Some asid \<Rightarrow> returnOk (ptr, asid) \<lbrace>?B9\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'6\<rbrace> throw \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>n = 12 \<or> n = 16; 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 [(p, unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. True \<and> ?P'7 s) and ?P'6) s proof (prove)
goal (4 subgoals):
 1. \<And>x. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'13 x\<rbrace> case x of (pd_object_id, asid) \<Rightarrow> doE 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 \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, -
 2. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'7\<rbrace> case asid' of None \<Rightarrow> throw | Some asid \<Rightarrow> returnOk (ptr, asid) \<lbrace>\<lambda>x s. True \<and> ?P'13 x s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'6\<rbrace> throw \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>n = 12 \<or> n = 16; 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 [(p, unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. True \<and> ?P'7 s) and ?P'6) s proof (prove)
goal (4 subgoals):
 1. \<And>x. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'13 x\<rbrace> case x of (pd_object_id, asid) \<Rightarrow> doE target_slots <- if n = 12 then doE p <- cdl_lookup_pt_slot pd_object_id vaddr;
returnOk [p]
odE else if n = 16 then doE p <- cdl_lookup_pt_slot pd_object_id vaddr;
returnOk [p]
odE else if n = 20 then doE p <- returnOk $ cdl_lookup_pd_slot pd_object_id vaddr;
returnOk [p]
odE else if n = 24 then doE p <- returnOk $ cdl_lookup_pd_slot pd_object_id vaddr;
returnOk [p]
odE else throw;
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 \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, -
 2. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'7\<rbrace> case asid' of None \<Rightarrow> throw | Some asid \<Rightarrow> returnOk (ptr, asid) \<lbrace>\<lambda>x s. True \<and> ?P'13 x s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. n = 12 \<or> n = 16 \<Longrightarrow> \<lbrace>?P'6\<rbrace> throw \<lbrace>(\<lambda>r s. R r) \<circ> InvokePage\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>n = 12 \<or> n = 16; 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 [(p, unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. True \<and> ?P'7 s) and ?P'6) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>n = 12 \<or> n = 16; 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 [(p, unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap p Fake None \<and>* (\<lambda>s. True)) s\<rbrakk> \<Longrightarrow> \<forall>a b. asid' = Some (a, b) \<longrightarrow> (n = 12 \<longrightarrow> R (InvokePage (PageMap (FrameCap dev frame_ptr rights 12 Real (Some ((a, b), vaddr))) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) 12) ref [(?p43 (ptr, a, b) ptr (a, b), unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap (?p41 (ptr, a, b) ptr (a, b)) Fake None \<and>* (\<lambda>s. True)) s) \<and> (n \<noteq> 12 \<longrightarrow> (n = 16 \<longrightarrow> R (InvokePage (PageMap (FrameCap dev frame_ptr rights 16 Real (Some ((a, b), vaddr))) (fake_frame_cap False frame_ptr (validate_vm_rights (rights \<inter> perms)) 16) ref [(?p59 (ptr, a, b) ptr (a, b), unat ((vaddr >> 12) && 0xFF))])) \<and> cdl.lift ((ptr, unat (vaddr >> 20)) \<mapsto>c PageTableCap (?p57 (ptr, a, b) ptr (a, b)) Fake None \<and>* (\<lambda>s. True)) 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])))))
flex-flex pairs:
\<lambda>x1 x2. ?p59 (x1, x2) x1 x2 \<equiv>\<^sup>? \<lambda>x1 x2. ?p57 (x1, x2) x1 x2
\<lambda>x1 x2. ?p43 (x1, x2) x1 x2 \<equiv>\<^sup>? \<lambda>x1 x2. ?p41 (x1, x2) x1 x2 proof (prove)
goal:
No subgoals!