Regression tests for #4485 and #4487 (fixed by #4515)

tests/bug-reports/closed/Bug4485.fst

@@ -0,0 +1,57 @@
+module Bug4485
+
+(* FStarLang/FStar#4485: the VC simplifier's [clearly_inhabited] judged an
+   arrow type inhabited from its result type alone, ignoring the
+   computation's postcondition, and so rewrote [nonempty e] and
+   [exists (g:e). True] to [True] for the empty type [e] below, proving
+   [False]. Since #4515, a computation type has only a result type, and the
+   postcondition is a refinement of it, which [clearly_inhabited] does not
+   consider inhabited. *)
+
+open FStar.Classical
+
+type e = unit -> Pure int (requires True) (ensures (fun r -> False))
+
+(* [e] is empty: a witness yields [False]. *)
+let witness_gives_false (g:e) : Lemma False = let _ = g () in ()
+
+[@@expect_failure [19]]
+let bad_nonempty () : Lemma False =
+  assert_norm (nonempty e);
+  exists_elim False #e #nonempty_tag () (fun g -> let _ = g () in ())
+
+[@@expect_failure [19]]
+let bad_exists () : Lemma False =
+  assert_norm (exists (g:e). True);
+  exists_elim False #e #(fun _ -> True) () (fun g -> let _ = g () in ())
+
+type e_bool = unit -> Pure bool (requires True) (ensures (fun r -> False))
+
+[@@expect_failure [19]]
+let bad_bool () : Lemma False =
+  assert_norm (exists (g:e_bool). True);
+  exists_elim False #e_bool #(fun _ -> True) () (fun g -> let _ = g () in ())
+
+(* Controls from the issue: [False] follows neither from an inhabited arrow
+   type, nor from an empty one given by a refinement of its result type, nor
+   from one that is inhabited only vacuously. *)
+type ok = unit -> Pure int (requires True) (ensures (fun r -> True))
+
+[@@expect_failure [19]]
+let bad_ok () : Lemma False =
+  assert_norm (exists (g:ok). True);
+  exists_elim False #ok #(fun _ -> True) () (fun g -> let _ = g () in ())
+
+type e_refine = unit -> Tot (r:int{False})
+
+[@@expect_failure [19]]
+let bad_refine () : Lemma False =
+  assert_norm (exists (g:e_refine). True);
+  exists_elim False #e_refine #(fun _ -> True) () (fun g -> let _ = g () in ())
+
+type vacuous = unit -> Pure int (requires False) (ensures (fun r -> False))
+
+let vacuous_witness : vacuous = fun () -> false_elim ()
+
+[@@expect_failure [19]]
+let bad_vacuous (g:vacuous) : Lemma False = let _ = g () in ()

tests/bug-reports/closed/Bug4487.fst

@@ -0,0 +1,55 @@
+module Bug4487
+
+(* FStarLang/FStar#4487: [U.term_eq] compared computation types by effect
+   and result type only, ignoring their pre- and postconditions, so the VC
+   simplifier rewrote [p ==> q] and [p <==> q] to [True] for [p], [q] that
+   differ only in the postcondition of an arrow, proving [False]. Since
+   #4515, a computation type has only a result type, and the postcondition
+   is a refinement of it, which [term_eq] compares. *)
+
+[@@expect_failure [19]]
+let imp = assert_norm ( (forall (f: (unit -> Lemma False)). False)
+                    ==> (forall (f: (unit -> Lemma True)). False) )
+
+(* Both directions of the [<==>] are sent to the SMT solver. *)
+[@@expect_failure [19; 19]]
+let iff = assert_norm ( (forall (f: (unit -> Lemma False)). False)
+                   <==> (forall (f: (unit -> Lemma True)). False) )
+
+let ta : Type0 = unit -> Lemma True
+let tb : Type0 = unit -> Lemma False
+
+(* [tb] is empty ... *)
+let step (f: tb) : Lemma False = f ()
+let lhs () : Lemma (forall (f: tb). False) = FStar.Classical.forall_intro step
+
+(* ... and [ta] is not, so these are false. *)
+[@@expect_failure [19]]
+let bridge () : Lemma ((forall (f: tb). False) ==> (forall (f: ta). False))
+  = assert_norm ((forall (f: tb). False) ==> (forall (f: ta). False))
+
+[@@expect_failure [19; 19]]
+let bridge_iff () : Lemma ((forall (f: tb). False) <==> (forall (f: ta). False))
+  = assert_norm ((forall (f: tb). False) <==> (forall (f: ta). False))
+
+let elim (g: ta) : Lemma (requires forall (f: ta). False) (ensures False) = ()
+
+(* The rest of the issue's proof of [False], with [bridge] as a hypothesis. *)
+let bad (bridge: squash ((forall (f: tb). False) ==> (forall (f: ta). False)))
+  : Lemma False =
+  lhs ();
+  elim (fun () -> ())
+
+(* Controls from the issue: arrows differing in their effect are not equal
+   ... *)
+let tc : Type0 = unit -> Ghost unit (requires True) (ensures fun _ -> True)
+
+[@@expect_failure [19]]
+let bridge_effect () : Lemma ((forall (f: tb). False) ==> (forall (f: tc). False))
+  = assert_norm ((forall (f: tb). False) ==> (forall (f: tc). False))
+
+(* ... and an implication between the same arrow type holds. *)
+let tb' : Type0 = unit -> Lemma False
+
+let bridge_same () : Lemma ((forall (f: tb). False) ==> (forall (f: tb'). False))
+  = assert_norm ((forall (f: tb). False) ==> (forall (f: tb'). False))