kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_R

lemma objBits_le_obj_bits_api:
  "makeObjectKO dev ty = Some ko \<Longrightarrow>
   objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us" apply (case_tac ty) apply (auto simp: default_arch_object_def pageBits_def archObjSize_def pteBits_def pdeBits_def
                      makeObjectKO_def objBits_simps' APIType_map2_def obj_bits_api_def slot_bits_def
               split: Structures_H.kernel_object.splits arch_kernel_object.splits object_type.splits
                      Structures_H.kernel_object.splits arch_kernel_object.splits apiobject_type.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makeObjectKO dev ty = Some ko \<Longrightarrow> objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>makeObjectKO dev ty = Some ko; ty = Inl a\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us
 2. \<And>b. \<lbrakk>makeObjectKO dev ty = Some ko; ty = Inr b\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us proof (prove)
goal:
No subgoals!
theory Retype_R

lemma foldr_upd_app_if': "foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then (f x) else g x)" apply (induct as) apply simp apply simp apply (rule ext) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then f x else g x) proof (prove)
goal (2 subgoals):
 1. foldr (\<lambda>p ps. ps(p := f p)) [] g = (\<lambda>x. if x \<in> set [] then f x else g x)
 2. \<And>a as. foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then f x else g x) \<Longrightarrow> foldr (\<lambda>p ps. ps(p := f p)) (a # as) g = (\<lambda>x. if x \<in> set (a # as) then f x else g x) proof (prove)
goal (1 subgoal):
 1. \<And>a as. foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then f x else g x) \<Longrightarrow> foldr (\<lambda>p ps. ps(p := f p)) (a # as) g = (\<lambda>x. if x \<in> set (a # as) then f x else g x) proof (prove)
goal (1 subgoal):
 1. \<And>a as. foldr (\<lambda>p ps a. if a = p then f p else ps a) as g = (\<lambda>x. if x \<in> set as then f x else g x) \<Longrightarrow> (\<lambda>b. if b = a then f a else foldr (\<lambda>p ps a. if a = p then f p else ps a) as g b) = (\<lambda>x. if x = a \<or> x \<in> set as then f x else g x) proof (prove)
goal (1 subgoal):
 1. \<And>a as x. foldr (\<lambda>p ps a. if a = p then f p else ps a) as g = (\<lambda>x. if x \<in> set as then f x else g x) \<Longrightarrow> (if x = a then f a else foldr (\<lambda>p ps a. if a = p then f p else ps a) as g x) = (if x = a \<or> x \<in> set as then f x else g x) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma etcb_rel_makeObject: "etcb_relation default_etcb makeObject" apply (simp add: etcb_relation_def default_etcb_def) apply (simp add: makeObject_tcb default_priority_def default_domain_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. etcb_relation default_etcb makeObject proof (prove)
goal (1 subgoal):
 1. default_priority = tcbPriority makeObject \<and> timeSlice = tcbTimeSlice makeObject \<and> default_domain = tcbDomain makeObject proof (prove)
goal:
No subgoals!
theory Retype_R

lemma ekh_at_tcb_at: "valid_etcbs_2 ekh kh \<Longrightarrow> ekh x = Some y  \<Longrightarrow> \<exists>tcb. kh x = Some (TCB tcb)" apply (simp add: valid_etcbs_2_def
                   st_tcb_at_kh_def obj_at_kh_def
                   is_etcb_at'_def obj_at_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs_2 ekh kh; ekh x = Some y\<rbrakk> \<Longrightarrow> \<exists>tcb. kh x = Some (TCB tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr. (\<exists>ko. kh ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekh ptr = Some y); ekh x = Some y\<rbrakk> \<Longrightarrow> \<exists>tcb. kh x = Some (TCB tcb) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma default_etcb_default_domain_futz [simp]:
  "default_etcb\<lparr>tcb_domain := default_domain\<rparr> = default_etcb" unfolding default_etcb_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. default_etcb\<lparr>tcb_domain := default_domain\<rparr> = default_etcb proof (prove)
goal (1 subgoal):
 1. \<lparr>tcb_priority = default_priority, tcb_time_slice = timeSlice, tcb_domain = default_domain\<rparr>\<lparr>tcb_domain := default_domain\<rparr> = \<lparr>tcb_priority = default_priority, tcb_time_slice = timeSlice, tcb_domain = default_domain\<rparr>
theory Retype_R

lemma pspace_no_overlapD':
  "\<lbrakk> ksPSpace s x = Some ko; pspace_no_overlap' p bits s \<rbrakk>
       \<Longrightarrow> {x .. x + 2 ^ objBitsKO ko - 1} \<inter> {p .. (p && ~~ mask bits) + 2 ^ bits - 1} = {}" apply (simp add:pspace_no_overlap'_def) apply (intro impI) apply (elim allE impE) apply (simp add:field_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some ko; pspace_no_overlap' p bits s\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> {p..(p && ~~ mask bits) + 2 ^ bits - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some ko; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> x \<le> (p && ~~ mask bits) + (2 ^ bits - 1) \<longrightarrow> p \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> p \<le> (p && ~~ mask bits) + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> x \<le> (p && ~~ mask bits) + 2 ^ bits - 1 \<longrightarrow> p \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> p \<le> (p && ~~ mask bits) + 2 ^ bits - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some ko; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> x \<le> (p && ~~ mask bits) + (2 ^ bits - 1) \<longrightarrow> p \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> x \<le> x + 2 ^ objBitsKO ko - 1 \<longrightarrow> \<not> p \<le> (p && ~~ mask bits) + (2 ^ bits - 1); x \<le> (p && ~~ mask bits) + 2 ^ bits - 1; p \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1\<rbrakk> \<Longrightarrow> \<not> p \<le> (p && ~~ mask bits) + 2 ^ bits - 1 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ksPSpace s x = Some ko; x \<le> (p && ~~ mask bits) + 2 ^ bits - 1; p \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1\<rbrakk> \<Longrightarrow> ksPSpace s ?x10 = Some ?ko11
 2. \<lbrakk>ksPSpace s x = Some ko; x \<le> (p && ~~ mask bits) + 2 ^ bits - 1; p \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1\<rbrakk> \<Longrightarrow> ?x10 \<le> (p && ~~ mask bits) + (2 ^ bits - 1)
 3. \<lbrakk>ksPSpace s x = Some ko; x \<le> (p && ~~ mask bits) + 2 ^ bits - 1; p \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1\<rbrakk> \<Longrightarrow> p \<le> ?x10 + 2 ^ objBitsKO ?ko11 - 1
 4. \<lbrakk>ksPSpace s x = Some ko; x \<le> (p && ~~ mask bits) + 2 ^ bits - 1; p \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1\<rbrakk> \<Longrightarrow> ?x10 \<le> ?x10 + 2 ^ objBitsKO ?ko11 - 1
 5. \<lbrakk>ksPSpace s x = Some ko; x \<le> (p && ~~ mask bits) + 2 ^ bits - 1; p \<le> x + 2 ^ objBitsKO ko - 1; x \<le> x + 2 ^ objBitsKO ko - 1; \<not> p \<le> (p && ~~ mask bits) + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> \<not> p \<le> (p && ~~ mask bits) + 2 ^ bits - 1 proof (prove)
goal:
No subgoals!
theory Retype_R

lemma ksPSpace_update_gs_eq[simp]:
  "ksPSpace (update_gs ty us ptrs s) = ksPSpace s" by (simp add: update_gs_def
           split: Structures_A.apiobject_type.splits aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace (update_gs ty us ptrs s) = ksPSpace s
theory Retype_R

lemma update_gs_id:
  "tp \<in> no_gs_types \<Longrightarrow> update_gs tp us addrs = id" by (simp add: no_gs_types_def update_gs_def
           split: Structures_A.apiobject_type.splits aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tp \<in> no_gs_types \<Longrightarrow> update_gs tp us addrs = id
theory Retype_R

lemma update_gs_simps[simp]:
  "update_gs Structures_A.apiobject_type.CapTableObject us ptrs =
   gsCNodes_update (\<lambda>cns x. if x \<in> ptrs then Some us else cns x)"
  "update_gs (ArchObject SmallPageObj) us ptrs =
   gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMSmallPage else ups x)"
  "update_gs (ArchObject LargePageObj) us ptrs =
   gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMLargePage else ups x)"
  "update_gs (ArchObject SectionObj) us ptrs =
   gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMSection else ups x)"
  "update_gs (ArchObject SuperSectionObj) us ptrs =
   gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMSuperSection
                               else ups x)" by (simp_all add: update_gs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (update_gs Structures_A.apiobject_type.CapTableObject us ptrs = gsCNodes_update (\<lambda>cns x. if x \<in> ptrs then Some us else cns x) &&& update_gs (ArchObject SmallPageObj) us ptrs = gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMSmallPage else ups x)) &&& update_gs (ArchObject LargePageObj) us ptrs = gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMLargePage else ups x) &&& update_gs (ArchObject SectionObj) us ptrs = gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMSection else ups x) &&& update_gs (ArchObject SuperSectionObj) us ptrs = gsUserPages_update (\<lambda>ups x. if x \<in> ptrs then Some ARMSuperSection else ups x)
theory Retype_R

lemma new_cap_addrs_fold':
  "1 \<le> n \<Longrightarrow>
   map (\<lambda>n. ptr + (n << objBitsKO ko)) [0.e.n - 1] =
   new_cap_addrs (unat n) ptr ko" by (clarsimp simp:new_cap_addrs_def ptr_add_def upto_enum_red'
           shiftl_t2n power_add field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 \<le> n \<Longrightarrow> map (\<lambda>n. ptr + (n << objBitsKO ko)) [0 .e. n - 1] = new_cap_addrs (unat n) ptr ko
theory Retype_R

lemma objBitsKO_gt_0: "0 < objBitsKO ko" apply (case_tac ko) apply (simp_all add: objBits_simps' pageBits_def) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object) apply (simp_all add:archObjSize_def pageBits_def pteBits_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < objBitsKO ko proof (prove)
goal (8 subgoals):
 1. \<And>x1. ko = KOEndpoint x1 \<Longrightarrow> 0 < objBitsKO ko
 2. \<And>x2. ko = KONotification x2 \<Longrightarrow> 0 < objBitsKO ko
 3. ko = KOKernelData \<Longrightarrow> 0 < objBitsKO ko
 4. ko = KOUserData \<Longrightarrow> 0 < objBitsKO ko
 5. ko = KOUserDataDevice \<Longrightarrow> 0 < objBitsKO ko
 6. \<And>x6. ko = KOTCB x6 \<Longrightarrow> 0 < objBitsKO ko
 7. \<And>x7. ko = KOCTE x7 \<Longrightarrow> 0 < objBitsKO ko
 8. \<And>x8. ko = KOArch x8 \<Longrightarrow> 0 < objBitsKO ko proof (prove)
goal (1 subgoal):
 1. \<And>x8. ko = KOArch x8 \<Longrightarrow> 0 < archObjSize x8 proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_object. ko = KOArch arch_kernel_object \<Longrightarrow> 0 < archObjSize arch_kernel_object proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_object x1. \<lbrakk>ko = KOArch arch_kernel_object; arch_kernel_object = KOASIDPool x1\<rbrakk> \<Longrightarrow> 0 < archObjSize arch_kernel_object
 2. \<And>arch_kernel_object x2. \<lbrakk>ko = KOArch arch_kernel_object; arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> 0 < archObjSize arch_kernel_object
 3. \<And>arch_kernel_object x3. \<lbrakk>ko = KOArch arch_kernel_object; arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> 0 < archObjSize arch_kernel_object proof (prove)
goal:
No subgoals!
theory Retype_R

lemma foldr_upd_app_if_eta_futz:
  "foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as = (\<lambda>g x. if x \<in> set as then Some (f x) else g x)" apply (rule ext) apply (rule foldr_upd_app_if) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as = (\<lambda>g x. if x \<in> set as then Some (f x) else g x) proof (prove)
goal (1 subgoal):
 1. \<And>g. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g = (\<lambda>x. if x \<in> set as then Some (f x) else g x) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma awkward_fold_futz:
  "fold (\<lambda>p ekh. ekh(p \<mapsto> the (ekh p)\<lparr>tcb_domain := cur_domain s\<rparr>)) ptrs ekh
 = (\<lambda>x. if x \<in> set ptrs then Some ((the (ekh x))\<lparr>tcb_domain := cur_domain s\<rparr>) else ekh x)" by (induct ptrs arbitrary: ekh) (simp_all add: fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>p ekh. ekh(p \<mapsto> the (ekh p)\<lparr>tcb_domain := cur_domain s\<rparr>)) ptrs ekh = (\<lambda>x. if x \<in> set ptrs then Some (the (ekh x)\<lparr>tcb_domain := cur_domain s\<rparr>) else ekh x)
theory Retype_R

lemma getObject_tcb_gets:
  "getObject addr >>= (\<lambda>x::tcb. gets proj >>= (\<lambda>y. G x y))
 = gets proj >>= (\<lambda>y. getObject addr >>= (\<lambda>x. G x y))" by (auto simp: exec_gets fun_eq_iff intro: bind_apply_cong dest!: in_inv_by_hoareD[OF getObject_inv_tcb])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- getObject addr;
gets proj >>= G x
od = do y <- gets proj;
x <- getObject addr;
G x y
od
theory Retype_R

lemma setObject_tcb_gets_ksCurDomain:
  "setObject addr (tcb::tcb) >>= (\<lambda>_. gets ksCurDomain >>= G)
 = gets ksCurDomain >>= (\<lambda>x. setObject addr tcb >>= (\<lambda>_. G x))" apply (clarsimp simp: exec_gets fun_eq_iff) apply (rule bind_apply_cong) apply simp apply (drule_tac P1="\<lambda>cdom. cdom = ksCurDomain x" in use_valid[OF _ setObject_cd_inv]) apply (simp_all add: exec_gets) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- setObject addr tcb;
gets ksCurDomain >>= G
od = do x <- gets ksCurDomain;
_ <- setObject addr tcb;
G x
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do _ <- setObject addr tcb;
gets ksCurDomain >>= G
od) x = (do _ <- setObject addr tcb;
G (ksCurDomain x)
od) x proof (prove)
goal (2 subgoals):
 1. \<And>x. setObject addr tcb x = setObject addr tcb x
 2. \<And>x rv st. (rv, st) \<in> fst (setObject addr tcb x) \<Longrightarrow> (gets ksCurDomain >>= G) st = G (ksCurDomain x) st proof (prove)
goal (1 subgoal):
 1. \<And>x rv st. (rv, st) \<in> fst (setObject addr tcb x) \<Longrightarrow> (gets ksCurDomain >>= G) st = G (ksCurDomain x) st proof (prove)
goal (2 subgoals):
 1. \<And>x rv st. ksCurDomain x = ksCurDomain x
 2. \<And>x rv st. ksCurDomain st = ksCurDomain x \<Longrightarrow> (gets ksCurDomain >>= G) st = G (ksCurDomain x) st proof (prove)
goal:
No subgoals!
theory Retype_R

lemma modify_ekheap_update_ekheap:
  "modify (\<lambda>s. ekheap_update f s) = do s \<leftarrow> gets ekheap; modify (\<lambda>s'. s'\<lparr>ekheap := f s\<rparr>) od" by (simp add: modify_def gets_def get_def put_def bind_def return_def split_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify (ekheap_update f) = do s <- gets ekheap;
modify (ekheap_update (\<lambda>_. f s))
od
theory Retype_R

lemma retype_ko_wp_at':
  assumes vs: "pspace_aligned' s" "pspace_distinct' s"
     and  pn: "pspace_no_overlap' ptr sz s"
   and cover: "range_cover ptr sz (objBitsKO obj) n"
  shows
  "ko_wp_at' P p (s \<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr obj)
                      (new_cap_addrs n ptr obj) (ksPSpace s)\<rparr>)
     = (if p \<in> set (new_cap_addrs n ptr obj) then P obj
                         else ko_wp_at' P p s)" apply (subst foldr_upd_app_if[folded data_map_insert_def]) apply (rule foldr_update_ko_wp_at' [OF vs]) apply (simp add: retype_aligned_distinct'' [OF vs pn cover])+ apply (rule new_cap_addrs_aligned) using cover apply (simp add:range_cover_def cover) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' P p (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr obj) (new_cap_addrs n ptr obj) (ksPSpace s)\<rparr>) = (if p \<in> set (new_cap_addrs n ptr obj) then P obj else ko_wp_at' P p s) proof (prove)
