one_shot.v 4.19 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2
From iris.algebra Require Import one_shot dec_agree.
From iris.program_logic Require Import hoare.
3
From iris.heap_lang Require Import assert proofmode notation.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From iris.proofmode Require Import invariants ghost_ownership.
Ralf Jung's avatar
Ralf Jung committed
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
Import uPred.

Definition one_shot_example : val := λ: <>,
  let: "x" := ref (InjL #0) in (
  (* tryset *) (λ: "n",
    CAS '"x" (InjL #0) (InjR '"n")),
  (* check  *) (λ: <>,
    let: "y" := !'"x" in λ: <>,
    match: '"y" with
      InjL <> => #()
    | InjR "n" =>
       match: !'"x" with
         InjL <> => Assert #false
       | InjR "m" => Assert ('"n" = '"m")
       end
    end)).

Class one_shotG Σ :=
  OneShotG { one_shot_inG :> inG heap_lang Σ (one_shotR (dec_agreeR Z)) }.
Definition one_shotGF : gFunctorList :=
  [GFunctor (constRF (one_shotR (dec_agreeR Z)))].
Instance inGF_one_shotG Σ : inGFs heap_lang Σ one_shotGF  one_shotG Σ.
Proof. intros [? _]; split; apply: inGF_inG. Qed.

Section proof.
Context {Σ : gFunctors} `{!heapG Σ, !one_shotG Σ}.
Context (heapN N : namespace) (HN : heapN  N).
Local Notation iProp := (iPropG heap_lang Σ).

Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
  (l  InjLV #0  own γ OneShotPending 
   n : Z, l  InjRV #n  own γ (Shot (DecAgree n)))%I.

Lemma wp_one_shot (Φ : val  iProp) :
  (heap_ctx heapN   f1 f2 : val,
40 41
    ( n : Z,  WP f1 #n {{ w, w = #true  w = #false }}) 
     WP f2 #() {{ g,  WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
Ralf Jung's avatar
Ralf Jung committed
42 43
   WP one_shot_example #() {{ Φ }}.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
  iIntros "[#? Hf] /=".
  rewrite /one_shot_example. wp_seq. wp_alloc l as "Hl". wp_let.
  iPvs (own_alloc OneShotPending) as {γ} "Hγ"; first done.
  iPvs (inv_alloc N _ (one_shot_inv γ l)) "[Hl Hγ]" as "#HN"; first done.
  { iNext. iLeft. by iSplitL "Hl". }
  iPvsIntro. iApply "Hf"; iSplit.
  - iIntros {n} "!". wp_let.
    iInv> N as "[[Hl Hγ]|H]"; last iDestruct "H" as {m} "[Hl Hγ]".
    + iApply wp_pvs. wp_cas_suc. iSplitL; [|by iLeft; iPvsIntro].
      iPvs own_update "Hγ" as "Hγ".
      { (* FIXME: canonical structures are not working *)
        by apply (one_shot_update_shoot (DecAgree n : dec_agreeR _)). }
      iPvsIntro; iRight; iExists n; by iSplitL "Hl".
    + wp_cas_fail. iSplitL. iRight; iExists m; by iSplitL "Hl". by iRight.
  - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
    iAssert ( v, l  v  ((v = InjLV #0  own γ OneShotPending) 
        n : Z, v = InjRV #n  own γ (Shot (DecAgree n))))%I as "Hv" with "-".
    { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as {m} "[Hl Hγ]".
      + iExists (InjLV #0). iFrame "Hl". iLeft; by iSplit.
      + iExists (InjRV #m). iFrame "Hl". iRight; iExists m; by iSplit. }
    iDestruct "Hv" as {v} "[Hl Hv]". wp_load.
    iAssert (one_shot_inv γ l  (v = InjLV #0   n : Z,
      v = InjRV #n  own γ (Shot (DecAgree n))))%I as "[Hl #Hv]" with "-".
    { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as {m} "[% ?]"; subst.
      + iSplit. iLeft; by iSplitL "Hl". by iLeft.
      + iSplit. iRight; iExists m; by iSplitL "Hl". iRight; iExists m; by iSplit. }
    iFrame "Hl". wp_let. iPvsIntro. iIntros "!". wp_seq.
    iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
    { wp_case. wp_seq. by iPvsIntro. }
    wp_case. wp_let. wp_focus (! _)%E.
    iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
    { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct own_valid "Hγ" as "%". }
    wp_load.
    iCombine "Hγ" "Hγ'" as "Hγ".
    iDestruct own_valid "Hγ !" as % [=->]%dec_agree_op_inv.
    iSplitL "Hl"; [iRight; iExists m; by iSplit|].
    wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=.
    iSplit. done. by iNext.
Ralf Jung's avatar
Ralf Jung committed
82 83 84 85
Qed.

Lemma hoare_one_shot (Φ : val  iProp) :
  heap_ctx heapN  {{ True }} one_shot_example #()
86 87 88
    {{ ff,
      ( n : Z, {{ True }} Fst ff #n {{ w, w = #true  w = #false }}) 
      {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
Ralf Jung's avatar
Ralf Jung committed
89 90
    }}.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92 93 94 95
  iIntros "#? ! _". iApply wp_one_shot. iSplit; first done.
  iIntros {f1 f2} "[#Hf1 #Hf2]"; iSplit.
  - iIntros {n} "! _". wp_proj. iApply "Hf1" "!".
  - iIntros "! _". wp_proj.
    iApply wp_wand_l; iFrame "Hf2". by iIntros {v} "#? ! _".
Ralf Jung's avatar
Ralf Jung committed
96 97
Qed.
End proof.