add one_shot_once example

tests/one_shot_once.ref

+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  one_shotG0 : one_shotG Σ
+  Φ : val → iProp Σ
+  N : namespace
+  l : loc
+  γ : gname
+  ============================
+  "HN" : inv N (one_shot_inv γ l)
+  --------------------------------------□
+  "Hl" : l ↦ InjLV #()
+  _ : own γ (Pending (1 / 2))
+  --------------------------------------∗
+  one_shot_inv γ l
+  ∗ (⌜InjLV #() = InjLV #()⌝
+     ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  one_shotG0 : one_shotG Σ
+  Φ : val → iProp Σ
+  N : namespace
+  l : loc
+  γ : gname
+  m, m' : Z
+  ============================
+  "HN" : inv N (one_shot_inv γ l)
+  "Hγ'" : own γ (Shot m)
+  --------------------------------------□
+  "Hl" : l ↦ InjRV #m'
+  "Hγ" : own γ (Shot m')
+  --------------------------------------∗
+  |={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
+               ∗ WP InjRV #m = InjRV #m' {{ v, ⌜v = #true⌝ ∧ ▷ True }}
+  

tests/one_shot_once.v

+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
+From iris.algebra Require Import frac agree csum.
+From iris.heap_lang Require Import assert proofmode notation adequacy.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang.lib Require Import par.
+Set Default Proof Using "Type".
+
+Definition one_shot_example : val := λ: <>,
+  let: "x" := ref NONE in (
+  (* set *) (λ: "n",
+    assert: CAS "x" NONE (SOME "n")),
+  (* check  *) (λ: <>,
+    let: "y" := !"x" in λ: <>,
+    match: "y" with
+      NONE => #()
+    | SOME <> => assert: "y" = !"x"
+    end)).
+
+Definition one_shotR := csumR fracR (agreeR ZO).
+Definition Pending (q : Qp) : one_shotR := Cinl q.
+Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
+
+Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
+Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
+Proof. solve_inG. Qed.
+
+Section proof.
+Local Set Default Proof Using "Type*".
+Context `{!heapG Σ, !one_shotG Σ}.
+
+Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
+  (l ↦ NONEV ∗ own γ (Pending (1/2)%Qp) ∨
+   ∃ n : Z, l ↦ SOMEV #n ∗ own γ (Shot n))%I.
+
+Lemma pending_split γ q :
+  own γ (Pending q) ⊣⊢ own γ (Pending (q/2)) ∗ own γ (Pending (q/2)).
+Proof.
+  rewrite /Pending. rewrite -own_op Cinl_op. rewrite frac_op' Qp_div_2 //.
+Qed.
+
+Lemma pending_shoot γ n :
+  own γ (Pending 1%Qp) ==∗ own γ (Shot n).
+Proof.
+  iIntros "Hγ". iMod (own_update with "Hγ") as "$"; last done.
+  by apply cmra_update_exclusive with (y:=Shot n).
+Qed.
+
+Lemma wp_one_shot (Φ : val → iProp Σ) :
+  (∀ (f1 f2 : val) (T : iProp Σ), T ∗
+    □ (∀ n : Z, T -∗ WP f1 #n {{ w, True }}) ∗
+    □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+  ⊢ WP one_shot_example #() {{ Φ }}.
+Proof.
+  iIntros "Hf /=". pose proof (nroot .@ "N") as N.
+  rewrite -wp_fupd. wp_lam. wp_alloc l as "Hl".
+  iMod (own_alloc (Pending 1%Qp)) as (γ) "Hγ"; first done.
+  iDestruct (pending_split with "Hγ") as "[Hγ1 Hγ2]".
+  iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ2]") as "#HN".
+  { iNext. iLeft. by iFrame. }
+  wp_pures. iModIntro. iApply ("Hf" $! _ _ (own γ (Pending (1/2)%Qp))).
+  iSplitL; first done. iSplit.
+  - iIntros (n) "!# Hγ1". wp_pures.
+    iApply wp_assert. wp_pures. wp_bind (CmpXchg _ _ _).
+    iInv N as ">[[Hl Hγ2]|H]"; last iDestruct "H" as (m) "[Hl Hγ']".
+    + iDestruct (pending_split with "[$Hγ1 $Hγ2]") as "Hγ".
+      iMod (pending_shoot _ n with "Hγ") as "Hγ".
+      wp_cmpxchg_suc. iModIntro. iSplitL; last (wp_pures; by eauto).
+      iNext; iRight; iExists n; by iFrame.
+    + by iDestruct (own_valid_2 with "Hγ1 Hγ'") as %?.
+  - iIntros "!# /=". wp_lam. wp_bind (! _)%E.
+    iInv N as ">Hγ".
+    iAssert (∃ v, l ↦ v ∗ (⌜v = NONEV⌝ ∗ own γ (Pending (1/2)%Qp) ∨
+       ∃ n : Z, ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hγ]" as "Hv".
+    { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
+      + iExists NONEV. iFrame. eauto.
+      + iExists (SOMEV #m). iFrame. eauto. }
+    iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
+    iAssert (one_shot_inv γ l ∗ (⌜v = NONEV⌝ ∨ ∃ n : Z,
+      ⌜v = SOMEV #n⌝ ∗ own γ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
+    { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
+      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
+      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
+    iSplitL "Hinv"; first by eauto.
+    iModIntro. wp_pures. iIntros "!#". wp_lam.
+    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
+      subst; wp_match; [done|].
+    wp_pures. iApply wp_assert. wp_bind (! _)%E.
+    iInv N as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]".
+    { by iDestruct (own_valid_2 with "Hγ Hγ'") as %?. }
+    wp_load. Show.
+    iDestruct (own_valid_2 with "Hγ Hγ'") as %?%agree_op_invL'; subst.
+    iModIntro. iSplitL "Hl".
+    { iNext; iRight; by eauto. }
+    wp_pures. by case_bool_decide.
+Qed.
+
+Lemma ht_one_shot (Φ : val → iProp Σ) :
+  {{ True }} one_shot_example #()
+    {{ ff, ∃ T, T ∗
+      (∀ n : Z, {{ T }} Fst ff #n {{ _, True }}) ∗
+      {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
+    }}.
+Proof.
+  iIntros "!# _". iApply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
+  iExists T. iFrame "HT". iSplit.
+  - iIntros (n) "!# HT". wp_apply "Hf1". done.
+  - iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
+Qed.
+End proof.
+
+(* Have a client with a closed proof. *)
+Definition client : expr :=
+  let: "ff" := one_shot_example #() in
+  (Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).
+
+Section client.
+  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+
+  Lemma client_safe : WP client {{ _, True }}%I.
+  Proof using Type*.
+    rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
+    wp_let. wp_apply (wp_par with "[HT]").
+    - wp_apply "Hf1". done.
+    - wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2".
+      iIntros (check) "Hcheck". wp_pures. iApply "Hcheck".
+    - auto.
+  Qed.
+End client.
+
+(** Put together all library functors. *)
+Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
+(** This lemma implicitly shows that these functors are enough to meet
+all library assumptions. *)
+Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
+Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.