theory Interrupt_C

lemma invokeIRQHandler_ClearIRQHandler_ccorres:
  "ccorres dc xfdc
          (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and K(irq \<le> 0xFF))
          (UNIV \<inter> {s. irq_' s = ucast irq}) []
      (InterruptDecls_H.invokeIRQHandler (ClearIRQHandler irq))
      (Call invokeIRQHandler_ClearIRQHandler_'proc)" apply (cinit lift: irq_' simp: Interrupt_H.invokeIRQHandler_def) apply (rule ccorres_Guard_intStateIRQNode_array_Ptr) apply (rule ccorres_move_array_assertion_irq) apply simp apply (ctac(no_vcg) add: getIRQSlot_ccorres[simplified]) apply (rule ccorres_symb_exec_r) apply (ctac add: cteDeleteOne_ccorres[where w="-1"]) apply vcg apply (rule conseqPre, vcg,
            clarsimp simp: rf_sr_def gs_set_assn_Delete_cstate_relation[unfolded o_def]) apply (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) apply wp apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def
                    ghost_assertion_data_set_def) apply (clarsimp simp: cte_at_irq_node' ucast_nat_def) apply (drule word_le_nat_alt[THEN iffD1]) apply clarsimp apply (case_tac "of_int (uint irq) \<noteq> 0 \<longrightarrow> 0 < unat irq") by (auto simp: Collect_const_mem unat_eq_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and K (irq \<le> 0xFF)) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>) [] (InterruptDecls_H.invokeIRQHandler (irqhandler_invocation.ClearIRQHandler irq)) (Call invokeIRQHandler_ClearIRQHandler_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>irqa. irqa = UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> ccorres dc xfdc (?Q203 irqa) (?Q'203 irqa) [SKIP] (getIRQSlot irq >>= cteDeleteOne) (Guard C_Guard {s. s \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr} (Guard MemorySafety \<lbrace>irqa = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irqa) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>irqSlot :== cte_Ptr (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C)))));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
