kings-crown/FVELER_Isabelle huggingface dataset:
theory Fastpath_Equiv

lemma valid_cnode_cap_cte_at':
  "\<lbrakk> s \<turnstile>' c; isCNodeCap c; ptr = capCNodePtr c; v < 2 ^ capCNodeBits c \<rbrakk>
      \<Longrightarrow> cte_at' (ptr + v * 2^cteSizeBits) s" apply (drule less_mask_eq) apply (drule(1) valid_cap_cte_at'[where addr=v]) apply (simp add: mult.commute mult.left_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' c s; isCNodeCap c; ptr = capCNodePtr c; v < 2 ^ capCNodeBits c\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (ptr + v * 2 ^ cteSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' c s; isCNodeCap c; ptr = capCNodePtr c; v && mask (capCNodeBits c) = v\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (ptr + v * 2 ^ cteSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' c s; ptr = capCNodePtr c; v && mask (capCNodeBits c) = v; cte_wp_at' (\<lambda>_. True) (capCNodePtr c + 2 ^ cteSizeBits * (v && mask (capCNodeBits c))) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (ptr + v * 2 ^ cteSizeBits) s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma of_bl_from_bool:
  "of_bl [x] = from_bool x" by (cases x, simp_all add: from_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bl [x] = from_bool x
theory Fastpath_Equiv

lemma dmo_clearExMonitor_setCurThread_swap:
  "(do _ \<leftarrow> doMachineOp ARM.clearExMonitor;
               setCurThread thread
            od)
    = (do _ \<leftarrow> setCurThread thread;
            doMachineOp ARM.clearExMonitor od)" apply (simp add: setCurThread_def doMachineOp_def split_def) apply (rule oblivious_modify_swap[symmetric]) apply (intro oblivious_bind, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- doMachineOp ARM.clearExMonitor;
setCurThread thread
od = do _ <- setCurThread thread;
doMachineOp ARM.clearExMonitor
od proof (prove)
goal (1 subgoal):
 1. do _ <- do ms <- gets ksMachineState;
p <- select_f (ARM.clearExMonitor ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od;
modify (ksCurThread_update (\<lambda>_. thread))
od = do _ <- modify (ksCurThread_update (\<lambda>_. thread));
ms <- gets ksMachineState;
p <- select_f (ARM.clearExMonitor ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od proof (prove)
goal (1 subgoal):
 1. oblivious (ksCurThread_update (\<lambda>_. thread)) (do ms <- gets ksMachineState;
p <- select_f (ARM.clearExMonitor ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma pd_at_asid_inj':
  "pd_at_asid' pd asid s \<Longrightarrow> pd_at_asid' pd' asid s \<Longrightarrow> pd' = pd" by (clarsimp simp: pd_at_asid'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd_at_asid' pd asid s; pd_at_asid' pd' asid s\<rbrakk> \<Longrightarrow> pd' = pd
theory Fastpath_Equiv

lemma bind_case_sum_rethrow:
  "rethrowFailure fl f >>= case_sum e g
     = f >>= case_sum (e \<circ> fl) g" apply (simp add: rethrowFailure_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. rethrowFailure fl f >>= case_sum e g = f >>= case_sum (e \<circ> fl) g proof (prove)
goal (1 subgoal):
 1. do x <- f;
y <- case x of Inl x \<Rightarrow> (throwError \<circ> fl) x | Inr v' \<Rightarrow> return (Inr v');
case y of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> g x
od = f >>= case_sum (e \<circ> fl) g proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. (v, s') \<in> fst (f s) \<Longrightarrow> (do y <- case v of Inl x \<Rightarrow> (throwError \<circ> fl) x | Inr v' \<Rightarrow> return (Inr v');
case y of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> g x
od) s' = (case v of Inl x \<Rightarrow> (e \<circ> fl) x | Inr x \<Rightarrow> g x) s' proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma lookupExtraCaps_null:
  "msgExtraCaps info = 0 \<Longrightarrow>
     lookupExtraCaps thread buffer info = returnOk []" by (clarsimp simp: lookupExtraCaps_def
                     getExtraCPtrs_def liftE_bindE
                     upto_enum_step_def mapM_Nil
              split: Types_H.message_info.split option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msgExtraCaps info = 0 \<Longrightarrow> lookupExtraCaps thread buffer info = returnOk []
theory Fastpath_Equiv

lemma isRecvEP_endpoint_case:
  "isRecvEP ep \<Longrightarrow> case_endpoint f g h ep = f (epQueue ep)" by (clarsimp simp: isRecvEP_def split: endpoint.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isRecvEP ep \<Longrightarrow> (case ep of Structures_H.endpoint.RecvEP x \<Rightarrow> f x | Structures_H.endpoint.IdleEP \<Rightarrow> g | Structures_H.endpoint.SendEP x \<Rightarrow> h x) = f (epQueue ep)
theory Fastpath_Equiv

lemma unifyFailure_catch_If:
  "catch (unifyFailure f >>=E g) h
     = f >>= (\<lambda>rv. if isRight rv then catch (g (theRight rv)) h else h ())" apply (simp add: unifyFailure_def rethrowFailure_def
                   handleE'_def catch_def bind_assoc
                   bind_bindE_assoc cong: if_cong) apply (rule bind_cong[OF refl]) apply (simp add: throwError_bind isRight_def return_returnOk
            split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (unifyFailure f >>=E g <catch> h) = do rv <- f;
if isRight rv then g (theRight rv) <catch> h else h ()
od proof (prove)
goal (1 subgoal):
 1. do rv <- f;
y <- (case rv of Inl x \<Rightarrow> (throwError \<circ> const ()) x | Inr v' \<Rightarrow> return (Inr v')) >>=E g;
case y of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x
od = do rv <- f;
if isRight rv then do x <- g (theRight rv);
case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b
od else h ()
od proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. (v, s') \<in> fst (f s) \<Longrightarrow> (do y <- (case v of Inl x \<Rightarrow> (throwError \<circ> const ()) x | Inr v' \<Rightarrow> return (Inr v')) >>=E g;
case y of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x
od) s' = (if isRight v then do x <- g (theRight v);
case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b
od else h ()) s' proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma st_tcb_at_not_in_ep_queue:
  "\<lbrakk> st_tcb_at' P t s; ko_at' ep epptr s; sym_refs (state_refs_of' s);
     ep \<noteq> IdleEP; \<And>ts. P ts \<Longrightarrow> tcb_st_refs_of' ts = {} \<rbrakk>
      \<Longrightarrow> t \<notin> set (epQueue ep)" apply clarsimp apply (drule(1) sym_refs_ko_atD') apply (cases ep, simp_all add: st_tcb_at_refs_of_rev') apply (fastforce simp: st_tcb_at'_def obj_at'_def projectKOs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; ko_at' ep epptr s; sym_refs (state_refs_of' s); ep \<noteq> Structures_H.endpoint.IdleEP; \<And>ts. P ts \<Longrightarrow> tcb_st_refs_of' ts = {}\<rbrakk> \<Longrightarrow> t \<notin> set (epQueue ep) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; ko_at' ep epptr s; sym_refs (state_refs_of' s); ep \<noteq> Structures_H.endpoint.IdleEP; \<And>ts. P ts \<Longrightarrow> tcb_st_refs_of' ts = {}; t \<in> set (epQueue ep)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; sym_refs (state_refs_of' s); ep \<noteq> Structures_H.endpoint.IdleEP; \<And>ts. P ts \<Longrightarrow> tcb_st_refs_of' ts = {}; t \<in> set (epQueue ep); state_refs_of' s epptr = refs_of' (injectKOS ep) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ep). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>st_tcb_at' P t s; sym_refs (state_refs_of' s); \<And>ts. P ts \<Longrightarrow> tcb_st_refs_of' ts = {}; t \<in> set x1; state_refs_of' s epptr = set x1 \<times> {EPRecv} \<and> (\<forall>x\<in>set x1. st_tcb_at' (\<lambda>ts. \<exists>a. ts = Structures_H.thread_state.BlockedOnReceive epptr a) x s); ep = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> False
 2. \<And>x3. \<lbrakk>st_tcb_at' P t s; sym_refs (state_refs_of' s); \<And>ts. P ts \<Longrightarrow> tcb_st_refs_of' ts = {}; t \<in> set x3; state_refs_of' s epptr = set x3 \<times> {EPSend} \<and> (\<forall>x\<in>set x3. st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s); ep = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma st_tcb_at_not_in_ntfn_queue:
  "\<lbrakk> st_tcb_at' P t s; ko_at' ntfn ntfnptr s; sym_refs (state_refs_of' s); ntfnObj ntfn = WaitingNtfn xs;
     \<And>ts. P ts \<Longrightarrow> (ntfnptr, TCBSignal) \<notin> tcb_st_refs_of' ts \<rbrakk>
      \<Longrightarrow> t \<notin> set xs" apply (drule(1) sym_refs_ko_atD') apply (clarsimp simp: st_tcb_at_refs_of_rev') apply (drule_tac x="(t, NTFNSignal)" in bspec, simp) apply (fastforce simp: st_tcb_at'_def obj_at'_def projectKOs ko_wp_at'_def tcb_bound_refs'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; ko_at' ntfn ntfnptr s; sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn xs; \<And>ts. P ts \<Longrightarrow> (ntfnptr, TCBSignal) \<notin> tcb_st_refs_of' ts\<rbrakk> \<Longrightarrow> t \<notin> set xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn xs; \<And>ts. P ts \<Longrightarrow> (ntfnptr, TCBSignal) \<notin> tcb_st_refs_of' ts; state_refs_of' s ntfnptr = refs_of' (injectKOS ntfn) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ntfn). ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> t \<notin> set xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn xs; \<And>ts. P ts \<Longrightarrow> (ntfnptr, TCBSignal) \<notin> tcb_st_refs_of' ts; state_refs_of' s ntfnptr = set xs \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); \<forall>x\<in>set xs \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn). case x of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s; t \<in> set xs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P t s; sym_refs (state_refs_of' s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn xs; \<And>ts. P ts \<Longrightarrow> (ntfnptr, TCBSignal) \<notin> tcb_st_refs_of' ts; state_refs_of' s ntfnptr = set xs \<times> {NTFNSignal} \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn); t \<in> set xs; case (t, NTFNSignal) of (x, tp) \<Rightarrow> ko_wp_at' (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma updateCap_cte_wp_at_cteMDBNode:
  "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteMDBNode cte)) p\<rbrace>
     updateCap ptr cap
   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteMDBNode cte)) p\<rbrace>" apply (wp updateCap_cte_wp_at_cases) apply (simp add: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteMDBNode cte)) p\<rbrace> updateCap ptr cap \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteMDBNode cte)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>cte. P (cteMDBNode cte)) p s \<Longrightarrow> (ptr = p \<longrightarrow> cte_wp_at' ((\<lambda>cte. P (cteMDBNode cte)) \<circ> cteCap_update (K cap)) p s) \<and> (ptr \<noteq> p \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteMDBNode cte)) p s) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma ctes_of_Some_cte_wp_at:
  "ctes_of s p = Some cte \<Longrightarrow> cte_wp_at' P p s = P cte" by (clarsimp simp: cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s p = Some cte \<Longrightarrow> cte_wp_at' P p s = P cte
theory Fastpath_Equiv

lemma setUntypedCapAsFull_replyCap[simp]:
  "setUntypedCapAsFull cap (ReplyCap curThread False cg) slot =  return ()" by (clarsimp simp:setUntypedCapAsFull_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setUntypedCapAsFull cap (capability.ReplyCap curThread False cg) slot = return ()
theory Fastpath_Equiv

lemma option_case_liftM_getNotification_wp:
  "\<lbrace>\<lambda>s. \<forall>rv. (case x of None \<Rightarrow> rv = v | Some p \<Rightarrow> obj_at' (\<lambda>ntfn. f ntfn = rv) p s)
    \<longrightarrow> Q rv s\<rbrace> case x of None \<Rightarrow> return v | Some ptr \<Rightarrow> liftM f $ getNotification ptr \<lbrace> Q \<rbrace>" apply (rule hoare_pre, (wpc; wp getNotification_wp)) apply (auto simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>rv. (case x of None \<Rightarrow> rv = v | Some p \<Rightarrow> obj_at' (\<lambda>ntfn. f ntfn = rv) p s) \<longrightarrow> Q rv s\<rbrace> case x of None \<Rightarrow> return v | Some ptr \<Rightarrow> liftM f $ getNotification ptr \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>rv. (case x of None \<Rightarrow> rv = v | Some p \<Rightarrow> obj_at' (\<lambda>ntfn. f ntfn = rv) p s) \<longrightarrow> Q rv s \<Longrightarrow> (x = None \<longrightarrow> Q v s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (\<forall>ntfn. ko_at' ntfn xa s \<longrightarrow> (Q \<circ> f) ntfn s)) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma threadSet_st_tcb_at_state:
  "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (if p = t
        then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s
        else st_tcb_at' P p s)\<rbrace>
  threadSet f t \<lbrace>\<lambda>_. st_tcb_at' P p\<rbrace>" apply (rule hoare_chain) apply (rule threadSet_obj_at'_really_strongest) prefer 2 apply (simp add: st_tcb_at'_def) apply (clarsimp split: if_splits simp: st_tcb_at'_def o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s)\<rbrace> threadSet f t \<lbrace>\<lambda>_. st_tcb_at' P p\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> threadSet f t \<lbrace>?Q\<rbrace>
 2. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s) \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> st_tcb_at' P p s proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = ?t'4 then ?P4 (f obj) else ?P4 obj) ?t'4 s
 2. \<And>rv s. obj_at' ?P4 ?t'4 s \<Longrightarrow> st_tcb_at' P p s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. obj_at' ?P4 ?t'4 s \<Longrightarrow> st_tcb_at' P p s
 2. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = ?t'4 then ?P4 (f obj) else ?P4 obj) ?t'4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = p then (P \<circ> tcbState) (f obj) else (P \<circ> tcbState) obj) p s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma recv_ep_queued_st_tcb_at':
  "\<lbrakk> ko_at' (Structures_H.endpoint.RecvEP ts) epptr s ;
     t \<in> set ts;
     sym_refs (state_refs_of' s) \<rbrakk>
   \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s" apply (drule obj_at_ko_at') apply clarsimp apply (drule (1) sym_refs_ko_atD') apply (clarsimp simp: pred_tcb_at'_def obj_at'_real_def refs_of_rev') apply (erule_tac x=t in ballE; clarsimp?) apply (erule ko_wp_at'_weakenE) apply (clarsimp simp: isBlockedOnReceive_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' (Structures_H.endpoint.RecvEP ts) epptr s; t \<in> set ts; sym_refs (state_refs_of' s)\<rbrakk> \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); \<exists>ko. ko_at' ko epptr s \<and> ko = Structures_H.endpoint.RecvEP ts\<rbrakk> \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); ko_at' (Structures_H.endpoint.RecvEP ts) epptr s\<rbrakk> \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); state_refs_of' s epptr = refs_of' (injectKOS (Structures_H.endpoint.RecvEP ts)) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS (Structures_H.endpoint.RecvEP ts)). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); state_refs_of' s epptr = set ts \<times> {EPRecv}; \<forall>x\<in>set ts. ko_wp_at' (\<lambda>ko. \<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = Structures_H.thread_state.BlockedOnReceive epptr a)) x s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> isBlockedOnReceive (tcbState obj)) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); state_refs_of' s epptr = set ts \<times> {EPRecv}; ko_wp_at' (\<lambda>ko. \<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = Structures_H.thread_state.BlockedOnReceive epptr a)) t s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> isBlockedOnReceive (tcbState obj)) t s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); state_refs_of' s epptr = set ts \<times> {EPRecv}; \<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = Structures_H.thread_state.BlockedOnReceive epptr a)\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj \<and> isBlockedOnReceive (tcbState obj) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma valid_ep_typ_at_lift':
  "\<lbrakk> \<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace> \<rbrakk>
      \<Longrightarrow> \<lbrace>\<lambda>s. valid_ep' ep s\<rbrace> f \<lbrace>\<lambda>rv s. valid_ep' ep s\<rbrace>" apply (cases ep, simp_all add: valid_ep'_def) apply (wp hoare_vcg_const_Ball_lift typ_at_lifts | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace>) \<Longrightarrow> \<lbrace>valid_ep' ep\<rbrace> f \<lbrace>\<lambda>rv. valid_ep' ep\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>\<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace>; ep = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. x1 \<noteq> [] \<and> (\<forall>t\<in>set x1. tcb_at' t s) \<and> distinct x1\<rbrace> f \<lbrace>\<lambda>rv s. x1 \<noteq> [] \<and> (\<forall>t\<in>set x1. tcb_at' t s) \<and> distinct x1\<rbrace>
 2. \<lbrakk>\<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace>; ep = Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace>
 3. \<And>x3. \<lbrakk>\<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace>; ep = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3\<rbrace> f \<lbrace>\<lambda>rv s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3\<rbrace> proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma threadSet_tcbState_valid_objs:
  "\<lbrace>valid_tcb_state' st and valid_objs'\<rbrace>
     threadSet (tcbState_update (\<lambda>_. st)) t
   \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (wp threadSet_valid_objs') apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_tcb_state' st and valid_objs'\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_tcb_state' st and valid_objs') s \<Longrightarrow> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. st) tcb) s)) s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma scheduleSwitchThreadFastfail_False_wp:
  "\<lbrace>\<lambda>s. ct \<noteq> it \<and> cprio \<le> tprio \<rbrace>
   scheduleSwitchThreadFastfail ct it cprio tprio
   \<lbrace>\<lambda>rv s. \<not> rv \<rbrace>" unfolding scheduleSwitchThreadFastfail_def by (wp threadGet_wp)
     (auto dest!: obj_at_ko_at' simp: le_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct \<noteq> it \<and> cprio \<le> tprio\<rbrace> scheduleSwitchThreadFastfail ct it cprio tprio \<lbrace>\<lambda>rv s. \<not> rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct \<noteq> it \<and> cprio \<le> tprio\<rbrace> if ct \<noteq> it then return (tprio < cprio) else return True \<lbrace>\<lambda>rv s. \<not> rv\<rbrace>
theory Fastpath_Equiv

lemma lookupBitmapPriority_lift:
  assumes prqL1: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>"
  and     prqL2: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>"
  shows   "\<lbrace>\<lambda>s. P (lookupBitmapPriority d s) \<rbrace> f \<lbrace>\<lambda>_ s. P (lookupBitmapPriority d s) \<rbrace>" unfolding lookupBitmapPriority_def apply (rule hoare_pre) apply (wps prqL1 prqL2) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (lookupBitmapPriority d s)\<rbrace> f \<lbrace>\<lambda>_ s. P (lookupBitmapPriority d s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))\<rbrace> f \<lbrace>\<lambda>_ s. P (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>_ s. P (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))))))\<rbrace>
 2. \<And>s. P (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. P (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap prev_s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap prev_s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap prev_s d))))))\<rbrace>
 2. \<And>s. P (l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) || word_of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))) \<Longrightarrow> ?P3 s s proof (prove)
goal:
No subgoals!