Commit fd912b5c authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/atomic' into 'master'

add a strong form of atomicity, for weak forms of weakest-pre

Closes #107

See merge request FP/iris-coq!77
parents 180cd032 418ca5de
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment