kings-crown/FVELER_Isabelle huggingface dataset:
theory CNode_AC

lemma auth_derived_mask_cap:
  "auth_derived cap cap' \<Longrightarrow> auth_derived (mask_cap R cap) cap'" using cap_rights_update_def acap_auth_conferred_acap_rights_update by (simp add: mask_cap_def split: cap.splits)
     (fastforce simp: cap_auth_conferred_def auth_derived_def
                      cap_rights_to_auth_def reply_cap_rights_to_auth_def
               split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. auth_derived cap cap' \<Longrightarrow> auth_derived (mask_cap R cap) cap' proof (prove)
using this:
cap_rights_update ?cr' ?cap \<equiv> case ?cap of EndpointCap oref badge cr \<Rightarrow> EndpointCap oref badge ?cr' | NotificationCap oref badge cr \<Rightarrow> NotificationCap oref badge (?cr' - {AllowGrant, AllowGrantReply}) | ReplyCap t m cr \<Rightarrow> ReplyCap t m (?cr' - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update ?cr' acap) | _ \<Rightarrow> ?cap
arch_cap_auth_conferred (acap_rights_update (acap_rights ?acap \<inter> ?R) ?acap) \<subseteq> arch_cap_auth_conferred ?acap

goal (1 subgoal):
 1. auth_derived cap cap' \<Longrightarrow> auth_derived (mask_cap R cap) cap'
theory CNode_AC

lemma auth_derived_update_cap_data:
  "\<lbrakk> auth_derived cap cap'; update_cap_data pres w cap \<noteq> NullCap \<rbrakk>
     \<Longrightarrow> auth_derived (update_cap_data pres w cap) cap'" apply (clarsimp simp: update_cap_data_def badge_update_def Let_def split_def
                        is_cap_simps auth_derived_arch_update_cap_data
                 split: if_split_asm) apply (simp_all add: auth_derived_def cap_auth_conferred_def the_cnode_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>auth_derived cap cap'; update_cap_data pres w cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> auth_derived (update_cap_data pres w cap) cap' proof (prove)
goal (3 subgoals):
 1. \<And>r R. \<lbrakk>auth_derived (EndpointCap r 0 R) cap'; cap = EndpointCap r 0 R; \<not> pres\<rbrakk> \<Longrightarrow> auth_derived (EndpointCap r (w && mask badge_bits) R) cap'
 2. \<And>r R. \<lbrakk>auth_derived (NotificationCap r 0 R) cap'; cap = NotificationCap r 0 R; \<not> pres\<rbrakk> \<Longrightarrow> auth_derived (NotificationCap r (w && mask badge_bits) R) cap'
 3. \<And>r bits g. \<lbrakk>auth_derived (CNodeCap r bits g) cap'; cap = CNodeCap r bits g; \<not> word_bits < unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits) + fst (snd (the_cnode_cap (CNodeCap r bits g)))\<rbrakk> \<Longrightarrow> (cap_ep_badge (CNodeCap r bits g) = 0 \<and> \<not> pres \<longrightarrow> auth_derived (CNodeCap (fst (the_cnode_cap (CNodeCap r bits g))) (fst (snd (the_cnode_cap (CNodeCap r bits g)))) (drop (size ((w >> cnode_padding_bits + cnode_guard_size_bits) && mask 18) - unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits)) (to_bl ((w >> cnode_padding_bits + cnode_guard_size_bits) && mask 18)))) cap') \<and> ((cap_ep_badge (CNodeCap r bits g) = 0 \<longrightarrow> pres) \<longrightarrow> auth_derived (CNodeCap (fst (the_cnode_cap (CNodeCap r bits g))) (fst (snd (the_cnode_cap (CNodeCap r bits g)))) (drop (size ((w >> cnode_padding_bits + cnode_guard_size_bits) && mask 18) - unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits)) (to_bl ((w >> cnode_padding_bits + cnode_guard_size_bits) && mask 18)))) cap') proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma cte_wp_at_auth_derived_mask_cap_strg:
  "cte_wp_at (auth_derived cap) p s
   \<longrightarrow> cte_wp_at (auth_derived (mask_cap R cap)) p s" by (clarsimp simp: cte_wp_at_caps_of_state auth_derived_mask_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (auth_derived cap) p s \<longrightarrow> cte_wp_at (auth_derived (mask_cap R cap)) p s
theory CNode_AC

lemma cte_wp_at_auth_derived_update_cap_data_strg:
  "cte_wp_at (auth_derived cap) p s \<and> update_cap_data pres w cap \<noteq> NullCap
   \<longrightarrow> cte_wp_at (auth_derived (update_cap_data pres w cap)) p s" by (clarsimp simp: cte_wp_at_caps_of_state auth_derived_update_cap_data)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (auth_derived cap) p s \<and> update_cap_data pres w cap \<noteq> NullCap \<longrightarrow> cte_wp_at (auth_derived (update_cap_data pres w cap)) p s
theory CNode_AC

lemma get_cap_auth_derived:
  "\<lbrace>\<top>\<rbrace> get_cap slot \<lbrace>\<lambda>rv. cte_wp_at (auth_derived rv) slot\<rbrace>" apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state auth_derived_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap slot \<lbrace>\<lambda>rv. cte_wp_at (auth_derived rv) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cte_wp_at (auth_derived cap) slot s proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma derive_cap_obj_refs_auth:
  "\<lbrace>\<lambda>s :: det_ext state. (\<forall>r\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. aag_has_auth_to aag auth r)\<rbrace>
   derive_cap slot cap
   \<lbrace>\<lambda>x s. (\<forall>r\<in>obj_refs_ac x. \<forall>auth\<in>cap_auth_conferred x. aag_has_auth_to aag auth r) \<rbrace>, -" by (wpsimp wp: arch_derive_cap_obj_refs_auth simp: derive_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag\<rbrace> derive_cap slot cap \<lbrace>\<lambda>x s. \<forall>r\<in>obj_refs_ac x. \<forall>auth\<in>cap_auth_conferred x. (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag\<rbrace>, -
theory CNode_AC

lemma derive_cap_cli:
  "\<lbrace>K (cap_links_irq aag l cap)\<rbrace>
   derive_cap slot cap
   \<lbrace>\<lambda>x s :: det_ext state. cap_links_irq aag l x\<rbrace>, -" unfolding derive_cap_def apply (rule hoare_pre) apply (wp arch_derive_cap_cli | wpc | simp add: comp_def cli_no_irqs)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (cap_links_irq aag l cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>x s. cap_links_irq aag l x\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (cap_links_irq aag l cap)\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>x s. cap_links_irq aag l x\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap \<lbrace>\<lambda>x s. cap_links_irq aag l x\<rbrace>, -
 2. \<And>s. K (cap_links_irq aag l cap) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. cap_links_irq aag l cap \<Longrightarrow> \<forall>x. cap = IRQHandlerCap x \<longrightarrow> cap_links_irq aag l (IRQHandlerCap x) proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma derive_cap_cap_cur_auth [wp]:
  "\<lbrace>\<lambda>s :: det_ext state. pas_cap_cur_auth aag cap\<rbrace>
   derive_cap slot cap
   \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag rv\<rbrace>, -" unfolding aag_cap_auth_def apply (rule hoare_pre) apply (wp derive_cap_aag_caps) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pas_cap_cur_auth aag cap\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. pas_cap_cur_auth aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) cap \<and> cap_links_irq aag (pasSubject aag) cap\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. (\<forall>x\<in>obj_refs_ac rv. \<forall>auth\<in>cap_auth_conferred rv. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range rv. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) rv \<and> cap_links_irq aag (pasSubject aag) rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. (\<forall>x\<in>obj_refs_ac rv. \<forall>auth\<in>cap_auth_conferred rv. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range rv. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) rv \<and> cap_links_irq aag (pasSubject aag) rv\<rbrace>, -
 2. \<And>s. (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) cap \<and> cap_links_irq aag (pasSubject aag) cap \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) cap \<and> cap_links_irq aag (pasSubject aag) cap \<Longrightarrow> (\<forall>r\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag r) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) cap \<and> K (cap_links_irq aag (pasSubject aag) cap) s proof (prove)
goal:
No subgoals!
theory CNode_AC

lemma update_cap_obj_refs_subset:
  "x \<in> obj_refs_ac (update_cap_data P dt cap) \<Longrightarrow> x \<in> obj_refs_ac cap" by (cases cap; simp add: update_cap_data_closedform arch_update_cap_obj_refs_subset split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> obj_refs_ac (update_cap_data P dt cap) \<Longrightarrow> x \<in> obj_refs_ac cap
theory CNode_AC

lemma update_cap_untyped_range_subset:
  "x \<in> untyped_range (update_cap_data P dt cap) \<Longrightarrow> x \<in> untyped_range cap" by (cases cap; simp add: update_cap_data_closedform split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> untyped_range (update_cap_data P dt cap) \<Longrightarrow> x \<in> untyped_range cap
theory CNode_AC

lemma P_0_1_spec:
  "\<lbrakk> (\<forall>x < length xs. P x); 2 \<le> length xs \<rbrakk> \<Longrightarrow> P 0 \<and> P 1" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x<length xs. P x; 2 \<le> length xs\<rbrakk> \<Longrightarrow> P 0 \<and> P 1
theory CNode_AC

lemma clas_update_cap_data [simp]:
  "cap_links_asid_slot aag p (update_cap_data pres w cap) = cap_links_asid_slot aag p cap" unfolding cap_links_asid_slot_def update_cap_data_closedform by (cases cap) (auto simp: arch_update_cap_links_asid_slot[simplified cap_links_asid_slot_def])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_links_asid_slot aag p (update_cap_data pres w cap) = cap_links_asid_slot aag p cap proof (prove)
goal (1 subgoal):
 1. (\<forall>asid\<in>cap_asid' (case cap of NullCap \<Rightarrow> NullCap | UntypedCap x xa xb xc \<Rightarrow> UntypedCap x xa xb xc | EndpointCap r badge rights \<Rightarrow> if badge = 0 \<and> \<not> pres then EndpointCap r (w && mask badge_bits) rights else NullCap | NotificationCap r badge rights \<Rightarrow> if badge = 0 \<and> \<not> pres then NotificationCap r (w && mask badge_bits) rights else NullCap | ReplyCap x xa xb \<Rightarrow> ReplyCap x xa xb | CNodeCap r bits guard \<Rightarrow> if word_bits < fst (update_cnode_cap_data w) + bits then NullCap else CNodeCap r bits (drop (size (snd (update_cnode_cap_data w)) - fst (update_cnode_cap_data w)) (to_bl (snd (update_cnode_cap_data w)))) | ThreadCap x \<Rightarrow> ThreadCap x | DomainCap \<Rightarrow> DomainCap | IRQControlCap \<Rightarrow> IRQControlCap | IRQHandlerCap x \<Rightarrow> IRQHandlerCap x | Zombie x xa xb \<Rightarrow> Zombie x xa xb | ArchObjectCap x \<Rightarrow> arch_update_cap_data pres w x). label_owns_asid_slot aag p asid) = (\<forall>asid\<in>cap_asid' cap. label_owns_asid_slot aag p asid)
theory CNode_AC

lemma update_cap_cap_auth_conferred_subset:
  "x \<in> cap_auth_conferred (update_cap_data b w cap) \<Longrightarrow> x \<in> cap_auth_conferred cap" unfolding update_cap_data_def by (auto simp: is_cap_simps cap_auth_conferred_def cap_rights_to_auth_def badge_update_def
                 the_cnode_cap_def Let_def arch_update_cap_cap_auth_conferred_subset
          split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> cap_auth_conferred (update_cap_data b w cap) \<Longrightarrow> x \<in> cap_auth_conferred cap proof (prove)
goal (1 subgoal):
 1. x \<in> cap_auth_conferred (if is_ep_cap cap then if cap_ep_badge cap = 0 \<and> \<not> b then badge_update w cap else NullCap else if is_ntfn_cap cap then if cap_ep_badge cap = 0 \<and> \<not> b then badge_update w cap else NullCap else if is_cnode_cap cap then let (oref, bits, guard) = the_cnode_cap cap; (guard_size', guard'') = update_cnode_cap_data w; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap cap then arch_update_cap_data b w (the_arch_cap cap) else cap) \<Longrightarrow> x \<in> cap_auth_conferred cap
theory CNode_AC

lemma update_cap_cli:
  "cap_links_irq aag l (update_cap_data b w cap) = cap_links_irq aag l cap" unfolding update_cap_data_def by (cases cap, simp_all add: is_cap_simps cli_no_irqs badge_update_def the_cnode_cap_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_links_irq aag l (update_cap_data b w cap) = cap_links_irq aag l cap proof (prove)
goal (1 subgoal):
 1. cap_links_irq aag l (if is_ep_cap cap then if cap_ep_badge cap = 0 \<and> \<not> b then badge_update w cap else NullCap else if is_ntfn_cap cap then if cap_ep_badge cap = 0 \<and> \<not> b then badge_update w cap else NullCap else if is_cnode_cap cap then let (oref, bits, guard) = the_cnode_cap cap; (guard_size', guard'') = update_cnode_cap_data w; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap cap then arch_update_cap_data b w (the_arch_cap cap) else cap) = cap_links_irq aag l cap
theory CNode_AC

lemma untyped_range_update_cap_data [simp]:
  "untyped_range (update_cap_data b w c) = untyped_range c" unfolding update_cap_data_def by (cases c, simp_all add: is_cap_simps badge_update_def Let_def the_cnode_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_range (update_cap_data b w c) = untyped_range c proof (prove)
goal (1 subgoal):
 1. untyped_range (if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> b then badge_update w c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> b then badge_update w c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data w; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data b w (the_arch_cap c) else c) = untyped_range c
theory ArchCNode_AC

lemma sata_cdt_update[CNode_AC_assms, simp]:
  "state_asids_to_policy aag (cdt_update f s) = state_asids_to_policy aag s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy aag (cdt_update f s) = state_asids_to_policy aag s
theory ArchCNode_AC

lemma sata_is_original_cap_update[CNode_AC_assms, simp]:
  "state_asids_to_policy aag (is_original_cap_update f s) = state_asids_to_policy aag s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy aag (is_original_cap_update f s) = state_asids_to_policy aag s
theory ArchCNode_AC

lemma sata_interrupt_states_update[CNode_AC_assms, simp]:
  "state_asids_to_policy aag (interrupt_states_update f s) = state_asids_to_policy aag s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy aag (interrupt_states_update f s) = state_asids_to_policy aag s
theory ArchCNode_AC

lemma sata_machine_state_update[CNode_AC_assms, simp]:
  "state_asids_to_policy aag (machine_state_update f s) = state_asids_to_policy aag s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy aag (machine_state_update f s) = state_asids_to_policy aag s
theory ArchCNode_AC

lemma sata_update[CNode_AC_assms]:
  "\<lbrakk> pas_wellformed aag;
     cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap;
     state_asids_to_policy_arch aag caps as vrefs \<subseteq> pasPolicy aag \<rbrakk>
     \<Longrightarrow> state_asids_to_policy_arch aag (caps(ptr \<mapsto> cap)) as vrefs \<subseteq> pasPolicy aag" by (fastforce intro: state_asids_to_policy_aux.intros
                 elim!: state_asids_to_policy_aux.cases
                 simp: cap_links_asid_slot_def label_owns_asid_slot_def
                split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_wellformed aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; state_asids_to_policy_arch aag caps as vrefs \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> state_asids_to_policy_arch aag (caps(ptr \<mapsto> cap)) as vrefs \<subseteq> pasPolicy aag
theory ArchCNode_AC

lemma sata_update2[CNode_AC_assms]:
  "\<lbrakk> pas_wellformed aag;
     cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap;
     cap_links_asid_slot aag (pasObjectAbs aag (fst ptr')) cap';
     state_asids_to_policy_arch aag caps as vrefs \<subseteq> pasPolicy aag \<rbrakk>
     \<Longrightarrow> state_asids_to_policy_arch aag (caps(ptr \<mapsto> cap, ptr' \<mapsto> cap')) as vrefs \<subseteq> pasPolicy aag" by (fastforce intro: state_asids_to_policy_aux.intros
                elim!: state_asids_to_policy_aux.cases
                 simp: cap_links_asid_slot_def label_owns_asid_slot_def
                split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_wellformed aag; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr)) cap; cap_links_asid_slot aag (pasObjectAbs aag (fst ptr')) cap'; state_asids_to_policy_arch aag caps as vrefs \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> state_asids_to_policy_arch aag (caps(ptr \<mapsto> cap, ptr' \<mapsto> cap')) as vrefs \<subseteq> pasPolicy aag
theory ArchCNode_AC

lemma set_cap_state_vrefs[CNode_AC_assms, wp]:
  "set_cap cap ptr \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace>" apply (wpsimp wp: get_object_wp simp: set_cap_def split_def set_object_def) apply (auto simp: obj_at_def state_vrefs_def
             elim!: rsubst[where P=P, OF _ ext]
             split: if_split_asm simp: vs_refs_no_global_pts_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>_ s. P (state_vrefs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (state_vrefs s); ko_at ko (fst ptr) s\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = a_type (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> P (state_vrefs (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap s a\<rparr>)))) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (state_vrefs (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (state_vrefs (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (state_vrefs (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (state_vrefs (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (state_vrefs (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap s a\<rparr>)))))))) proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma state_vrefs_tcb_upd[CNode_AC_assms]:
  "tcb_at t s \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s" apply (rule ext) apply (auto simp: state_vrefs_def vs_refs_no_global_pts_def tcb_at_def dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at t s \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s proof (prove)
goal (1 subgoal):
 1. \<And>x. tcb_at t s \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) x = state_vrefs s x proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma state_vrefs_simple_type_upd[CNode_AC_assms]:
  "\<lbrakk> ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val) \<rbrakk>
     \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>) = state_vrefs s" apply (rule ext) apply (auto simp: state_vrefs_def vs_refs_no_global_pts_def obj_at_def partial_inv_def a_type_def
             split: kernel_object.splits arch_kernel_obj.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val)\<rbrakk> \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>) = state_vrefs s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ko_at ko ptr s; is_simple_type ko; a_type ko = a_type (f val)\<rbrakk> \<Longrightarrow> state_vrefs (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f val)\<rparr>) x = state_vrefs s x proof (prove)
goal:
No subgoals!
theory ArchCNode_AC

lemma a_type_arch_object_not_tcb[CNode_AC_assms, simp]:
  "a_type (ArchObj arch_kernel_obj) \<noteq> ATCB" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a_type (ArchObj arch_kernel_obj) \<noteq> ATCB