fix tests

iris_heap_lang/primitive_laws.v

@@ -317,7 +317,7 @@ Lemma twp_xchg s E l v' v :
   [[{ RET v'; l ↦ v }]].
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; first done.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  iIntros (σ1 ns κs nt) "[Hσ Hκs] !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with head_step.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".

iris_staging/heap_lang/interpreter.v

@@ -535,6 +535,13 @@ Section interpreter.
       let '(l, _) := l_v0 in
       _ ← interp_modify_state (state_upd_heap <[l:=Some w]>);
       mret (LitV LitUnit)
+    | Xchg el e =>
+      w ← interp e;
+      vl ← interp el;
+      l_v0 ← read_loc "xchg" vl;
+      let '(l, v0) := l_v0 in
+      _ ← interp_modify_state (state_upd_heap <[l:=Some w]>);
+      mret v0
     | CmpXchg e e1 e2 =>
       v2 ← interp e2;
       v1 ← interp e1;

tests/heap_lang.ref

@@ -267,37 +267,6 @@ goal 2 is:
 --------------------------------------∗
 WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 
-"xchg_example"
-     : string
-1 goal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  l : loc
-  v₁, v₂ : val
-  Φ : val → iPropI Σ
-  ============================
-  "Hl" : l ↦ v₂
-  "HΦ" : l ↦ v₂ -∗ Φ v₁
-  --------------------------------------∗
-  |={⊤}=> Φ v₁
-  
-1 goal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  N : namespace
-  l : loc
-  v : val
-  Φ : language.val heap_lang → iPropI Σ
-  v' : val
-  ============================
-  "HΦ" : ∀ v'0 : language.val heap_lang, True -∗ Φ v'0
-  "Hl" : l ↦ v
-  "Hclose" : ▷ (∃ v0 : val, l ↦ v0) ={⊤ ∖ ↑N,⊤}=∗ emp
-  --------------------------------------∗
-  |={⊤ ∖ ↑N,⊤}=> Φ v'
-  
 1 goal
   
   Σ : gFunctors

tests/heap_lang.v

@@ -199,6 +199,37 @@ Section tests.
     iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
   Qed.
 
+  Lemma wp_xchg l (v₁ v₂ : val) :
+    {{{ l ↦ v₁ }}}
+      Xchg #l v₂
+    {{{ RET v₁; l ↦ v₂ }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ".
+    wp_xchg.
+    iApply "HΦ" => //.
+  Qed.
+
+   Lemma twp_xchg l (v₁ v₂ : val) :
+     l ↦ v₁ -∗
+       WP  Xchg #l v₂ [{ v₁, l ↦ v₂ }].
+  Proof.
+    iIntros "Hl".
+    wp_xchg => //.
+  Qed.
+
+  Lemma wp_xchg_inv N l (v : val) :
+    {{{ inv N (∃ v, l ↦ v) }}}
+      Xchg #l v
+    {{{ v', RET v'; True }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ".
+    iInv "Hl" as (v') "Hl" "Hclose".
+    wp_xchg.
+    iApply "HΦ".
+    iApply "Hclose".
+    iExists _ => //.
+  Qed.
+
   Lemma wp_alloc_split :
     ⊢ WP Alloc #0 {{ _, True }}.
   Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
@@ -383,29 +414,6 @@ Section atomic.
     iIntros (?) "H". iInv "H" as "H". Show.
   Abort.
 
-  Check "xchg_example".
-
-  Lemma xchg_example l (v₁ v₂ : val) :
-    {{{ l ↦ v₁ }}}
-      Xchg #l v₂
-    {{{ RET v₁; l ↦ v₂ }}}.
-  Proof.
-    iIntros (Φ) "Hl HΦ".
-    wp_xchg.
-    Show.
-  Abort.
-
-  Lemma xchg_inv_example N l (v : val) :
-    {{{ inv N (∃ v, l ↦ v) }}}
-      Xchg #l v
-    {{{ v', RET v'; True }}}.
-  Proof.
-    iIntros (Φ) "Hl HΦ".
-    iInv "Hl" as (v') "Hl" "Hclose".
-    wp_xchg.
-    Show.
-  Abort.
-
 End atomic.
 
 Section printing_tests.