theory ArchADT_IF_Refine_C

lemma handleInterrupt_ccorres[ADT_IF_Refine_assms]:
  "ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs') (UNIV) []
           (handleEvent Interrupt) (handleInterruptEntry_C_body_if)" proof - show ?thesis apply (rule ccorres_guard_imp2) apply (simp add: handleEvent_def minus_one_norm handleInterruptEntry_C_body_if_def irqInvalid_def2) apply (clarsimp simp: liftE_def bind_assoc) apply (rule ccorres_rhs_assoc) apply (ctac (no_vcg) add: getActiveIRQ_ccorres) apply (rule ccorres_Guard_Seq) apply (rule_tac P="rv \<noteq> Some 0xFFFF" in ccorres_gen_asm) apply wpc apply (simp add: ccorres_cond_empty_iff) apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply (clarsimp simp: ucast_helper_simps_32 ucast_not_helper ccorres_cond_univ_iff ucast_ucast_a is_down) apply (ctac (no_vcg) add: handleInterrupt_ccorres) apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply wp apply (rule_tac Q="\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)
                                     \<and> rv \<noteq> Some 0xFFFF" in hoare_post_imp) apply (clarsimp simp: Kernel_C.maxIRQ_def ARM.maxIRQ_def) apply (wp getActiveIRQ_le_maxIRQ getActiveIRQ_neq_Some0xFF | simp)+ apply (clarsimp simp: invs'_def valid_state'_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') invs' UNIV [] (handleEvent Interrupt) handleInterruptEntry_C_body_if proof (state)
goal (1 subgoal):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') invs' UNIV [] (handleEvent Interrupt) handleInterruptEntry_C_body_if proof (prove)
goal (1 subgoal):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') invs' UNIV [] (handleEvent Interrupt) handleInterruptEntry_C_body_if proof (prove)
goal (2 subgoals):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') ?Q ?Q' [] (handleEvent Interrupt) handleInterruptEntry_C_body_if
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') ?Q ?Q' [] (liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)) (\<acute>irq :== CALL getActiveIRQ_'proc();;
Guard SignedArithmetic UNIV (IF \<acute>irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc()
FI);;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') ?Q ?Q' [] (do x <- doMachineOp (getActiveIRQ False);
r <- case x of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
return (Inr ())
od) (\<acute>irq :== CALL getActiveIRQ_'proc();;
Guard SignedArithmetic UNIV (IF \<acute>irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc()
FI);;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') ?Q ?Q' [] (do x <- doMachineOp (getActiveIRQ False);
r <- case x of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
return (Inr ())
od) (\<acute>irq :== CALL getActiveIRQ_'proc();;
(Guard SignedArithmetic UNIV (IF \<acute>irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc()
FI);;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<And>rv irq. case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q13 rv) (?Q'13 rv irq) [] (do r <- case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
return (Inr ())
od) (Guard SignedArithmetic UNIV (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI);;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?Q13\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?Q'13 rv (ret__unsigned_long_' t)} proof (prove)
goal (3 subgoals):
 1. \<And>rv irq. case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q13 rv) (?C'85 rv irq) [] (do r <- case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
return (Inr ())
od) (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI;;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>?Q13\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?C'85 rv (ret__unsigned_long_' t) \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>rv irq. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF\<rbrakk> \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?G88 rv) (?C'85 rv irq) [] (do r <- case rv of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
return (Inr ())
od) (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI;;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. ?G88 rv and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> ?C'85 rv (ret__unsigned_long_' t) \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>rv irq. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = None\<rbrakk> \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R97 rv) (?R''99 rv irq) [] (do r <- return ();
return (Inr ())
od) (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI;;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R98 rv x2) (?R''100 rv irq x2) [] (do r <- handleInterrupt x2;
return (Inr ())
od) (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI;;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 3. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> ?R97 rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R98 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''99 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''100 rv (ret__unsigned_long_' t) x}} \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R97 None) (?R''99 None 0xFFFF) [] (return (Inr ())) (\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R98 rv x2) (?R''100 rv irq x2) [] (do r <- handleInterrupt x2;
return (Inr ())
od) (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI;;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 3. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> ?R97 rv s) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R98 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> ?R''99 rv (ret__unsigned_long_' t)} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''100 rv (ret__unsigned_long_' t) x}} \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (K dc \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R98 rv x2) (?R''100 rv irq x2) [] (do r <- handleInterrupt x2;
return (Inr ())
od) (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI;;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 3. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R98 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''100 rv (ret__unsigned_long_' t) x}} \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rparr>) \<in> rf_sr \<and> (K dc \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rparr>))}
 2. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R98 rv x2) (?R''100 rv irq x2) [] (do r <- handleInterrupt x2;
return (Inr ())
od) (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI;;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 3. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R98 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''100 rv (ret__unsigned_long_' t) x}} \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>rv irq x2. \<lbrakk>case rv of None \<Rightarrow> irq = 0xFFFF | Some x \<Rightarrow> irq = UCAST(10 \<rightarrow> 32) x; rv \<noteq> Some 0xFFFF; rv = Some x2\<rbrakk> \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R98 rv x2) (?R''100 rv irq x2) [] (do r <- handleInterrupt x2;
return (Inr ())
od) (IF irq \<noteq> 0xFFFF THEN
  CALL handleInterrupt_'proc(irq)
FI;;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R98 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''100 rv (ret__unsigned_long_' t) x}} \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R98 (Some x2) x2) (?R''100 (Some x2) (UCAST(10 \<rightarrow> 32) x2) x2) [] (do r <- handleInterrupt x2;
return (Inr ())
od) (CALL handleInterrupt_'proc(UCAST(10 \<rightarrow> 32) x2);;
\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> ?R98 rv x s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> ?R''100 rv (ret__unsigned_long_' t) x}} \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q150 x2 rv) (?Q'150 x2 rv xfdc) [] (return (Inr ())) (\<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)
 2. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R159 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>?Q150 x2\<rbrace>
 3. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R159 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'156 rv (ret__unsigned_long_' t) x ta rva}}} \<inter> UNIV}
