theory ArchFinalise_AI

lemma arch_finalise_case_no_lookup:
  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_objs and
    valid_cap (cap.ArchObjectCap acap) and (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s)
    and K (aobj_ref acap = Some w \<and> is_final)\<rbrace>
  arch_finalise_cap acap is_final
  \<lbrace>\<lambda>rv s. (\<forall>vs. vs_cap_ref (cap.ArchObjectCap acap) = Some vs \<longrightarrow> \<not> (vs \<unrhd> w) s)\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (simp add: arch_finalise_cap_def) apply (wpc | wp delete_asid_pool_unmapped hoare_vcg_imp_lift
                   unmap_page_table_unmapped3
              | simp add: vs_cap_ref_simps
                          vs_lookup_pages_eq_at[THEN fun_cong, symmetric]
                          vs_lookup_pages_eq_ap[THEN fun_cong, symmetric])+ apply (wp hoare_vcg_all_lift unmap_page_unmapped hoare_weak_lift_imp) apply (wpc|wp unmap_page_table_unmapped3 delete_asid_unmapped
      |simp add:vs_cap_ref_def
      vs_lookup_pages_eq_at[THEN fun_cong,symmetric]
      vs_lookup_pages_eq_ap[THEN fun_cong,symmetric])+ apply (auto simp: valid_cap_simps valid_arch_state_def data_at_def
              split: vmpage_size.split if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and valid_objs and valid_cap (ArchObjectCap acap) and (\<lambda>s. valid_asid_table (asid_table s) s) and K (aobj_ref acap = Some w \<and> is_final)\<rbrace> arch_finalise_cap acap is_final \<lbrace>\<lambda>rv s. \<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (1 subgoal):
 1. aobj_ref acap = Some w \<and> is_final \<Longrightarrow> \<lbrace>pspace_aligned and valid_vspace_objs and valid_objs and valid_cap (ArchObjectCap acap) and (\<lambda>s. valid_asid_table (asid_table s) s)\<rbrace> arch_finalise_cap acap is_final \<lbrace>\<lambda>rv s. \<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s\<rbrace> proof (prove)
goal (2 subgoals):
 1. aobj_ref acap = Some w \<and> is_final \<Longrightarrow> \<lbrace>?Q2\<rbrace> arch_finalise_cap acap is_final \<lbrace>\<lambda>rv s. \<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s\<rbrace>
 2. \<And>s. \<lbrakk>aobj_ref acap = Some w \<and> is_final; (pspace_aligned and valid_vspace_objs and valid_objs and valid_cap (ArchObjectCap acap) and (\<lambda>s. valid_asid_table (asid_table s) s)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. aobj_ref acap = Some w \<and> is_final \<Longrightarrow> \<lbrace>?Q2\<rbrace> case acap of ASIDPoolCap ptr b \<Rightarrow> case True of True \<Rightarrow> do delete_asid_pool b ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | ASIDControlCap \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s None \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do unmap_page s a v ptr;
return (NullCap, NullCap)
od | PageTableCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageTableCap ptr (Some (a, v)) \<Rightarrow> case True of True \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr (Some a) \<Rightarrow> case True of True \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s\<rbrace>
 2. \<And>s. \<lbrakk>aobj_ref acap = Some w \<and> is_final; (pspace_aligned and valid_vspace_objs and valid_objs and valid_cap (ArchObjectCap acap) and (\<lambda>s. valid_asid_table (asid_table s) s)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>x31 x33 x34 x35 x2 x1 x2a. \<lbrakk>is_final; acap = PageCap x31 w x33 x34 (Some (x1, x2a)); x35 = Some (x1, x2a); x2 = (x1, x2a)\<rbrakk> \<Longrightarrow> \<lbrace>?R81 x31 w x33 x34 (Some (x1, x2a)) (x1, x2a) x1 x2a\<rbrace> unmap_page x34 x1 x2a w \<lbrace>\<lambda>x a. \<forall>vs. vs_cap_ref (ArchObjectCap (PageCap x31 w x33 x34 (Some (x1, x2a)))) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages a\<rbrace>
 2. \<And>x41 x42. \<lbrakk>aobj_ref acap = Some w \<and> is_final; acap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x41 x42\<rbrace> case x42 of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> case True of True \<Rightarrow> do unmap_page_table a v x41;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s\<rbrace>
 3. \<And>x51 x52. \<lbrakk>aobj_ref acap = Some w \<and> is_final; acap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x51 x52\<rbrace> case x52 of None \<Rightarrow> return (NullCap, NullCap) | Some a \<Rightarrow> case True of True \<Rightarrow> do delete_asid a x51;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s\<rbrace>
 4. \<And>s. \<lbrakk>aobj_ref acap = Some w \<and> is_final; (pspace_aligned and valid_vspace_objs and valid_objs and valid_cap (ArchObjectCap acap) and (\<lambda>s. valid_asid_table (asid_table s) s)) s\<rbrakk> \<Longrightarrow> (\<forall>x xa. acap = ASIDPoolCap x xa \<longrightarrow> (True = True \<longrightarrow> True) \<and> (True = False \<longrightarrow> (\<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s))) \<and> (acap = ASIDControlCap \<longrightarrow> (\<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s)) \<and> (\<forall>x xa xb xc xd. acap = PageCap x xa xb xc xd \<longrightarrow> (xd = None \<longrightarrow> (\<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s)) \<and> (\<forall>xe. xd = Some xe \<longrightarrow> (\<forall>xf xg. xe = (xf, xg) \<longrightarrow> ?R81 x xa xb xc xd xe xf xg s))) \<and> (\<forall>x xa. acap = PageTableCap x xa \<longrightarrow> ?R32 x xa s) \<and> (\<forall>x xa. acap = PageDirectoryCap x xa \<longrightarrow> ?R33 x xa s) proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42. \<lbrakk>aobj_ref acap = Some w \<and> is_final; acap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>?R32 x41 x42\<rbrace> case x42 of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> case True of True \<Rightarrow> do unmap_page_table a v x41;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s\<rbrace>
 2. \<And>x51 x52. \<lbrakk>aobj_ref acap = Some w \<and> is_final; acap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>?R33 x51 x52\<rbrace> case x52 of None \<Rightarrow> return (NullCap, NullCap) | Some a \<Rightarrow> case True of True \<Rightarrow> do delete_asid a x51;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s\<rbrace>
 3. \<And>s. \<lbrakk>aobj_ref acap = Some w \<and> is_final; (pspace_aligned and valid_vspace_objs and valid_objs and valid_cap (ArchObjectCap acap) and (\<lambda>s. valid_asid_table (asid_table s) s)) s\<rbrakk> \<Longrightarrow> (\<forall>x xa. acap = ASIDPoolCap x xa \<longrightarrow> (True = True \<longrightarrow> True) \<and> (True = False \<longrightarrow> (\<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s))) \<and> (acap = ASIDControlCap \<longrightarrow> (\<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s)) \<and> (\<forall>x xa xb xc xd. acap = PageCap x xa xb xc xd \<longrightarrow> (xd = None \<longrightarrow> (\<forall>vs. vs_cap_ref (ArchObjectCap acap) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s)) \<and> (\<forall>xe. xd = Some xe \<longrightarrow> (\<forall>xf xg. xe = (xf, xg) \<longrightarrow> (\<forall>xe. vs_cap_ref (ArchObjectCap (PageCap x xa xb xc xd)) = Some xe \<longrightarrow> (pspace_aligned and valid_vspace_objs and data_at xc xa and valid_objs and (\<lambda>s. valid_asid_table (asid_table s) s) and K ((xc = ARMSmallPage \<or> xc = ARMLargePage \<longrightarrow> xe = [VSRef ((xg >> 12) && mask 8) (Some APageTable), VSRef (xg >> 20) (Some APageDirectory), VSRef (xf && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of xf)) None]) \<and> (xc = ARMSection \<or> xc = ARMSuperSection \<longrightarrow> xe = [VSRef (xg >> 20) (Some APageDirectory), VSRef (xf && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of xf)) None]) \<and> xa = xa)) s)))) \<and> (\<forall>x xa. acap = PageTableCap x xa \<longrightarrow> ?R32 x xa s) \<and> (\<forall>x xa. acap = PageDirectoryCap x xa \<longrightarrow> ?R33 x xa s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>aobj_ref acap = Some w \<and> is_final; pspace_aligned s \<and> valid_vspace_objs s \<and> valid_objs s \<and> s \<turnstile> ArchObjectCap acap \<and> valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd. acap = PageCap x xa xb xc xd \<longrightarrow> (xd = None \<longrightarrow> (\<forall>vs. (case xc of ARMSection \<Rightarrow> case None of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ARMSuperSection \<Rightarrow> case None of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> case None of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some vs \<longrightarrow> (vs, w) \<notin> vs_lookup_pages s)) \<and> (\<forall>a b. xd = Some (a, b) \<longrightarrow> (\<forall>x. (case xc of ARMSection \<Rightarrow> case Some (a, b) of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ARMSuperSection \<Rightarrow> case Some (a, b) of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> case Some (a, b) of None \<Rightarrow> None | Some (asid, vptr) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) = Some x \<longrightarrow> data_at xc xa s \<and> (xc = ARMSmallPage \<longrightarrow> x = [VSRef ((b >> 12) && mask 8) (Some APageTable), VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> (xc = ARMLargePage \<longrightarrow> x = [VSRef ((b >> 12) && mask 8) (Some APageTable), VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> (xc = ARMSection \<longrightarrow> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) \<and> (xc = ARMSuperSection \<longrightarrow> x = [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None])))) \<and> (\<forall>x xa. acap = PageTableCap x xa \<longrightarrow> (\<exists>a b. xa = Some (a, b)) \<longrightarrow> typ_at (AArch APageTable) x s) proof (prove)
goal:
No subgoals!