theory Retype_AC

lemma invoke_untyped_integrity:
  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs
                       and valid_untyped_inv ui
                       and K (authorised_untyped_inv aag ui)\<rbrace>
   invoke_untyped ui
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp only: valid_untyped_inv_wcap) apply (cases ui) apply (simp add: mapM_x_def[symmetric] authorised_untyped_inv_def
                   invoke_untyped_def) apply (rule hoare_pre) apply (wp mapM_x_wp[OF _ subset_refl] create_cap_integrity
             init_arch_objects_integrity retype_region_integrity
             retype_region_ret_is_subject
             set_cap_integrity_autarch hoare_vcg_if_lift
             whenE_wp reset_untyped_cap_integrity
          | clarsimp simp: split_paired_Ball
          | erule in_set_zipE
          | blast)+ apply (clarsimp simp: ptr_range_def p_assoc_help bits_of_def
                        cte_wp_at_caps_of_state) apply (frule(1) cap_cur_auth_caps_of_state, simp+) apply (clarsimp simp: aag_cap_auth_def pas_refined_all_auth_is_owns) apply (simp add: word_and_le2 field_simps
         | erule ball_subset[where A="{a && c .. b}" for a b c]
         | rule conjI impI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and valid_untyped_inv ui and K (authorised_untyped_inv aag ui)\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and pas_refined aag and valid_objs and valid_untyped_inv ui and K (authorised_untyped_inv aag ui)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sz idx. \<lbrakk>K (authorised_untyped_inv aag ui) s; valid_objs s; integrity aag X st s; pas_refined aag s; valid_untyped_inv_wcap ui (Some (case ui of Retype slot reset ptr_base ptr ty us slots dev \<Rightarrow> UntypedCap dev (ptr && ~~ mask sz) sz idx)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sz idx x1 x2 x3 x4 x5 x6 x7 x8. \<lbrakk>K (authorised_untyped_inv aag ui) s; valid_objs s; integrity aag X st s; pas_refined aag s; valid_untyped_inv_wcap ui (Some (case ui of Retype slot reset ptr_base ptr ty us slots dev \<Rightarrow> UntypedCap dev (ptr && ~~ mask sz) sz idx)) s; ui = Retype x1 x2 x3 x4 x5 x6 x7 x8\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> invoke_untyped ui \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sz idx x1 x2 x3 x4 x5 x6 x7 x8. \<lbrakk>is_subject aag (fst x1) \<and> 0 < word_of_nat (length x7) \<and> (\<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x) \<and> (\<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set x7. is_subject aag (fst x)); valid_objs s; integrity aag X st s; pas_refined aag s; \<exists>sza idxa. cte_wp_at (\<lambda>c. c = UntypedCap x8 x3 sza idxa \<and> UntypedCap x8 (x4 && ~~ mask sz) sz idx = c) x1 s \<and> range_cover x4 sza (obj_bits_api x5 x6) (length x7) \<and> (idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = 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> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5); ui = Retype x1 x2 x3 x4 x5 x6 x7 x8\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE x2 (reset_untyped_cap x1);
liftE (do cap <- get_cap x1;
y <- set_cap (UntypedCap x8 x3 (bits_of cap) (unat (x4 + (word_of_nat (length x7) << obj_bits_api x5 x6) - x3))) x1;
orefs <- retype_region x4 (length x7) x6 x5 x8;
y <- init_arch_objects x5 x4 (length x7) x6 orefs;
mapM_x (create_cap x5 x6 x1 x8) (zip x7 orefs)
od)
odE \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sz idx x1 x2 x3 x4 x5 x6 x7 x8. \<lbrakk>is_subject aag (fst x1) \<and> 0 < word_of_nat (length x7) \<and> (\<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x) \<and> (\<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set x7. is_subject aag (fst x)); valid_objs s; integrity aag X st s; pas_refined aag s; \<exists>sza idxa. cte_wp_at (\<lambda>c. c = UntypedCap x8 x3 sza idxa \<and> UntypedCap x8 (x4 && ~~ mask sz) sz idx = c) x1 s \<and> range_cover x4 sza (obj_bits_api x5 x6) (length x7) \<and> (idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = 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> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5); ui = Retype x1 x2 x3 x4 x5 x6 x7 x8\<rbrakk> \<Longrightarrow> \<lbrace>?Q9 s sz idx x1 x2 x3 x4 x5 x6 x7 x8\<rbrace> doE y <- whenE x2 (reset_untyped_cap x1);
liftE (do cap <- get_cap x1;
y <- set_cap (UntypedCap x8 x3 (bits_of cap) (unat (x4 + (word_of_nat (length x7) << obj_bits_api x5 x6) - x3))) x1;
orefs <- retype_region x4 (length x7) x6 x5 x8;
y <- init_arch_objects x5 x4 (length x7) x6 orefs;
mapM_x (create_cap x5 x6 x1 x8) (zip x7 orefs)
od)
odE \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s sz idx x1 x2 x3 x4 x5 x6 x7 x8 sa. \<lbrakk>is_subject aag (fst x1) \<and> 0 < word_of_nat (length x7) \<and> (\<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x) \<and> (\<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x) \<and> x5 \<noteq> ArchObject ASIDPoolObj \<and> (\<forall>x\<in>set x7. is_subject aag (fst x)); valid_objs s; integrity aag X st s; pas_refined aag s; \<exists>sza idxa. cte_wp_at (\<lambda>c. c = UntypedCap x8 x3 sza idxa \<and> UntypedCap x8 (x4 && ~~ mask sz) sz idx = c) x1 s \<and> range_cover x4 sza (obj_bits_api x5 x6) (length x7) \<and> (idxa \<le> unat (x4 - x3) \<or> x2 \<and> x4 = x3) \<and> x4 && ~~ mask sza = 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> x7 \<noteq> [] \<and> (x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5); ui = Retype x1 x2 x3 x4 x5 x6 x7 x8; s = sa\<rbrakk> \<Longrightarrow> ?Q9 s sz idx x1 x2 x3 x4 x5 x6 x7 x8 sa proof (prove)
goal (1 subgoal):
 1. \<And>sz idx a b x2 x4 x5 x6 x7 x8 sa sza idxa. \<lbrakk>valid_objs sa; integrity aag X st sa; pas_refined aag sa; ui = Retype (a, b) x2 (x4 && ~~ mask sza) x4 x5 x6 x7 x8; is_subject aag a; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sza) sza idxa \<and> UntypedCap x8 (x4 && ~~ mask sz) sz idx = c) (a, b) sa; 0 < word_of_nat (length x7); range_cover x4 sza (obj_bits_api x5 x6) (length x7); \<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x; idxa \<le> unat (x4 && mask sza) \<or> x2 \<and> x4 = x4 && ~~ mask sza; \<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x; x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x. (\<exists>y. (x, y) \<in> set x7) \<longrightarrow> is_subject aag x; x2 \<longrightarrow> descendants_of (a, b) (cdt sa) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot y. (slot, y) \<in> set x7 \<longrightarrow> cte_wp_at ((=) NullCap) (slot, y) sa \<and> ex_cte_cap_wp_to is_cnode_cap (slot, y) sa \<and> cap_table_at (length y) slot sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> (x2 \<longrightarrow> cte_wp_at is_untyped_cap (a, b) sa \<and> range_cover x4 (?sz1765 sa sz idx (a, b) True (x4 && ~~ mask sza) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1765 sa sz idx (a, b) True (x4 && ~~ mask sza) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1773 sa sz idx (a, b) True (x4 && ~~ mask sza) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1773 sa sz idx (a, b) True (x4 && ~~ mask sza) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1777 sa sz idx a b (a, b) True (x4 && ~~ mask sza) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7)) \<and> (\<not> x2 \<longrightarrow> range_cover x4 (?sz1765 sa sz idx (a, b) False (x4 && ~~ mask sza) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1765 sa sz idx (a, b) False (x4 && ~~ mask sza) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1773 sa sz idx (a, b) False (x4 && ~~ mask sza) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1773 sa sz idx (a, b) False (x4 && ~~ mask sza) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1777 sa sz idx a b (a, b) False (x4 && ~~ mask sza) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7)) proof (prove)
