kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_IF

lemma finalise_cap_only_timer_irq_inv:
  "\<lbrace>only_timer_irq_inv irq (st :: det_state)\<rbrace>
   finalise_cap cap final
   \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace>" apply (simp add: only_timer_irq_inv_def) apply (wp only_timer_irq_pres | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq_inv irq st\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. only_timer_irq_inv irq st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and only_timer_irq irq\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. domain_sep_inv False st and only_timer_irq irq\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_IF

lemma ev_pre_cont:
  "equiv_valid I A B \<bottom> f" by (simp add: equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B (\<lambda>_. False) f
theory Finalise_IF

lemma finalise_cap_transferable_ev:
  "equiv_valid_inv I A (K(is_transferable_cap cap)) (finalise_cap cap final)" by (rule gen_asm_ev) (erule is_transferable_capE; wpsimp wp: return_ev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (K (is_transferable_cap cap)) (finalise_cap cap final)
theory Finalise_IF

lemma rec_del_Finalise_transferableE_R:
  "\<lbrace>(\<lambda>s. is_transferable (caps_of_state s slot)) and P\<rbrace>
   rec_del (FinaliseSlotCall slot exposed)
   \<lbrace>\<lambda>_. P\<rbrace>, -" apply (rule hoare_pre) apply (simp add: validE_R_def) apply (rule hoare_post_impErr) apply (rule rec_del_Finalise_transferable) by force+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_transferable_in slot and P\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, -
 2. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'\<rbrace> rec_del (FinaliseSlotCall slot exposed) \<lbrace>?Q3\<rbrace>, \<lbrace>?E3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> P s
 3. \<And>e s. ?E3 e s \<Longrightarrow> True
 4. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (K (rv = (True, NullCap)) and ?E8) s \<Longrightarrow> P s
 2. \<And>e s. ?E8 s \<Longrightarrow> True
 3. \<And>s. (is_transferable_in slot and P) s \<Longrightarrow> (is_transferable_in slot and ?E8) s
theory Finalise_IF

lemma cap_delete_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs
                                           and simple_sched_action and pas_refined aag
                                           and emptyable slot and K (is_subject aag (fst slot)))
                    (cap_delete slot)" unfolding cap_delete_def by (wp rec_del_spec_reads_respects_f | rule use_spec_ev | simp | elim conjE | force)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and K (is_subject aag (fst slot))) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and emptyable slot and K (is_subject aag (fst slot))) (doE rec_del (CTEDeleteCall slot True);
returnOk ()
odE)
theory Finalise_IF

