kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_AI

lemma honestly_16_10:
  "is_aligned (p :: word32) 10 \<Longrightarrow> p + 16 \<in> {p .. p + 1023}" apply simp apply (intro conjI is_aligned_no_wrap' word_plus_mono_right,
         (assumption | simp add: word_bits_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 10 \<Longrightarrow> p + 0x10 \<in> {p..p + 0x3FF} proof (prove)
goal (1 subgoal):
 1. is_aligned p 10 \<Longrightarrow> p \<le> p + 0x10 \<and> p + 0x10 \<le> p + 0x3FF proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma of_nat_2: "((of_nat (2::nat))::word32) = 2" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat 2 = 2
theory Retype_AI

lemma subset_le_imp_less: "\<not> A \<subseteq> B \<Longrightarrow> \<not> A \<subset> B" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> A \<subseteq> B \<Longrightarrow> \<not> A \<subset> B
theory Retype_AI

lemma non_disjoing_subset: "\<lbrakk>A \<subseteq> B; A \<inter> C \<noteq> {}\<rbrakk> \<Longrightarrow> B \<inter> C \<noteq> {}" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; A \<inter> C \<noteq> {}\<rbrakk> \<Longrightarrow> B \<inter> C \<noteq> {}
theory Retype_AI

lemma pspace_no_overlap_same_type:
  "\<lbrakk>pspace_no_overlap S s; ko_at k p s; a_type ko = a_type k\<rbrakk>
    \<Longrightarrow> pspace_no_overlap S (kheap_update (\<lambda>_. (kheap s)(p \<mapsto> ko)) s)" unfolding pspace_no_overlap_def by (clarsimp simp: obj_at_def obj_bits_T)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap S s; ko_at k p s; a_type ko = a_type k\<rbrakk> \<Longrightarrow> pspace_no_overlap S (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x ko. kheap s x = Some ko \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> S = {}; ko_at k p s; a_type ko = a_type k\<rbrakk> \<Longrightarrow> \<forall>x koa. kheap (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) x = Some koa \<longrightarrow> {x..x + (2 ^ obj_bits koa - 1)} \<inter> S = {}
theory Retype_AI

lemma set_object_no_overlap:
  "\<lbrace>pspace_no_overlap S and obj_at (\<lambda>k. a_type ko = a_type k) p\<rbrace>
  set_object p ko \<lbrace>\<lambda>r. pspace_no_overlap S\<rbrace>" unfolding set_object_def get_object_def apply simp apply wp apply (clarsimp simp del: fun_upd_apply) apply (drule obj_at_ko_atD, erule exE) apply (rule pspace_no_overlap_same_type) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap S and obj_at (\<lambda>k. a_type ko = a_type k) p\<rbrace> set_object p ko \<lbrace>\<lambda>r. pspace_no_overlap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap S and obj_at (\<lambda>k. a_type ko = a_type k) p\<rbrace> do kobj <- do kh <- gets kheap;
assert (kh p \<noteq> None);
return $ the $ kh p
od;
assert (a_type kobj = a_type ko);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
od \<lbrace>\<lambda>r. pspace_no_overlap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap S and obj_at (\<lambda>k. a_type ko = a_type k) p\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = a_type ko);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
od \<lbrace>\<lambda>r. pspace_no_overlap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_no_overlap S and obj_at (\<lambda>k. a_type ko = a_type k) p) s \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type ko \<longrightarrow> pspace_no_overlap S (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pspace_no_overlap S s; obj_at (\<lambda>k. a_type ko = a_type k) p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> pspace_no_overlap S (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y k. \<lbrakk>pspace_no_overlap S s; kheap s p = Some y; a_type y = a_type ko; ko_at k p s \<and> a_type ko = a_type k\<rbrakk> \<Longrightarrow> pspace_no_overlap S (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s y k. \<lbrakk>pspace_no_overlap S s; kheap s p = Some y; a_type y = a_type ko; ko_at k p s \<and> a_type ko = a_type k\<rbrakk> \<Longrightarrow> pspace_no_overlap S s
 2. \<And>s y k. \<lbrakk>pspace_no_overlap S s; kheap s p = Some y; a_type y = a_type ko; ko_at k p s \<and> a_type ko = a_type k\<rbrakk> \<Longrightarrow> ko_at (?k21 s y k) p s
 3. \<And>s y k. \<lbrakk>pspace_no_overlap S s; kheap s p = Some y; a_type y = a_type ko; ko_at k p s \<and> a_type ko = a_type k\<rbrakk> \<Longrightarrow> a_type ko = a_type (?k21 s y k) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma set_cap_no_overlap:
  "\<lbrace>pspace_no_overlap S\<rbrace> set_cap cap cte \<lbrace>\<lambda>r. pspace_no_overlap S\<rbrace>" unfolding set_cap_def by (wpsimp wp: set_object_no_overlap get_object_wp
           simp: split_beta obj_at_def a_type_def wf_cs_upd [unfolded fun_upd_def])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap S\<rbrace> set_cap cap cte \<lbrace>\<lambda>r. pspace_no_overlap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap S\<rbrace> case cte of (oref, cref) \<Rightarrow> do obj <- get_object oref;
(case obj of CNode sz cn \<Rightarrow> if cref \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(cref \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object oref
od \<lbrace>\<lambda>r. pspace_no_overlap S\<rbrace>
theory Retype_AI

lemma null_filter_same:
  "cps p \<noteq> Some cap.NullCap \<Longrightarrow> null_filter cps p = cps p" by (simp add: null_filter_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cps p \<noteq> Some NullCap \<Longrightarrow> null_filter cps p = cps p
theory Retype_AI

lemma unsafe_rep2:
  "if_unsafe_then_cap =
    (\<lambda>s. if_unsafe_then_cap2 (null_filter (caps_of_state s)) (interrupt_irq_node s))" apply (simp only: if_unsafe_then_cap2_def o_def) apply (subst P_null_filter_caps_of_cte_wp_at, simp)+ apply (simp add: null_filter_same [where cps="caps_of_state s" for s, OF cte_wp_at_not_Null]) apply (fastforce simp: if_unsafe_then_cap2_def cte_wp_at_caps_of_state
                        if_unsafe_then_cap_def ex_cte_cap_wp_to_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap = (\<lambda>s. if_unsafe_then_cap2 (null_filter (caps_of_state s)) (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap = (\<lambda>s. \<forall>cref. null_filter (caps_of_state s) cref \<noteq> None \<and> the (null_filter (caps_of_state s) cref) \<noteq> NullCap \<longrightarrow> (\<exists>cref'. null_filter (caps_of_state s) cref' \<noteq> None \<and> cref \<in> cte_refs (the (null_filter (caps_of_state s) cref')) (interrupt_irq_node s) \<and> appropriate_cte_cap (the (null_filter (caps_of_state s) cref)) (the (null_filter (caps_of_state s) cref')))) proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap = (\<lambda>s. \<forall>cref. cte_wp_at (\<lambda>a. a \<noteq> NullCap) cref s \<longrightarrow> (\<exists>cref'. cte_wp_at (\<lambda>a. cref \<in> cte_refs a (interrupt_irq_node s) \<and> appropriate_cte_cap (the (null_filter (caps_of_state s) cref)) a) cref' s)) proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap = (\<lambda>s. \<forall>a b. cte_wp_at (\<lambda>a. a \<noteq> NullCap) (a, b) s \<longrightarrow> (\<exists>aa ba. cte_wp_at (\<lambda>c. (a, b) \<in> cte_refs c (interrupt_irq_node s) \<and> appropriate_cte_cap (the (caps_of_state s (a, b))) c) (aa, ba) s)) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma conj_cong2: "\<lbrakk>P = P'; P \<Longrightarrow> Q = Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = P'; P \<Longrightarrow> Q = Q'\<rbrakk> \<Longrightarrow> (P \<and> Q) = (P' \<and> Q')
theory Retype_AI

lemma valid_mdb_rep3:
  "valid_mdb = (\<lambda>s. \<exists>m r. cdt s = m \<and> is_original_cap s = r \<and> valid_mdb2 (null_filter (caps_of_state s)) m r)" by (simp add: valid_mdb_rep2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb = (\<lambda>s. \<exists>m r. cdt s = m \<and> is_original_cap s = r \<and> valid_mdb2 (null_filter (caps_of_state s)) m r)
theory Retype_AI

lemma retype_region_mdb[wp]:
  "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>" apply (simp add: retype_region_def split del: if_split cong: if_cong) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do y <- when (ty \<noteq> Untyped) (do kh <- gets kheap;
y <- do_extended_op (retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) ty);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object ty dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) kh))
od);
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n])
od \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma retype_region_revokable[wp]:
  "\<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. P (is_original_cap s)\<rbrace>" apply (simp add: retype_region_def split del: if_split cong: if_cong) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. P (is_original_cap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do y <- when (ty \<noteq> Untyped) (do kh <- gets kheap;
y <- do_extended_op (retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) ty);
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object ty dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]) kh))
od);
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n])
od \<lbrace>\<lambda>rv s. P (is_original_cap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma pspace_no_overlap_obj_not_in_range:
  "\<lbrakk> pspace_no_overlap S s; obj_at P ptr' s;
       pspace_aligned s; valid_objs s \<rbrakk>
     \<Longrightarrow> ptr' \<notin> S" apply (clarsimp simp add: pspace_no_overlap_def obj_at_def) apply (elim allE, drule(1) mp) apply (simp add: field_simps) apply (drule_tac x=ptr' in eqset_imp_iff) apply (erule pspace_alignedE, erule domI) apply (drule valid_obj_sizes, erule ranI) apply (clarsimp simp: add_diff_eq[symmetric]) apply (simp add: is_aligned_no_wrap') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap S s; obj_at P ptr' s; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> ptr' \<notin> S proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>\<forall>x ko. kheap s x = Some ko \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> S = {}; pspace_aligned s; valid_objs s; kheap s ptr' = Some ko; P ko; ptr' \<in> S\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_aligned s; valid_objs s; kheap s ptr' = Some ko; P ko; ptr' \<in> S; {ptr'..ptr' + (2 ^ obj_bits ko - 1)} \<inter> S = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_aligned s; valid_objs s; kheap s ptr' = Some ko; P ko; ptr' \<in> S; {ptr'..ptr' + 2 ^ obj_bits ko - 1} \<inter> S = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_aligned s; valid_objs s; kheap s ptr' = Some ko; P ko; ptr' \<in> S; (ptr' \<in> {ptr'..ptr' + 2 ^ obj_bits ko - 1} \<inter> S) = (ptr' \<in> {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs s; kheap s ptr' = Some ko; P ko; ptr' \<in> S; (ptr' \<in> {ptr'..ptr' + 2 ^ obj_bits ko - 1} \<inter> S) = (ptr' \<in> {}); is_aligned ptr' (obj_bits (the (kheap s ptr')))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>kheap s ptr' = Some ko; P ko; ptr' \<in> S; (ptr' \<in> {ptr'..ptr' + 2 ^ obj_bits ko - 1} \<inter> S) = (ptr' \<in> {}); is_aligned ptr' (obj_bits (the (kheap s ptr'))); obj_bits ko < word_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>kheap s ptr' = Some ko; P ko; ptr' \<in> S; \<not> ptr' \<le> ptr' + (2 ^ obj_bits ko - 1); is_aligned ptr' (obj_bits ko); obj_bits ko < word_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma obj_at_kheap_trans_state[simp]:"obj_at P ptr (kheap_update f (trans_state f' s)) = obj_at P ptr (kheap_update f s)" apply (simp only: trans_state_update[symmetric] more_update.obj_at_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P ptr (kheap_update f (trans_state f' s)) = obj_at P ptr (kheap_update f s) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma retype_region_obj_at_other:
  assumes ptrv: "ptr \<notin> set (retype_addrs ptr' ty n us)"
  shows "\<lbrace>obj_at P ptr\<rbrace> retype_region ptr' n us ty dev \<lbrace>\<lambda>r. obj_at P ptr\<rbrace>" using ptrv unfolding retype_region_def retype_addrs_def apply (simp only: foldr_upd_app_if fun_app_def K_bind_def) apply (wpsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at P ptr\<rbrace> retype_region ptr' n us ty dev \<lbrace>\<lambda>r. obj_at P ptr\<rbrace> proof (prove)
using this:
ptr \<notin> set (retype_addrs ptr' ty n us)

goal (1 subgoal):
 1. \<lbrace>obj_at P ptr\<rbrace> retype_region ptr' n us ty dev \<lbrace>\<lambda>r. obj_at P ptr\<rbrace> proof (prove)
using this:
ptr \<notin> set (map (\<lambda>p. ptr_add ptr' (p * 2 ^ obj_bits_api ty us)) [0..<n])

goal (1 subgoal):
 1. \<lbrace>obj_at P ptr\<rbrace> do obj_size <- return $ 2 ^ obj_bits_api ty us;
ptrs <- return $ map (\<lambda>p. ptr_add ptr' (p * obj_size)) [0..<n];
when (ty \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object ty dev us)) ptrs kh;
do_extended_op (retype_region_ext ptrs ty);
modify $ kheap_update (K kh')
od);
return $ ptrs
od \<lbrace>\<lambda>r. obj_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. ptr \<notin> set (map (\<lambda>p. ptr_add ptr' (p * 2 ^ obj_bits_api ty us)) [0..<n]) \<Longrightarrow> \<lbrace>obj_at P ptr\<rbrace> do obj_size <- return (2 ^ obj_bits_api ty us);
ptrs <- return (map (\<lambda>p. ptr_add ptr' (p * obj_size)) [0..<n]);
y <- when (ty \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return (\<lambda>x. if x \<in> set ptrs then Some (default_object ty dev us) else kh x);
y <- do_extended_op (retype_region_ext ptrs ty);
modify (kheap_update (K kh'))
od);
return ptrs
od \<lbrace>\<lambda>r. obj_at P ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma retype_region_obj_at_other3:
  "\<lbrace>\<lambda>s. pspace_no_overlap_range_cover ptr sz s \<and> obj_at P p s \<and> range_cover ptr sz (obj_bits_api ty us) n
           \<and> valid_objs s \<and> pspace_aligned s\<rbrace>
     retype_region ptr n us ty dev
   \<lbrace>\<lambda>rv. obj_at P p\<rbrace>" apply (rule hoare_pre) apply (rule retype_region_obj_at_other2) apply clarsimp apply (drule subsetD [rotated, OF _ retype_addrs_subset_ptr_bits]) apply simp apply (drule(3) pspace_no_overlap_obj_not_in_range) apply (simp add: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> obj_at P p s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> valid_objs s \<and> pspace_aligned s\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. obj_at P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. obj_at P p\<rbrace>
 2. \<And>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> obj_at P p s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> valid_objs s \<and> pspace_aligned s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> obj_at P p s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> valid_objs s \<and> pspace_aligned s \<Longrightarrow> p \<notin> set (retype_addrs ptr ty n us) \<and> obj_at P p s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; obj_at P p s; range_cover ptr sz (obj_bits_api ty us) n; valid_objs s; pspace_aligned s; p \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; obj_at P p s; range_cover ptr sz (obj_bits_api ty us) n; valid_objs s; pspace_aligned s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz9 s) (obj_bits_api ty us) n
 2. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; obj_at P p s; range_cover ptr sz (obj_bits_api ty us) n; valid_objs s; pspace_aligned s; p \<in> up_aligned_area ptr (?sz9 s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; obj_at P p s; range_cover ptr sz (obj_bits_api ty us) n; valid_objs s; pspace_aligned s; p \<in> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_at P p s; range_cover ptr sz (obj_bits_api ty us) n; valid_objs s; pspace_aligned s; p \<in> up_aligned_area ptr sz; p \<notin> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma retype_region_st_tcb_at:
  "\<lbrace>\<lambda>(s::'state_ext::state_ext state). pspace_no_overlap_range_cover ptr' sz s \<and> pred_tcb_at proj P t s \<and> range_cover ptr' sz (obj_bits_api ty us) n
          \<and> valid_objs s \<and> pspace_aligned s\<rbrace>
     retype_region ptr' n us ty dev \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" by (simp add: retype_region_obj_at_other3 pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap (up_aligned_area ptr' sz) s \<and> pred_tcb_at proj P t s \<and> range_cover ptr' sz (obj_bits_api ty us) n \<and> valid_objs s \<and> pspace_aligned s\<rbrace> retype_region ptr' n us ty dev \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>
theory Retype_AI

lemma retype_addrs_mem_sz_0_is_ptr:
  assumes "x \<in> set (retype_addrs ptr ty n us)"
  and     "n = 0"
  shows   "x = ptr" using assms unfolding retype_addrs_def by (clarsimp simp: ptr_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = ptr proof (prove)
using this:
x \<in> set (retype_addrs ptr ty n us)
n = 0

goal (1 subgoal):
 1. x = ptr proof (prove)
using this:
x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n])
n = 0

goal (1 subgoal):
 1. x = ptr
theory Retype_AI

lemma retype_addrs_obj_range_subset:
  "\<lbrakk>  p \<in> set (retype_addrs ptr ty n us);
      range_cover ptr sz (obj_bits (default_object ty dev us)) n;
  ty \<noteq> Untyped \<rbrakk>
  \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {ptr..(ptr && ~~ mask sz) + (2^sz - 1)}" by(simp add: obj_range_def obj_bits_api_default_object[symmetric]
                retype_addrs_range_subset p_assoc_help[symmetric]
           del: atLeastatMost_subset_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits (default_object ty dev us)) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> up_aligned_area ptr sz
theory Retype_AI

lemma retype_addrs_mem_subset_ptr_bits:
  assumes cover:"range_cover ptr sz (obj_bits_api ty us) n"
  and tynunt: "ty \<noteq> Untyped"
  and     xv: "x \<in> set (retype_addrs ptr ty n us)"
  shows "{x .. x + (2 ^ obj_bits_api ty us - 1)} \<subseteq> {ptr .. (ptr && ~~ mask sz) + (2 ^ sz - 1)}" apply (insert cover) using retype_addrs_obj_range_subset [OF xv _ tynunt] by (simp add: obj_bits_dev_irr tynunt obj_range_def field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits_api ty us - 1)} \<subseteq> up_aligned_area ptr sz proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> {x..x + (2 ^ obj_bits_api ty us - 1)} \<subseteq> up_aligned_area ptr sz proof (prove)
using this:
range_cover ptr ?sz (obj_bits (default_object ty ?dev us)) n \<Longrightarrow> obj_range x (default_object ty ?dev us) \<subseteq> up_aligned_area ptr ?sz

goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> {x..x + (2 ^ obj_bits_api ty us - 1)} \<subseteq> up_aligned_area ptr sz