aarch64 ainvs+refine: move lemmas from Refine

Signed-off-by: Gerwin Klein <[email protected]>

proof/invariant-abstract/AARCH64/ArchAcc_AI.thy

@@ -817,10 +817,6 @@ lemma set_asid_pool_valid_objs [wp]:
   unfolding set_asid_pool_def
   by (wpsimp wp: set_object_valid_objs simp: valid_obj_def)
 
-lemma invs_valid_global_arch_objs:
-  "invs s \<Longrightarrow> valid_global_arch_objs s"
-  by (clarsimp simp: invs_def valid_state_def valid_arch_state_def)
-
 lemma is_aligned_pt:
   "\<lbrakk> pt_at pt_t pt s; pspace_aligned s \<rbrakk> \<Longrightarrow> is_aligned pt (pt_bits pt_t)"
   apply (clarsimp simp: obj_at_def)
@@ -2826,7 +2822,7 @@ crunches do_machine_op
   and pspace_in_kernel_window[wp]: pspace_in_kernel_window
   and cap_refs_in_kernel_window[wp]: cap_refs_in_kernel_window
   and vspace_at_asid[wp]: "\<lambda>s. P (vspace_at_asid a pt s)"
-  and valid_vs_lookup[wp]: "valid_vs_lookup"
+  and valid_vs_lookup[wp]: "\<lambda>s. P (valid_vs_lookup s)"
   and valid_obj[wp]: "valid_obj t obj"
   (simp: valid_kernel_mappings_def wp: valid_obj_typ)
 

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -1392,6 +1392,16 @@ lemma vs_lookup_slot_pte_at:
   apply (rule is_aligned_add; simp add: is_aligned_shift)
   done
 
+(* used in Refine *)
+lemma pt_lookup_slot_pte_at:
+  "\<lbrakk> vspace_for_asid asid s = Some pt; pt_lookup_slot pt vref (ptes_of s) = Some (level, slot);
+     vref \<in> user_region; invs s\<rbrakk>
+   \<Longrightarrow> pte_at (level_type level) slot s"
+  apply (drule (1) pt_lookup_slot_vs_lookup_slotI)
+  apply clarsimp
+  apply (erule (3) vs_lookup_slot_pte_at)
+  done
+
 lemma vmpage_size_of_level_pt_bits_left:
   "\<lbrakk> pt_bits_left level = pageBitsForSize vmpage_size; level \<le> max_pt_level \<rbrakk> \<Longrightarrow>
    vmsize_of_level level = vmpage_size"

proof/invariant-abstract/AARCH64/ArchBits_AI.thy

@@ -50,6 +50,18 @@ lemma invs_valid_vs_lookup[elim!]:
   "invs s \<Longrightarrow> valid_vs_lookup s "
   by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
 
+lemma invs_vmid_inv[elim!]:
+  "invs s \<Longrightarrow> vmid_inv s"
+  by (auto simp: invs_def valid_state_def valid_arch_state_def)
+
+lemma invs_valid_vmid_table[elim!]:
+  "invs s \<Longrightarrow> valid_vmid_table s"
+  by (auto simp: invs_def valid_state_def valid_arch_state_def)
+
+lemma invs_valid_global_arch_objs[elim!]:
+  "invs s \<Longrightarrow> valid_global_arch_objs s"
+  by (clarsimp simp: invs_def valid_state_def valid_arch_state_def)
+
 lemma pbfs_atleast_pageBits:
   "pageBits \<le> pageBitsForSize sz"
   by (cases sz) (auto simp: pageBits_def)

proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy

@@ -587,12 +587,15 @@ definition pspace_in_kernel_window :: "'z::state_ext state \<Rightarrow> bool" w
 definition vspace_at_asid :: "asid \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
   "vspace_at_asid asid pt \<equiv> \<lambda>s. vspace_for_asid asid s = Some pt"
 
+definition kernel_window_range :: "obj_ref set" where
+  "kernel_window_range \<equiv> {pptr_base ..< pptrTop}"
+
 definition valid_uses_2 :: "arm_vspace_region_uses \<Rightarrow> bool" where
   "valid_uses_2 uses \<equiv>
      \<forall>p. (\<not>canonical_address p \<longrightarrow> uses p = ArmVSpaceInvalidRegion)