lemma globals_equiv_interrupt_states_update:
  "globals_equiv st (s\<lparr>interrupt_states := x\<rparr>) = globals_equiv st s" by (auto simp: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv st (s\<lparr>interrupt_states := x\<rparr>) = globals_equiv st s
theory Finalise_IF

lemma cancel_all_ipc_globals_equiv':
  "cancel_all_ipc epptr \<lbrace>globals_equiv st and valid_arch_state\<rbrace>" unfolding cancel_all_ipc_def by (wp mapM_x_wp[OF _ subset_refl] set_thread_state_globals_equiv
         set_simple_ko_globals_equiv hoare_vcg_all_lift get_object_inv dxo_wp_weak
      | wpc | simp | wp (once) hoare_drop_imps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do ep <- get_endpoint epptr;
case ep of IdleEP \<Rightarrow> return () | _ \<Rightarrow> do queue <- get_ep_queue ep;
set_endpoint epptr IdleEP;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) $ queue;
do_extended_op reschedule_required
od
od \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state\<rbrace>
theory Finalise_IF

lemma cancel_all_ipc_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   cancel_all_ipc epptr
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" by (fastforce intro: hoare_strengthen_post[OF cancel_all_ipc_globals_equiv'])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> cancel_all_ipc epptr \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Finalise_IF

lemma cancel_all_signals_globals_equiv':
  "cancel_all_signals epptr \<lbrace>globals_equiv st and valid_arch_state\<rbrace>" unfolding cancel_all_signals_def by (wp mapM_x_wp[OF _ subset_refl] set_thread_state_globals_equiv
         set_simple_ko_globals_equiv hoare_vcg_all_lift get_object_inv dxo_wp_weak
      | wpc | simp | wp (once) hoare_drop_imps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> cancel_all_signals epptr \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do ntfn <- get_notification epptr;
case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do _ <- set_notification epptr $ ntfn_set_obj ntfn IdleNtfn;
mapM_x (\<lambda>t. do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t)
od) queue;
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. globals_equiv st and valid_arch_state\<rbrace>
theory Finalise_IF

lemma cancel_all_signals_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   cancel_all_signals epptr
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" by (fastforce intro: hoare_strengthen_post[OF cancel_all_signals_globals_equiv'])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> cancel_all_signals epptr \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Finalise_IF

lemma unbind_notification_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   unbind_notification t
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding unbind_notification_def by (wpsimp wp: gbn_wp set_bound_notification_globals_equiv set_notification_globals_equiv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> unbind_notification t \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do ntfnptr <- get_bound_notification t;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t
od
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Finalise_IF

lemma unbind_maybe_notification_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace>
   unbind_maybe_notification a
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding unbind_maybe_notification_def by (wpsimp wp: gbn_wp set_bound_notification_globals_equiv
                 set_notification_globals_equiv get_simple_ko_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> unbind_maybe_notification a \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do ntfn <- get_notification a;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do_unbind_notification a ntfn t
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory Finalise_IF

lemma empty_slot_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state\<rbrace> empty_slot s b \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding empty_slot_def post_cap_deletion_def by (wpsimp wp: set_cap_globals_equiv'' set_original_globals_equiv hoare_vcg_if_lift2
                 set_cdt_globals_equiv dxo_wp_weak hoare_drop_imps hoare_vcg_all_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> empty_slot s b \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state\<rbrace> do cap <- get_cap s;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>sa. cdt sa s);
cdt <- gets cdt;
parent <- return $ cdt s;
set_cdt ((\<lambda>p. if cdt p = Some s then parent else cdt p)(s := None));
do_extended_op (empty_slot_ext s slot_p);
set_original s False;
set_cap NullCap s;
case b of IRQHandlerCap irq \<Rightarrow> deleted_irq_handler irq | ArchObjectCap acap \<Rightarrow> arch_post_cap_deletion acap | _ \<Rightarrow> return ()
od
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
theory ArchFinalise_IF

lemma dmo_maskInterrupt_reads_respects[Finalise_IF_assms]:
  "reads_respects aag l \<top> (do_machine_op (maskInterrupt m irq))" unfolding maskInterrupt_def apply (rule use_spec_ev) apply (rule do_machine_op_spec_reads_respects) apply (simp add: equiv_valid_def2) apply (rule modify_ev2) apply (fastforce simp: equiv_for_def) apply (wp modify_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (maskInterrupt m irq)) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (do_machine_op (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>st. spec_reads_respects st aag l (\<lambda>_. True) (do_machine_op (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>st. equiv_valid_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>))
 2. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (2 subgoals):
 1. equiv_valid_rv_inv (equiv_machine_state (aag_can_read aag)) (equiv_machine_state (aag_can_affect aag l)) (=) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>))
 2. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>equiv_machine_state (aag_can_read aag) s t; equiv_machine_state (aag_can_affect aag l) s t; True; True\<rbrakk> \<Longrightarrow> () = () \<and> equiv_machine_state (aag_can_read aag) (s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>) (t\<lparr>irq_masks := (irq_masks t)(irq := m)\<rparr>) \<and> equiv_machine_state (aag_can_affect aag l) (s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>) (t\<lparr>irq_masks := (irq_masks t)(irq := m)\<rparr>)
 2. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st P. \<lbrace>\<lambda>ms. P (irq_state ms)\<rbrace> modify (\<lambda>s. s\<lparr>irq_masks := (irq_masks s)(irq := m)\<rparr>) \<lbrace>\<lambda>_ ms. P (irq_state ms)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalise_IF

lemma arch_post_cap_deletion_read_respects[Finalise_IF_assms, wp]:
  "reads_respects aag l \<top> (arch_post_cap_deletion acap)" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (arch_post_cap_deletion acap)
theory ArchFinalise_IF

lemma equiv_asid_ready_queues_update[Finalise_IF_assms, simp]:
  "equiv_asid asid (ready_queues_update f s) s' = equiv_asid asid s s'"
  "equiv_asid asid s (ready_queues_update f s') = equiv_asid asid s s'" by (auto simp: equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_asid asid (ready_queues_update f s) s' = equiv_asid asid s s' &&& equiv_asid asid s (ready_queues_update f s') = equiv_asid asid s s'
theory ArchFinalise_IF

lemma arch_finalise_cap_makes_halted[Finalise_IF_assms]:
  "\<lbrace>invs and valid_cap (ArchObjectCap arch_cap)
        and (\<lambda>s. ex = is_final_cap' (ArchObjectCap arch_cap) s)
        and cte_wp_at ((=) (ArchObjectCap arch_cap)) slot\<rbrace>
   arch_finalise_cap arch_cap ex
   \<lbrace>\<lambda>rv s. \<forall>t \<in> obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>" by (wpsimp simp: arch_finalise_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap arch_cap) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap arch_cap) s) and cte_wp_at ((=) (ArchObjectCap arch_cap)) slot\<rbrace> arch_finalise_cap arch_cap ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs_ac (fst rv). halted_if_tcb t s\<rbrace>
theory ArchFinalise_IF

lemma set_tcb_queue_modifies_at_most:
  "modifies_at_most aag L (\<lambda>s. pasDomainAbs aag d \<inter> L \<noteq> {}) (set_tcb_queue d prio queue)" apply (rule modifies_at_mostI) apply (simp add: set_tcb_queue_def modify_def, wp) apply (force simp: equiv_but_for_labels_def states_equiv_for_def equiv_for_def equiv_asids_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modifies_at_most aag L (\<lambda>s. pasDomainAbs aag d \<inter> L \<noteq> {}) (set_tcb_queue d prio queue) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrace>(\<lambda>s. pasDomainAbs aag d \<inter> L \<noteq> {}) and equiv_but_for_labels aag L st\<rbrace> set_tcb_queue d prio queue \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st s. ((\<lambda>s. pasDomainAbs aag d \<inter> L \<noteq> {}) and equiv_but_for_labels aag L st) s \<Longrightarrow> equiv_but_for_labels aag L st (ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then queue else ready_queues s d' p) s) proof (prove)
goal:
No subgoals!
theory ArchFinalise_IF

lemma set_notification_equiv_but_for_labels[Finalise_IF_assms]:
  "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag ntfnptr \<in> L)\<rbrace>
   set_notification ntfnptr ntfn
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" unfolding set_simple_ko_def apply (wp set_object_equiv_but_for_labels get_object_wp) apply (clarsimp simp: asid_pool_at_kheap partial_inv_def obj_at_def split: kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag ntfnptr \<in> L)\<rbrace> set_notification ntfnptr ntfn \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag ntfnptr \<in> L)\<rbrace> do obj <- get_object ntfnptr;
assert (is_simple_type obj);
assert (partial_inv Notification obj \<noteq> None);
set_object ntfnptr (Notification ntfn)
od \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag ntfnptr \<in> L)) s \<Longrightarrow> \<forall>ko. ko_at ko ntfnptr s \<longrightarrow> is_simple_type ko \<longrightarrow> partial_inv Notification ko \<noteq> None \<longrightarrow> (equiv_but_for_labels aag L st and (\<lambda>s. \<not> typ_at (AArch AASIDPool) ntfnptr s) and K ((\<forall>asid_pool. Notification ntfn \<noteq> ArchObj (ASIDPool asid_pool)) \<and> pasObjectAbs aag ntfnptr \<in> L)) s proof (prove)
goal:
No subgoals!
theory ArchFinalise_IF

lemma aag_cap_auth_ASIDPoolCap:
  "pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap r asid)) \<Longrightarrow>
   pas_refined aag s \<Longrightarrow> is_subject aag r" unfolding aag_cap_auth_def by (simp add: clas_no_asid cap_auth_conferred_def arch_cap_auth_conferred_def
                cli_no_irqs pas_refined_all_auth_is_owns is_page_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap r asid)); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag r proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (ASIDPoolCap r asid)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag r
theory ArchFinalise_IF

lemma aag_cap_auth_PageDirectory:
  "pas_cap_cur_auth aag (ArchObjectCap (PageDirectoryCap word (Some a))) \<Longrightarrow>
    pas_refined aag s \<Longrightarrow> is_subject aag word" unfolding aag_cap_auth_def by (simp add: clas_no_asid cap_auth_conferred_def arch_cap_auth_conferred_def
                cli_no_irqs pas_refined_all_auth_is_owns is_page_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (PageDirectoryCap word (Some a))); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag word proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (PageDirectoryCap word (Some a))). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (PageDirectoryCap word (Some a))). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (PageDirectoryCap word (Some a))). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (PageDirectoryCap word (Some a))) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (PageDirectoryCap word (Some a))); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag word
