kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchKHeap_AI

lemma in_user_frame_obj_pred_lift:
 assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
                             \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
 shows "\<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace>" unfolding in_user_frame_def apply (wp hoare_vcg_ex_lift obj_at) apply (clarsimp simp: vspace_obj_pred_def) apply (auto simp: a_type_def aa_type_def split: kernel_object.splits arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace> f \<lbrace>\<lambda>_ s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sz. vspace_obj_pred (\<lambda>a. a_type a = AArch (AUserData sz))
 2. \<And>s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s \<Longrightarrow> \<exists>x. typ_at (AArch (AUserData x)) (p && ~~ mask (pageBitsForSize x)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s \<Longrightarrow> \<exists>x. typ_at (AArch (AUserData x)) (p && ~~ mask (pageBitsForSize x)) s proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_vspace_objs_lift_weak:
  assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
                             \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
  assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
  shows "\<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" apply (rule valid_vspace_objs_lift) apply (rule vs_lookup_vspace_obj_at_lift) apply (rule obj_at arch_state vspace_pred_imp; simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>
 2. \<And>ako p. \<lbrace>\<lambda>s. \<not> ako_at ako p s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> ako_at ako p s\<rbrace>
 3. \<And>p T. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>_. typ_at (AArch T) p\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>P Pa P' p. vspace_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. Pa (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. Pa (obj_at P' p s)\<rbrace>
 2. \<And>P Pa. \<lbrace>\<lambda>s. Pa (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. Pa (arch_state s)\<rbrace>
 3. \<And>ako p. \<lbrace>\<lambda>s. \<not> ako_at ako p s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> ako_at ako p s\<rbrace>
 4. \<And>p T. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>_. typ_at (AArch T) p\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma set_object_typ_at:
  "\<lbrace>\<lambda>s. P (typ_at T p' s)\<rbrace>
    set_object p obj
   \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace>" apply (simp add: set_object_def get_object_def) apply wp apply clarsimp apply (erule rsubst [where P=P]) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p' s)\<rbrace> set_object p obj \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p' s)\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = a_type obj);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>)
od \<lbrace>\<lambda>rv s. P (typ_at T p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (typ_at T p' s) \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type obj \<longrightarrow> P (typ_at T p' (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>P (typ_at T p' s); kheap s p = Some y; a_type y = a_type obj\<rbrakk> \<Longrightarrow> P (typ_at T p' (s\<lparr>kheap := \<lambda>a. if a = p then Some obj else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>kheap s p = Some y; a_type y = a_type obj\<rbrakk> \<Longrightarrow> typ_at T p' s = typ_at T p' (s\<lparr>kheap := \<lambda>a. if a = p then Some obj else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma set_object_valid_kernel_mappings:
  "\<lbrace>\<lambda>s. valid_kernel_mappings s
           \<and> valid_kernel_mappings_if_pd
                (set (arm_global_pts (arch_state s)))
                    ko\<rbrace>
     set_object ptr ko
   \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" apply (wpsimp wp: set_object_wp) apply (clarsimp simp: valid_kernel_mappings_def
                 elim!: ranE split: if_split_asm) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_kernel_mappings s \<and> valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) ko\<rbrace> set_object ptr ko \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_kernel_mappings s; valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) ko\<rbrakk> \<Longrightarrow> valid_kernel_mappings (s\<lparr>kheap := (kheap s)(ptr \<mapsto> ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>\<forall>x\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x; valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) ko; xa \<noteq> ptr; kheap s xa = Some x\<rbrakk> \<Longrightarrow> valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) x proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_vs_lookup_lift:
  assumes lookup: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>"
  assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
  shows "\<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>" unfolding valid_vs_lookup_def apply (rule hoare_lift_Pf [where f=vs_lookup_pages]) apply (rule hoare_lift_Pf [where f="\<lambda>s. (caps_of_state s)"]) apply (wp lookup cap)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>p ref. (ref, p) \<in> x \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>p ref. (ref, p) \<in> x \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. caps_of_state a p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>s. \<forall>p ref. (ref, p) \<in> x \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. xa p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>p ref. (ref, p) \<in> x \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>p' cap. xa p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_table_caps_lift:
  assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
  assumes pts: "\<And>P. \<lbrace>\<lambda>s. P (second_level_tables (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (second_level_tables (arch_state s))\<rbrace>"
  assumes obj: "\<And>S p. \<lbrace>obj_at (empty_table S) p\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) p\<rbrace>"
  shows "\<lbrace>valid_table_caps\<rbrace> f \<lbrace>\<lambda>_. valid_table_caps\<rbrace>" unfolding valid_table_caps_def apply (rule hoare_lift_Pf [where f="\<lambda>s. (caps_of_state s)"]) apply (rule hoare_lift_Pf [where f="\<lambda>s. second_level_tables (arch_state s)"]) apply (wp cap pts hoare_vcg_all_lift hoare_vcg_const_imp_lift obj)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_table_caps\<rbrace> f \<lbrace>\<lambda>_. valid_table_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r p cap. caps_of_state s p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>r p cap. caps_of_state s p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>r p cap. x p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>r p cap. x p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state a)))) r a\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>s. \<forall>r p cap. x p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set xa)) r s\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>r p cap. x p = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set xa)) r a\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>s. P (second_level_tables (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (second_level_tables (arch_state s))\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_arch_caps_lift_weak:
  "(\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>) \<Longrightarrow>
      \<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>" apply (rule valid_arch_caps_lift[OF _ _ arch aobj_at]) apply (rule vs_lookup_pages_vspace_obj_at_lift[OF aobj_at arch], assumption+) apply (rule empty_table.vspace_only) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>) \<Longrightarrow> \<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. (\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>
 2. \<And>P. (\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 3. \<And>S p. (\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>) \<Longrightarrow> vspace_obj_pred (empty_table S) proof (prove)
goal (1 subgoal):
 1. \<And>S p. (\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>) \<Longrightarrow> vspace_obj_pred (empty_table S) proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_global_objs_lift_weak:
  "\<lbrace>valid_global_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" apply (rule valid_global_objs_lift) apply (wp arch)+ apply (simp add: valid_vso_at_def) apply (rule hoare_vcg_ex_lift) apply (rule hoare_vcg_conj_lift) apply (wp aobj_at valid_vspace_obj_typ | simp | rule empty_table.vspace_only)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (arm_global_pts (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (arm_global_pts (arch_state s))\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (arm_global_pd (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (arm_global_pd (arch_state s))\<rbrace>
 3. \<And>p. \<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>
 4. \<And>ako p. \<lbrace>ako_at ako p\<rbrace> f \<lbrace>\<lambda>_. ako_at ako p\<rbrace>
 5. \<And>pd S. \<lbrace>obj_at (empty_table S) pd\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>
 2. \<And>ako p. \<lbrace>ako_at ako p\<rbrace> f \<lbrace>\<lambda>_. ako_at ako p\<rbrace>
 3. \<And>pd S. \<lbrace>obj_at (empty_table S) pd\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrace>\<lambda>s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace>
 2. \<And>ako p. \<lbrace>ako_at ako p\<rbrace> f \<lbrace>\<lambda>_. ako_at ako p\<rbrace>
 3. \<And>pd S. \<lbrace>obj_at (empty_table S) pd\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>p ao. \<lbrace>\<lambda>s. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace>
 2. \<And>ako p. \<lbrace>ako_at ako p\<rbrace> f \<lbrace>\<lambda>_. ako_at ako p\<rbrace>
 3. \<And>pd S. \<lbrace>obj_at (empty_table S) pd\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>p ao. \<lbrace>ako_at ao p\<rbrace> f \<lbrace>\<lambda>rv. ako_at ao p\<rbrace>
 2. \<And>p ao. \<lbrace>valid_vspace_obj ao\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_obj ao\<rbrace>
 3. \<And>ako p. \<lbrace>ako_at ako p\<rbrace> f \<lbrace>\<lambda>_. ako_at ako p\<rbrace>
 4. \<And>pd S. \<lbrace>obj_at (empty_table S) pd\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_asid_map_lift:
  "\<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" apply (simp add: valid_asid_map_def) apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) apply (simp add: vspace_at_asid_def) by (rule vs_lookup_vspace_obj_at_lift[OF aobj_at arch])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>rv. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)\<rbrace> f \<lbrace>\<lambda>rv s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. dom (arm_asid_map x) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map x). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)\<rbrace> f \<lbrace>\<lambda>_ a. dom (arm_asid_map x) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map x). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd a \<and> asid \<noteq> 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. dom (arm_asid_map x) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map x). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0)\<rbrace> f \<lbrace>\<lambda>_ a. dom (arm_asid_map x) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map x). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) a \<and> asid \<noteq> 0)\<rbrace>
