kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_R

lemma getObject_ko_at_tcb [wp]:
  "\<lbrace>\<top>\<rbrace> getObject p \<lbrace>\<lambda>rv::tcb. ko_at' rv p\<rbrace>" by (rule getObject_ko_at | simp add: objBits_simps')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getObject p \<lbrace>\<lambda>rv. ko_at' rv p\<rbrace>
theory KHeap_R

lemma OMG_getObject_tcb:
  "\<lbrace>obj_at' P t\<rbrace> getObject t \<lbrace>\<lambda>(tcb :: tcb) s. P tcb\<rbrace>" apply (rule obj_at_getObject) apply (clarsimp simp: loadObject_default_def in_monad projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> getObject t \<lbrace>\<lambda>tcb s. P tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b n ko s obj. \<lbrakk>(a, b) \<in> fst (loadObject t t n ko s); projectKO_opt ko = Some obj\<rbrakk> \<Longrightarrow> a = obj proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_nosch:
  assumes x: "\<And>p q n ko. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setObject t val \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp x | simp)+ done

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

lemma getObject_ep_inv: "\<lbrace>P\<rbrace> (getObject addr :: endpoint kernel) \<lbrace>\<lambda>rv. P\<rbrace>" apply (rule getObject_inv) apply (simp add: loadObject_default_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject addr \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>P\<rbrace> loadObject p q n ko \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma getObject_ntfn_inv:
  "\<lbrace>P\<rbrace> (getObject addr :: Structures_H.notification kernel) \<lbrace>\<lambda>rv. P\<rbrace>" apply (rule getObject_inv) apply (simp add: loadObject_default_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject addr \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>P\<rbrace> loadObject p q n ko \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma get_ep_inv'[wp]: "\<lbrace>P\<rbrace> getEndpoint ep \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getEndpoint_def getObject_ep_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getEndpoint ep \<lbrace>\<lambda>rv. P\<rbrace>
theory KHeap_R

lemma get_ntfn_inv'[wp]: "\<lbrace>P\<rbrace> getNotification ntfn \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: getNotification_def getObject_ntfn_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getNotification ntfn \<lbrace>\<lambda>rv. P\<rbrace>
theory KHeap_R

lemma get_ep'_valid_ep[wp]:
  "\<lbrace> invs' and ep_at' ep \<rbrace> getEndpoint ep \<lbrace> valid_ep' \<rbrace>" apply (simp add: getEndpoint_def) apply (rule hoare_chain) apply (rule getObject_valid_obj) apply simp apply (simp add: objBits_simps') apply clarsimp apply (simp add: valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ep_at' ep\<rbrace> getEndpoint ep \<lbrace>valid_ep'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ep_at' ep\<rbrace> getObject ep \<lbrace>valid_ep'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> getObject ep \<lbrace>?Q\<rbrace>
 2. \<And>s. (invs' and ep_at' ep) s \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> valid_ep' rv s proof (prove)
goal (4 subgoals):
 1. \<And>p q n ko. loadObject p q n ko = loadObject_default p q n ko
 2. \<And>v. 1 < 2 ^ objBits v
 3. \<And>s. (invs' and ep_at' ep) s \<Longrightarrow> valid_objs' s
 4. \<And>rv s. valid_obj' (injectKO rv) s \<Longrightarrow> valid_ep' rv s proof (prove)
goal (3 subgoals):
 1. \<And>v. 1 < 2 ^ objBits v
 2. \<And>s. (invs' and ep_at' ep) s \<Longrightarrow> valid_objs' s
 3. \<And>rv s. valid_obj' (injectKO rv) s \<Longrightarrow> valid_ep' rv s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and ep_at' ep) s \<Longrightarrow> valid_objs' s
 2. \<And>rv s. valid_obj' (injectKO rv) s \<Longrightarrow> valid_ep' rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. valid_obj' (injectKO rv) s \<Longrightarrow> valid_ep' rv s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma get_ntfn'_valid_ntfn[wp]:
  "\<lbrace> invs' and ntfn_at' ep \<rbrace> getNotification ep \<lbrace> valid_ntfn' \<rbrace>" apply (simp add: getNotification_def) apply (rule hoare_chain) apply (rule getObject_valid_obj) apply simp apply (simp add: objBits_simps') apply clarsimp apply (simp add: valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ntfn_at' ep\<rbrace> getNotification ep \<lbrace>valid_ntfn'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ntfn_at' ep\<rbrace> getObject ep \<lbrace>valid_ntfn'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> getObject ep \<lbrace>?Q\<rbrace>
 2. \<And>s. (invs' and ntfn_at' ep) s \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> valid_ntfn' rv s proof (prove)
goal (4 subgoals):
 1. \<And>p q n ko. loadObject p q n ko = loadObject_default p q n ko
 2. \<And>v. 1 < 2 ^ objBits v
 3. \<And>s. (invs' and ntfn_at' ep) s \<Longrightarrow> valid_objs' s
 4. \<And>rv s. valid_obj' (injectKO rv) s \<Longrightarrow> valid_ntfn' rv s proof (prove)
goal (3 subgoals):
 1. \<And>v. 1 < 2 ^ objBits v
 2. \<And>s. (invs' and ntfn_at' ep) s \<Longrightarrow> valid_objs' s
 3. \<And>rv s. valid_obj' (injectKO rv) s \<Longrightarrow> valid_ntfn' rv s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and ntfn_at' ep) s \<Longrightarrow> valid_objs' s
 2. \<And>rv s. valid_obj' (injectKO rv) s \<Longrightarrow> valid_ntfn' rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. valid_obj' (injectKO rv) s \<Longrightarrow> valid_ntfn' rv s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_distinct[wp]:
  shows     "\<lbrace>pspace_distinct'\<rbrace> setObject p val \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>" apply (clarsimp simp: setObject_def split_def valid_def in_monad
                        projectKOs pspace_distinct'_def ps_clear_upd
                        objBits_def[symmetric] lookupAround2_char1
                 split: if_split_asm
                 dest!: updateObject_objBitsKO) apply (fastforce dest: bspec[OF _ domI]) apply (fastforce dest: bspec[OF _ domI]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct'\<rbrace> setObject p val \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s y a ba. \<lbrakk>a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO y = objBitsKO ba; \<forall>x\<in>dom (ksPSpace s). ps_clear x (objBitsKO (the (ksPSpace s x))) s\<rbrakk> \<Longrightarrow> ps_clear a (objBitsKO ba) s
 2. \<And>s x y a ba obj'. \<lbrakk>a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO obj' = objBitsKO ba; \<forall>x\<in>dom (ksPSpace s). ps_clear x (objBitsKO (the (ksPSpace s x))) s; x \<noteq> a; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO y) s proof (prove)
goal (1 subgoal):
 1. \<And>s x y a ba obj'. \<lbrakk>a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO obj' = objBitsKO ba; \<forall>x\<in>dom (ksPSpace s). ps_clear x (objBitsKO (the (ksPSpace s x))) s; x \<noteq> a; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO y) s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_aligned[wp]:
  shows     "\<lbrace>pspace_aligned'\<rbrace> setObject p val \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>" apply (clarsimp simp: setObject_def split_def valid_def in_monad
                        projectKOs pspace_aligned'_def ps_clear_upd
                        objBits_def[symmetric] lookupAround2_char1
                 split: if_split_asm
                 dest!: updateObject_objBitsKO) apply (fastforce dest: bspec[OF _ domI]) apply (fastforce dest: bspec[OF _ domI]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> setObject p val \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s y a ba. \<lbrakk>a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO y = objBitsKO ba; \<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x)))\<rbrakk> \<Longrightarrow> is_aligned a (objBitsKO ba)
 2. \<And>s x y a ba obj'. \<lbrakk>a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO obj' = objBitsKO ba; \<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x))); x \<noteq> a; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO y) proof (prove)
