kings-crown/FVELER_Isabelle huggingface dataset:
theory Fastpath_C

lemma ptr_add_0xFF0:
  "pde_Ptr (pd + 0x3FC0) = CTypesDefs.ptr_add (pde_Ptr pd) 0xFF0" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pde_Ptr (pd + 0x3FC0) = pde_Ptr pd +\<^sub>p 4080
theory Fastpath_C

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 add: select_f_oblivious) 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_C

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_C

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_C

lemma ccorres_pre_getCTE2:
  "(\<And>rv. ccorresG rf_sr \<Gamma> r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow>
   ccorresG rf_sr \<Gamma> r xf (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s)
                         {s. \<forall>cte cte'. cslift s (cte_Ptr p) = Some cte' \<and> ccte_relation cte cte'
                                          \<longrightarrow> s \<in> P' cte} hs
         (getCTE p >>= (\<lambda>rv. f rv)) c" apply (rule ccorres_guard_imp2, erule ccorres_pre_getCTE) apply (clarsimp simp: map_comp_Some_iff ccte_relation_def
                        c_valid_cte_def cl_valid_cte_def
                        c_valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf (\<lambda>s. \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s) {s. \<forall>cte cte'. cslift s (cte_Ptr p) = Some cte' \<and> ccte_relation cte cte' \<longrightarrow> s \<in> P' cte} hs (getCTE p >>= f) c proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c; (s, s') \<in> rf_sr; \<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s; s' \<in> {s. \<forall>cte cte'. cslift s (cte_Ptr p) = Some cte' \<and> ccte_relation cte cte' \<longrightarrow> s \<in> P' cte}\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s p = Some cte \<longrightarrow> P cte s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> P' (cte_to_H cte')} proof (prove)
goal:
No subgoals!
theory Fastpath_C

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_C

lemma messageInfoFromWord_raw_spec:
  "\<forall>s. \<Gamma>\<turnstile> {s} Call messageInfoFromWord_raw_'proc
       \<lbrace>\<acute>ret__struct_seL4_MessageInfo_C
    = (seL4_MessageInfo_C (FCP (K \<^bsup>s\<^esup>w)))\<rbrace>" apply vcg apply (clarsimp simp: word_sless_def word_sle_def) apply (case_tac v) apply (simp add: cart_eq fcp_beta) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call messageInfoFromWord_raw_'proc \<lbrace>\<acute>ret__struct_seL4_MessageInfo_C = seL4_MessageInfo_C (FCP (K \<^bsup>s\<^esup>w))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>w. \<forall>v. 0 <s 1 \<and> 0 \<le>s 0 \<and> seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (UCAST(32 \<rightarrow> 32) w)) v = seL4_MessageInfo_C (FCP (K w)) proof (prove)
goal (1 subgoal):
 1. \<And>w v. seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v 0 w) v = seL4_MessageInfo_C (ARRAY i. w) proof (prove)
goal (1 subgoal):
 1. \<And>w v x. v = seL4_MessageInfo_C x \<Longrightarrow> seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v 0 w) v = seL4_MessageInfo_C (ARRAY i. w) proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma mi_check_messageInfo_raw:
  "length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi))))
                  \<le> scast n_msgRegisters
    \<Longrightarrow> seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))
        = mi_from_H (messageInfoFromWord mi)" apply (simp add: messageInfoFromWord_def Let_def mi_from_H_def
                   seL4_MessageInfo_lift_def fcp_beta msgLengthBits_def msgExtraCapBits_def
                   msgMaxExtraCaps_def shiftL_nat mask_def msgLabelBits_def) apply (subst if_not_P) apply (simp add: linorder_not_less msgMaxLength_def n_msgRegisters_def) apply (erule order_trans, simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi))) = mi_from_H (messageInfoFromWord mi) proof (prove)
goal (1 subgoal):
 1. mi && 0x7F \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> mi && 0x7F = (if msgMaxLength < mi && 0x7F then msgMaxLength else mi && 0x7F) proof (prove)
goal (2 subgoals):
 1. mi && 0x7F \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> \<not> msgMaxLength < mi && 0x7F
 2. mi && 0x7F \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> mi && 0x7F = mi && 0x7F proof (prove)
goal (2 subgoals):
 1. mi && 0x7F \<le> 4 \<Longrightarrow> mi && 0x7F \<le> 0x78
 2. mi && 0x7F \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> mi && 0x7F = mi && 0x7F proof (prove)
goal (1 subgoal):
 1. mi && 0x7F \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> mi && 0x7F = mi && 0x7F proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma isValidVTableRoot_fp_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call isValidVTableRoot_fp_'proc
       {t. ret__unsigned_long_' t = from_bool (isValidVTableRoot_C (pd_cap_' s))}" apply vcg apply (clarsimp simp: word_sle_def word_sless_def isValidVTableRoot_fp_lemma) apply (simp split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call isValidVTableRoot_fp_'proc \<lbrace>\<acute>ret__unsigned_long = from_bool (isValidVTableRoot_C \<^bsup>s\<^esup>pd_cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>pd_cap. 0 \<le>s 4 \<and> 4 <s 0x20 \<and> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> SCAST(32 signed \<rightarrow> 32) (if UCAST(32 \<rightarrow> 32) (cap_C.words_C pd_cap.[unat 0]) && (1 << unat 5) - 1 = (1 << unat 4) || SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0) = from_bool (isValidVTableRoot_C pd_cap) proof (prove)
