theory ArchArch_IF

lemma mapM_x_swp_store_pte_reads_respects':
  "reads_respects aag l (invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot
                              and K (is_subject aag word))
                  (mapM_x (swp store_pte InvalidPTE) [word , word + 4 .e. word + 2 ^ pt_bits - 1])" apply (rule gen_asm_ev) apply (wp mapM_x_ev) apply simp apply (rule equiv_valid_guard_imp) apply (wp store_pte_reads_respects) apply simp apply (elim conjE) apply (subgoal_tac "is_aligned word pt_bits") apply (frule (1) word_aligned_pt_slots) apply simp apply (frule cte_wp_valid_cap) apply (rule invs_valid_objs) apply simp apply (simp add: valid_cap_def cap_aligned_def pt_bits_def pageBits_def) apply simp apply wp apply simp apply (fastforce simp: is_cap_simps dest!: cte_wp_at_pt_exists_cap[OF invs_valid_objs]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot and K (is_subject aag word)) (mapM_x (swp store_pte InvalidPTE) [word , word + 4 .e. word + 2 ^ pt_bits - 1]) proof (prove)
goal (1 subgoal):
 1. is_subject aag word \<Longrightarrow> reads_respects aag l (invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot) (mapM_x (swp store_pte InvalidPTE) [word , word + 4 .e. word + 2 ^ pt_bits - 1]) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> reads_respects aag l (invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot) (swp store_pte InvalidPTE x)
 2. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> reads_respects aag l (invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot) (store_pte x InvalidPTE)
 2. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q3 x) (store_pte x InvalidPTE)
 2. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; (invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot) s\<rbrakk> \<Longrightarrow> ?Q3 x s
 3. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; (invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot) s\<rbrakk> \<Longrightarrow> K (is_subject aag (x && ~~ mask pt_bits)) s
 2. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s \<and> cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s\<rbrakk> \<Longrightarrow> is_subject aag (x && ~~ mask pt_bits)
 2. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s\<rbrakk> \<Longrightarrow> is_subject aag (x && ~~ mask pt_bits)
 2. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; is_aligned word pt_bits\<rbrakk> \<Longrightarrow> is_subject aag (x && ~~ mask pt_bits)
 2. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s\<rbrakk> \<Longrightarrow> is_aligned word pt_bits
 3. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; is_aligned word pt_bits; x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> is_subject aag (x && ~~ mask pt_bits)
 2. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s\<rbrakk> \<Longrightarrow> is_aligned word pt_bits
 3. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s\<rbrakk> \<Longrightarrow> is_aligned word pt_bits
 2. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; s \<turnstile> ArchObjectCap (PageTableCap word option)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits
 3. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s\<rbrakk> \<Longrightarrow> invs s
 2. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; s \<turnstile> ArchObjectCap (PageTableCap word option)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits
 3. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; s \<turnstile> ArchObjectCap (PageTableCap word option)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits
 2. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> swp store_pte InvalidPTE x \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> store_pte x InvalidPTE \<lbrace>\<lambda>_. invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; (invs and cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. (\<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte InvalidPTE s) and (\<lambda>s. wellformed_pte InvalidPTE) and (\<lambda>s. \<exists>slot asid. caps_of_state s slot = Some (ArchObjectCap (PageTableCap (x && ~~ mask pt_bits) asid)) \<and> (InvalidPTE = InvalidPTE \<or> asid \<noteq> None)) and (\<lambda>s. \<forall>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages InvalidPTE = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (x && mask pt_bits >> 2) (Some APageTable) # ref))))) s \<and> cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>is_subject aag word; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; invs s \<and> cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s\<rbrakk> \<Longrightarrow> \<exists>a b asid. caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap (x && ~~ mask pt_bits) asid)) proof (prove)
goal:
No subgoals!