From c5617d595bc09463db6687f8aa60adf10535461e Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Mon, 15 Apr 2024 21:38:32 -0700
Subject: [PATCH 1/4] a couple of temporary workarounds

---
 .../lib/Pulse.Lib.CancellableInvariant.fst    |  5 ++--
 lib/pulse/lib/Pulse.Lib.HigherArray.fst       | 28 ++++++++++++++++++-
 2 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
index bdcf924fa..c1afe2a57 100644
--- a/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
+++ b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
@@ -15,7 +15,7 @@
 *)
 
 module Pulse.Lib.CancellableInvariant
-
+#push-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection'"
 open Pulse.Lib.Pervasives
 
 module GR = Pulse.Lib.GhostReference
@@ -123,7 +123,6 @@ ghost
 fn gather_aux (#p1 #p2:perm) (c:cinv)
   requires active p1 c ** active p2 c
   ensures active (sum_perm p1 p2) c
-  opens emp_inames
 {
   unfold active;
   unfold active;
@@ -133,6 +132,7 @@ fn gather_aux (#p1 #p2:perm) (c:cinv)
 ```
 let gather = gather_aux
 
+#push-options "--admit_smt_queries true"
 ```pulse
 ghost
 fn __gather2 (#p : perm) (c:cinv)
@@ -143,6 +143,7 @@ fn __gather2 (#p : perm) (c:cinv)
   rewrite each (sum_perm (half_perm p) (half_perm p)) as p;
 }
 ```
+#pop-options
 let gather2 = __gather2
 
 ```pulse
diff --git a/lib/pulse/lib/Pulse.Lib.HigherArray.fst b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
index 8e38357f7..95e96d37c 100644
--- a/lib/pulse/lib/Pulse.Lib.HigherArray.fst
+++ b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
@@ -43,22 +43,48 @@ let base_len (#elt: Type) (b: base_t elt) : GTot nat = SZ.v (dfst b)
 let l_pcm_ref (elt:Type u#a) (base_len:SZ.t) =
   r:pcm_ref (PA.pcm elt (SZ.v base_len)){ is_pcm_ref_null r = false || base_len = 0sz }
 
+#push-options "--ext 'compat:injectivity'"
 noeq
 type ptr ([@@@strictly_positive]elt: Type u#a) : Type0 = {
   base_len: Ghost.erased SZ.t;
   base: l_pcm_ref elt base_len;
   offset: (offset: nat { offset <= SZ.v base_len });
 }
+#pop-options
 
 let null_ptr (a:Type u#a)
 : ptr a
 = { base_len = 0sz; base = pcm_ref_null (PA.pcm a 0) ; offset = 0 }
 
+// assume
+// val core_pcm_ref : Type0
+
+// assume
+// val as_core (#a:_) (#p:FStar.PCM.pcm a) (r:pcm_ref p) 
+//   : core_pcm_ref
+// assume
+// val of_core (#a:_) (p:FStar.PCM.pcm a) (r:core_pcm_ref) 
+//   : pcm_ref p
+// assume
+// val as_core_of_core (#a:_) (#p:FStar.PCM.pcm a) (r:core_pcm_ref)
+//   : Lemma (as_core (of_core p r) == r)
+// assume
+// val of_core_as_core (#a:_) (#p:FStar.PCM.pcm a) (r:pcm_ref p)
+//   : Lemma (of_core p (as_core r) == r)
+
+// assume
+// val is_pcm_ref_null
+//     (#a:Type)
+//     (#p:FStar.PCM.pcm a)
+//     (r:pcm_ref q)
+// : b:bool { b <==> r == pcm_ref_null p }
+
 let is_null_ptr (#elt: Type u#a) (p: ptr elt)
 : Pure bool
   (requires True)
   (ensures (fun res -> res == true <==> p == null_ptr elt))
 = is_pcm_ref_null p.base
+  
 
 let base (#elt: Type) (p: ptr elt)
 : Tot (base_t elt)
@@ -76,7 +102,7 @@ let ptr_base_offset_inj (#elt: Type) (p1 p2: ptr elt) : Lemma
   (ensures (
     p1 == p2
   ))
-= ()
+= admit()
 
 let base_len_null_ptr (elt: Type u#a)
 : Lemma

From 479d4c7ca288d1351c35284effae1d1ff690184d Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Mon, 15 Apr 2024 23:04:28 -0700
Subject: [PATCH 2/4] remove spurious parameterization by element type in
 HigherArray

---
 lib/pulse/lib/Pulse.Lib.HigherArray.fst | 196 ++++++++++++++----------
 1 file changed, 112 insertions(+), 84 deletions(-)

diff --git a/lib/pulse/lib/Pulse.Lib.HigherArray.fst b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
index 95e96d37c..31556137c 100644
--- a/lib/pulse/lib/Pulse.Lib.HigherArray.fst
+++ b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
@@ -31,70 +31,88 @@ module PA = Pulse.Lib.PCM.Array
 
 /// An abstract type to represent a base array (whole allocation
 /// unit), exposed for proof purposes only
+assume
+val core_pcm_ref : Type0
+assume
+val as_core (#a:_) (#p:FStar.PCM.pcm a) (r:pcm_ref p) 
+  : core_pcm_ref
+assume
+val of_core (#a:_) (p:FStar.PCM.pcm a) (r:core_pcm_ref) 
+  : pcm_ref p
+assume
+val as_core_of_core (#a:_) (#p:FStar.PCM.pcm a) (r:core_pcm_ref)
+  : Lemma (ensures as_core (of_core p r) == r)
+          [SMTPat (as_core (of_core p r))]
+
+assume
+val of_core_as_core (#a:_) (#p:FStar.PCM.pcm a) (r:pcm_ref p)
+  : Lemma (ensures of_core p (as_core r) == r)
+          [SMTPat (of_core p (as_core r))]
+assume
+val null_core_pcm_ref : core_pcm_ref
+assume
+val is_null_core_pcm_ref (p:core_pcm_ref)
+  : b:bool { b <==> p == null_core_pcm_ref }
+
+assume
+val relate_null
+    (#a:Type)
+    (#p:FStar.PCM.pcm a)
+    (r:pcm_ref p)
+: Lemma (is_pcm_ref_null r <==> (as_core r == null_core_pcm_ref))
+        [SMTPat (is_pcm_ref_null r)]
+
 [@@erasable]
-let base_t (elt: Type u#a)
-: Tot Type0
-= Ghost.erased (base_len: SZ.t & pcm_ref (PA.pcm elt (SZ.v base_len)))
+let base_t
+: Type0
+= Ghost.erased (SZ.t & core_pcm_ref)
 
-let base_len (#elt: Type) (b: base_t elt) : GTot nat = SZ.v (dfst b)
+let base_len (b: base_t) : GTot nat = SZ.v (fst b)
 
 /// An abstract type to represent a C pointer, as a base and an offset
 /// into its base
 let l_pcm_ref (elt:Type u#a) (base_len:SZ.t) =
-  r:pcm_ref (PA.pcm elt (SZ.v base_len)){ is_pcm_ref_null r = false || base_len = 0sz }
+  r:pcm_ref (PA.pcm elt (SZ.v base_len)){ 
+      as_core r =!= null_core_pcm_ref \/
+      base_len = 0sz
+  }
+
 
-#push-options "--ext 'compat:injectivity'"
 noeq
-type ptr ([@@@strictly_positive]elt: Type u#a) : Type0 = {
+type ptr : Type0 = {
   base_len: Ghost.erased SZ.t;
-  base: l_pcm_ref elt base_len;
+  base: (base:core_pcm_ref { base == null_core_pcm_ref ==> SZ.v base_len == 0});
   offset: (offset: nat { offset <= SZ.v base_len });
 }
-#pop-options
-
-let null_ptr (a:Type u#a)
-: ptr a
-= { base_len = 0sz; base = pcm_ref_null (PA.pcm a 0) ; offset = 0 }
-
-// assume
-// val core_pcm_ref : Type0
-
-// assume
-// val as_core (#a:_) (#p:FStar.PCM.pcm a) (r:pcm_ref p) 
-//   : core_pcm_ref
-// assume
-// val of_core (#a:_) (p:FStar.PCM.pcm a) (r:core_pcm_ref) 
-//   : pcm_ref p
-// assume
-// val as_core_of_core (#a:_) (#p:FStar.PCM.pcm a) (r:core_pcm_ref)
-//   : Lemma (as_core (of_core p r) == r)
-// assume
-// val of_core_as_core (#a:_) (#p:FStar.PCM.pcm a) (r:pcm_ref p)
-//   : Lemma (of_core p (as_core r) == r)
-
-// assume
-// val is_pcm_ref_null
-//     (#a:Type)
-//     (#p:FStar.PCM.pcm a)
-//     (r:pcm_ref q)
-// : b:bool { b <==> r == pcm_ref_null p }
-
-let is_null_ptr (#elt: Type u#a) (p: ptr elt)
+
+// noeq
+// type ptr ([@@@strictly_positive]elt: Type u#a) : Type0 = {
+//   base_len: Ghost.erased SZ.t;
+//   base: l_pcm_ref elt base_len;
+//   offset: (offset: nat { offset <= SZ.v base_len });
+// }
+// #pop-options
+
+let null_ptr
+: ptr
+= { base_len = 0sz; base = null_core_pcm_ref ; offset = 0 }
+
+
+let is_null_ptr (p:ptr)
 : Pure bool
   (requires True)
-  (ensures (fun res -> res == true <==> p == null_ptr elt))
-= is_pcm_ref_null p.base
-  
+  (ensures (fun res -> res == true <==> p == null_ptr))
+= is_null_core_pcm_ref p.base
 
-let base (#elt: Type) (p: ptr elt)
-: Tot (base_t elt)
-= (| Ghost.reveal p.base_len, p.base |)
+let base (p: ptr)
+: Tot base_t
+= ( Ghost.reveal p.base_len, p.base )
 
-let offset (#elt: Type) (p: ptr elt)
+let offset (p: ptr)
 : Ghost nat (requires True) (ensures (fun offset -> offset <= base_len (base p)))
 = p.offset
 
-let ptr_base_offset_inj (#elt: Type) (p1 p2: ptr elt) : Lemma
+let ptr_base_offset_inj (p1 p2: ptr) : Lemma
   (requires (
     base p1 == base p2 /\
     offset p1 == offset p2
@@ -102,34 +120,31 @@ let ptr_base_offset_inj (#elt: Type) (p1 p2: ptr elt) : Lemma
   (ensures (
     p1 == p2
   ))
-= admit()
+= ()
 
-let base_len_null_ptr (elt: Type u#a)
-: Lemma
-  (base_len (base (null_ptr elt)) == 0)
-  [SMTPat (base_len (base (null_ptr elt)))]
+let base_len_null_ptr : squash  (base_len (base (null_ptr)) == 0)
 = ()
 
 noeq
-type array ([@@@strictly_positive] elt: Type u#1)
+type array'
 : Type0
-= { p: ptr elt;
+= { p: ptr;
     length: (l:Ghost.erased nat {offset p + l <= base_len (base p)})
   }
-
+let array ([@@@strictly_positive] elt: Type u#1) : Type0 = array'
 let length (#elt: Type) (a: array elt) = a.length
 
 let ptr_of
   (#elt: Type)
   (a: array elt)
-: Tot (ptr elt)
+: Tot (ptr)
 = a.p
 
 let is_full_array (#elt: Type) (a: array elt) : Tot prop =
   length a == base_len (base (ptr_of a))
 
 let null (#a: Type u#1) : array a
-= { p = null_ptr a; length =Ghost.hide 0 }
+= { p = null_ptr; length =Ghost.hide 0 }
 
 let length_fits #elt a = ()
 
@@ -142,9 +157,19 @@ let valid_perm
 = let open FStar.Real in
   ((offset + slice_len <= len /\ slice_len > 0) ==> (p.v <=. one))
 
+let l_pcm_ref' (elt:Type u#a) (base_len:SZ.t) =
+  r:pcm_ref (PA.pcm elt (SZ.v base_len))
+
+let lptr_of (#elt:Type u#1) (a:array elt)
+  : Tot (l_pcm_ref elt ( (ptr_of a).base_len))
+  = of_core 
+       ((PA.pcm elt (SZ.v (ptr_of a).base_len)))
+       (ptr_of a).base
 
 let pts_to (#elt: Type u#1) (a: array elt) (#p: perm) (s: Seq.seq elt) : Tot vprop =
-  pcm_pts_to (ptr_of a).base (mk_carrier (SZ.v (ptr_of a).base_len) (ptr_of a).offset s p) **
+  pcm_pts_to
+    (lptr_of a)
+    (mk_carrier (SZ.v (ptr_of a).base_len) (ptr_of a).offset s p) **
   pure (
     valid_perm (SZ.v (ptr_of a).base_len) (ptr_of a).offset (Seq.length s) p /\
     Seq.length s == length a
@@ -158,7 +183,7 @@ let mk_array
     (base:l_pcm_ref elt base_len)
     (offset:nat { offset <= SZ.v base_len})
 : array elt
-= { p = { base_len; base; offset} ; length = Ghost.hide (SZ.v base_len - offset) }
+= { p = { base_len; base=as_core base; offset} ; length = Ghost.hide (SZ.v base_len - offset) }
 
 ```pulse
 ghost
@@ -176,7 +201,7 @@ ensures
 {
   let a = (mk_array base_len base offset);
   rewrite (pcm_pts_to base (mk_carrier (SZ.v base_len) offset s p))
-      as pcm_pts_to (ptr_of a).base
+      as pcm_pts_to (lptr_of a)
             (mk_carrier (SZ.v (ptr_of a).base_len) 
                         (ptr_of a).offset
                         s p);
@@ -203,6 +228,7 @@ ensures pts_to a #p x ** pure (length a == Seq.length x)
 ```
 let pts_to_len = pts_to_len'
 
+
 ```pulse
 fn alloc' 
     (#elt: Type u#1)
@@ -238,8 +264,8 @@ ensures
     pure (res == Seq.index s (SZ.v i))
 {
   unfold pts_to a #p s;
-  with w. assert (pcm_pts_to (ptr_of a).base w);
-  let v = Pulse.Lib.Core.read (ptr_of a).base w (fun _ -> w);
+  with w. assert (pcm_pts_to (lptr_of a) w);
+  let v = Pulse.Lib.Core.read (lptr_of a) w (fun _ -> w);
   fold (pts_to a #p s);
   fst (Some?.v (FStar.Map.sel v ((ptr_of a).offset + SZ.v i)));
 }
@@ -276,9 +302,9 @@ requires pts_to a s
 ensures pts_to a (Seq.upd s (SZ.v i) v)
 {
   unfold pts_to a #full_perm s;
-  with w. assert (pcm_pts_to (ptr_of a).base w);
+  with w. assert (pcm_pts_to (lptr_of a) w);
   mk_carrier_upd (SZ.v (ptr_of a).base_len) ((ptr_of a).offset) s (SZ.v i) v ();
-  Pulse.Lib.Core.write (ptr_of a).base w _
+  Pulse.Lib.Core.write (lptr_of a) w _
       (PM.lift_frame_preserving_upd
         _ _
         (Frac.mk_frame_preserving_upd
@@ -311,9 +337,9 @@ ensures
   emp
 {
   unfold pts_to a #full_perm s;
-  with w. assert (pcm_pts_to (ptr_of a).base w);
+  with w. assert (pcm_pts_to (lptr_of a) w);
   // Pulse.Lib.Core.write (ptr_of a).base w (PA.one #elt #(length a)) (frame_preserving_upd_one #elt (length a) s);
-  drop_ (pcm_pts_to (ptr_of a).base _)
+  drop_ (pcm_pts_to (lptr_of a) _)
 }
 ```
 let free = free'
@@ -365,13 +391,13 @@ requires pts_to arr #p s
 ensures pts_to arr #(half_perm p) s ** pts_to arr #(half_perm p) s
 {
   unfold pts_to arr #p s;
-  with w. assert (pcm_pts_to (ptr_of arr).base w);
+  with w. assert (pcm_pts_to (lptr_of arr) w);
   mk_carrier_share (SZ.v (ptr_of arr).base_len)
        (ptr_of arr).offset
        s 
        (half_perm p) 
        (half_perm p) ();
-  Pulse.Lib.Core.share (ptr_of arr).base
+  Pulse.Lib.Core.share (lptr_of arr)
     (mk_carrier (SZ.v (ptr_of arr).base_len) (ptr_of arr).offset s (half_perm p))
     (mk_carrier (SZ.v (ptr_of arr).base_len) (ptr_of arr).offset s (half_perm p));
   fold pts_to arr #(half_perm p) s;
@@ -449,10 +475,10 @@ requires pts_to arr #p0 s0 ** pts_to arr #p1 s1
 ensures pts_to arr #(sum_perm p0 p1) s0 ** pure (s0 == s1)
 {
   unfold pts_to arr #p0 s0;
-  with w0. assert (pcm_pts_to (ptr_of arr).base w0);
+  with w0. assert (pcm_pts_to (lptr_of arr) w0);
   unfold pts_to arr #p1 s1;
-  with w1. assert (pcm_pts_to (ptr_of arr).base w1);
-  Pulse.Lib.Core.gather (ptr_of arr).base w0 w1;
+  with w1. assert (pcm_pts_to (lptr_of arr) w1);
+  Pulse.Lib.Core.gather (lptr_of arr) w0 w1;
   of_squash (mk_carrier_gather (SZ.v (ptr_of arr).base_len) ((ptr_of arr).offset) s0 s1 p0 p1 ());
   of_squash (mk_carrier_valid_sum_perm (SZ.v (ptr_of arr).base_len) ((ptr_of arr).offset) s0 p0 p1);
   fold pts_to arr #(sum_perm p0 p1) s0;
@@ -461,10 +487,9 @@ ensures pts_to arr #(sum_perm p0 p1) s0 ** pure (s0 == s1)
 let gather = gather'
 
 let ptr_shift
-  (#elt: Type)
-  (p: ptr elt)
+  (p: ptr)
   (off: nat {offset p + off <= base_len (base p)})
-: ptr elt
+: ptr
 = {
     base_len = p.base_len;
     base = p.base;
@@ -651,11 +676,11 @@ ensures
   let xr = Seq.slice x i (Seq.length x);
   let vl = mk_carrier (SZ.v (ptr_of a).base_len) ((ptr_of a).offset) xl p;
   let vr = mk_carrier (SZ.v (ptr_of a).base_len) ((ptr_of a).offset + i) xr p;
-  Pulse.Lib.Core.share (ptr_of a).base vl vr;
-  rewrite pcm_pts_to (ptr_of a).base vl
-      as  pcm_pts_to (ptr_of (split_l a i)).base vl;
-  rewrite pcm_pts_to (ptr_of a).base vr
-      as  pcm_pts_to (ptr_of (split_r a i)).base vr;
+  Pulse.Lib.Core.share (lptr_of a) vl vr;
+  rewrite pcm_pts_to (lptr_of a) vl
+      as  pcm_pts_to (lptr_of (split_l a i)) vl;
+  rewrite pcm_pts_to (lptr_of a) vr
+      as  pcm_pts_to (lptr_of (split_r a i)) vr;
   fold (pts_to (split_l a i) #p xl);
   fold (pts_to (split_r a i) #p xr);
 }
@@ -764,7 +789,7 @@ let merge' (#elt: Type) (a1: array elt) (a2:array elt { adjacent a1 a2 })
 = { p = ptr_of a1; length=Ghost.hide (length a1 + length a2) }
 
 irreducible
-let merge #elt a1 a2
+let merge #elt (a1:array elt) (a2:array elt{ adjacent a1 a2})
 : i:array elt{ i == merge' a1 a2 } 
 = merge' a1 a2
 
@@ -783,14 +808,17 @@ ensures pts_to (merge a1 a2) #p (x1 `Seq.append` x2)
   unfold pts_to a2 #p x2;
   use_squash (mk_carrier_merge (SZ.v (ptr_of a1).base_len) ((ptr_of a1).offset) x1 x2 p ());
   with w. rewrite 
-          pcm_pts_to (ptr_of a2).base w
-      as  pcm_pts_to (ptr_of a1).base (mk_carrier (SZ.v (ptr_of a1).base_len) ((ptr_of a1).offset + Seq.length x1) x2 p);
-  Pulse.Lib.Core.gather (ptr_of a1).base
+          pcm_pts_to (lptr_of a2) w
+      as  pcm_pts_to (lptr_of a1) (mk_carrier (SZ.v (ptr_of a1).base_len) ((ptr_of a1).offset + Seq.length x1) x2 p);
+  Pulse.Lib.Core.gather (lptr_of a1)
     (mk_carrier (SZ.v (ptr_of a1).base_len) ((ptr_of a1).offset) x1 (p))
     (mk_carrier (SZ.v (ptr_of a1).base_len) ((ptr_of a1).offset + Seq.length x1) x2 (p));
   with w. rewrite
-          pcm_pts_to (ptr_of a1).base w
-      as  pcm_pts_to (ptr_of (merge a1 a2)).base (mk_carrier (SZ.v (ptr_of (merge a1 a2)).base_len) ((ptr_of (merge a1 a2)).offset) (x1 `Seq.append` x2) (p));
+          pcm_pts_to (lptr_of a1) w
+      as  pcm_pts_to 
+              (lptr_of (merge a1 a2))
+              (mk_carrier (SZ.v (ptr_of (merge a1 a2)).base_len)
+                          ((ptr_of (merge a1 a2)).offset) (x1 `Seq.append` x2) (p));
   fold (pts_to (merge a1 a2) #p (Seq.append x1 x2));
 }
 ```

From 93c46b27394855259a0751992c7315c642a20328 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Tue, 16 Apr 2024 14:48:26 -0700
Subject: [PATCH 3/4] clean up Pulse.Lib.HigherArray; expose core_ref and
 ghost_core_ref in Pulse.Lib.Core

---
 lib/pulse/core/PulseCore.Action.fst        |  9 ++---
 lib/pulse/core/PulseCore.Action.fsti       | 14 ++++---
 lib/pulse/core/PulseCore.Heap2.fst         |  2 +-
 lib/pulse/core/PulseCore.Heap2.fsti        |  3 +-
 lib/pulse/core/PulseCore.Memory.fst        |  2 +-
 lib/pulse/core/PulseCore.Memory.fsti       |  3 +-
 lib/pulse/core/PulseCore.TwoLevelHeap.fst  |  3 +-
 lib/pulse/core/PulseCore.TwoLevelHeap.fsti |  3 +-
 lib/pulse/lib/Pulse.Lib.Core.fst           | 10 ++---
 lib/pulse/lib/Pulse.Lib.Core.fsti          | 24 +++++++----
 lib/pulse/lib/Pulse.Lib.HigherArray.fst    | 46 ++--------------------
 11 files changed, 47 insertions(+), 72 deletions(-)

diff --git a/lib/pulse/core/PulseCore.Action.fst b/lib/pulse/core/PulseCore.Action.fst
index 192f49e38..cec5a1c08 100644
--- a/lib/pulse/core/PulseCore.Action.fst
+++ b/lib/pulse/core/PulseCore.Action.fst
@@ -409,10 +409,9 @@ let invariant_name_identifies_invariant p q i j =
 ///////////////////////////////////////////////////////////////////
 // Core operations on references
 ///////////////////////////////////////////////////////////////////
-
-let ref (a:Type u#a) (p:pcm a) = ref a p
-let ref_null (#a:Type u#a) (p:pcm a) = core_ref_null
-let is_ref_null (#a:Type u#a) (#p:pcm a) (r:ref a p) = core_ref_is_null r
+let core_ref = core_ref
+let core_ref_null = core_ref_null
+let is_core_ref_null = core_ref_is_null
 let pts_to = Mem.pts_to
 let pts_to_not_null #a #p r v #ictx = pts_to_not_null_action ictx r v
 
@@ -589,7 +588,7 @@ let elim_exists (#a:Type u#a) (p:a -> slprop)
 
 let drop p = fun #ictx -> drop #ictx p
 
-let ghost_ref = Mem.ghost_ref
+let core_ghost_ref = Mem.core_ghost_ref
 let ghost_pts_to = Mem.ghost_pts_to
 let ghost_alloc #a #pcm x = fun #ictx -> ghost_alloc #ictx #a #pcm x
 let ghost_read #a #p r x f = fun #ictx -> ghost_read #ictx #a #p r x f
diff --git a/lib/pulse/core/PulseCore.Action.fsti b/lib/pulse/core/PulseCore.Action.fsti
index 61776f6e9..e1ea41c9d 100644
--- a/lib/pulse/core/PulseCore.Action.fsti
+++ b/lib/pulse/core/PulseCore.Action.fsti
@@ -199,13 +199,16 @@ val invariant_name_identifies_invariant
 ////////////////////////////////////////////////////////////////////////
 // References
 ////////////////////////////////////////////////////////////////////////
+val core_ref : Type u#0
+val core_ref_null : core_ref
+val is_core_ref_null (r:core_ref) : b:bool { b <==> r == core_ref_null }
 
-val ref ([@@@unused] a:Type u#a) ([@@@unused] p:pcm a) : Type u#0
+let ref (a:Type u#a) (p:pcm a) : Type u#0 = core_ref
+let ref_null (#a:Type u#a) (p:pcm a) : ref a p = core_ref_null
 
-val ref_null (#a:Type u#a) (p:pcm a) : ref a p
-
-val is_ref_null (#a:Type) (#p:FStar.PCM.pcm a) (r:ref a p)
+let is_ref_null (#a:Type) (#p:FStar.PCM.pcm a) (r:ref a p)
 : b:bool { b <==> r == ref_null p }
+= is_core_ref_null r
 
 val pts_to (#a:Type u#1) (#p:pcm a) (r:ref a p) (v:a) : vprop
 
@@ -380,7 +383,8 @@ val drop (p:slprop)
 // Ghost References
 ////////////////////////////////////////////////////////////////////////
 [@@erasable]
-val ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused] p:pcm a) : Type u#0
+val core_ghost_ref : Type u#0
+let ghost_ref (#a:Type u#a) (p:pcm a) : Type u#0 = core_ghost_ref
 val ghost_pts_to (#a:Type u#1) (#p:pcm a) (r:ghost_ref p) (v:a) : vprop
 
 val ghost_alloc
diff --git a/lib/pulse/core/PulseCore.Heap2.fst b/lib/pulse/core/PulseCore.Heap2.fst
index 38d8f9ed7..7deb53ecf 100644
--- a/lib/pulse/core/PulseCore.Heap2.fst
+++ b/lib/pulse/core/PulseCore.Heap2.fst
@@ -530,7 +530,7 @@ let lift_erased
   in
   refined_pre_action_as_action g
 
-let ghost_ref #a p = erased H.core_ref
+let core_ghost_ref = erased H.core_ref
 let ghost_pts_to #a #p r v = llift GHOST (H.pts_to #a #p r v)
 let ghost_free_above_addr h addr = H.free_above_addr h.ghost addr
 
diff --git a/lib/pulse/core/PulseCore.Heap2.fsti b/lib/pulse/core/PulseCore.Heap2.fsti
index d645789d8..2cadd8c48 100644
--- a/lib/pulse/core/PulseCore.Heap2.fsti
+++ b/lib/pulse/core/PulseCore.Heap2.fsti
@@ -743,7 +743,8 @@ val lift_erased
 : action #ONLY_GHOST #allocs #hpre #hpost pre a post
 
 [@@erasable]
-val ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused]p:pcm a) : Type0
+val core_ghost_ref : Type0
+let ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused]p:pcm a) : Type0 = core_ghost_ref
 val ghost_pts_to (#a:Type u#a) (#p:pcm a) (r:ghost_ref p) (v:a) : slprop u#a
 
 val ghost_extend
diff --git a/lib/pulse/core/PulseCore.Memory.fst b/lib/pulse/core/PulseCore.Memory.fst
index 940dd38ee..67523f2f5 100644
--- a/lib/pulse/core/PulseCore.Memory.fst
+++ b/lib/pulse/core/PulseCore.Memory.fst
@@ -2131,7 +2131,7 @@ let pts_to_not_null_action
     (fun _ -> pts_to r v)
 = lift_tot_action (lift_heap_action e (H2.pts_to_not_null_action #a #pcm r v))
 
-let ghost_ref = H2.ghost_ref
+let core_ghost_ref = H2.core_ghost_ref
 let ghost_pts_to #a #pcm r v = up (H2.ghost_pts_to #a #pcm r v)
 
 let with_fresh_ghost_counter (#t:Type u#t) (#post:t -> H2.slprop u#a) (e:inames)
diff --git a/lib/pulse/core/PulseCore.Memory.fsti b/lib/pulse/core/PulseCore.Memory.fsti
index efa3140c2..b6f025f8b 100644
--- a/lib/pulse/core/PulseCore.Memory.fsti
+++ b/lib/pulse/core/PulseCore.Memory.fsti
@@ -435,7 +435,8 @@ val pts_to_not_null_action
 
 (* Ghost references to "small" types *)
 [@@erasable]
-val ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused]p:pcm a) : Type0
+val core_ghost_ref : Type0
+let ghost_ref (#a:Type u#a) (p:pcm a) : Type0 = core_ghost_ref
 val ghost_pts_to (#a:Type u#a) (#p:pcm a) (r:ghost_ref p) (v:a) : vprop u#a
 
 val ghost_alloc
diff --git a/lib/pulse/core/PulseCore.TwoLevelHeap.fst b/lib/pulse/core/PulseCore.TwoLevelHeap.fst
index c73ac9079..7c2286b0f 100644
--- a/lib/pulse/core/PulseCore.TwoLevelHeap.fst
+++ b/lib/pulse/core/PulseCore.TwoLevelHeap.fst
@@ -653,8 +653,7 @@ let extend
           (| y, h1 |)
     in
     ff
-
-let ghost_ref = H2.ghost_ref
+let core_ghost_ref = H2.core_ghost_ref
 let ghost_pts_to #a #pcm r v = up (H2.ghost_pts_to #a #pcm r v)
 let ghost_extend
   (#a:Type u#a)
diff --git a/lib/pulse/core/PulseCore.TwoLevelHeap.fsti b/lib/pulse/core/PulseCore.TwoLevelHeap.fsti
index 828bed124..26f0427f7 100644
--- a/lib/pulse/core/PulseCore.TwoLevelHeap.fsti
+++ b/lib/pulse/core/PulseCore.TwoLevelHeap.fsti
@@ -582,7 +582,8 @@ val extend
 
 (* Small ghost references *)
 [@@erasable]
-val ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused]p:pcm a) : Type0
+val core_ghost_ref : Type0
+let ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused]p:pcm a) : Type0 = core_ghost_ref
 
 (*** ghost_pts_to: Ownership of a ghost reference on the small heap *)
 val ghost_pts_to (#a:Type u#a) (#p:pcm a) (r:ghost_ref p) (v:a) : vprop u#a
diff --git a/lib/pulse/lib/Pulse.Lib.Core.fst b/lib/pulse/lib/Pulse.Lib.Core.fst
index 8156ef861..699546e3c 100644
--- a/lib/pulse/lib/Pulse.Lib.Core.fst
+++ b/lib/pulse/lib/Pulse.Lib.Core.fst
@@ -242,13 +242,13 @@ let elim_false (a:Type) (p:a -> vprop) =
 //////////////////////////////////////////////////////////////////////////
 // References
 //////////////////////////////////////////////////////////////////////////
-let pcm_ref #a p = PulseCore.Action.ref a p
+let core_pcm_ref = PulseCore.Action.core_ref
+let null_core_pcm_ref = PulseCore.Action.core_ref_null
+let is_null_core_pcm_ref r = PulseCore.Action.is_core_ref_null r
 
 let pcm_pts_to (#a:Type u#1) (#p:pcm a) (r:pcm_ref p) (v:a) =
-  PulseCore.Action.pts_to r v
+  PulseCore.Action.pts_to #a #p r v
 let is_small_pcm_pts_to #a #p r v = ()
-let pcm_ref_null #a p = PulseCore.Action.ref_null #a p
-let is_pcm_ref_null #a #p r = PulseCore.Action.is_ref_null #a #p r
 let pts_to_not_null #a #p r v = A.pts_to_not_null #a #p r v
 
 let alloc
@@ -290,7 +290,7 @@ let gather = A.gather
 ////////////////////////////////////////////////////////
 // ghost refs
 ////////////////////////////////////////////////////////
-let ghost_pcm_ref #a p = PulseCore.Action.ghost_ref #a p
+let core_ghost_pcm_ref = PulseCore.Action.core_ghost_ref
 
 instance non_informative_ghost_pcm_ref a p = {
   reveal = (fun r -> Ghost.reveal r) <: NonInformative.revealer (ghost_pcm_ref p);
diff --git a/lib/pulse/lib/Pulse.Lib.Core.fsti b/lib/pulse/lib/Pulse.Lib.Core.fsti
index 01a9c85f1..966e6d196 100644
--- a/lib/pulse/lib/Pulse.Lib.Core.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Core.fsti
@@ -611,10 +611,16 @@ val elim_false (a:Type) (p:a -> vprop)
 ////////////////////////////////////////////////////////
 //Core PCM references
 ////////////////////////////////////////////////////////
-val pcm_ref
-    (#[@@@unused] a:Type u#a)
-    ([@@@unused] p:FStar.PCM.pcm a)
+val core_pcm_ref : Type0
+val null_core_pcm_ref : core_pcm_ref
+val is_null_core_pcm_ref (p:core_pcm_ref)
+  : b:bool { b <==> p == null_core_pcm_ref }
+
+let pcm_ref
+    (#a:Type u#a)
+    (p:FStar.PCM.pcm a)
 : Type0
+= core_pcm_ref
 
 val pcm_pts_to
     (#a:Type u#1)
@@ -631,16 +637,18 @@ val is_small_pcm_pts_to
 : Lemma (is_small (pcm_pts_to r v))
         [SMTPat (is_small (pcm_pts_to r v))]
 
-val pcm_ref_null
+let pcm_ref_null
     (#a:Type)
     (p:FStar.PCM.pcm a)
 : pcm_ref p
+= null_core_pcm_ref
 
-val is_pcm_ref_null
+let is_pcm_ref_null
     (#a:Type)
     (#p:FStar.PCM.pcm a)
     (r:pcm_ref p)
 : b:bool { b <==> r == pcm_ref_null p }
+= is_null_core_pcm_ref r
 
 val pts_to_not_null
     (#a:Type)
@@ -705,12 +713,14 @@ val gather
     (fun _ -> pcm_pts_to r (op pcm v0 v1))
 
 /////////////////////////////////////////////////////////////////////////
-
 [@@erasable]
-val ghost_pcm_ref
+val core_ghost_pcm_ref : Type0
+
+let ghost_pcm_ref
     (#[@@@unused] a:Type u#a)
     ([@@@unused] p:FStar.PCM.pcm a)
 : Type0
+= core_ghost_pcm_ref
 
 instance val non_informative_ghost_pcm_ref
   (a:Type u#a) (p:FStar.PCM.pcm a)
diff --git a/lib/pulse/lib/Pulse.Lib.HigherArray.fst b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
index 31556137c..9bad15251 100644
--- a/lib/pulse/lib/Pulse.Lib.HigherArray.fst
+++ b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
@@ -31,37 +31,6 @@ module PA = Pulse.Lib.PCM.Array
 
 /// An abstract type to represent a base array (whole allocation
 /// unit), exposed for proof purposes only
-assume
-val core_pcm_ref : Type0
-assume
-val as_core (#a:_) (#p:FStar.PCM.pcm a) (r:pcm_ref p) 
-  : core_pcm_ref
-assume
-val of_core (#a:_) (p:FStar.PCM.pcm a) (r:core_pcm_ref) 
-  : pcm_ref p
-assume
-val as_core_of_core (#a:_) (#p:FStar.PCM.pcm a) (r:core_pcm_ref)
-  : Lemma (ensures as_core (of_core p r) == r)
-          [SMTPat (as_core (of_core p r))]
-
-assume
-val of_core_as_core (#a:_) (#p:FStar.PCM.pcm a) (r:pcm_ref p)
-  : Lemma (ensures of_core p (as_core r) == r)
-          [SMTPat (of_core p (as_core r))]
-assume
-val null_core_pcm_ref : core_pcm_ref
-assume
-val is_null_core_pcm_ref (p:core_pcm_ref)
-  : b:bool { b <==> p == null_core_pcm_ref }
-
-assume
-val relate_null
-    (#a:Type)
-    (#p:FStar.PCM.pcm a)
-    (r:pcm_ref p)
-: Lemma (is_pcm_ref_null r <==> (as_core r == null_core_pcm_ref))
-        [SMTPat (is_pcm_ref_null r)]
-
 [@@erasable]
 let base_t
 : Type0
@@ -73,7 +42,7 @@ let base_len (b: base_t) : GTot nat = SZ.v (fst b)
 /// into its base
 let l_pcm_ref (elt:Type u#a) (base_len:SZ.t) =
   r:pcm_ref (PA.pcm elt (SZ.v base_len)){ 
-      as_core r =!= null_core_pcm_ref \/
+      r =!= null_core_pcm_ref \/
       base_len = 0sz
   }
 
@@ -85,13 +54,6 @@ type ptr : Type0 = {
   offset: (offset: nat { offset <= SZ.v base_len });
 }
 
-// noeq
-// type ptr ([@@@strictly_positive]elt: Type u#a) : Type0 = {
-//   base_len: Ghost.erased SZ.t;
-//   base: l_pcm_ref elt base_len;
-//   offset: (offset: nat { offset <= SZ.v base_len });
-// }
-// #pop-options
 
 let null_ptr
 : ptr
@@ -162,9 +124,7 @@ let l_pcm_ref' (elt:Type u#a) (base_len:SZ.t) =
 
 let lptr_of (#elt:Type u#1) (a:array elt)
   : Tot (l_pcm_ref elt ( (ptr_of a).base_len))
-  = of_core 
-       ((PA.pcm elt (SZ.v (ptr_of a).base_len)))
-       (ptr_of a).base
+  = (ptr_of a).base
 
 let pts_to (#elt: Type u#1) (a: array elt) (#p: perm) (s: Seq.seq elt) : Tot vprop =
   pcm_pts_to
@@ -183,7 +143,7 @@ let mk_array
     (base:l_pcm_ref elt base_len)
     (offset:nat { offset <= SZ.v base_len})
 : array elt
-= { p = { base_len; base=as_core base; offset} ; length = Ghost.hide (SZ.v base_len - offset) }
+= { p = { base_len; base; offset} ; length = Ghost.hide (SZ.v base_len - offset) }
 
 ```pulse
 ghost

From e6d6d211227b40bc60dfe20a94e7390155f8b3be Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Wed, 17 Apr 2024 12:17:43 -0700
Subject: [PATCH 4/4] workaround F* issue #3252

---
 lib/pulse/lib/Pulse.Lib.BigGhostReference.fst    |  2 +-
 lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst | 14 +-------------
 lib/pulse/lib/Pulse.Lib.Core.fsti                |  4 ++--
 lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst |  2 +-
 4 files changed, 5 insertions(+), 17 deletions(-)

diff --git a/lib/pulse/lib/Pulse.Lib.BigGhostReference.fst b/lib/pulse/lib/Pulse.Lib.BigGhostReference.fst
index cd67929ee..490364cb0 100644
--- a/lib/pulse/lib/Pulse.Lib.BigGhostReference.fst
+++ b/lib/pulse/lib/Pulse.Lib.BigGhostReference.fst
@@ -20,7 +20,7 @@ open Pulse.Main
 open FStar.PCM
 open Pulse.Lib.PCM.Fraction
 module T = FStar.Tactics
-let ref (a:Type u#2) = ghost_pcm_ref (pcm_frac #a)
+let ref (a:Type u#2) = ghost_pcm_ref #(fractional a) (pcm_frac #a)
 
 instance non_informative_gref (a:Type u#2) : NonInformative.non_informative (ref a) = {
   reveal = (fun x -> reveal x) <: NonInformative.revealer (ref a);
diff --git a/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
index c1afe2a57..e8bf23f42 100644
--- a/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
+++ b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst
@@ -132,19 +132,7 @@ fn gather_aux (#p1 #p2:perm) (c:cinv)
 ```
 let gather = gather_aux
 
-#push-options "--admit_smt_queries true"
-```pulse
-ghost
-fn __gather2 (#p : perm) (c:cinv)
-  requires active (half_perm p) c ** active (half_perm p) c
-  ensures active p c
-{
-  gather c;
-  rewrite each (sum_perm (half_perm p) (half_perm p)) as p;
-}
-```
-#pop-options
-let gather2 = __gather2
+let gather2 #p c = gather #(half_perm p) #(half_perm p) c
 
 ```pulse
 ghost
diff --git a/lib/pulse/lib/Pulse.Lib.Core.fsti b/lib/pulse/lib/Pulse.Lib.Core.fsti
index 966e6d196..b78adc029 100644
--- a/lib/pulse/lib/Pulse.Lib.Core.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Core.fsti
@@ -717,8 +717,8 @@ val gather
 val core_ghost_pcm_ref : Type0
 
 let ghost_pcm_ref
-    (#[@@@unused] a:Type u#a)
-    ([@@@unused] p:FStar.PCM.pcm a)
+    (#a:Type u#a)
+    (p:FStar.PCM.pcm a)
 : Type0
 = core_ghost_pcm_ref
 
diff --git a/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst b/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst
index 5d01191a6..9dbfead89 100644
--- a/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst
+++ b/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst
@@ -20,7 +20,7 @@ open Pulse.Main
 open FStar.PCM
 open Pulse.Lib.PCM.Fraction
 module T = FStar.Tactics
-let ref (a:Type u#1) = ghost_pcm_ref (pcm_frac #a)
+let ref (a:Type u#1) = ghost_pcm_ref #_ (pcm_frac #a)
 
 instance non_informative_gref (a:Type u#1) : NonInformative.non_informative (ref a) = {
   reveal = (fun x -> Ghost.reveal x) <: NonInformative.revealer (ref a);