theory CSpace_C

lemma postCapDeletion_ccorres:
  "cleanup_info_wf' cap \<Longrightarrow>
   ccorres dc xfdc
      \<top> (UNIV \<inter> {s. ccap_relation cap (cap_' s)}) hs
      (postCapDeletion cap)
      (Call postCapDeletion_'proc)" supply Collect_const[simp del] apply (cinit lift: cap_' simp: Retype_H.postCapDeletion_def) apply csymbr apply (clarsimp simp: cap_get_tag_isCap) apply (rule ccorres_Cond_rhs) apply (clarsimp simp: isCap_simps ) apply (rule ccorres_symb_exec_r) apply (rule_tac xf'=irq_' in ccorres_abstract, ceqv) apply (rule_tac P="rv' = ucast (capIRQ cap)" in ccorres_gen_asm2) apply (frule cap_get_tag_to_H, solves \<open>clarsimp simp: cap_get_tag_isCap_unfolded_H_cap\<close>) apply (clarsimp simp: cap_irq_handler_cap_lift) apply (ctac(no_vcg) add: deletedIRQHandler_ccorres) apply vcg apply (rule conseqPre, vcg) apply clarsimp apply csymbr apply (clarsimp simp: cap_get_tag_isCap) apply (rule ccorres_Cond_rhs) apply (wpc; clarsimp simp: isCap_simps) apply (ctac(no_vcg) add: Arch_postCapDeletion_ccorres) apply (simp add: not_irq_or_arch_cap_case) apply (rule ccorres_return_Skip) apply clarsimp apply (rule conjI, clarsimp simp: isCap_simps  Kernel_C.maxIRQ_def) apply (frule cap_get_tag_isCap_unfolded_H_cap(5)) apply (clarsimp simp: cap_irq_handler_cap_lift ccap_relation_def cap_to_H_def
                         cleanup_info_wf'_def maxIRQ_def Kernel_C.maxIRQ_def) apply (rule conjI, clarsimp simp: isCap_simps) apply (rule conjI[rotated], clarsimp simp: isCap_simps) apply (clarsimp simp: isCap_simps) apply (frule cap_get_tag_isCap_unfolded_H_cap(5)) apply (clarsimp simp: cap_irq_handler_cap_lift ccap_relation_def cap_to_H_def
                        cleanup_info_wf'_def c_valid_cap_def cl_valid_cap_def mask_def) apply (clarsimp simp: word_size Kernel_C.maxIRQ_def maxIRQ_def) by word_bitwise

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cleanup_info_wf' cap \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace>) hs (global.postCapDeletion cap) (Call postCapDeletion_'proc) proof (prove)
goal (1 subgoal):
 1. cleanup_info_wf' cap \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace>) hs (global.postCapDeletion cap) (Call postCapDeletion_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q180 capa) (?Q'180 capa) (SKIP # hs) (case cap of capability.IRQHandlerCap irq \<Rightarrow> deletedIRQHandler irq | capability.ArchObjectCap c \<Rightarrow> Arch.postCapDeletion c | _ \<Rightarrow> return ()) (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(capa);;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap THEN
  \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned;;
CALL deletedIRQHandler_'proc(\<acute>irq)
ELSE
  \<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI
FI)
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q180 capa s \<and> s' \<in> ?Q'180 capa proof (prove)
goal (2 subgoals):
 1. \<And>capa ret__unsigned. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; ret__unsigned = cap_get_tag capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q180 capa) (?G'189 capa ret__unsigned) (SKIP # hs) (case cap of capability.IRQHandlerCap irq \<Rightarrow> deletedIRQHandler irq | capability.ArchObjectCap c \<Rightarrow> Arch.postCapDeletion c | _ \<Rightarrow> return ()) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap THEN
  \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned;;
CALL deletedIRQHandler_'proc(\<acute>irq)
ELSE
  \<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI
FI)
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q180 capa s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> ?G'189 capa v} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q180 capa) (?G'189 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (IF isIRQHandlerCap cap THEN
  \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned;;
CALL deletedIRQHandler_'proc()
ELSE
  \<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI
FI)
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q180 capa s \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> ?G'189 capa v} proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q327 capa) (?S331 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned;;
CALL deletedIRQHandler_'proc())
 2. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 3. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> ?Q327 capa s) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> ?S331 capa v) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (3 subgoals):
 1. \<And>capa v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q327 capa) (?S331 capa (cap_get_tag capa)) (SKIP # hs) (deletedIRQHandler v0) (\<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned;;
CALL deletedIRQHandler_'proc())
 2. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 3. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> ?Q327 capa s) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> ?S331 capa v) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (5 subgoals):
 1. \<And>capa v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q327 capa) (?Q'343 capa v0) (SKIP # hs) (deletedIRQHandler v0) (CALL deletedIRQHandler_'proc())
 2. \<And>capa v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa)) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned (?Q'343 capa v0)
 3. \<And>capa v0 s. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; ?Q327 capa s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s'. (s, s') \<in> rf_sr}
 4. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 5. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> ?Q327 capa s) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> ?S331 capa v) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (5 subgoals):
 1. \<And>capa v0 rv'. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q327 capa) (?G'349 capa v0 rv') (SKIP # hs) (deletedIRQHandler v0) (CALL deletedIRQHandler_'proc(rv'))
 2. \<And>capa v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa)) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s. s \<in> ?G'349 capa v0 (irq_' s)}
 3. \<And>capa v0 s. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; ?Q327 capa s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s'. (s, s') \<in> rf_sr}
 4. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 5. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> ?Q327 capa s) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> ?S331 capa v) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (5 subgoals):
 1. \<And>capa v0 rv'. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; rv' = UCAST(10 \<rightarrow> 32) (capIRQ cap)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q327 capa) (?G'370 capa v0 rv') (SKIP # hs) (deletedIRQHandler v0) (CALL deletedIRQHandler_'proc(rv'))
 2. \<And>capa v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa)) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s. s \<in> ?G'370 capa v0 (irq_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>irq = UCAST(10 \<rightarrow> 32) (capIRQ cap)\<rbrace>}
 3. \<And>capa v0 s. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; ?Q327 capa s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s'. (s, s') \<in> rf_sr}
 4. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 5. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> ?Q327 capa s) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> ?S331 capa v) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (5 subgoals):
 1. \<And>capa v0 rv'. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; rv' = UCAST(10 \<rightarrow> 32) (capIRQ cap); capability.IRQHandlerCap v0 = capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q327 capa) (?G'370 capa v0 rv') (SKIP # hs) (deletedIRQHandler v0) (CALL deletedIRQHandler_'proc(rv'))
 2. \<And>capa v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa)) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s. s \<in> ?G'370 capa v0 (irq_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>irq = UCAST(10 \<rightarrow> 32) (capIRQ cap)\<rbrace>}
 3. \<And>capa v0 s. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; ?Q327 capa s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s'. (s, s') \<in> rf_sr}
 4. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 5. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> ?Q327 capa s) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> ?S331 capa v) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (5 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa)))); ccap_relation (capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa)))) capa; cap = capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa)))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q327 capa) (?G'370 capa (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))))) (SKIP # hs) (deletedIRQHandler (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa)))) (CALL deletedIRQHandler_'proc(UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa)))))
 2. \<And>capa v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa)) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s. s \<in> ?G'370 capa v0 (irq_' s) \<inter> \<lbrace>\<^bsup>s\<^esup>irq = UCAST(10 \<rightarrow> 32) (capIRQ cap)\<rbrace>}
 3. \<And>capa v0 s. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; ?Q327 capa s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s'. (s, s') \<in> rf_sr}
 4. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 5. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> ?Q327 capa s) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> ?S331 capa v) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (4 subgoals):
 1. \<And>capa v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa)) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s. s \<in> {sa. irq_'_update (\<lambda>x. irq_' s) sa \<in> UNIV \<inter> \<lbrace>\<acute>irq = \<^bsup>s\<^esup>irq\<rbrace>} \<inter> \<lbrace>\<^bsup>s\<^esup>irq = UCAST(10 \<rightarrow> 32) (capIRQ cap)\<rbrace>}
 2. \<And>capa v0 s. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?S331 capa (cap_get_tag capa) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s'. (s, s') \<in> rf_sr}
 3. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 4. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> ?S331 capa v) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (3 subgoals):
 1. \<And>capa v0 s. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL cap_irq_handler_cap_get_capIRQ_'proc(capa);;
