kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_AI

lemma set_asid_pool_distinct [wp]:
  "set_asid_pool p ptr \<lbrace>pspace_distinct\<rbrace>" apply (simp add: set_asid_pool_def) including unfold_objects by (wpsimp wp: set_object_wp_strong pspace_distinct_same_type)

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

lemma store_pde_arch [wp]:
  "\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> store_pde p pde \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>" by (simp add: store_pde_def set_pd_def get_object_def) wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> store_pde p pde \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>
theory ArchAcc_AI

lemma store_pte_valid_pte [wp]:
  "\<lbrace>valid_pte pt\<rbrace> store_pte p pte \<lbrace>\<lambda>_. valid_pte pt\<rbrace>" by (wp valid_pte_lift store_pte_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pte pt\<rbrace> store_pte p pte \<lbrace>\<lambda>_. valid_pte pt\<rbrace>
theory ArchAcc_AI

lemma store_pde_valid_pde [wp]:
  "\<lbrace>valid_pde pde\<rbrace> store_pde slot pde' \<lbrace>\<lambda>rv. valid_pde pde\<rbrace>" by (wp valid_pde_lift store_pde_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde pde\<rbrace> store_pde slot pde' \<lbrace>\<lambda>rv. valid_pde pde\<rbrace>
theory ArchAcc_AI

lemma set_pd_typ_at [wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_pd ptr pd \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" apply (simp add: set_pd_def) by (wpsimp wp: set_object_wp_strong simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_pd ptr pd \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_object ptr (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>
theory ArchAcc_AI

lemma set_pd_valid_objs:
  "\<lbrace>(%s. \<forall>i. wellformed_pde (pd i)) and valid_objs\<rbrace>
   set_pd p pd
   \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: set_pd_def) by (wpsimp wp: set_object_valid_objs simp: valid_obj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>i. wellformed_pde (pd i)) and valid_objs\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>i. wellformed_pde (pd i)) and valid_objs\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_. valid_objs\<rbrace>
theory ArchAcc_AI

lemma set_pd_iflive:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap s\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_ s. if_live_then_nonz_cap s\<rbrace>" apply (subst set_pd_def) including unfold_objects by (wpsimp wp: set_object_iflive[THEN hoare_set_object_weaken_pre]
           simp: live_def hyp_live_def a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> set_pd p pd \<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 (PageDirectory pd)) \<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 (PageDirectory pd)) \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>
theory ArchAcc_AI

lemma set_pd_zombies:
  "\<lbrace>\<lambda>s. zombies_final s\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_ s. zombies_final s\<rbrace>" apply (subst set_pd_def) apply (wp set_object_zombies[THEN hoare_set_object_weaken_pre]) including unfold_objects by (clarsimp simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_pd p pd \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (PageDirectory pd)) = a_type ko \<longrightarrow> (zombies_final and obj_at (same_caps (ArchObj (PageDirectory pd))) p) s proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (PageDirectory pd)) = a_type ko \<longrightarrow> (zombies_final and obj_at (same_caps (ArchObj (PageDirectory pd))) p) s
theory ArchAcc_AI

lemma set_pd_zombies_state_refs:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace>" apply (subst set_pd_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_refs_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> set_pd p pd \<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 (PageDirectory pd)) \<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 (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>P (state_refs_of s); kheap s p = Some (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> P (state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x. kheap s p = Some (ArchObj (PageDirectory x3)) \<Longrightarrow> state_refs_of s x = state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) x proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_zombies_state_hyp_refs:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>" apply (subst set_pd_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_pd p pd \<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 (PageDirectory pd)) \<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 (PageDirectory pd)) \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>P (state_hyp_refs_of s); kheap s p = Some (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x3 x. kheap s p = Some (ArchObj (PageDirectory x3)) \<Longrightarrow> state_hyp_refs_of s x = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>) x proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_cdt:
  "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>" unfolding set_pd_def by (wpsimp wp: get_object_wp)

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

