theory Arch_DP

lemma decode_page_table_rv:
  "\<lbrace>Q (InvokePageTable
               (PageTableMap (PageTableCap ptr Real (get_mapped_asid (cap_asid (fst pd_cap_slot)) (vaddr && ~~ mask 20)))
                 (PageTableCap ptr Fake None) ref
                 (cdl_lookup_pd_slot (cap_object (fst pd_cap_slot)) vaddr))) \<rbrace>
  decode_invocation (PageTableCap ptr b asid) ref  [pd_cap_slot]
  (PageTableIntent (PageTableMapIntent vaddr vmattribs))
  \<lbrace>Q\<rbrace>, -" apply (case_tac pd_cap_slot) apply (simp add:decode_invocation_def get_page_table_intent_def
    throw_opt_def decode_page_table_invocation_def) apply (rule hoare_pre) apply (wp throw_on_none_wp | wpc | simp)+ apply (clarsimp split:option.splits simp:get_index_def cap_object_def
    cap_has_object_def get_mapped_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q (InvokePageTable (PageTableMap (PageTableCap ptr Real (get_mapped_asid (cap_asid (fst pd_cap_slot)) (vaddr && ~~ mask 20))) (PageTableCap ptr Fake None) ref (cdl_lookup_pd_slot (cap_object (fst pd_cap_slot)) vaddr)))\<rbrace> decode_invocation (PageTableCap ptr b asid) ref [pd_cap_slot] (PageTableIntent (PageTableMapIntent vaddr vmattribs)) \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a ba c. pd_cap_slot = (a, ba, c) \<Longrightarrow> \<lbrace>Q (InvokePageTable (PageTableMap (PageTableCap ptr Real (get_mapped_asid (cap_asid (fst pd_cap_slot)) (vaddr && ~~ mask 20))) (PageTableCap ptr Fake None) ref (cdl_lookup_pd_slot (cap_object (fst pd_cap_slot)) vaddr)))\<rbrace> decode_invocation (PageTableCap ptr b asid) ref [pd_cap_slot] (PageTableIntent (PageTableMapIntent vaddr vmattribs)) \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a ba c. pd_cap_slot = (a, ba, c) \<Longrightarrow> \<lbrace>Q (InvokePageTable (PageTableMap (PageTableCap ptr Real (get_mapped_asid (cap_asid a) (vaddr && ~~ mask 20))) (PageTableCap ptr Fake None) ref (cdl_lookup_pd_slot (cap_object a) vaddr)))\<rbrace> liftME InvokePageTable (doE y <- case cdl_get_pt_mapped_addr (PageTableCap ptr b asid) of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throw;
pd <- throw_on_none (get_index [(a, ba, c)] 0);
(pd_object_id, asid) <- case fst pd of PageDirectoryCap x xa None \<Rightarrow> throw | PageDirectoryCap x xa (Some asid) \<Rightarrow> returnOk (x, asid) | _ \<Rightarrow> throw;
returnOk (PageTableMap (PageTableCap ptr Real (Some (asid, vaddr && ~~ mask 20))) (PageTableCap ptr Fake None) ref (cdl_lookup_pd_slot pd_object_id vaddr))
odE \<sqinter> throw) \<lbrace>Q\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>a ba c. pd_cap_slot = (a, ba, c) \<Longrightarrow> \<lbrace>?P'1 a ba c\<rbrace> liftME InvokePageTable (doE y <- case cdl_get_pt_mapped_addr (PageTableCap ptr b asid) of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throw;
pd <- throw_on_none (get_index [(a, ba, c)] 0);
(pd_object_id, asid) <- case fst pd of PageDirectoryCap x xa None \<Rightarrow> throw | PageDirectoryCap x xa (Some asid) \<Rightarrow> returnOk (x, asid) | _ \<Rightarrow> throw;
returnOk (PageTableMap (PageTableCap ptr Real (Some (asid, vaddr && ~~ mask 20))) (PageTableCap ptr Fake None) ref (cdl_lookup_pd_slot pd_object_id vaddr))
odE \<sqinter> throw) \<lbrace>Q\<rbrace>, -
 2. \<And>a b c s. \<lbrakk>pd_cap_slot = (a, b, c); Q (InvokePageTable (PageTableMap (PageTableCap ptr Real (get_mapped_asid (cap_asid a) (vaddr && ~~ mask 20))) (PageTableCap ptr Fake None) ref (cdl_lookup_pd_slot (cap_object a) vaddr))) s\<rbrakk> \<Longrightarrow> ?P'1 a b c s proof (prove)
goal (1 subgoal):
 1. \<And>a ba c s. \<lbrakk>pd_cap_slot = (a, ba, c); Q (InvokePageTable (PageTableMap (PageTableCap ptr Real (get_mapped_asid (cap_asid a) (vaddr && ~~ mask 20))) (PageTableCap ptr Fake None) ref (cdl_lookup_pd_slot (cap_object a) vaddr))) s\<rbrakk> \<Longrightarrow> cdl_get_pt_mapped_addr (PageTableCap ptr b asid) = None \<longrightarrow> (case get_index [(a, ba, c)] 0 of None \<Rightarrow> True | Some y \<Rightarrow> True \<and> (fst y = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb. fst y = UntypedCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. fst y = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. fst y = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa. fst y = ReplyCap x xa \<longrightarrow> True) \<and> (\<forall>x. fst y = MasterReplyCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc. fst y = CNodeCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. fst y = TcbCap x \<longrightarrow> True) \<and> (fst y = DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. fst y = PendingSyncSendCap x xa xb xc xd xe \<longrightarrow> True) \<and> (\<forall>x xa xb. fst y = PendingSyncRecvCap x xa xb \<longrightarrow> True) \<and> (\<forall>x. fst y = PendingNtfnRecvCap x \<longrightarrow> True) \<and> (fst y = RestartCap \<longrightarrow> True) \<and> (fst y = RunningCap \<longrightarrow> True) \<and> (fst y = IrqControlCap \<longrightarrow> True) \<and> (\<forall>x. fst y = IrqHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. fst y = FrameCap x xa xb xc xd xe \<longrightarrow> True) \<and> (\<forall>x xa xb. fst y = PageTableCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. fst y = PageDirectoryCap x xa xb \<longrightarrow> (xb = None \<longrightarrow> True) \<and> (\<forall>xa. xb = Some xa \<longrightarrow> (\<forall>xb xc. (x, xa) = (xb, xc) \<longrightarrow> (Q \<circ> InvokePageTable) (PageTableMap (PageTableCap ptr Real (Some (xc, vaddr && ~~ mask 20))) (PageTableCap ptr Fake None) ref (cdl_lookup_pd_slot xb vaddr)) s))) \<and> (fst y = AsidControlCap \<longrightarrow> True) \<and> (\<forall>x xa. fst y = AsidPoolCap x xa \<longrightarrow> True) \<and> (\<forall>x xa. fst y = IOPortsCap x xa \<longrightarrow> True) \<and> (fst y = IOSpaceMasterCap \<longrightarrow> True) \<and> (\<forall>x. fst y = IOSpaceCap x \<longrightarrow> True) \<and> (\<forall>x. fst y = IOPageTableCap x \<longrightarrow> True) \<and> (\<forall>x. fst y = ZombieCap x \<longrightarrow> True) \<and> (\<forall>x. fst y = BoundNotificationCap x \<longrightarrow> True)) proof (prove)
goal:
No subgoals!