kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_C

lemma ctcb_relation_tcbDomain_maxDomain_numDomains:
  "\<lbrakk> ctcb_relation tcb tcb'; tcbDomain tcb \<le> maxDomain \<rbrakk>
   \<Longrightarrow> unat (tcbDomain_C tcb') < Kernel_Config.numDomains" apply (subst ctcb_relation_tcbDomain[symmetric], simp) apply (simp add: le_maxDomain_eq_less_numDomains) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_relation tcb tcb'; tcbDomain tcb \<le> maxDomain\<rbrakk> \<Longrightarrow> unat (tcbDomain_C tcb') < numDomains proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_relation tcb tcb'; tcbDomain tcb \<le> maxDomain\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) (tcbDomain tcb)) < numDomains proof (prove)
goal:
No subgoals!
theory Finalise_C

lemma ctcb_relation_tcbPriority_maxPriority_numPriorities:
  "\<lbrakk> ctcb_relation tcb tcb'; tcbPriority tcb \<le> maxPriority \<rbrakk>
    \<Longrightarrow> unat (tcbPriority_C tcb') < numPriorities" apply (subst ctcb_relation_tcbPriority[symmetric], simp) apply (simp add: maxPriority_def numPriorities_def word_le_nat_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_relation tcb tcb'; tcbPriority tcb \<le> maxPriority\<rbrakk> \<Longrightarrow> unat (tcbPriority_C tcb') < Config_H.numPriorities proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_relation tcb tcb'; tcbPriority tcb \<le> maxPriority\<rbrakk> \<Longrightarrow> unat (UCAST(8 \<rightarrow> 32) (tcbPriority tcb)) < Config_H.numPriorities proof (prove)
goal:
No subgoals!
theory Finalise_C

lemma use_tcb_queue_relation2:
  "tcb_queue_relation getNext getPrev hp xs qprev qhead
     = (tcb_queue_relation2 getNext getPrev hp
            (map tcb_ptr_to_ctcb_ptr xs) qprev (tcb_Ptr 0)
           \<and> qhead = (hd (map tcb_ptr_to_ctcb_ptr xs @ [tcb_Ptr 0])))" apply (induct xs arbitrary: qhead qprev) apply simp apply (simp add: conj_comms cong: conj_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev hp xs qprev qhead = (tcb_queue_relation2 getNext getPrev hp (map tcb_ptr_to_ctcb_ptr xs) qprev NULL \<and> qhead = hd (map tcb_ptr_to_ctcb_ptr xs @ [NULL])) proof (prove)
goal (2 subgoals):
 1. \<And>qhead qprev. tcb_queue_relation getNext getPrev hp [] qprev qhead = (tcb_queue_relation2 getNext getPrev hp (map tcb_ptr_to_ctcb_ptr []) qprev NULL \<and> qhead = hd (map tcb_ptr_to_ctcb_ptr [] @ [NULL]))
 2. \<And>x1 xs qhead qprev. (\<And>qhead qprev. tcb_queue_relation getNext getPrev hp xs qprev qhead = (tcb_queue_relation2 getNext getPrev hp (map tcb_ptr_to_ctcb_ptr xs) qprev NULL \<and> qhead = hd (map tcb_ptr_to_ctcb_ptr xs @ [NULL]))) \<Longrightarrow> tcb_queue_relation getNext getPrev hp (x1 # xs) qprev qhead = (tcb_queue_relation2 getNext getPrev hp (map tcb_ptr_to_ctcb_ptr (x1 # xs)) qprev NULL \<and> qhead = hd (map tcb_ptr_to_ctcb_ptr (x1 # xs) @ [NULL])) proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs qhead qprev. (\<And>qhead qprev. tcb_queue_relation getNext getPrev hp xs qprev qhead = (tcb_queue_relation2 getNext getPrev hp (map tcb_ptr_to_ctcb_ptr xs) qprev NULL \<and> qhead = hd (map tcb_ptr_to_ctcb_ptr xs @ [NULL]))) \<Longrightarrow> tcb_queue_relation getNext getPrev hp (x1 # xs) qprev qhead = (tcb_queue_relation2 getNext getPrev hp (map tcb_ptr_to_ctcb_ptr (x1 # xs)) qprev NULL \<and> qhead = hd (map tcb_ptr_to_ctcb_ptr (x1 # xs) @ [NULL])) proof (prove)
goal:
No subgoals!
theory Finalise_C

lemma option_to_ptr_not_NULL:
  "option_to_ptr x \<noteq> NULL \<Longrightarrow> x \<noteq> None" by (auto simp: option_to_ptr_def option_to_0_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. option_to_ptr x \<noteq> NULL \<Longrightarrow> x \<noteq> None
theory Finalise_C

lemma offset_xf_for_sequence:
  "\<forall>s f. offset_' (offset_'_update f s) = f (offset_' s)
          \<and> globals (offset_'_update f s) = globals s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s f. offset_' (offset_'_update f s) = f (offset_' s) \<and> globals (offset_'_update f s) = globals s
theory Finalise_C

lemma invs'_invs_no_cicd':
  "invs' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s" by (simp add: invs'_invs_no_cicd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s
theory Finalise_C

lemma findPDForASID_nonzero:
  "\<lbrace>\<top>\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv s. rv \<noteq> 0\<rbrace>,-" apply (simp add: findPDForASID_def cong: option.case_cong) apply (wp | wpc | simp only: o_def simp_thms)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv s. rv \<noteq> 0\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE y <- assertE (0 < asid);
y <- assertE (asid \<le> snd asidRange);
asidTable <- liftE (gets (armKSASIDTable \<circ> ksArchState));
pool <- liftME (inv asidpool.ASIDPool) (case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> liftE (getObject ptr));
case pool (asid && mask local.asid_low_bits) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> doE y <- assertE (ptr \<noteq> 0);
y <- liftE (checkPDAt ptr);
returnOk ptr
odE
odE \<lbrace>\<lambda>rv s. rv \<noteq> 0\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Finalise_C

lemma no_0_pd_at'[elim!]:
  "\<lbrakk> page_directory_at' 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" apply (clarsimp simp: page_directory_at'_def) apply (drule spec[where x=0], clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_directory_at' 0 s; no_0_obj' s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y<0x1000. pde_at' (y << 2) s; no_0_obj' s\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Finalise_C

lemma getIRQSlot_ccorres_stuff:
  "\<lbrakk> (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow>
   CTypesDefs.ptr_add intStateIRQNode_Ptr (uint (irq :: 10 word))
     = Ptr (irq_node' s + 2 ^ cte_level_bits * ucast irq)" apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def
                            cinterrupt_relation_def) apply (simp add: objBits_simps cte_level_bits_def
                   size_of_def mult.commute mult.left_commute of_int_uint_ucast ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> intStateIRQNode_Ptr +\<^sub>p uint irq = cte_Ptr (irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); symbol_table ''intStateIRQNode'' = irq_node' s; \<forall>irq\<le>UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ. irqstate_to_C (intStateIRQTable (ksInterruptState s) irq) = intStateIRQTable_' (globals s').[unat irq]; cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c PTR(cte_C[256]) (irq_node' s); {irq_node' s..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)) = 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq proof (prove)
goal:
No subgoals!
theory Finalise_C

lemma irq_opt_relation_Some_ucast:
  "\<lbrakk> x && mask 10 = x; ucast x \<le> (ucast Kernel_C.maxIRQ :: 10 word) \<or> x \<le> (ucast Kernel_C.maxIRQ :: machine_word) \<rbrakk>
    \<Longrightarrow> irq_opt_relation (Some (ucast x)) (ucast ((ucast x):: irq))" using ucast_ucast_mask[where x=x and 'a=10, symmetric] apply (simp add: irq_opt_relation_def) apply (rule conjI, clarsimp simp: minus_one_norm irqInvalid_def Kernel_C.maxIRQ_def) apply (simp only: unat_arith_simps) by (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> irq_opt_relation (Some (UCAST(32 \<rightarrow> 10) x)) (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)) proof (prove)
using this:
x && mask LENGTH(10) = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)

goal (1 subgoal):
 1. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ\<rbrakk> \<Longrightarrow> irq_opt_relation (Some (UCAST(32 \<rightarrow> 10) x)) (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; x = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 10) x \<noteq> UCAST(32 \<rightarrow> 10) kernel_all_global_addresses.irqInvalid \<and> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask 10 = x; UCAST(32 \<rightarrow> 10) x \<le> UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ \<or> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; x = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)\<rbrakk> \<Longrightarrow> x \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (x && mask 10) = unat (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)); unat (UCAST(32 \<rightarrow> 10) x) \<le> unat (UCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ) \<or> unat (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)) \<le> unat (UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ); unat x = unat (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x))\<rbrakk> \<Longrightarrow> unat (UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x)) \<le> unat (UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)
theory Finalise_C

lemma ccap_relation_IRQHandler_mask:
  "\<lbrakk> ccap_relation acap ccap; isIRQHandlerCap acap \<rbrakk>
    \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 10
        = capIRQ_CL (cap_irq_handler_cap_lift ccap)" apply (simp only: cap_get_tag_isCap[symmetric]) apply (drule ccap_relation_c_valid_cap) apply (simp add: c_valid_cap_def cap_irq_handler_cap_lift cl_valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation acap ccap; isIRQHandlerCap acap\<rbrakk> \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 10 = capIRQ_CL (cap_irq_handler_cap_lift ccap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation acap ccap; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap\<rbrakk> \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 10 = capIRQ_CL (cap_irq_handler_cap_lift ccap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap; c_valid_cap ccap\<rbrakk> \<Longrightarrow> capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 10 = capIRQ_CL (cap_irq_handler_cap_lift ccap) proof (prove)
goal:
No subgoals!
theory Interrupt_C

lemma invokeIRQHandler_AckIRQ_ccorres:
  "ccorres dc xfdc
       invs' (UNIV \<inter> {s. irq_' s = ucast irq}) []
     (InterruptDecls_H.invokeIRQHandler (AckIRQ irq)) (Call invokeIRQHandler_AckIRQ_'proc)" apply (cinit lift: irq_' simp: Interrupt_H.invokeIRQHandler_def invokeIRQHandler_def) apply (ctac add: maskInterrupt_ccorres) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc invs' (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>) [] (InterruptDecls_H.invokeIRQHandler (AckIRQ irq)) (Call invokeIRQHandler_AckIRQ_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>irqa. irqa = UCAST(10 \<rightarrow> 32) irq \<Longrightarrow> ccorres dc xfdc (?Q30 irqa) (?Q'30 irqa) [SKIP] (doMachineOp (maskInterrupt False irq)) (CALL maskInterrupt_'proc(SCAST(32 signed \<rightarrow> 32) false,irqa))
 2. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q30 irqa s \<and> s' \<in> ?Q'30 irqa proof (prove)
goal (1 subgoal):
 1. \<And>irqa s s'. \<lbrakk>irqa = UCAST(10 \<rightarrow> 32) irq; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. irq_'_update (\<lambda>_. irqa) (disable_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s) \<in> \<lbrace>\<acute>disable = from_bool False\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} proof (prove)
goal:
No subgoals!
theory Interrupt_C

lemma getIRQSlot_ccorres:
  "ccorres ((=) \<circ> Ptr) irqSlot_'
          \<top> UNIV hs
      (getIRQSlot irq)
      (\<acute>irqSlot :== CTypesDefs.ptr_add intStateIRQNode_Ptr (uint irq))" apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def
                        locateSlot_conv) apply (simp add: simpler_gets_def bind_def return_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                        cinterrupt_relation_def size_of_def
                        sint_ucast_eq_uint is_down of_int_uint_ucast
                        cte_level_bits_def mult.commute mult.left_commute ucast_nat_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres ((=) \<circ> cte_Ptr) irqSlot_' (\<lambda>_. True) UNIV hs (getIRQSlot irq) (\<acute>irqSlot :== intStateIRQNode_Ptr +\<^sub>p uint irq) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>irqSlot :== intStateIRQNode_Ptr +\<^sub>p uint irq {s. \<exists>(rv, \<sigma>')\<in>fst (getIRQSlot irq \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ((=) \<circ> cte_Ptr) rv (irqSlot_' s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (getIRQSlot irq \<sigma>). (\<sigma>', irqSlot_'_update (\<lambda>_. intStateIRQNode_Ptr +\<^sub>p uint irq) s) \<in> rf_sr \<and> cte_Ptr rv = intStateIRQNode_Ptr +\<^sub>p uint irq} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> \<exists>xa\<in>fst ((do x <- gets ksInterruptState;
return (intStateIRQNode x + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> rv = symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> irq_node' \<sigma> + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq = symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)) proof (prove)
goal:
No subgoals!
theory Interrupt_C

lemma ptr_add_assertion_irq_guard:
"ccorres dc xfdc P Q hs a
     (Guard F
       \<lbrace>uint irq = 0 \<or> array_assertion intStateIRQNode_Ptr (nat (uint irq)) (hrs_htd \<acute>t_hrs)\<rbrace>
       c;;m)
  \<Longrightarrow> ccorres dc xfdc P Q hs a
            (Guard F
              \<lbrace>ptr_add_assertion intStateIRQNode_Ptr
                (sint (ucast (irq :: 16 word)::32 signed word)) False
                (hrs_htd \<acute>t_hrs)\<rbrace> c ;; m)" by (simp add: ptr_add_assertion_def sint_ucast_eq_uint is_down)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc P Q hs a (Guard F \<lbrace>uint irq = 0 \<or> array_assertion intStateIRQNode_Ptr (nat (uint irq)) (hrs_htd \<acute>t_hrs)\<rbrace> c;;
m) \<Longrightarrow> ccorres dc xfdc P Q hs a (Guard F \<lbrace>ptr_add_assertion intStateIRQNode_Ptr (sint (UCAST(16 \<rightarrow> 32 signed) irq)) False (hrs_htd \<acute>t_hrs)\<rbrace> c;;
m)
theory Interrupt_C

lemma cte_at_irq_node':
  "invs' s \<Longrightarrow>
    cte_at' (irq_node' s + 2 ^ cte_level_bits * ucast (irq :: 10 word)) s" by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def
                     cte_level_bits_def real_cte_at' cteSizeBits_def shiftl_t2n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s
theory Interrupt_C

lemma ntfn_case_can_send:
  "(case cap of NotificationCap x1 x2 x3 x4 \<Rightarrow> f x3
        | _ \<Rightarrow> v) = (if isNotificationCap cap then f (capNtfnCanSend cap)
                     else v)" by (cases cap, simp_all add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.NotificationCap x1 x2 x3 x4 \<Rightarrow> f x3 | _ \<Rightarrow> v) = (if isNotificationCap cap then f (capNtfnCanSend cap) else v)