theory ArchKHeap_AI

lemma valid_global_pts_lift:
  "\<lbrace>valid_global_pts\<rbrace> f \<lbrace>\<lambda>rv. valid_global_pts\<rbrace>" apply (simp add: valid_global_pts_def) apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) apply (rule hoare_vcg_ball_lift) apply (rule aobj_at) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_pts\<rbrace> f \<lbrace>\<lambda>rv. valid_global_pts\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>p\<in>set (arm_global_pts (arch_state s)). typ_at (AArch APageTable) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>p\<in>set (arm_global_pts x). typ_at (AArch APageTable) p s\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>p\<in>set (arm_global_pts x). typ_at (AArch APageTable) p a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x p. p \<in> set (arm_global_pts x) \<Longrightarrow> \<lbrace>typ_at (AArch APageTable) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch APageTable) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x p. p \<in> set (arm_global_pts x) \<Longrightarrow> arch_obj_pred (\<lambda>a. a_type a = AArch APageTable) proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_arch_state_lift_aobj_at:
  "\<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>" apply (simp add: valid_arch_state_def valid_asid_table_def) apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) apply (wp hoare_vcg_conj_lift hoare_vcg_ball_lift valid_global_pts_lift | (rule aobj_at, clarsimp))+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>rv. 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> valid_global_pts s \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrace> f \<lbrace>\<lambda>rv 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> valid_global_pts s \<and> is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 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> valid_global_pts 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> valid_global_pts a \<and> is_inv (arm_hwasid_table x) (map_option fst \<circ> arm_asid_map x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x 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> valid_global_pts s \<and> is_inv (arm_hwasid_table x) (map_option fst \<circ> arm_asid_map x) \<Longrightarrow> (\<forall>x\<in>ran (arm_asid_table x). typ_at (AArch AASIDPool) x s) \<and> inj_on (arm_asid_table x) (dom (arm_asid_table x)) \<and> typ_at (AArch APageDirectory) (arm_global_pd x) s \<and> valid_global_pts s \<and> is_inv (arm_hwasid_table x) (map_option fst \<circ> arm_asid_map x) proof (prove)
goal:
No subgoals!