\<acute>irq :== \<acute>ret__unsigned {s'. (s, s') \<in> rf_sr}
 2. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 3. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (3 subgoals):
 1. \<And>capa v0 s. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; cap = capability.IRQHandlerCap v0; UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> \<lbrace>cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> (s, irq_'_update (\<lambda>_. capIRQ_CL (cap_irq_handler_cap_lift capa)) (sa\<lparr>ret__unsigned_' := capIRQ_CL (cap_irq_handler_cap_lift capa)\<rparr>)) \<in> rf_sr)}
 2. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 3. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?T330 capa (cap_get_tag capa)) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (\<acute>ret__unsigned_long :== CALL isArchCap_'proc(capa);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> ?T330 capa v)}} proof (prove)
goal (2 subgoals):
 1. \<And>capa ret__unsigned_long. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap; ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag capa))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?G'447 capa (cap_get_tag capa) ret__unsigned_long) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (IF ret__unsigned_long \<noteq> 0 THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> {s. \<forall>va. va = from_bool (isArchCap_tag (cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> ?G'447 capa v va})}} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R327 capa) (?G'447 capa (cap_get_tag capa) (from_bool (isArchCap (\<lambda>_. True) cap))) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (IF isArchCap (\<lambda>_. True) cap THEN
  CALL Arch_postCapDeletion_'proc(capa)
FI)
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> ?R327 capa s)) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> {s. \<forall>va. va = from_bool (isArchCap_tag (cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> ?G'447 capa v va})}} proof (prove)
goal (3 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap; isArchCap (\<lambda>_. True) cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q506 capa) (?S510 capa (cap_get_tag capa) (from_bool (isArchCap (\<lambda>_. True) cap))) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) (CALL Arch_postCapDeletion_'proc(capa))
 2. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap; \<not> isArchCap (\<lambda>_. True) cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R506 capa) (?T509 capa (cap_get_tag capa) (from_bool (isArchCap (\<lambda>_. True) cap))) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) SKIP
 3. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> (isArchCap (\<lambda>_. True) cap \<longrightarrow> ?Q506 capa s) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> ?R506 capa s))) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> {s. \<forall>va. va = from_bool (isArchCap_tag (cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> {s. (isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> ?S510 capa v va) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> ?T509 capa v va)}})}} proof (prove)
