theory ArchVSpace_AI

lemma lookup_pt_slot_cap_to_multiple2:
  "\<lbrace>invs and \<exists>\<rhd> pd and K (is_aligned pd pd_bits) and K (vptr < kernel_base) and K (is_aligned vptr 16)\<rbrace>
      lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at
              (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c \<and> is_pt_cap c)
                  (oref, cref) s\<rbrace>, -" apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to_multiple1) apply (clarsimp simp: upto_enum_step_def image_image field_simps
                        linorder_not_le[symmetric]
                 split: if_split_asm) apply (erule notE, erule is_aligned_no_wrap') apply simp apply (fastforce simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base) and K (is_aligned vptr 16)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c \<and> is_pt_cap c) (oref, cref) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. is_aligned rv 6 \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s) \<Longrightarrow> \<exists>oref cref. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c \<and> is_pt_cap c) (oref, cref) s proof (prove)
goal (2 subgoals):
 1. \<And>rv s a b. \<lbrakk>\<not> rv \<le> rv + 0x3C; is_aligned rv 6; cte_wp_at (\<lambda>c. is_pt_cap c \<and> (\<exists>y. cap_asid c = Some y)) (a, b) s\<rbrakk> \<Longrightarrow> \<exists>oref cref. cte_wp_at (\<lambda>c. (\<lambda>x. rv + x * 4 && ~~ mask pt_bits) ` {x. x \<le> 0xF} \<subseteq> obj_refs c \<and> is_pt_cap c) (oref, cref) s
 2. \<And>rv s a b. \<lbrakk>rv \<le> rv + 0x3C; is_aligned rv 6; cte_wp_at (\<lambda>c. is_pt_cap c \<and> (\<exists>y. cap_asid c = Some y) \<and> (\<lambda>x. rv + x * 4 && ~~ mask pt_bits) ` {x. x \<le> 0xF} \<subseteq> obj_refs c) (a, b) s\<rbrakk> \<Longrightarrow> \<exists>oref cref. cte_wp_at (\<lambda>c. (\<lambda>x. rv + x * 4 && ~~ mask pt_bits) ` {x. x \<le> 0xF} \<subseteq> obj_refs c \<and> is_pt_cap c) (oref, cref) s proof (prove)
goal (2 subgoals):
 1. \<And>rv s a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> (\<exists>y. cap_asid c = Some y)) (a, b) s \<Longrightarrow> 0x3C < 2 ^ 6
 2. \<And>rv s a b. \<lbrakk>rv \<le> rv + 0x3C; is_aligned rv 6; cte_wp_at (\<lambda>c. is_pt_cap c \<and> (\<exists>y. cap_asid c = Some y) \<and> (\<lambda>x. rv + x * 4 && ~~ mask pt_bits) ` {x. x \<le> 0xF} \<subseteq> obj_refs c) (a, b) s\<rbrakk> \<Longrightarrow> \<exists>oref cref. cte_wp_at (\<lambda>c. (\<lambda>x. rv + x * 4 && ~~ mask pt_bits) ` {x. x \<le> 0xF} \<subseteq> obj_refs c \<and> is_pt_cap c) (oref, cref) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s a b. \<lbrakk>rv \<le> rv + 0x3C; is_aligned rv 6; cte_wp_at (\<lambda>c. is_pt_cap c \<and> (\<exists>y. cap_asid c = Some y) \<and> (\<lambda>x. rv + x * 4 && ~~ mask pt_bits) ` {x. x \<le> 0xF} \<subseteq> obj_refs c) (a, b) s\<rbrakk> \<Longrightarrow> \<exists>oref cref. cte_wp_at (\<lambda>c. (\<lambda>x. rv + x * 4 && ~~ mask pt_bits) ` {x. x \<le> 0xF} \<subseteq> obj_refs c \<and> is_pt_cap c) (oref, cref) s proof (prove)
goal:
No subgoals!