Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove FStar.Ghost.Pull #291

Merged
merged 3 commits into from
Jan 7, 2025
Merged

Remove FStar.Ghost.Pull #291

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d9f1a89
Remove FStar.Ghost.Pull
gebner Dec 17, 2024
30ab2ab
Merge branch 'main' into gebner_rm_ghost_pull
gebner Jan 7, 2025
9f39174
Merge branch 'main' into gebner_rm_ghost_pull
gebner Jan 7, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion lib/core/PulseCore.Action.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion lib/core/PulseCore.Action.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
160 changes: 82 additions & 78 deletions lib/core/PulseCore.Atomic.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
51 changes: 31 additions & 20 deletions lib/core/PulseCore.Atomic.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down
Loading
Loading