theory Arch_R

lemma findPDForASID_aligned[wp]:
  "\<lbrace>valid_objs'\<rbrace> findPDForASID p \<lbrace>\<lambda>rv s. is_aligned rv pdBits\<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)+ apply clarsimp apply (drule(1) obj_at_valid_objs') apply (clarsimp simp: projectKOs valid_obj'_def inv_ASIDPool ranI
                 split: asidpool.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> findPDForASID p \<lbrace>\<lambda>rv s. is_aligned rv pdBits\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> doE y <- if 0 < p then returnOk () else fail;
y <- if p \<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 p)) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> liftE (getObject ptr));
case pool (p && 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>\<lambda>rv s. is_aligned rv pdBits\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'4\<rbrace> doE y <- if 0 < p then returnOk () else fail;
y <- if p \<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 p)) of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> liftE (getObject ptr));
case pool (p && 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>\<lambda>rv s. is_aligned rv pdBits\<rbrace>, -
 2. \<And>s. valid_objs' s \<Longrightarrow> ?P'4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<Longrightarrow> True \<and> True \<and> True \<and> True \<and> (0 < p \<longrightarrow> (p \<le> snd asidRange \<longrightarrow> ((armKSASIDTable \<circ> ksArchState) s (UCAST(7 \<rightarrow> 32) (asid_high_bits_of p)) = None \<longrightarrow> True) \<and> (\<forall>x. (armKSASIDTable \<circ> ksArchState) s (UCAST(7 \<rightarrow> 32) (asid_high_bits_of p)) = Some x \<longrightarrow> (\<forall>ko. ko_at' ko x s \<longrightarrow> ((\<lambda>pool s. (pool (p && mask local.asid_low_bits) = None \<longrightarrow> True) \<and> (\<forall>x. pool (p && mask local.asid_low_bits) = Some x \<longrightarrow> True \<and> True \<and> is_aligned x pdBits)) \<circ> inv asidpool.ASIDPool) ko s))) \<and> (\<not> p \<le> snd asidRange \<longrightarrow> True)) \<and> (\<not> 0 < p \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s x ko xa. \<lbrakk>valid_objs' s; 0 < p; p \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of p)) = Some x; ko_at' ko x s; inv asidpool.ASIDPool ko (p && mask local.asid_low_bits) = Some xa\<rbrakk> \<Longrightarrow> is_aligned xa pdBits proof (prove)
goal (1 subgoal):
 1. \<And>s x ko xa. \<lbrakk>valid_objs' s; 0 < p; p \<le> snd asidRange; armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of p)) = Some x; inv asidpool.ASIDPool ko (p && mask local.asid_low_bits) = Some xa; \<exists>k. k = ko \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> is_aligned xa pdBits proof (prove)
goal:
No subgoals!