Mark the (deprecated) alloc/free for Array and Ref as private

lib/pulse/lib/Pulse.Lib.Array.Core.fst

@@ -71,7 +71,7 @@ fn pts_to_len (#t:Type) (a:array t) (#p:perm) (#x:FStar.Seq.seq t)
 
 
 
-fn alloc (#elt:Type0) (x:elt) (n:SZ.t)
+fn __alloc (#elt:Type0) (x:elt) (n:SZ.t)
   requires emp
   returns a:array elt
 ensures
@@ -84,7 +84,7 @@ ensures
   fold (pts_to a (Seq.create (SZ.v n) x));
   a
 }
-
+let alloc = __alloc
 
 
 fn op_Array_Access
@@ -128,7 +128,7 @@ ensures
 
 
 
-fn free
+fn __free
     (#elt: Type)
     (a: array elt)
     (#s: Ghost.erased (Seq.seq elt))
@@ -140,7 +140,7 @@ ensures
   unfold (pts_to a s);
   H.free a;
 }
-
+let free = __free
 
 let share #a arr #s #p = H.share arr #(raise_seq s) #p
 

lib/pulse/lib/Pulse.Lib.Array.Core.fsti

@@ -56,7 +56,8 @@ fn pts_to_len (#t:Type0) (a:array t) (#p:perm) (#x:Seq.seq t)
   requires pts_to a #p x
   ensures  pts_to a #p x ** pure (length a == Seq.length x)
 
-[@@deprecated "Array.Core.alloc is meant to be generated by the Pulse elaborator, not called directly; use Vec.alloc instead"]
+(* Not to be called directly. You may want Vec.alloc instead. *)
+private
 fn alloc (#elt: Type) (x: elt) (n: SZ.t)
   requires emp
   returns  a : array elt
@@ -81,7 +82,8 @@ fn op_Array_Assignment
   requires pts_to a s
   ensures  pts_to a (Seq.upd s (SZ.v i) v)
 
-[@@deprecated "Array.Core.free is not meant to be called directly; use Vec.free instead"]
+(* Not to be called directly. You may want Vec.free instead. *)
+private
 fn free (#elt: Type) (a: array elt) (#s: erased (Seq.seq elt))
   requires pts_to a s ** pure (is_full_array a)
   ensures emp

lib/pulse/lib/Pulse.Lib.Box.fst

@@ -19,6 +19,7 @@ module Pulse.Lib.Box
 open Pulse.Lib.Core
 
 module R = Pulse.Lib.Reference
+friend Pulse.Lib.Reference
 
 #lang-pulse
 
@@ -29,28 +30,23 @@ let pts_to b #p v = R.pts_to b.r #p v
 
 let pts_to_timeless _ _ _ = ()
 
-(* This function is extracted primitively. The implementation
-below is only a model, and uses the internal Ref.alloc. Hence
-we disable the warning about using Ref.alloc. *)
-#push-options "--warn_error -288"
 fn alloc (#a:Type0) (x:a)
   requires emp
   returns  b : box a
   ensures  pts_to b x
 {
-  let r = R.alloc x;
+  let r = R.__alloc x;
   rewrite R.pts_to r x as pts_to (B r) x;
   (B r);
 }
-#pop-options
 
 fn op_Bang (#a:Type0) (b:box a) (#v:erased a) (#p:perm)
   requires pts_to b #p v
   returns  x : a
   ensures  pts_to b #p v ** pure (reveal v == x)
 {
   unfold (pts_to b #p v);
-  let x = R.(!b.r);
+  let x = R.read b.r;
   fold (pts_to b #p v);
   x
 }
@@ -60,16 +56,13 @@ fn op_Colon_Equals (#a:Type0) (b:box a) (x:a) (#v:erased a)
   ensures  pts_to b (hide x)
 {
   unfold (pts_to b v);
-  R.(b.r := x);
+  R.write b.r x;
   fold (pts_to b (hide x));
 }
 
 #lang-fstar // 'rewrite' below is not the keyword!
 
-(* Same comment as for alloc. *)
-#push-options "--warn_error -288"
-let free b #v = R.free b.r #v
-#pop-options
+let free b #v = R.__free b.r #v
 
 let share b = R.share b.r
 let gather b = R.gather b.r

lib/pulse/lib/Pulse.Lib.Reference.fst

@@ -32,7 +32,7 @@ let pts_to
 let pts_to_timeless r p x = H.pts_to_timeless r p (U.raise_val x)
 
 
-fn alloc (#a:Type u#0) (v:a)
+fn __alloc (#a:Type u#0) (v:a)
   requires emp
   returns r:ref a
   ensures pts_to r v
@@ -41,7 +41,7 @@ fn alloc (#a:Type u#0) (v:a)
   fold (pts_to r #1.0R v);
   r
 }
-
+let alloc = __alloc
 
 
 fn read
@@ -77,13 +77,14 @@ fn write
 let op_Colon_Equals = write
 
 
-fn free #a (r:ref a) (#n:erased a)
+fn __free #a (r:ref a) (#n:erased a)
   requires pts_to r #1.0R n
   ensures emp
 {
   unfold (pts_to r #1.0R n);
   H.free r;
 }
+let free = __free
 
 
 

lib/pulse/lib/Pulse.Lib.Reference.fsti

@@ -42,7 +42,8 @@ val pts_to_timeless (#a:Type) ([@@@mkey] r:ref a) (p:perm) (x:a)
   : Lemma (timeless (pts_to r #p x))
           [SMTPat (timeless (pts_to r #p x))]
 
-[@@deprecated "Reference.alloc is unsound; use Box.alloc instead"]
+(* Not to be called directly. You may want Box.alloc instead. *)
+private
 fn alloc
   (#a:Type)
   (x:a)
@@ -87,8 +88,8 @@ fn op_Colon_Equals
   ensures  r |-> x
 
 
-[@@deprecated "Reference.free is unsound; use Box.free instead"]
-
+(* Not to be called directly. You may want Box.free instead. *)
+private
 fn free
   (#a:Type)
   (r:ref a)

lib/pulse/lib/Pulse.Lib.Vec.fst

@@ -22,6 +22,7 @@ open Pulse.Lib.Pervasives
 
 module R = Pulse.Lib.Reference
 module A = Pulse.Lib.Array
+friend Pulse.Lib.Array.Core
 
 type vec a = A.array a
 let length v = A.length v
@@ -30,18 +31,10 @@ let pts_to v #p s = A.pts_to v #p s
 let pts_to_timeless _ _ _ = ()
 let pts_to_len v = A.pts_to_len v
 
-(* This function is extracted primitively. The implementation
-below is only a model, and uses the internal Ref.alloc. Hence
-we disable the warning about using Array.alloc. *)
-#push-options "--warn_error -288"
-let alloc x n = A.alloc x n
-#pop-options
+let alloc x n = A.__alloc x n
 let op_Array_Access v i #p #s = A.op_Array_Access v i #p #s
 let op_Array_Assignment v i x #s = A.op_Array_Assignment v i x #s
-(* Same comment as above *)
-#push-options "--warn_error -288"
-let free v #s = A.free v #s
-#pop-options
+let free v #s = A.__free v #s
 let share v = A.share v
 let gather v = A.gather v
 

test/Test.ReflikeClass.fst

@@ -5,27 +5,22 @@ open FStar.Tactics.Typeclasses
 open Pulse.Lib.Pervasives
 module Box = Pulse.Lib.Box
 
+(* Note: no alloc/free so we can catch both Box and Ref. *)
 [@@fundeps [0]; pulse_unfold]
 class reflike (vt:Type) (rt:Type) = {
   ( |-> ) : rt -> vt -> slprop;
-  alloc   : v:vt -> stt rt emp (fun r -> r |-> v);
   (!) : r:rt -> #v0:erased vt -> stt vt (r |-> v0) (fun v -> (r |-> v0) ** pure (Ghost.reveal v0 == v));
   (:=) : r:rt -> v:vt -> #v0:erased vt -> stt unit (r |-> v0) (fun _ -> r |-> v);
 }
 
-(* Prevent warning about using alloc... this is just a test. *)
-#push-options "--warn_error -288"
 instance reflike_ref (a:Type) : reflike a (ref a) = {
   ( |-> ) = (fun r v -> Pulse.Lib.Reference.pts_to r v);
-  alloc   = Pulse.Lib.Reference.alloc;
   ( ! )   = (fun r #v0 -> Pulse.Lib.Reference.op_Bang r #v0 #1.0R);
   ( := )  = (fun r v #v0 -> Pulse.Lib.Reference.op_Colon_Equals r v #v0);
 }
-#pop-options
 
 instance reflike_box (a:Type) : reflike a (Box.box a) = {
   ( |-> ) = (fun r v -> Pulse.Lib.Box.pts_to r v);
-  alloc   = Pulse.Lib.Box.alloc;
   ( ! )   = (fun r #v0 -> Pulse.Lib.Box.op_Bang r #v0 #1.0R);
   ( := )  = (fun r v #v0 -> Pulse.Lib.Box.op_Colon_Equals r v #v0);
 }