theory Untyped_R

lemma sts_valid_untyped_inv':
  "\<lbrace>valid_untyped_inv' ui\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_untyped_inv' ui\<rbrace>" apply (cases ui, simp add: ex_cte_cap_to'_def) apply (rule hoare_pre) apply (rule hoare_use_eq_irq_node' [OF setThreadState_ksInterruptState]) apply (wp hoare_vcg_const_Ball_lift hoare_vcg_ex_lift | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_untyped_inv' ui\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_untyped_inv' ui\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>sz idx. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. \<exists>cref. cte_wp_at' (\<lambda>c. slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. \<exists>sz idx. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. \<exists>cref. cte_wp_at' (\<lambda>c. slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> \<lbrace>?Q6 x1 x2 x3 x4 x5 x6 x7 x8\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. \<exists>sz idx. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. \<exists>cref. cte_wp_at' (\<lambda>c. slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 x7 x8 s. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; \<exists>sz idx. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. \<exists>cref. cte_wp_at' (\<lambda>c. slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits\<rbrakk> \<Longrightarrow> ?Q6 x1 x2 x3 x4 x5 x6 x7 x8 s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 f. ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> \<lbrace>?P9 x1 x2 x3 x4 x5 x6 x7 x8 f\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. \<exists>sz idx. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. \<exists>cref. cte_wp_at' (\<lambda>c. slot \<in> cte_refs' (cteCap c) f) cref s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits\<rbrace>
 2. \<And>x1 x2 x3 x4 x5 x6 x7 x8 s. \<lbrakk>ui = Invocations_H.untyped_invocation.Retype x1 x2 x3 x4 x5 x6 x7 x8; \<exists>sz idx. cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (APIType_capBits x5 x6) (length x7) \<and> (\<not> x2 \<and> idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of' x1 (ctes_of s) = {}) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> x6 \<and> x6 \<le> maxUntypedSizeBits) \<and> (\<forall>slot\<in>set x7. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) \<and> (\<forall>slot\<in>set x7. \<exists>cref. cte_wp_at' (\<lambda>c. slot \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> sch_act_simple s \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = APIObjectType ArchTypes_H.apiobject_type.Untyped \<or> isFrameType x5) \<and> APIType_capBits x5 x6 \<le> maxUntypedSizeBits\<rbrakk> \<Longrightarrow> ?P9 x1 x2 x3 x4 x5 x6 x7 x8 (irq_node' s) s proof (prove)
goal:
No subgoals!