wip

Author: gebner

lib/common/Pulse.Lib.Core.fsti

@@ -749,7 +749,6 @@ val share
     (pcm_pts_to r (v0 `op pcm` v1))
     (fun _ -> pcm_pts_to r v0 ** pcm_pts_to r v1)
 
-[@@allow_ambiguous]
 val gather
     (#a:Type)
     (#pcm:pcm a)
@@ -916,7 +915,6 @@ val big_share
     (big_pcm_pts_to r (v0 `op pcm` v1))
     (fun _ -> big_pcm_pts_to r v0 ** big_pcm_pts_to r v1)
 
-[@@allow_ambiguous]
 val big_gather
     (#a:Type)
     (#pcm:pcm a)
@@ -987,7 +985,6 @@ val big_ghost_share
     (big_ghost_pcm_pts_to r (v0 `op pcm` v1))
     (fun _ -> big_ghost_pcm_pts_to r v0 ** big_ghost_pcm_pts_to r v1)
 
-[@@allow_ambiguous]
 val big_ghost_gather
     (#a:Type)
     (#pcm:pcm a)

lib/pulse/lib/Pulse.Lib.AVLTree.fst

@@ -120,14 +120,16 @@ fn cases_of_is_tree #t (x:tree_t t) (ft:T.tree t)
     T.Leaf -> {
       unfold (is_tree x T.Leaf);
       fold (is_tree_cases None ft);
+      rewrite is_tree_cases None ft as is_tree_cases x ft;
     }
     T.Node data ltree rtree -> {
       unfold (is_tree x (T.Node data ltree rtree));
       with p lct rct. _;
       with n. assert p |-> n;
       with l'. rewrite is_tree lct l' as is_tree n.left l';
       with r'. rewrite is_tree rct r' as is_tree n.right r';
-      fold (is_tree_cases (Some p) (T.Node data ltree rtree))
+      fold (is_tree_cases (Some p) ft);
+      rewrite (is_tree_cases (Some p) ft) as is_tree_cases x ft;
     }
   }
 }
@@ -240,8 +242,6 @@ fn node_cons (#t:Type0) (v:t) (ltree:tree_t t) (rtree:tree_t t) (#l:(T.tree t))
   ensures is_tree y (T.Node v l r) ** (pure (Some? y))
 {
   let y = Box.alloc { data=v; left =ltree; right = rtree };
-  rewrite each ltree as ({data = v; left = ltree; right = rtree}).left in (is_tree ltree l);
-  rewrite each rtree as ({data = v; left = ltree; right = rtree}).right in (is_tree rtree r);
   intro_is_tree_node (Some y) y;
   Some y
 }
@@ -293,18 +293,12 @@ fn rec append_left (#t:Type0) (x:tree_t t) (v:t) (#ft:G.erased (T.tree t))
 
       is_tree_case_some (Some vl) vl;
 
-      with _node _ltree _rtree._;
-
       let node = !vl;
 
       let left_new = append_left node.left v;
 
       vl := {node with left = left_new};
 
-      rewrite each left_new as ({ node with left = left_new }).left in (is_tree left_new ((T.append_left (reveal _ltree) v)));
-      
-      rewrite each node.right as ({ node with left = left_new }).right in (is_tree node.right _rtree);
-
       intro_is_tree_node x vl;
 
       x
@@ -344,18 +338,12 @@ fn rec append_right (#t:Type0) (x:tree_t t) (v:t) (#ft:G.erased (T.tree t))
     Some np -> {
       is_tree_case_some (Some np) np;
 
-      with _node _ltree _rtree._;
-      
       let node = !np;
 
       let right_new = append_right node.right v;
 
       np := {node with right = right_new};
 
-      rewrite each right_new as ({ node with right = right_new }).right in (is_tree right_new ((T.append_right (reveal _rtree) v)));
-      
-      rewrite each node.left as ({node with right = right_new}).left in (is_tree node.left _ltree);
-      
       intro_is_tree_node x np;
 
       x

lib/pulse/lib/Pulse.Lib.BigGhostReference.fst

@@ -99,7 +99,7 @@ fn free (#a:Type u#2) (r:ref a) (#n:erased a)
 {
   unfold pts_to r #1.0R n;
   Pulse.Lib.Core.big_ghost_write r _ _ (mk_frame_preserving_upd_none n);
-  Pulse.Lib.Core.drop_ _;
+  Pulse.Lib.Core.drop_ (big_ghost_pcm_pts_to _ _);
 }
 
 

lib/pulse/lib/Pulse.Lib.CancellableInvariant.fsti

@@ -25,9 +25,9 @@ val cinv : Type0
 instance val non_informative_cinv
   : NonInformative.non_informative cinv
 
-val cinv_vp (c:cinv) (v:slprop) : slprop
+val cinv_vp ([@@@mkey] c:cinv) (v:slprop) : slprop
 
-val active (c:cinv) (p:perm) : slprop
+val active ([@@@mkey] c:cinv) (p:perm) : slprop
 
 val active_timeless (c:cinv) (p:perm)
   : Lemma (timeless (active c p))

lib/pulse/lib/Pulse.Lib.ConditionVar.fst

@@ -167,7 +167,7 @@ ensures
      later_intro (cvar_inv b.core p);
      drop_ (Box.pts_to b.core.r #0.5R _)
   };
-  drop_ _
+  drop_ (inv _ _)
 }
 
 fn signal (c:cvar_t) (#p:slprop)

lib/pulse/lib/Pulse.Lib.Deque.fst

@@ -21,15 +21,6 @@ type deque (t:Type0) = {
   tail: option (node_ptr t);
 }
 
-(* Note: since within this module there is usually a *single* linked list
-around, we mark the list predicated with no_mkeys so the matcher can be
-more liberal. Crucially, this attribute is only set behind the interface,
-and clients will just use the mkey in is_deque.
-
-This is a bit of a hack, the fact that F* allows the attributes to differ
-between fst/fsti is probably wrong. Maybe we should have a typeclass? *)
-
-[@@no_mkeys]
 let rec is_deque_suffix
   (#t:Type0)
   ([@@@mkey] p:node_ptr t)
@@ -82,7 +73,6 @@ fn fold_is_deque_suffix_cons
 
 
 
-[@@no_mkeys]
 let is_deque #t ([@@@mkey] x:deque t) (l:list t)
   : Tot slprop (decreases l)
   = match l with
@@ -120,7 +110,7 @@ fn push_front_empty (#t:Type) (l : deque t) (x : t)
   };
   let node = Box.alloc vnode;
 
-  fold (is_deque_suffix node [x] None node);
+  fold (is_deque_suffix node [x] None node None);
 
   let l' = {
     head = Some node;
@@ -287,10 +277,8 @@ let is_deque_suffix_factored
 : Tot slprop
   = exists* (v:node t).
       pts_to x v **
-      pure (
-        v.value == List.Tot.hd l /\
-        v.dprev == prev
-      ) **
+      pure (v.value == List.Tot.hd l) **
+      pure (v.dprev == prev) **
       is_deque_suffix_factored_next x l tail last v.dnext
 
 
@@ -655,7 +643,7 @@ fn pop_front (#t:Type) (l : deque t)
 {
   let b = is_singleton l;
   if b {
-    pop_front_nil l;
+    pop_front_nil l #x;
   } else {
     pop_front_cons l;
   }

lib/pulse/lib/Pulse.Lib.Forall.fst

@@ -47,7 +47,7 @@ fn elim_forall u#a
 {
   unfold (forall* x. p x);
   unfold uquant (F.on_dom a (fun x -> p x));
-  with v. assert token v; unfold token v;
+  with v. unfold token v;
   extract_q v (F.on_domain a (fun x -> p x)) () x;
 }
 

lib/pulse/lib/Pulse.Lib.GhostReference.fst

@@ -69,7 +69,7 @@ fn write (#a:Type) (r:ref a) (x:erased a) (#n:erased a)
   ensures pts_to r #1.0R x
 {
   unfold (pts_to r #1.0R n);
-  H.(r := (U.raise_val x));
+  H.(r := U.raise_val (reveal x));
   fold (pts_to r #1.0R x)
 }
 

lib/pulse/lib/Pulse.Lib.HashTable.fst

@@ -555,7 +555,6 @@ fn delete
     if (voff = ht.sz)
     {
       cont := false;
-      rewrite each vcont as false; // also relying on #110
     }
     else
     {
@@ -583,7 +582,6 @@ fn delete
         {
           cont := false;
           assert (pure (pht.repr == (PHT.delete pht k).repr));
-          rewrite each vcont as false; // also relying on #110
         }
         Zombie ->
         {

lib/pulse/lib/Pulse.Lib.HashTable.fsti

@@ -44,13 +44,13 @@ let related #kt #vt (ht:ht_t kt vt) (pht:pht_t kt vt) : prop =
   SZ.v ht.sz == pht.repr.sz /\
   pht.repr.hashf == lift_hash_fun ht.hashf
 
-let models #kt #vt (ht:ht_t kt vt) (pht:pht_t kt vt) : slprop =
+let models #kt #vt ([@@@mkey]ht: ht_t kt vt) (pht:pht_t kt vt) : slprop =
   V.pts_to ht.contents pht.repr.seq **
   pure (related ht pht /\
         V.is_full_vec ht.contents /\
         SZ.fits (2 `op_Multiply` SZ.v ht.sz))
 
-val models_timeless #kt #vt (ht:ht_t kt vt) (pht:pht_t kt vt)
+val models_timeless #kt #vt ([@@@mkey] ht:ht_t kt vt) (pht:pht_t kt vt)
 : Lemma (timeless (models ht pht))
         [SMTPat (timeless (models ht pht))]