kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_AI

lemma as_user_in_user_frame[wp]:
  "\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> as_user t m \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>" unfolding in_user_frame_def by (wp hoare_vcg_ex_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p\<rbrace> as_user t m \<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> as_user t m \<lbrace>\<lambda>_ s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace>
theory ArchAcc_AI

lemma as_user_in_device_frame[wp]:
  "\<lbrace>\<lambda>s. in_device_frame p s\<rbrace> as_user t m \<lbrace>\<lambda>_ s. in_device_frame p s\<rbrace>" unfolding in_device_frame_def by (wp hoare_vcg_ex_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_device_frame p\<rbrace> as_user t m \<lbrace>\<lambda>_. in_device_frame p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>sz. typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace> as_user t m \<lbrace>\<lambda>_ s. \<exists>sz. typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace>
theory ArchAcc_AI

lemma load_word_offs_in_user_frame[wp]:
  "\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> load_word_offs a x \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>" unfolding in_user_frame_def by (wp hoare_vcg_ex_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p\<rbrace> load_word_offs a x \<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> load_word_offs a x \<lbrace>\<lambda>_ s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace>
theory ArchAcc_AI

lemma valid_machine_state_heap_updI:
assumes vm : "valid_machine_state s"
assumes tyat : "typ_at type p s"
shows
  " a_type obj = type \<Longrightarrow> valid_machine_state (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>)" apply (clarsimp simp: valid_machine_state_def) subgoal for p apply (rule valid_machine_stateE[OF vm,where p = p]) apply (elim disjE,simp_all) apply (drule(1) in_user_frame_same_type_upd[OF tyat]) apply simp+ done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a_type obj = type \<Longrightarrow> valid_machine_state (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>type = a_type obj; underlying_memory (machine_state s) pa \<noteq> 0\<rbrakk> \<Longrightarrow> in_user_frame pa (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type = a_type obj; underlying_memory (machine_state s) p \<noteq> 0\<rbrakk> \<Longrightarrow> in_user_frame p (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type = a_type obj; underlying_memory (machine_state s) p \<noteq> 0; in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrakk> \<Longrightarrow> in_user_frame p (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type = a_type obj; underlying_memory (machine_state s) p \<noteq> 0; in_user_frame p s\<rbrakk> \<Longrightarrow> in_user_frame p (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>underlying_memory (machine_state s) p \<noteq> 0; in_user_frame p s; in_user_frame p (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>)\<rbrakk> \<Longrightarrow> in_user_frame p (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_vms[wp]:
  "\<lbrace>valid_machine_state\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" unfolding set_pt_def including unfold_objects apply (wpsimp wp: set_object_wp_strong simp: a_type_def) apply (erule valid_machine_state_heap_updI) apply (fastforce simp: a_type_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_machine_state s; kheap s p = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> valid_machine_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> typ_at (?type48 s x2) p s
 2. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> a_type (ArchObj (PageTable pt)) = ?type48 s x2 proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_asid_pool_iflive [wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap s\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. if_live_then_nonz_cap s\<rbrace>" apply (simp add: set_asid_pool_def) including unfold_objects by (wpsimp wp: set_object_iflive[THEN hoare_set_object_weaken_pre]
           simp: a_type_def live_def hyp_live_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_zombies [wp]:
  "\<lbrace>\<lambda>s. zombies_final s\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. zombies_final s\<rbrace>" unfolding set_asid_pool_def including unfold_objects by (wpsimp wp: set_object_zombies[THEN hoare_set_object_weaken_pre]
           simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. zombies_final\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_zombies_state_refs [wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace>" unfolding set_asid_pool_def including unfold_objects apply (wpsimp wp: set_object_wp_strong
              simp: a_type_def) apply (erule rsubst [where P=P], rule ext) apply (clarsimp simp: state_refs_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1. \<lbrakk>P (state_refs_of s); kheap s p = Some (ArchObj (ASIDPool x1))\<rbrakk> \<Longrightarrow> P (state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x. kheap s p = Some (ArchObj (ASIDPool x1)) \<Longrightarrow> state_refs_of s x = state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) x proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_asid_pool_zombies_state_hyp_refs [wp]:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>" unfolding set_asid_pool_def including unfold_objects apply (wpsimp wp: set_object_wp_strong
              simp: a_type_def) apply (erule rsubst [where P=P], rule ext) apply (simp add: state_hyp_refs_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x1. \<lbrakk>P (state_hyp_refs_of s); kheap s p = Some (ArchObj (ASIDPool x1))\<rbrakk> \<Longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x. kheap s p = Some (ArchObj (ASIDPool x1)) \<Longrightarrow> state_hyp_refs_of s x = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool ap))\<rparr>) x proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_asid_pool_cdt [wp]:
  "\<lbrace>\<lambda>s. P (cdt s)\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>" unfolding set_asid_pool_def including unfold_objects by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_valid_mdb [wp]:
  "\<lbrace>\<lambda>s. valid_mdb s\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. valid_mdb s\<rbrace>" including unfold_objects by (wpsimp wp: valid_mdb_lift simp: set_asid_pool_def set_object_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_mdb\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_valid_idle [wp]:
  "\<lbrace>\<lambda>s. valid_idle s\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. valid_idle s\<rbrace>" including unfold_objects by (wpsimp wp: valid_idle_lift simp: set_asid_pool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_idle\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_ifunsafe [wp]:
  "\<lbrace>\<lambda>s. if_unsafe_then_cap s\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. if_unsafe_then_cap s\<rbrace>" unfolding set_asid_pool_def including unfold_objects by (wpsimp wp: set_object_ifunsafe[THEN hoare_set_object_weaken_pre]
           simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_reply_caps [wp]:
  "\<lbrace>\<lambda>s. valid_reply_caps s\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. valid_reply_caps s\<rbrace>" by (wp valid_reply_caps_st_cte_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_reply_masters [wp]:
  "\<lbrace>valid_reply_masters\<rbrace>
   set_asid_pool p ap
   \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" by (wp valid_reply_masters_cte_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_valid_global [wp]:
  "\<lbrace>\<lambda>s. valid_global_refs s\<rbrace>
  set_asid_pool p ap
  \<lbrace>\<lambda>_ s. valid_global_refs s\<rbrace>" by (wp valid_global_refs_cte_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_global_refs\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_vspace_objs_unmap':
  "\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (ASIDPool ap) s) and
    obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace>
  set_asid_pool p ap \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" unfolding set_asid_pool_def including unfold_objects apply (wpsimp wp: set_object_vspace_objs simp: a_type_simps) apply (fastforce simp: vs_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (ASIDPool ap) s) and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (ASIDPool ap) s) and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (ASIDPool ap) s) and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace> set_object p (ArchObj (ASIDPool ap)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ap' a b. \<lbrakk>valid_vspace_objs s; (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>ran ap. \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory); kheap s p = Some (ArchObj (ASIDPool ap')); graph_of ap \<subseteq> graph_of ap'; (a, b) \<in> vs_refs (ArchObj (ASIDPool ap))\<rbrakk> \<Longrightarrow> (a, b) \<in> vs_refs (ArchObj (ASIDPool ap')) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_asid_pool_vspace_objs_unmap:
  "\<lbrace>valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>
  set_asid_pool p (ap |` S)  \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" apply (wp set_asid_pool_vspace_objs_unmap') apply (clarsimp simp: obj_at_def graph_of_restrict_map) apply (drule valid_vspace_objsD, simp add: obj_at_def, assumption) apply simp by (auto simp: obj_at_def dest!: ran_restrictD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and ako_at (ASIDPool ap) p\<rbrace> set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and ako_at (ASIDPool ap) p) s \<Longrightarrow> (valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (ASIDPool (ap |` S)) s) and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of (ap |` S) \<subseteq> graph_of ap') p) s proof (prove)
goal (1 subgoal):
 1. \<And>s x ref. \<lbrakk>valid_vspace_objs s; kheap s p = Some (ArchObj (ASIDPool ap)); x \<in> ran (ap |` S); (ref \<rhd> p) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory proof (prove)
goal (1 subgoal):
 1. \<And>s x ref. \<lbrakk>valid_vspace_objs s; kheap s p = Some (ArchObj (ASIDPool ap)); x \<in> ran (ap |` S); valid_vspace_obj (ASIDPool ap) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>valid_vspace_objs s; kheap s p = Some (ArchObj (ASIDPool ap)); x \<in> ran (ap |` S); \<forall>x\<in>ran ap. typ_at (AArch APageDirectory) x s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s x = Some ko \<and> a_type ko = AArch APageDirectory
theory ArchAcc_AI

lemma set_asid_pool_vs_lookup_unmap:
  "\<lbrace>valid_vs_lookup and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>
  set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>" apply (wp set_asid_pool_vs_lookup_unmap') by (clarsimp simp: obj_at_def
                 elim!: subsetD [OF graph_of_restrict_map])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and ako_at (ASIDPool ap) p\<rbrace> set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vs_lookup and ako_at (ASIDPool ap) p) s \<Longrightarrow> (valid_vs_lookup and obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of (ap |` S) \<subseteq> graph_of ap') p) s
theory ArchAcc_AI

lemma valid_pte_typ_at:
  "(\<And>T p. typ_at (AArch T) p s = typ_at (AArch T) p s') \<Longrightarrow>
   valid_pte pte s = valid_pte pte s'" by (case_tac pte, auto simp add: data_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>T p. typ_at (AArch T) p s = typ_at (AArch T) p s') \<Longrightarrow> valid_pte pte s = valid_pte pte s'
theory ArchAcc_AI

lemma valid_pde_typ_at:
  "(\<And>T p. typ_at (AArch T) p s = typ_at (AArch T) p s') \<Longrightarrow>
   valid_pde pde s = valid_pde pde s'" by (case_tac pde, auto simp add: data_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>T p. typ_at (AArch T) p s = typ_at (AArch T) p s') \<Longrightarrow> valid_pde pde s = valid_pde pde s'
theory ArchAcc_AI

lemma valid_vspace_obj_same_type:
  "\<lbrakk>valid_vspace_obj ao s;  kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk>
  \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ko')\<rparr>)" apply (rule hoare_to_pure_kheap_upd[OF valid_vspace_obj_typ]) by (auto simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow> valid_vspace_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> ko')\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>f pa T. \<lbrakk>valid_vspace_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko; \<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>r s. P (typ_at (AArch T) p s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>typ_at (AArch T) pa\<rbrace> f \<lbrace>\<lambda>_. typ_at (AArch T) pa\<rbrace>
 2. \<lbrakk>valid_vspace_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow> a_type ko' = a_type ?ko
 3. \<lbrakk>valid_vspace_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s
 4. \<lbrakk>valid_vspace_obj ao s; kheap s p = Some ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow> ko_at ?ko p s
theory ArchAcc_AI

lemma set_asid_pool_asid_map_unmap:
  "\<lbrace>valid_asid_map and ko_at (ArchObj (ASIDPool ap)) p and
    (\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow>
                ucast asid = x \<longrightarrow>
                arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
                arm_asid_map (arch_state s) asid = None)\<rbrace>
       set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" using set_asid_pool_restrict_asid_map[where S="- {x}"] by (simp add: restrict_map_def fun_upd_def if_flip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and ako_at (ASIDPool ap) p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid = x \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None)\<rbrace> set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
using this:
\<lbrace>valid_asid_map and ako_at (ASIDPool ?ap) ?p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid \<notin> - {x} \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some ?p \<longrightarrow> arm_asid_map (arch_state s) asid = None)\<rbrace> set_asid_pool ?p (?ap |` (- {x})) \<lbrace>\<lambda>_. valid_asid_map\<rbrace>

goal (1 subgoal):
 1. \<lbrace>valid_asid_map and ako_at (ASIDPool ap) p and (\<lambda>s. \<forall>asid\<le>mask local.asid_bits. UCAST(32 \<rightarrow> 10) asid = x \<longrightarrow> asid_table s (asid_high_bits_of asid) = Some p \<longrightarrow> arm_asid_map (arch_state s) asid = None)\<rbrace> set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_asid_map\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_vspace_objs_unmap_single:
  "\<lbrace>valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>
       set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" using set_asid_pool_vspace_objs_unmap[where S="- {x}"] by (simp add: restrict_map_def fun_upd_def if_flip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and ako_at (ASIDPool ap) p\<rbrace> set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
using this:
\<lbrace>valid_vspace_objs and ako_at (ASIDPool ?ap) ?p\<rbrace> set_asid_pool ?p (?ap |` (- {x})) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>

goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and ako_at (ASIDPool ap) p\<rbrace> set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_only_idle [wp]:
  "\<lbrace>only_idle\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. only_idle\<rbrace>" by (wp only_idle_lift set_asid_pool_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. only_idle\<rbrace>
theory ArchAcc_AI

lemma set_asid_pool_equal_mappings [wp]:
  "\<lbrace>equal_kernel_mappings\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" by (simp add: set_asid_pool_def | wp set_object_equal_mappings get_object_wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equal_kernel_mappings\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>