Merge pull request #487 from FStarLang/gebner_ghost_null

gebner · web-flow · commit 47b4e2103e3c · 2025-09-30T17:49:56.000-07:00
Null ghost references.
diff --git a/lib/common/Pulse.Lib.Core.fsti b/lib/common/Pulse.Lib.Core.fsti
@@ -498,6 +498,8 @@ val later_equiv (p q: slprop) : squash (later (equiv p q) == equiv (later p) (la
 [@@erasable]
 val slprop_ref : Type0
 
+val null_slprop_ref : slprop_ref
+
 val slprop_ref_pts_to ([@@@mkey]x: slprop_ref) (y: slprop) : slprop
 
 val slprop_ref_alloc (y: slprop)
@@ -765,6 +767,8 @@ val gather
 [@@erasable]
 val core_ghost_pcm_ref : Type0
 
+val null_core_ghost_pcm_ref : core_ghost_pcm_ref
+
 let ghost_pcm_ref
     (#a:Type u#a)
     (p:FStar.PCM.pcm a)
@@ -790,6 +794,16 @@ val timeless_ghost_pcm_pts_to
 : Lemma (timeless (ghost_pcm_pts_to r v))
         [SMTPat (timeless (ghost_pcm_pts_to r v))]
 
+val ghost_pts_to_not_null
+    (#a:Type)
+    (#p:pcm a)
+    (r:ghost_pcm_ref p)
+    (v:a)
+: stt_ghost (squash (r =!= null_core_ghost_pcm_ref))
+            emp_inames
+            (ghost_pcm_pts_to r v)
+            (fun _ -> ghost_pcm_pts_to r v)
+
 val ghost_alloc
     (#a:Type u#1)
     (#pcm:pcm a)
diff --git a/lib/core/Pulse.Lib.Core.fst b/lib/core/Pulse.Lib.Core.fst
@@ -239,6 +239,7 @@ let later_equiv = Sep.later_equiv
 
 // TODO: these are write-once for now, though it's possible to construct fractional permission variables out of this
 let slprop_ref = PulseCore.Action.slprop_ref
+let null_slprop_ref = PulseCore.Action.null_slprop_ref
 let slprop_ref_pts_to x y = PulseCore.Action.slprop_ref_pts_to x y
 let slprop_ref_alloc x = A.slprop_ref_alloc x
 let slprop_ref_share x #y = A.slprop_ref_share x y
@@ -358,12 +359,15 @@ let gather = A.gather
 ////////////////////////////////////////////////////////
 let core_ghost_pcm_ref = PulseCore.Action.core_ghost_ref
 
+let null_core_ghost_pcm_ref = PulseCore.Action.core_ghost_ref_null
+
 instance non_informative_ghost_pcm_ref a p = {
   reveal = (fun r -> Ghost.reveal r) <: NonInformative.revealer (ghost_pcm_ref p);
 }
 
 let ghost_pcm_pts_to #a #p r v = PulseCore.Action.ghost_pts_to #a #p r v
 let timeless_ghost_pcm_pts_to #a #p r v = PulseCore.Action.timeless_ghost_pts_to #a #p r v
+let ghost_pts_to_not_null #a #p r v = A.ghost_pts_to_not_null #a #p r v
 let ghost_alloc = A.ghost_alloc
 let ghost_read = A.ghost_read
 let ghost_write = A.ghost_write
diff --git a/lib/core/PulseCore.Action.fst b/lib/core/PulseCore.Action.fst
@@ -726,8 +726,12 @@ let elim_exists (#a:Type u#a) (p:a -> slprop)
 let drop p = lift_pre_act0_act fun #ictx -> ITA.drop #ictx p
 
 let core_ghost_ref = Mem.core_ghost_ref
+let core_ghost_ref_null = Mem.core_ghost_ref_null
 let ghost_pts_to #a #pcm r x = Sep.lift (Mem.ghost_pts_to #a #pcm r x)
 let timeless_ghost_pts_to #a #p r x = Sep.timeless_lift (Mem.ghost_pts_to #a #p r x)
+let ghost_pts_to_not_null #a #p r v =
+  lift_pre_act0_act fun #ictx ->
+  ITA.lift_mem_action (Mem.ghost_pts_to_not_null_action #a #p r v)
 let ghost_alloc #a #pcm x = let open Mem in lift_eqs (); lift_pre_act0_act fun #ictx -> ITA.lift_mem_action <| ghost_alloc #a #pcm x
 let ghost_read #a #p r x f = let open Mem in lift_eqs(); lift_pre_act1_act fun #ictx -> ITA.lift_mem_action <| ghost_read #a #p r x f
 let ghost_write #a #p r x y f = let open Mem in lift_eqs(); lift_pre_act0_act fun #ictx -> ITA.lift_mem_action <| ghost_write #a #p r x y f
@@ -770,6 +774,7 @@ let equiv_elim (a b:slprop) =
   lift_pre_act0_act fun #ictx -> ITA.equiv_elim #ictx a b
 
 let slprop_ref = Sep.slprop_ref
+let null_slprop_ref = Sep.null_slprop_ref
 let slprop_ref_pts_to = Sep.slprop_ref_pts_to
 let slprop_ref_alloc y = lift_pre_act0_act fun #ictx -> ITA.slprop_ref_alloc #ictx y
 let slprop_ref_share x y = lift_pre_act0_act fun #ictx -> ITA.slprop_ref_share #ictx x y
diff --git a/lib/core/PulseCore.Action.fsti b/lib/core/PulseCore.Action.fsti
@@ -465,6 +465,7 @@ val drop (p:slprop)
 ////////////////////////////////////////////////////////////////////////
 [@@erasable]
 val core_ghost_ref : Type u#0
+val core_ghost_ref_null : core_ghost_ref
 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) : slprop
 
@@ -475,6 +476,13 @@ val timeless_ghost_pts_to
     (v:a)
 : Lemma (timeless (ghost_pts_to r v))
 
+val ghost_pts_to_not_null (#a:Type u#1) (#p:FStar.PCM.pcm a) (r:ghost_ref p) (v:a)
+: act (squash (r =!= core_ghost_ref_null))
+    Ghost
+    emp_inames 
+    (ghost_pts_to r v)
+    (fun _ -> ghost_pts_to r v)
+
 val ghost_alloc
     (#a:Type u#1)
     (#pcm:pcm a)
@@ -675,6 +683,8 @@ val equiv_elim (a b:slprop)
 [@@erasable]
 val slprop_ref : Type0
 
+val null_slprop_ref : slprop_ref
+
 val slprop_ref_pts_to (x: slprop_ref) (y: slprop) : slprop
 
 val slprop_ref_alloc (y: slprop)
diff --git a/lib/core/PulseCore.Atomic.fst b/lib/core/PulseCore.Atomic.fst
@@ -296,6 +296,7 @@ let write r x y f = A.write r x y f
 let share #a #pcm r v0 v1 = lift_neutral_ghost (A.share r v0 v1)
 let gather #a #pcm r v0 v1 = lift_neutral_ghost (A.gather r v0 v1)
 
+let ghost_pts_to_not_null #a #p r v = lift_neutral_ghost (A.ghost_pts_to_not_null #a #p r v)
 let ghost_alloc #a #pcm x = lift_neutral_ghost <| A.ghost_alloc #a #pcm x
 let ghost_read
     (#a:Type)
diff --git a/lib/core/PulseCore.Atomic.fsti b/lib/core/PulseCore.Atomic.fsti
@@ -382,6 +382,16 @@ val gather
 ////////////////////////////////////////////////////////////////////////
 // Ghost References
 ////////////////////////////////////////////////////////////////////////
+val ghost_pts_to_not_null
+    (#a:Type u#1)
+    (#p:FStar.PCM.pcm a)
+    (r:ghost_ref p)
+    (v:a)
+: stt_ghost (squash (r =!= core_ghost_ref_null))
+    emp_inames
+    (ghost_pts_to r v)
+    (fun _ -> ghost_pts_to r v)
+
 val ghost_alloc
     (#a:Type u#1)
     (#pcm:pcm a)
diff --git a/lib/core/PulseCore.BaseHeapSig.fst b/lib/core/PulseCore.BaseHeapSig.fst
@@ -230,6 +230,9 @@ let ghost_share #a #p r x y =
 let ghost_gather #a #p r x y =
   lift_heap_action (H2.ghost_gather #a #p r x y)
     #(fun _ -> ghost_pts_to r (op p x y))
+let ghost_pts_to_not_null_action #a #p r x =
+  lift_heap_action (H2.ghost_pts_to_not_null_action #a #p r x)
+    #(fun _ -> ghost_pts_to #a #p r x)
 
 let extend #a #pcm x = fun frame m0 ->
   let (| y, m1 |) = H2.apply_action (H2.extend #a #pcm x) frame m0 in
@@ -267,6 +270,9 @@ let ghost_share' #a #p r x y =
 let ghost_gather' #a #p r x y =
   ghost_gather #_ #(R.raise p) r (U.raise_val (reveal x)) (U.raise_val (reveal y))
 
+let ghost_pts_to_not_null_action' #a #p r v =
+  ghost_pts_to_not_null_action #_ #(R.raise p) r (U.raise_val (reveal v))
+
 let pts_to' #a #p r x =
   H2.pts_to #(U.raise_t a) #(R.raise p) r (U.raise_val x)
 
diff --git a/lib/core/PulseCore.BaseHeapSig.fsti b/lib/core/PulseCore.BaseHeapSig.fsti
@@ -22,6 +22,7 @@ let is_null : core_ref -> GTot bool = H2.core_ref_is_null
 let ref (a:Type u#a) (p:pcm a) = core_ref
 
 let core_ghost_ref : Type u#0 = H2.core_ghost_ref
+let core_ghost_ref_null = H2.core_ghost_ref_null
 let ghost_ref (a:Type u#a) (p:pcm a) = core_ghost_ref
 let add (#a:Type) (f:Set.decide_eq a) (x:a) (y:Set.set a) = Set.union (Set.singleton f x) y
 
@@ -181,6 +182,15 @@ val ghost_gather
     (ghost_pts_to r v0 `star` ghost_pts_to r v1)
     (fun _ -> ghost_pts_to r (op pcm v0 v1))
 
+val ghost_pts_to_not_null_action
+      (#a:Type)
+      (#pcm:pcm a)
+      (r:ghost_ref a pcm)
+      (v:Ghost.erased a)
+: ghost_action_except (squash (r =!= core_ghost_ref_null))
+    (ghost_pts_to r v)
+    (fun _ -> ghost_pts_to r v)
+
 val extend
     (#a:Type)
     (#pcm:pcm a)
@@ -288,6 +298,15 @@ val ghost_gather'
     (ghost_pts_to' u#a u#b r v0 `star` ghost_pts_to' u#a u#b r v1)
     (fun _ -> ghost_pts_to' u#a u#b r (op pcm v0 v1))
 
+val ghost_pts_to_not_null_action'
+      (#a:Type u#a)
+      (#pcm:pcm a)
+      (r:ghost_ref a pcm)
+      (v:Ghost.erased a)
+: ghost_action_except (squash (r =!= core_ghost_ref_null))
+    (ghost_pts_to' u#a u#b r v)
+    (fun _ -> ghost_pts_to' u#a u#b r v)
+
 val pts_to' (#a:Type u#a) (#p:pcm a) (r:ref a p) (x:a) : slprop u#(max a b)
 
 val extend'
diff --git a/lib/core/PulseCore.Heap2.fst b/lib/core/PulseCore.Heap2.fst
@@ -471,6 +471,7 @@ let lift_erased
   refined_pre_action_as_action g
 
 let core_ghost_ref = erased H.core_ref
+let core_ghost_ref_null = H.core_ref_null
 let core_ghost_ref_eq x y = H.core_ref_eq (reveal x) (reveal y)
 let ghost_pts_to #a #p r v = llift GHOST (H.pts_to #a #p r v)
 
@@ -652,3 +653,6 @@ let ghost_gather
     (Ghost.hide <|
       lift_action_ghost ni_squash (H.gather_action #a #pcm r v0 v1))
 #pop-options
+
+let ghost_pts_to_not_null_action #a #p r v =
+  lift_action_ghost ni_squash (H.pts_to_not_null_action #a #p r v)
diff --git a/lib/core/PulseCore.Heap2.fsti b/lib/core/PulseCore.Heap2.fsti
@@ -630,6 +630,7 @@ val lift_erased
 
 [@@erasable]
 val core_ghost_ref : Type0
+val core_ghost_ref_null : core_ghost_ref
 val core_ghost_ref_eq (x y:core_ghost_ref) : GTot (b:bool{b <==> (x==y)})
 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
@@ -728,3 +729,13 @@ val ghost_gather
     (ghost_pts_to r v0 `star` ghost_pts_to r v1)
     (squash (composable pcm v0 v1))
     (fun _ -> ghost_pts_to r (op pcm v0 v1))
+
+val ghost_pts_to_not_null_action 
+      (#a:Type u#a)
+      (#pcm:pcm a)
+      (r:ghost_ref pcm)
+      (v:Ghost.erased a)
+: action #IMMUTABLE
+    (ghost_pts_to r v)
+    (squash (r =!= core_ghost_ref_null))
+    (fun _ -> ghost_pts_to r v)
diff --git a/lib/core/PulseCore.IndirectionTheorySep.fst b/lib/core/PulseCore.IndirectionTheorySep.fst
@@ -1164,6 +1164,8 @@ let invariant_name_identifies_invariant i p q =
 
 let slprop_ref = address
 
+let null_slprop_ref = 0
+
 let slprop_ref_pts_to x y =
   reveal_mem_le ();
   mk_slprop fun m ->
diff --git a/lib/core/PulseCore.IndirectionTheorySep.fsti b/lib/core/PulseCore.IndirectionTheorySep.fsti
@@ -436,6 +436,8 @@ val invariant_name_identifies_invariant (i: iref) (p q: slprop) :
 [@@erasable]
 val slprop_ref : Type0
 
+val null_slprop_ref : slprop_ref
+
 val slprop_ref_pts_to (x: slprop_ref) (y: slprop) : slprop
 
 val fresh_slprop_ref
diff --git a/lib/core/PulseCore.MemoryAlt.fst b/lib/core/PulseCore.MemoryAlt.fst
@@ -122,12 +122,14 @@ let pts_to_not_null_action = B.pts_to_not_null_action' u#(a+1) u#(a+3)
 (* Ghost references to "small" types *)
 [@@erasable]
 let core_ghost_ref : Type0 = B.core_ghost_ref
+let core_ghost_ref_null = PulseCore.Heap2.core_ghost_ref_null
 let ghost_pts_to = B.ghost_pts_to' u#(a+1) u#(a+3)
 let ghost_alloc = B.ghost_extend' u#(a+1) u#(a+3)
 let ghost_read = B.ghost_read' u#(a+1) u#(a+3)
 let ghost_write = B.ghost_write' u#(a+1) u#(a+3)
 let ghost_share = B.ghost_share' u#(a+1) u#(a+3)
 let ghost_gather = B.ghost_gather' u#(a+1) u#(a+3)
+let ghost_pts_to_not_null_action #a #pcm = B.ghost_pts_to_not_null_action' u#(a+1) u#(a+3) #a #pcm
 
 (* Concrete references to "big" types *)
 let big_pts_to = B.pts_to' u#(a+2) u#(a+3)
diff --git a/lib/core/PulseCore.MemoryAlt.fsti b/lib/core/PulseCore.MemoryAlt.fsti
@@ -213,6 +213,7 @@ val pts_to_not_null_action
 (* Ghost references to "small" types *)
 [@@erasable]
 val core_ghost_ref : Type0
+val core_ghost_ref_null : core_ghost_ref
 let ghost_ref (#a:Type u#a) (p:pcm a) : Type0 = core_ghost_ref
 val ghost_pts_to (#a:Type u#(a+1)) (#p:pcm a) (r:ghost_ref p) (v:a) : slprop u#a
 
@@ -269,6 +270,14 @@ val ghost_gather
     (ghost_pts_to r v0 `star` ghost_pts_to r v1)
     (fun _ -> ghost_pts_to r (op pcm v0 v1))
 
+val ghost_pts_to_not_null_action 
+      (#a:Type u#(a + 1)) (#pcm:pcm a)
+      (r:ghost_ref pcm)
+      (v:Ghost.erased a)
+: pst_ghost_action_except (squash (r =!= core_ghost_ref_null))
+    (ghost_pts_to r v)
+    (fun _ -> ghost_pts_to r v)
+
 (* Concrete references to "big" types *)
 val big_pts_to (#a:Type u#(a + 2)) (#pcm:_) (r:ref a pcm) (v:a) : slprop u#a
 
diff --git a/lib/pulse/lib/Pulse.Lib.GhostReference.fst b/lib/pulse/lib/Pulse.Lib.GhostReference.fst
@@ -22,6 +22,8 @@ module H = Pulse.Lib.HigherGhostReference
 module U = Pulse.Lib.Raise
 let ref a = H.ref (U.raise_t a)
 
+let null #a = H.null
+
 instance non_informative_gref (a:Type0) : NonInformative.non_informative (ref a) = {
   reveal = (fun x -> Ghost.reveal x) <: NonInformative.revealer (ref a);
 }
@@ -156,3 +158,12 @@ fn pts_to_perm_bound (#a:_) (#p:_) (r:ref a) (#v:a)
   fold pts_to r #p v;
 }
 
+ghost
+fn pts_to_not_null #a (#p:_) (r:ref a) (#v:a)
+  preserves r |-> Frac p v
+  ensures  pure (r =!= null)
+{
+  unfold pts_to r #p v;
+  H.pts_to_not_null r;
+  fold pts_to r #p v;
+}
diff --git a/lib/pulse/lib/Pulse.Lib.GhostReference.fsti b/lib/pulse/lib/Pulse.Lib.GhostReference.fsti
@@ -26,6 +26,8 @@ open FStar.Ghost
 [@@erasable]
 val ref ([@@@unused] a:Type u#0) : Type u#0
 
+val null #a : ref a
+
 instance val non_informative_gref (a:Type0)
   : NonInformative.non_informative (ref a)
 
@@ -102,3 +104,8 @@ ghost
 fn pts_to_perm_bound (#a:_) (#p:_) (r:ref a) (#v:a)
   preserves r |-> Frac p v
   ensures   pure (p <=. 1.0R)
+
+ghost
+fn pts_to_not_null #a (#p:_) (r:ref a) (#v:a)
+  preserves r |-> Frac p v
+  ensures  pure (r =!= null)
diff --git a/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst b/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst
@@ -23,6 +23,8 @@ open Pulse.Lib.PCM.Fraction
 module T = FStar.Tactics
 let ref (a:Type u#1) = ghost_pcm_ref #_ (pcm_frac #a)
 
+let null #a = null_core_ghost_pcm_ref
+
 instance non_informative_gref (a:Type u#1) : NonInformative.non_informative (ref a) = {
   reveal = (fun x -> Ghost.reveal x) <: NonInformative.revealer (ref a);
 }
@@ -163,3 +165,13 @@ fn pts_to_perm_bound (#a:_) (#p:_) (r:ref a) (#v:a)
   fold pts_to r #p v;
 }
 
+
+ghost
+fn pts_to_not_null #a (#p:_) (r:ref a) (#v:a)
+  preserves r |-> Frac p v
+  ensures  pure (r =!= null)
+{
+  unfold pts_to r #p v;
+  ghost_pts_to_not_null r _;
+  fold pts_to r #p v;
+}
diff --git a/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fsti b/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fsti
@@ -25,6 +25,8 @@ open Pulse.Class.PtsTo
 
 [@@erasable]
 val ref ([@@@unused] a:Type u#1) : Type u#0
+
+val null #a : ref a
       
 instance val non_informative_gref (a:Type u#1)
   : NonInformative.non_informative (ref a)
@@ -103,3 +105,8 @@ ghost
 fn pts_to_perm_bound (#a:_) (#p:_) (r:ref a) (#v:a)
   requires r |-> Frac p v
   ensures  (r |-> Frac p v) ** pure (p <=. 1.0R)
+
+ghost
+fn pts_to_not_null #a (#p:_) (r:ref a) (#v:a)
+  preserves r |-> Frac p v
+  ensures  pure (r =!= null)
