part3.v 983 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
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 Σ} :
  {{{ True }}} coin_flip #() {{{ n, RET #n;  n = 0  n = 1  }}}.
Proof.
  iIntros (Φ) "_ Post". wp_let. wp_alloc l as "Hl". wp_let.
  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.