kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_AI

lemma cap_range_def2:
  "cap_range (default_cap ty ptr us dev) = (if ty = Untyped then {ptr..ptr + 2 ^ us - 1} else {ptr})" apply (case_tac ty) by (simp_all add: cap_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_range (default_cap ty ptr us dev) = (if ty = Untyped then {ptr..ptr + 2 ^ us - 1} else {ptr}) proof (prove)
goal (6 subgoals):
 1. ty = Untyped \<Longrightarrow> cap_range (default_cap ty ptr us dev) = (if ty = Untyped then {ptr..ptr + 2 ^ us - 1} else {ptr})
 2. ty = TCBObject \<Longrightarrow> cap_range (default_cap ty ptr us dev) = (if ty = Untyped then {ptr..ptr + 2 ^ us - 1} else {ptr})
 3. ty = EndpointObject \<Longrightarrow> cap_range (default_cap ty ptr us dev) = (if ty = Untyped then {ptr..ptr + 2 ^ us - 1} else {ptr})
 4. ty = NotificationObject \<Longrightarrow> cap_range (default_cap ty ptr us dev) = (if ty = Untyped then {ptr..ptr + 2 ^ us - 1} else {ptr})
 5. ty = CapTableObject \<Longrightarrow> cap_range (default_cap ty ptr us dev) = (if ty = Untyped then {ptr..ptr + 2 ^ us - 1} else {ptr})
 6. \<And>x6. ty = ArchObject x6 \<Longrightarrow> cap_range (default_cap ty ptr us dev) = (if ty = Untyped then {ptr..ptr + 2 ^ us - 1} else {ptr})
theory Untyped_AI

lemma set_untyped_cap_refs_respects_device_simple:
  "\<lbrace>K (is_untyped_cap cap) and cte_wp_at ((=) cap) cref and cap_refs_respects_device_region \<rbrace> set_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) cref
    \<lbrace>\<lambda>rv s. cap_refs_respects_device_region s\<rbrace>" apply (wp set_cap_cap_refs_respects_device_region) apply (clarsimp simp del: split_paired_Ex) apply (rule_tac x = cref in exI) apply (erule cte_wp_at_weakenE) apply (case_tac cap,auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_untyped_cap cap) and cte_wp_at ((=) cap) cref and cap_refs_respects_device_region\<rbrace> set_cap (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) cref \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (K (is_untyped_cap cap) and cte_wp_at ((=) cap) cref and cap_refs_respects_device_region) s \<Longrightarrow> (cap_refs_respects_device_region and (\<lambda>s. \<exists>ptr. cte_wp_at (\<lambda>c. cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<subseteq> cap_range c \<and> (cap_range (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) \<noteq> {} \<longrightarrow> cap_is_device (UntypedCap (cap_is_device cap) (obj_ref_of cap) (cap_bits cap) idx) = cap_is_device c)) ptr s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_untyped_cap cap; cte_wp_at ((=) cap) cref s; cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> \<exists>ptr. cte_wp_at (\<lambda>c. {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} \<subseteq> cap_range c \<and> (obj_ref_of cap \<le> obj_ref_of cap + 2 ^ cap_bits cap - 1 \<longrightarrow> cap_is_device cap = cap_is_device c)) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_untyped_cap cap; cte_wp_at ((=) cap) cref s; cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} \<subseteq> cap_range c \<and> (obj_ref_of cap \<le> obj_ref_of cap + 2 ^ cap_bits cap - 1 \<longrightarrow> cap_is_device cap = cap_is_device c)) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s c. \<lbrakk>is_untyped_cap cap; cap_refs_respects_device_region s; cap = c\<rbrakk> \<Longrightarrow> {obj_ref_of cap..obj_ref_of cap + 2 ^ cap_bits cap - 1} \<subseteq> cap_range c \<and> (obj_ref_of cap \<le> obj_ref_of cap + 2 ^ cap_bits cap - 1 \<longrightarrow> cap_is_device cap = cap_is_device c) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma caps_overlap_reserved_detype:
  "caps_overlap_reserved S s \<Longrightarrow> caps_overlap_reserved S (detype H s)" apply (clarsimp simp: caps_overlap_reserved_def ) apply (erule ranE) apply (clarsimp split: if_splits) apply (drule bspec) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_overlap_reserved S s \<Longrightarrow> caps_overlap_reserved S (detype H 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> S = {}; cap \<in> ran (\<lambda>p. if fst p \<in> H then None else caps_of_state s p); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; is_untyped_cap cap; (if fst x \<in> H then None else caps_of_state s x) = Some cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap a b. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; is_untyped_cap cap; a \<notin> H; caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>cap a b. \<lbrakk>is_untyped_cap cap; a \<notin> H; caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> ?cap19 cap a b \<in> ran (caps_of_state s)
 2. \<And>cap a b. \<lbrakk>is_untyped_cap cap; a \<notin> H; caps_of_state s (a, b) = Some cap; is_untyped_cap (?cap19 cap a b) \<longrightarrow> usable_untyped_range (?cap19 cap a b) \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>cap a b. \<lbrakk>is_untyped_cap cap; a \<notin> H; caps_of_state s (a, b) = Some cap; is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma caps_no_overlap_detype:
  "caps_no_overlap ptr sz s \<Longrightarrow> caps_no_overlap ptr sz (detype H s)" apply (clarsimp simp: caps_no_overlap_def) apply (erule ranE) apply (clarsimp split: if_splits) apply (drule bspec,fastforce) apply clarsimp apply (erule subsetD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_no_overlap ptr sz s \<Longrightarrow> caps_no_overlap ptr sz (detype H s) proof (prove)
goal (1 subgoal):
 1. \<And>cap x. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; cap \<in> ran (\<lambda>p. if fst p \<in> H then None else caps_of_state s p); untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x xa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (if fst xa \<in> H then None else caps_of_state s xa) = Some cap\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x a b. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; a \<notin> H; caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x a b. \<lbrakk>untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; a \<notin> H; caps_of_state s (a, b) = Some cap; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x a b. \<lbrakk>untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; a \<notin> H; caps_of_state s (a, b) = Some cap; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>cap x a b. \<lbrakk>untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; a \<notin> H; caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma not_inD:"\<lbrakk>x \<notin> A; y \<in> A\<rbrakk> \<Longrightarrow>x \<noteq> y" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<noteq> y
theory Untyped_AI

lemma descendants_range_in_subseteq:
  "\<lbrakk>descendants_range_in A p ms ;B\<subseteq> A\<rbrakk> \<Longrightarrow> descendants_range_in B p ms" by (auto simp: descendants_range_in_def cte_wp_at_caps_of_state dest!: bspec)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range_in A p ms; B \<subseteq> A\<rbrakk> \<Longrightarrow> descendants_range_in B p ms
theory Untyped_AI

lemma shiftr_then_mask_commute:
  "(x >> n) && mask m = (x && mask (m + n)) >> n" using test_bit_size[where w=x] by (auto intro: word_eqI simp add: word_size nth_shiftr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x >> n) && mask m = x && mask (m + n) >> n proof (prove)
using this:
x !! ?n \<Longrightarrow> ?n < size x

goal (1 subgoal):
 1. (x >> n) && mask m = x && mask (m + n) >> n
theory Untyped_AI

lemma add_minus_neg_mask:
 "ptr + a - (ptr && ~~ mask sz) = (ptr && mask sz) + a" apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz" and t = ptr]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr + a - (ptr && ~~ mask sz) = (ptr && mask sz) + a proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz) + (ptr && ~~ mask sz) + a - (ptr && ~~ mask sz) = (ptr && mask sz) + a proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma not_0_ptr[simp]: "ptr\<noteq> 0" using misc vui apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule(1) caps_of_state_valid) apply (clarsimp simp: valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr \<noteq> 0 proof (prove)
using this:
ct_active s
invs s
valid_untyped_inv_wcap (Retype cref reset ptr_base ptr tp us slots dev) (Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. ptr \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; invs s; caps_of_state s cref = Some (UntypedCap dev 0 sz idx); ptr_base = 0; range_cover 0 sz (obj_bits_api tp us) (length slots); idx = 0 \<or> reset; reset \<longrightarrow> descendants_of cref (cdt s) = {}; tp = CapTableObject \<longrightarrow> 0 < us; tp = Untyped \<longrightarrow> untyped_min_bits \<le> us; cref \<notin> set slots; distinct slots; \<forall>slot\<in>set slots. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; tp \<noteq> ArchObject ASIDPoolObj; slots \<noteq> []; dev \<longrightarrow> tp = Untyped \<or> is_frame_type tp; ptr = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; caps_of_state s cref = Some (UntypedCap dev 0 sz idx); ptr_base = 0; range_cover 0 sz (obj_bits_api tp us) (length slots); idx = 0 \<or> reset; reset \<longrightarrow> descendants_of cref (cdt s) = {}; tp = CapTableObject \<longrightarrow> 0 < us; tp = Untyped \<longrightarrow> untyped_min_bits \<le> us; cref \<notin> set slots; distinct slots; \<forall>slot\<in>set slots. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; tp \<noteq> ArchObject ASIDPoolObj; slots \<noteq> []; dev \<longrightarrow> tp = Untyped \<or> is_frame_type tp; ptr = 0; s \<turnstile> UntypedCap dev 0 sz idx\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma cover: "range_cover ptr sz (obj_bits_api tp us) (length slots)" using vui by (clarsimp simp:cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api tp us) (length slots) proof (prove)
using this:
valid_untyped_inv_wcap (Retype cref reset ptr_base ptr tp us slots dev) (Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api tp us) (length slots)
theory Untyped_AI

lemma misc2:
  "distinct slots"
  "slots \<noteq> []" using vui by (auto simp:cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct slots &&& slots \<noteq> [] proof (prove)
using this:
valid_untyped_inv_wcap (Retype cref reset ptr_base ptr tp us slots dev) (Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. distinct slots &&& slots \<noteq> []
theory Untyped_AI

lemma subset_stuff[simp]:
  "retype_range \<subseteq> usable_range" apply (rule range_cover_subset'[OF cover]) apply (simp add:misc2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. length slots \<noteq> 0 proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma cte_wp_at:
  "cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s" using vui by (clarsimp simp: cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s proof (prove)
using this:
valid_untyped_inv_wcap (Retype cref reset ptr_base ptr tp us slots dev) (Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s
theory Untyped_AI

lemma idx_cases:
  "(idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz)" using vui by (clarsimp simp: cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz proof (prove)
using this:
valid_untyped_inv_wcap (Retype cref reset ptr_base ptr tp us slots dev) (Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz
theory Untyped_AI

lemma desc_range:
  "reset \<longrightarrow> descendants_range_in S cref s" using vui by (clarsimp simp: empty_descendants_range_in)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset \<longrightarrow> descendants_range_in S cref s proof (prove)
using this:
valid_untyped_inv_wcap (Retype cref reset ptr_base ptr tp us slots dev) (Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. reset \<longrightarrow> descendants_range_in S cref s
theory Untyped_AI

lemma vc[simp] : "s \<turnstile>UntypedCap dev (ptr && ~~ mask sz) sz idx" using misc cte_wp_at apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule caps_of_state_valid) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx proof (prove)
using this:
ct_active s
invs s
cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s

goal (1 subgoal):
 1. s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> caps_of_state s ?p3 = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma ps_no_overlap[simp]: "\<not> reset \<longrightarrow> pspace_no_overlap_range_cover ptr sz s" using misc cte_wp_at cover idx_cases apply clarsimp apply (erule cte_wp_at_pspace_no_overlapI[OF  _ _ _
                 range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) apply (simp add: cte_wp_at_caps_of_state) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> reset \<longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s proof (prove)
using this:
ct_active s
invs s
cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s
range_cover ptr sz (obj_bits_api tp us) (length slots)
idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz

goal (1 subgoal):
 1. \<not> reset \<longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr && mask sz); \<not> reset\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr && mask sz); \<not> reset\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = UntypedCap ?dev6 (ptr && ~~ mask sz) sz ?idx6) ?cref6 s
 2. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr && mask sz); \<not> reset\<rbrakk> \<Longrightarrow> ?idx6 \<le> unat (ptr && mask sz)
 3. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr && mask sz); \<not> reset\<rbrakk> \<Longrightarrow> range_cover ?ptr7 sz ?sbit7 ?n7 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr && mask sz); \<not> reset\<rbrakk> \<Longrightarrow> idx \<le> unat (ptr && mask sz)
 2. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr && mask sz); \<not> reset\<rbrakk> \<Longrightarrow> range_cover ?ptr7 sz ?sbit7 ?n7 proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma idx_compare'[simp]:"unat ((ptr && mask sz) + (of_nat (length slots)<< (obj_bits_api tp us))) \<le> 2 ^ sz" apply (rule le_trans[OF unat_plus_gt]) apply (simp add:range_cover.unat_of_nat_n_shift[OF cover] range_cover_unat) apply (insert range_cover.range_cover_compare_bound[OF cover]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat ((ptr && mask sz) + (word_of_nat (length slots) << obj_bits_api tp us)) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat (length slots) << obj_bits_api tp us) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz) + length slots * 2 ^ obj_bits_api tp us \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. length slots * 2 ^ obj_bits_api tp us + unat (ptr && mask sz) \<le> 2 ^ sz \<Longrightarrow> unat (ptr && mask sz) + length slots * 2 ^ obj_bits_api tp us \<le> 2 ^ sz proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma cref_inv: "fst cref \<notin> usable_range" apply (insert misc cte_wp_at) apply (drule if_unsafe_then_capD) apply (simp add:invs_def valid_state_def) apply clarsimp apply (drule ex_cte_no_overlap) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> fst cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ct_active s; invs s\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s
 2. \<And>cap. \<lbrakk>ct_active s; invs s; UntypedCap dev (ptr && ~~ mask sz) sz idx = cap\<rbrakk> \<Longrightarrow> cap \<noteq> NullCap
 3. \<lbrakk>ct_active s; invs s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. UntypedCap dev (ptr && ~~ mask sz) sz idx = cap' \<and> appropriate_cte_cap cap' cap) cref s\<rbrakk> \<Longrightarrow> fst cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cap. \<lbrakk>ct_active s; invs s; UntypedCap dev (ptr && ~~ mask sz) sz idx = cap\<rbrakk> \<Longrightarrow> cap \<noteq> NullCap
 2. \<lbrakk>ct_active s; invs s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. UntypedCap dev (ptr && ~~ mask sz) sz idx = cap' \<and> appropriate_cte_cap cap' cap) cref s\<rbrakk> \<Longrightarrow> fst cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; invs s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. UntypedCap dev (ptr && ~~ mask sz) sz idx = cap' \<and> appropriate_cte_cap cap' cap) cref s\<rbrakk> \<Longrightarrow> fst cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; invs s; fst cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> fst cref \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma detype_locale:"ptr && ~~ mask sz = ptr
    \<Longrightarrow> detype_locale (UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s" using cte_wp_at descendants_range misc by (simp add:detype_locale_def descendants_range_def2 blah invs_untyped_children)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr && ~~ mask sz = ptr \<Longrightarrow> detype_locale (UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s proof (prove)
using this:
cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s
descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s
descendants_range_in {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} cref s
ct_active s
invs s

goal (1 subgoal):
 1. ptr && ~~ mask sz = ptr \<Longrightarrow> detype_locale (UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s