lemma set_pd_valid_mdb:
  "\<lbrace>\<lambda>s. valid_mdb s\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_ s. valid_mdb s\<rbrace>" apply (rule valid_mdb_lift) by (wpsimp wp: set_pd_cdt set_object_wp simp: set_pd_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace>
theory ArchAcc_AI

lemma set_pd_valid_idle:
  "\<lbrace>\<lambda>s. valid_idle s\<rbrace> set_pd p pd \<lbrace>\<lambda>_ s. valid_idle s\<rbrace>" by (wpsimp wp: valid_idle_lift set_object_wp simp: set_pd_def)

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

lemma set_pd_ifunsafe:
  "\<lbrace>\<lambda>s. if_unsafe_then_cap s\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_ s. if_unsafe_then_cap s\<rbrace>" unfolding set_pd_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_pd p pd \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace>
theory ArchAcc_AI

lemma set_pd_reply_caps:
  "\<lbrace>\<lambda>s. valid_reply_caps s\<rbrace>
  set_pd p pd
  \<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_pd p pd \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory ArchAcc_AI

lemma set_pd_reply_masters:
  "\<lbrace>valid_reply_masters\<rbrace>
   set_pd p pd
   \<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_pd p pd \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>
theory ArchAcc_AI

lemma global_refs_kheap [simp]:
  "global_refs (kheap_update f s) = global_refs s" by (simp add: global_refs_def)

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

lemma set_pd_valid_arch:
  "\<lbrace>\<lambda>s. valid_arch_state s\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_ s. valid_arch_state s\<rbrace>" by (wp valid_arch_state_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
theory ArchAcc_AI

lemma set_pd_cur:
  "\<lbrace>\<lambda>s. cur_tcb s\<rbrace>
  set_pd p pd
  \<lbrace>\<lambda>_ s. cur_tcb s\<rbrace>" apply (simp add: cur_tcb_def set_pd_def) including unfold_objects apply (wpsimp wp: set_object_wp_strong simp: a_type_simps) apply (simp add: is_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> set_pd p pd \<lbrace>\<lambda>_. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (cur_thread s) s\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. tcb_at (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (cur_thread s) s\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>_ s. tcb_at (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>is_tcb ko; p = cur_thread s; kheap s (cur_thread s) = Some ko; AArch APageDirectory = a_type ko\<rbrakk> \<Longrightarrow> is_tcb (ArchObj (PageDirectory pd)) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_vspace_objs_unmap:
  "\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd') s) and
    obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p\<rbrace>
  set_pd p pd' \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" apply (simp add: set_pd_def) apply (wpsimp wp: set_object_vspace_objs[THEN hoare_set_object_weaken_pre]) including unfold_objects apply (clarsimp simp: a_type_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 (PageDirectory pd') s) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p\<rbrace> set_pd p pd' \<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> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd' x) s)) and obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p\<rbrace> set_object p (ArchObj (PageDirectory pd')) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_vspace_objs s; (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd' x) s); obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p s; ko_at ko p s; a_type (ArchObj (PageDirectory pd')) = a_type ko\<rbrakk> \<Longrightarrow> typ_at (a_type ko) p s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_vspace_objs s; (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x\<in>- kernel_mapping_slots. valid_pde (pd' x) s); obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p s; ko_at ko p s; a_type (ArchObj (PageDirectory pd')) = a_type ko\<rbrakk> \<Longrightarrow> typ_at (a_type ko) p s proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_typ_at [wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_pt ptr pt \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" apply (simp add: set_pt_def) by (wpsimp wp: set_object_wp_strong simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_pt ptr pt \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_object ptr (ArchObj (PageTable pt)) \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>
theory ArchAcc_AI

lemma set_pt_valid_objs:
  "\<lbrace>(%s. \<forall>i. wellformed_pte (pt i)) and valid_objs\<rbrace>
   set_pt p pt
   \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: set_pt_def) apply (wp set_object_valid_objs) apply (clarsimp split: kernel_object.splits
                         arch_kernel_obj.splits) apply (clarsimp simp: valid_obj_def obj_at_def a_type_def
                        arch_valid_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>i. wellformed_pte (pt i)) and valid_objs\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>i. wellformed_pte (pt i)) and valid_objs\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>i. wellformed_pte (pt i)) and valid_objs) s \<Longrightarrow> (valid_objs and valid_obj p (ArchObj (PageTable pt))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>i. wellformed_pte (pt i); valid_objs s\<rbrakk> \<Longrightarrow> valid_obj p (ArchObj (PageTable pt)) s proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_iflive:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap s\<rbrace>
  set_pt p pt
  \<lbrace>\<lambda>_ s. if_live_then_nonz_cap s\<rbrace>" unfolding set_pt_def including unfold_objects apply (wpsimp wp: set_object_iflive[THEN hoare_set_object_weaken_pre]
              simp: live_def hyp_live_def a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> set_pt p pt \<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 (PageTable pt)) \<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 (PageTable pt)) \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_zombies:
  "\<lbrace>\<lambda>s. zombies_final s\<rbrace>
  set_pt p pt
  \<lbrace>\<lambda>_ s. zombies_final s\<rbrace>" unfolding set_pt_def including unfold_objects apply (wpsimp wp: set_object_zombies[THEN hoare_set_object_weaken_pre]
              simp: a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_pt p pt \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. zombies_final\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_zombies_state_refs:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
  set_pt p pt
  \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace>" unfolding set_pt_def including unfold_objects apply (wpsimp wp: set_object_wp_strong simp: a_type_def) apply (erule rsubst [where P=P]) apply (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_pt p pt \<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 (PageTable pt)) \<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 (PageTable pt)) \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>P (state_refs_of s); kheap s p = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> P (state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> state_refs_of s = state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> state_refs_of s x = state_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) x proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_zombies_state_hyp_refs:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
  set_pt p pt
  \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>" unfolding set_pt_def including unfold_objects apply (wpsimp wp: set_object_wp_strong simp: a_type_def) apply (erule rsubst [where P=P]) apply (rule ext) apply (clarsimp simp: 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_pt p pt \<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 (PageTable pt)) \<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 (PageTable pt)) \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>P (state_hyp_refs_of s); kheap s p = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> state_hyp_refs_of s = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x. kheap s p = Some (ArchObj (PageTable x2)) \<Longrightarrow> state_hyp_refs_of s x = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) x proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_cdt:
  "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_pt p pt \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>" unfolding set_pt_def including unfold_objects by wpsimp

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

