kings-crown/FVELER_Isabelle huggingface dataset:
theory Fastpath_Equiv

lemma setEndpoint_getCTE_pivot[unfolded K_bind_def]:
  "do setEndpoint p val; v <- getCTE slot; f v od
     = do v <- getCTE slot; setEndpoint p val; f v od" apply (simp add: getCTE_assert_opt setEndpoint_def
                   setObject_modify_assert
                   fun_eq_iff bind_assoc) apply (simp add: exec_gets assert_def assert_opt_def
                   exec_modify update_ep_map_to_ctes
            split: if_split option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do setEndpoint p val;
getCTE slot >>= f
od = do v <- getCTE slot;
setEndpoint p val;
f v
od proof (prove)
goal (1 subgoal):
 1. \<forall>x. (do fa <- gets (ep_at' p);
y <- assert fa;
y <- modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint val)));
x <- gets (\<lambda>s. ctes_of s slot);
assert_opt x >>= f
od) x = (do x <- gets (\<lambda>s. ctes_of s slot);
v <- assert_opt x;
fa <- gets (ep_at' p);
y <- assert fa;
y <- modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint val)));
f v
od) x proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma setEndpoint_updateMDB_pivot[unfolded K_bind_def]:
  "do setEndpoint p val; updateMDB slot mf; f od =
     do updateMDB slot mf; setEndpoint p val; f od" by (clarsimp simp: updateMDB_def bind_assoc
                     setEndpoint_getCTE_pivot
                     setEndpoint_setCTE_pivot
              split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do setEndpoint p val;
updateMDB slot mf;
f
od = do updateMDB slot mf;
setEndpoint p val;
f
od
theory Fastpath_Equiv

lemma modify_setEndpoint_pivot[unfolded K_bind_def]:
  "\<lbrakk> \<And>ksf s. ksPSpace_update ksf (sf s) = sf (ksPSpace_update ksf s) \<rbrakk>
    \<Longrightarrow> (do modify sf; setEndpoint p val; f od) =
          (do setEndpoint p val; modify sf; f od)" apply (subgoal_tac "\<forall>s. ep_at' p (sf s) = ep_at' p s") apply (simp add: setEndpoint_def setObject_modify_assert
                    bind_assoc fun_eq_iff
                    exec_gets exec_modify assert_def
             split: if_split) apply atomize apply clarsimp apply (drule_tac x="\<lambda>_. ksPSpace s" in spec) apply (drule_tac x="s" in spec) apply (drule_tac f="ksPSpace" in arg_cong) apply simp apply (metis obj_at'_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>ksf s. ksPSpace_update ksf (sf s) = sf (ksPSpace_update ksf s)) \<Longrightarrow> do modify sf;
setEndpoint p val;
f
od = do setEndpoint p val;
modify sf;
f
od proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>ksf s. ksPSpace_update ksf (sf s) = sf (ksPSpace_update ksf s); \<forall>s. ep_at' p (sf s) = ep_at' p s\<rbrakk> \<Longrightarrow> do modify sf;
setEndpoint p val;
f
od = do setEndpoint p val;
modify sf;
f
od
 2. (\<And>ksf s. ksPSpace_update ksf (sf s) = sf (ksPSpace_update ksf s)) \<Longrightarrow> \<forall>s. ep_at' p (sf s) = ep_at' p s proof (prove)
goal (1 subgoal):
 1. (\<And>ksf s. ksPSpace_update ksf (sf s) = sf (ksPSpace_update ksf s)) \<Longrightarrow> \<forall>s. ep_at' p (sf s) = ep_at' p s proof (prove)
goal (1 subgoal):
 1. \<forall>ksf s. ksPSpace_update ksf (sf s) = sf (ksPSpace_update ksf s) \<Longrightarrow> \<forall>s. ep_at' p (sf s) = ep_at' p s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>ksf s. ksPSpace_update ksf (sf s) = sf (ksPSpace_update ksf s) \<Longrightarrow> ep_at' p (sf s) = ep_at' p s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>sa. sf sa\<lparr>ksPSpace := ksPSpace s\<rparr> = sf (sa\<lparr>ksPSpace := ksPSpace s\<rparr>) \<Longrightarrow> ep_at' p (sf s) = ep_at' p s proof (prove)
goal (1 subgoal):
 1. \<And>s. sf s\<lparr>ksPSpace := ksPSpace s\<rparr> = sf (s\<lparr>ksPSpace := ksPSpace s\<rparr>) \<Longrightarrow> ep_at' p (sf s) = ep_at' p s proof (prove)
goal (1 subgoal):
 1. \<And>s. ksPSpace (sf s\<lparr>ksPSpace := ksPSpace s\<rparr>) = ksPSpace (sf (s\<lparr>ksPSpace := ksPSpace s\<rparr>)) \<Longrightarrow> ep_at' p (sf s) = ep_at' p s proof (prove)
goal (1 subgoal):
 1. \<And>s. ksPSpace s = ksPSpace (sf s) \<Longrightarrow> ep_at' p (sf s) = ep_at' p s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma setEndpoint_clearUntypedFreeIndex_pivot[unfolded K_bind_def]:
  "do setEndpoint p val; v <- clearUntypedFreeIndex slot; f od
     = do v <- clearUntypedFreeIndex slot; setEndpoint p val; f od" supply option.case_cong_weak[cong del] by (simp add: clearUntypedFreeIndex_def bind_assoc getSlotCap_def setEndpoint_getCTE_pivot
                updateTrackedFreeIndex_def modify_setEndpoint_pivot
         split: capability.split
      | rule bind_cong[OF refl] allI impI bind_apply_cong[OF refl])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do setEndpoint p val;
