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

Ghost functions have a model supporting their erasure #10

Merged
merged 20 commits into from
Feb 29, 2024
Merged

Ghost functions have a model supporting their erasure #10

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
8606ec9
wip, adding an erased heap
nikswamy Feb 27, 2024
def8e24
refine actions, and provide heap extension as an action with pre & po…
nikswamy Feb 28, 2024
1afe5ca
checkpoint; provide heap interface for heap2
nikswamy Feb 28, 2024
7ee821b
cleanup straggling admits
nikswamy Feb 28, 2024
6eecb69
a type of ghost actions
nikswamy Feb 28, 2024
0e3f763
erased non-informative ghost actions can be unerased
nikswamy Feb 28, 2024
a5ad38c
checkpoint; implementing ghost refs
nikswamy Feb 28, 2024
fd13aaa
some genericity with lenses
nikswamy Feb 28, 2024
57c8a1a
ghost interface to heap2
nikswamy Feb 28, 2024
ecc5392
fix up a mis-naming in Heap; add a typeclass for HeapLike
nikswamy Feb 28, 2024
35a4a09
restore PulseCore.Memory, except for alloc_action
nikswamy Feb 28, 2024
814cff0
restore alloc_action
nikswamy Feb 28, 2024
976e47f
add a ghost allocation counter
nikswamy Feb 28, 2024
9774f22
separate ghost actions
nikswamy Feb 28, 2024
d5b2faf
expose more ghost actions in memory
nikswamy Feb 28, 2024
524d3dd
implement ghost_alloc
nikswamy Feb 28, 2024
76c37dc
propagating ghost to PulseCore.Action
nikswamy Feb 29, 2024
70a4e8f
erased ghost actions in PulseCore.Action
nikswamy Feb 29, 2024
8631125
remove axiom about lifting stt_ghost to stt_atomic neutral
nikswamy Feb 29, 2024
4e73180
removing ghost_witness/ghost_recall
nikswamy Feb 29, 2024
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
129 changes: 100 additions & 29 deletions lib/pulse/core/PulseCore.Action.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,17 +91,29 @@ let stt_of_action2 (#a:Type u#2) #pre #post (m:action a Set.empty pre post)

let iname = iname

let maybe_ghost (r:reifiability { r =!= UsesInvariants}) =
match r with
| Ghost -> true
| _ -> false

let pre_act
(a:Type u#a)
(r:reifiability)
(opens:inames)
(pre:slprop)
(post:a -> slprop)
= match r with
| Reifiable ->
Mem.pst_action_except a opens pre post
| _ ->
| UsesInvariants ->
Mem.action_except a opens pre post
| _ ->
Mem._pst_action_except a (maybe_ghost r) opens pre post

let force
#a (#r:reifiability { r =!= UsesInvariants})
(#opens:inames) (#pre:slprop) (#post:a -> slprop)
(f:pre_act a r opens pre post)
: Mem._pst_action_except a (maybe_ghost r) opens pre post
= f

let mem_action_as_action
(#a:Type u#a)
Expand Down Expand Up @@ -135,8 +147,8 @@ let action_of_pre_act
(f:pre_act a r opens pre post)
: action a opens pre post
= match r with
| Reifiable -> mem_pst_action_as_action f
| _ -> mem_action_as_action f
| UsesInvariants -> mem_action_as_action f
| _ -> mem_pst_action_as_action f

let act
(a:Type u#a)
Expand All @@ -147,14 +159,27 @@ let act
: Type u#(max a 2)
= #ictx:inames_disj opens ->
pre_act a r ictx pre post

let return_pre_act
(#a:Type u#a)
(#except:inames)
(#post:a -> slprop)
(x:a)
: pre_act a Reifiable except (post x) post
= fun frame m0 -> x, m0
: pre_act a Ghost except (post x) post
= Mem.ghost_action_preorder ();
fun frame m0 -> x, m0

let bind_pre_act_ghost
(#a:Type u#a)
(#b:Type u#b)
(#except:inames)
(#pre1 #post1 #post2:_)
(f:pre_act a Ghost except pre1 post1)
(g:(x:a -> pre_act b Ghost except (post1 x) post2))
: pre_act b Ghost except pre1 post2
= Mem.ghost_action_preorder ();
fun frame ->
PST.weaken (PST.bind (f frame) (fun x -> g x frame))

let bind_pre_act_reifiable
(#a:Type u#a)
Expand Down Expand Up @@ -189,11 +214,21 @@ let bind_pre_act
(g:(x:a -> pre_act b r except (post1 x) post2))
: pre_act b r except pre1 post2
= match r with
| Ghost ->
bind_pre_act_ghost #a #b #except #pre1 #post1 #post2 f g
| Reifiable ->
bind_pre_act_reifiable #a #b #except #pre1 #post1 #post2 f g
| UsesInvariants ->
bind_pre_act_non_reifiable #a #b #except #pre1 #post1 #post2 f g

let frame_pre_act_ghost
(#a:Type u#a)
(#except:inames)
(#pre #post #frame:_)
(f:pre_act a Ghost except pre post)
: pre_act a Ghost except (pre `star` frame) (fun x -> post x `star` frame)
= fun frame' -> f (frame `star` frame')

let frame_pre_act_reifiable
(#a:Type u#a)
(#except:inames)
Expand All @@ -218,9 +253,18 @@ let frame_pre_act
(f:pre_act a r except pre post)
: pre_act a r except (pre `star` frame) (fun x -> post x `star` frame)
= match r with
| Ghost -> frame_pre_act_ghost #a #except #pre #post #frame f
| Reifiable -> frame_pre_act_reifiable #a #except #pre #post #frame f
| _ -> frame_pre_act_non_reifiable #a #except #pre #post #frame f

let lift_pre_act_ghost
(#a:Type u#a)
(#except:inames)
(#pre #post:_)
(f:pre_act a Ghost except pre post)
: pre_act a Reifiable except pre post
= f

let lift_pre_act_reifiablity
(#a:Type u#a)
(#r:_)
Expand All @@ -245,6 +289,7 @@ let return
= fun #ictx ->
let m = return_pre_act #a #ictx #post x in
match r with
| Ghost -> m
| Reifiable -> m
| _ -> lift_pre_act_reifiablity m

Expand All @@ -268,6 +313,15 @@ let frame
: act a r opens (pre `star` frame) (fun x -> post x `star` frame)
= fun #ictx -> frame_pre_act (f #ictx)

let lift_ghost_reifiable
(#a:Type)
(#pre:slprop)
(#post:a -> slprop)
(#opens:inames)
(f:act a Ghost opens pre post)
: act a Reifiable opens pre post
= fun #ictx -> lift_pre_act_ghost (f #ictx)

let lift_reifiability
(#a:Type)
(#r:_)
Expand All @@ -286,22 +340,25 @@ let weaken
(#opens opens':inames)
(f:act a r0 opens pre post)
: act a (r0 ^^ r1) (Set.union opens opens') pre post
= match r0 with
| UsesInvariants -> f
| _ ->
match r1 with
| Reifiable -> f
| _ -> lift_reifiability f
= if r0 = r1 then f
else (
match r0, r1 with
| UsesInvariants, _ -> f
| _, UsesInvariants -> lift_reifiability f
| Reifiable, Ghost -> f
| Ghost, Reifiable -> lift_ghost_reifiable #a #pre #post #opens f
)

let sub_pre_act_reifiable
(#a:Type)
(#r:reifiability { r =!= UsesInvariants})
(#pre:slprop)
(#post:a -> slprop)
(#opens:inames)
(pre':slprop { slprop_equiv pre pre' })
(post':a -> slprop { forall x. slprop_equiv (post x) (post' x) })
(f:pre_act a Reifiable opens pre post)
: pre_act a Reifiable opens pre' post'
(f:pre_act a r opens pre post)
: pre_act a r opens pre' post'
= I.slprop_equiv_elim pre pre';
introduce forall x. post x == post' x
with I.slprop_equiv_elim (post x) (post' x);
Expand Down Expand Up @@ -332,10 +389,10 @@ let sub
(f:act a r opens pre post)
: act a r opens pre' post'
= match r with
| Reifiable ->
fun #ictx -> sub_pre_act_reifiable #a #pre #post #ictx pre' post' (f #ictx)
| _ ->
| UsesInvariants ->
fun #ictx -> sub_pre_act_non_reifiable #a #pre #post #ictx pre' post' (f #ictx)
| _ ->
fun #ictx -> sub_pre_act_reifiable #a #r #pre #post #ictx pre' post' (f #ictx)

let action_of_act
(#a:Type)
Expand Down Expand Up @@ -420,7 +477,7 @@ let invariant_name_identifies_invariant
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 pts_to = pts_to
let pts_to = Mem.pts_to
let pts_to_not_null #a #p r v #ictx = pts_to_not_null_action ictx r v

let alloc
Expand Down Expand Up @@ -465,7 +522,7 @@ let share
(v0:FStar.Ghost.erased a)
(v1:FStar.Ghost.erased a{composable pcm v0 v1})
: act unit
Reifiable
Ghost
emp_inames
(pts_to r (v0 `op pcm` v1))
(fun _ -> pts_to r v0 `star` pts_to r v1)
Expand All @@ -478,7 +535,7 @@ let gather
(v0:FStar.Ghost.erased a)
(v1:FStar.Ghost.erased a)
: act (squash (composable pcm v0 v1))
Reifiable
Ghost
emp_inames
(pts_to r v0 `star` pts_to r v1)
(fun _ -> pts_to r (op pcm v0 v1))
Expand Down Expand Up @@ -522,11 +579,11 @@ let pure_true ()
coerce_eq () <| slprop_equiv_refl (pure True)

let intro_pure (p:prop) (pf:squash p)
: act unit Reifiable emp_inames emp (fun _ -> pure p)
: act unit Ghost emp_inames emp (fun _ -> pure p)
= fun #ictx -> intro_pure #ictx p pf

let elim_pure (p:prop)
: act (squash p) Reifiable emp_inames (pure p) (fun _ -> emp)
: act (squash p) Ghost emp_inames (pure p) (fun _ -> emp)
= fun #ictx -> elim_pure #ictx p

///////////////////////////////////////////////////////////////////
Expand All @@ -542,23 +599,37 @@ let exists_equiv (#a:_) (#p:a -> slprop)
let thunk (p:slprop) = fun (_:unit) -> p

let intro_exists' (#a:Type u#a) (p:a -> slprop) (x:erased a)
: act unit Reifiable emp_inames (p x) (thunk (op_exists_Star p))
: act unit Ghost emp_inames (p x) (thunk (op_exists_Star p))
= fun #ictx -> intro_exists #ictx (F.on_dom a p) x

let intro_exists'' (#a:Type u#a) (p:a -> slprop) (x:erased a)
: act unit Reifiable emp_inames (p x) (thunk (exists* x. p x))
: act unit Ghost emp_inames (p x) (thunk (exists* x. p x))
= coerce_eq (exists_equiv #a #p) (intro_exists' #a p x)

let intro_exists (#a:Type u#a) (p:a -> slprop) (x:erased a)
: act unit Reifiable emp_inames (p x) (fun _ -> exists* x. p x)
: act unit Ghost emp_inames (p x) (fun _ -> exists* x. p x)
= intro_exists'' p x

let elim_exists' (#a:Type u#a) (p:a -> slprop)
: act (erased a) Reifiable emp_inames (op_exists_Star p) (fun x -> p x)
: act (erased a) Ghost emp_inames (op_exists_Star p) (fun x -> p x)
= fun #ictx -> witness_h_exists #ictx (F.on_dom a p)

let elim_exists (#a:Type u#a) (p:a -> slprop)
: act (erased a) Reifiable emp_inames (exists* x. p x) (fun x -> p x)
: act (erased a) Ghost emp_inames (exists* x. p x) (fun x -> p x)
= coerce_eq (exists_equiv #a #p) (elim_exists' #a p)

let drop p = fun #ictx -> drop #ictx p

let ghost_ref = Mem.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
let ghost_write #a #p r x y f = fun #ictx -> ghost_write #ictx #a #p r x y f
let ghost_share #a #pcm r v0 v1 = fun #ictx -> ghost_share #ictx #a #pcm r v0 v1
let ghost_gather #a #pcm r v0 v1 = fun #ictx -> ghost_gather #ictx #a #pcm r v0 v1
let lift_erased #a ni_a #opens #pre #post f =
fun #ictx ->
let f : erased (pre_act a Ghost ictx pre post) =
hide (reveal f #ictx)
in
lift_ghost #a #ictx #pre #post ni_a f
Loading
Loading