kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_R

lemma lec_derived'[wp]:
  "\<lbrace>invs'\<rbrace>
     lookupExtraCaps t buffer info
   \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. cte_wp_at' (badge_derived' (fst x) o cteCap) (snd x) s)\<rbrace>,-" apply (simp add: lookupExtraCaps_def split del: if_split) apply (rule hoare_pre) apply (wp mapME_set) apply (simp add: lookupCapAndSlot_def split_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> lookupExtraCaps t buffer info \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> liftE (getExtraCPtrs buffer info) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot t cptr)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs buffer info) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot t cptr)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x) s\<rbrace>, -
 2. \<And>s. invs' s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> lookupCapAndSlot t x \<lbrace>\<lambda>x. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x)\<rbrace>, -
 2. \<And>cptrs x y. \<lbrace>?B4 cptrs and cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x)\<rbrace> capFaultOnFailure y False (lookupCapAndSlot t y) \<lbrace>\<lambda>_. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> capFaultOnFailure x False (lookupCapAndSlot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs buffer info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> doE slot <- lookupSlotForThread t x;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE \<lbrace>\<lambda>x. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x)\<rbrace>, -
 2. \<And>cptrs x y. \<lbrace>?B4 cptrs and cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x)\<rbrace> capFaultOnFailure y False (lookupCapAndSlot t y) \<lbrace>\<lambda>_. cte_wp_at' (badge_derived' (fst x) \<circ> cteCap) (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> capFaultOnFailure x False (lookupCapAndSlot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs buffer info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma get_mrs_length_rv[wp]:
  "\<lbrace>\<lambda>s. \<forall>n. n \<le> msg_max_length \<longrightarrow> P n\<rbrace> get_mrs thread buf mi \<lbrace>\<lambda>rv s. P (length rv)\<rbrace>" apply (simp add: get_mrs_def cong: option.case_cong_weak[cong]) apply (rule hoare_pre) apply (wp mapM_length | wpc | simp del: upt.simps)+ apply (clarsimp simp: msgRegisters_unfold
                        msg_max_length_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>n\<le>msg_max_length. P n\<rbrace> get_mrs thread buf mi \<lbrace>\<lambda>rv s. P (length rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>n\<le>msg_max_length. P n\<rbrace> do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) thread;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length];
return (take (unat (mi_length mi)) (map context msg_registers) @ take (unat (mi_length mi) - length msg_registers) buf_mrs)
od \<lbrace>\<lambda>rv s. P (length rv)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) thread;
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length];
return (take (unat (mi_length mi)) (map context msg_registers) @ take (unat (mi_length mi) - length msg_registers) buf_mrs)
od \<lbrace>\<lambda>rv s. P (length rv)\<rbrace>
 2. \<And>s. \<forall>n\<le>msg_max_length. P n \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<forall>n\<le>msg_max_length. P n \<Longrightarrow> (buf = None \<longrightarrow> P (min (length msg_registers) (unat (mi_length mi)))) \<and> ((\<exists>x. buf = Some x) \<longrightarrow> P (min (length msg_registers) (unat (mi_length mi)) + min (msg_max_length - length msg_registers) (unat (mi_length mi) - length msg_registers))) proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma st_tcb_at_idle_thread':
  "\<lbrakk> st_tcb_at' P (ksIdleThread s) s; valid_idle' s \<rbrakk>
        \<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>st_tcb_at' P (ksIdleThread s) s; valid_idle' s\<rbrakk> \<Longrightarrow> P Structures_H.thread_state.IdleThreadState
theory Syscall_R