goal (1 subgoal):
 1. ko_wp_at' P p (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr obj) then Some obj else ksPSpace s x\<rparr>) = (if p \<in> set (new_cap_addrs n ptr obj) then P obj else ko_wp_at' P p s) proof (prove)
goal (3 subgoals):
 1. pspace_aligned' (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr obj) then Some obj else ksPSpace s x\<rparr>)
 2. pspace_distinct' (s\<lparr>ksPSpace := \<lambda>x. if x \<in> set (new_cap_addrs n ptr obj) then Some obj else ksPSpace s x\<rparr>)
 3. \<forall>uu_\<in>set (new_cap_addrs n ptr obj). is_aligned uu_ (objBitsKO obj) proof (prove)
goal (1 subgoal):
 1. \<forall>uu_\<in>set (new_cap_addrs n ptr obj). is_aligned uu_ (objBitsKO obj) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr (objBitsKO obj) proof (prove)
using this:
range_cover ptr sz (objBitsKO obj) n

goal (1 subgoal):
 1. is_aligned ptr (objBitsKO obj) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma retype_obj_at':
  assumes vs: "pspace_aligned' s" "pspace_distinct' s"
     and  pn: "pspace_no_overlap' ptr sz s"
     and cover: "range_cover ptr sz (objBitsKO obj) n"
  shows
  "obj_at' P p (s \<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr obj)
                      (new_cap_addrs n ptr obj) (ksPSpace s)\<rparr>)
     = (if p \<in> set (new_cap_addrs n ptr obj) then (\<exists>ko. projectKO_opt obj = Some ko \<and> P ko)
                         else obj_at' P p s)" unfolding obj_at'_real_def apply (rule retype_ko_wp_at'[OF vs pn cover]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr obj) (new_cap_addrs n ptr obj) (ksPSpace s)\<rparr>) = (if p \<in> set (new_cap_addrs n ptr obj) then \<exists>ko. projectKO_opt obj = Some ko \<and> P ko else obj_at' P p s) proof (prove)
goal (1 subgoal):
 1. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr obj) (new_cap_addrs n ptr obj) (ksPSpace s)\<rparr>) = (if p \<in> set (new_cap_addrs n ptr obj) then \<exists>ko. projectKO_opt obj = Some ko \<and> P ko else ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_ko_at:
  fixes ptr :: word32
  assumes    cover: "range_cover ptr sz ((objBitsKO ko) + gbits) n"
  assumes    not_0: "n\<noteq> 0"
  assumes       pi: "projectKO_opt ko = Some val"
  shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace>
             createObjects ptr n ko gbits
         \<lbrace>\<lambda>r s. \<forall>x \<in> set r. \<forall>offs < 2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace>" by (wp createObjects_ko_at_strg[OF cover not_0 pi],fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. ko_at' val (x + (offs << objBitsKO ko)) s\<rbrace>
theory Retype_R

lemma createObjects_obj_at:
  fixes ptr :: word32 and val :: "'a :: pspace_storable"
  assumes  cover:"range_cover ptr sz ((objBitsKO ko) + gbits) n"
  and      not_0:"n \<noteq> 0"
  and       pi: "\<exists>(val::'a). projectKO_opt ko = Some val"
  shows "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace>
  createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x \<in> set r. \<forall>offs < 2 ^ gbits.
                                     obj_at' (\<lambda>(x::'a). True) (x + (offs << objBitsKO ko)) s\<rbrace>" apply (rule exE[OF pi]) apply (erule_tac val1 = x in
    hoare_post_imp [OF _ createObjects_ko_at [OF cover not_0 ],rotated]) apply (intro allI ballI impI) apply (drule(1) bspec) apply (drule spec, drule(1) mp) apply (clarsimp elim!: obj_at'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. obj_at' (\<lambda>x. True) (x + (offs << objBitsKO ko)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. projectKO_opt ko = Some x \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> valid_pspace' s\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>r s. \<forall>x\<in>set r. \<forall>offs<2 ^ gbits. obj_at' (\<lambda>x. True) (x + (offs << objBitsKO ko)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x rv s. \<forall>xa\<in>set rv. \<forall>offs<2 ^ gbits. ko_at' x (xa + (offs << objBitsKO ko)) s \<Longrightarrow> \<forall>x\<in>set rv. \<forall>offs<2 ^ gbits. obj_at' (\<lambda>x. True) (x + (offs << objBitsKO ko)) s proof (prove)
goal (1 subgoal):
 1. \<And>x rv s xa offs. \<lbrakk>\<forall>xa\<in>set rv. \<forall>offs<2 ^ gbits. ko_at' x (xa + (offs << objBitsKO ko)) s; xa \<in> set rv; offs < 2 ^ gbits\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) (xa + (offs << objBitsKO ko)) s proof (prove)
goal (1 subgoal):
 1. \<And>x rv s xa offs. \<lbrakk>xa \<in> set rv; offs < 2 ^ gbits; \<forall>offs<2 ^ gbits. ko_at' x (xa + (offs << objBitsKO ko)) s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) (xa + (offs << objBitsKO ko)) s proof (prove)
goal (1 subgoal):
 1. \<And>x rv s xa offs. \<lbrakk>xa \<in> set rv; offs < 2 ^ gbits; ko_at' x (xa + (offs << objBitsKO ko)) s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) (xa + (offs << objBitsKO ko)) s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_aligned:
  assumes al: "is_aligned ptr (objBitsKO ko + gbits)"
  and bound :"n < 2 ^ word_bits" "n\<noteq>0"
  and bound':"objBitsKO ko + gbits < word_bits"
  shows "\<lbrace>\<top>\<rbrace> createObjects ptr n ko gbits
         \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. is_aligned x (objBitsKO ko + gbits)\<rbrace>" apply (rule hoare_strengthen_post) apply (rule createObjects_ret[OF bound]) apply (clarsimp dest!: less_two_pow_divD) apply (rule is_aligned_ptr_add_helper[OF al]) apply (simp_all add:bound') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> createObjects ptr n ko gbits \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. is_aligned x (objBitsKO ko + gbits)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> createObjects ptr n ko gbits \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x (objBitsKO ko + gbits) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ objBitsKO ko * 2 ^ gbits)) [0..<n] \<Longrightarrow> \<forall>x\<in>set rv. is_aligned x (objBitsKO ko + gbits) proof (prove)
goal (1 subgoal):
 1. \<And>x. x < n \<Longrightarrow> is_aligned (ptr_add ptr (x * 2 ^ objBitsKO ko * 2 ^ gbits)) (objBitsKO ko + gbits) proof (prove)
goal (4 subgoals):
 1. \<And>x. x < n \<Longrightarrow> objBitsKO ko + gbits < word_bits
 2. \<And>x. x < n \<Longrightarrow> objBitsKO ko + gbits \<le> objBitsKO ko + gbits
 3. \<And>x. x < n \<Longrightarrow> objBitsKO ko + gbits \<le> objBitsKO ko + gbits
 4. \<And>x. x < n \<Longrightarrow> objBitsKO ko + gbits < word_bits proof (prove)
goal:
No subgoals!