diff --git a/IRIS_VERSION b/IRIS_VERSION
index 608d8663746e0bc0c8336688093ba01d47e2a46a..e9dc549d2ae7ac29151d13f817d9f9b5b211d6c9 100644
--- a/IRIS_VERSION
+++ b/IRIS_VERSION
@@ -1 +1 @@
-05a588df59ddfdc2e7a4aec5a98a50614c819693
+6cb76aaaf15d46c74c2a779f1e4e1ca1a53c0838
diff --git a/atomic.v b/atomic.v
index e765fa87c44b8802ef9aed0287aae95ecf1da087..be3168a8b4d0952d4d4b3a0c369fc4dfe912bb99 100644
--- a/atomic.v
+++ b/atomic.v
@@ -6,24 +6,18 @@ From iris.prelude Require Export coPset.
 Import uPred.
 
 Section atomic.
-  Context `{irisG Λ Σ} (A: Type).
+  Context `{irisG Λ Σ} {A: Type}.
 
   (* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
-  (* TODO RJ: Don't define atomic_triple_base; everybody should only ever use atomic_triple anyway. *)
-  (* TODO RJ: We probably will want to make `A` an implicit parameter. *)
-  Definition atomic_triple_base
+  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
+  Definition atomic_triple
              (α: A → iProp Σ) (* atomic pre-condition *)
              (β: A → val _ → iProp Σ) (* atomic post-condition *)
              (Ei Eo: coPset) (* inside/outside masks *)
-             (e: expr _) P Q : iProp Σ :=
-    ((P ={Eo, Ei}=> ∃ x:A,
+             (e: expr _) : iProp Σ :=
+    (∀ P Q, (P ={Eo, Ei}=> ∃ x:A,
                        α x ★
                        ((α x ={Ei, Eo}=★ P) ∧
-                        (∀ v, β x v ={Ei, Eo}=★ Q x v))
-     ) -★ {{ P }} e @ ⊤ {{ v, (∃ x: A, Q x v) }})%I.
-
-  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
-  Definition atomic_triple α β Ei Eo e := (∀ P Q, atomic_triple_base α β Ei Eo e P Q)%I.
-
-  Arguments atomic_triple {_} _ _ _ _.
+                        (∀ v, β x v ={Ei, Eo}=★ Q v))
+     ) -★ {{ P }} e @ ⊤ {{ Q }})%I.
 End atomic.
diff --git a/atomic_incr.v b/atomic_incr.v
index 03e6825737f2b41658a79bf883a1ec369a122ca3..6e5dbba04034890dba2a460344dc34dc0f27f4e4 100644
--- a/atomic_incr.v
+++ b/atomic_incr.v
@@ -19,11 +19,11 @@ Section incr.
 
   (* TODO: Can we have a more WP-style definition and avoid the equality? *)
   Definition incr_triple (l: loc) :=
-    atomic_triple _ (fun (v: Z) => l ↦ #v)%I
-                    (fun v ret => ret = #v ★ l ↦ #(v + 1))%I
-                    (nclose heapN)
-                    ⊤
-                    (incr #l).
+    atomic_triple (fun (v: Z) => l ↦ #v)%I
+                  (fun v ret => ret = #v ★ l ↦ #(v + 1))%I
+                  (nclose heapN)
+                  ⊤
+                  (incr #l).
 
   Lemma incr_atomic_spec: ∀ (l: loc), heapN ⊥ N → heap_ctx ⊢ incr_triple l.
   Proof.
@@ -46,7 +46,7 @@ Section incr.
       iSpecialize ("Hvs'" $! #x').
       wp_cas_suc.
       iMod ("Hvs'" with "[Hl]") as "HQ"; first by iFrame.
-      iModIntro. wp_if. iModIntro. by iExists x'.
+      iModIntro. wp_if. done.
     - iDestruct "Hvs'" as "[Hvs' _]".
       wp_cas_fail.
       iMod ("Hvs'" with "[Hl]") as "HP"; first by iFrame.
@@ -80,7 +80,7 @@ Section user.
     (* prove worker triple *)
     iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
     rewrite /incr_triple /atomic_triple.
-    iSpecialize ("Hincr"  $! True%I (fun _ _ => True%I) with "[]").
+    iSpecialize ("Hincr"  $! True%I (fun _ => True%I) with "[]").
     - iIntros "!# _".
       (* open the invariant *)
       iInv N as (x') ">Hl'" "Hclose".
diff --git a/atomic_pcas.v b/atomic_pcas.v
index 316a0dafcbdffbeaac08738e8b25e8e8767407ce..4b6b397ec66695b6acd750a9abcf1275b99df933 100644
--- a/atomic_pcas.v
+++ b/atomic_pcas.v
@@ -33,13 +33,14 @@ Section atomic_pair.
 
   Local Opaque β.
   
-  Lemma pcas_seq_spec: seq_spec N pcas_seq ϕ α β ⊤.
+  (* TODO: This needs updating for the new atomic_syncer.
+  Lemma pcas_seq_spec x: atomic_seq_spec ϕ α β ⊤ pcas_seq x.
   Proof.
-    iIntros (_ l) "!# _". wp_seq. iModIntro. iPureIntro.
+    iIntros (_ l) "!# _". wp_seq. iPureIntro.
     iIntros (x Φ g HN) "(#Hh & Hg & #Hα & HΦ)".
     iDestruct "Hg" as (l1 l2 x1 x2) "(% & % & Hl1 & Hl2)".
     iDestruct "Hα" as (a b) "%".
-    subst. simpl. wp_let. wp_proj. wp_load. wp_proj.
+    subst. simpl. iApply wp_fupd. wp_let. wp_proj. wp_load. wp_proj.
     wp_op=>[?|Hx1na].
     - subst.
       wp_if. wp_proj. wp_load. wp_proj.
@@ -75,6 +76,6 @@ Section atomic_pair.
     iDestruct (atomic_spec with "[Hl1 Hl2]") as "Hspec"=>//.
     - apply pcas_seq_spec.
     - iFrame "Hh". iExists l1, l2, x1, x2. iFrame. eauto.
-  Qed.
+  Qed.*)
 End atomic_pair.
 
diff --git a/atomic_sync.v b/atomic_sync.v
index 3e68efb3440ef4bb699325a073f57e7c3a5c4717..02c6b22b0b35f9495b205cd6e6d8079ca36604ff 100644
--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -15,63 +15,52 @@ Proof. by intros ?%subG_inG. Qed.
 Section atomic_sync.
   Context `{EqDecision A, !heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR A))} (N : namespace).
 
+  (* TODO: Rename and make opaque; the fact that this is a half should not be visible
+           to the user. *)
   Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, DecAgree g).
 
-  Definition atomic_triple'
-             (α: val → A → iProp Σ)
-             (β: val → A → A → val → iProp Σ)
-             (Ei Eo: coPset)
-             (f x: val) γ : iProp Σ :=
-    (∀ P Q, atomic_triple_base A (fun g => gHalf γ g ★ □ α x g)
-                                 (fun g v => ∃ g':A, gHalf γ g' ★ β x g g' v)
-                                 Ei Eo
-                                (f x) (P x) (fun _ => Q x))%I.
+  Definition atomic_seq_spec (ϕ: A → iProp Σ) α β (f x: val) :=
+    (∀ g, {{ ϕ g ★ α g }} f x {{ v, ∃ g', ϕ g' ★ β g g' v }})%I.
 
-  Definition sync (mk_syncer: val) : val :=
-    λ: "f_seq" "l",
-       let: "s" := mk_syncer #() in
-       "s" ("f_seq" "l").
+  (* 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_triple (fun g => gHalf γ g ★ □ α g)%I
+                                     (fun g v => ∃ g', gHalf γ g' ★ β g g' v)%I
+                                     ∅ ⊤ (f' x))%I.
 
-  Definition seq_spec (f: val) (ϕ: val → A → iProp Σ) α β (E: coPset) :=
-      ∀ (Φ: val → iProp Σ) (l: val),
-         {{ True }} f l {{ f', ■ (∀ (x: val) (Φ: val → iProp Σ) (g: A),
-                               heapN ⊥ N →
-                               heap_ctx ★ ϕ l g ★ □ α x g ★
-                               (∀ (v: val) (g': A),
-                                  ϕ l g' -★ β x g g' v ={E}=★ Φ v)
-                               ⊢ WP f' x @ E {{ Φ }} )}}.
-  (* The linear view shift in the above post-condition is for the final step
-     of computation. The client side of such triple will have to prove that the
-     specific post-condition he wants can be lvs'd from whatever threaded together
-     by magic wands. The library side, when proving seq_spec, will always have
-     a view shift at the end of evalutation, which is exactly what we need.  *)
+  (* 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
+     be no loss in expressiveness, but probably more annoying to apply.
+     How much more annoying? And how much to we gain in terms of things
+     becomign easier to prove? *)
+  (* This is really the core of the spec: It says that executing `s` on `f`
+     turns the sequential spec with f, α, β into the concurrent triple with f', α, β. *)
+  Definition is_atomic_syncer (ϕ: A → iProp Σ) γ (s: val) := 
+    (□ ∀ (f: val), WP s f {{ f', atomic_synced ϕ γ f f' }})%I.
 
-  Lemma atomic_spec (mk_syncer f_seq l: val) (ϕ: val → A → iProp Σ) α β Ei:
-      ∀ (g0: A),
-        heapN ⊥ N → seq_spec f_seq ϕ α β ⊤ →
-        mk_syncer_spec N mk_syncer →
-        heap_ctx ★ ϕ l g0
-        ⊢ WP (sync mk_syncer) f_seq l {{ f, ∃ γ, gHalf γ g0 ★ ∀ x, □ atomic_triple' α β Ei ⊤ f x γ  }}.
+  Definition atomic_syncer_spec (mk_syncer: val) :=
+    ∀ (g0: A) (ϕ: A → iProp Σ),
+      heapN ⊥ N →
+      {{{ heap_ctx ★ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 ★ is_atomic_syncer ϕ γ s }}}.
+
+  Lemma atomic_spec (mk_syncer: val):
+      mk_syncer_spec N mk_syncer → atomic_syncer_spec mk_syncer.
   Proof.
-    iIntros (g0 HN Hseq Hsync) "[#Hh HÏ•]".
+    iIntros (Hsync g0 Ï• HN ret) "[#Hh HÏ•] Hret".
     iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
     { by rewrite pair_op dec_agree_idemp. }
-    repeat wp_let. wp_bind (mk_syncer _).
-    iApply (Hsync (∃ g: A, ϕ l g ★ gHalf γ g)%I)=>//. iFrame "Hh".
-    iSplitL "Hg1 HÏ•".
+    iApply (Hsync (∃ g: A, ϕ g ★ gHalf γ g)%I with "[$Hh Hg1 Hϕ]")=>//.
     { iExists g0. by iFrame. }
-    iIntros (s) "#Hsyncer".
-    wp_let. wp_bind (f_seq _). iApply wp_wand_r.
-    iSplitR; first iApply Hseq=>//; auto.
-    iIntros (f) "%".
-    iApply wp_wand_r.
-    iSplitR; first iApply "Hsyncer".
-    iIntros (f') "#Hsynced".
-    iExists γ. iFrame.
-    iIntros (x). iAlways.
-    iIntros (P Q) "#Hvss".
+    iNext. iIntros (s) "#Hsyncer". iApply "Hret".
+    iSplitL "Hg2"; first done. iIntros "!#".
+    iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
+    iIntros (f') "#Hsynced {Hsyncer}".
+    iAlways. iIntros (α β x) "#Hseq".
+    iIntros (P Q) "#Hvss !# HP".
+    (* TODO: Why can't I iApply "Hsynced"? *)
     iSpecialize ("Hsynced" $! P Q x).
-    iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
+    iApply wp_wand_r. iSplitL "HP".
     - iApply ("Hsynced" with "[]")=>//.
       iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[HÏ• Hg1]".
       (* we should view shift at this point *)
@@ -79,10 +68,11 @@ Section atomic_sync.
       iMod "Hvss'". iDestruct "Hvss'" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
       iDestruct (m_frag_agree with "[Hg1 Hg2]") as %Heq; first iFrame. subst.
       iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
-      iModIntro. iApply H=>//.
-      iFrame "Hh Hϕ". iSplitR; first done. iIntros (ret g') "Hϕ' Hβ".
+      iModIntro. iApply wp_fupd. iApply wp_wand_r. iSplitL "HÏ•".
+      { iApply "Hseq". iFrame. done. }
+      iIntros (v) "H". iDestruct "H" as (g') "[Hϕ' Hβ]".
       iMod ("Hvss" with "HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
-      iSpecialize ("Hvs2" $! ret).
+      iSpecialize ("Hvs2" $! v).
       iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
       rewrite Qp_div_2.
       iAssert (|==> own γ (((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g')))%I
@@ -93,7 +83,7 @@ Section atomic_sync.
       { iExists g'. iFrame. }
       iModIntro. iSplitL "Hg2 HÏ•'"; last done.
       iExists g'. by iFrame.
-    - iIntros (?) "?". by iExists g0.
+    - iIntros (?) "?". done.
   Qed.
 
 End atomic_sync.
diff --git a/flat.v b/flat.v
index 6f3d1d7ec01b3ab344ce327e395df47d2a00d936..c7d587777b944aefc417fa5f6f3e222e988958a5 100644
--- a/flat.v
+++ b/flat.v
@@ -130,9 +130,9 @@ Section proof.
       by iApply "HΦ".
   Qed.
 
-  Definition installed_recp (ts: toks) (x: val) (Q: val → val → iProp Σ) :=
+  Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) :=
     let '(γx, _, γ3, _, γq) := ts in
-    (own γ3 (Excl ()) ★ own γx ((1/2)%Qp, DecAgree x) ★ saved_prop_own γq (Q x))%I.
+    (own γ3 (Excl ()) ★ own γx ((1/2)%Qp, DecAgree x) ★ saved_prop_own γq Q)%I.
 
   Lemma install_spec
         R P Q
@@ -140,7 +140,7 @@ Section proof.
         (Φ: val → iProp Σ):
     heapN ⊥ N →
     heap_ctx ★ inv N (srv_stack_inv R γs γm γr s ★ srv_tokm_inv γm) ★
-    P x ★ ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) ★
+    P ★ ({{ R ★ P }} f x {{ v, R ★ Q v }}) ★
     (∀ (p: loc) (ts: toks), installed_recp ts x Q -★ evm γm p ts -★(∃ hd, evs γs hd #p) -★ Φ #p)
     ⊢ WP install f x #s {{ Φ }}.
   Proof.
@@ -151,7 +151,7 @@ Section proof.
     iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
     iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
     iMod (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
-    iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) (Q x)%I) as (γq) "#?".
+    iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) Q) as (γq) "#?".
     iInv N as "[Hrs >Hm]" "Hclose".
     iDestruct "Hm" as (m) "[Hm HRm]".
     destruct (m !! p) eqn:Heqn.
@@ -170,8 +170,10 @@ Section proof.
         iApply install_push_spec=>//.
         iFrame "#". rewrite /evm /installed_s. iFrame.
         iSplitL "Hpx Hf".
-        { iExists P, Q. by iFrame. }
-        iIntros "Hhd". wp_seq. iModIntro.
+        { (* TODO: Something somewhere can be simplified so that we don't have
+             to add these dummy arguments any more. *)
+          iExists (fun _ => P), (fun _ => Q). by iFrame. }
+        iIntros "Hhd". wp_seq. 
         iSpecialize ("HΦ" $! p (γx, γ1, γ3, γ4, γq) with "[-Hhd]")=>//.
         { rewrite /installed_recp. iFrame. iFrame "#". }
         by iApply ("HΦ" with "[]").
@@ -206,7 +208,7 @@ Section proof.
           iFrame "Hom". iDestruct (big_sepM_delete _ m with "[-]") as "?"=>//.
           iFrame. iExists #p''. iSplitR; first done. iExists ts, p''.
           iSplitR; first done. iFrame "#". iLeft. iExists y. iFrame. }
-        iModIntro. wp_match. iModIntro. iApply ("HΦ'" with "[Hor HR]"). iFrame.
+        iModIntro. wp_match. iApply ("HΦ'" with "[Hor HR]"). iFrame.
       + iDestruct "Hp" as (f' x') "(Hp & Hs)".
         wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
         iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
@@ -227,7 +229,7 @@ Section proof.
         wp_bind (f' _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
         { iApply "Hf'". iFrame. }
         iIntros (v) "[HR HQ]".
-        wp_value. iModIntro. iInv N as "[Hs >Hm]" "Hclose".
+        wp_value. iInv N as "[Hs >Hm]" "Hclose".
         iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]".
         iDestruct "HRs" as (m') "[>Hom HRs]".
         iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame.
@@ -304,8 +306,8 @@ Section proof.
   Proof.
     iIntros (?) "(#? & #? & #? & HΦ)".
     wp_seq. wp_let.
-    wp_bind (try_acquire _). iApply try_acquire_spec.
-    iFrame "#". iNext. iIntros ([]); last by (iIntros; wp_if).
+    wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
+    iNext. iIntros ([]); last by (iIntros; wp_if).
     (* acquired the lock *)
     iIntros "[Hlocked [Ho2 HR]]".
     wp_if. wp_bind (! _)%E.
@@ -320,8 +322,8 @@ Section proof.
     { iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) ★ R ★ v = #()))%I=>//.      
       iFrame "#". iFrame. iIntros "? ?". by iFrame. }
     iIntros (f') "[Ho [HR %]]". subst.
-    wp_let. iApply release_spec. iFrame "#".
-    iFrame. iNext. iIntros. done.
+    wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#★".
+    iNext. iIntros. done.
   Qed.
 
   Lemma loop_spec R (p s: loc) (lk: val)
@@ -390,20 +392,20 @@ Section proof.
 
   Lemma mk_flat_spec: mk_syncer_spec N mk_flat.
   Proof.
-    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
+    iIntros (R HN Φ) "(#Hh & HR) HΦ".
     iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
     iMod (own_alloc (● (∅: tokmR) ⋅ ◯ ∅)) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
     iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
     { iExists ∅. iFrame. by rewrite big_sepM_empty. }
     wp_seq. wp_bind (newlock _).
-    iApply (newlock_spec _ (own γr (Excl ()) ★ R))%I=>//.
-    iFrame "Hh Ho2 HR". iNext. iIntros (lk γlk) "#Hlk".
+    iApply (newlock_spec _ (own γr (Excl ()) ★ R)%I with "[$Hh $Ho2 $HR]")=>//.
+    iNext. iIntros (lk γlk) "#Hlk".
     wp_let. wp_bind (new_stack _).
     iApply (new_stack_spec' _ (p_inv _ γm γr))=>//.
     iFrame "Hh Hm". iIntros (γ s) "#Hss".
-    wp_let. iModIntro. iApply "HΦ". rewrite /synced.
+    wp_let. iApply "HΦ". rewrite /synced.
     iAlways.
-    iIntros (f). wp_let. iModIntro. iAlways.
+    iIntros (f). wp_let. iAlways.
     iIntros (P Q x) "#Hf".
     iIntros "!# Hp". wp_let.
     wp_bind (install _ _ _).
diff --git a/peritem.v b/peritem.v
index ae09eb76f96ff83a74653e48d95e3748c79e1d42..ce12b4741d39325b14b116e7a21cf689b32bbf3a 100644
--- a/peritem.v
+++ b/peritem.v
@@ -92,7 +92,7 @@ Lemma new_stack_spec' Φ RI:
     heap_ctx ★ RI ★ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ★ RI) -★ Φ #s)
     ⊢ WP new_stack #() {{ Φ }}.
   Proof.
-    iIntros (HN) "(#Hh & HR & HΦ)".
+    iIntros (HN) "(#Hh & HR & HΦ)". iApply wp_fupd.
     iMod (own_alloc (● (∅: evmapR loc val unitR) ⋅ ◯ ∅)) as (γ) "[Hm Hm']".
     { apply auth_valid_discrete_2. done. }
     wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
@@ -115,10 +115,10 @@ Lemma new_stack_spec' Φ RI:
     induction xs as [|x xs' IHxs'].
     - simpl. iIntros (hd f f' HN ? ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
       iDestruct "Hxs1" as (q) "Hhd".
-      wp_rec. wp_value. iModIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
+      wp_rec. wp_value. wp_let. wp_load. wp_match. by iApply "HΦ".
     - simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
       iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
-      wp_rec. wp_value. iModIntro. wp_let. wp_load. wp_match. wp_proj.
+      wp_rec. wp_value. wp_let. wp_load. wp_match. wp_proj.
       wp_bind (f' _). iApply Hf=>//. iFrame "#".
       iSplitL "Hev"; first eauto. iFrame. iIntros "HRf".
       wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.
@@ -133,7 +133,7 @@ Lemma new_stack_spec' Φ RI:
   Proof.
     iIntros (HN) "(#Hh & HRx & #? & HΦ)".
     iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//.
-    iSpecialize ("Hpush" $! (R x) (fun _ ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]").
+    iSpecialize ("Hpush" $! (R x) (fun ret => (∃ hd, evs γ hd x) ★ ret = #())%I with "[]").
     - iIntros "!# Rx".
       (* open the invariant *)
       iInv N as "[IH1 ?]" "Hclose".
@@ -180,7 +180,7 @@ Lemma new_stack_spec' Φ RI:
         iModIntro. iSplitL; last auto. by iExists hd'.
     - iApply wp_wand_r. iSplitL "HRx Hpush".
       + by iApply "Hpush".
-      + iIntros (?) "H". iDestruct "H" as (_) "[? %]". subst.
+      + iIntros (?) "[? %]". subst.
         by iApply "HΦ".
   Qed.
 
diff --git a/simple_sync.v b/simple_sync.v
index a8b8a073bbe4ef2bfb10a64705897f8e54d46d30..0f02078edb340c0fc079d1d628b356fed578ec65 100644
--- a/simple_sync.v
+++ b/simple_sync.v
@@ -23,20 +23,19 @@ Section syncer.
   
   Lemma mk_sync_spec: mk_syncer_spec N mk_sync.
   Proof.
-    iIntros (R Φ HN) "(#Hh & HR & HΦ)".
+    iIntros (R HN Φ) "(#Hh & HR) HΦ".
     wp_seq. wp_bind (newlock _).
-    iApply newlock_spec; first done.
-    iSplitL "HR"; first by iFrame. iNext.
+    iApply (newlock_spec _ R with "[$Hh $HR]"); first done. iNext.
     iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
-    iIntros (f). wp_let. iModIntro. iAlways.
+    iIntros (f). wp_let. iAlways.
     iIntros (P Q x) "#Hf !# HP".
     wp_let. wp_bind (acquire _).
-    iApply acquire_spec. iSplit; first done. iNext.
+    iApply (acquire_spec with "Hl"). iNext.
     iIntros "[Hlocked R]". wp_seq. wp_bind (f _).
-    iDestruct ("Hf" with "[R HP]") as "Hf'"; first by iFrame.
-    iApply wp_wand_r.  iSplitL "Hf'"; first done.
+    iSpecialize ("Hf" with "[R HP]"); first by iFrame.
+    iApply wp_wand_r.  iSplitL "Hf"; first done.
     iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
-    iApply release_spec. iFrame "HR Hl Hlocked".
+    iApply (release_spec with "[$HR $Hl $Hlocked]").
     iNext. iIntros "_". by wp_seq.
   Qed.
 End syncer.
diff --git a/sync.v b/sync.v
index 23cf7152faea4f67de1f98c5b4c578e662d3366e..9de76b8e5e0e112e4090cdd60ada784109714c09 100644
--- a/sync.v
+++ b/sync.v
@@ -7,15 +7,22 @@ From iris.heap_lang Require Import proofmode notation.
 Section sync.
   Context `{!heapG Σ} (N : namespace).
 
-  Definition synced R (f' f: val) :=
-    (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) →
-                       ({{ P x }} f' x {{ v, Q x v }}))%I.
+  (* TODO: We could get rid of the x, and hard-code a unit. That would
+     be no loss in expressiveness, but probably more annoying to apply.
+     How much more annoying? And how much to we gain in terms of things
+     becomign easier to prove? *)
+  Definition synced R (f f': val) :=
+    (□ ∀ P Q (x: val), {{ R ★ P }} f x {{ v, R ★ Q v }} →
+                       {{ P }} f' x {{ Q }})%I.
 
+  (* Notice that `s f` is *unconditionally safe* to execute, and only 
+     when executing the returned f' we have to provide a spec for f.
+     This is crucial. *)
+  (* TODO: Use our usual style with a generic post-condition. *)
   Definition is_syncer (R: iProp Σ) (s: val) :=
-    (□ ∀ (f : val), WP s f {{ f', synced R f' f }})%I.
+    (□ ∀ (f : val), WP s f {{ f', synced R f f' }})%I.
 
   Definition mk_syncer_spec (mk_syncer: val) :=
-    ∀ (R: iProp Σ) (Φ: val -> iProp Σ),
-      heapN ⊥ N →
-      heap_ctx ★ R ★ (∀ s, is_syncer R s -★ Φ s) ⊢ WP mk_syncer #() {{ Φ }}.
+    ∀ (R: iProp Σ), heapN ⊥ N →
+      {{{ heap_ctx ★ R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
 End sync.
diff --git a/treiber.v b/treiber.v
index 1a436b007ca96ece4d5ed5ca06333da56f5e6577..59c9b694dbb7944f28be746d33c4248cd87e74fe 100644
--- a/treiber.v
+++ b/treiber.v
@@ -107,15 +107,15 @@ Section proof.
   Qed.
 
   Definition push_triple (s: loc) (x: val) :=
-  atomic_triple _ (fun xs_hd: list val * loc =>
-                       let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
-                  (fun xs_hd ret =>
-                     let '(xs, hd) := xs_hd in 
-                     ∃ hd': loc,
-                       ret = #() ★ s ↦ #hd' ★ hd' ↦ SOMEV (x, #hd) ★ is_list hd xs)%I
-                  (nclose heapN)
-                  ⊤
-                  (push #s x).
+  atomic_triple (fun xs_hd: list val * loc =>
+                     let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
+                (fun xs_hd ret =>
+                   let '(xs, hd) := xs_hd in 
+                   ∃ hd': loc,
+                     ret = #() ★ s ↦ #hd' ★ hd' ↦ SOMEV (x, #hd) ★ is_list hd xs)%I
+                (nclose heapN)
+                ⊤
+                (push #s x).
   
   Lemma push_atomic_spec (s: loc) (x: val) :
     heapN ⊥ N → heap_ctx ⊢ push_triple s x.
@@ -133,7 +133,7 @@ Section proof.
     * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
       iMod ("Hvs'" $! #() with "[-]") as "HQ".
       { iExists l. iSplitR; first done. by iFrame. }
-      iModIntro. wp_if. iModIntro. eauto.
+      iModIntro. wp_if. eauto.
     * wp_cas_fail.
       iDestruct "Hvs'" as "[Hvs' _]".
       iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
@@ -141,16 +141,16 @@ Section proof.
   Qed.
 
   Definition pop_triple (s: loc) :=
-  atomic_triple _ (fun xs_hd: list val * loc =>
-                     let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
-                  (fun xs_hd ret =>
-                     let '(xs, hd) := xs_hd in
-                     (ret = NONEV ★ xs = [] ★ s ↦ #hd ★ is_list hd []) ∨
-                     (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ★ ret = SOMEV x ★
-                                            xs = x :: xs' ★ s ↦ #hd' ★ is_list hd' xs'))%I
-                  (nclose heapN)
-                  ⊤
-                  (pop #s).
+  atomic_triple (fun xs_hd: list val * loc =>
+                   let '(xs, hd) := xs_hd in s ↦ #hd ★ is_list hd xs)%I
+                (fun xs_hd ret =>
+                   let '(xs, hd) := xs_hd in
+                   (ret = NONEV ★ xs = [] ★ s ↦ #hd ★ is_list hd []) ∨
+                   (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ★ ret = SOMEV x ★
+                                          xs = x :: xs' ★ s ↦ #hd' ★ is_list hd' xs'))%I
+                (nclose heapN)
+                ⊤
+                (pop #s).
 
   Lemma pop_atomic_spec (s: loc):
     heapN ⊥ N → heap_ctx ⊢ pop_triple s.
@@ -167,7 +167,7 @@ Section proof.
       iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
       { iLeft. iSplit=>//. iSplit=>//. iFrame. eauto. }
       iModIntro. wp_let. wp_load. wp_match.
-      iModIntro. eauto.
+      eauto.
     - simpl. iDestruct "Hhd" as (hd' q) "([[Hhd1 Hhd2] Hhd'] & Hxs')".
       iDestruct (dup_is_list with "[Hxs']") as "[Hxs1 Hxs2]"; first by iFrame.
       wp_load. iDestruct "Hvs'" as "[Hvs' _]".