theory Finalise_R

lemma deleteASID_invs'[wp]:
  "\<lbrace>invs'\<rbrace> deleteASID asid pd \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: deleteASID_def cong: option.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ apply (rule_tac Q="\<lambda>rv. valid_obj' (injectKO rv) and invs'"
              in hoare_post_imp) apply (rename_tac rv s) apply (clarsimp split: if_split_asm del: subsetI) apply (simp add: fun_upd_def[symmetric] valid_obj'_def) apply (case_tac rv, simp) apply (subst inv_f_f, rule inj_onI, simp)+ apply (rule conjI) apply clarsimp apply (drule subsetD, blast) apply clarsimp apply (auto dest!: ran_del_subset)[1] apply (wp getObject_valid_obj getObject_inv loadObject_default_inv
             | simp add: objBits_simps archObjSize_def pageBits_def)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> deleteASID asid pd \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do asidTable <- gets (armKSASIDTable \<circ> ksArchState);
case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) of None \<Rightarrow> return () | Some poolPtr \<Rightarrow> do pool <- liftM (inv asidpool.ASIDPool) (getObject poolPtr);
when (pool (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject poolPtr (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
od
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do asidTable <- gets (armKSASIDTable \<circ> ksArchState);
case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) of None \<Rightarrow> return () | Some poolPtr \<Rightarrow> do pool <- liftM (inv asidpool.ASIDPool) (getObject poolPtr);
when (pool (asid && mask local.asid_low_bits) = Some pd) (do y <- flushSpace asid;
y <- invalidateASIDEntry asid;
y <- setObject poolPtr (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None)));
getCurThread >>= setVMRoot
od)
od
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>(\<lambda>pool. if pool (asid && mask local.asid_low_bits) = Some pd then \<lambda>s. invs' s \<and> valid_asid_pool' (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None))) s else invs') \<circ> inv asidpool.ASIDPool\<rbrace>
 2. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 3. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asidTable x2 rv s. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; (valid_obj' (injectKOS rv) and invs') s\<rbrakk> \<Longrightarrow> ((\<lambda>pool. if pool (asid && mask local.asid_low_bits) = Some pd then \<lambda>s. invs' s \<and> valid_asid_pool' (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None))) s else invs') \<circ> inv asidpool.ASIDPool) rv s
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asidTable x2 rv s. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; (valid_obj' (injectKOS rv) and invs') s\<rbrakk> \<Longrightarrow> ((\<lambda>pool. if pool (asid && mask local.asid_low_bits) = Some pd then \<lambda>s. invs' s \<and> valid_asid_pool' (asidpool.ASIDPool (pool(asid && mask local.asid_low_bits := None))) s else invs') \<circ> inv asidpool.ASIDPool) rv s
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asidTable x2 rv s. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; valid_obj' (KOArch (KOASIDPool rv)) s; invs' s; inv asidpool.ASIDPool rv (asid && mask local.asid_low_bits) = Some pd\<rbrakk> \<Longrightarrow> dom (inv asidpool.ASIDPool rv) - {asid && mask local.asid_low_bits} \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool rv)(asid && mask local.asid_low_bits := None)) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool rv)(asid && mask local.asid_low_bits := None)). is_aligned x pdBits)
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asidTable x2 rv s. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; valid_asid_pool' rv s; invs' s; inv asidpool.ASIDPool rv (asid && mask local.asid_low_bits) = Some pd\<rbrakk> \<Longrightarrow> dom (inv asidpool.ASIDPool rv) - {asid && mask local.asid_low_bits} \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool rv)(asid && mask local.asid_low_bits := None)) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool rv)(asid && mask local.asid_low_bits := None)). is_aligned x pdBits)
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asidTable x2 rv s x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran x \<and> (\<forall>x\<in>ran x. is_aligned x pdBits); invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; rv = asidpool.ASIDPool x\<rbrakk> \<Longrightarrow> dom (inv asidpool.ASIDPool (asidpool.ASIDPool x)) - {asid && mask local.asid_low_bits} \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran ((inv asidpool.ASIDPool (asidpool.ASIDPool x))(asid && mask local.asid_low_bits := None)) \<and> (\<forall>x\<in>ran ((inv asidpool.ASIDPool (asidpool.ASIDPool x))(asid && mask local.asid_low_bits := None)). is_aligned x pdBits)
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asidTable x2 rv s x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran x \<and> (\<forall>x\<in>ran x. is_aligned x pdBits); invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; rv = asidpool.ASIDPool x\<rbrakk> \<Longrightarrow> dom x - {asid && mask local.asid_low_bits} \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran (x(asid && mask local.asid_low_bits := None)) \<and> (\<forall>x\<in>ran (x(asid && mask local.asid_low_bits := None)). is_aligned x pdBits)
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2 rv s x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran x \<and> (\<forall>x\<in>ran x. is_aligned x pdBits); invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; rv = asidpool.ASIDPool x\<rbrakk> \<Longrightarrow> dom x - {asid && mask local.asid_low_bits} \<subseteq> {0..2 ^ local.asid_low_bits - 1}
 2. \<And>asidTable x2 rv s x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran x \<and> (\<forall>x\<in>ran x. is_aligned x pdBits); invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; rv = asidpool.ASIDPool x\<rbrakk> \<Longrightarrow> 0 \<notin> ran (x(asid && mask local.asid_low_bits := None)) \<and> (\<forall>x\<in>ran (x(asid && mask local.asid_low_bits := None)). is_aligned x pdBits)
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2 s x xa y. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; \<not> xa \<le> 2 ^ local.asid_low_bits - 1; x xa = Some y; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran x; \<forall>x\<in>ran x. is_aligned x pdBits\<rbrakk> \<Longrightarrow> xa = asid && mask local.asid_low_bits
 2. \<And>asidTable x2 rv s x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran x \<and> (\<forall>x\<in>ran x. is_aligned x pdBits); invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; rv = asidpool.ASIDPool x\<rbrakk> \<Longrightarrow> 0 \<notin> ran (x(asid && mask local.asid_low_bits := None)) \<and> (\<forall>x\<in>ran (x(asid && mask local.asid_low_bits := None)). is_aligned x pdBits)
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>asidTable x2 s x xa y. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; \<not> xa \<le> 2 ^ local.asid_low_bits - 1; x xa = Some y; 0 \<notin> ran x; \<forall>x\<in>ran x. is_aligned x pdBits; xa \<in> {0..2 ^ local.asid_low_bits - 1}\<rbrakk> \<Longrightarrow> xa = asid && mask local.asid_low_bits
 2. \<And>asidTable x2 rv s x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran x \<and> (\<forall>x\<in>ran x. is_aligned x pdBits); invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; rv = asidpool.ASIDPool x\<rbrakk> \<Longrightarrow> 0 \<notin> ran (x(asid && mask local.asid_low_bits := None)) \<and> (\<forall>x\<in>ran (x(asid && mask local.asid_low_bits := None)). is_aligned x pdBits)
 3. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>asidTable x2 rv s x. \<lbrakk>asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2; dom x \<subseteq> {0..2 ^ local.asid_low_bits - 1} \<and> 0 \<notin> ran x \<and> (\<forall>x\<in>ran x. is_aligned x pdBits); invs' s; inv asidpool.ASIDPool (asidpool.ASIDPool x) (asid && mask local.asid_low_bits) = Some pd; rv = asidpool.ASIDPool x\<rbrakk> \<Longrightarrow> 0 \<notin> ran (x(asid && mask local.asid_low_bits := None)) \<and> (\<forall>x\<in>ran (x(asid && mask local.asid_low_bits := None)). is_aligned x pdBits)
 2. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<And>asidTable x2. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x2 \<Longrightarrow> \<lbrace>?R19 asidTable x2\<rbrace> getObject x2 \<lbrace>\<lambda>rv. valid_obj' (injectKOS rv) and invs'\<rbrace>
 2. \<lbrace>?Q4\<rbrace> gets (armKSASIDTable \<circ> ksArchState) \<lbrace>\<lambda>asidTable s. (asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None \<longrightarrow> invs' s) \<and> (\<forall>x. asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x \<longrightarrow> ?R19 asidTable x s)\<rbrace>
 3. \<And>s. invs' s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> (\<exists>x. armKSASIDTable (ksArchState s) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = Some x) \<longrightarrow> valid_objs' s proof (prove)
goal:
No subgoals!