atomic.ref

1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  aheap : atomic_heap
  Q : iProp Σ
  l : loc
  v : val
  ============================
  "Hl" : l ↦ v
  --------------------------------------∗
  atomic_acc (⊤ ∖ ∅) ∅ (tele_app (λ (v0 : val) (q : dfrac), l ↦{q} v0))
    (l ↦ v) (tele_app (λ (v0 : val) (q : dfrac), tele_app (l ↦{q} v0)))
    (λ.. (_ : [tele (_ : val) (_ : dfrac)]) (_ : [tele]), Q -∗ Q)
"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 }}