From 3fc4166e7e4fa64b71bc333d67e973bb553298dc Mon Sep 17 00:00:00 2001
From: Japheth Lim <Japheth.Lim@data61.csiro.au>
Date: Thu, 31 Jan 2019 17:46:19 +1100
Subject: [PATCH] AInvs: cleaner way to express ARM page table alignment

---
 proof/infoflow/Example_Valid_State.thy                 | 2 +-
 proof/invariant-abstract/ARM/ArchArch_AI.thy           | 3 ++-
 proof/invariant-abstract/ARM/ArchInvariants_AI.thy     | 4 +---
 proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy | 3 +--
 4 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/proof/infoflow/Example_Valid_State.thy b/proof/infoflow/Example_Valid_State.thy
index 71af97c59..ec06a963f 100644
--- a/proof/infoflow/Example_Valid_State.thy
+++ b/proof/infoflow/Example_Valid_State.thy
@@ -1268,7 +1268,7 @@ lemma valid_obj_s0[simp]:
                                 Low_pt_ptr_def High_pt_ptr_def
                                 shared_page_ptr_def
                                 valid_vm_rights_def vm_kernel_only_def
-                                kernel_base_def pageBits_def vmsz_aligned_def
+                                kernel_base_def pageBits_def pt_bits_def vmsz_aligned_def
                                 is_aligned_def[THEN meta_eq_to_obj_eq, THEN iffD2]
                                 is_aligned_addrFromPPtr_n)+
      apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def
diff --git a/proof/invariant-abstract/ARM/ArchArch_AI.thy b/proof/invariant-abstract/ARM/ArchArch_AI.thy
index fd541129f..5765e08b6 100644
--- a/proof/invariant-abstract/ARM/ArchArch_AI.thy
+++ b/proof/invariant-abstract/ARM/ArchArch_AI.thy
@@ -1507,7 +1507,8 @@ lemma arch_decode_inv_wf[wp]:
     apply (clarsimp simp: neq_Nil_conv)
     apply (thin_tac "Ball S P" for S P)
     apply (rule conjI)
-     apply (clarsimp simp: valid_cap_def cap_aligned_def is_aligned_addrFromPPtr_n)
+     apply (clarsimp simp: valid_cap_def cap_aligned_def
+                           pt_bits_def pageBits_def is_aligned_addrFromPPtr_n)
     apply (rule conjI)
      apply (clarsimp simp: valid_cap_def cap_aligned_def)
     apply (rule conjI)
diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy
index 5e22aed73..a83f9cda4 100644
--- a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy
+++ b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy
@@ -308,9 +308,7 @@ definition
 where
   "wellformed_pde pde \<equiv> case pde of
      pde.PageTablePDE p attr mw \<Rightarrow>
-       attr \<subseteq> {ParityEnabled}
-       \<comment> \<open>We don't have a variant of this alignment check that takes an @{const APageTable}. Yuck.\<close>
-       \<and> is_aligned p (arch_obj_size (PageTableCap undefined undefined))
+       attr \<subseteq> {ParityEnabled} \<and> is_aligned p pt_bits
    | pde.SectionPDE p attr mw r \<Rightarrow>
        r \<in> valid_vm_rights \<and> vmsz_aligned p ARMSection
    | pde.SuperSectionPDE p attr r \<Rightarrow>
diff --git a/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
index 0d2910ca6..6bb5ed7eb 100644
--- a/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy
@@ -324,8 +324,7 @@ definition
 where
   "wellformed_pde pde \<equiv> case pde of
      pde.PageTablePDE p \<Rightarrow>
-       \<comment> \<open>We don't have a variant of this alignment check that takes an @{const APageTable}. Yuck.\<close>
-       is_aligned p (arch_obj_size (PageTableCap undefined undefined))
+       is_aligned p pt_bits
    | pde.SectionPDE p attr r \<Rightarrow>
        r \<in> valid_vm_rights \<and> vmsz_aligned p ARMSection
    | pde.SuperSectionPDE p attr r \<Rightarrow>