goal (1 subgoal):
 1. \<And>s x y a ba obj'. \<lbrakk>a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO obj' = objBitsKO ba; \<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x))); x \<noteq> a; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO y) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_aligned' [wp]:
  "\<lbrace>pspace_aligned'\<rbrace> setEndpoint ep v  \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>" unfolding setEndpoint_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> setEndpoint ep v \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> setObject ep v \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
theory KHeap_R

lemma set_ep_distinct' [wp]:
  "\<lbrace>pspace_distinct'\<rbrace> setEndpoint ep v  \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>" unfolding setEndpoint_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct'\<rbrace> setEndpoint ep v \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct'\<rbrace> setObject ep v \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
theory KHeap_R

lemma setEndpoint_pred_tcb_at'[wp]:
  "\<lbrace>pred_tcb_at' proj P t\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>" apply (simp add: pred_tcb_at'_def setEndpoint_def) apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma get_ntfn_ko':
  "\<lbrace>\<top>\<rbrace> getNotification ep \<lbrace>\<lambda>rv. ko_at' rv ep\<rbrace>" apply (simp add: getNotification_def) apply (rule getObject_ko_at) apply simp apply (simp add: objBits_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getNotification ep \<lbrace>\<lambda>rv. ko_at' rv ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getObject ep \<lbrace>\<lambda>rv. ko_at' rv ep\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>q n ko. loadObject ep q n ko = loadObject_default ep q n ko
 2. \<And>v. 1 < 2 ^ objBits v proof (prove)
goal (1 subgoal):
 1. \<And>v. 1 < 2 ^ objBits v proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_aligned'[wp]:
  "\<lbrace>pspace_aligned'\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>" unfolding setNotification_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
theory KHeap_R

lemma set_ntfn_distinct'[wp]:
  "\<lbrace>pspace_distinct'\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>" unfolding setNotification_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct'\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct'\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
theory KHeap_R

lemma setNotification_cte_wp_at':
  "\<lbrace>cte_wp_at' P p\<rbrace> setNotification ptr v \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>" unfolding setNotification_def apply (rule setObject_cte_wp_at'[where Q="\<top>", simplified]) apply (clarsimp simp add: updateObject_default_def in_monad
                             projectKOs
                     intro!: set_eqI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p\<rbrace> setNotification ptr v \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p\<rbrace> setObject ptr v \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) ptr x n s); lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb)
 2. \<And>x n cte s. fst (updateObject v (KOCTE cte) ptr x n s) = {} proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_ntfn_tcb':
  "\<lbrace>tcb_at' t\<rbrace> setObject p (e::Structures_H.notification) \<lbrace>\<lambda>_. tcb_at' t\<rbrace>" apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> setObject p e \<lbrace>\<lambda>_. tcb_at' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_tcb' [wp]:
  "\<lbrace> tcb_at' t \<rbrace> setNotification ntfn v \<lbrace> \<lambda>rv. tcb_at' t \<rbrace>" by (simp add: setNotification_def setObject_ntfn_tcb')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> setNotification ntfn v \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
theory KHeap_R

lemma pspace_dom_update:
  "\<lbrakk> ps ptr = Some x; a_type x = a_type v \<rbrakk> \<Longrightarrow> pspace_dom (ps(ptr \<mapsto> v)) = pspace_dom ps" apply (simp add: pspace_dom_def dom_fun_upd2 del: dom_fun_upd) apply (rule SUP_cong [OF refl]) apply clarsimp apply (simp add: obj_relation_cuts_def3) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps ptr = Some x; a_type x = a_type v\<rbrakk> \<Longrightarrow> pspace_dom (ps(ptr \<mapsto> v)) = pspace_dom ps proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps ptr = Some x; a_type x = a_type v\<rbrakk> \<Longrightarrow> (\<Union>x\<in>dom ps. fst ` obj_relation_cuts (the (if x = ptr then Some v else ps x)) x) = (\<Union>x\<in>dom ps. fst ` obj_relation_cuts (the (ps x)) x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>ps ptr = Some x; a_type x = a_type v; xa \<in> dom ps\<rbrakk> \<Longrightarrow> fst ` obj_relation_cuts (the (if xa = ptr then Some v else ps xa)) xa = fst ` obj_relation_cuts (the (ps xa)) xa proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_type x = a_type v; ps ptr = Some x\<rbrakk> \<Longrightarrow> fst ` obj_relation_cuts v ptr = fst ` obj_relation_cuts x ptr proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma tcb_cte_cases_small:
  "\<lbrakk> tcb_cte_cases v = Some (getF, setF) \<rbrakk>
      \<Longrightarrow> v < 2 ^ tcbBlockSizeBits" by (simp add: tcb_cte_cases_def objBits_defs split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cte_cases v = Some (getF, setF) \<Longrightarrow> v < 2 ^ tcbBlockSizeBits
theory KHeap_R

lemma ctes_of_from_cte_wp_at:
  assumes x: "\<And>P P' p. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> Q s\<rbrace> f \<lbrace>\<lambda>r s. P (cte_wp_at' P' p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (ctes_of s) \<and> Q s\<rbrace> f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" apply (clarsimp simp: valid_def
                 elim!: rsubst[where P=P]
                intro!: ext) apply (case_tac "ctes_of s x", simp_all) apply (drule_tac P1=Not and P'1="\<top>" and p1=x in use_valid [OF _ x],
           simp_all add: cte_wp_at_ctes_of) apply (drule_tac P1=id and P'1="(=) aa" and p1=x in use_valid [OF _ x],
          simp_all add: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s) \<and> Q s\<rbrace> f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); Q s\<rbrakk> \<Longrightarrow> ctes_of s x = ctes_of b x proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); Q s; ctes_of s x = None\<rbrakk> \<Longrightarrow> None = ctes_of b x
 2. \<And>s a b x aa. \<lbrakk>(a, b) \<in> fst (f s); Q s; ctes_of s x = Some aa\<rbrakk> \<Longrightarrow> Some aa = ctes_of b x proof (prove)
