diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v index 88c82f8eb78b43b8d7b951ff497cf450c0b69722..51318c3fde85092e66630ff179ac6ce340ef7e6f 100644 --- a/theories/program_logic/language.v +++ b/theories/program_logic/language.v @@ -52,9 +52,22 @@ Section language. Definition irreducible (e : expr Λ) (σ : state Λ) := ∀ e' σ' efs, ¬prim_step e σ e' σ' efs. + (* This (weak) form of atomicity is enough to open invariants when WP ensures + safety, i.e., programs never can get stuck. We have an example in + lambdaRust of an expression that is atomic in this sense, but not in the + stronger sense defined below, and we have to be able to open invariants + around that expression. See `CasStuckS` in + [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). *) Definition atomic (e : expr Λ) : Prop := ∀ σ e' σ' efs, prim_step e σ e' σ' efs → irreducible e' σ'. + (* To open invariants with a WP that does not ensure safety, we need a + stronger form of atomicity. With the above definition, in case `e` reduces + to a stuck non-value, there is no proof that the invariants have been + established again. *) + Definition strongly_atomic (e : expr Λ) : Prop := + ∀ σ e' σ' efs, prim_step e σ e' σ' efs → is_Some (to_val e'). + Inductive step (ρ1 ρ2 : cfg Λ) : Prop := | step_atomic e1 σ1 e2 σ2 efs t1 t2 : ρ1 = (t1 ++ e1 :: t2, σ1) → @@ -74,6 +87,10 @@ Section language. Global Instance of_val_inj : Inj (=) (=) (@of_val Λ). Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. + Lemma strongly_atomic_atomic e : + strongly_atomic e → atomic e. + Proof. unfold strongly_atomic, atomic. eauto using val_irreducible. Qed. + Lemma reducible_fill `{LanguageCtx Λ K} e σ : to_val e = None → reducible (K e) σ → reducible e σ. Proof.