kings-crown/FVELER_Isabelle huggingface dataset:
theory FinalCaps

lemma new_irq_handler_caps_are_intra_label:
  "\<lbrakk> cte_wp_at ((=) (IRQControlCap)) slot s; pas_refined aag s; is_subject aag (fst slot) \<rbrakk>
     \<Longrightarrow> cap_points_to_label aag (IRQHandlerCap irq) (pasSubject aag)" apply (clarsimp simp: cap_points_to_label_def) apply (frule cap_cur_auth_caps_of_state[rotated]) apply assumption apply (simp add: cte_wp_at_caps_of_state) apply (clarsimp simp: aag_cap_auth_def cap_links_irq_def) apply (blast intro: aag_Control_into_owns_irq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> cap_points_to_label aag (IRQHandlerCap irq) (pasSubject aag) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> is_subject_irq aag irq proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> is_subject aag (fst ?p9)
 2. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> caps_of_state s ?p9 = Some ?cap9
 3. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot); pas_cap_cur_auth aag ?cap9\<rbrakk> \<Longrightarrow> is_subject_irq aag irq proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> caps_of_state s slot = Some ?cap9
 2. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot); pas_cap_cur_auth aag ?cap9\<rbrakk> \<Longrightarrow> is_subject_irq aag irq proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot); pas_cap_cur_auth aag IRQControlCap\<rbrakk> \<Longrightarrow> is_subject_irq aag irq proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) IRQControlCap) slot s; pas_refined aag s; is_subject aag (fst slot); cap_links_asid_slot aag (pasSubject aag) IRQControlCap; \<forall>irq. (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject_irq aag irq proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma valid_ep_recv_dequeue':
  "\<lbrakk> ko_at (Endpoint (Structures_A.endpoint.RecvEP (t # ts))) epptr s; valid_objs s \<rbrakk>
     \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> RecvEP ts) s" unfolding valid_objs_def valid_obj_def valid_ep_def obj_at_def apply (drule bspec) apply (auto split: list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (Endpoint (RecvEP (t # ts))) epptr s; valid_objs s\<rbrakk> \<Longrightarrow> valid_ep (case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> RecvEP ts) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>ko. kheap s epptr = Some ko \<and> Endpoint (RecvEP (t # ts)) = ko; \<forall>ptr\<in>dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint IdleEP \<Rightarrow> True | Endpoint (SendEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | Endpoint (RecvEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s)\<rbrakk> \<Longrightarrow> case case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> RecvEP ts of IdleEP \<Rightarrow> True | SendEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | RecvEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts proof (prove)
