kings-crown/FVELER_Isabelle huggingface dataset:
theory Arch_R

lemma lookup_pt_slot_no_fail_corres[simp]:
  "lookupPTSlotFromPT pt vptr
    = (do stateAssert (page_table_at' pt) []; return (lookup_pt_slot_no_fail pt vptr) od)" by (simp add: lookup_pt_slot_no_fail_def lookupPTSlotFromPT_def mask_def checkPTAt_def
                ptBits_def pteBits_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookupPTSlotFromPT pt vptr = do stateAssert (page_table_at' pt) [];
return (lookup_pt_slot_no_fail pt vptr)
od
theory Arch_R

lemma page_base_corres[simp]:
  "pageBase vaddr vmsize = page_base vaddr vmsize" by (clarsimp simp: pageBase_def page_base_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBase vaddr vmsize = page_base vaddr vmsize
theory Arch_R

lemma flush_type_map:
  "ARM_H.isPageFlushLabel (invocation_type (mi_label mi))
   \<or> ARM_H.isPDFlushLabel (invocation_type (mi_label mi))
  \<Longrightarrow> labelToFlushType (mi_label mi) =
          flush_type_map (label_to_flush_type (invocation_type (mi_label mi)))" by (clarsimp simp: label_to_flush_type_def labelToFlushType_def flush_type_map_def
                        ARM_H.isPageFlushLabel_def ARM_H.isPDFlushLabel_def
                 split: ARM_A.flush_type.splits invocation_label.splits arch_invocation_label.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isPageFlushLabel (invocation_type (mi_label mi)) \<or> isPDFlushLabel (invocation_type (mi_label mi)) \<Longrightarrow> labelToFlushType (mi_label mi) = flush_type_map (label_to_flush_type (invocation_type (mi_label mi)))
theory Arch_R

lemma vs_lookup_pages1I:
  "\<lbrakk> ko_at ko p s; (r, p') \<in> vs_refs_pages ko;
          rs' = r # rs \<rbrakk> \<Longrightarrow> ((rs,p) \<unrhd>1 (rs',p')) s" by (fastforce simp add: vs_lookup_pages1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at ko p s; (r, p') \<in> vs_refs_pages ko; rs' = r # rs\<rbrakk> \<Longrightarrow> ((rs, p), rs', p') \<in> vs_lookup_pages1 s
theory Arch_R

lemma vs_refs_pages_ptI:
  "pt x = pte \<Longrightarrow> pte_ref_pages pte = Some r'
    \<Longrightarrow> (VSRef (ucast x) (Some APageTable), r') \<in> vs_refs_pages (ArchObj (PageTable pt))" apply (simp add: vs_refs_pages_def) apply (rule image_eqI[rotated], rule graph_ofI[where x=x], simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pt x = pte; pte_ref_pages pte = Some r'\<rbrakk> \<Longrightarrow> (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable), r') \<in> vs_refs_pages (ArchObj (PageTable pt)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pt x = pte; pte_ref_pages pte = Some r'\<rbrakk> \<Longrightarrow> (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable), r') \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), x)) ` graph_of (pte_ref_pages \<circ> pt) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pt x = pte; pte_ref_pages pte = Some r'\<rbrakk> \<Longrightarrow> (VSRef (UCAST(8 \<rightarrow> 32) x) (Some APageTable), r') = (case (x, r') of (r, x) \<Rightarrow> (VSRef (UCAST(8 \<rightarrow> 32) r) (Some APageTable), x)) proof (prove)
goal:
No subgoals!
theory Arch_R

lemma vs_refs_pages_pdI:
  "pd x = pde \<Longrightarrow> pde_ref_pages pde = Some r'
    \<Longrightarrow> x \<notin> kernel_mapping_slots
    \<Longrightarrow> (VSRef (ucast x) (Some APageDirectory), r') \<in> vs_refs_pages (ArchObj (PageDirectory pd))" apply (simp add: vs_refs_pages_def) apply (rule image_eqI[rotated], rule graph_ofI[where x=x], simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd x = pde; pde_ref_pages pde = Some r'; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r') \<in> vs_refs_pages (ArchObj (PageDirectory pd)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd x = pde; pde_ref_pages pde = Some r'; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r') \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref_pages (pd x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd x = pde; pde_ref_pages pde = Some r'; x \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) x) (Some APageDirectory), r') = (case (x, r') of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) proof (prove)
