Library leuvenss.theories.shared_memory_stronger

From iris.algebra Require Import lib.frac_auth numbers.
From iris.program_logic Require Import weakestpre.
From iris.heap_lang Require Import adequacy proofmode notation.
From iris.heap_lang.lib Require Import par.

Definition prog : expr :=
  let: "c" := ref #0 in
  (par (λ: ≠, FAA "c" #1) (λ: ≠, FAA "c" #2));;
  ! "c".

Section proof.
  Context `{!heapGS Σ, !spawnG Σ, inG Σ (frac_authUR natUR)}.

  Definition inv_name := nroot .@ "inv".

  Definition Sum (γ : gname) (n : nat) : iProp Σ := own γ (●F n).
  Definition Left (γ : gname) (n : nat) : iProp Σ := own γ (◯F{1/2} n).
  Definition Right (γ : gname) (n : nat) : iProp Σ := own γ (◯F{1/2} n).

  Lemma Contr_alloc : ⊢ |==> ∃ γ, Sum γ 0 ∗ Left γ 0 ∗ Right γ 0.
  Proof.
    iMod (own_alloc (●F 0 ⋅ ◯F 0)) as (γ) "[HS [HL HR]]";
      first by apply frac_auth_valid.
    iModIntro. iExists _; iFrame.
  Qed.

  Lemma Contr_sum γ n m k :
    Sum γ n -∗ Left γ m -∗ Right γ k -∗ ⌜n = (m + k)%nat⌝.
  Proof.
    iIntros "H1 H2 H3".
    iCombine "H2" "H3" as "H23".
    iDestruct (own_valid_2 with "H1 H23") as %->%frac_auth_agree_L.
    done.
  Qed.

  Lemma Contr_incr_left γ n m k :
    Sum γ n -∗ Left γ m -∗ |==> Sum γ (n + k) ∗ Left γ (m + k).
  Proof.
    iIntros "H1 H2".
    iCombine "H1" "H2" as "H".
    iMod (own_update _ _ (●F (n + k) ⋅ ◯F{1/2} (m + k)) with "H") as "[H1 H2]".
    { apply frac_auth_update, nat_local_update; lia. }
    iFrame; done.
  Qed.

  Lemma Contr_incr_right γ n m k :
    Sum γ n -∗ Right γ m -∗ |==> Sum γ (n + k) ∗ Right γ (m + k).
  Proof.
    iIntros "H1 H2".
    iCombine "H1" "H2" as "H".
    iMod (own_update _ _ (●F (n + k) ⋅ ◯F{1/2} (m + k)) with "H") as "[H1 H2]".
    { apply frac_auth_update, nat_local_update; lia. }
    iFrame; done.
  Qed.

  Lemma prog_spec : {{{ True }}} prog {{{ n, RET #n; ⌜n = 3⌝%Z }}}.
  Proof.
    unfold prog.
    iIntros (Φ) "_ HΦ".
    wp_alloc c as "Hc".
    wp_pures.
    iMod Contr_alloc as (γ) "[HS [HL HR]]".
    iMod (inv_alloc inv_name _ (∃ n : nat, c ↦ #n ∗ Sum γ n)%I with "[Hc HS]")
      as "#inv".
    { iExists 0; iFrame. }
    wp_apply (wp_par (λ _, Left γ 1)%I (λ _, Right γ 2)%I with "[HL] [HR]").
    { iInv inv_name as (n) ">[Hc HS]".
      wp_faa.
      iMod (Contr_incr_left _ _ _ 1 with "HS HL") as "[HS HL]".
      iModIntro; iSplitR "HL"; last done.
      iNext; iExists (n+1); iFrame.
      replace ((n + 1)%nat : Z) with (n + 1)%Z by lia.
      done. }
    { iInv inv_name as (n) ">[Hc HS]".
      wp_faa.
      iMod (Contr_incr_right _ _ _ 2 with "HS HR") as "[HS HR]".
      iModIntro; iSplitR "HR"; last done.
      iNext; iExists (n+2); iFrame.
      replace ((n + 2)%nat : Z) with (n + 2)%Z by lia.
      done. }
    iIntros (v1 v2) "[HL HR]".
    iNext.
    wp_pures.
    iInv inv_name as (n) ">[Hc HS]".
    wp_load.
    iDestruct (Contr_sum with "HS HL HR") as %Hn.
    rewrite Hn; simpl in ×.
    iModIntro; iSplitR "HΦ".
    { iNext; iExists _; iFrame. }
    iApply "HΦ"; done.
  Qed.

End proof.

Lemma prog_adequacy : adequate NotStuck prog {|heap := ∅; used_proph_id := ∅ |} (λ v _, v = #3).
Proof.
  assert (∀ Σ, subG (GFunctor (frac_authUR natUR)) Σ → inG Σ (frac_authUR natUR)).
  { solve_inG. }
  apply (heap_adequacy #[heapΣ; spawnΣ; GFunctor (frac_authUR natUR)]).
  iIntros (?) "Hinv".
  iApply prog_spec; first done.
  iNext; iIntros (? ->); done.
Qed.