goal (3 subgoals):
 1. \<And>capa x8. \<lbrakk>cleanup_info_wf' (capability.ArchObjectCap x8); ccap_relation (capability.ArchObjectCap x8) capa; cap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R544 capa x8) (?R''584 capa (cap_get_tag capa) (SCAST(32 signed \<rightarrow> 32) true) x8) (SKIP # hs) (Arch.postCapDeletion x8) (CALL Arch_postCapDeletion_'proc(capa))
 2. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap; \<not> isArchCap (\<lambda>_. True) cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R506 capa) (?T509 capa (cap_get_tag capa) (from_bool (isArchCap (\<lambda>_. True) cap))) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) SKIP
 3. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> (isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> ?R566 capa x s) \<and> (cap = capability.NullCap \<longrightarrow> ?R564 capa s) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> ?R563 capa x xa xb xc s) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> ?R558 capa x s) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> ?R556 capa x xa xb xc xd xe s) \<and> (cap = capability.DomainCap \<longrightarrow> ?R549 capa s) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> ?R548 capa x xa xb s) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> ?R544 capa x s) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> ?R542 capa x xa xb s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R538 capa x xa xb xc s) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R533 capa x xa xb xc s) \<and> (cap = capability.IRQControlCap \<longrightarrow> ?R528 capa s)) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> ?R506 capa s))) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> {s. \<forall>va. va = from_bool (isArchCap_tag (cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> {s. (isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. cap = capability.ThreadCap x \<longrightarrow> s \<in> ?R''591 capa v va x}} \<inter> ({s. cap = capability.NullCap \<longrightarrow> s \<in> ?R''590 capa v va} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> ?R''589 capa v va x xa xb xc}}}}} \<inter> ({s. \<forall>x. s \<in> {s. cap = capability.IRQHandlerCap x \<longrightarrow> s \<in> ?R''588 capa v va x}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> ?R''587 capa v va x xa xb xc xd xe}}}}}}} \<inter> ({s. cap = capability.DomainCap \<longrightarrow> s \<in> ?R''586 capa v va} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. cap = capability.Zombie x xa xb \<longrightarrow> s \<in> ?R''585 capa v va x xa xb}}}} \<inter> ({s. \<forall>x. s \<in> {s. cap = capability.ArchObjectCap x \<longrightarrow> s \<in> ?R''584 capa v va x}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. cap = capability.ReplyCap x xa xb \<longrightarrow> s \<in> ?R''583 capa v va x xa xb}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s \<in> ?R''582 capa v va x xa xb xc}}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s \<in> ?R''581 capa v va x xa xb xc}}}}} \<inter> {s. cap = capability.IRQControlCap \<longrightarrow> s \<in> ?R''580 capa v va}))))))))))) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> ?T509 capa v va)}})}} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap; \<not> isArchCap (\<lambda>_. True) cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R506 capa) (?T509 capa (cap_get_tag capa) (from_bool (isArchCap (\<lambda>_. True) cap))) (SKIP # hs) (case cap of capability.IRQHandlerCap x \<Rightarrow> deletedIRQHandler x | capability.ArchObjectCap x \<Rightarrow> Arch.postCapDeletion x | _ \<Rightarrow> return ()) SKIP
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> (isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> ?R566 capa x s) \<and> (cap = capability.NullCap \<longrightarrow> ?R564 capa s) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> ?R563 capa x xa xb xc s) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> ?R558 capa x s) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> ?R556 capa x xa xb xc xd xe s) \<and> (cap = capability.DomainCap \<longrightarrow> ?R549 capa s) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> ?R548 capa x xa xb s) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> ?R542 capa x xa xb s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R538 capa x xa xb xc s) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R533 capa x xa xb xc s) \<and> (cap = capability.IRQControlCap \<longrightarrow> ?R528 capa s)) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> ?R506 capa s))) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> {s. \<forall>va. va = from_bool (isArchCap_tag (cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> {s. (isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. cap = capability.ThreadCap x \<longrightarrow> s \<in> ?R''591 capa v va x}} \<inter> ({s. cap = capability.NullCap \<longrightarrow> s \<in> ?R''590 capa v va} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> ?R''589 capa v va x xa xb xc}}}}} \<inter> ({s. \<forall>x. s \<in> {s. cap = capability.IRQHandlerCap x \<longrightarrow> s \<in> ?R''588 capa v va x}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> ?R''587 capa v va x xa xb xc xd xe}}}}}}} \<inter> ({s. cap = capability.DomainCap \<longrightarrow> s \<in> ?R''586 capa v va} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. cap = capability.Zombie x xa xb \<longrightarrow> s \<in> ?R''585 capa v va x xa xb}}}} \<inter> ({s. \<forall>x. s \<in> {s. cap = capability.ArchObjectCap x \<longrightarrow> s \<in> {s. cap_'_update (\<lambda>_. capa) s \<in> UNIV \<inter> \<lbrace>ccap_relation (capability.ArchObjectCap x) \<acute>cap\<rbrace>}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. cap = capability.ReplyCap x xa xb \<longrightarrow> s \<in> ?R''583 capa v va x xa xb}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s \<in> ?R''582 capa v va x xa xb xc}}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s \<in> ?R''581 capa v va x xa xb xc}}}}} \<inter> {s. cap = capability.IRQControlCap \<longrightarrow> s \<in> ?R''580 capa v va}))))))))))) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> ?T509 capa v va)}})}} proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; \<not> isIRQHandlerCap cap; \<not> isArchCap (\<lambda>_. True) cap\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R506 capa) (?T509 capa (cap_get_tag capa) (SCAST(32 signed \<rightarrow> 32) false)) (SKIP # hs) (return ()) SKIP
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> (isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> ?R566 capa x s) \<and> (cap = capability.NullCap \<longrightarrow> ?R564 capa s) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> ?R563 capa x xa xb xc s) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> ?R558 capa x s) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> ?R556 capa x xa xb xc xd xe s) \<and> (cap = capability.DomainCap \<longrightarrow> ?R549 capa s) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> ?R548 capa x xa xb s) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> ?R542 capa x xa xb s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R538 capa x xa xb xc s) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R533 capa x xa xb xc s) \<and> (cap = capability.IRQControlCap \<longrightarrow> ?R528 capa s)) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> ?R506 capa s))) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> {s. \<forall>va. va = from_bool (isArchCap_tag (cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> {s. (isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. cap = capability.ThreadCap x \<longrightarrow> s \<in> ?R''591 capa v va x}} \<inter> ({s. cap = capability.NullCap \<longrightarrow> s \<in> ?R''590 capa v va} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> ?R''589 capa v va x xa xb xc}}}}} \<inter> ({s. \<forall>x. s \<in> {s. cap = capability.IRQHandlerCap x \<longrightarrow> s \<in> ?R''588 capa v va x}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> ?R''587 capa v va x xa xb xc xd xe}}}}}}} \<inter> ({s. cap = capability.DomainCap \<longrightarrow> s \<in> ?R''586 capa v va} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. cap = capability.Zombie x xa xb \<longrightarrow> s \<in> ?R''585 capa v va x xa xb}}}} \<inter> ({s. \<forall>x. s \<in> {s. cap = capability.ArchObjectCap x \<longrightarrow> s \<in> {s. cap_'_update (\<lambda>_. capa) s \<in> UNIV \<inter> \<lbrace>ccap_relation (capability.ArchObjectCap x) \<acute>cap\<rbrace>}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. cap = capability.ReplyCap x xa xb \<longrightarrow> s \<in> ?R''583 capa v va x xa xb}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s \<in> ?R''582 capa v va x xa xb xc}}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s \<in> ?R''581 capa v va x xa xb xc}}}}} \<inter> {s. cap = capability.IRQControlCap \<longrightarrow> s \<in> ?R''580 capa v va}))))))))))) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> ?T509 capa v va)}})}} proof (prove)
goal (1 subgoal):
 1. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> (isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> ?R566 capa x s) \<and> (cap = capability.NullCap \<longrightarrow> ?R564 capa s) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> ?R563 capa x xa xb xc s) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> ?R558 capa x s) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> ?R556 capa x xa xb xc xd xe s) \<and> (cap = capability.DomainCap \<longrightarrow> ?R549 capa s) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> ?R548 capa x xa xb s) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> ?R542 capa x xa xb s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R538 capa x xa xb xc s) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R533 capa x xa xb xc s) \<and> (cap = capability.IRQControlCap \<longrightarrow> ?R528 capa s)) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> True))) \<and> s' \<in> {s. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. (isIRQHandlerCap cap \<longrightarrow> s \<in> \<lbrace>v = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = capIRQ_CL (cap_irq_handler_cap_lift capa) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))\<rbrace>) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> s \<in> {s. \<forall>va. va = from_bool (isArchCap_tag (cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)))) \<longrightarrow> s\<lparr>ret__unsigned_long_' := va\<rparr> \<in> {s. (isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. cap = capability.ThreadCap x \<longrightarrow> s \<in> ?R''591 capa v va x}} \<inter> ({s. cap = capability.NullCap \<longrightarrow> s \<in> ?R''590 capa v va} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> ?R''589 capa v va x xa xb xc}}}}} \<inter> ({s. \<forall>x. s \<in> {s. cap = capability.IRQHandlerCap x \<longrightarrow> s \<in> ?R''588 capa v va x}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> ?R''587 capa v va x xa xb xc xd xe}}}}}}} \<inter> ({s. cap = capability.DomainCap \<longrightarrow> s \<in> ?R''586 capa v va} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. cap = capability.Zombie x xa xb \<longrightarrow> s \<in> ?R''585 capa v va x xa xb}}}} \<inter> ({s. \<forall>x. s \<in> {s. cap = capability.ArchObjectCap x \<longrightarrow> s \<in> {s. cap_'_update (\<lambda>_. capa) s \<in> UNIV \<inter> \<lbrace>ccap_relation (capability.ArchObjectCap x) \<acute>cap\<rbrace>}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. cap = capability.ReplyCap x xa xb \<longrightarrow> s \<in> ?R''583 capa v va x xa xb}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s \<in> ?R''582 capa v va x xa xb xc}}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s \<in> ?R''581 capa v va x xa xb xc}}}}} \<inter> {s. cap = capability.IRQControlCap \<longrightarrow> s \<in> ?R''580 capa v va}))))))))))) \<and> (\<not> isArchCap (\<lambda>_. True) cap \<longrightarrow> s \<in> UNIV)}})}} proof (prove)
goal (1 subgoal):
 1. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (isIRQHandlerCap cap \<longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> ?R566 capa x s) \<and> (cap = capability.NullCap \<longrightarrow> ?R564 capa s) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> ?R563 capa x xa xb xc s) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> ?R558 capa x s) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> ?R556 capa x xa xb xc xd xe s) \<and> (cap = capability.DomainCap \<longrightarrow> ?R549 capa s) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> ?R548 capa x xa xb s) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> ?R542 capa x xa xb s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R538 capa x xa xb xc s) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R533 capa x xa xb xc s) \<and> (cap = capability.IRQControlCap \<longrightarrow> ?R528 capa s)) \<and> (isIRQHandlerCap cap \<longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> ((\<exists>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''591 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (cap = capability.NullCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''590 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''589 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''588 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''587 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc xd xe) \<and> (cap = capability.DomainCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''586 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''585 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> ccap_relation (capability.ArchObjectCap x) capa) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''583 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''582 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''581 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (cap = capability.IRQControlCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''580 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))))) proof (prove)
