Pulse: let-bind applications on return

pulse/lib/pulse/lib/Pulse.Lib.AVLTree.fst

@@ -463,6 +463,11 @@ fn read_node
   let n = !p;
   rewrite p |-> n as Some?.v tree |-> n;
   (n.left, n.data, n.right, ())
+  // let x
+  //   : (tree_t a & a & tree_t a & squash (Some? tree))
+  //   = (n.left, n.data, n.right, ());
+  // assert rewrites_to x (n.left, n.data, n.right, ());
+  // x
 }
 
 fn write_node

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

@@ -200,6 +200,26 @@ let check_tot_bind
 = let g = Pulse.Typing.Env.push_context g "check_tot_bind" t.range in
 
   let Tm_TotBind { binder=b; head=e1; body=e2 } = t.term in
+  // When binding an application at an annotated type, first bind it at its
+  // inferred type, then coerce to the annotation:
+  //   let x : t = e   ~>   let x0 = e in let x : t = x0
+  // This way any logical content of e's inferred type (e.g. a Lemma's
+  // postcondition, which shows up as a refinement) is brought into scope
+  // before we force x to have type t. Otherwise `let x : unit = lem ()` would
+  // check `lem ()` at the bare type `unit` and drop the postcondition.
+  // Mirrors the returned-application handling for #4314. See Bug4314.
+  let _, args = T.collect_app_ln e1 in
+  if (not (Tm_Unknown? (inspect_term b.binder_ty))) && Cons? args
+  then (
+    let x0 = fresh g in
+    let b0 = mk_binder_ppname tm_unknown b.binder_ppname in
+    let inner = { t with term = Tm_TotBind { binder=b; head=term_of_no_name_var x0; body=e2 } } in
+    let inner = close_st_term inner x0 in
+    let tt = { t with term = Tm_TotBind { binder=b0; head=e1; body=inner } } in
+    Pulse.Checker.Util.debug g "pulse.hoist" (fun _ ->
+      Printf.sprintf "check_tot_bind: sequencing annotated application binding (Bug4314):\n%s\n" (show tt));
+    check g pre post_hint res_ppname tt
+  ) else (
   let rebuild (head:either term st_term) : T.Tac (t:st_term { Tm_Bind? t.term }) =
     match head with
     | Inl e1' ->
@@ -221,4 +241,5 @@ let check_tot_bind
       (show t)
       (show t'));
     check g pre post_hint res_ppname t'
-#pop-options
+  )
+#pop-options

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

@@ -178,8 +178,45 @@ let check
         match ctag_of_effect_annot p.effect_annot with
         | Some c -> c
         | None -> STT_Atomic in
-      check_core g ctxt post_hint res_ppname st (Some ctag)
-
+      // If we are returning an application, introduce an intermediate binding
+      // for it. This makes sure whatever logical payload the call provides (as
+      // a postcondition) is available to prove the postcondition of the current
+      // function (the caller). See #4314.
+      let _, args = T.collect_app_ln f.term in
+      if Cons? args then (
+        let x = fresh g in
+        let expected_type =
+          match post_hint with
+          | PostHint t -> t.ret_ty
+          | TypeHint t -> t
+          | NoHint -> f.expected_type // This seems always = to tm_unknown, oh well
+        in
+        Pulse.Checker.Util.debug g "pulse.return" (fun _ ->
+          Printf.sprintf "About to let-bind return, expected type = %s" 
+            (Pulse.Show.show expected_type));
+        let b = mk_binder_ppname expected_type res_ppname in
+        let body =
+          mk_term (Tm_Return { expected_type
+                             ; insert_eq = false
+                             ; term = term_of_no_name_var x }) st.range in
+        (* Add a rewrites_to, so the extra alias does not prevent slprop proving. *)
+        let assertion =
+          ASSERT { elaborated=true;
+                   p = tm_pure (mk_rewrites_to_p u_unknown expected_type (term_of_no_name_var x) f.term)
+                   }
+        in
+        let tt = { st with term = Tm_ProofHintWithBinders {
+                                    hint_type = assertion;
+                                    binders = [];
+                                    t = body; } } in
+        let tt = close_st_term tt x in
+        let tt = { st with term = Tm_TotBind { binder = b; head = f.term; body=tt } } in
+        Pulse.Checker.Util.debug g "pulse.return" (fun _ ->
+          Printf.sprintf "Sequencing tail return (#4314): %s"
+            (Pulse.Syntax.Printer.st_term_to_string tt));
+        check g ctxt post_hint res_ppname tt
+      ) else
+        check_core g ctxt post_hint res_ppname st (Some ctag)
     )
     | _ ->  check_core g ctxt post_hint res_ppname st None
   )

