diff --git a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
new file mode 100644
index 000000000..d88416ed0
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
@@ -0,0 +1,94 @@
+module Pulse.Lib.MonotonicGhostRef
+#lang-pulse
+open Pulse.Lib.Pervasives
+open Pulse.Lib.GhostPCMReference
+open FStar.Preorder
+module GR = Pulse.Lib.GhostPCMReference
+module FP = Pulse.Lib.PCM.FractionalPreorder
+module PP = PulseCore.Preorder
+
+
+let mref (#t:Type) (p:preorder t) = GR.gref (FP.fp_pcm p)
+
+instance non_informative_mref t p = {
+  reveal = (fun r -> Ghost.reveal r) <: NonInformative.revealer (mref p);
+}
+
+let pts_to (#t:Type) 
+           (#p:preorder t) 
+           (r:mref p)
+           (#f:perm)
+           (v:t)
+= exists* h. GR.pts_to r (Some f, h) ** pure (Cons? h /\ PulseCore.Preorder.curval h == v)
+
+let snapshot (#t:Type)
+             (#p:preorder t) 
+             (r:mref p)
+             (v:t)
+= exists* h. GR.pts_to r (None, h) ** pure (Cons? h /\ PulseCore.Preorder.curval h == v)
+  
+let full (#t:Type) (#p:preorder t) (v:t) : FP.pcm_carrier p = 
+  (Some 1.0R, [v])
+
+ghost
+fn alloc (#t:Type0) (#p:preorder t) (v:t)
+requires emp
+returns r:mref p
+ensures pts_to r #1.0R v
+{
+  let r = alloc #_ #(FP.fp_pcm p) (full v);
+  fold (pts_to r #1.0R v);
+  r
+}
+
+ghost
+fn take_snapshot (#t:Type) (#p:preorder t) (r:mref p) (#f:perm) (v:t)
+requires pts_to r #f v
+ensures pts_to r #f v ** snapshot r v
+{
+  unfold pts_to;
+  with h. assert (GR.pts_to r (Some f, h));
+  rewrite (GR.pts_to r (Some f, h)) as 
+          (GR.pts_to r ((Some f, h) `(FP.fp_pcm p).p.op` (None, h)));
+  GR.share r (Some f, h) (None, h);
+  fold (pts_to r #f v);
+  fold (snapshot r v);
+}
+ 
+ghost
+fn recall_snapshot (#t:Type) (#p:preorder t) (r:mref p) (#f:perm) (#v #u:t)
+requires pts_to r #f v ** snapshot r u
+ensures  pts_to r #f v ** snapshot r u ** pure (as_prop (p u v))
+{
+  unfold pts_to;
+  with h. assert (GR.pts_to r (Some f, h));
+  unfold snapshot;
+  with h'. assert (GR.pts_to r (None, h'));
+  GR.gather r (Some f, h) (None, h');
+  GR.share r (Some f, h) (None, h');
+  fold (snapshot r u);
+  fold (pts_to r #f v);
+}
+
+ghost
+fn dup_snapshot (#t:Type) (#p:preorder t) (r:mref p) (#u:t)
+requires snapshot r u
+ensures snapshot r u ** snapshot r u
+{
+  unfold snapshot;
+  with h. assert (GR.pts_to r (None, h));
+  GR.share r (None, h) (None, h);
+  fold (snapshot r u);
+  fold (snapshot r u);
+}
+
+ghost
+fn update (#t:Type) (#p:preorder t) (r:mref p) (#u:t) (v:t)
+requires pts_to r #1.0R u ** pure (as_prop (p u v))
+ensures pts_to r #1.0R v
+{
+  unfold pts_to;
+  with f h. assert (GR.pts_to r (f, h));
+  GR.write r _ _ (FP.mk_frame_preserving_upd p h v);
+  fold pts_to;
+}
\ No newline at end of file
diff --git a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti
new file mode 100644
index 000000000..695761293
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fsti
@@ -0,0 +1,56 @@
+module Pulse.Lib.MonotonicGhostRef
+#lang-pulse
+open Pulse.Lib.Pervasives
+open Pulse.Lib.GhostPCMReference
+open FStar.Preorder
+module GR = Pulse.Lib.GhostPCMReference
+module FP = Pulse.Lib.PCM.FractionalPreorder
+module PP = PulseCore.Preorder
+
+let as_prop (t:Type0) = t <==> True
+
+[@@erasable]
+val mref (#t:Type0) (p:preorder t) : Type0
+
+instance val non_informative_mref
+  (t:Type u#0) (p:preorder t)
+  : NonInformative.non_informative (mref p)
+
+val pts_to (#t:Type) 
+           (#p:preorder t) 
+           (r:mref p)
+           (#f:perm)
+           (v:t)
+: slprop2
+
+val snapshot (#t:Type)
+             (#p:preorder t) 
+             (r:mref p)
+             (v:t)
+: slprop2
+  
+ghost
+fn alloc (#t:Type0) (#p:preorder t) (v:t)
+requires emp
+returns r:mref p
+ensures pts_to r #1.0R v
+
+ghost
+fn take_snapshot (#t:Type) (#p:preorder t) (r:mref p) (#f:perm) (v:t)
+requires pts_to r #f v
+ensures pts_to r #f v ** snapshot r v
+ 
+ghost
+fn recall_snapshot (#t:Type) (#p:preorder t) (r:mref p) (#f:perm) (#v #u:t)
+requires pts_to r #f v ** snapshot r u
+ensures  pts_to r #f v ** snapshot r u ** pure (as_prop (p u v))
+
+ghost
+fn dup_snapshot (#t:Type) (#p:preorder t) (r:mref p) (#u:t)
+requires snapshot r u
+ensures snapshot r u ** snapshot r u
+
+ghost
+fn update (#t:Type) (#p:preorder t) (r:mref p) (#u:t) (v:t)
+requires pts_to r #1.0R u ** pure (as_prop (p u v))
+ensures pts_to r #1.0R v
diff --git a/share/pulse/examples/by-example/PulseTutorial.MonotonicCounter.fst b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounter.fst
new file mode 100644
index 000000000..7d6ce75af
--- /dev/null
+++ b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounter.fst
@@ -0,0 +1,114 @@
+module PulseTutorial.MonotonicCounter
+#lang-pulse
+open Pulse.Lib.Pervasives
+open FStar.Preorder
+module MR = Pulse.Lib.MonotonicGhostRef
+module PP = PulseCore.Preorder
+noeq
+type ctr = {
+    inv: int -> slprop;
+    snapshot : int -> slprop;
+    next:    i:erased int -> stt int (inv i) (fun y -> inv (i + 1) ** pure (y == reveal i));
+    destroy: i:erased int -> stt unit (inv i) (fun _ -> emp);
+    snap:    i:erased int -> stt_ghost unit emp_inames (inv i) (fun _ -> snapshot i ** inv i);
+    recall:  i:erased int -> j:erased int -> stt_ghost unit emp_inames (snapshot i ** inv j) (fun y -> snapshot i ** inv j ** pure (i <= j));
+    dup:     i:erased int -> stt_ghost unit emp_inames (snapshot i) (fun y -> snapshot i ** snapshot i);
+}
+
+let next c #i = c.next i
+let destroy c #i = c.destroy i
+let snap c #i = c.snap i
+let recall c #i #j = c.recall i j
+let dup c #i = c.dup i
+let increases : preorder int = fun x y -> b2t (x <= y)
+let mctr = MR.mref increases
+
+fn new_counter ()
+requires emp
+returns c:ctr
+ensures c.inv 0
+{
+    open Pulse.Lib.Box;
+    let x = alloc 0;
+    let mr : MR.mref increases = MR.alloc #int #increases 0;
+    fn next (i:erased int)
+    requires pts_to x i ** MR.pts_to mr #1.0R i
+    returns j:int
+    ensures (pts_to x (i + 1) ** MR.pts_to mr #1.0R (i + 1)) ** pure (j == reveal i)
+    {
+        let j = !x;
+        x := j + 1;
+        MR.update mr (j + 1);
+        j
+    };
+    fn destroy (i:erased int)
+    requires pts_to x i ** MR.pts_to mr #1.0R i
+    ensures emp
+    {
+       free x;
+       drop_ (MR.pts_to mr _);
+    };
+    ghost
+    fn snap (i:erased int)
+    requires pts_to x i ** MR.pts_to mr #1.0R i
+    ensures  MR.snapshot mr i ** (pts_to x i ** MR.pts_to mr #1.0R i)
+    {
+        MR.take_snapshot mr #1.0R i;
+    };
+    ghost
+    fn recall (i:erased int) (j:erased int)
+    requires  MR.snapshot mr i ** (pts_to x j ** MR.pts_to mr #1.0R j)
+    ensures  MR.snapshot mr i ** (pts_to x j ** MR.pts_to mr #1.0R j) ** pure (i <= j)
+    {
+        MR.recall_snapshot mr;
+    };
+    ghost
+    fn dup (i:erased int)
+    requires MR.snapshot mr i
+    ensures MR.snapshot mr i ** MR.snapshot mr i
+    {
+        MR.dup_snapshot mr;
+    };
+    let c = { 
+        inv = (fun i -> pts_to x i ** MR.pts_to mr #1.0R i);
+        snapshot = MR.snapshot mr;
+        next;
+        destroy;
+        snap;
+        recall;
+        dup 
+    };
+    rewrite (pts_to x 0 ** MR.pts_to mr #1.0R 0) as (c.inv 0);
+    c
+}
+
+
+fn do_something (c:ctr) (#i #k:erased int)
+requires c.inv i ** c.snapshot k
+ensures exists* j. c.inv j
+{
+  let recall = c.recall;
+  recall _ _;
+  drop_ (c.snapshot _);
+}
+
+fn test_counter ()
+requires emp
+ensures emp
+{
+    let c = new_counter ();
+    snap c;
+    assert (c.snapshot 0);
+    let x = next c;
+    assert pure (x == 0);
+    let x = next c;
+    assert pure (x == 1);
+    dup c;
+    do_something c;
+    recall c;
+    let z = next c;
+    assert pure (z >= 0);
+    destroy c;
+    drop_ (c.snapshot _);
+    assert pure (z >= 0);
+}
diff --git a/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareable.fst b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareable.fst
new file mode 100644
index 000000000..576ac0761
--- /dev/null
+++ b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareable.fst
@@ -0,0 +1,115 @@
+module PulseTutorial.MonotonicCounterShareable
+#lang-pulse
+open Pulse.Lib.Pervasives
+open FStar.Preorder
+module MR = Pulse.Lib.MonotonicGhostRef
+module PP = PulseCore.Preorder
+module B = Pulse.Lib.Box
+
+assume
+val incr_atomic_box (r:B.box int) (#n:erased int)
+  : stt_atomic int emp_inames
+        (B.pts_to r n) 
+        (fun i -> B.pts_to r i ** pure (i == n + 1))
+
+noeq
+type ctr = {
+    inv:  int -> slprop;
+    next: i:erased int -> stt int (inv i) (fun j -> inv j ** pure (i < j));
+    dup:  i:erased int -> stt_ghost unit emp_inames (inv i) (fun y -> inv i ** inv i);
+}
+
+let next c #i = c.next i
+let dup c #i = c.dup i
+let increases : preorder int = fun x y -> b2t (x <= y)
+let mctr = MR.mref increases
+
+let inv_core (x:B.box int) (mr:MR.mref increases)
+: slprop2
+= exists* j. B.pts_to x j ** MR.pts_to mr #1.0R j
+
+fn new_counter ()
+requires emp
+returns c:ctr
+ensures c.inv 0
+{
+    open Pulse.Lib.Box;
+    let x = alloc 0;
+    let mr : MR.mref increases = MR.alloc #int #increases 0;
+    MR.take_snapshot mr #1.0R 0;
+    fold (inv_core x mr);
+    let ii = new_invariant (inv_core x mr);
+    fn next (i:erased int)
+    requires inv ii (inv_core x mr) ** MR.snapshot mr i
+    returns j:int
+    ensures (inv ii (inv_core x mr) ** MR.snapshot mr j) ** pure (i < j)
+    {
+        with_invariants ii {
+            unfold inv_core;
+            let res = incr_atomic_box x;
+            MR.recall_snapshot mr;
+            MR.update mr res;
+            drop_ (MR.snapshot mr i);
+            MR.take_snapshot mr #1.0R res;
+            fold (inv_core);
+            res
+        }
+    };
+    ghost
+    fn dup (i:erased int)
+    requires inv ii (inv_core x mr) ** MR.snapshot mr i
+    ensures (inv ii (inv_core x mr) ** MR.snapshot mr i) **
+            (inv ii (inv_core x mr) ** MR.snapshot mr i)
+    {
+        MR.dup_snapshot mr;
+        dup_inv ii _;
+    };
+    let c = { inv = (fun i -> inv ii (inv_core x mr) ** MR.snapshot mr i);
+              next; dup };
+    rewrite (inv ii (inv_core x mr) ** MR.snapshot mr 0) as (c.inv 0);
+    c
+}
+
+fn do_something (c:ctr) (#i:erased int) (_:unit)
+requires c.inv i
+ensures exists* j. c.inv j
+{ 
+    let v1 = next c;
+    let v2 = next c;
+    assert pure (v1 < v2);
+}
+
+fn test_counter ()
+requires emp
+ensures emp
+{
+    let c = new_counter ();
+    dup c;
+    par (do_something c #0) (do_something c #0);
+    // with j. assert (c.inv j);
+    // show_proof_state;
+    admit() //ambiguity with identical slprops in the context
+}
+
+let named (name:string) (p:slprop) = p
+
+fn do_something' (name:string) (c:ctr) (#i:erased int) (_:unit)
+requires c.inv i
+ensures named name (exists* j. c.inv j)
+{ 
+    let v1 = next c;
+    let v2 = next c;
+    assert pure (v1 < v2);
+    fold (named name (exists* j. c.inv j));
+}
+
+fn test_counter' ()
+requires emp
+ensures emp
+{
+    let c = new_counter ();
+    dup c;
+    par (do_something' "left" c #0) (do_something' "right" c #0);
+    drop_ (named "left" _);
+    drop_ (named "right" _)
+}
\ No newline at end of file
diff --git a/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareableFreeable.fst b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareableFreeable.fst
new file mode 100644
index 000000000..5038d1397
--- /dev/null
+++ b/share/pulse/examples/by-example/PulseTutorial.MonotonicCounterShareableFreeable.fst
@@ -0,0 +1,135 @@
+module PulseTutorial.MonotonicCounterShareableFreeable
+#lang-pulse
+open Pulse.Lib.Pervasives
+open FStar.Preorder
+module MR = Pulse.Lib.MonotonicGhostRef
+module PP = PulseCore.Preorder
+module B = Pulse.Lib.Box
+module CI = Pulse.Lib.CancellableInvariant
+
+assume
+val incr_atomic_box (r:B.box int) (#n:erased int)
+  : stt_atomic int emp_inames
+        (B.pts_to r n) 
+        (fun i -> B.pts_to r i ** pure (i == n + 1))
+
+noeq
+type ctr = {
+    inv:     perm -> int -> slprop;
+    next:    p:perm -> i:erased int -> stt int (inv p i) (fun j -> inv p j ** pure (i < j));
+    share:   p:perm -> i:erased int -> stt_ghost unit emp_inames (inv p i) (fun y -> inv (p /. 2.0R) i ** inv (p /. 2.0R) i);
+    gather:  p:perm -> q:perm -> i:erased int -> j:erased int -> stt_ghost unit emp_inames (inv p i ** inv q j) (fun y -> inv (p +. q) i);
+    destroy: i:erased int -> stt unit (inv 1.0R i) (fun _ -> emp);
+}
+
+let next c #p #i = c.next p i
+let share c #p #i = c.share p i
+let destroy c #i = c.destroy i
+[@@allow_ambiguous]
+ghost
+fn gather (c:ctr) #p #q #i #j
+requires c.inv p i ** c.inv q j
+ensures c.inv (p +. q) i
+{
+    let gather = c.gather;
+    gather p q i j
+}
+
+let increases : preorder int = fun x y -> b2t (x <= y)
+let mctr = MR.mref increases
+
+let inv_core (x:B.box int) (mr:MR.mref increases)
+: slprop2
+= exists* j. B.pts_to x j ** MR.pts_to mr #1.0R j
+
+fn new_counter ()
+requires emp
+returns c:ctr
+ensures c.inv 1.0R 0
+{
+    open Pulse.Lib.Box;
+    open CI;
+    let x = alloc 0;
+    let mr : MR.mref increases = MR.alloc #int #increases 0;
+    MR.take_snapshot mr #1.0R 0;
+    fold (inv_core x mr);
+    let ii = CI.new_cancellable_invariant (inv_core x mr);
+
+    fn next (p:perm) (i:erased int)
+    requires inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii p ** MR.snapshot mr i
+    returns j:int
+    ensures (inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii p ** MR.snapshot mr j) ** pure (i < j)
+    { 
+        with_invariants (iname_of ii) {
+            unpack_cinv_vp ii;
+            unfold inv_core;
+            let res = incr_atomic_box x;
+            MR.recall_snapshot mr;
+            MR.update mr res;
+            drop_ (MR.snapshot mr i);
+            MR.take_snapshot mr #1.0R res;
+            fold (inv_core);
+            pack_cinv_vp ii;
+            res
+        }
+    };
+
+    ghost
+    fn share (p:perm) (i:erased int)
+    requires inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii p ** MR.snapshot mr i
+    ensures (inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii (p /. 2.0R) ** MR.snapshot mr i) **
+            (inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii (p /. 2.0R) ** MR.snapshot mr i)
+    {
+        MR.dup_snapshot mr;
+        dup_inv (iname_of ii) _;
+        CI.share ii;
+    };
+
+    ghost
+    fn gather (p q:perm) (i j:erased int)
+    requires (inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii p ** MR.snapshot mr i) **
+             (inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii q ** MR.snapshot mr j)
+    ensures (inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii (p +. q) ** MR.snapshot mr i)
+    {
+        CI.gather #p #q ii;
+        drop_ (MR.snapshot mr j);
+        drop_ (inv (iname_of ii) (cinv_vp ii (inv_core x mr)));
+    };
+
+    fn destroy (i:erased int)
+    requires inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii 1.0R ** MR.snapshot mr i
+    ensures emp
+    {
+        CI.cancel ii;
+        unfold inv_core;
+        B.free x;
+        drop_ (MR.pts_to mr _);
+        drop_ (MR.snapshot mr _);
+    };
+
+    let c = { inv = (fun p i -> inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii p ** MR.snapshot mr i);
+              next; share; gather; destroy };
+            
+    rewrite (inv (iname_of ii) (cinv_vp ii (inv_core x mr)) ** CI.active ii 1.0R ** MR.snapshot mr 0) as (c.inv 1.0R 0);
+    c
+}
+
+fn do_something (c:ctr) #p (#i:erased int) (_:unit)
+requires c.inv p i
+ensures exists* j. c.inv p j
+{ 
+    let v1 = next c;
+    let v2 = next c;
+    assert pure (v1 < v2);
+}
+
+fn test_counter ()
+requires emp
+ensures emp
+{
+    let c = new_counter ();
+    share c;
+    par (do_something c #_ #_) (do_something c #_ #_);
+    gather c;
+    destroy c
+}
\ No newline at end of file