lib+ainvs+aarch64 ainvs: cleanup + move lemmas into lib

- make kheap crunch for do_machine_op generic
- make None_Some_strg available generically in LevityCatch
- move word lemmas up into Word_Lib
- move wp lemmas up into lib + minor lib cleanup

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/Monad_Lists.thy

@@ -515,10 +515,7 @@ proof (induct xs)
 next
   case (Cons y ys)
   have PQ_inv: "\<And>x. x \<in> set ys \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. P and Q y\<rbrace>"
-    apply (simp add: pred_conj_def)
-    apply (rule hoare_pre)
-     apply (wp Cons|simp)+
-    done
+    by (wpsimp wp: Cons)
   show ?case
     apply (simp add: mapM_Cons)
     apply wp
@@ -531,6 +528,17 @@ next
     done
 qed
 
+lemma mapM_set_inv:
+  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>"
+  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>"
+  assumes "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>"
+  shows "\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. P s \<and> (\<forall>x \<in> set xs. Q x s)\<rbrace>"
+  apply (rule hoare_weaken_pre, rule hoare_vcg_conj_lift)
+    apply (rule mapM_wp', erule assms)
+   apply (rule mapM_set; rule assms; assumption)
+  apply simp
+  done
+
 lemma mapM_x_wp:
   assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
   shows      "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>rv. P\<rbrace>"

lib/Monads/NonDetMonadVCG.thy

@@ -1338,7 +1338,11 @@ lemma hoare_weak_lift_imp:
 lemma hoare_vcg_weaken_imp:
   "\<lbrakk> \<And>rv s. Q rv s \<Longrightarrow> Q' rv s ; \<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> R rv s\<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
-  by (clarsimp simp: valid_def split_def)
+  by (rule hoare_weaken_imp)
+
+lemma hoare_pre_cases:
+  "\<lbrakk> \<lbrace>\<lambda>s. R s \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. \<not>R s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q\<rbrace>"
+  unfolding valid_def by fastforce
 
 lemma hoare_vcg_ex_lift:
   "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>"
@@ -1393,8 +1397,7 @@ lemma hoare_vcg_R_conj:
 
 lemma valid_validE:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>,\<lbrace>\<lambda>rv. Q\<rbrace>"
-  apply (simp add: validE_def)
-  done
+  by (rule hoare_post_imp_dc)
 
 lemma valid_validE2:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s. Q' s \<Longrightarrow> Q s; \<And>s. Q' s \<Longrightarrow> E s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>\<lambda>_. E\<rbrace>"

lib/Monads/OptionMonad.thy

@@ -189,6 +189,12 @@ lemma opt_pred_unfold_proj:
   "(P |< (f ||> g))=  (P o g |< f)"
   by (clarsimp simp: opt_map_def split: option.splits)
 
+(* This rule is useful when fun_upd_apply is not in the simp set: *)
+lemma opt_pred_proj_upd_eq[simp]:
+  "(P |< proj (p \<mapsto> v)) p = P v"
+  by simp
+
+
 (* obind, etc. *)
 
 definition

lib/Word_Lib/Word_Lemmas_Internal.thy

@@ -658,6 +658,17 @@ lemmas shiftl_t2n' = shiftl_eq_mult[where x="w::'a::len word" for w]
 
 (* candidates for moving to AFP Word_Lib: *)
 
+lemma word_mask_shift_eqI:
+  "\<lbrakk> x && mask n = y && mask n; x >> n = y >> n \<rbrakk> \<Longrightarrow> x = y"
+  apply (subst mask_or_not_mask[of x n, symmetric])
+  apply (subst mask_or_not_mask[of y n, symmetric])
+  apply (rule arg_cong2[where f="(OR)"]; blast intro: shiftr_eq_neg_mask_eq)
+  done
+
+lemma mask_shiftr_mask_eq:
+  "m \<le> m' + n \<Longrightarrow> (w && mask m >> n) && mask m' = w && mask m >> n" for w :: "'a::len word"
+  by word_eqI_solve
+
 lemma mask_split_aligned:
   assumes len: "m \<le> a + len_of TYPE('a)"
   assumes align: "is_aligned p a"

proof/invariant-abstract/AARCH64/ArchAcc_AI.thy

@@ -2234,11 +2234,6 @@ lemma pt_index_table_index_slot_offset_eq:
   using table_base_index_eq pt_slot_offset_def
   by force
 
-(* FIXME AARCH64: move *)
-lemma mask_shiftr_mask_eq:
-  "m \<le> m' + n \<Longrightarrow> (w && mask m >> n) && mask m' = w && mask m >> n" for w :: "'a::len word"
-  by word_eqI_solve
-
 (* If you start with a lookup from asid down to level, and you split off a walk at level', then an
    update at level' does not affect the extended pt_walk from level'-1 down to level. *)
 (* FIXME: we should do the same on RISCV64 *)

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -1173,11 +1173,6 @@ lemma arch_thread_set_vcpus_of[wp]:
   apply (clarsimp simp: obj_at_def opt_map_def)
   done
 
-(* FIXME AARCH64: move *)
-lemma opt_pred_proj_upd_eq[simp]:
-  "(P |< proj (p \<mapsto> v)) p = P v"
-  by simp
-
 lemma associate_vcpu_tcb_valid_arch_state[wp]:
   "associate_vcpu_tcb vcpu tcb \<lbrace>valid_arch_state\<rbrace>"
   supply fun_upd_apply[simp del]

proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy

@@ -60,18 +60,6 @@ lemma invs_arm_asid_table_unmap:
                    valid_asid_pool_caps_def equal_kernel_mappings_asid_table_unmap)
   done
 
