theory ArchKHeap_AI

lemma valid_global_vspace_mappings_lift:
  "\<lbrace>valid_global_vspace_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" apply (simp add: valid_global_vspace_mappings_def valid_pd_kernel_mappings_def
              del: valid_pd_kernel_mappings_arch_def) apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) apply (rule_tac f="valid_pd_kernel_mappings_arch (arm_kernel_vspace x)" in hoare_lift_Pf) apply (rule aobj_at; simp) apply (subst valid_pd_kernel_mappings_arch_def valid_pde_kernel_mappings_def)+ apply (clarsimp simp add: valid_def) apply (erule_tac P=P in rsubst) apply (rule ext) apply (clarsimp intro!: iff_allI split: arch_kernel_obj.splits pde.splits) apply (safe; clarsimp simp add: valid_pt_kernel_mappings_def
                        simp del: valid_pt_kernel_mappings_arch_def) apply (erule use_valid[OF _ aobj_at[where P="\<lambda>x. x"]]; simp add:)+ by (rule classical,
          drule use_valid[OF _ aobj_at[where P="\<lambda>x. \<not>x", OF vspace_obj_pred_fun_lift_id]],
          simp+)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_vspace_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (vspace_obj_fun_lift (valid_pd_kernel_mappings_arch (arm_kernel_vspace (arch_state s)) s) False) (arm_global_pd (arch_state s)) s\<rbrace> f \<lbrace>\<lambda>rv s. obj_at (vspace_obj_fun_lift (valid_pd_kernel_mappings_arch (arm_kernel_vspace (arch_state s)) s) False) (arm_global_pd (arch_state s)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. obj_at (vspace_obj_fun_lift (valid_pd_kernel_mappings_arch (arm_kernel_vspace x) s) False) (arm_global_pd x) s\<rbrace> f \<lbrace>\<lambda>_ a. obj_at (vspace_obj_fun_lift (valid_pd_kernel_mappings_arch (arm_kernel_vspace x) a) False) (arm_global_pd x) a\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrace>obj_at (vspace_obj_fun_lift xa False) (arm_global_pd x)\<rbrace> f \<lbrace>\<lambda>_. obj_at (vspace_obj_fun_lift xa False) (arm_global_pd x)\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>s. P (valid_pd_kernel_mappings_arch (arm_kernel_vspace x) s)\<rbrace> f \<lbrace>\<lambda>_ s. P (valid_pd_kernel_mappings_arch (arm_kernel_vspace x) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x P. \<lbrace>\<lambda>s. P (valid_pd_kernel_mappings_arch (arm_kernel_vspace x) s)\<rbrace> f \<lbrace>\<lambda>_ s. P (valid_pd_kernel_mappings_arch (arm_kernel_vspace x) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x P. \<lbrace>\<lambda>s. P (\<lambda>a. case a of PageDirectory pd \<Rightarrow> \<forall>xa. (case pd xa of InvalidPDE \<Rightarrow> \<lambda>s. \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow | PageTablePDE ptr xb xaa \<Rightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr ptr) | SectionPDE ptr atts xb rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> rghts = {} | SuperSectionPDE ptr atts rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) && ~~ mask (pageBitsForSize ARMSuperSection) \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> rghts = {}) s | _ \<Rightarrow> False)\<rbrace> f \<lbrace>\<lambda>_ s. P (\<lambda>a. case a of PageDirectory pd \<Rightarrow> \<forall>xa. (case pd xa of InvalidPDE \<Rightarrow> \<lambda>s. \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow | PageTablePDE ptr xb xaa \<Rightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr ptr) | SectionPDE ptr atts xb rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> rghts = {} | SuperSectionPDE ptr atts rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) && ~~ mask (pageBitsForSize ARMSuperSection) \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> rghts = {}) s | _ \<Rightarrow> False)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x P s a b. \<lbrakk>P (case_arch_kernel_obj (\<lambda>fun. False) (\<lambda>fun. False) (\<lambda>pd. \<forall>xa. (case pd xa of InvalidPDE \<Rightarrow> \<lambda>s. \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow | PageTablePDE ptr xb xaa \<Rightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr ptr) | SectionPDE ptr atts xb rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> rghts = {} | SuperSectionPDE ptr atts rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) && ~~ mask (pageBitsForSize ARMSuperSection) \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> rghts = {}) s) (\<lambda>bool vmpage_size. False)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> P (case_arch_kernel_obj (\<lambda>fun. False) (\<lambda>fun. False) (\<lambda>pd. \<forall>xa. (case pd xa of InvalidPDE \<Rightarrow> \<lambda>s. \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow | PageTablePDE ptr xb xaa \<Rightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr ptr) | SectionPDE ptr atts xb rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> rghts = {} | SuperSectionPDE ptr atts rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) && ~~ mask (pageBitsForSize ARMSuperSection) \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> rghts = {}) b) (\<lambda>bool vmpage_size. False)) proof (prove)
