kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchInvariants_AI

lemma atyp_at_eq_kheap_obj:
  "typ_at (AArch AASIDPool) p s \<longleftrightarrow> (\<exists>f. kheap s p = Some (ArchObj (ASIDPool f)))"
  "typ_at (AArch APageTable) p s \<longleftrightarrow> (\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))"
  "typ_at (AArch APageDirectory) p s \<longleftrightarrow> (\<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)))"
  "typ_at (AArch (AUserData sz)) p s \<longleftrightarrow> (kheap s p = Some (ArchObj (DataPage False sz)))"
  "typ_at (AArch (ADeviceData sz)) p s \<longleftrightarrow> (kheap s p = Some (ArchObj (DataPage True sz)))" apply (auto simp add: obj_at_def) apply (simp_all add: a_type_def
                split: if_split_asm kernel_object.splits arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (typ_at (AArch AASIDPool) p s = (\<exists>f. kheap s p = Some (ArchObj (ASIDPool f))) &&& typ_at (AArch APageTable) p s = (\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))) &&& typ_at (AArch APageDirectory) p s = (\<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd))) &&& typ_at (AArch (AUserData sz)) p s = (kheap s p = Some (ArchObj (DataPage False sz))) &&& typ_at (AArch (ADeviceData sz)) p s = (kheap s p = Some (ArchObj (DataPage True sz))) proof (prove)
goal (10 subgoals):
 1. \<And>ko. \<lbrakk>kheap s p = Some ko; a_type ko = AArch AASIDPool\<rbrakk> \<Longrightarrow> \<exists>f. ko = ArchObj (ASIDPool f)
 2. \<And>f. kheap s p = Some (ArchObj (ASIDPool f)) \<Longrightarrow> a_type (ArchObj (ASIDPool f)) = AArch AASIDPool
 3. \<And>ko. \<lbrakk>kheap s p = Some ko; a_type ko = AArch APageTable\<rbrakk> \<Longrightarrow> \<exists>pt. ko = ArchObj (PageTable pt)
 4. \<And>pt. kheap s p = Some (ArchObj (PageTable pt)) \<Longrightarrow> a_type (ArchObj (PageTable pt)) = AArch APageTable
 5. \<And>ko. \<lbrakk>kheap s p = Some ko; a_type ko = AArch APageDirectory\<rbrakk> \<Longrightarrow> \<exists>pd. ko = ArchObj (PageDirectory pd)
 6. \<And>pd. kheap s p = Some (ArchObj (PageDirectory pd)) \<Longrightarrow> a_type (ArchObj (PageDirectory pd)) = AArch APageDirectory
 7. \<And>ko. \<lbrakk>kheap s p = Some ko; a_type ko = AArch (AUserData sz)\<rbrakk> \<Longrightarrow> ko = ArchObj (DataPage False sz)
 8. kheap s p = Some (ArchObj (DataPage False sz)) \<Longrightarrow> a_type (ArchObj (DataPage False sz)) = AArch (AUserData sz)
 9. \<And>ko. \<lbrakk>kheap s p = Some ko; a_type ko = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> ko = ArchObj (DataPage True sz)
 10. kheap s p = Some (ArchObj (DataPage True sz)) \<Longrightarrow> a_type (ArchObj (DataPage True sz)) = AArch (ADeviceData sz) proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma shows
  aa_type_AASIDPoolE:
  "\<lbrakk>a_type ko = AArch AASIDPool;
    (\<And>ap. ko = ArchObj (ASIDPool ap) \<Longrightarrow> R)\<rbrakk>
   \<Longrightarrow> R" and
  aa_type_APageDirectoryE:
  "\<lbrakk>a_type ko = AArch APageDirectory;
    (\<And>pd. ko = ArchObj (PageDirectory pd) \<Longrightarrow> R)\<rbrakk>
   \<Longrightarrow> R" and
   aa_type_APageTableE:
  "\<lbrakk>a_type ko = AArch APageTable; (\<And>pt. ko = ArchObj (PageTable pt) \<Longrightarrow> R)\<rbrakk>
   \<Longrightarrow> R" and
   aa_type_AUserDataE:
  "\<lbrakk>a_type ko = AArch (AUserData sz); ko = ArchObj (DataPage False sz) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   and
   aa_type_ADeviceDataE:
  "\<lbrakk>a_type ko = AArch (ADeviceData sz); ko = ArchObj (DataPage True sz) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by (rule kernel_object_exhaust[of ko]; clarsimp simp add: a_type_simps split: if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>a_type ko = AArch AASIDPool; \<And>ap. ko = ArchObj (ASIDPool ap) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R) &&& (\<lbrakk>a_type ko = AArch APageDirectory; \<And>pd. ko = ArchObj (PageDirectory pd) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R)) &&& (\<lbrakk>a_type ko = AArch APageTable; \<And>pt. ko = ArchObj (PageTable pt) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R) &&& (\<lbrakk>a_type ko = AArch (AUserData sz); ko = ArchObj (DataPage False sz) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R) &&& (\<lbrakk>a_type ko = AArch (ADeviceData sz); ko = ArchObj (DataPage True sz) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R)
