From 7499c0fa2f1517e8572a18ea24b04bf1dd881a71 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Dec 2020 19:40:08 +0100
Subject: [PATCH] Add `mapsto_persist` to `atomic_heap`.

---
 iris_heap_lang/lib/atomic_heap.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 27e44b081..62edb1d2c 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -18,9 +18,11 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   (* -- mapsto properties -- *)
   mapsto_timeless l q v :> Timeless (mapsto l q v);
   mapsto_fractional l v :> Fractional (λ (q : Qp), mapsto l (DfracOwn q) v);
+  mapsto_persistent l v :> Persistent (mapsto l DfracDiscarded v);
   mapsto_as_fractional l q v :>
     AsFractional (mapsto l (DfracOwn q) v) (λ q, mapsto l (DfracOwn q) v) q;
-  mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 -∗ mapsto l q2 v2 -∗ ⌜v1 = v2⌝;
+  mapsto_agree l dq1 dq2 v1 v2 : mapsto l dq1 v1 -∗ mapsto l dq2 v2 -∗ ⌜v1 = v2⌝;
+  mapsto_persist l dq v : mapsto l dq v ==∗ mapsto l DfracDiscarded v;
   (* -- operation specs -- *)
   alloc_spec (v : val) :
     {{{ True }}} alloc v {{{ l, RET #l; mapsto l (DfracOwn 1) v }}};
@@ -144,4 +146,5 @@ Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
      load_spec := primitive_load_spec;
      store_spec := primitive_store_spec;
      cmpxchg_spec := primitive_cmpxchg_spec;
+     mapsto_persist := primitive_laws.mapsto_persist;
      mapsto_agree := primitive_laws.mapsto_agree |}.
-- 
GitLab