theory ArchFinalise_IF

lemma aag_cap_auth_PageCap_asid:
  "\<lbrakk> pas_cap_cur_auth aag (ArchObjectCap (PageCap dev ref r sz (Some (a, b)))); pas_refined aag s \<rbrakk>
     \<Longrightarrow> is_subject_asid aag a" by (auto simp: aag_cap_auth_def cap_links_asid_slot_def label_owns_asid_slot_def
          intro: pas_refined_Control_into_is_subject_asid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (PageCap dev ref r sz (Some (a, b)))); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject_asid aag a
theory ArchFinalise_IF

lemma aag_cap_auth_PageTableCap:
  "\<lbrakk> pas_cap_cur_auth aag (ArchObjectCap (PageTableCap word option)); pas_refined aag s \<rbrakk>
     \<Longrightarrow> is_subject aag word" unfolding aag_cap_auth_def by (simp add: clas_no_asid cap_auth_conferred_def arch_cap_auth_conferred_def
                cli_no_irqs pas_refined_all_auth_is_owns is_page_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (PageTableCap word option)); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag word proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (PageTableCap word option)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (PageTableCap word option)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (PageTableCap word option)). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (PageTableCap word option)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (PageTableCap word option)); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag word
theory ArchFinalise_IF

lemma aag_cap_auth_PageTableCap_asid:
  "\<lbrakk> pas_cap_cur_auth aag (ArchObjectCap (PageTableCap word (Some (a, b)))); pas_refined aag s \<rbrakk>
     \<Longrightarrow> is_subject_asid aag a" by (auto simp: aag_cap_auth_def cap_links_asid_slot_def label_owns_asid_slot_def
          intro: pas_refined_Control_into_is_subject_asid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (PageTableCap word (Some (a, b)))); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject_asid aag a
