theory Arch_R

lemma findPDForASID_page_directory_at':
  notes checkPDAt_inv[wp del]
  shows "\<lbrace>\<top>\<rbrace> findPDForASID asiv
    \<lbrace>\<lambda>rv s. page_directory_at' (lookup_pd_slot rv vptr && ~~ mask pdBits) s\<rbrace>,-" apply (simp add:findPDForASID_def) apply (wp getASID_wp|simp add:checkPDAt_def | wpc)+ apply (clarsimp simp:lookup_pd_slot_def pdBits_def pdeBits_def) apply (subst vaddr_segment_nonsense[unfolded pd_bits_def pdeBits_def pageBits_def,simplified]) apply (simp add:page_directory_at'_def pdBits_def pageBits_def pdeBits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> findPDForASID asiv \<lbrace>\<lambda>rv. page_directory_at' (lookup_pd_slot rv vptr && ~~ mask pdBits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE y <- assertE (0 < asiv);
y <- assertE (asiv \<le> snd asidRange);
asidTable <- liftE (gets (armKSASIDTable \<circ> ksArchState));
pool <- liftME (inv asidpool.ASIDPool) (case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asiv)) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> liftE (getObject ptr));
case pool (asiv && mask local.asid_low_bits) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> doE y <- assertE (ptr \<noteq> 0);
y <- liftE (checkPDAt ptr);
returnOk ptr
odE
odE \<lbrace>\<lambda>rv. page_directory_at' (lookup_pd_slot rv vptr && ~~ mask pdBits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. 0 < asiv \<longrightarrow> asiv \<le> snd asidRange \<longrightarrow> (\<forall>x. armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asiv)) = Some x \<longrightarrow> (\<forall>ko. ko_at' ko x s \<longrightarrow> (\<forall>x. inv asidpool.ASIDPool ko (asiv && mask local.asid_low_bits) = Some x \<longrightarrow> x \<noteq> 0 \<longrightarrow> page_directory_at' x s \<longrightarrow> page_directory_at' (lookup_pd_slot x vptr && ~~ mask pdBits) s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x ko xa. \<lbrakk>0 < asiv; asiv \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asiv)) = Some x; ko_at' ko x s; inv asidpool.ASIDPool ko (asiv && mask local.asid_low_bits) = Some xa; xa \<noteq> 0; page_directory_at' xa s\<rbrakk> \<Longrightarrow> page_directory_at' (xa + (vptr >> 20 << 2) && ~~ mask 14) s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko xa. \<lbrakk>0 < asiv; asiv \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asiv)) = Some x; ko_at' ko x s; inv asidpool.ASIDPool ko (asiv && mask local.asid_low_bits) = Some xa; xa \<noteq> 0; page_directory_at' xa s\<rbrakk> \<Longrightarrow> is_aligned xa 14
 2. \<And>s x ko xa. \<lbrakk>0 < asiv; asiv \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asiv)) = Some x; ko_at' ko x s; inv asidpool.ASIDPool ko (asiv && mask local.asid_low_bits) = Some xa; xa \<noteq> 0; page_directory_at' xa s\<rbrakk> \<Longrightarrow> page_directory_at' xa s proof (prove)
goal (1 subgoal):
 1. \<And>s x ko xa. \<lbrakk>0 < asiv; asiv \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asiv)) = Some x; ko_at' ko x s; inv asidpool.ASIDPool ko (asiv && mask local.asid_low_bits) = Some xa; xa \<noteq> 0; page_directory_at' xa s\<rbrakk> \<Longrightarrow> page_directory_at' xa s proof (prove)
goal:
No subgoals!