kings-crown/FVELER_Isabelle huggingface dataset:
theory Move_C

lemma setTCB_cur:
  "\<lbrace>cur_tcb'\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>_. cur_tcb'\<rbrace>" including no_pre apply (wp cur_tcb_lift) apply (simp add: setObject_def split_def updateObject_default_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setObject t v \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setObject t v \<lbrace>\<lambda>_. cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject t v \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 (fromPPtr t) ps));
obj' <- do y <- assert (fromPPtr t = fst p);
_ <- projectKO (snd p);
y <- alignCheck (fromPPtr t) (objBits v);
y <- magnitudeCheck (fromPPtr t) (snd (lookupAround2 (fromPPtr t) ps)) (objBits v);
return (KOTCB v)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P s. P (ksCurThread s) \<Longrightarrow> fst (lookupAround2 (fromPPtr t) (ksPSpace s)) \<noteq> None \<longrightarrow> fromPPtr t = fst (the (fst (lookupAround2 (fromPPtr t) (ksPSpace s)))) \<longrightarrow> P (ksCurThread (s\<lparr>ksPSpace := (ksPSpace s)(fst (the (fst (lookupAround2 (fromPPtr t) (ksPSpace s)))) \<mapsto> KOTCB v)\<rparr>)) proof (prove)
goal:
No subgoals!
theory Move_C

lemma empty_fail_slotCapLongRunningDelete:
  "empty_fail (slotCapLongRunningDelete slot)" by (auto simp: slotCapLongRunningDelete_def Let_def
                 case_Null_If isFinalCapability_def
          split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (slotCapLongRunningDelete slot)
theory Move_C

lemma invs_cicd_arch_state' [elim!]:
  "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_arch_state' s" by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_arch_state' s
theory Move_C

lemma invs_cicd_no_0_obj'[elim!]:
  "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> no_0_obj' s" by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_pspace'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> no_0_obj' s
theory Move_C

lemma getSlotCap_wp':
  "\<lbrace>\<lambda>s. \<forall>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<longrightarrow> Q cap s\<rbrace> getSlotCap p \<lbrace>Q\<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>s. \<forall>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<longrightarrow> Q cap s\<rbrace> getSlotCap p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<longrightarrow> Q cap s\<rbrace> do cte <- getCTE p;
return (cteCap cte)
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<longrightarrow> Q cap s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) p s \<longrightarrow> Q (cteCap cte) s proof (prove)
goal:
No subgoals!
theory Move_C

lemma invs_cicd_valid_objs' [elim!]:
  "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_objs' s" by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_objs' s
theory Move_C

lemma st_tcb_at'_opeq_simp:
  "st_tcb_at' ((=) Structures_H.thread_state.Running) (ksCurThread s) s
    = st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s" by (fastforce simp add: st_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' ((=) Structures_H.thread_state.Running) (ksCurThread s) s = st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s
theory Move_C

lemma invs_queues_imp:
  "invs' s \<longrightarrow> valid_queues s" by clarsimp

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

lemma invs'_pspace_domain_valid:
  "invs' s \<Longrightarrow> pspace_domain_valid s" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> pspace_domain_valid s
theory Move_C

lemma and_eq_0_is_nth:
  fixes x :: "('a :: len) word"
  shows "y = 1 << n \<Longrightarrow> ((x && y) = 0) = (\<not> (x !! n))" by (metis (poly_guards_query) and_eq_0_is_nth)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y = 1 << n \<Longrightarrow> (x && y = 0) = (\<not> x !! n)
theory Move_C

lemma tcbSchedEnqueue_obj_at_unchangedT:
  assumes y: "\<And>f. \<forall>tcb. P (tcbQueued_update f tcb) = P tcb"
  shows  "\<lbrace>obj_at' P t\<rbrace> tcbSchedEnqueue t' \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" apply (simp add: tcbSchedEnqueue_def unless_def) apply (wp | simp add: y)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> tcbSchedEnqueue t' \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> do queued <- threadGet tcbQueued t';
when (\<not> queued) (do tdom <- threadGet tcbDomain t';
prio <- threadGet tcbPriority t';
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t' # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t'
od)
od \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal:
No subgoals!
theory Move_C

