Library leuvenss.theories.shared_memory

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 Σ}.

  Definition inv_name := nroot .@ "inv".

  Lemma prog_spec : {{{ True }}} prog {{{ n, RET #n; ⌜0 ≤ n⌝%Z }}}.
  Proof.
    unfold prog.
    iIntros (Φ) "_ HΦ".
    wp_alloc c as "Hc".
    wp_pures.
    iMod (inv_alloc inv_name _ (∃ n : Z, c ↦ #n ∗ ⌜0 ≤ n⌝%Z)%I with "[Hc]")
      as "#inv".
    { auto. }
    wp_apply (wp_par (λ _, True)%I (λ _, True)%I with "[] []").
    { iInv inv_name as (n) ">[Hc %]".
      wp_faa.
      iModIntro; iSplitL; last trivial.
      iNext; iExists (n+1)%Z; iFrame; eauto with lia. }
    { iInv inv_name as (n) ">[Hc %]".
      wp_faa.
      iModIntro; iSplitL; last trivial.
      iNext; iExists (n+2)%Z; iFrame; eauto with lia. }
    iIntros (v1 v2) "[_ _]".
    iNext.
    wp_pures.
    iInv inv_name as (n) ">[Hc %]".
    wp_load.
    iModIntro; iSplitR "HΦ".
    { iNext; eauto. }
    iApply "HΦ"; done.
  Qed.

End proof.

Lemma prog_adequacy :
  adequate NotStuck prog {|heap := ∅; used_proph_id := ∅ |} (λ v _, ∃ n : Z, v = #n ∧ (0 ≤ n)%Z).
Proof.
  apply (heap_adequacy #[heapΣ; spawnΣ]).
  iIntros (?) "Hinv".
  iApply prog_spec; first done.
  iNext; iIntros (? ?); iExists _; done.
Qed.