theory Syscall_C

lemma ccorres_pre_getIRQState:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows   "ccorres r xf
                  (\<lambda>s. irq \<le> ucast Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s)
                  {s. \<forall>rv. index (intStateIRQTable_' (globals s)) (unat irq) = irqstate_to_C rv \<longrightarrow> s \<in> P' rv }
                          hs (getIRQState irq >>= (\<lambda>rv. f rv)) c" apply (rule ccorres_guard_imp) apply (rule ccorres_symb_exec_l) defer apply (simp add: getIRQState_def getInterruptState_def) apply wp apply simp apply (rule getIRQState_sp) apply (simp add: getIRQState_def getInterruptState_def) apply assumption prefer 2 apply (rule ccorres_guard_imp) apply (rule cc) apply simp apply assumption apply clarsimp apply (erule allE) apply (erule impE) prefer 2 apply assumption apply (clarsimp simp: rf_sr_def cstate_relation_def
                        Let_def cinterrupt_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s) {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} hs (getIRQState irq >>= f) c proof (prove)
goal (3 subgoals):
 1. ccorres r xf ?Q ?Q' hs (getIRQState irq >>= f) c
 2. \<And>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c
 2. \<And>s. \<lbrace>(=) s\<rbrace> getIRQState irq \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getIRQState irq \<lbrace>?Q4\<rbrace>
 4. empty_fail (getIRQState irq)
 5. \<And>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q s
 6. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> getIRQState irq \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getIRQState irq \<lbrace>?Q4\<rbrace>
 3. empty_fail (getIRQState irq)
 4. \<And>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q s
 5. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv}
 6. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> liftM (swp id irq \<circ> intStateIRQTable) (gets ksInterruptState) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getIRQState irq \<lbrace>?Q4\<rbrace>
 3. empty_fail (getIRQState irq)
 4. \<And>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q s
 5. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv}
 6. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c proof (prove)
goal (6 subgoals):
 1. \<And>s sa. s = sa \<Longrightarrow> ((\<lambda>r. (=) s) \<circ> (swp id irq \<circ> intStateIRQTable)) (ksInterruptState sa) sa
 2. \<lbrace>?Q\<rbrace> getIRQState irq \<lbrace>?Q4\<rbrace>
 3. empty_fail (getIRQState irq)
 4. \<And>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q s
 5. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv}
 6. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q\<rbrace> getIRQState irq \<lbrace>?Q4\<rbrace>
 2. empty_fail (getIRQState irq)
 3. \<And>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q s
 4. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q4 rv s \<longrightarrow> s' \<in> ?Q'4 rv}
 5. \<And>rv. ccorres r xf (?Q4 rv) (?Q'4 rv) hs (f rv) c proof (prove)
goal (4 subgoals):
 1. empty_fail (getIRQState irq)
 2. \<And>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> rv = intStateIRQTable (ksInterruptState s) irq \<and> ?Q s \<longrightarrow> s' \<in> ?Q'4 rv}
 4. \<And>rv. ccorres r xf (\<lambda>s. rv = intStateIRQTable (ksInterruptState s) irq \<and> ?Q s) (?Q'4 rv) hs (f rv) c proof (prove)
goal (3 subgoals):
 1. \<And>s. irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q s
 2. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> rv = intStateIRQTable (ksInterruptState s) irq \<and> ?Q s \<longrightarrow> s' \<in> ?Q'4 rv}
 3. \<And>rv. ccorres r xf (\<lambda>s. rv = intStateIRQTable (ksInterruptState s) irq \<and> ?Q s) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<longrightarrow> s' \<in> ?Q'4 rv}
 2. \<And>rv. ccorres r xf (\<lambda>s. rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s) (?Q'4 rv) hs (f rv) c proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres r xf (\<lambda>s. rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s) (?Q'4 rv) hs (f rv) c
 2. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres r xf (?Q15 rv) (?Q'15 rv) hs (f rv) c
 2. \<And>rv s. rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> ?Q15 rv s
 3. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> ?Q'15 rv
 4. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (3 subgoals):
 1. \<And>rv s. rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<Longrightarrow> P rv s
 2. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> P' rv
 3. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (2 subgoals):
 1. \<And>rv s. s \<in> ?Q'4 rv \<Longrightarrow> s \<in> P' rv
 2. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<longrightarrow> s' \<in> ?Q'4 rv} proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> {s. \<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv} \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> rv = intStateIRQTable (ksInterruptState s) irq \<and> irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<and> P (intStateIRQTable (ksInterruptState s) irq) s \<longrightarrow> s' \<in> P' rv} proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>\<forall>rv. intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C rv \<longrightarrow> s \<in> P' rv; (sa, s) \<in> rf_sr; irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; P (intStateIRQTable (ksInterruptState sa) irq) sa\<rbrakk> \<Longrightarrow> s \<in> P' (intStateIRQTable (ksInterruptState sa) irq) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(sa, s) \<in> rf_sr; irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; P (intStateIRQTable (ksInterruptState sa) irq) sa; intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C (?rv26 s sa) \<longrightarrow> s \<in> P' (?rv26 s sa)\<rbrakk> \<Longrightarrow> s \<in> P' (intStateIRQTable (ksInterruptState sa) irq) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>(sa, s) \<in> rf_sr; irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; P (intStateIRQTable (ksInterruptState sa) irq) sa\<rbrakk> \<Longrightarrow> intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C (?rv26 s sa)
 2. \<And>s sa. \<lbrakk>(sa, s) \<in> rf_sr; irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; P (intStateIRQTable (ksInterruptState sa) irq) sa; s \<in> P' (?rv26 s sa)\<rbrakk> \<Longrightarrow> s \<in> P' (intStateIRQTable (ksInterruptState sa) irq) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>(sa, s) \<in> rf_sr; irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; P (intStateIRQTable (ksInterruptState sa) irq) sa; s \<in> P' (?rv26 s sa)\<rbrakk> \<Longrightarrow> s \<in> P' (intStateIRQTable (ksInterruptState sa) irq)
 2. \<And>s sa. \<lbrakk>(sa, s) \<in> rf_sr; irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; P (intStateIRQTable (ksInterruptState sa) irq) sa\<rbrakk> \<Longrightarrow> intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C (?rv26 s sa) proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(sa, s) \<in> rf_sr; irq \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ; P (intStateIRQTable (ksInterruptState sa) irq) sa\<rbrakk> \<Longrightarrow> intStateIRQTable_' (globals s).[unat irq] = irqstate_to_C (intStateIRQTable (ksInterruptState sa) irq) proof (prove)
goal:
No subgoals!