-(* FIXME AARCH64: move next to mapM_set *)
-lemma mapM_set_inv:
-  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>"
-  assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. Q x\<rbrace>"
-  assumes "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>P and Q y\<rbrace> f x \<lbrace>\<lambda>_. Q y\<rbrace>"
-  shows "\<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>_ s. P s \<and> (\<forall>x \<in> set xs. Q x s)\<rbrace>"
-  apply (rule hoare_weaken_pre, rule hoare_vcg_conj_lift)
-    apply (rule mapM_wp', erule assms)
-   apply (rule mapM_set; rule assms; assumption)
-  apply simp
-  done
-
 lemma asid_low_bits_of_add:
   "\<lbrakk> is_aligned base asid_low_bits; offset \<le> mask asid_low_bits \<rbrakk> \<Longrightarrow>
    asid_low_bits_of (base + offset) = ucast offset"
@@ -1229,11 +1217,6 @@ lemma vs_lookup_target_clear_asid_strg:
   by (clarsimp simp: vs_lookup_target_def vs_lookup_slot_def vs_lookup_table_def pool_for_asid_def
                      obind_def)
 
-(* FIXME AARCH64: move *)
-lemma None_Some_strg:
-  "x = None \<Longrightarrow> x \<noteq> Some y"
-  by simp
-
 lemma delete_asid_pool_not_target[wp]:
   "\<lbrace>asid_pool_at ptr and valid_vspace_objs and valid_asid_table and pspace_aligned\<rbrace>
    delete_asid_pool asid ptr
@@ -1306,11 +1289,6 @@ lemma delete_asid_no_vs_lookup_target_vspace:
                   split: if_split_asm)
   done
 
-(* FIXME AARCH64: move *)
-lemma hoare_pre_cases:
-  "\<lbrakk> \<lbrace>\<lambda>s. R s \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. \<not>R s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q\<rbrace>"
-  unfolding valid_def by fastforce
-
 lemma delete_asid_no_vs_lookup_target_no_vspace:
   "\<lbrace>\<lambda>s. vspace_for_asid asid s \<noteq> Some pt \<and> 0 < asid \<and> vref \<in> user_region \<and> vspace_pt_at pt s \<and>
         valid_vspace_objs s \<and> valid_asid_table s \<and> pspace_aligned s \<rbrace>

proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy

@@ -142,14 +142,6 @@ lemma vs_lookup_target_clear_asid_table:
   apply blast
   done
 
-(* FIXME AARCH64: move to Word_Lib *)
-lemma word_mask_shift_eqI:
-  "\<lbrakk> x && mask n = y && mask n; x >> n = y >> n \<rbrakk> \<Longrightarrow> x = y"
-  apply (subst mask_or_not_mask[of x n, symmetric])
-  apply (subst mask_or_not_mask[of y n, symmetric])
-  apply (rule arg_cong2[where f="(OR)"]; blast intro: shiftr_eq_neg_mask_eq)
-  done
-
 lemma vmid_for_asid_unmap_pool:
   "\<forall>asid_low. vmid_for_asid_2 (asid_of asid_high asid_low) table pools = None \<Longrightarrow>
    vmid_for_asid_2 asid (table(asid_high := None)) pools = vmid_for_asid_2 asid table pools"
@@ -333,9 +325,6 @@ lemma vcpu_update_vtimer_hyp_live[wp]:
   "vcpu_update vcpu_ptr (vcpu_vtimer_update f) \<lbrace> obj_at hyp_live p \<rbrace>"
   by (wpsimp wp: vcpu_update_obj_at simp: obj_at_def in_omonad)
 
-crunches do_machine_op (* FIXME AARCH64: move to KHeap crunches *)
-  for kheap[wp]: "\<lambda>s. P (kheap s)"
-
 crunches vcpu_save_reg, vcpu_write_reg
   for vcpu_hyp_live[wp]: "\<lambda>s. P (vcpu_hyp_live_of s)"
   (simp_del: fun_upd_apply simp: opt_map_upd_triv)

proof/invariant-abstract/KHeap_AI.thy

@@ -997,6 +997,7 @@ crunches do_machine_op
   and valid_global_refs[wp]: valid_global_refs
   and valid_irq_node[wp]: valid_irq_node
   and irq_states[wp]: "\<lambda>s. P (interrupt_states s)"
+  and kheap[wp]: "\<lambda>s. P (kheap s)"
   (simp: cur_tcb_def zombies_final_pspaceI state_refs_of_pspaceI ex_nonz_cap_to_def ct_in_state_def
    wp: crunch_wps valid_arch_state_lift vs_lookup_vspace_obj_at_lift)
 

proof/invariant-abstract/LevityCatch_AI.thy

@@ -50,6 +50,10 @@ declare select_singleton[simp]
 
 crunch_ignore (add: do_extended_op)
 
+lemma None_Some_strg:
+  "x = None \<Longrightarrow> x \<noteq> Some y"
+  by simp
+
 (* Weakest precondition lemmas that need ASpec concepts: *)
 
 lemma const_on_failure_wp: