theory VSpace_R

lemma findPDForASID_pd_at_wp:
  "\<lbrace>\<lambda>s. \<forall>pd. (page_directory_at' pd s \<longrightarrow> pd_at_asid' pd asid s)
            \<longrightarrow> P pd s\<rbrace> findPDForASID asid \<lbrace>P\<rbrace>,-" apply (simp add: findPDForASID_def assertE_def
             cong: option.case_cong
               split del: if_split) apply (rule hoare_pre) apply (wp getASID_wp | wpc | simp add: o_def split del: if_split)+ apply (clarsimp simp: pd_at_asid'_def) apply (case_tac ko, simp) apply (subst(asm) inv_f_f) apply (rule inj_onI, simp+) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. (page_directory_at' pd s \<longrightarrow> pd_at_asid' pd asid s) \<longrightarrow> P pd s\<rbrace> findPDForASID asid \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. (page_directory_at' pd s \<longrightarrow> pd_at_asid' pd asid s) \<longrightarrow> P pd s\<rbrace> doE y <- if 0 < asid then returnOk () else fail;
y <- if asid \<le> snd asidRange then returnOk () else fail;
asidTable <- liftE (gets (armKSASIDTable \<circ> ksArchState));
pool <- liftME (inv asidpool.ASIDPool) (case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> liftE (getObject ptr));
case pool (asid && mask local.asid_low_bits) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> doE y <- if ptr \<noteq> 0 then returnOk () else fail;
y <- liftE (checkPDAt ptr);
returnOk ptr
odE
odE \<lbrace>P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'4\<rbrace> doE y <- if 0 < asid then returnOk () else fail;
y <- if asid \<le> snd asidRange then returnOk () else fail;
asidTable <- liftE (gets (armKSASIDTable \<circ> ksArchState));
pool <- liftME (inv asidpool.ASIDPool) (case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> liftE (getObject ptr));
case pool (asid && mask local.asid_low_bits) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> doE y <- if ptr \<noteq> 0 then returnOk () else fail;
y <- liftE (checkPDAt ptr);
returnOk ptr
odE
odE \<lbrace>P\<rbrace>, -
 2. \<And>s. \<forall>pd. (page_directory_at' pd s \<longrightarrow> pd_at_asid' pd asid s) \<longrightarrow> P pd s \<Longrightarrow> ?P'4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>pd. (page_directory_at' pd s \<longrightarrow> pd_at_asid' pd asid s) \<longrightarrow> P pd s \<Longrightarrow> 0 < asid \<longrightarrow> asid \<le> snd asidRange \<longrightarrow> (\<forall>x. armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> (\<forall>ko. ko_at' ko x s \<longrightarrow> (\<forall>x. inv asidpool.ASIDPool ko (asid && mask local.asid_low_bits) = Some x \<longrightarrow> x \<noteq> 0 \<longrightarrow> P x s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x ko xa. \<lbrakk>\<forall>pd. (page_directory_at' pd s \<longrightarrow> (\<exists>pool. ko_at' (asidpool.ASIDPool pool) x s \<and> pool (asid && mask local.asid_low_bits) = Some pd)) \<longrightarrow> P pd s; 0 < asid; asid \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x; ko_at' ko x s; inv asidpool.ASIDPool ko (asid && mask local.asid_low_bits) = Some xa; xa \<noteq> 0\<rbrakk> \<Longrightarrow> P xa s proof (prove)
goal (1 subgoal):
 1. \<And>s x ko xa xb. \<lbrakk>\<forall>pd. (page_directory_at' pd s \<longrightarrow> (\<exists>pool. ko_at' (asidpool.ASIDPool pool) x s \<and> pool (asid && mask local.asid_low_bits) = Some pd)) \<longrightarrow> P pd s; 0 < asid; asid \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x; ko_at' (asidpool.ASIDPool xb) x s; inv asidpool.ASIDPool (asidpool.ASIDPool xb) (asid && mask local.asid_low_bits) = Some xa; xa \<noteq> 0; ko = asidpool.ASIDPool xb\<rbrakk> \<Longrightarrow> P xa s proof (prove)
goal (2 subgoals):
 1. \<And>s x ko xa xb. \<lbrakk>xa \<noteq> 0; ko = asidpool.ASIDPool xb; \<forall>pd. (page_directory_at' pd s \<longrightarrow> (\<exists>pool. ko_at' (asidpool.ASIDPool pool) x s \<and> pool (asid && mask local.asid_low_bits) = Some pd)) \<longrightarrow> P pd s; 0 < asid; asid \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x; ko_at' (asidpool.ASIDPool xb) x s\<rbrakk> \<Longrightarrow> inj asidpool.ASIDPool
 2. \<And>s x ko xa xb. \<lbrakk>\<forall>pd. (page_directory_at' pd s \<longrightarrow> (\<exists>pool. ko_at' (asidpool.ASIDPool pool) x s \<and> pool (asid && mask local.asid_low_bits) = Some pd)) \<longrightarrow> P pd s; 0 < asid; asid \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x; ko_at' (asidpool.ASIDPool xb) x s; xb (asid && mask local.asid_low_bits) = Some xa; xa \<noteq> 0; ko = asidpool.ASIDPool xb\<rbrakk> \<Longrightarrow> P xa s proof (prove)
goal (1 subgoal):
 1. \<And>s x ko xa xb. \<lbrakk>\<forall>pd. (page_directory_at' pd s \<longrightarrow> (\<exists>pool. ko_at' (asidpool.ASIDPool pool) x s \<and> pool (asid && mask local.asid_low_bits) = Some pd)) \<longrightarrow> P pd s; 0 < asid; asid \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x; ko_at' (asidpool.ASIDPool xb) x s; xb (asid && mask local.asid_low_bits) = Some xa; xa \<noteq> 0; ko = asidpool.ASIDPool xb\<rbrakk> \<Longrightarrow> P xa s proof (prove)
goal:
No subgoals!