theory Interrupt_C

lemma ucast_maxIRQ_le_eq:
  "UCAST(10 \<rightarrow> 32) irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow>
   UCAST(10 \<rightarrow> 16) irq \<le> SCAST(32 signed \<rightarrow> 16) Kernel_C.maxIRQ" apply (subst ucast_le_ucast[where 'a=16 and 'b=32, symmetric]) apply simp by (clarsimp simp: ucast_up_ucast is_up Kernel_C.maxIRQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> UCAST(10 \<rightarrow> 16) irq \<le> SCAST(32 signed \<rightarrow> 16) Kernel_C.maxIRQ proof (prove)
goal (2 subgoals):
 1. UCAST(10 \<rightarrow> 32) irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> LENGTH(16) \<le> LENGTH(32)
 2. UCAST(10 \<rightarrow> 32) irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> UCAST(16 \<rightarrow> 32) (UCAST(10 \<rightarrow> 16) irq) \<le> UCAST(16 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 16) Kernel_C.maxIRQ) proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<Longrightarrow> UCAST(16 \<rightarrow> 32) (UCAST(10 \<rightarrow> 16) irq) \<le> UCAST(16 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 16) Kernel_C.maxIRQ)
theory Interrupt_C

lemma Platform_maxIRQ:
  "ARM.maxIRQ = scast Kernel_C.maxIRQ" by (simp add: ARM.maxIRQ_def Kernel_C.maxIRQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.maxIRQ = SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ
theory Interrupt_C

lemma maxIRQ_ucast_scast [simp]:
  "ucast (scast Kernel_C.maxIRQ :: 10 word) = scast Kernel_C.maxIRQ" by (clarsimp simp: Kernel_C.maxIRQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 'a) (SCAST(32 signed \<rightarrow> 10) Kernel_C.maxIRQ) = SCAST(32 signed \<rightarrow> 'a) Kernel_C.maxIRQ
theory Interrupt_C

lemma decodeIRQ_arch_helper: "x \<noteq> IRQIssueIRQHandler \<Longrightarrow>
         (case x of IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g" by (clarsimp split: gen_invocation_labels.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> gen_invocation_labels.IRQIssueIRQHandler \<Longrightarrow> (case x of gen_invocation_labels.IRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g
theory Interrupt_C

lemma decodeIRQ_arch_helper': "x \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<Longrightarrow>
         (case x of ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> f | _ \<Rightarrow> g) = g" by (clarsimp split: invocation_label.splits arch_invocation_label.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler \<Longrightarrow> (case x of GenInvocationLabel gen_invocation_labels \<Rightarrow> g | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> f | ArchInvocationLabel _ \<Rightarrow> g) = g
theory Interrupt_C

lemma checkIRQ_ret_good:
  "\<lbrace>\<lambda>s. (irq \<le> scast Kernel_C.maxIRQ \<longrightarrow> P s) \<and> Q s\<rbrace> checkIRQ irq \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace>" apply (clarsimp simp: checkIRQ_def rangeCheck_def Platform_maxIRQ minIRQ_def) apply (rule hoare_pre,wp) by (clarsimp simp: Kernel_C.maxIRQ_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> P s) \<and> Q s\<rbrace> checkIRQ irq \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> P s) \<and> Q s\<rbrace> unlessE (irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) (throwError (Fault_H.syscall_error.RangeError 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ))) \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ \<longrightarrow> P s) \<and> Q s \<Longrightarrow> (if irq \<le> SCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ then P else (\<lambda>s. Q s \<and> True)) s