kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_C

lemma setNextPC_ccorres:
  "ccorres dc xfdc \<top>
       (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>
             \<inter> {s. v_' s = val}) []
       (asUser thread (setNextPC val))
       (Call setNextPC_'proc)" apply (cinit') apply (simp add: setNextPC_def) apply (ctac add: setRegister_ccorres) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = val\<rbrace>) [] (asUser thread (setNextPC val)) (Call setNextPC_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 [SKIP] (asUser thread (setNextPC val)) (CALL setRegister_'proc(\<acute>thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP,\<acute>v))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = val\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 [SKIP] (asUser thread (setRegister register.NextIP val)) (CALL setRegister_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP,\<acute>v))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = val\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = val\<rbrace>\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. w_'_update (\<lambda>_. v_' s) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP) s) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H register.NextIP\<rbrace> \<inter> \<lbrace>\<acute>w = val\<rbrace>} proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma postModifyRegisters_ccorres:
  "ccorres dc xfdc \<top> UNIV hs
      (asUser dest $ postModifyRegisters ct dest)
      (Call Arch_postModifyRegisters_'proc)" apply (cinit simp: postModifyRegisters_def) apply (subst asUser_return) apply (rule ccorres_stateAssert) apply (rule ccorres_return_Skip) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) UNIV hs (asUser dest $ postModifyRegisters ct dest) (Call Arch_postModifyRegisters_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 (SKIP # hs) (asUser dest (return ())) SKIP
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 (SKIP # hs) (do u <- stateAssert (tcb_at' dest) [];
return ()
od) SKIP
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?P18 ?Q'9 (SKIP # hs) (return ()) SKIP
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' dest s \<longrightarrow> ?P18 s) \<and> s' \<in> ?Q'9 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' dest s \<longrightarrow> True) \<and> s' \<in> UNIV proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma doMachineOp_context:
  "(rv,s') \<in> fst (doMachineOp f s) \<Longrightarrow>
  (rv,s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)
  \<in> fst (doMachineOp f (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>))" apply (clarsimp simp: doMachineOp_def split_def in_monad select_f_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (doMachineOp f s) \<Longrightarrow> (rv, s'\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>) \<in> fst (doMachineOp f (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(rv, b) \<in> fst (f (ksMachineState s)); s' = s\<lparr>ksMachineState := b\<rparr>\<rbrakk> \<Longrightarrow> \<exists>ba. (rv, ba) \<in> fst (f (ksMachineState s)) \<and> s\<lparr>ksMachineState := b, ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko))\<rparr> = s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbContext_update (\<lambda>_. st) ko)), ksMachineState := ba\<rparr> proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma asUser_sysargs_rel:
  "\<lbrace>\<lambda>s. t \<noteq> ksCurThread s \<and> sysargs_rel args buffer s\<rbrace>
  asUser t f \<lbrace>\<lambda>_. sysargs_rel args buffer\<rbrace>" apply (cases buffer, simp_all add: sysargs_rel_def) apply (rule hoare_pre) apply (wp asUser_getMRs_rel hoare_valid_ipc_buffer_ptr_typ_at'|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t \<noteq> ksCurThread s \<and> sysargs_rel args buffer s\<rbrace> asUser t f \<lbrace>\<lambda>_. sysargs_rel args buffer\<rbrace> proof (prove)
goal (2 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>\<lambda>s. t \<noteq> ksCurThread s \<and> cur_tcb' s \<and> getMRs_rel args None s \<and> \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args\<rbrace> asUser t f \<lbrace>\<lambda>_. cur_tcb' and getMRs_rel args None and (\<lambda>_. \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args)\<rbrace>
 2. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. t \<noteq> ksCurThread s \<and> cur_tcb' s \<and> valid_ipc_buffer_ptr' a s \<and> getMRs_rel args (Some a) s\<rbrace> asUser t f \<lbrace>\<lambda>_. cur_tcb' and valid_ipc_buffer_ptr' a and getMRs_rel args (Some a)\<rbrace> proof (prove)
goal (3 subgoals):
 1. buffer = None \<Longrightarrow> \<lbrace>?Q4\<rbrace> asUser t f \<lbrace>\<lambda>_. cur_tcb' and getMRs_rel args None and (\<lambda>_. \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args)\<rbrace>
 2. \<And>s. \<lbrakk>buffer = None; t \<noteq> ksCurThread s \<and> cur_tcb' s \<and> getMRs_rel args None s \<and> \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>a. buffer = Some a \<Longrightarrow> \<lbrace>\<lambda>s. t \<noteq> ksCurThread s \<and> cur_tcb' s \<and> valid_ipc_buffer_ptr' a s \<and> getMRs_rel args (Some a) s\<rbrace> asUser t f \<lbrace>\<lambda>_. cur_tcb' and valid_ipc_buffer_ptr' a and getMRs_rel args (Some a)\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma threadSet_same:
  "\<lbrace>\<lambda>s. \<exists>tcb'. ko_at' tcb' t s \<and> tcb = f tcb'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ko_at' tcb t\<rbrace>" unfolding threadSet_def by (wpsimp wp: setObject_tcb_strongest getObject_tcb_wp) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>tcb'. ko_at' tcb' t s \<and> tcb = f tcb'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ko_at' tcb t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>tcb'. ko_at' tcb' t s \<and> tcb = f tcb'\<rbrace> do tcb <- getObject t;
setObject t $ f tcb
od \<lbrace>\<lambda>rv. ko_at' tcb t\<rbrace>
theory Tcb_C

lemma Arch_decodeTransfer_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call Arch_decodeTransfer_'proc {s'. ret__unsigned_long_' s' = 0}" by (vcg, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call Arch_decodeTransfer_'proc \<lbrace>\<acute>ret__unsigned_long = 0\<rbrace>
theory Tcb_C

lemma mapM_x_split_append:
  "mapM_x f xs = do _ \<leftarrow> mapM_x f (take n xs); mapM_x f (drop n xs) od" using mapM_x_append[where f=f and xs="take n xs" and ys="drop n xs"] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f xs = do _ <- mapM_x f (take n xs);
mapM_x f (drop n xs)
od proof (prove)
using this:
mapM_x f (take n xs @ drop n xs) = do mapM_x f (take n xs);
mapM_x f (drop n xs)
od

goal (1 subgoal):
 1. mapM_x f xs = do _ <- mapM_x f (take n xs);
mapM_x f (drop n xs)
od
theory Tcb_C

lemma ccorres_abstract_cong:
  "\<lbrakk> \<And>s s'. \<lbrakk> P s ; s' \<in> P'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> a s = b s \<rbrakk> \<Longrightarrow>
   ccorres_underlying sr G r xf ar axf P P' hs a c
        = ccorres_underlying sr G r xf ar axf P P' hs b c" by (simp add: ccorres_underlying_def split_paired_Ball imp_conjL
          cong: conj_cong xstate.case_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> a s = b s) \<Longrightarrow> ccorres_underlying sr G r xf ar axf P P' hs a c = ccorres_underlying sr G r xf ar axf P P' hs b c
theory Tcb_C

lemma valid_ipc_buffer_ptr_the_strengthen:
  "x \<noteq> None \<and> case_option \<top> valid_ipc_buffer_ptr' x s \<longrightarrow> valid_ipc_buffer_ptr' (the x) s" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> None \<and> (case x of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s \<longrightarrow> valid_ipc_buffer_ptr' (the x) s
theory Tcb_C

lemma lookupIPCBuffer_Some_0:
  "\<lbrace>\<top>\<rbrace> lookupIPCBuffer w t \<lbrace>\<lambda>rv s. rv \<noteq> Some 0\<rbrace>" apply (simp add: lookupIPCBuffer_def
                   ARM_H.lookupIPCBuffer_def
                   Let_def getThreadBufferSlot_def
                   locateSlot_conv
             cong: if_cong) apply (wp haskell_assert_wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookupIPCBuffer w t \<lbrace>\<lambda>rv s. rv \<noteq> Some 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do bufferPtr <- threadGet tcbIPCBuffer t;
getSlotCap (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) >>= case_capability (\<lambda>word. return None) (return None) (\<lambda>word1 word2 bool1 bool2. return None) (\<lambda>word. return None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. return None) (return None) (\<lambda>word zombie_type nat. return None) (case_arch_capability (\<lambda>word1 word2. return None) (return None) (\<lambda>bool baseptr rights sz x. case bool of True \<Rightarrow> return Nothing | False \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = vmrights.VMReadWrite \<or> \<not> w \<and> rights = vmrights.VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr bufferPtr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od) (\<lambda>word option. return None) (\<lambda>word option. return None)) (\<lambda>word bool1 bool2. return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 nat1 word2 nat2. return None) (return None)
od \<lbrace>\<lambda>rv s. rv \<noteq> Some 0\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma asUser_valid_ipc_buffer_ptr':
  "\<lbrace> valid_ipc_buffer_ptr' p \<rbrace> asUser t m \<lbrace> \<lambda>rv s. valid_ipc_buffer_ptr' p s \<rbrace>" by (simp add: valid_ipc_buffer_ptr'_def, wp, auto simp: valid_ipc_buffer_ptr'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ipc_buffer_ptr' p\<rbrace> asUser t m \<lbrace>\<lambda>rv. valid_ipc_buffer_ptr' p\<rbrace>
theory Tcb_C

lemma isDevice_PageCap_ccap_relation:
  "ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data)) cap
  \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap) \<noteq> 0)  = d" by (clarsimp elim!: ccap_relationE
                 simp: isPageCap_def generic_frame_cap_get_capFIsDevice_CL_def cap_to_H_def
                       Let_def to_bool_def
                split: arch_capability.split_asm cap_CL.split_asm if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz data)) cap \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap) \<noteq> 0) = d
