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 dec_agree frac.
From iris_atomic Require Import atomic_pcas'.
Import uPred.

Section atomic_pair.
  Context `{!heapG Σ, !lockG Σ, !syncG Σ} (N : namespace).
  
  Definition pcas_seq : val :=
    λ: "ls" "ab",
       if: !(Fst "ls") = Fst "ab"
         then if: !(Snd "ls") = Fst "ab"
                then Fst "ls" <- Snd "ab";; Snd "ls" <- Snd "ab";; #true
                else #false
         else #false.

  Local Opaque pcas_seq.

  Definition α (x: val) : iProp Σ := (∃ a b: val, x = (a, b)%V)%I.
  
  Definition ϕ (ls: val) (xs: val) : iProp Σ :=
    (∃ (l1 l2: loc) (x1 x2: val),
       ls = (#l1, #l2)%V ★ xs = (x1, x2)%V ★ l1 ↦ x1 ★ l2 ↦ x2)%I.

  Definition β (ab: val) (xs xs': val) (v: val) : iProp Σ :=
    (■ ∃ a b x1 x2 x1' x2': val,
         ab = (a, b)%V ∧ xs = (x1, x2)%V ∧ xs' = (x1', x2')%V ∧
         ((v = #true  ∧ x1 = a ∧ x2 = a ∧ x1' = b ∧ x2' = b) ∨
          (v = #false ∧ (x1 ≠ a ∨ x2 ≠ a) ∧ xs = xs')))%I.

  Local Opaque β.
  
  Lemma pcas_seq_spec: seq_spec N pcas_seq ϕ α β ⊤.
  Proof.
    rewrite /seq_spec.
    intros Φ l.
    iIntros "!# _". wp_seq. iVsIntro. iPureIntro. clear Φ.
    iIntros (x Φ g HN) "(#Hh & Hg & #Hα & HΦ)".
    rewrite /ϕ /α.
    iDestruct "Hg" as (l1 l2 x1 x2) "(% & % & Hl1 & Hl2)".
    iDestruct "Hα" as (a b) "%".
    subst. simpl. wp_let. wp_proj. wp_load. wp_proj.
    wp_op=>[?|Hx1na].
    - subst.
      wp_if. wp_proj. wp_load. wp_proj.
      wp_op=>[?|Hx2na]. subst.
      + wp_if. wp_proj. wp_proj. wp_store. wp_proj. wp_proj. wp_store.
        iDestruct ("HΦ" $! #true (b, b)%V) as "HΦ".
        iApply ("HΦ" with "[Hl1 Hl2]").
        { iExists l1, l2, b, b. iFrame. eauto. }
        rewrite /β.
        iPureIntro. exists a, b, a, a, b, b. repeat (split; first done). left. eauto.
      + wp_if.
        iDestruct ("HΦ" $! #false (a, x2)%V) as "H".
        iApply ("H" with "[Hl1 Hl2]").
        { iExists l1, l2, a, x2. iFrame. eauto. }
        rewrite /β.
        iPureIntro. exists a, b, a, x2, a, x2. repeat (split; first done). right. eauto.
    - subst.
      wp_if.
      iDestruct ("HΦ" $! #false (x1, x2)%V) as "H".
      iApply ("H" with "[Hl1 Hl2]").
      { iExists l1, l2, x1, x2. iFrame. eauto. }
      rewrite /β.
      iPureIntro. exists a, b, x1, x2, x1, x2. repeat (split; first done). right. eauto.
  Qed.

  Lemma pcas_atomic_spec:
    heapN ⊥ N → heap_ctx ⊢ WP sync (λ: <>, (ref #0, ref #0))%V pcas_seq {{ f, ∃ γ, gHalf γ (#0, #0) ★ ∀ x, □ atomic_triple' α β ⊤ ⊤ f x γ  }}.
  Proof.
    iIntros (HN) "#Hh".
    iDestruct (atomic_spec with "[]") as "Hspec"=>//.
    - apply pcas_seq_spec.
    - rewrite /cons_spec.
      iIntros (Φ _) "[#Hh HΦ]".
      wp_seq.
      wp_alloc l1 as "Hl1".
      wp_alloc l2 as "Hl2".
      iVs (own_alloc (gFullR (#0, #0) ⋅ gHalfR (#0, #0))) as (γ) "[HgFull HgHalf]".
      { rewrite /gHalfR /gFullR. split; first by simpl. simpl. by rewrite dec_agree_idemp. }
      rewrite /ϕ.
      iSpecialize ("HΦ" $! (#l1, #l2)%V γ).
      rewrite /gFull /gHalf.
      iVsIntro.
      iAssert ((∃ (l0 l3 : loc) (x1 x2 : val),
            (#l1, #l2)%V = (#l0, #l3)%V
            ★ (#0, #0)%V = (x1, x2)%V ★ l0 ↦ x1 ★ l3 ↦ x2))%I with "[Hl1 Hl2]" as "H'".
      { iExists l1, l2, #0, #0. iFrame. eauto. }
      iApply ("HΦ" with "H' HgFull HgHalf").
   Qed.
End atomic_pair.