(* Some refinement from the paper
   "The effects of higher-order state and control on local relational reasoning"
   D. Dreyer, G. Neis, L. Birkedal
*)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import csum agree excl.
From iris_logrel Require Import logrel examples.lock examples.counter.

Section refinement.
  Context `{logrelG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).

  Lemma refinement1 Γ :
    Γ ⊨
      let: "x" := ref #1 in
      (λ: "f", "f" #();; !"x")
    ≤log≤
      (λ: "f", "f" #();; #1)
    : TArrow (TArrow TUnit TUnit) TNat.
  Proof.
  iIntros (Δ).
  rel_alloc_l as x "Hx".
  iMod (inv_alloc (nroot.@"xinv") _ (x ↦ᵢ #1)%I with "Hx") as "#Hinv".
  rel_let_l.
  iApply bin_log_related_arrow; auto.
  iIntros "!#" (f1 f2) "Hf".
  rel_let_l. rel_let_r.
  iApply (bin_log_related_seq with "[Hf]"); auto.
  - iApply (bin_log_related_app with "Hf").
    by rel_vals.
  - rel_load_l_atomic.
    iInv (nroot.@"xinv") as "Hx" "Hcl".
    iModIntro. iExists _; iFrame "Hx".
    iNext. iIntros "Hx".
    iMod ("Hcl" with "Hx").
    rel_vals; eauto.
  Qed.

  Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
  Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
  Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
  Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
  Proof. solve_inG. Qed.

  Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
  Definition shot γ `{oneshotG Σ} := own γ (Cinr (to_agree ())).
  Lemma new_pending `{oneshotG Σ} : (|==> ∃ γ, pending γ)%I.
  Proof. by apply own_alloc. Qed.
  Lemma shoot γ `{oneshotG Σ} : pending γ ==∗ shot γ.
  Proof.
    apply own_update.
    intros n [f |]; simpl; eauto.
    destruct f; simpl; try by inversion 1.
  Qed.
  Definition shootN := nroot .@ "shootN".
  Lemma shot_not_pending γ `{oneshotG Σ} :
    shot γ -∗ pending γ -∗ False.
  Proof.
    iIntros "Hs Hp".
    iPoseProof (own_valid_2 with "Hs Hp") as "H".
    iDestruct "H" as %[].
  Qed.

  Lemma refinement2 `{oneshotG Σ} Γ :
    Γ ⊨
      let: "x" := ref #0 in
      (λ: "f", "x" <- #1;; "f" #();; !"x")
    ≤log≤
      (let: "x" := ref #1 in
       λ: "f", "f" #();; !"x")
    : TArrow (TArrow TUnit TUnit) TNat.
  Proof.
    iIntros (Δ).
    rel_alloc_l as x "Hx".
    rel_alloc_r as y "Hy".
    rel_let_l; rel_let_r.
    iApply fupd_logrel.
    iMod new_pending as (γ) "Ht". (*TODO typeclasses for this?*)
    iModIntro.
    iMod (inv_alloc shootN _ ((x ↦ᵢ #0 ∗ pending γ ∨ x ↦ᵢ #1 ∗ shot γ) ∗ y ↦ₛ #1)%I with "[Hx Ht $Hy]") as "#Hinv".
    { iNext. iLeft. iFrame. }
    iApply bin_log_related_arrow; auto.
    iIntros "!#" (f1 f2) "Hf".
    rel_let_l. rel_let_r.
    rel_store_l_atomic.
    iInv shootN as "[[[Hx Hp] | [Hx #Hs]] Hy]" "Hcl";
      iModIntro; iExists _; iFrame "Hx"; iNext; iIntros "Hx"; rel_rec_l.
    - iApply fupd_logrel'.
      iMod (shoot γ with "Hp") as "#Hs".
      iModIntro.
      iMod ("Hcl" with "[$Hy Hx]") as "_".
      { iNext. iRight. by iFrame. }
      iApply (bin_log_related_seq with "[Hf]"); auto.
      + iApply (bin_log_related_app with "Hf").
        by rel_vals.
      + rel_load_l_atomic.
        iInv shootN as "[[[Hx >Hp] | [Hx Hs']] Hy]" "Hcl".
        { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
        iModIntro. iExists _; iFrame. iNext.
        iIntros "Hx".
        rel_load_r.
        iMod ("Hcl" with "[-]").
        { iNext. iFrame. iRight; by iFrame. }
        rel_vals; eauto.
    - iMod ("Hcl" with "[$Hy Hx]") as "_".
      { iNext. iRight. by iFrame. }
      iApply (bin_log_related_seq with "[Hf]"); auto.
      + iApply (bin_log_related_app with "Hf").
        by rel_vals.
      + rel_load_l_atomic.
        iInv shootN as "[[[Hx >Hp] | [Hx Hs']] Hy]" "Hcl".
        { iExFalso. iApply (shot_not_pending with "Hs Hp"). }
        iModIntro. iExists _; iFrame. iNext.
        iIntros "Hx".
        rel_load_r.
        iMod ("Hcl" with "[-]").
        { iNext. iFrame. iRight; by iFrame. }
        rel_vals; eauto.
  Qed.

  Definition i3 x x' b b' : iProp Σ :=
    ((∃ (n : nat), x ↦ᵢ #n ∗ x' ↦ₛ #n ∗
                 b ↦ᵢ #true ∗ b' ↦ₛ #true)
               ∨ (b ↦ᵢ #false ∗ b' ↦ₛ #false))%I.
  Definition i3n := nroot .@ "i3".
  Lemma refinement3 Γ :
    Γ ⊨
      let: "b" := ref #true in
      let: "x" := ref #0 in
      (λ: "f", if: CAS "b" #true #false
               then "f" #();; "x" <- !"x" + #1 ;; "b" <- #true
               else #())
    ≤log≤
      (let: "b" := ref #true in
      let: "x" := ref #0 in
      (λ: "f", if: CAS "b" #true #false
               then let: "n" := !"x" in
                    "f" #();; "x" <- "n" + #1 ;; "b" <- #true
               else #()))
    : TArrow (TArrow TUnit TUnit) TUnit.
  Proof.
    iIntros (Δ).
    rel_alloc_l as b "Hb".
    rel_let_l.
    rel_alloc_l as x "Hx".
    rel_let_l.
    rel_alloc_r as b' "Hb'".
    rel_let_r.
    rel_alloc_r as x' "Hx'".
    rel_let_r.
    iMod (inv_alloc i3n _ (i3 x x' b b') with "[-]") as "#Hinv".
    { iNext. unfold i3.
      iLeft. iExists 0. iFrame. }
    iApply bin_log_related_arrow; eauto.
    iAlways. iIntros (f f') "Hf".
    rel_let_l.
    rel_let_r.
    rel_cas_l_atomic.
    iInv i3n as ">Hbb" "Hcl".
    rewrite {2}/i3.
    iDestruct "Hbb" as "[Hbb | (Hb & Hb')]"; last first.
    { iModIntro; iExists _; iFrame.
      iSplitL; last by iIntros (?); congruence.
      iIntros (?); iNext; iIntros "Hb".
      rel_cas_fail_r; rel_if_r; rel_if_l.
      iMod ("Hcl" with "[-]").
      { iNext. iRight. iFrame. }
      rel_vals; eauto.
    }
    { iDestruct "Hbb" as (n) "(Hx & Hx' & Hb & Hb')".
      iModIntro. iExists _; iFrame.
      iSplitR; first by iIntros (?); congruence.
      iIntros (?); iNext; iIntros "Hb".
      rel_cas_suc_r; rel_if_r; rel_if_l.
      rel_load_r. rel_let_r.
      iMod ("Hcl" with "[Hb Hb']") as "_".
      { iNext. iRight. iFrame. }
      iApply (bin_log_related_seq with "[Hf]"); auto.
      { iApply (bin_log_related_app with "Hf").
        iApply bin_log_related_unit. }
      rel_load_l.
      rel_op_l. rel_op_r.
      rel_store_l. rel_store_r.
      rel_seq_l. rel_seq_r.
      rel_store_l_atomic.
      iInv i3n as ">Hi3" "Hcl".
      iDestruct "Hi3" as "[Hi3 | [Hb Hb']]".
      { iDestruct "Hi3" as (m) "(Hx1 & Hx1' & Hb & Hb')".
        iModIntro. iExists _; iFrame; iNext. iIntros "Hb".
        iDestruct (mapsto_valid_2 x with "Hx Hx1") as %Hfoo.
        cbv in Hfoo. by exfalso. }
      iModIntro; iExists _; iFrame; iNext; iIntros "Hb".
      rel_store_r.
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iLeft. iExists _. iFrame. }
      rel_vals; eauto. }
  Qed.

  Definition bot : val := rec: "bot" <> := "bot" #().
  Lemma bot_l ϕ Δ Γ E K t τ :
    (ϕ -∗ {E,E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ) -∗
    {E,E;Δ;Γ} ⊨ fill K (bot #()) ≤log≤ t : τ.
  Proof.
    iIntros "Hlog".
    iLöb as "IH".
    rel_rec_l.
    unlock bot; simpl_subst/=.
    iApply ("IH" with "Hlog").
  Qed.

  (* /Sort of/ a well-bracketedness example.
     Without locking in the first expression, the callback can reenter
     the body in a forked thread to change the value of x
  *)
  Lemma refinement4 Γ `{!lockG Σ}:
    Γ ⊨
      (let: "x" := ref #1 in
       let: "l" := newlock #() in
       λ: "f", acquire "l";;
               "x" <- #0;; "f" #();;
               "x" <- #1;; "f" #();;
               let: "v" := !"x" in
               release "l";; "v")
    ≤log≤
      (let: "x" := ref #0 in
       λ: "f", "f" #();; "x" <- #1;; "f" #();; !"x")
    : TArrow (TArrow TUnit TUnit) TNat.
  Proof.
    iIntros (Δ).
    rel_alloc_l as x "Hx".
    rel_alloc_r as y "Hy".
    rel_let_l; rel_let_r.
    pose (N:=logrelN.@"lock").
    rel_apply_l (bin_log_related_newlock_l N (∃ (n m : nat), x ↦ᵢ #n ∗ y ↦ₛ #m)%I with "[Hx Hy]").
    { iExists _, _. iFrame. }
    iIntros (l γ) "#Hl".
    rel_let_l.
    iApply bin_log_related_arrow_val; auto.
    iIntros "!#" (f1 f2) "#Hf".
    rel_let_l. rel_let_r.
    rel_apply_l (bin_log_related_acquire_l N _ l with "Hl"); auto.
    iIntros "Hlocked". iDestruct 1 as (n m) "[Hx Hy]".
    rel_seq_l.
    rel_store_l. rel_seq_l.
    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit with "[Hf]"); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hf]").
      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
      iApply bin_log_related_unit. }
    rel_store_l. rel_seq_l.
    rel_store_r. rel_seq_r.
    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit with "[Hf]"); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hf]").
      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
      iApply bin_log_related_unit. }
    rel_load_l.
    rel_let_l.
    rel_load_r.
    rel_apply_l (bin_log_related_release_l N _ l γ with "Hl Hlocked [Hx Hy]"); eauto.
    { iExists _,_. iFrame. }
    rel_seq_l.
    rel_vals; eauto.
  Qed.

  (* "Single return" example *)
  Lemma refinement5 Γ :
    Γ ⊨
      (λ: "f", let: "x" := ref #0 in
               let: "y" := ref #0 in
               "f" #();;
               "x" <- !"y";;
               "y" <- #1;;
               !"x")
    ≤log≤
      (λ: "f", let: "x" := ref #0 in
               let: "y" := ref #0 in
               "f" #();;
               "x" <- !"y";;
               "y" <- #2;;
               !"x")
    : TArrow (TArrow TUnit TUnit) TNat.
  Proof.
    iIntros (Δ).
    iApply bin_log_related_arrow; eauto.
    iAlways.
    iIntros (f1 f2) "Hf".
    rel_let_l. rel_let_r.
    rel_alloc_l as x "Hx". rel_let_l.
    rel_alloc_l as y "Hy". rel_let_l.
    rel_alloc_r as x' "Hx'". rel_let_r.
    rel_alloc_r as y' "Hy'". rel_let_r.
    iApply (bin_log_related_seq with "[Hf]"); eauto.
    { iApply (bin_log_related_app with "Hf").
      iApply bin_log_related_unit. }
    rel_load_l. rel_load_r.
    rel_store_l. rel_store_r.
    rel_let_l. rel_let_r.
    rel_store_l. rel_store_r.
    rel_let_l. rel_let_r.
    rel_load_l. rel_load_r.
    iApply bin_log_related_nat.
  Qed.

  (** Higher-order profiling *)
  Definition τg := TArrow TUnit TUnit.
  Definition τf := TArrow τg TUnit.
  Definition p : val := λ: "g", let: "c" := ref #0 in
                                (λ: <>, FG_increment "c" #();; "g" #(), λ: <>, !"c").
  (** The idea for the invariant is that we have to states:
       a) c1 = n, c2 = n
       b) c1 = n+1, c2 = n
      We start in state (a) and can only transition to the state (b) by giving away an exclusive token.
      But once we have transitioned to (b), we remain there forever.
      To that extent we use to resources algebras two model two of those conditions, and we tie it all together in the invariant.
  *)
  Definition i6 `{oneshotG Σ} `{inG Σ (exclR unitR)} (c1 c2 : loc) γ γ' :=
    (∃ (n : nat),
     (c1 ↦ᵢ #n ∗ c2 ↦ₛ #n ∗ pending γ)
   ∨ (c1 ↦ᵢ #(S n) ∗ c2 ↦ₛ #n ∗ shot γ ∗ own γ' (Excl ())))%I.
  Lemma profiled_g `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
    inv shootN (i6 c1 c2 γ γ') -∗
    ⟦ τg ⟧ Δ (g1, g2) -∗
    {⊤,⊤;Δ;Γ} ⊨
      (FG_increment #c1 #() ;; g1 #())
    ≤log≤
      (FG_increment #c2 #() ;; g2 #()) : TUnit.
  Proof.
    iIntros "#Hinv #Hg".
    iApply (bin_log_related_seq); auto; last first.
    { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit).
      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
      iApply bin_log_related_unit. }
    rel_rec_l.
    rel_apply_l (bin_log_FG_increment_logatomic _
      (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I True%I); first done.
    iAlways.
    iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht)]" "Hcl";
      iModIntro; iExists _; iFrame.
    - iSplitL "Hc2 Ht".
      { iLeft. iFrame. }
      iSplit.
      { iDestruct 1 as (m) "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
        iApply ("Hcl" with "[-]"); iNext.
        + iExists m. iLeft. iFrame.
        + iExists (m-1). iRight.
          rewrite minus_Sn_m // /= -minus_n_O.
          iFrame. }
      { iIntros (m) "[Hc1 Hc] _".
        iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
        - unlock FG_increment. simpl.
          rel_rec_r. rel_rec_r.
          rel_load_r. rel_rec_r.
          rel_op_r.
          rel_cas_suc_r.
          rel_if_r.
          iMod ("Hcl" with "[-]") as "_".
          { iNext. iExists (S m). iFrame. iLeft; iFrame. }
          iApply bin_log_related_unit.
        - unlock FG_increment. simpl.
          rel_rec_r. rel_rec_r.
          rel_load_r. rel_rec_r.
          rel_op_r.
          rel_cas_suc_r.
          rel_if_r.
          iMod ("Hcl" with "[-]") as "_".
          { iNext. iExists m.
            rewrite minus_Sn_m // /= -minus_n_O.
            iFrame. iRight; iFrame. }
            iApply bin_log_related_unit. }
    - iSplitL "Hc2 Ht".
      { rewrite /= -minus_n_O. iRight. iFrame.
        iDestruct "Ht" as "[$ $]".
        iPureIntro. omega. }
      iSplit.
      { iDestruct 1 as (m) "[Hc1 [(Hc2 & Ht) | (Hc2 & Ht & Ht' & %)]]";
        iApply ("Hcl" with "[-]"); iNext.
        + iExists m. iLeft. iFrame.
        + iExists (m-1). iRight.
          rewrite minus_Sn_m // /= -minus_n_O.
          iFrame. }
      { iIntros (m) "[Hc1 Hc] _".
        iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
        - unlock FG_increment. simpl.
          rel_rec_r. rel_rec_r.
          rel_load_r. rel_rec_r.
          rel_op_r.
          rel_cas_suc_r.
          rel_if_r.
          iMod ("Hcl" with "[-]") as "_".
          { iNext. iExists (S m). iFrame. iLeft; iFrame. }
          iApply bin_log_related_unit.
        - unlock FG_increment. simpl.
          rel_rec_r. rel_rec_r.
          rel_load_r. rel_rec_r.
          rel_op_r.
          rel_cas_suc_r.
          rel_if_r.
          iMod ("Hcl" with "[-]") as "_".
          { iNext. iExists m.
            rewrite minus_Sn_m // /= -minus_n_O.
            iFrame. iRight; iFrame. }
            iApply bin_log_related_unit. }
  Qed.

  Lemma profiled_g' `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
    inv shootN (i6 c1 c2 γ γ') -∗
    ⟦ τg ⟧ Δ (g1, g2) -∗
    {⊤,⊤;Δ;Γ} ⊨
      (λ: <>, FG_increment #c1 #() ;; g1 #())
    ≤log≤
      (λ: <>, FG_increment #c2 #() ;; g2 #()) : τg.
  Proof.
    iIntros "#Hinv #Hg".
    iApply bin_log_related_arrow_val; auto.
    iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
    rel_seq_l. rel_seq_r.
    iApply profiled_g; eauto.
  Qed.

  Lemma close_i6 c1 c2 γ γ' `{oneshotG Σ} `{inG Σ (exclR unitR)} :
    ((∃ n : nat, c1 ↦ᵢ #n
     ∗ (c2 ↦ₛ #n ∗ pending γ
       ∨ c2 ↦ₛ #(n - 1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))
     -∗ i6 c1 c2 γ γ')%I.
  Proof.
    iDestruct 1 as (m) "[Hc1 Hc2]".
    iDestruct "Hc2" as "[[Hc2 Hp] | (Hc2 & Hs & Ht & %)]";
      [iExists m; iLeft | iExists (m - 1); iRight]; iFrame.
    rewrite minus_Sn_m // /= -minus_n_O; done.
  Qed.

  Lemma refinement6_helper Δ Γ f'1 f'2 g1 g2 c1 c2 γ γ' m `{oneshotG Σ} `{inG Σ (exclR unitR)} :
    inv shootN (i6 c1 c2 γ γ') -∗
    ⟦ τg ⟧ Δ (g1, g2) -∗
    ⟦ τf ⟧ Δ (f'1, f'2) -∗
    (▷ i6 c1 c2 γ γ' ={⊤ ∖ ↑shootN,⊤}=∗ True) -∗
    c1 ↦ᵢ #(S m) -∗
    (c2 ↦ₛ #m ∗ pending γ
      ∨ c2 ↦ₛ #(m - 1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ m⌝) -∗
    own γ' (Excl ()) -∗
    {⊤ ∖ ↑shootN,⊤;Δ;Γ} ⊨
      (g1 #() ;; f'1 (λ: <>, (FG_increment #c1) #() ;; g1 #()) ;; #() ;; ! #c1)
    ≤log≤
      (g2 #() ;;
       f'2 (λ: <>, (FG_increment #c2) #() ;; g2 #()) ;; (#() ;; ! #c2) + #1) : TNat.
  Proof.
    iIntros "#Hinv #Hg #Hf Hcl Hc1 Hc2 Ht".
    iDestruct "Hc2" as "[(Hc2 & Hp) | (Hc2 & Hs & Ht'2 & %)]"; last first.
    { iDestruct (own_valid_2 with "Ht Ht'2") as %Hfoo.
      inversion Hfoo. }
    iApply fupd_logrel.
    iMod (shoot γ with "Hp") as "#Hs".
    iMod ("Hcl" with "[-]") as "_".
    { iNext. iExists m. iRight. iFrame. done. }
    iModIntro.
    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]").
      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
      iApply bin_log_related_unit. }
    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]").
      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
        by iApply profiled_g'. }
    rel_seq_l. rel_seq_r.
    rel_load_l_atomic. clear m.
    iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht')]" "Hcl";
      iModIntro; iExists _; iFrame.
    { iExFalso. by iApply shot_not_pending. }
    iNext. iIntros "Hc1".
    rel_load_r. rel_op_r.
    iMod ("Hcl" with "[-]") as "_".
    { iNext. iExists m. iRight. iFrame. }
    rewrite Nat.add_1_r.
    iApply bin_log_related_nat.
  Qed.

  Lemma refinement6 `{oneshotG Σ} `{inG Σ (exclR unitR)} Γ :
    Γ ⊨
      (λ: "f" "g" "f'",
       let: "pg" := p "g" in
       let: "g'" := Fst "pg" in
       let: "g''" := Snd "pg" in
       "f" "g'";; "g'" #();; "f'" "g'";; "g''" #())
    ≤log≤
      (λ: "f" "g" "f'",
       let: "pg" := p "g" in
       let: "g'" := Fst "pg" in
       let: "g''" := Snd "pg" in
       "f" "g'";; "g" #();; "f'" "g'";; "g''" #() + #1)
    : TArrow τf (TArrow τg (TArrow τf TNat)).
  Proof.
    iIntros (Δ).
    iApply bin_log_related_arrow_val; auto.
    iIntros "!#" (f1 f2) "#Hf". fold interp.
    rel_let_l. rel_let_r.
    iApply bin_log_related_arrow_val; auto.
    iIntros "!#" (g1 g2)"#Hg". fold interp.
    rel_let_l. rel_let_r.
    iApply bin_log_related_arrow_val; auto.
    iIntros "!#" (f'1 f'2) "#Hf'". fold interp.
    rel_let_l. rel_let_r.
    unlock p. simpl.
    rel_let_l. rel_let_r.
    rel_alloc_l as c1 "Hc1".
    rel_alloc_r as c2 "Hc2".
    iApply fupd_logrel.
    iMod new_pending as (γ) "Ht". (*TODO typeclasses for this?*)
    iMod (own_alloc (Excl ())) as (γ') "Ht'"; first done.
    iModIntro.
    iMod (inv_alloc shootN _ (i6 c1 c2 γ γ') with "[Hc1 Hc2 Ht]") as "#Hinv".
    { iNext. iExists 0. iLeft. iFrame. }
    rel_let_l. rel_let_r.
    rel_let_l. rel_let_r.
    rel_proj_l. rel_proj_r.
    rel_let_l. rel_let_r.
    rel_proj_l. rel_proj_r.
    rel_let_l. rel_let_r.
    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
    { iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]").
      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
      iApply profiled_g'; eauto. }
    rel_seq_l.
    rel_bind_l (FG_increment _). rel_rec_l.
    rel_apply_l (bin_log_FG_increment_logatomic _
      (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I with "Ht'").
    iAlways.
    iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
      iModIntro; iExists _; iFrame; last first.
    { iSplitL "Hc2 Ht Ht'2".
      { iRight. simpl. rewrite -minus_n_O. iFrame. iPureIntro. omega. }
      iSplit.
      - iIntros. iApply "Hcl". by iApply close_i6.
      - iIntros (m) "[Hc1 Hc2] Ht".
        rel_seq_l.
        iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
    }
    { iSplitL "Hc2 Ht".
      { iLeft. by iFrame. }
      iSplit.
      - iIntros. iApply "Hcl". by iApply close_i6.
      - iIntros (m) "[Hc1 Hc2] Ht".
        rel_seq_l.
        iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
    }
  Qed.

End refinement.