one_shot.v 4.02 KB
Newer Older
1
From iris.algebra Require Import dec_agree csum.
2
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.
5 6 7 8 9
Import uPred.

Definition one_shot_example : val := λ: <>,
  let: "x" := ref (InjL #0) in (
  (* tryset *) (λ: "n",
10
    CAS "x" (InjL #0) (InjR "n")),
11
  (* check  *) (λ: <>,
12 13
    let: "y" := !"x" in λ: <>,
    match: "y" with
14 15
      InjL <> => #()
    | InjR "n" =>
16
       match: !"x" with
17 18
         InjL <> => assert: #false
       | InjR "m" => assert: "n" = "m"
19 20
       end
    end)).
21
Global Opaque one_shot_example.
22 23

Class one_shotG Σ :=
24
  one_shot_inG :> inG heap_lang Σ (csumR (exclR unitC)(dec_agreeR Z)).
25
Definition one_shotGF : gFunctorList :=
26
  [GFunctor (constRF (csumR (exclR unitC)(dec_agreeR Z)))].
27
Instance inGF_one_shotG Σ : inGFs heap_lang Σ one_shotGF  one_shotG Σ.
28 29 30
Proof. intros [? _]; apply: inGF_inG. Qed.

Notation Pending := (Cinl (Excl ())).
31 32 33 34 35 36 37

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 :=
38 39
  (l  InjLV #0  own γ Pending 
   n : Z, l  InjRV #n  own γ (Cinr (DecAgree n)))%I.
40 41

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

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