theory VSpace_R

lemma set_cap_valid_page_map_inv:
  "\<lbrace>valid_page_inv (ARM_A.page_invocation.PageMap asid cap slot m)\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv. valid_page_map_inv asid cap slot m\<rbrace>" apply (simp add: valid_page_inv_def valid_page_map_inv_def) apply (wp set_cap_cte_wp_at_cases hoare_vcg_ex_lift| simp)+ apply clarsimp apply (rule conjI, fastforce simp: cte_wp_at_def) apply (rule_tac x=a in exI, rule_tac x=b in exI) apply (subgoal_tac "(a,b) \<noteq> slot") apply clarsimp apply (clarsimp simp: cte_wp_at_def parent_for_refs_def) apply (auto simp: is_pt_cap_def is_pg_cap_def is_pd_cap_def split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_page_inv (ARM_A.PageMap asid cap slot m)\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv. valid_page_map_inv asid cap slot m\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (is_arch_update cap) slot and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) slot or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs m c s) slot s)) and cte_wp_at is_pg_cap slot and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s)\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv. (\<lambda>s. caps_of_state s slot = Some cap) and same_refs m cap and valid_slots m and valid_cap cap and (\<lambda>y. is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (is_arch_update cap) slot s \<and> (cte_wp_at (\<lambda>c. vs_cap_ref c = None) slot s \<or> cte_wp_at (\<lambda>c. same_refs m c s) slot s) \<and> cte_wp_at is_pg_cap slot s \<and> same_refs m cap s \<and> valid_slots m s \<and> s \<turnstile> cap \<and> is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0 \<and> (\<exists>a b. cte_wp_at (parent_for_refs m) (a, b) s) \<and> (\<exists>pd. vspace_at_asid asid pd s) \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s \<and> (\<exists>x xa. ((x, xa) = slot \<longrightarrow> parent_for_refs m cap) \<and> ((x, xa) \<noteq> slot \<longrightarrow> cte_wp_at (parent_for_refs m) (x, xa) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a pd b. \<lbrakk>cte_wp_at (is_arch_update cap) slot s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) slot s \<or> cte_wp_at (\<lambda>c. same_refs m c s) slot s; cte_wp_at is_pg_cap slot s; same_refs m cap s; valid_slots m s; s \<turnstile> cap; is_pg_cap cap; empty_refs m; asid \<le> mask local.asid_bits; asid \<noteq> 0; vspace_at_asid asid pd s; cte_wp_at (parent_for_refs m) (a, b) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s \<and> (\<exists>x xa. ((x, xa) = slot \<longrightarrow> parent_for_refs m cap) \<and> ((x, xa) \<noteq> slot \<longrightarrow> cte_wp_at (parent_for_refs m) (x, xa) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a pd b. \<lbrakk>cte_wp_at (is_arch_update cap) slot s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) slot s \<or> cte_wp_at (\<lambda>c. same_refs m c s) slot s; cte_wp_at is_pg_cap slot s; same_refs m cap s; valid_slots m s; s \<turnstile> cap; is_pg_cap cap; empty_refs m; asid \<le> mask local.asid_bits; asid \<noteq> 0; vspace_at_asid asid pd s; cte_wp_at (parent_for_refs m) (a, b) s\<rbrakk> \<Longrightarrow> \<exists>x xa. ((x, xa) = slot \<longrightarrow> parent_for_refs m cap) \<and> ((x, xa) \<noteq> slot \<longrightarrow> cte_wp_at (parent_for_refs m) (x, xa) s) proof (prove)
goal (1 subgoal):
 1. \<And>s a pd b. \<lbrakk>cte_wp_at (is_arch_update cap) slot s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) slot s \<or> cte_wp_at (\<lambda>c. same_refs m c s) slot s; cte_wp_at is_pg_cap slot s; same_refs m cap s; valid_slots m s; s \<turnstile> cap; is_pg_cap cap; empty_refs m; asid \<le> mask local.asid_bits; asid \<noteq> 0; vspace_at_asid asid pd s; cte_wp_at (parent_for_refs m) (a, b) s\<rbrakk> \<Longrightarrow> ((a, b) = slot \<longrightarrow> parent_for_refs m cap) \<and> ((a, b) \<noteq> slot \<longrightarrow> cte_wp_at (parent_for_refs m) (a, b) s) proof (prove)
goal (2 subgoals):
 1. \<And>s a pd b. \<lbrakk>cte_wp_at (is_arch_update cap) slot s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) slot s \<or> cte_wp_at (\<lambda>c. same_refs m c s) slot s; cte_wp_at is_pg_cap slot s; same_refs m cap s; valid_slots m s; s \<turnstile> cap; is_pg_cap cap; empty_refs m; asid \<le> mask local.asid_bits; asid \<noteq> 0; vspace_at_asid asid pd s; cte_wp_at (parent_for_refs m) (a, b) s; (a, b) \<noteq> slot\<rbrakk> \<Longrightarrow> ((a, b) = slot \<longrightarrow> parent_for_refs m cap) \<and> ((a, b) \<noteq> slot \<longrightarrow> cte_wp_at (parent_for_refs m) (a, b) s)
 2. \<And>s a pd b. \<lbrakk>cte_wp_at (is_arch_update cap) slot s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) slot s \<or> cte_wp_at (\<lambda>c. same_refs m c s) slot s; cte_wp_at is_pg_cap slot s; same_refs m cap s; valid_slots m s; s \<turnstile> cap; is_pg_cap cap; empty_refs m; asid \<le> mask local.asid_bits; asid \<noteq> 0; vspace_at_asid asid pd s; cte_wp_at (parent_for_refs m) (a, b) s\<rbrakk> \<Longrightarrow> (a, b) \<noteq> slot proof (prove)
goal (1 subgoal):
 1. \<And>s a pd b. \<lbrakk>cte_wp_at (is_arch_update cap) slot s; cte_wp_at (\<lambda>c. vs_cap_ref c = None) slot s \<or> cte_wp_at (\<lambda>c. same_refs m c s) slot s; cte_wp_at is_pg_cap slot s; same_refs m cap s; valid_slots m s; s \<turnstile> cap; is_pg_cap cap; empty_refs m; asid \<le> mask local.asid_bits; asid \<noteq> 0; vspace_at_asid asid pd s; cte_wp_at (parent_for_refs m) (a, b) s\<rbrakk> \<Longrightarrow> (a, b) \<noteq> slot proof (prove)
goal (1 subgoal):
 1. \<And>s a pd b capa. \<lbrakk>vs_cap_ref capa = None \<or> same_refs m capa s; same_refs m cap s; valid_slots m s; s \<turnstile> cap; is_pg_cap cap; empty_refs m; asid \<le> mask local.asid_bits; asid \<noteq> 0; vspace_at_asid asid pd s; is_arch_update cap capa; is_pg_cap capa; fst (get_cap (a, b) s) = {(capa, s)}; case m of Inl (xa, slots) \<Rightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs capa \<and> is_pt_cap capa \<and> cap_asid capa \<noteq> None | Inr (xa, slots) \<Rightarrow> (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> obj_refs capa \<and> is_pd_cap capa \<and> cap_asid capa \<noteq> None; slot = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!