From af04988e1184b1a83636b8a56c309dbbc96fe8e0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jan 2021 10:34:15 +0100
Subject: [PATCH] Tests.

---
 tests/heap_lang.ref | 53 +++++++++++++++++++++++++++++++++++++++++++++
 tests/heap_lang.v   | 30 ++++++++++++++++++++++++-
 2 files changed, 82 insertions(+), 1 deletion(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 0118b3b39..b17918505 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -188,6 +188,59 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   Heq : ∀ v : val, I v ↔ I #true
   ============================
   ⊢ l ↦_(λ _ : val, I #true) □
+"wp_iMod_fupd_atomic"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  E1, E2 : coPset
+  P : iPropI Σ
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : P
+--------------------------------------∗
+WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
+
+"wp_iInv_atomic"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  N : namespace
+  E : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : â–· P
+"Hclose" : ▷ P ={E ∖ ↑N,E}=∗ emp
+--------------------------------------∗
+WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
+
+"wp_iInv_atomic_acc"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  N : namespace
+  E : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : â–· P
+--------------------------------------∗
+WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
+
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 88c103024..5196629e5 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,4 +1,4 @@
-From iris.base_logic.lib Require Import gen_inv_heap.
+From iris.base_logic.lib Require Import gen_inv_heap invariants.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
@@ -323,6 +323,34 @@ Section inv_mapsto_tests.
   Abort.
 End inv_mapsto_tests.
 
+Section atomic.
+  Context `{!heapG Σ}.
+
+  (* These tests check if a side-condition for [Atomic] is generated *)
+  Check "wp_iMod_fupd_atomic".
+  Lemma wp_iMod_fupd_atomic E1 E2 P :
+    (|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
+  Proof.
+    iIntros "H". iMod "H". Show.
+  Abort.
+
+  Check "wp_iInv_atomic".
+  Lemma wp_iInv_atomic N E P :
+    ↑ N ⊆ E →
+    inv N P -∗ WP #() #() @ E {{ _, True }}.
+  Proof.
+    iIntros (?) "H". iInv "H" as "H" "Hclose". Show.
+  Abort.
+  Check "wp_iInv_atomic_acc".
+  Lemma wp_iInv_atomic_acc N E P :
+    ↑ N ⊆ E →
+    inv N P -∗ WP #() #() @ E {{ _, True }}.
+  Proof.
+    (* Test if a side-condition for [Atomic] is generated *)
+    iIntros (?) "H". iInv "H" as "H". Show.
+  Abort.
+End atomic.
+
 Section printing_tests.
   Context `{!heapG Σ}.
 
-- 
GitLab