theory ArchInvariants_AI

lemma wellformed_arch_typ:
   assumes P: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
   shows   "\<lbrace>\<lambda>s. arch_valid_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. arch_valid_obj ao s\<rbrace>" by (cases ao; clarsimp; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>arch_valid_obj ao\<rbrace> f \<lbrace>\<lambda>rv. arch_valid_obj ao\<rbrace>
theory ArchInvariants_AI

lemma aobj_bits_T:
  "arch_kobj_size v = arch_obj_bits_type (aa_type v)" unfolding arch_obj_bits_type_def aa_type_def by (cases v; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_kobj_size v = arch_obj_bits_type (aa_type v) proof (prove)
goal (1 subgoal):
 1. arch_kobj_size v = (case case v of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz of AASIDPool \<Rightarrow> arch_kobj_size (ASIDPool undefined) | APageTable \<Rightarrow> arch_kobj_size (PageTable undefined) | APageDirectory \<Rightarrow> arch_kobj_size (PageDirectory undefined) | AUserData sz \<Rightarrow> arch_kobj_size (DataPage False sz) | ADeviceData sz \<Rightarrow> arch_kobj_size (DataPage True sz))
theory ArchInvariants_AI

lemma valid_ipc_buffer_cap_null:
  "valid_ipc_buffer_cap NullCap buf" by (simp add: valid_ipc_buffer_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ipc_buffer_cap NullCap buf
theory ArchInvariants_AI

lemma pageBits_clb_less_word_bits [simp]:
  "pageBits - cte_level_bits < word_bits" by (rule less_imp_diff_less, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBits - cte_level_bits < word_bits
theory ArchInvariants_AI

lemma in_user_frame_update[iff]:
  "in_user_frame p (f s) = in_user_frame p s" by (simp add: in_user_frame_def pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. in_user_frame p (f s) = in_user_frame p s
theory ArchInvariants_AI

lemma obj_at_update [iff]:
  "obj_at P p (f s) = obj_at P p s" by (fastforce intro: obj_at_pspaceI simp: pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P p (f s) = obj_at P p s
theory ArchInvariants_AI

lemma valid_asid_table_update [iff]:
  "valid_asid_table t (f s) = valid_asid_table t s" by (simp add: valid_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_table t (f s) = valid_asid_table t s
theory ArchInvariants_AI

lemma valid_global_pts_update [iff]:
  "arm_global_pts (arch_state (f s)) = arm_global_pts (arch_state s) \<Longrightarrow>
   valid_global_pts (f s) = valid_global_pts s" by (simp add: valid_global_pts_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_global_pts (arch_state (f s)) = arm_global_pts (arch_state s) \<Longrightarrow> valid_global_pts (f s) = valid_global_pts s
theory ArchInvariants_AI

lemma valid_pte_update [iff]:
  "valid_pte pte (f s) = valid_pte pte s" by (cases pte) (auto simp: data_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pte pte (f s) = valid_pte pte s
theory ArchInvariants_AI

lemma valid_pde_update [iff]:
  "valid_pde pde (f s) = valid_pde pde s" by (cases pde) (auto simp: data_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pde pde (f s) = valid_pde pde s
theory ArchInvariants_AI

lemma valid_vspace_obj_update [iff]:
  "valid_vspace_obj ao (f s) = valid_vspace_obj ao s" by (cases ao) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_obj ao (f s) = valid_vspace_obj ao s
theory ArchInvariants_AI

lemma valid_ao_at_update [iff]:
  "valid_ao_at p (f s) = valid_ao_at p s" by (simp add: valid_ao_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ao_at p (f s) = valid_ao_at p s
theory ArchInvariants_AI

lemma valid_vso_at_update [iff]:
  "valid_vso_at p (f s) = valid_vso_at p s" by (simp add: valid_vso_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vso_at p (f s) = valid_vso_at p s
theory ArchInvariants_AI

lemma equal_kernel_mappings_update [iff]:
  "equal_kernel_mappings (f s) = equal_kernel_mappings s" by (simp add: equal_kernel_mappings_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equal_kernel_mappings (f s) = equal_kernel_mappings s
theory ArchInvariants_AI

lemma valid_pt_kernel_mappings [iff]:
  "valid_pde_kernel_mappings pde vref uses (f s)
      = valid_pde_kernel_mappings pde vref uses s" by (cases pde, simp_all add: valid_pde_kernel_mappings_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pde_kernel_mappings pde vref uses (f s) = valid_pde_kernel_mappings pde vref uses s
theory ArchInvariants_AI

lemma valid_pd_kernel_mappings [iff]:
  "valid_pd_kernel_mappings uses (f s)
      = valid_pd_kernel_mappings uses s" by (rule ext, simp add: valid_pd_kernel_mappings_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pd_kernel_mappings uses (f s) = valid_pd_kernel_mappings uses s
theory ArchInvariants_AI

lemma caps_of_state_update [iff]:
  "caps_of_state (f s) = caps_of_state s" by (rule ext) (auto simp: caps_of_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state (f s) = caps_of_state s
theory ArchInvariants_AI

lemma arch_valid_obj_update:
  "\<And>ao. b = ArchObj ao \<Longrightarrow> arch_valid_obj ao (f s) = arch_valid_obj ao s" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ao. b = ArchObj ao \<Longrightarrow> arch_valid_obj ao (f s) = arch_valid_obj ao s
theory ArchInvariants_AI

lemma global_refs_update [iff]:
  "global_refs (f s) = global_refs s" by (simp add: global_refs_def arch idle irq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_refs (f s) = global_refs s
theory ArchInvariants_AI

lemma vs_lookup1_update [iff]:
  "vs_lookup1 (f s) = vs_lookup1 s" by (simp add: vs_lookup1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup1 (f s) = vs_lookup1 s
theory ArchInvariants_AI

lemma vs_lookup_update [iff]:
  "vs_lookup (f s) = vs_lookup s" by (simp add: vs_lookup_def arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup (f s) = vs_lookup s
theory ArchInvariants_AI

lemma vs_lookup_pages1_update [iff]:
  "vs_lookup_pages1 (f s) = vs_lookup_pages1 s" by (simp add: vs_lookup_pages1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages1 (f s) = vs_lookup_pages1 s
theory ArchInvariants_AI

lemma vs_lookup_pages_update [iff]:
  "vs_lookup_pages (f s) = vs_lookup_pages s" by (simp add: vs_lookup_pages_def arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages (f s) = vs_lookup_pages s
theory ArchInvariants_AI

lemma valid_vs_lookup_update [iff]:
  "valid_vs_lookup (f s) = valid_vs_lookup s" by (simp add: valid_vs_lookup_def arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vs_lookup (f s) = valid_vs_lookup s
theory ArchInvariants_AI

lemma valid_table_caps_update [iff]:
  "valid_table_caps (f s) = valid_table_caps s" by (simp add: valid_table_caps_def arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_table_caps (f s) = valid_table_caps s
theory ArchInvariants_AI

lemma valid_vspace_objs_update' [iff]:
  "valid_vspace_objs (f s) = valid_vspace_objs s" by (simp add: valid_vspace_objs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs (f s) = valid_vspace_objs s
theory ArchInvariants_AI

lemma global_refs_equiv:
  assumes "idle_thread s = idle_thread s'"
  assumes "interrupt_irq_node s = interrupt_irq_node s'"
  assumes "arm_globals_frame (arch_state s) = arm_globals_frame (arch_state s')"
  assumes "arm_global_pd (arch_state s) = arm_global_pd (arch_state s')"
  assumes "set (arm_global_pts (arch_state s)) = set (arm_global_pts (arch_state s'))"
  assumes "ran (arm_asid_table (arch_state s)) = ran (arm_asid_table (arch_state s'))"
  shows "global_refs s = global_refs s'" by (simp add: assms global_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_refs s = global_refs s'
theory ArchInvariants_AI

lemma global_refs_lift:
  assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
  assumes idle: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>"
  assumes irq: "\<And>P. \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> f \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (global_refs s) \<rbrace> f \<lbrace>\<lambda>r s. P (global_refs s) \<rbrace>" unfolding global_refs_def apply (rule hoare_lift_Pf [where f="arch_state", OF _ arch]) apply (rule hoare_lift_Pf [where f="idle_thread", OF _ idle]) apply (rule hoare_lift_Pf [where f="interrupt_irq_node", OF _ irq]) apply (rule hoare_vcg_prop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> f \<lbrace>\<lambda>r s. P (global_refs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ({idle_thread s, arm_global_pd (arch_state s)} \<union> range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s)))\<rbrace> f \<lbrace>\<lambda>r s. P ({idle_thread s, arm_global_pd (arch_state s)} \<union> range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. P ({idle_thread s, arm_global_pd x} \<union> range (interrupt_irq_node s) \<union> set (arm_global_pts x))\<rbrace> f \<lbrace>\<lambda>_ a. P ({idle_thread a, arm_global_pd x} \<union> range (interrupt_irq_node a) \<union> set (arm_global_pts x))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. P ({xa, arm_global_pd x} \<union> range (interrupt_irq_node s) \<union> set (arm_global_pts x))\<rbrace> f \<lbrace>\<lambda>_ a. P ({xa, arm_global_pd x} \<union> range (interrupt_irq_node a) \<union> set (arm_global_pts x))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrace>\<lambda>s. P ({xa, arm_global_pd x} \<union> range xb \<union> set (arm_global_pts x))\<rbrace> f \<lbrace>\<lambda>_ a. P ({xa, arm_global_pd x} \<union> range xb \<union> set (arm_global_pts x))\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma valid_arch_state_lift:
  assumes typs: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>_. typ_at (AArch T) p\<rbrace>"
  assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
  shows "\<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" apply (simp add: valid_arch_state_def valid_asid_table_def
                   valid_global_pts_def) apply (rule hoare_lift_Pf[where f="\<lambda>s. arch_state s"]) apply (wp arch typs hoare_vcg_conj_lift hoare_vcg_const_Ball_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> inj_on (asid_table s) (dom (asid_table s)) \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> (\<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s) \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. (\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s) \<and> inj_on (asid_table s) (dom (asid_table s)) \<and> typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s \<and> (\<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s) \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. (\<forall>p\<in>ran (arm_asid_table x). typ_at (AArch AASIDPool) p s) \<and> inj_on (arm_asid_table x) (dom (arm_asid_table x)) \<and> typ_at (AArch APageDirectory) (arm_global_pd x) s \<and> (\<forall>p\<in>set (arm_global_pts x). typ_at (AArch APageTable) p s) \<and> is_inv (arm_hwasid_table x) (map_option fst \<circ> arm_asid_map x)\<rbrace> f \<lbrace>\<lambda>_ a. (\<forall>p\<in>ran (arm_asid_table x). typ_at (AArch AASIDPool) p a) \<and> inj_on (arm_asid_table x) (dom (arm_asid_table x)) \<and> typ_at (AArch APageDirectory) (arm_global_pd x) a \<and> (\<forall>p\<in>set (arm_global_pts x). typ_at (AArch APageTable) p a) \<and> is_inv (arm_hwasid_table x) (map_option fst \<circ> arm_asid_map x)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma aobj_at_default_arch_cap_valid:
  assumes "ty \<noteq> ASIDPoolObj"
  assumes "ko_at (ArchObj (default_arch_object ty dev us)) x s"
  shows "valid_arch_cap (arch_default_cap ty x us dev) s" using assms by (auto elim!: obj_at_weakenE
        simp add: arch_default_cap_def valid_arch_cap_def default_arch_object_def
                  a_type_def
                  valid_vm_rights_def
           split: apiobject_type.splits aobject_type.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_cap (arch_default_cap ty x us dev) s proof (prove)
using this:
ty \<noteq> ASIDPoolObj
ako_at (default_arch_object ty dev us) x s

goal (1 subgoal):
 1. valid_arch_cap (arch_default_cap ty x us dev) s
theory ArchInvariants_AI

lemma aobj_ref_default:
  "aobj_ref (arch_default_cap x6 x us dev) = Some x" by (auto simp add: arch_default_cap_def split: aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aobj_ref (arch_default_cap x6 x us dev) = Some x
theory ArchInvariants_AI

lemma valid_pde_lift:
  assumes x: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
  shows "\<lbrace>\<lambda>s. valid_pde pde s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pde pde s\<rbrace>" by (cases pde) (simp add: data_at_def | wp x hoare_vcg_disj_lift)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde pde\<rbrace> f \<lbrace>\<lambda>rv. valid_pde pde\<rbrace>
theory ArchInvariants_AI

lemma valid_pte_lift:
  assumes x: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
  shows "\<lbrace>\<lambda>s. valid_pte pte s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pte pte s\<rbrace>" by (cases pte) (simp add: data_at_def| wp x hoare_vcg_disj_lift)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pte pte\<rbrace> f \<lbrace>\<lambda>rv. valid_pte pte\<rbrace>
theory ArchInvariants_AI

lemma pde_at_atyp:
  assumes x: "\<And>p T. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
  shows      "\<lbrace>pde_at p\<rbrace> f \<lbrace>\<lambda>rv. pde_at p\<rbrace>" by (simp add: pde_at_def | wp x)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pde_at p\<rbrace> f \<lbrace>\<lambda>rv. pde_at p\<rbrace>
theory ArchInvariants_AI

lemma pte_at_atyp:
  assumes x: "\<And>p T. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>"
  shows      "\<lbrace>pte_at p\<rbrace> f \<lbrace>\<lambda>rv. pte_at p\<rbrace>" by (simp add: pte_at_def | wp x)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pte_at p\<rbrace> f \<lbrace>\<lambda>rv. pte_at p\<rbrace>
theory ArchInvariants_AI

lemma physical_arch_cap_has_ref:
  "(acap_class arch_cap = PhysicalClass) = (\<exists>y. aobj_ref arch_cap = Some y)" by (cases arch_cap; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (acap_class arch_cap = PhysicalClass) = (\<exists>y. aobj_ref arch_cap = Some y)
theory ArchInvariants_AI

lemma vs_lookup1_is_arch:
  "(a \<rhd>1 b) s \<Longrightarrow> \<exists>ao'. ko_at (ArchObj ao') (snd a) s" apply (clarsimp simp: vs_lookup1_def) apply (case_tac ko, auto simp: vs_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> vs_lookup1 s \<Longrightarrow> \<exists>ao'. ako_at ao' (snd a) s proof (prove)
goal (1 subgoal):
 1. \<And>x y ya ko r. \<lbrakk>a = (x, y); b = (r # x, ya); ko_at ko y s; (r, ya) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> \<exists>ao'. ako_at ao' y s proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_trancl_step:
  "\<lbrakk> r \<in> vs_lookup s; (r, r') \<in> (vs_lookup1 s)^+ \<rbrakk> \<Longrightarrow> r' \<in> vs_lookup s" apply (clarsimp simp add: vs_lookup_def) apply (drule (1) rtrancl_trancl_trancl) apply (drule trancl_into_rtrancl)+ apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> vs_lookup s; (r, r') \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> r' \<in> vs_lookup s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(r, r') \<in> (vs_lookup1 s)\<^sup>+; ((a, b), r) \<in> (vs_lookup1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> r' \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(r, r') \<in> (vs_lookup1 s)\<^sup>+; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), r') \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> r' \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); (r, r') \<in> (vs_lookup1 s)\<^sup>*; ((a, b), r') \<in> (vs_lookup1 s)\<^sup>*\<rbrakk> \<Longrightarrow> r' \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_pages_trancl_step:
  "\<lbrakk> r \<in> vs_lookup_pages s; (r, r') \<in> (vs_lookup_pages1 s)^+ \<rbrakk> \<Longrightarrow> r' \<in> vs_lookup_pages s" apply (clarsimp simp add: vs_lookup_pages_def) apply (drule (1) rtrancl_trancl_trancl) apply (drule trancl_into_rtrancl)+ apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> vs_lookup_pages s; (r, r') \<in> (vs_lookup_pages1 s)\<^sup>+\<rbrakk> \<Longrightarrow> r' \<in> vs_lookup_pages s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(r, r') \<in> (vs_lookup_pages1 s)\<^sup>+; ((a, b), r) \<in> (vs_lookup_pages1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> r' \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(r, r') \<in> (vs_lookup_pages1 s)\<^sup>+; (a, b) \<in> vs_asid_refs (asid_table s); ((a, b), r') \<in> (vs_lookup_pages1 s)\<^sup>+\<rbrakk> \<Longrightarrow> r' \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); (r, r') \<in> (vs_lookup_pages1 s)\<^sup>*; ((a, b), r') \<in> (vs_lookup_pages1 s)\<^sup>*\<rbrakk> \<Longrightarrow> r' \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal:
No subgoals!