Merge pull request #518 from mtzguido/ghostbag

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

Author: mtzguido

share/pulse/examples/GhostBag.fst

@@ -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
@@ -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 })
@@ -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) =
   {
@@ -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
 
@@ -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))
 
 
 
@@ -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);
@@ -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 **
@@ -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)
@@ -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))
 }