theory InterruptAcc_AI

lemma set_irq_state_invs[wp]:
  "\<And>state irq.
    \<lbrace>\<lambda>s::'state_ext state. invs s
          \<and> (state \<noteq> irq_state.IRQSignal \<longrightarrow> cap.IRQHandlerCap irq \<notin> ran (caps_of_state s))\<rbrace>
      set_irq_state state irq
    \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: set_irq_state_def) apply (wp dmo_maskInterrupt_invs) apply (clarsimp simp: invs_def valid_state_def cur_tcb_def valid_mdb_def all_invs_but_valid_irq_states_for_def) apply (simp add: mdb_cte_at_def valid_irq_node_def
                   valid_irq_handlers_def irq_issued_def) apply (rule conjI) apply (clarsimp simp: cap_irqs_def cap_irq_opt_def
              split: cap.split_asm) apply(clarsimp simp: valid_machine_state_def valid_irq_states_but_def valid_irq_masks_but_def, blast elim: valid_irq_statesE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>state irq. \<lbrace>\<lambda>s. invs s \<and> (state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (caps_of_state s))\<rbrace> set_irq_state state irq \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state irq. \<lbrace>\<lambda>s. invs s \<and> (state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (caps_of_state s))\<rbrace> do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>);
do_machine_op (maskInterrupt (state = IRQInactive) irq)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state irq s. invs s \<and> (state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (caps_of_state s)) \<Longrightarrow> (all_invs_but_valid_irq_states_for irq and (\<lambda>s. state = interrupt_states s irq)) (s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>state irq s. \<lbrakk>valid_pspace s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>)) (cdt s) \<and> valid_irq_handlers (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) \<and> valid_irq_states_but irq (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) \<and> valid_machine_state (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>state irq s. \<lbrakk>valid_pspace s; \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s); \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> ((\<exists>cap\<in>ran (caps_of_state s). irq \<in> cap_irqs cap) \<longrightarrow> state = IRQSignal) \<and> valid_irq_states_but irq (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) \<and> valid_machine_state (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>state irq s. \<lbrakk>valid_pspace s; \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s); \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> (\<exists>cap\<in>ran (caps_of_state s). irq \<in> cap_irqs cap) \<longrightarrow> state = IRQSignal
 2. \<And>state irq s. \<lbrakk>valid_pspace s; \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s); \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_irq_states_but irq (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) \<and> valid_machine_state (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>state irq s. \<lbrakk>valid_pspace s; \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s); \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; tcb_at (cur_thread s) s; state \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap irq \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_irq_states_but irq (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) \<and> valid_machine_state (s\<lparr>interrupt_states := \<lambda>a. if a = irq then state else interrupt_states s a\<rparr>) proof (prove)
goal:
No subgoals!