Merge pull request #4257 from FStarLang/gebner_fix4255

Check equality of slprops in prover.

Author: gebner

pulse/src/checker/Pulse.Checker.Prover.fst

@@ -1091,7 +1091,7 @@ let try_apply_elim_lemma (pg: penv) (lid: R.name) (i: nat) (ctxt: slprop_view) :
           let typing = core_check_term g t T.E_Ghost ty in
           let t' = wtag (Some STT_Ghost) (Tm_ST { t; args=[] }) in
 
-
+          check_slprop_equiv_ext (RU.range_of_term pre) g (elab_slprop ctxt) pre;
 
           assume (elab_slprop ctxt == pre);
           let k_t = cont_elab_with_bind_nondep_unit c t' in
@@ -1133,9 +1133,7 @@ let try_apply_eager_intro_lemma (pg: penv) (lid: R.name) (i: nat) ctxt (goal: sl
           let typing = core_check_term g'' t T.E_Ghost ty in
           let t' = wtag (Some STT_Ghost) (Tm_ST { t; args=[] }) in
 
-
-
-
+          check_slprop_equiv_ext (RU.range_of_term (elab_slprop goal)) g post' (elab_slprop goal);
 
           let k_typing = cont_elab_with_bind_nondep_unit c t' in
           cont_elab_refl g ctxt ([] @ ctxt),
@@ -1238,9 +1236,7 @@ let try_apply_intro_lemma (pg: penv) (lid: R.name) (i: nat) ctxt (goal: slprop_v
           let typing = core_check_term g' t T.E_Ghost ty in
           let t' = wtag (Some STT_Ghost) (Tm_ST { t; args=[] }) in
 
-
-
-
+          check_slprop_equiv_ext (RU.range_of_term (elab_slprop goal)) g (elab_slprop post''_i) (elab_slprop goal);
 
           let k_typing = cont_elab_with_bind_nondep_unit c t' in
           let k_typing = cont_elab_frame k_typing ctxt' in

pulse/test/Bug4256.fst

@@ -0,0 +1,58 @@
+module Bug4256
+#lang-pulse
+open Pulse
+
+let foo ([@@@mkey] m: nat) (n: nat) : slprop =
+  pure (m = n)
+
+[@@pulse_intro]
+ghost fn foo_refl (m: nat)
+  ensures foo m m
+{
+  fold foo m m
+}
+
+[@@expect_failure [19]]
+ghost fn uhoh_intro ()
+  ensures pure False
+{
+  assert foo 2 3;
+  unfold foo
+}
+
+let bar ([@@@mkey] m: nat) (n: nat) : slprop =
+  pure (m = n)
+
+[@@pulse_eager_intro]
+ghost fn bar_refl (m: nat)
+  ensures bar m m
+{
+  fold bar m m
+}
+
+[@@expect_failure [19]]
+ghost fn uhoh_eager_intro ()
+  ensures pure False
+{
+  assert bar 2 3;
+  unfold bar
+}
+
+let baz ([@@@mkey] m: nat) (n: nat) : slprop =
+  pure (m <> n)
+
+[@@pulse_eager_elim]
+ghost fn baz_refl (m: nat)
+  requires baz m m
+  ensures is_unreachable
+{
+  unfold baz m m;
+  unreachable ()
+}
+
+[@@expect_failure [19]]
+ghost fn uhoh_eager_elim ()
+  ensures pure False
+{
+  fold baz 2 3;
+}