pulse/src/checker/Pulse.Typing.fst

@@ -81,13 +81,15 @@ let mk_slprop_eq (e0 e1:term) : term =
 
 let rewrites_to_p_lid = Pulse.Reflection.Util.mk_pulse_lib_core_lid "rewrites_to_p"
 
-let mk_sq_rewrites_to_p u t x y =
+let mk_rewrites_to_p u t x y =
   let open R in
   let hd = pack_fv rewrites_to_p_lid in
   let hd = pack_ln (Tv_UInst hd [u]) in
   let args = [(t, Q_Implicit); (x, Q_Explicit); (y, Q_Explicit)] in
-  mk_squash (R.mk_app hd args)
+  R.mk_app hd args
 
+let mk_sq_rewrites_to_p u t x y =
+  mk_squash (mk_rewrites_to_p u t x y)
 
 let mk_ref (t:term) : term = tm_pureapp (tm_uinst (as_fv ref_lid) [u0]) None t
 
@@ -613,4 +615,4 @@ let comp_post_matches_hint (c:comp_st) (post_hint:post_hint_opt_t) =
     comp_u c == post_hint.u /\
     comp_post c == post_hint.post /\
     effect_annot_matches c post_hint.effect_annot
-  | _ -> True
+  | _ -> True

pulse/test/bug-reports/Bug.DesugaringError.fst.output.expected

@@ -9,6 +9,7 @@
 
 * Info at Bug.DesugaringError.fst(25,9-25,10):
   - Expected failure:
+  - Ill-typed term
   - Expected expression of type Prims.nat got expression y of type Prims.bool
 
 * Info at Bug.DesugaringError.fst(36,4-36,8):

pulse/test/bug-reports/Bug36.fst.output.expected

@@ -1,4 +1,5 @@
 * Info at Bug36.fst(12,6-12,7):
   - Expected failure:
+  - Ill-typed term
   - Expected expression of type Type got expression n of type Prims.nat
 

pulse/test/error_messages/ReturnImplicit.fst.output.expected

@@ -3,7 +3,9 @@
   - Ill-typed term
   - Assertion failed
   - The SMT solver could not prove the query.
-  - Env = (uu___0 : Prims.unit)
-  - VC = Prims.l_False
+  - Env =
+      (uu___0 : Prims.unit) (_fret : Prims.int)
+      (__ : Prims.squash (_fret == -1))
+  - VC = _fret >= 0
   - Also see: Prims.fst(642,18-642,24)
 

stage3/dune/main.ml

@@ -32,7 +32,9 @@ let x =
 
       (* Only on stage3: we've baked Pulse into the compiler, which
          brings in the plugin library. Make sure F* knows this so it
-         will not try to load it again. *)
+         will not try to load it again. Also mark Pulse as loaded plugin,
+         so #lang-pulse will not attempt to load it again. *)
       Fstarcompiler.FStarC_Plugins.loaded_plugin_lib := true;
+      Fstarcompiler.FStarC_Plugins.loaded := "pulse" :: !Fstarcompiler.FStarC_Plugins.loaded;
 
       Fstarcompiler.FStarC_Main.main ()

tests/bug-reports/closed/Bug4314.fst

@@ -0,0 +1,30 @@
+module Bug4314
+
+#lang-pulse
+open Pulse
+
+assume val q : prop
+
+assume val lem () : Lemma (ensures q)
+fn test0 ()
+  ensures pure q
+  { let x : unit = lem (); () }
+
+fn test ()
+  ensures pure q
+  { lem (); }
+
+assume val slem () : squash q
+fn test2 ()
+  ensures pure q
+  { slem (); }
+
+assume val slem0 : squash q
+fn test3 ()
+  ensures pure q
+  { slem0; }
+
+assume val plem () : ghost fn ensures pure q
+fn ptest ()
+  ensures pure q
+  { plem (); }