kings-crown/FVELER_Isabelle huggingface dataset:
theory Fastpath_Equiv

lemma fastpathBestSwitchCandidateI:
  "\<lbrakk> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0
     \<or> tcbPriority ctcb \<le> tcbPriority ttcb
     \<or> lookupBitmapPriority (ksCurDomain s) s \<le> tcbPriority ttcb;
     ko_at' ttcb t s; ko_at' ctcb (ksCurThread s) s\<rbrakk>
   \<Longrightarrow> fastpathBestSwitchCandidate t s" unfolding fastpathBestSwitchCandidate_def by normalise_obj_at'

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> tcbPriority ctcb \<le> tcbPriority ttcb \<or> lookupBitmapPriority (ksCurDomain s) s \<le> tcbPriority ttcb; ko_at' ttcb t s; ko_at' ctcb (ksCurThread s) s\<rbrakk> \<Longrightarrow> fastpathBestSwitchCandidate t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> tcbPriority ctcb \<le> tcbPriority ttcb \<or> lookupBitmapPriority (ksCurDomain s) s \<le> tcbPriority ttcb; ko_at' ttcb t s; ko_at' ctcb (ksCurThread s) s\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> (\<forall>tprio. obj_at' (\<lambda>tcb. tcbPriority tcb = tprio) t s \<longrightarrow> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> tprio) (ksCurThread s) s \<or> lookupBitmapPriority (ksCurDomain s) s \<le> tprio)
theory Fastpath_Equiv

lemma resolveAddressBits_points_somewhere:
  "\<lbrace>\<lambda>s. \<forall>slot. Q slot s\<rbrace> resolveAddressBits cp cptr bits \<lbrace>Q\<rbrace>,-" apply (rule_tac Q'="\<lambda>rv s. \<forall>rv. Q rv s" in hoare_post_imp_R) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>slot. Q slot s\<rbrace> CSpace_H.resolveAddressBits cp cptr bits \<lbrace>Q\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>slot. Q slot s\<rbrace> CSpace_H.resolveAddressBits cp cptr bits \<lbrace>\<lambda>rv s. \<forall>rv. Q rv s\<rbrace>, -
 2. \<And>rv s. \<forall>rv. Q rv s \<Longrightarrow> Q rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>rv. Q rv s \<Longrightarrow> Q rv s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma foldr_copy_register_tsrs:
  "foldr (\<lambda>r . copy_register_tsrs x y r r (\<lambda>x. x)) rs s
       = (s (y := TCBStateRegs (tsrState (s y))
                       (\<lambda>r. if r \<in> set rs then tsrContext (s x) r
                                 else tsrContext (s y) r)))" apply (induct rs) apply simp apply (simp add: copy_register_tsrs_def fun_eq_iff
            split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>r. copy_register_tsrs x y r r (\<lambda>x. x)) rs s = s(y := TCBStateRegs (tsrState (s y)) (\<lambda>r. if r \<in> set rs then tsrContext (s x) r else tsrContext (s y) r)) proof (prove)
goal (2 subgoals):
 1. foldr (\<lambda>r. copy_register_tsrs x y r r (\<lambda>x. x)) [] s = s(y := TCBStateRegs (tsrState (s y)) (\<lambda>r. if r \<in> set [] then tsrContext (s x) r else tsrContext (s y) r))
 2. \<And>a rs. foldr (\<lambda>r. copy_register_tsrs x y r r (\<lambda>x. x)) rs s = s(y := TCBStateRegs (tsrState (s y)) (\<lambda>r. if r \<in> set rs then tsrContext (s x) r else tsrContext (s y) r)) \<Longrightarrow> foldr (\<lambda>r. copy_register_tsrs x y r r (\<lambda>x. x)) (a # rs) s = s(y := TCBStateRegs (tsrState (s y)) (\<lambda>r. if r \<in> set (a # rs) then tsrContext (s x) r else tsrContext (s y) r)) proof (prove)
goal (1 subgoal):
 1. \<And>a rs. foldr (\<lambda>r. copy_register_tsrs x y r r (\<lambda>x. x)) rs s = s(y := TCBStateRegs (tsrState (s y)) (\<lambda>r. if r \<in> set rs then tsrContext (s x) r else tsrContext (s y) r)) \<Longrightarrow> foldr (\<lambda>r. copy_register_tsrs x y r r (\<lambda>x. x)) (a # rs) s = s(y := TCBStateRegs (tsrState (s y)) (\<lambda>r. if r \<in> set (a # rs) then tsrContext (s x) r else tsrContext (s y) r)) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma monadic_rewrite_threadGet:
  "monadic_rewrite E F (obj_at' (\<lambda>tcb. f tcb = v) t)
    (threadGet f t) (return v)" unfolding getThreadState_def threadGet_def apply (simp add: liftM_def) apply monadic_rewrite_symb_exec_l apply (rule_tac P="\<lambda>_. f x = v" in monadic_rewrite_pre_imp_eq) apply blast apply (wpsimp wp: OMG_getObject_tcb simp: obj_tcb_at')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite E F (obj_at' (\<lambda>tcb. f tcb = v) t) (threadGet f t) (return v) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite E F (obj_at' (\<lambda>tcb. f tcb = v) t) (liftM f $ getObject t) (return v) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite E F (obj_at' (\<lambda>tcb. f tcb = v) t) (do x <- getObject t;
return (f x)
od) (return v) proof (prove)
goal (3 subgoals):
 1. \<And>x. monadic_rewrite E F (?Q2 x) (return (f x)) (return v)
 2. \<lbrace>?P2\<rbrace> getObject t \<lbrace>?Q2\<rbrace>
 3. \<And>s. obj_at' (\<lambda>tcb. f tcb = v) t s \<Longrightarrow> (?P2 and tcb_at' t) s proof (prove)
goal (3 subgoals):
 1. \<And>x s. f x = v \<Longrightarrow> return (f x) s = return v s
 2. \<lbrace>?P2\<rbrace> getObject t \<lbrace>\<lambda>x _. f x = v\<rbrace>
 3. \<And>s. obj_at' (\<lambda>tcb. f tcb = v) t s \<Longrightarrow> (?P2 and tcb_at' t) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P2\<rbrace> getObject t \<lbrace>\<lambda>x _. f x = v\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. f tcb = v) t s \<Longrightarrow> (?P2 and tcb_at' t) s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma monadic_rewrite_getThreadState:
  "monadic_rewrite E F (obj_at' (\<lambda>tcb. tcbState tcb = v) t)
    (getThreadState t) (return v)" unfolding getThreadState_def by (rule monadic_rewrite_threadGet)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite E F (obj_at' (\<lambda>tcb. tcbState tcb = v) t) (getThreadState t) (return v) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite E F (obj_at' (\<lambda>tcb. tcbState tcb = v) t) (threadGet tcbState t) (return v)
theory Fastpath_Equiv

lemma setCTE_obj_at'_tcbIPCBuffer:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t\<rbrace>" unfolding setCTE_def by (rule setObject_cte_obj_at_tcb', simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t\<rbrace> setObject p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbIPCBuffer tcb)) t\<rbrace>
theory Fastpath_Equiv

