Remove FStar.Ghost.Pull

lib/core/PulseCore.Action.fst

@@ -232,9 +232,10 @@ let lift_pre_act_ghost
 let return 
     (#a:Type u#a)
     (#r:reifiability)
+    #opens
     (#post:a -> slprop)
     (x:a)
-: act a r emp_inames (post x) post
+: act a r opens (post x) post
 = fun #ictx -> return_pre_act #a #ictx #post x
 
 let bind_ghost

lib/core/PulseCore.Action.fsti

@@ -62,9 +62,10 @@ val act
 val return 
     (#a:Type u#a)
     (#r:_)
+    #opens
     (#post:a -> slprop)
     (x:a)
-: act a r emp_inames (post x) post
+: act a r opens (post x) post
 
 val bind_ghost
      (#a:Type u#a)

lib/core/PulseCore.Atomic.fst

@@ -63,7 +63,7 @@ let return_eq' #a #r x post
 : act a r emp_inames
       (post x ** pure (x == x))
       (fun r -> post r ** pure (r == x))
-= A.return #a #_ #(fun r -> post r ** pure (r == x)) x
+= A.return x
 
 let return_eq 
     (#a:Type u#a)
@@ -81,7 +81,7 @@ let return_atomic #a x post
       (fun r -> post r ** pure (r == x))
 = return_eq x
 
-let return_atomic_noeq #a x post = A.return #a #_ #post x
+let return_atomic_noeq #a x post = A.return #a #_ #_ #post x
 
 let bind_atomic
     (#a:Type u#a)
@@ -188,24 +188,16 @@ let sub_invs_stt_atomic
   A.weaken #_ #_ #_ #_ #(r_of_obs obs) opens2 e
 
 let stt_ghost a opens pre post =
-  Ghost.erased (act a Ghost opens pre post)
+  Ghost.erased (act (erased a) Ghost opens pre (as_ghost_post post))
 
-let return_ghost #a x p = Ghost.hide (return_eq x)
-let return_ghost_noeq #a x p = Ghost.hide (A.return #_ #_ #p x)
-
-let bind_ghost
+let lift_ghost_neutral'
     (#a:Type u#a)
-    (#b:Type u#b)
     (#opens:inames)
-    (#pre1:slprop)
-    (#post1:a -> slprop)
-    (#post2:b -> slprop)
-    (e1:stt_ghost a opens pre1 post1)
-    (e2:(x:a -> stt_ghost b opens (post1 x) post2))
-: stt_ghost b opens pre1 post2
-= let e1 = Ghost.reveal e1 in
-  let e2 = FStar.Ghost.Pull.pull (fun (x:a) -> Ghost.reveal (e2 x)) in
-  Ghost.hide (A.bind_ghost e1 e2)
+    (#pre:slprop)
+    (#post:a -> slprop)
+    (e:stt_ghost a opens pre post)
+: stt_atomic (erased a) #Neutral opens pre (as_ghost_post post)
+= A.lift_erased (fun (x: erased (erased a)) -> reveal x) e
 
 let lift_ghost_neutral
     (#a:Type u#a)
@@ -215,7 +207,7 @@ let lift_ghost_neutral
     (e:stt_ghost a opens pre post)
     (reveal_a:non_informative_witness a)
 : stt_atomic a #Neutral opens pre post
-= Action.lift_erased reveal_a e
+= A.bind_ghost (lift_ghost_neutral' e) (fun x -> return #_ #_ #_ #post (reveal_a x))
 
 let lift_neutral_ghost
     (#a:Type u#a)
@@ -224,7 +216,22 @@ let lift_neutral_ghost
     (#post:a -> slprop)
     (e:stt_atomic a #Neutral opens pre post)
 : stt_ghost a opens pre post
-= Ghost.hide e
+= A.bind_ghost e fun x -> A.return #_ #_ #_ #(as_ghost_post post) (hide x)
+
+let return_ghost #a x p = lift_neutral_ghost (return_eq x)
+let return_ghost_noeq #a x p = lift_neutral_ghost (A.return x)
+
+let bind_ghost
+    (#a:Type u#a)
+    (#b:Type u#b)
+    (#opens:inames)
+    (#pre1:slprop)
+    (#post1:a -> slprop)
+    (#post2:b -> slprop)
+    (e1:stt_ghost a opens pre1 post1)
+    (e2:(x:a -> stt_ghost b opens (post1 x) post2))
+: stt_ghost b opens pre1 post2
+= A.bind_ghost e1 fun x -> lift_ghost_neutral' (e2 x)
 
 let frame_ghost
     (#a:Type u#a)
@@ -237,7 +244,7 @@ let frame_ghost
 = Ghost.hide (A.frame (Ghost.reveal e))
 
 let sub_ghost pre2 post2 pf1 pf2 e
-= Ghost.hide (A.sub pre2 post2 e)
+= Ghost.hide (A.sub pre2 (as_ghost_post post2) e)
 
 let sub_invs_stt_ghost
     (#a:Type u#a)
@@ -252,76 +259,73 @@ let sub_invs_stt_ghost
 
 let noop (p:slprop)
 : stt_ghost unit emp_inames p (fun _ -> p)
-= Ghost.hide (A.return #_ #_ #(fun _ -> p) ())
+= lift_neutral_ghost (A.return ())
 
 let intro_pure (p:prop) (pf:squash p)
 : stt_ghost unit emp_inames emp (fun _ -> pure p)
-= Ghost.hide (A.intro_pure p pf)
+= lift_neutral_ghost (A.intro_pure p pf)
 
 let elim_pure (p:prop)
 : stt_ghost (squash p) emp_inames (pure p) (fun _ -> emp)
-= Ghost.hide (A.elim_pure p)
+= lift_neutral_ghost (A.elim_pure p)
 
 let intro_exists (#a:Type u#a) (p:a -> slprop) (x:erased a)
 : stt_ghost unit emp_inames   (p x) (fun _ -> exists* x. p x)
-= Ghost.hide (A.intro_exists p x)
+= lift_neutral_ghost (A.intro_exists p x)
 
 let elim_exists (#a:Type u#a) (p:a -> slprop)
 : stt_ghost (erased a) emp_inames (exists* x. p x) (fun x -> p x)
-= Ghost.hide (A.elim_exists p)
+= lift_neutral_ghost (A.elim_exists p)
 
 let ghost_reveal (a:Type) (x:erased a)
 : stt_ghost a emp_inames emp (fun y -> pure (reveal x == y))
 = let m
     : stt_ghost a emp_inames
         (pure (reveal x == reveal x))
         (fun y -> pure (reveal x == y))
-    = Ghost.hide (A.return #_ #_ #(fun y -> pure (reveal x == y)) (reveal x))
+    = lift_neutral_ghost (A.return (reveal x))
   in
   pure_trivial (reveal x == reveal x) ();
   m
 
 
-let dup_inv (i:iref) (p:slprop) = A.dup_inv i p
+let dup_inv (i:iref) (p:slprop) = lift_neutral_ghost (A.dup_inv i p)
 
 let new_invariant (p:slprop)
 : stt_ghost iref emp_inames p (fun i -> inv i p)
-= A.new_invariant p
+= lift_neutral_ghost (A.new_invariant p)
 
-let fresh_invariant ctx p = A.fresh_invariant ctx p
+let fresh_invariant ctx p = lift_neutral_ghost (A.fresh_invariant ctx p)
 
-let inames_live_inv (i:iref) (p:slprop) = A.inames_live_inv i p
+let inames_live_inv (i:iref) (p:slprop) = lift_neutral_ghost (A.inames_live_inv i p)
 
 let with_invariant #a #fp #fp' #f_opens #p i $f =
   A.with_invariant i f
 
-let pull_up_ghost (#a #b:Type) (f:a -> GTot b) : GTot (g:(a -> b) {forall x. f x == g x }) =
-  FStar.Ghost.Pull.pull f
-
 let with_invariant_g #a #fp #fp' #f_opens #p i $f =
-  let f : unit -> stt_ghost a f_opens (later p ** fp) (fun x -> later p ** fp' x) = f in
-  let f : unit -> Ghost.erased (act a Ghost f_opens (later p ** fp) (fun x -> later p ** fp' x)) = f in
-  let g : unit -> GTot (act a Ghost f_opens (later p ** fp) (fun x -> later p ** fp' x)) =
-    fun () -> 
-    let r = f () in
-    Ghost.reveal r
-  in
-  let g : unit -> act a Ghost f_opens (later p ** fp) (fun x -> later p ** fp' x) = pull_up_ghost g in
-  A.with_invariant #a #Ghost #fp #fp' #f_opens #p i g
-
-let invariant_name_identifies_invariant p q i j = Ghost.hide (A.invariant_name_identifies_invariant p q i)
-let later_intro p = Ghost.hide (A.later_intro p)
-let later_elim p = Ghost.hide (A.later_elim p)
+  let f: act (erased a) Ghost f_opens (later p ** fp) (fun x -> later p ** fp' x) = f () in
+  A.with_invariant #(erased a) #Ghost #fp #(as_ghost_post fp') #f_opens #p i (fun _ -> f)
+
+let slprop_post_equiv_intro #t (#p #q: t->slprop) (h: (x:t -> squash (p x == q x))) : slprop_post_equiv p q =
+  IndefiniteDescription.elim_squash
+    (introduce forall x. slprop_equiv (p x) (q x) with
+      (h x; Squash.return_squash (slprop_equiv_refl (p x))))
+
+let invariant_name_identifies_invariant p q i j =
+  sub_ghost _ _ (slprop_equiv_refl _) (slprop_post_equiv_intro (fun x -> ()))
+    (lift_neutral_ghost (A.invariant_name_identifies_invariant p q i))
+let later_intro p = lift_neutral_ghost (A.later_intro p)
+let later_elim p = lift_neutral_ghost (A.later_elim p)
 let buy1 = A.buy1
 
-let pts_to_not_null #a #p r v = Ghost.hide (A.pts_to_not_null #a #p r v)
+let pts_to_not_null #a #p r v = lift_neutral_ghost (A.pts_to_not_null #a #p r v)
 let alloc #a #pcm x = A.alloc x
 let read r x f = A.read r x f
 let write r x y f = A.write r x y f
-let share #a #pcm r v0 v1 = Ghost.hide (A.share r v0 v1)
-let gather #a #pcm r v0 v1 = Ghost.hide (A.gather r v0 v1)
+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_alloc #a #pcm x = Ghost.hide <| A.ghost_alloc #a #pcm x
+let ghost_alloc #a #pcm x = lift_neutral_ghost <| A.ghost_alloc #a #pcm x
 let ghost_read
     (#a:Type)
     (#p:pcm a)
@@ -334,47 +338,47 @@ let ghost_read
     emp_inames
     (ghost_pts_to r x)
     (fun v -> ghost_pts_to r (f v))
-= Ghost.hide <| A.ghost_read r x f
+= lift_neutral_ghost <| A.ghost_read r x f
 
-let ghost_write r x y f = Ghost.hide (A.ghost_write r x y f)
-let ghost_share r v0 v1 = Ghost.hide (A.ghost_share r v0 v1)
-let ghost_gather r v0 v1 = Ghost.hide (A.ghost_gather r v0 v1) 
+let ghost_write r x y f = lift_neutral_ghost (A.ghost_write r x y f)
+let ghost_share r v0 v1 = lift_neutral_ghost (A.ghost_share r v0 v1)
+let ghost_gather r v0 v1 = lift_neutral_ghost (A.ghost_gather r v0 v1) 
 
-let big_pts_to_not_null #a #p r v = Ghost.hide (A.big_pts_to_not_null #a #p r v)
+let big_pts_to_not_null #a #p r v = lift_neutral_ghost (A.big_pts_to_not_null #a #p r v)
 let big_alloc #a #pcm x = A.big_alloc x
 let big_read r x f = A.big_read r x f
 let big_write r x y f = A.big_write r x y f
-let big_share #a #pcm r v0 v1 = Ghost.hide (A.big_share r v0 v1)
-let big_gather #a #pcm r v0 v1 = Ghost.hide (A.big_gather r v0 v1)
+let big_share #a #pcm r v0 v1 = lift_neutral_ghost (A.big_share r v0 v1)
+let big_gather #a #pcm r v0 v1 = lift_neutral_ghost (A.big_gather r v0 v1)
 
 
-let big_ghost_alloc #a #pcm x = Ghost.hide <| A.big_ghost_alloc #a #pcm x
-let big_ghost_read #a #p r x f = Ghost.hide <| A.big_ghost_read r x f
-let big_ghost_write r x y f = Ghost.hide (A.big_ghost_write r x y f)
-let big_ghost_share r v0 v1 = Ghost.hide (A.big_ghost_share r v0 v1)
-let big_ghost_gather r v0 v1 = Ghost.hide (A.big_ghost_gather r v0 v1) 
+let big_ghost_alloc #a #pcm x = lift_neutral_ghost <| A.big_ghost_alloc #a #pcm x
+let big_ghost_read #a #p r x f = lift_neutral_ghost <| A.big_ghost_read r x f
+let big_ghost_write r x y f = lift_neutral_ghost (A.big_ghost_write r x y f)
+let big_ghost_share r v0 v1 = lift_neutral_ghost (A.big_ghost_share r v0 v1)
+let big_ghost_gather r v0 v1 = lift_neutral_ghost (A.big_ghost_gather r v0 v1) 
 
-let nb_pts_to_not_null #a #p r v = Ghost.hide (A.nb_pts_to_not_null #a #p r v)
+let nb_pts_to_not_null #a #p r v = lift_neutral_ghost (A.nb_pts_to_not_null #a #p r v)
 let nb_alloc #a #pcm x = A.nb_alloc x
 let nb_read r x f = A.nb_read r x f
 let nb_write r x y f = A.nb_write r x y f
-let nb_share #a #pcm r v0 v1 = Ghost.hide (A.nb_share r v0 v1)
-let nb_gather #a #pcm r v0 v1 = Ghost.hide (A.nb_gather r v0 v1)
+let nb_share #a #pcm r v0 v1 = lift_neutral_ghost (A.nb_share r v0 v1)
+let nb_gather #a #pcm r v0 v1 = lift_neutral_ghost (A.nb_gather r v0 v1)
 
 
-let nb_ghost_alloc #a #pcm x = Ghost.hide <| A.nb_ghost_alloc #a #pcm x
-let nb_ghost_read #a #p r x f = Ghost.hide <| A.nb_ghost_read r x f
-let nb_ghost_write r x y f = Ghost.hide (A.nb_ghost_write r x y f)
-let nb_ghost_share r v0 v1 = Ghost.hide (A.nb_ghost_share r v0 v1)
-let nb_ghost_gather r v0 v1 = Ghost.hide (A.nb_ghost_gather r v0 v1) 
+let nb_ghost_alloc #a #pcm x = lift_neutral_ghost <| A.nb_ghost_alloc #a #pcm x
+let nb_ghost_read #a #p r x f = lift_neutral_ghost <| A.nb_ghost_read r x f
+let nb_ghost_write r x y f = lift_neutral_ghost (A.nb_ghost_write r x y f)
+let nb_ghost_share r v0 v1 = lift_neutral_ghost (A.nb_ghost_share r v0 v1)
+let nb_ghost_gather r v0 v1 = lift_neutral_ghost (A.nb_ghost_gather r v0 v1) 
 
-let drop p = Ghost.hide (A.drop p)
+let drop p = lift_neutral_ghost (A.drop p)
 
-let equiv_refl a = Ghost.hide (A.equiv_refl a)
-let equiv_dup a b = Ghost.hide (A.equiv_dup a b)
-let equiv_trans (a b c:slprop) = Ghost.hide (A.equiv_trans a b c)
-let equiv_elim (a b:slprop) = Ghost.hide (A.equiv_elim a b)
+let equiv_refl a = lift_neutral_ghost (A.equiv_refl a)
+let equiv_dup a b = lift_neutral_ghost (A.equiv_dup a b)
+let equiv_trans (a b c:slprop) = lift_neutral_ghost (A.equiv_trans a b c)
+let equiv_elim (a b:slprop) = lift_neutral_ghost (A.equiv_elim a b)
 
-let slprop_ref_alloc y = Ghost.hide (A.slprop_ref_alloc y)
-let slprop_ref_share x y = Ghost.hide (A.slprop_ref_share x y)
-let slprop_ref_gather x y1 y2 = Ghost.hide (A.slprop_ref_gather x y1 y2)
+let slprop_ref_alloc y = lift_neutral_ghost (A.slprop_ref_alloc y)
+let slprop_ref_share x y = lift_neutral_ghost (A.slprop_ref_share x y)
+let slprop_ref_gather x y1 y2 = lift_neutral_ghost (A.slprop_ref_gather x y1 y2)

lib/core/PulseCore.Atomic.fsti

@@ -140,6 +140,9 @@ val sub_invs_stt_atomic
     (_ : squash (inames_subset opens1 opens2))
 : stt_atomic a #obs opens2 pre post
 
+let as_ghost_post #t (post: t->slprop) : erased t -> slprop =
+  fun x -> post (reveal x)
+
 (* stt_ghost a opens pre post: The type of a pulse computation
    that when run in a state satisfying `pre`
    takes a single ghost atomic step (i.e. a step that does not modify the heap, and does not get extracted)
@@ -154,6 +157,34 @@ val stt_ghost
     (post:a -> slprop)
 : Type u#(max 4 a)
 
+type non_informative_witness (a:Type u#a) =
+  x:Ghost.erased a -> y:a{y == Ghost.reveal x}
+
+val lift_ghost_neutral'
+    (#a:Type u#a)
+    (#opens:inames)
+    (#pre:slprop)
+    (#post:a -> slprop)
+    (e:stt_ghost a opens pre post)
+: stt_atomic (erased a) #Neutral opens pre (as_ghost_post post)
+
+val lift_ghost_neutral
+    (#a:Type u#a)
+    (#opens:inames)
+    (#pre:slprop)
+    (#post:a -> slprop)
+    (e:stt_ghost a opens pre post)
+    (reveal_a:non_informative_witness a)
+: stt_atomic a #Neutral opens pre post
+
+val lift_neutral_ghost
+    (#a:Type u#a)
+    (#opens:inames)
+    (#pre:slprop)
+    (#post:a -> slprop)
+    (e:stt_atomic a #Neutral opens pre post)
+: stt_ghost a opens pre post
+
 val return_ghost
     (#a:Type u#a)
     (x:a)
@@ -177,26 +208,6 @@ val bind_ghost
     (e2:(x:a -> stt_ghost b opens (post1 x) post2))
 : stt_ghost b opens pre1 post2
 
-type non_informative_witness (a:Type u#a) =
-  x:Ghost.erased a -> y:a{y == Ghost.reveal x}
-
-val lift_ghost_neutral
-    (#a:Type u#a)
-    (#opens:inames)
-    (#pre:slprop)
-    (#post:a -> slprop)
-    (e:stt_ghost a opens pre post)
-    (reveal_a:non_informative_witness a)
-: stt_atomic a #Neutral opens pre post
-
-val lift_neutral_ghost
-    (#a:Type u#a)
-    (#opens:inames)
-    (#pre:slprop)
-    (#post:a -> slprop)
-    (e:stt_atomic a #Neutral opens pre post)
-: stt_ghost a opens pre post
-
 val frame_ghost
     (#a:Type u#a)
     (#opens:inames)