lemma rescheduleRequired_obj_at_unchangedT:
  assumes y: "\<And>f. \<forall>tcb. P (tcbQueued_update f tcb) = P tcb"
  shows  "\<lbrace>obj_at' P t\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp tcbSchedEnqueue_obj_at_unchangedT[OF y] | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P t s \<Longrightarrow> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' P t s) \<and> (ksSchedulerAction s = ChooseNewThread \<longrightarrow> obj_at' P t s) \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> obj_at' P t s) proof (prove)
goal:
No subgoals!
theory Move_C

lemma setThreadState_obj_at_unchangedT:
  assumes x: "\<And>f. \<forall>tcb. P (tcbState_update f tcb) = P tcb"
  assumes y: "\<And>f. \<forall>tcb. P (tcbQueued_update f tcb) = P tcb"
  shows "\<lbrace>obj_at' P t\<rbrace> setThreadState t' ts \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" apply (simp add: setThreadState_def) apply (wp rescheduleRequired_obj_at_unchangedT[OF y], simp) apply (wp threadSet_obj_at'_strongish) apply (clarsimp simp: obj_at'_def projectKOs x cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setThreadState t' ts \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. t')) ts;
runnable <- isRunnable ts;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = ts \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. t')) ts \<lbrace>\<lambda>y. obj_at' P t\<rbrace>
 2. \<And>s. obj_at' P t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P t s \<Longrightarrow> obj_at' (\<lambda>obj. if ts = t then P (tcbState_update (\<lambda>_. t') obj) else P obj) t s proof (prove)
goal:
No subgoals!
theory Move_C

lemma setBoundNotification_obj_at_unchangedT:
  assumes x: "\<And>f. \<forall>tcb. P (tcbBoundNotification_update f tcb) = P tcb"
  shows "\<lbrace>obj_at' P t\<rbrace> setBoundNotification t' ts \<lbrace>\<lambda>rv. obj_at' P t\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_obj_at'_strongish) apply (clarsimp simp: obj_at'_def projectKOs x cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setBoundNotification t' ts \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. t')) ts \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P t s \<Longrightarrow> obj_at' (\<lambda>obj. if ts = t then P (tcbBoundNotification_update (\<lambda>_. t') obj) else P obj) t s proof (prove)
goal:
No subgoals!
theory Move_C

lemma magnitudeCheck_assert2:
  "\<lbrakk> is_aligned x n; (1 :: machine_word) < 2 ^ n; ksPSpace s x = Some v \<rbrakk> \<Longrightarrow>
   magnitudeCheck x (snd (lookupAround2 x (ksPSpace (s :: kernel_state)))) n
     = assert (ps_clear x n s)" using in_magnitude_check[where x=x and n=n and s=s and s'=s and v="()"] by (simp add: magnitudeCheck_assert in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v\<rbrakk> \<Longrightarrow> magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n = assert (ps_clear x n s) proof (prove)
using this:
\<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some ?y\<rbrakk> \<Longrightarrow> (((), s) \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s)) = (s = s \<and> ps_clear x n s)

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; 1 < 2 ^ n; ksPSpace s x = Some v\<rbrakk> \<Longrightarrow> magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n = assert (ps_clear x n s)
theory Move_C

lemma range_cover_mask_offset_bound:
  "(ptr && mask sz) + (of_nat p << us) < 2 ^ sz" proof - note sz = range_cover.sz[OF cover] note al = range_cover.aligned[OF cover] have 1: "unat (ptr && mask sz >> us) + p < 2 ^ (sz - us)" using sz(3) p by simp have 2: "(ptr && mask sz >> us) + of_nat p < 2 ^ (sz - us)" using of_nat_power[OF 1 less_imp_diff_less, OF sz(1)]
          of_nat_add word_unat.Rep_inverse by simp have 3: "ptr && mask sz >> us << us = ptr && mask sz" by (rule is_aligned_shiftr_shiftl[OF is_aligned_after_mask[OF al sz(2)]]) have 4: "((ptr && mask sz >> us) + of_nat p) << us < 2 ^ sz" by (rule shiftl_less_t2n[OF 2 sz(1)]) show ?thesis by (rule 4[simplified 3 word_shiftl_add_distrib]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (state)
goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (state)
this:
sz < LENGTH('a)
us \<le> sz
n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)

goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (state)
this:
is_aligned ptr us

goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz >> us) + p < 2 ^ (sz - us) proof (prove)
using this:
n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)
p < n

goal (1 subgoal):
 1. unat (ptr && mask sz >> us) + p < 2 ^ (sz - us) proof (state)
this:
unat (ptr && mask sz >> us) + p < 2 ^ (sz - us)

goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz >> us) + word_of_nat p < 2 ^ (sz - us) proof (prove)
using this:
word_of_nat (unat (ptr && mask sz >> us) + p) < 2 ^ (sz - us)
of_nat (?m + ?n) = of_nat ?m + of_nat ?n
word_of_nat (unat ?x) = ?x