lemma setThreadState_runnable_bitmap_inv:
  "runnable' ts \<Longrightarrow>
    \<lbrace> \<lambda>s. P (ksReadyQueuesL1Bitmap s) \<rbrace> setThreadState ts t \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s) \<rbrace>"
  "runnable' ts \<Longrightarrow>
    \<lbrace> \<lambda>s. Q (ksReadyQueuesL2Bitmap s) \<rbrace> setThreadState ts t \<lbrace>\<lambda>rv s. Q (ksReadyQueuesL2Bitmap s) \<rbrace>" by (simp_all add: setThreadState_runnable_simp, wp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (runnable' ts \<Longrightarrow> \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> setThreadState ts t \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>) &&& (runnable' ts \<Longrightarrow> \<lbrace>\<lambda>s. Q (ksReadyQueuesL2Bitmap s)\<rbrace> setThreadState ts t \<lbrace>\<lambda>rv s. Q (ksReadyQueuesL2Bitmap s)\<rbrace>)
theory Fastpath_Equiv

lemma capability_case_Null_ReplyCap:
  "(case cap of NullCap \<Rightarrow> f | ReplyCap t b cg \<Rightarrow> g t b cg | _ \<Rightarrow> h)
     = (if isReplyCap cap then g (capTCBPtr cap) (capReplyMaster cap) (capReplyCanGrant cap)
             else if isNullCap cap then f else h)" by (simp add: isCap_simps split: capability.split split del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.NullCap \<Rightarrow> f | capability.ReplyCap t b cg \<Rightarrow> g t b cg | _ \<Rightarrow> h) = (if isReplyCap cap then g (capTCBPtr cap) (capReplyMaster cap) (capReplyCanGrant cap) else if isNullCap cap then f else h)