goal (2 subgoals):
 1. \<And>capa s s' v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; (s, s') \<in> rf_sr; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> 0x9F
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> ?R566 capa x s) \<and> (cap = capability.NullCap \<longrightarrow> ?R564 capa s) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> ?R563 capa x xa xb xc s) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> ?R558 capa x s) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> ?R556 capa x xa xb xc xd xe s) \<and> (cap = capability.DomainCap \<longrightarrow> ?R549 capa s) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> ?R548 capa x xa xb s) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> ?R542 capa x xa xb s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R538 capa x xa xb xc s) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R533 capa x xa xb xc s) \<and> (cap = capability.IRQControlCap \<longrightarrow> ?R528 capa s)) \<and> (isIRQHandlerCap cap \<longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> ((\<exists>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''591 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (cap = capability.NullCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''590 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''589 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''588 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''587 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc xd xe) \<and> (cap = capability.DomainCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''586 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''585 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> ccap_relation (capability.ArchObjectCap x) capa) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''583 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''582 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''581 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (cap = capability.IRQControlCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''580 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))))) proof (prove)
goal (2 subgoals):
 1. \<And>capa s s' v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; (s, s') \<in> rf_sr; cap = capability.IRQHandlerCap v0; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> 0x9F
 2. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> ?R566 capa x s) \<and> (cap = capability.NullCap \<longrightarrow> ?R564 capa s) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> ?R563 capa x xa xb xc s) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> ?R558 capa x s) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> ?R556 capa x xa xb xc xd xe s) \<and> (cap = capability.DomainCap \<longrightarrow> ?R549 capa s) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> ?R548 capa x xa xb s) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> ?R542 capa x xa xb s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R538 capa x xa xb xc s) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R533 capa x xa xb xc s) \<and> (cap = capability.IRQControlCap \<longrightarrow> ?R528 capa s)) \<and> (isIRQHandlerCap cap \<longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> ((\<exists>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''591 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (cap = capability.NullCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''590 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''589 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''588 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''587 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc xd xe) \<and> (cap = capability.DomainCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''586 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''585 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> ccap_relation (capability.ArchObjectCap x) capa) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''583 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''582 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''581 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (cap = capability.IRQControlCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''580 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))))) proof (prove)
