theory ArchInvariants_AI

lemma valid_vspace_obj_typ:
  assumes P: "\<And>p T. \<lbrace>\<lambda>s. (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s.  (typ_at (AArch T) p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_vspace_obj ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_vspace_obj ob s\<rbrace>" apply (cases ob, simp_all add: valid_vspace_obj_def) apply (rule hoare_vcg_const_Ball_lift [OF P]) apply (rule hoare_vcg_all_lift) apply (rename_tac "fun" x) apply (case_tac "fun x",simp_all add: data_at_def hoare_vcg_prop P) apply (wp hoare_vcg_disj_lift P)+ apply (rule hoare_vcg_ball_lift) apply (rename_tac "fun" x) apply (case_tac "fun x", simp_all add: data_at_def hoare_vcg_prop P) apply (wp hoare_vcg_disj_lift P)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_obj ob\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_obj ob\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x1. ob = ASIDPool x1 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>ran x1. typ_at (AArch APageDirectory) x s\<rbrace>
 2. \<And>x2. ob = PageTable x2 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. valid_pte (x2 x) s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. valid_pte (x2 x) s\<rbrace>
 3. \<And>x3. ob = PageDirectory x3 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace>
 4. \<And>x41 x42. ob = DataPage x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x2. ob = PageTable x2 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. valid_pte (x2 x) s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. valid_pte (x2 x) s\<rbrace>
 2. \<And>x3. ob = PageDirectory x3 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace>
 3. \<And>x41 x42. ob = DataPage x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x2 x. ob = PageTable x2 \<Longrightarrow> \<lbrace>valid_pte (x2 x)\<rbrace> f \<lbrace>\<lambda>rv. valid_pte (x2 x)\<rbrace>
 2. \<And>x3. ob = PageDirectory x3 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace>
 3. \<And>x41 x42. ob = DataPage x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>fun x. ob = PageTable fun \<Longrightarrow> \<lbrace>valid_pte (fun x)\<rbrace> f \<lbrace>\<lambda>rv. valid_pte (fun x)\<rbrace>
 2. \<And>x3. ob = PageDirectory x3 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace>
 3. \<And>x41 x42. ob = DataPage x41 x42 \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>fun x x21 x22 x23. \<lbrakk>ob = PageTable fun; fun x = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch (AUserData ARMLargePage)) (ptrFromPAddr x21) s \<or> typ_at (AArch (ADeviceData ARMLargePage)) (ptrFromPAddr x21) s\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (AArch (AUserData ARMLargePage)) (ptrFromPAddr x21) s \<or> typ_at (AArch (ADeviceData ARMLargePage)) (ptrFromPAddr x21) s\<rbrace>
 2. \<And>fun x x31 x32 x33. \<lbrakk>ob = PageTable fun; fun x = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch (AUserData ARMSmallPage)) (ptrFromPAddr x31) s \<or> typ_at (AArch (ADeviceData ARMSmallPage)) (ptrFromPAddr x31) s\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (AArch (AUserData ARMSmallPage)) (ptrFromPAddr x31) s \<or> typ_at (AArch (ADeviceData ARMSmallPage)) (ptrFromPAddr x31) s\<rbrace>
 3. \<And>x3. ob = PageDirectory x3 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. ob = PageDirectory x3 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3 x. \<lbrakk>ob = PageDirectory x3; x \<in> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>valid_pde (x3 x)\<rbrace> f \<lbrace>\<lambda>rv. valid_pde (x3 x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>fun x. \<lbrakk>ob = PageDirectory fun; x \<in> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>valid_pde (fun x)\<rbrace> f \<lbrace>\<lambda>rv. valid_pde (fun x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>fun x x31 x32 x33 x34. \<lbrakk>ob = PageDirectory fun; x \<notin> kernel_mapping_slots; fun x = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch (AUserData ARMSection)) (ptrFromPAddr x31) s \<or> typ_at (AArch (ADeviceData ARMSection)) (ptrFromPAddr x31) s\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (AArch (AUserData ARMSection)) (ptrFromPAddr x31) s \<or> typ_at (AArch (ADeviceData ARMSection)) (ptrFromPAddr x31) s\<rbrace>
 2. \<And>fun x x41 x42 x43. \<lbrakk>ob = PageDirectory fun; x \<notin> kernel_mapping_slots; fun x = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (AArch (AUserData ARMSuperSection)) (ptrFromPAddr x41) s \<or> typ_at (AArch (ADeviceData ARMSuperSection)) (ptrFromPAddr x41) s\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (AArch (AUserData ARMSuperSection)) (ptrFromPAddr x41) s \<or> typ_at (AArch (ADeviceData ARMSuperSection)) (ptrFromPAddr x41) s\<rbrace> proof (prove)
goal:
No subgoals!