theory Tcb_C

lemma isValidVTableRoot_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call isValidVTableRoot_'proc
    {s'. ret__unsigned_long_' s' = from_bool (isValidVTableRoot_C (cap_' s))}" apply vcg apply (clarsimp simp: isValidVTableRoot_C_def if_1_0_0 from_bool_0) apply (simp add: to_bool_def split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call isValidVTableRoot_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (isValidVTableRoot_C \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> ((if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0) \<noteq> 0 \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capPDIsMapped_CL (cap_page_directory_cap_lift cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) (if capPDIsMapped_CL (cap_page_directory_cap_lift cap) \<noteq> 0 then 1 else 0) = from_bool (isValidVTableRoot_C cap))) \<and> ((if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0) = 0 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = from_bool (isValidVTableRoot_C cap)) proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift cap) \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift cap))) proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma updateCapData_spec:
  "\<forall>cap preserve newData. \<Gamma>\<turnstile> \<lbrace>ccap_relation cap \<acute>cap \<and> preserve = to_bool \<acute>preserve \<and> newData = \<acute>newData\<rbrace>
             Call updateCapData_'proc
         \<lbrace>ccap_relation (RetypeDecls_H.updateCapData preserve newData cap) \<acute>ret__struct_cap_C\<rbrace>" by (simp add: updateCapData_spec)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cap preserve newData. \<Gamma>\<turnstile> \<lbrace>ccap_relation cap \<acute>cap \<and> preserve = to_bool \<acute>preserve \<and> newData = \<acute>newData\<rbrace> Call updateCapData_'proc \<lbrace>ccap_relation (global.updateCapData preserve newData cap) \<acute>ret__struct_cap_C\<rbrace>
