part3.v 987 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import par.
Local Definition N := nroot .@ "example".

(* PART 3: Basic concurrency *)
Definition coin_flip : val := λ: <>,
  let: "l" := ref #0 in
  (("l" <- #0) ||| ("l" <- #1));;
  !"l".

Lemma test2_spec `{heapG Σ, spawnG Σ} :
Robbert Krebbers's avatar
Robbert Krebbers committed
12
  {{{ True }}} coin_flip #() {{{ n, RET #n;  n = 0%Z  n = 1%Z  }}}.
13
Proof.
14
  iIntros (Φ) "_ Post". wp_lam. wp_alloc l as "Hl". wp_let.
15
16
17
18
19
20
21
22
23
24
25
26
27
  iMod (inv_alloc N _
    ( x : Z, l  #x   x = 0  x = 1 )%I with "[Hl]") as "#?".
  { eauto 10. }
  wp_apply (wp_par (λ _, True)%I (λ _, True)%I).
  - iInv N as (n) ">[Hl _]" "Hclose".
    wp_store. iMod ("Hclose" with "[Hl]"); eauto 10.
  - iInv N as (n) ">[Hl _]" "Hclose".
    wp_store. iMod ("Hclose" with "[Hl]"); eauto 10.
  - iIntros (v1 v2) "_ !> /=". wp_seq.
    iInv N as (n) ">[Hl %]" "Hclose".
    wp_load. iMod ("Hclose" with "[Hl]") as "_"; first eauto 10.
    iApply "Post"; auto.
Qed.