x64: fix sorry proofs in ArchAInvsPre_AI

The canonical_address constant (but not its definition) is now exported
to generic theories, and used in do_user_op. On ARM, all virtual
addresses are canonical.

proof/invariant-abstract/ADT_AI.thy

@@ -220,10 +220,14 @@ definition
                        ,(ds \<circ> ptrFromPAddr) |`  {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va} ) 
                      ));
       do_machine_op (user_memory_update
-                       ((um' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va}
+                       ((um' |` {pa. \<exists>va. canonical_address va
+                                            \<and> conv va = Some pa
+                                            \<and> AllowWrite \<in> rights va}
                       \<circ> addrFromPPtr) |` (- dom ds)));
       do_machine_op (device_memory_update
-                       ((ds' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va}
+                       ((ds' |` {pa. \<exists>va. canonical_address va
+                                            \<and> conv va = Some pa
+                                            \<and> AllowWrite \<in> rights va}
                       \<circ> addrFromPPtr) |` (dom ds)));
       return (e, tc')
    od" 

proof/invariant-abstract/AInvs.thy

@@ -115,8 +115,7 @@ lemma do_user_op_invs:
                         restrict_map_def invs_def cur_tcb_def
                  split: option.splits if_split_asm)
   apply (frule ptable_rights_imp_frame)
-    apply fastforce
+     apply fastforce+
-   apply simp
   apply (clarsimp simp: valid_state_def device_frame_in_device_region)
   done
 

proof/invariant-abstract/AInvsPre.thy

@@ -16,7 +16,7 @@ locale AInvsPre =
   fixes state_ext_type1 :: "('a :: state_ext) itself"
   assumes ptable_rights_imp_frame:
     "\<And> (s :: 'a state) t x y. 
-     valid_state s \<Longrightarrow> 
+     valid_state s \<Longrightarrow> canonical_address x \<Longrightarrow>
        ptable_rights t s x \<noteq> {} \<Longrightarrow>
        ptable_lift t s x = Some (addrFromPPtr y) \<Longrightarrow>
          in_user_frame y s \<or> in_device_frame y s"

proof/invariant-abstract/ARM/ArchAInvsPre.thy

@@ -202,7 +202,7 @@ named_theorems AInvsPre_asms
 
 
 lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]:
-  assumes "valid_state s"
+  assumes "valid_state s" "canonical_address x"
   shows "ptable_rights t s x \<noteq> {} \<Longrightarrow>
          ptable_lift t s x = Some (addrFromPPtr y) \<Longrightarrow>
          in_user_frame y s \<or> in_device_frame y s"

proof/invariant-abstract/ARM/ArchInvariants_AI.thy

@@ -75,6 +75,11 @@ lemmas a_type_simps = a_type_def[split_simps kernel_object.split arch_kernel_obj
 definition
   "vmsz_aligned ref sz \<equiv> is_aligned ref (pageBitsForSize sz)"
 
+(* There are no non-canonical addresses on 32-bit ARM. *)
+definition canonical_address :: "obj_ref \<Rightarrow> bool"
+where
+  "canonical_address p \<equiv> True"
+
 definition
   "wellformed_mapdata sz \<equiv>
    \<lambda>(asid, vref). 0 < asid \<and> asid \<le> 2^asid_bits - 1

proof/invariant-abstract/Invariants_AI.thy

@@ -45,6 +45,7 @@ requalify_consts
 
   ASIDPoolObj
 
+  canonical_address
   vs_lookup1
   vs_lookup_trans
   vs_refs

proof/invariant-abstract/X64/ArchADT_AI.thy

@@ -234,7 +234,7 @@ text {*
   @{text get_page_info} takes the architecture-specific part of the kernel heap,
   a reference to the page directory, and a virtual memory address.
   It returns a tuple containing
-  (a) the physical address, where the associated page table starts,
+  (a) the physical address, where the associated page starts,
   (b) the page table's size in bits, and
   (c) the page attributes (cachable, XNever, etc)
   (d) the access rights (a subset of @{term "{AllowRead, AllowWrite}"}).

proof/invariant-abstract/X64/ArchAInvsPre.thy

@@ -115,18 +115,15 @@ lemma get_page_info_gpd_kmaps:
     get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
                   (x64_global_pml4 (arch_state s)) p = Some (b, a, attr, r)\<rbrakk>
    \<Longrightarrow> p \<in> kernel_mappings"
-   apply (clarsimp simp: valid_global_objs_def valid_arch_state_def)
+  apply (clarsimp simp: valid_global_objs_def valid_arch_state_def
-   apply (thin_tac "Ball x y" for x y)
+                        obj_at_def valid_ao_at_def
-   apply (clarsimp simp add: obj_at_def valid_ao_at_def)
+                        empty_table_def kernel_mappings_slots_eq)
-   apply (clarsimp simp: empty_table_def kernel_mappings_slots_eq)
+  apply (drule_tac x="ucast (p >> pml4_shift_bits)" in spec; clarsimp)
-   apply (drule_tac x="ucast (p >> pml4_shift_bits)" in spec)
+  apply (rule ccontr)
-   apply (rule ccontr, simp)
+  apply (clarsimp simp: get_page_info_def get_pml4_entry_def get_arch_obj_def
-   apply (clarsimp simp: get_page_info_def get_pml4_entry_def get_arch_obj_def
+                        bit_simps ucast_ucast_mask9
-                         get_pdpt_info_def get_pdpt_entry_def get_pd_info_def get_pd_entry_def
+                 split: option.splits pml4e.splits arch_kernel_obj.splits)
-                         get_pt_info_def get_pt_entry_def
+  done
-                  split: option.splits arch_kernel_obj.splits kernel_object.splits
-                         pml4e.splits pdpte.splits pde.splits pte.splits)
-   sorry
 
 lemma get_vspace_of_thread_reachable:
   "get_vspace_of_thread (kheap s) (arch_state s) t \<noteq> x64_global_pml4 (arch_state s)
@@ -145,60 +142,29 @@ lemma is_aligned_ptrFromPAddrD:
   done
 
 lemma some_get_page_info_umapsD:
-  "\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r);
+  "\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pml4_ref p = Some (b, a, attr, r);
-    (\<exists>\<rhd> pd_ref) s; p \<notin> kernel_mappings; valid_arch_objs s; pspace_aligned s;
+    (\<exists>\<rhd> pml4_ref) s; p \<notin> kernel_mappings; valid_arch_objs s; pspace_aligned s;
+    canonical_address p;
     valid_asid_table (x64_asid_table (arch_state s)) s; valid_objs s\<rbrakk>
-   \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and>
+   \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s"
-             typ_at (AArch (AIntData sz)) (ptrFromPAddr b) s)"
+  apply (clarsimp simp: get_page_info_def get_pdpt_info_def get_pd_info_def get_pt_info_def
-  apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def
+                        get_pml4_entry_def get_pdpt_entry_def get_pd_entry_def get_pt_entry_def
+                        get_arch_obj_def valid_asid_table_def bit_simps
                         kernel_mappings_slots_eq
-                 split: option.splits Structures_A.kernel_object.splits
+                 split: option.splits kernel_object.splits arch_kernel_obj.splits
-                        arch_kernel_obj.splits)
+                        pml4e.splits pdpte.splits pde.splits pte.splits)
-  apply (frule (1) valid_arch_objsD[rotated 2])
+    apply (all \<open>drule (2) vs_lookup_step_alt[OF _ _ vs_refs_pml4I],
-   apply (simp add: obj_at_def)
+                simp add: ucast_ucast_mask9, fastforce\<close>)
-  sorry (*
+    prefer 3 subgoal
-  apply (simp add: valid_arch_obj_def)
+      by (rule exI[of _ X64HugePage]; frule (3) valid_arch_objs_entryD;
-  apply (drule bspec, simp)
+          clarsimp simp: bit_simps vmsz_aligned_def)
-  apply (simp split: pde.splits)
+   apply (all \<open>drule (2) vs_lookup_step_alt[OF _ _ vs_refs_pdptI], fastforce\<close>)
-     apply (rename_tac rs pd pt_ref rights w)
+   prefer 2 subgoal
-     apply (subgoal_tac
+     by (rule exI[of _ X64LargePage]; frule (3) valid_arch_objs_entryD;
-        "((rs, pd_ref) \<rhd>1
+         clarsimp simp: bit_simps vmsz_aligned_def)
-          (VSRef (ucast (ucast (p >> 20))) (Some APageDirectory) # rs,
+  apply (drule (2) vs_lookup_step_alt[OF _ _ vs_refs_pdI], fastforce)
-           ptrFromPAddr pt_ref)) s")
+  by (rule exI[of _ X64SmallPage]; frule (3) valid_arch_objs_entryD;
-     prefer 2
+      clarsimp simp: bit_simps vmsz_aligned_def)
-     apply (rule vs_lookup1I[rotated 2], simp)
-      apply (simp add: obj_at_def)
-     apply (simp add: vs_refs_def pde_ref_def image_def graph_of_def)
-     apply (rule exI, rule conjI, simp+)
-    apply (frule (1) vs_lookup_step)
-    apply (drule (2) stronger_arch_objsD[where ref="x # xs" for x xs])
-    apply clarsimp
-    apply (case_tac ao, simp_all add: a_type_simps obj_at_def)[1]
-    apply (simp add: get_pt_info_def get_pt_entry_def)
-    apply (drule_tac x="(ucast ((p >> 12) && mask 8))" in spec)
-    apply (clarsimp simp: obj_at_def valid_arch_obj_def
-      split: pte.splits)
-     apply (clarsimp simp: pspace_aligned_def)
-     apply (drule_tac x = "(ptrFromPAddr b)" in  bspec, fastforce)
-     apply (drule is_aligned_ptrFromPAddrD)
-      apply simp
-     apply (clarsimp simp:a_type_simps)
-    apply (clarsimp simp: pspace_aligned_def)
-    apply (drule_tac x = "(ptrFromPAddr b)" in  bspec, fastforce)
-    apply (drule is_aligned_ptrFromPAddrD)
-     apply simp
-    apply (clarsimp simp:a_type_simps)
-   apply (clarsimp simp: pspace_aligned_def obj_at_def)
-   apply (drule_tac x = "(ptrFromPAddr b)" in  bspec, fastforce)
-   apply (drule is_aligned_ptrFromPAddrD)
-    apply simp
-   apply (clarsimp simp:a_type_simps)
-  apply (clarsimp simp: pspace_aligned_def obj_at_def)
-  apply (drule_tac x = "(ptrFromPAddr b)" in  bspec, fastforce)
-  apply (drule is_aligned_ptrFromPAddrD)
-   apply simp
-   apply (clarsimp simp:a_type_simps)
-  done *)
 
 lemma user_mem_dom_cong:
   "kheap s = kheap s' \<Longrightarrow> dom (user_mem s) = dom (user_mem s')"
@@ -216,52 +182,49 @@ lemma device_frame_in_device_region:
 global_naming Arch
 named_theorems AInvsPre_asms
 
-lemma (* ptable_rights_imp_user_frame *)[AInvsPre_asms]:
+lemma ptable_rights_imp_frame[AInvsPre_asms]:
-  assumes "valid_state s"
+  assumes "valid_state s" "canonical_address x"
   shows "ptable_rights t s x \<noteq> {} \<Longrightarrow>
          ptable_lift t s x = Some (addrFromPPtr y) \<Longrightarrow>
-         in_user_frame y s"
+         in_user_frame y s \<or> in_device_frame y s"
-  sorry (*
+  apply (rule ccontr)
-  apply (clarsimp simp: ptable_rights_def ptable_lift_def in_user_frame_def
+  using assms
+  apply (clarsimp simp: ptable_lift_def ptable_rights_def
+                        in_user_frame_def in_device_frame_def
                  split: option.splits)
-  apply (rename_tac b a r)
   apply (case_tac "x \<in> kernel_mappings")
-   apply (frule (1) some_get_page_info_kmapsD)
+   apply (frule (2) some_get_page_info_kmapsD; fastforce simp: valid_state_def)
-     using assms
-     apply (clarsimp simp add: valid_state_def)
-    using assms
-    apply (clarsimp simp add: valid_state_def)
-   apply simp
   apply (frule some_get_page_info_umapsD)
-       apply (rule get_vspace_of_thread_reachable)
+        apply (rule get_vspace_of_thread_reachable)
-       apply clarsimp
+        apply clarsimp
-       apply (frule get_page_info_gpd_kmaps[rotated 2])
+        apply (frule get_page_info_gpd_kmaps[rotated 2])
-          using assms
+           apply (simp_all add: valid_state_def valid_pspace_def
-          apply (simp_all add: valid_state_def valid_pspace_def
+                                valid_arch_state_def)
-                               valid_arch_state_def)
+    apply (clarsimp simp: data_at_def)+
-  apply clarsimp
+  apply (drule_tac x=sz in spec)+
-  apply (frule is_aligned_add_helper[OF _ and_mask_less',
+  apply (rename_tac p_addr attr rghts sz)
-                                     THEN conjunct2, of _ _ x])
+  apply (frule is_aligned_add_helper[OF _ and_mask_less', THEN conjunct2, of _ _ x])
    apply (simp only: pbfs_less_wb'[simplified word_bits_def])
-  apply (clarsimp simp: ptrFromPAddr_def Platform.X64.addrFromPPtr_def
+  apply (clarsimp simp: data_at_def ptrFromPAddr_def addrFromPPtr_def field_simps)
-                        field_simps)
+  apply (subgoal_tac "p_addr + (pptrBase + (x && mask (pageBitsForSize sz)))
-  apply (rule_tac x=sz in exI)
+                        && ~~ mask (pageBitsForSize sz) = p_addr + pptrBase")
+   apply simp
   apply (subst add.assoc[symmetric])
   apply (subst is_aligned_add_helper)
     apply (erule aligned_add_aligned)
-      apply (case_tac sz, simp_all add: physMappingOffset_def
+     apply (case_tac sz; simp add: is_aligned_def pptrBase_def bit_simps)
-                            kernelBase_addr_def physBase_def is_aligned_def)[1]
+    apply simp
-     apply (case_tac sz, simp_all add: word_bits_conv)[1]
    apply (rule and_mask_less')
-   apply (case_tac sz, simp_all add: word_bits_conv)[1]
+   apply (case_tac sz; simp add: bit_simps)
   apply simp
-  done *)
+  done
+
 end
 
 interpretation AInvsPre?: AInvsPre
   proof goal_cases
   interpret Arch .
-  case 1 show ?case apply (intro_locales; (unfold_locales, fact AInvsPre_asms)?) sorry
+  case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_asms)?)
   qed
 
 requalify_facts
@@ -269,5 +232,4 @@ requalify_facts
   X64.device_mem_dom_cong
   X64.device_frame_in_device_region
 
-
 end

proof/invariant-abstract/X64/ArchInvariants_AI.thy

@@ -2973,6 +2973,40 @@ lemma valid_arch_obj_default':
   unfolding default_arch_object_def
   by (cases aobject_type; simp)
 
+lemma valid_arch_obj_entryD:
+  shows valid_arch_obj_pml4eD: "\<lbrakk>valid_arch_obj (PageMapL4 pm) s; pm i = pml4e; i \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_pml4e pml4e s"
+    and valid_arch_obj_pdpteD: "\<lbrakk>valid_arch_obj (PDPointerTable pdpt) s; pdpt i = pdpte\<rbrakk> \<Longrightarrow> valid_pdpte pdpte s"
+    and valid_arch_obj_pdeD  : "\<lbrakk>valid_arch_obj (PageDirectory pd) s; pd i = pde\<rbrakk> \<Longrightarrow> valid_pde pde s"
+    and valid_arch_obj_pteD  : "\<lbrakk>valid_arch_obj (PageTable pt) s; pt i = pte\<rbrakk> \<Longrightarrow> valid_pte pte s"
+  by fastforce+
+
+lemmas valid_arch_objsD_alt'
+  = valid_arch_objsD[simplified obj_at_def, simplified]
+
+lemmas valid_arch_objs_entryD
+  = valid_arch_obj_entryD[OF valid_arch_objsD_alt']
+
+lemmas vs_lookup_step_alt
+  = vs_lookup_step[OF _ vs_lookup1I[OF _ _ refl], simplified obj_at_def, simplified]
+
+lemma pdpte_graph_ofI:
+  "\<lbrakk>pdpt x = pdpte; pdpte_ref pdpte = Some v\<rbrakk> \<Longrightarrow> (x, v) \<in> graph_of (pdpte_ref \<circ> pdpt)"
+  by (rule graph_ofI, simp)
+
+lemma vs_refs_pdptI:
+  "\<lbrakk>pdpt ((ucast (r :: machine_word)) :: 9 word) = PageDirectoryPDPTE x a b;
+     \<forall>n \<ge> 9. n < 64 \<longrightarrow> \<not> r !! n\<rbrakk>
+   \<Longrightarrow> (VSRef r (Some APDPointerTable), ptrFromPAddr x) \<in> vs_refs (ArchObj (PDPointerTable pdpt))"
+  apply (simp add: vs_refs_def)
+  apply (rule image_eqI[rotated])
+   apply (erule pdpte_graph_ofI)
+   apply (simp add: pdpte_ref_def)
+  apply (simp add: ucast_ucast_mask)
+  apply (rule word_eqI)
+  apply (simp add: word_size)
+  apply (rule ccontr, auto)
+  done
+
 end 
 
 (* 

proof/invariant-abstract/X64/ArchVSpace_AI.thy

@@ -35,7 +35,6 @@ lemma do_machine_op_lift_invs:
 
 abbreviation "canonicalise x \<equiv> (scast ((ucast x) :: 48 word)) :: 64 word"
 
-(* FIXME x64: this needs canonical_address shenanigans *)
 lemma pptr_base_shift_cast_le:
   fixes x :: "9 word"
   shows  "((pptr_base >> pml4_shift_bits) && mask ptTranslationBits \<le> ucast x) =