Do not force type constructors to be injective

.github/agents/FStarDev.md

@@ -185,6 +185,12 @@ make -j$(nproc) 3 FSTAR_EXTERNAL_STAGE0=/path/to/fstar.exe
 3. Test: `make test-3` or run targeted tests
 4. Repeat
 
+If you make a change that modifies the behavior of the compiler and you need to test
+that it does not introduce any regressions without doing a full bootstrap, you can do
+`make clean-2` followed by `make`: this will rebuild the compiler, then the
+standard library using the new compiler, then stage3 and Pulse etc, without needing to
+rebuild stage0 and stage1.
+
 Note: as the compiler is modified and rebuilt, the tests that succeeded
 are not invalidated to make iteration faster. A final `make -C tests clean && make test`
 is usually useful.

pulse/lib/common/Pulse.Lib.Core.fsti

@@ -67,7 +67,7 @@ val allow_ambiguous : unit
 (***** begin slprop_equiv *****)
 
 (* A full slprop. In universe 4 (currently!) *)
-[@@erasable]
+[@@erasable; unifier_hint_injective_type]
 val slprop : Type u#4
 
 val timeless (p: slprop) : prop

pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst

@@ -671,7 +671,9 @@ let array_swap_inner_invariant
         Seq.index s idx == Seq.index s0 (if i' < i || (i' = i && j' < j) then jump (n) (l) idx else idx)
   )
 
-#push-options "--z3rlimit 20"
+#restart-solver
+#push-options "--z3rlimit 10"
+
 let array_swap_inner_invariant_end
   (#t: Type)
   (n: nat)

pulse/test/Bug4239.fst

@@ -0,0 +1,28 @@
+module Bug4239
+open Pulse.Nolib
+#lang-pulse
+
+let natlt (n: nat) = i:nat { i < n }
+
+let works #n (x: natlt n -> bool) (i: nat { i < n }) =
+  let a: (natlt i -> bool) = x in
+  ()
+
+fn doesnt_work #n (x: natlt n -> bool) (i: nat { i < n }) {
+  let a: (natlt i -> bool) = x;
+  ()
+}
+
+module SZ = FStar.SizeT
+type sz  = FStar.SizeT.t
+type szlt (n:int) = i:sz{SZ.v i <  n}
+fn bug
+  (x y : sz {SZ.v y <= SZ.v x})
+  (k : szlt (SZ.v y))
+{
+  assert pure (SZ.v k < SZ.v y);
+  assert pure (SZ.v y <= SZ.v x);
+  assert pure (SZ.v k < SZ.v x);
+  let k : szlt (SZ.v x) = k; // Fails, but should work
+  ();
+}

pulse/test/LoopInvariants.fst.output.expected

@@ -1,4 +1,4 @@
-* Info at LoopInvariants.fst(65,4-65,8):
+* Info at LoopInvariants.fst(65,6-65,8):
   - Expected failure:
   - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to s 3
@@ -10,10 +10,10 @@
       (s : Pulse.Lib.Reference.ref Prims.int) (meas : Prims.unit)
       (__ : Prims.squash (meas == ())) (__ : Prims.squash (true == true))
       (__ : Prims.unit)
-  - VC = Pulse.Lib.Reference.pts_to s 3 == Pulse.Lib.Reference.pts_to s 2
-  - See also LoopInvariants.fst(65,4-65,10)
+  - VC = Prims.l_False
+  - See also LoopInvariants.fst(65,9-65,10)
 
-* Info at LoopInvariants.fst(76,4-76,8):
+* Info at LoopInvariants.fst(76,6-76,8):
   - Expected failure:
   - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to s 3
@@ -25,6 +25,6 @@
       (s : Pulse.Lib.Reference.ref Prims.int) (meas : Prims.unit)
       (__ : Prims.squash (meas == ())) (__ : Prims.squash (true == true))
       (__ : Prims.unit)
-  - VC = Pulse.Lib.Reference.pts_to s 3 == Pulse.Lib.Reference.pts_to s 2
-  - See also LoopInvariants.fst(76,4-76,10)
+  - VC = Prims.l_False
+  - See also LoopInvariants.fst(76,9-76,10)
 

pulse/test/bug-reports/Bug4239Variant.fst

@@ -0,0 +1,40 @@
+module Bug4239Variant
+
+#lang-pulse
+open Pulse
+module FE = FStar.FunctionalExtensionality
+
+assume val rel : Type0 -> Type0 -> Type0
+let type_spec (impl_elt: Type0) = dtuple2 Type0 (rel impl_elt)
+
+let mk_spec
+  (#impl_elt: Type0)
+  (#src_elt: Type0)
+  (r: rel impl_elt src_elt)
+: Tot (Ghost.erased (type_spec impl_elt))
+= Ghost.hide (| _, r |)
+
+let eq_test_for (#t: Type) (x1: t) : Type =
+  FE.restricted_t t (fun x2 -> (y: bool { y == true <==> x1 == x2 }))
+
+let eq_test (t: Type) : Type =
+  FE.restricted_t t (fun x1 -> eq_test_for x1)
+
+let mk_iterator 
+    (#tkey: Type0)
+    (key_eq: Ghost.erased (eq_test tkey))
+    (#ikey: Type0)
+    (#r1: rel ikey tkey)
+= 
+ let kk : Ghost.erased (eq_test (dfst (mk_spec r1))) = key_eq in
+ ()
+
+fn mk_iterator2
+  (#tkey: Type0)
+    (key_eq: Ghost.erased (eq_test tkey))
+    (#ikey: Type0)
+    (#r1: rel ikey tkey)
+{
+ let kk : Ghost.erased (eq_test (dfst (mk_spec r1))) = key_eq;
+ ()
+}

pulse/test/nolib/AdmitDoesNotSimpl.fst.output.expected

@@ -3,20 +3,20 @@
   - Current context:
       foo x
   - In typing environment:
-      y#292 : int
-      x#290 : int
+      y#294 : int
+      x#292 : int
 
-      goto _return#345 requires foo x
+      goto _return#347 requires foo x
 
 * Info at AdmitDoesNotSimpl.fst(20,2-20,9):
   - Admitting continuation.
   - Current context:
       foo x
   - In typing environment:
-      y#292 : int
-      x#290 : int
+      y#294 : int
+      x#292 : int
 
-      goto _return#345 requires foo x
+      goto _return#347 requires foo x
 
 * Info at AdmitDoesNotSimpl.fst(27,2-27,9):
   - Admitting continuation.

src/parser/FStarC.Parser.Const.fst

@@ -361,6 +361,8 @@ let normalize_for_extraction_type_lid = psconst "normalize_for_extraction_type"
 let tcdecltime_attr = attr "tcdecltime"
 let noextract_to_attr = attr "noextract_to"
 let unifier_hint_injective_lid = attr "unifier_hint_injective"
+let unifier_hint_not_injective_lid = attr "unifier_hint_not_injective"
+let unifier_hint_injective_type_lid = attr "unifier_hint_injective_type"
 let commute_nested_matches_lid = attr "commute_nested_matches"
 let ite_soundness_by_attr = attr "ite_soundness_by"
 let default_effect_attr = attr "default_effect"