Unify implicit type arguments in slprops.

Author: gebner

lib/pulse/lib/Pulse.Lib.Array.Core.fst

@@ -238,6 +238,7 @@ fn mask_alloc_with_vis u#a (elt: Type u#a) {| small_type u#a |}
   let arr: array elt = { base_ref = b; base_len = SZ.v n; length = SZ.v n; offset = 0; alloc_loc = l; vis };
   rewrite each b as lptr_of arr;
   assert pure (v `Map.equal` mk_carrier' arr 1.0R (Seq.create (SZ.v n) None) (fun _ -> l_True) (vis l));
+  rewrite each hide (SZ.v n) as arr.base_len;
   fold pts_to_mask arr (Seq.create (SZ.v n) None) (fun _ -> l_True);
   arr
 }
@@ -290,6 +291,7 @@ ghost fn pcm_rw u#a (#t: Type u#a)
   let i = get_mask_idx m2 (length a2);
   assert pure (mask_nonempty m2 (length a2) ==>
     Map.sel (mk_carrier' a2 p2 s2 m2 (process_of l)) (i + a2.offset) == Some ((Seq.index s2 i, process_of l), p2));
+  rewrite each a1.base_len as a2.base_len;
   fold pts_to_mask a2 #p2 s2 m2;
 }
 

lib/pulse/lib/Pulse.Lib.GhostPCMReference.fst

@@ -71,8 +71,8 @@ fn read u#a
   returns v:(v:a { compatible p x v /\ p.refine v })
   ensures pts_to r (f v)
 {
-  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));
+  with inst. assert small_token inst;
+  U.downgrade_val (C.ghost_read #(U.raise_t #inst a) r (U.raise_val (reveal x)) (raise_refine p x f));
 }
 
 
@@ -100,8 +100,8 @@ fn write u#a
   requires pts_to r x
   ensures  pts_to r y
 {
-  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)))
+  with inst. assert small_token inst;
+  C.ghost_write #(U.raise_t #inst a) r (U.raise_val (reveal x)) (U.raise_val (reveal y))
     (raise_upd f)
 }
 
@@ -116,10 +116,9 @@ fn share u#a
   ensures pts_to r v0
   ensures pts_to r v1
 {
-  with inst. unfold small_token u#a inst; let inst = inst;
+  with inst. assert small_token inst;
   fold small_token inst;
-  fold small_token inst;
-  C.ghost_share #_ #(PR.raise pcm) r (U.raise_val v0) (U.raise_val v1)
+  C.ghost_share #(U.raise_t #inst a) r (U.raise_val v0) (U.raise_val v1)
 }
 
 [@@allow_ambiguous]