v <- clearUntypedFreeIndex slot;
f
od = do v <- clearUntypedFreeIndex slot;
setEndpoint p val;
f
od proof (prove)
goal (1 subgoal):
 1. do setEndpoint p val;
v <- clearUntypedFreeIndex slot;
f
od = do v <- clearUntypedFreeIndex slot;
setEndpoint p val;
f
od
theory Fastpath_Equiv

lemma emptySlot_setEndpoint_pivot[unfolded K_bind_def]:
  "(do emptySlot slot NullCap; setEndpoint p val; f od) =
      (do setEndpoint p val; emptySlot slot NullCap; f od)" apply (rule ext) apply (simp add: emptySlot_def bind_assoc
                   setEndpoint_getCTE_pivot
                   setEndpoint_updateCap_pivot
                   setEndpoint_updateMDB_pivot
                   case_Null_If Retype_H.postCapDeletion_def
                   setEndpoint_clearUntypedFreeIndex_pivot
            split: if_split
         | rule bind_apply_cong[OF refl])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do emptySlot slot capability.NullCap;
setEndpoint p val;
f
od = do setEndpoint p val;
emptySlot slot capability.NullCap;
f
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do emptySlot slot capability.NullCap;
setEndpoint p val;
f
od) x = (do setEndpoint p val;
emptySlot slot capability.NullCap;
f
od) x proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma set_getCTE[unfolded K_bind_def]:
  "do setCTE p cte; v <- getCTE p; f v od
      = do setCTE p cte; f cte od" apply (simp add: getCTE_assert_opt bind_assoc) apply (rule monadic_rewrite_to_eq) apply (rule monadic_rewrite_bind_tail) apply (monadic_rewrite_symb_exec_l) apply (monadic_rewrite_symb_exec_l_known cte, rule monadic_rewrite_refl) apply (wpsimp simp: assert_opt_def wp: gets_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do setCTE p cte;
getCTE p >>= f
od = do setCTE p cte;
f cte
od proof (prove)
goal (1 subgoal):
 1. do y <- setCTE p cte;
