kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_AC

lemma pas_refined_detype:
  "pas_refined aag s \<Longrightarrow> pas_refined aag (detype R s)" apply (rule pas_refined_by_subsets) apply (blast intro!: sta_detype sata_detype sita_detype interrupt_irq_node_detype dtsa_detype)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined aag s \<Longrightarrow> pas_refined aag (detype R s) proof (prove)
goal (6 subgoals):
 1. pas_refined aag s \<Longrightarrow> pas_refined aag ?s
 2. pas_refined aag s \<Longrightarrow> state_objs_to_policy (detype R s) \<subseteq> state_objs_to_policy ?s
 3. pas_refined aag s \<Longrightarrow> state_asids_to_policy aag (detype R s) \<subseteq> state_asids_to_policy aag ?s
 4. pas_refined aag s \<Longrightarrow> state_irqs_to_policy aag (detype R s) \<subseteq> state_irqs_to_policy aag ?s
 5. pas_refined aag s \<Longrightarrow> domains_of_state (detype R s) \<subseteq> domains_of_state ?s
 6. pas_refined aag s \<Longrightarrow> interrupt_irq_node (detype R s) = interrupt_irq_node ?s proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma delete_objects_respects[wp]:
  "\<lbrace>\<lambda>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and>
        word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace>
   delete_objects ptr bits
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: delete_objects_def) apply (rule_tac seq_ext) apply (rule hoare_triv[of P _ "%_. P" for P]) apply (wp dmo_freeMemory_respects | simp)+ by (fastforce simp: ptr_range_def intro!: detype_integrity)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace> do y <- do_machine_op (freeMemory ptr bits);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>?B\<rbrace>
 2. \<And>y. \<lbrace>?B y\<rbrace> modify (detype {ptr..ptr + 2 ^ bits - 1}) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>_ s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace>
 2. \<And>y. \<lbrace>\<lambda>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p)\<rbrace> modify (detype {ptr..ptr + 2 ^ bits - 1}) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. integrity aag X st s \<and> is_aligned ptr bits \<and> bits < word_bits \<and> word_size_bits \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p) \<Longrightarrow> integrity aag X st (detype {ptr..ptr + 2 ^ bits - 1} s)
theory Retype_AC

lemma integrity_irq_state_independent[intro!, simp]:
  "integrity x y z (s\<lparr>machine_state :=
                      machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) =
   integrity x y z s" by (simp add: integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity x y z (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = integrity x y z s
theory Retype_AC

lemma obj_refs_default':
  "is_aligned oref (obj_bits_api tp sz)
   \<Longrightarrow> obj_refs_ac (default_cap tp oref sz dev) \<subseteq> ptr_range oref (obj_bits_api tp sz)" by (cases tp; auto simp: ptr_range_memI obj_bits_api_def dest: rev_subsetD[OF _ aobj_refs'_default'])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned oref (obj_bits_api tp sz) \<Longrightarrow> obj_refs_ac (default_cap tp oref sz dev) \<subseteq> ptr_range oref (obj_bits_api tp sz)
theory Retype_AC

