branching_proofs.v 1.34 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic Require Import invariants.
From osiris.typing Require Import side stype.
From osiris.encodings Require Import branching.
From osiris.examples Require Import branching_examples.

Section BranchingExampleProofs.
  Context `{!heapG Σ} (N : namespace).
  Context `{!logrelG val Σ}.

  Lemma branch_proof b :
    {{{ True }}}
      branch_example b
    {{{ v, RET v; match b with
17
18
                  | Left => v = #5
                  | Right => v = #()
19
20
21
22
                  end }}}.
  Proof.
    iIntros (Φ H) "HΦ".
    rewrite /branch_example.
23
    wp_apply (new_chan_st_spec N
24
      ((<?> v @ v = 5, TEnd) <+> (TEnd)))=> //;
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
    iIntros (c γ) "[Hstl Hstr]".
    wp_apply (select_st_spec with "Hstl");
    iIntros "Hstl".
    wp_pures.
    wp_apply (wp_fork with "[Hstr]").
    - iNext.
      wp_apply (branch_st_spec N with "Hstr");
      iIntros "Hstr".
      + wp_apply (send_st_spec N Z with "[$Hstr //]");
        iIntros "Hstr". done.
      + wp_pures. done.
    - destruct b.
      + wp_apply (recv_st_spec N Z with "Hstl");
        iIntros (v) "[Hstl HP]".
        iDestruct "HP" as %->.
        by iApply "HΦ".
      + wp_pures. by iApply "HΦ".
  Qed.

End BranchingExampleProofs.