goal (1 subgoal):
 1. (ptr && mask sz >> us) + word_of_nat p < 2 ^ (sz - us) proof (state)
this:
(ptr && mask sz >> us) + word_of_nat p < 2 ^ (sz - us)

goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. ptr && mask sz >> us << us = ptr && mask sz proof (state)
this:
ptr && mask sz >> us << us = ptr && mask sz

goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz >> us) + word_of_nat p << us < 2 ^ sz proof (state)
this:
(ptr && mask sz >> us) + word_of_nat p << us < 2 ^ sz

goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (state)
this:
(ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz

goal:
No subgoals!
theory Move_C

lemma range_cover_neg_mask_offset:
  "ptr + (of_nat p << us) && ~~ mask sz = ptr && ~~ mask sz" apply (subst AND_NOT_mask_plus_AND_mask_eq[of ptr sz, symmetric], subst add.assoc) apply (rule is_aligned_add_helper[THEN conjunct2]) apply (rule Aligned.is_aligned_neg_mask[OF order_refl]) apply (rule range_cover_mask_offset_bound) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr + (word_of_nat p << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. (ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat p << us)) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (2 subgoals):
 1. is_aligned (ptr && ~~ mask sz) sz
 2. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz) + (word_of_nat p << us) < 2 ^ sz proof (prove)
goal:
No subgoals!
theory Move_C

lemma ko_at_projectKO_opt:
  "ko_at' ko p s \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m ksPSpace s) p = Some ko" by (clarsimp elim!: obj_atE' simp: projectKOs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' ko p s \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m ksPSpace s) p = Some ko
theory Move_C

lemma capFaultOnFailure_if_case_sum:
  " (capFaultOnFailure epCPtr b (if c then f else g) >>=
      sum.case_sum (handleFault thread) return) =
    (if c then ((capFaultOnFailure epCPtr b  f)
                 >>= sum.case_sum (handleFault thread) return)
          else ((capFaultOnFailure epCPtr b  g)
                 >>= sum.case_sum (handleFault thread) return))" by (case_tac c, clarsimp, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capFaultOnFailure epCPtr b (if c then f else g) >>= case_sum (handleFault thread) return = (if c then capFaultOnFailure epCPtr b f >>= case_sum (handleFault thread) return else capFaultOnFailure epCPtr b g >>= case_sum (handleFault thread) return)
theory Move_C

lemma dmo_machine_valid_lift:
  "(\<And>s f m. P s = P (ksMachineState_update f s)) \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp f' \<lbrace>\<lambda>rv. P\<rbrace>" apply (wpsimp simp: split_def doMachineOp_def machine_op_lift_def machine_rest_lift_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s f m. P s = P (ksMachineState_update f s)) \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp f' \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Move_C

lemma tcb_runnable_imp_simple:
  "obj_at' (\<lambda>s. runnable' (tcbState s)) t s \<Longrightarrow> obj_at' (\<lambda>s. simple' (tcbState s)) t s" apply (clarsimp simp: obj_at'_def) apply (case_tac "tcbState obj" ; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (\<lambda>s. runnable' (tcbState s)) t s \<Longrightarrow> obj_at' (\<lambda>s. simple' (tcbState s)) t s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; runnable' (tcbState obj); ps_clear t (objBitsKO ko) s; tcbState obj \<noteq> Structures_H.thread_state.Inactive; tcbState obj \<noteq> Structures_H.thread_state.Running; tcbState obj \<noteq> Structures_H.thread_state.Restart; tcbState obj \<noteq> Structures_H.thread_state.BlockedOnReply\<rbrakk> \<Longrightarrow> idle' (tcbState obj) proof (prove)
goal:
No subgoals!
theory Move_C

lemma injection_handler_returnOk:
  "injection_handler injector (returnOk v) = returnOk v" by (simp add: returnOk_liftE injection_liftE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler injector (returnOk v) = returnOk v
theory Move_C

lemma injection_handler_If:
  "injection_handler injector (If P a b)
     = If P (injection_handler injector a)
            (injection_handler injector b)" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler injector (if P then a else b) = (if P then injection_handler injector a else injection_handler injector b)
theory Move_C

lemma injection_handler_throwError:
  "injection_handler f (throwError v) = throwError (f v)" by (simp add: injection_handler_def handleE'_def
                throwError_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler f (throwError v) = throwError (f v)
theory Move_C

lemma injection_handler_whenE:
  "injection_handler injf (whenE P f)
    = whenE P (injection_handler injf f)" by (simp add: whenE_def injection_handler_returnOk split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler injf (whenE P f) = whenE P (injection_handler injf f)
theory Move_C

lemma if_n_updateCapData_valid_strg:
  "s \<turnstile>' cap \<longrightarrow> s \<turnstile>' (if P then cap else updateCapData prs v cap)" by (simp add: valid_updateCapDataI split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' cap s \<longrightarrow> valid_cap' (if P then cap else global.updateCapData prs v cap) s
theory Move_C

lemma tcb_in_cur_domain'_def':
  "tcb_in_cur_domain' t = (\<lambda>s. obj_at' (\<lambda>tcb. tcbDomain tcb = ksCurDomain s) t s)" unfolding tcb_in_cur_domain'_def by (auto simp: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_in_cur_domain' t = (\<lambda>s. obj_at' (\<lambda>tcb. tcbDomain tcb = ksCurDomain s) t s) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s) = (\<lambda>s. obj_at' (\<lambda>tcb. tcbDomain tcb = ksCurDomain s) t s)
theory Move_C

lemma updateCapData_Untyped:
  "isUntypedCap a
         \<Longrightarrow> updateCapData b c a = a" by (clarsimp simp: isCap_simps updateCapData_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap a \<Longrightarrow> global.updateCapData b c a = a
theory Move_C

lemma ctes_of_valid_strengthen:
  "(invs' s \<and> ctes_of s p = Some cte) \<longrightarrow> valid_cap' (cteCap cte) s" apply (case_tac cte) apply clarsimp apply (erule ctes_of_valid_cap') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<and> ctes_of s p = Some cte \<longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. cte = CTE x1 x2 \<Longrightarrow> invs' s \<and> ctes_of s p = Some cte \<longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>cte = CTE x1 x2; invs' s; ctes_of s p = Some (CTE x1 x2)\<rbrakk> \<Longrightarrow> valid_cap' x1 s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>cte = CTE x1 x2; invs' s\<rbrakk> \<Longrightarrow> valid_objs' s proof (prove)
goal:
No subgoals!
theory Move_C

lemma finaliseCap_Reply:
  "\<lbrace>Q (NullCap,NullCap) and K (isReplyCap cap)\<rbrace> finaliseCapTrue_standin cap is_final \<lbrace>Q\<rbrace>" apply (rule Nondet_VCG.hoare_gen_asm) apply (wpsimp simp: finaliseCapTrue_standin_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q (capability.NullCap, capability.NullCap) and K (isReplyCap cap)\<rbrace> finaliseCapTrue_standin cap is_final \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. isReplyCap cap \<Longrightarrow> \<lbrace>Q (capability.NullCap, capability.NullCap)\<rbrace> finaliseCapTrue_standin cap is_final \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Move_C

lemma cteDeleteOne_Reply:
  "\<lbrace>st_tcb_at' P t and cte_wp_at' (isReplyCap o cteCap) slot\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>" apply (simp add: cteDeleteOne_def unless_def split_def) apply (wp finaliseCap_Reply isFinalCapability_inv getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t and cte_wp_at' (isReplyCap \<circ> cteCap) slot\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' P t and cte_wp_at' (isReplyCap \<circ> cteCap) slot\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at' P t and cte_wp_at' (isReplyCap \<circ> cteCap) slot) s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> (if cteCap cte \<noteq> capability.NullCap then (\<lambda>s. capRemovable (fst (capability.NullCap, capability.NullCap)) slot \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<longrightarrow> st_tcb_at' P t s) and K (isReplyCap (cteCap cte)) else st_tcb_at' P t) s proof (prove)
goal:
No subgoals!