theory Syscall_AC

lemma handle_interrupt_integrity:
  "\<lbrace>integrity aag X st and pas_refined aag and invs
                       and (\<lambda>s. pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal)
                       and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace>
   handle_interrupt irq
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: handle_interrupt_def
             cong: irq_state.case_cong bind_cong) apply (rule conjI; rule impI; rule hoare_pre) apply (wp (once) send_signal_respects get_cap_wp dmo_mol_respects dmo_no_mem_respects
                      ackInterrupt_device_state_inv resetTimer_device_state_inv
            | wpc
            | simp add: get_irq_slot_def get_irq_state_def)+ apply clarsimp apply (rule conjI, fastforce)+ \<comment> \<open>valid_objs etc.\<close> apply (clarsimp simp: cte_wp_at_caps_of_state) apply (rule_tac s = s in hacky_ipc_Send [where irq = irq]) apply (drule (1) cap_auth_caps_of_state) apply (clarsimp simp: aag_cap_auth_def is_cap_simps cap_auth_conferred_def
                         cap_rights_to_auth_def split: if_split_asm) apply assumption+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and invs and (\<lambda>s. pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal) and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (maxIRQ < irq \<longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and invs and (\<lambda>s. pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal) and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> do_machine_op (do a <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>) \<and> (\<not> maxIRQ < irq \<longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and invs and (\<lambda>s. pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal) and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> do v <- get_irq_state irq;
a <- case v of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do v <- get_irq_slot irq;
v <- get_cap v;
a <- when (is_ntfn_cap v \<and> AllowWrite \<in> cap_rights v) (send_signal (obj_ref_of v) (cap_ep_badge v));
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do a <- timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>) proof (prove)
goal (4 subgoals):
 1. maxIRQ < irq \<Longrightarrow> \<lbrace>?Q41\<rbrace> do_machine_op (do a <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>maxIRQ < irq; (integrity aag X st and pas_refined aag and invs and (\<lambda>s. pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal) and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?Q41 s
 3. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q36\<rbrace> do v <- get_irq_state irq;
a <- case v of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do v <- get_irq_slot irq;
v <- get_cap v;
a <- when (is_ntfn_cap v \<and> AllowWrite \<in> cap_rights v) (send_signal (obj_ref_of v) (cap_ep_badge v));
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do a <- timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op (ackInterrupt irq)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>s. \<lbrakk>\<not> maxIRQ < irq; (integrity aag X st and pas_refined aag and invs and (\<lambda>s. pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal) and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?Q36 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s \<and> pas_refined aag s \<and> invs s \<and> (pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal) \<and> (ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal \<longrightarrow> (\<forall>cap. is_ntfn_cap cap \<and> AllowWrite \<in> cap_rights cap \<longrightarrow> cte_wp_at ((=) cap) (interrupt_irq_node s irq, []) s \<longrightarrow> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (pasSubject aag, Notify, pasObjectAbs aag (obj_ref_of cap)) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; cte_wp_at ((=) cap) (interrupt_irq_node s irq, []) s; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (pasSubject aag, Notify, pasObjectAbs aag (obj_ref_of cap)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; cte_wp_at ((=) cap) (interrupt_irq_node s irq, []) s; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag (obj_ref_of cap)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag (obj_ref_of cap)) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (interrupt_irq_node s irq), Notify, pasObjectAbs aag (obj_ref_of cap)) \<in> pasPolicy aag
 2. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> pasMaySendIrqs aag proof (prove)
goal (3 subgoals):
 1. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; pasMaySendIrqs aag; aag_cap_auth aag (pasObjectAbs aag (fst (interrupt_irq_node s irq, []))) cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (interrupt_irq_node s irq), Notify, pasObjectAbs aag (obj_ref_of cap)) \<in> pasPolicy aag
 2. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> pas_refined aag s
 3. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> pasMaySendIrqs aag proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<And>s cap. \<lbrakk>\<not> maxIRQ < irq; integrity aag X st s; pas_refined aag s; invs s; ct_active s \<longrightarrow> is_subject aag (cur_thread s); interrupt_states s irq = IRQSignal; is_ntfn_cap cap; AllowWrite \<in> cap_rights cap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> pasMaySendIrqs aag proof (prove)
goal:
No subgoals!