theory ArchAcc_AI

lemma get_master_pte_wp:
  "\<lbrace>\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s \<longrightarrow>
          Q (case pt (ucast (p && ~~ mask 6 && mask pt_bits >> 2)) of
              LargePagePTE x xa xb \<Rightarrow>
                pt (ucast (p && ~~ mask 6 && mask pt_bits >> 2))
              | _ \<Rightarrow> pt (ucast (p && mask pt_bits >> 2)))
           s\<rbrace>
  get_master_pte p \<lbrace>Q\<rbrace>" apply (simp add: get_master_pte_def) apply (wp get_pte_wp | wpc)+ including pagebits by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (case pt (UCAST(32 \<rightarrow> 8) (p && ~~ mask 6 && mask pt_bits >> 2)) of LargePagePTE x xa xb \<Rightarrow> pt (UCAST(32 \<rightarrow> 8) (p && ~~ mask 6 && mask pt_bits >> 2)) | _ \<Rightarrow> pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s\<rbrace> get_master_pte p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (case pt (UCAST(32 \<rightarrow> 8) (p && ~~ mask 6 && mask pt_bits >> 2)) of LargePagePTE x xa xb \<Rightarrow> pt (UCAST(32 \<rightarrow> 8) (p && ~~ mask 6 && mask pt_bits >> 2)) | _ \<Rightarrow> pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s\<rbrace> do pte <- get_pte (p && ~~ mask 6);
case pte of LargePagePTE x xa xb \<Rightarrow> return pte | _ \<Rightarrow> get_pte p
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (case pt (UCAST(32 \<rightarrow> 8) (p && ~~ mask 6 && mask pt_bits >> 2)) of LargePagePTE x xa xb \<Rightarrow> pt (UCAST(32 \<rightarrow> 8) (p && ~~ mask 6 && mask pt_bits >> 2)) | _ \<Rightarrow> pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) ((p && ~~ mask 6) && ~~ mask pt_bits) s \<longrightarrow> (pt (UCAST(32 \<rightarrow> 8) ((p && ~~ mask 6) && mask pt_bits >> 2)) = InvalidPTE \<longrightarrow> (\<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s)) \<and> (\<forall>x xa xb. pt (UCAST(32 \<rightarrow> 8) ((p && ~~ mask 6) && mask pt_bits >> 2)) = LargePagePTE x xa xb \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) ((p && ~~ mask 6) && mask pt_bits >> 2))) s) \<and> (\<forall>x xa xb. pt (UCAST(32 \<rightarrow> 8) ((p && ~~ mask 6) && mask pt_bits >> 2)) = SmallPagePTE x xa xb \<longrightarrow> (\<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (case pt (UCAST(32 \<rightarrow> 8) (p && ~~ mask 6 && mask pt_bits >> 2)) of LargePagePTE x xa xb \<Rightarrow> pt (UCAST(32 \<rightarrow> 8) (p && ~~ mask 6 && mask pt_bits >> 2)) | _ \<Rightarrow> pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) ((p && ~~ mask 6) && ~~ mask pt_bits) s \<longrightarrow> (pt (UCAST(32 \<rightarrow> 8) ((p && ~~ mask 6) && mask pt_bits >> 2)) = InvalidPTE \<longrightarrow> (\<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s)) \<and> (\<forall>x xa xb. pt (UCAST(32 \<rightarrow> 8) ((p && ~~ mask 6) && mask pt_bits >> 2)) = LargePagePTE x xa xb \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) ((p && ~~ mask 6) && mask pt_bits >> 2))) s) \<and> (\<forall>x xa xb. pt (UCAST(32 \<rightarrow> 8) ((p && ~~ mask 6) && mask pt_bits >> 2)) = SmallPagePTE x xa xb \<longrightarrow> (\<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) s))