Skip to content

GhostBag: remove use of option type, use 0.0R for None #518

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mtzguido merged 1 commit into from
Nov 28, 2025
Merged

GhostBag: remove use of option type, use 0.0R for None #518

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
104 changes: 50 additions & 54 deletions share/pulse/examples/GhostBag.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,8 @@ module GhostBag
open FStar.PCM
open Pulse.Lib.Pervasives

type map (a:eqtype) = m:Map.t a (option perm) { forall (x:a). Map.contains m x }
let perm0 = r:real{r >=. 0.0R}
type map (a:eqtype) = m:Map.t a perm0 { forall (x:a). Map.contains m x }

//
// P represents the partial knowledge of the set membership
Expand Down Expand Up @@ -67,26 +68,21 @@ let gbag_pcm_composable #a : symrel (gbag_pcm_carrier a) =
match x, y with
| P m1, P m2 ->
forall (x:a).
(Map.sel m1 x == None) \/
(Map.sel m2 x == None) \/
((Some?.v (Map.sel m1 x)) +. (Some?.v ((Map.sel m2 x)))) <=. 1.0R
(Map.sel m1 x == 0.0R) \/
(Map.sel m2 x == 0.0R) \/
(Map.sel m1 x +. Map.sel m2 x) <=. 1.0R

| F m1, P m2
| P m2, F m1 ->
forall (x:a).
(Map.sel m2 x == None) \/
(Some? (Map.sel m1 x) /\ ((Some?.v (Map.sel m1 x)) +. (Some?.v ((Map.sel m2 x)))) <=. 1.0R)
(Map.sel m2 x == 0.0R) \/
(Map.sel m1 x >. 0.0R /\ Map.sel m1 x +. Map.sel m2 x <=. 1.0R)

| _ -> False

let op_maps #a (m1:map a) (m2:map a) : map a =
Map.map_literal #a #(option perm) (fun x ->
match Map.sel m1 x, Map.sel m2 x with
| None, None -> None
| Some p, None -> Some p
| None, Some p -> Some p
| Some p1, Some p2 ->
Some (p1 +. p2)
Map.map_literal #a #perm0 (fun x ->
Map.sel m1 x +. Map.sel m2 x
)

let gbag_pcm_op #a (x:gbag_pcm_carrier a) (y:gbag_pcm_carrier a { gbag_pcm_composable x y })
Expand All @@ -97,7 +93,7 @@ let gbag_pcm_op #a (x:gbag_pcm_carrier a) (y:gbag_pcm_carrier a { gbag_pcm_compo
| F m1, P m2
| P m1, F m2 -> F (op_maps m1 m2)

let gbag_pcm_one #a : gbag_pcm_carrier a = P (Map.const None)
let gbag_pcm_one #a : gbag_pcm_carrier a = P (Map.const 0.0R)

let gbag_pcm' a : pcm' (gbag_pcm_carrier a) =
{
Expand Down Expand Up @@ -154,41 +150,39 @@ let gbag_pcm a : pcm (gbag_pcm_carrier a) = {
refine = (fun _ -> True)
}

#restart-solver
#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1 --split_queries no --warn_error -271"
let fp_upd_add #a
(m:map a)
(x:a { Map.sel m x == None })
: frame_preserving_upd (gbag_pcm a) (F m) (F (Map.upd m x (Some 1.0R))) =
(x:a { Map.sel m x == 0.0R })
: frame_preserving_upd (gbag_pcm a) (F m) (F (Map.upd m x 1.0R)) =

fun v ->
let F mv = v in
let v_new = F (Map.upd mv x (Some 1.0R)) in
let v_new = F (Map.upd mv x 1.0R) in

eliminate exists (frame:gbag_pcm_carrier a). composable (gbag_pcm a) (F m) frame /\
op (gbag_pcm a) frame (F m) == v
returns compatible (gbag_pcm a) (F (Map.upd m x (Some 1.0R))) v_new
returns compatible (gbag_pcm a) (F (Map.upd m x 1.0R)) v_new
with _. (match frame with
| P m_frame
| F m_frame ->
assert (Map.equal (op_maps m_frame (Map.upd m x (Some 1.0R)))
(Map.upd mv x (Some 1.0R))));
assert (Map.equal (op_maps m_frame (Map.upd m x 1.0R))
(Map.upd mv x 1.0R)));

