theory Untyped_R

lemma slots_invD: "\<And>x. x \<in> set slots \<Longrightarrow>
      x \<noteq> cref \<and> x \<notin> usable_range \<and>  ex_cte_cap_wp_to' (\<lambda>_. True) x s" using misc cte_wp_at' vui apply - apply clarsimp apply (drule(1) bspec)+ apply (drule ex_cte_no_overlap') apply simp apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set slots \<Longrightarrow> x \<noteq> cref \<and> x \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x s proof (prove)
using this:
ct_active' s
invs' s
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s
valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype cref reset ptr_base ptr tp us slots dev) (Some (capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s

goal (1 subgoal):
 1. \<And>x. x \<in> set slots \<Longrightarrow> x \<noteq> cref \<and> x \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> set slots; ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; valid_untyped_inv_wcap' (Invocations_H.untyped_invocation.Retype cref reset ptr_base ptr tp us slots dev) (Some (capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s\<rbrakk> \<Longrightarrow> x \<noteq> cref \<and> x \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> ex_cte_cap_wp_to' (\<lambda>_. True) x s proof (prove)
goal (1 subgoal):
 1. \<And>x sza idxa. \<lbrakk>x \<in> set slots; ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sza) sza idxa \<and> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx = cteCap cte) cref s; range_cover ptr sza (APIType_capBits tp us) (length slots); \<not> reset \<and> idxa \<le> unat (ptr && mask sza) \<or> reset \<and> ptr = ptr && ~~ mask sza; ptr_base = ptr && ~~ mask sza; reset \<longrightarrow> descendants_of' cref (ctes_of s) = {}; cref \<notin> set slots; distinct slots; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; \<forall>slot\<in>set slots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; \<forall>slot\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) slot s; sch_act_simple s; slots \<noteq> []; dev \<longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType tp; APIType_capBits tp us \<le> maxUntypedSizeBits\<rbrakk> \<Longrightarrow> x \<noteq> cref \<and> (ptr \<le> x \<longrightarrow> \<not> x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>x sza idxa. \<lbrakk>x \<in> set slots; ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sza) sza idxa \<and> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx = cteCap cte) cref s; range_cover ptr sza (APIType_capBits tp us) (length slots); \<not> reset \<and> idxa \<le> unat (ptr && mask sza) \<or> reset \<and> ptr = ptr && ~~ mask sza; ptr_base = ptr && ~~ mask sza; reset \<longrightarrow> descendants_of' cref (ctes_of s) = {}; cref \<notin> set slots; distinct slots; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; sch_act_simple s; slots \<noteq> []; dev \<longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType tp; APIType_capBits tp us \<le> maxUntypedSizeBits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s; ex_cte_cap_wp_to' (\<lambda>_. True) x s\<rbrakk> \<Longrightarrow> x \<noteq> cref \<and> (ptr \<le> x \<longrightarrow> \<not> x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>x sza idxa. \<lbrakk>x \<in> set slots; ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sza) sza idxa \<and> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx = cteCap cte) cref s; range_cover ptr sza (APIType_capBits tp us) (length slots); \<not> reset \<and> idxa \<le> unat (ptr && mask sza) \<or> reset \<and> ptr = ptr && ~~ mask sza; ptr_base = ptr && ~~ mask sza; reset \<longrightarrow> descendants_of' cref (ctes_of s) = {}; cref \<notin> set slots; distinct slots; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; sch_act_simple s; slots \<noteq> []; dev \<longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType tp; APIType_capBits tp us \<le> maxUntypedSizeBits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s; x \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<noteq> cref \<and> (ptr \<le> x \<longrightarrow> \<not> x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<And>x sza idxa. \<lbrakk>x \<in> set slots; ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sza) sza idxa \<and> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx = cteCap cte) cref s; range_cover ptr sza (APIType_capBits tp us) (length slots); \<not> reset \<and> idxa \<le> unat (ptr && mask sza) \<or> reset \<and> ptr = ptr && ~~ mask sza; ptr_base = ptr && ~~ mask sza; reset \<longrightarrow> descendants_of' cref (ctes_of s) = {}; cref \<notin> set slots; distinct slots; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us \<and> us \<le> maxUntypedSizeBits; sch_act_simple s; slots \<noteq> []; dev \<longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType tp; APIType_capBits tp us \<le> maxUntypedSizeBits; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) x s; ptr \<le> x \<longrightarrow> \<not> x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> x \<noteq> cref proof (prove)
goal:
No subgoals!