Skip to content

Commit 06b1ed3

Browse files
gebnergebner
committed
Add impersonate combinators.
1 parent e2f6b68 commit 06b1ed3

File tree

4 files changed

+130
-0
lines changed

4 files changed

+130
-0
lines changed

‎lib/common/Pulse.Lib.Core.fsti‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -459,6 +459,23 @@ val on_star_eq l a b : squash (on l (a ** b) == on l a ** on l b)
459459
val on_on_eq l1 l2 a : squash (on l1 (on l2 a) == on l2 a)
460460
val on_loc_eq l1 l2 : squash (on l1 (loc l2) == pure (l1 == l2))
461461

462+
inline_for_extraction
463+
[@@deprecated "impersonate_core is unsound; only use for model implementations";
464+
extract_as (`(fun (#a:Type0) () () () (f: unit -> Dv a) -> f ()))]
465+
val impersonate_core #a
466+
(l: loc_id) (pre: slprop) (post: a -> slprop)
467+
(f: unit -> stt a pre (fun x -> post x))
468+
: stt a (on l pre) (fun x -> on l (post x))
469+
470+
inline_for_extraction
471+
[@@deprecated "atomic impersonate_core is unsound; only use for model implementations";
472+
extract_as (`(fun (#a:Type0) () () () () () (f: unit -> Dv a) -> f ()))]
473+
val atomic_impersonate_core #a
474+
(#[T.exact (`emp_inames)] is: inames) #obs
475+
(l: loc_id) (pre: slprop) (post: a -> slprop)
476+
(f: unit -> stt_atomic a #obs is pre (fun x -> post x))
477+
: stt_atomic a #obs is (on l pre) (fun x -> on l (post x))
478+
462479
val ghost_impersonate_core
463480
(#[T.exact (`emp_inames)] is: inames)
464481
(l: loc_id) (pre post: slprop)

‎lib/core/Pulse.Lib.Core.fst‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,8 @@ let on_star_eq = Sep.on_star_eq
202202
let on_on_eq = Sep.on_on_eq
203203
let on_loc_eq = Sep.on_loc_eq
204204

205+
let impersonate_core l pre post f = PulseCore.Action.impersonate_stt l (f ())
206+
let atomic_impersonate_core l pre post f = A.impersonate_atomic l (f ())
205207
let ghost_impersonate_core l pre post f = A.impersonate_ghost l (f ())
206208

207209
//////////////////////////////////////////////////////////////////////////

‎lib/pulse/lib/Pulse.Lib.Send.fst‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,79 @@ ghost fn placeless_on (l: loc_id) (p: slprop) : placeless (on l p) = l1 l2 {
5252
on_on_eq l2 l p; rewrite on l p as on l2 (on l p);
5353
}
5454

55+
[@@deprecated "impersonate is unsound; only use for model implementations"]
56+
noextract inline_for_extraction
57+
fn impersonate
58+
u#a (a: Type u#a)
59+
(l: loc_id) (pre: slprop) (post: a -> slprop)
60+
{| placeless pre, ((x:a) -> placeless (post x)) |}
61+
(f: unit -> stt a (loc l ** pre) (fun x -> loc l ** post x))
62+
requires pre
63+
returns x: a
64+
ensures post x
65+
{
66+
on_loc_eq l l; rewrite pure (l == l) as on l (loc l);
67+
placeless_on_intro pre l;
68+
on_star_eq l (loc l) pre; rewrite on l (loc l) ** on l pre as on l (loc l ** pre);
69+
let x = impersonate_core l (loc l ** pre) post fn _ {
70+
let x = f ();
71+
drop_ (loc l);
72+
x
73+
};
74+
placeless_on_elim (post x) l;
75+
x
76+
}
77+
78+
[@@deprecated "atomic_impersonate is unsound; only use for model implementations"]
79+
noextract inline_for_extraction
80+
atomic fn atomic_impersonate
81+
u#a (a: Type u#a)
82+
(#[T.exact (`emp_inames)] is: inames)
83+
(l: loc_id) (pre: slprop) (post: a -> slprop)
84+
{| placeless pre, ((x:a) -> placeless (post x)) |}
85+
(f: unit -> stt_atomic a is (loc l ** pre) (fun x -> loc l ** post x))
86+
opens is
87+
requires pre
88+
returns x: a
89+
ensures post x
90+
{
91+
on_loc_eq l l; rewrite pure (l == l) as on l (loc l);
92+
placeless_on_intro pre l;
93+
on_star_eq l (loc l) pre; rewrite on l (loc l) ** on l pre as on l (loc l ** pre);
94+
let x = atomic_impersonate_core #a #is #Observable l (loc l ** pre) post fn _ {
95+
let x = f ();
96+
drop_ (loc l);
97+
x
98+
};
99+
placeless_on_elim (post x) l;
100+
x
101+
}
102+
103+
[@@deprecated "unobservable_impersonate is unsound; only use for model implementations"]
104+
noextract inline_for_extraction
105+
unobservable fn unobservable_impersonate
106+
u#a (a: Type u#a)
107+
(#[T.exact (`emp_inames)] is: inames)
108+
(l: loc_id) (pre: slprop) (post: a -> slprop)
109+
{| placeless pre, ((x:a) -> placeless (post x)) |}
110+
(f: unit -> stt_atomic a #Neutral is (loc l ** pre) (fun x -> loc l ** post x))
111+
opens is
112+
requires pre
113+
returns x: a
114+
ensures post x
115+
{
116+
on_loc_eq l l; rewrite pure (l == l) as on l (loc l);
117+
placeless_on_intro pre l;
118+
on_star_eq l (loc l) pre; rewrite on l (loc l) ** on l pre as on l (loc l ** pre);
119+
let x = atomic_impersonate_core #a #is #Neutral l (loc l ** pre) post fn _ {
120+
let x = f ();
121+
drop_ (loc l);
122+
x
123+
};
124+
placeless_on_elim (post x) l;
125+
x
126+
}
127+
55128
ghost fn ghost_impersonate
56129
(#[T.exact (`emp_inames)] is: inames)
57130
(l: loc_id) (pre post: slprop) {| placeless pre, placeless post |}

‎lib/pulse/lib/Pulse.Lib.Send.fsti‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
module Pulse.Lib.Send
1818
open Pulse.Lib.Core
1919
open Pulse.Class.Duplicable
20+
open PulseCore.Observability
2021
open Pulse.Main
2122
module T = FStar.Tactics.V2
2223
#lang-pulse
@@ -31,6 +32,43 @@ irreducible let anywhere (l: loc_id) = ()
3132
type placeless (p: slprop) =
3233
is_send_across anywhere p
3334

35+
[@@deprecated "impersonate is unsound; only use for model implementations"]
36+
noextract inline_for_extraction
37+
fn impersonate
38+
u#a (a: Type u#a)
39+
(l: loc_id) (pre: slprop) (post: a -> slprop)
40+
{| placeless pre, ((x:a) -> placeless (post x)) |}
41+
(f: unit -> stt a (loc l ** pre) (fun x -> loc l ** post x))
42+
requires pre
43+
returns x: a
44+
ensures post x
45+
46+
[@@deprecated "atomic_impersonate is unsound; only use for model implementations"]
47+
noextract inline_for_extraction
48+
atomic fn atomic_impersonate
49+
u#a (a: Type u#a)
50+
(#[T.exact (`emp_inames)] is: inames)
51+
(l: loc_id) (pre: slprop) (post: a -> slprop)
52+
{| placeless pre, ((x:a) -> placeless (post x)) |}
53+
(f: unit -> stt_atomic a is (loc l ** pre) (fun x -> loc l ** post x))
54+
opens is
55+
requires pre
56+
returns x: a
57+
ensures post x
58+
59+
[@@deprecated "unobservable_impersonate is unsound; only use for model implementations"]
60+
noextract inline_for_extraction
61+
unobservable fn unobservable_impersonate
62+
u#a (a: Type u#a)
63+
(#[T.exact (`emp_inames)] is: inames)
64+
(l: loc_id) (pre: slprop) (post: a -> slprop)
65+
{| placeless pre, ((x:a) -> placeless (post x)) |}
66+
(f: unit -> stt_atomic a #Neutral is (loc l ** pre) (fun x -> loc l ** post x))
67+
opens is
68+
requires pre
69+
returns x: a
70+
ensures post x
71+
3472
ghost fn ghost_impersonate
3573
(#[T.exact (`emp_inames)] is: inames)
3674
(l: loc_id) (pre post: slprop) {| placeless pre, placeless post |}

0 commit comments

Comments
 (0)