theory Arch_R

lemma get_master_pte_wp:
  "\<lbrace> \<lambda>s. (\<forall>pt pt_slot'. ko_at (ArchObj (PageTable pt)) (pt_slot && ~~ mask pt_bits) s
        \<and> pt_slot' && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits
            \<longrightarrow> Q (pt (ucast (pt_slot' && mask pt_bits >> 2))) s)  \<rbrace>
    get_master_pte pt_slot \<lbrace> Q \<rbrace>" apply (simp add: get_master_pte_def) apply (wp get_pte_wp | wpc)+ apply clarsimp apply (drule spec, drule_tac x="pt_slot && ~~ mask 6" in spec) apply (cut_tac max.absorb2[where a=6 and b=pt_bits]) apply (simp add: word_bw_assocs neg_mask_combine obj_at_def) apply fastforce apply (simp add: pt_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pt pt_slot'. ako_at (PageTable pt) (pt_slot && ~~ mask pt_bits) s \<and> pt_slot' && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrace> get_master_pte pt_slot \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pt pt_slot'. ako_at (PageTable pt) (pt_slot && ~~ mask pt_bits) s \<and> pt_slot' && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrace> do pte <- get_pte (pt_slot && ~~ mask 6);
case pte of ARM_A.LargePagePTE x xa xb \<Rightarrow> return pte | _ \<Rightarrow> get_pte pt_slot
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>pt pt_slot'. ako_at (PageTable pt) (pt_slot && ~~ mask pt_bits) s \<and> pt_slot' && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) ((pt_slot && ~~ mask 6) && ~~ mask pt_bits) s \<longrightarrow> (pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.InvalidPTE \<longrightarrow> (\<forall>pt. ako_at (PageTable pt) (pt_slot && ~~ mask pt_bits) s \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (pt_slot && mask pt_bits >> 2))) s)) \<and> (\<forall>x xa xb. pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2))) s) \<and> (\<forall>x xa xb. pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb \<longrightarrow> (\<forall>pt. ako_at (PageTable pt) (pt_slot && ~~ mask pt_bits) s \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (pt_slot && mask pt_bits >> 2))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s pt x xa xb. \<lbrakk>\<forall>pt pt_slot'. ako_at (PageTable pt) (pt_slot && ~~ mask pt_bits) s \<and> pt_slot' && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; ako_at (PageTable pt) ((pt_slot && ~~ mask 6) && ~~ mask pt_bits) s; pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb\<rbrakk> \<Longrightarrow> Q (ARM_A.LargePagePTE x xa xb) s proof (prove)
goal (1 subgoal):
 1. \<And>s pt x xa xb. \<lbrakk>ako_at (PageTable pt) ((pt_slot && ~~ mask 6) && ~~ mask pt_bits) s; pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb; ako_at (PageTable (?pt40 s pt x xa xb)) (pt_slot && ~~ mask pt_bits) s \<and> (pt_slot && ~~ mask 6) && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (?pt40 s pt x xa xb (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> Q (ARM_A.LargePagePTE x xa xb) s proof (prove)
goal (2 subgoals):
 1. \<And>s pt x xa xb. \<lbrakk>ako_at (PageTable pt) ((pt_slot && ~~ mask 6) && ~~ mask pt_bits) s; pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb; ako_at (PageTable (?pt40 s pt x xa xb)) (pt_slot && ~~ mask pt_bits) s \<and> (pt_slot && ~~ mask 6) && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (?pt40 s pt x xa xb (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2))) s; max 6 pt_bits = pt_bits\<rbrakk> \<Longrightarrow> Q (ARM_A.LargePagePTE x xa xb) s
 2. \<And>s pt x xa xb. \<lbrakk>ako_at (PageTable pt) ((pt_slot && ~~ mask 6) && ~~ mask pt_bits) s; pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb; ako_at (PageTable (?pt40 s pt x xa xb)) (pt_slot && ~~ mask pt_bits) s \<and> (pt_slot && ~~ mask 6) && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (?pt40 s pt x xa xb (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> 6 \<le> pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>s pt x xa xb. \<lbrakk>kheap s (pt_slot && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt (UCAST(32 \<rightarrow> 8) (pt_slot && ~~ mask 6 && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb; ?pt40 s pt x xa xb = pt \<longrightarrow> Q (?pt40 s pt x xa xb (UCAST(32 \<rightarrow> 8) (pt_slot && ~~ mask 6 && mask pt_bits >> 2))) s; max 6 pt_bits = pt_bits\<rbrakk> \<Longrightarrow> Q (ARM_A.LargePagePTE x xa xb) s
 2. \<And>s pt x xa xb. \<lbrakk>ako_at (PageTable pt) ((pt_slot && ~~ mask 6) && ~~ mask pt_bits) s; pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb; ako_at (PageTable (?pt40 s pt x xa xb)) (pt_slot && ~~ mask pt_bits) s \<and> (pt_slot && ~~ mask 6) && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (?pt40 s pt x xa xb (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> 6 \<le> pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>s pt x xa xb. \<lbrakk>ako_at (PageTable pt) ((pt_slot && ~~ mask 6) && ~~ mask pt_bits) s; pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb; ako_at (PageTable pt) (pt_slot && ~~ mask pt_bits) s \<and> (pt_slot && ~~ mask 6) && ~~ mask pt_bits = pt_slot && ~~ mask pt_bits \<longrightarrow> Q (pt (UCAST(32 \<rightarrow> 8) ((pt_slot && ~~ mask 6) && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> 6 \<le> pt_bits proof (prove)
goal:
No subgoals!