goal:
No subgoals!
theory Arch_R

lemma asid_pool_typ_at_ext':
  "asid_pool_at' = obj_at' (\<top>::asidpool \<Rightarrow> bool)" apply (rule ext)+ apply (simp add: typ_at_to_obj_at_arches) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_pool_at' = obj_at' (\<lambda>_. True) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. asid_pool_at' x xa = obj_at' (\<lambda>_. True) x xa proof (prove)
goal:
No subgoals!
theory Arch_R

lemma sts_cte_cap_to'[wp]:
  "\<lbrace>ex_cte_cap_to' p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ex_cte_cap_to' p\<rbrace>" by (wp ex_cte_cap_to'_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace>
theory Arch_R

lemma tcbSchedEnqueue_vs_entry_align[wp]:
 "\<lbrace>\<lambda>s. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p s\<rbrace>
   tcbSchedEnqueue pa
  \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace>" apply (clarsimp simp: tcbSchedEnqueue_def setQueue_def) by (wp unless_wp | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> tcbSchedEnqueue pa \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> do queued <- threadGet tcbQueued pa;
unless queued (do tdom <- threadGet tcbDomain pa;
prio <- threadGet tcbPriority pa;
queue <- getQueue tdom prio;
y <- modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((tdom, prio) := pa # queue)\<rparr>);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) pa
od)
od \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace>
theory Arch_R

lemma inv_ASIDPool: "inv ASIDPool = (\<lambda>v. case v of ASIDPool a \<Rightarrow> a)" apply (rule ext) apply (case_tac v) apply simp apply (rule inv_f_f, rule inj_onI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inv asidpool.ASIDPool = (\<lambda>v. case v of asidpool.ASIDPool a \<Rightarrow> a) proof (prove)
goal (1 subgoal):
 1. \<And>v. inv asidpool.ASIDPool v = (case v of asidpool.ASIDPool a \<Rightarrow> a) proof (prove)
goal (1 subgoal):
 1. \<And>v x. v = asidpool.ASIDPool x \<Longrightarrow> inv asidpool.ASIDPool v = (case v of asidpool.ASIDPool a \<Rightarrow> a) proof (prove)
goal (1 subgoal):
 1. \<And>v x. v = asidpool.ASIDPool x \<Longrightarrow> inv asidpool.ASIDPool (asidpool.ASIDPool x) = x proof (prove)
goal (1 subgoal):
 1. \<And>v x xa y. \<lbrakk>v = asidpool.ASIDPool x; xa \<in> UNIV; y \<in> UNIV; asidpool.ASIDPool xa = asidpool.ASIDPool y\<rbrakk> \<Longrightarrow> xa = y proof (prove)
goal:
No subgoals!
theory Arch_R

lemma findPDForASID_valid_offset'[wp]:
  "\<lbrace>valid_objs' and K (vptr < pptrBase)\<rbrace> findPDForASID p
   \<lbrace>\<lambda>rv s. valid_pde_mapping_offset' (rv + (vptr >> 20 << 2) && mask pdBits)\<rbrace>,-" apply (rule hoare_gen_asmE) apply (rule hoare_post_imp_R, rule findPDForASID_aligned) apply (simp add: mask_add_aligned) apply (erule less_pptrBase_valid_pde_offset'') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and K (vptr < pptrBase)\<rbrace> findPDForASID p \<lbrace>\<lambda>rv s. valid_pde_mapping_offset' (rv + (vptr >> 20 << 2) && mask pdBits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. vptr < pptrBase \<Longrightarrow> \<lbrace>valid_objs'\<rbrace> findPDForASID p \<lbrace>\<lambda>rv s. valid_pde_mapping_offset' (rv + (vptr >> 20 << 2) && mask pdBits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>vptr < pptrBase; is_aligned rv pdBits\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (rv + (vptr >> 20 << 2) && mask pdBits) proof (prove)
goal (1 subgoal):
 1. \<And>rv. \<lbrakk>vptr < pptrBase; is_aligned rv pdBits\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' ((vptr >> 20 << 2) && mask pdBits) proof (prove)
goal:
No subgoals!
theory Arch_R

lemma eq_arch_update':
  "ArchObjectCap cp = cteCap cte \<Longrightarrow> is_arch_update' (ArchObjectCap cp) cte" by (clarsimp simp: is_arch_update'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capability.ArchObjectCap cp = cteCap cte \<Longrightarrow> is_arch_update' (capability.ArchObjectCap cp) cte
theory Arch_R

lemma lookupPTSlot_page_table_at':
  "\<lbrace>valid_objs'\<rbrace> lookupPTSlot pd vptr
  \<lbrace>\<lambda>rv s. page_table_at' (rv && ~~ mask ptBits) s\<rbrace>,-" apply (simp add:lookupPTSlot_def) apply (wp getPDE_wp|wpc|simp add:checkPTAt_def)+ apply (clarsimp simp:ptBits_def lookup_pt_slot_no_fail_def pteBits_def) apply (subst vaddr_segment_nonsense3[unfolded pt_bits_def pageBits_def,simplified]) apply (simp add:page_table_at'_def ptBits_def pageBits_def pteBits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>rv. page_table_at' (rv && ~~ mask ptBits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> doE pde <- liftE (getObject (lookup_pd_slot pd vptr));
case pde of ARM_H.PageTablePDE x xa xb \<Rightarrow> doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 20
odE \<lbrace>\<lambda>rv. page_table_at' (rv && ~~ mask ptBits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<Longrightarrow> \<forall>ko. ko_at' ko (lookup_pd_slot pd vptr) s \<longrightarrow> (\<forall>x. (\<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb) \<longrightarrow> page_table_at' (ptrFromPAddr x) s \<longrightarrow> page_table_at' (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr && ~~ mask ptBits) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pd vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask 10) s proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pd vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s x xa xb. \<lbrakk>valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pd vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x) s proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pd vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x) s proof (prove)
goal:
No subgoals!
theory Arch_R

lemma ex_cte_not_in_untyped_range:
  "\<lbrakk>(ctes_of s) cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode);
    descendants_of' cref (ctes_of s) = {}; invs' s;
    ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s\<rbrakk>
   \<Longrightarrow> x \<notin> {ptr .. ptr + 2 ^ bits - 1}" apply clarsimp apply (drule(1) cte_cap_in_untyped_range) apply (fastforce simp:cte_wp_at_ctes_of)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode); descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s\<rbrakk> \<Longrightarrow> x \<notin> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode); descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s; ptr \<le> x; x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ctes_of s cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode); descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s; x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap ?d2 ptr bits ?idx2) ?cref2 ?s2
 2. \<lbrakk>ctes_of s cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode); descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s; x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> descendants_of' ?cref2 (ctes_of ?s2) = {}
 3. \<lbrakk>ctes_of s cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode); descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s; x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> invs' ?s2
 4. \<lbrakk>ctes_of s cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode); descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s; x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) x ?s2
 5. \<lbrakk>ctes_of s cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode); descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s; x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> valid_global_refs' ?s2
 6. \<lbrakk>ctes_of s cref = Some (CTE (capability.UntypedCap d ptr bits idx) mnode); descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s; x \<le> ptr + 2 ^ bits - 1; False\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Arch_R

