theory ArchVSpace_AI

lemma find_pd_for_asid_lookup_slot_large_page [wp]:
  "\<lbrace>pspace_aligned and valid_vspace_objs and K (x \<in> set [0, 4 .e. 0x3C] \<and> is_aligned vptr 24)\<rbrace>
  find_pd_for_asid asid
  \<lbrace>\<lambda>rv. \<exists>\<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)\<rbrace>, -" apply (rule hoare_pre) apply (rule hoare_post_imp_R) apply (rule hoare_vcg_R_conj) apply (rule hoare_vcg_R_conj) apply (rule find_pd_for_asid_inv [where P="K (x \<in> set [0, 4 .e. 0x3C] \<and> is_aligned vptr 24)", THEN valid_validE_R]) apply (rule find_pd_for_asid_lookup) apply (rule find_pd_for_asid_aligned_pd) apply (subst lookup_pd_slot_add_eq) apply (simp_all add: pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. \<exists>ref. (ref \<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. \<exists>ref. (ref \<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)) s\<rbrace>, -
 2. \<And>s. (pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace> find_pd_for_asid asid \<lbrace>?Q'3\<rbrace>, -
 2. \<And>rv s. ?Q'3 rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 3. \<And>s. (pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P6\<rbrace> find_pd_for_asid asid \<lbrace>?Q6\<rbrace>, -
 2. \<lbrace>?P'6\<rbrace> find_pd_for_asid asid \<lbrace>?Q'6\<rbrace>, -
 3. \<And>rv s. ?Q6 rv s \<and> ?Q'6 rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 4. \<And>s. (pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)) s \<Longrightarrow> ?P6 s \<and> ?P'6 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P9\<rbrace> find_pd_for_asid asid \<lbrace>?Q9\<rbrace>, -
 2. \<lbrace>?P'9\<rbrace> find_pd_for_asid asid \<lbrace>?Q'9\<rbrace>, -
 3. \<lbrace>?P'6\<rbrace> find_pd_for_asid asid \<lbrace>?Q'6\<rbrace>, -
 4. \<And>rv s. (?Q9 rv s \<and> ?Q'9 rv s) \<and> ?Q'6 rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 5. \<And>s. (pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)) s \<Longrightarrow> (?P9 s \<and> ?P'9 s) \<and> ?P'6 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'9\<rbrace> find_pd_for_asid asid \<lbrace>?Q'9\<rbrace>, -
 2. \<lbrace>?P'6\<rbrace> find_pd_for_asid asid \<lbrace>?Q'6\<rbrace>, -
 3. \<And>rv s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> ?Q'9 rv s) \<and> ?Q'6 rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 4. \<And>s. (pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)) s \<Longrightarrow> (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> ?P'9 s) \<and> ?P'6 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'6\<rbrace> find_pd_for_asid asid \<lbrace>?Q'6\<rbrace>, -
 2. \<And>rv s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> (\<exists>ref. (ref \<rhd> rv) s)) \<and> ?Q'6 rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 3. \<And>s. (pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)) s \<Longrightarrow> (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> True) \<and> ?P'6 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> (\<exists>ref. (ref \<rhd> rv) s)) \<and> is_aligned rv 14 \<Longrightarrow> \<exists>ref. (ref \<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)) s
 2. \<And>s. (pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)) s \<Longrightarrow> (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> True) \<and> (pspace_aligned and valid_vspace_objs) s proof (prove)
goal (5 subgoals):
 1. \<And>rv s ref. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> (\<exists>ref. (ref \<rhd> rv) s)) \<and> is_aligned rv 14 \<Longrightarrow> is_aligned rv pd_bits
 2. \<And>rv s ref. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> (\<exists>ref. (ref \<rhd> rv) s)) \<and> is_aligned rv 14 \<Longrightarrow> is_aligned vptr 24
 3. \<And>rv s ref. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> (\<exists>ref. (ref \<rhd> rv) s)) \<and> is_aligned rv 14 \<Longrightarrow> x \<in> set [0 , 4 .e. 0x3C]
 4. \<And>rv s. (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> (\<exists>ref. (ref \<rhd> rv) s)) \<and> is_aligned rv 14 \<Longrightarrow> \<exists>ref. (ref \<rhd> rv) s
 5. \<And>s. (pspace_aligned and valid_vspace_objs and K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24)) s \<Longrightarrow> (K (x \<in> set [0 , 4 .e. 0x3C] \<and> is_aligned vptr 24) s \<and> True) \<and> (pspace_aligned and valid_vspace_objs) s proof (prove)
goal:
No subgoals!