diff --git a/theories/logatom/flat_combiner/atomic_sync.v b/theories/logatom/flat_combiner/atomic_sync.v
new file mode 100644
index 0000000000000000000000000000000000000000..08cfa3d3b442c1ac01e8d726a1248ace7e7d7100
--- /dev/null
+++ b/theories/logatom/flat_combiner/atomic_sync.v
@@ -0,0 +1,89 @@
+
+From iris.program_logic Require Export weakestpre hoare atomic.
+From iris.heap_lang Require Export lang proofmode notation.
+From iris.heap_lang.lib Require Import spin_lock.
+From iris.algebra Require Import agree frac.
+From iris_atomic Require Import sync misc.
+
+(** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
+
+Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
+Class syncG Σ := sync_tokG :> inG Σ syncR.
+Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
+
+Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ.
+Proof. by intros ?%subG_inG. Qed.
+
+Section atomic_sync.
+  Context `{EqDecision A, !heapG Σ, !lockG Σ}.
+  Canonical AC := leibnizC A.
+  Context `{!inG Σ (prodR fracR (agreeR AC))}.
+
+  (* 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, to_agree g).
+
+  Definition atomic_seq_spec (ϕ: A → iProp Σ) α β (f x: val) :=
+    (∀ g, {{ ϕ g ∗ α g }} f x {{ v, ∃ g', ϕ g' ∗ β g g' v }})%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 →
+                       <<< ∀ g, gHalf γ g ∗ □ α g >>> f' x @ ⊤ <<< ∃ v, ∃ g', gHalf γ g' ∗ β g g' v, RET v >>>)%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
+     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.
+
+  Definition atomic_syncer_spec (mk_syncer: val) :=
+    ∀ (g0: A) (ϕ: A → iProp Σ),
+      {{{ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 ∗ is_atomic_syncer ϕ γ s }}}.
+
+  Lemma atomic_spec (mk_syncer: val):
+      mk_syncer_spec mk_syncer → atomic_syncer_spec mk_syncer.
+  Proof.
+    iIntros (Hsync g0 ϕ ret) "Hϕ Hret".
+    iMod (own_alloc (((1 / 2)%Qp, to_agree g0) ⋅ ((1 / 2)%Qp, to_agree g0))) as (γ) "[Hg1 Hg2]".
+    { by rewrite pair_op agree_idemp. }
+    iApply (Hsync (∃ g: A, ϕ g ∗ gHalf γ g)%I with "[Hg1 Hϕ]")=>//.
+    { iExists g0. by iFrame. }
+    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". change (ofe_car AC) with A.
+    iApply wp_atomic_intro. iIntros (Φ') "?".
+    (* TODO: Why can't I iApply "Hsynced"? *)
+    iSpecialize ("Hsynced" $! _ Φ' x).
+    iApply wp_wand_r. iSplitL.
+    - iApply ("Hsynced" with "[]")=>//; last iAccu.
+      iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ Hg1]".
+      (* we should view shift at this point *)
+      iApply fupd_wp. iMod "HP" as (?) "[[Hg2 #Hα] [Hvs1 _]]".
+      iDestruct (m_frag_agree with "Hg1 Hg2") as %Heq. subst.
+      iMod ("Hvs1" with "[Hg2]") as "HP"; first by iFrame.
+      iModIntro. iApply wp_fupd. iApply wp_wand_r. iSplitL "Hϕ".
+      { iApply "Hseq". iFrame. done. }
+      iIntros (v) "H". iDestruct "H" as (g') "[Hϕ' Hβ]".
+      iMod ("HP") as (g'') "[[Hg'' _] [_ Hvs2]]".
+      iSpecialize ("Hvs2" $! v).
+      iDestruct (m_frag_agree' with "Hg'' Hg1") as "[Hg %]". subst.
+      rewrite Qp_div_2.
+      iAssert (|==> own γ (((1 / 2)%Qp, to_agree g') ⋅ ((1 / 2)%Qp, to_agree g')))%I
+              with "[Hg]" as ">[Hg1 Hg2]".
+      { iApply own_update; last by iAssumption.
+        apply cmra_update_exclusive. by rewrite pair_op agree_idemp. }
+      iMod ("Hvs2" with "[Hg1 Hβ]").
+      { iExists g'. iFrame. }
+      iModIntro. iSplitL "Hg2 Hϕ'"; last done.
+      iExists g'. by iFrame.
+    - iIntros (?) "?". done.
+  Qed.
+
+End atomic_sync.
diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v
new file mode 100644
index 0000000000000000000000000000000000000000..c6b0b316d26e9aa3a4a4181b88871619d16e356e
--- /dev/null
+++ b/theories/logatom/flat_combiner/flat.v
@@ -0,0 +1,301 @@
+(* Flat Combiner *)
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang.lib Require Import spin_lock.
+From iris.algebra Require Import auth frac agree excl agree gset gmap.
+From iris.base_logic Require Import saved_prop.
+From iris_atomic Require Import misc peritem sync.
+
+Definition doOp : val :=
+  λ: "p",
+     match: !"p" with
+       InjL "req" => "p" <- InjR ((Fst "req") (Snd "req"))
+     | InjR "_" => #()
+     end.
+
+Definition try_srv : val :=
+  λ: "lk" "s",
+    if: try_acquire "lk"
+      then let: "hd" := !"s" in
+           iter "hd" doOp;;
+           release "lk"
+      else #().
+
+Definition loop: val :=
+  rec: "loop" "p" "s" "lk" :=
+    match: !"p" with
+    InjL "_" =>
+        try_srv "lk" "s";;
+        "loop" "p" "s" "lk"
+    | InjR "r" => "r"
+    end.
+
+Definition install : val :=
+  λ: "f" "x" "s",
+     let: "p" := ref (InjL ("f", "x")) in
+     push "s" "p";;
+     "p".
+
+Definition mk_flat : val :=
+  λ: <>,
+   let: "lk" := newlock #() in
+   let: "s" := new_stack #() in
+   λ: "f" "x",
+      let: "p" := install "f" "x" "s" in
+      let: "r" := loop "p" "s" "lk" in
+      "r".
+
+Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *)
+Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
+Class flatG Σ := FlatG {
+  req_G :> inG Σ reqR;
+  sp_G  :> savedPredG Σ val
+}.
+
+Definition flatΣ : gFunctors :=
+  #[ GFunctor (constRF reqR);
+     savedPredΣ val ].
+
+Instance subG_flatΣ {Σ} : subG flatΣ Σ → flatG Σ.
+Proof. intros [?%subG_inG [? _]%subG_inv]%subG_inv. split; apply _. Qed.
+
+Section proof.
+  Context `{!heapG Σ, !lockG Σ, !flatG Σ} (N: namespace).
+
+  Definition init_s (ts: toks) :=
+    let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ()) ∗ own γ3 (Excl ()))%I.
+
+  Definition installed_s R (ts: toks) (f x: val) :=
+    let '(γx, γ1, _, γ4, γq) := ts in
+    (∃ (P: val → iProp Σ) Q,
+       own γx ((1/2)%Qp, to_agree x) ∗ P x ∗ ({{ R ∗ P x }} f x {{ v, R ∗ Q x v }}) ∗
+       saved_pred_own γq (Q x) ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.
+
+  Definition received_s (ts: toks) (x: val) γr :=
+    let '(γx, _, _, γ4, _) := ts in
+    (own γx ((1/2/2)%Qp, to_agree x) ∗ own γr (Excl ()) ∗ own γ4 (Excl ()))%I.
+
+  Definition finished_s (ts: toks) (x y: val) :=
+    let '(γx, γ1, _, γ4, γq) := ts in
+    (∃ Q: val → val → iProp Σ,
+       own γx ((1/2)%Qp, to_agree x) ∗ saved_pred_own γq (Q x) ∗
+       Q x y ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.
+  
+  Definition p_inv R (γm γr: gname) (ts: toks) (p : loc) :=
+    ( (* INIT *)
+      (∃ y: val, p ↦ InjRV y ∗ init_s ts) ∨
+      (* INSTALLED *)
+      (∃ f x: val, p ↦ InjLV (f, x) ∗ installed_s R ts f x) ∨
+      (* RECEIVED *)
+      (∃ f x: val, p ↦ InjLV (f, x) ∗ received_s ts x γr) ∨
+      (* FINISHED *)
+      (∃ x y: val, p ↦ InjRV y ∗ finished_s ts x y))%I.
+
+  Definition p_inv' R γm γr : val → iProp Σ :=
+    (λ v: val, ∃ ts (p: loc), ⌜v = #p⌝ ∗ inv N (p_inv R γm γr ts p))%I.
+
+  Definition srv_bag R γm γr s := (∃ xs, is_bag_R N (p_inv' R γm γr) xs s)%I.
+
+  Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) :=
+    let '(γx, _, γ3, _, γq) := ts in
+    (own γ3 (Excl ()) ∗ own γx ((1/2)%Qp, to_agree x) ∗ saved_pred_own γq Q)%I.
+
+  Lemma install_spec R P Q (f x: val) (γm γr: gname) (s: loc):
+    {{{ inv N (srv_bag R γm γr s) ∗ P ∗ ({{ R ∗ P }} f x {{ v, R ∗ Q v }}) }}}
+      install f x #s
+    {{{ p ts, RET #p; installed_recp ts x Q ∗ inv N (p_inv R γm γr ts p) }}}.
+  Proof.
+    iIntros (Φ) "(#? & HP & Hf) HΦ".
+    wp_lam. wp_pures. wp_alloc p as "Hl".
+    iApply fupd_wp.
+    iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
+    iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
+    iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
+    iMod (own_alloc (1%Qp, to_agree x)) as (γx) "Hx"; first done.
+    iMod (saved_pred_alloc Q) as (γq) "#?".
+    iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
+    iModIntro. wp_let. wp_bind (push _ _).
+    iMod (inv_alloc N _ (p_inv R γm γr (γx, γ1, γ3, γ4, γq) p)
+          with "[-HΦ Hx2 Ho3]") as "#HRx"; first eauto.
+    { iNext. iRight. iLeft. iExists f, x. iFrame.
+      iExists (λ _, P), (λ _ v, Q v).
+      iFrame. iFrame "#". }
+    iApply (push_spec N (p_inv' R γm γr) s #p
+            with "[-HΦ Hx2 Ho3]")=>//.
+    { iFrame "#". iExists (γx, γ1, γ3, γ4, γq), p.
+      iSplitR; first done. iFrame "#". }
+    iNext. iIntros "?".
+    wp_seq. iApply ("HΦ" $! p (γx, γ1, γ3, γ4, γq)).
+    iFrame. iFrame "#".
+  Qed.
+
+  Lemma doOp_f_spec R γm γr (p: loc) ts:
+    f_spec N (p_inv R γm γr ts p) doOp (own γr (Excl ()) ∗ R)%I #p.
+  Proof.
+    iIntros (Φ) "(#H1 & Hor & HR) HΦ".
+    wp_rec. wp_bind (! _)%E.
+    iInv N as "Hp" "Hclose".
+    iDestruct "Hp" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
+    - iDestruct "Hp" as (y) "[>Hp Hts]".
+      wp_load. iMod ("Hclose" with "[-Hor HR HΦ]").
+      { iNext. iFrame "#". iLeft. iExists y. iFrame. }
+      iModIntro. wp_match. iApply ("HΦ" with "[Hor HR]"). iFrame.
+    - destruct ts as [[[[γx γ1] γ3] γ4] γq].
+      iDestruct "Hp" as (f x) "(>Hp & Hts)".
+      iDestruct "Hts" as (P Q) "(>Hx & Hpx & Hf' & HoQ & >Ho1 & >Ho4)".
+      iAssert (|==> own γx (((1/2/2)%Qp, to_agree x) ⋅
+                            ((1/2/2)%Qp, to_agree x)))%I with "[Hx]" as ">[Hx1 Hx2]".
+      { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
+        rewrite -{1}(Qp_div_2 (1/2)%Qp).
+        by apply pair_l_frac_op'. }
+      wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ Hpx]").
+      { iNext. iFrame. iFrame "#". iRight. iRight. iLeft. iExists f, x. iFrame. }
+      iModIntro. wp_match. wp_pures.
+      wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
+      { iApply "Hf'". iFrame. }
+      iIntros (v) "[HR HQ]". wp_pures.
+      iInv N as "Hx" "Hclose".
+      iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
+      * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
+        iApply excl_falso. iFrame.
+      * iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
+        iApply excl_falso. iFrame.
+      * iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
+        wp_store. iDestruct (m_frag_agree' with "Hx Hx2") as "[Hx %]".
+        subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
+        { iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
+          iRight. iExists _, v. iFrame. iExists Q. iFrame. }
+        iApply "HΦ". iFrame. done.
+      * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
+        iApply excl_falso. iFrame.
+    - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
+      iApply excl_falso. iFrame.
+    - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
+        iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
+        wp_load. iMod ("Hclose" with "[-HΦ HR Hor]").
+        { iNext. iRight. iRight. iRight. iExists x', y. iFrame. iExists Q. iFrame. }
+        iModIntro. wp_match. iApply "HΦ". iFrame.
+  Qed.
+
+  Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
+  Definition finished_recp (ts: toks) (x y: val) :=
+    let '(γx, _, _, _, γq) := ts in
+    (∃ Q, own γx ((1 / 2)%Qp, to_agree x) ∗ saved_pred_own γq (Q x) ∗ Q x y)%I.
+
+  Lemma loop_iter_doOp_spec R (γm γr: gname) xs:
+  ∀ (hd: loc),
+    {{{ is_list_R N (p_inv' R γm γr) hd xs ∗ own γr (Excl ()) ∗ R }}}
+      iter #hd doOp
+    {{{ RET #(); own γr (Excl ()) ∗ R }}}.
+  Proof.
+    induction xs as [|x xs' IHxs].
+    - iIntros (hd Φ) "[Hxs ?] HΦ".
+      simpl. wp_rec. wp_let.
+      iDestruct "Hxs" as (?) "Hhd".
+      wp_load. wp_match. by iApply "HΦ".
+    - iIntros (hd Φ) "[Hxs HRf] HΦ". simpl.
+      iDestruct "Hxs" as (hd' ?) "(Hhd & #Hinv & Hxs')".
+      wp_rec. wp_let. wp_bind (! _)%E.
+      iInv N as "H" "Hclose".
+      iDestruct "H" as (ts p) "[>% #?]". subst.
+      wp_load. iMod ("Hclose" with "[]").
+      { iNext. iExists ts, p. eauto. }
+      iModIntro. wp_match. wp_proj. wp_bind (doOp _).
+      iDestruct (doOp_f_spec R γm γr p ts) as "Hf".
+      iApply ("Hf" with "[HRf]").
+      { iFrame. iFrame "#". }
+      iNext. iIntros "HRf".
+      wp_seq. wp_proj. iApply (IHxs with "[-HΦ]")=>//.
+      iFrame "#"; first by iFrame.
+  Qed.
+
+  Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
+    inv N (srv_bag R γm γr s) ∗
+    is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ Φ #()
+    ⊢ WP try_srv lk #s {{ Φ }}.
+  Proof.
+    iIntros "(#? & #? & HΦ)". wp_lam. wp_pures.
+    wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
+    iNext. iIntros ([]); last by (iIntros; wp_if).
+    iIntros "[Hlocked [Ho2 HR]]".
+    wp_if. wp_bind (! _)%E.
+    iInv N as "H" "Hclose".
+    iDestruct "H" as (xs' hd') "[>Hs Hxs]".
+    wp_load. iDestruct (dup_is_list_R with "[Hxs]") as ">[Hxs1 Hxs2]"; first by iFrame.
+    iMod ("Hclose" with "[Hs Hxs1]").
+    { iNext. iFrame. iExists xs', hd'. by iFrame. }
+    iModIntro. wp_let. wp_bind (iter _ _).
+    iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
+    { iApply (loop_iter_doOp_spec R _ _ _ _ (λ _, own γr (Excl ()) ∗ R)%I with "[-]")=>//.
+      iFrame "#". iFrame. eauto. }
+    iIntros (f') "[Ho HR]". wp_seq.
+    iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗".
+    iNext. iIntros. done.
+  Qed.
+
+  Lemma loop_spec R (p s: loc) (lk: val)
+        (γs γr γm γlk: gname) (ts: toks):
+    {{{ inv N (srv_bag R γm γr s) ∗ inv N (p_inv R γm γr ts p) ∗
+        is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ own_γ3 ts }}}
+      loop #p #s lk
+    {{{ x y, RET y; finished_recp ts x y }}}.
+  Proof.
+    iIntros (Φ) "(#? & #? & #? & Ho3) HΦ".
+    iLöb as "IH". wp_rec. repeat wp_let.
+    wp_bind (! _)%E. iInv N as "Hp" "Hclose".
+    destruct ts as [[[[γx γ1] γ3] γ4] γq].
+    iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
+    + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
+      iApply excl_falso. iFrame.
+    + iDestruct "Hp" as (f x) "(>Hp & Hs')".
+      wp_load. iMod ("Hclose" with "[Hp Hs']").
+      { iNext. iFrame. iRight. iLeft. iExists f, x. iFrame. }
+      iModIntro. wp_match. wp_bind (try_srv _ _). iApply try_srv_spec=>//.
+      iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
+    + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
+      wp_load. iMod ("Hclose" with "[-Ho3 HΦ]").
+      { iNext. iFrame. iRight. iRight. iLeft. iExists f, x. iFrame. }
+      iModIntro. wp_match.
+      wp_bind (try_srv _ _). iApply try_srv_spec=>//.
+      iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
+    + iDestruct "Hp" as (x y) "[>Hp Hs']".
+      iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
+      wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
+      { iNext. iFrame. iLeft. iExists y. iFrame. }
+      iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
+      iExists Q. iFrame.
+  Qed.
+
+  Lemma mk_flat_spec (γm: gname): mk_syncer_spec mk_flat.
+  Proof.
+    iIntros (R Φ) "HR HΦ".
+    iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
+    wp_lam. wp_bind (newlock _).
+    iApply (newlock_spec _ (own γr (Excl ()) ∗ R)%I with "[$Ho2 $HR]")=>//.
+    iNext. iIntros (lk γlk) "#Hlk".
+    wp_let. wp_bind (new_stack _).
+    iApply (new_bag_spec N (p_inv' R γm γr))=>//.
+    iNext. iIntros (s) "#Hss".
+    wp_pures. iApply "HΦ". rewrite /synced.
+    iAlways. iIntros (f). wp_pures. iAlways.
+    iIntros (P Q x) "#Hf".
+    iIntros "!# Hp". wp_pures. wp_bind (install _ _ _).
+    iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
+    { iFrame. iFrame "#". }
+    iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
+    wp_let. wp_bind (loop _ _ _).
+    iApply (loop_spec with "[-Hx HoQ]")=>//.
+    { iFrame "#". iFrame. }
+    iNext. iIntros (? ?) "Hs".
+    iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
+    destruct (decide (x = a)) as [->|Hneq].
+    - iDestruct (saved_pred_agree _ _ _ a0 with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
+      wp_let. by iRewrite -"Heq" in "HQ'".
+    - iExFalso. iCombine "Hx" "Hx'" as "Hx".
+      iDestruct (own_valid with "Hx") as %[_ H1].
+      rewrite //= in H1.
+      by apply agree_op_inv' in H1.
+  Qed.
+
+End proof.
diff --git a/theories/logatom/flat_combiner/misc.v b/theories/logatom/flat_combiner/misc.v
new file mode 100644
index 0000000000000000000000000000000000000000..07ee8cc9917f5775e48358166d616a02b0012fba
--- /dev/null
+++ b/theories/logatom/flat_combiner/misc.v
@@ -0,0 +1,87 @@
+(* Miscellaneous lemmas *)
+
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang proofmode notation.
+From iris.algebra Require Import auth frac gmap agree.
+From iris.bi Require Import fractional.
+From iris.base_logic Require Import auth.
+
+Import uPred.
+
+Section lemmas.
+  Lemma pair_l_frac_op' (p q: Qp) (g g': val):
+     ((p + q)%Qp, to_agree g') ~~> (((p, to_agree g') ⋅ (q, to_agree g'))).
+  Proof. by rewrite pair_op agree_idemp frac_op'. Qed.
+
+  Lemma pair_l_frac_op_1' (g g': val):
+     (1%Qp, to_agree g') ~~> (((1/2)%Qp, to_agree g') ⋅ ((1/2)%Qp, to_agree g')).
+  Proof. by rewrite pair_op agree_idemp frac_op' Qp_div_2. Qed.
+  
+End lemmas.
+
+Section excl.
+  Context `{!inG Σ (exclR unitC)}.
+  Lemma excl_falso γ Q':
+    own γ (Excl ()) ∗ own γ (Excl ()) ⊢ Q'.
+  Proof.
+    iIntros "[Ho1 Ho2]". iCombine "Ho1" "Ho2" as "Ho".
+    iExFalso. by iDestruct (own_valid with "Ho") as "%".
+  Qed.
+End excl.
+
+Section heap_extra.
+  Context `{heapG Σ}.
+
+  Lemma bogus_heap p (q1 q2: Qp) a b:
+    ~((q1 + q2)%Qp ≤ 1%Qp)%Qc →
+    p ↦{q1} a ∗ p ↦{q2} b ⊢ False.
+  Proof.
+    iIntros (?) "Hp".
+    iDestruct "Hp" as "[Hl Hr]".
+    iDestruct (@mapsto_valid_2 with "Hl Hr") as %H'. done.
+  Qed.
+
+End heap_extra.
+
+Section big_op_later.
+  Context {M : ucmraT}.
+  Context `{Countable K} {A : Type}.
+  Implicit Types m : gmap K A.
+  Implicit Types Φ Ψ : K → A → uPred M. 
+
+  Lemma big_sepM_delete_later Φ m i x :
+    m !! i = Some x →
+    ▷ ([∗ map] k↦y ∈ m, Φ k y) ⊣⊢ ▷ Φ i x ∗ ▷ [∗ map] k↦y ∈ delete i m, Φ k y.
+  Proof. intros ?. rewrite big_sepM_delete=>//. apply later_sep. Qed.
+
+  Lemma big_sepM_insert_later Φ m i x :
+    m !! i = None →
+    ▷ ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ ▷ Φ i x ∗ ▷ [∗ map] k↦y ∈ m, Φ k y.
+  Proof. intros ?. rewrite big_sepM_insert=>//. apply later_sep. Qed.
+End big_op_later.
+
+Section pair.
+  Context {A : ofeT} `{EqDecision A, !OfeDiscrete A, !LeibnizEquiv A, !inG Σ (prodR fracR (agreeR A))}.
+
+  Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
+    own γm (q1, to_agree a1) -∗ own γm (q2, to_agree a2) -∗ ⌜a1 = a2⌝.
+  Proof.
+    iIntros "Ho Ho'".
+    destruct (decide (a1 = a2)) as [->|Hneq]=>//.
+    iCombine "Ho" "Ho'" as "Ho".
+    iDestruct (own_valid with "Ho") as %Hvalid.
+    exfalso. destruct Hvalid as [_ Hvalid].
+    simpl in Hvalid. apply agree_op_inv in Hvalid. apply (inj to_agree) in Hvalid.
+    apply Hneq. by fold_leibniz.
+  Qed.
+  
+  Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
+    own γm (q1, to_agree a1) -∗ own γm (q2, to_agree a2)
+    -∗ own γm ((q1 + q2)%Qp, to_agree a1) ∗ ⌜a1 = a2⌝.
+  Proof.
+    iIntros "Ho Ho'".
+    iDestruct (m_frag_agree with "Ho Ho'") as %Heq.
+    subst. iCombine "Ho" "Ho'" as "Ho".
+    by iFrame.
+  Qed.
+End pair.
diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v
new file mode 100644
index 0000000000000000000000000000000000000000..5590e2b98c3eab25f3a0f61294551879fab23922
--- /dev/null
+++ b/theories/logatom/flat_combiner/peritem.v
@@ -0,0 +1,88 @@
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import frac auth gmap csum.
+From iris_atomic Require Export treiber misc.
+From iris.base_logic.lib Require Import invariants.
+
+Section defs.
+  Context `{heapG Σ} (N: namespace).
+  Context (R: val → iProp Σ) `{∀ x, TimelessP (R x)}.
+
+  Fixpoint is_list_R (hd: loc) (xs: list val) : iProp Σ :=
+    match xs with
+    | [] => (∃ q, hd ↦{ q } NONEV)%I
+    | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ∗ inv N (R x) ∗ is_list_R hd' xs)%I
+    end.
+
+  Definition is_bag_R xs s := (∃ hd: loc, s ↦ #hd ∗ is_list_R hd xs)%I.
+
+  Lemma dup_is_list_R : ∀ xs hd,
+    is_list_R hd xs ⊢ |==> is_list_R hd xs ∗ is_list_R hd xs.
+  Proof.
+    induction xs as [|y xs' IHxs'].
+    - iIntros (hd) "Hs".
+      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
+    - iIntros (hd) "Hs". simpl.
+      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hinv & Hs')".
+      iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
+      iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
+  Qed.
+
+  Definition f_spec (R: iProp Σ) (f: val) (Rf: iProp Σ) x :=
+    {{{ inv N R ∗ Rf }}}
+      f x
+    {{{ RET #(); Rf }}}.
+
+End defs.
+
+Section proofs.
+  Context `{heapG Σ} (N: namespace).
+  Context (R: val → iProp Σ).
+
+  Definition bag_inv s: iProp Σ := inv N (∃ xs, is_bag_R N R xs s)%I.
+
+  Lemma new_bag_spec:
+    {{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". iApply wp_fupd.
+    wp_lam. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
+    wp_alloc s as "Hs".
+    iAssert ((∃ xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
+    { iFrame. iExists [], l.
+      iFrame. simpl. eauto. }
+    iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
+    iApply "HΦ". iFrame "#". done.
+  Qed.
+  
+  Lemma push_spec (s: loc) (x: val):
+    {{{ R x ∗ bag_inv s }}} push #s x {{{ RET #() ; inv N (R x) }}}.
+  Proof.
+    iIntros (Φ) "(HRx & #?) HΦ".
+    iLöb as "IH". wp_rec. wp_let.
+    wp_bind (! _)%E.
+    iInv N as "H1" "Hclose".
+    iDestruct "H1" as (xs hd) "[>Hs H1]".
+    wp_load. iMod ("Hclose" with "[Hs H1]").
+    { iNext. iFrame. iExists xs, hd. iFrame. }
+    iModIntro. wp_let. wp_alloc l as "Hl".
+    wp_let. wp_bind (CAS _ _ _)%E.
+    iInv N as "H1" "Hclose".
+    iDestruct "H1" as (xs' hd') "[>Hs H1]".
+    destruct (decide (hd = hd')) as [->|Hneq].
+    - wp_cas_suc.
+      iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
+      iMod ("Hclose" with "[Hs Hl H1]").
+      { iNext. iFrame. iExists (x::xs'), l.
+        iFrame. simpl. iExists hd', 1%Qp. iFrame.
+        by iFrame "#". }
+      iModIntro. wp_if. by iApply "HΦ".
+    - wp_cas_fail.
+      iMod ("Hclose" with "[Hs H1]").
+      { iNext. iFrame. iExists (xs'), hd'. iFrame. }
+      iModIntro. wp_if. iApply ("IH" with "HRx").
+      by iNext.
+  Qed.
+
+End proofs.
diff --git a/theories/logatom/flat_combiner/simple_sync.v b/theories/logatom/flat_combiner/simple_sync.v
new file mode 100644
index 0000000000000000000000000000000000000000..b601b31d1211e449dfcdc25146216b67f4e518cc
--- /dev/null
+++ b/theories/logatom/flat_combiner/simple_sync.v
@@ -0,0 +1,39 @@
+(* Coarse-grained syncer *)
+
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang proofmode notation.
+From iris.heap_lang.lib Require Import spin_lock.
+From iris.algebra Require Import frac.
+From iris_atomic Require Import sync.
+Import uPred.
+
+Definition mk_sync: val :=
+  λ: <>,
+       let: "l" := newlock #() in
+       λ: "f" "x",
+          acquire "l";;
+          let: "ret" := "f" "x" in
+          release "l";;
+          "ret".
+
+Section syncer.
+  Context `{!heapG Σ, !lockG Σ} (N: namespace).
+  
+  Lemma mk_sync_spec: mk_syncer_spec mk_sync.
+  Proof.
+    iIntros (R Φ) "HR HΦ".
+    wp_lam. wp_bind (newlock _).
+    iApply (newlock_spec N R with "[HR]"); first done. iNext.
+    iIntros (lk γ) "#Hl". wp_pures. iApply "HΦ". iIntros "!#".
+    iIntros (f). wp_pures. iAlways.
+    iIntros (P Q x) "#Hf !# HP".
+    wp_pures. wp_bind (acquire _).
+    iApply (acquire_spec with "Hl"). iNext.
+    iIntros "[Hlocked R]". wp_seq. wp_bind (f _).
+    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 with "[$Hl $HR $Hlocked]").
+    iNext. iIntros "_". by wp_seq.
+  Qed.
+End syncer.
diff --git a/theories/logatom/flat_combiner/sync.v b/theories/logatom/flat_combiner/sync.v
new file mode 100644
index 0000000000000000000000000000000000000000..198a8cb5d5edfa5c46db41048a7a9f40ec6cc4ce
--- /dev/null
+++ b/theories/logatom/flat_combiner/sync.v
@@ -0,0 +1,28 @@
+(* Syncer spec *)
+
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+
+Section sync.
+  Context `{!heapG Σ} (N : namespace).
+
+  (* 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
+     becoming 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.
+
+  Definition mk_syncer_spec (mk_syncer: val) :=
+    ∀ (R: iProp Σ),
+      {{{ R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
+End sync.
diff --git a/theories/logatom/treiber.v b/theories/logatom/treiber.v
new file mode 100644
index 0000000000000000000000000000000000000000..d2d2297f29252083fedef5f059b75b423a79faba
--- /dev/null
+++ b/theories/logatom/treiber.v
@@ -0,0 +1,173 @@
+From stdpp Require Import namespaces.
+From iris.program_logic Require Export weakestpre atomic.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import frac auth gmap csum.
+
+Definition new_stack: val := λ: <>, ref (ref NONE).
+
+Definition push: val :=
+  rec: "push" "s" "x" :=
+      let: "hd" := !"s" in
+      let: "s'" := ref SOME ("x", "hd") in
+      if: CAS "s" "hd" "s'"
+        then #()
+        else "push" "s" "x".
+
+Definition pop: val :=
+  rec: "pop" "s" :=
+      let: "hd" := !"s" in
+      match: !"hd" with
+        SOME "cell" =>
+        if: CAS "s" "hd" (Snd "cell")
+          then SOME (Fst "cell")
+          else "pop" "s"
+      | NONE => NONE
+      end.
+
+Definition iter: val :=
+  rec: "iter" "hd" "f" :=
+      match: !"hd" with
+        NONE => #()
+      | SOME "cell" => "f" (Fst "cell") ;; "iter" (Snd "cell") "f"
+      end.
+
+Section proof.
+  Context `{!heapG Σ} (N: namespace).
+
+  Fixpoint is_list (hd: loc) (xs: list val) : iProp Σ :=
+    match xs with
+    | [] => (∃ q, hd ↦{ q } NONEV)%I
+    | x :: xs => (∃ (hd': loc) q, hd ↦{ q } SOMEV (x, #hd') ∗ is_list hd' xs)%I
+    end.
+
+  Lemma dup_is_list : ∀ xs hd,
+    is_list hd xs ⊢ is_list hd xs ∗ is_list hd xs.
+  Proof.
+    induction xs as [|y xs' IHxs'].
+    - iIntros (hd) "Hs".
+      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
+    - iIntros (hd) "Hs". simpl.
+      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hs')".
+      iDestruct (IHxs' with "[Hs']") as "[Hs1 Hs2]"; first by iFrame.
+      iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
+  Qed.
+
+  Lemma uniq_is_list:
+    ∀ xs ys hd, is_list hd xs ∗ is_list hd ys ⊢ ⌜xs = ys⌝.
+  Proof.
+    induction xs as [|x xs' IHxs'].
+    - induction ys as [|y ys' IHys'].
+      + auto.
+      + iIntros (hd) "(Hxs & Hys)".
+        simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
+        iExFalso. iDestruct "Hxs" as (?) "Hhd'".
+        (* FIXME: If I dont use the @ here and below through this file, it loops. *)
+        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
+    - induction ys as [|y ys' IHys'].
+      + iIntros (hd) "(Hxs & Hys)".
+        simpl.
+        iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
+        iDestruct "Hys" as (?) "Hhd'".
+        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
+      + iIntros (hd) "(Hxs & Hys)".
+        simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
+        iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
+        iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
+        subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
+        by subst.
+  Qed.
+
+  Definition is_stack (s: loc) xs: iProp Σ := (∃ hd: loc, s ↦ #hd ∗ is_list hd xs)%I.
+
+  Global Instance is_list_timeless xs hd: Timeless (is_list hd xs).
+  Proof. generalize hd. induction xs; apply _. Qed.
+
+  Global Instance is_stack_timeless xs hd: Timeless (is_stack hd xs).
+  Proof. generalize hd. induction xs; apply _. Qed.
+
+  Lemma new_stack_spec:
+    ∀ (Φ: val → iProp Σ),
+      (∀ s, is_stack s [] -∗ Φ #s) ⊢ WP new_stack #() {{ Φ }}.
+  Proof.
+    iIntros (Φ) "HΦ". wp_lam.
+    wp_bind (ref NONE)%E. wp_alloc l as "Hl".
+    wp_alloc l' as "Hl'".
+    iApply "HΦ". rewrite /is_stack. iExists l.
+    iFrame. by iExists 1%Qp.
+  Qed.
+
+  Definition push_triple (s: loc) (x: val) :=
+    <<< ∀ (xs : list val) (hd : loc), s ↦ #hd ∗ is_list hd xs >>>
+      push #s x @ ⊤
+    <<< ∃ hd' : loc, s ↦ #hd' ∗ hd' ↦ SOMEV (x, #hd) ∗ is_list hd xs, RET #() >>>.
+  
+  Lemma push_atomic_spec (s: loc) (x: val) :
+    push_triple s x.
+  Proof.
+    rewrite /push_triple. iApply wp_atomic_intro.
+    iIntros (Φ) "HP". iLöb as "IH". wp_rec.
+    wp_let. wp_bind (! _)%E.
+    iMod "HP" as (xs hd) "[[Hs Hhd] [Hvs' _]]".
+    wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
+    iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
+    wp_bind (CAS _ _ _)%E.
+    iMod "HP" as (xs' hd') "[[Hs Hhd'] Hvs']".
+    destruct (decide (hd = hd')) as [->|Hneq].
+    * wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
+      iMod ("Hvs'" with "[-]") as "HQ".
+      { by iFrame. }
+      iModIntro. wp_if. eauto.
+    * wp_cas_fail.
+      iDestruct "Hvs'" as "[Hvs' _]".
+      iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
+      iModIntro. wp_if. by iApply "IH".
+  Qed.
+
+  Definition pop_triple (s: loc) :=
+    <<< ∀ (xs : list val) (hd : loc), s ↦ #hd ∗ is_list hd xs >>>
+      pop #s @ ⊤
+    <<< match xs with [] => s ↦ #hd ∗ is_list hd []
+                | x::xs' => ∃ q (hd': loc), hd ↦{q} SOMEV (x, #hd') ∗ s ↦ #hd' ∗ is_list hd' xs' end,
+    RET match xs with [] => NONEV | x :: _ => SOMEV x end >>>.
+
+  Lemma pop_atomic_spec (s: loc):
+    pop_triple s.
+  Proof.
+    rewrite /pop_triple. iApply wp_atomic_intro.
+    iIntros (Φ) "HP". iLöb as "IH". wp_rec.
+    wp_bind (! _)%E.
+    iMod "HP" as (xs hd) "[[Hs Hhd] Hvs']".
+    destruct xs as [|y' xs'].
+    - simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
+      iDestruct "Hhd" as (q) "[Hhd Hhd']".
+      iMod ("Hvs'" with "[-Hhd]") as "HQ".
+      { iFrame. eauto. }
+      iModIntro. wp_let. wp_load. wp_pures.
+      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' _]".
+      iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
+      { iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
+      iModIntro. wp_let. wp_load. wp_match. wp_proj.
+      wp_bind (CAS _ _ _).
+      iMod "HP" as (xs hd'') "[[Hs Hhd''] Hvs']".
+      destruct (decide (hd = hd'')) as [->|Hneq].
+      + wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
+        destruct xs as [|x' xs''].
+        { simpl. iDestruct "Hhd''" as (?) "H".
+          iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?. }
+        simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
+        iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=]. subst.
+        iMod ("Hvs'" with "[-]") as "HQ".
+        { iExists (q / 2 / 2)%Qp, _.
+          iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
+          repeat (iSplitR "Hxs1 Hs"; first done).
+          iFrame. }
+        iModIntro. wp_if. wp_pures. eauto.
+      + wp_cas_fail. iDestruct "Hvs'" as "[Hvs' _]".
+        iMod ("Hvs'" with "[-]") as "HP"; first by iFrame.
+        iModIntro. wp_if. by iApply "IH".
+  Qed.
+End proof.