x <- gets (\<lambda>s. ctes_of s p);
assert_opt x >>= f
od = do y <- setCTE p cte;
f cte
od proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False True (\<lambda>_. True) (do y <- setCTE p cte;
x <- gets (\<lambda>s. ctes_of s p);
assert_opt x >>= f
od) (do y <- setCTE p cte;
f cte
od) proof (prove)
goal (2 subgoals):
 1. \<And>y. monadic_rewrite False True (?Q2 y) (do x <- gets (\<lambda>s. ctes_of s p);
assert_opt x >>= f
od) (f cte)
 2. \<lbrace>\<lambda>_. True\<rbrace> setCTE p cte \<lbrace>?Q2\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y x. monadic_rewrite False True (?Q6 y x) (assert_opt x >>= f) (f cte)
 2. \<And>y. \<lbrace>?P6 y\<rbrace> gets (\<lambda>s. ctes_of s p) \<lbrace>?Q6 y\<rbrace>
 3. \<lbrace>\<lambda>_. True\<rbrace> setCTE p cte \<lbrace>\<lambda>y. ?P6 y and (\<lambda>_. True)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y x. \<lbrace>?P44 y x\<rbrace> assert_opt x \<lbrace>\<lambda>rv' s. rv' = cte\<rbrace>
 2. \<And>y. \<lbrace>?P6 y\<rbrace> gets (\<lambda>s. ctes_of s p) \<lbrace>\<lambda>x. ?P44 y x and (\<lambda>_. x \<noteq> None) and (\<lambda>_. True)\<rbrace>
 3. \<lbrace>\<lambda>_. True\<rbrace> setCTE p cte \<lbrace>\<lambda>y. ?P6 y and (\<lambda>_. True)\<rbrace> proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma all_prio_not_inQ_not_tcbQueued: "\<lbrakk> obj_at' (\<lambda>a. (\<forall>d p. \<not> inQ d p a)) t s \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>a. \<not> tcbQueued a) t s" apply (clarsimp simp: obj_at'_def inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (\<lambda>a. \<forall>d p. \<not> inQ d p a) t s \<Longrightarrow> obj_at' (\<lambda>a. \<not> tcbQueued a) t s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma valid_objs_ntfn_at_tcbBoundNotification:
  "ko_at' tcb t s \<Longrightarrow> valid_objs' s \<Longrightarrow> tcbBoundNotification tcb \<noteq> None
   \<Longrightarrow> ntfn_at' (the (tcbBoundNotification tcb)) s" apply (drule(1) ko_at_valid_objs', simp add: projectKOs) apply (simp add: valid_obj'_def valid_tcb'_def valid_bound_ntfn'_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' tcb t s; valid_objs' s; tcbBoundNotification tcb \<noteq> None\<rbrakk> \<Longrightarrow> ntfn_at' (the (tcbBoundNotification tcb)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; tcbBoundNotification tcb \<noteq> None; valid_obj' (injectKOS tcb) s\<rbrakk> \<Longrightarrow> ntfn_at' (the (tcbBoundNotification tcb)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; \<exists>y. tcbBoundNotification tcb = Some y; (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF tcb)) s) \<and> valid_tcb_state' (tcbState tcb) s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrakk> \<Longrightarrow> ntfn_at' (the (tcbBoundNotification tcb)) s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma emptySlot_tcb_at'[wp]:
  "\<lbrace>\<lambda>s. Q (tcb_at' t s)\<rbrace> emptySlot a b \<lbrace>\<lambda>_ s. Q (tcb_at' t s)\<rbrace>" by (simp add: tcb_at_typ_at', wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (tcb_at' t s)\<rbrace> emptySlot a b \<lbrace>\<lambda>_ s. Q (tcb_at' t s)\<rbrace>
theory Fastpath_Equiv

lemma asUser_tcb_at'_Q[wp]:
  "\<lbrace>\<lambda>s. Q (tcb_at' t s)\<rbrace> asUser a b \<lbrace>\<lambda>_ s. Q (tcb_at' t s)\<rbrace>" by (simp add: tcb_at_typ_at', wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (tcb_at' t s)\<rbrace> asUser a b \<lbrace>\<lambda>_ s. Q (tcb_at' t s)\<rbrace>
theory Fastpath_Equiv

lemma active_ntfn_check_wp:
  "\<lbrace>\<lambda>s. Q (\<exists>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s
      \<and> \<not> obj_at' (Not o isActive) ntfnptr s) s \<rbrace> do bound_ntfn \<leftarrow> getBoundNotification thread;
      case bound_ntfn of None \<Rightarrow> return False
       | Some ntfnptr \<Rightarrow> liftM EndpointDecls_H.isActive $ getNotification ntfnptr
   od \<lbrace>Q\<rbrace>" apply (rule hoare_pre) apply (wp getNotification_wp gbn_wp' | wpc)+ apply (auto simp: pred_tcb_at'_def obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (\<exists>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<and> \<not> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s) s\<rbrace> do bound_ntfn <- getBoundNotification thread;
case bound_ntfn of None \<Rightarrow> return False | Some ntfnptr \<Rightarrow> liftM EndpointDecls_H.isActive $ getNotification ntfnptr
od \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do bound_ntfn <- getBoundNotification thread;
case bound_ntfn of None \<Rightarrow> return False | Some ntfnptr \<Rightarrow> liftM EndpointDecls_H.isActive $ getNotification ntfnptr
od \<lbrace>Q\<rbrace>
 2. \<And>s. Q (\<exists>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<and> \<not> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. Q (\<exists>ntfnptr. bound_tcb_at' ((=) (Some ntfnptr)) thread s \<and> \<not> obj_at' (Not \<circ> EndpointDecls_H.isActive) ntfnptr s) s \<Longrightarrow> \<forall>ntfn. bound_tcb_at' ((=) ntfn) thread s \<longrightarrow> (ntfn = None \<longrightarrow> Q False s) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> (Q \<circ> EndpointDecls_H.isActive) ntfn s)) proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma setCTE_obj_at'_queued:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued 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 (tcbQueued tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> setObject p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace>
theory Fastpath_C

lemma getEndpoint_obj_at':
  "\<lbrace>obj_at' P ptr\<rbrace> getEndpoint ptr \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (wp getEndpoint_wp) apply (clarsimp simp: obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P ptr\<rbrace> getEndpoint ptr \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P ptr s \<Longrightarrow> \<forall>ep. ko_at' ep ptr s \<longrightarrow> P ep proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma tcbSchedEnqueue_tcbContext[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
     tcbSchedEnqueue t'
   \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (rule tcbSchedEnqueue_obj_at_unchangedT[OF all_tcbI]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> tcbSchedEnqueue t' \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>f a b c d e fa g h i j k l m n p q. P ((atcbContextGet \<circ> tcbArch) (tcbQueued_update f (Thread a b c d e fa g h i j k l m n p q))) = P ((atcbContextGet \<circ> tcbArch) (Thread a b c d e fa g h i j k l m n p q)) proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma setCTE_tcbContext:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
  setCTE slot cte
  \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb', simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> setCTE slot cte \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) t\<rbrace> setObject slot cte \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma seThreadState_tcbContext:
 "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
    setThreadState a b
  \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (rule setThreadState_obj_at_unchanged) apply (clarsimp simp: atcbContext_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> setThreadState a b \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>f a b c d e fa g h i j k l m n p q. P ((atcbContextGet \<circ> tcbArch) (tcbState_update f (Thread a b c d e fa g h i j k l m n p q))) = P ((atcbContextGet \<circ> tcbArch) (Thread a b c d e fa g h i j k l m n p q))
 2. \<And>f a b c d e fa g h i j k l m n p q. P ((atcbContextGet \<circ> tcbArch) (tcbQueued_update f (Thread a b c d e fa g h i j k l m n p q))) = P ((atcbContextGet \<circ> tcbArch) (Thread a b c d e fa g h i j k l m n p q)) proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma setBoundNotification_tcbContext:
 "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
    setBoundNotification a b
  \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (rule setBoundNotification_obj_at_unchanged) apply (clarsimp simp: atcbContext_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> setBoundNotification a b \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>f a b c d e fa g h i j k l m n p q. P ((atcbContextGet \<circ> tcbArch) (tcbBoundNotification_update f (Thread a b c d e fa g h i j k l m n p q))) = P ((atcbContextGet \<circ> tcbArch) (Thread a b c d e fa g h i j k l m n p q)) proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma obj_at_tcbs_of:
  "obj_at' P t s = (EX tcb. tcbs_of s t = Some tcb & P tcb)" apply (simp add: tcbs_of_def split: if_split) apply (intro conjI impI) apply (clarsimp simp: obj_at'_def projectKOs) apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P t s = (\<exists>tcb. tcbs_of s t = Some tcb \<and> P tcb) proof (prove)
goal (1 subgoal):
 1. (tcb_at' t s \<longrightarrow> obj_at' P t s = (\<exists>tcb. projectKO_opt (the (ksPSpace s t)) = Some tcb \<and> P tcb)) \<and> (\<not> tcb_at' t s \<longrightarrow> \<not> obj_at' P t s) proof (prove)
goal (2 subgoals):
 1. tcb_at' t s \<Longrightarrow> obj_at' P t s = (\<exists>tcb. projectKO_opt (the (ksPSpace s t)) = Some tcb \<and> P tcb)
 2. \<not> tcb_at' t s \<Longrightarrow> \<not> obj_at' P t s proof (prove)
goal (1 subgoal):
 1. \<not> tcb_at' t s \<Longrightarrow> \<not> obj_at' P t s proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma st_tcb_at_tcbs_of:
  "st_tcb_at' P t s = (EX tcb. tcbs_of s t = Some tcb & P (tcbState tcb))" by (simp add: st_tcb_at'_def obj_at_tcbs_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' P t s = (\<exists>tcb. tcbs_of s t = Some tcb \<and> P (tcbState tcb))
theory Fastpath_C

lemma tcbs_of_ko_at':
  "\<lbrakk> tcbs_of s p = Some tcb \<rbrakk> \<Longrightarrow> ko_at' tcb p s" by (simp add: obj_at_tcbs_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcbs_of s p = Some tcb \<Longrightarrow> ko_at' tcb p s
theory Fastpath_C

lemma cap_'_cap_'_update_var_props:
  "cap_' (cap_'_update f s) = f (cap_' s) \<and>
         ((s', cap_'_update f s) \<in> rf_sr) = ((s', s) \<in> rf_sr)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_' (cap_'_update f s) = f (cap_' s) \<and> ((s', cap_'_update f s) \<in> rf_sr) = ((s', s) \<in> rf_sr)
theory Fastpath_C

lemma acc_CNodeCap_repr:
  "isCNodeCap cap
     \<Longrightarrow> cap = CNodeCap (capCNodePtr cap) (capCNodeBits cap)
                        (capCNodeGuard cap) (capCNodeGuardSize cap)" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isCNodeCap cap \<Longrightarrow> cap = capability.CNodeCap (capCNodePtr cap) (capCNodeBits cap) (capCNodeGuard cap) (capCNodeGuardSize cap)
theory Fastpath_C

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_C

lemma ccorres_abstract_all:
  "\<lbrakk>\<And>rv' t t'. ceqv Gamm xf' rv' t t' d (d' rv');
    \<And>rv'. ccorres_underlying sr Gamm r xf arrel axf (G rv') (G' rv') hs a (d' rv')\<rbrakk>
       \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. \<forall>rv'. G rv' s) {s. s \<in> G' (xf' s)} hs a d" apply (erule ccorres_abstract) apply (rule ccorres_guard_imp2) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv' t t'. ceqv Gamm xf' rv' t t' d (d' rv'); \<And>rv'. ccorres_underlying sr Gamm r xf arrel axf (G rv') (G' rv') hs a (d' rv')\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. \<forall>rv'. G rv' s) {s. s \<in> G' (xf' s)} hs a d proof (prove)
goal (1 subgoal):
 1. \<And>rv'. (\<And>rv'. ccorres_underlying sr Gamm r xf arrel axf (G rv') (G' rv') hs a (d' rv')) \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (\<lambda>s. \<forall>rv'. G rv' s) (G' rv') hs a (d' rv') proof (prove)
goal (2 subgoals):
 1. \<And>rv'. (\<And>rv'. ccorres_underlying sr Gamm r xf arrel axf (G rv') (G' rv') hs a (d' rv')) \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf (?Q2 rv') (?Q'2 rv') hs a (d' rv')
 2. \<And>rv' s s'. \<lbrakk>\<And>rv'. ccorres_underlying sr Gamm r xf arrel axf (G rv') (G' rv') hs a (d' rv'); (s, s') \<in> sr; \<forall>rv'. G rv' s; s' \<in> G' rv'\<rbrakk> \<Longrightarrow> ?Q2 rv' s \<and> s' \<in> ?Q'2 rv' proof (prove)
goal (1 subgoal):
 1. \<And>rv' s s'. \<lbrakk>\<And>rv'. ccorres_underlying sr Gamm r xf arrel axf (G rv') (G' rv') hs a (d' rv'); (s, s') \<in> sr; \<forall>rv'. G rv' s; s' \<in> G' rv'\<rbrakk> \<Longrightarrow> G rv' s \<and> s' \<in> G' rv' proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma isCNodeCap_capUntypedPtr_capCNodePtr:
  "isCNodeCap c \<Longrightarrow> capUntypedPtr c = capCNodePtr c" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isCNodeCap c \<Longrightarrow> global.capUntypedPtr c = capCNodePtr c
theory Fastpath_C

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

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

lemma ccap_relation_case_sum_Null_endpoint:
  "ccap_relation (case x of Inl v => NullCap | Inr v => v) ccap
     \<Longrightarrow> (cap_get_tag ccap = scast cap_endpoint_cap)
           = (isRight x \<and> isEndpointCap (theRight x))" by (clarsimp simp: cap_get_tag_isCap isRight_def isCap_simps
              split: sum.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation (case x of Inl v \<Rightarrow> capability.NullCap | Inr v \<Rightarrow> v) ccap \<Longrightarrow> (cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap) = (isRight x \<and> isEndpointCap (theRight x))
theory Fastpath_C

lemma ccap_relation_pd_helper:
  "\<lbrakk> ccap_relation cap cap'; cap_get_tag cap' = scast cap_page_directory_cap \<rbrakk>
        \<Longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift cap') = capPDBasePtr (capCap cap)" by (clarsimp simp: cap_lift_page_directory_cap cap_to_H_simps
                     cap_page_directory_cap_lift
              elim!: ccap_relationE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift cap') = capPDBasePtr (capCap cap)