theory ArchUntyped_AI

lemma obj_is_device_vui_eq[Untyped_AI_assms]:
  "valid_untyped_inv ui s
      \<Longrightarrow> case ui of Retype slot reset ptr_base ptr tp us slots dev
          \<Rightarrow> obj_is_device tp dev = dev" apply (cases ui, clarsimp) apply (clarsimp simp: obj_is_device_def
                 split: apiobject_type.split) apply (intro impI conjI allI, simp_all add: is_frame_type_def default_object_def) apply (simp add: default_arch_object_def split: aobject_type.split) apply (auto simp: arch_is_frame_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_untyped_inv ui s \<Longrightarrow> case ui of Retype slot reset ptr_base ptr tp us slots dev \<Rightarrow> obj_is_device tp dev = dev proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api x5 x6) (length x7); 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. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> obj_is_device x5 x8 = x8 proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx. \<lbrakk>ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api x5 x6) (length x7); 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. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> (x5 = TCBObject \<longrightarrow> (case default_object TCBObject x8 0 of ArchObj (DataPage dev xa) \<Rightarrow> dev | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) = x8) \<and> (x5 = EndpointObject \<longrightarrow> (case default_object EndpointObject x8 0 of ArchObj (DataPage dev xa) \<Rightarrow> dev | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) = x8) \<and> (x5 = NotificationObject \<longrightarrow> (case default_object NotificationObject x8 0 of ArchObj (DataPage dev xa) \<Rightarrow> dev | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) = x8) \<and> (x5 = CapTableObject \<longrightarrow> (case default_object CapTableObject x8 0 of ArchObj (DataPage dev xa) \<Rightarrow> dev | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) = x8) \<and> (\<forall>x6. x5 = ArchObject x6 \<longrightarrow> (case default_object (ArchObject x6) x8 0 of ArchObj (DataPage dev xa) \<Rightarrow> dev | ArchObj _ \<Rightarrow> False | _ \<Rightarrow> False) = x8) proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx x6a. \<lbrakk>ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 (ArchObject x6a) x6 x7 x8; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api (ArchObject x6a) x6) (length x7); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; (a, b) \<notin> set x7; distinct x7; \<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; x6a \<noteq> ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> arch_is_frame_type x6a; x5 = ArchObject x6a\<rbrakk> \<Longrightarrow> (case default_arch_object x6a x8 0 of DataPage dev x \<Rightarrow> dev | _ \<Rightarrow> False) = x8 proof (prove)
goal (1 subgoal):
 1. \<And>a b x2 x4 x5 x6 x7 x8 sz idx x6a. \<lbrakk>ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 (ArchObject x6a) x6 x7 x8; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; range_cover x4 sz (obj_bits_api (ArchObject x6a) x6) (length x7); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; (a, b) \<notin> set x7; distinct x7; \<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; x6a \<noteq> ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> arch_is_frame_type x6a; x5 = ArchObject x6a\<rbrakk> \<Longrightarrow> (x6a = PageTableObj \<longrightarrow> \<not> x8) \<and> (x6a = PageDirectoryObj \<longrightarrow> \<not> x8) proof (prove)
goal:
No subgoals!