lemma doFlush_underlying_memory[wp]:
  "\<lbrace> \<lambda>m'. underlying_memory m' p = um \<rbrace>
   doFlush flush_type vstart vend pstart
   \<lbrace> \<lambda>_ m'. underlying_memory m' p = um \<rbrace>" unfolding doFlush_def by(cases flush_type; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> doFlush flush_type vstart vend pstart \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> case flush_type of ARM_H.Clean \<Rightarrow> cleanCacheRange_RAM vstart vend pstart | ARM_H.Invalidate \<Rightarrow> invalidateCacheRange_RAM vstart vend pstart | ARM_H.CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM vstart vend pstart | ARM_H.Unify \<Rightarrow> do cleanCacheRange_PoU vstart vend pstart;
dsb;
invalidateCacheRange_I vstart vend pstart;
branchFlushRange vstart vend pstart;
isb
od \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory Arch_R

lemma dmo_invs'_simple:
  "no_irq f \<Longrightarrow>
   (\<And>p um. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> f \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>) \<Longrightarrow>
   \<lbrace> invs' \<rbrace> doMachineOp f \<lbrace> \<lambda>y. invs' \<rbrace>" by (rule hoare_pre, rule dmo_invs', wp no_irq, simp_all add:valid_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_irq f; \<And>p um. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> f \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> doMachineOp f \<lbrace>\<lambda>y. invs'\<rbrace>
