diff --git a/atomic.v b/atomic.v
index e765fa87c44b8802ef9aed0287aae95ecf1da087..ee42b9071f07ef2716d3a5ff4e9c3ec4bdaea5af 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 {_} _ _ _ _.
 End atomic.
diff --git a/atomic_incr.v b/atomic_incr.v
index 5f612bc1ea2ee6ecc10a40aa1f69facd1046b165..9b17c020c159c0cf366e2f03f04b80dcf186b847 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.
diff --git a/atomic_pcas.v b/atomic_pcas.v
index 33a7d32bb3831a6406dc889941386e85c99b4e5f..4b6b397ec66695b6acd750a9abcf1275b99df933 100644
--- a/atomic_pcas.v
+++ b/atomic_pcas.v
@@ -33,7 +33,8 @@ 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. iPureIntro.
     iIntros (x Φ g HN) "(#Hh & Hg & #Hα & HΦ)".
@@ -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 03ae1c746c13e41da0a8817e11e04352d0900b5e..0466de9b523725a5cf9e017e2e0211c0556d4d90 100644
--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -15,62 +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 with "[$Hh Hg1 Hϕ]")=>//.
+    iApply (Hsync (∃ g: A, ϕ g ★ gHalf γ g)%I with "[$Hh Hg1 Hϕ]")=>//.
     { iExists g0. by iFrame. }
-    iNext. 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".
-    iSpecialize ("Hsynced" $! (P x) (Q x) x).
-    iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
+    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 (fun v => ∃ x, Q x v)%I x).
+    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 *)
@@ -78,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
@@ -90,9 +81,9 @@ Section atomic_sync.
         apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
       iMod ("Hvs2" with "[Hg1 Hβ]").
       { iExists g'. iFrame. }
-      iModIntro. iSplitL "Hg2 HÏ•'"; last done.
+      iModIntro. iSplitL "Hg2 HÏ•'"; last by iExists g''.
       iExists g'. by iFrame.
-    - iIntros (?) "?". by iExists g0.
+    - iIntros (?) "?". done.
   Qed.
 
 End atomic_sync.
diff --git a/treiber.v b/treiber.v
index 56c04fc0a72c44ed64c46e1094de1499934d2607..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.
@@ -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.