From 3886016b4d0062270263cad84e4c3314f1b9ec9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 11 Jun 2026 10:51:55 -0700 Subject: [PATCH 1/5] Pulse: let-bind applications on return This makes sure their return value and postconditions are in-scope for proving the postcondition of the caller. Fixes #4314 --- pulse/src/checker/Pulse.Checker.Return.fst | 22 ++++++++++++++++-- tests/bug-reports/closed/Bug4314.fst | 26 ++++++++++++++++++++++ 2 files changed, 46 insertions(+), 2 deletions(-) create mode 100644 tests/bug-reports/closed/Bug4314.fst diff --git a/pulse/src/checker/Pulse.Checker.Return.fst b/pulse/src/checker/Pulse.Checker.Return.fst index e86f5b1328c..8bc7870e0c1 100644 --- a/pulse/src/checker/Pulse.Checker.Return.fst +++ b/pulse/src/checker/Pulse.Checker.Return.fst @@ -178,8 +178,26 @@ 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 applications, 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 b = mk_binder_ppname tm_unknown res_ppname in + let body = + mk_term (Tm_Return { expected_type = tm_unknown + ; insert_eq = false + ; term = term_of_no_name_var x }) st.range in + let body = close_st_term body x in + let tt = { st with term = Tm_TotBind { binder = b; head = f.term; body } } 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 ) diff --git a/tests/bug-reports/closed/Bug4314.fst b/tests/bug-reports/closed/Bug4314.fst new file mode 100644 index 00000000000..66e9472e912 --- /dev/null +++ b/tests/bug-reports/closed/Bug4314.fst @@ -0,0 +1,26 @@ +module Bug4314 + +#lang-pulse +open Pulse + +assume val q : prop + +assume val lem () : Lemma (ensures q) +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 (); } From 5e71f9bb5998b421bf3a43a7adec19bf26acc60a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 11 Jun 2026 10:58:55 -0700 Subject: [PATCH 2/5] Update expected error output --- .../bug-reports/Bug.DesugaringError.fst.output.expected | 1 + pulse/test/bug-reports/Bug36.fst.output.expected | 1 + .../test/error_messages/ReturnImplicit.fst.output.expected | 6 ++++-- 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/pulse/test/bug-reports/Bug.DesugaringError.fst.output.expected b/pulse/test/bug-reports/Bug.DesugaringError.fst.output.expected index a0b24fa94ca..356178db573 100644 --- a/pulse/test/bug-reports/Bug.DesugaringError.fst.output.expected +++ b/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): diff --git a/pulse/test/bug-reports/Bug36.fst.output.expected b/pulse/test/bug-reports/Bug36.fst.output.expected index 55ba788a279..ebd1cab8832 100644 --- a/pulse/test/bug-reports/Bug36.fst.output.expected +++ b/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 diff --git a/pulse/test/error_messages/ReturnImplicit.fst.output.expected b/pulse/test/error_messages/ReturnImplicit.fst.output.expected index f9e2fd24e7e..fd6c52582c1 100644 --- a/pulse/test/error_messages/ReturnImplicit.fst.output.expected +++ b/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) From 6f7e7c1b013fad7a7a1964ec95aac076ea6a9b29 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 11 Jun 2026 11:52:50 -0700 Subject: [PATCH 3/5] fix --- pulse/src/checker/Pulse.Checker.Return.fst | 27 ++++++++++++++++++---- pulse/src/checker/Pulse.Typing.fst | 8 ++++--- 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/pulse/src/checker/Pulse.Checker.Return.fst b/pulse/src/checker/Pulse.Checker.Return.fst index 8bc7870e0c1..ee5f983df87 100644 --- a/pulse/src/checker/Pulse.Checker.Return.fst +++ b/pulse/src/checker/Pulse.Checker.Return.fst @@ -185,13 +185,32 @@ let check let _, args = T.collect_app_ln f.term in if Cons? args then ( let x = fresh g in - let b = mk_binder_ppname tm_unknown res_ppname 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 = tm_unknown + mk_term (Tm_Return { expected_type ; insert_eq = false ; term = term_of_no_name_var x }) st.range in - let body = close_st_term body x in - let tt = { st with term = Tm_TotBind { binder = b; head = f.term; body } } 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)); diff --git a/pulse/src/checker/Pulse.Typing.fst b/pulse/src/checker/Pulse.Typing.fst index 813008da2bf..ba59177e4f7 100644 --- a/pulse/src/checker/Pulse.Typing.fst +++ b/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 \ No newline at end of file + | _ -> True From 89b189015e2b659ba66c73307f0023083970600e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 11 Jun 2026 14:59:04 -0700 Subject: [PATCH 4/5] cp --- pulse/lib/pulse/lib/Pulse.Lib.AVLTree.fst | 5 +++++ pulse/src/checker/Pulse.Checker.Return.fst | 10 +++++----- stage3/dune/main.ml | 4 +++- tests/bug-reports/closed/Bug4314.fst | 4 ++++ 4 files changed, 17 insertions(+), 6 deletions(-) diff --git a/pulse/lib/pulse/lib/Pulse.Lib.AVLTree.fst b/pulse/lib/pulse/lib/Pulse.Lib.AVLTree.fst index 91933dce60e..66becc17005 100644 --- a/pulse/lib/pulse/lib/Pulse.Lib.AVLTree.fst +++ b/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 diff --git a/pulse/src/checker/Pulse.Checker.Return.fst b/pulse/src/checker/Pulse.Checker.Return.fst index ee5f983df87..31113644d6f 100644 --- a/pulse/src/checker/Pulse.Checker.Return.fst +++ b/pulse/src/checker/Pulse.Checker.Return.fst @@ -178,10 +178,10 @@ let check match ctag_of_effect_annot p.effect_annot with | Some c -> c | None -> STT_Atomic in - // If we are returning an applications, 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. + // 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 @@ -192,7 +192,7 @@ let check | 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" + 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 = diff --git a/stage3/dune/main.ml b/stage3/dune/main.ml index 9d7686eff04..0310420621d 100644 --- a/stage3/dune/main.ml +++ b/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 () diff --git a/tests/bug-reports/closed/Bug4314.fst b/tests/bug-reports/closed/Bug4314.fst index 66e9472e912..1ca73eaaaeb 100644 --- a/tests/bug-reports/closed/Bug4314.fst +++ b/tests/bug-reports/closed/Bug4314.fst @@ -6,6 +6,10 @@ 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 (); } From 149a28352945900e9f048d354bef6933cd3feeba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 12 Jun 2026 06:39:51 -0700 Subject: [PATCH 5/5] Bind fix --- pulse/src/checker/Pulse.Checker.Bind.fst | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/pulse/src/checker/Pulse.Checker.Bind.fst b/pulse/src/checker/Pulse.Checker.Bind.fst index addd037dbe2..23067ef9532 100644 --- a/pulse/src/checker/Pulse.Checker.Bind.fst +++ b/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 \ No newline at end of file + ) +#pop-options