theory ArchArch_AC

lemma lookup_pt_slot_authorised2:
  "\<lbrace>\<exists>\<rhd> pd and K (is_subject aag pd) and
    K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and
    valid_vspace_objs and valid_arch_state and equal_kernel_mappings and
    valid_global_objs and pspace_aligned and pas_refined aag\<rbrace>
   lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv _. \<forall>x\<in>set [0 , 4 .e. 0x3C]. is_subject aag (x + rv && ~~ mask pt_bits)\<rbrace>, -" apply (clarsimp simp: validE_R_def valid_def validE_def
                 split: sum.split) apply (frule use_validE_R[OF _ lookup_pt_slot_authorised]) apply fastforce apply (frule use_validE_R[OF _ lookup_pt_slot_is_aligned_6]) apply (fastforce simp add: vmsz_aligned_def pd_bits_def pageBits_def) apply (simp add: is_aligned_6_masks) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_subject aag pd) and K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and valid_vspace_objs and valid_arch_state and equal_kernel_mappings and valid_global_objs and pspace_aligned and pas_refined aag\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv _. \<forall>x\<in>set [0 , 4 .e. 0x3C]. is_subject aag (x + rv && ~~ mask pt_bits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s b r ref x. \<lbrakk>(Inr r, b) \<in> fst (lookup_pt_slot pd vptr s); (ref \<rhd> pd) s; is_subject aag pd; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; valid_global_objs s; pspace_aligned s; pas_refined aag s; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> is_subject aag (x + r && ~~ mask pt_bits) proof (prove)
goal (2 subgoals):
 1. \<And>s b r ref x. \<lbrakk>(Inr r, b) \<in> fst (lookup_pt_slot pd vptr s); (ref \<rhd> pd) s; is_subject aag pd; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; valid_global_objs s; pspace_aligned s; pas_refined aag s; x \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and valid_vspace_objs and pspace_aligned and pas_refined (?aag24 s b r ref x) and K (is_subject (?aag24 s b r ref x) pd) and K (is_aligned pd 14 \<and> vptr < kernel_base)) s
 2. \<And>s b r ref x. \<lbrakk>(Inr r, b) \<in> fst (lookup_pt_slot pd vptr s); (ref \<rhd> pd) s; is_subject aag pd; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; valid_global_objs s; pspace_aligned s; pas_refined aag s; x \<in> set [0 , 4 .e. 0x3C]; is_subject (?aag24 s b r ref x) (r && ~~ mask pt_bits)\<rbrakk> \<Longrightarrow> is_subject aag (x + r && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s b r ref x. \<lbrakk>(Inr r, b) \<in> fst (lookup_pt_slot pd vptr s); (ref \<rhd> pd) s; is_subject aag pd; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; valid_global_objs s; pspace_aligned s; pas_refined aag s; x \<in> set [0 , 4 .e. 0x3C]; is_subject aag (r && ~~ mask pt_bits)\<rbrakk> \<Longrightarrow> is_subject aag (x + r && ~~ mask pt_bits) proof (prove)
goal (2 subgoals):
 1. \<And>s b r ref x. \<lbrakk>(Inr r, b) \<in> fst (lookup_pt_slot pd vptr s); (ref \<rhd> pd) s; is_subject aag pd; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; valid_global_objs s; pspace_aligned s; pas_refined aag s; x \<in> set [0 , 4 .e. 0x3C]; is_subject aag (r && ~~ mask pt_bits)\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (vmsz_aligned vptr ARMLargePage) and K (is_aligned pd pd_bits) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs) s
 2. \<And>s b r ref x. \<lbrakk>(Inr r, b) \<in> fst (lookup_pt_slot pd vptr s); (ref \<rhd> pd) s; is_subject aag pd; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; valid_global_objs s; pspace_aligned s; pas_refined aag s; x \<in> set [0 , 4 .e. 0x3C]; is_subject aag (r && ~~ mask pt_bits); is_aligned r 6\<rbrakk> \<Longrightarrow> is_subject aag (x + r && ~~ mask pt_bits) proof (prove)
goal (1 subgoal):
 1. \<And>s b r ref x. \<lbrakk>(Inr r, b) \<in> fst (lookup_pt_slot pd vptr s); (ref \<rhd> pd) s; is_subject aag pd; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; valid_global_objs s; pspace_aligned s; pas_refined aag s; x \<in> set [0 , 4 .e. 0x3C]; is_subject aag (r && ~~ mask pt_bits); is_aligned r 6\<rbrakk> \<Longrightarrow> is_subject aag (x + r && ~~ mask pt_bits) proof (prove)
goal:
No subgoals!