kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_AI

lemma (in Detype_AI) mapM_storeWord_clear_um:
  "is_aligned p n \<Longrightarrow> word_size_bits\<le>n \<Longrightarrow> n<=word_bits \<Longrightarrow>
   do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [p, p + word_size .e. p + 2 ^ n - 1]) =
   modify (clear_um {x.  \<exists>k. x = p + of_nat k \<and> k < 2 ^ n})" apply (simp add: mapM_x_storeWord_step) apply (rule ext) apply (simp add: do_machine_op_def select_f_def split_def simpler_modify_def
                   simpler_gets_def bind_def return_def clear_um_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; word_size_bits \<le> n; n \<le> word_bits\<rbrakk> \<Longrightarrow> do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [p , p + word_size .e. p + 2 ^ n - 1]) = modify (clear_um {p + word_of_nat k |k. k < 2 ^ n}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; word_size_bits \<le> n; n \<le> word_bits\<rbrakk> \<Longrightarrow> do_machine_op (modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = p + word_of_nat k \<and> k < 2 ^ n then 0 else m x))) = modify (clear_um {p + word_of_nat k |k. k < 2 ^ n}) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p n; word_size_bits \<le> n; n \<le> word_bits\<rbrakk> \<Longrightarrow> do_machine_op (modify (underlying_memory_update (\<lambda>m x. if \<exists>k. x = p + word_of_nat k \<and> k < 2 ^ n then 0 else m x))) x = modify (clear_um {p + word_of_nat k |k. k < 2 ^ n}) x proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma intvl_range_conv:
  "\<lbrakk>is_aligned (ptr :: 'a :: len word) bits; bits \<le> len_of TYPE('a)\<rbrakk> \<Longrightarrow>
   {x. \<exists>k. x = ptr + of_nat k \<and> k < 2 ^ bits} = {ptr .. ptr + 2 ^ bits - 1}" by (rule set_eqI) (simp add: intvl_range_conv')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> {ptr + word_of_nat k |k. k < 2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}
theory Detype_AI