theory Tcb_C

lemma length_excaps_map:
  "length (excaps_map xcs) = length xcs" by (simp add: excaps_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (excaps_map xcs) = length xcs
theory Tcb_C

lemma tcb_at_capTCBPtr_CL:
  "ccap_relation cp cap \<Longrightarrow> valid_cap' cp s
    \<Longrightarrow> isThreadCap cp
    \<Longrightarrow> tcb_at' (cap_thread_cap_CL.capTCBPtr_CL
        (cap_thread_cap_lift cap) && ~~mask tcbBlockSizeBits) s" apply (clarsimp simp: cap_get_tag_isCap[symmetric]
                        valid_cap_simps'
                 dest!: cap_get_tag_to_H) apply (frule ctcb_ptr_to_tcb_ptr_mask[OF tcb_aligned'], simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cp cap; valid_cap' cp s; isThreadCap cp\<rbrakk> \<Longrightarrow> tcb_at' (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap) && ~~ mask tcbBlockSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap; cp = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)))); capAligned (capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))))); tcb_at' (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)))) s\<rbrakk> \<Longrightarrow> tcb_at' (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap) && ~~ mask tcbBlockSizeBits) s proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma mcpriority_tcb_at'_prio_bounded':
  assumes "mcpriority_tcb_at' (\<lambda>mcp. prio \<le> ucast mcp) t s"
          "priorityBits \<le> len_of TYPE('a)"
  shows "(prio::'a::len word) \<le> ucast (max_word :: priority)" using assms by (clarsimp simp: pred_tcb_at'_def obj_at'_def priorityBits_def ucast_le_ucast
               simp del: unsigned_uminus1
               elim!: order.trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prio \<le> UCAST(8 \<rightarrow> 'a) (- 1) proof (prove)
using this:
mcpriority_tcb_at' (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 'a) mcp) t s
priorityBits \<le> LENGTH('a)

goal (1 subgoal):
 1. prio \<le> UCAST(8 \<rightarrow> 'a) (- 1)
theory Tcb_C

lemma not_isThreadCap_case:
  "\<lbrakk>\<not>isThreadCap cap\<rbrakk> \<Longrightarrow>
   (case cap of ThreadCap x \<Rightarrow> f x | _ \<Rightarrow> g) = g" by (clarsimp simp: isThreadCap_def split: capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isThreadCap cap \<Longrightarrow> (case cap of capability.ThreadCap x \<Rightarrow> f x | _ \<Rightarrow> g) = g
theory Tcb_C

lemma ucast_le_8_32_equiv:
  "x \<le> UCAST (8 \<rightarrow> 32) max_word \<Longrightarrow>
  (UCAST (32 \<rightarrow> 8) x \<le> y) = (x \<le> UCAST (8 \<rightarrow> 32) y)" apply (rule iffI) apply (word_bitwise; simp) apply (simp add: le_ucast_ucast_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> UCAST(8 \<rightarrow> 32) (- 1) \<Longrightarrow> (UCAST(32 \<rightarrow> 8) x \<le> y) = (x \<le> UCAST(8 \<rightarrow> 32) y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> UCAST(8 \<rightarrow> 32) (- 1); UCAST(32 \<rightarrow> 8) x \<le> y\<rbrakk> \<Longrightarrow> x \<le> UCAST(8 \<rightarrow> 32) y
 2. \<lbrakk>x \<le> UCAST(8 \<rightarrow> 32) (- 1); x \<le> UCAST(8 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> UCAST(8 \<rightarrow> 32) (- 1); x \<le> UCAST(8 \<rightarrow> 32) y\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> y proof (prove)
goal:
No subgoals!
theory Tcb_C

lemma mcpriority_tcb_at'_le_ucast:
  "pred_tcb_at' itcbMCP (\<lambda>mcp. x \<le> UCAST(8 \<rightarrow> 32) mcp) v s \<Longrightarrow>
   pred_tcb_at' itcbMCP (\<lambda>mcp. UCAST(32 \<rightarrow> 8) x \<le> mcp) v s" by (clarsimp simp: ucast_le_8_32_equiv mcpriority_tcb_at'_prio_bounded simp del: unsigned_uminus1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mcpriority_tcb_at' (\<lambda>mcp. x \<le> UCAST(8 \<rightarrow> 32) mcp) v s \<Longrightarrow> mcpriority_tcb_at' ((\<le>) (UCAST(32 \<rightarrow> 8) x)) v s
theory Tcb_C

lemma bindNTFN_alignment_junk:
  "\<lbrakk> is_aligned tcb tcbBlockSizeBits; bits \<le> ctcb_size_bits \<rbrakk>
    \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask bits = ptr_val (tcb_ptr_to_ctcb_ptr tcb)" apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def projectKOs) apply (rule is_aligned_neg_mask_eq) apply (erule aligned_add_aligned) apply (erule is_aligned_weaken[rotated]) by (auto simp add: is_aligned_def objBits_defs ctcb_offset_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned tcb tcbBlockSizeBits; bits \<le> ctcb_size_bits\<rbrakk> \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr tcb) && ~~ mask bits = ptr_val (tcb_ptr_to_ctcb_ptr tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned tcb tcbBlockSizeBits; bits \<le> ctcb_size_bits\<rbrakk> \<Longrightarrow> tcb + ctcb_offset && ~~ mask bits = tcb + ctcb_offset proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned tcb tcbBlockSizeBits; bits \<le> ctcb_size_bits\<rbrakk> \<Longrightarrow> is_aligned (tcb + ctcb_offset) bits proof (prove)
goal (2 subgoals):
 1. bits \<le> ctcb_size_bits \<Longrightarrow> is_aligned ctcb_offset bits
 2. bits \<le> ctcb_size_bits \<Longrightarrow> bits \<le> tcbBlockSizeBits proof (prove)
goal (2 subgoals):
 1. is_aligned ctcb_offset ctcb_size_bits
 2. bits \<le> ctcb_size_bits \<Longrightarrow> bits \<le> tcbBlockSizeBits
theory Tcb_C

lemma valid_objs_boundNTFN_NULL:
  "ko_at' tcb p s ==> valid_objs' s \<Longrightarrow> no_0_obj' s \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0" apply (drule(1) obj_at_valid_objs') apply (clarsimp simp: valid_tcb'_def projectKOs valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' tcb p s; valid_objs' s; no_0_obj' s\<rbrakk> \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; no_0_obj' s; \<exists>k. k = tcb \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0 proof (prove)
goal:
No subgoals!
theory Schedule_C

lemma Arch_switchToIdleThread_ccorres:
  "ccorres dc xfdc (invs_no_cicd') UNIV []
           Arch.switchToIdleThread (Call Arch_switchToIdleThread_'proc)" apply (cinit simp: ARM_H.switchToIdleThread_def) apply (rule ccorres_pre_getIdleThread) apply (ctac (no_vcg) add: setVMRoot_ccorres) apply (clarsimp simp: valid_idle'_tcb_at'_ksIdleThread[OF invs_no_cicd'_valid_idle']) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] Arch.switchToIdleThread (Call Arch_switchToIdleThread_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q55 ?Q'55 [SKIP] (getIdleThread >>= setVMRoot) (CALL setVMRoot_'proc(\<acute>ksIdleThread))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q55 s \<and> s' \<in> ?Q'55 proof (prove)
goal (2 subgoals):
 1. \<And>t. ccorres dc xfdc (?P61 t) (?P'61 t) [SKIP] (setVMRoot t) (CALL setVMRoot_'proc(\<acute>ksIdleThread))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksIdleThread s = rv \<longrightarrow> ?P61 rv s) \<and> s' \<in> {s. \<forall>rv. ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'61 rv} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; all_invs_but_ct_idle_or_in_cur_domain' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksIdleThread s = rv \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' rv) s) \<and> s' \<in> {s. \<forall>rv. ksIdleThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksIdleThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>}} proof (prove)
goal:
No subgoals!