atomic.ref

"test_awp_apply"
     : string
1 goal
  
  H : atomic_heap
  Σ : gFunctors
  heapGS0 : heapGS Σ
  atomic_heapGS0 : atomic_heapGS Σ
  Q : iProp Σ
  l : loc
  v : val
  ============================
  "HQ" : Q
  "Hl" : l ↦ v
  --------------------------------------∗
  AACC <{ ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT Q ∗ l ↦ v }>
       @ ⊤ ∖ ∅, ∅
       <{ l ↦{q} v0, COMM Q }>
"test_awp_apply_without"
     : string
1 goal
  
  H : atomic_heap
  Σ : gFunctors
  heapGS0 : heapGS Σ
  atomic_heapGS0 : atomic_heapGS Σ
  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 }>
"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 ∗ 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 ∗ 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 }}
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : val → iProp Σ
  ============================
  ⊢ <<{ ∀∀ x : val, P x }>>
      code @ ∅
    <<{ ∃∃ y : val, P y | z : val, RET z; P z }>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : val → iProp Σ
  ============================
  ⊢ <<{ ∀∀ x : val, P x }>> code @ ∅ <<{ ∃∃ y : val, P y | RET y; P y }>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : val → iProp Σ
  ============================
  ⊢ <<{ ∀∀ x : val, P x }>> code @ ∅ <<{ P x | RET x; P x }>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : val → iProp Σ
  ============================
  ⊢ <<{ P #() }>> code @ ∅ <<{ ∃∃ y : val, P y | RET y; P y }>>
1 goal
  
  Σ : gFunctors
  heapGS0 : heapGS Σ
  P : iProp Σ
  ============================
  ⊢ <<{ P }>> code @ ∅ <<{ P | RET #42; P }>>
"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 }}