let aux (frame:gbag_pcm_carrier a)
: Lemma
(requires
gbag_pcm_composable (F m) frame /\
gbag_pcm_op (F m) frame == v)
(ensures
gbag_pcm_composable (F (Map.upd m x (Some 1.0R))) frame /\
gbag_pcm_op (F (Map.upd m x (Some 1.0R))) frame == v_new)
gbag_pcm_composable (F (Map.upd m x 1.0R)) frame /\
gbag_pcm_op (F (Map.upd m x 1.0R)) frame == v_new)
[SMTPat ()] =

match frame with
| P m_frame
| F m_frame ->
assert (Map.equal (op_maps (Map.upd m x (Some 1.0R)) m_frame)
(Map.upd mv x (Some 1.0R)));
assert (Map.equal (op_maps (Map.upd m x 1.0R) m_frame)
(Map.upd mv x 1.0R));
()
in

Expand All @@ -197,54 +191,53 @@ let fp_upd_add #a

let fp_upd_rem #a
(m:map a)
(x:a { Map.sel m x == Some 1.0R })
: frame_preserving_upd (gbag_pcm a) (F m) (F (Map.upd m x None)) =
(x:a { Map.sel m x == 1.0R })
: frame_preserving_upd (gbag_pcm a) (F m) (F (Map.upd m x 0.0R)) =

fun v ->
let F mv = v in
let v_new = F (Map.upd mv x None) in
let v_new = F (Map.upd mv x 0.0R) in

eliminate exists (frame:gbag_pcm_carrier a). composable (gbag_pcm a) (F m) frame /\
op (gbag_pcm a) frame (F m) == v
returns compatible (gbag_pcm a) (F (Map.upd m x None)) v_new
returns compatible (gbag_pcm a) (F (Map.upd m x 0.0R)) v_new
with _. (match frame with
| P m_frame
| F m_frame ->
assert (Map.equal (op_maps m_frame (Map.upd m x None))
(Map.upd mv x None));
assert (composable (gbag_pcm a) (F (Map.upd m x None)) frame));
assert (Map.equal (op_maps m_frame (Map.upd m x 0.0R))
(Map.upd mv x 0.0R));
assert (composable (gbag_pcm a) (F (Map.upd m x 0.0R)) frame));

let aux (frame:gbag_pcm_carrier a)
: Lemma
(requires
gbag_pcm_composable (F m) frame /\
gbag_pcm_op (F m) frame == v)
(ensures
gbag_pcm_composable (F (Map.upd m x None)) frame /\
gbag_pcm_op (F (Map.upd m x None)) frame == v_new)
gbag_pcm_composable (F (Map.upd m x 0.0R)) frame /\
gbag_pcm_op (F (Map.upd m x 0.0R)) frame == v_new)
[SMTPat ()] =

match frame with
| P m_frame
| F m_frame ->
assert (Map.equal (op_maps (Map.upd m x None) m_frame)
(Map.upd mv x None));
assert (Map.equal (op_maps (Map.upd m x 0.0R) m_frame)
(Map.upd mv x 0.0R));
()
in

v_new
#pop-options

module GR = Pulse.Lib.GhostPCMReference

let gbag #a (r:GR.gref (gbag_pcm a)) (s:Set.set a) : slprop =
exists* (m:map a).
GR.pts_to r (F m) **
(pure (forall (x:a). (~ (Set.mem x s)) ==> Map.sel m x == None)) **
(pure (forall (x:a). Set.mem x s ==> Map.sel m x == Some 0.5R))
(pure (forall (x:a). (~ (Set.mem x s)) ==> Map.sel m x == 0.0R)) **
(pure (forall (x:a). Set.mem x s ==> Map.sel m x == 0.5R))

