kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_R

lemma setupCallerCap_vq[wp]:
  "\<lbrace>Invariants_H.valid_queues and (\<lambda>s. \<forall>p. send \<notin> set (ksReadyQueues s p))\<rbrace>
   setupCallerCap send recv grant \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" apply (simp add: setupCallerCap_def) apply (wp crunch_wps sts_valid_queues) apply (fastforce simp: valid_queues_def obj_at'_def inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and (\<lambda>s. \<forall>p. send \<notin> set (ksReadyQueues s p))\<rbrace> setupCallerCap send recv grant \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and (\<lambda>s. \<forall>a b. send \<notin> set (ksReadyQueues s (a, b)))\<rbrace> do y <- setThreadState Structures_H.thread_state.BlockedOnReply send;
replySlot <- getThreadReplySlot send;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- getThreadCallerSlot recv;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap send False grant) replySlot callerSlot
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (Invariants_H.valid_queues and (\<lambda>s. \<forall>a b. send \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> Invariants_H.valid_queues s \<and> ((\<exists>p. send \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.BlockedOnReply) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma is_derived_ReplyCap' [simp]:
  "\<And>m p g. is_derived' m p (capability.ReplyCap t False g) =
            (\<lambda>c. \<exists> g. c = capability.ReplyCap t True g)" apply (subst fun_eq_iff) apply clarsimp apply (case_tac x, simp_all add: is_derived'_def isCap_simps
                                   badge_derived'_def
                                   vsCapRef_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m p g. is_derived' m p (capability.ReplyCap t False g) = (\<lambda>c. \<exists>g. c = capability.ReplyCap t True g) proof (prove)
goal (1 subgoal):
 1. \<And>m p g. \<forall>x. is_derived' m p (capability.ReplyCap t False g) x = (\<exists>g. x = capability.ReplyCap t True g) proof (prove)
goal (1 subgoal):
 1. \<And>m p g x. is_derived' m p (capability.ReplyCap t False g) x = (\<exists>g. x = capability.ReplyCap t True g) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma unique_master_reply_cap':
  "\<And>c t. isReplyCap c \<and> capReplyMaster c \<and> capTCBPtr c = t \<longleftrightarrow>
          (\<exists>g . c = capability.ReplyCap t True g)" by (fastforce simp: isCap_simps conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>c t. (isReplyCap c \<and> capReplyMaster c \<and> capTCBPtr c = t) = (\<exists>g. c = capability.ReplyCap t True g)
theory Ipc_R

lemma getSlotCap_cte_wp_at:
  "\<lbrace>\<top>\<rbrace> getSlotCap sl \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = rv) sl\<rbrace>" apply (simp add: getSlotCap_def) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getSlotCap sl \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = rv) sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do cte <- getCTE sl;
return (cteCap cte)
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = rv) sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s \<and> cte_wp_at' (\<lambda>c. cteCap c = cteCap cte) sl s) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma setupCallerCap_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' sender\<rbrace>
   setupCallerCap sender rcvr grant
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" unfolding setupCallerCap_def getThreadCallerSlot_def
            getThreadReplySlot_def locateSlot_conv by (wp getSlotCap_cte_wp_at
          | simp add: unique_master_reply_cap'
          | strengthen eq_imp_strg
          | wp (once) hoare_drop_imp[where f="getCTE rs" for rs])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' sender\<rbrace> setupCallerCap sender rcvr grant \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' sender\<rbrace> do setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- return (sender + 2 ^ cte_level_bits * tcbReplySlot);
masterCTE <- getCTE replySlot;
masterCap <- return (cteCap masterCTE);
haskell_assert (isReplyCap masterCap \<and> capReplyMaster masterCap \<and> capTCBPtr masterCap = sender) [];
haskell_assert (mdbNext (cteMDBNode masterCTE) = nullPointer) [];
callerSlot <- return (rcvr + 2 ^ cte_level_bits * tcbCallerSlot);
callerCap <- getSlotCap callerSlot;
haskell_assert (isNullCap callerCap) [];
cteInsert (capability.ReplyCap sender False grant) replySlot callerSlot
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
theory Ipc_R

lemma setupCallerCap_global_refs'[wp]:
  "\<lbrace>valid_global_refs'\<rbrace>
     setupCallerCap sender rcvr grant
   \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" unfolding setupCallerCap_def getThreadCallerSlot_def
            getThreadReplySlot_def locateSlot_conv apply (wp getSlotCap_cte_wp_at
    | simp add: o_def unique_master_reply_cap'
    | strengthen eq_imp_strg
    | wp (once) getCTE_wp | clarsimp simp: cte_wp_at_ctes_of)+ 
  (* at setThreadState *)
   apply (rule_tac Q="\<lambda>_. valid_global_refs'" in hoare_post_imp, wpsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> setupCallerCap sender rcvr grant \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> do setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- return (sender + 2 ^ cte_level_bits * tcbReplySlot);
masterCTE <- getCTE replySlot;
masterCap <- return (cteCap masterCTE);
haskell_assert (isReplyCap masterCap \<and> capReplyMaster masterCap \<and> capTCBPtr masterCap = sender) [];
haskell_assert (mdbNext (cteMDBNode masterCTE) = nullPointer) [];
callerSlot <- return (rcvr + 2 ^ cte_level_bits * tcbCallerSlot);
callerCap <- getSlotCap callerSlot;
haskell_assert (isNullCap callerCap) [];
cteInsert (capability.ReplyCap sender False grant) replySlot callerSlot
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x a. (\<exists>cte. ctes_of a (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte) \<longrightarrow> (\<exists>cte. ctes_of a (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<and> ((\<exists>g. cteCap cte = capability.ReplyCap sender True g) \<longrightarrow> valid_global_refs' a \<and> (\<exists>cte. ctes_of a (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<and> (\<exists>g. cteCap cte = capability.ReplyCap sender True g))))\<rbrace>
 2. \<And>s. valid_global_refs' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>x a. (\<exists>cte. ctes_of a (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte) \<longrightarrow> (\<exists>cte. ctes_of a (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<and> ((\<exists>g. cteCap cte = capability.ReplyCap sender True g) \<longrightarrow> valid_global_refs' a \<and> (\<exists>cte. ctes_of a (sender + 2 ^ cte_level_bits * tcbReplySlot) = Some cte \<and> (\<exists>g. cteCap cte = capability.ReplyCap sender True g))))\<rbrace>
 2. \<And>s. valid_global_refs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma setupCallerCap_irq_handlers'[wp]:
  "\<lbrace>valid_irq_handlers'\<rbrace>
   setupCallerCap sender rcvr grant
   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" unfolding setupCallerCap_def getThreadCallerSlot_def
            getThreadReplySlot_def locateSlot_conv by (wp hoare_drop_imps | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers'\<rbrace> setupCallerCap sender rcvr grant \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers'\<rbrace> do setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- return (sender + 2 ^ cte_level_bits * tcbReplySlot);
masterCTE <- getCTE replySlot;
masterCap <- return (cteCap masterCTE);
haskell_assert (isReplyCap masterCap \<and> capReplyMaster masterCap \<and> capTCBPtr masterCap = sender) [];
haskell_assert (mdbNext (cteMDBNode masterCTE) = nullPointer) [];
callerSlot <- return (rcvr + 2 ^ cte_level_bits * tcbCallerSlot);
callerCap <- getSlotCap callerSlot;
haskell_assert (isNullCap callerCap) [];
cteInsert (capability.ReplyCap sender False grant) replySlot callerSlot
od \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>
theory Ipc_R

lemma st_tcb_idle':
  "\<lbrakk>valid_idle' s; st_tcb_at' P t s\<rbrakk> \<Longrightarrow>
   (t = ksIdleThread s) \<longrightarrow> P IdleThreadState" by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle' s; st_tcb_at' P t s\<rbrakk> \<Longrightarrow> t = ksIdleThread s \<longrightarrow> P Structures_H.thread_state.IdleThreadState
theory Ipc_R

lemma setupCallerCap_idle'[wp]:
  "\<lbrace>valid_idle' and valid_pspace' and
    (\<lambda>s. st \<noteq> ksIdleThread s \<and> rt \<noteq> ksIdleThread s)\<rbrace>
   setupCallerCap st rt gr
   \<lbrace>\<lambda>_. valid_idle'\<rbrace>" by (simp add: setupCallerCap_def capRange_def | wp hoare_drop_imps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle' and valid_pspace' and (\<lambda>s. st \<noteq> ksIdleThread s \<and> rt \<noteq> ksIdleThread s)\<rbrace> setupCallerCap st rt gr \<lbrace>\<lambda>_. valid_idle'\<rbrace>
theory Ipc_R

lemma setupCallerCap_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> setupCallerCap sender receiver grant \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (simp add: setupCallerCap_def) apply (wp hoare_drop_imp setThreadState_ct_not_inQ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> setupCallerCap sender receiver grant \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> do y <- setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- getThreadReplySlot sender;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- getThreadCallerSlot receiver;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) replySlot callerSlot
od \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma asUser_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> asUser t m \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace>" apply (simp add: asUser_def split_def) apply (wp hoare_drop_imps threadSet_not_inQ | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> asUser t m \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (m uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma ntfn_q_refs_no_bound_refs': "rf : ntfn_q_refs_of' (ntfnObj ob) \<Longrightarrow> rf ~: ntfn_bound_refs' (ntfnBoundTCB ob')" by (auto simp add: ntfn_q_refs_of'_def ntfn_bound_refs'_def
           split: Structures_H.ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rf \<in> ntfn_q_refs_of' (ntfnObj ob) \<Longrightarrow> rf \<notin> ntfn_bound_refs' (ntfnBoundTCB ob')
theory Ipc_R

lemma getCTE_cap_to_refs[wp]:
  "\<lbrace>\<top>\<rbrace> getCTE p \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' (cteCap rv). ex_nonz_cap_to' r s\<rbrace>" apply (rule hoare_strengthen_post [OF getCTE_sp]) apply (clarsimp simp: ex_nonz_cap_to'_def) apply (fastforce elim: cte_wp_at_weakenE') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getCTE p \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' (cteCap rv). ex_nonz_cap_to' r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (cte_wp_at' (\<lambda>c. c = rv) p and (\<lambda>_. True)) s \<Longrightarrow> \<forall>r\<in>zobj_refs' (cteCap rv). ex_nonz_cap_to' r s proof (prove)
goal (1 subgoal):
 1. \<And>rv s r. \<lbrakk>cte_wp_at' (\<lambda>c. c = rv) p s; r \<in> zobj_refs' (cteCap rv)\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at' (\<lambda>c. r \<in> zobj_refs' (cteCap c)) cref s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma lookupCap_cap_to_refs[wp]:
  "\<lbrace>\<top>\<rbrace> lookupCap t cref \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' rv. ex_nonz_cap_to' r s\<rbrace>,-" apply (simp add: lookupCap_def lookupCapAndSlot_def split_def
                   getSlotCap_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookupCap t cref \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' rv. ex_nonz_cap_to' r s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> liftME fst (doE slot <- lookupSlotForThread t cref;
cap <- liftE (do cte <- getCTE slot;
return (cteCap cte)
od);
returnOk (cap, slot)
odE) \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' rv. ex_nonz_cap_to' r s\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma arch_stt_objs' [wp]:
  "\<lbrace>valid_objs'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (simp add: ARM_H.switchToThread_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do y <- setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma cteInsert_invs_bits[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
      cteInsert a b c
   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
  "\<lbrace>Invariants_H.valid_queues\<rbrace> cteInsert a b c \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
  "\<lbrace>cur_tcb'\<rbrace> cteInsert a b c \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>"
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>
      cteInsert a b c
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (wp sch_act_wf_lift valid_queues_lift
          cur_tcb_lift tcb_in_cur_domain'_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> cteInsert a b c \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> &&& \<lbrace>Invariants_H.valid_queues\<rbrace> cteInsert a b c \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>) &&& \<lbrace>cur_tcb'\<rbrace> cteInsert a b c \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> &&& \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> cteInsert a b c \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma gts_st_tcb':
  "\<lbrace>\<top>\<rbrace> getThreadState t \<lbrace>\<lambda>r. st_tcb_at' (\<lambda>st. st = r) t\<rbrace>" apply (rule hoare_strengthen_post) apply (rule gts_sp') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getThreadState t \<lbrace>\<lambda>r. st_tcb_at' (\<lambda>st. st = r) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> getThreadState t \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> st_tcb_at' (\<lambda>st. st = rv) t s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (st_tcb_at' (\<lambda>st. st = rv) t and (\<lambda>_. True)) s \<Longrightarrow> st_tcb_at' (\<lambda>st. st = rv) t s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma setupCallerCap_pred_tcb_unchanged:
  "\<lbrace>pred_tcb_at' proj P t and K (t \<noteq> t')\<rbrace>
     setupCallerCap t' t'' g
   \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>" apply (simp add: setupCallerCap_def getThreadCallerSlot_def
                   getThreadReplySlot_def) apply (wp sts_pred_tcb_neq' hoare_drop_imps) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t and K (t \<noteq> t')\<rbrace> setupCallerCap t' t'' g \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState Structures_H.thread_state.BlockedOnReply t';
replySlot <- locateSlotTCB t' tcbReplySlot;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = t');
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- locateSlotTCB t'' tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap t' False g) replySlot callerSlot
od \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pred_tcb_at' proj P t and (\<lambda>y. t \<noteq> t')) s \<Longrightarrow> (pred_tcb_at' proj P t and K (t \<noteq> t')) s proof (prove)
goal:
No subgoals!
theory Invocations_R

lemma invocationType_eq[simp]:
  "invocationType = invocation_type" unfolding invocationType_def invocation_type_def Let_def by (rule ext, simp) (metis from_to_enum maxBound_is_bound')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invocationType = invocation_type proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if fromIntegral x \<le> fromEnum maxBound then toEnum (fromIntegral x) else if True then GenInvocationLabel InvalidInvocation else undefined) = (\<lambda>x. if \<exists>v. fromEnum v = data_to_nat x then toEnum (data_to_nat x) else GenInvocationLabel InvalidInvocation)
theory Invocations_R

lemma genInvocationType_eq[simp]:
  "genInvocationType = gen_invocation_type" by (rule ext) (simp add: genInvocationType_def gen_invocation_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. genInvocationType = gen_invocation_type
theory CNodeInv_R

lemma rightsFromWord_correspondence:
  "rightsFromWord w = rights_mask_map (data_to_rights w)" by (simp add: rightsFromWord_def rights_mask_map_def data_to_rights_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rightsFromWord w = rights_mask_map (data_to_rights w)
theory CNodeInv_R

lemma corres_split_liftM2:
  assumes    corr: "corres (\<lambda>x y. r' x (f y)) P P' a c"
  and r1: "\<And>rv rv'. r' rv rv' \<Longrightarrow> corres r (R rv) (R' rv') (b rv) (d rv')"
  and h1: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>" and h2: "\<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>x. R' (f x)\<rbrace>"
  shows "corres r (P and Q) (P' and Q') (a >>= b) (liftM f c >>= d)" apply (rule corres_guard_imp) apply (rule corres_split[OF _ _ h1]) apply (simp add: o_def) apply (rule corr) apply (erule r1) apply wp apply (simp add: o_def) apply (rule h2) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (P and Q) (P' and Q') (a >>= b) (liftM f c >>= d) proof (prove)
goal (3 subgoals):
 1. corres r ?Q ?Q' (a >>= b) (liftM f c >>= d)
 2. \<And>s. (P and Q) s \<Longrightarrow> ?Q s
 3. \<And>s. (P' and Q') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. corres ?r'4 ?P4 ?P'4 a (liftM f c)
 2. \<And>rv rv'. ?r'4 rv rv' \<Longrightarrow> corres r (R rv) (?R'4 rv') (b rv) (d rv')
 3. \<lbrace>?Q'4\<rbrace> liftM f c \<lbrace>?R'4\<rbrace>
 4. \<And>s. (P and Q) s \<Longrightarrow> (?P4 and Q) s
 5. \<And>s. (P' and Q') s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. corres (\<lambda>x xa. ?r'4 x (f xa)) ?P4 ?P'4 a c
 2. \<And>rv rv'. ?r'4 rv rv' \<Longrightarrow> corres r (R rv) (?R'4 rv') (b rv) (d rv')
 3. \<lbrace>?Q'4\<rbrace> liftM f c \<lbrace>?R'4\<rbrace>
 4. \<And>s. (P and Q) s \<Longrightarrow> (?P4 and Q) s
 5. \<And>s. (P' and Q') s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. r' rv rv' \<Longrightarrow> corres r (R rv) (?R'4 rv') (b rv) (d rv')
 2. \<lbrace>?Q'4\<rbrace> liftM f c \<lbrace>?R'4\<rbrace>
 3. \<And>s. (P and Q) s \<Longrightarrow> (P and Q) s
 4. \<And>s. (P' and Q') s \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> liftM f c \<lbrace>R'\<rbrace>
 2. \<And>s. (P and Q) s \<Longrightarrow> (P and Q) s
 3. \<And>s. (P' and Q') s \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> c \<lbrace>R' \<circ> f\<rbrace>
 2. \<And>s. (P and Q) s \<Longrightarrow> (P and Q) s
 3. \<And>s. (P' and Q') s \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> c \<lbrace>\<lambda>x. R' (f x)\<rbrace>
 2. \<And>s. (P and Q) s \<Longrightarrow> (P and Q) s
 3. \<And>s. (P' and Q') s \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (P and Q) s \<Longrightarrow> (P and Q) s
 2. \<And>s. (P' and Q') s \<Longrightarrow> (P' and Q') s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P' and Q') s \<Longrightarrow> (P' and Q') s proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma cap_relation_NullCapI:
  "cap_relation c c' \<Longrightarrow> (c = cap.NullCap) = (c' = NullCap)" by (cases c, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> (c = cap.NullCap) = (c' = capability.NullCap)
theory CNodeInv_R

lemma isCNodeCap_CNodeCap:
  "isCNodeCap (CNodeCap a b c d)" by (simp add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isCNodeCap (capability.CNodeCap a b c d)
theory CNodeInv_R

lemma get_cap_corres':
  "cte_ptr' = cte_map cte_ptr \<Longrightarrow>
   corres (\<lambda>x y. cap_relation x (cteCap y)) (cte_at cte_ptr)
    (pspace_aligned' and pspace_distinct') (get_cap cte_ptr)
    (getCTE cte_ptr')" by (simp add: get_cap_corres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_ptr' = cte_map cte_ptr \<Longrightarrow> corres (\<lambda>x y. cap_relation x (cteCap y)) (cte_wp_at (\<lambda>_. True) cte_ptr) (pspace_aligned' and pspace_distinct') (get_cap cte_ptr) (getCTE cte_ptr')
theory CNodeInv_R

lemma cnode_invok_case_cleanup:
  "i \<notin> {CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeRotate, CNodeSaveCaller}
        \<Longrightarrow> (case i of CNodeRevoke \<Rightarrow> P | CNodeDelete \<Rightarrow> Q | CNodeCancelBadgedSends \<Rightarrow> R
                 | CNodeRotate \<Rightarrow> S | CNodeSaveCaller \<Rightarrow> T
                 | _ \<Rightarrow> U) = U" by (simp split: gen_invocation_labels.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i \<notin> {CNodeRevoke, CNodeDelete, CNodeCancelBadgedSends, CNodeRotate, CNodeSaveCaller} \<Longrightarrow> (case i of CNodeRevoke \<Rightarrow> P | CNodeDelete \<Rightarrow> Q | CNodeCancelBadgedSends \<Rightarrow> R | CNodeRotate \<Rightarrow> S | CNodeSaveCaller \<Rightarrow> T | _ \<Rightarrow> U) = U