theory Untyped_AI

lemma sts_valid_untyped_inv:
  "\<lbrace>valid_untyped_inv ui\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_untyped_inv ui\<rbrace>" apply (cases ui, simp add: descendants_range_in_def) apply (wp hoare_vcg_const_Ball_lift hoare_vcg_ex_lift hoare_vcg_imp_lift | wps)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_untyped_inv ui\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_untyped_inv ui\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. ui = Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>sz idx. cte_wp_at (\<lambda>c. c = UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (obj_bits_api x5 x6) (length x7) \<and> (idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of x1 (cdt s) = {}) \<and> (x5 = CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (\<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. \<exists>sz idx. cte_wp_at (\<lambda>c. c = UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (obj_bits_api x5 x6) (length x7) \<and> (idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of x1 (cdt s) = {}) \<and> (x5 = CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (\<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8 s. \<lbrakk>ui = Retype x1 x2 x3 x4 x5 x6 x7 x8; \<exists>sz idx. cte_wp_at (\<lambda>c. c = UntypedCap x8 x3 sz idx) x1 s \<and> range_cover x4 sz (obj_bits_api x5 x6) (length x7) \<and> (idx \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sz = x3 \<and> (x2 \<longrightarrow> descendants_of x1 (cdt s) = {}) \<and> (x5 = CapTableObject \<longrightarrow> 0 < x6) \<and> (x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (\<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5)\<rbrakk> \<Longrightarrow> \<exists>x xa. cte_wp_at (\<lambda>c. c = UntypedCap x8 x3 x xa) x1 s \<and> range_cover x4 x (obj_bits_api x5 x6) (length x7) \<and> (xa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask x = x3 \<and> (\<not> x2 \<or> descendants_of x1 (cdt s) = {}) \<and> (x5 \<noteq> CapTableObject \<or> 0 < x6) \<and> (x5 \<noteq> Untyped \<or> untyped_min_bits \<le> x6) \<and> x1 \<notin> set x7 \<and> distinct x7 \<and> (\<forall>x\<in>set x7. cte_wp_at ((=) NullCap) x s \<and> ex_cte_cap_wp_to is_cnode_cap x s \<and> real_cte_at x s) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5) proof (prove)
goal:
No subgoals!