Minor refactoring.

theories/atomic_pcas.v

@@ -61,17 +61,27 @@ Section atomic_pair.
       repeat (split; first done). right. eauto.
   Qed.
 
+  Lemma pcas_synced_spec (l1 l2: loc) γ s:
+    is_atomic_syncer (ϕ (#l1, #l2)) γ s -∗
+    □ WP s pcas_seq
+         {{ f', □ ∀ xs, atomic_sync_wp γ (α xs) (β xs) f' ((#l1, #l2), xs) }}.
+  Proof.
+    iIntros "#Hsyncer !#".
+    iApply wp_wand=>//.
+    iIntros (f') "#HΦ !#".
+    iIntros (xs).
+    iApply "HΦ".
+    iApply pcas_seq_spec.
+  Qed.
+
   Lemma pcas_atomic_spec (mk_syncer : val) (l1 l2: loc) (x1 x2:val) :
     mk_syncer_spec mk_syncer →
     {{{ l1 ↦ x1 ∗ l2 ↦ x2 }}}
       mk_syncer #()
     {{{ (s : val) γ, RET s;
-        (WP (s pcas_seq)%V
-            {{ f', gHalf γ (x1, x2)%V ∗
-                   □ ∀ (x1' x2' : val),
-                     atomic_wp (fun g => gHalf γ g ∗ □ (α (x1', x2')) g)
-                               (fun g v => ∃ g', gHalf γ g' ∗ (β (x1', x2')) g g' v)
-                               ∅ ⊤ (f' ((#l1, #l2), (x1', x2'))%V) }}) }}}.
+        WP (s pcas_seq)%V
+           {{ f', gHalf γ (x1, x2)%V ∗
+                  □ ∀ xs, atomic_sync_wp γ (α xs) (β xs) f' ((#l1, #l2), xs) }} }}}.
   Proof.
     iIntros (Hmksyncer Φ) "[Hl1 Hl2] Hsynced".
     iApply (atomic_spec with "[Hl1 Hl2]"); first done.
@@ -82,12 +92,6 @@ Section atomic_pair.
       iIntros (γ s) "[Hg Hsync]".
       iApply ("Hsynced" $! s γ).
       iFrame.
-      iApply (wp_wand with "Hsync").
-      iIntros (f') "#HΦ".
-      iAlways.
-      iIntros (x1' x2').
-      iSpecialize ("HΦ" $! (α (x1', x2')) (β (x1', x2')) ((#l1, #l2), (x1', x2'))%V).
-      iApply "HΦ".
-      iApply pcas_seq_spec.
+      iApply (pcas_synced_spec with "Hsync").
   Qed.
 End atomic_pair.
\ No newline at end of file

theories/atomic_sync.v

@@ -24,12 +24,15 @@ Section atomic_sync.
   Definition atomic_seq_spec (ϕ: A → iProp Σ) α β (f x: val) :=
     (∀ g, {{ ϕ g ∗ α g }} f x {{ v, ∃ g', ϕ g' ∗ β g g' v }})%I.
 
+  Definition atomic_sync_wp γ α β (f' x: val) :=
+    atomic_wp (fun g => gHalf γ g ∗ □ α g)%I
+              (fun g v => ∃ g', gHalf γ g' ∗ β g g' v)%I
+              ∅ ⊤ (f' x)%I.
+
   (* TODO: Provide better masks. ∅ as inner mask is pretty weak. *)
   Definition atomic_synced (ϕ: A → iProp Σ) γ (f f': val) :=
     (□ ∀ α β (x: val), atomic_seq_spec ϕ α β f x -∗
-                       atomic_wp     (fun g => gHalf γ g ∗ □ α g)%I
-                                     (fun g v => ∃ g', gHalf γ g' ∗ β g g' v)%I
-                                     ∅ ⊤ (f' x))%I.
+                       atomic_sync_wp γ α β f' x)%I.
 
   (* TODO: Use our usual style with a generic post-condition. *)
   (* TODO: We could get rid of the x, and hard-code a unit. That would