kings-crown/FVELER_Isabelle huggingface dataset:
theory Move_C

lemma cancelSignal_st_tcb':
  "\<lbrace>\<lambda>s. t\<noteq>t' \<and> st_tcb_at' P t' s\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>" apply (simp add: cancelSignal_def Let_def) apply (rule hoare_pre) apply (wp sts_pred_tcb_neq' getNotification_wp | wpc)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t \<noteq> t' \<and> st_tcb_at' P t' s\<rbrace> cancelSignal t ntfn \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t \<noteq> t' \<and> st_tcb_at' P t' s\<rbrace> do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ntfna <- getNotification ntfn;
y <- assert (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfna)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfna))) (ntfnObj ntfna);
y <- setNotification ntfn (ntfnObj_update (\<lambda>_. ntfn') ntfna);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 2. \<And>s. t \<noteq> t' \<and> st_tcb_at' P t' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. t \<noteq> t' \<and> st_tcb_at' P t' s \<Longrightarrow> \<forall>ntfna. ko_at' ntfna ntfn s \<longrightarrow> (case ntfnObj ntfna of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (ntfnQueue (ntfnObj ntfna)) = [] \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) \<and> (\<forall>x xa. remove1 t (ntfnQueue (ntfnObj ntfna)) = x # xa \<longrightarrow> st_tcb_at' P t' s \<and> K (t' \<noteq> t) s) proof (prove)
goal:
No subgoals!
theory Move_C

lemma suspend_st_tcb_at':
  "\<lbrace>\<lambda>s. (t\<noteq>t' \<longrightarrow> st_tcb_at' P t' s) \<and> (t=t' \<longrightarrow> P Inactive)\<rbrace>
  suspend t
  \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>" apply (simp add: suspend_def unless_def) unfolding updateRestartPC_def apply (cases "t=t'") apply (simp | wp cancelIPC_st_tcb_at' sts_st_tcb')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (t \<noteq> t' \<longrightarrow> st_tcb_at' P t' s) \<and> (t = t' \<longrightarrow> P Structures_H.thread_state.Inactive)\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (t \<noteq> t' \<longrightarrow> st_tcb_at' P t' s) \<and> (t = t' \<longrightarrow> P Structures_H.thread_state.Inactive)\<rbrace> do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (t \<noteq> t' \<longrightarrow> st_tcb_at' P t' s) \<and> (t = t' \<longrightarrow> P Structures_H.thread_state.Inactive)\<rbrace> do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>\<lambda>s. (t \<noteq> t' \<longrightarrow> st_tcb_at' P t' s) \<and> (t = t' \<longrightarrow> P Structures_H.thread_state.Inactive)\<rbrace> do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. (t \<noteq> t' \<longrightarrow> st_tcb_at' P t' s) \<and> (t = t' \<longrightarrow> P Structures_H.thread_state.Inactive)\<rbrace> do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>_. st_tcb_at' P t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Move_C

lemma typ_at'_no_0_objD:
  "typ_at' P p s \<Longrightarrow> no_0_obj' s \<Longrightarrow> p \<noteq> 0" by (cases "p = 0" ; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at' P p s; no_0_obj' s\<rbrakk> \<Longrightarrow> p \<noteq> 0
theory Move_C

lemma ko_at'_not_NULL:
  "\<lbrakk> ko_at' ko p s ; no_0_obj' s\<rbrakk>
   \<Longrightarrow> p \<noteq> 0" by (fastforce simp:  word_gt_0 typ_at'_no_0_objD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko p s; no_0_obj' s\<rbrakk> \<Longrightarrow> p \<noteq> 0
theory Move_C

lemma sts_running_ksReadyQueuesL1Bitmap[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
   setThreadState Structures_H.thread_state.Running t
   \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>" unfolding setThreadState_def apply wp apply (rule hoare_pre_cont) apply (wpsimp simp: if_apply_def2
                    wp: hoare_drop_imps hoare_vcg_disj_lift threadSet_tcbState_st_tcb_at')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> setThreadState Structures_H.thread_state.Running t \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.Running)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) $ rescheduleRequired
od \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x runnable curThread action. \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread \<Longrightarrow> \<lbrace>?Q7 x runnable curThread action\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
 2. \<And>x runnable curThread. \<lbrace>?B4 x runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. if \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread then ?Q7 x runnable curThread action else (\<lambda>s. P (ksReadyQueuesL1Bitmap s))\<rbrace>
 3. \<And>x runnable. \<lbrace>?B3 x runnable\<rbrace> getCurThread \<lbrace>?B4 x runnable\<rbrace>
 4. \<And>x. \<lbrace>?B1 x\<rbrace> isRunnable t \<lbrace>?B3 x\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.Running)) t \<lbrace>?B1\<rbrace>
 6. \<And>s. P (ksReadyQueuesL1Bitmap s) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x runnable curThread. \<lbrace>?B4 x runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. if \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread then \<lambda>_. False else (\<lambda>s. P (ksReadyQueuesL1Bitmap s))\<rbrace>
 2. \<And>x runnable. \<lbrace>?B3 x runnable\<rbrace> getCurThread \<lbrace>?B4 x runnable\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> isRunnable t \<lbrace>?B3 x\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.Running)) t \<lbrace>?B1\<rbrace>
 5. \<And>s. P (ksReadyQueuesL1Bitmap s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Move_C

lemma sts_running_ksReadyQueuesL2Bitmap[wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
   setThreadState Structures_H.thread_state.Running t
   \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>" unfolding setThreadState_def apply wp apply (rule hoare_pre_cont) apply (wpsimp simp: if_apply_def2
                    wp: hoare_drop_imps hoare_vcg_disj_lift threadSet_tcbState_st_tcb_at')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> setThreadState Structures_H.thread_state.Running t \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.Running)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) $ rescheduleRequired
od \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x runnable curThread action. \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread \<Longrightarrow> \<lbrace>?Q7 x runnable curThread action\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
 2. \<And>x runnable curThread. \<lbrace>?B4 x runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. if \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread then ?Q7 x runnable curThread action else (\<lambda>s. P (ksReadyQueuesL2Bitmap s))\<rbrace>
 3. \<And>x runnable. \<lbrace>?B3 x runnable\<rbrace> getCurThread \<lbrace>?B4 x runnable\<rbrace>
 4. \<And>x. \<lbrace>?B1 x\<rbrace> isRunnable t \<lbrace>?B3 x\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.Running)) t \<lbrace>?B1\<rbrace>
 6. \<And>s. P (ksReadyQueuesL2Bitmap s) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x runnable curThread. \<lbrace>?B4 x runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. if \<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread then \<lambda>_. False else (\<lambda>s. P (ksReadyQueuesL2Bitmap s))\<rbrace>
 2. \<And>x runnable. \<lbrace>?B3 x runnable\<rbrace> getCurThread \<lbrace>?B4 x runnable\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> isRunnable t \<lbrace>?B3 x\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.Running)) t \<lbrace>?B1\<rbrace>
 5. \<And>s. P (ksReadyQueuesL2Bitmap s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Move_C

lemma asUser_obj_at_not_queued[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace>" apply (simp add: asUser_def split_def) apply (wp hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<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. obj_at' (\<lambda>tcb. \<not> tcbQueued tcb) p\<rbrace> proof (prove)
goal:
No subgoals!
theory Move_C

lemma ko_at'_obj_at'_field:
  "ko_at' ko (t s) s \<Longrightarrow> obj_at' (\<lambda>ko'. f ko' = f ko) (t s) s" by (erule obj_at'_weakenE, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' ko (t s) s \<Longrightarrow> obj_at' (\<lambda>ko'. f ko' = f ko) (t s) s
theory Move_C

lemma cond_throw_whenE:
   "(if P then f else throwError e) = (whenE (\<not> P) (throwError e) >>=E (\<lambda>_. f))" by (auto split: if_splits
             simp: throwError_def bindE_def
                   whenE_def bind_def returnOk_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then f else throwError e) = doE _ <- whenE (\<not> P) (throwError e);
f
odE
theory Move_C

lemma ksPSpace_update_eq_ExD:
  "s = t\<lparr> ksPSpace := ksPSpace s\<rparr>
     \<Longrightarrow> \<exists>ps. s = t \<lparr> ksPSpace := ps \<rparr>" by (erule exI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s = t\<lparr>ksPSpace := ksPSpace s\<rparr> \<Longrightarrow> \<exists>ps. s = t\<lparr>ksPSpace := ps\<rparr>
theory Move_C

lemma tcbSchedEnqueue_queued_queues_inv:
  "\<lbrace>\<lambda>s.  obj_at' tcbQueued t s \<and> P (ksReadyQueues s) \<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>" unfolding tcbSchedEnqueue_def unless_def apply (wpsimp simp: if_apply_def2 wp: threadGet_wp) apply normalise_obj_at' done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' tcbQueued t s \<and> P (ksReadyQueues s)\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' tcbQueued t s \<and> P (ksReadyQueues s)\<rbrace> do queued <- threadGet tcbQueued t;
when (\<not> queued) $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ t # queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s tcb tcba tcbb. \<lbrakk>obj_at' tcbQueued t s; P (ksReadyQueues s); ko_at' tcb t s; \<not> tcbQueued tcb; ko_at' tcba t s; ko_at' tcbb t s\<rbrakk> \<Longrightarrow> P (\<lambda>a. if a = (tcbDomain tcba, tcbPriority tcbb) then t # ksReadyQueues s (tcbDomain tcba, tcbPriority tcbb) else ksReadyQueues s a) proof (prove)
goal:
No subgoals!
theory Move_C

lemma word_clz_1[simp]:
  "word_clz (1::32 word) = 31"
  "word_clz (1::64 word) = 63" by (clarsimp simp: word_clz_def to_bl_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_clz 1 = 31 &&& word_clz 1 = 63
theory Move_C

lemma word_ctz_0[simp]:
  "word_ctz (0::32 word) = 32"
  "word_ctz (0::64 word) = 64" by (clarsimp simp: word_ctz_def to_bl_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_ctz 0 = 32 &&& word_ctz 0 = 64
theory Move_C

lemma unat_trans_ucast_helper:
  "\<lbrakk> unat x < n ; n \<le> Suc 0 \<rbrakk> \<Longrightarrow> ucast x = 0" by (simp add: le_Suc_eq unsigned_eq_0_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x < n; n \<le> Suc 0\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 'b) x = 0
theory Move_C

lemma numPriorities_machine_word_safe:
  "unat (of_nat numPriorities :: machine_word) = numPriorities" by (simp add: numPriorities_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat Config_H.numPriorities) = Config_H.numPriorities
theory Move_C

lemma word_zero_less_one[simp]:
  "0 < (1::'a::len word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < 1
theory Move_C

lemma koTypeOf_injectKO:
  fixes v :: "'a :: pspace_storable" shows
  "koTypeOf (injectKO v) = koType TYPE('a)" apply (cut_tac v1=v in iffD2 [OF project_inject, OF refl]) apply (simp add: project_koType[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. koTypeOf (injectKOS v) = koType TYPE('a) proof (prove)
goal (1 subgoal):
 1. projectKO_opt (injectKOS v) = Some v \<Longrightarrow> koTypeOf (injectKOS v) = koType TYPE('a) proof (prove)
goal:
No subgoals!
theory Move_C

lemma ctes_of_cte_at:
  "ctes_of s p = Some x \<Longrightarrow> cte_at' p s" by (simp add: cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s p = Some x \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s
theory Move_C

lemma updateObject_cte_tcb:
  assumes tc: "tcb_cte_cases (ptr - ptr') = Some (accF, updF)"
  shows   "updateObject ctea (KOTCB tcb) ptr ptr' next =
   (do alignCheck ptr' (objBits tcb);
        magnitudeCheck ptr' next (objBits tcb);
        return (KOTCB (updF (\<lambda>_. ctea) tcb))
    od)" using tc unfolding tcb_cte_cases_def apply - apply (clarsimp simp add: updateObject_cte Let_def
    tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n
    split: if_split_asm cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. updateObject ctea (KOTCB tcb) ptr ptr' next = do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od proof (prove)
using this:
tcb_cte_cases (ptr - ptr') = Some (accF, updF)

goal (1 subgoal):
 1. updateObject ctea (KOTCB tcb) ptr ptr' next = do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od proof (prove)
using this:
[0 \<mapsto> (tcbCTable, tcbCTable_update), 0x10 \<mapsto> (tcbVTable, tcbVTable_update), 0x20 \<mapsto> (tcbReply, tcbReply_update), 0x30 \<mapsto> (tcbCaller, tcbCaller_update), 0x40 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update)] (ptr - ptr') = Some (accF, updF)

goal (1 subgoal):
 1. updateObject ctea (KOTCB tcb) ptr ptr' next = do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od proof (prove)
goal (1 subgoal):
 1. [0 \<mapsto> (tcbCTable, tcbCTable_update), 0x10 \<mapsto> (tcbVTable, tcbVTable_update), 0x20 \<mapsto> (tcbReply, tcbReply_update), 0x30 \<mapsto> (tcbCaller, tcbCaller_update), 0x40 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update)] (ptr - ptr') = Some (accF, updF) \<Longrightarrow> updateObject ctea (KOTCB tcb) ptr ptr' next = do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od proof (prove)
goal:
No subgoals!
theory Move_C

lemma tcb_cte_cases_in_range1:
  assumes tc:"tcb_cte_cases (y - x) = Some v"
  and     al: "is_aligned x tcbBlockSizeBits"
  shows   "x \<le> y" proof - note objBits_defs [simp] from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ tcbBlockSizeBits" unfolding tcb_cte_cases_def by (simp add: diff_eq_eq split: if_split_asm) have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al by (rule is_aligned_no_overflow) hence "x \<le> x + q" using qv apply simp apply unat_arith apply simp done thus ?thesis using yq by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> y proof (state)
goal (1 subgoal):
 1. x \<le> y proof (state)
this:
tcbBlockSizeBits \<equiv> 9
epSizeBits \<equiv> 4
ntfnSizeBits \<equiv> wordSizeCase 4 5
cteSizeBits \<equiv> wordSizeCase 4 5

goal (1 subgoal):
 1. x \<le> y proof (chain)
picking this:
tcb_cte_cases (y - x) = Some v proof (prove)
using this:
tcb_cte_cases (y - x) = Some v

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>y = x + q; q < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
[0 \<mapsto> (tcbCTable, tcbCTable_update), 0x10 \<mapsto> (tcbVTable, tcbVTable_update), 0x20 \<mapsto> (tcbReply, tcbReply_update), 0x30 \<mapsto> (tcbCaller, tcbCaller_update), 0x40 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update)] (y - x) = Some v

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>y = x + q; q < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
y = x + q
q < 2 ^ tcbBlockSizeBits

goal (1 subgoal):
 1. x \<le> y proof (prove)
goal (1 subgoal):
 1. x \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (prove)
using this:
is_aligned x tcbBlockSizeBits

goal (1 subgoal):
 1. x \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
this:
x \<le> x + 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. x \<le> y proof (prove)
using this:
x \<le> x + 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. x \<le> x + q proof (prove)
using this:
x \<le> x + 2 ^ tcbBlockSizeBits - 1
q < 2 ^ tcbBlockSizeBits

goal (1 subgoal):
 1. x \<le> x + q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0x1FF + x; q < 0x200\<rbrakk> \<Longrightarrow> x \<le> x + q proof (prove)
goal (1 subgoal):
 1. \<And>n na nb nc nd. \<lbrakk>n < 2 ^ LENGTH(32); n < 512; na < 2 ^ LENGTH(32); \<not> 511 + na < 2 ^ LENGTH(32); nb < 2 ^ LENGTH(32); nb \<le> 511 + nb - 2 ^ LENGTH(32); \<not> nd + nc < 2 ^ LENGTH(32); nc < 2 ^ LENGTH(32); nd < 2 ^ LENGTH(32); unat q = n; unat x = na; unat x = nb; unat q = nc; unat x = nd\<rbrakk> \<Longrightarrow> nd \<le> nd + nc - 2 ^ LENGTH(32) proof (prove)
goal:
No subgoals! proof (state)
this:
x \<le> x + q

goal (1 subgoal):
 1. x \<le> y proof (prove)
using this:
x \<le> x + q

goal (1 subgoal):
 1. x \<le> y proof (prove)
using this:
x \<le> x + q
y = x + q

goal (1 subgoal):
 1. x \<le> y proof (state)
this:
x \<le> y

goal:
No subgoals!
theory Move_C

lemma tcb_cte_cases_in_range2:
  assumes tc: "tcb_cte_cases (y - x) = Some v"
  and     al: "is_aligned x tcbBlockSizeBits"
  shows   "y \<le> x + 2 ^ tcbBlockSizeBits - 1" proof - note objBits_defs [simp] from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1" unfolding tcb_cte_cases_def by (simp add: diff_eq_eq split: if_split_asm) have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv apply (rule word_plus_mono_right) apply (rule is_aligned_no_overflow' [OF al]) done thus ?thesis using yq by (simp add: field_simps) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
goal (1 subgoal):
 1. y \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
this:
tcbBlockSizeBits \<equiv> 9
epSizeBits \<equiv> 4
ntfnSizeBits \<equiv> wordSizeCase 4 5
cteSizeBits \<equiv> wordSizeCase 4 5

goal (1 subgoal):
 1. y \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (chain)
picking this:
tcb_cte_cases (y - x) = Some v proof (prove)
using this:
tcb_cte_cases (y - x) = Some v

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>y = x + q; q \<le> 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
[0 \<mapsto> (tcbCTable, tcbCTable_update), 0x10 \<mapsto> (tcbVTable, tcbVTable_update), 0x20 \<mapsto> (tcbReply, tcbReply_update), 0x30 \<mapsto> (tcbCaller, tcbCaller_update), 0x40 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update)] (y - x) = Some v

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>y = x + q; q \<le> 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
y = x + q
q \<le> 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. y \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. x + q \<le> x + (2 ^ tcbBlockSizeBits - 1) proof (prove)
using this:
q \<le> 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. x + q \<le> x + (2 ^ tcbBlockSizeBits - 1) proof (prove)
goal (1 subgoal):
 1. x \<le> x + (2 ^ tcbBlockSizeBits - 1) proof (prove)
goal:
No subgoals! proof (state)
this:
x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)

goal (1 subgoal):
 1. y \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (prove)
using this:
x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)

goal (1 subgoal):
 1. y \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (prove)
using this:
x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)
y = x + q

goal (1 subgoal):
 1. y \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
this:
y \<le> x + 2 ^ tcbBlockSizeBits - 1

goal:
No subgoals!