goal (1 subgoal):
 1. \<And>sz idx a b x2 x4 x5 x6 x7 x8 sa. \<lbrakk>valid_objs sa; integrity aag X st sa; pas_refined aag sa; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state sa (a, b) = Some (UntypedCap x8 (x4 && ~~ mask sz) sz idx); 0 < word_of_nat (length x7); range_cover x4 sz (obj_bits_api x5 x6) (length x7); \<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x; idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; \<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x; x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x. (\<exists>y. (x, y) \<in> set x7) \<longrightarrow> is_subject aag x; x2 \<longrightarrow> descendants_of (a, b) (cdt sa) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot y. (slot, y) \<in> set x7 \<longrightarrow> caps_of_state sa (slot, y) = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap (slot, y) sa \<and> cap_table_at (length y) slot sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> (x2 \<longrightarrow> range_cover x4 (?sz1765 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1765 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1773 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1773 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1777 sa sz idx a b (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7)) \<and> (\<not> x2 \<longrightarrow> range_cover x4 (?sz1765 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1765 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1773 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1773 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1777 sa sz idx a b (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7)) proof (prove)
goal (1 subgoal):
 1. \<And>sz idx a b x2 x4 x5 x6 x7 x8 sa. \<lbrakk>valid_objs sa; integrity aag X st sa; pas_refined aag sa; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state sa (a, b) = Some (UntypedCap x8 (x4 && ~~ mask sz) sz idx); 0 < word_of_nat (length x7); range_cover x4 sz (obj_bits_api x5 x6) (length x7); \<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x; idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; \<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x; x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x. (\<exists>y. (x, y) \<in> set x7) \<longrightarrow> is_subject aag x; x2 \<longrightarrow> descendants_of (a, b) (cdt sa) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot y. (slot, y) \<in> set x7 \<longrightarrow> caps_of_state sa (slot, y) = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap (slot, y) sa \<and> cap_table_at (length y) slot sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5; pas_cap_cur_auth aag (UntypedCap x8 (x4 && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> (x2 \<longrightarrow> range_cover x4 (?sz1765 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1765 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1773 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1773 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1777 sa sz idx a b (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7)) \<and> (\<not> x2 \<longrightarrow> range_cover x4 (?sz1765 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1765 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1773 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1773 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1777 sa sz idx a b (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7)) proof (prove)
goal (1 subgoal):
 1. \<And>sz idx a b x2 x4 x5 x6 x7 x8 sa. \<lbrakk>valid_objs sa; integrity aag X st sa; pas_refined aag sa; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state sa (a, b) = Some (UntypedCap x8 (x4 && ~~ mask sz) sz idx); 0 < word_of_nat (length x7); range_cover x4 sz (obj_bits_api x5 x6) (length x7); \<forall>x\<in>set (retype_addrs x4 x5 (length x7) x6). is_subject aag x; idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; \<forall>x\<in>{x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1}. is_subject aag x; x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x. (\<exists>y. (x, y) \<in> set x7) \<longrightarrow> is_subject aag x; x2 \<longrightarrow> descendants_of (a, b) (cdt sa) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot y. (slot, y) \<in> set x7 \<longrightarrow> caps_of_state sa (slot, y) = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap (slot, y) sa \<and> cap_table_at (length y) slot sa; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5; \<forall>x\<in>{x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}. is_subject aag x; cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx); cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> (x2 \<longrightarrow> range_cover x4 (?sz1765 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1765 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1773 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1773 sa sz idx (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1777 sa sz idx a b (a, b) True (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7)) \<and> (\<not> x2 \<longrightarrow> range_cover x4 (?sz1765 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1765 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1773 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7) \<and> (\<forall>x\<in>up_aligned_area x4 (?sz1773 sa sz idx (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8). is_subject aag x) \<and> range_cover x4 (?sz1777 sa sz idx a b (a, b) False (x4 && ~~ mask sz) x4 x5 x6 x7 x8) (obj_bits_api x5 x6) (length x7)) proof (prove)
goal:
No subgoals!