From b5eee6f94ef00155d9b7f1940350dff991550b45 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 27 Jun 2025 10:22:59 -0700 Subject: [PATCH] Mark the (deprecated) alloc/free for Array and Ref as private They cannot be removed from the fsti as they are needed for extraction, but marking them private makes them unaccessible to users, instead of just warning. --- lib/pulse/lib/Pulse.Lib.Array.Core.fst | 8 ++++---- lib/pulse/lib/Pulse.Lib.Array.Core.fsti | 6 ++++-- lib/pulse/lib/Pulse.Lib.Box.fst | 17 +++++------------ lib/pulse/lib/Pulse.Lib.Reference.fst | 7 ++++--- lib/pulse/lib/Pulse.Lib.Reference.fsti | 7 ++++--- lib/pulse/lib/Pulse.Lib.Vec.fst | 13 +++---------- test/Test.ReflikeClass.fst | 7 +------ 7 files changed, 25 insertions(+), 40 deletions(-) diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fst b/lib/pulse/lib/Pulse.Lib.Array.Core.fst index 93fb932fe..fff95e3f2 100644 --- a/lib/pulse/lib/Pulse.Lib.Array.Core.fst +++ b/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 diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fsti b/lib/pulse/lib/Pulse.Lib.Array.Core.fsti index 47ca24f69..05ff798b3 100644 --- a/lib/pulse/lib/Pulse.Lib.Array.Core.fsti +++ b/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 diff --git a/lib/pulse/lib/Pulse.Lib.Box.fst b/lib/pulse/lib/Pulse.Lib.Box.fst index 3651194c3..8c3bd88e7 100644 --- a/lib/pulse/lib/Pulse.Lib.Box.fst +++ b/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,20 +30,15 @@ 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 @@ -50,7 +46,7 @@ fn op_Bang (#a:Type0) (b:box a) (#v:erased a) (#p:perm) 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 diff --git a/lib/pulse/lib/Pulse.Lib.Reference.fst b/lib/pulse/lib/Pulse.Lib.Reference.fst index d0dfd4c77..bddc96330 100644 --- a/lib/pulse/lib/Pulse.Lib.Reference.fst +++ b/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 diff --git a/lib/pulse/lib/Pulse.Lib.Reference.fsti b/lib/pulse/lib/Pulse.Lib.Reference.fsti index 86107fecf..141ea95b2 100644 --- a/lib/pulse/lib/Pulse.Lib.Reference.fsti +++ b/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) diff --git a/lib/pulse/lib/Pulse.Lib.Vec.fst b/lib/pulse/lib/Pulse.Lib.Vec.fst index 579ce5eab..2e88f43ea 100644 --- a/lib/pulse/lib/Pulse.Lib.Vec.fst +++ b/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 diff --git a/test/Test.ReflikeClass.fst b/test/Test.ReflikeClass.fst index c9dfcb82c..7ce9becc0 100644 --- a/test/Test.ReflikeClass.fst +++ b/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); }