lemma set_pt_valid_mdb:
  "\<lbrace>\<lambda>s. valid_mdb s\<rbrace> set_pt p pt \<lbrace>\<lambda>_ s. valid_mdb s\<rbrace>" including unfold_objects by (wpsimp wp: set_pt_cdt valid_mdb_lift simp: set_pt_def set_object_def)

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

lemma set_pt_valid_idle:
  "\<lbrace>\<lambda>s. valid_idle s\<rbrace> set_pt p pt \<lbrace>\<lambda>_ s. valid_idle s\<rbrace>" including unfold_objects by (wpsimp wp: valid_idle_lift simp: set_pt_def)

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

lemma set_pt_ifunsafe:
  "\<lbrace>\<lambda>s. if_unsafe_then_cap s\<rbrace> set_pt p pt \<lbrace>\<lambda>_ s. if_unsafe_then_cap s\<rbrace>" including unfold_objects by (wpsimp wp: set_object_ifunsafe[THEN hoare_set_object_weaken_pre]
                                    simp: set_pt_def a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_pt p pt \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_pt p pt \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace>
theory ArchAcc_AI

lemma set_pt_reply_caps:
  "\<lbrace>\<lambda>s. valid_reply_caps s\<rbrace> set_pt p pt \<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_pt p pt \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory ArchAcc_AI

lemma set_pt_reply_masters:
  "\<lbrace>valid_reply_masters\<rbrace>  set_pt p pt  \<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_pt p pt \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>