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 1 commit
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
26 changes: 0 additions & 26 deletions lib/pulse/core/PulseCore.Atomic.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -302,30 +302,4 @@ let ghost_read
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_witnessed
(#a:Type u#1)
(#p:pcm a)
(r:ghost_ref p)
(f:property a)
= admit() //witnessed (reveal r) f

let ghost_witness
(#a:Type)
(#pcm:pcm a)
(r:ghost_ref pcm)
(fact:stable_property pcm)
(v:Ghost.erased a)
(pf:squash (forall z. compatible pcm v z ==> fact z))
= admit() //A.witness r fact v pf

let ghost_recall
(#a:Type u#1)
(#pcm:pcm a)
(#fact:property a)
(r:ghost_ref pcm)
(v:Ghost.erased a)
(w:ghost_witnessed r fact)
= admit() //A.recall r v w

let drop p = Ghost.hide (A.drop p)
64 changes: 33 additions & 31 deletions lib/pulse/core/PulseCore.Atomic.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -401,37 +401,39 @@ val ghost_gather
(ghost_pts_to r v0 ** ghost_pts_to r v1)
(fun _ -> ghost_pts_to r (op pcm v0 v1))

val ghost_witnessed
(#a:Type u#1)
(#p:pcm a)
(r:ghost_ref p)
(f:property a)
: Type0

val ghost_witness
(#a:Type)
(#pcm:pcm a)
(r:ghost_ref pcm)
(fact:stable_property pcm)
(v:Ghost.erased a)
(pf:squash (forall z. compatible pcm v z ==> fact z))
: stt_atomic
(ghost_witnessed r fact)
#Unobservable emp_inames
(ghost_pts_to r v)
(fun _ -> ghost_pts_to r v)

val ghost_recall
(#a:Type u#1)
(#pcm:pcm a)
(#fact:property a)
(r:ghost_ref pcm)
(v:Ghost.erased a)
(w:ghost_witnessed r fact)
: stt_atomic (v1:Ghost.erased a{compatible pcm v v1})
#Unobservable emp_inames
(ghost_pts_to r v)
(fun v1 -> ghost_pts_to r v ** pure (fact v1))
// Unused?
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are unused, but @mtzguido tells me that they are expected to be required soon. I will restore them in a follow-up PR.


// val ghost_witnessed
// (#a:Type u#1)
// (#p:pcm a)
// (r:ghost_ref p)
// (f:property a)
// : Type0

// val ghost_witness
// (#a:Type)
// (#pcm:pcm a)
// (r:ghost_ref pcm)
// (fact:stable_property pcm)
// (v:Ghost.erased a)
// (pf:squash (forall z. compatible pcm v z ==> fact z))
// : stt_atomic
// (ghost_witnessed r fact)
// #Unobservable emp_inames
// (ghost_pts_to r v)
// (fun _ -> ghost_pts_to r v)

// val ghost_recall
// (#a:Type u#1)
// (#pcm:pcm a)
// (#fact:property a)
// (r:ghost_ref pcm)
// (v:Ghost.erased a)
// (w:ghost_witnessed r fact)
// : stt_atomic (v1:Ghost.erased a{compatible pcm v v1})
// #Unobservable emp_inames
// (ghost_pts_to r v)
// (fun v1 -> ghost_pts_to r v ** pure (fact v1))

val drop (p:slprop)
: stt_ghost unit p (fun _ -> emp)
Loading