theory ArchVSpace_AI

lemma pd_at_asid_uniq:
  "\<lbrakk> vspace_at_asid asid pd s; asid \<le> mask asid_bits; valid_asid_map s;
      unique_table_refs (caps_of_state s); valid_vs_lookup s;
      valid_vspace_objs s; valid_global_objs s; valid_arch_state s \<rbrakk>
       \<Longrightarrow> pd_at_uniq asid pd s" apply (clarsimp simp: pd_at_uniq_def ran_option_map
                 dest!: ran_restrictD) apply (clarsimp simp: valid_asid_map_def) apply (drule bspec, erule graph_ofI) apply clarsimp apply (rule pd_at_asid_unique, assumption+) apply (drule subsetD, erule domI) apply (simp add: mask_def) apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; valid_asid_map s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s\<rbrakk> \<Longrightarrow> pd_at_uniq asid pd s proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; valid_asid_map s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd)\<rbrakk> \<Longrightarrow> x = asid proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> x = asid proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; case (x, a, pd) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> x = asid proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; vspace_at_asid x pd s; x \<noteq> 0\<rbrakk> \<Longrightarrow> x = asid proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; vspace_at_asid x pd s; x \<noteq> 0\<rbrakk> \<Longrightarrow> x < 2 ^ local.asid_bits
 2. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; vspace_at_asid x pd s; x \<noteq> 0\<rbrakk> \<Longrightarrow> asid < 2 ^ local.asid_bits proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd); vspace_at_asid x pd s; x \<noteq> 0; x \<in> {0..mask local.asid_bits}\<rbrakk> \<Longrightarrow> x < 2 ^ local.asid_bits
 2. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; vspace_at_asid x pd s; x \<noteq> 0\<rbrakk> \<Longrightarrow> asid < 2 ^ local.asid_bits proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>vspace_at_asid asid pd s; asid \<le> mask local.asid_bits; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, pd); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; vspace_at_asid x pd s; x \<noteq> 0\<rbrakk> \<Longrightarrow> asid < 2 ^ local.asid_bits proof (prove)
goal:
No subgoals!