theory ArchVSpace_AI

lemma find_pd_for_asid_lookup_none:
  "\<lbrace>\<top>\<rbrace>
    find_pd_for_asid asid
   -, \<lbrace>\<lambda>e s. \<forall>p. \<not> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool),
   VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> p) s\<rbrace>" apply (simp add: find_pd_for_asid_def assertE_def
                 split del: if_split) apply (rule hoare_pre) apply (wp | wpc)+ apply clarsimp apply (intro allI conjI impI) apply (clarsimp simp: vs_lookup_def vs_asid_refs_def up_ucast_inj_eq
                  dest!: vs_lookup1_rtrancl_iterations
                         graph_ofD vs_lookup1D) apply (clarsimp simp: vs_lookup_def vs_asid_refs_def
                 dest!: vs_lookup1_rtrancl_iterations
                        graph_ofD vs_lookup1D) apply (clarsimp simp: obj_at_def vs_refs_def up_ucast_inj_eq
                        mask_asid_low_bits_ucast_ucast
                 dest!: graph_ofD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> find_pd_for_asid asid -, \<lbrace>\<lambda>e s. \<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 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE y <- if 0 < asid then returnOk () else fail;
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE -, \<lbrace>\<lambda>e s. \<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 s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE y <- if 0 < asid then returnOk () else fail;
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE -, \<lbrace>\<lambda>e s. \<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 s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (0 < asid \<longrightarrow> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = None \<longrightarrow> (\<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 s) \<and> True) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> True) \<and> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (pool (UCAST(32 \<rightarrow> 10) asid) = None \<longrightarrow> (\<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 s)) \<and> (\<forall>x. pool (UCAST(32 \<rightarrow> 10) asid) = Some x \<longrightarrow> True)))) \<and> (\<not> 0 < asid \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s. 0 < asid \<Longrightarrow> (asid_table s (asid_high_bits_of asid) = None \<longrightarrow> (\<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 s)) \<and> (\<forall>x. asid_table s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> pool (UCAST(32 \<rightarrow> 10) asid) = None \<longrightarrow> (\<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 s))) proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = None\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup s
 2. \<And>s x pool p. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = None\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool p. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = None\<rbrakk> \<Longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], p) \<notin> vs_lookup s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool aa pa p' ko. \<lbrakk>0 < asid; asid_table s (asid_high_bits_of asid) = Some x; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = None; asid_table s aa = Some pa; ko_at ko pa s; (VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), p') \<in> vs_refs ko; UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) = UCAST(7 \<rightarrow> 32) aa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!