goal (1 subgoal):
 1. \<And>pd_cap. (if isValidVTableRoot_C pd_cap then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) = from_bool (isValidVTableRoot_C pd_cap) proof (prove)
goal:
No subgoals!
theory Fastpath_C

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_C

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_C

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_C

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_C

lemma cntfn_relation_double_fun_upd:
  "\<lbrakk> cnotification_relation mp ntfn ntfn'
       = cnotification_relation (mp(a := b)) ntfn ntfn';
     cnotification_relation (mp(a := b)) ntfn ntfn'
       = cnotification_relation (mp(a := b, c := d)) ntfn ntfn' \<rbrakk>
   \<Longrightarrow> cnotification_relation mp ntfn ntfn'
         = cnotification_relation (mp(a := b, c := d)) ntfn ntfn'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cnotification_relation mp ntfn ntfn' = cnotification_relation (mp(a := b)) ntfn ntfn'; cnotification_relation (mp(a := b)) ntfn ntfn' = cnotification_relation (mp(a := b, c := d)) ntfn ntfn'\<rbrakk> \<Longrightarrow> cnotification_relation mp ntfn ntfn' = cnotification_relation (mp(a := b, c := d)) ntfn ntfn'
theory Fastpath_C

lemma getCTE_setCTE_rf_sr:
  "\<lbrakk> (\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte;
     t_hrs_' (globals s') = hrs_mem_update
        (heap_update (cte_Ptr ptr) cte')
        (t_hrs_' (globals s));
     ccte_relation (f cte) cte';
     (globals s')\<lparr> t_hrs_' := undefined \<rparr>
          = (globals s)\<lparr> t_hrs_' := undefined \<rparr> \<rbrakk>

      \<Longrightarrow>
   \<exists>x\<in>fst ((do cte \<leftarrow> getCTE ptr;
                      setCTE ptr (f cte)
                    od)
                    \<sigma>).
             (snd x, s') \<in> rf_sr" apply (drule setCTE_rf_sr, assumption+) apply (clarsimp simp: Bex_def in_bind_split in_getCTE2 cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation (f cte) cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do cte <- getCTE ptr;
setCTE ptr (f cte)
od) \<sigma>). (snd x, s') \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of \<sigma> ptr = Some cte; t_hrs_' (globals s') = hrs_mem_update (heap_update (cte_Ptr ptr) cte') (t_hrs_' (globals s)); ccte_relation (f cte) cte'; globals s'\<lparr>t_hrs_' := undefined\<rparr> = globals s\<lparr>t_hrs_' := undefined\<rparr>; \<exists>x\<in>fst (setCTE ptr (f cte) \<sigma>). (snd x, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do cte <- getCTE ptr;
setCTE ptr (f cte)
od) \<sigma>). (snd x, s') \<in> rf_sr proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma ccte_relation_eq_ccap_relation:
  notes option.case_cong_weak [cong]
  shows
  "ccte_relation cte ccte
      = (ccap_relation (cteCap cte) (cte_C.cap_C ccte)
            \<and> mdb_node_to_H (mdb_node_lift (cteMDBNode_C ccte))
                   = (cteMDBNode cte))" apply (simp add: ccte_relation_def map_option_Some_eq2 cte_lift_def
                   ccap_relation_def) apply (simp add: cte_to_H_def split: option.split) apply (cases cte, clarsimp simp: c_valid_cte_def conj_comms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccte_relation cte ccte = (ccap_relation (cteCap cte) (cte_C.cap_C ccte) \<and> mdb_node_to_H (mdb_node_lift (cteMDBNode_C ccte)) = cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. ((\<exists>z. (case cap_lift (cte_C.cap_C ccte) of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C ccte)\<rparr>) = Some z \<and> cte_to_H z = cte) \<and> c_valid_cte ccte) = ((\<exists>z. cap_lift (cte_C.cap_C ccte) = Some z \<and> cap_to_H z = cteCap cte) \<and> c_valid_cap (cte_C.cap_C ccte) \<and> mdb_node_to_H (mdb_node_lift (cteMDBNode_C ccte)) = cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<forall>x2. cap_lift (cte_C.cap_C ccte) = Some x2 \<longrightarrow> (CTE (cap_to_H x2) (mdb_node_to_H (mdb_node_lift (cteMDBNode_C ccte))) = cte \<and> c_valid_cte ccte) = (cap_to_H x2 = cteCap cte \<and> c_valid_cap (cte_C.cap_C ccte) \<and> mdb_node_to_H (mdb_node_lift (cteMDBNode_C ccte)) = cteMDBNode cte) proof (prove)
goal:
No subgoals!
theory Fastpath_C

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_C

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_C

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_C

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!