kings-crown/FVELER_Isabelle huggingface dataset:
theory Arch_C

lemma injection_handler_stateAssert_relocate:
  "injection_handler Inl (stateAssert ass xs >>= f) >>=E g
    = do v \<leftarrow> stateAssert ass xs; injection_handler Inl (f ()) >>=E g od" by (simp add: injection_handler_def handleE'_def bind_bindE_assoc bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler Inl (stateAssert ass xs >>= f) >>=E g = do v <- stateAssert ass xs;
injection_handler Inl (f ()) >>=E g
od
theory Syscall_C

lemma one_on_true_True[simp]: "one_on_true True = 1" by (simp add: one_on_true_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. one_on_true True = 1
theory Syscall_C

lemma one_on_true_eq_0[simp]: "(one_on_true P = 0) = (\<not> P)" by (simp add: one_on_true_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (one_on_true P = 0) = (\<not> P)
theory Syscall_C

lemma cap_cases_one_on_true_sum:
  "one_on_true (isZombie cap) + one_on_true (isArchObjectCap cap)
     + one_on_true (isThreadCap cap) + one_on_true (isCNodeCap cap)
     + one_on_true (isNotificationCap cap) + one_on_true (isEndpointCap cap)
     + one_on_true (isUntypedCap cap) + one_on_true (isReplyCap cap)
     + one_on_true (isIRQControlCap cap) + one_on_true (isIRQHandlerCap cap)
     + one_on_true (isNullCap cap) + one_on_true (isDomainCap cap) = 1" by (cases cap, simp_all add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. one_on_true (isZombie cap) + one_on_true (isArchObjectCap cap) + one_on_true (isThreadCap cap) + one_on_true (isCNodeCap cap) + one_on_true (isNotificationCap cap) + one_on_true (isEndpointCap cap) + one_on_true (isUntypedCap cap) + one_on_true (isReplyCap cap) + one_on_true (isIRQControlCap cap) + one_on_true (isIRQHandlerCap cap) + one_on_true (isNullCap cap) + one_on_true (isDomainCap cap) = 1
theory Syscall_C

lemma wordFromRights_mask_0:
  "wordFromRights rghts && ~~ mask 4 = 0" apply (simp add: wordFromRights_def word_ao_dist word_or_zero
            split: cap_rights.split) apply (simp add: mask_def split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wordFromRights rghts && ~~ mask 4 = 0 proof (prove)
goal (1 subgoal):
 1. \<forall>x1 x2 x3 x4. rghts = CapRights x1 x2 x3 x4 \<longrightarrow> (if x1 then HaskellLib_H.bit 0 else 0) && ~~ mask 4 = 0 \<and> (if x2 then HaskellLib_H.bit (Suc 0) else 0) && ~~ mask 4 = 0 \<and> (if x3 then HaskellLib_H.bit 2 else 0) && ~~ mask 4 = 0 \<and> (if x4 then HaskellLib_H.bit 3 else 0) && ~~ mask 4 = 0 proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma getSlotCap_slotcap_in_mem:
  "\<lbrace>\<top>\<rbrace> getSlotCap slot \<lbrace>\<lambda>cap s. slotcap_in_mem cap slot (ctes_of s)\<rbrace>" apply (simp add: getSlotCap_def) apply (wp getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of slotcap_in_mem_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getSlotCap slot \<lbrace>\<lambda>cap s. slotcap_in_mem cap slot (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do cte <- getCTE slot;
return (cteCap cte)
od \<lbrace>\<lambda>cap s. slotcap_in_mem cap slot (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> slotcap_in_mem (cteCap cte) slot (ctes_of s) proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma lookupExtraCaps_excaps_in_mem[wp]:
  "\<lbrace>\<top>\<rbrace> lookupExtraCaps thread buffer info \<lbrace>\<lambda>rv s. excaps_in_mem rv (ctes_of s)\<rbrace>,-" apply (simp add: excaps_in_mem_def lookupExtraCaps_def lookupCapAndSlot_def
                   split_def) apply (wp mapME_set) apply (wp getSlotCap_slotcap_in_mem | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookupExtraCaps thread buffer info \<lbrace>\<lambda>rv s. excaps_in_mem rv (ctes_of s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> liftE (getExtraCPtrs buffer info) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (doE slot <- lookupSlotForThread thread cptr;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. slotcap_in_mem (fst x) (snd x) (ctes_of s)\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<And>cptrs x slot. \<lbrace>?P'13 cptrs x slot\<rbrace> getSlotCap slot \<lbrace>\<lambda>cap a. slotcap_in_mem (fst (cap, slot)) (snd (cap, slot)) (ctes_of a)\<rbrace>
 2. \<And>cptrs x. \<lbrace>?B7 cptrs\<rbrace> lookupSlotForThread thread x \<lbrace>\<lambda>slot s. True \<and> ?P'13 cptrs x slot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cptrs x y. \<lbrace>?B7 cptrs and (\<lambda>s. slotcap_in_mem (fst x) (snd x) (ctes_of s))\<rbrace> capFaultOnFailure y False (doE slot <- lookupSlotForThread thread y;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>_ s. slotcap_in_mem (fst x) (snd x) (ctes_of s)\<rbrace>, -
 4. \<And>cptrs x. \<lbrace>?B7 cptrs\<rbrace> capFaultOnFailure x False (doE slot <- lookupSlotForThread thread x;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>_. ?B7 cptrs\<rbrace>, -
 5. \<lbrace>?P'6\<rbrace> liftE (getExtraCPtrs buffer info) \<lbrace>?B7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. True \<Longrightarrow> ?P'6 s proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma getCurThread_ccorres:
  "ccorres ((=) \<circ> tcb_ptr_to_ctcb_ptr) thread_'
       \<top> UNIV hs getCurThread (\<acute>thread :== \<acute>ksCurThread)" apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: getCurThread_def simpler_gets_def
                        rf_sr_ksCurThread) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres ((=) \<circ> tcb_ptr_to_ctcb_ptr) thread_' (\<lambda>_. True) UNIV hs getCurThread (\<acute>thread :== \<acute>ksCurThread) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>thread :== \<acute>ksCurThread {s. \<exists>(rv, \<sigma>')\<in>fst (getCurThread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> ((=) \<circ> tcb_ptr_to_ctcb_ptr) rv (thread_' 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 (getCurThread \<sigma>). (\<sigma>', thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> rf_sr \<and> tcb_ptr_to_ctcb_ptr rv = ksCurThread_' (globals s)} proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma getMessageInfo_ccorres:
  "ccorres (\<lambda>rv rv'. rv = messageInfoFromWord rv') ret__unsigned_long_' \<top>
       (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}
             \<inter> {s. reg_' s = register_from_H ARM_H.msgInfoRegister}) []
       (getMessageInfo thread) (Call getRegister_'proc)" apply (simp add: getMessageInfo_def liftM_def[symmetric]
                   ccorres_liftM_simp) apply (rule ccorres_rel_imp, rule ccorres_guard_imp2, rule getRegister_ccorres) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = messageInfoFromWord rv') ret__unsigned_long_' (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>) [] (getMessageInfo thread) (Call getRegister_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres ((\<lambda>rv rv'. rv = messageInfoFromWord rv') \<circ> messageInfoFromWord) ret__unsigned_long_' (\<lambda>_. True) (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>) [] (asUser thread (getRegister TCB_H.msgInfoRegister)) (Call getRegister_'proc) proof (prove)
goal (2 subgoals):
 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>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>\<rbrakk> \<Longrightarrow> True \<and> s' \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>
 2. \<And>x y. x = ret__unsigned_long_' y \<Longrightarrow> ((\<lambda>rv rv'. rv = messageInfoFromWord rv') \<circ> messageInfoFromWord) x (ret__unsigned_long_' y) proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = ret__unsigned_long_' y \<Longrightarrow> ((\<lambda>rv rv'. rv = messageInfoFromWord rv') \<circ> messageInfoFromWord) x (ret__unsigned_long_' y) proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma messageInfoFromWord_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call messageInfoFromWord_'proc
            {s'. seL4_MessageInfo_lift (ret__struct_seL4_MessageInfo_C_' s')
                  = mi_from_H (messageInfoFromWord (w_' s))}" apply (rule allI, rule conseqPost, rule messageInfoFromWord_spec[rule_format]) apply simp_all apply (clarsimp simp: seL4_MessageInfo_lift_def mi_from_H_def
                        messageInfoFromWord_def Let_def msgLabelBits_def
                        Types_H.msgLengthBits_def Types_H.msgExtraCapBits_def
                        Types_H.msgMaxExtraCaps_def shiftL_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call messageInfoFromWord_'proc \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = mi_from_H (messageInfoFromWord \<^bsup>s\<^esup>w)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = (\<^bsup>s\<^esup>w >> 12) && 0xFFFFF, capsUnwrapped_CL = (\<^bsup>s\<^esup>w >> 9) && 7, extraCaps_CL = (\<^bsup>s\<^esup>w >> 7) && 3, length_CL = let v = \<^bsup>s\<^esup>w && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>\<rbrace> \<subseteq> \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = mi_from_H (messageInfoFromWord \<^bsup>s\<^esup>w)\<rbrace>
 2. \<And>s. {} \<subseteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = (\<^bsup>s\<^esup>w >> 12) && 0xFFFFF, capsUnwrapped_CL = (\<^bsup>s\<^esup>w >> 9) && 7, extraCaps_CL = (\<^bsup>s\<^esup>w >> 7) && 3, length_CL = let v = \<^bsup>s\<^esup>w && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>\<rbrace> \<subseteq> \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = mi_from_H (messageInfoFromWord \<^bsup>s\<^esup>w)\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma thread_state_to_tsType_eq_Restart:
  "(thread_state_to_tsType ts = scast ThreadState_Restart)
       = (ts = Restart)" by (cases ts, simp_all add: "StrictC'_thread_state_defs")

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (thread_state_to_tsType ts = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) = (ts = Structures_H.thread_state.Restart)
theory Syscall_C

lemma wordFromMessageInfo_spec:
  "\<forall>s. \<Gamma>\<turnstile> {s} Call wordFromMessageInfo_'proc
      {s'. \<forall>mi. seL4_MessageInfo_lift (mi_' s) = mi_from_H mi
                   \<longrightarrow> ret__unsigned_long_' s' = wordFromMessageInfo mi}" apply (rule allI, rule conseqPost, rule wordFromMessageInfo_spec2[rule_format]) prefer 2 apply simp apply (clarsimp simp: wordFromMessageInfo_def Let_def Types_H.msgExtraCapBits_def
                        Types_H.msgLengthBits_def Types_H.msgMaxExtraCaps_def
                        shiftL_nat) apply (clarsimp simp: mi_from_H_def seL4_MessageInfo_lift_def
                        word_bw_comms word_bw_assocs word_bw_lcs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call wordFromMessageInfo_'proc \<lbrace>\<forall>mia. seL4_MessageInfo_lift \<^bsup>s\<^esup>mi = mi_from_H mia \<longrightarrow> \<acute>ret__unsigned_long = wordFromMessageInfo mia\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrace>\<acute>ret__unsigned_long = (label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 9) || (extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 7) || length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi)\<rbrace> \<subseteq> \<lbrace>\<forall>mia. seL4_MessageInfo_lift \<^bsup>s\<^esup>mi = mi_from_H mia \<longrightarrow> \<acute>ret__unsigned_long = wordFromMessageInfo mia\<rbrace>
 2. \<And>s. {} \<subseteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>s. {} \<subseteq> {}
 2. \<And>s. \<lbrace>\<acute>ret__unsigned_long = (label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 9) || (extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 7) || length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi)\<rbrace> \<subseteq> \<lbrace>\<forall>mia. seL4_MessageInfo_lift \<^bsup>s\<^esup>mi = mi_from_H mia \<longrightarrow> \<acute>ret__unsigned_long = wordFromMessageInfo mia\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>\<acute>ret__unsigned_long = (label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 9) || (extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 7) || length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi)\<rbrace> \<subseteq> \<lbrace>\<forall>mia. seL4_MessageInfo_lift \<^bsup>s\<^esup>mi = mi_from_H mia \<longrightarrow> \<acute>ret__unsigned_long = wordFromMessageInfo mia\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x mi. \<lbrakk>ret__unsigned_long_' x = (label_CL (mi_from_H mi) << 12) || (capsUnwrapped_CL (mi_from_H mi) << 9) || (extraCaps_CL (mi_from_H mi) << 7) || length_CL (mi_from_H mi); seL4_MessageInfo_lift (mi_' s) = mi_from_H mi\<rbrakk> \<Longrightarrow> (label_CL (mi_from_H mi) << 12) || (capsUnwrapped_CL (mi_from_H mi) << 9) || (extraCaps_CL (mi_from_H mi) << 7) || length_CL (mi_from_H mi) = (msgLabel mi << 12) || (msgExtraCaps mi << 7) || (msgCapsUnwrapped mi << 9) || msgLength mi proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma cap_case_EndpointCap:
  "(case cap of EndpointCap ep b cs cr cg cgr \<Rightarrow> f ep b cs cr cg cgr | _ \<Rightarrow> g)
   = (if isEndpointCap cap then f (capEPPtr cap)  (capEPBadge cap) (capEPCanSend cap)
                                  (capEPCanReceive cap) (capEPCanGrant cap) (capEPCanGrantReply cap)
     else g)" by (cases cap; clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.EndpointCap ep b cs cr cg cgr \<Rightarrow> f ep b cs cr cg cgr | _ \<Rightarrow> g) = (if isEndpointCap cap then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap) (capEPCanGrant cap) (capEPCanGrantReply cap) else g)
theory Syscall_C

lemma cap_case_EndpointCap_CanSend_CanGrant:
  "(case cap of EndpointCap v0 v1 True v3 True v4 \<Rightarrow> f v0 v1 v3 v4
              | _ \<Rightarrow> g)
   = (if (isEndpointCap cap \<and> capEPCanSend cap \<and> capEPCanGrant cap)
      then f (capEPPtr cap)  (capEPBadge cap) (capEPCanReceive cap) (capEPCanGrantReply cap)
      else g)" by (simp add: isCap_simps
           split: capability.split bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.EndpointCap v0 v1 True v3 True v4 \<Rightarrow> f v0 v1 v3 v4 | capability.EndpointCap v0 v1 True v3 False v4 \<Rightarrow> g | capability.EndpointCap v0 v1 False v3 bool3 v4 \<Rightarrow> g | _ \<Rightarrow> g) = (if isEndpointCap cap \<and> capEPCanSend cap \<and> capEPCanGrant cap then f (capEPPtr cap) (capEPBadge cap) (capEPCanReceive cap) (capEPCanGrantReply cap) else g)
theory Syscall_C

lemma rf_sr_tcb_update_twice:
  "h_t_valid (hrs_htd (hrs2 (globals s') (t_hrs_' (gs2 (globals s'))))) c_guard
      (ptr (t_hrs_' (gs2 (globals s'))) (globals s'))
    \<Longrightarrow> ((s, globals_update (\<lambda>gs. t_hrs_'_update (\<lambda>ths.
        hrs_mem_update (heap_update (ptr ths gs :: tcb_C ptr) (v ths gs))
            (hrs_mem_update (heap_update (ptr ths gs) (v' ths gs)) (hrs2 gs ths))) (gs2 gs)) s') \<in> rf_sr)
    = ((s, globals_update (\<lambda>gs. t_hrs_'_update (\<lambda>ths.
        hrs_mem_update (heap_update (ptr ths gs) (v ths gs)) (hrs2 gs ths)) (gs2 gs)) s') \<in> rf_sr)" by (simp add: rf_sr_def cstate_relation_def Let_def
                cpspace_relation_def typ_heap_simps'
                carch_state_relation_def
                cmachine_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hrs_htd (hrs2 (globals s') (t_hrs_' (gs2 (globals s')))) \<Turnstile>\<^sub>t ptr (t_hrs_' (gs2 (globals s'))) (globals s') \<Longrightarrow> ((s, globals_update (\<lambda>gs. t_hrs_'_update (\<lambda>ths. hrs_mem_update (heap_update (ptr ths gs) (v ths gs)) (hrs_mem_update (heap_update (ptr ths gs) (v' ths gs)) (hrs2 gs ths))) (gs2 gs)) s') \<in> rf_sr) = ((s, globals_update (\<lambda>gs. t_hrs_'_update (\<lambda>ths. hrs_mem_update (heap_update (ptr ths gs) (v ths gs)) (hrs2 gs ths)) (gs2 gs)) s') \<in> rf_sr)
theory Syscall_C

lemma tcb_cte_cases_tcbFault_update_simp:
  "(f, u) \<in> ran tcb_cte_cases \<Longrightarrow> f (tcbFault_update (\<lambda>_. Some fault) tcb) = f tcb" unfolding tcb_cte_cases_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f, u) \<in> ran tcb_cte_cases \<Longrightarrow> f (tcbFault_update (\<lambda>_. Some fault) tcb) = f tcb proof (prove)
goal (1 subgoal):
 1. (f, u) \<in> ran [0 \<mapsto> (tcb.tcbCTable, tcbCTable_update), 0x10 \<mapsto> (tcb.tcbVTable, tcbVTable_update), 0x20 \<mapsto> (tcb.tcbReply, tcbReply_update), 0x30 \<mapsto> (tcb.tcbCaller, tcbCaller_update), 0x40 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update)] \<Longrightarrow> f (tcbFault_update (\<lambda>_. Some fault) tcb) = f tcb
theory Syscall_C

lemma hrs_mem_update_use_hrs_mem:
  "hrs_mem_update f = (\<lambda>hrs. (hrs_mem_update $ (\<lambda>_. f (hrs_mem hrs))) hrs)" by (simp add: hrs_mem_update_def hrs_mem_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hrs_mem_update f = (\<lambda>hrs. (hrs_mem_update $ (\<lambda>_. f (hrs_mem hrs))) hrs)
theory Syscall_C

lemma length_CL_from_H [simp]:
  "length_CL (mi_from_H mi) = msgLength mi" by (simp add: mi_from_H_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length_CL (mi_from_H mi) = msgLength mi
theory Syscall_C

lemma getMessageInfo_msgLength':
  "\<lbrace>\<top>\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgLength rv \<le> 0x78\<rbrace>" including no_pre apply (simp add: getMessageInfo_def) apply wp apply (rule hoare_strengthen_post, rule hoare_vcg_prop) apply (simp add: messageInfoFromWord_def Let_def msgMaxLength_def not_less
                   Types_H.msgExtraCapBits_def split: if_split ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgLength rv \<le> 0x78\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getMessageInfo t \<lbrace>\<lambda>rv s. msgLength rv \<le> 0x78\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do x <- asUser t (getRegister TCB_H.msgInfoRegister);
return (messageInfoFromWord x)
od \<lbrace>\<lambda>rv s. msgLength rv \<le> 0x78\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> asUser t (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>x a. msgLength (messageInfoFromWord x) \<le> 0x78\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. True \<Longrightarrow> msgLength (messageInfoFromWord rv) \<le> 0x78 proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma invs_valid_objs_strengthen:
  "invs' s \<longrightarrow> valid_objs' s" by fastforce

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

lemma option_to_ctcb_ptr_valid_ntfn:
  "valid_ntfn' ntfn s ==> (option_to_ctcb_ptr (ntfnBoundTCB ntfn) = NULL) = (ntfnBoundTCB ntfn = None)" apply (cases "ntfnBoundTCB ntfn", simp_all add: option_to_ctcb_ptr_def) apply (clarsimp simp: valid_ntfn'_def tcb_at_not_NULL) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ntfn' ntfn s \<Longrightarrow> (option_to_ctcb_ptr (ntfnBoundTCB ntfn) = NULL) = (ntfnBoundTCB ntfn = None) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_ntfn' ntfn s; ntfnBoundTCB ntfn = Some a\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr a \<noteq> NULL proof (prove)
goal:
No subgoals!
theory Syscall_C

lemma getIRQSlot_ccorres3:
  "(\<And>rv. ccorresG rf_sr \<Gamma> r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow>
   ccorresG rf_sr \<Gamma> r xf
     (\<lambda>s. P (intStateIRQNode (ksInterruptState s) + 2 ^ cte_level_bits * of_nat (unat irq)) s)
     {s. s \<in> P' (ptr_val (CTypesDefs.ptr_add intStateIRQNode_Ptr (uint (ucast irq :: word32))))} hs
     (getIRQSlot irq >>= f) c" apply (simp add: getIRQSlot_def locateSlot_conv liftM_def getInterruptState_def) apply (intro ccorres_symb_exec_l'[OF _ _gets_sp] empty_fail_gets gets_inv) apply (rule ccorres_guard_imp2, assumption) by (clarsimp simp: cte_C_size cte_level_bits_def ucast_nat_def
                     rf_sr_def cstate_relation_def Let_def cinterrupt_relation_def
              elim!: rsubst[of "\<lambda>t. _ \<in> P' t"])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf (\<lambda>s. P (irq_node' s + 2 ^ cte_level_bits * word_of_nat (unat irq)) s) {s. s \<in> P' (ptr_val (intStateIRQNode_Ptr +\<^sub>p uint (UCAST(10 \<rightarrow> 32) irq)))} hs (getIRQSlot irq >>= f) c proof (prove)
goal (1 subgoal):
 1. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf (\<lambda>s. P (irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s) (P' (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)))) hs (do x <- gets ksInterruptState;
f (intStateIRQNode x + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)
od) c proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf ((\<lambda>s. P (irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s) and (\<lambda>s. ksInterruptState s = x)) (P' (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)))) hs (f (intStateIRQNode x + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)) c proof (prove)
goal (1 subgoal):
 1. \<And>x s s'. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; ((\<lambda>s. P (irq_node' s + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s) and (\<lambda>s. ksInterruptState s = x)) s; s' \<in> P' (symbol_table ''intStateIRQNode'' + UCAST(10 \<rightarrow> 32) irq * word_of_nat (size_of TYPE(cte_C)))\<rbrakk> \<Longrightarrow> P (intStateIRQNode x + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq) s \<and> s' \<in> P' (intStateIRQNode x + 2 ^ cte_level_bits * UCAST(10 \<rightarrow> 32) irq)