lemma gets_modify_def:
  "gets f >>= (\<lambda>x. modify (g x)) = modify (\<lambda>s. g (f s) s)" by (simp add: simpler_gets_def simpler_modify_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- gets f;
modify (g x)
od = modify (\<lambda>s. g (f s) s)
theory Detype_AI

lemma valid_pspace_well_formed_cnode[intro?]:
  "\<lbrakk>valid_pspace s; kheap s x = Some (CNode sz ct)\<rbrakk> \<Longrightarrow> well_formed_cnode_n sz ct" by (erule (1) well_formed_cnode_valid_cs_size [OF valid_cs_sizeI])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace s; kheap s x = Some (CNode sz ct)\<rbrakk> \<Longrightarrow> well_formed_cnode_n sz ct
theory Detype_AI

lemma cte_wp_at_domI:
  "cte_wp_at P c s \<Longrightarrow> fst c \<in> dom (kheap s)" by (auto elim: cte_wp_atE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P c s \<Longrightarrow> fst c \<in> dom (kheap s)
theory Detype_AI

lemma dom_known_length:
  "\<lbrakk> dom f = {x. length x = n}; f xs = Some cap \<rbrakk> \<Longrightarrow> n = length xs" by (drule domI[where m=f], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom f = {x. length x = n}; f xs = Some cap\<rbrakk> \<Longrightarrow> n = length xs
theory Detype_AI

lemma invs_untyped_children[elim!]:
  "invs s \<Longrightarrow> untyped_children_in_mdb s" by (clarsimp simp: invs_def valid_state_def valid_mdb_def
                     untyped_mdb_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> untyped_children_in_mdb s
theory Detype_AI

lemma dmo_valid_cap[wp]:
  "\<lbrace>\<lambda>s. s \<turnstile> cap.UntypedCap dev base magnitude idx\<rbrace>
   do_machine_op f
   \<lbrace>\<lambda>rv s. s \<turnstile> cap.UntypedCap dev base magnitude idx\<rbrace>" by (simp add: do_machine_op_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s \<turnstile> UntypedCap dev base magnitude idx\<rbrace> do_machine_op f \<lbrace>\<lambda>rv s. s \<turnstile> UntypedCap dev base magnitude idx\<rbrace>
theory Detype_AI

lemma (in Detype_AI)cte_map_not_null_outside':
  "\<lbrakk>cte_wp_at ((=) (cap.UntypedCap dev q n m)) p' (s :: 'a state);
    descendants_range (cap.UntypedCap dev q n m) p' s; untyped_children_in_mdb s;
    if_unsafe_then_cap s; valid_global_refs s;
    cte_wp_at ((\<noteq>) cap.NullCap) p s\<rbrakk>
   \<Longrightarrow> fst p \<notin> untyped_range (cap.UntypedCap dev q n m)" by (erule (1) cte_map_not_null_outside, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev q n m)) p' s; descendants_range (UntypedCap dev q n m) p' s; untyped_children_in_mdb s; if_unsafe_then_cap s; valid_global_refs s; cte_wp_at ((\<noteq>) NullCap) p s\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range (UntypedCap dev q n m)
theory Detype_AI

lemma refl_spec[simp]:
  "\<not> (\<forall>x. x \<noteq> y)" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>x. x \<noteq> y)
theory Detype_AI

lemma pspace_no_overlap_obj_range:
  "\<lbrakk> pspace_no_overlap S s; kheap s p = Some obj \<rbrakk>
     \<Longrightarrow> obj_range p obj \<inter> S = {}" by (auto simp add: pspace_no_overlap_def obj_range_def field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap S s; kheap s p = Some obj\<rbrakk> \<Longrightarrow> obj_range p obj \<inter> S = {}
theory Detype_AI

lemma range_cover_full:
  "\<lbrakk>is_aligned (ptr :: 'a :: len word) sz;sz < len_of TYPE('a)\<rbrakk> \<Longrightarrow> range_cover ptr sz sz (Suc 0)" by (clarsimp simp:range_cover_def
     unat_eq_0 le_mask_iff[symmetric] word_and_le1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> range_cover ptr sz sz (Suc 0)
theory Detype_AI

lemma range_cover_plus_us:
  "range_cover ptr sz (m + us) (Suc 0) \<Longrightarrow> range_cover ptr sz m (2^us)" apply (erule range_cover_rel) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (m + us) (Suc 0) \<Longrightarrow> range_cover ptr sz m (2 ^ us) proof (prove)
goal (2 subgoals):
 1. m \<le> m + us
 2. 2 ^ us = 2 ^ (m + us - m) * Suc 0 proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma caps_overlap_reserved_subseteq:
  "\<lbrakk>caps_overlap_reserved B s; A\<subseteq> B\<rbrakk> \<Longrightarrow> caps_overlap_reserved A s" apply (clarsimp simp:caps_overlap_reserved_def) apply (drule(1) bspec) apply (erule disjoint_subset2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_overlap_reserved B s; A \<subseteq> B\<rbrakk> \<Longrightarrow> caps_overlap_reserved A s proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> B = {}; A \<subseteq> B; cap \<in> ran (caps_of_state s); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> A = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>A \<subseteq> B; cap \<in> ran (caps_of_state s); is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> B = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> A = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap \<in> ran (caps_of_state s); is_untyped_cap cap; is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> B = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> B = {} proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma range_cover_le:
  "\<lbrakk>range_cover ptr sz us m; n\<le>m\<rbrakk> \<Longrightarrow> range_cover ptr sz us n" by (clarsimp simp:range_cover_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us m; n \<le> m\<rbrakk> \<Longrightarrow> range_cover ptr sz us n
theory Detype_AI

lemma range_cover_ptr_le:
  "\<lbrakk>range_cover ptr sz us (Suc (Suc n));ptr\<noteq> 0\<rbrakk>
   \<Longrightarrow> ptr \<le> ptr + (1 + of_nat n << us)" apply (frule range_cover_subset[where p = 0
    ,OF range_cover_le[where n = "Suc n"]]) apply simp+ apply (frule is_aligned_no_overflow[OF range_cover.aligned]) apply (simp add:shiftl_t2n field_simps) apply (erule order_trans)+ apply (rule word_sub_1_le) apply (drule(1) range_cover_no_0[where p = "Suc n"]) apply simp apply (simp add:word_arith_nat_Suc power_add[symmetric] field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (1 + word_of_nat n << us) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> Suc n \<le> Suc (Suc n)
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < Suc n
 3. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> Suc n \<noteq> 0
 4. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat (Suc n) * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + 2 ^ us - 1 \<longrightarrow> ptr + 2 ^ us - 1 \<le> ptr + (1 + word_of_nat n) * 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + 2 ^ us - 1 \<longrightarrow> ptr + 2 ^ us - 1 \<le> ptr + (1 + word_of_nat n) * 2 ^ us - 1; ptr \<le> ptr + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr + 2 ^ us - 1 \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) - 1; ptr \<le> ptr + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) - 1 \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz us (Suc (Suc n)) \<Longrightarrow> Suc n < Suc (Suc n)
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr + word_of_nat (Suc n) * 2 ^ us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr + word_of_nat (Suc n) * 2 ^ us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) \<noteq> 0 proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma range_cover_unat:
  "range_cover (ptr :: 'a :: len word) sz sb n
   \<Longrightarrow> unat ((ptr && mask sz) + (of_nat n * 2^ sb)) =
       unat (ptr && mask sz) + unat ( (of_nat n) * (2::'a word) ^ sb)" apply (rule unat_add_lem[THEN iffD1]) apply (rule le_less_trans) apply (frule range_cover.unat_of_nat_shift[OF _ le_refl le_refl]) apply (simp add:field_simps) apply (subst add.commute) apply (erule range_cover.range_cover_compare_bound) apply (rule power_strict_increasing) apply (clarsimp simp:range_cover_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sb n \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) = unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ sb) proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sb n \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ sb) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz sb n \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ sb) \<le> ?y3
 2. range_cover ptr sz sb n \<Longrightarrow> ?y3 < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sb n; unat (word_of_nat n * 2 ^ sb) = n * 2 ^ sb\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ sb) \<le> ?y3
 2. range_cover ptr sz sb n \<Longrightarrow> ?y3 < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sb n; unat (word_of_nat n * 2 ^ sb) = n * 2 ^ sb\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + n * 2 ^ sb \<le> ?y3
 2. range_cover ptr sz sb n \<Longrightarrow> ?y3 < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sb n; unat (word_of_nat n * 2 ^ sb) = n * 2 ^ sb\<rbrakk> \<Longrightarrow> n * 2 ^ sb + unat (ptr && mask sz) \<le> ?y3
 2. range_cover ptr sz sb n \<Longrightarrow> ?y3 < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sb n \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz sb n \<Longrightarrow> sz < LENGTH('a)
 2. range_cover ptr sz sb n \<Longrightarrow> 1 < 2 proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma range_cover_sz':
  "range_cover (a :: 'a :: len word) b bits d \<Longrightarrow> bits < len_of TYPE('a)" by (clarsimp simp:range_cover_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover a b bits d \<Longrightarrow> bits < LENGTH('a)
theory ArchDetype_AI

lemma valid_globals_irq_node[Detype_AI_asms]:
    "\<lbrakk> valid_global_refs s; cte_wp_at ((=) cap) ptr s \<rbrakk>
          \<Longrightarrow> interrupt_irq_node s irq \<notin> cap_range cap" apply (erule(1) valid_global_refsD) apply (simp add: global_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs s; cte_wp_at ((=) cap) ptr s\<rbrakk> \<Longrightarrow> interrupt_irq_node s irq \<notin> cap_range cap proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) cap) ptr s \<Longrightarrow> interrupt_irq_node s irq \<in> global_refs s proof (prove)
goal:
No subgoals!
theory ArchDetype_AI

lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)" by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (freeMemory ptr bits)
theory ArchDetype_AI

lemma region_in_kernel_window_detype[simp]:
  "region_in_kernel_window S (detype S' s)
      = region_in_kernel_window S s" by (simp add: region_in_kernel_window_def detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. region_in_kernel_window S (detype S' s) = region_in_kernel_window S s
theory ArchDetype_AI

lemma region_in_kernel_window_machine_state_update[simp]:
  "region_in_kernel_window S (machine_state_update f s) =
   region_in_kernel_window S s" by (simp add: region_in_kernel_window_def)

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

lemma region_in_kernel_window_delete_objects[wp]:
  "\<lbrace>region_in_kernel_window S\<rbrace>
   delete_objects ptr bits
   \<lbrace>\<lambda>_. region_in_kernel_window S\<rbrace>" by (wp | simp add: delete_objects_def do_machine_op_def split_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>region_in_kernel_window S\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_. region_in_kernel_window S\<rbrace>
theory ArchDetype_AI

lemma state_hyp_refs_of_detype:
  "state_hyp_refs_of (detype S s) = (\<lambda>x. if x \<in> S then {} else state_hyp_refs_of s x)" by (rule ext, simp add: state_hyp_refs_of_def detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_hyp_refs_of (detype S s) = (\<lambda>x. if x \<in> S then {} else state_hyp_refs_of s x)
theory ArchDetype_AI

lemma valid_ioports_detype[Detype_AI_asms]:
  "valid_ioports s \<Longrightarrow> valid_ioports (detype (untyped_range cap) s)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioports s \<Longrightarrow> valid_ioports (detype (untyped_range cap) s)
theory ArchDetype_AI

lemma state_hyp_refs: "state_hyp_refs_of (detype (untyped_range cap) s) = state_hyp_refs_of s" apply (rule ext, clarsimp simp add: state_hyp_refs_of_detype) apply (rule sym, rule equals0I, drule state_hyp_refs_of_elemD) apply (drule live_okE, rule hyp_refs_of_live, clarsimp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_hyp_refs_of (detype (untyped_range cap) s) = state_hyp_refs_of s proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> untyped_range cap \<Longrightarrow> {} = state_hyp_refs_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> untyped_range cap; obj_at (\<lambda>obj. y \<in> hyp_refs_of obj) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> untyped_range cap; x \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchDetype_AI

lemma hyp_refsym : "sym_refs (state_hyp_refs_of s)" using invs by (simp add: invs_def valid_state_def valid_pspace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sym_refs (state_hyp_refs_of s) proof (prove)
using this:
invs s

goal (1 subgoal):
 1. sym_refs (state_hyp_refs_of s)
theory ArchDetype_AI

lemma hyp_refs_of: "\<And>obj p. \<lbrakk> ko_at obj p s \<rbrakk> \<Longrightarrow> hyp_refs_of obj \<subseteq> (UNIV - untyped_range cap \<times> UNIV)" by (fastforce intro: hyp_refs_of_live dest!: hyp_sym_refs_ko_atD[OF _ hyp_refsym] live_okE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>obj p. ko_at obj p s \<Longrightarrow> hyp_refs_of obj \<subseteq> UNIV - untyped_range cap \<times> UNIV
theory ArchDetype_AI

lemma arch_valid_obj[detype_invs_proofs]:
    "\<And>p ao. \<lbrakk>ko_at (ArchObj ao) p s; arch_valid_obj ao s\<rbrakk>
       \<Longrightarrow> arch_valid_obj ao (detype (untyped_range cap) s)" apply (frule hyp_refs_of) apply (auto simp: arch_valid_obj_def split: arch_kernel_obj.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>ako_at ao p s; arch_valid_obj ao s\<rbrakk> \<Longrightarrow> arch_valid_obj ao (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>ako_at ao p s; arch_valid_obj ao s; hyp_refs_of (ArchObj ao) \<subseteq> UNIV - untyped_range cap \<times> UNIV\<rbrakk> \<Longrightarrow> arch_valid_obj ao (detype (untyped_range cap) s) proof (prove)
goal:
No subgoals!
theory ArchDetype_AI

lemma sym_hyp_refs_detype[detype_invs_proofs]:
  "sym_refs (state_hyp_refs_of (detype (untyped_range cap) s))" using hyp_refsym by (simp add: state_hyp_refs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sym_refs (state_hyp_refs_of (detype (untyped_range cap) s)) proof (prove)
using this:
sym_refs (state_hyp_refs_of s)

goal (1 subgoal):
 1. sym_refs (state_hyp_refs_of (detype (untyped_range cap) s))
theory ArchDetype_AI

lemma valid_cap[detype_invs_proofs]:
    "\<And>cap'. \<lbrakk> s \<turnstile> cap'; obj_reply_refs cap' \<subseteq> (UNIV - untyped_range cap) \<rbrakk>
      \<Longrightarrow> detype (untyped_range cap) s \<turnstile> cap'" by (auto simp: valid_cap_def valid_untyped_def obj_reply_refs_def
          split: cap.split_asm option.splits if_splits
                 arch_cap.split_asm bool.split_asm )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>s \<turnstile> cap'; obj_reply_refs cap' \<subseteq> UNIV - untyped_range cap\<rbrakk> \<Longrightarrow> detype (untyped_range cap) s \<turnstile> cap'
theory ArchDetype_AI

lemma valid_idle_detype[detype_invs_proofs]: "valid_idle (detype (untyped_range cap) s)" proof - have "valid_idle s" using invs by (simp add: invs_def valid_state_def) thus ?thesis using valid_global_refsD [OF globals cap] by (fastforce simp add: valid_idle_def state_refs idle cap_range_def
                            global_refs_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. valid_idle (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_idle s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_idle s proof (state)
this:
valid_idle s

goal (1 subgoal):
 1. valid_idle (detype (untyped_range cap) s) proof (prove)
using this:
valid_idle s

goal (1 subgoal):
 1. valid_idle (detype (untyped_range cap) s) proof (prove)
using this:
valid_idle s
?r \<in> global_refs s \<Longrightarrow> ?r \<notin> cap_range cap

goal (1 subgoal):
 1. valid_idle (detype (untyped_range cap) s) proof (state)
this:
valid_idle (detype (untyped_range cap) s)

goal:
No subgoals!
theory ArchDetype_AI

lemma valid_vs_lookup: "valid_vs_lookup s" using valid_arch_caps by (simp add: valid_arch_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vs_lookup s proof (prove)
using this:
valid_arch_caps s

goal (1 subgoal):
 1. valid_vs_lookup s
theory ArchDetype_AI

lemma hyp_live_strg:
  "hyp_live ko \<Longrightarrow> live ko" by (cases ko; simp add: live_def hyp_live_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hyp_live ko \<Longrightarrow> live ko
theory ArchDetype_AI

lemma obj_at_hyp_live_strg:
  "obj_at hyp_live p s \<Longrightarrow> obj_at live p s" by (erule obj_at_weakenE, rule hyp_live_strg)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at hyp_live p s \<Longrightarrow> obj_at live p s
theory ArchDetype_AI

lemma tcb_arch_detype[detype_invs_proofs]:
  "\<lbrakk>ko_at (TCB t) p s; valid_arch_tcb (tcb_arch t) s\<rbrakk>
      \<Longrightarrow> valid_arch_tcb (tcb_arch t) (detype (untyped_range cap) s)" apply (clarsimp simp: valid_arch_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB t) p s; valid_arch_tcb (tcb_arch t) s\<rbrakk> \<Longrightarrow> valid_arch_tcb (tcb_arch t) (detype (untyped_range cap) s) proof (prove)
goal:
No subgoals!
theory ArchDetype_AI

lemma global_pts: (* ARCH SPECIFIC STATEMENT*)
  "\<And>p. \<lbrakk> p \<in> set (arm_global_pts (arch_state s)); p \<in> untyped_range cap \<rbrakk>  \<Longrightarrow> False" using valid_global_refsD [OF globals cap] by (simp add: cap_range_def global_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> set (arm_global_pts (arch_state s)); p \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
?r \<in> global_refs s \<Longrightarrow> ?r \<notin> cap_range cap

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> set (arm_global_pts (arch_state s)); p \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False
theory ArchDetype_AI

lemma vs_lookup_preserved:
  "\<And>x rf. \<lbrakk> x \<in> untyped_range cap; (rf \<rhd> x) s \<rbrakk> \<Longrightarrow> False" apply (drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI valid_vs_lookup]) apply (fastforce intro: global_pts no_obj_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x rf. \<lbrakk>x \<in> untyped_range cap; (rf \<rhd> x) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x rf. \<lbrakk>x \<in> untyped_range cap; \<exists>slot cap. caps_of_state s slot = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some rf\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchDetype_AI

lemma vs_lookup_pages_preserved:
  "\<And>x rf. \<lbrakk> x \<in> untyped_range cap; (rf \<unrhd> x) s \<rbrakk> \<Longrightarrow> False" apply (drule valid_vs_lookupD[OF _ valid_vs_lookup]) apply (fastforce intro: global_pts no_obj_refs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x rf. \<lbrakk>x \<in> untyped_range cap; (rf \<unrhd> x) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x rf. \<lbrakk>x \<in> untyped_range cap; \<exists>slot cap. caps_of_state s slot = Some cap \<and> x \<in> obj_refs cap \<and> vs_cap_ref cap = Some rf\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!