one_shot.ref 1.09 KB
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 28 29 30 31 32 33 34 35 36 37
1 subgoal
  
  Σ : 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
  --------------------------------------∗
  one_shot_inv γ l
  ∗ (⌜InjLV #() = InjLV #()⌝
     ∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
  
1 subgoal
  
  Σ : 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
38
               ∗ WP match: InjRV #m' with
39 40 41 42
                      InjL <> => assert: #false
                    | InjR "m" => assert: #m = "m"
                    end {{ _, True }}
  
Ralf Jung's avatar
Ralf Jung committed
43
Closed under the global context