lemma rct_sch_act_simple[simp]:
  "ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> sch_act_simple s" by (simp add: sch_act_simple_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> sch_act_simple s
theory Syscall_R

lemma rct_sch_act_sane[simp]:
  "ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> sch_act_sane s" by (simp add: sch_act_sane_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> sch_act_sane s
theory Syscall_R

lemma lookupCapAndSlot_real_cte_at'[wp]:
  "\<lbrace>valid_objs'\<rbrace> lookupCapAndSlot thread ptr \<lbrace>\<lambda>rv. real_cte_at' (snd rv)\<rbrace>, -" apply (simp add: lookupCapAndSlot_def lookupSlotForThread_def) apply (wp resolveAddressBits_real_cte_at' | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupCapAndSlot thread ptr \<lbrace>\<lambda>rv. real_cte_at' (snd rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> doE slot <- doE threadRootSlot <- liftE (getThreadCSpaceRoot thread);
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot ptr (size ptr);
returnOk s
odE;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE \<lbrace>\<lambda>rv. real_cte_at' (snd rv)\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma setTCB_valid_duplicates'[wp]:
 "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  setObject a (tcb::tcb) \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (clarsimp simp: setObject_def split_def valid_def in_monad
                        projectKOs pspace_aligned'_def ps_clear_upd
                        objBits_def[symmetric] lookupAround2_char1
                 split: if_split_asm) apply (frule pspace_storable_class.updateObject_type[where v = tcb,simplified]) apply (clarsimp simp:updateObject_default_def assert_def bind_def
    alignCheck_def in_monad when_def alignError_def magnitudeCheck_def
    assert_opt_def return_def fail_def typeError_def
    split:if_splits option.splits Structures_H.kernel_object.splits) apply (erule valid_duplicates'_non_pd_pt_I[rotated 3],simp+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> setObject a tcb \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj'. \<lbrakk>vs_valid_duplicates' (ksPSpace s); aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(aa \<mapsto> obj')) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj'. \<lbrakk>vs_valid_duplicates' (ksPSpace s); aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default tcb ba a aa (snd (lookupAround2 a (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(aa \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s ba s''a aa. \<lbrakk>TCBT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 a (ksPSpace s)) = None; (aa, s''a) \<in> fst (projectKO ba s); a && mask (objBits tcb) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB tcb))
 2. \<And>s ba s''a x2 aa. \<lbrakk>TCBT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 a (ksPSpace s)) = Some x2; \<not> x2 - a < 2 ^ objBits tcb; (aa, s''a) \<in> fst (projectKO ba s); a && mask (objBits tcb) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB tcb)) proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma tcbSchedEnqueue_valid_duplicates'[wp]:
 "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  tcbSchedEnqueue a \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" by (simp add:tcbSchedEnqueue_def unless_def setQueue_def | wp | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> tcbSchedEnqueue a \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
theory Syscall_R

lemma ts_Restart_case_helper':
  "(case ts of Structures_H.Restart \<Rightarrow> A | _ \<Rightarrow> B)
 = (if ts = Structures_H.Restart then A else B)" by (cases ts, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case ts of Structures_H.thread_state.Restart \<Rightarrow> A | _ \<Rightarrow> B) = (if ts = Structures_H.thread_state.Restart then A else B)
theory Syscall_R

lemma gts_imp':
  "\<lbrace>Q\<rbrace> getThreadState t \<lbrace>R\<rbrace> \<Longrightarrow>
   \<lbrace>\<lambda>s. st_tcb_at' P t s \<longrightarrow> Q s\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. P rv \<longrightarrow> R rv s\<rbrace>" apply (simp only: imp_conv_disj) apply (erule hoare_vcg_disj_lift[rotated]) apply (rule hoare_strengthen_post [OF gts_sp']) apply (clarsimp simp: pred_tcb_at'_def obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> getThreadState t \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' P t s \<longrightarrow> Q s\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. P rv \<longrightarrow> R rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> getThreadState t \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> st_tcb_at' P t s \<or> Q s\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. \<not> P rv \<or> R rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> st_tcb_at' P t s\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. \<not> P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (st_tcb_at' (\<lambda>st. st = rv) t and (\<lambda>s. \<not> st_tcb_at' P t s)) s \<Longrightarrow> \<not> P rv proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma rfk_ksQ[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> replyFromKernel t x1 \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>" apply (case_tac x1) apply (simp add: replyFromKernel_def) apply (wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> replyFromKernel t x1 \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. x1 = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> replyFromKernel t x1 \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. x1 = (a, b) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> do destIPCBuffer <- lookupIPCBuffer True t;
y <- asUser t (setRegister Notification_H.badgeRegister 0);
len <- setMRs t destIPCBuffer b;
setMessageInfo t (Types_H.message_info.MI len 0 0 a)
od \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma handleSend_corres:
  "corres (dc \<oplus> dc)
          (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
          (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
           (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active')
          (handle_send blocking) (handleSend blocking)" by (simp add: handle_send_def handleSend_def handleInvocation_corres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') (handle_send blocking) (handleSend blocking)
theory Syscall_R

lemma hs_invs'[wp]:
  "\<lbrace>invs' and ct_active' and
    (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
    (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>
   handleSend blocking \<lbrace>\<lambda>r. invs'\<rbrace>" apply (rule validE_valid) apply (simp add: handleSend_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> handleSend blocking \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> handleSend blocking \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> handleInvocation False blocking \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma getThreadCallerSlot_map:
  "getThreadCallerSlot t = return (cte_map (t, tcb_cnode_index 3))" by (simp add: getThreadCallerSlot_def locateSlot_conv
                cte_map_def tcb_cnode_index_def tcbCallerSlot_def
                cte_level_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getThreadCallerSlot t = return (cte_map (t, tcb_cnode_index 3))
theory Syscall_R

lemma tcb_at_cte_at_map:
  "\<lbrakk> tcb_at' t s; offs \<in> dom tcb_cap_cases \<rbrakk> \<Longrightarrow> cte_at' (cte_map (t, offs)) s" apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (drule tcb_cases_related) apply (auto elim: cte_wp_at_tcbI') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at' t s; offs \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, offs)) s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b obj. \<lbrakk>tcb_cap_cases offs = Some (a, aa, b); ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, offs)) s proof (prove)
goal (1 subgoal):
 1. \<And>a aa b obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; \<exists>getF' setF'. (\<forall>x. tcb_cte_cases (cte_map (x, offs) - x) = Some (getF', setF')) \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (a tcb) (cteCap (getF' tcb')))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (t, offs)) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma deleteCallerCap_invs[wp]:
  "\<lbrace>invs'\<rbrace> deleteCallerCap t \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: deleteCallerCap_def getThreadCallerSlot_def
                locateSlot_conv) apply (wp cteDeleteOne_invs hoare_drop_imps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> deleteCallerCap t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do callerCap <- getSlotCap (t + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne (t + 2 ^ cte_level_bits * tcbCallerSlot)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma deleteCallerCap_simple[wp]:
  "\<lbrace>st_tcb_at' simple' t\<rbrace> deleteCallerCap t' \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>" apply (simp add: deleteCallerCap_def getThreadCallerSlot_def
                   locateSlot_conv) apply (wp cteDeleteOne_st_tcb_at hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' simple' t\<rbrace> deleteCallerCap t' \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' simple' t\<rbrace> do callerCap <- getSlotCap (t' + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (isReplyCap callerCap \<or> callerCap = capability.NullCap);
cteDeleteOne (t' + 2 ^ cte_level_bits * tcbCallerSlot)
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma delete_caller_cap_valid_ep_cap:
  "\<lbrace>valid_cap (cap.EndpointCap r a b)\<rbrace> delete_caller_cap thread \<lbrace>\<lambda>rv. valid_cap (cap.EndpointCap r a b)\<rbrace>" apply (clarsimp simp: delete_caller_cap_def cap_delete_one_def valid_cap_def) apply (rule hoare_pre) by (wp get_cap_wp fast_finalise_typ_at abs_typ_at_lifts(1)
       | simp add: unless_def valid_cap_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap (cap.EndpointCap r a b)\<rbrace> delete_caller_cap thread \<lbrace>\<lambda>rv. valid_cap (cap.EndpointCap r a b)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap (cap.EndpointCap r a b)\<rbrace> do cap <- get_cap (thread, tcb_cnode_index 3);
unless (cap = cap.NullCap) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot (thread, tcb_cnode_index 3) cap.NullCap
od)
od \<lbrace>\<lambda>rv. valid_cap (cap.EndpointCap r a b)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cap <- get_cap (thread, tcb_cnode_index 3);
unless (cap = cap.NullCap) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot (thread, tcb_cnode_index 3) cap.NullCap
od)
od \<lbrace>\<lambda>rv. valid_cap (cap.EndpointCap r a b)\<rbrace>
 2. \<And>s. s \<turnstile> cap.EndpointCap r a b \<Longrightarrow> ?Q s
theory Syscall_R

lemma lookupCap_refs[wp]:
  "\<lbrace>invs'\<rbrace> lookupCap t ref \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' rv. ex_nonz_cap_to' r s\<rbrace>,-" by (simp add: lookupCap_def split_def | wp | simp add: o_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> lookupCap t ref \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' rv. ex_nonz_cap_to' r s\<rbrace>, -
theory Syscall_R

lemma deleteCallerCap_ksQ_ct':
  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane and
     (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> thread = ksCurThread s)\<rbrace>
      deleteCallerCap thread
   \<lbrace>\<lambda>rv s. thread \<notin> set (ksReadyQueues s p)\<rbrace>" apply (rule_tac Q="\<lambda>rv s. thread = ksCurThread s \<and> ksCurThread s \<notin> set (ksReadyQueues s p)"
            in hoare_strengthen_post) apply (wp deleteCallerCap_ct_not_ksQ) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> thread = ksCurThread s)\<rbrace> deleteCallerCap thread \<lbrace>\<lambda>rv s. thread \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> thread = ksCurThread s)\<rbrace> deleteCallerCap thread \<lbrace>\<lambda>rv s. thread = ksCurThread s \<and> ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>rv s. thread = ksCurThread s \<and> ksCurThread s \<notin> set (ksReadyQueues s p) \<Longrightarrow> thread \<notin> set (ksReadyQueues s p) proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> thread = ksCurThread s)) s \<Longrightarrow> thread = ksCurThread s \<and> (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))) s
 2. \<And>rv s. thread = ksCurThread s \<and> ksCurThread s \<notin> set (ksReadyQueues s p) \<Longrightarrow> thread \<notin> set (ksReadyQueues s p) proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma setSchedulerAction_obj_at'[wp]:
  "\<lbrace>obj_at' P p\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. obj_at' P p\<rbrace>" unfolding setSchedulerAction_def by (wp, clarsimp elim!: obj_at'_pspaceI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P p\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P p\<rbrace> modify (ksSchedulerAction_update (\<lambda>_. sa)) \<lbrace>\<lambda>rv. obj_at' P p\<rbrace>