theory Arch_R

lemma doFlush_invs[wp]:
  "\<lbrace> invs' \<rbrace> doMachineOp (doFlush flush_type vstart vend pstart) \<lbrace> \<lambda>y. invs' \<rbrace>" by(wp dmo_invs'_simple)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (doFlush flush_type vstart vend pstart) \<lbrace>\<lambda>y. invs'\<rbrace>
theory Arch_R

lemma performPageDirectoryInvocation_invs'[wp]:
  "\<lbrace> invs' \<rbrace> performPageDirectoryInvocation pdi \<lbrace> \<lambda>rv. invs' \<rbrace>" by(cases pdi, simp_all add:performPageDirectoryInvocation_def, (wp|simp)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> performPageDirectoryInvocation pdi \<lbrace>\<lambda>rv. invs'\<rbrace>
theory Arch_R

lemma arch_performInvocation_invs':
  "\<lbrace>invs' and ct_active' and valid_arch_inv' invocation\<rbrace>
  Arch.performInvocation invocation
  \<lbrace>\<lambda>rv. invs'\<rbrace>" unfolding ARM_H.performInvocation_def by (cases invocation,
      simp_all add: performARMMMUInvocation_def valid_arch_inv'_def,
      (wp|simp)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and valid_arch_inv' invocation\<rbrace> Arch.performInvocation invocation \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and valid_arch_inv' invocation\<rbrace> performARMMMUInvocation invocation \<lbrace>\<lambda>rv. invs'\<rbrace>
theory Interrupt_R

lemma isIRQActive_wp:
  "\<lbrace>\<lambda>s. \<forall>rv. (irq_issued' irq s \<longrightarrow> rv) \<longrightarrow> Q rv s\<rbrace> isIRQActive irq \<lbrace>Q\<rbrace>" apply (simp add: isIRQActive_def getIRQState_def
                   getInterruptState_def) apply wp apply (clarsimp simp: irq_issued'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>rv. (irq_issued' irq s \<longrightarrow> rv) \<longrightarrow> Q rv s\<rbrace> isIRQActive irq \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>rv. (irq_issued' irq s \<longrightarrow> rv) \<longrightarrow> Q rv s\<rbrace> liftM (\<lambda>x. x \<noteq> irqstate.IRQInactive) (liftM (swp id irq \<circ> intStateIRQTable) (gets ksInterruptState)) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>rv. (irq_issued' irq s \<longrightarrow> rv) \<longrightarrow> Q rv s \<Longrightarrow> (Q \<circ> (\<lambda>x. x \<noteq> irqstate.IRQInactive) \<circ> (swp id irq \<circ> intStateIRQTable)) (ksInterruptState s) s proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma checkIRQ_corres:
  "corres (ser \<oplus> dc) \<top> \<top> (arch_check_irq irq) (checkIRQ irq)" unfolding arch_check_irq_def checkIRQ_def rangeCheck_def apply (rule corres_guard_imp) apply (clarsimp simp: minIRQ_def unlessE_whenE not_le) apply (rule corres_whenE) apply (fastforce simp: ucast_nat_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (arch_check_irq irq) (checkIRQ irq) proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq) $ throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ))) (unlessE (fromIntegral (fromEnum minIRQ) \<le> irq \<and> irq \<le> fromIntegral (fromEnum maxIRQ)) $ throw $ Fault_H.syscall_error.RangeError (fromIntegral (fromEnum minIRQ)) (fromIntegral (fromEnum maxIRQ))) proof (prove)
