iris/tests/one_shot_once.ref at master · TyGuS/iris · GitHub

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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
1 goal

  Σ : gFunctors
  heapG0 : heapG Σ
  one_shotG0 : one_shotG Σ
  Φ : val → iProp Σ
  N : namespace
  l : loc
  γ : gname
  ============================
  "HN" : inv N (one_shot_inv γ l)
  --------------------------------------□
  "Hl" : l ↦ InjLV #()
  _ : own γ (Pending (1 / 2))
  --------------------------------------∗
  one_shot_inv γ l
  ∗ (⌜InjLV #() = InjLV #()⌝
     ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))

1 goal

  Σ : gFunctors
  heapG0 : heapG Σ
  one_shotG0 : one_shotG Σ
  Φ : val → iProp Σ
  N : namespace
  l : loc
  γ : gname
  m, m' : Z
  ============================
  "HN" : inv N (one_shot_inv γ l)
  "Hγ'" : own γ (Shot m)
  --------------------------------------□
  "Hl" : l ↦ InjRV #m'
  "Hγ" : own γ (Shot m')
  --------------------------------------∗
  |={⊤ ∖ ↑N}=> ▷ one_shot_inv γ l
               ∗ WP let: "y'" := InjRV #m' in
                    match: InjRV #m with
                      InjL <> => #()
                    | InjR <> => assert: InjRV #m = "y'"
                    end {{ _, True }}