theory ArchVSpace_AI

lemma find_pd_for_asid_lots:
  "\<lbrace>\<lambda>s. (\<forall>rv. ([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
   VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> rv) s
           \<longrightarrow> (valid_vspace_objs s \<longrightarrow> page_directory_at rv s)
           \<longrightarrow> Q rv s)
       \<and> ((\<forall>rv. \<not> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
   VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> rv) s) \<longrightarrow> (\<forall>e. E e s))\<rbrace>
    find_pd_for_asid asid
  \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (clarsimp simp: validE_def valid_def) apply (frule in_inv_by_hoareD [OF find_pd_for_asid_inv]) apply (frule use_valid [OF _ find_pd_for_asid_lookup_none
                                [unfolded validE_E_def validE_def]]) apply simp apply (frule use_valid [OF _ find_pd_for_asid_lookup_ref
                                [unfolded validE_R_def validE_def]]) apply simp apply (clarsimp split: sum.split_asm) apply (drule spec, drule uncurry, erule mp) apply clarsimp apply (frule use_valid [OF _ find_pd_for_asid_page_directory
                                [unfolded validE_R_def validE_def]]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s) \<and> ((\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s))\<rbrace> find_pd_for_asid asid \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s)\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); b = s\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); b = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); b = s; case a of Inl e \<Rightarrow> \<forall>p. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup b | Inr r \<Rightarrow> True\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); b = s; case a of Inl e \<Rightarrow> \<forall>p. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup b | Inr r \<Rightarrow> True\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); b = s; case a of Inl e \<Rightarrow> \<forall>p. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup b | Inr r \<Rightarrow> True\<rbrakk> \<Longrightarrow> True
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); b = s; case a of Inl e \<Rightarrow> \<forall>p. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup b | Inr r \<Rightarrow> True; case a of Inl e \<Rightarrow> True | Inr r \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> r) b\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); b = s; case a of Inl e \<Rightarrow> \<forall>p. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup b | Inr r \<Rightarrow> True; case a of Inl e \<Rightarrow> True | Inr r \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> r) b\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> Q r b proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x2) s; (Inr x2, s) \<in> fst (find_pd_for_asid asid s); \<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<longrightarrow> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) rv s) \<longrightarrow> Q rv s; (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s)\<rbrakk> \<Longrightarrow> Q x2 s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x2) s; (Inr x2, s) \<in> fst (find_pd_for_asid asid s); (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s)\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x2) s \<and> (valid_vspace_objs s \<longrightarrow> typ_at (AArch APageDirectory) x2 s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x2) s; (Inr x2, s) \<in> fst (find_pd_for_asid asid s); (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); valid_vspace_objs s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x2 s proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x2) s; (Inr x2, s) \<in> fst (find_pd_for_asid asid s); (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); valid_vspace_objs s\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>s x2. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x2) s; (Inr x2, s) \<in> fst (find_pd_for_asid asid s); (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); valid_vspace_objs s; case Inr x2 of Inl e \<Rightarrow> True | Inr r \<Rightarrow> typ_at (AArch APageDirectory) r s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x2 s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x2) s; (Inr x2, s) \<in> fst (find_pd_for_asid asid s); (\<forall>rv. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], rv) \<notin> vs_lookup s) \<longrightarrow> (\<forall>e. E e s); valid_vspace_objs s; case Inr x2 of Inl e \<Rightarrow> True | Inr r \<Rightarrow> typ_at (AArch APageDirectory) r s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) x2 s proof (prove)
goal:
No subgoals!