Skip to content

Commit c9fbaa3

Browse files
gebnergebner
committed
Add impersonate combinators.
1 parent bb4ad6b commit c9fbaa3

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.SendSync.fst‎

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

39+
[@@deprecated "impersonate is unsound; only use for model implementations"]
40+
noextract inline_for_extraction
41+
fn impersonate
42+
u#a (a: Type u#a)
43+
(l: loc_id) (pre: slprop) (post: a -> slprop)
44+
{| placeless pre, ((x:a) -> placeless (post x)) |}
45+
(f: unit -> stt a (loc l ** pre) (fun x -> loc l ** post x))
46+
requires pre
47+
returns x: a
48+
ensures post x
49+
{
50+
on_loc_eq l l; rewrite pure (l == l) as on l (loc l);
51+
placeless_on_intro pre l;
52+
on_star_eq l (loc l) pre; rewrite on l (loc l) ** on l pre as on l (loc l ** pre);
53+
let x = impersonate_core l (loc l ** pre) post fn _ {
54+
let x = f ();
55+
drop_ (loc l);
56+
x
57+
};
58+
placeless_on_elim (post x) l;
59+
x
60+
}
61+
62+
[@@deprecated "atomic_impersonate is unsound; only use for model implementations"]
63+
noextract inline_for_extraction
64+
atomic fn atomic_impersonate
65+
u#a (a: Type u#a)
66+
(#[T.exact (`emp_inames)] is: inames)
67+
(l: loc_id) (pre: slprop) (post: a -> slprop)
68+
{| placeless pre, ((x:a) -> placeless (post x)) |}
69+
(f: unit -> stt_atomic a is (loc l ** pre) (fun x -> loc l ** post x))
70+
opens is
71+
requires pre
72+
returns x: a
73+
ensures post x
74+
{
75+
on_loc_eq l l; rewrite pure (l == l) as on l (loc l);
76+
placeless_on_intro pre l;
77+
on_star_eq l (loc l) pre; rewrite on l (loc l) ** on l pre as on l (loc l ** pre);
78+
let x = atomic_impersonate_core #a #is #Observable l (loc l ** pre) post fn _ {
79+
let x = f ();
80+
drop_ (loc l);
81+
x
82+
};
83+
placeless_on_elim (post x) l;
84+
x
85+
}
86+
87+
[@@deprecated "unobservable_impersonate is unsound; only use for model implementations"]
88+
noextract inline_for_extraction
89+
unobservable fn unobservable_impersonate
90+
u#a (a: Type u#a)
91+
(#[T.exact (`emp_inames)] is: inames)
92+
(l: loc_id) (pre: slprop) (post: a -> slprop)
93+
{| placeless pre, ((x:a) -> placeless (post x)) |}
94+
(f: unit -> stt_atomic a #Neutral is (loc l ** pre) (fun x -> loc l ** post x))
95+
opens is
96+
requires pre
97+
returns x: a
98+
ensures post x
99+
{
100+
on_loc_eq l l; rewrite pure (l == l) as on l (loc l);
101+
placeless_on_intro pre l;
102+
on_star_eq l (loc l) pre; rewrite on l (loc l) ** on l pre as on l (loc l ** pre);
103+
let x = atomic_impersonate_core #a #is #Neutral l (loc l ** pre) post fn _ {
104+
let x = f ();
105+
drop_ (loc l);
106+
x
107+
};
108+
placeless_on_elim (post x) l;
109+
x
110+
}
111+
39112
ghost fn ghost_impersonate
40113
(#[T.exact (`emp_inames)] is: inames)
41114
(l: loc_id) (pre post: slprop) {| placeless pre, placeless post |}

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

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
module Pulse.Lib.SendSync
22
open Pulse.Lib.Core
33
open Pulse.Class.Duplicable
4+
open PulseCore.Observability
45
open Pulse.Main
56
module T = FStar.Tactics.V2
67
#lang-pulse
@@ -15,6 +16,43 @@ irreducible let anywhere (l: loc_id) = ()
1516
type placeless (p: slprop) =
1617
is_send_across anywhere p
1718

19+
[@@deprecated "impersonate is unsound; only use for model implementations"]
20+
noextract inline_for_extraction
21+
fn impersonate
22+
u#a (a: Type u#a)
23+
(l: loc_id) (pre: slprop) (post: a -> slprop)
24+
{| placeless pre, ((x:a) -> placeless (post x)) |}
25+
(f: unit -> stt a (loc l ** pre) (fun x -> loc l ** post x))
26+
requires pre
27+
returns x: a
28+
ensures post x
29+
30+
[@@deprecated "atomic_impersonate is unsound; only use for model implementations"]
31+
noextract inline_for_extraction
32+
atomic fn atomic_impersonate
33+
u#a (a: Type u#a)
34+
(#[T.exact (`emp_inames)] is: inames)
35+
(l: loc_id) (pre: slprop) (post: a -> slprop)
36+
{| placeless pre, ((x:a) -> placeless (post x)) |}
37+
(f: unit -> stt_atomic a is (loc l ** pre) (fun x -> loc l ** post x))
38+
opens is
39+
requires pre
40+
returns x: a
41+
ensures post x
42+
43+
[@@deprecated "unobservable_impersonate is unsound; only use for model implementations"]
44+
noextract inline_for_extraction
45+
unobservable fn unobservable_impersonate
46+
u#a (a: Type u#a)
47+
(#[T.exact (`emp_inames)] is: inames)
48+
(l: loc_id) (pre: slprop) (post: a -> slprop)
49+
{| placeless pre, ((x:a) -> placeless (post x)) |}
50+
(f: unit -> stt_atomic a #Neutral is (loc l ** pre) (fun x -> loc l ** post x))
51+
opens is
52+
requires pre
53+
returns x: a
54+
ensures post x
55+
1856
ghost fn ghost_impersonate
1957
(#[T.exact (`emp_inames)] is: inames)
2058
(l: loc_id) (pre post: slprop) {| placeless pre, placeless post |}

0 commit comments

Comments
 (0)