goal (2 subgoals):
 1. \<exists>ko. kheap s epptr = Some ko \<and> Endpoint (RecvEP (t # ts)) = ko \<Longrightarrow> ?ptr \<in> (dom $ kheap s)
 2. \<lbrakk>\<exists>ko. kheap s epptr = Some ko \<and> Endpoint (RecvEP (t # ts)) = ko; \<exists>obj. kheap s ?ptr = Some obj \<and> (case obj of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ?ptr t s | Endpoint IdleEP \<Rightarrow> True | Endpoint (SendEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | Endpoint (RecvEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s)\<rbrakk> \<Longrightarrow> case case ts of [] \<Rightarrow> IdleEP | b # bs \<Rightarrow> RecvEP ts of IdleEP \<Rightarrow> True | SendEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts | RecvEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko) \<and> distinct ts proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma get_tcb_Some:
  "get_tcb t s = Some v \<longleftrightarrow> kheap s t = Some (TCB v)" by (simp add: get_tcb_def split: kernel_object.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (get_tcb t s = Some v) = (kheap s t = Some (TCB v))
theory FinalCaps

lemma do_ipc_transfer_silc_inv:
  "\<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_objs and valid_mdb and pas_refined aag
                    and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace>
   do_ipc_transfer sender ep badge grant receiver
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding do_ipc_transfer_def apply (wp do_normal_transfer_silc_inv hoare_vcg_all_lift | wpc | wp (once) hoare_drop_imps)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do_ipc_transfer sender ep badge grant receiver \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)\<rbrace> do recv_buffer <- lookup_ipc_buffer True receiver;
fault <- thread_get tcb_fault sender;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False sender;
do_normal_transfer sender send_buffer ep badge grant receiver recv_buffer
od | Some f \<Rightarrow> do_fault_transfer badge sender receiver recv_buffer
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<Longrightarrow> (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)) s \<and> (\<forall>x. silc_inv aag st s) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma setup_caller_cap_silc_inv:
  "\<lbrace>silc_inv aag st and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver)
       and K (pasObjectAbs aag sender \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel)\<rbrace>
     setup_caller_cap sender receiver grant
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding setup_caller_cap_def apply (wp cap_insert_silc_inv''' hoare_vcg_imp_lift hoare_vcg_ex_lift
            slots_holding_overlapping_caps_from_silc_inv[where aag=aag and st=st and P="\<top>"]
        | simp)+ apply (auto simp: cap_points_to_label_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) and K (pasObjectAbs aag sender \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel)\<rbrace> setup_caller_cap sender receiver grant \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) and K (pasObjectAbs aag sender \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel)\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (receiver, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> (grant \<longrightarrow> is_subject aag sender \<and> is_subject aag receiver) \<and> pasObjectAbs aag sender \<noteq> SilcLabel \<and> pasObjectAbs aag receiver \<noteq> SilcLabel \<Longrightarrow> (grant \<longrightarrow> cap_points_to_label aag (ReplyCap sender False {AllowGrant, AllowWrite}) (pasSubject aag) \<or> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ReplyCap sender False {AllowGrant, AllowWrite}) s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> (\<not> grant \<longrightarrow> cap_points_to_label aag (ReplyCap sender False {AllowWrite}) (pasObjectAbs aag receiver) \<or> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ReplyCap sender False {AllowWrite}) s) \<and> pasObjectAbs aag a = SilcLabel)) proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma setup_reply_master_silc_inv:
  "\<lbrace>silc_inv aag st and K (is_subject aag thread)\<rbrace>
   setup_reply_master thread
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding setup_reply_master_def apply (wp set_cap_silc_inv hoare_vcg_ex_lift
            slots_holding_overlapping_caps_from_silc_inv[where aag=aag and st=st and P="\<top>"]
            get_cap_wp hoare_weak_lift_imp
         | simp)+ apply (clarsimp simp: cap_points_to_label_def silc_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (is_subject aag thread)\<rbrace> setup_reply_master thread \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and K (is_subject aag thread)\<rbrace> do old_cap <- get_cap (thread, tcb_cnode_index 2);
when (old_cap = NullCap) $ do set_original (thread, tcb_cnode_index 2) True;
set_cap (ReplyCap thread True {AllowGrant, AllowWrite}) (thread, tcb_cnode_index 2)
od
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> is_subject aag thread \<Longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 2) s \<longrightarrow> (\<not> cap_points_to_label aag (ReplyCap thread True {AllowGrant, AllowWrite}) (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (ReplyCap thread True {AllowGrant, AllowWrite}) s) \<and> pasObjectAbs aag a = SilcLabel)) \<and> pasSubject aag \<noteq> SilcLabel proof (prove)
goal:
No subgoals!
theory FinalCaps

lemma thread_set_tcb_ipc_buffer_update_silc_inv[wp]:
  "\<lbrace>silc_inv aag st\<rbrace>
   thread_set (tcb_ipc_buffer_update blah) t
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> thread_set (tcb_ipc_buffer_update blah) t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory FinalCaps

lemma thread_set_tcb_fault_handler_update_silc_inv[wp]:
  "\<lbrace>silc_inv aag st\<rbrace>
   thread_set (tcb_fault_handler_update blah) t
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> thread_set (tcb_fault_handler_update blah) t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory FinalCaps

lemma set_mcpriority_silc_inv[wp]:
  "set_mcpriority t mcp \<lbrace>silc_inv aag st\<rbrace>" unfolding set_mcpriority_def by (rule thread_set_silc_inv; simp add: tcb_cap_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> set_mcpriority t mcp \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> thread_set (tcb_mcpriority_update (\<lambda>_. mcp)) t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory FinalCaps

lemma cap_delete_tcb[wp]:
 "cap_delete ptr \<lbrace>\<lambda>s. P (tcb_at t s)\<rbrace>" unfolding cap_delete_def tcb_at_typ by (simp add: tcb_at_typ | wp rec_del_typ_at)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_at t s)\<rbrace> cap_delete ptr \<lbrace>\<lambda>_ s. P (tcb_at t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at ATCB t s)\<rbrace> doE rec_del (CTEDeleteCall ptr True);
returnOk ()
odE \<lbrace>\<lambda>_ s. P (typ_at ATCB t s)\<rbrace>
theory FinalCaps

lemma st_tcb_at_triv:
  "st_tcb_at (\<lambda>_. P) t s \<longleftrightarrow> P \<and> tcb_at t s" by (simp add:tcb_at_st_tcb_at st_tcb_at_tcb_states_of_state) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at (\<lambda>_. P) t s = (P \<and> tcb_at t s)
theory FinalCaps

lemma cap_insert_no_tcb_at[wp]:
 "cap_insert cap src dest \<lbrace>\<lambda>s. \<not> tcb_at t s\<rbrace>" unfolding tcb_at_st_tcb_at by (wp cap_insert_no_pred_tcb_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> tcb_at t s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_ s. \<not> tcb_at t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> st_tcb_at (\<lambda>_. True) t s\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_ s. \<not> st_tcb_at (\<lambda>_. True) t s\<rbrace>
theory FinalCaps

lemma intra_label_cap_cur_thread[simp]:
  "intra_label_cap aag slot (s\<lparr>cur_thread := X\<rparr>) = intra_label_cap aag slot s" by (simp add: intra_label_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intra_label_cap aag slot (s\<lparr>cur_thread := X\<rparr>) = intra_label_cap aag slot s
theory FinalCaps

lemma silc_inv_cur_thread[simp]:
  "silc_inv aag st (s\<lparr>cur_thread := X\<rparr>) = silc_inv aag st s" by (simp add: silc_inv_def silc_dom_equiv_def equiv_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_inv aag st (s\<lparr>cur_thread := X\<rparr>) = silc_inv aag st s
theory FinalCaps

lemma cte_wp_at_caps_of_state':
  "cte_wp_at ((=) c) slot s \<Longrightarrow> caps_of_state s slot = Some c" by (simp add: caps_of_state_def cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) c) slot s \<Longrightarrow> caps_of_state s slot = Some c
theory FinalCaps

lemma handle_reply_silc_inv:
  "\<lbrace>silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace>
   handle_reply
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding handle_reply_def apply (wp hoare_vcg_all_lift get_cap_wp | wpc )+ by (force dest: cap_auth_caps_of_state silc_inv_not_subject
            simp: cte_wp_at_caps_of_state aag_cap_auth_def cap_auth_conferred_def
                  reply_cap_rights_to_auth_def
           intro: aag_Control_into_owns)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> handle_reply \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> \<forall>x. cte_wp_at ((=) x) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (x = NullCap \<longrightarrow> silc_inv aag st s) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = ReplyCap xa xb xc \<longrightarrow> (xb = True \<longrightarrow> True) \<and> (xb = False \<longrightarrow> (silc_inv aag st and (pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and valid_mdb and pas_refined aag and K (AllowGrant \<in> xc \<longrightarrow> is_subject aag (cur_thread s) \<and> is_subject aag xa)) and K (pasObjectAbs aag (fst (cur_thread s, tcb_cnode_index 3)) \<noteq> SilcLabel)) s)) \<and> (\<forall>xa xb xc. x = CNodeCap xa xb xc \<longrightarrow> True) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> True) \<and> (x = DomainCap \<longrightarrow> True) \<and> (x = IRQControlCap \<longrightarrow> True) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> True) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> True)
theory FinalCaps

lemma handle_interrupt_silc_inv:
  "handle_interrupt irq \<lbrace>silc_inv aag st\<rbrace>" unfolding handle_interrupt_def by (wpsimp wp: hoare_drop_imps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> if maxIRQ < irq then do_machine_op $ do maskInterrupt True irq;
ackInterrupt irq
od else do st <- get_irq_state irq;
case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op $ ackInterrupt irq
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory FinalCaps

lemma call_kernel_silc_inv:
  "\<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag
                    and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)
                    and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
   call_kernel ev
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (simp add: call_kernel_def) apply (wp handle_interrupt_silc_inv handle_event_silc_inv[where st'=st'] | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> call_kernel ev \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> do y <- handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchFinalCaps

lemma FIXME_arch_gen_refs[FinalCaps_assms]:
  "arch_gen_refs cap = {}" by (clarsimp simp: arch_cap_set_map_def arch_gen_obj_refs_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_gen_refs cap = {}
theory ArchFinalCaps

lemma aobj_ref_same_aobject[FinalCaps_assms]:
  "same_aobject_as cp cp' \<Longrightarrow> aobj_ref cp = aobj_ref cp'" by (cases cp; cases cp'; clarsimp)

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

lemma mapM_x_swp_store_pte_silc_inv[wp]:
  "mapM_x (swp store_pte A) slots \<lbrace>silc_inv aag st\<rbrace>" by (wp mapM_x_wp[OF _ subset_refl] | simp add: swp_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> mapM_x (swp store_pte A) slots \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
theory ArchFinalCaps

lemma is_arch_eq_pt_is_pt_or_pg_cap:
  "cte_wp_at ((=) (ArchObjectCap (PageTableCap xa xb))) slot s
   \<Longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) slot s" apply (erule cte_wp_at_weakenE) by (clarsimp simp: is_pg_cap_def is_pt_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) (ArchObjectCap (PageTableCap xa xb))) slot s \<Longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) slot s proof (prove)
goal (1 subgoal):
 1. \<And>c. ArchObjectCap (PageTableCap xa xb) = c \<Longrightarrow> is_pt_cap c \<or> is_pg_cap c
theory ArchFinalCaps

lemma is_arch_eq_pg_is_pt_or_pg_cap:
  "cte_wp_at ((=) (ArchObjectCap (PageCap dev x xa xb xc))) slot s
   \<Longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) slot s" apply (erule cte_wp_at_weakenE) by (clarsimp simp: is_pg_cap_def is_pt_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) (ArchObjectCap (PageCap dev x xa xb xc))) slot s \<Longrightarrow> cte_wp_at (\<lambda>a. is_pt_cap a \<or> is_pg_cap a) slot s proof (prove)
goal (1 subgoal):
 1. \<And>c. ArchObjectCap (PageCap dev x xa xb xc) = c \<Longrightarrow> is_pt_cap c \<or> is_pg_cap c