goal (1 subgoal):
 1. \<And>x P s a b. (a, b) \<in> fst (f s) \<Longrightarrow> case_arch_kernel_obj (\<lambda>fun. False) (\<lambda>fun. False) (\<lambda>pd. \<forall>xa. (case pd xa of InvalidPDE \<Rightarrow> \<lambda>s. \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow | PageTablePDE ptr xb xaa \<Rightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr ptr) | SectionPDE ptr atts xb rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> rghts = {} | SuperSectionPDE ptr atts rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) && ~~ mask (pageBitsForSize ARMSuperSection) \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> rghts = {}) s) (\<lambda>bool vmpage_size. False) = case_arch_kernel_obj (\<lambda>fun. False) (\<lambda>fun. False) (\<lambda>pd. \<forall>xa. (case pd xa of InvalidPDE \<Rightarrow> \<lambda>s. \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow | PageTablePDE ptr xb xaa \<Rightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr ptr) | SectionPDE ptr atts xb rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> rghts = {} | SuperSectionPDE ptr atts rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) && ~~ mask (pageBitsForSize ARMSuperSection) \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> rghts = {}) b) (\<lambda>bool vmpage_size. False) proof (prove)
goal (1 subgoal):
 1. \<And>x P s a b xa. (a, b) \<in> fst (f s) \<Longrightarrow> (case xa of PageDirectory pd \<Rightarrow> \<forall>xa. (case pd xa of InvalidPDE \<Rightarrow> \<lambda>s. \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow | PageTablePDE ptr xb xaa \<Rightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr ptr) | SectionPDE ptr atts xb rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> rghts = {} | SuperSectionPDE ptr atts rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) && ~~ mask (pageBitsForSize ARMSuperSection) \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> rghts = {}) s | _ \<Rightarrow> False) = (case xa of PageDirectory pd \<Rightarrow> \<forall>xa. (case pd xa of InvalidPDE \<Rightarrow> \<lambda>s. \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow | PageTablePDE ptr xb xaa \<Rightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr ptr) | SectionPDE ptr atts xb rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> rghts = {} | SuperSectionPDE ptr atts rghts \<Rightarrow> \<lambda>s. ptrFromPAddr ptr = (UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) && ~~ mask (pageBitsForSize ARMSuperSection) \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xa << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> rghts = {}) b | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>x s a b x3 xb. (a, b) \<in> fst (f s) \<Longrightarrow> ((x3 xb = InvalidPDE \<longrightarrow> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow)) \<and> (\<forall>x21. (\<exists>x22 x23. x3 xb = PageTablePDE x21 x22 x23) \<longrightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr x21) s) \<and> (\<forall>x31 x32 x33 x34. x3 xb = SectionPDE x31 x32 x33 x34 \<longrightarrow> ptrFromPAddr x31 = UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> x34 = {}) \<and> (\<forall>x41 x42 x43. x3 xb = SuperSectionPDE x41 x42 x43 \<longrightarrow> ptrFromPAddr x41 = (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) && ~~ mask 24 \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> x43 = {})) = ((x3 xb = InvalidPDE \<longrightarrow> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow)) \<and> (\<forall>x21. (\<exists>x22 x23. x3 xb = PageTablePDE x21 x22 x23) \<longrightarrow> obj_at (valid_pt_kernel_mappings (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) (ptrFromPAddr x21) b) \<and> (\<forall>x31 x32 x33 x34. x3 xb = SectionPDE x31 x32 x33 x34 \<longrightarrow> ptrFromPAddr x31 = UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits \<and> (\<exists>use. (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = use) \<and> (use = ArmVSpaceKernelWindow \<or> use = ArmVSpaceDeviceWindow)) \<and> x34 = {}) \<and> (\<forall>x41 x42 x43. x3 xb = SuperSectionPDE x41 x42 x43 \<longrightarrow> ptrFromPAddr x41 = (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) && ~~ mask 24 \<and> (\<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa = ArmVSpaceKernelWindow) \<and> x43 = {})) proof (prove)
goal (4 subgoals):
 1. \<And>x s a b x3 xb x21 x22 x23. \<lbrakk>(a, b) \<in> fst (f s); obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) s; x3 xb = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) b
 2. \<And>x s a b x3 xb x21 x22 x23. \<lbrakk>(a, b) \<in> fst (f s); obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) s; \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow; x3 xb = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) b
 3. \<And>x s a b x3 xb x21 x22 x23. \<lbrakk>(a, b) \<in> fst (f s); obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) b; x3 xb = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) s
 4. \<And>x s a b x3 xb x21 x22 x23. \<lbrakk>(a, b) \<in> fst (f s); obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) b; \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow; x3 xb = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) s proof (prove)
goal (2 subgoals):
 1. \<And>x s a b x3 xb x21 x22 x23. \<lbrakk>(a, b) \<in> fst (f s); obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) b; x3 xb = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) s
 2. \<And>x s a b x3 xb x21 x22 x23. \<lbrakk>(a, b) \<in> fst (f s); obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) b; \<forall>xa\<in>{UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits..(UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) + 2 ^ pde_mapping_bits - 1}. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow; x3 xb = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> obj_at (vspace_obj_fun_lift (valid_pt_kernel_mappings_arch (UCAST(12 \<rightarrow> 32) xb << pde_mapping_bits) (arm_kernel_vspace x)) False) (ptrFromPAddr x21) s