Phase-1 matcher

lib/common/Pulse.Lib.Core.fsti

@@ -613,6 +613,16 @@ let match_rewrite_tac (_:unit) : T.Tac unit =
     T.mapply (`slprop_equiv_ext');
     T.trefl ()
 
+let match_rename_tac (_:unit) : T.Tac unit =
+    let open T in
+    let b = T.nth_var (-1) in
+    T.norm []; // Needed, or otherwise the `tcut` in grewrite_eq can fail, unsure why.
+    try (
+      T.grewrite_eq b;
+      T.trefl ()
+    )
+    with _ -> T.smt()
+
 [@@deprecated "Use (rewrite .. as .. by ..) syntax instead!"]
 val rewrite_by (p:slprop) (q:slprop)
                (t:unit -> T.Tac unit)

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.Borrow.fst

@@ -41,7 +41,7 @@ noeq type blockchain_root = {
 type lifetime : Type0 =
   ref blockchain_root
 
-let fpts_to #t (r: ref t) (x: t) = exists* p. pts_to r #p x
+let fpts_to #t ([@@@mkey] r: ref t) (x: t) = exists* p. pts_to r #p x
 
 ghost fn dup_fpts_to u#t (t: Type u#t) r x () : duplicable_f (fpts_to #t r x) = {
   unfold fpts_to r x;
@@ -189,7 +189,7 @@ type stored_shape =
   | Stored
   | StoredBoth : stored_shape -> stored_shape -> stored_shape
 
-let rec bc_stored ([@@@mkey] x: blockchain_edge) ([@@@mkey] d: stored_shape) (y: slprop) : Tot slprop (decreases d) =
+let rec bc_stored ([@@@mkey] x: blockchain_edge) (d: stored_shape) (y: slprop) : Tot slprop (decreases d) =
   match d with
   | Stored -> exists* z. slprop_ref_pts_to x.be_prop z ** later z ** trade (later z) y
   | StoredCheckedOut -> live x.be_ref ** y
@@ -199,15 +199,15 @@ let rec bc_stored ([@@@mkey] x: blockchain_edge) ([@@@mkey] d: stored_shape) (y:
     bc_stored b db yb **
     trade (ya ** yb) y
 
-let rec rt_stored ([@@@mkey] x: ref blockchain_root) ([@@@mkey] n: unat) (b: slprop) : Tot slprop (decreases n) =
+let rec rt_stored ([@@@mkey] x: ref blockchain_root) (n: unat) (b: slprop) : Tot slprop (decreases n) =
   match n with
   | Zero -> trade emp b
   | Succ n -> exists* r (b1 b2: slprop). fpts_to x r **
     (exists* d. bc_stored r.rt_tree d b1) **
     rt_stored r.rt_next n b2 **
     trade (b1 ** b2) b
 
-let owns_end ([@@@mkey] x: ref blockchain_root) ([@@@mkey] n: unat) =
+let owns_end ([@@@mkey] x: ref blockchain_root) (n: unat) =
   exists* y. root_idx x n y ** live y
 
 ghost fn elim_owns_end_zero x
@@ -574,7 +574,7 @@ ghost fn share_borrow' #a (p q1 q2: slprop)
   dup (slprop_ref_pts_to eb.be_prop q2) ();
   fold valid_split l.be_prop ea.be_prop eb.be_prop;
   dup (bc_idx r.rt_tree is l) ();
-  dup (valid_split l.be_prop ra rb) ();
+  dup (valid_split l.be_prop ea.be_prop eb.be_prop) ();
   push_bc_idx r.rt_tree is false l; 
   push_bc_idx r.rt_tree is true l; 
   dup (root_idx' a n r) ();

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.GhostPCMReference.fst

@@ -63,7 +63,7 @@ fn read u#a
   returns v:(v:a { compatible p x v /\ p.refine v })
   ensures pts_to r (f v)
 {
-  with inst. assert small_token u#a inst; let inst = inst;
+  with inst. unfold small_token u#a inst; let inst = inst; fold small_token inst;
   U.downgrade_val (C.ghost_read #(U.raise_t a) #(raise p) r (hide (U.raise_val (reveal x))) (raise_refine p x f));
 }
 
@@ -92,7 +92,7 @@ fn write u#a
   requires pts_to r x
   ensures  pts_to r y
 {
-  with inst. assert small_token u#a inst; let inst = inst;
+  with inst. unfold small_token u#a inst; let inst = inst; fold small_token inst;
   C.ghost_write #(U.raise_t a) #(raise p) r (hide (U.raise_val (reveal x))) (hide (U.raise_val (reveal y)))
     (raise_upd f)
 }
@@ -107,18 +107,12 @@ fn share u#a
   requires pts_to r (v0 `op pcm` v1)
   ensures  pts_to r v0 ** pts_to r v1
 {
-  with inst. assert small_token u#a inst; let inst = inst;
-  fold small_token u#a inst;
+  with inst. unfold small_token u#a inst; let inst = inst;
+  fold small_token inst;
+  fold small_token inst;
   C.ghost_share #_ #(PR.raise pcm) r (U.raise_val v0) (U.raise_val v1)
 }
 
-[@@allow_ambiguous]
-ghost fn drop_amb (p: slprop)
-  requires p
-{
-  drop_ p
-}
-
 [@@allow_ambiguous]
 ghost
 fn gather u#a
@@ -131,11 +125,9 @@ fn gather u#a
   returns  squash (composable pcm v0 v1)
   ensures  pts_to r (op pcm v0 v1)
 {
-  with inst. assert C.ghost_pcm_pts_to #_ #(raise #a #inst pcm) r (U.raise_val v1);
-  with inst'. assert C.ghost_pcm_pts_to #_ #(raise #a #inst' pcm) r (U.raise_val v1);
-  drop_amb (small_token u#a inst');
-  let inst = inst;
-  C.ghost_gather #_ #(PR.raise pcm) r (U.raise_val v0) (U.raise_val v1)
+  with inst. assert C.ghost_pcm_pts_to #_ #(raise #a #inst pcm) r (U.raise_val #a #inst v1);
+  drop_ (small_token inst);
+  C.ghost_gather #_ #(PR.raise #a #inst pcm) r (U.raise_val #a #inst v0) (U.raise_val #a #inst v1)
 }
 
 ghost fn pts_to_not_null u#a (#a:Type u#a)

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

@@ -556,7 +556,6 @@ fn delete
     if (voff = ht.sz)
     {
       cont := false;
-      rewrite each vcont as false; // also relying on #110
     }
     else
     {
@@ -584,7 +583,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))]
 

lib/pulse/lib/Pulse.Lib.InsertionSort.fst

@@ -134,6 +134,7 @@ let step_outer_invariant
 #pop-options
 
 
+#push-options "--z3rlimit_factor 2"
 fn insertion_sort u#a
       (#t:Type u#a)
       {| total_order t |}
@@ -202,6 +203,7 @@ ensures exists* s'. (a |-> s') **
   with s'. assert (a |-> s');
   assert pure (Seq.slice s' 0 (Seq.length s') `Seq.equal` s');
 }
+#pop-options
 
 instance total_order_int : total_order int = {
   compare = FStar.Order.compare_int;

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

@@ -290,6 +290,9 @@ fn move_next (#t:Type) (x:llist t)
     let node = !np;
     intro_yields_cons np;
     rewrite each (Some np) as x;
+    with tl. assert is_list node.tail 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
 }
 
@@ -408,20 +411,24 @@ fn non_empty_list (#t:Type0) (x:llist t)
     intro_is_list_cons x v #n #tl;
 }
 
+let is_cons #t ([@@@mkey] x: list t) hd tl = pure (x == hd :: tl)
+
 fn move_next_forall (#t:Type) (x:llist t)
     requires is_list x 'l ** pure (Some? x)
     returns y:llist t
     ensures exists* hd tl.
         is_list y tl **
         (forall* tl'. is_list y tl' @==> is_list x (hd::tl')) **
-        pure ('l == hd::tl)
+        is_cons 'l hd tl
 { 
     let np = Some?.v x;
     is_list_cases_some x np;
     let node = !np;
     intro (forall* tl'. is_list node.tail tl' @==> is_list x (node.head::tl')) #(np |-> node) fn _ tl' {
       intro_is_list_cons x np;
     };
+    with tl. assert is_list node.tail tl;
+    fold is_cons 'l node.head tl;
     node.tail
 }
 
@@ -458,14 +465,14 @@ fn append_iter (#t:Type) (x y:llist t)
     with ll pfx sfx. _;
     some_iff_cons ll;
     let next = move_next_forall Pulse.Lib.Reference.(!cur);
-    with hd tl. _;
+    with hd tl. unfold is_cons sfx hd tl;
     (* this is the key induction step *)
     FA.trans_compose
         (is_list next) (is_list ll) (is_list x)
-        (fun tl -> hd :: tl)
+        (fun tl -> reveal hd :: tl)
         (fun tl -> pfx @ tl);
-    rewrite (forall* tl. is_list next tl @==> is_list x (pfx@(hd::tl)))
-          as (forall* tl. is_list next tl @==> is_list x ((pfx@[hd])@tl));
+    rewrite (forall* tl. is_list next tl @==> is_list x (pfx@(reveal hd::tl)))
+          as (forall* tl. is_list next tl @==> is_list x ((pfx@[reveal hd])@tl));
     Pulse.Lib.Reference.(cur := next);
   };
   with ll pfx sfx. _;
@@ -526,7 +533,7 @@ fn split (#t:Type0) (x:llist t) (n:U32.t) (#xl:erased (list t))
   {
     with i ll pfx sfx. _;
     let next = move_next_forall Pulse.Lib.Reference.(!cur);
-    with hd tl. _;
+    with hd tl. unfold is_cons sfx hd tl;
     (* this is the key induction step *)
     FA.trans_compose
         (is_list next) (is_list ll) (is_list x)

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)
 }