kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchCNode_AC

lemma arch_post_cap_deletion_cur_domain[CNode_AC_assms, wp]:
  "arch_post_cap_deletion acap \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> arch_post_cap_deletion acap \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
theory ArchCNode_AC

lemma arch_post_cap_deletion_integrity[CNode_AC_assms]:
  "arch_post_cap_deletion acap \<lbrace>integrity aag X st\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> arch_post_cap_deletion acap \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchCNode_AC

lemma integrity_asids_set_cap_Nullcap[CNode_AC_assms]:
  "\<lbrace>(=) s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity_asids aag subjects x a s\<rbrace>" unfolding integrity_asids_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity_asids aag subjects x a s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_ s'. asid_table s (asid_high_bits_of a) = asid_table s' (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> pasASIDAbs aag asid' \<in> subjects)\<rbrace>
theory ArchCNode_AC

lemma arch_post_cap_deletion_pas_refined[CNode_AC_assms, wp]:
  "arch_post_cap_deletion irqopt \<lbrace>pas_refined aag\<rbrace>" by (wpsimp simp: post_cap_deletion_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> arch_post_cap_deletion irqopt \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory ArchCNode_AC

lemma aobj_ref'_same_aobject[CNode_AC_assms]:
  "same_aobject_as ao' ao \<Longrightarrow> aobj_ref' ao = aobj_ref' ao'" by (cases ao; clarsimp split: arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_aobject_as ao' ao \<Longrightarrow> aobj_ref' ao = aobj_ref' ao'
theory ArchCNode_AC

lemma pas_refined_tcb_domain_map_wellformed[CNode_AC_assms, wp]:
  assumes tdmw: "f \<lbrace>tcb_domain_map_wellformed aag\<rbrace>"
  shows "f \<lbrace>pas_refined aag\<rbrace>" apply (simp add: pas_refined_def) apply (wp tdmw) apply (wp lift_inv) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> f \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrace> f \<lbrace>\<lambda>_ s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'12\<rbrace> f \<lbrace>\<lambda>rv s. state_objs_in_policy aag s \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrace>
 2. \<And>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag \<Longrightarrow> pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> ?P'12 s proof (prove)
goal (2 subgoals):
 1. \<And>s g. (state_objs_in_policy aag (trans_state g s) \<and> state_asids_to_policy_aux aag (caps_of_state (trans_state g s)) (asid_table (trans_state g s)) (state_vrefs (trans_state g s)) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag (trans_state g s) \<subseteq> pasPolicy aag) = (state_objs_in_policy aag s \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag)
 2. \<And>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag \<Longrightarrow> pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma cap_asid'_cap_rights_update[CNode_AC_assms, simp]:
  "acap_asid' (acap_rights_update rights ao) = acap_asid' ao" by (cases ao; clarsimp simp: cap_rights_update_def acap_rights_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. acap_asid' (acap_rights_update rights ao) = acap_asid' ao
theory ArchCNode_AC

lemma untyped_range_cap_rights_update[CNode_AC_assms, simp]:
  "untyped_range (cap_rights_update rights (ArchObjectCap ao)) = untyped_range (ArchObjectCap ao)" by (cases ao; clarsimp simp: cap_rights_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_range (cap_rights_update rights (ArchObjectCap ao)) = untyped_range (ArchObjectCap ao)
theory ArchCNode_AC

lemma auth_derived_arch_update_cap_data[CNode_AC_assms]:
  "auth_derived (ArchObjectCap ao) cap' \<Longrightarrow> auth_derived (arch_update_cap_data pres w ao) cap'" by (simp add: update_cap_data_def is_cap_simps arch_update_cap_data_def
                  split del: if_split cong: if_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. auth_derived (ArchObjectCap ao) cap' \<Longrightarrow> auth_derived (arch_update_cap_data pres w ao) cap'
theory ArchCNode_AC

lemma acap_auth_conferred_acap_rights_update[CNode_AC_assms]:
  "arch_cap_auth_conferred (acap_rights_update (acap_rights acap \<inter> R) acap)
   \<subseteq> arch_cap_auth_conferred acap" by (auto simp: arch_cap_auth_conferred_def vspace_cap_rights_to_auth_def acap_rights_update_def
                 validate_vm_rights_def vm_kernel_only_def vm_read_only_def
          split: arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_cap_auth_conferred (acap_rights_update (acap_rights acap \<inter> R) acap) \<subseteq> arch_cap_auth_conferred acap
theory ArchCNode_AC

lemma arch_derive_cap_clas[CNode_AC_assms]:
  "\<lbrace>\<lambda>s. cap_links_asid_slot aag p (ArchObjectCap acap)\<rbrace>
   arch_derive_cap acap
   \<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, -" apply (simp add: arch_derive_cap_def cong: cap.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ apply (auto simp: is_cap_simps cap_links_asid_slot_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_links_asid_slot aag p (ArchObjectCap acap)\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_links_asid_slot aag p (ArchObjectCap acap)\<rbrace> case acap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap acap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap acap) | _ \<Rightarrow> returnOk (ArchObjectCap acap) \<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case acap of PageCap dev r R pgs x \<Rightarrow> returnOk (ArchObjectCap (PageCap dev r R pgs None)) | PageTableCap xa None \<Rightarrow> throwError IllegalOperation | PageTableCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap acap) | PageDirectoryCap xa None \<Rightarrow> throwError IllegalOperation | PageDirectoryCap xa (Some x) \<Rightarrow> returnOk (ArchObjectCap acap) | _ \<Rightarrow> returnOk (ArchObjectCap acap) \<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, -
 2. \<And>s. cap_links_asid_slot aag p (ArchObjectCap acap) \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_links_asid_slot aag p (ArchObjectCap acap) \<Longrightarrow> (\<forall>x xa. acap = ASIDPoolCap x xa \<longrightarrow> cap_links_asid_slot aag p (ArchObjectCap acap)) \<and> (acap = ASIDControlCap \<longrightarrow> cap_links_asid_slot aag p (ArchObjectCap acap)) \<and> (\<forall>x xa xb xc xd. acap = PageCap x xa xb xc xd \<longrightarrow> cap_links_asid_slot aag p (ArchObjectCap (PageCap x xa xb xc None))) \<and> (\<forall>x xa. acap = PageTableCap x xa \<longrightarrow> (xa = None \<longrightarrow> True) \<and> (\<forall>x. xa = Some x \<longrightarrow> cap_links_asid_slot aag p (ArchObjectCap acap))) \<and> (\<forall>x xa. acap = PageDirectoryCap x xa \<longrightarrow> (xa = None \<longrightarrow> True) \<and> (\<forall>x. xa = Some x \<longrightarrow> cap_links_asid_slot aag p (ArchObjectCap acap))) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma arch_derive_cap_clip[CNode_AC_assms]:
  "\<lbrace>K (cap_links_irq aag l (ArchObjectCap ac))\<rbrace>
   arch_derive_cap ac
   \<lbrace>\<lambda>x s. cap_links_irq aag l x\<rbrace>, -" by (wpsimp simp: arch_derive_cap_def comp_def cli_no_irqs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (cap_links_irq aag l (ArchObjectCap ac))\<rbrace> arch_derive_cap ac \<lbrace>\<lambda>x s. cap_links_irq aag l x\<rbrace>, -
theory ArchCNode_AC

lemma arch_update_cap_untyped_range_empty[CNode_AC_assms, simp]:
  "untyped_range (arch_update_cap_data pres data cap) = {}" by (simp add: arch_update_cap_data_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_range (arch_update_cap_data pres data cap) = {}
theory ArchCNode_AC

lemma arch_update_cap_irqs_controlled_empty[CNode_AC_assms, simp]:
  "cap_irqs_controlled (arch_update_cap_data pres data cap) = {}" by (simp add: arch_update_cap_data_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_irqs_controlled (arch_update_cap_data pres data cap) = {}
theory ArchCNode_AC

lemma arch_update_cap_links_asid_slot[CNode_AC_assms]:
  "cap_links_asid_slot aag p (arch_update_cap_data pres w acap) =
   cap_links_asid_slot aag p (ArchObjectCap acap)" by (simp add: arch_update_cap_data_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_links_asid_slot aag p (arch_update_cap_data pres w acap) = cap_links_asid_slot aag p (ArchObjectCap acap)
theory ArchCNode_AC

lemma arch_update_cap_cap_auth_conferred_subset[CNode_AC_assms]:
  "y \<in> cap_auth_conferred (arch_update_cap_data b w acap) \<Longrightarrow> y \<in> arch_cap_auth_conferred acap" by (simp add: arch_update_cap_data_def cap_auth_conferred_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<in> cap_auth_conferred (arch_update_cap_data b w acap) \<Longrightarrow> y \<in> arch_cap_auth_conferred acap
theory ArchCNode_AC

lemma pas_refined_arch_state_update_not_asids[simp]:
 "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s)
  \<Longrightarrow> pas_refined aag (arch_state_update f s) = pas_refined aag s" by (simp add: pas_refined_def state_objs_to_policy_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> pas_refined aag (arch_state_update f s) = pas_refined aag s
theory ArchCNode_AC

lemma store_pte_state_refs[wp]:
  "store_pte p pte \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>" apply (simp add: store_pte_def set_pt_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: obj_at_def state_refs_of_def
                 elim!: rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> store_pte p pte \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> do pt <- get_pt (p && ~~ mask pt_bits);
kobj <- get_object (p && ~~ mask pt_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>)
od \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_refs_of s) \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pt_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) \<longrightarrow> P (state_refs_of (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>))) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma all_rsubst:
  "\<lbrakk> \<forall>v. P (f v); \<exists>v. f v = r \<rbrakk> \<Longrightarrow> P r" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>v. P (f v); \<exists>v. f v = r\<rbrakk> \<Longrightarrow> P r
theory ArchCNode_AC

lemma store_pte_thread_st_auth[wp]:
  "store_pte p pte \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" apply (simp add: store_pte_def set_pt_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: thread_st_auth_def obj_at_def get_tcb_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> store_pte p pte \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> do pt <- get_pt (p && ~~ mask pt_bits);
kobj <- get_object (p && ~~ mask pt_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>)
od \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (thread_st_auth s) \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pt_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) \<longrightarrow> P (thread_st_auth (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>))) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma store_pte_thread_bound_ntfns[wp]:
  "store_pte p pte \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace>" apply (simp add: store_pte_def set_pt_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: thread_bound_ntfns_def obj_at_def get_tcb_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> store_pte p pte \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> do pt <- get_pt (p && ~~ mask pt_bits);
kobj <- get_object (p && ~~ mask pt_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>)
od \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (thread_bound_ntfns s) \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pt_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)))) \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(p && ~~ mask pt_bits \<mapsto> ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))\<rparr>))) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma auth_graph_map_def2:
  "auth_graph_map f S = (\<lambda>(x, auth, y). (f x, auth, f y)) ` S" by (auto simp add: auth_graph_map_def image_def intro: rev_bexI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. auth_graph_map f S = (\<lambda>(x, auth, y). (f x, auth, f y)) ` S
theory ArchCNode_AC

lemma store_pte_ekheap[wp]:
  "store_pte p pte \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>" apply (simp add: store_pte_def set_pt_def) apply (wp get_object_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> store_pte p pte \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> do pt <- get_pt (p && ~~ mask pt_bits);
set_object (p && ~~ mask pt_bits) (ArchObj (PageTable (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))))
od \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ekheap s) \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> P (ekheap s) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma store_pde_thread_st_auth[wp]:
  "store_pde p pde \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: thread_st_auth_def obj_at_def get_tcb_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> store_pde p pde \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_st_auth s)\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
kobj <- get_object (p && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>)
od \<lbrace>\<lambda>_ s. P (thread_st_auth s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (thread_st_auth s) \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<longrightarrow> P (thread_st_auth (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>))) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma store_pde_thread_bound_ntfns[wp]:
  "store_pde p pde \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: thread_bound_ntfns_def obj_at_def get_tcb_def tcb_states_of_state_def
                 elim!: rsubst[where P=P, OF _ ext]
                 split: kernel_object.split_asm option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> store_pde p pde \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
kobj <- get_object (p && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>)
od \<lbrace>\<lambda>_ s. P (thread_bound_ntfns s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (thread_bound_ntfns s) \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (p && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde)))) \<longrightarrow> P (thread_bound_ntfns (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>))) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma set_asid_pool_st_vrefs[wp]:
  "\<lbrace>\<lambda>s. P ((state_vrefs s) (p := (\<lambda>(r, p). (p, ucast r, AASIDPool, Control)) ` graph_of pool))\<rbrace>
   set_asid_pool p pool
   \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>" apply (simp add: set_asid_pool_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp: state_vrefs_def fun_upd_def[symmetric] fun_upd_comp obj_at_def
                        vs_refs_no_global_pts_def
                 split: kernel_object.split_asm arch_kernel_obj.split_asm
                 elim!: rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_vrefs s)(p := (\<lambda>(r, p). (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool))\<rbrace> set_asid_pool p pool \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_vrefs s)(p := (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool))\<rbrace> do kobj <- get_object p;
y <- assert (a_type kobj = a_type (ArchObj (ASIDPool pool)));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool pool))\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((state_vrefs s)(p := (\<lambda>x. case x of (r, p) \<Rightarrow> (p, UCAST(10 \<rightarrow> 32) r, AASIDPool, Control)) ` graph_of pool)) \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type ko = a_type (ArchObj (ASIDPool pool)) \<longrightarrow> P (state_vrefs (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (ASIDPool pool))\<rparr>)) proof (prove)
goal:
No subgoals!