Introduce Logically-atomic WP with rec. atomic shift.

theories/atomic.v

@@ -8,16 +8,45 @@ Import uPred.
 Section atomic.
   Context `{irisG Λ Σ} {A: Type}.
 
+Notation atomic_shift'_type Σ := 
+  (coPset -c> coPset -c> (A → iProp Σ) -c> (A → val Λ → iProp Σ) -c> (val _ → iProp Σ) -c> iProp Σ).
+Definition atomic_shift'_pre (F : atomic_shift'_type Σ) :
+  atomic_shift'_type Σ :=
+  λ Eo Ei α β Φ, (|={Eo,Ei}=> ∃ x : A,
+        α x ∗ ((α x ={Ei,Eo}=∗ ▷ F Eo Ei α β Φ) ∧ ∀ y, β x y ={Ei,Eo}=∗ Φ y))%I.
+
+Instance atomic_shift'_pre_contractive:
+  Contractive (@atomic_shift'_pre).
+Proof.
+  repeat intros ?.
+  rewrite /atomic_shift'_pre.
+  repeat apply (_ : Proper (dist n ==> dist n) _).
+  apply: uPred.exist_ne => ?.
+  repeat apply (_ : Proper (dist n ==> dist n) _).
+  repeat apply (_ : Proper (dist n ==> dist n ==> dist n) _) => //.
+  repeat apply (_ : Proper (_ ==> dist n) _).
+  case: n H => [//|? /(_ _ _ _ _ _) //=].
+Qed.
+
+Definition atomic_shift := fixpoint (@atomic_shift'_pre).
+(* Definition atomic_shift'_aux := {| unseal := (@atomic_shift'_def); seal_eq := eq_refl |}. *)
+(* Definition atomic_shift' := unseal (@atomic_shift'_aux). *)
+
+Lemma atomic_shift_unfold Eo Ei α β Φ :
+  @atomic_shift Eo Ei α β Φ ≡
+  (|={Eo,Ei}=> ∃ x : A,
+     α x ∗ ((α x ={Ei,Eo}=∗ ▷ atomic_shift Eo Ei α β Φ) ∧ ∀ y, β x y ={Ei,Eo}=∗ Φ y))%I.
+Proof.
+  by rewrite {1}/atomic_shift (fixpoint_unfold atomic_shift'_pre _ _ _ _ _).
+Qed.
+
   (* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
-  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
-  Definition atomic_triple
+  (* logically atomic wp: <x, α> e @ E_i, E_o <v, β x v> *)
+  Definition atomic_wp
              (α: A → iProp Σ) (* atomic pre-condition *)
              (β: A → val _ → iProp Σ) (* atomic post-condition *)
              (Ei Eo: coPset) (* inside/outside masks *)
              (e: expr _) : iProp Σ :=
-    (∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
-                       α x ∗
-                       ((α x ={Ei, Eo}=∗ P) ∧
-                        (∀ v, β x v ={Ei, Eo}=∗ Q v))
-     ) -∗ {{ P }} e @ ⊤ {{ Q }})%I.
+    (∀ Φ, atomic_shift Eo Ei α β Φ
+                       -∗ WP e @ Eo {{ Φ }})%I.
 End atomic.