theory Fastpath_Equiv

lemma injection_handler_catch:
  "catch (injection_handler f x) y
      = catch x (y o f)" apply (simp add: injection_handler_def catch_def handleE'_def
                   bind_assoc) apply (rule bind_cong[OF refl]) apply (simp add: throwError_bind split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (injection_handler f x <catch> y) = (x <catch> y \<circ> f) proof (prove)
goal (1 subgoal):
 1. do x <- x;
ya <- case x of Inl e \<Rightarrow> throwError (f e) | Inr v' \<Rightarrow> return (Inr v');
case ya of Inl x \<Rightarrow> y x | Inr x \<Rightarrow> return x
od = do x <- x;
case x of Inl e \<Rightarrow> (y \<circ> f) e | Inr b \<Rightarrow> return b
od proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. (v, s') \<in> fst (x s) \<Longrightarrow> (do ya <- case v of Inl e \<Rightarrow> throwError (f e) | Inr v' \<Rightarrow> return (Inr v');
case ya of Inl x \<Rightarrow> y x | Inr x \<Rightarrow> return x
od) s' = (case v of Inl e \<Rightarrow> (y \<circ> f) e | Inr b \<Rightarrow> return b) s' proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma empty_fail_isFinalCapability:
  "empty_fail (isFinalCapability cte)" by (simp add: isFinalCapability_def Let_def empty_fail_cond split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (isFinalCapability cte)
theory Fastpath_Equiv

lemma cteDeleteOne_nullcap_rewrite:
  "monadic_rewrite True False
     (cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) slot)
     (cteDeleteOne slot)
     (return ())" apply (simp add: cteDeleteOne_def unless_def when_def) apply (monadic_rewrite_l monadic_rewrite_if_l_False \<open>wpsimp wp: getCTE_wp'\<close>) apply (monadic_rewrite_symb_exec_l, rule monadic_rewrite_refl) apply (wpsimp wp: getCTE_wp' simp: cte_wp_at_ctes_of)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot) (cteDeleteOne slot) (return ()) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot) (do cte <- getCTE slot;
if cteCap cte \<noteq> capability.NullCap then do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od else return ()
od) (return ()) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True False ?Q1 (do cte <- getCTE slot;
return ()
od) (return ())
 2. \<And>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s \<Longrightarrow> ((\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> ((\<lambda>_. \<not> cteCap cte \<noteq> capability.NullCap) and (\<lambda>_. True)) s) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> getCTE slot \<lbrace>\<lambda>cte _. True\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) slot s \<Longrightarrow> ((\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> ((\<lambda>_. \<not> cteCap cte \<noteq> capability.NullCap) and (\<lambda>_. True)) s) and ?Q1) s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma deleteCallerCap_nullcap_rewrite:
  "monadic_rewrite True False
     (cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) (thread + 2 ^ cte_level_bits * tcbCallerSlot))
     (deleteCallerCap thread)
     (return ())" apply (simp add: deleteCallerCap_def getThreadCallerSlot_def locateSlot_conv
                   getSlotCap_def) apply (monadic_rewrite_l cteDeleteOne_nullcap_rewrite \<open>wpsimp wp: getCTE_wp\<close>) apply (monadic_rewrite_symb_exec_l+, rule monadic_rewrite_refl) apply (wpsimp simp: cte_wp_at_ctes_of)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (thread + 2 ^ cte_level_bits * tcbCallerSlot)) (deleteCallerCap thread) (return ()) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (thread + 2 ^ cte_level_bits * tcbCallerSlot)) (do cte <- getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (isReplyCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (thread + 2 ^ cte_level_bits * tcbCallerSlot)
od) (return ()) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True False ?Q2 (do x <- getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (isReplyCap (cteCap x) \<or> cteCap x = capability.NullCap);
return ()
od) (return ())
 2. \<And>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (thread + 2 ^ cte_level_bits * tcbCallerSlot) s \<Longrightarrow> ((\<lambda>s. cte_wp_at' (\<lambda>_. True) (thread + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (thread + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (isReplyCap (cteCap cte) \<or> cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (thread + 2 ^ cte_level_bits * tcbCallerSlot) s))) and ?Q2) s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?Q33 x\<rbrace> assert (isReplyCap (cteCap x) \<or> cteCap x = capability.NullCap) \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<lbrace>?Q2\<rbrace> getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q33\<rbrace>
 3. \<And>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (thread + 2 ^ cte_level_bits * tcbCallerSlot) s \<Longrightarrow> ((\<lambda>s. cte_wp_at' (\<lambda>_. True) (thread + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (thread + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (isReplyCap (cteCap cte) \<or> cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) (thread + 2 ^ cte_level_bits * tcbCallerSlot) s))) and ?Q2) s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma emptySlot_cnode_caps:
  "\<lbrace>\<lambda>s. P (only_cnode_caps (ctes_of s)) \<and> cte_wp_at' (\<lambda>cte. \<not> isCNodeCap (cteCap cte)) slot s\<rbrace>
     emptySlot slot NullCap
   \<lbrace>\<lambda>rv s. P (only_cnode_caps (ctes_of s))\<rbrace>" apply (simp add: only_cnode_caps_def map_option_comp2
                   o_assoc[symmetric] cteCaps_of_def[symmetric]) apply (wp emptySlot_cteCaps_of) apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of
                 elim!: rsubst[where P=P] del: ext intro!: ext
                 split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (only_cnode_caps (ctes_of s)) \<and> cte_wp_at' (\<lambda>cte. \<not> isCNodeCap (cteCap cte)) slot s\<rbrace> emptySlot slot capability.NullCap \<lbrace>\<lambda>rv s. P (only_cnode_caps (ctes_of s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (map_option (\<lambda>x. if isCNodeCap x then x else capability.NullCap) \<circ> cteCaps_of s) \<and> cte_wp_at' (\<lambda>cte. \<not> isCNodeCap (cteCap cte)) slot s\<rbrace> emptySlot slot capability.NullCap \<lbrace>\<lambda>rv s. P (map_option (\<lambda>x. if isCNodeCap x then x else capability.NullCap) \<circ> cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (map_option (\<lambda>x. if isCNodeCap x then x else capability.NullCap) \<circ> cteCaps_of s) \<and> cte_wp_at' (\<lambda>cte. \<not> isCNodeCap (cteCap cte)) slot s \<Longrightarrow> P (map_option (\<lambda>x. if isCNodeCap x then x else capability.NullCap) \<circ> (cteCaps_of s)(slot \<mapsto> capability.NullCap)) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma asUser_obj_at_ep[wp]:
  "\<lbrace>obj_at' P p\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' (P :: endpoint \<Rightarrow> bool) 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' P p\<rbrace> asUser t m \<lbrace>\<lambda>rv. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P 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' P p\<rbrace> proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma setCTE_obj_at_ep[wp]:
  "\<lbrace>obj_at' (P :: endpoint \<Rightarrow> bool) p\<rbrace> setCTE ptr cte \<lbrace>\<lambda>rv. obj_at' P p\<rbrace>" unfolding setCTE_def apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_cte typeError_def in_monad
                 split: Structures_H.kernel_object.split_asm
                        if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P p\<rbrace> setCTE ptr cte \<lbrace>\<lambda>rv. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P p\<rbrace> setObject ptr cte \<lbrace>\<lambda>rv. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.endpoint) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma setCTE_obj_at_ntfn[wp]:
  "\<lbrace>obj_at' (P :: Structures_H.notification \<Rightarrow> bool) p\<rbrace> setCTE ptr cte \<lbrace>\<lambda>rv. obj_at' P p\<rbrace>" unfolding setCTE_def apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_cte typeError_def in_monad
                 split: Structures_H.kernel_object.split_asm
                        if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P p\<rbrace> setCTE ptr cte \<lbrace>\<lambda>rv. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P p\<rbrace> setObject ptr cte \<lbrace>\<lambda>rv. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.notification) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma tcbSchedDequeue_rewrite_not_queued:
  "monadic_rewrite True False (tcb_at' t and obj_at' (Not \<circ> tcbQueued) t)
     (tcbSchedDequeue t) (return ())" apply (simp add: tcbSchedDequeue_def when_def) apply (monadic_rewrite_l monadic_rewrite_if_l_False \<open>wp threadGet_const\<close>) apply (monadic_rewrite_symb_exec_l, rule monadic_rewrite_refl) apply wp+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (tcb_at' t and obj_at' (Not \<circ> tcbQueued) t) (tcbSchedDequeue t) (return ()) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (tcb_at' t and obj_at' (Not \<circ> tcbQueued) t) (do queued <- threadGet tcbQueued t;
if queued then do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- if null (filter (\<lambda>x. x \<noteq> t) queue) then removeFromBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. False)) t
od else return ()
od) (return ()) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True False ?Q1 (do queued <- threadGet tcbQueued t;
return ()
od) (return ())
 2. \<And>s. (tcb_at' t and obj_at' (Not \<circ> tcbQueued) t) s \<Longrightarrow> ((\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' ((\<lambda>rv. \<not> rv \<and> True) \<circ> tcbQueued) t s) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued _. True\<rbrace>
 2. \<And>s. (tcb_at' t and obj_at' (Not \<circ> tcbQueued) t) s \<Longrightarrow> ((\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' ((\<lambda>rv. \<not> rv \<and> True) \<circ> tcbQueued) t s) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' t and obj_at' (Not \<circ> tcbQueued) t) s \<Longrightarrow> ((\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' ((\<lambda>rv. \<not> rv \<and> True) \<circ> tcbQueued) t s) and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma tcb_at_cte_at_offset:
  "\<lbrakk> tcb_at' t s; 2 ^ cte_level_bits * off \<in> dom tcb_cte_cases \<rbrakk>
    \<Longrightarrow> cte_at' (t + 2 ^ cte_level_bits * off) s" apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (erule(2) cte_wp_at_tcbI') apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at' t s; 2 ^ cte_level_bits * off \<in> dom tcb_cte_cases\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (t + 2 ^ cte_level_bits * off) s proof (prove)
goal (1 subgoal):
 1. \<And>a b obj. \<lbrakk>tcb_cte_cases (2 ^ cte_level_bits * off) = Some (a, b); ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (t + 2 ^ cte_level_bits * off) s proof (prove)
goal (2 subgoals):
 1. \<And>a b obj. \<lbrakk>tcb_cte_cases (2 ^ cte_level_bits * off) = Some (a, b); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (t + 2 ^ cte_level_bits * off - t) = Some (?getF9 a b obj, ?setF9 a b obj)
 2. \<And>a b obj. \<lbrakk>tcb_cte_cases (2 ^ cte_level_bits * off) = Some (a, b); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (1 subgoal):
 1. \<And>a b obj. \<lbrakk>tcb_cte_cases (2 ^ cte_level_bits * off) = Some (a, b); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma emptySlot_cte_wp_at_cteCap:
  "\<lbrace>\<lambda>s. (p = p' \<longrightarrow> P NullCap) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s)\<rbrace>
     emptySlot p' irqopt
   \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>" apply (simp add: tree_cte_cteCap_eq[unfolded o_def]) apply (wp emptySlot_cteCaps_of) apply (clarsimp split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (p = p' \<longrightarrow> P capability.NullCap) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s)\<rbrace> emptySlot p' irqopt \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (p = p' \<longrightarrow> P capability.NullCap) \<and> (p \<noteq> p' \<longrightarrow> (case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2))\<rbrace> emptySlot p' irqopt \<lbrace>\<lambda>rv s. case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (p = p' \<longrightarrow> P capability.NullCap) \<and> (p \<noteq> p' \<longrightarrow> (case cteCaps_of s p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2)) \<Longrightarrow> case ((cteCaps_of s)(p' \<mapsto> capability.NullCap)) p of None \<Rightarrow> False | Some x2 \<Rightarrow> P x2 proof (prove)
goal:
No subgoals!