one_shot.v 4.19 KB
Newer Older
1 2
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
3
From iris.algebra Require Import excl dec_agree csum.
4
From iris.heap_lang Require Import assert proofmode notation.
5
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
6 7

Definition one_shot_example : val := λ: <>,
8
  let: "x" := ref NONE in (
Ralf Jung's avatar
Ralf Jung committed
9
  (* tryset *) (λ: "n",
10
    CAS "x" NONE (SOME "n")),
Ralf Jung's avatar
Ralf Jung committed
11
  (* check  *) (λ: <>,
12 13
    let: "y" := !"x" in λ: <>,
    match: "y" with
14 15
      NONE => #()
    | SOME "n" =>
16
       match: !"x" with
17 18
         NONE => assert: #false
       | SOME "m" => assert: "n" = "m"
Ralf Jung's avatar
Ralf Jung committed
19 20 21
       end
    end)).

22 23 24 25
Definition one_shotR := csumR (exclR unitC) (dec_agreeR Z).
Definition Pending : one_shotR := (Cinl (Excl ()) : one_shotR).
Definition Shot (n : Z) : one_shotR := (Cinr (DecAgree n) : one_shotR).

26 27 28 29
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor (constRF one_shotR)].
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ  one_shotG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
30

Ralf Jung's avatar
Ralf Jung committed
31
Section proof.
32
Context `{!heapG Σ, !one_shotG Σ} (N : namespace) (HN : heapN  N).
Ralf Jung's avatar
Ralf Jung committed
33

34
Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
35
  (l  NONEV  own γ Pending   n : Z, l  SOMEV #n  own γ (Shot n))%I.
Ralf Jung's avatar
Ralf Jung committed
36

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

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

Global Opaque one_shot_example.