@@ -135,9 +134,11 @@ 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 #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)
+  with inst0. assert C.ghost_pcm_pts_to r (U.raise_val #a #inst0 v0);
+  with inst1. assert C.ghost_pcm_pts_to r (U.raise_val #a #inst1 v1);
+  drop_ (small_token inst1);
+  rewrite each inst1 as inst0;
+  C.ghost_gather #(U.raise_t #inst0 a) r (U.raise_val v0) (U.raise_val v1)
 }
 
 ghost fn pts_to_not_null u#a (#a:Type u#a)

lib/pulse/lib/Pulse.Lib.PCMReference.fst

@@ -79,21 +79,17 @@ fn read u#a (#a:Type u#a) (#p:pcm a) (r:pcm_ref p) (x:erased a)
   returns v:(v:a {compatible p x v /\ p.refine v})
   ensures pcm_pts_to r (f v)
 {
-  let inst = pts_to_small r _;
-  drop_ (small_token u#a _);
-  fold small_token u#a inst;
-  U.downgrade_val (C.read #(U.raise_t a) #(raise p) r (hide (U.raise_val (reveal x))) (raise_refine p x f));
+  with inst. assert small_token inst;
+  U.downgrade_val (C.read #(U.raise_t #inst a) r (U.raise_val (reveal x)) (raise_refine p x f));
 }
 
 fn write u#a (#a:Type u#a) (#p:pcm a) (r:pcm_ref p) (x y:erased a)
     (f:frame_preserving_upd p x y)
   requires pcm_pts_to r x
   ensures pcm_pts_to r y
 {
-  let inst = pts_to_small r _;
-  drop_ (small_token u#a _);
-  fold small_token u#a inst;
-  C.write #(U.raise_t a) #(raise p) r (hide (U.raise_val (reveal x))) (hide (U.raise_val (reveal y)))
+  with inst. assert small_token inst;
+  C.write #(U.raise_t #inst a) r (U.raise_val (reveal x)) (U.raise_val (reveal y))
     (raise_upd f)
 }
 
@@ -103,11 +99,9 @@ ghost fn share u#a (#a:Type u#a) (#pcm:pcm a) (r:pcm_ref pcm)
   ensures pcm_pts_to r v0
   ensures pcm_pts_to r v1
 {
-  let inst = pts_to_small r _;
-  drop_ (small_token u#a _);
-  fold small_token inst;
+  with inst. assert small_token inst;
   fold small_token inst;
-  C.share #(U.raise_t a) #(raise pcm) r (U.raise_val v0) (U.raise_val v1);
+  C.share #(U.raise_t #inst a) r (U.raise_val v0) (U.raise_val v1);
 }
 
 [@@allow_ambiguous]
@@ -117,9 +111,9 @@ ghost fn gather u#a (#a:Type u#a) (#pcm:pcm a) (r:pcm_ref pcm) (v0:a) (v1:a)
   returns _: squash (composable pcm v0 v1)
   ensures pcm_pts_to r (op pcm v0 v1)
 {
-  let inst = pts_to_small r v0;
-  with inst'. assert C.pcm_pts_to #_ #(raise #a #inst' pcm) r (U.raise_val #a #inst' v1);
-  rewrite each inst' as inst;
-  drop_ (small_token u#a inst');
-  C.gather #(U.raise_t #inst a) #(raise #a #inst pcm) r (U.raise_val #a #inst v0) (U.raise_val #a #inst v1);
+  with inst0. assert C.pcm_pts_to r (U.raise_val #a #inst0 v0);
+  with inst1. assert C.pcm_pts_to r (U.raise_val #a #inst1 v1);
+  drop_ (small_token inst1);
+  rewrite each inst1 as inst0;
+  C.gather #(U.raise_t #inst0 a) r (U.raise_val v0) (U.raise_val v1);
 }

lib/pulse/lib/Pulse.Lib.Send.fst

@@ -304,24 +304,6 @@ ghost fn on_exists_intro u#a #l (#a: Type u#a) (p: a -> slprop)
   }
 }
 
-[@@pulse_eager_intro]
-ghost fn on_exists_intro2 u#a u#b #l (#a: Type u#a) (#b: Type u#b)
-    (p: (x:a -> y:b -> slprop))
-  requires literally (exists* (x:a) (y:b). on l (p x y))
-  ensures on l (exists* (x:a) (y:b). p x y)
-{
-  admit ()
-}
-
-[@@pulse_eager_intro]
-ghost fn on_exists_intro3 u#a u#b u#c #l (#a: Type u#a) (#b: Type u#b) (#c: Type u#c)
-    (p: (a -> b -> c -> slprop))
-  requires literally (exists* (x:a) (y:b) (z:c). on l (p x y z))
-  ensures on l (exists* (x:a) (y:b) (z:c). p x y z)
-{
-  admit()
-}
-
 [@@pulse_eager_elim]
 ghost fn on_exists_elim u#a #l (#a: Type u#a) (p: a -> slprop)
   requires on l (exists* x. p x)
@@ -424,11 +406,13 @@ ghost fn is_send_across_exists' u#a #b #g (#a: Type u#a) (p: a->slprop) {| ((x:a
 let is_send_across_exists = is_send_across_exists'
 
 ghost fn is_send_in_same_process p : is_send (in_same_process p) = l l' {
-  admit ();
   ghost_impersonate l
     (on l (in_same_process p))
     (on l' (in_same_process p))
     fn _ {
+      on_elim (in_same_process p);
+      unfold in_same_process p;
+      loc_gather l;
       ghost_impersonate l' emp (on l' (in_same_process p)) fn _ {
         loc_dup l';
         fold in_same_process p;
@@ -463,7 +447,6 @@ let timeless_on_same_process p =
   assert_norm (on_same_process p == (exists* l. in_same_process l ** on l p))
 
 ghost fn is_send_on_same_process p : is_send (on_same_process p) = l1 l2 {
-  admit ();
   ghost_impersonate l1
     (on l1 (on_same_process p))
     (on l2 (on_same_process p))
@@ -503,7 +486,6 @@ ghost fn sendable_intro p {| inst: is_send p |}
 }
 
 ghost fn is_send_sendable p : is_send (sendable p) = l1 l2 {
-  admit ();
   ghost_impersonate l1 (on l1 (sendable p)) (on l2 (sendable p)) fn _ {
     on_elim (sendable p);
     unfold sendable p;

src/checker/Pulse.Checker.Prover.fst

@@ -754,7 +754,10 @@ let is_mkey (t:R.term) : bool =
   | _ -> false
 
 let binder_is_mkey (b:R.binder) : bool =
-  List.Tot.existsb is_mkey (R.inspect_binder b).attrs
+  if List.Tot.existsb is_mkey (R.inspect_binder b).attrs then true else
+  // Treat type arguments as mkeys, as F* will happily unify terms of different types.
+  if R.Tv_Type? (R.inspect_ln (R.inspect_binder b).sort) then true else
+  false
 
 let binder_is_pred (b:R.binder) : option nat =
   let doms, c = R.collect_arr_ln (R.inspect_binder b).sort in

test/bug-reports/Bug174.fst.output.expected

@@ -1,13 +1,8 @@
-* Info at Bug174.fst(15,30-15,42):
+* Info at Bug174.fst(15,10-15,37):
   - Expected failure:
-  - Ill-typed term: !r
-  - Expected a term of type
-      fn
-        requires r |-> Frac 1.0R v
-        returns x : t
-        ensures r |-> Frac 1.0R v ** rewrites_to x v
-  - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
-  - See also Bug174.fst(14,1-15,40)
+  - Tactic failed
+  - Cannot prove:
+      Pulse.Lib.Reference.pts_to r (*?u173*)_
+  - In the context:
+      Pulse.Lib.Reference.pts_to r v