diff --git a/lib/Monad_Lists.thy b/lib/Monad_Lists.thy index 7c8d1118a..876edf1e9 100644 --- a/lib/Monad_Lists.thy +++ b/lib/Monad_Lists.thy @@ -515,10 +515,7 @@ proof (induct xs) next case (Cons y ys) have PQ_inv: "\x. x \ set ys \ \P and Q y\ f x \\_. P and Q y\" - 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 "\x. x \ set xs \ \P\ f x \\_. P\" + assumes "\x. x \ set xs \ \P\ f x \\_. Q x\" + assumes "\x y. \ x \ set xs; y \ set xs \ \ \P and Q y\ f x \\_. Q y\" + shows "\P\ mapM f xs \\_ s. P s \ (\x \ set xs. Q x s)\" + 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: "\x. x \ S \ \P\ f x \\rv. P\" shows "set xs \ S \ \P\ mapM_x f xs \\rv. P\" diff --git a/lib/Monads/NonDetMonadVCG.thy b/lib/Monads/NonDetMonadVCG.thy index aac5ade4c..eb935d8fc 100644 --- a/lib/Monads/NonDetMonadVCG.thy +++ b/lib/Monads/NonDetMonadVCG.thy @@ -1338,7 +1338,11 @@ lemma hoare_weak_lift_imp: lemma hoare_vcg_weaken_imp: "\ \rv s. Q rv s \ Q' rv s ; \ P \ f \\rv s. Q' rv s \ R rv s\ \ \ \ P \ f \\rv s. Q rv s \ R rv s\" - by (clarsimp simp: valid_def split_def) + by (rule hoare_weaken_imp) + +lemma hoare_pre_cases: + "\ \\s. R s \ P s\ f \Q\; \\s. \R s \ P' s\ f \Q\ \ \ \P and P'\ f \Q\" + unfolding valid_def by fastforce lemma hoare_vcg_ex_lift: "\ \x. \P x\ f \Q x\ \ \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\" @@ -1393,8 +1397,7 @@ lemma hoare_vcg_R_conj: lemma valid_validE: "\P\ f \\rv. Q\ \ \P\ f \\rv. Q\,\\rv. Q\" - apply (simp add: validE_def) - done + by (rule hoare_post_imp_dc) lemma valid_validE2: "\ \P\ f \\_. Q'\; \s. Q' s \ Q s; \s. Q' s \ E s \ \ \P\ f \\_. Q\,\\_. E\" diff --git a/lib/Monads/OptionMonad.thy b/lib/Monads/OptionMonad.thy index 79543639b..305edefed 100644 --- a/lib/Monads/OptionMonad.thy +++ b/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 \ v)) p = P v" + by simp + + (* obind, etc. *) definition diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy index 88c18af68..961467039 100644 --- a/lib/Word_Lib/Word_Lemmas_Internal.thy +++ b/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: + "\ x && mask n = y && mask n; x >> n = y >> n \ \ 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 \ m' + n \ (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 \ a + len_of TYPE('a)" assumes align: "is_aligned p a" diff --git a/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy b/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy index 4ee6fa8bb..5e2bba97e 100644 --- a/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy +++ b/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 \ m' + n \ (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 *) diff --git a/proof/invariant-abstract/AARCH64/ArchArch_AI.thy b/proof/invariant-abstract/AARCH64/ArchArch_AI.thy index c773861b8..4ab675a40 100644 --- a/proof/invariant-abstract/AARCH64/ArchArch_AI.thy +++ b/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 \ v)) p = P v" - by simp - lemma associate_vcpu_tcb_valid_arch_state[wp]: "associate_vcpu_tcb vcpu tcb \valid_arch_state\" supply fun_upd_apply[simp del] diff --git a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy index 8970bf37f..18944676a 100644 --- a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy +++ b/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 "\x. x \ set xs \ \P\ f x \\_. P\" - assumes "\x. x \ set xs \ \P\ f x \\_. Q x\" - assumes "\x y. \ x \ set xs; y \ set xs \ \ \P and Q y\ f x \\_. Q y\" - shows "\P\ mapM f xs \\_ s. P s \ (\x \ set xs. Q x s)\" - 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: "\ is_aligned base asid_low_bits; offset \ mask asid_low_bits \ \ 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 \ x \ Some y" - by simp - lemma delete_asid_pool_not_target[wp]: "\asid_pool_at ptr and valid_vspace_objs and valid_asid_table and pspace_aligned\ 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: - "\ \\s. R s \ P s\ f \Q\; \\s. \R s \ P' s\ f \Q\ \ \ \P and P'\ f \Q\" - unfolding valid_def by fastforce - lemma delete_asid_no_vs_lookup_target_no_vspace: "\\s. vspace_for_asid asid s \ Some pt \ 0 < asid \ vref \ user_region \ vspace_pt_at pt s \ valid_vspace_objs s \ valid_asid_table s \ pspace_aligned s \ diff --git a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy index 383d2c55f..953b43601 100644 --- a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy +++ b/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: - "\ x && mask n = y && mask n; x >> n = y >> n \ \ 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: "\asid_low. vmid_for_asid_2 (asid_of asid_high asid_low) table pools = None \ 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) \ obj_at hyp_live p \" 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]: "\s. P (kheap s)" - crunches vcpu_save_reg, vcpu_write_reg for vcpu_hyp_live[wp]: "\s. P (vcpu_hyp_live_of s)" (simp_del: fun_upd_apply simp: opt_map_upd_triv) diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy index 9d2e946d2..5df2a6c96 100644 --- a/proof/invariant-abstract/KHeap_AI.thy +++ b/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]: "\s. P (interrupt_states s)" + and kheap[wp]: "\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) diff --git a/proof/invariant-abstract/LevityCatch_AI.thy b/proof/invariant-abstract/LevityCatch_AI.thy index afb310fef..fc826a649 100644 --- a/proof/invariant-abstract/LevityCatch_AI.thy +++ b/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 \ x \ Some y" + by simp + (* Weakest precondition lemmas that need ASpec concepts: *) lemma const_on_failure_wp: