kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchArch_IF

lemma delete_asid_valid_vspace_objs[wp]:
  "\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace>
   delete_asid a b
   \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" unfolding delete_asid_def apply (wpsimp wp: set_asid_pool_vspace_objs_unmap'') apply (fastforce simp: restrict_eq_asn_none) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> delete_asid a b \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of a) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) a) = Some b) $ do flush_space a;
invalidate_asid_entry a;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) a := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od
od \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x pool. \<lbrakk>valid_vspace_objs s; pspace_aligned s; asid_table s (asid_high_bits_of a) = Some x; pool (UCAST(32 \<rightarrow> 10) a) = Some b; ako_at (ASIDPool pool) x s\<rbrakk> \<Longrightarrow> ako_at (ASIDPool (?ap65 (asid_table s) x pool (pool(UCAST(32 \<rightarrow> 10) a := None)))) x s \<and> pool(UCAST(32 \<rightarrow> 10) a := None) = ?ap65 (asid_table s) x pool (pool(UCAST(32 \<rightarrow> 10) a := None)) |` ?S71 (asid_table s) x pool (pool(UCAST(32 \<rightarrow> 10) a := None)) proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma pd_bits_store_pde_helper:
  "\<lbrakk> xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits \<rbrakk>
     \<Longrightarrow> ((xa << 2) + word && ~~ mask pd_bits) = word" apply (clarsimp simp: field_simps) apply (subst is_aligned_add_helper) apply simp apply (rule shiftl_less_t2n) apply (erule order_le_less_trans) apply (simp add: kernel_base_def  pd_bits_def pageBits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> (xa << 2) + word && ~~ mask pd_bits = word proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> word + (xa << 2) && ~~ mask pd_bits = word proof (prove)
goal (3 subgoals):
 1. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> is_aligned word pd_bits
 2. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> xa << 2 < 2 ^ pd_bits
 3. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> word = word proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> xa << 2 < 2 ^ pd_bits
 2. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> word = word proof (prove)
goal (3 subgoals):
 1. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> xa < 2 ^ (pd_bits - 2)
 2. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 3. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> word = word proof (prove)
goal (3 subgoals):
 1. is_aligned word pd_bits \<Longrightarrow> (kernel_base >> 20) - 1 < 2 ^ (pd_bits - 2)
 2. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32)
 3. \<lbrakk>xa \<le> (kernel_base >> 20) - 1; is_aligned word pd_bits\<rbrakk> \<Longrightarrow> word = word proof (prove)
goal:
No subgoals!
theory ArchArch_IF

lemma mapM_x_swp_store_pde_pas_refined_simple:
  "mapM_x (swp store_pde InvalidPDE) A \<lbrace>pas_refined aag\<rbrace>" by (wpsimp wp: mapM_x_wp' store_pde_pas_refined_simple)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> mapM_x (swp store_pde InvalidPDE) A \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory PasUpdates

lemma preemption_point_domain_fields[wp]:
  "preemption_point \<lbrace>domain_fields P\<rbrace>" by (simp add: preemption_point_def
      | wp OR_choiceE_weak_wp modify_wp
      | wpc
      | simp add: reset_work_units_def update_work_units_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> preemption_point \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
theory PasUpdates

lemma cap_revoke_domain_fields[wp]:
  "cap_revoke a \<lbrace>domain_fields P\<rbrace>" by (rule cap_revoke_preservation2; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> cap_revoke a \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
theory PasUpdates

lemma invoke_cnode_domain_fields[wp]:
  "invoke_cnode a \<lbrace>domain_fields P\<rbrace>" unfolding invoke_cnode_def by (wpsimp wp: get_cap_wp hoare_vcg_all_lift hoare_vcg_imp_lift | rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> invoke_cnode a \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> case a of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
theory PasUpdates

lemma pas_wellformed_noninterference_domains_distinct:
  "pas_wellformed_noninterference aag \<Longrightarrow> pas_domains_distinct aag" by (simp add: pas_wellformed_noninterference_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_wellformed_noninterference aag \<Longrightarrow> pas_domains_distinct aag
theory PasUpdates

lemma pas_wellformed_noninterference_silc[intro!]:
  "pas_wellformed_noninterference aag \<Longrightarrow> SilcLabel \<notin> pasDomainAbs aag d" by (fastforce simp: pas_wellformed_noninterference_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_wellformed_noninterference aag \<Longrightarrow> SilcLabel \<notin> pasDomainAbs aag d
theory PasUpdates

lemma pasObjectAbs_pasSubject_update:
  "pasObjectAbs (aag\<lparr>pasSubject := x\<rparr>) = pasObjectAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasObjectAbs (aag\<lparr>pasSubject := x\<rparr>) = pasObjectAbs aag
theory PasUpdates

lemma pasASIDAbs_pasSubject_update:
  "pasASIDAbs (aag\<lparr>pasSubject := x\<rparr>) = pasASIDAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasASIDAbs (aag\<lparr>pasSubject := x\<rparr>) = pasASIDAbs aag
theory PasUpdates

lemma pasIRQAbs_pasSubject_update:
  "pasIRQAbs (aag\<lparr>pasSubject := x\<rparr>) = pasIRQAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasIRQAbs (aag\<lparr>pasSubject := x\<rparr>) = pasIRQAbs aag
theory PasUpdates

lemma irq_map_wellformed_pasSubject_update:
  "irq_map_wellformed_aux (aag\<lparr>pasSubject := x\<rparr>) irqn =
   irq_map_wellformed_aux aag irqn" by (clarsimp simp: irq_map_wellformed_aux_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_map_wellformed_aux (aag\<lparr>pasSubject := x\<rparr>) irqn = irq_map_wellformed_aux aag irqn
theory PasUpdates

lemma tcb_domain_map_wellformed_pasSubject_update:
  "tcb_domain_map_wellformed_aux (aag\<lparr>pasSubject := x\<rparr>) irqn =
   tcb_domain_map_wellformed_aux aag irqn" by (clarsimp simp: tcb_domain_map_wellformed_aux_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_domain_map_wellformed_aux (aag\<lparr>pasSubject := x\<rparr>) irqn = tcb_domain_map_wellformed_aux aag irqn
theory PasUpdates

lemma pas_wellformed_pasSubject_update:
  "\<lbrakk> pas_wellformed_noninterference aag; l \<in> pasDomainAbs aag d \<rbrakk>
     \<Longrightarrow> pas_wellformed (aag\<lparr>pasSubject := l\<rparr>)" by (auto simp: pas_wellformed_noninterference_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_wellformed_noninterference aag; l \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> pas_wellformed (aag\<lparr>pasSubject := l\<rparr>)
theory PasUpdates

lemma guarded_pas_domain_pasSubject_update[simp]:
  "guarded_pas_domain (aag\<lparr>pasSubject := x\<rparr>) s = guarded_pas_domain aag s" by (simp add: guarded_pas_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guarded_pas_domain (aag\<lparr>pasSubject := x\<rparr>) s = guarded_pas_domain aag s
theory PasUpdates

lemma silc_inv_pasSubject_update:
  "\<lbrakk> silc_inv aag st s; pas_wellformed_noninterference aag; l \<in> pasDomainAbs aag d \<rbrakk>
     \<Longrightarrow> silc_inv (aag\<lparr>pasSubject := l\<rparr>) st s" by (fastforce intro: silc_inv_pasSubject_update' dest: pas_wellformed_noninterference_silc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; pas_wellformed_noninterference aag; l \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> silc_inv (aag\<lparr>pasSubject := l\<rparr>) st s
theory PasUpdates

lemma prop_of_pasMayActivate_update_idemp:
  "\<lbrakk> P aag; pasMayActivate aag = v \<rbrakk> \<Longrightarrow> P (aag\<lparr>pasMayActivate := v\<rparr>)" by (hypsubst, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P aag; pasMayActivate aag = v\<rbrakk> \<Longrightarrow> P (aag\<lparr>pasMayActivate := v\<rparr>)
theory PasUpdates

lemma pasObjectAbs_pasMayActivate_update:
  "pasObjectAbs (aag\<lparr>pasMayActivate := x\<rparr>) = pasObjectAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasObjectAbs (aag\<lparr>pasMayActivate := x\<rparr>) = pasObjectAbs aag
theory PasUpdates

lemma pasASIDAbs_pasMayActivate_update:
  "pasASIDAbs (aag\<lparr>pasMayActivate := x\<rparr>) = pasASIDAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasASIDAbs (aag\<lparr>pasMayActivate := x\<rparr>) = pasASIDAbs aag
theory PasUpdates

lemma pasIRQAbs_pasMayActivate_update:
  "pasIRQAbs (aag\<lparr>pasMayActivate := x\<rparr>) = pasIRQAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasIRQAbs (aag\<lparr>pasMayActivate := x\<rparr>) = pasIRQAbs aag
theory PasUpdates

lemma state_irqs_to_policy_pasMayActivate_update:
  "state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s =
   state_irqs_to_policy aag s" apply (rule equalityI) apply (clarify) apply (erule state_irqs_to_policy_aux.cases
          | simp
          | fastforce intro: state_irqs_to_policy_aux.intros)+ apply (clarify) apply (erule state_irqs_to_policy_aux.cases) apply (simp, subst pasObjectAbs_pasMayActivate_update[symmetric]
             , subst pasIRQAbs_pasMayActivate_update[symmetric]
             , rule state_irqs_to_policy_aux.intros, assumption+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s = state_irqs_to_policy aag s proof (prove)
goal (2 subgoals):
 1. state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s \<subseteq> state_irqs_to_policy aag s
 2. state_irqs_to_policy aag s \<subseteq> state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy aag s
 2. state_irqs_to_policy aag s \<subseteq> state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy aag s \<subseteq> state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy aag s \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy (aag\<lparr>pasMayActivate := x\<rparr>) s proof (prove)
goal:
No subgoals!
theory PasUpdates

lemma guarded_pas_domainMayActivate_update[simp]:
  "guarded_pas_domain (aag\<lparr>pasMayActivate := False\<rparr>) = guarded_pas_domain aag" by (simp add: guarded_pas_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guarded_pas_domain (aag\<lparr>pasMayActivate := False\<rparr>) = guarded_pas_domain aag
theory PasUpdates

lemma cdt_change_allowedMayActivate_update[simp]:
  "cdt_change_allowed (aag\<lparr>pasMayActivate := x\<rparr>) = cdt_change_allowed aag " by (simp add: cdt_change_allowed_def[abs_def] cdt_direct_change_allowed.simps direct_call_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt_change_allowed (aag\<lparr>pasMayActivate := x\<rparr>) = cdt_change_allowed aag
theory PasUpdates

lemma prop_of_pasMayEditReadyQueues_update_idemp:
  "\<lbrakk> P aag; pasMayEditReadyQueues aag = v \<rbrakk> \<Longrightarrow> P (aag\<lparr>pasMayEditReadyQueues := v\<rparr>)" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P aag; pasMayEditReadyQueues aag = v\<rbrakk> \<Longrightarrow> P (aag\<lparr>pasMayEditReadyQueues := v\<rparr>)
theory PasUpdates

lemma pasObjectAbs_pasMayEditReadyQueues_update:
  "pasObjectAbs (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) = pasObjectAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasObjectAbs (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) = pasObjectAbs aag
theory PasUpdates

lemma pasASIDAbs_pasMayEditReadyQueues_update:
  "pasASIDAbs (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) = pasASIDAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasASIDAbs (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) = pasASIDAbs aag
theory PasUpdates

lemma pasIRQAbs_pasMayEditReadyQueues_update:
  "pasIRQAbs (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) = pasIRQAbs aag" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasIRQAbs (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) = pasIRQAbs aag
theory PasUpdates

lemma state_irqs_to_policy_pasMayEditReadyQueues_update:
  "state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s =
   state_irqs_to_policy aag s" apply (rule equalityI) apply (clarify) apply (erule state_irqs_to_policy_aux.cases
          | simp
          | fastforce intro: state_irqs_to_policy_aux.intros)+ apply (clarify) apply (erule state_irqs_to_policy_aux.cases) apply (simp, subst pasObjectAbs_pasMayEditReadyQueues_update[symmetric]
             , subst pasIRQAbs_pasMayEditReadyQueues_update[symmetric]
             , rule state_irqs_to_policy_aux.intros, assumption+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s = state_irqs_to_policy aag s proof (prove)
goal (2 subgoals):
 1. state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s \<subseteq> state_irqs_to_policy aag s
 2. state_irqs_to_policy aag s \<subseteq> state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy aag s
 2. state_irqs_to_policy aag s \<subseteq> state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s proof (prove)
goal (1 subgoal):
 1. state_irqs_to_policy aag s \<subseteq> state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_irqs_to_policy aag s \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ptr cap irq. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasIRQAbs aag irq; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s proof (prove)
goal:
No subgoals!
theory PasUpdates

lemma pas_refined_pasMayEditReadyQueues_update:
  "pas_refined aag s
   \<Longrightarrow> pas_refined (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s" by (clarsimp simp: pas_refined_def irq_map_wellformed_aux_def tcb_domain_map_wellformed_aux_def
                     state_asids_to_policy_pasMayEditReadyQueues_update[simplified]
                     state_irqs_to_policy_pasMayEditReadyQueues_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> pas_refined (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) s
theory PasUpdates

lemma guarded_pas_domainMayEditReadyQueues_update[simp]:
  "guarded_pas_domain (aag\<lparr>pasMayEditReadyQueues := False\<rparr>) = guarded_pas_domain aag" by (simp add: guarded_pas_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guarded_pas_domain (aag\<lparr>pasMayEditReadyQueues := False\<rparr>) = guarded_pas_domain aag
theory PasUpdates

lemma cdt_change_allowedMayEditReadyQueues_update[simp]:
  "cdt_change_allowed (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) =
   cdt_change_allowed aag" by (simp add: cdt_change_allowed_def[abs_def] cdt_direct_change_allowed.simps direct_call_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt_change_allowed (aag\<lparr>pasMayEditReadyQueues := x\<rparr>) = cdt_change_allowed aag
theory ArchPasUpdates

lemma state_asids_to_policy_aux_pasSubject_update:
  "state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs =
   state_asids_to_policy_aux aag caps asid vrefs" apply (rule equalityI) apply clarify apply (erule state_asids_to_policy_aux.cases
          | simp
          | fastforce intro: state_asids_to_policy_aux.intros)+ apply clarify apply (erule state_asids_to_policy_aux.cases) apply (simp, subst pasObjectAbs_pasSubject_update[symmetric]
               , subst pasASIDAbs_pasSubject_update[symmetric]
               , rule state_asids_to_policy_aux.intros
               , assumption+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs = state_asids_to_policy_aux aag caps asid vrefs proof (prove)
goal (2 subgoals):
 1. state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs \<subseteq> state_asids_to_policy_aux aag caps asid vrefs
 2. state_asids_to_policy_aux aag caps asid vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux aag caps asid vrefs
 2. state_asids_to_policy_aux aag caps asid vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy_aux aag caps asid vrefs \<subseteq> state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. (a, aa, b) \<in> state_asids_to_policy_aux aag caps asid vrefs \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ptr acap asida. \<lbrakk>a = pasObjectAbs aag (fst ptr); aa = Control; b = pasASIDAbs aag asida; caps ptr = Some (ArchObjectCap acap); asida \<in> acap_asid' acap\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs
 2. \<And>a aa b asida poolptr pdptr ab. \<lbrakk>a = pasASIDAbs aag asida; aa = ab; b = pasObjectAbs aag pdptr; asid (asid_high_bits_of asida) = Some poolptr; (pdptr, asida && mask local.asid_low_bits, AASIDPool, ab) \<in> vrefs poolptr\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs
 3. \<And>a aa b asida poolptr. \<lbrakk>a = pasObjectAbs aag poolptr; aa = AAuth ASIDPoolMapsASID; b = pasASIDAbs aag asida; asid (asid_high_bits_of asida) = Some poolptr; asida \<noteq> 0\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy_aux (aag\<lparr>pasSubject := x\<rparr>) caps asid vrefs proof (prove)
goal:
No subgoals!
theory ArchPasUpdates

lemma state_asids_to_policy_pasSubject_update[PasUpdates_assms]:
  "state_asids_to_policy (aag\<lparr>pasSubject := x\<rparr>) s =
   state_asids_to_policy aag s" by (simp add: state_asids_to_policy_aux_pasSubject_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_asids_to_policy (aag\<lparr>pasSubject := x\<rparr>) s = state_asids_to_policy aag s