flex-flex pairs:
\<lambda>x2. ?Q'156 (Some x2) (UCAST(10 \<rightarrow> 32) x2) x2 \<equiv>\<^sup>? \<lambda>x2 t rv. ?Q'150 x2 rv (xfdc t) proof (prove)
goal (4 subgoals):
 1. \<And>x2 rv xfdc. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned_long :== SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (K dc \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R159 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R159 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}} \<inter> UNIV} proof (prove)
goal (4 subgoals):
 1. \<And>x2 rv xfdc \<sigma>. \<lbrakk>x2 \<noteq> 0x3FF; dc rv xfdc\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rparr>) \<in> rf_sr \<and> (K dc \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rparr>))}
 2. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R159 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R159 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}} \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>x2. x2 \<noteq> 0x3FF \<Longrightarrow> \<lbrace>?R159 (Some x2) x2\<rbrace> handleInterrupt x2 \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and ?R159 rv x) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}} \<inter> UNIV} proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. (\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and (\<lambda>a. True)) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)\<rbrace>
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}} \<inter> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> local.maxIRQ) \<and> rv \<noteq> Some 0xFFFF \<Longrightarrow> ((\<lambda>s. (rv = None \<longrightarrow> True) \<and> (\<forall>x. rv = Some x \<longrightarrow> (invs' and (\<lambda>a. True)) s)) and (\<lambda>_. rv \<noteq> Some 0xFFFF)) s
 2. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> local.maxIRQ) \<and> rv \<noteq> Some 0xFFFF\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}} \<inter> UNIV} proof (prove)
goal (2 subgoals):
 1. \<lbrace>?R13\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. invs' s \<and> (\<forall>x. rv = Some x \<longrightarrow> x \<le> local.maxIRQ) \<and> rv \<noteq> Some 0xFFFF\<rbrace>
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R13) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. (case rv of None \<Rightarrow> ret__unsigned_long_' t = 0xFFFF | Some x \<Rightarrow> ret__unsigned_long_' t = UCAST(10 \<rightarrow> 32) x) \<longrightarrow> irq_'_update (\<lambda>_. ret__unsigned_long_' t) (s'\<lparr>globals := globals t\<rparr>) \<in> {s. rv = None \<longrightarrow> s \<in> UNIV} \<inter> {s. \<forall>x. s \<in> {s. rv = Some x \<longrightarrow> s \<in> {s. irq_'_update (\<lambda>x. ret__unsigned_long_' t) s \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>t\<^esup>ret__unsigned_long\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}}} \<inter> UNIV} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s\<rbrakk> \<Longrightarrow> irqs_masked' s \<and> valid_irq_states' s proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') invs' UNIV [] (handleEvent Interrupt) handleInterruptEntry_C_body_if

goal:
No subgoals!