atomic.ref

1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  aheap : atomic_heap Σ
  Q : iProp Σ
  l : loc
  v : val
  ============================
  "Hl" : l ↦ v
  --------------------------------------∗
  AACC << ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
       @ ⊤ ∖ ∅, ∅
       << l ↦{q} v0, COMM Q -∗ Q >>
"non_laterable"
     : string
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  aheap : atomic_heap Σ
  P : iProp Σ
  l : loc
  ============================
  "HP" : ▷ P
  --------------------------------------∗
  AACC << ∃∃ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
       @ ⊤ ∖ ∅, ∅
       << l ↦{q} v, COMM True >>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  aheap : atomic_heap Σ
  P : iProp Σ
  l : loc
  ============================
  "HP" : ▷ P
  --------------------------------------∗
  AACC << ∃∃ (v : val) (q : dfrac), l ↦{q} v, ABORT ▷ P >>
       @ ⊤ ∖ ∅, ∅
       << l ↦{q} v, COMM True >>
"printing"
     : string
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : val → iProp Σ
  ============================
  ⊢ <<< ∀∀ x : val, P x >>> code @ ∅ <<< ∃∃ y : val, P y, RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : val → iProp Σ
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << ∃∃ x : val, P x >> @ ⊤, ∅ << ∀∀ y : val, P y, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : val → iProp Σ
  Φ : language.val heap_lang → iProp Σ
  ============================
  _ : AACC << ∃∃ x : val, P x,
              ABORT AU << ∃∃ x : val, P x >>
                       @ ⊤, ∅
                       << ∀∀ y : val, P y, COMM Φ #() >> >>
           @ ⊤, ∅
           << ∀∀ y : val, P y, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  ============================
  ⊢ <<< ∀∀ x : val, l ↦ x >>> code @ ∅ <<< l ↦ x, RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << ∃∃ x : val, l ↦ x >> @ ⊤ ∖ ∅, ∅ << l ↦ x, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  _ : AACC << ∃∃ x : val, l ↦ x,
              ABORT AU << ∃∃ x : val, l ↦ x >>
                       @ ⊤ ∖ ∅, ∅
                       << l ↦ x, COMM Φ #() >> >>
           @ ⊤ ∖ ∅, ∅
           << l ↦ x, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  ============================
  ⊢ <<< l ↦ #() >>> code @ ∅ <<< ∃∃ y : val, l ↦ y, RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << ∀∀ y : val, l ↦ y, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  _ : AACC << l ↦ #(),
              ABORT AU << l ↦ #() >>
                       @ ⊤ ∖ ∅, ∅
                       << ∀∀ y : val, l ↦ y, COMM Φ #() >> >>
           @ ⊤ ∖ ∅, ∅
           << ∀∀ y : val, l ↦ y, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  ============================
  ⊢ <<< l ↦ #() >>> code @ ∅ <<< l ↦ #(), RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  _ : AACC << l ↦ #(),
              ABORT AU << l ↦ #() >> @ ⊤ ∖ ∅, ∅ << l ↦ #(), COMM Φ #() >> >>
           @ ⊤ ∖ ∅, ∅
           << l ↦ #(), COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
"Now come the long pre/post tests"
     : string
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  ============================
  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x >>>
      code @ ∅
    <<< ∃ y : val, l ↦ y, RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x >>
            @ ⊤ ∖ ∅, ∅
            << ∃ y : val, l ↦ y, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  ============================
  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
      code @ ∅
    <<< ∃∃ y : val, l ↦ y, RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
            @ ⊤ ∖ ∅, ∅
            << ∀∀ y : val, l ↦ y, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  ============================
  ⊢ <<< ∀∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
      code @ ∅
    <<< ∃∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
        RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  _ : AU << ∃∃ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
         @ ⊤ ∖ ∅, ∅
         << ∀∀ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
            l ↦ xx, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  ============================
  ⊢ <<< ∀∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
      code @ ∅
    <<< l ↦ x, RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << ∃∃ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
            @ ⊤ ∖ ∅, ∅
            << l ↦ x, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  x : val
  ============================
  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
      code @ ∅
    <<< ∃∃ y : val, l ↦ y, RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  x : val
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
            @ ⊤ ∖ ∅, ∅
            << ∀∀ y : val, l ↦ y, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  x : val
  ============================
  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
      code @ ∅
    <<< l ↦ #(), RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  x : val
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
            @ ⊤ ∖ ∅, ∅
            << l ↦ #(), COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  xx, yyyy : val
  ============================
  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
      code @ ∅
    <<< l ↦ yyyy, RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  xx, yyyy : val
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
            @ ⊤ ∖ ∅, ∅
            << l ↦ yyyy, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  xx, yyyy : val
  ============================
  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
      code @ ∅
    <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
        RET #() >>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  l : loc
  xx, yyyy : val
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
            @ ⊤ ∖ ∅, ∅
            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗
               l ↦ xx, COMM Φ #() >>
  --------------------------------------∗
  WP code {{ v, Φ v }}
"Prettification"
     : string
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : val → iProp Σ
  Φ : language.val heap_lang → iProp Σ
  ============================
  "AU" : ∃ x : val, P x ∗
           (P x ={∅,⊤}=∗
            AU << ∃∃ x0 : val, P x0 >>
               @ ⊤ ∖ ∅, ∅
               << ∀∀ y : val, P y, COMM Φ #() >>)
           ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
  --------------------------------------∗
  WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}