theory Retype_AC

lemma authorised_untyped_invI:
  notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                         Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
  shows "\<lbrakk> valid_untyped_inv ui s; pas_refined aag s; authorised_untyped_inv' aag ui \<rbrakk>
           \<Longrightarrow> authorised_untyped_inv aag ui" apply (case_tac ui) apply (clarsimp simp: cte_wp_at_caps_of_state
                       authorised_untyped_inv_def authorised_untyped_inv'_def
                  del: ballI) apply (frule(1) cap_cur_auth_caps_of_state, simp) apply (simp add: aag_cap_auth_def aag_has_Control_iff_owns) apply (frule range_cover_subset'', simp) apply (frule retype_addrs_subset_ptr_bits) apply (subgoal_tac "case ui of Retype src r base aligned_free_ref new_type obj_sz slots dev \<Rightarrow>
                        {aligned_free_ref .. base + 2 ^ sz - 1} \<subseteq> {base .. base + 2 ^ sz - 1}") apply (simp add: field_simps) apply blast apply (simp add: blah word_and_le2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_untyped_inv ui s; pas_refined aag s; authorised_untyped_inv' aag ui\<rbrakk> \<Longrightarrow> authorised_untyped_inv aag ui proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. \<lbrakk>valid_untyped_inv ui s; pas_refined aag s; authorised_untyped_inv' aag ui; ui = Retype x1 x2 x3 x4 x5 x6 x7 x8\<rbrakk> \<Longrightarrow> authorised_untyped_inv aag ui proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> (\<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) proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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> (\<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) proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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) \<and> cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx) \<and> cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> (\<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) proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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) \<and> cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx) \<and> cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx); {x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1} \<subseteq> {x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> (\<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) proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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) \<and> cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx) \<and> cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx); {x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1} \<subseteq> {x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}; set (retype_addrs x4 x5 (length x7) x6) \<subseteq> up_aligned_area x4 sz\<rbrakk> \<Longrightarrow> (\<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) proof (prove)
goal (2 subgoals):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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) \<and> cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx) \<and> cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx); {x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1} \<subseteq> {x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}; set (retype_addrs x4 x5 (length x7) x6) \<subseteq> up_aligned_area x4 sz; case ui of Retype src r base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> {aligned_free_ref..base + 2 ^ sz - 1} \<subseteq> {base..base + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> (\<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)
 2. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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) \<and> cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx) \<and> cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx); {x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1} \<subseteq> {x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}; set (retype_addrs x4 x5 (length x7) x6) \<subseteq> up_aligned_area x4 sz\<rbrakk> \<Longrightarrow> case ui of Retype src r base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> {aligned_free_ref..base + 2 ^ sz - 1} \<subseteq> {base..base + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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) \<and> cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx) \<and> cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx); {x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1} \<subseteq> {x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}; set (retype_addrs x4 x5 (length x7) x6) \<subseteq> {x4..(x4 && ~~ mask sz) + 2 ^ sz - 1}; {x4..(x4 && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> (\<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)
 2. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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) \<and> cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx) \<and> cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx); {x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1} \<subseteq> {x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}; set (retype_addrs x4 x5 (length x7) x6) \<subseteq> up_aligned_area x4 sz\<rbrakk> \<Longrightarrow> case ui of Retype src r base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> {aligned_free_ref..base + 2 ^ sz - 1} \<subseteq> {base..base + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>pas_refined aag s; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; is_subject aag a; caps_of_state s (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); x5 \<noteq> ArchObject ASIDPoolObj; \<forall>x\<in>set x7. is_subject aag (fst x); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; 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) \<and> cap_links_asid_slot aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx) \<and> cap_links_irq aag (pasSubject aag) (UntypedCap x8 (x4 && ~~ mask sz) sz idx); {x4..x4 + word_of_nat (length x7) * 2 ^ obj_bits_api x5 x6 - 1} \<subseteq> {x4 && ~~ mask sz..(x4 && ~~ mask sz) + 2 ^ sz - 1}; set (retype_addrs x4 x5 (length x7) x6) \<subseteq> up_aligned_area x4 sz\<rbrakk> \<Longrightarrow> case ui of Retype src r base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> {aligned_free_ref..base + 2 ^ sz - 1} \<subseteq> {base..base + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!