theory ArchFinalise_IF

lemma aag_cap_auth_PageDirectoryCap:
  "\<lbrakk> pas_cap_cur_auth aag (ArchObjectCap (PageDirectoryCap word option));  pas_refined aag s \<rbrakk>
     \<Longrightarrow> is_subject aag word" unfolding aag_cap_auth_def by (simp add: clas_no_asid cap_auth_conferred_def arch_cap_auth_conferred_def
                cli_no_irqs pas_refined_all_auth_is_owns is_page_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (PageDirectoryCap word option)); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag word proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (PageDirectoryCap word option)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (PageDirectoryCap word option)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (PageDirectoryCap word option)). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (PageDirectoryCap word option)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (PageDirectoryCap word option)); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject aag word
theory ArchFinalise_IF

lemma aag_cap_auth_PageDirectoryCap_asid:
  "\<lbrakk> pas_cap_cur_auth aag (ArchObjectCap (PageDirectoryCap word (Some a))); pas_refined aag s \<rbrakk>
     \<Longrightarrow> is_subject_asid aag a" unfolding aag_cap_auth_def by (auto simp: cap_links_asid_slot_def label_owns_asid_slot_def
          intro: pas_refined_Control_into_is_subject_asid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (PageDirectoryCap word (Some a))); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject_asid aag a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (PageDirectoryCap word (Some a))). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (PageDirectoryCap word (Some a))). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (PageDirectoryCap word (Some a))). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (PageDirectoryCap word (Some a))) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (PageDirectoryCap word (Some a))); pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject_asid aag a