CALL cteDeleteOne_'proc(\<acute>irqSlot)))
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q203 irqa s \<and> s' \<in> ?Q'203 irqa proof (prove)
goal (2 subgoals):
 1. \<And>irqa. irqa = UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> ccorres dc xfdc (?Q203 irqa) (?Q'203 irqa) [SKIP] (getIRQSlot irq >>= cteDeleteOne) (Guard MemorySafety \<lbrace>irqa = 0 \<or> array_assertion intStateIRQNode_Ptr (unat irqa) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>irqSlot :== cte_Ptr (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C))));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
CALL cteDeleteOne_'proc(\<acute>irqSlot)))
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q203 irqa s \<and> s' \<in> ?Q'203 irqa proof (prove)
goal (2 subgoals):
 1. \<And>irqa. irqa = UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> ccorres dc xfdc (?A211 irqa) (?C'211 irqa) [SKIP] (getIRQSlot irq >>= cteDeleteOne) (\<acute>irqSlot :== cte_Ptr (symbol_table ''intStateIRQNode'' + irqa * word_of_nat (size_of TYPE(cte_C)));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
CALL cteDeleteOne_'proc(\<acute>irqSlot)))
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A211 irqa and (\<lambda>s. True)) s \<and> s' \<in> ?C'211 irqa \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?A211 (UCAST(10 \<rightarrow> 32) irq)) (?C'211 (UCAST(10 \<rightarrow> 32) irq)) [SKIP] (getIRQSlot irq >>= cteDeleteOne) (\<acute>irqSlot :== cte_Ptr (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)));;
(\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
CALL cteDeleteOne_'proc(\<acute>irqSlot)))
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A211 irqa and (\<lambda>s. True)) s \<and> s' \<in> ?C'211 irqa \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv irqSlot. ((=) \<circ> cte_Ptr) rv irqSlot \<Longrightarrow> ccorres dc xfdc (?Q225 rv) (?Q'225 rv irqSlot) [SKIP] (cteDeleteOne rv) (\<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1));;
CALL cteDeleteOne_'proc(irqSlot))
 2. \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q225\<rbrace>
 3. \<And>s rv. ((=) \<circ> cte_Ptr) rv (irqSlot_' s) \<Longrightarrow> s \<in> ?Q'225 rv (irqSlot_' s)
 4. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R229 irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv irqSlot. ((=) \<circ> cte_Ptr) rv irqSlot \<Longrightarrow> ccorres dc xfdc (?Q225 rv) (?Q'286 rv irqSlot) [SKIP] (cteDeleteOne rv) (CALL cteDeleteOne_'proc(irqSlot))
 2. \<And>rv irqSlot. ((=) \<circ> cte_Ptr) rv irqSlot \<Longrightarrow> \<Gamma>\<turnstile> (?Q'225 rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) (?Q'286 rv irqSlot)
 3. \<And>rv irqSlot s. \<lbrakk>((=) \<circ> cte_Ptr) rv irqSlot; ?Q225 rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'225 rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 4. \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>?Q225\<rbrace>
 5. \<And>s rv. ((=) \<circ> cte_Ptr) rv (irqSlot_' s) \<Longrightarrow> s \<in> ?Q'225 rv (irqSlot_' s)
 6. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R229 irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv irqSlot. ((=) \<circ> cte_Ptr) rv irqSlot \<Longrightarrow> \<Gamma>\<turnstile> (?Q'225 rv irqSlot) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s. slot_'_update (\<lambda>_. irqSlot) s \<in> \<lbrace>gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = - 1\<rbrace> \<inter> \<lbrace>\<acute>slot = cte_Ptr rv\<rbrace>}
 2. \<And>rv irqSlot s. \<lbrakk>((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'225 rv irqSlot \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 3. \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a\<rbrace>
 4. \<And>s rv. ((=) \<circ> cte_Ptr) rv (irqSlot_' s) \<Longrightarrow> s \<in> ?Q'225 rv (irqSlot_' s)
 5. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R229 irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv irqSlot s. \<lbrakk>((=) \<circ> cte_Ptr) rv irqSlot; (invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> irqSlot = cte_Ptr rv\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>globals :== ghost'state_'_update (gs_set_assn cteDeleteOne_'proc (- 1)) {s'. (s, s') \<in> rf_sr}
 2. \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a\<rbrace>
 3. \<And>s rv. ((=) \<circ> cte_Ptr) rv (irqSlot_' s) \<Longrightarrow> s \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv\<rbrace>
 4. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R229 irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> getIRQSlot irq \<lbrace>\<lambda>a. invs' and cte_wp_at' (\<lambda>ct. - 1 = - 1 \<or> cteCap ct = capability.NullCap \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = - 1)) a\<rbrace>
 2. \<And>s rv. ((=) \<circ> cte_Ptr) rv (irqSlot_' s) \<Longrightarrow> s \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv\<rbrace>
 3. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R229 irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R229 (UCAST(10 \<rightarrow> 32) irq)\<rbrace> do node <- liftM intStateIRQNode (gets ksInterruptState);
return (node + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od \<lbrace>\<lambda>a b. invs' b \<and> cte_wp_at' (\<lambda>ct. True) a b\<rbrace>
 2. \<And>s rv. ((=) \<circ> cte_Ptr) rv (irqSlot_' s) \<Longrightarrow> s \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv\<rbrace>
 3. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R229 irqa and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s rv. ((=) \<circ> cte_Ptr) rv (irqSlot_' s) \<Longrightarrow> s \<in> \<lbrace>ghost_assertion_data_get cteDeleteOne_'proc (\<lambda>x. snd (snd x)) (ghost_assertion_data_set cteDeleteOne_'proc (- 1) (\<lambda>x. apsnd (apsnd x)) \<acute>ghost'state) = - 1 \<and> \<^bsup>s\<^esup>irqSlot = cte_Ptr rv\<rbrace>
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. ((\<lambda>x a. invs' a \<and> cte_wp_at' (\<lambda>ct. True) (x + 2 ^ cte_level_bits * irqa) a) \<circ> intStateIRQNode) (ksInterruptState a) a) and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>y. irq \<le> 0xFF)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. ((\<lambda>x a. invs' a \<and> cte_wp_at' (\<lambda>ct. True) (x + 2 ^ cte_level_bits * irqa) a) \<circ> intStateIRQNode) (ksInterruptState a) a) and (\<lambda>s. True)) s \<and> s' \<in> UNIV \<inter> \<lbrace>unat irqa \<le> 256 \<and> (irqa \<noteq> 0 \<longrightarrow> unat irqa \<noteq> 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s; irq \<le> 0xFF\<rbrakk> \<Longrightarrow> s' \<in> (if unat irq \<le> 256 \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> 0 < unat irq) then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s; unat irq \<le> unat 0xFF\<rbrakk> \<Longrightarrow> s' \<in> (if unat irq \<le> 256 \<and> (UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> 0 < unat irq) then UNIV else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s; unat irq \<le> 255\<rbrakk> \<Longrightarrow> s' \<in> (if UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> 0 < unat irq then UNIV else {}) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s; unat irq \<le> 255; of_int (uint irq) \<noteq> (0::?'a322) \<longrightarrow> 0 < unat irq\<rbrakk> \<Longrightarrow> s' \<in> (if UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> 0 < unat irq then UNIV else {})
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; weak_sch_act_wf (ksSchedulerAction s) s; unat irq \<le> 255; \<not> (of_int (uint irq) \<noteq> (0::?'a322) \<longrightarrow> 0 < unat irq)\<rbrakk> \<Longrightarrow> s' \<in> (if UCAST(10 \<rightarrow> 32) irq \<noteq> 0 \<longrightarrow> 0 < unat irq then UNIV else {})