goal (3 subgoals):
 1. corres (ser \<oplus> dc) ?Q ?Q' (whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq) $ throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ))) (unlessE (fromIntegral (fromEnum minIRQ) \<le> irq \<and> irq \<le> fromIntegral (fromEnum maxIRQ)) $ throw $ Fault_H.syscall_error.RangeError (fromIntegral (fromEnum minIRQ)) (fromIntegral (fromEnum maxIRQ)))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres (ser \<oplus> dc) ?Q ?Q' (whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq) (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)))) (whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq) (throwError (Fault_H.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ))))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. (UCAST(10 \<rightarrow> 32) maxIRQ < irq) = (UCAST(10 \<rightarrow> 32) maxIRQ < irq)
 2. corres (ser \<oplus> dc) ?P6 ?P'6 (throwError (ExceptionTypes_A.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ))) (throwError (Fault_H.syscall_error.RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)))
 3. dc () ()
 4. \<And>s. True \<Longrightarrow> UCAST(10 \<rightarrow> 32) maxIRQ < irq \<longrightarrow> ?P6 s
 5. \<And>s. True \<Longrightarrow> UCAST(10 \<rightarrow> 32) maxIRQ < irq \<longrightarrow> ?P'6 s proof (prove)
goal:
No subgoals!
theory Interrupt_R

lemma whenE_rangeCheck_eq:
  "(rangeCheck (x :: 'a :: {linorder, integral}) y z) =
    (whenE (x < fromIntegral y \<or> fromIntegral z < x)
      (throwError (RangeError (fromIntegral y) (fromIntegral z))))" by (simp add: rangeCheck_def unlessE_whenE linorder_not_le[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rangeCheck x y z = whenE (x < fromIntegral y \<or> fromIntegral z < x) (throwError (Fault_H.syscall_error.RangeError (fromIntegral y) (fromIntegral z)))
theory Interrupt_R

lemma unat_ucast_ucast_shenanigans[simp]:
  "unat (yf :: machine_word) \<le> (125::nat) \<Longrightarrow> ucast ((ucast yf) :: word8) = yf" apply (subgoal_tac "unat yf \<le> unat 125") apply (thin_tac "unat yf \<le> 125") apply (subst (asm) word_le_nat_alt[symmetric]) apply (simp add: ucast_ucast_mask mask_def) by (word_bitwise, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat yf \<le> 125 \<Longrightarrow> UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) yf) = yf proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat yf \<le> 125; unat yf \<le> unat 0x7D\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) yf) = yf
 2. unat yf \<le> 125 \<Longrightarrow> unat yf \<le> unat 0x7D proof (prove)
goal (2 subgoals):
 1. unat yf \<le> unat 0x7D \<Longrightarrow> UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) yf) = yf
 2. unat yf \<le> 125 \<Longrightarrow> unat yf \<le> unat 0x7D proof (prove)
goal (2 subgoals):
 1. yf \<le> 0x7D \<Longrightarrow> UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) yf) = yf
 2. unat yf \<le> 125 \<Longrightarrow> unat yf \<le> unat 0x7D proof (prove)
goal (2 subgoals):
 1. yf \<le> 0x7D \<Longrightarrow> yf && 0xFF = yf
 2. unat yf \<le> 125 \<Longrightarrow> unat yf \<le> unat 0x7D