some more examples of monotonic counters

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;
+}

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

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);
+}

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" _)
+}