let gbagh #a (r:GR.gref (gbag_pcm a)) (x:a) : slprop =
GR.pts_to r (P (Map.upd (Map.const None) x (Some 0.5R)))
GR.pts_to r (P (Map.upd (Map.const 0.0R) x 0.5R))



Expand All @@ -254,7 +247,7 @@ fn gbag_create (a:eqtype)
returns r:GR.gref (gbag_pcm a)
ensures gbag r Set.empty
{
let r = GR.alloc #_ #(gbag_pcm a) (F (Map.const None));
let r = GR.alloc #_ #(gbag_pcm a) (F (Map.const 0.0R));
with _m. rewrite (GR.pts_to r (Ghost.reveal (Ghost.hide _m))) as
(GR.pts_to r _m);
fold (gbag r Set.empty);
Expand All @@ -263,6 +256,9 @@ fn gbag_create (a:eqtype)



#set-options "--split_queries always --debug SMTFail"


ghost
fn gbag_add #a (r:GR.gref (gbag_pcm a)) (s:Set.set a) (x:a)
requires gbag r s **
Expand All @@ -272,16 +268,16 @@ fn gbag_add #a (r:GR.gref (gbag_pcm a)) (s:Set.set a) (x:a)
{
unfold gbag;
with mf. assert (GR.pts_to r (F mf));
GR.write r (F mf) (F (Map.upd mf x (Some 1.0R))) (fp_upd_add mf x);
assert (pure (Map.equal (Map.upd mf x (Some 1.0R))
(op_maps (Map.upd mf x (Some 0.5R))
(Map.upd (Map.const None) x (Some 0.5R)))));
rewrite (GR.pts_to r (F (Map.upd mf x (Some 1.0R)))) as
GR.write r (F mf) (F (Map.upd mf x 1.0R)) (fp_upd_add mf x);
assert (pure (Map.equal (Map.upd mf x 1.0R)
(op_maps (Map.upd mf x 0.5R)
(Map.upd (Map.const #a #perm0 0.0R) x 0.5R))));
rewrite (GR.pts_to r (F (Map.upd mf x 1.0R))) as
(GR.pts_to r (op (gbag_pcm a)
(F (Map.upd mf x (Some 0.5R)))
(P (Map.upd (Map.const None) x (Some 0.5R)))));
GR.share r (F (Map.upd mf x (Some 0.5R)))
(P (Map.upd (Map.const None) x (Some 0.5R)));
(F (Map.upd mf x 0.5R))
(P (Map.upd (Map.const #a #perm0 0.0R) x 0.5R))));
GR.share r (F (Map.upd mf x 0.5R))
(P (Map.upd (Map.const #a #perm0 0.0R) x 0.5R));
fold (gbag r (Set.add x s));
with _v. rewrite (GR.pts_to r (Ghost.reveal (Ghost.hide _v))) as
(gbagh r x)
Expand All @@ -299,13 +295,13 @@ fn gbag_remove #a (r:GR.gref (gbag_pcm a)) (s:Set.set a) (x:a)
unfold gbag;
with mf. assert (GR.pts_to r (F mf));
unfold gbagh;
let mp = Map.upd (Map.const #_ #(option perm) None) x (Some 0.5R);
let mp = Map.upd (Map.const #_ #perm0 0.0R) x 0.5R;
with _m. rewrite (GR.pts_to r (P _m)) as
(GR.pts_to r (P mp));
GR.gather r (F mf) (P mp);
assert (pure (x `Set.mem` s));
let mop = op_maps mf mp;
GR.write r (F mop) (F (Map.upd mop x None)) (fp_upd_rem mop x);
GR.write r (F mop) (F (Map.upd mop x 0.0R)) (fp_upd_rem mop x);
fold (gbag r (Set.remove x s))
}

Loading