diff --git a/lib/pulse/core/PulseCore.Action.fst b/lib/pulse/core/PulseCore.Action.fst index 3b1597c08..5be2a85ec 100644 --- a/lib/pulse/core/PulseCore.Action.fst +++ b/lib/pulse/core/PulseCore.Action.fst @@ -91,6 +91,11 @@ 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) @@ -98,10 +103,17 @@ let pre_act (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) @@ -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) @@ -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) @@ -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) @@ -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:_) @@ -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 @@ -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:_) @@ -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); @@ -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) @@ -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 @@ -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) @@ -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)) @@ -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 /////////////////////////////////////////////////////////////////// @@ -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 \ No newline at end of file diff --git a/lib/pulse/core/PulseCore.Action.fsti b/lib/pulse/core/PulseCore.Action.fsti index aee6f350a..d9e44b8fa 100644 --- a/lib/pulse/core/PulseCore.Action.fsti +++ b/lib/pulse/core/PulseCore.Action.fsti @@ -6,13 +6,18 @@ open FStar.PCM open FStar.Ghost type reifiability = + | Ghost | Reifiable | UsesInvariants let ( ^^ ) (r1 r2 : reifiability) : reifiability = - match r1, r2 with - | Reifiable, Reifiable -> Reifiable - | _ -> UsesInvariants + if r1 = r2 then r1 + else ( + match r1, r2 with + | Ghost, Reifiable + | Reifiable, Ghost -> Reifiable + | _ -> UsesInvariants + ) val iname : eqtype @@ -65,6 +70,13 @@ val frame (f:act a r opens pre post) : act a r opens (pre ** frame) (fun x -> post x ** frame) +val 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 val lift_reifiability (#a:Type) @@ -192,7 +204,7 @@ val pts_to (#a:Type u#1) (#p:pcm a) (r:ref a p) (v:a) : slprop val pts_to_not_null (#a:Type) (#p:FStar.PCM.pcm a) (r:ref a p) (v:a) : act (squash (not (is_ref_null r))) - Reifiable + Ghost emp_inames (pts_to r v) (fun _ -> pts_to r v) @@ -240,7 +252,7 @@ val 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 ** pts_to r v1) @@ -252,7 +264,7 @@ val 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 ** pts_to r v1) (fun _ -> pts_to r (op pcm v0 v1)) @@ -300,22 +312,90 @@ val pure_true () : slprop_equiv (pure True) emp val 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) val elim_pure (p:prop) -: act (squash p) Reifiable emp_inames (pure p) (fun _ -> emp) +: act (squash p) Ghost emp_inames (pure p) (fun _ -> emp) /////////////////////////////////////////////////////////////////// // exists* /////////////////////////////////////////////////////////////////// val 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) val 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) /////////////////////////////////////////////////////////////////// // Other utils /////////////////////////////////////////////////////////////////// val drop (p:slprop) -: act unit Reifiable emp_inames p (fun _ -> emp) \ No newline at end of file +: act unit Ghost emp_inames p (fun _ -> emp) + +//////////////////////////////////////////////////////////////////////// +// Ghost References +//////////////////////////////////////////////////////////////////////// +[@@erasable] +val ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused] p:pcm a) : Type u#0 +val ghost_pts_to (#a:Type u#1) (#p:pcm a) (r:ghost_ref p) (v:a) : slprop + +val ghost_alloc + (#a:Type u#1) + (#pcm:pcm a) + (x:erased a{compatible pcm x x /\ pcm.refine x}) +: act (ghost_ref pcm) Ghost emp_inames + emp + (fun r -> ghost_pts_to r x) + +val ghost_read + (#a:Type) + (#p:pcm a) + (r:ghost_ref p) + (x:erased a) + (f:(v:a{compatible p x v} + -> GTot (y:a{compatible p y v /\ + FStar.PCM.frame_compatible p x v y}))) +: act (erased (v:a{compatible p x v /\ p.refine v})) Ghost emp_inames + (ghost_pts_to r x) + (fun v -> ghost_pts_to r (f v)) + +val ghost_write + (#a:Type) + (#p:pcm a) + (r:ghost_ref p) + (x y:Ghost.erased a) + (f:FStar.PCM.frame_preserving_upd p x y) +: act unit Ghost emp_inames + (ghost_pts_to r x) + (fun _ -> ghost_pts_to r y) + +val ghost_share + (#a:Type) + (#pcm:pcm a) + (r:ghost_ref pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a{composable pcm v0 v1}) +: act unit Ghost emp_inames + (ghost_pts_to r (v0 `op pcm` v1)) + (fun _ -> ghost_pts_to r v0 ** ghost_pts_to r v1) + +val ghost_gather + (#a:Type) + (#pcm:pcm a) + (r:ghost_ref pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a) +: act (squash (composable pcm v0 v1)) Ghost emp_inames + (ghost_pts_to r v0 ** ghost_pts_to r v1) + (fun _ -> ghost_pts_to r (op pcm v0 v1)) + +let non_informative a = x:erased a -> y:a { reveal x == y} + +val lift_erased + (#a:Type) + (ni_a:non_informative a) + (#opens:inames) + (#pre:slprop) + (#post:a -> slprop) + (f:erased (act a Ghost opens pre post)) +: act a Ghost opens pre post \ No newline at end of file diff --git a/lib/pulse/core/PulseCore.Atomic.fst b/lib/pulse/core/PulseCore.Atomic.fst index 0f4fff4cb..dde42b631 100644 --- a/lib/pulse/core/PulseCore.Atomic.fst +++ b/lib/pulse/core/PulseCore.Atomic.fst @@ -5,7 +5,7 @@ open PulseCore.InstantiatedSemantics open PulseCore.Action let r_of_obs = function - | Neutral -> Reifiable + | Neutral -> Ghost | _ -> UsesInvariants let stt_atomic a #obs opens pre post = @@ -77,9 +77,9 @@ let bind_atomic (e1:stt_atomic a #obs1 opens pre1 post1) (e2:(x:a -> stt_atomic b #obs2 opens (post1 x) post2)) = match r_of_obs obs1, r_of_obs obs2 with - | Reifiable, Reifiable -> - let e1 : act a Reifiable opens pre1 post1 = e1 in - let e2 : x:a -> act b Reifiable opens (post1 x) post2 = e2 in + | Ghost, Ghost -> + let e1 : act a Ghost opens pre1 post1 = e1 in + let e2 : x:a -> act b Ghost opens (post1 x) post2 = e2 in A.bind e1 e2 | _ -> let e1 : act a UsesInvariants opens pre1 post1 = A.lift_reifiability e1 in @@ -164,7 +164,7 @@ let sub_invs_stt_atomic = assert (Set.equal (Set.union opens1 opens2) opens2); A.weaken #_ #_ #_ #_ #(r_of_obs obs) opens2 e -let stt_ghost a pre post = Ghost.erased (act a Reifiable emp_inames pre post) +let stt_ghost a pre post = Ghost.erased (act a Ghost emp_inames pre 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 @@ -187,7 +187,7 @@ let lift_ghost_neutral (e:stt_ghost a pre post) (reveal_a:non_informative_witness a) : stt_atomic a #Neutral emp_inames pre post -= admit() //This is the main axiom about ghost computations; in Steel, this axiom is implemented within the effect system += Action.lift_erased reveal_a e let lift_neutral_ghost (#a:Type u#a) @@ -273,8 +273,8 @@ let gather #a #pcm r v0 v1 = Ghost.hide (A.gather r v0 v1) let witness #a #pcm r f v pf = A.witness r f v pf let recall #a #pcm #fact r v w = A.recall r v w -let ghost_ref #a p = Ghost.erased (ref a p) -let ghost_pts_to #a #p r v = pts_to r v +let ghost_ref = A.ghost_ref +let ghost_pts_to = A.ghost_pts_to let hide_ghost #a #pre #post (f:stt_ghost a pre post) : stt_ghost (erased a) pre (fun x -> post (reveal x)) @@ -285,7 +285,7 @@ let hide_ghost #a #pre #post A.return #(erased a) #_ #(fun (x:erased a) -> post (reveal x)) (hide r)) -let ghost_alloc #a #pcm x = hide_ghost (Ghost.hide <| A.alloc #a x) +let ghost_alloc #a #pcm x = Ghost.hide <| A.ghost_alloc #a #pcm x let ghost_read (#a:Type) (#p:pcm a) @@ -297,36 +297,9 @@ let ghost_read : stt_ghost (erased (v:a{compatible p x v /\ p.refine v})) (ghost_pts_to r x) (fun v -> ghost_pts_to r (f v)) -= hide_ghost <| Ghost.hide <|A.read r x f - -let ghost_write r x y f = Ghost.hide (A.write r x y f) - -let ghost_share r v0 v1 = Ghost.hide (A.share r v0 v1) -let ghost_gather r v0 v1 = Ghost.hide (A.gather r v0 v1) - -let ghost_witnessed - (#a:Type u#1) - (#p:pcm a) - (r:ghost_ref p) - (f:property a) -= 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)) -= 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) -= A.recall r v w += Ghost.hide <| 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 drop p = Ghost.hide (A.drop p) \ No newline at end of file diff --git a/lib/pulse/core/PulseCore.Atomic.fsti b/lib/pulse/core/PulseCore.Atomic.fsti index ebb9c4556..cdf2af58a 100644 --- a/lib/pulse/core/PulseCore.Atomic.fsti +++ b/lib/pulse/core/PulseCore.Atomic.fsti @@ -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? + +// 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) \ No newline at end of file diff --git a/lib/pulse/core/PulseCore.Heap.fst b/lib/pulse/core/PulseCore.Heap.fst index 0929bc40c..411b4b80b 100644 --- a/lib/pulse/core/PulseCore.Heap.fst +++ b/lib/pulse/core/PulseCore.Heap.fst @@ -253,6 +253,7 @@ let join_associative2 (m0 m1 m2:heap) join_commutative (join m0 m1) m2; join_associative m2 m0 m1 +let join_empty h = assert (join h empty_heap `mem_equiv` h) //////////////////////////////////////////////////////////////////////////////// let slprop = p:(heap ^-> prop) { heap_prop_is_affine p } @@ -264,6 +265,8 @@ let interp (p:slprop u#a) (m:heap u#a) = p m let as_slprop p = FStar.FunctionalExtensionality.on _ p +let of_slprop p = p +let slprop_inj (f:slprop) = () let slprop_extensionality (p q:slprop) : Lemma @@ -735,9 +738,9 @@ let witnessed_ref_stability #a #pcm (r:ref a pcm) (fact:a -> prop) () #set-options "--fuel 2 --ifuel 2" - +#restart-solver let sel_action (#a:_) (#pcm:_) (r:ref a pcm) (v0:erased a) - : action (pts_to r v0) (v:a{compatible pcm v0 v}) (fun _ -> pts_to r v0) + : action #immut_heap #no_allocs (pts_to r v0) (v:a{compatible pcm v0 v}) (fun _ -> pts_to r v0) = let f : pre_action (pts_to r v0) (v:a{compatible pcm v0 v}) @@ -753,34 +756,23 @@ let sel_action' (#a:_) (#pcm:_) (r:ref a pcm) (v0:erased a) (h:full_hheap (pts_t compatible pcm frame v)} = sel_v r v0 h -let refined_pre_action (fp0:slprop) (a:Type) (fp1:a -> slprop) = +let refined_pre_action (#immut:bool) (#allocates:bool) + (#[T.exact (`trivial_pre)]pre:heap ->prop) + (#[T.exact (`trivial_pre)]post:heap -> prop) + (fp0:slprop) (a:Type) (fp1:a -> slprop) = m0:full_hheap fp0 -> Pure (x:a & full_hheap (fp1 x)) - (requires True) + (requires pre m0) (ensures fun (| x, m1 |) -> - forall frame. frame_related_heaps m0 m1 fp0 (fp1 x) frame false) + post m1 /\ + (forall frame. frame_related_heaps m0 m1 fp0 (fp1 x) frame immut allocates)) -let refined_pre_action_as_action (#fp0:slprop) (#a:Type) (#fp1:a -> slprop) - ($f:refined_pre_action fp0 a fp1) - : action fp0 a fp1 +#restart-solver +let refined_pre_action_as_action #immut #allocs #pre #post (#fp0:slprop) (#a:Type) (#fp1:a -> slprop) + ($f:refined_pre_action #immut #allocs #pre #post fp0 a fp1) + : action #immut #allocs #pre #post fp0 a fp1 = let g : pre_action fp0 a fp1 = fun m -> f m in - let aux (frame:slprop) - (m0:full_hheap (fp0 `star` frame)) - : Lemma - (ensures - (affine_star fp0 frame m0; - let (| x, m1 |) = g m0 in - interp (fp1 x `star` frame) m1 /\ - (forall (hp:hprop frame). hp m0 == hp m1) /\ - heap_evolves m0 m1 /\ - (forall ctr. m0 `free_above_addr` ctr ==> m1 `free_above_addr` ctr))) - [SMTPat ()] - = affine_star fp0 frame m0; - let (| x', m1' |) = g m0 in - let (| x, m1 |) = f m0 in - assert (x == x' /\ m1 == m1') - in g let select_join #a #p (r:ref a p) (x:erased a) (h:full_heap) (hl hr:heap) @@ -804,7 +796,7 @@ let select_refine_pre (#a:_) (#p:_) (f:(v:a{compatible p x v} -> GTot (y:a{compatible p y v /\ frame_compatible p x v y}))) - : refined_pre_action + : refined_pre_action #immut_heap #no_allocs (pts_to r x) (v:a{compatible p x v /\ p.refine v}) (fun v -> pts_to r (f v)) @@ -894,7 +886,7 @@ let select_refine (#a:_) (#p:_) (f:(v:a{compatible p x v} -> GTot (y:a{compatible p y v /\ frame_compatible p x v y}))) - : action (pts_to r x) + : action #immut_heap #no_allocs (pts_to r x) (v:a{compatible p x v /\ p.refine v}) (fun v -> pts_to r (f v)) = refined_pre_action_as_action (select_refine_pre r x f) @@ -1029,13 +1021,13 @@ let upd_gen_frame_preserving (#a:Type u#a) (#p:pcm a) = FStar.PropositionalExtensionality.apply (hp h) (hp h1) in () - +#restart-solver let upd_gen_action #a (#p:pcm a) (r:ref a p) (x y:Ghost.erased a) (f:frame_preserving_upd p x y) - : action (pts_to r x) + : action #mut_heap #no_allocs (pts_to r x) unit (fun _ -> pts_to r y) - = let refined : refined_pre_action + = let refined : refined_pre_action #mut_heap #no_allocs (pts_to r x) unit (fun _ -> pts_to r y) @@ -1044,7 +1036,6 @@ let upd_gen_action #a (#p:pcm a) (r:ref a p) (x y:Ghost.erased a) (f:frame_prese FStar.Classical.forall_intro (FStar.Classical.move_requires (upd_gen_frame_preserving r x y f h)); upd_gen_full_evolution r x y f h; let h1 : full_hheap (pts_to r y) = h1 in - assert (forall x. contains_addr h1 x ==> contains_addr h x); assert (forall ctr. h `free_above_addr` ctr ==> h1 `free_above_addr` ctr); (| (), h1 |) in @@ -1108,7 +1099,28 @@ let pts_to_not_null_action #a #pcm r v //////////////////////////////////////////////////////////////////////////////// #push-options "--z3rlimit 20" -let extend #a #pcm x addr h = +let extend_alt + (#a:Type u#a) + (#pcm:pcm a) + (x:a{compatible pcm x x /\ pcm.refine x}) + (addr:nat) +: refined_pre_action #mut_heap #allocs + #(fun h -> h `free_above_addr` addr) + #(fun h -> h `free_above_addr` (addr + 1)) + emp + (ref a pcm) + (fun r -> pts_to r x) + // (h:full_heap{h `free_above_addr` addr}) + // : ( + // r:ref a pcm + // & h':full_heap{ + // (forall (frame: slprop u#a). + // frame_related_heaps h h' emp (pts_to r x) frame mut_heap allocs) /\ + // h' `free_above_addr` (addr + 1) /\ + // heap_evolves h h' + // } + // ) + = fun h -> let r : ref a pcm = Addr addr in let h' = update_addr_full_heap h addr (Ref a pcm Frac.full_perm x) in assert (h' `free_above_addr` (addr + 1)); @@ -1127,8 +1139,8 @@ let extend #a #pcm x addr h = interp (pts_to r x) h0' /\ h' == join h0' hf /\ heap_evolves h h' /\ - interp (pts_to r x `star` frame) h' /\ - (forall (hp:hprop frame). hp h == hp h') + interp (pts_to r x `star` frame) h' ///\ + // (forall (hp:hprop frame). hp h == hp h') )) [SMTPat (interp emp h0); SMTPat (interp frame hf)] @@ -1139,16 +1151,21 @@ let extend #a #pcm x addr h = // assert (h' == (join h0' hf)); intro_star (pts_to r x) frame h0' hf; // assert (interp (pts_to r x `star` frame) h'); - let aux (hp:hprop frame) - : Lemma (ensures (hp h == hp h')) - [SMTPat ()] - = FStar.PropositionalExtensionality.apply (hp h) (hp h') - in + // let aux (hp:hprop frame) + // : Lemma (ensures (hp h == hp h')) + // [SMTPat ()] + // = FStar.PropositionalExtensionality.apply (hp h) (hp h') + // in () in (| r, h' |) #pop-options +let extend #a #pcm + (x:a{compatible pcm x x /\ pcm.refine x}) + (addr:nat) + = refined_pre_action_as_action (extend_alt x addr) + let hprop_sub (p q:slprop) (h0 h1:heap) : Lemma (requires (forall (hp:hprop (p `star` q)). hp h0 == hp h1)) (ensures (forall (hp:hprop q). hp h0 == hp h1)) @@ -1157,97 +1174,43 @@ let hprop_sub (p q:slprop) (h0 h1:heap) #push-options "--z3rlimit_factor 4 --max_fuel 1 --max_ifuel 1" #restart-solver let frame (#a:Type) + (#immut #allocates #hpre #hpost:_) (#pre:slprop) (#post:a -> slprop) (frame:slprop) ($f:action pre a post) - = let g : refined_pre_action (pre `star` frame) a (fun x -> post x `star` frame) + = let g + : refined_pre_action #immut #allocates #hpre #hpost + (pre `star` frame) a (fun x -> post x `star` frame) = fun h0 -> assert (interp (pre `star` frame) h0); affine_star pre frame h0; let (| x, h1 |) = f h0 in assert (interp (post x) h1); assert (interp (post x `star` frame) h1); - assert (forall frame'. frame_related_heaps h0 h1 pre (post x) frame' false); - let aux (frame':slprop) - : Lemma (requires - interp ((pre `star` frame) `star` frame') h0) - (ensures - interp ((post x `star` frame) `star` frame') h1 /\ - (forall (hp:hprop frame'). hp h0 == hp h1)) - = star_associative pre frame frame'; - star_associative (post x) frame frame'; - hprop_sub frame frame' h0 h1 - in - let aux (frame':slprop) - : Lemma - (requires interp ((pre `star` frame) `star` frame') h0) - (ensures interp ((post x `star` frame) `star` frame') h1 /\ - heap_evolves h0 h1 /\ - (forall (hp:hprop frame'). hp h0 == hp h1) /\ - (forall ctr. h0 `free_above_addr` ctr ==> h1 `free_above_addr` ctr)) - [SMTPat ((pre `star` frame) `star` frame')] - = aux frame' - in - assert (forall frame'. frame_related_heaps h0 h1 (pre `star` frame) (post x `star` frame) frame' false); + assert (forall frame'. frame_related_heaps h0 h1 pre (post x) frame' immut allocates); + introduce forall frame'. + (interp ((pre `star` frame) `star` frame') h0 ==> + interp ((post x `star` frame) `star` frame') h1) + with ( + star_associative pre frame frame'; + star_associative (post x) frame frame' + ); (| x, h1 |) in refined_pre_action_as_action g let change_slprop (p q:slprop) (proof: (h:heap -> Lemma (requires interp p h) (ensures interp q h))) - : action p unit (fun _ -> q) + : action #immut_heap #no_allocs p unit (fun _ -> q) = let g : refined_pre_action p unit (fun _ -> q) = fun h -> - proof h; - let aux (frame:slprop) - : Lemma (requires - interp (p `star` frame) h) - (ensures - interp (q `star` frame) h) - [SMTPat ()] - = FStar.Classical.forall_intro (FStar.Classical.move_requires proof) - in + FStar.Classical.forall_intro (FStar.Classical.move_requires proof); (| (), h |) in refined_pre_action_as_action g -let id_elim_star p q m = - let starprop (ml:heap) (mr:heap) = - disjoint ml mr - /\ m == join ml mr - /\ interp p ml - /\ interp q mr - in - elim_star p q m; - let p1 : heap -> prop = fun ml -> (exists mr. starprop ml mr) in - let ml = IndefiniteDescription.indefinite_description_tot _ p1 in - let starpropml mr : prop = starprop ml mr in // this prop annotation seems needed - let mr = IndefiniteDescription.indefinite_description_tot _ starpropml in - (ml, mr) - -let id_elim_exists #a p m = - let existsprop (x:a) = interp (p x) m in - elim_h_exists p m; - let x = IndefiniteDescription.indefinite_description_tot _ existsprop in - x - -let witinv_framon #a (p : a -> slprop) - : Lemma (requires (is_witness_invariant p)) - (ensures (is_frame_monotonic p)) - = - let aux x y h frame : Lemma (requires (interp (p x `star` frame) h /\ interp (p y) h)) - (ensures (interp (p y `star` frame) h)) = - assert (interp (p x `star` frame) h); - let (hl, hr) = id_elim_star (p x) frame h in - affine_star (p x) frame h; - assert (interp (p x) h); - assert (x == y); - () - in - Classical.forall_intro_4 (fun x y m frame -> Classical.move_requires (aux x y m) frame) - let witness_h_exists #a p = fun frame h0 -> let w = FStar.IndefiniteDescription.indefinite_description_tot @@ -1259,11 +1222,11 @@ let intro_exists #a p x = fun frame h0 -> intro_h_exists (reveal x) p h0; (| (), h0 |) - +module U = FStar.Universe let lift_h_exists (#a:_) (p:a -> slprop) : action (h_exists p) unit (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p)) - = let g : refined_pre_action (h_exists p) unit (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p)) + = let g : refined_pre_action #immut_heap #no_allocs (h_exists p) unit (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p)) = fun h -> let aux (x:a) (h:heap) : Lemma @@ -1304,3 +1267,22 @@ let drop p = fun h -> (| (), h |) in refined_pre_action_as_action f + + +let erase_action_result + (#pre #post:_) + (#immut #alloc:_) + (#fp:slprop) + (#a:Type) + (#fp':a -> slprop) + (act:action #immut #alloc #pre #post fp a fp') +: action #immut #alloc #pre #post fp (erased a) (fun x -> fp' x) += let g + : refined_pre_action #immut #alloc #pre #post fp (erased a) (fun x -> fp' x) + = fun h -> + let (| x, h1 |) = act h in + let y : erased a = hide x in + let h1 : full_hheap (fp' (reveal y)) = h1 in + (| y, h1 |) + in + refined_pre_action_as_action g \ No newline at end of file diff --git a/lib/pulse/core/PulseCore.Heap.fsti b/lib/pulse/core/PulseCore.Heap.fsti index 3e31385c9..a11f3f744 100644 --- a/lib/pulse/core/PulseCore.Heap.fsti +++ b/lib/pulse/core/PulseCore.Heap.fsti @@ -103,6 +103,10 @@ val join_associative (h0 h1 h2:heap) disjoint (join h0 h1) h2 /\ join h0 (join h1 h2) == join (join h0 h1) h2)) +val join_empty (h:heap) + : Lemma (disjoint h empty_heap /\ + join h empty_heap == h) + (**** Separation logic over heaps *) (** @@ -137,6 +141,9 @@ val interp (p:slprop u#a) (m:heap u#a) : prop Promoting an affine heap proposition to an slprop *) val as_slprop (f:a_heap_prop) : p:slprop{forall h.interp p h <==> f h} +val of_slprop (f:slprop u#a) : a_heap_prop u#a +val slprop_inj (f:slprop) : Lemma (as_slprop (of_slprop f) == f) + [SMTPat (of_slprop f)] (** An [hprop] is heap predicate indexed by a footprint [fp:slprop]. @@ -405,8 +412,14 @@ val weaken_free_above (h:heap) (a b:nat) The base type for an action is indexed by two separation logic propositions, representing the heap specification of the action before and after. *) -let pre_action (fp:slprop u#a) (a:Type u#b) (fp':a -> slprop u#a) = - full_hheap fp -> (x:a & full_hheap (fp' x)) +let trivial_pre (h:heap) : prop = True +module T = FStar.Tactics +let pre_action (#[T.exact (`trivial_pre)]pre:heap -> prop) + (#[T.exact (`trivial_pre)]post:heap -> prop) + (fp:slprop u#a) + (a:Type u#b) + (fp':a -> slprop u#a) + = h0:full_hheap fp { pre h0 } -> res:(x:a & full_hheap (fp' x)) { post (dsnd res) } (** This is how the heaps before and after the action relate: @@ -414,11 +427,18 @@ let pre_action (fp:slprop u#a) (a:Type u#b) (fp':a -> slprop u#a) = - not allocating any new references; - preserving the validity of any heap proposition affecting any frame *) +let immut_heap = true +let mut_heap = false +let allocs = true +let no_allocs = false unfold -let action_related_heaps (frame:slprop) (h0 h1:full_heap) = +let action_related_heaps + (#[T.exact (`mut_heap)] immut:bool) + (#[T.exact (`no_allocs)] allocates:bool) + (h0 h1:full_heap) = heap_evolves h0 h1 /\ - (forall ctr. h0 `free_above_addr` ctr ==> h1 `free_above_addr` ctr) /\ - (forall (hp:hprop frame). hp h0 == hp h1) + (not allocates ==> (forall ctr. h0 `free_above_addr` ctr ==> h1 `free_above_addr` ctr)) /\ + (immut ==> h0 == h1) (** We only want to consider heap updates that are "frame-preserving", meaning that they only @@ -429,19 +449,26 @@ let action_related_heaps (frame:slprop) (h0 h1:full_heap) = *) let is_frame_preserving (#a: Type u#a) + (#pre #post:_) (#fp: slprop u#b) (#fp': a -> slprop u#b) - (f:pre_action fp a fp') + (immut:bool) + (allocates:bool) + (f:pre_action #pre #post fp a fp') = - forall (frame: slprop u#b) (h0:full_hheap (fp `star` frame)). + forall (frame: slprop u#b) (h0:full_hheap (fp `star` frame) { pre h0 }). (affine_star fp frame h0; let (| x, h1 |) = f h0 in interp (fp' x `star` frame) h1 /\ - action_related_heaps frame h0 h1) + action_related_heaps #immut #allocates h0 h1) (** Every action is frame-preserving *) -let action (fp:slprop u#b) (a:Type u#a) (fp':a -> slprop u#b) = - f:pre_action fp a fp'{ is_frame_preserving f } +let action (#[T.exact (`mut_heap)] immut:bool) + (#[T.exact (`no_allocs)] allocates:bool) + (#[T.exact (`trivial_pre)]pre:heap -> prop) + (#[T.exact (`trivial_pre)]post:heap -> prop) + (fp:slprop u#b) (a:Type u#a) (fp':a -> slprop u#b) = + f:pre_action #pre #post fp a fp'{ is_frame_preserving immut allocates f } (** We define a second, but equivalent, type for actions that @@ -458,18 +485,16 @@ let action_with_frame h0:full_hheap (fp `star` frame) -> Pure (x:a & full_hheap (fp' x `star` frame)) (requires True) - (ensures fun (| x, h1 |) -> action_related_heaps frame h0 h1) + (ensures fun (| x, h1 |) -> action_related_heaps #immut_heap #no_allocs h0 h1) (** Two heaps [h0] and [h1] are frame-related if you can get from [h0] to [h1] with a frame-preserving update. *) -let frame_related_heaps (h0 h1:full_heap) (fp0 fp1 frame:slprop) (allocates:bool) = +let frame_related_heaps (h0 h1:full_heap) (fp0 fp1 frame:slprop) (immut:bool) (allocates:bool) = interp (fp0 `star` frame) h0 ==> interp (fp1 `star` frame) h1 /\ - heap_evolves h0 h1 /\ - (forall (hp:hprop frame). hp h0 == hp h1) /\ - (not allocates ==> (forall ctr. h0 `free_above_addr` ctr ==> h1 `free_above_addr` ctr)) + action_related_heaps #immut #allocates h0 h1 (** @@ -478,14 +503,15 @@ let frame_related_heaps (h0 h1:full_heap) (fp0 fp1 frame:slprop) (allocates:bool *) let action_framing (#a: Type u#a) + (#immut #allocates:bool) (#fp: slprop u#b) (#fp': a -> slprop u#b) - ($f:action fp a fp') + ($f:action #immut #allocates fp a fp') (frame:slprop) (h0:full_hheap (fp `star` frame)) : Lemma ( affine_star fp frame h0; let (| x, h1 |) = f h0 in - frame_related_heaps h0 h1 fp (fp' x) frame false + frame_related_heaps h0 h1 fp (fp' x) frame immut allocates ) = affine_star fp frame h0; @@ -527,7 +553,8 @@ val sel_action (#pcm:pcm a) (r:ref a pcm) (v0:erased a) - : action (pts_to r v0) (v:a{compatible pcm v0 v}) (fun _ -> pts_to r v0) + : action #immut_heap #no_allocs + (pts_to r v0) (v:a{compatible pcm v0 v}) (fun _ -> pts_to r v0) (** A version of select that incorporates a ghost update of local @@ -539,7 +566,7 @@ val select_refine (#a:_) (#p:_) (f:(v:a{compatible p x v} -> GTot (y:a{compatible p y v /\ FStar.PCM.frame_compatible p x v y}))) - : action (pts_to r x) + : action #immut_heap #no_allocs (pts_to r x) (v:a{compatible p x v /\ p.refine v}) (fun v -> pts_to r (f v)) @@ -547,7 +574,7 @@ val select_refine (#a:_) (#p:_) (** Updating a ref cell for a user-defined PCM *) val upd_gen_action (#a:Type) (#p:pcm a) (r:ref a p) (x y:Ghost.erased a) (f:FStar.PCM.frame_preserving_upd p x y) - : action (pts_to r x) + : action #mut_heap #no_allocs (pts_to r x) unit (fun _ -> pts_to r y) @@ -561,7 +588,7 @@ val upd_action (r:ref a pcm) (v0:FStar.Ghost.erased a) (v1:a {FStar.PCM.frame_preserving pcm v0 v1 /\ pcm.refine v1}) - : action (pts_to r v0) unit (fun _ -> pts_to r v1) + : action #mut_heap #no_allocs (pts_to r v0) unit (fun _ -> pts_to r v1) (** Deallocating a reference, by actually replacing its value by the unit of the PCM *) val free_action @@ -569,7 +596,7 @@ val free_action (#pcm:pcm a) (r:ref a pcm) (v0:FStar.Ghost.erased a {exclusive pcm v0 /\ pcm.refine pcm.FStar.PCM.p.one}) - : action (pts_to r v0) unit (fun _ -> pts_to r pcm.FStar.PCM.p.one) + : action #mut_heap #no_allocs (pts_to r v0) unit (fun _ -> pts_to r pcm.FStar.PCM.p.one) (** Splitting a permission on a composite resource into two separate permissions *) @@ -579,7 +606,7 @@ val split_action (r:ref a pcm) (v0:FStar.Ghost.erased a) (v1:FStar.Ghost.erased a{composable pcm v0 v1}) - : action (pts_to r (v0 `op pcm` v1)) unit (fun _ -> pts_to r v0 `star` pts_to r v1) + : action #immut_heap #no_allocs (pts_to r (v0 `op pcm` v1)) unit (fun _ -> pts_to r v0 `star` pts_to r v1) (** Combining separate permissions into a single composite permission *) val gather_action @@ -588,14 +615,15 @@ val gather_action (r:ref a pcm) (v0:FStar.Ghost.erased a) (v1:FStar.Ghost.erased a) - : action (pts_to r v0 `star` pts_to r v1) (_:unit{composable pcm v0 v1}) (fun _ -> pts_to r (op pcm v0 v1)) + : action #immut_heap #no_allocs + (pts_to r v0 `star` pts_to r v1) (_:unit{composable pcm v0 v1}) (fun _ -> pts_to r (op pcm v0 v1)) val pts_to_not_null_action (#a:Type u#a) (#pcm:pcm a) (r:erased (ref a pcm)) (v:Ghost.erased a) -: action +: action #immut_heap #no_allocs (pts_to r v) (squash (not (is_null r))) (fun _ -> pts_to r v) @@ -606,53 +634,51 @@ val extend (#pcm:pcm a) (x:a{compatible pcm x x /\ pcm.refine x}) (addr:nat) - (h:full_heap{h `free_above_addr` addr}) - : ( - r:ref a pcm - & h':full_heap{ - (forall (frame: slprop u#a). - frame_related_heaps h h' emp (pts_to r x) frame (true)) /\ - h' `free_above_addr` (addr + 1) /\ - heap_evolves h h' - } - ) + : action + #mut_heap #allocs + #(fun h -> h `free_above_addr` addr) + #(fun h -> h `free_above_addr` (addr + 1)) + emp + (ref a pcm) + (fun r -> pts_to r x) val frame (#a:Type) + #immut #allocates #hpre #hpost (#pre:slprop) (#post:a -> slprop) (frame:slprop) - ($f:action pre a post) - : action (pre `star` frame) a (fun x -> post x `star` frame) + ($f:action #immut #allocates #hpre #hpost pre a post) + : action #immut #allocates #hpre #hpost (pre `star` frame) a (fun x -> post x `star` frame) val change_slprop (p q:slprop) (proof: (h:heap -> Lemma (requires interp p h) (ensures interp q h))) - : action p unit (fun _ -> q) + : action #immut_heap #no_allocs p unit (fun _ -> q) -module U = FStar.Universe +// module U = FStar.Universe -val id_elim_star (p q:slprop) (h:heap) - : Pure (erased heap & erased heap ) - (requires (interp (p `star` q) h)) - (ensures (fun (hl, hr) -> disjoint hl hr - /\ h == join hl hr - /\ interp p hl - /\ interp q hr)) +// val id_elim_star (p q:slprop) (h:heap) +// : Pure (erased heap & erased heap ) +// (requires (interp (p `star` q) h)) +// (ensures (fun (hl, hr) -> disjoint hl hr +// /\ h == join hl hr +// /\ interp p hl +// /\ interp q hr)) -val id_elim_exists (#a:Type) (p : a -> slprop) (h:heap) - : Pure (erased a) - (requires (interp (h_exists p) h)) - (ensures (fun x -> interp (p x) h)) +// val id_elim_exists (#a:Type) (p : a -> slprop) (h:heap) +// : Pure (erased a) +// (requires (interp (h_exists p) h)) +// (ensures (fun x -> interp (p x) h)) -let is_frame_monotonic #a (p : a -> slprop) : prop = - forall x y m frame. interp (p x `star` frame) m /\ interp (p y) m ==> interp (p y `star` frame) m +// let is_frame_monotonic #a (p : a -> slprop) : prop = +// forall x y m frame. interp (p x `star` frame) m /\ interp (p y) m ==> interp (p y `star` frame) m -let is_witness_invariant #a (p : a -> slprop) = - forall x y m. interp (p x) m /\ interp (p y) m ==> x == y +// let is_witness_invariant #a (p : a -> slprop) = +// forall x y m. interp (p x) m /\ interp (p y) m ==> x == y -val witinv_framon (#a:_) (p : a -> slprop) - : Lemma (requires (is_witness_invariant p)) - (ensures (is_frame_monotonic p)) +// val witinv_framon (#a:_) (p : a -> slprop) +// : Lemma (requires (is_witness_invariant p)) +// (ensures (is_frame_monotonic p)) (** @@ -668,18 +694,27 @@ val intro_exists (#a:_) (p:a -> slprop) (x:erased a) : action_with_frame (p x) unit (fun _ -> h_exists p) val lift_h_exists (#a:_) (p:a -> slprop) - : action (h_exists p) unit - (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p)) + : action #immut_heap #no_allocs (h_exists p) unit + (fun _a -> h_exists #(FStar.Universe.raise_t a) (FStar.Universe.lift_dom p)) val elim_pure (p:prop) - : action (pure p) (u:unit{p}) (fun _ -> emp) + : action #immut_heap #no_allocs (pure p) (u:unit{p}) (fun _ -> emp) val intro_pure (p:prop) (_:squash p) - : action emp unit (fun _ -> pure p) + : action #immut_heap #no_allocs emp unit (fun _ -> pure p) val pts_to_evolve (#a:Type u#a) (#pcm:_) (r:ref a pcm) (x y : a) (h:heap) : Lemma (requires (interp (pts_to r x) h /\ compatible pcm y x)) (ensures (interp (pts_to r y) h)) val drop (p:slprop) - : action p unit (fun _ -> emp) \ No newline at end of file + : action #immut_heap #no_allocs p unit (fun _ -> emp) + +val erase_action_result + (#pre #post:_) + (#immut #alloc:_) + (#fp:slprop) + (#a:Type) + (#fp':a -> slprop) + (act:action #immut #alloc #pre #post fp a fp') +: action #immut #alloc #pre #post fp (erased a) (fun x -> fp' x) \ No newline at end of file diff --git a/lib/pulse/core/PulseCore.Heap2.fst b/lib/pulse/core/PulseCore.Heap2.fst new file mode 100644 index 000000000..c541213f3 --- /dev/null +++ b/lib/pulse/core/PulseCore.Heap2.fst @@ -0,0 +1,731 @@ +module PulseCore.Heap2 +module F = FStar.FunctionalExtensionality +open FStar.FunctionalExtensionality +open FStar.PCM +module Frac = PulseCore.FractionalPermission +module PP = PulseCore.Preorder +module H = PulseCore.Heap + +noeq +type heap : Type u#(a + 1) = { + concrete : H.heap u#a; + ghost : erased (H.heap u#a); +} +let concrete h = h.concrete +let ghost h = h.ghost +let upd_ghost_heap (h0:heap) (h1:erased heap { concrete h0 == concrete h1 }) + : h2:heap { h2 == reveal h1 } + = { h0 with ghost = h1.ghost } +let empty_heap = { concrete = H.empty_heap; ghost = H.empty_heap } + +let get (t:tag) (h:heap u#a) : GTot (H.heap u#a) = + match t with + | CONCRETE -> h.concrete + | GHOST -> h.ghost +let put (t:tag) (h':H.heap u#a) (h:heap u#a) : GTot (heap u#a) = + match t with + | CONCRETE -> { h with concrete = h' } + | GHOST -> { h with ghost = h' } + +let core_ref = H.core_ref +let core_ref_null = H.core_ref_null +let core_ref_is_null = H.core_ref_is_null + +let disjoint (h1:heap) (h2:heap) = + H.disjoint h1.concrete h2.concrete /\ H.disjoint h1.ghost h2.ghost + +let disjoint_sym h0 h1 = () +let join h0 h1 = { + concrete = H.join h0.concrete h1.concrete; + ghost = H.join h0.ghost h1.ghost; +} +let join_commutative' (m0 m1:heap) + : Lemma + (requires + disjoint m0 m1) + (ensures + join m0 m1 == join m1 m0) + [SMTPat (join m0 m1)] + = H.join_commutative m0.concrete m1.concrete; + H.join_commutative m0.ghost m1.ghost + +let join_commutative h0 h1 = + H.join_commutative h0.concrete h1.concrete; + H.join_commutative h0.ghost h1.ghost +let disjoint_join h0 h1 h2 = + H.disjoint_join h0.concrete h1.concrete h2.concrete; + H.disjoint_join h0.ghost h1.ghost h2.ghost +let join_associative h0 h1 h2 = + H.join_associative h0.concrete h1.concrete h2.concrete; + H.join_associative h0.ghost h1.ghost h2.ghost + +let join_associative2 (m0 m1 m2:heap) + : Lemma + (requires + disjoint m0 m1 /\ + disjoint (join m0 m1) m2) + (ensures + disjoint m1 m2 /\ + disjoint m0 (join m1 m2) /\ + join m0 (join m1 m2) == join (join m0 m1) m2) + [SMTPat (join (join m0 m1) m2)] + = disjoint_join m2 m0 m1; + join_commutative m2 m1; + join_associative m0 m1 m2 + +// let splittable_heap : splittable (heap u#a) = { +// disjoint; +// join; +// laws = FStar.Classical.forall_intro_3 disjoint_join +// } +// let splittable_hheap : splittable (H.heap u#a) = { +// disjoint = H.disjoint; +// join = H.join; +// laws = admit() +// } +// let lens_concrete : lens (heap u#a) (H.heap u#a) = { +// get = (fun h -> h.concrete); +// put = (fun concrete h -> { h with concrete }); +// sa = splittable_heap; +// sb = splittable_hheap; +// lens_laws = (); +// law0 = (fun x y -> ()); +// law1 = (fun x y l m -> ()) +// } +// let lens_ghost : lens (heap u#a) (H.heap u#a) = { +// get = (fun h -> reveal h.ghost); +// put = (fun ghost h -> { h with ghost }); +// sa = splittable_heap; +// sb = splittable_hheap; +// lens_laws = (); +// law0 = (fun x y -> ()); +// law1 = (fun x y l m -> ()) +// } + +let slprop = p:(heap ^-> prop) { heap_prop_is_affine p } +let interp p m = p m +let as_slprop f = F.on _ f +let slprop_extensionality p q = FStar.PredicateExtensionality.predicateExtensionality _ p q +let emp = as_slprop (fun _ -> True) +let llift (t:tag) (p:H.slprop) : slprop = + as_slprop (fun h -> H.of_slprop p (get t h)) +let lift (p:H.slprop) : slprop = llift CONCRETE p +let pts_to #a #pcm (r:ref a pcm) (v:a) = lift (H.pts_to #a #pcm r v) +let star p1 p2 = + as_slprop (fun (h: heap) -> + exists (h1 h2 : heap). + h1 `disjoint` h2 /\ + h == join h1 h2 /\ + interp p1 h1 /\ + interp p2 h2) +let h_exists #a f = as_slprop (fun h -> exists (x:a). interp (f x) h) +let affine_star p1 p2 h = () +let equiv_symmetric p1 p2 = () +let equiv_extensional_on_star p1 p2 p3 = () +let h_join_empty (h:H.heap) + : Lemma (H.disjoint h H.empty_heap /\ + H.join h H.empty_heap == h) + [SMTPatOr + [[SMTPat (H.disjoint h H.empty_heap)]; + [SMTPat (H.join h H.empty_heap)]]] + = H.join_empty h +let emp_unit p = + assert (forall h. disjoint h empty_heap /\ join h empty_heap == h) +let intro_emp h = () +let h_exists_cong #a p q = () +let intro_h_exists x p h = () +let elim_h_exists #a p h = () +let interp_depends_only_on hp = () +#restart-solver +#push-options "--fuel 0 --ifuel 2 --z3rlimit_factor 4 --split_queries always" +let lift_star (l:tag) (p q:H.slprop) +: Lemma (llift l (p `H.star` q) == (llift l p `star` llift l q)) + [SMTPat (llift l (p `H.star` q))] += introduce forall m. + interp (llift l (p `H.star` q)) m <==> + interp (llift l p `star` llift l q) m + with ( + introduce + interp (llift l p `star` llift l q) m ==> + interp (llift l (p `H.star` q)) m + with _ . ( + eliminate exists h0 h1. + disjoint h0 h1 /\ + m == join h0 h1 /\ + interp (llift l p) h0 /\ + interp (llift l q) h1 + returns interp (llift l (p `H.star` q)) m + with _ . ( + H.intro_star p q (get l h0) (get l h1) + ) + ); + introduce + interp (llift l (p `H.star` q)) m ==> + interp (llift l p `star` llift l q) m + with _ . ( + H.elim_star p q (get l m); + eliminate exists c0 c1. + H.disjoint c0 c1 /\ + get l m == H.join c0 c1 /\ + H.interp p c0 /\ + H.interp q c1 + returns interp (llift l p `star` llift l q) m + with _ . ( + let h0 = put l c0 m in + let h1 = put l c1 empty_heap in + assert (join h0 h1 == m) + ) + ); + () + ); + slprop_extensionality (llift l (p `H.star` q)) (llift l p `star` llift l q) +#pop-options +let lift_emp : squash (lift H.emp == emp) = + FStar.Classical.forall_intro H.intro_emp; + slprop_extensionality (lift H.emp) emp + +let pts_to_compatible #a #pcm (x:ref a pcm) (v0 v1:a) h = + H.pts_to_compatible #a #pcm x v0 v1 h.concrete; + lift_star CONCRETE (H.pts_to #a #pcm x v0) (H.pts_to #a #pcm x v1) + +let pts_to_join #a #pcm (r:ref a pcm) (v1 v2:a) h = + H.pts_to_join #a #pcm r v1 v2 h.concrete + +let pts_to_join' #a #pcm r v1 v2 h = + H.pts_to_join' #a #pcm r v1 v2 h.concrete + +let pts_to_compatible_equiv #a #pcm r v0 v1 = + H.pts_to_compatible_equiv #a #pcm r v0 v1; + lift_star CONCRETE (H.pts_to #a #pcm r v0) (H.pts_to #a #pcm r v1) + +let pts_to_not_null #a #pcm x v m = H.pts_to_not_null #a #pcm x v m.concrete + +let intro_star p q h hq = () +let elim_star p q h = () +let star_commutative p1 p2 = () +#push-options "--fuel 0 --ifuel 4 --z3rlimit_factor 4 --z3cliopt smt.qi.eager_threshold=1000000" +let star_associative p1 p2 p3 = () +#pop-options +let star_congruence p1 p2 q1 q2 = () + +let pure p = as_slprop (fun _ -> p) +let pure_equiv p q = FStar.PropositionalExtensionality.apply p q +let pure_interp q h = () +let pure_star_interp p q h = () + +let stronger_star p q r = () +let weaken p q r h = () + +let full_heap_pred h = H.full_heap_pred h.concrete /\ H.full_heap_pred h.ghost +let heap_evolves (h0 h1:full_heap) = + H.heap_evolves h0.concrete h1.concrete /\ + H.heap_evolves h0.ghost h1.ghost +let free_above_addr tag h a = H.free_above_addr (get tag h) a +let weaken_free_above tag h a b = H.weaken_free_above (get tag h) a b + +(** [sel_v] is a ghost read of the value contained in a heap reference *) +let sel_v' (#a:Type u#h) (#pcm:pcm a) (r:ref a pcm) (v:erased a) (m:full_hheap (pts_to r v)) + : v':a{ compatible pcm v v' /\ + pcm.refine v' /\ + interp (ptr r) m /\ + True + } + = let v = H.sel_v #a #pcm r v m.concrete in + v + +let lower_ptr #a #pcm (r:ref a pcm) (m:full_hheap (ptr r)) +: Lemma (H.interp (H.ptr #a #pcm r) m.concrete) += eliminate exists v. H.interp (H.pts_to #a #pcm r v) m.concrete + returns H.interp (H.ptr #a #pcm r) m.concrete + with _ . ( H.intro_h_exists v (H.pts_to #a #pcm r) m.concrete ) + +let raise_ptr #a #pcm (r:ref a pcm) (m:full_heap) +: Lemma + (requires + H.interp (H.ptr #a #pcm r) m.concrete) + (ensures + interp (ptr r) m) += H.elim_h_exists (H.pts_to #a #pcm r) m.concrete; + eliminate exists v. H.interp (H.pts_to #a #pcm r v) m.concrete + returns interp (ptr #a #pcm r) m + with _ . () + +(** [sel] is a ghost read of the value contained in a heap reference *) +let sel (#a:Type u#h) (#pcm:pcm a) (r:ref a pcm) (m:full_hheap (ptr r)) : a = + lower_ptr r m; + H.sel #a #pcm r m.concrete + +let sel_v (#a:Type u#h) (#pcm:pcm a) (r:ref a pcm) (v:erased a) (m:full_hheap (pts_to r v)) + : v':a{ compatible pcm v v' /\ + pcm.refine v' /\ + interp (ptr r) m /\ + v' == sel r m + } + = H.sel_v #a #pcm r v m.concrete + +let sel_lemma #a #pcm r m = lower_ptr r m; H.sel_lemma #a #pcm r m.concrete +let heap_evolves_iff (h0 h1:full_heap) +: Lemma + (ensures + heap_evolves h0 h1 <==> ( + H.heap_evolves h0.concrete h1.concrete /\ + H.heap_evolves h0.ghost h1.ghost)) += assert (heap_evolves h0 h1 <==> + (H.heap_evolves h0.concrete h1.concrete /\ H.heap_evolves h0.ghost h1.ghost)) + by (FStar.Tactics.norm [delta_only [`%heap_evolves]]) + + +let witnessed_ref_stability #a #pcm r fact = + H.witnessed_ref_stability #a #pcm r fact; + assert (FStar.Preorder.stable (H.witnessed_ref #a #pcm r fact) H.heap_evolves); + introduce forall h0 h1. + (witnessed_ref r fact h0 /\ + heap_evolves h0 h1) ==> + witnessed_ref r fact h1 + with ( + introduce _ ==> _ + with _ . ( + assert (interp (ptr r) h0 /\ fact (sel r h0)); + lower_ptr r h0; + assert (H.interp (H.ptr #a #pcm r) h0.concrete); + assert (heap_evolves h0 h1); + heap_evolves_iff h0 h1; + assert (H.heap_evolves h0.concrete h1.concrete); + assert (H.witnessed_ref #a #pcm r fact h1.concrete); + raise_ptr r h1; + assert (sel r h1 == H.sel #a #pcm r h1.concrete) + ) + ) + +let llift_pred (l:tag) (pre:H.heap -> prop) + : heap -> prop + = fun h -> pre (get l h) +let lift_pred = llift_pred CONCRETE +let lift_heap_pre_action + (#pre #post:_) (#fp:H.slprop) (#a:Type) (#fp':a -> H.slprop) + (act:H.pre_action #pre #post fp a fp') +: pre_action #(lift_pred pre) #(lift_pred post) (lift fp) a (fun x -> lift (fp' x)) += fun (h0:full_hheap (lift fp) { lift_pred pre h0 }) -> + let (| x, c |) = act h0.concrete in + let h1 : full_hheap (lift (fp' x)) = { h0 with concrete=c } in + (| x, h1 |) + +#restart-solver + +#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 4" +let lift_immut (m:bool) = if m then IMMUTABLE else MUTABLE +let lift_allocs (m:bool) = if m then Some CONCRETE else None +let lift_action + (#immut #allocs #pre #post:_) + (#fp:H.slprop) (#a:Type) (#fp':a -> H.slprop) + (act:H.action #immut #allocs #pre #post fp a fp') +: action #(lift_immut immut) #(lift_allocs allocs) #(lift_pred pre) #(lift_pred post) + (lift fp) a (fun x -> lift (fp' x)) += let p = lift_heap_pre_action act in + let mut = lift_immut immut in + let allocs = lift_allocs allocs in + introduce forall frame (h0:full_hheap (lift fp `star` frame) { lift_pred pre h0 }). + let (| x, h1 |) = p h0 in + interp (lift (fp' x) `star` frame) h1 /\ + action_related_heaps #mut #allocs h0 h1 + with ( + assert (interp (lift fp `star` frame) h0); + let (| x, h1 |) = p h0 in + eliminate exists h0' h1'. + disjoint h0' h1' /\ + h0 == join h0' h1' /\ + interp (lift fp) h0' /\ + interp frame h1' + returns + interp (lift (fp' x) `star` frame) h1 /\ + action_related_heaps #mut #allocs h0 h1 + with _ . ( + let hframe : H.heap -> prop = (fun h -> interp frame { concrete = h; ghost = h1'.ghost }) in + introduce forall c0 c1. + (hframe c0 /\ H.disjoint c0 c1) + ==> + hframe (H.join c0 c1) + with ( + introduce _ ==> _ + with _ . ( + let h0g = {concrete=c0; ghost=h1'.ghost} in + assert (interp frame h0g); + assert (H.disjoint c0 c1); + assert (heap_prop_is_affine frame); + let h1g = { concrete = c1; ghost = H.empty_heap } in + assert (disjoint h0g h1g); + assert (interp frame (join h0g h1g)); + assert (hframe (H.join c0 c1)) + ) + ); + assert (H.heap_prop_is_affine hframe); + let hframe : H.slprop = H.as_slprop hframe in + assert (H.interp fp h0'.concrete); + assert (H.interp hframe h1'.concrete); + H.intro_star fp hframe h0'.concrete h1'.concrete; + let h00 : H.full_hheap (fp `H.star` hframe) = h0.concrete in + let h11 : H.full_hheap (fp' x `H.star` hframe) = dsnd (act h00) in + assert (h1 == { h0 with concrete = h11 }); + H.elim_star (fp' x) hframe h11; + eliminate exists c0 c1. + H.disjoint c0 c1 /\ + h11 == H.join c0 c1 /\ + H.interp (fp' x) c0 /\ + H.interp hframe c1 + returns interp (lift (fp' x) `star` frame) h1 + with _ . ( + let h10 = { concrete = c0; ghost = h0'.ghost } in + let h11 = { concrete = c1; ghost = h1'.ghost } in + assert (interp (lift (fp' x)) h10); + assert (interp frame h11); + assert (disjoint h10 h11) + ); + heap_evolves_iff h0 h1; + assert (action_related_heaps #mut #allocs h0 h1) + ) + ); + p + +let sel_action #a #pcm r v0 = lift_action (H.sel_action #a #pcm r v0) +let select_refine #a #p r x f = lift_action (H.select_refine #a #p r x f) +let upd_gen_action #a #p r x y f = lift_action (H.upd_gen_action #a #p r x y f) +let upd_action #a #p r x y = lift_action (H.upd_action #a #p r x y) +let free_action #a #p r v0 = lift_action (H.free_action #a #p r v0) +let split_action #a #p r v0 v1 = lift_action (H.split_action #a #p r v0 v1) +let gather_action #a #p r v0 v1 = lift_action (H.gather_action #a #p r v0 v1) +let pts_to_not_null_action #a #p r v = lift_action (H.pts_to_not_null_action #a #p r v) +let extend #a #pcm x addr = lift_action (H.extend #a #pcm x addr) + +let refined_pre_action (#mut:mutability) (#allocates:option tag) + (#[T.exact (`trivial_pre)]pre:heap ->prop) + (#[T.exact (`trivial_pre)]post:heap -> prop) + (fp0:slprop) (a:Type) (fp1:a -> slprop) = + m0:full_hheap fp0 -> + Pure (x:a & + full_hheap (fp1 x)) + (requires pre m0) + (ensures fun (| x, m1 |) -> + post m1 /\ + (forall frame. frame_related_heaps m0 m1 fp0 (fp1 x) frame mut allocates)) + +#restart-solver +let refined_pre_action_as_action #immut #allocs #pre #post (#fp0:slprop) (#a:Type) (#fp1:a -> slprop) + ($f:refined_pre_action #immut #allocs #pre #post fp0 a fp1) + : action #immut #allocs #pre #post fp0 a fp1 + = let g : pre_action fp0 a fp1 = fun m -> f m in + g + +let frame (#a:Type) + (#immut #allocates #hpre #hpost:_) + (#pre:slprop) + (#post:a -> slprop) + (frame:slprop) + ($f:action pre a post) + = let g + : refined_pre_action #immut #allocates #hpre #hpost + (pre `star` frame) a (fun x -> post x `star` frame) + = fun h0 -> + assert (interp (pre `star` frame) h0); + affine_star pre frame h0; + let (| x, h1 |) = f h0 in + assert (interp (post x) h1); + assert (interp (post x `star` frame) h1); + assert (forall frame'. frame_related_heaps h0 h1 pre (post x) frame' immut allocates); + introduce forall frame'. + (interp ((pre `star` frame) `star` frame') h0 ==> + interp ((post x `star` frame) `star` frame') h1) + with ( + star_associative pre frame frame'; + star_associative (post x) frame frame' + ); + (| x, h1 |) + in + refined_pre_action_as_action g + + +let change_slprop (p q:slprop) + (proof: (h:heap -> Lemma (requires interp p h) (ensures interp q h))) + : action #IMMUTABLE #no_allocs p unit (fun _ -> q) + = let g + : refined_pre_action p unit (fun _ -> q) + = fun h -> + FStar.Classical.forall_intro (FStar.Classical.move_requires proof); + (| (), h |) + in + refined_pre_action_as_action g + + +let elim_exists #a p = + fun frame h0 -> + let w = FStar.IndefiniteDescription.indefinite_description_tot + a + (fun x -> interp (p x `star` frame) h0) in + (| w, h0 |) + +let intro_exists #a p x = + fun frame h0 -> + intro_h_exists (reveal x) p h0; + (| (), h0 |) + +module U = FStar.Universe + +let lift_exists (#a:_) (p:a -> slprop) + : action (h_exists p) unit + (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p)) + = let g : refined_pre_action #IMMUTABLE #no_allocs (h_exists p) unit (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p)) + = fun h -> + introduce forall x h. + interp (p x) h ==> + interp (h_exists (U.lift_dom p)) h + with ( + introduce _ ==> _ + with _ . ( + assert (interp (U.lift_dom p (U.raise_val x)) h) + ) + ); + (| (), h |) + in + refined_pre_action_as_action g + +let elim_pure (p:prop) + : action (pure p) (u:unit{p}) (fun _ -> emp) + = let f + : refined_pre_action (pure p) (_:unit{p}) (fun _ -> emp) + = fun h -> (| (), h |) + in + refined_pre_action_as_action f + +let intro_pure (p:prop) (_:squash p) +: action emp unit (fun _ -> pure p) += let f + : refined_pre_action emp unit (fun _ -> pure p) + = fun h -> (| (), h |) + in + refined_pre_action_as_action f + +let pts_to_evolve (#a:Type u#a) (#pcm:_) (r:ref a pcm) (x y : a) (h:heap) + : Lemma (requires (interp (pts_to r x) h /\ compatible pcm y x)) + (ensures (interp (pts_to r y) h)) + = H.pts_to_evolve #a #pcm r x y h.concrete + +let drop p += let f + : refined_pre_action p unit (fun _ -> emp) + = fun h -> (| (), h |) + in + refined_pre_action_as_action f + +let is_frame_preserving_only_ghost + (#allocs:option tag) + (#a: Type u#a) + (#pre #post:_) + (#fp: slprop u#b) + (#fp': a -> slprop u#b) + (f:pre_action #pre #post fp a fp') + (h:full_hheap fp { pre h }) +: Lemma + (requires is_frame_preserving ONLY_GHOST allocs f) + (ensures (dsnd (f h)).concrete == h.concrete) += emp_unit fp; + let h : full_hheap (fp `star` emp) = h in + eliminate forall frame (h0:full_hheap (fp `star` frame) { pre h0 }). ( + affine_star fp frame h0 ; + (dsnd (f h0)).concrete == h0.concrete) + with emp h + +let lift_erased + (#a:Type) + (#ni_a:non_informative a) + (#allocs:option tag) + #hpre #hpost + (#pre:slprop) + (#post:a -> slprop) + ($f:erased (action #ONLY_GHOST #allocs #hpre #hpost pre a post)) +: action #ONLY_GHOST #allocs #hpre #hpost pre a post += let g : refined_pre_action #ONLY_GHOST #allocs #hpre #hpost pre a post = + fun h -> + let gg : erased (a & H.heap) = + let ff : action #ONLY_GHOST #allocs #hpre #hpost pre a post = reveal f in + let (| x, hh' |) = ff h in + is_frame_preserving_only_ghost #allocs ff h; + Ghost.hide (x, Ghost.reveal hh'.ghost) + in + let x = ni_a (Ghost.hide (fst gg)) in + let gg = Ghost.hide (snd gg) in + (| x, { h with ghost = gg } |) + in + refined_pre_action_as_action g + +let ghost_ref #a p = erased H.core_ref +let ghost_pts_to #a #p r v = llift GHOST (H.pts_to #a #p r v) +let ghost_free_above_addr h addr = H.free_above_addr h.ghost addr + + +let lift_heap_pre_action_ghost + (#pre #post:_) (#fp:H.slprop) (#a:Type) (#fp':a -> H.slprop) + (ni_a:non_informative a) + (act:H.pre_action #pre #post fp a fp') +: pre_action #(llift_pred GHOST pre) #(llift_pred GHOST post) + (llift GHOST fp) + a + (fun x -> llift GHOST (fp' x)) += fun (h0:full_hheap (llift GHOST fp) { llift_pred GHOST pre h0 }) -> + let xg : erased (a & H.heap) = + let (| x, g |) = act (reveal h0.ghost) in + hide (x, g) + in + let h1 = { h0 with ghost=hide (snd (reveal xg)) } in + let x = ni_a (hide (fst (reveal xg))) in + (| x, h1 |) + +#restart-solver + +#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 4" +let lift_immut_ghost (m:bool) = if m then IMMUTABLE else ONLY_GHOST +let lift_allocs_ghost (m:bool) = if m then Some GHOST else None +let lift_action_ghost + (#immut #allocs #pre #post:_) + (#fp:H.slprop) (#a:Type) (#fp':a -> H.slprop) + (ni_a:non_informative a) + (act:H.action #immut #allocs #pre #post fp a fp') +: action #(lift_immut_ghost immut) + #(lift_allocs_ghost allocs) + #(llift_pred GHOST pre) #(llift_pred GHOST post) + (llift GHOST fp) a (fun x -> llift GHOST (fp' x)) += let p = lift_heap_pre_action_ghost ni_a act in + let mut = lift_immut immut in + let allocs = lift_allocs_ghost allocs in + introduce forall frame (h0:full_hheap (llift GHOST fp `star` frame) { llift_pred GHOST pre h0 }). + let (| x, h1 |) = p h0 in + interp (llift GHOST (fp' x) `star` frame) h1 /\ + action_related_heaps #mut #allocs h0 h1 + with ( + assert (interp (llift GHOST fp `star` frame) h0); + let (| x, h1 |) = p h0 in + eliminate exists h0' h1'. + disjoint h0' h1' /\ + h0 == join h0' h1' /\ + interp (llift GHOST fp) h0' /\ + interp frame h1' + returns + interp (llift GHOST (fp' x) `star` frame) h1 /\ + action_related_heaps #mut #allocs h0 h1 + with _ . ( + let hframe : H.heap -> prop = (fun h -> interp frame { concrete = h1'.concrete; ghost = h }) in + introduce forall c0 c1. + (hframe c0 /\ H.disjoint c0 c1) + ==> + hframe (H.join c0 c1) + with ( + introduce _ ==> _ + with _ . ( + let h0g = {concrete=h1'.concrete; ghost=c0 } in + assert (interp frame h0g); + assert (H.disjoint c0 c1); + assert (heap_prop_is_affine frame); + let h1g = { concrete = H.empty_heap; ghost=c1} in + assert (disjoint h0g h1g); + assert (interp frame (join h0g h1g)); + assert (hframe (H.join c0 c1)) + ) + ); + assert (H.heap_prop_is_affine hframe); + let hframe : H.slprop = H.as_slprop hframe in + assert (H.interp fp h0'.ghost); + assert (H.interp hframe h1'.ghost); + H.intro_star fp hframe h0'.ghost h1'.ghost; + let h00 : H.full_hheap (fp `H.star` hframe) = h0.ghost in + let h11 : H.full_hheap (fp' x `H.star` hframe) = dsnd (act h00) in + assert (h1 == { h0 with ghost = h11 }); + H.elim_star (fp' x) hframe h11; + eliminate exists c0 c1. + H.disjoint c0 c1 /\ + h11 == H.join c0 c1 /\ + H.interp (fp' x) c0 /\ + H.interp hframe c1 + returns interp (llift GHOST (fp' x) `star` frame) h1 + with _ . ( + let h10 = { concrete = h0'.concrete; ghost=c0 } in + let h11 = { concrete = h1'.concrete; ghost=c1 } in + assert (interp (llift GHOST (fp' x)) h10); + assert (interp frame h11); + assert (disjoint h10 h11) + ); + heap_evolves_iff h0 h1; + assert (action_related_heaps #mut #allocs h0 h1) + ) + ); + p + +let ni_erased a : non_informative (erased a) = fun x -> reveal x +let ni_unit : non_informative unit = fun x -> reveal x + +let lift_ghost_emp : squash (llift GHOST H.emp == emp) = + FStar.Classical.forall_intro H.intro_emp; + slprop_extensionality (llift GHOST H.emp) emp +let ghost_extend + (#a:Type u#a) + (#pcm:pcm a) + (x:erased a{compatible pcm x x /\ pcm.refine x}) + (addr:erased nat) += lift_erased #_ #(ni_erased H.core_ref) + (Ghost.hide <| + lift_action_ghost (ni_erased H.core_ref) (H.erase_action_result (H.extend #a #pcm x addr))) + + +let ghost_read + (#a:Type) + (#p:pcm a) + (r:ghost_ref p) + (x:erased a) + (f:(v:a{compatible p x v} + -> GTot (y:a{compatible p y v /\ + FStar.PCM.frame_compatible p x v y}))) += lift_erased #_ #(ni_erased _) #None + (Ghost.hide <| + lift_action_ghost (ni_erased _) (H.erase_action_result (H.select_refine #a #p r x f))) + +let ghost_write + (#a:Type) + (#p:pcm a) + (r:ghost_ref p) + (x y:Ghost.erased a) + (f:FStar.PCM.frame_preserving_upd p x y) +: action #ONLY_GHOST #None + (ghost_pts_to r x) + unit + (fun _ -> ghost_pts_to r y) += lift_erased #_ #(ni_unit) #None + (Ghost.hide <| + lift_action_ghost ni_unit (H.upd_gen_action #a #p r x y f)) + + +let ghost_share + (#a:Type) + (#pcm:pcm a) + (r:ghost_ref pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a{composable pcm v0 v1}) +: action #IMMUTABLE + (ghost_pts_to r (v0 `op pcm` v1)) + unit + (fun _ -> ghost_pts_to r v0 `star` ghost_pts_to r v1) += lift_erased #_ #(ni_unit) #None + (Ghost.hide <| + lift_action_ghost ni_unit (H.split_action #a #pcm r v0 v1)) + +let ni_squash #a : non_informative (squash a) = fun x -> reveal x + +let ghost_gather + (#a:Type) + (#pcm:pcm a) + (r:ghost_ref pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a) +: action #IMMUTABLE + (ghost_pts_to r v0 `star` ghost_pts_to r v1) + (squash (composable pcm v0 v1)) + (fun _ -> ghost_pts_to r (op pcm v0 v1)) += lift_erased #_ #(ni_squash ) #None + (Ghost.hide <| + lift_action_ghost ni_squash (H.gather_action #a #pcm r v0 v1)) diff --git a/lib/pulse/core/PulseCore.Heap2.fsti b/lib/pulse/core/PulseCore.Heap2.fsti new file mode 100644 index 000000000..d1014c36c --- /dev/null +++ b/lib/pulse/core/PulseCore.Heap2.fsti @@ -0,0 +1,806 @@ +(* + Copyright 2019 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module PulseCore.Heap2 +open FStar.Ghost +open FStar.PCM +module T = FStar.Tactics +module H = PulseCore.Heap +/// This module defines the behavior of a structured heap where each memory cell is governed by +/// a partial commutative monoid. This PCM structure is reused for the entire heap as it is possible +/// to talk about disjoint heaps and join them together. +/// +/// In a sense, a heap here can be seen as a partial heap, containing a partial view of the state of +/// the memory. Combining disjoint heaps is then equivalent to conciling two partial views of the +/// memory together. This is our base for separation logic. +/// +/// The heap is instrumented with affine heap predicates, heap predicates that don't change if you +/// augment the heap on which they're valid by joining another partial heap. These affine heap +/// predicates are the terms of our separation logic. +/// +/// Finally, the module defines actions for heap, which are frame-preserving heap updates. + +(**** The base : partial heaps *) + +(** + Abstract type of heaps. Can conceptually be thought of as a map from addresses to + contents of memory cells. +*) +val heap : Type u#(a + 1) +val concrete (h:heap u#a) : H.heap u#a +val ghost (h:heap u#a) : erased (H.heap u#a) +val upd_ghost_heap (h0:heap) (h1:erased heap { concrete h0 == concrete h1 }) + : h2:heap { h2 == reveal h1 } +type tag = + | GHOST + | CONCRETE +(* An empty heap *) +val empty_heap : heap u#a + +(** A [core_ref] is a key into the [heap] or [null] *) +val core_ref : Type u#0 + +(** We index a [core_ref] by the type of its heap contents + and a [pcm] governing it, for ease of type inference *) +let ref (a:Type u#a) (pcm:pcm a) : Type u#0 = core_ref + +val core_ref_null : core_ref + +(** [null] is a specific reference, that is not associated to any value +*) +let null (#a:Type u#a) (#pcm:pcm a) : ref a pcm = core_ref_null + +(** Checking whether [r] is the null pointer is decidable through [is_null] +*) +val core_ref_is_null (r:core_ref) : b:bool { b <==> r == core_ref_null } + +(** Checking whether [r] is the null pointer is decidable through [is_null] +*) +let is_null (#a:Type u#a) (#pcm:pcm a) (r:ref a pcm) : (b:bool{b <==> r == null}) = core_ref_is_null r + +(** The predicate describing non-overlapping heaps *) +val disjoint (h0 h1:heap u#h) : prop + +(** Disjointness is symmetric *) +val disjoint_sym (h0 h1:heap u#h) + : Lemma (disjoint h0 h1 <==> disjoint h1 h0) + [SMTPat (disjoint h0 h1)] + +(** Disjoint heaps can be combined into a bigger heap*) +val join (h0:heap u#h) (h1:heap u#h{disjoint h0 h1}) : heap u#h + +(** The join operation is commutative *) +val join_commutative (h0 h1:heap) + : Lemma + (requires + disjoint h0 h1) + (ensures + (disjoint h1 h0 /\ + join h0 h1 == join h1 h0)) + +(** Disjointness distributes over join *) +val disjoint_join (h0 h1 h2:heap) + : Lemma (disjoint h1 h2 /\ + disjoint h0 (join h1 h2) ==> + disjoint h0 h1 /\ + disjoint h0 h2 /\ + disjoint (join h0 h1) h2 /\ + disjoint (join h0 h2) h1) + +(** Join is associative *) +val join_associative (h0 h1 h2:heap) + : Lemma + (requires + disjoint h1 h2 /\ + disjoint h0 (join h1 h2)) + (ensures + (disjoint h0 h1 /\ + disjoint (join h0 h1) h2 /\ + join h0 (join h1 h2) == join (join h0 h1) h2)) + +(**** Separation logic over heaps *) + +(** + An affine heap proposition or affine heap predicate is a proposition whose validity does not + change if the heap on which it is valid grows. In other terms, it is a proposition that is + compatible with the disjoint/join operations for partial heaps. These affine heap predicates + are the base of our separation logic. +*) +let heap_prop_is_affine (p:heap u#a -> prop) : prop = + forall (h0 h1: heap u#a). p h0 /\ disjoint h0 h1 ==> p (join h0 h1) + +(** + An affine heap proposition + *) +let a_heap_prop = p:(heap -> prop) { heap_prop_is_affine p } + +(** + [slprop] is an abstract "separation logic proposition" + + The [erasable] attribute says that it is computationally irrelevant + and will be extracted to [()] +*) +[@@erasable] +val slprop : Type u#(a + 1) + +(** + [slprop]s can be "interpreted" over any heap, yielding a [prop] +*) +val interp (p:slprop u#a) (m:heap u#a) : prop + +(** + Promoting an affine heap proposition to an slprop + *) +val as_slprop (f:a_heap_prop) : p:slprop{forall h.interp p h <==> f h} + +(** + An [hprop] is heap predicate indexed by a footprint [fp:slprop]. + Its validity depends only on the fragment of the heap that satisfies [fp]. + Note, it is unrelated to affinity, since the forward implication only applies + to heaps [h0] that validate [fp] +*) +let hprop (fp:slprop u#a) = + q:(heap u#a -> prop){ + forall (h0:heap{interp fp h0}) (h1:heap{disjoint h0 h1}). + q h0 <==> q (join h0 h1) + } + +(** A common abbreviation: [hheap p] is a heap on which [p] is valid *) +let hheap (p:slprop u#a) = m:heap u#a {interp p m} + +(** + Equivalence relation on [slprop]s is just + equivalence of their interpretations +*) +let equiv (p1 p2:slprop) = + forall m. interp p1 m <==> interp p2 m + +(** + An extensional equivalence principle for slprop + *) +val slprop_extensionality (p q:slprop) + : Lemma + (requires p `equiv` q) + (ensures p == q) + +/// We can now define all the standard connectives of separation logic + +(** [emp] is the empty [slprop], valid on all heaps. It acts as the unit element *) +val emp : slprop u#a +(** "Points to" allows to talk about the heap contents *) +val pts_to (#a:Type u#a) (#pcm:_) (r:ref a pcm) (v:a) : slprop u#a +// val h_and (p1 p2:slprop u#a) : slprop u#a +// val h_or (p1 p2:slprop u#a) : slprop u#a +val star (p1 p2:slprop u#a) : slprop u#a +// val wand (p1 p2:slprop u#a) : slprop u#a +val h_exists (#[@@@strictly_positive] a:Type u#b) + ([@@@strictly_positive] f: (a -> slprop u#a)) + : slprop u#a +// val h_forall (#a:Type u#b) (f: (a -> slprop u#a)) : slprop u#a +(** + [h_refine] consists of refining a separation logic proposition [p] with an affine heap predicate + [r]. Since both types are equal, this is equivalent to [h_and]. +*) +// val h_refine (p:slprop u#a) (r:a_heap_prop u#a) : slprop u#a + +(***** Basic properties of separation logic *) + +(** If [p * q] is valid on [h], then [p] and [q] are valid on [h] *) +val affine_star (p q:slprop) (h:heap) + : Lemma ((interp (p `star` q) h ==> interp p h /\ interp q h)) + +(** Equivalence of separation logic propositions is symmetric *) +val equiv_symmetric (p1 p2:slprop) + : squash (p1 `equiv` p2 ==> p2 `equiv` p1) + +(** If [p1 ~ p2] then [p1 * p3 ~ p2 * p3] *) +val equiv_extensional_on_star (p1 p2 p3:slprop) + : squash (p1 `equiv` p2 ==> (p1 `star` p3) `equiv` (p2 `star` p3)) + +(** [p ~~ p * emp] *) +val emp_unit (p:slprop) + : Lemma (p `equiv` (p `star` emp)) + +(** [emp] is trivial *) +val intro_emp (h:heap) + : Lemma (interp emp h) + +(** Introduction rule for equivalence of [h_exists] propositions *) +val h_exists_cong (#a:Type) (p q : a -> slprop) + : Lemma + (requires (forall x. p x `equiv` q x)) + (ensures (h_exists p `equiv` h_exists q)) + +(** Introducing [h_exists] by presenting a witness *) +val intro_h_exists (#a:_) (x:a) (p:a -> slprop) (h:heap) + : Lemma (interp (p x) h ==> interp (h_exists p) h) + +(** Eliminate an existential by simply getting a proposition. *) +val elim_h_exists (#a:_) (p:a -> slprop) (h:heap) + : Lemma (interp (h_exists p) h ==> (exists x. interp (p x) h)) + +(** + The interpretation of a separation logic proposition [hp] is itself an [hprop] of footprint + [hp] +*) +val interp_depends_only_on (hp:slprop u#a) + : Lemma + (forall (h0:hheap hp) (h1:heap u#a{disjoint h0 h1}). + interp hp h0 <==> interp hp (join h0 h1)) + + +(***** [pts_to] properties *) + +(** + [ptr r] is a separation logic proposition asserting the existence of an allocated cell at + reference [r] +*) +let ptr (#a: Type u#a) (#pcm: pcm a) (r:ref a pcm) = + h_exists (pts_to r) + +(** + If we have [pts_to x v0] and [pts_to y v1] on the same heap, then [v0] and [v1] are are related + by the PCM governing [x]. Indeed, the [pts_to] predicate is not stricly injective, as our partial + heaps offer only a partial view on the contents of the memory cell. This partial view is governed + by [pcm], and this lemma shows that you can combine two [pts_to] predicates into a third, with + a new value with is the composition of [v0] and [v1] by [pcm]. + This lemma is equivalent to injectivity of [pts_to] if you instantiate [pcm] with the exclusive + PCM. +*) +val pts_to_compatible + (#a:Type u#a) + (#pcm: pcm a) + (x:ref a pcm) + (v0 v1:a) + (h:heap u#a) + : Lemma + (interp (pts_to x v0 `star` pts_to x v1) h + <==> + (composable pcm v0 v1 /\ + interp (pts_to x (op pcm v0 v1)) h)) + +(** If a reference points to two different values, they must be joinable +in the PCM, even when the pointing does not happen separately. *) +val pts_to_join (#a:Type u#a) (#pcm:_) (r:ref a pcm) (v1 v2:a) (m:heap) + : Lemma (requires (interp (pts_to r v1) m /\ interp (pts_to r v2) m)) + (ensures joinable pcm v1 v2) + +(** Further, the value in the heap is a witness for that property *) +val pts_to_join' (#a:Type u#a) (#pcm:_) (r:ref a pcm) (v1 v2:a) (m:heap) + : Lemma (requires (interp (pts_to r v1) m /\ interp (pts_to r v2) m)) + (ensures (exists z. compatible pcm v1 z /\ compatible pcm v2 z /\ + interp (pts_to r z) m)) + +val pts_to_compatible_equiv (#a:Type) + (#pcm:_) + (x:ref a pcm) + (v0:a) + (v1:a{composable pcm v0 v1}) + : Lemma (equiv (pts_to x v0 `star` pts_to x v1) + (pts_to x (op pcm v0 v1))) + +val pts_to_not_null (#a:Type) + (#pcm:_) + (x:ref a pcm) + (v:a) + (m:heap) + : Lemma (requires interp (pts_to x v) m) + (ensures x =!= null) + +(***** Properties of separating conjunction *) + +(** The separating conjunction [star] arises from the disjointness of partial heaps *) +val intro_star (p q:slprop) (hp:hheap p) (hq:hheap q) + : Lemma + (requires disjoint hp hq) + (ensures interp (p `star` q) (join hp hq)) + +val elim_star (p q:slprop) (h:hheap (p `star` q)) + : Lemma + (requires interp (p `star` q) h) + (ensures exists hl hr. + disjoint hl hr /\ + h == join hl hr /\ + interp p hl /\ + interp q hr) + +(** [star] is commutative *) +val star_commutative (p1 p2:slprop) + : Lemma ((p1 `star` p2) `equiv` (p2 `star` p1)) + +(** [star] is associative *) +val star_associative (p1 p2 p3:slprop) + : Lemma ( + (p1 `star` (p2 `star` p3)) + `equiv` + ((p1 `star` p2) `star` p3) + ) + +(** If [p1 ~ p3] and [p2 ~ p4], then [p1 * p2 ~ p3 * p4] *) +val star_congruence (p1 p2 p3 p4:slprop) + : Lemma (requires p1 `equiv` p3 /\ p2 `equiv` p4) + (ensures (p1 `star` p2) `equiv` (p3 `star` p4)) + +(***** Properties of the refinement *) + +// (** [h_refine p q] is just interpreting the affine heap prop [q] when [p] is valid *) +// val refine_interp (p:slprop u#a) (q:a_heap_prop u#a) (h:heap u#a) +// : Lemma (interp p h /\ q h <==> interp (h_refine p q) h) + +// (** +// Equivalence on [h_refine] propositions is define by logical equivalence of the refinements +// on all heaps +// *) +// val refine_equiv (p0 p1:slprop u#a) (q0 q1:a_heap_prop u#a) +// : Lemma (p0 `equiv` p1 /\ (forall h. q0 h <==> q1 h) ==> +// equiv (h_refine p0 q0) (h_refine p1 q1)) + +(** + A [pure] separation logic predicate is a refinement on the empty heap. That is how we + lift pure propositions to the separation logic world +*) +val pure (p:prop) : slprop + +(** Equivalence of pure propositions is the equivalence of the underlying propositions *) +val pure_equiv (p q:prop) + : Lemma ((p <==> q) ==> (pure p `equiv` pure q)) + +(** And the interpretation of pure propositions is their underlying propositions *) +val pure_interp (q:prop) (h:heap u#a) + : Lemma (interp (pure q) h <==> q) + +(** A helper lemma for interpreting a pure proposition with another [slprop] *) +val pure_star_interp (p:slprop u#a) (q:prop) (h:heap u#a) + : Lemma (interp (p `star` pure q) h <==> + interp (p `star` emp) h /\ q) + +(***** Magic wand and implications properties *) + +(** We can define a [stronger] relation on [slprops], defined by interpretation implication *) +let stronger (p q:slprop) = + forall h. interp p h ==> interp q h + +(** [stronger] is stable when adding another starred [slprop] *) +val stronger_star (p q r:slprop) + : Lemma (stronger q r ==> stronger (p `star` q) (p `star` r)) + +(** If [q > r] and [p * q] is valid, then [p * r] is valid *) +val weaken (p q r:slprop) (h:heap u#a) + : Lemma (q `stronger` r /\ interp (p `star` q) h ==> interp (p `star` r) h) + +(**** Actions *) + +(** An abstract predicate classifying a "full" heap, i.e., the entire + heap of the executing program, not just a fragment of it *) +val full_heap_pred : heap -> prop + +let full_heap = h:heap { full_heap_pred h } + +let full_hheap fp = h:hheap fp { full_heap_pred h } + +(** + This modules exposes a preorder that is respected for every well-formed update of the heap. + The preorder represents the fact that once a reference is allocated, its type and PCM cannot + change and the trace of values contained in the PCM respects the preorder induced by the + PCM (see Steel.Preorder). +*) +val heap_evolves : FStar.Preorder.preorder full_heap + +(** + This predicate allows us to maintain an allocation counter, as all references above [a] + in [h] are free. +*) +val free_above_addr (t:tag) (h:heap u#a) (a:nat) : prop + +(** [free_above_addr] is abstract but can be weakened consistently with its intended behavior *) +val weaken_free_above (t:tag) (h:heap) (a b:nat) + : Lemma (free_above_addr t h a /\ a <= b ==> free_above_addr t h b) + +(** + The base type for an action is indexed by two separation logic propositions, representing + the heap specification of the action before and after. +*) +let trivial_pre (h:heap) : prop = True + +let pre_action (#[T.exact (`trivial_pre)]pre:heap -> prop) + (#[T.exact (`trivial_pre)]post:heap -> prop) + (fp:slprop u#a) + (a:Type u#b) + (fp':a -> slprop u#a) + = h0:full_hheap fp { pre h0 } -> res:(x:a & full_hheap (fp' x)) { post (dsnd res) } + +(** + This is how the heaps before and after the action relate: + - evolving the heap according to the heap preorder; + - not allocating any new references; + - preserving the validity of any heap proposition affecting any frame +*) +type mutability = + | ONLY_GHOST + | IMMUTABLE + | MUTABLE +let no_allocs : option tag = None +let does_not_allocate (t:tag) (h0 h1:heap) = + forall ctr. free_above_addr t h0 ctr ==> free_above_addr t h1 ctr +let maybe_allocates (t:option tag) (h0 h1:heap) = + match t with + | None -> + does_not_allocate CONCRETE h0 h1 /\ + does_not_allocate GHOST h0 h1 + | Some CONCRETE -> + does_not_allocate GHOST h0 h1 + | Some GHOST -> + does_not_allocate CONCRETE h0 h1 + +unfold +let action_related_heaps + (#[T.exact (`MUTABLE)] m:mutability) + (#[T.exact (`no_allocs)] allocates:option tag) + (h0 h1:full_heap) = + heap_evolves h0 h1 /\ + maybe_allocates allocates h0 h1 /\ + (match m with + | ONLY_GHOST -> + concrete h0 == concrete h1 + | IMMUTABLE -> + h0 == h1 + | _ -> True) + + +(** + We only want to consider heap updates that are "frame-preserving", meaning that they only + modify the portion of the heap that they're allowed to, without messing with any other + partial view of the heap that is compatible with the one you own. This includes : + - preserving correct interpretation in presence of a frame; + - heaps are related as defined above +*) +let is_frame_preserving + (#a: Type u#a) + (#pre #post:_) + (#fp: slprop u#b) + (#fp': a -> slprop u#b) + (immut:mutability) + (allocates:option tag) + (f:pre_action #pre #post fp a fp') + = + forall (frame: slprop u#b) (h0:full_hheap (fp `star` frame) { pre h0 }). + (affine_star fp frame h0; + let (| x, h1 |) = f h0 in + interp (fp' x `star` frame) h1 /\ + action_related_heaps #immut #allocates h0 h1) + +(** Every action is frame-preserving *) +let action (#[T.exact (`MUTABLE)] mut:mutability) + (#[T.exact (`no_allocs)] allocates:option tag) + (#[T.exact (`trivial_pre)]pre:heap -> prop) + (#[T.exact (`trivial_pre)]post:heap -> prop) + (fp:slprop u#b) (a:Type u#a) (fp':a -> slprop u#b) = + f:pre_action #pre #post fp a fp'{ is_frame_preserving mut allocates f } + +(** + We define a second, but equivalent, type for actions that + instead of quantifying over the frame, are explicitly passed a frame + from outside + + This notion of action is useful for defining actions like witness_h_exists, see comments at the declaration of witness_h_exists +*) +let action_with_frame + (fp:slprop u#a) + (a:Type u#b) + (fp':a -> slprop u#a) + = frame:slprop u#a -> + h0:full_hheap (fp `star` frame) -> + Pure (x:a & full_hheap (fp' x `star` frame)) + (requires True) + (ensures fun (| x, h1 |) -> action_related_heaps #IMMUTABLE #no_allocs h0 h1) + +(** + Two heaps [h0] and [h1] are frame-related if you can get from [h0] to [h1] with a + frame-preserving update. +*) +let frame_related_heaps (h0 h1:full_heap) (fp0 fp1 frame:slprop) + (mut:mutability) (allocates:option tag) = + interp (fp0 `star` frame) h0 ==> + interp (fp1 `star` frame) h1 /\ + action_related_heaps #mut #allocates h0 h1 + + +(** + A frame-preserving action applied on [h0] produces an [h1] such that [h0] and [h1] are + frame-related +*) +let action_framing + (#a: Type u#a) + (#mut #allocates:_) + (#fp: slprop u#b) + (#fp': a -> slprop u#b) + ($f:action #mut #allocates fp a fp') + (frame:slprop) (h0:full_hheap (fp `star` frame)) + : Lemma ( + affine_star fp frame h0; + let (| x, h1 |) = f h0 in + frame_related_heaps h0 h1 fp (fp' x) frame mut allocates + ) + = + affine_star fp frame h0; + emp_unit fp + +(** [sel] is a ghost read of the value contained in a heap reference *) +val sel (#a:Type u#h) (#pcm:pcm a) (r:ref a pcm) (m:full_hheap (ptr r)) : a + +(** [sel_v] is a ghost read of the value contained in a heap reference *) +val sel_v (#a:Type u#h) (#pcm:pcm a) (r:ref a pcm) (v:erased a) (m:full_hheap (pts_to r v)) + : v':a{ compatible pcm v v' /\ + pcm.refine v' /\ + interp (ptr r) m /\ + v' == sel r m } + +(** [sel] respect [pts_to] *) +val sel_lemma (#a:_) (#pcm:_) (r:ref a pcm) (m:full_hheap (ptr r)) + : Lemma (interp (pts_to r (sel r m)) m) + +let witnessed_ref (#a:Type u#a) + (#pcm:pcm a) + (r:ref a pcm) + (fact:a -> prop) + (h:full_heap) + = interp (ptr r) h /\ + fact (sel r h) + +val witnessed_ref_stability (#a:Type) (#pcm:pcm a) (r:ref a pcm) (fact:a -> prop) + : Lemma + (requires FStar.Preorder.stable fact (PulseCore.Preorder.preorder_of_pcm pcm)) + (ensures FStar.Preorder.stable (witnessed_ref r fact) heap_evolves) + +(** + The action variant of [sel], returning the "true" value inside the heap. This "true" value + can be different of the [pts_to] value you assumed at the beginning, because of the PCM structure +*) +val sel_action + (#a:Type u#a) + (#pcm:pcm a) + (r:ref a pcm) + (v0:erased a) + : action #IMMUTABLE #no_allocs + (pts_to r v0) (v:a{compatible pcm v0 v}) (fun _ -> pts_to r v0) + +(** + A version of select that incorporates a ghost update of local + knowledge of a ref cell based on the value that was read + *) +val select_refine (#a:_) (#p:_) + (r:ref a p) + (x:erased a) + (f:(v:a{compatible p x v} + -> GTot (y:a{compatible p y v /\ + FStar.PCM.frame_compatible p x v y}))) + : action #IMMUTABLE #no_allocs (pts_to r x) + (v:a{compatible p x v /\ p.refine v}) + (fun v -> pts_to r (f v)) + + +(** Updating a ref cell for a user-defined PCM *) +val upd_gen_action (#a:Type) (#p:pcm a) (r:ref a p) (x y:Ghost.erased a) + (f:FStar.PCM.frame_preserving_upd p x y) + : action #MUTABLE #no_allocs (pts_to r x) + unit + (fun _ -> pts_to r y) + +(** + The update action needs you to prove that the mutation from [v0] to [v1] is frame-preserving + with respect to the individual PCM governing the reference [r]. See [FStar.PCM.frame_preserving] +*) +val upd_action + (#a:Type u#a) + (#pcm:pcm a) + (r:ref a pcm) + (v0:FStar.Ghost.erased a) + (v1:a {FStar.PCM.frame_preserving pcm v0 v1 /\ pcm.refine v1}) + : action #MUTABLE #no_allocs (pts_to r v0) unit (fun _ -> pts_to r v1) + +(** Deallocating a reference, by actually replacing its value by the unit of the PCM *) +val free_action + (#a:Type u#a) + (#pcm:pcm a) + (r:ref a pcm) + (v0:FStar.Ghost.erased a {exclusive pcm v0 /\ pcm.refine pcm.FStar.PCM.p.one}) + : action #MUTABLE #no_allocs (pts_to r v0) unit (fun _ -> pts_to r pcm.FStar.PCM.p.one) + + +(** Splitting a permission on a composite resource into two separate permissions *) +val split_action + (#a:Type u#a) + (#pcm:pcm a) + (r:ref a pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a{composable pcm v0 v1}) + : action #IMMUTABLE #no_allocs (pts_to r (v0 `op pcm` v1)) unit (fun _ -> pts_to r v0 `star` pts_to r v1) + +(** Combining separate permissions into a single composite permission *) +val gather_action + (#a:Type u#a) + (#pcm:pcm a) + (r:ref a pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a) + : action #IMMUTABLE #no_allocs + (pts_to r v0 `star` pts_to r v1) (_:unit{composable pcm v0 v1}) (fun _ -> pts_to r (op pcm v0 v1)) + +val pts_to_not_null_action + (#a:Type u#a) + (#pcm:pcm a) + (r:erased (ref a pcm)) + (v:Ghost.erased a) +: action #IMMUTABLE #no_allocs + (pts_to r v) + (squash (not (is_null r))) + (fun _ -> pts_to r v) + +(** Allocating is a pseudo action here, the context needs to provide a fresh address *) +val extend + (#a:Type u#a) + (#pcm:pcm a) + (x:a{compatible pcm x x /\ pcm.refine x}) + (addr:nat) + : action + #MUTABLE #(Some CONCRETE) + #(fun h -> h `free_above_addr CONCRETE` addr) + #(fun h -> h `free_above_addr CONCRETE` (addr + 1)) + emp + (ref a pcm) + (fun r -> pts_to r x) + +val frame (#a:Type) + #immut #allocates #hpre #hpost + (#pre:slprop) + (#post:a -> slprop) + (frame:slprop) + ($f:action #immut #allocates #hpre #hpost pre a post) + : action #immut #allocates #hpre #hpost (pre `star` frame) a (fun x -> post x `star` frame) + +val change_slprop (p q:slprop) + (proof: (h:heap -> Lemma (requires interp p h) (ensures interp q h))) + : action #IMMUTABLE #no_allocs p unit (fun _ -> q) + +// module U = FStar.Universe + +// val id_elim_star (p q:slprop) (h:heap) +// : Pure (erased heap & erased heap ) +// (requires (interp (p `star` q) h)) +// (ensures (fun (hl, hr) -> disjoint hl hr +// /\ h == join hl hr +// /\ interp p hl +// /\ interp q hr)) + +// val id_elim_exists (#a:Type) (p : a -> slprop) (h:heap) +// : Pure (erased a) +// (requires (interp (h_exists p) h)) +// (ensures (fun x -> interp (p x) h)) + + +// let is_frame_monotonic #a (p : a -> slprop) : prop = +// forall x y m frame. interp (p x `star` frame) m /\ interp (p y) m ==> interp (p y `star` frame) m + +// let is_witness_invariant #a (p : a -> slprop) = +// forall x y m. interp (p x) m /\ interp (p y) m ==> x == y + +// val witinv_framon (#a:_) (p : a -> slprop) +// : Lemma (requires (is_witness_invariant p)) +// (ensures (is_frame_monotonic p)) + + +(** + witness_h_exists is defined with action_with_frame as it allows us to define it with any p + + With the quantified frame actions, it creates an issue, since we have to prove that the witness is ok for all frames + whereas with an explicit frame, we can pick the witness for that particular frame +*) +val elim_exists (#a:_) (p:a -> slprop) + : action_with_frame (h_exists p) (erased a) (fun x -> p x) + +val intro_exists (#a:_) (p:a -> slprop) (x:erased a) + : action_with_frame (p x) unit (fun _ -> h_exists p) + +val lift_exists (#a:_) (p:a -> slprop) + : action #IMMUTABLE #no_allocs (h_exists p) unit + (fun _a -> h_exists #(FStar.Universe.raise_t a) (FStar.Universe.lift_dom p)) + +val elim_pure (p:prop) + : action #IMMUTABLE #no_allocs (pure p) (u:unit{p}) (fun _ -> emp) + +val intro_pure (p:prop) (_:squash p) + : action #IMMUTABLE #no_allocs emp unit (fun _ -> pure p) + +val pts_to_evolve (#a:Type u#a) (#pcm:_) (r:ref a pcm) (x y : a) (h:heap) + : Lemma (requires (interp (pts_to r x) h /\ compatible pcm y x)) + (ensures (interp (pts_to r y) h)) + +val drop (p:slprop) + : action #IMMUTABLE #no_allocs p unit (fun _ -> emp) + +let non_informative (a:Type u#a) = + x:Ghost.erased a -> y:a{y == Ghost.reveal x} + +val lift_erased + (#a:Type) + (#ni_a:non_informative a) + (#allocs:option tag) + #hpre #hpost + (#pre:slprop) + (#post:a -> slprop) + ($f:erased (action #ONLY_GHOST #allocs #hpre #hpost pre a post)) +: action #ONLY_GHOST #allocs #hpre #hpost pre a post + +[@@erasable] +val ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused]p:pcm a) : Type0 +val ghost_pts_to (#a:Type u#a) (#p:pcm a) (r:ghost_ref p) (v:a) : slprop u#a + +val ghost_extend + (#a:Type u#a) + (#pcm:pcm a) + (x:erased a{compatible pcm x x /\ pcm.refine x}) + (addr:erased nat) +: action #ONLY_GHOST #(Some GHOST) + #(fun h -> h `free_above_addr GHOST` addr) + #(fun h -> h `free_above_addr GHOST` (addr + 1)) + emp + (ghost_ref pcm) + (fun r -> ghost_pts_to r x) + +val ghost_read + (#a:Type) + (#p:pcm a) + (r:ghost_ref p) + (x:erased a) + (f:(v:a{compatible p x v} + -> GTot (y:a{compatible p y v /\ + FStar.PCM.frame_compatible p x v y}))) +: action #IMMUTABLE + (ghost_pts_to r x) + (erased (v:a{compatible p x v /\ p.refine v})) + (fun v -> ghost_pts_to r (f v)) + +val ghost_write + (#a:Type) + (#p:pcm a) + (r:ghost_ref p) + (x y:Ghost.erased a) + (f:FStar.PCM.frame_preserving_upd p x y) +: action #ONLY_GHOST + (ghost_pts_to r x) + unit + (fun _ -> ghost_pts_to r y) + +val ghost_share + (#a:Type) + (#pcm:pcm a) + (r:ghost_ref pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a{composable pcm v0 v1}) +: action #IMMUTABLE + (ghost_pts_to r (v0 `op pcm` v1)) + unit + (fun _ -> ghost_pts_to r v0 `star` ghost_pts_to r v1) + +val ghost_gather + (#a:Type) + (#pcm:pcm a) + (r:ghost_ref pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a) +: action #IMMUTABLE + (ghost_pts_to r v0 `star` ghost_pts_to r v1) + (squash (composable pcm v0 v1)) + (fun _ -> ghost_pts_to r (op pcm v0 v1)) diff --git a/lib/pulse/core/PulseCore.HeapLike.fst b/lib/pulse/core/PulseCore.HeapLike.fst new file mode 100644 index 000000000..87653a53c --- /dev/null +++ b/lib/pulse/core/PulseCore.HeapLike.fst @@ -0,0 +1,39 @@ +module PulseCore.HeapLike +noeq +type splittable (a:Type) = { + disjoint : a -> a -> prop; + join : x:a -> y:a {disjoint x y } -> a; + laws : squash ( + (forall (x:a) (y:a). disjoint x y <==> disjoint y x) /\ + (forall (x:a) (y:a) (z:a). disjoint y z /\ disjoint x (join y z) ==> + disjoint x y /\ + disjoint x z /\ + disjoint (join x y) z /\ + disjoint (join x z) y /\ + join x (join y z) == join (join x y) z) + ) +} +noeq +type lens (a:Type) (b:Type) = { + get : a -> GTot b; + put : b -> a -> GTot a; + sa: splittable a; + sb: splittable b; + lens_laws : squash ( + (forall (x:a). put (get x) x == x) /\ + (forall (x:a) (y:b). get (put y x) == y) /\ + (forall (x:a) (y:b) (z:b). put z (put y x) == put z x + ) + ); + law0: (x:a) -> (y:a) -> Lemma ( + sa.disjoint x y ==> + sb.disjoint (get x) (get y) /\ + get (sa.join x y) == sb.join (get x) (get y) + ); + law1: (x:a) -> (y:a) -> l:b -> m:b -> Lemma ( + sa.disjoint x y /\ + sb.disjoint l m ==> + sa.disjoint (put l x) (put m y) /\ + sa.join (put l x) (put m y) == put (sb.join l m) (sa.join x y) + ) +} diff --git a/lib/pulse/core/PulseCore.Memory.fst b/lib/pulse/core/PulseCore.Memory.fst index 766f2935c..5f9f239d1 100644 --- a/lib/pulse/core/PulseCore.Memory.fst +++ b/lib/pulse/core/PulseCore.Memory.fst @@ -19,7 +19,7 @@ open FStar.PCM module M_ = PulseCore.NondeterministicMonotonicStateMonad module F = FStar.FunctionalExtensionality open FStar.FunctionalExtensionality -module H = PulseCore.Heap +module H = PulseCore.Heap2 module PP = PulseCore.Preorder @@ -33,6 +33,7 @@ noeq type mem : Type u#(a + 1) = { ctr: nat; + ghost_ctr: erased nat; heap: H.heap u#a; locks: lock_store u#a; } @@ -41,16 +42,24 @@ let heap_of_mem (x:mem) : H.heap = x.heap let mem_of_heap (h:H.heap) : mem = { ctr = 0; + ghost_ctr = 0; heap = h; locks = [] } let mem_set_heap (m:mem) (h:H.heap) : mem = { - ctr = m.ctr; - heap = h; - locks = m.locks; + m with heap = h; } +let is_ghost_action m0 m1 = + H.concrete m0.heap == H.concrete m1.heap /\ + m0.ctr == m1.ctr /\ + m0.locks == m1.locks + +let ghost_action_preorder (_:unit) + : Lemma (FStar.Preorder.preorder_rel is_ghost_action) + = () + let core_mem (m:mem) : mem = mem_of_heap (heap_of_mem m) val core_mem_invol (m: mem u#a) : Lemma @@ -62,6 +71,7 @@ let core_mem_invol m = () let disjoint (m0 m1:mem u#h) : prop = m0.ctr == m1.ctr /\ + m0.ghost_ctr == m1.ghost_ctr /\ H.disjoint m0.heap m1.heap /\ m0.locks == m1.locks @@ -75,6 +85,7 @@ let disjoint_sym (m0 m1:mem u#h) let join (m0:mem u#h) (m1:mem u#h{disjoint m0 m1}) : mem u#h = { ctr = m0.ctr; + ghost_ctr = m0.ghost_ctr; heap = H.join m0.heap m1.heap; locks = m0.locks } @@ -123,7 +134,7 @@ let slprop_extensionality p q = let aux (h:H.heap) : Lemma (H.interp p h <==> H.interp q h) [SMTPat (H.interp p h)] - = let m : mem = { ctr = 0; heap = h; locks = [] } in + = let m : mem = { ctr = 0; ghost_ctr=0; heap = h; locks = [] } in assert (interp p m <==> interp q m) in assert (forall h. H.interp p h <==> H.interp q h); @@ -143,12 +154,8 @@ let core_ref_is_null r = H.core_ref_is_null r let emp : slprop u#a = H.emp let pure = H.pure let pts_to = H.pts_to -let h_and = H.h_and -let h_or = H.h_or let star = H.star -let wand = H.wand let h_exists = H.h_exists -let h_forall = H.h_forall //////////////////////////////////////////////////////////////////////////////// //properties of equiv @@ -447,16 +454,17 @@ let rec move_invariant (e:inames) (l:lock_store) (p:slprop) end end -let heap_ctr_valid (ctr:nat) (h:H.heap u#a) : prop = - h `H.free_above_addr` ctr +let heap_ctr_valid (ctr:nat) (ghost_ctr:nat) (h:H.heap u#a) : prop = + h `H.free_above_addr H.CONCRETE` ctr /\ + h `H.free_above_addr H.GHOST` ghost_ctr -let ctr_validity (ctr:nat) (h:H.heap) : slprop = - H.pure (heap_ctr_valid ctr h) +let ctr_validity (ctr:nat) (ghost_ctr:nat) (h:H.heap) : slprop = + H.pure (heap_ctr_valid ctr ghost_ctr h) let locks_invariant (e:inames) (m:mem u#a) : slprop u#a = lock_store_invariant e m.locks `star` - ctr_validity m.ctr (heap_of_mem m) + ctr_validity m.ctr m.ghost_ctr (heap_of_mem m) let full_mem_pred (m:mem) = H.full_heap_pred (heap_of_mem m) @@ -496,10 +504,10 @@ let mem_prop_is_affine let a_mem_prop (sl: slprop u#a) : Type u#(a+1) = (f: (hmem sl -> Tot prop) { mem_prop_is_affine sl f }) -val refine_slprop - (sl: slprop u#a) - (f: a_mem_prop sl) -: Tot (slprop u#a) +// val refine_slprop +// (sl: slprop u#a) +// (f: a_mem_prop sl) +// : Tot (slprop u#a) let core_mem_interp (hp:slprop u#a) (m:mem u#a) = () @@ -526,125 +534,125 @@ let a_mem_prop_as_a_heap_prop Classical.forall_intro_2 phi1; g -let refine_slprop sl f = H.as_slprop (a_mem_prop_as_a_heap_prop sl f) - -val interp_refine_slprop - (sl: slprop u#a) - (f: a_mem_prop sl) - (m: mem u#a) -: Lemma - (interp (refine_slprop sl f) m <==> (interp sl m /\ f m)) - [SMTPat (interp (refine_slprop sl f) m)] - -let interp_refine_slprop sl f m = - assert ((interp sl m /\ f m) <==> interp sl (core_mem m) /\ f (core_mem m)) - -let dep_hprop - (s: slprop) - (f: (hmem s -> Tot slprop)) - (h: H.heap) -: Tot prop -= exists (h1: H.heap) . exists (h2: H.heap) . interp s (mem_of_heap h1) /\ H.disjoint h1 h2 /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ h == h1 `H.join` h2 - -let dep_hprop_is_affine0 - (s: slprop) - (f: (hmem s -> Tot slprop)) - (h h': H.heap) - (sq' : squash (dep_hprop s f h /\ H.disjoint h h')) -: Lemma - (H.disjoint h h' /\ dep_hprop s f (H.join h h')) -= - let p2 (h h1 h2: H.heap) : Tot prop = - interp s (mem_of_heap h1) /\ - H.disjoint h1 h2 /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ h == h1 `H.join` h2 - in - let p1 (h h1: H.heap) : Tot prop = - (exists h2 . p2 h h1 h2) - in - let h1 = - FStar.IndefiniteDescription.indefinite_description_ghost H.heap (p1 h) - in - let h2 = - FStar.IndefiniteDescription.indefinite_description_ghost H.heap (p2 h h1) - in - H.disjoint_join h' h1 h2; - assert (H.disjoint h2 h'); - let h2' = H.join h2 h' in - H.join_commutative h2 h' ; - assert (h2' == H.join h' h2); - assert (H.disjoint h1 h2'); - assert (mem_of_heap h2' == mem_of_heap h2 `join` mem_of_heap h'); - interp_depends_only_on (f (mem_of_heap h1)); - assert (interp (f (mem_of_heap h1)) (mem_of_heap h2')); - H.join_commutative h1 h2; - H.join_associative h' h2 h1; - H.join_commutative h' h; - H.join_commutative h2' h1; - assert (H.join h h' == h1 `H.join` h2') - -let impl_intro_gen (#p: Type0) (#q: Type0) ($prf: (squash p -> Lemma (q ))) - : Lemma (p ==> q) -= Classical.impl_intro_gen #p #(fun _ -> q) prf - -let dep_hprop_is_affine1 - (s: slprop) - (f: (hmem s -> Tot slprop)) - (h0 h1: H.heap) -: Lemma - ((dep_hprop s f h0 /\ H.disjoint h0 h1) ==> (H.disjoint h0 h1 /\ dep_hprop s f (H.join h0 h1))) -= impl_intro_gen (dep_hprop_is_affine0 s f h0 h1) - -let dep_hprop_is_affine - (s: slprop) - (f: (hmem s -> Tot slprop)) -: Lemma - (H.heap_prop_is_affine (dep_hprop s f)) -= Classical.forall_intro_2 (dep_hprop_is_affine1 s f) - -let sdep - (s: slprop) - (f: (hmem s -> Tot slprop)) -: Tot slprop -= - dep_hprop_is_affine s f; - H.as_slprop (dep_hprop s f) - -let dep_slprop_is_affine - (s: slprop) - (f: (hmem s -> Tot slprop)) -: Tot prop -= (forall (h: hmem s) . f h `equiv` f (core_mem h)) - -let interp_sdep - (s: slprop) - (f: (hmem s -> Tot slprop)) - (m: mem) -: Lemma - (requires (dep_slprop_is_affine s f)) - (ensures ( - interp (sdep s f) m <==> (exists m1 m2 . interp s m1 /\ interp (f m1) m2 /\ disjoint m1 m2 /\ join m1 m2 == m) - )) -= - dep_hprop_is_affine s f; - assert (forall m1 m2 . (interp s m1 /\ interp (f m1) m2 /\ disjoint m1 m2 /\ join m1 m2 == m) ==> ( - interp s (mem_of_heap m1.heap) /\ interp (f (mem_of_heap m1.heap)) (mem_of_heap m2.heap) /\ - H.disjoint m1.heap m2.heap /\ - H.join m1.heap m2.heap == m.heap - )); - interp_depends_only_on s; - Classical.forall_intro (fun m -> interp_depends_only_on (f m)); - assert (forall h1 h2 . (interp s (mem_of_heap h1) /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ H.disjoint h1 h2 /\ H.join h1 h2 == m.heap) ==> ( - core_mem (mem_of_heap h1) == core_mem (mem_set_heap m h1) /\ - interp s (core_mem (mem_of_heap h1)) /\ - interp s (mem_set_heap m h1) /\ - core_mem (mem_of_heap h1) == core_mem (mem_set_heap m h1) /\ - f (mem_set_heap m h1) `equiv` f (mem_of_heap h1) /\ - interp (f (mem_set_heap m h1)) (mem_of_heap h2) /\ - interp (f (mem_set_heap m h1)) (mem_set_heap m h2) /\ - disjoint (mem_set_heap m h1) (mem_set_heap m h2) /\ - join (mem_set_heap m h1) (mem_set_heap m h2) == m - )); - () +// let refine_slprop sl f = H.as_slprop (a_mem_prop_as_a_heap_prop sl f) + +// val interp_refine_slprop +// (sl: slprop u#a) +// (f: a_mem_prop sl) +// (m: mem u#a) +// : Lemma +// (interp (refine_slprop sl f) m <==> (interp sl m /\ f m)) +// [SMTPat (interp (refine_slprop sl f) m)] + +// let interp_refine_slprop sl f m = +// assert ((interp sl m /\ f m) <==> interp sl (core_mem m) /\ f (core_mem m)) + +// let dep_hprop +// (s: slprop) +// (f: (hmem s -> Tot slprop)) +// (h: H.heap) +// : Tot prop +// = exists (h1: H.heap) . exists (h2: H.heap) . interp s (mem_of_heap h1) /\ H.disjoint h1 h2 /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ h == h1 `H.join` h2 + +// let dep_hprop_is_affine0 +// (s: slprop) +// (f: (hmem s -> Tot slprop)) +// (h h': H.heap) +// (sq' : squash (dep_hprop s f h /\ H.disjoint h h')) +// : Lemma +// (H.disjoint h h' /\ dep_hprop s f (H.join h h')) +// = +// let p2 (h h1 h2: H.heap) : Tot prop = +// interp s (mem_of_heap h1) /\ +// H.disjoint h1 h2 /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ h == h1 `H.join` h2 +// in +// let p1 (h h1: H.heap) : Tot prop = +// (exists h2 . p2 h h1 h2) +// in +// let h1 = +// FStar.IndefiniteDescription.indefinite_description_ghost H.heap (p1 h) +// in +// let h2 = +// FStar.IndefiniteDescription.indefinite_description_ghost H.heap (p2 h h1) +// in +// H.disjoint_join h' h1 h2; +// assert (H.disjoint h2 h'); +// let h2' = H.join h2 h' in +// H.join_commutative h2 h' ; +// assert (h2' == H.join h' h2); +// assert (H.disjoint h1 h2'); +// assert (mem_of_heap h2' == mem_of_heap h2 `join` mem_of_heap h'); +// interp_depends_only_on (f (mem_of_heap h1)); +// assert (interp (f (mem_of_heap h1)) (mem_of_heap h2')); +// H.join_commutative h1 h2; +// H.join_associative h' h2 h1; +// H.join_commutative h' h; +// H.join_commutative h2' h1; +// assert (H.join h h' == h1 `H.join` h2') + +// let impl_intro_gen (#p: Type0) (#q: Type0) ($prf: (squash p -> Lemma (q ))) +// : Lemma (p ==> q) +// = Classical.impl_intro_gen #p #(fun _ -> q) prf + +// let dep_hprop_is_affine1 +// (s: slprop) +// (f: (hmem s -> Tot slprop)) +// (h0 h1: H.heap) +// : Lemma +// ((dep_hprop s f h0 /\ H.disjoint h0 h1) ==> (H.disjoint h0 h1 /\ dep_hprop s f (H.join h0 h1))) +// = impl_intro_gen (dep_hprop_is_affine0 s f h0 h1) + +// let dep_hprop_is_affine +// (s: slprop) +// (f: (hmem s -> Tot slprop)) +// : Lemma +// (H.heap_prop_is_affine (dep_hprop s f)) +// = Classical.forall_intro_2 (dep_hprop_is_affine1 s f) + +// let sdep +// (s: slprop) +// (f: (hmem s -> Tot slprop)) +// : Tot slprop +// = +// dep_hprop_is_affine s f; +// H.as_slprop (dep_hprop s f) + +// let dep_slprop_is_affine +// (s: slprop) +// (f: (hmem s -> Tot slprop)) +// : Tot prop +// = (forall (h: hmem s) . f h `equiv` f (core_mem h)) + +// let interp_sdep +// (s: slprop) +// (f: (hmem s -> Tot slprop)) +// (m: mem) +// : Lemma +// (requires (dep_slprop_is_affine s f)) +// (ensures ( +// interp (sdep s f) m <==> (exists m1 m2 . interp s m1 /\ interp (f m1) m2 /\ disjoint m1 m2 /\ join m1 m2 == m) +// )) +// = +// dep_hprop_is_affine s f; +// assert (forall m1 m2 . (interp s m1 /\ interp (f m1) m2 /\ disjoint m1 m2 /\ join m1 m2 == m) ==> ( +// interp s (mem_of_heap m1.heap) /\ interp (f (mem_of_heap m1.heap)) (mem_of_heap m2.heap) /\ +// H.disjoint m1.heap m2.heap /\ +// H.join m1.heap m2.heap == m.heap +// )); +// interp_depends_only_on s; +// Classical.forall_intro (fun m -> interp_depends_only_on (f m)); +// assert (forall h1 h2 . (interp s (mem_of_heap h1) /\ interp (f (mem_of_heap h1)) (mem_of_heap h2) /\ H.disjoint h1 h2 /\ H.join h1 h2 == m.heap) ==> ( +// core_mem (mem_of_heap h1) == core_mem (mem_set_heap m h1) /\ +// interp s (core_mem (mem_of_heap h1)) /\ +// interp s (mem_set_heap m h1) /\ +// core_mem (mem_of_heap h1) == core_mem (mem_set_heap m h1) /\ +// f (mem_set_heap m h1) `equiv` f (mem_of_heap h1) /\ +// interp (f (mem_set_heap m h1)) (mem_of_heap h2) /\ +// interp (f (mem_set_heap m h1)) (mem_set_heap m h2) /\ +// disjoint (mem_set_heap m h1) (mem_set_heap m h2) /\ +// join (mem_set_heap m h1) (mem_set_heap m h2) == m +// )); +// () (** See [Steel.Heap.h_exists_cong] *) val h_exists_cong (#a:Type) (p q : a -> slprop) @@ -730,11 +738,11 @@ effect MstTotNF (a:Type u#a) (except:inames) (expects:slprop u#1) (provides: a - - via MstTotNF for the rest *) -let tot_pre_action_nf_except (e:inames) (fp:slprop u#a) (a:Type u#b) (fp':a -> slprop u#a) = - hmem_with_inv_except e fp -> - (x:a & hmem_with_inv_except e (fp' x)) +let tot_pre_action_nf_except (maybe_ghost:bool) (e:inames) (fp:slprop u#a) (a:Type u#b) (fp':a -> slprop u#a) = + m0:hmem_with_inv_except e fp -> + res:(x:a & hmem_with_inv_except e (fp' x)) { maybe_ghost_action maybe_ghost m0 (dsnd res)} -let tot_pre_action_nf = tot_pre_action_nf_except S.empty +let tot_pre_action_nf maybe_ghost = tot_pre_action_nf_except maybe_ghost S.empty let ac_reasoning_for_m_frame_preserving (p q r:slprop u#a) (m:mem u#a) @@ -753,35 +761,36 @@ let ac_reasoning_for_m_frame_preserving affine_star q (p `star` r) m let is_frame_preserving + (#mg:bool) (#e:inames) (#a:Type u#b) (#fp:slprop u#a) (#fp':a -> slprop u#a) - (f:tot_pre_action_nf_except e fp a fp') = + (f:tot_pre_action_nf_except mg e fp a fp') = forall (frame:slprop u#a) (m0:hmem_with_inv_except e (fp `star` frame)). (ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0; let (| x, m1 |) = f m0 in interp ((fp' x `star` frame) `star` locks_invariant e m1) m1 /\ - mem_evolves m0 m1 /\ - (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1))) + mem_evolves m0 m1) -let tot_action_nf_except (e:inames) (fp:slprop u#a) (a:Type u#b) (fp':a -> slprop u#a) = - f:tot_pre_action_nf_except e fp a fp'{ is_frame_preserving f } +let tot_action_nf_except (mg:bool) (e:inames) (fp:slprop u#a) (a:Type u#b) (fp':a -> slprop u#a) = + f:tot_pre_action_nf_except mg e fp a fp'{ is_frame_preserving f } -let tot_action_nf = tot_action_nf_except S.empty +let tot_action_nf mg = tot_action_nf_except mg S.empty let linv e (m:mem) = locks_invariant e m let hheap_of_hmem #fp #e (m:hmem_with_inv_except e fp) - : h:H.hheap (fp `star` linv e m) { h `H.free_above_addr` m.ctr} + : h:H.hheap (fp `star` linv e m) { + heap_ctr_valid m.ctr m.ghost_ctr h + } = let h = heap_of_mem m in - H.pure_interp (heap_ctr_valid m.ctr (heap_of_mem m)) h; + H.pure_interp (heap_ctr_valid m.ctr m.ghost_ctr (heap_of_mem m)) h; h -module Heap = PulseCore.Heap let hmem_of_hheap #e (#fp0 #fp1:slprop) (m:hmem_with_inv_except e fp0) (h:H.full_hheap (fp1 `star` linv e m) { - h `Heap.free_above_addr` m.ctr + heap_ctr_valid m.ctr m.ghost_ctr h }) : m1:hmem_with_inv_except e fp1{linv e m `equiv` linv e m1} = let m1 : mem = { m with heap = h } in @@ -789,19 +798,19 @@ let hmem_of_hheap #e (#fp0 #fp1:slprop) (m:hmem_with_inv_except e fp0) star_commutative fp1 (linv e m); assert (interp (linv e m `star` fp1) m1); assert (linv e m1 == (lock_store_invariant e m1.locks) - `star` ctr_validity m1.ctr (heap_of_mem m1)); + `star` ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1)); assert (linv e m == (lock_store_invariant e m1.locks) - `star` ctr_validity m1.ctr (heap_of_mem m)); - H.pure_interp (heap_ctr_valid m1.ctr (heap_of_mem m)) + `star` ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m)); + H.pure_interp (heap_ctr_valid m1.ctr m1.ghost_ctr (heap_of_mem m)) (heap_of_mem m); - assert (heap_ctr_valid m1.ctr (heap_of_mem m) <==> - heap_ctr_valid m1.ctr (heap_of_mem m1)); - H.pure_equiv (heap_ctr_valid m1.ctr (heap_of_mem m)) - (heap_ctr_valid m1.ctr (heap_of_mem m1)); + assert (heap_ctr_valid m1.ctr m1.ghost_ctr (heap_of_mem m) <==> + heap_ctr_valid m1.ctr m1.ghost_ctr (heap_of_mem m1)); + H.pure_equiv (heap_ctr_valid m1.ctr m1.ghost_ctr (heap_of_mem m)) + (heap_ctr_valid m1.ctr m1.ghost_ctr (heap_of_mem m1)); H.star_congruence (lock_store_invariant e m1.locks) - (ctr_validity m1.ctr (heap_of_mem m1)) + (ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1)) (lock_store_invariant e m1.locks) - (ctr_validity m1.ctr (heap_of_mem m)); + (ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m)); assert (linv e m `equiv` linv e m1); let _ = equiv_extensional_on_star (linv e m) (linv e m1) fp1 in assert ((linv e m `star` fp1) `equiv` (linv e m1 `star` fp1)); @@ -825,23 +834,28 @@ let as_hprop (frame:slprop) (mp:mprop frame) in f -let mprop_preservation_of_hprop_preservation - (p:slprop) (m0 m1:mem) - : Lemma - (requires (forall (hp:H.hprop p). hp (heap_of_mem m0) == hp (heap_of_mem m1))) - (ensures (forall (mp:mprop p). mp (core_mem m0) == mp (core_mem m1))) - = let aux (mp:mprop p) - : Lemma (mp (core_mem m0) == mp (core_mem m1)) - [SMTPat()] - = assert (as_hprop p mp (heap_of_mem m0) == as_hprop p mp (heap_of_mem m1)) - in - () - -let lift_heap_action (#fp:slprop) (#a:Type) (#fp':a -> slprop) +// let mprop_preservation_of_hprop_preservation +// (p:slprop) (m0 m1:mem) +// : Lemma +// (requires (forall (hp:H.hprop p). hp (heap_of_mem m0) == hp (heap_of_mem m1))) +// (ensures (forall (mp:mprop p). mp (core_mem m0) == mp (core_mem m1))) +// = let aux (mp:mprop p) +// : Lemma (mp (core_mem m0) == mp (core_mem m1)) +// [SMTPat()] +// = assert (as_hprop p mp (heap_of_mem m0) == as_hprop p mp (heap_of_mem m1)) +// in +// () + +let mg_of_mut (m:H.mutability) = + match m with + | H.MUTABLE -> false + | _ -> true + +let lift_heap_action (#fp:slprop) (#a:Type) (#fp':a -> slprop) (#mut:_) (e:inames) - ($f:H.action fp a fp') - : tot_action_nf_except e fp a fp' - = let g : tot_pre_action_nf_except e fp a fp' = fun m -> + ($f:H.action #mut #None fp a fp') + : tot_action_nf_except (mg_of_mut mut) e fp a fp' + = let g : tot_pre_action_nf_except (mg_of_mut mut) e fp a fp' = fun m -> let h0 = hheap_of_hmem m in let (| x, h' |) = f h0 in (| x, hmem_of_hheap m h' |) @@ -852,8 +866,9 @@ let lift_heap_action (#fp:slprop) (#a:Type) (#fp':a -> slprop) (ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0; let (| x, m1 |) = g m0 in interp ((fp' x `star` frame) `star` locks_invariant e m1) m1 /\ - mem_evolves m0 m1 /\ - (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1)))) + mem_evolves m0 m1 + + )) [SMTPat ()] = ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0; let (| x, m1 |) = g m0 in @@ -869,14 +884,14 @@ let lift_heap_action (#fp:slprop) (#a:Type) (#fp':a -> slprop) let h1' : H.hheap ((fp' x `star` frame) `star` linv e m0) = h1 in assert (m1 == hmem_of_hheap m0 h1'); assert (with_inv_except m1 e (fp' x `star` frame)); - assert (forall (hp:H.hprop frame). hp h0 == hp h1); - mprop_preservation_of_hprop_preservation frame m0 m1; + // assert (forall (hp:H.hprop frame). hp h0 == hp h1); + // mprop_preservation_of_hprop_preservation frame m0 m1; () in assert (is_frame_preserving g); g -let frame_preserving_respects_preorder #a #e #fp #fp' ($f:tot_action_nf_except e fp a fp') (m0:hmem_with_inv_except e fp) +let frame_preserving_respects_preorder #mg #a #e #fp #fp' ($f:tot_action_nf_except mg e fp a fp') (m0:hmem_with_inv_except e fp) : Lemma (let (| x, m1 |) = f m0 in mem_evolves m0 m1) = let aux (frame:slprop) (m0:hmem_with_inv_except e (fp `star` frame)) @@ -893,9 +908,9 @@ let frame_preserving_respects_preorder #a #e #fp #fp' ($f:tot_action_nf_except e assert (interp ((fp `star` emp) `star` linv e m0) m0); aux emp m0 -let lift_tot_action #a #e #fp #fp' - ($f:tot_action_nf_except e fp a fp') -: pst_action_except a e fp fp' +let lift_tot_action #a #mg #e #fp #fp' + ($f:tot_action_nf_except mg e fp a fp') +: _pst_action_except a mg e fp fp' = fun (frame:slprop) m0 -> ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0; assert (interp (fp `star` frame `star` locks_invariant e m0) m0); @@ -914,6 +929,7 @@ let lift_tot_action #a #e #fp #fp' *) let tot_action_with_frame_except + (mg:bool) (e:inames) (fp:slprop u#a) (a:Type u#b) @@ -923,10 +939,10 @@ let tot_action_with_frame_except Pure (x:a & hmem_with_inv_except e (fp' x `star` frame)) (requires True) (ensures fun (| x, m1 |) -> - mem_evolves m0 m1 /\ - (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1))) + maybe_ghost_action mg m0 m1 /\ + mem_evolves m0 m1) -let tot_action_with_frame = tot_action_with_frame_except S.empty +let tot_action_with_frame mg = tot_action_with_frame_except mg S.empty let lift_heap_action_with_frame (#fp:slprop u#a) @@ -934,7 +950,7 @@ let lift_heap_action_with_frame (#fp':a -> slprop u#a) (e:inames) ($f:H.action_with_frame fp a fp') - : tot_action_with_frame_except e fp a fp' + : tot_action_with_frame_except true e fp a fp' = fun frame m0 -> let h0 = hheap_of_hmem m0 in @@ -959,13 +975,11 @@ let lift_heap_action_with_frame let m1 = hmem_of_hheap m0 h1 in assert (mem_evolves m0 m1); - mprop_preservation_of_hprop_preservation (frame `star` locks_invariant e m0) m0 m1; - assert (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1)); (| x, m1 |) -let lift_tot_action_with_frame #a #e #fp #fp' - ($f:tot_action_with_frame_except e fp a fp') -: pst_action_except a e fp fp' +let lift_tot_action_with_frame #mg #a #e #fp #fp' + ($f:tot_action_with_frame_except mg e fp a fp') +: _pst_action_except a mg e fp fp' = fun (frame:slprop) m0 -> assert (inames_ok e m0); ac_reasoning_for_m_frame_preserving fp frame (locks_invariant e m0) m0; @@ -1017,27 +1031,27 @@ let inc_ctr (#p:slprop) #e (m:hmem_with_inv_except e p) assert (interp (p `star` linv e m) m'); assert (linv e m == lock_store_invariant e m.locks `star` - ctr_validity m.ctr (heap_of_mem m)); + ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)); assert (linv e m' == lock_store_invariant e m.locks `star` - ctr_validity (m.ctr + 1) (heap_of_mem m)); - H.weaken_free_above (heap_of_mem m) m.ctr (m.ctr + 1); - weaken_pure (heap_ctr_valid m.ctr (heap_of_mem m)) - (heap_ctr_valid (m.ctr + 1) (heap_of_mem m)); + ctr_validity (m.ctr + 1) m.ghost_ctr (heap_of_mem m)); + H.weaken_free_above H.CONCRETE (heap_of_mem m) m.ctr (m.ctr + 1); + weaken_pure (heap_ctr_valid m.ctr m.ghost_ctr (heap_of_mem m)) + (heap_ctr_valid (m.ctr + 1) m.ghost_ctr (heap_of_mem m)); assert (H.stronger - (ctr_validity m.ctr (heap_of_mem m)) - (ctr_validity (m.ctr + 1) (heap_of_mem m))); + (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)) + (ctr_validity (m.ctr + 1) m.ghost_ctr (heap_of_mem m))); H.star_associative p (lock_store_invariant e m.locks) - (ctr_validity m.ctr (heap_of_mem m)); + (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)); H.stronger_star (lock_store_invariant e m.locks) - (ctr_validity m.ctr (heap_of_mem m)) - (ctr_validity (m.ctr + 1) (heap_of_mem m)); + (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)) + (ctr_validity (m.ctr + 1) m.ghost_ctr (heap_of_mem m)); H.weaken (p `star` lock_store_invariant e m.locks) - (ctr_validity m.ctr (heap_of_mem m)) - (ctr_validity (m.ctr + 1) (heap_of_mem m)) + (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)) + (ctr_validity (m.ctr + 1) m.ghost_ctr (heap_of_mem m)) (heap_of_mem m'); H.star_associative p (lock_store_invariant e m.locks) - (ctr_validity (m.ctr + 1) (heap_of_mem m)); + (ctr_validity (m.ctr + 1) m.ghost_ctr (heap_of_mem m)); let m' : hmem_with_inv_except e p = m' in m' @@ -1045,21 +1059,21 @@ let frame_related_mems (fp0 fp1:slprop u#a) e (m0:hmem_with_inv_except e fp0) (m forall (frame:slprop u#a). interp ((fp0 `star` frame) `star` linv e m0) m0 ==> interp ((fp1 `star` frame) `star` linv e m1) m1 /\ - mem_evolves m0 m1 /\ - (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1)) + mem_evolves m0 m1 -let refined_pre_action e (fp0:slprop) (a:Type) (fp1:a -> slprop) = +let refined_pre_action mg e (fp0:slprop) (a:Type) (fp1:a -> slprop) = m0:hmem_with_inv_except e fp0 -> Pure (x:a & hmem_with_inv_except e (fp1 x)) (requires True) (ensures fun (| x, m1 |) -> + maybe_ghost_action mg m0 m1 /\ frame_related_mems fp0 (fp1 x) e m0 m1) let refined_pre_action_as_action (#fp0:slprop) (#a:Type) (#fp1:a -> slprop) - #e ($f:refined_pre_action e fp0 a fp1) - : tot_action_nf_except e fp0 a fp1 - = let g : tot_pre_action_nf_except e fp0 a fp1 = fun m -> f m in + #mg #e ($f:refined_pre_action mg e fp0 a fp1) + : tot_action_nf_except mg e fp0 a fp1 + = let g : tot_pre_action_nf_except mg e fp0 a fp1 = fun m -> f m in let aux (frame:slprop) (m0:hmem_with_inv_except e (fp0 `star` frame)) : Lemma @@ -1067,8 +1081,7 @@ let refined_pre_action_as_action (#fp0:slprop) (#a:Type) (#fp1:a -> slprop) (ac_reasoning_for_m_frame_preserving fp0 frame (locks_invariant e m0) m0; let (| x, m1 |) = g m0 in interp ((fp1 x `star` frame) `star` locks_invariant e m1) m1 /\ - mem_evolves m0 m1 /\ - (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1)))) + mem_evolves m0 m1)) [SMTPat ()] = ac_reasoning_for_m_frame_preserving fp0 frame (locks_invariant e m0) m0; let (| x', m1' |) = g m0 in @@ -1077,30 +1090,22 @@ let refined_pre_action_as_action (#fp0:slprop) (#a:Type) (#fp1:a -> slprop) in g + let alloc_action #a #pcm e x - = let f : refined_pre_action e emp (ref a pcm) (fun r -> pts_to r x) - = fun m0 -> - (* NS: 9/29/22 I needed to annotate h : Heap.full_heap, for use with the Core checker - which generates a guard for checking the implicit pattern "dot" term in the dependent - pair pattern on the next line. That guard expects `h` to be a full_heap, which is it, - because it is a projection of m0. However, this is not reflected in `h`'s type. So, - the Core checker, which produces a guard for the pat_dot_term in isolation, cannot - recheck the term. If we were to fold in the checking of pat_dot_terms and their guards - with the rest of the VC, this would work. *) - let h : Heap.full_heap = hheap_of_hmem m0 in + = let f : refined_pre_action false e emp (ref a pcm) (fun r -> pts_to r x) + = fun m0 -> + let h = hheap_of_hmem m0 in let (|r, h'|) = H.extend #a #pcm x m0.ctr h in let m' : hmem_with_inv_except e emp = inc_ctr m0 in let h' : H.hheap (pts_to #a #pcm r x `star` linv e m') = weaken _ (linv e m0) (linv e m') h' in let m1 : hmem_with_inv_except e (pts_to #a #pcm r x) = hmem_of_hheap m' h' in - assert (forall frame. H.frame_related_heaps h h' emp (pts_to #a #pcm r x) frame true); let aux (frame:slprop) : Lemma (requires interp ((emp `star` frame) `star` linv e m0) m0) (ensures interp ((pts_to #a #pcm r x `star` frame) `star` linv e m1) m1 /\ - mem_evolves m0 m1 /\ - (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1))) + mem_evolves m0 m1) [SMTPat (emp `star` frame)] = star_associative emp frame (linv e m0); assert (H.interp (emp `star` (frame `star` linv e m0)) h); @@ -1111,10 +1116,7 @@ let alloc_action #a #pcm e x assert (H.equiv (linv e m') (linv e m1)); assert (H.stronger (linv e m0) (linv e m1)); let h' : H.hheap ((pts_to #a #pcm r x `star` frame) `star` linv e m1) = weaken _ (linv e m0) (linv e m1) h' in - assert (H.interp ((pts_to #a #pcm r x `star` frame) `star` linv e m1) h'); - assert (forall (mp:H.hprop frame). mp h == mp h'); - mprop_preservation_of_hprop_preservation frame m0 m1; - assert (forall (mp:mprop frame). mp (core_mem m0) == mp (core_mem m1)) + assert (H.interp ((pts_to #a #pcm r x `star` frame) `star` linv e m1) h') in assert (frame_related_mems emp (pts_to r x) e m0 m1); (| r, m1 |) @@ -1298,17 +1300,17 @@ let ( >--> ) (i:iname) (p:slprop) : Type0 = W.witnessed full_mem mem_evolves (in let hmem_with_inv_equiv e (m:mem) (p:slprop) : Lemma (interp (p `star` linv e m) m <==> interp (p `star` lock_store_invariant e m.locks) m /\ - heap_ctr_valid m.ctr (heap_of_mem m)) + heap_ctr_valid m.ctr m.ghost_ctr (heap_of_mem m)) = calc (<==>) { interp (p `star` linv e m) m; - (<==>) { H.star_associative p (lock_store_invariant e m.locks) (ctr_validity m.ctr (heap_of_mem m)) } - interp ((p `star` lock_store_invariant e m.locks) `star` ctr_validity m.ctr (heap_of_mem m)) m; - (<==>) { H.pure_star_interp (p `star` lock_store_invariant e m.locks) (heap_ctr_valid m.ctr (heap_of_mem m)) (heap_of_mem m) } + (<==>) { H.star_associative p (lock_store_invariant e m.locks) (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)) } + interp ((p `star` lock_store_invariant e m.locks) `star` ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)) m; + (<==>) { H.pure_star_interp (p `star` lock_store_invariant e m.locks) (heap_ctr_valid m.ctr m.ghost_ctr (heap_of_mem m)) (heap_of_mem m) } interp ((p `star` lock_store_invariant e m.locks) `star` emp) m /\ - (heap_ctr_valid m.ctr (heap_of_mem m)); + (heap_ctr_valid m.ctr m.ghost_ctr (heap_of_mem m)); (<==>) { H.emp_unit (p `star` lock_store_invariant e m.locks) } interp (p `star` lock_store_invariant e m.locks) m /\ - (heap_ctr_valid m.ctr (heap_of_mem m)); + (heap_ctr_valid m.ctr m.ghost_ctr (heap_of_mem m)); } @@ -1328,17 +1330,17 @@ let new_invariant_tot_action (e:inames) (p:slprop) (m0:hmem_with_inv_except e p{ (equiv) {} (lock_store_invariant e m1.locks `star` - ctr_validity m1.ctr (heap_of_mem m1)); + ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1)); (equiv) {} ((p `star` lock_store_invariant e m0.locks) `star` - ctr_validity m1.ctr (heap_of_mem m1)); + ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1)); (equiv) { - H.star_associative p (lock_store_invariant e m0.locks) (ctr_validity m1.ctr (heap_of_mem m1)) + H.star_associative p (lock_store_invariant e m0.locks) (ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1)) } (p `star` (lock_store_invariant e m0.locks `star` - ctr_validity m1.ctr (heap_of_mem m1))); + ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1))); (equiv) { } (p `star` linv e m0); }; @@ -1394,7 +1396,7 @@ let pts_to_not_null_action (e:inames) (r:erased (ref a pcm)) (v:Ghost.erased a) -: pst_action_except (squash (not (is_null r))) e +: pst_ghost_action_except (squash (not (is_null r))) e (pts_to r v) (fun _ -> pts_to r v) = lift_tot_action (lift_heap_action e (H.pts_to_not_null_action #a #pcm r v)) @@ -1527,7 +1529,7 @@ let preserves_frame_invariant (fp fp':slprop) interp ((fp' `star` frame) `star` linv opened_invariants m1) m1 /\ (forall (f_frame:mprop frame). f_frame (core_mem m0) == f_frame (core_mem m1))) [SMTPat()] - = rearrange_invariant (fp `star` frame) (lock_store_invariant opened_invariants m0.locks) (ctr_validity m0.ctr (heap_of_mem m0)) + = rearrange_invariant (fp `star` frame) (lock_store_invariant opened_invariants m0.locks) (ctr_validity m0.ctr m0.ghost_ctr (heap_of_mem m0)) p (lock_store_invariant (set_add (name_of_inv i) opened_invariants) m0.locks); assert (interp ((p `star` (fp `star` frame)) `star` linv (set_add (name_of_inv i) opened_invariants) m0) m0); star_associative p fp frame; @@ -1539,7 +1541,7 @@ let preserves_frame_invariant (fp fp':slprop) star_congruence ((p `star` fp') `star` frame) (linv (set_add (name_of_inv i) opened_invariants) m1) (p `star` (fp' `star` frame)) (linv (set_add (name_of_inv i) opened_invariants) m1); assert (interp ((p `star` (fp' `star` frame)) `star` linv (set_add (name_of_inv i) opened_invariants) m1) m1); - rearrange_invariant (fp' `star` frame) (lock_store_invariant opened_invariants m1.locks) (ctr_validity m1.ctr (heap_of_mem m1)) + rearrange_invariant (fp' `star` frame) (lock_store_invariant opened_invariants m1.locks) (ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1)) p (lock_store_invariant (set_add (name_of_inv i) opened_invariants) m1.locks); assert (interp ((fp' `star` frame) `star` linv opened_invariants m1) m1); () @@ -1621,7 +1623,7 @@ let with_invariant (#a:Type) assert (interp (fp `star` frame `star` locks_invariant opened_invariants m0) m0); assert (interp (fp `star` frame `star` (lock_store_invariant opened_invariants m0.locks `star` - ctr_validity m0.ctr (heap_of_mem m0))) m0); + ctr_validity m0.ctr m0.ghost_ctr (heap_of_mem m0))) m0); move_invariant opened_invariants m0.locks p (name_of_inv i); assert (lock_store_invariant opened_invariants m0.locks `equiv` @@ -1631,7 +1633,7 @@ let with_invariant (#a:Type) fp frame (lock_store_invariant opened_invariants m0.locks) - (ctr_validity m0.ctr (heap_of_mem m0)) + (ctr_validity m0.ctr m0.ghost_ctr (heap_of_mem m0)) p (lock_store_invariant (set_add (name_of_inv i) opened_invariants) m0.locks); @@ -1643,7 +1645,7 @@ let with_invariant (#a:Type) assert (interp (p `star` fp' r `star` frame `star` locks_invariant (set_add (name_of_inv i) opened_invariants) m1) m1); assert (interp (p `star` fp' r `star` frame `star` (lock_store_invariant (set_add (name_of_inv i) opened_invariants) m1.locks `star` - ctr_validity m1.ctr (heap_of_mem m1))) m1); + ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1))) m1); MSTTotal.recall _ mem_evolves (iname_for_p_mem (name_of_inv i) p) (token_of_inv i); @@ -1655,7 +1657,7 @@ let with_invariant (#a:Type) (fp' r) frame (lock_store_invariant opened_invariants m1.locks) - (ctr_validity m1.ctr (heap_of_mem m1)) + (ctr_validity m1.ctr m1.ghost_ctr (heap_of_mem m1)) p (lock_store_invariant (set_add (name_of_inv i) opened_invariants) m1.locks); @@ -1694,12 +1696,13 @@ let frame (#a:Type) let pst_frame (#a:Type) + (#mg:_) (#opened_invariants:inames) (#pre:slprop) (#post:a -> slprop) (frame:slprop) - ($f:pst_action_except a opened_invariants pre post) -: pst_action_except a opened_invariants (pre `star` frame) (fun x -> post x `star` frame) + ($f:_pst_action_except a mg opened_invariants pre post) +: _pst_action_except a mg opened_invariants (pre `star` frame) (fun x -> post x `star` frame) = fun frame0 m0 -> equiv_pqrs_p_qr_s pre frame frame0 (linv opened_invariants m0); assert (interp (pre `star` frame `star` frame0 `star` linv opened_invariants m0) m0); @@ -1713,7 +1716,7 @@ let pst_frame let change_slprop (#opened_invariants:inames) (p q:slprop) (proof: (m:mem -> Lemma (requires interp p m) (ensures interp q m))) -: pst_action_except unit opened_invariants p (fun _ -> q) +: pst_ghost_action_except unit opened_invariants p (fun _ -> q) = let proof (h:H.heap) : Lemma (requires H.interp p h) (ensures H.interp q h) @@ -1721,46 +1724,112 @@ let change_slprop (#opened_invariants:inames) in lift_tot_action (lift_heap_action opened_invariants (H.change_slprop p q proof)) - -let is_frame_monotonic #a (p : a -> slprop) : prop = - forall x y m frame. interp (p x `star` frame) m /\ interp (p y) m ==> interp (p y `star` frame) m - -let is_witness_invariant #a (p : a -> slprop) = - forall x y m. interp (p x) m /\ interp (p y) m ==> x == y - -(* This module reuses is_frame_monotonic from Heap, but does not expose that -to clients, so we need this lemma to typecheck witness_h_exists below. *) -let relate_frame_monotonic_1 #a p - : Lemma (requires (H.is_frame_monotonic p)) - (ensures (is_frame_monotonic p)) - = () - -let relate_frame_monotonic_2 #a p -: Lemma (requires (is_frame_monotonic p)) - (ensures (H.is_frame_monotonic p)) -= introduce - forall x y h f. - (H.interp (p x `H.star` f) h /\ H.interp (p y) h) ==> - H.interp (p y `H.star` f) h - with - introduce _ ==> _ - with _ . ( - let m = mem_of_heap h in - assert (interp (p x `star` f) m); - assert (interp (p y) m); - assert (interp (p y `star` f) m) - ) - let witness_h_exists #opened_invariants #a p = - lift_tot_action_with_frame (lift_heap_action_with_frame opened_invariants (H.witness_h_exists p)) + lift_tot_action_with_frame (lift_heap_action_with_frame opened_invariants (H.elim_exists p)) let intro_exists #opened_invariants #a p x = lift_tot_action_with_frame (lift_heap_action_with_frame opened_invariants (H.intro_exists p x)) -let lift_h_exists #opened_invariants p = lift_tot_action (lift_heap_action opened_invariants (H.lift_h_exists p)) +let lift_h_exists #opened_invariants p = lift_tot_action (lift_heap_action opened_invariants (H.lift_exists p)) let elim_pure #opened_invariants p = lift_tot_action (lift_heap_action opened_invariants (H.elim_pure p)) let intro_pure #opened_invariants p pf = lift_tot_action (lift_heap_action opened_invariants (H.intro_pure p pf)) -let drop #o p = lift_tot_action (lift_heap_action o (H.drop p)) \ No newline at end of file +let drop #o p = lift_tot_action (lift_heap_action o (H.drop p)) + +let lift_ghost + (#a:Type) + #opened_invariants #p #q + (ni_a:non_info a) + (f:erased (pst_ghost_action_except a opened_invariants p q)) + : pst_ghost_action_except a opened_invariants p q + = fun frame m0 -> + let xm1 : erased (a * full_mem) = + let ff = reveal f in + let x, m1 = ff frame m0 in + assert (maybe_ghost_action true m0 m1); + hide (x, m1) + in + let m1' : erased full_mem = hide (snd (reveal xm1)) in + let x' : erased a = hide (fst (reveal xm1)) in + let m1 : full_mem = + { m0 with heap = H.upd_ghost_heap m0.heap (hide (m1'.heap)); + ghost_ctr = (reveal m1').ghost_ctr } in + let x = ni_a (hide (fst (reveal xm1))) in + (x, m1) + +let ghost_ref = H.ghost_ref +let ghost_pts_to = H.ghost_pts_to + + +let inc_ghost_ctr (#p:slprop) #e (m:hmem_with_inv_except e p) + : m':hmem_with_inv_except e p{reveal m'.ghost_ctr = m.ghost_ctr + 1 /\ H.stronger (linv e m) (linv e m')} + = let m' : mem = { m with ghost_ctr = m.ghost_ctr + 1} in + assert (interp (p `star` linv e m) m'); + assert (linv e m == lock_store_invariant e m.locks + `star` + ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)); + assert (linv e m' == lock_store_invariant e m.locks + `star` + ctr_validity m.ctr (m.ghost_ctr + 1) (heap_of_mem m)); + H.weaken_free_above H.GHOST (heap_of_mem m) m.ghost_ctr (m.ghost_ctr + 1); + weaken_pure (heap_ctr_valid m.ctr m.ghost_ctr (heap_of_mem m)) + (heap_ctr_valid m.ctr (m.ghost_ctr + 1) (heap_of_mem m)); + assert (H.stronger + (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)) + (ctr_validity m.ctr (m.ghost_ctr + 1) (heap_of_mem m))); + H.star_associative p (lock_store_invariant e m.locks) + (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)); + H.stronger_star (lock_store_invariant e m.locks) + (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)) + (ctr_validity m.ctr (m.ghost_ctr + 1) (heap_of_mem m)); + H.weaken (p `star` lock_store_invariant e m.locks) + (ctr_validity m.ctr m.ghost_ctr (heap_of_mem m)) + (ctr_validity m.ctr (m.ghost_ctr + 1) (heap_of_mem m)) + (heap_of_mem m'); + H.star_associative p (lock_store_invariant e m.locks) + (ctr_validity m.ctr (m.ghost_ctr + 1) (heap_of_mem m)); + let m' : hmem_with_inv_except e p = m' in + m' + +let ghost_alloc #e #a #pcm x + = let f : refined_pre_action true e emp (ghost_ref pcm) (fun r -> ghost_pts_to r x) + = fun m0 -> + let h = hheap_of_hmem m0 in + let (|r, h'|) = H.ghost_extend #a #pcm x m0.ghost_ctr h in + let m' : hmem_with_inv_except e emp = inc_ghost_ctr m0 in + let h' : H.hheap (ghost_pts_to #a #pcm r x `star` linv e m') = weaken _ (linv e m0) (linv e m') h' in + let m1 : hmem_with_inv_except e (ghost_pts_to #a #pcm r x) = hmem_of_hheap m' h' in + let aux (frame:slprop) + : Lemma + (requires + interp ((emp `star` frame) `star` linv e m0) m0) + (ensures + interp ((ghost_pts_to #a #pcm r x `star` frame) `star` linv e m1) m1 /\ + mem_evolves m0 m1) + [SMTPat (emp `star` frame)] + = star_associative emp frame (linv e m0); + assert (H.interp (emp `star` (frame `star` linv e m0)) h); + assert (H.interp (ghost_pts_to #a #pcm r x `star` (frame `star` linv e m0)) h'); + star_associative (ghost_pts_to #a #pcm r x) frame (linv e m0); + assert (H.interp ((ghost_pts_to #a #pcm r x `star` frame) `star` linv e m0) h'); + assert (H.stronger (linv e m0) (linv e m')); + assert (H.equiv (linv e m') (linv e m1)); + assert (H.stronger (linv e m0) (linv e m1)); + let h' : H.hheap ((ghost_pts_to #a #pcm r x `star` frame) `star` linv e m1) = weaken _ (linv e m0) (linv e m1) h' in + assert (H.interp ((ghost_pts_to #a #pcm r x `star` frame) `star` linv e m1) h') + in + assert (frame_related_mems emp (ghost_pts_to r x) e m0 m1); + (| r, m1 |) + in + lift_tot_action (refined_pre_action_as_action f) + +let ghost_read #o #a #p r x f + = lift_tot_action (lift_heap_action o (H.ghost_read #a #p r x f)) +let ghost_write #o #a #p r x y f + = lift_tot_action (lift_heap_action o (H.ghost_write #a #p r x y f)) +let ghost_share #o #a #p r v0 v1 + = lift_tot_action (lift_heap_action o (H.ghost_share #a #p r v0 v1)) +let ghost_gather #o #a #p r v0 v1 + = lift_tot_action (lift_heap_action o (H.ghost_gather #a #p r v0 v1)) diff --git a/lib/pulse/core/PulseCore.Memory.fsti b/lib/pulse/core/PulseCore.Memory.fsti index 57c63d0f4..0a55cfa1b 100644 --- a/lib/pulse/core/PulseCore.Memory.fsti +++ b/lib/pulse/core/PulseCore.Memory.fsti @@ -28,6 +28,12 @@ module PST = PulseCore.PreorderStateMonad (** Abstract type of memories *) val mem : Type u#(a + 1) +val is_ghost_action (m0 m1:mem u#a) : prop +let maybe_ghost_action (b:bool) (m0 m1:mem u#a) = b ==> is_ghost_action m0 m1 + +val ghost_action_preorder (_:unit) + : Lemma (FStar.Preorder.preorder_rel is_ghost_action) + (** The memory is built on top of the heap, adding on the memory invariants. However, some of the properties exposed for memories need only to talk about the underlying heap, putting aside @@ -182,6 +188,7 @@ effect MstTot let _PST (a:Type u#a) + (maybe_ghost:bool) (except:inames) (expects:slprop u#1) (provides: a -> slprop u#1) @@ -191,17 +198,31 @@ let _PST inames_ok except m0 /\ interp (expects `star` frame `star` locks_invariant except m0) m0) (ensures fun m0 x m1 -> + maybe_ghost_action maybe_ghost m0 m1 /\ inames_ok except m1 /\ interp (expects `star` frame `star` locks_invariant except m0) m0 /\ //TODO: fix the effect so as not to repeat this interp (provides x `star` frame `star` locks_invariant except m1) m1) (** An action is just a thunked computation in [MstTot] that takes a frame as argument *) -let action_except (a:Type u#a) (except:inames) (expects:slprop) (provides: a -> slprop) = +let action_except (a:Type u#a) (except:inames) (expects:slprop) (provides: a -> slprop) + : Type u#(max a 2) = frame:slprop -> MstTot a except expects provides frame (** An action is just a thunked computation in [MstTot] that takes a frame as argument *) +let _pst_action_except + (a:Type u#a) + (maybe_ghost:bool) + (except:inames) + (expects:slprop) + (provides: a -> slprop) + : Type u#(max a 2) + = frame:slprop -> _PST a maybe_ghost except expects provides frame + let pst_action_except (a:Type u#a) (except:inames) (expects:slprop) (provides: a -> slprop) = - frame:slprop -> _PST a except expects provides frame + _pst_action_except a false except expects provides + +let pst_ghost_action_except (a:Type u#a) (except:inames) (expects:slprop) (provides: a -> slprop) = + _pst_action_except a true except expects provides val sel_action (#a:Type u#1) (#pcm:_) (e:inames) (r:ref a pcm) (v0:erased a) : pst_action_except (v:a{compatible pcm v0 v}) e (pts_to r v0) (fun _ -> pts_to r v0) @@ -224,7 +245,7 @@ val split_action (r:ref a pcm) (v0:FStar.Ghost.erased a) (v1:FStar.Ghost.erased a{composable pcm v0 v1}) - : pst_action_except unit e (pts_to r (v0 `op pcm` v1)) (fun _ -> pts_to r v0 `star` pts_to r v1) + : pst_ghost_action_except unit e (pts_to r (v0 `op pcm` v1)) (fun _ -> pts_to r v0 `star` pts_to r v1) (** Combining separate permissions into a single composite permission *) val gather_action @@ -234,7 +255,7 @@ val gather_action (r:ref a pcm) (v0:FStar.Ghost.erased a) (v1:FStar.Ghost.erased a) - : pst_action_except (_:unit{composable pcm v0 v1}) e (pts_to r v0 `star` pts_to r v1) (fun _ -> pts_to r (op pcm v0 v1)) + : pst_ghost_action_except (_:unit{composable pcm v0 v1}) e (pts_to r v0 `star` pts_to r v1) (fun _ -> pts_to r (op pcm v0 v1)) val alloc_action (#a:Type u#1) (#pcm:pcm a) (e:inames) (x:a{compatible pcm x x /\ pcm.refine x}) : pst_action_except (ref a pcm) e emp (fun r -> pts_to r x) @@ -292,7 +313,7 @@ val pts_to_not_null_action (e:inames) (r:erased (ref a pcm)) (v:Ghost.erased a) -: pst_action_except (squash (not (is_null r))) e +: pst_ghost_action_except (squash (not (is_null r))) e (pts_to r v) (fun _ -> pts_to r v) @@ -361,35 +382,108 @@ val frame (#a:Type) : action_except a opened_invariants (pre `star` frame) (fun x -> post x `star` frame) val pst_frame (#a:Type) + (#maybe_ghost:bool) (#opened_invariants:inames) (#pre:slprop) (#post:a -> slprop) (frame:slprop) - ($f:pst_action_except a opened_invariants pre post) - : pst_action_except a opened_invariants (pre `star` frame) (fun x -> post x `star` frame) + ($f:_pst_action_except a maybe_ghost opened_invariants pre post) + : _pst_action_except a maybe_ghost opened_invariants (pre `star` frame) (fun x -> post x `star` frame) module U = FStar.Universe val witness_h_exists (#opened_invariants:_) (#a:_) (p:a -> slprop) - : pst_action_except (erased a) opened_invariants + : pst_ghost_action_except (erased a) opened_invariants (h_exists p) (fun x -> p x) val intro_exists (#opened_invariants:_) (#a:_) (p:a -> slprop) (x:erased a) - : pst_action_except unit opened_invariants + : pst_ghost_action_except unit opened_invariants (p x) (fun _ -> h_exists p) val lift_h_exists (#opened_invariants:_) (#a:_) (p:a -> slprop) - : pst_action_except unit opened_invariants + : pst_ghost_action_except unit opened_invariants (h_exists p) (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p)) val elim_pure (#opened_invariants:_) (p:prop) - : pst_action_except (u:unit{p}) opened_invariants (pure p) (fun _ -> emp) + : pst_ghost_action_except (u:unit{p}) opened_invariants (pure p) (fun _ -> emp) val intro_pure (#opened_invariants:_) (p:prop) (_:squash p) - : pst_action_except unit opened_invariants emp (fun _ -> pure p) + : pst_ghost_action_except unit opened_invariants emp (fun _ -> pure p) val drop (#opened_invariants:_) (p:slprop) - : pst_action_except unit opened_invariants p (fun _ -> emp) \ No newline at end of file + : pst_ghost_action_except unit opened_invariants p (fun _ -> emp) + +let non_info a = x:erased a -> y:a { reveal x == y} +val lift_ghost + (#a:Type) + #opened_invariants #p #q + (ni_a:non_info a) + (f:erased (pst_ghost_action_except a opened_invariants p q)) + : pst_ghost_action_except a opened_invariants p q + +[@@erasable] +val ghost_ref (#[@@@unused] a:Type u#a) ([@@@unused]p:pcm a) : Type0 +val ghost_pts_to (#a:Type u#a) (#p:pcm a) (r:ghost_ref p) (v:a) : slprop u#a + +val ghost_alloc + (#o:_) + (#a:Type u#1) + (#pcm:pcm a) + (x:erased a{compatible pcm x x /\ pcm.refine x}) +: pst_ghost_action_except + (ghost_ref pcm) + o + emp + (fun r -> ghost_pts_to r x) + +val ghost_read + #o + (#a:Type) + (#p:pcm a) + (r:ghost_ref p) + (x:erased a) + (f:(v:a{compatible p x v} + -> GTot (y:a{compatible p y v /\ + FStar.PCM.frame_compatible p x v y}))) +: pst_ghost_action_except + (erased (v:a{compatible p x v /\ p.refine v})) + o + (ghost_pts_to r x) + (fun v -> ghost_pts_to r (f v)) + +val ghost_write + #o + (#a:Type) + (#p:pcm a) + (r:ghost_ref p) + (x y:Ghost.erased a) + (f:FStar.PCM.frame_preserving_upd p x y) +: pst_ghost_action_except unit o + (ghost_pts_to r x) + (fun _ -> ghost_pts_to r y) + +val ghost_share + #o + (#a:Type) + (#pcm:pcm a) + (r:ghost_ref pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a{composable pcm v0 v1}) +: pst_ghost_action_except unit o + (ghost_pts_to r (v0 `op pcm` v1)) + (fun _ -> ghost_pts_to r v0 `star` ghost_pts_to r v1) + +val ghost_gather + #o + (#a:Type) + (#pcm:pcm a) + (r:ghost_ref pcm) + (v0:FStar.Ghost.erased a) + (v1:FStar.Ghost.erased a) +: pst_ghost_action_except + (squash (composable pcm v0 v1)) o + (ghost_pts_to r v0 `star` ghost_pts_to r v1) + (fun _ -> ghost_pts_to r (op pcm v0 v1))