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.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;
@@ -655,7 +645,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.HigherGhostReference.fst

@@ -103,7 +103,7 @@ fn free #a (r:ref a) (#n:erased a)
 {
   unfold pts_to r #1.0R n;
   Pulse.Lib.Core.ghost_write r _ _ (mk_frame_preserving_upd_none n);
-  Pulse.Lib.Core.drop_ _;
+  Pulse.Lib.Core.drop_ (ghost_pcm_pts_to _ _);
 }
 
 

lib/pulse/lib/Pulse.Lib.LinkedList.fst

@@ -290,6 +290,8 @@ fn move_next (#t:Type) (x:llist t)
     let node = !np;
     intro_yields_cons np;
     rewrite each (Some np) as x;
+    with tl. rewrite trade (is_list node.tail tl) (is_list x (node.head :: tl))
+                  as trade (is_list node.tail tl) (is_list x 'l);
     node.tail
 }
 

lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst

@@ -131,5 +131,5 @@ fn update (#t:Type) (#p:preorder t) (r:mref p) (#u:t) (v:t)
   unfold pts_to;
   with f h. assert (GR.pts_to r (f, h));
   GR.write r _ _ (FP.mk_frame_preserving_upd p h v);
-  fold pts_to;
+  fold pts_to r #1.0R v;
 }

lib/pulse/lib/Pulse.Lib.Mutex.fst

@@ -94,7 +94,7 @@ fn unlock (#a:Type0) (#v:a -> slprop) (#p:perm) (m:mutex a) (mg:mutex_guard a)
   unfold (mg `belongs_to` m);
   with x. rewrite (pts_to mg x) as (R.pts_to (B.box_to_ref m.r) x);
   B.to_box_pts_to m.r;
-  fold lock_inv;
+  fold lock_inv m.r v;
   release m.l;
   fold (mutex_live m #p v)
 }

lib/pulse/lib/Pulse.Lib.OnRange.fst

@@ -481,6 +481,7 @@ fn rec on_range_unzip (p q:nat -> slprop) (i j:nat)
     rewrite (on_range (fun k -> p k ** q k) i j) as pure False;
     unreachable ();
   } else if (j = i) {
+    rewrite each j as i;
     on_range_empty_elim (fun k -> p k ** q k) i;
     on_range_empty p i;
     on_range_empty q i;