goal (1 subgoal):
 1. \<And>s a b x aa. \<lbrakk>(a, b) \<in> fst (f s); Q s; ctes_of s x = Some aa\<rbrakk> \<Longrightarrow> Some aa = ctes_of b x proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma ctes_of_eq_cte_wp_at':
  "cte_wp_at' ((=) cte) x s \<Longrightarrow> ctes_of s x = Some cte" by (simp add: cte_wp_at_ctes_of)

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

lemma tcb_cte_cases_change:
  "tcb_cte_cases x = Some (getF, setF) \<Longrightarrow>
   (\<exists>getF. (\<exists>setF. tcb_cte_cases y = Some (getF, setF)) \<and> getF (setF f tcb) \<noteq> getF tcb)
     = (x = y \<and> f (getF tcb) \<noteq> getF tcb)" apply (rule iffI) apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm) apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cte_cases x = Some (getF, setF) \<Longrightarrow> (\<exists>getF. (\<exists>setF. tcb_cte_cases y = Some (getF, setF)) \<and> getF (setF f tcb) \<noteq> getF tcb) = (x = y \<and> f (getF tcb) \<noteq> getF tcb) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_cte_cases x = Some (getF, setF); \<exists>getF. (\<exists>setF. tcb_cte_cases y = Some (getF, setF)) \<and> getF (setF f tcb) \<noteq> getF tcb\<rbrakk> \<Longrightarrow> x = y \<and> f (getF tcb) \<noteq> getF tcb
 2. \<lbrakk>tcb_cte_cases x = Some (getF, setF); x = y \<and> f (getF tcb) \<noteq> getF tcb\<rbrakk> \<Longrightarrow> \<exists>getF. (\<exists>setF. tcb_cte_cases y = Some (getF, setF)) \<and> getF (setF f tcb) \<noteq> getF tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_cte_cases x = Some (getF, setF); x = y \<and> f (getF tcb) \<noteq> getF tcb\<rbrakk> \<Longrightarrow> \<exists>getF. (\<exists>setF. tcb_cte_cases y = Some (getF, setF)) \<and> getF (setF f tcb) \<noteq> getF tcb proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma cte_level_bits_nonzero [simp]: "0 < cte_level_bits" by (simp add: cte_level_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < cte_level_bits
theory KHeap_R

lemma real_cte_at':
  "real_cte_at' p s \<Longrightarrow> cte_at' p s" by (clarsimp simp add: cte_wp_at_cases' obj_at'_def projectKOs
                         objBits_simps' cte_level_bits_def
                    del: disjCI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. real_cte_at' p s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s
theory KHeap_R

lemma setObject_ct_inv:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

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

lemma setObject_cd_inv:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject t v \<lbrace>\<lambda>rv 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 t ps));
obj' <- updateObject_default v (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_it_inv:
"\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setObject t (v::tcb) \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject_default v (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace> proof (prove)
goal:
No subgoals!