theory ArchArch_IF

lemma mapM_x_swp_store_pde_reads_respects':
  "reads_respects aag l
     (cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs
                                                                    and K (is_subject aag w))
     (mapM_x (swp store_pde InvalidPDE)
             (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]))" apply (wp mapM_x_ev) apply simp apply (rule equiv_valid_guard_imp) apply (wp store_pde_reads_respects) apply clarsimp apply (subgoal_tac "is_aligned w pd_bits") apply (simp add: pd_bits_store_pde_helper) apply (frule (1) cte_wp_valid_cap) apply (simp add: valid_cap_def cap_aligned_def pd_bits_def pageBits_def) apply simp apply wp apply (clarsimp simp: wellformed_pde_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)) (mapM_x (swp store_pde InvalidPDE) (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1])) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> reads_respects aag l (cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)) (swp store_pde InvalidPDE x)
 2. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> (\<lambda>x. (x << 2) + w) ` {x. x \<le> (kernel_base >> 20) - 1} \<Longrightarrow> reads_respects aag l (cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and (\<lambda>y. is_subject aag w)) (store_pde x InvalidPDE)
 2. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> (\<lambda>x. (x << 2) + w) ` {x. x \<le> (kernel_base >> 20) - 1} \<Longrightarrow> reads_respects aag l (?Q6 x) (store_pde x InvalidPDE)
 2. \<And>x s. \<lbrakk>x \<in> (\<lambda>x. (x << 2) + w) ` {x. x \<le> (kernel_base >> 20) - 1}; (cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and (\<lambda>y. is_subject aag w)) s\<rbrakk> \<Longrightarrow> ?Q6 x s
 3. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> (\<lambda>x. (x << 2) + w) ` {x. x \<le> (kernel_base >> 20) - 1}; (cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and (\<lambda>y. is_subject aag w)) s\<rbrakk> \<Longrightarrow> K (is_subject aag (x && ~~ mask pd_bits)) s
 2. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s xa. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot s; valid_objs s; is_subject aag w\<rbrakk> \<Longrightarrow> is_subject aag ((xa << 2) + w && ~~ mask pd_bits)
 2. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s xa. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot s; valid_objs s; is_subject aag w; is_aligned w pd_bits\<rbrakk> \<Longrightarrow> is_subject aag ((xa << 2) + w && ~~ mask pd_bits)
 2. \<And>s xa. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot s; valid_objs s; is_subject aag w\<rbrakk> \<Longrightarrow> is_aligned w pd_bits
 3. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s xa. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot s; valid_objs s; is_subject aag w\<rbrakk> \<Longrightarrow> is_aligned w pd_bits
 2. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s xa. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot s; valid_objs s; is_subject aag w; s \<turnstile> ArchObjectCap (PageDirectoryCap w opt)\<rbrakk> \<Longrightarrow> is_aligned w pd_bits
 2. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (map ((\<lambda>x. x + w) \<circ> swp (<<) 2) [0 .e. (kernel_base >> 20) - 1]) \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> swp store_pde InvalidPDE x \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and K (is_subject aag w)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>x. (x << 2) + w) ` {x. x \<le> (kernel_base >> 20) - 1} \<Longrightarrow> \<lbrace>cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and (\<lambda>y. is_subject aag w)\<rbrace> store_pde x InvalidPDE \<lbrace>\<lambda>_. cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and (\<lambda>y. is_subject aag w)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>x \<in> (\<lambda>x. (x << 2) + w) ` {x. x \<le> (kernel_base >> 20) - 1}; (cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot and valid_objs and (\<lambda>y. is_subject aag w)) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap w opt))) slot s \<and> ((\<lambda>s. wellformed_pde InvalidPDE) and valid_objs) s \<and> is_subject aag w proof (prove)
goal:
No subgoals!