kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace1_R

lemma getCTE_ctes_of:
  "\<lbrace>\<lambda>s. ctes_of s p \<noteq> None \<longrightarrow> P (the (ctes_of s p)) (ctes_of s)\<rbrace> getCTE p \<lbrace>\<lambda>rv s. P rv (ctes_of s)\<rbrace>" apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ctes_of s p \<noteq> None \<longrightarrow> P (the (ctes_of s p)) (ctes_of s)\<rbrace> getCTE p \<lbrace>\<lambda>rv s. P rv (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ctes_of s p \<noteq> None \<longrightarrow> P (the (ctes_of s p)) (ctes_of s) \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> P cte (ctes_of s)) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma getCTE_wp':
  "\<lbrace>\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) p s \<longrightarrow> Q cte s\<rbrace> getCTE p \<lbrace>Q\<rbrace>" apply (clarsimp simp add: getCTE_def valid_def cte_wp_at'_def) apply (drule getObject_cte_det) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) p s \<longrightarrow> Q cte s\<rbrace> getCTE p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>cte. fst (getObject p s) = {(cte, s)} \<longrightarrow> Q cte s; (a, b) \<in> fst (getObject p s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>cte. fst (getObject p s) = {(cte, s)} \<longrightarrow> Q cte s; fst (getObject p s) = {(a, s)} \<and> b = s\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma getSlotCap_corres:
  "cte_ptr' = cte_map cte_ptr \<Longrightarrow>
   corres cap_relation
     (cte_at cte_ptr)
     (pspace_distinct' and pspace_aligned')
     (get_cap cte_ptr)
     (getSlotCap cte_ptr')" apply (simp add: getSlotCap_def) apply (subst bind_return [symmetric]) apply (corresKsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_ptr' = cte_map cte_ptr \<Longrightarrow> corres cap_relation (cte_wp_at (\<lambda>_. True) cte_ptr) (pspace_distinct' and pspace_aligned') (get_cap cte_ptr) (getSlotCap cte_ptr') proof (prove)
goal (1 subgoal):
 1. cte_ptr' = cte_map cte_ptr \<Longrightarrow> corres cap_relation (cte_wp_at (\<lambda>_. True) cte_ptr) (pspace_distinct' and pspace_aligned') (get_cap cte_ptr) (do cte <- getCTE (cte_map cte_ptr);
return (cteCap cte)
od) proof (prove)
goal (1 subgoal):
 1. cte_ptr' = cte_map cte_ptr \<Longrightarrow> corres cap_relation (cte_wp_at (\<lambda>_. True) cte_ptr) (pspace_distinct' and pspace_aligned') (get_cap cte_ptr >>= return) (do cte <- getCTE (cte_map cte_ptr);
return (cteCap cte)
od) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma maskCapRights [simp]:
  "cap_relation c c' \<Longrightarrow>
  cap_relation (mask_cap msk c) (maskCapRights (rights_mask_map msk) c')" by (simp add: mask_cap_def cap_relation_masks)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c c' \<Longrightarrow> cap_relation (mask_cap msk c) (global.maskCapRights (rights_mask_map msk) c')
theory CSpace1_R

lemma maskCap_valid [simp]:
  "s \<turnstile>' RetypeDecls_H.maskCapRights R cap = s \<turnstile>' cap" by (simp    add: valid_cap'_def maskCapRights_def isCap_simps
                   capAligned_def ARM_H.maskCapRights_def
            split: capability.split arch_capability.split
        split del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' (global.maskCapRights R cap) s = valid_cap' cap s
theory CSpace1_R

lemma getSlotCap_valid_cap:
  "\<lbrace>valid_objs'\<rbrace> getSlotCap t \<lbrace>\<lambda>r. valid_cap' r and cte_at' t\<rbrace>" apply (simp add: getSlotCap_def) apply (wp getCTE_valid_cap | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> getSlotCap t \<lbrace>\<lambda>r. valid_cap' r and cte_wp_at' (\<lambda>_. True) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do cte <- getCTE t;
return (cteCap cte)
od \<lbrace>\<lambda>r. valid_cap' r and cte_wp_at' (\<lambda>_. True) t\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma resolveAddressBits_cte_at':
  "\<lbrace> valid_objs' and valid_cap' cap \<rbrace>
  resolveAddressBits cap addr depth
  \<lbrace>\<lambda>rv. cte_at' (fst rv)\<rbrace>, \<lbrace>\<lambda>rv s. True\<rbrace>" apply (fold validE_R_def) apply (rule hoare_post_imp_R) apply (rule resolveAddressBits_real_cte_at') apply (erule real_cte_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> CSpace_H.resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) (fst rv)\<rbrace>, \<lbrace>\<lambda>rv s. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> CSpace_H.resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) (fst rv)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> CSpace_H.resolveAddressBits cap addr depth \<lbrace>?Q'\<rbrace>, -
 2. \<And>rv s. ?Q' rv s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (fst rv) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. real_cte_at' (fst rv) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (fst rv) s proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma cte_map_shift':
  "\<lbrakk> to_bl cref' = zs @ cref; guard \<le> cref; length cref = cbits + length guard;
    is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits \<rbrakk> \<Longrightarrow>
  ptr + 2^cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)" by (auto dest: cte_map_shift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>to_bl cref' = zs @ cref; guard \<le> cref; length cref = cbits + length guard; is_aligned ptr (cte_level_bits + cbits); cbits \<le> word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> ptr + 2 ^ cte_level_bits * (cref' && mask cbits) = cte_map (ptr, drop (length guard) cref)
theory CSpace1_R

lemma cap_relation_Null2 [simp]:
  "cap_relation c NullCap = (c = cap.NullCap)" by (cases c) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation c capability.NullCap = (c = cap.NullCap)
theory CSpace1_R

lemma getThreadCSpaceRoot:
  "getThreadCSpaceRoot t = return t" by (simp add: getThreadCSpaceRoot_def locateSlot_conv
                tcbCTableSlot_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getThreadCSpaceRoot t = return t
theory CSpace1_R

lemma getThreadVSpaceRoot:
  "getThreadVSpaceRoot t = return (t + 2^cteSizeBits)" by (simp add: getThreadVSpaceRoot_def locateSlot_conv objBits_simps'
                tcbVTableSlot_def shiftl_t2n cte_level_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getThreadVSpaceRoot t = return (t + 2 ^ cteSizeBits)
theory CSpace1_R

lemma lookupSlot_cte_at_wp[wp]:
  "\<lbrace>valid_objs'\<rbrace> lookupSlotForThread t addr \<lbrace>\<lambda>rv. cte_at' rv\<rbrace>, \<lbrace>\<lambda>r. \<top>\<rbrace>" apply (simp add: lookupSlotForThread_def) apply (simp add: getThreadCSpaceRoot_def locateSlot_conv tcbCTableSlot_def) apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupSlotForThread t addr \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>r _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> doE threadRootSlot <- liftE (getThreadCSpaceRoot t);
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot addr (size addr);
returnOk s
odE \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>r _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> doE threadRootSlot <- liftE (return t);
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot addr (size addr);
returnOk s
odE \<lbrace>cte_wp_at' (\<lambda>_. True)\<rbrace>, \<lbrace>\<lambda>r _. True\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma lookupSlot_inv[wp]:
  "\<lbrace>P\<rbrace> lookupSlotForThread t addr \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: lookupSlotForThread_def) apply (simp add: getThreadCSpaceRoot_def locateSlot_conv tcbCTableSlot_def) apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> lookupSlotForThread t addr \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE threadRootSlot <- liftE (getThreadCSpaceRoot t);
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot addr (size addr);
returnOk s
odE \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE threadRootSlot <- liftE (return t);
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot addr (size addr);
returnOk s
odE \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma setObject_cte_obj_at_tcb':
  assumes x: "\<And>tcb f. P (tcbCTable_update f tcb) = P tcb"
             "\<And>tcb f. P (tcbVTable_update f tcb) = P tcb"
             "\<And>tcb f. P (tcbReply_update f tcb) = P tcb"
             "\<And>tcb f. P (tcbCaller_update f tcb) = P tcb"
             "\<And>tcb f. P (tcbIPCBufferFrame_update f tcb) = P tcb"
  shows
  "\<lbrace>\<lambda>s. P' (obj_at' (P :: tcb \<Rightarrow> bool) p s)\<rbrace>
  setObject c (cte::cte)
  \<lbrace>\<lambda>_ s. P' (obj_at' P p s)\<rbrace>" apply (clarsimp simp: setObject_def in_monad split_def
                        valid_def lookupAround2_char1
                        obj_at'_def ps_clear_upd projectKOs
             split del: if_split) apply (clarsimp elim!: rsubst[where P=P']) apply (clarsimp simp: updateObject_cte in_monad objBits_simps
                        tcbCTableSlot_def tcbVTableSlot_def x
                        typeError_def
                 split: if_split_asm
                        Structures_H.kernel_object.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (obj_at' P p s)\<rbrace> setObject c cte \<lbrace>\<lambda>_ s. P' (obj_at' P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s''a obj'. \<lbrakk>P' (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. ko = KOTCB obj \<and> P obj \<and> ps_clear p (objBitsKO ko) s)); a \<le> c; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> c \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject cte ba c a (snd (lookupAround2 c (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> P' (\<exists>ko. (if p = a then Some obj' else ksPSpace s p) = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. ko = KOTCB obj \<and> P obj \<and> ps_clear p (objBitsKO ko) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s ba s''a obj'. \<lbrakk>p \<le> c; ksPSpace s p = Some ba; \<forall>z. p < z \<and> z \<le> c \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject cte ba c p (snd (lookupAround2 c (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> (is_aligned p (objBitsKO ba) \<and> (\<exists>obj. ba = KOTCB obj \<and> P obj \<and> ps_clear p (objBitsKO ba) s)) = (is_aligned p (objBitsKO obj') \<and> (\<exists>obj. obj' = KOTCB obj \<and> P obj \<and> ps_clear p (objBitsKO obj') s)) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma setCTE_typ_at':
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setCTE c cte \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>" by (clarsimp simp add: setCTE_def) (wp setObject_typ_at')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setCTE c cte \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>
theory CSpace1_R

lemma setCTE_typ_at [wp]:
  "\<lbrace>typ_at' T p\<rbrace> setCTE c cte \<lbrace>\<lambda>_. typ_at' T p\<rbrace>" by (clarsimp simp add: setCTE_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at' T p\<rbrace> setCTE c cte \<lbrace>\<lambda>_. typ_at' T p\<rbrace>
theory CSpace1_R

lemma setObject_cte_ksCurDomain[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject ptr (cte::cte) \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp updateObject_cte_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject ptr cte \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr ps));
obj' <- updateObject cte (snd p) ptr (fst p) (snd (lookupAround2 ptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma setCTE_tcb_in_cur_domain':
  "\<lbrace>tcb_in_cur_domain' t\<rbrace>
     setCTE c cte
   \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>" unfolding tcb_in_cur_domain'_def setCTE_def apply (rule_tac f="\<lambda>s. ksCurDomain s" in hoare_lift_Pf) apply (wp setObject_cte_obj_at_tcb' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> setCTE c cte \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> setObject c cte \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace> setObject c cte \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. x = tcbDomain tcb) t\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject c cte \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma setCTE_ctes_of_wp [wp]:
  "\<lbrace>\<lambda>s. P ((ctes_of s) (p \<mapsto> cte))\<rbrace>
  setCTE p cte
  \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" by (simp add: setCTE_def ctes_of_setObject_cte)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((ctes_of s)(p \<mapsto> cte))\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>
theory CSpace1_R

lemma setCTE_weak_cte_wp_at:
 "\<lbrace>\<lambda>s. (if p = ptr then P (cteCap cte) else cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace>
  setCTE ptr cte
  \<lbrace>\<lambda>uu s. cte_wp_at'(\<lambda>c. P (cteCap c)) p s\<rbrace>" apply (simp add: cte_wp_at_ctes_of) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = ptr then P (cteCap cte) else cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace> setCTE ptr cte \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (p = ptr \<longrightarrow> P (cteCap cte)) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)))\<rbrace> setCTE ptr cte \<lbrace>\<lambda>uu s. \<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (p = ptr \<longrightarrow> P (cteCap cte)) \<and> (p \<noteq> ptr \<longrightarrow> (\<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte))) \<Longrightarrow> \<exists>ctea. ((ctes_of s)(ptr \<mapsto> cte)) p = Some ctea \<and> P (cteCap ctea) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma updateMDB_weak_cte_wp_at:
 "\<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
  updateMDB m f
  \<lbrace>\<lambda>uu. cte_wp_at'(\<lambda>c. P (cteCap c)) p\<rbrace>" unfolding updateMDB_def apply simp apply safe apply (wp setCTE_weak_cte_wp_at getCTE_wp) apply (auto simp: cte_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> updateMDB m f \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> let slot = m in if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (f mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. m \<noteq> 0 \<longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> do cte <- getCTE m;
setCTE m (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> do cte <- getCTE m;
setCTE m (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>m \<noteq> 0; cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) m s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) m s \<and> (if p = m then P (cteCap (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)) else cte_wp_at' (\<lambda>c. P (cteCap c)) p s)) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma maxFreeIndex_update_valid_cap'[simp]:
  "s \<turnstile>' capability.UntypedCap d v0a v1a fa \<Longrightarrow>
   s \<turnstile>' capability.UntypedCap d v0a v1a (maxFreeIndex v1a)" apply (rule capFreeIndex_update_valid_cap'[rotated -1]) apply assumption apply (clarsimp simp: valid_cap'_def capAligned_def ko_wp_at'_def
                        maxFreeIndex_def shiftL_nat)+ apply (erule is_aligned_weaken[OF is_aligned_triv]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap d v0a v1a fa) s \<Longrightarrow> valid_cap' (capability.UntypedCap d v0a v1a (maxFreeIndex v1a)) s proof (prove)
goal (4 subgoals):
 1. valid_cap' (capability.UntypedCap d v0a v1a fa) s \<Longrightarrow> valid_cap' (capability.UntypedCap d v0a v1a ?fa) s
 2. valid_cap' (capability.UntypedCap d v0a v1a fa) s \<Longrightarrow> ?fa \<le> maxFreeIndex v1a
 3. valid_cap' (capability.UntypedCap d v0a v1a fa) s \<Longrightarrow> maxFreeIndex v1a \<le> 2 ^ v1a
 4. valid_cap' (capability.UntypedCap d v0a v1a fa) s \<Longrightarrow> is_aligned (word_of_nat (maxFreeIndex v1a)) minUntypedSizeBits proof (prove)
goal (3 subgoals):
 1. valid_cap' (capability.UntypedCap d v0a v1a fa) s \<Longrightarrow> fa \<le> maxFreeIndex v1a
 2. valid_cap' (capability.UntypedCap d v0a v1a fa) s \<Longrightarrow> maxFreeIndex v1a \<le> 2 ^ v1a
 3. valid_cap' (capability.UntypedCap d v0a v1a fa) s \<Longrightarrow> is_aligned (word_of_nat (maxFreeIndex v1a)) minUntypedSizeBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned v0a v1a; v1a < word_bits; valid_untyped' d v0a v1a fa s; v0a \<noteq> 0; minUntypedSizeBits \<le> v1a; v1a \<le> maxUntypedSizeBits; fa \<le> 2 ^ v1a; is_aligned (word_of_nat fa) minUntypedSizeBits\<rbrakk> \<Longrightarrow> is_aligned (2 ^ v1a) minUntypedSizeBits proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma ctes_of_valid_cap'':
  "\<lbrakk> ctes_of s p = Some r; valid_objs' s\<rbrakk> \<Longrightarrow> s \<turnstile>' (cteCap r)" apply (rule cte_wp_at_valid_objs_valid_cap'[where P="(=) r", simplified]) apply (simp add: cte_wp_at_ctes_of) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some r; valid_objs' s\<rbrakk> \<Longrightarrow> valid_cap' (cteCap r) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some r; valid_objs' s\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) r) ?p s
 2. \<lbrakk>ctes_of s p = Some r; valid_objs' s\<rbrakk> \<Longrightarrow> valid_objs' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some r; valid_objs' s\<rbrakk> \<Longrightarrow> valid_objs' s proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma setCTE_valid_cap:
  "\<lbrace>valid_cap' c\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r. valid_cap' c\<rbrace>" by (rule typ_at_lifts, rule setCTE_typ_at')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' c\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r. valid_cap' c\<rbrace>
theory CSpace1_R

lemma set_is_modify:
  "m p = Some cte \<Longrightarrow>
  m (p \<mapsto> cteMDBNode_update (\<lambda>_. (f (cteMDBNode cte))) cte) =
  m (p \<mapsto> cteMDBNode_update f cte)" apply (case_tac cte) apply (rule ext) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some cte \<Longrightarrow> m(p \<mapsto> cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) = m(p \<mapsto> cteMDBNode_update f cte) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>m p = Some cte; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> m(p \<mapsto> cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) = m(p \<mapsto> cteMDBNode_update f cte) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x. \<lbrakk>m p = Some cte; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> (m(p \<mapsto> cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)) x = (m(p \<mapsto> cteMDBNode_update f cte)) x proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma updateMDB_ctes_of_wp:
  "\<lbrace>\<lambda>s. (p \<noteq> 0 \<longrightarrow> P (modify_map (ctes_of s) p (cteMDBNode_update f))) \<and>
        (p = 0 \<longrightarrow> P (ctes_of s))\<rbrace>
  updateMDB p f
  \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" apply (simp add: updateMDB_def) apply safe apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) apply (simp add: modify_map_def set_is_modify) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (p \<noteq> 0 \<longrightarrow> P (modify_map (ctes_of s) p (cteMDBNode_update f))) \<and> (p = 0 \<longrightarrow> P (ctes_of s))\<rbrace> updateMDB p f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<longrightarrow> \<lbrace>\<lambda>s. P (modify_map (ctes_of s) p (cteMDBNode_update f))\<rbrace> do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. P (modify_map (ctes_of s) p (cteMDBNode_update f))\<rbrace> do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> 0; P (modify_map (ctes_of s) p (cteMDBNode_update f))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> P ((ctes_of s)(p \<mapsto> cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>p \<noteq> 0; P (modify_map (ctes_of s) p (cteMDBNode_update f)); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> P ((ctes_of s)(p \<mapsto> cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma updateMDB_ctes_of_no_0 [wp]:
  "\<lbrace>\<lambda>s. no_0 (ctes_of s) \<and>
        P (modify_map (ctes_of s) p (cteMDBNode_update f))\<rbrace>
  updateMDB p f
  \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" by (wp updateMDB_ctes_of_wp) clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_0 (ctes_of s) \<and> P (modify_map (ctes_of s) p (cteMDBNode_update f))\<rbrace> updateMDB p f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>