goal (1 subgoal):
 1. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> ?R566 capa x s) \<and> (cap = capability.NullCap \<longrightarrow> ?R564 capa s) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> ?R563 capa x xa xb xc s) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> ?R558 capa x s) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> ?R556 capa x xa xb xc xd xe s) \<and> (cap = capability.DomainCap \<longrightarrow> ?R549 capa s) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> ?R548 capa x xa xb s) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> ?R542 capa x xa xb s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R538 capa x xa xb xc s) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R533 capa x xa xb xc s) \<and> (cap = capability.IRQControlCap \<longrightarrow> ?R528 capa s)) \<and> (isIRQHandlerCap cap \<longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> ((\<exists>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''591 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (cap = capability.NullCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''590 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''589 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''588 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''587 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc xd xe) \<and> (cap = capability.DomainCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''586 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''585 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> ccap_relation (capability.ArchObjectCap x) capa) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''583 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''582 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''581 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (cap = capability.IRQControlCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''580 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))))) proof (prove)
goal (1 subgoal):
 1. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (isIRQHandlerCap cap \<longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> ((\<exists>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap))) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> isArchCap (\<lambda>_. True) cap \<longrightarrow> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''591 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (cap = capability.NullCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''590 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''589 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''588 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''587 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc xd xe) \<and> (cap = capability.DomainCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''586 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa)))) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''585 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> ccap_relation (capability.ArchObjectCap x) capa) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''583 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''582 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''581 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))) x xa xb xc) \<and> (cap = capability.IRQControlCap \<longrightarrow> s'\<lparr>ret__unsigned_' := cap_get_tag capa, ret__unsigned_long_' := from_bool (isArchCap_tag (cap_get_tag capa))\<rparr> \<in> ?R''580 capa (cap_get_tag capa) (from_bool (isArchCap_tag (cap_get_tag capa))))) proof (prove)
goal (1 subgoal):
 1. \<And>capa s s'. \<lbrakk>cleanup_info_wf' cap; ccap_relation cap capa; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> isIRQHandlerCap cap \<longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> ((\<exists>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (capIRQ cap)) proof (prove)
goal (1 subgoal):
 1. \<And>capa s s' v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; (s, s') \<in> rf_sr; cap = capability.IRQHandlerCap v0\<rbrakk> \<Longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> ((\<exists>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) v0) proof (prove)
goal (1 subgoal):
 1. \<And>capa s s' v0. \<lbrakk>cleanup_info_wf' (capability.IRQHandlerCap v0); ccap_relation (capability.IRQHandlerCap v0) capa; (s, s') \<in> rf_sr; cap = capability.IRQHandlerCap v0; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap \<and> ((\<exists>t. ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)) \<longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) v0) proof (prove)
goal (1 subgoal):
 1. \<And>capa s s' t. \<lbrakk>UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; capIRQ_CL (cap_irq_handler_cap_lift capa) && 0x3FF = capIRQ_CL (cap_irq_handler_cap_lift capa); (s, s') \<in> rf_sr; cap = capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))); cap_lift capa = Some (Cap_irq_handler_cap (cap_irq_handler_cap_lift capa)); ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)\<rbrakk> \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) proof (prove)
goal (1 subgoal):
 1. \<And>capa s s' t. \<lbrakk>UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))) \<le> 0x9F; capIRQ_CL (cap_irq_handler_cap_lift capa) && 0x3FF = capIRQ_CL (cap_irq_handler_cap_lift capa); (s, s') \<in> rf_sr; cap = capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa))); cap_lift capa = Some (Cap_irq_handler_cap (cap_irq_handler_cap_lift capa)); ret__unsigned_' t = capIRQ_CL (cap_irq_handler_cap_lift capa)\<rbrakk> \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift capa) = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (capIRQ_CL (cap_irq_handler_cap_lift capa)))