Merge pull request #53 from FStarLang/nik_injectivity

Nik injectivity
FStarLang · Apr 17, 2024 · 680a750 · 680a750
2 parents bd1af96 + e6d6d21
commit 680a750
Show file tree

Hide file tree

Showing 14 changed files with 118 additions and 100 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.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
@@ -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,17 +132,7 @@ fn gather_aux (#p1 #p2:perm) (c:cinv)
 ```
 let gather = gather_aux
 
-```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;
-}
-```
-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.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
@@ -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
-    (#[@@@unused] a:Type u#a)
-    ([@@@unused] p:FStar.PCM.pcm a)
+val core_ghost_pcm_ref : Type0
+
+let ghost_pcm_ref
+    (#a:Type u#a)
+    (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)