theory Syscall_AC

lemma handle_interrupt_integrity_autarch:
  "\<lbrace>integrity aag X st and pas_refined aag and invs
                       and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))
                       and K (is_subject_irq aag irq)\<rbrace>
   handle_interrupt irq
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: handle_interrupt_def  cong: irq_state.case_cong) apply (rule conjI; rule impI; rule hoare_pre) apply (wp (once) send_signal_respects get_cap_auth_wp [where aag = aag] dmo_mol_respects
                      ackInterrupt_device_state_inv resetTimer_device_state_inv
            | simp add: get_irq_slot_def get_irq_state_def
            | wp dmo_no_mem_respects
            | wpc)+ apply (fastforce simp: is_cap_simps aag_cap_auth_def cap_auth_conferred_def
                         cap_rights_to_auth_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and invs and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and K (is_subject_irq aag irq)\<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. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>y. is_subject_irq aag irq)\<rbrace> do_machine_op (do y <- 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. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>y. is_subject_irq aag irq)\<rbrace> do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
y <- when (is_ntfn_cap cap \<and> AllowWrite \<in> cap_rights cap) (send_signal (obj_ref_of cap) (cap_ep_badge cap));
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do y <- 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>?Q31\<rbrace> do_machine_op (do y <- 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. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>y. is_subject_irq aag irq)) s\<rbrakk> \<Longrightarrow> ?Q31 s
 3. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>?Q26\<rbrace> do st <- get_irq_state irq;
y <- case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
y <- when (is_ntfn_cap cap \<and> AllowWrite \<in> cap_rights cap) (send_signal (obj_ref_of cap) (cap_ep_badge cap));
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do y <- 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. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>y. is_subject_irq aag irq)) s\<rbrakk> \<Longrightarrow> ?Q26 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> (ct_active s \<longrightarrow> is_subject aag (cur_thread s)) \<and> is_subject_irq aag irq\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal \<longrightarrow> (\<forall>cap. is_ntfn_cap cap \<and> AllowWrite \<in> cap_rights cap \<longrightarrow> caps_of_state s (interrupt_irq_node s irq, []) = Some cap \<and> pas_cap_cur_auth aag cap \<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:
No subgoals!