lemma ts_eq[simp]: "thread_st_auth s' = thread_st_auth s" apply (rule ext) apply (simp add: s'_def ps_def thread_st_auth_def get_tcb_def orthr tcb_states_of_state_def
            split: option.split Structures_A.kernel_object.split) apply (simp add: default_object_def default_tcb_def tyunt
            split: Structures_A.apiobject_type.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_st_auth s' = thread_st_auth s proof (prove)
goal (1 subgoal):
 1. \<And>x. thread_st_auth s' x = thread_st_auth s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x2. default_object ty dev us = TCB x2 \<longrightarrow> kheap s x = None \<longrightarrow> x \<in> set (retype_addrs ptr ty n us) \<longrightarrow> tcb_st_to_auth (tcb_state x2) = {} proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma bas_eq[simp]: "thread_bound_ntfns s' = thread_bound_ntfns s" apply (rule ext) apply (simp add: s'_def ps_def thread_bound_ntfns_def get_tcb_def orthr tcb_states_of_state_def
            split: option.split Structures_A.kernel_object.split) apply (simp add: default_object_def default_tcb_def tyunt
            split: Structures_A.apiobject_type.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_bound_ntfns s' = thread_bound_ntfns s proof (prove)
goal (1 subgoal):
 1. \<And>x. thread_bound_ntfns s' x = thread_bound_ntfns s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x2. default_object ty dev us = TCB x2 \<longrightarrow> kheap s x = None \<longrightarrow> x \<in> set (retype_addrs ptr ty n us) \<longrightarrow> tcb_bound_notification x2 = None proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma domains_of_state: "domains_of_state s' \<subseteq> domains_of_state s" unfolding s'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. domains_of_state s' \<subseteq> domains_of_state s proof (prove)
goal (1 subgoal):
 1. domains_of_state (s\<lparr>kheap := ps\<rparr>) \<subseteq> domains_of_state s
theory Retype_AC

lemma cte_wp_at_pres:
  "cte_wp_at P p s \<Longrightarrow> cte_wp_at P p s'" unfolding cte_wp_at_cases s'_def ps_def apply (erule disjE) apply (clarsimp simp: well_formed_cnode_n_def orthr)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p s \<Longrightarrow> cte_wp_at P p s' proof (prove)
goal (1 subgoal):
 1. (\<exists>sz fun cap. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap \<and> P cap) \<or> (\<exists>tcb get set restr. kheap s (fst p) = Some (TCB tcb) \<and> tcb_cap_cases (snd p) = Some (get, set, restr) \<and> P (get tcb)) \<Longrightarrow> (\<exists>sz fun cap. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap \<and> P cap) \<or> (\<exists>tcb get seta restr. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (TCB tcb) \<and> tcb_cap_cases (snd p) = Some (get, seta, restr) \<and> P (get tcb)) proof (prove)
goal (2 subgoals):
 1. \<exists>sz fun cap. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap \<and> P cap \<Longrightarrow> (\<exists>sz fun cap. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap \<and> P cap) \<or> (\<exists>tcb get seta restr. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (TCB tcb) \<and> tcb_cap_cases (snd p) = Some (get, seta, restr) \<and> P (get tcb))
 2. \<exists>tcb get set restr. kheap s (fst p) = Some (TCB tcb) \<and> tcb_cap_cases (snd p) = Some (get, set, restr) \<and> P (get tcb) \<Longrightarrow> (\<exists>sz fun cap. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some cap \<and> P cap) \<or> (\<exists>tcb get seta restr. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (TCB tcb) \<and> tcb_cap_cases (snd p) = Some (get, seta, restr) \<and> P (get tcb)) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma caps_of_state_pres:
  "caps_of_state s p = Some cap \<Longrightarrow> caps_of_state s' p = Some cap" using cte_wp_at_pres by (simp add: F)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s p = Some cap \<Longrightarrow> caps_of_state s' p = Some cap proof (prove)
using this:
cte_wp_at ?P ?p s \<Longrightarrow> cte_wp_at ?P ?p s'

goal (1 subgoal):
 1. caps_of_state s p = Some cap \<Longrightarrow> caps_of_state s' p = Some cap
theory Retype_AC

lemma retype_region_ext_kheap_update:
  "\<lbrace>Q xs and R xs\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. Q xs\<rbrace>
   \<Longrightarrow> \<lbrace>\<lambda>s. Q xs (kheap_update f s) \<and> R xs (kheap_update f s)\<rbrace>
       retype_region_ext xs ty
       \<lbrace>\<lambda>_ s. Q xs (kheap_update f s)\<rbrace>" apply (clarsimp simp: valid_def retype_region_ext_def) apply (erule_tac x="kheap_update f s" in allE) apply (clarsimp simp: split_def bind_def gets_def get_def return_def modify_def put_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q xs and R xs\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. Q xs\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. Q xs (kheap_update f s) \<and> R xs (kheap_update f s)\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_ s. Q xs (kheap_update f s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<forall>s. Q xs s \<and> R xs s \<longrightarrow> (\<forall>x\<in>fst ((do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext ty cdom)) xs ekh))
od) s). case x of (r, x) \<Rightarrow> Q xs x); ((), b) \<in> fst ((do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext ty cdom)) xs ekh))
od) s); Q xs (kheap_update f s); R xs (kheap_update f s)\<rbrakk> \<Longrightarrow> Q xs (kheap_update f b) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst ((do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext ty cdom)) xs ekh))
od) s); Q xs (kheap_update f s); R xs (kheap_update f s); Q xs (kheap_update f s) \<and> R xs (kheap_update f s) \<longrightarrow> (\<forall>x\<in>fst ((do ekh <- gets ekheap;
cdom <- gets cur_domain;
modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext ty cdom)) xs ekh))
od) (kheap_update f s)). case x of (r, x) \<Rightarrow> Q xs x)\<rbrakk> \<Longrightarrow> Q xs (kheap_update f b) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma pas_refined_tcb_domain_map_wellformed':
  assumes tdmw: "\<lbrace>tcb_domain_map_wellformed aag and P\<rbrace> f \<lbrace>\<lambda>_. tcb_domain_map_wellformed aag\<rbrace>"
  shows "\<lbrace>pas_refined aag and P\<rbrace> f \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: pas_refined_def) apply (wp tdmw) apply (wp lift_inv) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and P\<rbrace> f \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and P\<rbrace> f \<lbrace>\<lambda>_ s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'12\<rbrace> f \<lbrace>\<lambda>rv s. state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrace>
 2. \<And>s. ((\<lambda>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and P) s \<Longrightarrow> pas_wellformed aag \<and> irq_map_wellformed aag s \<and> (tcb_domain_map_wellformed aag and P) s \<and> ?P'12 s proof (prove)
goal (2 subgoals):
 1. \<And>s g. (state_objs_in_policy aag (trans_state g s) \<and> state_asids_to_policy aag (trans_state g s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag (trans_state g s) \<subseteq> pasPolicy aag) = (state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag)
 2. \<And>s. ((\<lambda>s. pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) and P) s \<Longrightarrow> pas_wellformed aag \<and> irq_map_wellformed aag s \<and> (tcb_domain_map_wellformed aag and P) s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma pspace_no_overlap_msu[simp]:
  "pspace_no_overlap S (machine_state_update f s) = pspace_no_overlap S s" by (clarsimp simp: pspace_no_overlap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap S (machine_state_update f s) = pspace_no_overlap S s
theory Retype_AC

lemma descendants_range_in_msu[simp]:
  "descendants_range_in S slot (machine_state_update f s) = descendants_range_in S slot s" by (clarsimp simp: descendants_range_in_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_range_in S slot (machine_state_update f s) = descendants_range_in S slot s
theory Retype_AC

lemma cte_wp_at_sym:
  "cte_wp_at (\<lambda> c. c = cap) slot s = cte_wp_at ((=) cap) slot s" by (simp add: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>c. c = cap) slot s = cte_wp_at ((=) cap) slot s
theory Retype_AC

lemma untyped_slots_not_in_untyped_range:
  "\<lbrakk> invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s;
     is_untyped_cap cap; S = untyped_range cap; T \<subseteq> S\<rbrakk>
     \<Longrightarrow> fst slot \<notin> T" apply (erule contra_subsetD) proof - assume i: "invs s" and
         dr: "descendants_range_in S slot s" and
         ct: "cte_wp_at ((=) cap) slot s" and
         ut: "is_untyped_cap cap" and
          r: "S = untyped_range cap" hence dt: "detype_locale cap slot s" by (simp add: detype_locale_def descendants_range_def2 invs_untyped_children) show "fst slot \<notin> S" apply - apply (insert r) apply (simp, rule detype_locale.non_null_present[OF dt]) apply (insert ct ut) apply (case_tac cap, simp_all) apply (auto simp: cte_wp_at_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s; is_untyped_cap cap; S = untyped_range cap; T \<subseteq> S\<rbrakk> \<Longrightarrow> fst slot \<notin> T proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s; is_untyped_cap cap; S = untyped_range cap\<rbrakk> \<Longrightarrow> fst slot \<notin> S proof (state)
goal (1 subgoal):
 1. \<lbrakk>invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s; is_untyped_cap cap; S = untyped_range cap\<rbrakk> \<Longrightarrow> fst slot \<notin> S proof (state)
this:
invs s
descendants_range_in S slot s
cte_wp_at ((=) cap) slot s
is_untyped_cap cap
S = untyped_range cap

goal (1 subgoal):
 1. \<lbrakk>invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s; is_untyped_cap cap; S = untyped_range cap\<rbrakk> \<Longrightarrow> fst slot \<notin> S proof (prove)
using this:
invs s
descendants_range_in S slot s
cte_wp_at ((=) cap) slot s
is_untyped_cap cap
S = untyped_range cap

goal (1 subgoal):
 1. detype_locale cap slot s proof (state)
this:
detype_locale cap slot s

goal (1 subgoal):
 1. \<lbrakk>invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s; is_untyped_cap cap; S = untyped_range cap\<rbrakk> \<Longrightarrow> fst slot \<notin> S proof (prove)
goal (1 subgoal):
 1. fst slot \<notin> S proof (prove)
goal (1 subgoal):
 1. fst slot \<notin> S proof (prove)
goal (1 subgoal):
 1. S = untyped_range cap \<Longrightarrow> fst slot \<notin> S proof (prove)
goal (1 subgoal):
 1. S = untyped_range cap \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = untyped_range cap; cte_wp_at ((=) cap) slot s; is_untyped_cap cap\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) slot s proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24. \<lbrakk>S = {x22..x22 + 2 ^ x23 - 1}; cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) slot s; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) slot s proof (prove)
goal:
No subgoals! proof (state)
this:
fst slot \<notin> S

goal:
No subgoals!
theory Retype_AC

lemma descendants_range_in_detype_ex:
  "\<lbrakk> invs s; descendants_range_in S slot s; \<exists> cap. cte_wp_at ((=) cap) slot s \<and>
     is_untyped_cap cap \<and> S = untyped_range cap; T \<subseteq> S \<rbrakk>
     \<Longrightarrow> descendants_range_in T slot (detype S s)" apply clarsimp apply (blast intro: descendants_range_in_detype) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; descendants_range_in S slot s; \<exists>cap. cte_wp_at ((=) cap) slot s \<and> is_untyped_cap cap \<and> S = untyped_range cap; T \<subseteq> S\<rbrakk> \<Longrightarrow> descendants_range_in T slot (detype S s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; descendants_range_in (untyped_range cap) slot s; T \<subseteq> untyped_range cap; cte_wp_at ((=) cap) slot s; is_untyped_cap cap; S = untyped_range cap\<rbrakk> \<Longrightarrow> descendants_range_in T slot (detype (untyped_range cap) s) proof (prove)
goal:
No subgoals!
theory Retype_AC

lemma descendants_range_in_detype_ex_strengthen:
  "(invs s \<and> descendants_range_in S slot s \<and> T \<subseteq> S \<and>
    (\<exists>cap. cte_wp_at ((=) cap) slot s \<and> is_untyped_cap cap \<and> S = untyped_range cap))
   \<longrightarrow> descendants_range_in T slot (detype S s)" by (blast intro: descendants_range_in_detype_ex)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<and> descendants_range_in S slot s \<and> T \<subseteq> S \<and> (\<exists>cap. cte_wp_at ((=) cap) slot s \<and> is_untyped_cap cap \<and> S = untyped_range cap) \<longrightarrow> descendants_range_in T slot (detype S s)
theory Retype_AC

lemma untyped_cap_aligned:
  "\<lbrakk> cte_wp_at ((=) (UntypedCap dev word sz idx)) slot s; valid_objs s \<rbrakk>
     \<Longrightarrow> is_aligned word sz" by (fastforce dest: cte_wp_at_valid_objs_valid_cap simp: valid_cap_def cap_aligned_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev word sz idx)) slot s; valid_objs s\<rbrakk> \<Longrightarrow> is_aligned word sz
theory Retype_AC

lemma delete_objects_descendants_range_in'':
  "\<lbrace>invs and (\<lambda> s :: det_ext state. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s)
         and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>
   delete_objects word2 sz
   \<lbrace>\<lambda>_. descendants_range_in {word2..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot\<rbrace>" apply (clarsimp simp: valid_def) apply (frule untyped_cap_aligned, fastforce) apply (clarsimp) apply (erule use_valid) apply (wp delete_objects_descendants_range_in' | clarsimp | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace> delete_objects word2 sz \<lbrace>\<lambda>_. descendants_range_in {word2..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s\<rbrakk> \<Longrightarrow> descendants_range_in {word2..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot b proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; is_aligned word2 sz\<rbrakk> \<Longrightarrow> descendants_range_in {word2..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot b proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; is_aligned word2 sz\<rbrakk> \<Longrightarrow> descendants_range_in {word2..word2 + 2 ^ sz - 1} slot b proof (prove)
goal (2 subgoals):
 1. \<And>s b idx. \<lbrakk>invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; is_aligned word2 sz\<rbrakk> \<Longrightarrow> \<lbrace>?P18 s b idx\<rbrace> delete_objects word2 sz \<lbrace>\<lambda>a. descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>
 2. \<And>s b idx. \<lbrakk>invs s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; is_aligned word2 sz\<rbrakk> \<Longrightarrow> ?P18 s b idx s proof (prove)
goal:
No subgoals!