-          \<and> (p \<in> {pptr_base ..< pptrTop}
+          \<and> (p \<in> kernel_window_range
              \<longrightarrow> uses p \<in> {ArmVSpaceKernelWindow, ArmVSpaceInvalidRegion})
-          \<and> (uses p = ArmVSpaceKernelWindow \<longrightarrow> p \<in> {pptr_base ..< pptrTop})
+          \<and> (uses p = ArmVSpaceKernelWindow \<longrightarrow> p \<in> kernel_window_range)
           \<comment> \<open>The kernel device window doesn't occupy the entire region above kdev_base\<close>
           \<and> (kdev_base \<le> p \<longrightarrow> uses p \<in> {ArmVSpaceDeviceWindow, ArmVSpaceInvalidRegion})
           \<comment> \<open>No user window in hyp kernel address space\<close>
@@ -1518,7 +1521,12 @@ lemma pptrTop_le_ipa_size:
   "pptrTop \<le> mask ipa_size"
   by (simp add: bit_simps pptrTop_def mask_def)
 
-lemma addrFromPPtr_mask_ipa: (* FIXME AARCH64: check if used; Refine needs this with >> pageBits *)
+lemma below_pptrTop_ipa_size:
+  "p < pptrTop \<Longrightarrow> p \<le> mask ipa_size"
+  using pptrTop_le_ipa_size
+  by simp
+
+lemma addrFromPPtr_mask_ipa:
   "\<lbrakk> pptr_base \<le> pt_ptr; pt_ptr < pptrTop \<rbrakk>
    \<Longrightarrow> addrFromPPtr pt_ptr && mask ipa_size = addrFromPPtr pt_ptr"
   using pptrTop_le_ipa_size
@@ -1536,7 +1544,24 @@ lemmas window_defs =
 lemma valid_uses_kernel_window:
   "\<lbrakk> valid_uses s; p \<in> kernel_window s \<rbrakk> \<Longrightarrow> p \<in> {pptr_base ..< pptrTop} \<and> canonical_address p"
   unfolding valid_uses_def window_defs
-  by (erule_tac x=p in allE) auto
+  by (erule_tac x=p in allE) (auto simp: kernel_window_range_def)
+
+lemma kernel_window_bounded:
+  "\<lbrakk> p \<in> kernel_window s; valid_uses s \<rbrakk> \<Longrightarrow> p \<in> kernel_window_range"
+  by (fastforce dest: valid_uses_kernel_window simp: kernel_window_range_def)
+
+lemma pspace_in_kw_bounded:
+  "\<lbrakk> kheap s p = Some ko; pspace_in_kernel_window s; valid_uses s; pspace_aligned s \<rbrakk> \<Longrightarrow>
+   p \<in> kernel_window_range"
+  unfolding pspace_aligned_def
+  apply (drule bspec, fastforce)
+  apply (simp add: pspace_in_kernel_window_def)
+  apply (erule allE, erule allE, erule (1) impE)
+  apply (prop_tac "p \<in> kernel_window s")
+   apply (erule set_mp)
+   apply (clarsimp simp: is_aligned_no_overflow)
+  apply (fastforce dest: kernel_window_bounded)
+  done
 
 lemma pt_walk_max_level:
   "pt_walk top_level bot_level pt_ptr vptr ptes = Some (level, p)
@@ -2281,6 +2306,15 @@ lemma valid_vspace_objsD:
    valid_vspace_obj level ao s"
   by (simp add: valid_vspace_objs_def)
 
+lemma vspace_for_asid_not_normal_pt:
+  "\<lbrakk>vspace_for_asid asid s = Some pt; normal_pt_at pt s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> False"
+  apply (drule vspace_for_asid_vs_lookup)
+  apply (clarsimp simp: pt_at_eq)
+  apply (drule (1) valid_vspace_objsD, simp)
+   apply (fastforce simp: in_omonad)
+  apply clarsimp
+  done
+
 (* A static bound on the size of pt_bits. For PA_40 configurations this is 40 (size of the
    PA/IPA address space). For PA_44 configurations, this is 48, because the page tables can
    theoretically translate 48 bits, even though the PA/IPA space is only 44 bits wide *)
@@ -2364,6 +2398,29 @@ lemma is_aligned_addrFromPPtr[intro!]:
   "is_aligned p pageBits \<Longrightarrow> is_aligned (addrFromPPtr p) pageBits"
   by (simp add: is_aligned_addrFromPPtr_n pageBits_def pptrBaseOffset_alignment_def)
 
+lemma pptrTop_ucast_ppn:
+  "\<lbrakk> p < pptrTop; is_aligned p pageBits \<rbrakk> \<Longrightarrow>
+   ucast (ucast (p >> pageBits)::ppn) = p >> pageBits"
+  apply (drule below_pptrTop_ipa_size)
+  apply word_eqI
+  using ppn_len_def'[unfolded ppn_len_def]
+  by (fastforce dest: bit_imp_le_length)
+
+lemma kernel_window_range_addrFromPPtr:
+  "p \<in> kernel_window_range \<Longrightarrow> addrFromPPtr p < pptrTop"
+  apply (simp add: kernel_window_range_def addrFromPPtr_def pptrBaseOffset_def
+                   paddrBase_def pptr_base_def)
+  apply unat_arith
+  done
+
+lemma kernel_window_addrFromPPtr:
+  "\<lbrakk> p \<in> kernel_window_range; is_aligned p pageBits \<rbrakk> \<Longrightarrow>
+   ucast (ucast (addrFromPPtr p >> pageBits)::ppn) = addrFromPPtr p >> pageBits"
+  apply (rule pptrTop_ucast_ppn)
+   apply (erule kernel_window_range_addrFromPPtr)
+  apply (erule is_aligned_addrFromPPtr)
+  done
+
 lemma is_aligned_ptrFromPAddr_n:
   "\<lbrakk>is_aligned x sz; sz \<le> pptrBaseOffset_alignment\<rbrakk>
    \<Longrightarrow> is_aligned (ptrFromPAddr x) sz"

proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy

@@ -739,12 +739,6 @@ lemma valid_arch_caps_lift:
     apply (wpsimp wp: cap archvspace asidtable pts)+
   done
 
-lemma valid_asid_map_lift_strong:
-  assumes "\<And>P. f \<lbrace>\<lambda>s. P (asid_table s)\<rbrace>"
-  assumes "\<And>P. f \<lbrace>\<lambda>s. P (asid_pools_of s)\<rbrace>"
-  shows "f \<lbrace>valid_asid_map\<rbrace>"
-  by (wpsimp simp: valid_asid_map_def wp: entry_for_asid_lift assms)
-
 context
   fixes f :: "'a::state_ext state \<Rightarrow> ('b \<times> 'a state) set \<times> bool"
   assumes arch: "\<And>P. f \<lbrace>\<lambda>s. P (arch_state s)\<rbrace>"

proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy

@@ -216,7 +216,7 @@ proof -
   ultimately
   show ?thesis
     unfolding valid_uses_2_def init_vspace_uses_def window_defs
-    by auto
+    by (auto simp: kernel_window_range_def)
 qed
 
 lemma valid_global_arch_objs_init_A_st[simp]:

proof/invariant-abstract/Invariants_AI.thy

@@ -3463,6 +3463,10 @@ lemma valid_mask_vm_rights[simp]:
   "mask_vm_rights V R \<in> valid_vm_rights"
   by (simp add: mask_vm_rights_def)
 
+lemma invs_pspace_in_kernel_window[elim!]:
+  "invs s \<Longrightarrow> pspace_in_kernel_window s"
+  by (simp add: invs_def valid_state_def)
+
 lemmas invs_implies =
   invs_equal_kernel_mappings
   invs_arch_state
@@ -3488,6 +3492,7 @@ lemmas invs_implies =
   invs_hyp_sym_refs
   invs_sym_refs
   tcb_at_invs
+  invs_pspace_in_kernel_window
 
 (* Pull invs out of a complex goal and prove it only once. Use as (strengthen invs_strengthen)+,
    best in combination with simp and potentially conj_cong. *)

proof/refine/AARCH64/ArchAcc_R.thy

@@ -91,10 +91,8 @@ lemma obj_relation_cuts_range_limit:
      apply (simp add: is_aligned_shift of_bl_shift_cte_level_bits)
     apply (rule_tac x=pte_bits in exI)
     apply (simp add: is_aligned_shift mask_def)
-    apply (rule conjI, simp add: bit_simps)
     apply (rule shiftl_less_t2n)
      apply (simp add: table_size_def)
-     apply (erule word_leq_minus_one_le[rotated], simp add: bit_simps)
     apply (simp add: bit_simps)
    apply (rule_tac x=pageBits in exI)
    apply (simp add: is_aligned_shift pbfs_atleast_pageBits)

proof/refine/AARCH64/Arch_R.thy

@@ -678,77 +678,11 @@ lemma maybeVSpaceForASID_corres:
      apply wpsimp+
   done
 
- (* FIXME AARCH64: move, use in valid_uses *)
-definition kernel_window_range :: "obj_ref set" where
-  "kernel_window_range \<equiv> {pptr_base..<AARCH64.pptrTop}"
-
-lemma kernel_window_bounded: (* FIXME AARCH64: move *)
-  "\<lbrakk> p \<in> kernel_window s; valid_uses s \<rbrakk> \<Longrightarrow> p \<in> kernel_window_range"
-  by (fastforce dest: valid_uses_kernel_window simp: kernel_window_range_def)
-
-lemma pspace_in_kw_bounded: (* FIXME AARCH64: move *)
-  "\<lbrakk> kheap s p = Some ko; pspace_in_kernel_window s; valid_uses s; pspace_aligned s \<rbrakk> \<Longrightarrow>
-   p \<in> kernel_window_range"
-  apply (erule pspace_alignedE, fastforce)
-  apply (simp add: pspace_in_kernel_window_def)
-  apply (erule allE, erule allE, erule (1) impE)
-  apply (prop_tac "p \<in> kernel_window s")
-   apply (erule set_mp)
-   apply (clarsimp simp: is_aligned_no_overflow)
-  apply (fastforce dest: kernel_window_bounded)
-  done
-
-lemma below_pptrTop_ipa_size: (* FIXME AARCH64: move *)
-  "p < AARCH64.pptrTop \<Longrightarrow> p \<le> mask ipa_size"
-  using pptrTop_le_ipa_size
-  by simp
-
-(* FIXME AARCH64: move? *)
-lemma pptrTop_ucast_ppn:
-  "\<lbrakk> p < AARCH64.pptrTop; is_aligned p pageBits \<rbrakk> \<Longrightarrow>
-   ucast (ucast (p >> pageBits)::ppn) = p >> pageBits"
-  apply (drule below_pptrTop_ipa_size)
-  apply word_eqI
-  using ppn_len_def'[unfolded ppn_len_def]
-  by (fastforce dest: bit_imp_le_length)
-
-(* FIXME AARCH64: move? *)
-lemma kernel_window_range_addrFromPPtr:
-  "p \<in> kernel_window_range  \<Longrightarrow> addrFromPPtr p < AARCH64.pptrTop"
-  apply (simp add: kernel_window_range_def addrFromPPtr_def pptrBaseOffset_def
-                   paddrBase_def pptr_base_def)
-  apply unat_arith
-  done
-
-(* FIXME AARCH64: move? *)
-lemma kernel_window_addrFromPPtr:
-  "\<lbrakk> p \<in> kernel_window_range; is_aligned p pageBits \<rbrakk> \<Longrightarrow>
-   ucast (ucast (addrFromPPtr p >> pageBits)::ppn) = addrFromPPtr p >> pageBits"
-  apply (rule pptrTop_ucast_ppn)
-   apply (erule kernel_window_range_addrFromPPtr)
-  apply (erule is_aligned_addrFromPPtr)
-  done
-
 (* FIXME AARCH64: move to ArchAcc_R *)
 lemma pageBits_leq_table_size[simp, intro!]:
   "pageBits \<le> table_size (pt_type pt)"
   by (simp add: bit_simps)
 
-(* FIXME AARCH64: move *)
-lemma invs_pspace_in_kernel_window[elim!]:
-  "invs s \<Longrightarrow> pspace_in_kernel_window s"
-  by (simp add: invs_def valid_state_def)
-
-(* FIXME AARCH64: move *)
-lemma pt_lookup_slot_pte_at:
-  "\<lbrakk> vspace_for_asid asid s = Some pt; pt_lookup_slot pt vref (ptes_of s) = Some (level, slot);
-     vref \<in> user_region; invs s\<rbrakk>
-   \<Longrightarrow> pte_at (level_type level) slot s"
-  apply (drule (1) pt_lookup_slot_vs_lookup_slotI)
-  apply clarsimp
-  apply (erule (3) vs_lookup_slot_pte_at)
-  done
-
 lemma decodeARMPageTableInvocation_corres:
   "\<lbrakk>cap = arch_cap.PageTableCap p pt_t opt; acap_relation cap cap';
     list_all2 cap_relation (map fst excaps) (map fst excaps');

proof/refine/AARCH64/Finalise_R.thy

@@ -2401,7 +2401,6 @@ lemma deleteASID_invs'[wp]:
   unfolding deleteASID_def
   by (wpsimp wp: getASID_wp hoare_drop_imps simp: getPoolPtr_def)
 
-(* FIXME AARCH64 move next to valid_objs_valid_tcb *)
 lemma valid_objs_valid_tcb':
   "\<lbrakk> valid_objs' s ; ko_at' (t :: tcb) p s \<rbrakk> \<Longrightarrow> valid_tcb' t s"
   by (fastforce simp add: obj_at'_def ran_def valid_obj'_def valid_objs'_def)
@@ -3835,16 +3834,6 @@ lemma return_NullCap_pair_corres[corres]:
           (return (cap.NullCap, cap.NullCap)) (return (NullCap, NullCap))"
   by (corres corres: corres_returnTT)
 
-(* FIXME AARCH64: move *)
-lemma vspace_for_asid_not_normal_pt:
-  "\<lbrakk>vspace_for_asid asid s = Some pt; normal_pt_at pt s; valid_vspace_objs s\<rbrakk> \<Longrightarrow> False"
-  apply (drule vspace_for_asid_vs_lookup)
-  apply (clarsimp simp: pt_at_eq)
-  apply (drule (1) valid_vspace_objsD, simp)
-   apply (fastforce simp: in_omonad)
-  apply clarsimp
-  done
-
 lemma arch_finaliseCap_corres:
   "\<lbrakk> final_matters' (ArchObjectCap cap') \<Longrightarrow> final = final'; acap_relation cap cap' \<rbrakk>
      \<Longrightarrow> corres (\<lambda>r r'. cap_relation (fst r) (fst r') \<and> cap_relation (snd r) (snd r'))

proof/refine/AARCH64/Schedule_R.thy

@@ -91,11 +91,6 @@ lemma set_vcpu_vmid_inv[wp]:
   unfolding vmid_inv_def
   by (wp_pre, wps, wpsimp, simp)
 
-(* FIXME AARCH64 move to ArchVSpace_AI to match ARM_HYP *)
-crunches do_machine_op
-  for valid_vs_lookup2[wp]: "\<lambda>s. P (valid_vs_lookup s)"
-  (ignore: get_object set_object)
-
 lemma vmid_inv_cur_vcpu[simp]:
   "vmid_inv (s\<lparr>arch_state := arch_state s\<lparr>arm_current_vcpu := x\<rparr>\<rparr>) = vmid_inv s"
   by (simp add: vmid_inv_def)

proof/refine/AARCH64/VSpace_R.thy

@@ -49,7 +49,8 @@ lemma asidBits_asid_bits[simp]:
   "asidBits = asid_bits"
   by (simp add: bit_simps' asid_bits_def asidBits_def)
 
-(* FIXME AARCH64: where is this added? it should have this name and not crunch_param_rules(8) *)
+(* FIXME AARCH64: Added to crunch_param_rules in Crunch_Instances_NonDet as
+   trans[OF liftE_bindE return_bind]; move to monad equations instead and give it the name below *)
 lemma liftE_return_bindE:
   "liftE (return x) >>=E f = f x"
   by (rule Crunch.crunch_param_rules(8))
@@ -1799,16 +1800,6 @@ lemma invalidateASIDEntry_corres[corres]:
   unfolding invalidate_asid_entry_def invalidateASIDEntry_def
   by (corres simp: vspace_for_asid_def)
 
-lemma invs_vmid_inv[elim!]: (* FIXME AARCH64: move *)
-  "invs s \<Longrightarrow> vmid_inv s"
-  by (auto simp: invs_def valid_state_def valid_arch_state_def)
-
-lemma invs_valid_vmid_table[elim!]: (* FIXME AARCH64: move *)
-  "invs s \<Longrightarrow> valid_vmid_table s"
-  by (auto simp: invs_def valid_state_def valid_arch_state_def)
-
-declare invs_valid_global_arch_objs[elim!] (* FIXME AARCH64: declare at origin *)
-
 lemma deleteASID_corres [corres]:
   assumes "asid' = ucast asid" "pm' = pm"
   shows "corres dc (invs and K (asid \<noteq> 0)) no_0_obj'