kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_C

lemma ccorres_add_returnOk2:
  "ccorres_underlying rf_sr G r xf arrel axf P P' hs (a >>=E returnOk) c
    \<Longrightarrow> ccorres_underlying rf_sr G r xf arrel axf P P' hs a c" by (rule ccorres_add_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr G r xf arrel axf P P' hs (a >>=E returnOk) c \<Longrightarrow> ccorres_underlying rf_sr G r xf arrel axf P P' hs a c
theory Ipc_C

lemma interpret_excaps_empty:
  "(interpret_excaps caps = []) = (index (excaprefs_C caps) 0 = NULL)" by (simp add: interpret_excaps_test_null)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (interpret_excaps caps = []) = (excaprefs_C caps.[0] = NULL)
theory Ipc_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 Ipc_C

lemma lookupIPCBuffer_not_Some_0:
  "\<lbrace>\<top>\<rbrace> lookupIPCBuffer r t \<lbrace>\<lambda>rv. K (rv \<noteq> Some 0)\<rbrace>" apply (simp add: lookupIPCBuffer_def ARM_H.lookupIPCBuffer_def) apply (wp hoare_post_taut haskell_assert_wp
    | simp add: Let_def getThreadBufferSlot_def locateSlotTCB_def
    | intro conjI impI | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookupIPCBuffer r t \<lbrace>\<lambda>rv. K (rv \<noteq> Some 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do bufferPtr <- threadGet tcbIPCBuffer t;
bufferFrameSlot <- getThreadBufferSlot t;
bufferCap <- getSlotCap bufferFrameSlot;
case bufferCap of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz x) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz x) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = vmrights.VMReadWrite \<or> \<not> r \<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 | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing
od \<lbrace>\<lambda>rv y. rv \<noteq> Some 0\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma pbfs_msg_align_bits [simp]:
  "msg_align_bits \<le> pageBitsForSize sz" by (cases sz, auto simp: msg_align_bits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msg_align_bits \<le> pageBitsForSize sz
theory Ipc_C

lemma fault_to_fault_tag_nonzero:
  "fault_to_fault_tag f \<noteq> 0" apply (case_tac f; simp add: seL4_Fault_tag_defs) apply (rename_tac af) apply (case_tac af; simp add: seL4_Fault_tag_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fault_to_fault_tag f \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> arch_fault_to_fault_tag x4 \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>af. f = Fault_H.fault.ArchFault af \<Longrightarrow> arch_fault_to_fault_tag af \<noteq> 0 proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma length_exceptionMessage:
  "length ARM_H.exceptionMessage = unat n_exceptionMessage" by (simp add: ARM_H.exceptionMessage_def ARM.exceptionMessage_def n_exceptionMessage_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length FaultHandler_H.exceptionMessage = unat n_exceptionMessage
theory Ipc_C

lemma Arch_getSanitiseRegisterInfo_ccorres:
  "ccorres ((=) \<circ> from_bool) ret__unsigned_long_'
     (\<top>)
     (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr r}) hs
     (getSanitiseRegisterInfo r)
     (Call Arch_getSanitiseRegisterInfo_'proc)" apply (cinit' lift: thread_' simp: getSanitiseRegisterInfo_def) apply (rule ccorres_return_C, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres ((=) \<circ> from_bool) ret__unsigned_long_' (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr r\<rbrace>) hs (local.getSanitiseRegisterInfo r) (Call Arch_getSanitiseRegisterInfo_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>thread. thread = tcb_ptr_to_ctcb_ptr r \<Longrightarrow> ccorres ((=) \<circ> from_bool) ret__unsigned_long_' (?Q26 thread) (?Q'26 thread) (SKIP # hs) (return False) (return_C ret__unsigned_long_'_update (\<lambda>s. 0))
 2. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr r; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q26 thread s \<and> s' \<in> ?Q'26 thread proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma valid_drop_case: "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s\<rbrace> \<rbrakk>
                       \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some x \<Rightarrow> P' rv s\<rbrace>" apply (simp only: valid_def Ball_def split: prod.split) apply (rule allI impI)+ apply (case_tac x1) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some x \<Rightarrow> P' rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (\<forall>x. x \<in> fst (f s) \<longrightarrow> (case x of (x, xa) \<Rightarrow> P' x xa)) \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>x x1 x2. x = (x1, x2) \<longrightarrow> x \<in> fst (f s) \<longrightarrow> (case x1 of None \<Rightarrow> True | Some x \<Rightarrow> P' x1 x2)) proof (prove)
goal (1 subgoal):
 1. \<And>s x x1 x2. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x. x \<in> fst (f s) \<longrightarrow> (case x of (x, xa) \<Rightarrow> P' x xa)); P s; x = (x1, x2); x \<in> fst (f s)\<rbrakk> \<Longrightarrow> case x1 of None \<Rightarrow> True | Some x \<Rightarrow> P' x1 x2 proof (prove)
goal (2 subgoals):
 1. \<And>s x x1 x2. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x. x \<in> fst (f s) \<longrightarrow> (case x of (x, xa) \<Rightarrow> P' x xa)); P s; x = (x1, x2); x \<in> fst (f s); x1 = None\<rbrakk> \<Longrightarrow> case x1 of None \<Rightarrow> True | Some x \<Rightarrow> P' x1 x2
 2. \<And>s x x1 x2 a. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x. x \<in> fst (f s) \<longrightarrow> (case x of (x, xa) \<Rightarrow> P' x xa)); P s; x = (x1, x2); x \<in> fst (f s); x1 = Some a\<rbrakk> \<Longrightarrow> case x1 of None \<Rightarrow> True | Some x \<Rightarrow> P' x1 x2 proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma sbn_tcbFault:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
  setBoundNotification st t'
  \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_obj_at' | simp cong: if_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> setBoundNotification st t' \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. st)) t' \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma doNormalTransfer_local_slots:
  assumes weak: "\<And>c cap. P (maskedAsFull c cap) = P c"
  shows "\<lbrace> valid_objs' and (Not o real_cte_at' slot)
        and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot \<rbrace>
    doNormalTransfer sender sendBuffer ep badge grant receiver receiveBuffer
   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace>" apply (simp add: doNormalTransfer_def) apply (wp transferCaps_local_slots weak copyMRs_typ_at'[where T=CTET, unfolded typ_at_cte]
    | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> doNormalTransfer sender sendBuffer ep badge grant receiver receiveBuffer \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> do tag <- getMessageInfo sender;
caps <- if grant then lookupExtraCaps sender sendBuffer tag `~catchFailure~` const (return []) else return [];
msgTransferred <- copyMRs sender sendBuffer receiver receiveBuffer (msgLength tag);
tag' <- transferCaps tag caps ep receiver receiveBuffer;
y <- setMessageInfo receiver (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser receiver (setRegister Notification_H.badgeRegister badge)
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma doIPCTransfer_local_slots:
  assumes weak: "\<And>c cap. P (maskedAsFull c cap) = P c"
  shows "\<lbrace> valid_objs' and (Not o real_cte_at' slot)
        and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot \<rbrace>
    doIPCTransfer sender ep badge grant receiver
    \<lbrace> \<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot \<rbrace>" apply (simp add: doIPCTransfer_def) apply (wp doNormalTransfer_local_slots weak threadGet_wp | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> doIPCTransfer sender ep badge grant receiver \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> do receiveBuffer <- lookupIPCBuffer True receiver;
fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer ep badge grant receiver receiveBuffer
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver receiveBuffer
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot) s \<Longrightarrow> \<forall>tcb. ko_at' tcb sender s \<longrightarrow> (tcbFault tcb = None \<longrightarrow> (valid_objs' and Not \<circ> real_cte_at' slot and cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot) s) \<and> (\<forall>x. tcbFault tcb = Some x \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) slot s) proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma rf_sr_tcb_update_twice:
  "h_t_valid (hrs_htd hrs) c_guard ptr
    \<Longrightarrow> ((s, s'\<lparr>globals := globals s''\<lparr>t_hrs_' :=
        hrs_mem_update (heap_update (ptr :: tcb_C ptr) v)
            (hrs_mem_update (heap_update ptr v') hrs)\<rparr>\<rparr>) \<in> rf_sr)
    = ((s, s'\<lparr>globals := globals s''\<lparr>t_hrs_' :=
        hrs_mem_update (heap_update (ptr :: tcb_C ptr) v) hrs\<rparr>\<rparr>) \<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 hrs \<Turnstile>\<^sub>t ptr \<Longrightarrow> ((s, s'\<lparr>globals := globals s''\<lparr>t_hrs_' := hrs_mem_update (heap_update ptr v) (hrs_mem_update (heap_update ptr v') hrs)\<rparr>\<rparr>) \<in> rf_sr) = ((s, s'\<lparr>globals := globals s''\<lparr>t_hrs_' := hrs_mem_update (heap_update ptr v) hrs\<rparr>\<rparr>) \<in> rf_sr)
theory Ipc_C

lemma tcb_queue_relation_last_not_NULL:
  assumes   tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and     tcbs: "queue \<noteq> []"
  shows "tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL" proof - note last_in_set [where as = queue] with tq valid_ep(1) show ?thesis by (rule tcb_queue_relation_not_NULL') fact+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL proof (state)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL proof (state)
this:
queue \<noteq> [] \<Longrightarrow> last queue \<in> set queue

goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL proof (chain)
picking this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
\<forall>t\<in>set queue. tcb_at' t s
queue \<noteq> [] \<Longrightarrow> last queue \<in> set queue proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
\<forall>t\<in>set queue. tcb_at' t s
queue \<noteq> [] \<Longrightarrow> last queue \<in> set queue

goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL proof (state)
this:
tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL

goal:
No subgoals!
theory Ipc_C

lemma tcb_queue_relation_qend_mem':
  "\<lbrakk> tcb_queue_relation' getNext getPrev mp queue qhead qend;
  (\<forall>tcb\<in>set queue. tcb_at' tcb t) \<rbrakk>
  \<Longrightarrow> qend \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qend \<in> set queue" by (clarsimp simp: tcb_queue_head_empty_iff tcb_queue_relation'_def
              split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' getNext getPrev mp queue qhead qend; \<forall>tcb\<in>set queue. tcb_at' tcb t\<rbrakk> \<Longrightarrow> qend \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qend \<in> set queue
theory Ipc_C

lemma tcb_queue_relation_qend_valid':
  "\<lbrakk> tcb_queue_relation' getNext getPrev (cslift s') queue qhead qend;
  (s, s') \<in> rf_sr; (\<forall>tcb\<in>set queue. tcb_at' tcb s) \<rbrakk>
  \<Longrightarrow> qend \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c qend" apply (frule (1) tcb_queue_relation_qend_mem') apply clarsimp apply (drule (3) tcb_queue_memberD [OF tcb_queue_relation'_queue_rel]) apply (simp add: h_t_valid_clift_Some_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' getNext getPrev (cslift s') queue qhead qend; (s, s') \<in> rf_sr; \<forall>tcb\<in>set queue. tcb_at' tcb s\<rbrakk> \<Longrightarrow> qend \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c qend proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' getNext getPrev (cslift s') queue qhead qend; (s, s') \<in> rf_sr; \<forall>tcb\<in>set queue. tcb_at' tcb s; qend \<noteq> NULL \<longrightarrow> ctcb_ptr_to_tcb_ptr qend \<in> set queue\<rbrakk> \<Longrightarrow> qend \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c qend proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' getNext getPrev (cslift s') queue qhead qend; (s, s') \<in> rf_sr; \<forall>tcb\<in>set queue. tcb_at' tcb s; qend \<noteq> NULL; ctcb_ptr_to_tcb_ptr qend \<in> set queue\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c qend proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; \<forall>tcb\<in>set queue. tcb_at' tcb s; qend \<noteq> NULL; ctcb_ptr_to_tcb_ptr qend \<in> set queue; \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr qend)) = Some tcb\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c qend proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma ctcb_relation_blockingIPCCanGrantD:
  "\<lbrakk> ctcb_relation ko ko' ; isReceive (tcbState ko) \<or> isSend (tcbState ko) \<rbrakk>
   \<Longrightarrow> blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko'))
      = from_bool (blockingIPCCanGrant (tcbState ko))" apply (erule disjE; case_tac "tcbState ko" ; clarsimp simp: isReceive_def isSend_def) apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def
                         thread_state_lift_def from_bool_to_bool_iff mask_eq1_nochoice)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_relation ko ko'; isReceive (tcbState ko) \<or> isSend (tcbState ko)\<rbrakk> \<Longrightarrow> blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko')) = from_bool (blockingIPCCanGrant (tcbState ko)) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12. \<lbrakk>ctcb_relation ko ko'; tcbState ko = Structures_H.thread_state.BlockedOnReceive x11 x12\<rbrakk> \<Longrightarrow> blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko')) = from_bool x12
 2. \<And>x71 x72 x73 x74 x75. \<lbrakk>ctcb_relation ko ko'; tcbState ko = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko')) = from_bool x73 proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma ctcb_relation_blockingIPCCanGrantReplyD:
  "\<lbrakk> ctcb_relation ko ko' ; isSend (tcbState ko) \<rbrakk>
   \<Longrightarrow> blockingIPCCanGrantReply_CL (thread_state_lift (tcbState_C ko'))
      = from_bool (blockingIPCCanGrantReply (tcbState ko))" apply ( case_tac "tcbState ko" ; clarsimp simp: isReceive_def isSend_def) apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def
                        thread_state_lift_def from_bool_to_bool_iff mask_eq1_nochoice)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_relation ko ko'; isSend (tcbState ko)\<rbrakk> \<Longrightarrow> blockingIPCCanGrantReply_CL (thread_state_lift (tcbState_C ko')) = from_bool (blockingIPCCanGrantReply (tcbState ko)) proof (prove)
goal (1 subgoal):
 1. \<And>x71 x72 x73 x74 x75. \<lbrakk>ctcb_relation ko ko'; tcbState ko = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> blockingIPCCanGrantReply_CL (thread_state_lift (tcbState_C ko')) = from_bool x74 proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma doNBRecvFailedTransfer_ccorres[corres]:
  "ccorres dc xfdc
            \<top>
            (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread})
            [] (doNBRecvFailedTransfer thread)
            (Call doNBRecvFailedTransfer_'proc)" apply (cinit lift: thread_') apply (ctac add: setRegister_ccorres) by (clarsimp simp: Kernel_C.badgeRegister_def ARM_H.badgeRegister_def
                        ARM.badgeRegister_def Kernel_C.R0_def)

(* 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>) [] (doNBRecvFailedTransfer thread) (Call doNBRecvFailedTransfer_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q30 threada) (?Q'30 threada) [SKIP] (asUser thread (setRegister Notification_H.badgeRegister 0)) (CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0))
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q30 threada s \<and> s' \<in> ?Q'30 threada proof (prove)
goal (1 subgoal):
 1. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>}
theory Ipc_C

lemma st_tcb_at'_ko_at':
  "st_tcb_at' ((=) st) t s = (\<exists>tcb. tcbState tcb = st \<and> ko_at' tcb t s)" unfolding pred_tcb_at'_def by (auto dest: obj_at_ko_at' elim: obj_at'_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' ((=) st) t s = (\<exists>tcb. tcbState tcb = st \<and> ko_at' tcb t s) proof (prove)
goal (1 subgoal):
 1. obj_at' (\<lambda>ko. st = itcbState (tcb_to_itcb' ko)) t s = (\<exists>tcb. tcbState tcb = st \<and> ko_at' tcb t s)
theory Ipc_C

lemma sts_runnable:
  "\<lbrace>if t \<noteq> dest then st_tcb_at' runnable' t else st_tcb_at' \<top> t\<rbrace>
  setThreadState Structures_H.thread_state.Running dest
          \<lbrace>\<lambda>rv. st_tcb_at' runnable' t\<rbrace>" apply (rule hoare_pre) apply (wp sts_st_tcb_at'_cases) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if t \<noteq> dest then st_tcb_at' runnable' t else st_tcb_at' (\<lambda>_. True) t\<rbrace> setThreadState Structures_H.thread_state.Running dest \<lbrace>\<lambda>rv. st_tcb_at' runnable' t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setThreadState Structures_H.thread_state.Running dest \<lbrace>\<lambda>rv. st_tcb_at' runnable' t\<rbrace>
 2. \<And>s. (if t \<noteq> dest then st_tcb_at' runnable' t else st_tcb_at' (\<lambda>_. True) t) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (if t \<noteq> dest then st_tcb_at' runnable' t else st_tcb_at' (\<lambda>_. True) t) s \<Longrightarrow> (dest = t \<longrightarrow> runnable' Structures_H.thread_state.Running \<and> tcb_at' t s) \<and> (dest \<noteq> t \<longrightarrow> st_tcb_at' runnable' t s) proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma ntfn_q_refs_of_no_NTFNBound':
  "(x, NTFNBound) \<notin> ntfn_q_refs_of' ntfn" by (auto simp: ntfn_q_refs_of'_def split: Structures_H.ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, NTFNBound) \<notin> ntfn_q_refs_of' ntfn
theory Ipc_C

lemma ntfnBound_state_refs_equivalence:
  "ko_at' ntfn ntfnptr s \<Longrightarrow> {r \<in> state_refs_of' s ntfnptr. snd r = NTFNBound} = ntfn_bound_refs' (ntfnBoundTCB ntfn)" by (auto simp: ko_at_state_refs_ofD' set_eq_subset ntfn_q_refs_of_no_NTFNBound' ntfn_bound_refs'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' ntfn ntfnptr s \<Longrightarrow> {r \<in> state_refs_of' s ntfnptr. snd r = NTFNBound} = ntfn_bound_refs' (ntfnBoundTCB ntfn)