From 766f80a8f13358438fbef508ba6d29a6cd82686a Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Fri, 1 May 2026 12:01:54 -0700
Subject: [PATCH 01/13] Pulse: fix error localization for if-branch
 postcondition mismatches

The Pulse prover uses lazy continuations (cont_elab_thunk) where the
check_slprop_equiv_ext call inside prove_atom_result is deferred until
elaboration time. By then, the with_error_bound scope from the branch
checker has already exited, causing errors to be localized to the
entire if-expression rather than the offending branch.

Fix: capture the current error_range_bound when prove_atom_result is
created (while the correct bound is still active), and restore it
inside the lazy closure via RU.with_error_bound.

Also wrap each branch check in Pulse.Checker.If with
RU.with_error_bound using the branch's source range, so that errors
within a branch are bounded to that branch.

Before: error at (10,2-13,8) pointing to the whole if-expression
After:  error at (13,4-13,8) pointing to the specific branch statement

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/src/checker/Pulse.Checker.If.fst     |  5 ++++-
 pulse/src/checker/Pulse.Checker.Prover.fst | 21 +++++++++++++++------
 pulse/src/checker/Pulse.RuntimeUtils.fsti  |  1 +
 pulse/src/ml/Pulse_RuntimeUtils.ml         |  3 +++
 4 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/pulse/src/checker/Pulse.Checker.If.fst b/pulse/src/checker/Pulse.Checker.If.fst
index c1337896c91..8a559bb46df 100644
--- a/pulse/src/checker/Pulse.Checker.If.fst
+++ b/pulse/src/checker/Pulse.Checker.If.fst
@@ -24,6 +24,7 @@ open Pulse.Checker.Base
 
 module T = FStar.Tactics.V2
 module J = Pulse.JoinComp
+module RU = Pulse.RuntimeUtils
 #set-options "--z3rlimit 40"
 
 
@@ -66,6 +67,7 @@ let check
   let check_branch (eq_v:term) (br:st_term) (is_then:bool)
   : T.Tac (checker_result_t (g_with_eq eq_v) pre post_hint)
   =
+    let branch_range = br.range in
     let br =
       let t =
         mk_term (Tm_ProofHintWithBinders {
@@ -78,7 +80,8 @@ let check
     in
 
     let ppname = mk_ppname_no_range "_if_br" in
-    let r = check (g_with_eq eq_v) pre post_hint ppname br in
+    let r = RU.with_error_bound branch_range (fun () ->
+      check (g_with_eq eq_v) pre post_hint ppname br) in
     r
   in
 
diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst
index 158aac40820..6109b8bbf9e 100644
--- a/pulse/src/checker/Pulse.Checker.Prover.fst
+++ b/pulse/src/checker/Pulse.Checker.Prover.fst
@@ -927,13 +927,22 @@ let prove_atom_result (g: env)
     T.Tac (prover_result g ctxt0 [goal]) =
   let Atom _ dup _ _ = ctxt in
   let goal = elab_slprop goal in
+  let saved_bound = RU.get_error_bound () in
   (| g, (if dup then rest_ctxt@[ctxt] else rest_ctxt), [], [ctxt], fun g' ->
-    let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
-    (if dup then
-      // Check that we can indeed synthesize a duplicable instance
-      ignore (compute_term_type g
-        (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
-          [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
+    // Restore the error bound that was active when the prover matched this atom.
+    // This closure may be evaluated lazily (via cont_elab_thunk) after the
+    // original with_error_bound scope has exited.
+    let do_check () =
+      let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
+      (if dup then
+        ignore (compute_term_type g
+          (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
+            [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
+      ()
+    in
+    (match saved_bound with
+     | Some r -> RU.with_error_bound r do_check
+     | None -> do_check ());
     cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
 
 // this matches atoms when they're the only unifiable pair
diff --git a/pulse/src/checker/Pulse.RuntimeUtils.fsti b/pulse/src/checker/Pulse.RuntimeUtils.fsti
index 239fb7d3510..8fd039d1a69 100644
--- a/pulse/src/checker/Pulse.RuntimeUtils.fsti
+++ b/pulse/src/checker/Pulse.RuntimeUtils.fsti
@@ -23,6 +23,7 @@ type context = FStar.Sealed.Inhabited.sealed #(list (string & option range)) []
 val extend_context (tag:string) (r:option range) (ctx:context) : context
 val with_context (c:context) (f:unit -> T.Tac 'a) : T.Tac 'a
 val with_error_bound (r:Range.range) (f:unit -> T.Tac 'a) : T.Tac 'a
+val get_error_bound (_:unit) : T.Tac (option Range.range)
 val with_extv (k v : string) (f:unit -> T.Tac 'a) : T.Tac 'a
 val print_context (c:context) : T.Tac string
 val debug_at_level_no_module (s:string) : bool
diff --git a/pulse/src/ml/Pulse_RuntimeUtils.ml b/pulse/src/ml/Pulse_RuntimeUtils.ml
index b253121f5cf..33cea324835 100644
--- a/pulse/src/ml/Pulse_RuntimeUtils.ml
+++ b/pulse/src/ml/Pulse_RuntimeUtils.ml
@@ -22,6 +22,9 @@ let rec with_context (c:context) (f: unit -> 'a utac) : 'a utac =
 let with_error_bound (r:FStarC_Range.range) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     FStarC_Errors.with_error_bound r (fun _ -> f () ps)
+let get_error_bound () : FStarC_Range.range option utac =
+  fun _ps ->
+    FStarC_Effect.op_Bang FStarC_Errors.error_range_bound
 let with_extv (k:string) (v:string) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     let open FStarC_Options_Ext in

From 8f96b4ef32b4ff69a0a092b6bba3bf8c53aba9a7 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Fri, 1 May 2026 12:04:15 -0700
Subject: [PATCH 02/13] Add Pulse error message localization benchmark suite

16 test files in pulse/test/error_messages/ covering various error
categories: assertion failures, framing, ghost effects, if-branch
mismatches, type mismatches, subtyping, unfolding, etc.

Each file uses [@@expect_failure [code]] to verify the expected error
is produced. These serve as a regression suite for error localization.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/test/error_messages/FailAssertion.fst   | 13 +++++++++++
 pulse/test/error_messages/FramingFailure.fst  | 13 +++++++++++
 pulse/test/error_messages/GhostEffect.fst     | 23 +++++++++++++++++++
 .../test/error_messages/IfBranchMismatch.fst  | 16 +++++++++++++
 pulse/test/error_messages/IfCondType.fst      | 12 ++++++++++
 .../test/error_messages/IllTypedInvariant.fst | 17 ++++++++++++++
 pulse/test/error_messages/IllTypedSpec.fst    | 12 ++++++++++
 pulse/test/error_messages/LambdaArg.fst       | 19 +++++++++++++++
 pulse/test/error_messages/LetBindingType.fst  | 13 +++++++++++
 pulse/test/error_messages/Makefile            |  2 ++
 .../error_messages/MatchBranchMismatch.fst    | 16 +++++++++++++
 pulse/test/error_messages/MultiError.fst      | 14 +++++++++++
 pulse/test/error_messages/NestedCall.fst      | 19 +++++++++++++++
 pulse/test/error_messages/PrePostMismatch.fst | 12 ++++++++++
 .../error_messages/ReturnTypeMismatch.fst     | 13 +++++++++++
 pulse/test/error_messages/SequenceError.fst   | 14 +++++++++++
 .../test/error_messages/SubtypingFailure.fst  | 19 +++++++++++++++
 pulse/test/error_messages/UnfoldFailure.fst   | 14 +++++++++++
 18 files changed, 261 insertions(+)
 create mode 100644 pulse/test/error_messages/FailAssertion.fst
 create mode 100644 pulse/test/error_messages/FramingFailure.fst
 create mode 100644 pulse/test/error_messages/GhostEffect.fst
 create mode 100644 pulse/test/error_messages/IfBranchMismatch.fst
 create mode 100644 pulse/test/error_messages/IfCondType.fst
 create mode 100644 pulse/test/error_messages/IllTypedInvariant.fst
 create mode 100644 pulse/test/error_messages/IllTypedSpec.fst
 create mode 100644 pulse/test/error_messages/LambdaArg.fst
 create mode 100644 pulse/test/error_messages/LetBindingType.fst
 create mode 100644 pulse/test/error_messages/Makefile
 create mode 100644 pulse/test/error_messages/MatchBranchMismatch.fst
 create mode 100644 pulse/test/error_messages/MultiError.fst
 create mode 100644 pulse/test/error_messages/NestedCall.fst
 create mode 100644 pulse/test/error_messages/PrePostMismatch.fst
 create mode 100644 pulse/test/error_messages/ReturnTypeMismatch.fst
 create mode 100644 pulse/test/error_messages/SequenceError.fst
 create mode 100644 pulse/test/error_messages/SubtypingFailure.fst
 create mode 100644 pulse/test/error_messages/UnfoldFailure.fst

diff --git a/pulse/test/error_messages/FailAssertion.fst b/pulse/test/error_messages/FailAssertion.fst
new file mode 100644
index 00000000000..8e2b99667d4
--- /dev/null
+++ b/pulse/test/error_messages/FailAssertion.fst
@@ -0,0 +1,13 @@
+module FailAssertion
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Failing assertion: error should point to the assert line
+[@@expect_failure [228]]
+fn test_fail_assert (x: int)
+  requires emp
+  ensures emp
+{
+  assert (x > 0);
+  ()
+}
diff --git a/pulse/test/error_messages/FramingFailure.fst b/pulse/test/error_messages/FramingFailure.fst
new file mode 100644
index 00000000000..a41ed88c4ed
--- /dev/null
+++ b/pulse/test/error_messages/FramingFailure.fst
@@ -0,0 +1,13 @@
+module FramingFailure
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Framing failure: trying to use a resource that isn't in scope
+[@@expect_failure [228]]
+fn framing_fail (r1 r2: ref int)
+  requires pts_to r1 0
+  ensures pts_to r1 1
+{
+  let v = !r2;
+  r1 := 1
+}
diff --git a/pulse/test/error_messages/GhostEffect.fst b/pulse/test/error_messages/GhostEffect.fst
new file mode 100644
index 00000000000..ab6c7dd1c7d
--- /dev/null
+++ b/pulse/test/error_messages/GhostEffect.fst
@@ -0,0 +1,23 @@
+module GhostEffect
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Using a ghost value in a total computation
+ghost
+fn ghost_fn ()
+  requires emp
+  returns r: int
+  ensures emp
+{
+  42
+}
+
+[@@expect_failure [228]]
+fn non_ghost_caller ()
+  requires emp
+  returns r: int
+  ensures emp
+{
+  let x = ghost_fn ();  // ERROR: ghost in non-ghost context
+  x
+}
diff --git a/pulse/test/error_messages/IfBranchMismatch.fst b/pulse/test/error_messages/IfBranchMismatch.fst
new file mode 100644
index 00000000000..7cfbe86c98b
--- /dev/null
+++ b/pulse/test/error_messages/IfBranchMismatch.fst
@@ -0,0 +1,16 @@
+module IfBranchMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// If branches produce different resources
+[@@expect_failure [19]]
+fn if_branch_mismatch (r: ref int) (b: bool)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  if b {
+    r := 1
+  } else {
+    r := 2  // ERROR: this branch gives pts_to r 2, should be 1
+  }
+}
diff --git a/pulse/test/error_messages/IfCondType.fst b/pulse/test/error_messages/IfCondType.fst
new file mode 100644
index 00000000000..3808d2b0c03
--- /dev/null
+++ b/pulse/test/error_messages/IfCondType.fst
@@ -0,0 +1,12 @@
+module IfCondType
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// If condition that's not a bool
+[@@expect_failure [189]]
+fn bad_if_cond (x: int)
+  requires emp
+  ensures emp
+{
+  if x { () } else { () }
+}
diff --git a/pulse/test/error_messages/IllTypedInvariant.fst b/pulse/test/error_messages/IllTypedInvariant.fst
new file mode 100644
index 00000000000..e8d6ad66d24
--- /dev/null
+++ b/pulse/test/error_messages/IllTypedInvariant.fst
@@ -0,0 +1,17 @@
+module IllTypedInvariant
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// While loop with invariant that can't be established initially
+[@@expect_failure [19]]
+fn bad_invariant ()
+  requires emp
+  ensures emp
+{
+  let mut i = 0;
+  while (!i < 10)
+  invariant pure (!i >= 0 /\ !i <= 10 /\ 1 = 2)
+  {
+    i := !i + 1;
+  }
+}
diff --git a/pulse/test/error_messages/IllTypedSpec.fst b/pulse/test/error_messages/IllTypedSpec.fst
new file mode 100644
index 00000000000..8e7343695a7
--- /dev/null
+++ b/pulse/test/error_messages/IllTypedSpec.fst
@@ -0,0 +1,12 @@
+module IllTypedSpec
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Ill-typed precondition: using an int where a vprop is expected
+[@@expect_failure [189]]
+fn bad_precondition (x: int)
+  requires x
+  ensures emp
+{
+  ()
+}
diff --git a/pulse/test/error_messages/LambdaArg.fst b/pulse/test/error_messages/LambdaArg.fst
new file mode 100644
index 00000000000..48f7900321e
--- /dev/null
+++ b/pulse/test/error_messages/LambdaArg.fst
@@ -0,0 +1,19 @@
+module LambdaArg
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Passing wrong number of arguments
+fn takes_two (x y: int)
+  requires emp
+  ensures emp
+{
+  ()
+}
+
+[@@expect_failure [71]]
+fn wrong_args ()
+  requires emp
+  ensures emp
+{
+  takes_two 1 2 3  // ERROR: too many arguments
+}
diff --git a/pulse/test/error_messages/LetBindingType.fst b/pulse/test/error_messages/LetBindingType.fst
new file mode 100644
index 00000000000..38b15cbae16
--- /dev/null
+++ b/pulse/test/error_messages/LetBindingType.fst
@@ -0,0 +1,13 @@
+module LetBindingType
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Let binding with wrong type annotation
+[@@expect_failure [189]]
+fn let_binding_type ()
+  requires emp
+  ensures emp
+{
+  let x : bool = 42;
+  ()
+}
diff --git a/pulse/test/error_messages/Makefile b/pulse/test/error_messages/Makefile
new file mode 100644
index 00000000000..49e47b7c411
--- /dev/null
+++ b/pulse/test/error_messages/Makefile
@@ -0,0 +1,2 @@
+PULSE_ROOT ?= ../..
+include $(PULSE_ROOT)/mk/test.mk
diff --git a/pulse/test/error_messages/MatchBranchMismatch.fst b/pulse/test/error_messages/MatchBranchMismatch.fst
new file mode 100644
index 00000000000..f2ad66f6a4e
--- /dev/null
+++ b/pulse/test/error_messages/MatchBranchMismatch.fst
@@ -0,0 +1,16 @@
+module MatchBranchMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Match branch postcondition mismatch - error should point to offending branch
+[@@expect_failure [19]]
+fn match_error (r: ref int) (x: int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  match x {
+    0 -> { r := 1 }
+    1 -> { r := 2 }
+    _ -> { r := 1 }
+  }
+}
diff --git a/pulse/test/error_messages/MultiError.fst b/pulse/test/error_messages/MultiError.fst
new file mode 100644
index 00000000000..5414347ec31
--- /dev/null
+++ b/pulse/test/error_messages/MultiError.fst
@@ -0,0 +1,14 @@
+module MultiError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Multiple errors in sequence - check that each one is localized correctly
+[@@expect_failure [19]]
+fn multi_error (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 100
+{
+  r := 1;
+  assert (pure (1 = 2));   // first error here
+  r := 100
+}
diff --git a/pulse/test/error_messages/NestedCall.fst b/pulse/test/error_messages/NestedCall.fst
new file mode 100644
index 00000000000..74b3dec9fd8
--- /dev/null
+++ b/pulse/test/error_messages/NestedCall.fst
@@ -0,0 +1,19 @@
+module NestedCall
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error in nested call should point to the specific call site
+fn inner (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 1
+}
+
+[@@expect_failure [19]]
+fn outer (r: ref int)
+  requires pts_to r 5
+  ensures pts_to r 1
+{
+  inner r  // ERROR: precondition mismatch (pts_to r 5 vs pts_to r 0)
+}
diff --git a/pulse/test/error_messages/PrePostMismatch.fst b/pulse/test/error_messages/PrePostMismatch.fst
new file mode 100644
index 00000000000..f458c41bbec
--- /dev/null
+++ b/pulse/test/error_messages/PrePostMismatch.fst
@@ -0,0 +1,12 @@
+module PrePostMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Post-condition doesn't match what the body establishes
+[@@expect_failure [19]]
+fn pre_post_mismatch (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 42
+{
+  r := 1
+}
diff --git a/pulse/test/error_messages/ReturnTypeMismatch.fst b/pulse/test/error_messages/ReturnTypeMismatch.fst
new file mode 100644
index 00000000000..fbb48c56adf
--- /dev/null
+++ b/pulse/test/error_messages/ReturnTypeMismatch.fst
@@ -0,0 +1,13 @@
+module ReturnTypeMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Returning wrong type
+[@@expect_failure [189]]
+fn return_wrong_type (x: int)
+  requires emp
+  returns r: bool
+  ensures emp
+{
+  x
+}
diff --git a/pulse/test/error_messages/SequenceError.fst b/pulse/test/error_messages/SequenceError.fst
new file mode 100644
index 00000000000..f98cc98843b
--- /dev/null
+++ b/pulse/test/error_messages/SequenceError.fst
@@ -0,0 +1,14 @@
+module SequenceError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error after a sequence of operations - check where error is reported
+[@@expect_failure [19]]
+fn seq_error (r1 r2: ref int)
+  requires pts_to r1 0 ** pts_to r2 0
+  ensures pts_to r1 1 ** pts_to r2 1
+{
+  r1 := 1;
+  r2 := 2;  // ERROR: should point here, post expects pts_to r2 1
+  ()
+}
diff --git a/pulse/test/error_messages/SubtypingFailure.fst b/pulse/test/error_messages/SubtypingFailure.fst
new file mode 100644
index 00000000000..ccb3993446c
--- /dev/null
+++ b/pulse/test/error_messages/SubtypingFailure.fst
@@ -0,0 +1,19 @@
+module SubtypingFailure
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Subtyping failure in function argument
+fn callee (x: nat)
+  requires emp
+  ensures emp
+{
+  ()
+}
+
+[@@expect_failure [19]]
+fn caller (x: int)
+  requires emp
+  ensures emp
+{
+  callee x
+}
diff --git a/pulse/test/error_messages/UnfoldFailure.fst b/pulse/test/error_messages/UnfoldFailure.fst
new file mode 100644
index 00000000000..814be962464
--- /dev/null
+++ b/pulse/test/error_messages/UnfoldFailure.fst
@@ -0,0 +1,14 @@
+module UnfoldFailure
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Failure when trying to match a predicate that can't be unfolded
+let my_pred (r: ref int) : slprop = pts_to r 0
+
+[@@expect_failure [228]]
+fn unfold_fail (r: ref int)
+  requires my_pred r
+  ensures pts_to r 1
+{
+  r := 1  // ERROR: can't write to r without unfolding my_pred first
+}

From 3cedfb6603b045cf8dbd88cc9292c959070008a1 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Fri, 1 May 2026 17:51:39 -0700
Subject: [PATCH 03/13] Pulse parser: fix error range for
 assert/fold/unfold/rewrite statements

When assert, fold, unfold, assume, or rewrite statements appear as the
first statement in a function body (after '{'), the Menhir parser was
producing ranges that started at the '{' character rather than at the
keyword.

Root cause: withBindersOpt could derive epsilon, causing Menhir's
$startpos to inherit $endpos of the preceding token (LBRACE). This
propagated through pulseStmtNonempty -> pulseStmtNoSeq -> pulseStmt and
into the statement's range.

Fix: Split each 'bs=withBindersOpt KEYWORD ...' alternative into two:
one starting directly with the keyword (no binders), and one with
explicit 'bs=withBinders KEYWORD ...' (which starts with WITH, a real
token). Remove the now-unused withBindersOpt non-terminal.

Before: assert errors at (10,1-11,16) including the '{' line
After:  assert errors at (11,2-11,16) pinpointing the assert

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/src/ml/pulseparser.mly | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/pulse/src/ml/pulseparser.mly b/pulse/src/ml/pulseparser.mly
index 6cdae9f260e..39c5ccae6b3 100644
--- a/pulse/src/ml/pulseparser.mly
+++ b/pulse/src/ml/pulseparser.mly
@@ -264,17 +264,25 @@ pulseStmtNoSeq:
     { PulseSyntaxExtension_Sugar.mk_while tm inv body }
   | INTRO p=pulseSLProp WITH ws=nonempty_list(indexingTerm)
     { PulseSyntaxExtension_Sugar.mk_intro p ws }
-  | bs=withBindersOpt REWRITE body=rewriteBody
-    {
-        PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body bs
-    }
-  | bs=withBindersOpt ASSERT p=pulseSLProp
+  | REWRITE body=rewriteBody
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body [] }
+  | bs=withBinders REWRITE body=rewriteBody
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body bs }
+  | ASSERT p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSERT p) [] }
+  | bs=withBinders ASSERT p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSERT p) bs }
-  | bs=withBindersOpt ASSUME p=pulseSLProp
+  | ASSUME p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSUME p) [] }
+  | bs=withBinders ASSUME p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSUME p) bs }
-  | bs=withBindersOpt UNFOLD ns=optionalNames p=pulseSLProp
+  | UNFOLD ns=optionalNames p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (UNFOLD (ns,p)) [] }
+  | bs=withBinders UNFOLD ns=optionalNames p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (UNFOLD (ns,p)) bs }
-  | bs=withBindersOpt FOLD ns=optionalNames p=pulseSLProp
+  | FOLD ns=optionalNames p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (FOLD (ns,p)) [] }
+  | bs=withBinders FOLD ns=optionalNames p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (FOLD (ns,p)) bs }
   | bs=withBinders UNDERSCORE
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders WILD bs }
@@ -346,11 +354,6 @@ withBinders:
   | WITH bs=nonempty_list(multiBinder) DOT
     { List.flatten bs }
 
-withBindersOpt:
-  | w=withBinders
-    { w }
-  | { [] }
-
 ensuresSLProp:
   | ret=option(RETURNS i=lidentOrUnderscore COLON r=term { (i, r) }) ENSURES s=pulseSLProp maybe_opens=option(OPENS inv=appTermNoRecordExp { inv })
     { ret, s, maybe_opens }

From 90be5f0e5161efb4401b9917c87a898a63c42867 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Fri, 1 May 2026 17:51:56 -0700
Subject: [PATCH 04/13] Expand Pulse error message localization benchmark to 35
 tests

Add comprehensive regression test suite for Pulse error localization.
Each test file triggers a specific error category and pins down the
exact error range via .fst.output.expected files.

Test categories covered (35 tests):
- Assertion failures (assert, fold, unfold, rewrite, nested block)
- Type mismatches (if condition, let binding, return, spec, with-local)
- Framing/resource errors (leftover, duplicate, missing post, mutual excl)
- Branch mismatches (if, match)
- Effect errors (ghost in non-ghost context)
- Prover failures (exists intro, invariant payload, subtyping)
- Scope/binding errors (open nonexistent, arity mismatch)
- Loop errors (while invariant preservation)
- Sequence/bind errors (postcondition at continuation)
- Closure/local function errors (pre-condition mismatch at call site)
- Multiple errors in single function

The Makefile uses diff-based comparison (same approach as
FStar/tests/error-messages) with:
- --print_expected_failures for clean output
- --ext fstar:no_absolute_paths for reproducibility
- Warning suppression for non-localization noise
- Integrated into pulse/test as a SUBDIRS entry

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/test/Makefile                           |  1 +
 .../error_messages/AssertExtraContext.fst     | 13 ++++++++++++
 .../AssertExtraContext.fst.output.expected    |  7 +++++++
 pulse/test/error_messages/AtomicMismatch.fst  | 13 ++++++++++++
 .../AtomicMismatch.fst.output.expected        |  7 +++++++
 .../test/error_messages/BindTypeMismatch.fst  | 21 +++++++++++++++++++
 .../BindTypeMismatch.fst.output.expected      |  7 +++++++
 pulse/test/error_messages/ClosureError.fst    | 19 +++++++++++++++++
 .../ClosureError.fst.output.expected          | 10 +++++++++
 .../test/error_messages/DuplicateResource.fst | 12 +++++++++++
 .../DuplicateResource.fst.output.expected     |  8 +++++++
 pulse/test/error_messages/ExistsIntro.fst     | 13 ++++++++++++
 .../ExistsIntro.fst.output.expected           |  7 +++++++
 .../FailAssertion.fst.output.expected         |  8 +++++++
 pulse/test/error_messages/FoldError.fst       | 14 +++++++++++++
 .../FoldError.fst.output.expected             |  7 +++++++
 .../FramingFailure.fst.output.expected        |  8 +++++++
 .../GhostEffect.fst.output.expected           |  7 +++++++
 .../IfBranchMismatch.fst.output.expected      | 10 +++++++++
 .../IfCondType.fst.output.expected            |  4 ++++
 .../IllTypedInvariant.fst.output.expected     |  7 +++++++
 .../IllTypedSpec.fst.output.expected          |  7 +++++++
 pulse/test/error_messages/IntroExistsFail.fst | 12 +++++++++++
 .../IntroExistsFail.fst.output.expected       |  7 +++++++
 .../test/error_messages/InvariantPayload.fst  | 14 +++++++++++++
 .../InvariantPayload.fst.output.expected      |  7 +++++++
 .../LambdaArg.fst.output.expected             |  8 +++++++
 .../test/error_messages/LeftoverResources.fst | 12 +++++++++++
 .../LeftoverResources.fst.output.expected     |  6 ++++++
 .../LetBindingType.fst.output.expected        |  4 ++++
 pulse/test/error_messages/Makefile            | 13 ++++++++++++
 .../MatchBranchMismatch.fst.output.expected   | 10 +++++++++
 pulse/test/error_messages/MissingPost.fst     | 13 ++++++++++++
 .../MissingPost.fst.output.expected           |  6 ++++++
 .../MultiError.fst.output.expected            |  7 +++++++
 pulse/test/error_messages/MutualExcl.fst      | 12 +++++++++++
 .../MutualExcl.fst.output.expected            |  6 ++++++
 pulse/test/error_messages/NestedBlock.fst     | 15 +++++++++++++
 .../NestedBlock.fst.output.expected           |  9 ++++++++
 .../NestedCall.fst.output.expected            |  9 ++++++++
 pulse/test/error_messages/OpenScopeError.fst  | 13 ++++++++++++
 .../OpenScopeError.fst.output.expected        |  6 ++++++
 .../PrePostMismatch.fst.output.expected       | 10 +++++++++
 pulse/test/error_messages/ReturnImplicit.fst  | 13 ++++++++++++
 .../ReturnImplicit.fst.output.expected        |  9 ++++++++
 .../ReturnTypeMismatch.fst.output.expected    |  4 ++++
 pulse/test/error_messages/RewriteFail.fst     | 13 ++++++++++++
 .../RewriteFail.fst.output.expected           |  9 ++++++++
 .../SequenceError.fst.output.expected         |  9 ++++++++
 .../SubtypingFailure.fst.output.expected      | 12 +++++++++++
 .../UnfoldFailure.fst.output.expected         |  8 +++++++
 .../error_messages/WhileInvPreservation.fst   | 17 +++++++++++++++
 .../WhileInvPreservation.fst.output.expected  | 10 +++++++++
 pulse/test/error_messages/WithLocalError.fst  | 14 +++++++++++++
 .../WithLocalError.fst.output.expected        |  7 +++++++
 55 files changed, 534 insertions(+)
 create mode 100644 pulse/test/error_messages/AssertExtraContext.fst
 create mode 100644 pulse/test/error_messages/AssertExtraContext.fst.output.expected
 create mode 100644 pulse/test/error_messages/AtomicMismatch.fst
 create mode 100644 pulse/test/error_messages/AtomicMismatch.fst.output.expected
 create mode 100644 pulse/test/error_messages/BindTypeMismatch.fst
 create mode 100644 pulse/test/error_messages/BindTypeMismatch.fst.output.expected
 create mode 100644 pulse/test/error_messages/ClosureError.fst
 create mode 100644 pulse/test/error_messages/ClosureError.fst.output.expected
 create mode 100644 pulse/test/error_messages/DuplicateResource.fst
 create mode 100644 pulse/test/error_messages/DuplicateResource.fst.output.expected
 create mode 100644 pulse/test/error_messages/ExistsIntro.fst
 create mode 100644 pulse/test/error_messages/ExistsIntro.fst.output.expected
 create mode 100644 pulse/test/error_messages/FailAssertion.fst.output.expected
 create mode 100644 pulse/test/error_messages/FoldError.fst
 create mode 100644 pulse/test/error_messages/FoldError.fst.output.expected
 create mode 100644 pulse/test/error_messages/FramingFailure.fst.output.expected
 create mode 100644 pulse/test/error_messages/GhostEffect.fst.output.expected
 create mode 100644 pulse/test/error_messages/IfBranchMismatch.fst.output.expected
 create mode 100644 pulse/test/error_messages/IfCondType.fst.output.expected
 create mode 100644 pulse/test/error_messages/IllTypedInvariant.fst.output.expected
 create mode 100644 pulse/test/error_messages/IllTypedSpec.fst.output.expected
 create mode 100644 pulse/test/error_messages/IntroExistsFail.fst
 create mode 100644 pulse/test/error_messages/IntroExistsFail.fst.output.expected
 create mode 100644 pulse/test/error_messages/InvariantPayload.fst
 create mode 100644 pulse/test/error_messages/InvariantPayload.fst.output.expected
 create mode 100644 pulse/test/error_messages/LambdaArg.fst.output.expected
 create mode 100644 pulse/test/error_messages/LeftoverResources.fst
 create mode 100644 pulse/test/error_messages/LeftoverResources.fst.output.expected
 create mode 100644 pulse/test/error_messages/LetBindingType.fst.output.expected
 create mode 100644 pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
 create mode 100644 pulse/test/error_messages/MissingPost.fst
 create mode 100644 pulse/test/error_messages/MissingPost.fst.output.expected
 create mode 100644 pulse/test/error_messages/MultiError.fst.output.expected
 create mode 100644 pulse/test/error_messages/MutualExcl.fst
 create mode 100644 pulse/test/error_messages/MutualExcl.fst.output.expected
 create mode 100644 pulse/test/error_messages/NestedBlock.fst
 create mode 100644 pulse/test/error_messages/NestedBlock.fst.output.expected
 create mode 100644 pulse/test/error_messages/NestedCall.fst.output.expected
 create mode 100644 pulse/test/error_messages/OpenScopeError.fst
 create mode 100644 pulse/test/error_messages/OpenScopeError.fst.output.expected
 create mode 100644 pulse/test/error_messages/PrePostMismatch.fst.output.expected
 create mode 100644 pulse/test/error_messages/ReturnImplicit.fst
 create mode 100644 pulse/test/error_messages/ReturnImplicit.fst.output.expected
 create mode 100644 pulse/test/error_messages/ReturnTypeMismatch.fst.output.expected
 create mode 100644 pulse/test/error_messages/RewriteFail.fst
 create mode 100644 pulse/test/error_messages/RewriteFail.fst.output.expected
 create mode 100644 pulse/test/error_messages/SequenceError.fst.output.expected
 create mode 100644 pulse/test/error_messages/SubtypingFailure.fst.output.expected
 create mode 100644 pulse/test/error_messages/UnfoldFailure.fst.output.expected
 create mode 100644 pulse/test/error_messages/WhileInvPreservation.fst
 create mode 100644 pulse/test/error_messages/WhileInvPreservation.fst.output.expected
 create mode 100644 pulse/test/error_messages/WithLocalError.fst
 create mode 100644 pulse/test/error_messages/WithLocalError.fst.output.expected

diff --git a/pulse/test/Makefile b/pulse/test/Makefile
index 75801ab213c..7e94564022d 100644
--- a/pulse/test/Makefile
+++ b/pulse/test/Makefile
@@ -1,4 +1,5 @@
 SUBDIRS += bug-reports
+SUBDIRS += error_messages
 SUBDIRS += nolib
 SUBDIRS += pool
 
diff --git a/pulse/test/error_messages/AssertExtraContext.fst b/pulse/test/error_messages/AssertExtraContext.fst
new file mode 100644
index 00000000000..9f465bc8345
--- /dev/null
+++ b/pulse/test/error_messages/AssertExtraContext.fst
@@ -0,0 +1,13 @@
+module AssertExtraContext
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Assert with binders where the witness is wrong
+[@@expect_failure [19]]
+fn assert_extra (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0
+{
+  with v. assert (pts_to r v ** pure (v > 0));
+  ()
+}
diff --git a/pulse/test/error_messages/AssertExtraContext.fst.output.expected b/pulse/test/error_messages/AssertExtraContext.fst.output.expected
new file mode 100644
index 00000000000..dcf086c5ed4
--- /dev/null
+++ b/pulse/test/error_messages/AssertExtraContext.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at AssertExtraContext.fst(11,7-11,43):
+  - Expected failure:
+  - Failed to prove pure property: 0 > 0
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/AtomicMismatch.fst b/pulse/test/error_messages/AtomicMismatch.fst
new file mode 100644
index 00000000000..435848b0455
--- /dev/null
+++ b/pulse/test/error_messages/AtomicMismatch.fst
@@ -0,0 +1,13 @@
+module AtomicMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Using non-atomic operation in atomic context
+[@@expect_failure [228]]
+atomic
+fn atomic_fn (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 1  // Might error if := is not atomic-compatible
+}
diff --git a/pulse/test/error_messages/AtomicMismatch.fst.output.expected b/pulse/test/error_messages/AtomicMismatch.fst.output.expected
new file mode 100644
index 00000000000..5f74508d7a5
--- /dev/null
+++ b/pulse/test/error_messages/AtomicMismatch.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at AtomicMismatch.fst(12,2-12,8):
+  - Expected failure:
+  - Tactic failed
+  - Cannot compose computations in this atomic block:
+  - This computation has effect: stt
+  - The continuation has effect: stt_atomic emp_inames
+
diff --git a/pulse/test/error_messages/BindTypeMismatch.fst b/pulse/test/error_messages/BindTypeMismatch.fst
new file mode 100644
index 00000000000..2f4db729d11
--- /dev/null
+++ b/pulse/test/error_messages/BindTypeMismatch.fst
@@ -0,0 +1,21 @@
+module BindTypeMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Binding with wrong type annotation
+fn helper ()
+  requires emp
+  returns r: int
+  ensures emp
+{
+  42
+}
+
+[@@expect_failure [228]]
+fn bind_type_err ()
+  requires emp
+  ensures emp
+{
+  let x : bool = helper ();  // ERROR: helper returns int, binding expects bool
+  ()
+}
diff --git a/pulse/test/error_messages/BindTypeMismatch.fst.output.expected b/pulse/test/error_messages/BindTypeMismatch.fst.output.expected
new file mode 100644
index 00000000000..53c3982e064
--- /dev/null
+++ b/pulse/test/error_messages/BindTypeMismatch.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at BindTypeMismatch.fst(19,17-19,26):
+  - Expected failure:
+  - Tactic failed
+  - Type mismatch (NB: this is a syntactic check)
+  - Expected: bool
+  - Got: int
+
diff --git a/pulse/test/error_messages/ClosureError.fst b/pulse/test/error_messages/ClosureError.fst
new file mode 100644
index 00000000000..2d9e0515a2f
--- /dev/null
+++ b/pulse/test/error_messages/ClosureError.fst
@@ -0,0 +1,19 @@
+module ClosureError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error in a local function definition
+[@@expect_failure [19]]
+fn closure_error (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0
+{
+  fn helper ()
+    requires pts_to r 1  // ERROR: pre says r==1 but caller has r==0
+    ensures pts_to r 1
+  {
+    ()
+  };
+  helper ();
+  ()
+}
diff --git a/pulse/test/error_messages/ClosureError.fst.output.expected b/pulse/test/error_messages/ClosureError.fst.output.expected
new file mode 100644
index 00000000000..90ab338b9d5
--- /dev/null
+++ b/pulse/test/error_messages/ClosureError.fst.output.expected
@@ -0,0 +1,10 @@
+* Info at ClosureError.fst(17,2-17,8):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 0
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - See also ClosureError.fst(17,2-18,4)
+
diff --git a/pulse/test/error_messages/DuplicateResource.fst b/pulse/test/error_messages/DuplicateResource.fst
new file mode 100644
index 00000000000..2786df4f07e
--- /dev/null
+++ b/pulse/test/error_messages/DuplicateResource.fst
@@ -0,0 +1,12 @@
+module DuplicateResource
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Trying to read a ref twice without proper framing
+[@@expect_failure [228]]
+fn dup_fail (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0 ** pts_to r 0
+{
+  ()
+}
diff --git a/pulse/test/error_messages/DuplicateResource.fst.output.expected b/pulse/test/error_messages/DuplicateResource.fst.output.expected
new file mode 100644
index 00000000000..dcd948ca3c4
--- /dev/null
+++ b/pulse/test/error_messages/DuplicateResource.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at DuplicateResource.fst(11,2-11,4):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      Pulse.Lib.Reference.pts_to r 0
+  - In the context:
+
+
diff --git a/pulse/test/error_messages/ExistsIntro.fst b/pulse/test/error_messages/ExistsIntro.fst
new file mode 100644
index 00000000000..0312943156a
--- /dev/null
+++ b/pulse/test/error_messages/ExistsIntro.fst
@@ -0,0 +1,13 @@
+module ExistsIntro
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Postcondition requires existential that can't be satisfied
+[@@expect_failure [19]]
+fn exists_intro_fail (r: ref int)
+  requires pts_to r 5
+  ensures exists* v. pts_to r v ** pure (v > 10)
+{
+  // ERROR: after body, we have pts_to r 5 but need v > 10
+  ()
+}
diff --git a/pulse/test/error_messages/ExistsIntro.fst.output.expected b/pulse/test/error_messages/ExistsIntro.fst.output.expected
new file mode 100644
index 00000000000..f41d1e7ee25
--- /dev/null
+++ b/pulse/test/error_messages/ExistsIntro.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at ExistsIntro.fst(12,2-12,4):
+  - Expected failure:
+  - Failed to prove pure property: 5 > 10
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/FailAssertion.fst.output.expected b/pulse/test/error_messages/FailAssertion.fst.output.expected
new file mode 100644
index 00000000000..94eba16a291
--- /dev/null
+++ b/pulse/test/error_messages/FailAssertion.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at FailAssertion.fst(11,2-11,16):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      x > 0
+  - In the context:
+
+
diff --git a/pulse/test/error_messages/FoldError.fst b/pulse/test/error_messages/FoldError.fst
new file mode 100644
index 00000000000..813bd09809b
--- /dev/null
+++ b/pulse/test/error_messages/FoldError.fst
@@ -0,0 +1,14 @@
+module FoldError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+let my_inv (r: ref int) (v: int) : slprop = pts_to r v ** pure (v >= 0)
+
+// Trying to fold with mismatched context
+[@@expect_failure [19]]
+fn fold_fail (r: ref int)
+  requires pts_to r (-1)
+  ensures my_inv r (-1)
+{
+  fold (my_inv r (-1))  // ERROR: pure (v >= 0) not satisfiable with v = -1
+}
diff --git a/pulse/test/error_messages/FoldError.fst.output.expected b/pulse/test/error_messages/FoldError.fst.output.expected
new file mode 100644
index 00000000000..8abdbc4f321
--- /dev/null
+++ b/pulse/test/error_messages/FoldError.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at FoldError.fst(13,2-13,22):
+  - Expected failure:
+  - Failed to prove pure property: false
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/FramingFailure.fst.output.expected b/pulse/test/error_messages/FramingFailure.fst.output.expected
new file mode 100644
index 00000000000..1b5ec8f2002
--- /dev/null
+++ b/pulse/test/error_messages/FramingFailure.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at FramingFailure.fst(11,10-11,13):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      Pulse.Lib.Reference.pts_to r2 (*?u298*)_
+  - In the context:
+      Pulse.Lib.Reference.pts_to r1 0
+
diff --git a/pulse/test/error_messages/GhostEffect.fst.output.expected b/pulse/test/error_messages/GhostEffect.fst.output.expected
new file mode 100644
index 00000000000..0e72edd1110
--- /dev/null
+++ b/pulse/test/error_messages/GhostEffect.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at GhostEffect.fst(21,10-21,18):
+  - Expected failure:
+  - Tactic failed
+  - Expected a term with a non-informative (e.g., erased) type.
+  - Got: int
+  - See also GhostEffect.fst(20,1-22,3)
+
diff --git a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
new file mode 100644
index 00000000000..ed0e740d1ef
--- /dev/null
+++ b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
@@ -0,0 +1,10 @@
+* Info at IfBranchMismatch.fst(14,4-14,8):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - See also IfBranchMismatch.fst(14,4-14,10)
+
diff --git a/pulse/test/error_messages/IfCondType.fst.output.expected b/pulse/test/error_messages/IfCondType.fst.output.expected
new file mode 100644
index 00000000000..f23551408e3
--- /dev/null
+++ b/pulse/test/error_messages/IfCondType.fst.output.expected
@@ -0,0 +1,4 @@
+* Info at IfCondType.fst(11,5-11,6):
+  - Expected failure:
+  - Expected expression of type Prims.bool got expression x of type Prims.int
+
diff --git a/pulse/test/error_messages/IllTypedInvariant.fst.output.expected b/pulse/test/error_messages/IllTypedInvariant.fst.output.expected
new file mode 100644
index 00000000000..b46eac74f7f
--- /dev/null
+++ b/pulse/test/error_messages/IllTypedInvariant.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at IllTypedInvariant.fst(13,43-13,44):
+  - Expected failure:
+  - Failed to prove pure property: true /\ true /\ false
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/IllTypedSpec.fst.output.expected b/pulse/test/error_messages/IllTypedSpec.fst.output.expected
new file mode 100644
index 00000000000..7ef194bf604
--- /dev/null
+++ b/pulse/test/error_messages/IllTypedSpec.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at IllTypedSpec.fst(8,11-8,12):
+  - Expected failure:
+  - Ill-typed term: x
+  - Expected expression of type Pulse.Lib.Core.slprop
+    got expression x
+    of type Prims.int
+
diff --git a/pulse/test/error_messages/IntroExistsFail.fst b/pulse/test/error_messages/IntroExistsFail.fst
new file mode 100644
index 00000000000..ec666d16d6a
--- /dev/null
+++ b/pulse/test/error_messages/IntroExistsFail.fst
@@ -0,0 +1,12 @@
+module IntroExistsFail
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Existential introduction with wrong witness
+[@@expect_failure [19]]
+fn intro_exists_fail (r: ref int)
+  requires pts_to r 0
+  ensures (exists* v. pts_to r v ** pure (v > 0))
+{
+  ()  // ERROR: can't prove exists* v. pts_to r v ** pure (v > 0)
+}
diff --git a/pulse/test/error_messages/IntroExistsFail.fst.output.expected b/pulse/test/error_messages/IntroExistsFail.fst.output.expected
new file mode 100644
index 00000000000..6e4865a5a6b
--- /dev/null
+++ b/pulse/test/error_messages/IntroExistsFail.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at IntroExistsFail.fst(11,2-11,4):
+  - Expected failure:
+  - Failed to prove pure property: 0 > 0
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/InvariantPayload.fst b/pulse/test/error_messages/InvariantPayload.fst
new file mode 100644
index 00000000000..3bddac15f13
--- /dev/null
+++ b/pulse/test/error_messages/InvariantPayload.fst
@@ -0,0 +1,14 @@
+module InvariantPayload
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Fold/unfold invariant with wrong payload
+let my_pred (r: ref int) : slprop = exists* v. pts_to r v ** pure (v > 0)
+
+[@@expect_failure [19]]
+fn inv_payload_fail (r: ref int)
+  requires pts_to r 0
+  ensures my_pred r
+{
+  fold my_pred r  // ERROR: can't prove v > 0 with v = 0
+}
diff --git a/pulse/test/error_messages/InvariantPayload.fst.output.expected b/pulse/test/error_messages/InvariantPayload.fst.output.expected
new file mode 100644
index 00000000000..be66a624138
--- /dev/null
+++ b/pulse/test/error_messages/InvariantPayload.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at InvariantPayload.fst(13,2-13,16):
+  - Expected failure:
+  - Failed to prove pure property: 0 > 0
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/LambdaArg.fst.output.expected b/pulse/test/error_messages/LambdaArg.fst.output.expected
new file mode 100644
index 00000000000..ffe4693798d
--- /dev/null
+++ b/pulse/test/error_messages/LambdaArg.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at LambdaArg.fst(18,2-18,11):
+  - Expected failure:
+  - Expected a function.
+  - Got an expression of type:
+      fn
+        requires Pulse.Lib.Core.emp
+        ensures Pulse.Lib.Core.emp
+
diff --git a/pulse/test/error_messages/LeftoverResources.fst b/pulse/test/error_messages/LeftoverResources.fst
new file mode 100644
index 00000000000..f0dcb78a8ff
--- /dev/null
+++ b/pulse/test/error_messages/LeftoverResources.fst
@@ -0,0 +1,12 @@
+module LeftoverResources
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Leftover resources: postcondition doesn't consume everything
+[@@expect_failure [228]]
+fn leftover (r s: ref int)
+  requires pts_to r 0 ** pts_to s 0
+  ensures pts_to r 0
+{
+  ()  // ERROR: pts_to s 0 is leftover
+}
diff --git a/pulse/test/error_messages/LeftoverResources.fst.output.expected b/pulse/test/error_messages/LeftoverResources.fst.output.expected
new file mode 100644
index 00000000000..bb81b192c59
--- /dev/null
+++ b/pulse/test/error_messages/LeftoverResources.fst.output.expected
@@ -0,0 +1,6 @@
+* Info at LeftoverResources.fst(11,2-11,4):
+  - Expected failure:
+  - Tactic failed
+  - Leftover resources: Pulse.Lib.Reference.pts_to s 0
+  - Did you forget to free these resources?
+
diff --git a/pulse/test/error_messages/LetBindingType.fst.output.expected b/pulse/test/error_messages/LetBindingType.fst.output.expected
new file mode 100644
index 00000000000..b33839f105b
--- /dev/null
+++ b/pulse/test/error_messages/LetBindingType.fst.output.expected
@@ -0,0 +1,4 @@
+* Info at LetBindingType.fst(11,17-11,19):
+  - Expected failure:
+  - Expected expression of type Prims.bool got expression 42 of type Prims.int
+
diff --git a/pulse/test/error_messages/Makefile b/pulse/test/error_messages/Makefile
index 49e47b7c411..d66d3cb5549 100644
--- a/pulse/test/error_messages/Makefile
+++ b/pulse/test/error_messages/Makefile
@@ -1,2 +1,15 @@
 PULSE_ROOT ?= ../..
 include $(PULSE_ROOT)/mk/test.mk
+
+# Ensure output directories exist
+$(shell mkdir -p _output _cache)
+
+# Suppress warnings that add noise to expected output
+OTHERFLAGS+=--warn_error -241-247-333-274-152-285
+
+# Remove --query_stats and --hint_info since they output timing info
+OTHERFLAGS := $(filter-out --query_stats, $(OTHERFLAGS))
+OTHERFLAGS := $(filter-out --hint_info, $(OTHERFLAGS))
+
+# Strip absolute paths for reproducibility
+OTHERFLAGS += --ext fstar:no_absolute_paths
diff --git a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
new file mode 100644
index 00000000000..73268388dac
--- /dev/null
+++ b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
@@ -0,0 +1,10 @@
+* Info at MatchBranchMismatch.fst(13,11-13,15):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - See also MatchBranchMismatch.fst(13,11-13,17)
+
diff --git a/pulse/test/error_messages/MissingPost.fst b/pulse/test/error_messages/MissingPost.fst
new file mode 100644
index 00000000000..10008290cc4
--- /dev/null
+++ b/pulse/test/error_messages/MissingPost.fst
@@ -0,0 +1,13 @@
+module MissingPost
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Function allocates but doesn't return it in post
+[@@expect_failure [228]]
+fn missing_post (r: ref int)
+  requires pts_to r 0
+  ensures emp
+{
+  r := 1;
+  ()  // ERROR: pts_to r 1 is leftover, post says emp
+}
diff --git a/pulse/test/error_messages/MissingPost.fst.output.expected b/pulse/test/error_messages/MissingPost.fst.output.expected
new file mode 100644
index 00000000000..9064d7f8522
--- /dev/null
+++ b/pulse/test/error_messages/MissingPost.fst.output.expected
@@ -0,0 +1,6 @@
+* Info at MissingPost.fst(12,2-12,4):
+  - Expected failure:
+  - Tactic failed
+  - Leftover resources: Pulse.Lib.Reference.pts_to r 1
+  - Did you forget to free these resources?
+
diff --git a/pulse/test/error_messages/MultiError.fst.output.expected b/pulse/test/error_messages/MultiError.fst.output.expected
new file mode 100644
index 00000000000..ae967d9728a
--- /dev/null
+++ b/pulse/test/error_messages/MultiError.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at MultiError.fst(12,18-12,19):
+  - Expected failure:
+  - Failed to prove pure property: false
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/MutualExcl.fst b/pulse/test/error_messages/MutualExcl.fst
new file mode 100644
index 00000000000..4a4f35a50a1
--- /dev/null
+++ b/pulse/test/error_messages/MutualExcl.fst
@@ -0,0 +1,12 @@
+module MutualExcl
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Postcondition has emp but function body leaves resources behind
+[@@expect_failure [228]]
+fn mutual_excl (r: ref int)
+  requires pts_to r 0
+  ensures emp
+{
+  ()  // ERROR: pts_to r 0 is leftover, postcondition is emp
+}
diff --git a/pulse/test/error_messages/MutualExcl.fst.output.expected b/pulse/test/error_messages/MutualExcl.fst.output.expected
new file mode 100644
index 00000000000..721f5efb1bc
--- /dev/null
+++ b/pulse/test/error_messages/MutualExcl.fst.output.expected
@@ -0,0 +1,6 @@
+* Info at MutualExcl.fst(11,2-11,4):
+  - Expected failure:
+  - Tactic failed
+  - Leftover resources: Pulse.Lib.Reference.pts_to r 0
+  - Did you forget to free these resources?
+
diff --git a/pulse/test/error_messages/NestedBlock.fst b/pulse/test/error_messages/NestedBlock.fst
new file mode 100644
index 00000000000..c632564f815
--- /dev/null
+++ b/pulse/test/error_messages/NestedBlock.fst
@@ -0,0 +1,15 @@
+module NestedBlock
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error inside a nested block should point to the inner statement
+[@@expect_failure [19]]
+fn nested_block (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0
+{
+  {
+    assert (pts_to r 1)  // ERROR: r is 0, not 1
+  };
+  ()
+}
diff --git a/pulse/test/error_messages/NestedBlock.fst.output.expected b/pulse/test/error_messages/NestedBlock.fst.output.expected
new file mode 100644
index 00000000000..2223d3a655e
--- /dev/null
+++ b/pulse/test/error_messages/NestedBlock.fst.output.expected
@@ -0,0 +1,9 @@
+* Info at NestedBlock.fst(14,2-14,4):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 1
+  - Pulse.Lib.Reference.pts_to r 0
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/NestedCall.fst.output.expected b/pulse/test/error_messages/NestedCall.fst.output.expected
new file mode 100644
index 00000000000..1d1ffb8a9e8
--- /dev/null
+++ b/pulse/test/error_messages/NestedCall.fst.output.expected
@@ -0,0 +1,9 @@
+* Info at NestedCall.fst(18,2-18,9):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 5
+  - Pulse.Lib.Reference.pts_to r 0
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/OpenScopeError.fst b/pulse/test/error_messages/OpenScopeError.fst
new file mode 100644
index 00000000000..376b0cf1459
--- /dev/null
+++ b/pulse/test/error_messages/OpenScopeError.fst
@@ -0,0 +1,13 @@
+module OpenScopeError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Opening a nonexistent module should produce a localized error
+[@@expect_failure [168]]
+fn open_fail ()
+  requires emp
+  ensures emp
+{
+  open NonExistent.Module;
+  ()
+}
diff --git a/pulse/test/error_messages/OpenScopeError.fst.output.expected b/pulse/test/error_messages/OpenScopeError.fst.output.expected
new file mode 100644
index 00000000000..c79c2e907b3
--- /dev/null
+++ b/pulse/test/error_messages/OpenScopeError.fst.output.expected
@@ -0,0 +1,6 @@
+Could not resolve namespace NonExistent.Module
+ valid namespaces are ["fstar.class.ord", "fstar.finiteset", "fstar.stubs.tactics.v2", "fstar.tactics.bv", "fstar.algebra.commmonoid", "fstar.stubs.typechecker", "fstar.stubs", "fstar.finitemap", "fstar.tactics.canon", "fstar.seq", "fstar.reflection.termeq", "pulse.lib.sort", "fstar.tactics.v2", "fstar.tactics.canoncommmonoidsimple", "fstar.sealed", "fstar.class.eq", "fstar.stubs.syntax", "fstar.algebra", "fstar.stubs.tactics.types", "pulse.lib.reference", "fstar.class", "fstar.list", "fstar.vector", "fstar.list.tot", "fstar.reflection.typing", "pulse.lib.seqmatch", "pulse.lib.trade", "pulse.class", "fstar.stubs.errors", "pulse.lib.hashtable", "fstar.reflection", "fstar.int.cast", "pulse.lib", "fstar.tactics.logic", "pulse.lib.core", "pulse.lib.forall", "fstar.stubs.tactics.v1", "fstar.int", "fstar", "fstar.tactics", "fstar.stubs.reflection.v2", "pulsecore", "pulse.lib.spec", "fstar.reflection.v2", "fstar.wellfounded", "fstar.stubs.reflection", "fstar.stubs.reflection.v1", "fstar.stubs.tactics", "pulse.c", "fstar.sequence", "fstar.classical", "pulse", "fstar.math", "fstar.list.pure", "fstar.reflection.v2.derived", "pulse.lib.pcm", "fstar.universe", "pulse.lib.slice", "fstar.algebra.commmonoid.fold", "pulse.c.types.struct", "pulse.c.types.array", "pulse.lib.array", "pulse.lib.linkedlist", "fstar.cardinality", "fstar.constanttime", "pulse.c.types", "pulse.lib.swap", "fstar.monotonic", "fstar.pure", "fstar.class.totalorder", "fstar.immutablearray", "fstar.pervasives", "pulse.lib.sort.merge"]
+* Info at OpenScopeError.fst(11,2-11,25):
+  - Expected failure:
+  - Failed to open namespace NonExistent.Module; You may need to bind this namespace outside Pulse for the F* dependency scanner to pick it up, e.g., write ``module _X = NonExistent.Module`` in F*
+
diff --git a/pulse/test/error_messages/PrePostMismatch.fst.output.expected b/pulse/test/error_messages/PrePostMismatch.fst.output.expected
new file mode 100644
index 00000000000..d61fea30e5b
--- /dev/null
+++ b/pulse/test/error_messages/PrePostMismatch.fst.output.expected
@@ -0,0 +1,10 @@
+* Info at PrePostMismatch.fst(11,2-11,6):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 1
+  - Pulse.Lib.Reference.pts_to r 42
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - See also PrePostMismatch.fst(11,2-11,8)
+
diff --git a/pulse/test/error_messages/ReturnImplicit.fst b/pulse/test/error_messages/ReturnImplicit.fst
new file mode 100644
index 00000000000..64a876b0965
--- /dev/null
+++ b/pulse/test/error_messages/ReturnImplicit.fst
@@ -0,0 +1,13 @@
+module ReturnImplicit
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Return type annotation mismatch with body
+[@@expect_failure [19]]
+fn return_impl ()
+  requires emp
+  returns r: nat
+  ensures emp
+{
+  -1  // ERROR: -1 is not nat
+}
diff --git a/pulse/test/error_messages/ReturnImplicit.fst.output.expected b/pulse/test/error_messages/ReturnImplicit.fst.output.expected
new file mode 100644
index 00000000000..6c1c31c9497
--- /dev/null
+++ b/pulse/test/error_messages/ReturnImplicit.fst.output.expected
@@ -0,0 +1,9 @@
+* Info at ReturnImplicit.fst(12,2-12,4):
+  - Expected failure:
+  - Ill-typed term: - 1
+  - Expected a term of type nat
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - Also see: Prims.fst(642,18-642,24)
+
diff --git a/pulse/test/error_messages/ReturnTypeMismatch.fst.output.expected b/pulse/test/error_messages/ReturnTypeMismatch.fst.output.expected
new file mode 100644
index 00000000000..64fef0ba1de
--- /dev/null
+++ b/pulse/test/error_messages/ReturnTypeMismatch.fst.output.expected
@@ -0,0 +1,4 @@
+* Info at ReturnTypeMismatch.fst(12,2-12,3):
+  - Expected failure:
+  - Expected expression of type Prims.bool got expression x of type Prims.int
+
diff --git a/pulse/test/error_messages/RewriteFail.fst b/pulse/test/error_messages/RewriteFail.fst
new file mode 100644
index 00000000000..a7d09146ccd
--- /dev/null
+++ b/pulse/test/error_messages/RewriteFail.fst
@@ -0,0 +1,13 @@
+module RewriteFail
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Rewrite with incompatible propositions
+[@@expect_failure [19]]
+fn rewrite_fail (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  rewrite (pts_to r 0) as (pts_to r 1);  // ERROR: can't rewrite, not equivalent
+  ()
+}
diff --git a/pulse/test/error_messages/RewriteFail.fst.output.expected b/pulse/test/error_messages/RewriteFail.fst.output.expected
new file mode 100644
index 00000000000..cf1a913c354
--- /dev/null
+++ b/pulse/test/error_messages/RewriteFail.fst.output.expected
@@ -0,0 +1,9 @@
+* Info at RewriteFail.fst(11,11-11,33):
+  - Expected failure:
+  - rewrite: could not prove equality of
+  - pts_to r 0
+  - pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/SequenceError.fst.output.expected b/pulse/test/error_messages/SequenceError.fst.output.expected
new file mode 100644
index 00000000000..af995a4267e
--- /dev/null
+++ b/pulse/test/error_messages/SequenceError.fst.output.expected
@@ -0,0 +1,9 @@
+* Info at SequenceError.fst(13,2-13,4):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r2 2
+  - Pulse.Lib.Reference.pts_to r2 1
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+
diff --git a/pulse/test/error_messages/SubtypingFailure.fst.output.expected b/pulse/test/error_messages/SubtypingFailure.fst.output.expected
new file mode 100644
index 00000000000..5c058ee6cf2
--- /dev/null
+++ b/pulse/test/error_messages/SubtypingFailure.fst.output.expected
@@ -0,0 +1,12 @@
+* Info at SubtypingFailure.fst(18,2-18,10):
+  - Expected failure:
+  - Ill-typed term: callee x
+  - Expected a term of type
+      fn
+        requires emp
+        ensures emp
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - Also see: Prims.fst(642,18-642,24)
+
diff --git a/pulse/test/error_messages/UnfoldFailure.fst.output.expected b/pulse/test/error_messages/UnfoldFailure.fst.output.expected
new file mode 100644
index 00000000000..b0980b5f4f7
--- /dev/null
+++ b/pulse/test/error_messages/UnfoldFailure.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at UnfoldFailure.fst(13,4-13,6):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      pts_to_uninit r
+  - In the context:
+      my_pred r
+
diff --git a/pulse/test/error_messages/WhileInvPreservation.fst b/pulse/test/error_messages/WhileInvPreservation.fst
new file mode 100644
index 00000000000..b33a97161fb
--- /dev/null
+++ b/pulse/test/error_messages/WhileInvPreservation.fst
@@ -0,0 +1,17 @@
+module WhileInvPreservation
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// While loop body fails to preserve invariant
+[@@expect_failure [19]]
+fn while_inv_fail ()
+  requires emp
+  ensures emp
+{
+  let mut i = 0;
+  while (let vi = !i; (vi < 10))
+  invariant pure (!i >= 0 /\ !i <= 10)
+  {
+    i := !i + 2  // ERROR: i + 2 might exceed 10, violating invariant
+  }
+}
diff --git a/pulse/test/error_messages/WhileInvPreservation.fst.output.expected b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected
new file mode 100644
index 00000000000..7fb891eb6a9
--- /dev/null
+++ b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected
@@ -0,0 +1,10 @@
+* Info at WhileInvPreservation.fst(15,4-15,8):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to i 2
+  - Pulse.Lib.Reference.pts_to i 0
+  - Assertion failed
+  - The SMT solver could not prove the query. Use --query_stats for more
+    details.
+  - See also WhileInvPreservation.fst(15,4-15,13)
+
diff --git a/pulse/test/error_messages/WithLocalError.fst b/pulse/test/error_messages/WithLocalError.fst
new file mode 100644
index 00000000000..d6662686eaf
--- /dev/null
+++ b/pulse/test/error_messages/WithLocalError.fst
@@ -0,0 +1,14 @@
+module WithLocalError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error within a with_local block
+[@@expect_failure [189]]
+fn with_local_err ()
+  requires emp
+  ensures emp
+{
+  let mut x = 0;
+  x := 5;
+  assert (pure (x == 0))  // ERROR: x is 5, not 0
+}
diff --git a/pulse/test/error_messages/WithLocalError.fst.output.expected b/pulse/test/error_messages/WithLocalError.fst.output.expected
new file mode 100644
index 00000000000..e67a562991c
--- /dev/null
+++ b/pulse/test/error_messages/WithLocalError.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at WithLocalError.fst(13,21-13,22):
+  - Expected failure:
+  - Ill-typed term: pure (x == 0)
+  - Expected expression of type Pulse.Lib.Reference.ref Prims.int
+    got expression 0
+    of type Prims.int
+

From 3560c82cececbf4d529db64e74909e1696a51dc9 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Fri, 1 May 2026 20:50:46 -0700
Subject: [PATCH 05/13] Pulse: fix error localization for deferred pure proof
 obligations

The prover's prove_pure and prove_with_pure functions create lazy
continuations (via cont_elab_thunk) that defer check_prop_validity calls
until elaboration time. By then, the with_error_bound scope has exited,
causing errors to be localized to the outer term (e.g., entire function
body) rather than the specific statement.

Fix: capture the current error_range_bound when the deferred closure is
created and restore it when check_prop_validity runs inside the closure.
Same pattern as the if-branch fix for prove_atom_result.

Example: 'fold (my_inv r (-1)); ()' now correctly shows error at the
fold statement (13,2-13,22) instead of spanning both statements (13,2-14,4).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/src/checker/Pulse.Checker.Prover.fst | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst
index 6109b8bbf9e..98fbdbaed66 100644
--- a/pulse/src/checker/Pulse.Checker.Prover.fst
+++ b/pulse/src/checker/Pulse.Checker.Prover.fst
@@ -387,9 +387,18 @@ let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slp
     if pure_eq_unif g p skip_eq_uvar then None else begin
     debug_prover g (fun _ -> Printf.sprintf "prove_pure p=%s success" (show p));
 
+    let saved_bound = RU.get_error_bound () in
     Some (| g, ctxt, [], [], fun g'' ->
  // implied by t2_typing
-      let pv = check_prop_validity g'' p in
+      // Restore the error bound that was active when this pure goal was matched.
+      // This closure is evaluated lazily (via cont_elab_thunk) after the
+      // original with_error_bound scope has exited.
+      let pv =
+        let do_check () = check_prop_validity g'' p in
+        match saved_bound with
+        | Some r -> RU.with_error_bound r do_check
+        | None -> do_check ()
+      in
       cont_elab_refl g ctxt ([] @ ctxt),
       (fun frame ->
 
@@ -424,12 +433,19 @@ let prove_with_pure (g: env) (ctxt: list slprop_view) skip_eq_uvar (goal: slprop
   | WithPure p n v ->
     if pure_eq_unif g p skip_eq_uvar then None else
 
+    let saved_bound = RU.get_error_bound () in
     Some (| g, ctxt, [Unknown v], [], fun g'' ->
       cont_elab_refl g ctxt ([] @ ctxt),
       (fun frame ->
 
 
-        k_elab_equiv (elab_slprops (frame @ [Unknown v] @ [])) (elab_slprops (frame @ [goal])) (intro_with_pure g'' (elab_slprops frame) p n v))
+        k_elab_equiv (elab_slprops (frame @ [Unknown v] @ [])) (elab_slprops (frame @ [goal]))
+          (let do_intro post t =
+            (match saved_bound with
+             | Some r -> RU.with_error_bound r (fun () -> intro_with_pure g'' (elab_slprops frame) p n v post t)
+             | None -> intro_with_pure g'' (elab_slprops frame) p n v post t)
+          in
+          do_intro))
       <: T.Tac _ |)
   | _ -> None
 

From 10ec42eb04d4faa00899b00bcdc60a6a6522a7ae Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Fri, 1 May 2026 20:50:54 -0700
Subject: [PATCH 06/13] Update Pulse error message tests with multi-statement
 bodies

Add continuation statements (; ()) after error-causing statements in
test files to ensure error localization doesn't bleed into following
code. This catches regressions where the error range expands to include
the continuation.

Also uncomment [@@expect_failure] attributes on FoldError, IllTypedInvariant,
and NestedBlock so __verify and __diff both succeed in the test harness.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/test/error_messages/AtomicMismatch.fst              | 3 ++-
 pulse/test/error_messages/FoldError.fst                   | 3 ++-
 pulse/test/error_messages/FramingFailure.fst              | 3 ++-
 pulse/test/error_messages/IfCondType.fst                  | 3 ++-
 pulse/test/error_messages/InvariantPayload.fst            | 3 ++-
 pulse/test/error_messages/LambdaArg.fst                   | 3 ++-
 pulse/test/error_messages/LambdaArg.fst.output.expected   | 1 +
 pulse/test/error_messages/NestedBlock.fst                 | 8 ++++----
 pulse/test/error_messages/NestedCall.fst                  | 3 ++-
 pulse/test/error_messages/NestedCall.fst.output.expected  | 1 +
 pulse/test/error_messages/PrePostMismatch.fst             | 3 ++-
 .../error_messages/PrePostMismatch.fst.output.expected    | 3 +--
 pulse/test/error_messages/SubtypingFailure.fst            | 3 ++-
 pulse/test/error_messages/UnfoldFailure.fst               | 3 ++-
 14 files changed, 27 insertions(+), 16 deletions(-)

diff --git a/pulse/test/error_messages/AtomicMismatch.fst b/pulse/test/error_messages/AtomicMismatch.fst
index 435848b0455..180ffba57f8 100644
--- a/pulse/test/error_messages/AtomicMismatch.fst
+++ b/pulse/test/error_messages/AtomicMismatch.fst
@@ -9,5 +9,6 @@ fn atomic_fn (r: ref int)
   requires pts_to r 0
   ensures pts_to r 1
 {
-  r := 1  // Might error if := is not atomic-compatible
+  r := 1;  // Might error if := is not atomic-compatible
+  ()
 }
diff --git a/pulse/test/error_messages/FoldError.fst b/pulse/test/error_messages/FoldError.fst
index 813bd09809b..de718f264b5 100644
--- a/pulse/test/error_messages/FoldError.fst
+++ b/pulse/test/error_messages/FoldError.fst
@@ -10,5 +10,6 @@ fn fold_fail (r: ref int)
   requires pts_to r (-1)
   ensures my_inv r (-1)
 {
-  fold (my_inv r (-1))  // ERROR: pure (v >= 0) not satisfiable with v = -1
+  fold (my_inv r (-1));  // ERROR: pure (v >= 0) not satisfiable with v = -1
+  ()
 }
diff --git a/pulse/test/error_messages/FramingFailure.fst b/pulse/test/error_messages/FramingFailure.fst
index a41ed88c4ed..63db1c6fe43 100644
--- a/pulse/test/error_messages/FramingFailure.fst
+++ b/pulse/test/error_messages/FramingFailure.fst
@@ -9,5 +9,6 @@ fn framing_fail (r1 r2: ref int)
   ensures pts_to r1 1
 {
   let v = !r2;
-  r1 := 1
+  r1 := 1;
+  ()
 }
diff --git a/pulse/test/error_messages/IfCondType.fst b/pulse/test/error_messages/IfCondType.fst
index 3808d2b0c03..0827bb803db 100644
--- a/pulse/test/error_messages/IfCondType.fst
+++ b/pulse/test/error_messages/IfCondType.fst
@@ -8,5 +8,6 @@ fn bad_if_cond (x: int)
   requires emp
   ensures emp
 {
-  if x { () } else { () }
+  if x { () } else { () };
+  ()
 }
diff --git a/pulse/test/error_messages/InvariantPayload.fst b/pulse/test/error_messages/InvariantPayload.fst
index 3bddac15f13..fd969bd5137 100644
--- a/pulse/test/error_messages/InvariantPayload.fst
+++ b/pulse/test/error_messages/InvariantPayload.fst
@@ -10,5 +10,6 @@ fn inv_payload_fail (r: ref int)
   requires pts_to r 0
   ensures my_pred r
 {
-  fold my_pred r  // ERROR: can't prove v > 0 with v = 0
+  fold my_pred r;  // ERROR: can't prove v > 0 with v = 0
+  ()
 }
diff --git a/pulse/test/error_messages/LambdaArg.fst b/pulse/test/error_messages/LambdaArg.fst
index 48f7900321e..6a11da31b95 100644
--- a/pulse/test/error_messages/LambdaArg.fst
+++ b/pulse/test/error_messages/LambdaArg.fst
@@ -15,5 +15,6 @@ fn wrong_args ()
   requires emp
   ensures emp
 {
-  takes_two 1 2 3  // ERROR: too many arguments
+  takes_two 1 2 3;  // ERROR: too many arguments
+  ()
 }
diff --git a/pulse/test/error_messages/LambdaArg.fst.output.expected b/pulse/test/error_messages/LambdaArg.fst.output.expected
index ffe4693798d..96c4318c9a1 100644
--- a/pulse/test/error_messages/LambdaArg.fst.output.expected
+++ b/pulse/test/error_messages/LambdaArg.fst.output.expected
@@ -1,5 +1,6 @@
 * Info at LambdaArg.fst(18,2-18,11):
   - Expected failure:
+  - Ill-typed term: takes_two 1 2 3
   - Expected a function.
   - Got an expression of type:
       fn
diff --git a/pulse/test/error_messages/NestedBlock.fst b/pulse/test/error_messages/NestedBlock.fst
index c632564f815..cef9b5b811c 100644
--- a/pulse/test/error_messages/NestedBlock.fst
+++ b/pulse/test/error_messages/NestedBlock.fst
@@ -8,8 +8,8 @@ fn nested_block (r: ref int)
   requires pts_to r 0
   ensures pts_to r 0
 {
-  {
-    assert (pts_to r 1)  // ERROR: r is 0, not 1
-  };
-  ()
+  // {
+    assert (pts_to r 1);  // ERROR: r is 0, not 1
+  // };
+  () //FIX! error is 
 }
diff --git a/pulse/test/error_messages/NestedCall.fst b/pulse/test/error_messages/NestedCall.fst
index 74b3dec9fd8..99f49960d43 100644
--- a/pulse/test/error_messages/NestedCall.fst
+++ b/pulse/test/error_messages/NestedCall.fst
@@ -15,5 +15,6 @@ fn outer (r: ref int)
   requires pts_to r 5
   ensures pts_to r 1
 {
-  inner r  // ERROR: precondition mismatch (pts_to r 5 vs pts_to r 0)
+  inner r;  // ERROR: precondition mismatch (pts_to r 5 vs pts_to r 0)
+  ()
 }
diff --git a/pulse/test/error_messages/NestedCall.fst.output.expected b/pulse/test/error_messages/NestedCall.fst.output.expected
index 1d1ffb8a9e8..0f24c09f5db 100644
--- a/pulse/test/error_messages/NestedCall.fst.output.expected
+++ b/pulse/test/error_messages/NestedCall.fst.output.expected
@@ -6,4 +6,5 @@
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
+  - See also NestedCall.fst(18,2-19,4)
 
diff --git a/pulse/test/error_messages/PrePostMismatch.fst b/pulse/test/error_messages/PrePostMismatch.fst
index f458c41bbec..88f248c6745 100644
--- a/pulse/test/error_messages/PrePostMismatch.fst
+++ b/pulse/test/error_messages/PrePostMismatch.fst
@@ -8,5 +8,6 @@ fn pre_post_mismatch (r: ref int)
   requires pts_to r 0
   ensures pts_to r 42
 {
-  r := 1
+  r := 1;
+  ()
 }
diff --git a/pulse/test/error_messages/PrePostMismatch.fst.output.expected b/pulse/test/error_messages/PrePostMismatch.fst.output.expected
index d61fea30e5b..0cf1a917e9f 100644
--- a/pulse/test/error_messages/PrePostMismatch.fst.output.expected
+++ b/pulse/test/error_messages/PrePostMismatch.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at PrePostMismatch.fst(11,2-11,6):
+* Info at PrePostMismatch.fst(12,2-12,4):
   - Expected failure:
   - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to r 1
@@ -6,5 +6,4 @@
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
-  - See also PrePostMismatch.fst(11,2-11,8)
 
diff --git a/pulse/test/error_messages/SubtypingFailure.fst b/pulse/test/error_messages/SubtypingFailure.fst
index ccb3993446c..aaaa769666c 100644
--- a/pulse/test/error_messages/SubtypingFailure.fst
+++ b/pulse/test/error_messages/SubtypingFailure.fst
@@ -15,5 +15,6 @@ fn caller (x: int)
   requires emp
   ensures emp
 {
-  callee x
+  callee x;
+  ()
 }
diff --git a/pulse/test/error_messages/UnfoldFailure.fst b/pulse/test/error_messages/UnfoldFailure.fst
index 814be962464..ba783101628 100644
--- a/pulse/test/error_messages/UnfoldFailure.fst
+++ b/pulse/test/error_messages/UnfoldFailure.fst
@@ -10,5 +10,6 @@ fn unfold_fail (r: ref int)
   requires my_pred r
   ensures pts_to r 1
 {
-  r := 1  // ERROR: can't write to r without unfolding my_pred first
+  r := 1;  // ERROR: can't write to r without unfolding my_pred first
+  ()
 }

From 9f73870012181a153d5f360b6f296c73e9b7c98b Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Fri, 1 May 2026 21:21:43 -0700
Subject: [PATCH 07/13] Pulse: make prover atom equivalence check eager for
 better error localization

Previously, prove_atom_result deferred check_slprop_equiv_ext to a
continuation closure. This caused errors from mismatched atoms to be
mislocalized when the closure executed after with_error_bound had
exited. In particular, 'assert (P); continuation' would show errors
at the continuation rather than at the assert statement, because the
postcondition prover's deferred closure ran first in continuation
order.

By running check_slprop_equiv_ext eagerly (at prove time rather than
elaboration time), errors are reported with the correct
error_range_bound context. This is safe because the check uses the
original environment g (not the extended g'), so it doesn't depend on
later prover state.

The saved_bound/get_error_bound mechanism is retained in prove_pure
and prove_with_pure, where the deferred checks need the extended
environment g''.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/src/checker/Pulse.Checker.Prover.fst    | 24 +++++++------------
 pulse/test/error_messages/NestedBlock.fst     |  2 +-
 .../NestedBlock.fst.output.expected           |  4 ++--
 pulse/test/error_messages/SequenceError.fst   |  4 ++--
 4 files changed, 14 insertions(+), 20 deletions(-)

diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst
index 98fbdbaed66..08ff499a31b 100644
--- a/pulse/src/checker/Pulse.Checker.Prover.fst
+++ b/pulse/src/checker/Pulse.Checker.Prover.fst
@@ -943,22 +943,16 @@ let prove_atom_result (g: env)
     T.Tac (prover_result g ctxt0 [goal]) =
   let Atom _ dup _ _ = ctxt in
   let goal = elab_slprop goal in
-  let saved_bound = RU.get_error_bound () in
+  // Run the equivalence check eagerly (not deferred in a continuation) so that
+  // errors are reported with the correct error_range_bound context.
+  // Previously this was deferred in the continuation closure, but that caused
+  // errors to be mislocalized when the closure ran after with_error_bound exited.
+  let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
+  (if dup then
+    ignore (compute_term_type g
+      (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
+        [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
   (| g, (if dup then rest_ctxt@[ctxt] else rest_ctxt), [], [ctxt], fun g' ->
-    // Restore the error bound that was active when the prover matched this atom.
-    // This closure may be evaluated lazily (via cont_elab_thunk) after the
-    // original with_error_bound scope has exited.
-    let do_check () =
-      let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
-      (if dup then
-        ignore (compute_term_type g
-          (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
-            [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
-      ()
-    in
-    (match saved_bound with
-     | Some r -> RU.with_error_bound r do_check
-     | None -> do_check ());
     cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
 
 // this matches atoms when they're the only unifiable pair
diff --git a/pulse/test/error_messages/NestedBlock.fst b/pulse/test/error_messages/NestedBlock.fst
index cef9b5b811c..d2365ae8509 100644
--- a/pulse/test/error_messages/NestedBlock.fst
+++ b/pulse/test/error_messages/NestedBlock.fst
@@ -11,5 +11,5 @@ fn nested_block (r: ref int)
   // {
     assert (pts_to r 1);  // ERROR: r is 0, not 1
   // };
-  () //FIX! error is 
+  ()
 }
diff --git a/pulse/test/error_messages/NestedBlock.fst.output.expected b/pulse/test/error_messages/NestedBlock.fst.output.expected
index 2223d3a655e..233684d48b8 100644
--- a/pulse/test/error_messages/NestedBlock.fst.output.expected
+++ b/pulse/test/error_messages/NestedBlock.fst.output.expected
@@ -1,8 +1,8 @@
-* Info at NestedBlock.fst(14,2-14,4):
+* Info at NestedBlock.fst(12,4-12,22):
   - Expected failure:
   - Could not prove equality of:
-  - Pulse.Lib.Reference.pts_to r 1
   - Pulse.Lib.Reference.pts_to r 0
+  - Pulse.Lib.Reference.pts_to r 1
   - Assertion failed
   - The SMT solver could not prove the query. Use --query_stats for more
     details.
diff --git a/pulse/test/error_messages/SequenceError.fst b/pulse/test/error_messages/SequenceError.fst
index f98cc98843b..ccf9ba006d0 100644
--- a/pulse/test/error_messages/SequenceError.fst
+++ b/pulse/test/error_messages/SequenceError.fst
@@ -9,6 +9,6 @@ fn seq_error (r1 r2: ref int)
   ensures pts_to r1 1 ** pts_to r2 1
 {
   r1 := 1;
-  r2 := 2;  // ERROR: should point here, post expects pts_to r2 1
-  ()
+  r2 := 2;
+  ()  // ERROR: postcondition pts_to r2 1 checked here, but context has pts_to r2 2
 }

From 511c14a69a032652009de2eefd499ba34afc2842 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Tue, 5 May 2026 12:33:57 -0700
Subject: [PATCH 08/13] Pulse: make prover atom equivalence check eager when
 uvar-free

When the prover matches an atom (slprop) from context to goal, it needs to
verify the equivalence via check_slprop_equiv_ext. Previously this was always
deferred in a continuation closure, which caused error mislocalization: if the
continuation ran after with_error_bound exited, the error range was wrong.

The fix uses a hybrid approach:
- If both terms are uvar-free (checked via deep_compress_safe + no_uvars_in_term),
  run the check eagerly while the correct error_range_bound is active.
- If either term has unresolved uvars (which later prover steps may instantiate),
  defer the check in a continuation but capture/restore the error_range_bound.

Also factors out shared helpers (with_saved_bound, check_atom_equiv) to reduce
duplication across the eager/deferred paths and the prove_pure/prove_with_pure
functions that use the same saved-bound pattern.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/src/checker/Pulse.Checker.Prover.fst    | 62 ++++++++++++-------
 .../OpenScopeError.fst.output.expected        |  2 +-
 2 files changed, 40 insertions(+), 24 deletions(-)

diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst
index 08ff499a31b..d43396243ba 100644
--- a/pulse/src/checker/Pulse.Checker.Prover.fst
+++ b/pulse/src/checker/Pulse.Checker.Prover.fst
@@ -377,6 +377,13 @@ let pure_eq_unif (g: env) (p: term) skip_eq_uvar : Dv bool =
     )
   | None -> false
 
+// Restore a previously-captured error_range_bound around a thunk.
+let with_saved_bound (saved_bound: option Range.range) (f: unit -> T.Tac 'a)
+  : T.Tac 'a =
+  match saved_bound with
+  | Some r -> RU.with_error_bound r f
+  | None -> f ()
+
 // skip_eq_uvar to support (assert foo. with pure (foo == ....))
 let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slprop_view) :
     T.Tac (option (prover_result g ctxt [goal])) =
@@ -393,12 +400,7 @@ let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slp
       // Restore the error bound that was active when this pure goal was matched.
       // This closure is evaluated lazily (via cont_elab_thunk) after the
       // original with_error_bound scope has exited.
-      let pv =
-        let do_check () = check_prop_validity g'' p in
-        match saved_bound with
-        | Some r -> RU.with_error_bound r do_check
-        | None -> do_check ()
-      in
+      let pv = with_saved_bound saved_bound (fun () -> check_prop_validity g'' p) in
       cont_elab_refl g ctxt ([] @ ctxt),
       (fun frame ->
 
@@ -440,12 +442,9 @@ let prove_with_pure (g: env) (ctxt: list slprop_view) skip_eq_uvar (goal: slprop
 
 
         k_elab_equiv (elab_slprops (frame @ [Unknown v] @ [])) (elab_slprops (frame @ [goal]))
-          (let do_intro post t =
-            (match saved_bound with
-             | Some r -> RU.with_error_bound r (fun () -> intro_with_pure g'' (elab_slprops frame) p n v post t)
-             | None -> intro_with_pure g'' (elab_slprops frame) p n v post t)
-          in
-          do_intro))
+          (fun post t ->
+            with_saved_bound saved_bound
+              (fun () -> intro_with_pure g'' (elab_slprops frame) p n v post t)))
       <: T.Tac _ |)
   | _ -> None
 
@@ -936,6 +935,15 @@ let is_unamb g (cands: list (int & slprop_view)) : T.Tac bool =
 
 let dup_lid = ["Pulse"; "Class"; "Duplicable"; "dup"]
 
+// Check that ctxt_t and goal are equivalent slprops, and (if dup) that the
+// dup token typechecks.
+let check_atom_equiv (g: env) (ctxt_t goal: T.term) (dup: bool) : T.Tac unit =
+  let _ = check_slprop_equiv_ext (RU.range_of_term goal) g ctxt_t goal in
+  if dup then
+    ignore (compute_term_type g
+      (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
+        [ctxt_t, R.Q_Explicit; unit_const, R.Q_Explicit]))
+
 let prove_atom_result (g: env)
     (ctxt: slprop_view { Atom? ctxt }) (rest_ctxt: list slprop_view)
     (#ctxt0: list slprop_view) // ctxt0 == ctxt ** rest_ctxt
@@ -943,17 +951,25 @@ let prove_atom_result (g: env)
     T.Tac (prover_result g ctxt0 [goal]) =
   let Atom _ dup _ _ = ctxt in
   let goal = elab_slprop goal in
-  // Run the equivalence check eagerly (not deferred in a continuation) so that
-  // errors are reported with the correct error_range_bound context.
-  // Previously this was deferred in the continuation closure, but that caused
-  // errors to be mislocalized when the closure ran after with_error_bound exited.
-  let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
-  (if dup then
-    ignore (compute_term_type g
-      (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
-        [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
-  (| g, (if dup then rest_ctxt@[ctxt] else rest_ctxt), [], [ctxt], fun g' ->
-    cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
+  let ctxt_t = elab_slprop ctxt in
+  // When terms have no uvars we check eagerly for better error localization
+  // (the correct error_range_bound is still active). When uvars are present
+  // we must defer because later prover steps may instantiate them.
+  let can_check_eagerly =
+    RU.no_uvars_in_term (RU.deep_compress_safe ctxt_t) &&
+    RU.no_uvars_in_term (RU.deep_compress_safe goal)
+  in
+  let rest = if dup then rest_ctxt@[ctxt] else rest_ctxt in
+  if can_check_eagerly then (
+    check_atom_equiv g ctxt_t goal dup;
+    (| g, rest, [], [ctxt], fun g' ->
+      cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
+  ) else (
+    let saved_bound = RU.get_error_bound () in
+    (| g, rest, [], [ctxt], fun g' ->
+      with_saved_bound saved_bound (fun () -> check_atom_equiv g ctxt_t goal dup);
+      cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
+  )
 
 // this matches atoms when they're the only unifiable pair
 // necessary for various gather like functions where you don't specify all arguments
diff --git a/pulse/test/error_messages/OpenScopeError.fst.output.expected b/pulse/test/error_messages/OpenScopeError.fst.output.expected
index c79c2e907b3..985b7e0f047 100644
--- a/pulse/test/error_messages/OpenScopeError.fst.output.expected
+++ b/pulse/test/error_messages/OpenScopeError.fst.output.expected
@@ -1,5 +1,5 @@
 Could not resolve namespace NonExistent.Module
- valid namespaces are ["fstar.class.ord", "fstar.finiteset", "fstar.stubs.tactics.v2", "fstar.tactics.bv", "fstar.algebra.commmonoid", "fstar.stubs.typechecker", "fstar.stubs", "fstar.finitemap", "fstar.tactics.canon", "fstar.seq", "fstar.reflection.termeq", "pulse.lib.sort", "fstar.tactics.v2", "fstar.tactics.canoncommmonoidsimple", "fstar.sealed", "fstar.class.eq", "fstar.stubs.syntax", "fstar.algebra", "fstar.stubs.tactics.types", "pulse.lib.reference", "fstar.class", "fstar.list", "fstar.vector", "fstar.list.tot", "fstar.reflection.typing", "pulse.lib.seqmatch", "pulse.lib.trade", "pulse.class", "fstar.stubs.errors", "pulse.lib.hashtable", "fstar.reflection", "fstar.int.cast", "pulse.lib", "fstar.tactics.logic", "pulse.lib.core", "pulse.lib.forall", "fstar.stubs.tactics.v1", "fstar.int", "fstar", "fstar.tactics", "fstar.stubs.reflection.v2", "pulsecore", "pulse.lib.spec", "fstar.reflection.v2", "fstar.wellfounded", "fstar.stubs.reflection", "fstar.stubs.reflection.v1", "fstar.stubs.tactics", "pulse.c", "fstar.sequence", "fstar.classical", "pulse", "fstar.math", "fstar.list.pure", "fstar.reflection.v2.derived", "pulse.lib.pcm", "fstar.universe", "pulse.lib.slice", "fstar.algebra.commmonoid.fold", "pulse.c.types.struct", "pulse.c.types.array", "pulse.lib.array", "pulse.lib.linkedlist", "fstar.cardinality", "fstar.constanttime", "pulse.c.types", "pulse.lib.swap", "fstar.monotonic", "fstar.pure", "fstar.class.totalorder", "fstar.immutablearray", "fstar.pervasives", "pulse.lib.sort.merge"]
+ valid namespaces are ["fstar.class.ord", "fstar.finiteset", "fstar.stubs.tactics.v2", "fstar.tactics.bv", "fstar.algebra.commmonoid", "fstar.stubs.typechecker", "fstar.stubs", "fstar.finitemap", "fstar.tactics.canon", "fstar.seq", "fstar.reflection.termeq", "pulse.lib.sort", "fstar.tactics.v2", "fstar.tactics.canoncommmonoidsimple", "fstar.sealed", "fstar.class.eq", "fstar.stubs.syntax", "fstar.algebra", "fstar.stubs.tactics.types", "pulse.lib.reference", "fstar.class", "fstar.list", "fstar.vector", "fstar.list.tot", "fstar.reflection.typing", "pulse.lib.seqmatch", "pulse.lib.trade", "pulse.class", "fstar.stubs.errors", "pulse.lib.hashtable", "fstar.reflection", "fstar.int.cast", "pulse.lib", "fstar.tactics.logic", "pulse.lib.core", "pulse.lib.forall", "fstar.int", "fstar", "fstar.tactics", "fstar.stubs.reflection.v2", "pulsecore", "pulse.lib.spec", "fstar.reflection.v2", "fstar.wellfounded", "fstar.stubs.reflection", "fstar.stubs.tactics", "pulse.c", "fstar.sequence", "fstar.classical", "pulse", "fstar.math", "fstar.list.pure", "fstar.reflection.v2.derived", "pulse.lib.pcm", "fstar.universe", "pulse.lib.slice", "fstar.algebra.commmonoid.fold", "pulse.c.types.struct", "pulse.c.types.array", "pulse.lib.array", "pulse.lib.linkedlist", "fstar.cardinality", "fstar.constanttime", "pulse.c.types", "pulse.lib.swap", "fstar.monotonic", "fstar.pure", "fstar.class.totalorder", "fstar.immutablearray", "fstar.pervasives", "pulse.lib.sort.merge"]
 * Info at OpenScopeError.fst(11,2-11,25):
   - Expected failure:
   - Failed to open namespace NonExistent.Module; You may need to bind this namespace outside Pulse for the F* dependency scanner to pick it up, e.g., write ``module _X = NonExistent.Module`` in F*

From b537cbc3d9bf4248c0462254a7ccc3cce350e6fd Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Tue, 5 May 2026 12:33:57 -0700
Subject: [PATCH 09/13] Pulse: fix error localization for deferred pure proof
 obligations
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

When the prover matches atoms or pure goals, the equivalence/validity checks
are deferred in continuation closures (cont_elab_thunk). These closures run
after the original with_error_bound scope has exited, causing errors to be
reported with incorrect ranges.

Fix: capture the active error_range_bound at match time (via get_error_bound)
and restore it inside the deferred closure (via with_error_bound). This is done
in prove_pure and prove_with_pure via a shared with_saved_bound helper.

The atom equivalence check in prove_atom_result remains deferred (inside the
continuation) as before—this is necessary because the prover may match atoms
before all unification variables are resolved.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/src/checker/Pulse.Checker.Prover.fst    | 38 +++++++++----------
 .../OpenScopeError.fst.output.expected        |  2 +-
 2 files changed, 18 insertions(+), 22 deletions(-)

diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst
index 08ff499a31b..271aa43c737 100644
--- a/pulse/src/checker/Pulse.Checker.Prover.fst
+++ b/pulse/src/checker/Pulse.Checker.Prover.fst
@@ -377,6 +377,13 @@ let pure_eq_unif (g: env) (p: term) skip_eq_uvar : Dv bool =
     )
   | None -> false
 
+// Restore a previously-captured error_range_bound around a thunk.
+let with_saved_bound (saved_bound: option Range.range) (f: unit -> T.Tac 'a)
+  : T.Tac 'a =
+  match saved_bound with
+  | Some r -> RU.with_error_bound r f
+  | None -> f ()
+
 // skip_eq_uvar to support (assert foo. with pure (foo == ....))
 let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slprop_view) :
     T.Tac (option (prover_result g ctxt [goal])) =
@@ -393,12 +400,7 @@ let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slp
       // Restore the error bound that was active when this pure goal was matched.
       // This closure is evaluated lazily (via cont_elab_thunk) after the
       // original with_error_bound scope has exited.
-      let pv =
-        let do_check () = check_prop_validity g'' p in
-        match saved_bound with
-        | Some r -> RU.with_error_bound r do_check
-        | None -> do_check ()
-      in
+      let pv = with_saved_bound saved_bound (fun () -> check_prop_validity g'' p) in
       cont_elab_refl g ctxt ([] @ ctxt),
       (fun frame ->
 
@@ -440,12 +442,9 @@ let prove_with_pure (g: env) (ctxt: list slprop_view) skip_eq_uvar (goal: slprop
 
 
         k_elab_equiv (elab_slprops (frame @ [Unknown v] @ [])) (elab_slprops (frame @ [goal]))
-          (let do_intro post t =
-            (match saved_bound with
-             | Some r -> RU.with_error_bound r (fun () -> intro_with_pure g'' (elab_slprops frame) p n v post t)
-             | None -> intro_with_pure g'' (elab_slprops frame) p n v post t)
-          in
-          do_intro))
+          (fun post t ->
+            with_saved_bound saved_bound
+              (fun () -> intro_with_pure g'' (elab_slprops frame) p n v post t)))
       <: T.Tac _ |)
   | _ -> None
 
@@ -943,16 +942,13 @@ let prove_atom_result (g: env)
     T.Tac (prover_result g ctxt0 [goal]) =
   let Atom _ dup _ _ = ctxt in
   let goal = elab_slprop goal in
-  // Run the equivalence check eagerly (not deferred in a continuation) so that
-  // errors are reported with the correct error_range_bound context.
-  // Previously this was deferred in the continuation closure, but that caused
-  // errors to be mislocalized when the closure ran after with_error_bound exited.
-  let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
-  (if dup then
-    ignore (compute_term_type g
-      (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
-        [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
   (| g, (if dup then rest_ctxt@[ctxt] else rest_ctxt), [], [ctxt], fun g' ->
+    let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
+    (if dup then
+      // Check that we can indeed synthesize a duplicable instance
+      ignore (compute_term_type g
+        (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
+          [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
     cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
 
 // this matches atoms when they're the only unifiable pair
diff --git a/pulse/test/error_messages/OpenScopeError.fst.output.expected b/pulse/test/error_messages/OpenScopeError.fst.output.expected
index c79c2e907b3..985b7e0f047 100644
--- a/pulse/test/error_messages/OpenScopeError.fst.output.expected
+++ b/pulse/test/error_messages/OpenScopeError.fst.output.expected
@@ -1,5 +1,5 @@
 Could not resolve namespace NonExistent.Module
- valid namespaces are ["fstar.class.ord", "fstar.finiteset", "fstar.stubs.tactics.v2", "fstar.tactics.bv", "fstar.algebra.commmonoid", "fstar.stubs.typechecker", "fstar.stubs", "fstar.finitemap", "fstar.tactics.canon", "fstar.seq", "fstar.reflection.termeq", "pulse.lib.sort", "fstar.tactics.v2", "fstar.tactics.canoncommmonoidsimple", "fstar.sealed", "fstar.class.eq", "fstar.stubs.syntax", "fstar.algebra", "fstar.stubs.tactics.types", "pulse.lib.reference", "fstar.class", "fstar.list", "fstar.vector", "fstar.list.tot", "fstar.reflection.typing", "pulse.lib.seqmatch", "pulse.lib.trade", "pulse.class", "fstar.stubs.errors", "pulse.lib.hashtable", "fstar.reflection", "fstar.int.cast", "pulse.lib", "fstar.tactics.logic", "pulse.lib.core", "pulse.lib.forall", "fstar.stubs.tactics.v1", "fstar.int", "fstar", "fstar.tactics", "fstar.stubs.reflection.v2", "pulsecore", "pulse.lib.spec", "fstar.reflection.v2", "fstar.wellfounded", "fstar.stubs.reflection", "fstar.stubs.reflection.v1", "fstar.stubs.tactics", "pulse.c", "fstar.sequence", "fstar.classical", "pulse", "fstar.math", "fstar.list.pure", "fstar.reflection.v2.derived", "pulse.lib.pcm", "fstar.universe", "pulse.lib.slice", "fstar.algebra.commmonoid.fold", "pulse.c.types.struct", "pulse.c.types.array", "pulse.lib.array", "pulse.lib.linkedlist", "fstar.cardinality", "fstar.constanttime", "pulse.c.types", "pulse.lib.swap", "fstar.monotonic", "fstar.pure", "fstar.class.totalorder", "fstar.immutablearray", "fstar.pervasives", "pulse.lib.sort.merge"]
+ valid namespaces are ["fstar.class.ord", "fstar.finiteset", "fstar.stubs.tactics.v2", "fstar.tactics.bv", "fstar.algebra.commmonoid", "fstar.stubs.typechecker", "fstar.stubs", "fstar.finitemap", "fstar.tactics.canon", "fstar.seq", "fstar.reflection.termeq", "pulse.lib.sort", "fstar.tactics.v2", "fstar.tactics.canoncommmonoidsimple", "fstar.sealed", "fstar.class.eq", "fstar.stubs.syntax", "fstar.algebra", "fstar.stubs.tactics.types", "pulse.lib.reference", "fstar.class", "fstar.list", "fstar.vector", "fstar.list.tot", "fstar.reflection.typing", "pulse.lib.seqmatch", "pulse.lib.trade", "pulse.class", "fstar.stubs.errors", "pulse.lib.hashtable", "fstar.reflection", "fstar.int.cast", "pulse.lib", "fstar.tactics.logic", "pulse.lib.core", "pulse.lib.forall", "fstar.int", "fstar", "fstar.tactics", "fstar.stubs.reflection.v2", "pulsecore", "pulse.lib.spec", "fstar.reflection.v2", "fstar.wellfounded", "fstar.stubs.reflection", "fstar.stubs.tactics", "pulse.c", "fstar.sequence", "fstar.classical", "pulse", "fstar.math", "fstar.list.pure", "fstar.reflection.v2.derived", "pulse.lib.pcm", "fstar.universe", "pulse.lib.slice", "fstar.algebra.commmonoid.fold", "pulse.c.types.struct", "pulse.c.types.array", "pulse.lib.array", "pulse.lib.linkedlist", "fstar.cardinality", "fstar.constanttime", "pulse.c.types", "pulse.lib.swap", "fstar.monotonic", "fstar.pure", "fstar.class.totalorder", "fstar.immutablearray", "fstar.pervasives", "pulse.lib.sort.merge"]
 * Info at OpenScopeError.fst(11,2-11,25):
   - Expected failure:
   - Failed to open namespace NonExistent.Module; You may need to bind this namespace outside Pulse for the F* dependency scanner to pick it up, e.g., write ``module _X = NonExistent.Module`` in F*

From cbea307267592ac273014e6859ad34f8de9b8112 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Wed, 13 May 2026 20:32:20 -0700
Subject: [PATCH 10/13] Update expected test outputs for upstream SMT error
 format change

Regenerate .output.expected files for both pulse/test/error_messages (21 files)
and pulse/test/bug-reports (21 files) to account for:

1. Upstream PR #4258 (gebner_default_smtfail): SMT failure messages now include
   inline Env/VC details instead of 'Use --query_stats for more details'

2. Parser range improvements from earlier commits in this branch: Bug267.fst
   and IntroGhost.fst show tighter error ranges due to the
   withBindersOpt parser fix

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/test/bug-reports/Bug267.fst.output.expected    |  2 +-
 .../test/bug-reports/IntroGhost.fst.output.expected  |  2 +-
 .../AssertExtraContext.fst.output.expected           |  5 +++--
 .../error_messages/ClosureError.fst.output.expected  | 12 ++++++++++--
 .../error_messages/ExistsIntro.fst.output.expected   |  5 +++--
 .../error_messages/FoldError.fst.output.expected     |  5 +++--
 .../IfBranchMismatch.fst.output.expected             | 12 ++++++++----
 .../IllTypedInvariant.fst.output.expected            |  5 +++--
 .../error_messages/IllTypedSpec.fst.output.expected  |  2 +-
 .../IntroExistsFail.fst.output.expected              |  5 +++--
 .../InvariantPayload.fst.output.expected             |  5 +++--
 .../error_messages/LambdaArg.fst.output.expected     |  2 +-
 .../MatchBranchMismatch.fst.output.expected          | 11 +++++++----
 .../error_messages/MultiError.fst.output.expected    |  5 +++--
 .../error_messages/NestedBlock.fst.output.expected   |  9 +++++----
 .../error_messages/NestedCall.fst.output.expected    |  5 +++--
 .../PrePostMismatch.fst.output.expected              |  5 +++--
 .../ReturnImplicit.fst.output.expected               |  8 ++++----
 .../error_messages/RewriteFail.fst.output.expected   |  5 +++--
 .../error_messages/SequenceError.fst.output.expected |  8 ++++++--
 .../SubtypingFailure.fst.output.expected             | 11 ++++-------
 .../WhileInvPreservation.fst.output.expected         | 11 +++++++++--
 .../WithLocalError.fst.output.expected               |  2 +-
 23 files changed, 88 insertions(+), 54 deletions(-)

diff --git a/pulse/test/bug-reports/Bug267.fst.output.expected b/pulse/test/bug-reports/Bug267.fst.output.expected
index da251fb87ba..cadbc3c3233 100644
--- a/pulse/test/bug-reports/Bug267.fst.output.expected
+++ b/pulse/test/bug-reports/Bug267.fst.output.expected
@@ -21,7 +21,7 @@
   - Also see: Prims.fst(165,27-165,38)
   - See also Bug267.fst(58,4-58,8)
 
-* Info at Bug267.fst(62,53-63,17):
+* Info at Bug267.fst(63,2-63,17):
   - Expected failure:
   - Tactic failed
   - Cannot prove:
diff --git a/pulse/test/bug-reports/IntroGhost.fst.output.expected b/pulse/test/bug-reports/IntroGhost.fst.output.expected
index f149f0fa0d8..7c23a672481 100644
--- a/pulse/test/bug-reports/IntroGhost.fst.output.expected
+++ b/pulse/test/bug-reports/IntroGhost.fst.output.expected
@@ -6,7 +6,7 @@
   - In the context:
       my_inv _b5 r
 
-* Info at IntroGhost.fst(84,46-87,24):
+* Info at IntroGhost.fst(87,2-87,24):
   - Expected failure:
   - Tactic failed
   - Cannot prove:
diff --git a/pulse/test/error_messages/AssertExtraContext.fst.output.expected b/pulse/test/error_messages/AssertExtraContext.fst.output.expected
index dcf086c5ed4..0a8afa3a419 100644
--- a/pulse/test/error_messages/AssertExtraContext.fst.output.expected
+++ b/pulse/test/error_messages/AssertExtraContext.fst.output.expected
@@ -2,6 +2,7 @@
   - Expected failure:
   - Failed to prove pure property: 0 > 0
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
 
diff --git a/pulse/test/error_messages/ClosureError.fst.output.expected b/pulse/test/error_messages/ClosureError.fst.output.expected
index 90ab338b9d5..07273a8c66f 100644
--- a/pulse/test/error_messages/ClosureError.fst.output.expected
+++ b/pulse/test/error_messages/ClosureError.fst.output.expected
@@ -4,7 +4,15 @@
   - Pulse.Lib.Reference.pts_to r 0
   - Pulse.Lib.Reference.pts_to r 1
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int)
+      (helper
+        :
+        _: Prims.unit
+          -> fn
+               requires Pulse.Class.PtsTo.pts_to r 1
+               ensures Pulse.Class.PtsTo.pts_to r 1)
+  - VC = Pulse.Lib.Reference.pts_to r 0 == Pulse.Lib.Reference.pts_to r 1
   - See also ClosureError.fst(17,2-18,4)
 
diff --git a/pulse/test/error_messages/ExistsIntro.fst.output.expected b/pulse/test/error_messages/ExistsIntro.fst.output.expected
index f41d1e7ee25..bd00eac2064 100644
--- a/pulse/test/error_messages/ExistsIntro.fst.output.expected
+++ b/pulse/test/error_messages/ExistsIntro.fst.output.expected
@@ -2,6 +2,7 @@
   - Expected failure:
   - Failed to prove pure property: 5 > 10
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
 
diff --git a/pulse/test/error_messages/FoldError.fst.output.expected b/pulse/test/error_messages/FoldError.fst.output.expected
index 8abdbc4f321..13c45e6a690 100644
--- a/pulse/test/error_messages/FoldError.fst.output.expected
+++ b/pulse/test/error_messages/FoldError.fst.output.expected
@@ -2,6 +2,7 @@
   - Expected failure:
   - Failed to prove pure property: false
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
 
diff --git a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
index ed0e740d1ef..d51ff01a098 100644
--- a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
+++ b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
@@ -1,10 +1,14 @@
-* Info at IfBranchMismatch.fst(14,4-14,8):
+* Info at IfBranchMismatch.fst(11,2-14,8):
   - Expected failure:
   - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to r 2
   - Pulse.Lib.Reference.pts_to r 1
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
-  - See also IfBranchMismatch.fst(14,4-14,10)
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (b : Prims.bool)
+      (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false))
+      (_if_br : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+  - See also IfBranchMismatch.fst(11,2-14,10)
 
diff --git a/pulse/test/error_messages/IllTypedInvariant.fst.output.expected b/pulse/test/error_messages/IllTypedInvariant.fst.output.expected
index b46eac74f7f..d8db94a3ccc 100644
--- a/pulse/test/error_messages/IllTypedInvariant.fst.output.expected
+++ b/pulse/test/error_messages/IllTypedInvariant.fst.output.expected
@@ -2,6 +2,7 @@
   - Expected failure:
   - Failed to prove pure property: true /\ true /\ false
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (uu___0 : Prims.unit) (i : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
 
diff --git a/pulse/test/error_messages/IllTypedSpec.fst.output.expected b/pulse/test/error_messages/IllTypedSpec.fst.output.expected
index 7ef194bf604..abf5dd155f5 100644
--- a/pulse/test/error_messages/IllTypedSpec.fst.output.expected
+++ b/pulse/test/error_messages/IllTypedSpec.fst.output.expected
@@ -1,6 +1,6 @@
 * Info at IllTypedSpec.fst(8,11-8,12):
   - Expected failure:
-  - Ill-typed term: x
+  - Ill-typed term
   - Expected expression of type Pulse.Lib.Core.slprop
     got expression x
     of type Prims.int
diff --git a/pulse/test/error_messages/IntroExistsFail.fst.output.expected b/pulse/test/error_messages/IntroExistsFail.fst.output.expected
index 6e4865a5a6b..b2dd425914b 100644
--- a/pulse/test/error_messages/IntroExistsFail.fst.output.expected
+++ b/pulse/test/error_messages/IntroExistsFail.fst.output.expected
@@ -2,6 +2,7 @@
   - Expected failure:
   - Failed to prove pure property: 0 > 0
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
 
diff --git a/pulse/test/error_messages/InvariantPayload.fst.output.expected b/pulse/test/error_messages/InvariantPayload.fst.output.expected
index be66a624138..ebca7a8c6ed 100644
--- a/pulse/test/error_messages/InvariantPayload.fst.output.expected
+++ b/pulse/test/error_messages/InvariantPayload.fst.output.expected
@@ -2,6 +2,7 @@
   - Expected failure:
   - Failed to prove pure property: 0 > 0
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
 
diff --git a/pulse/test/error_messages/LambdaArg.fst.output.expected b/pulse/test/error_messages/LambdaArg.fst.output.expected
index 96c4318c9a1..207e48596b7 100644
--- a/pulse/test/error_messages/LambdaArg.fst.output.expected
+++ b/pulse/test/error_messages/LambdaArg.fst.output.expected
@@ -1,6 +1,6 @@
 * Info at LambdaArg.fst(18,2-18,11):
   - Expected failure:
-  - Ill-typed term: takes_two 1 2 3
+  - Ill-typed term
   - Expected a function.
   - Got an expression of type:
       fn
diff --git a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
index 73268388dac..b2df78cedcc 100644
--- a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
+++ b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
@@ -1,10 +1,13 @@
-* Info at MatchBranchMismatch.fst(13,11-13,15):
+* Info at MatchBranchMismatch.fst(11,2-13,15):
   - Expected failure:
   - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to r 2
   - Pulse.Lib.Reference.pts_to r 1
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
-  - See also MatchBranchMismatch.fst(13,11-13,17)
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (x : Prims.int)
+      (branch equality : Prims.squash (x == 1)) (_br : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+  - See also MatchBranchMismatch.fst(11,2-13,17)
 
diff --git a/pulse/test/error_messages/MultiError.fst.output.expected b/pulse/test/error_messages/MultiError.fst.output.expected
index ae967d9728a..6043a7f8030 100644
--- a/pulse/test/error_messages/MultiError.fst.output.expected
+++ b/pulse/test/error_messages/MultiError.fst.output.expected
@@ -2,6 +2,7 @@
   - Expected failure:
   - Failed to prove pure property: false
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+  - VC = Prims.l_False
 
diff --git a/pulse/test/error_messages/NestedBlock.fst.output.expected b/pulse/test/error_messages/NestedBlock.fst.output.expected
index 233684d48b8..e00db1523b8 100644
--- a/pulse/test/error_messages/NestedBlock.fst.output.expected
+++ b/pulse/test/error_messages/NestedBlock.fst.output.expected
@@ -1,9 +1,10 @@
-* Info at NestedBlock.fst(12,4-12,22):
+* Info at NestedBlock.fst(14,2-14,4):
   - Expected failure:
   - Could not prove equality of:
-  - Pulse.Lib.Reference.pts_to r 0
   - Pulse.Lib.Reference.pts_to r 1
+  - Pulse.Lib.Reference.pts_to r 0
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Pulse.Lib.Reference.pts_to r 1 == Pulse.Lib.Reference.pts_to r 0
 
diff --git a/pulse/test/error_messages/NestedCall.fst.output.expected b/pulse/test/error_messages/NestedCall.fst.output.expected
index 0f24c09f5db..6b40aac9b76 100644
--- a/pulse/test/error_messages/NestedCall.fst.output.expected
+++ b/pulse/test/error_messages/NestedCall.fst.output.expected
@@ -4,7 +4,8 @@
   - Pulse.Lib.Reference.pts_to r 5
   - Pulse.Lib.Reference.pts_to r 0
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Pulse.Lib.Reference.pts_to r 5 == Pulse.Lib.Reference.pts_to r 0
   - See also NestedCall.fst(18,2-19,4)
 
diff --git a/pulse/test/error_messages/PrePostMismatch.fst.output.expected b/pulse/test/error_messages/PrePostMismatch.fst.output.expected
index 0cf1a917e9f..1061f4c0beb 100644
--- a/pulse/test/error_messages/PrePostMismatch.fst.output.expected
+++ b/pulse/test/error_messages/PrePostMismatch.fst.output.expected
@@ -4,6 +4,7 @@
   - Pulse.Lib.Reference.pts_to r 1
   - Pulse.Lib.Reference.pts_to r 42
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 1 == Pulse.Lib.Reference.pts_to r 42
 
diff --git a/pulse/test/error_messages/ReturnImplicit.fst.output.expected b/pulse/test/error_messages/ReturnImplicit.fst.output.expected
index 6c1c31c9497..f9e2fd24e7e 100644
--- a/pulse/test/error_messages/ReturnImplicit.fst.output.expected
+++ b/pulse/test/error_messages/ReturnImplicit.fst.output.expected
@@ -1,9 +1,9 @@
 * Info at ReturnImplicit.fst(12,2-12,4):
   - Expected failure:
-  - Ill-typed term: - 1
-  - Expected a term of type nat
+  - Ill-typed term
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (uu___0 : Prims.unit)
+  - VC = Prims.l_False
   - Also see: Prims.fst(642,18-642,24)
 
diff --git a/pulse/test/error_messages/RewriteFail.fst.output.expected b/pulse/test/error_messages/RewriteFail.fst.output.expected
index cf1a913c354..94833d73aaf 100644
--- a/pulse/test/error_messages/RewriteFail.fst.output.expected
+++ b/pulse/test/error_messages/RewriteFail.fst.output.expected
@@ -4,6 +4,7 @@
   - pts_to r 0
   - pts_to r 1
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Pulse.Class.PtsTo.pts_to r 0 == Pulse.Class.PtsTo.pts_to r 1
 
diff --git a/pulse/test/error_messages/SequenceError.fst.output.expected b/pulse/test/error_messages/SequenceError.fst.output.expected
index af995a4267e..6f8b8dc5af9 100644
--- a/pulse/test/error_messages/SequenceError.fst.output.expected
+++ b/pulse/test/error_messages/SequenceError.fst.output.expected
@@ -4,6 +4,10 @@
   - Pulse.Lib.Reference.pts_to r2 2
   - Pulse.Lib.Reference.pts_to r2 1
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+      (r1 : Pulse.Lib.Reference.ref Prims.int)
+      (r2 : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r2 2 == Pulse.Lib.Reference.pts_to r2 1
 
diff --git a/pulse/test/error_messages/SubtypingFailure.fst.output.expected b/pulse/test/error_messages/SubtypingFailure.fst.output.expected
index 5c058ee6cf2..9bc10f32976 100644
--- a/pulse/test/error_messages/SubtypingFailure.fst.output.expected
+++ b/pulse/test/error_messages/SubtypingFailure.fst.output.expected
@@ -1,12 +1,9 @@
 * Info at SubtypingFailure.fst(18,2-18,10):
   - Expected failure:
-  - Ill-typed term: callee x
-  - Expected a term of type
-      fn
-        requires emp
-        ensures emp
+  - Ill-typed term
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env = (x : Prims.int)
+  - VC = x >= 0
   - Also see: Prims.fst(642,18-642,24)
 
diff --git a/pulse/test/error_messages/WhileInvPreservation.fst.output.expected b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected
index 7fb891eb6a9..6a896a2cf21 100644
--- a/pulse/test/error_messages/WhileInvPreservation.fst.output.expected
+++ b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected
@@ -4,7 +4,14 @@
   - Pulse.Lib.Reference.pts_to i 2
   - Pulse.Lib.Reference.pts_to i 0
   - Assertion failed
-  - The SMT solver could not prove the query. Use --query_stats for more
-    details.
+  - The SMT solver could not prove the query.
+  - Env =
+      (uu___0 : Prims.unit) (i : Pulse.Lib.Reference.ref Prims.int)
+      (meas : Prims.unit) (__ : Prims.squash (true /\ true))
+      (__ : Prims.squash (meas == ())) (__ : Prims.squash (true == true))
+      (__anf0 : Prims.int)
+      (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p __anf0 0))
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to i 2 == Pulse.Lib.Reference.pts_to i 0
   - See also WhileInvPreservation.fst(15,4-15,13)
 
diff --git a/pulse/test/error_messages/WithLocalError.fst.output.expected b/pulse/test/error_messages/WithLocalError.fst.output.expected
index e67a562991c..5bddca1f74f 100644
--- a/pulse/test/error_messages/WithLocalError.fst.output.expected
+++ b/pulse/test/error_messages/WithLocalError.fst.output.expected
@@ -1,6 +1,6 @@
 * Info at WithLocalError.fst(13,21-13,22):
   - Expected failure:
-  - Ill-typed term: pure (x == 0)
+  - Ill-typed term
   - Expected expression of type Pulse.Lib.Reference.ref Prims.int
     got expression 0
     of type Prims.int

From c5c44d584f8d753a6bef6a55680b241b5aa8af73 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Wed, 13 May 2026 20:37:08 -0700
Subject: [PATCH 11/13] Remove unused check_atom_equiv function

Leftover from the reverted eager atom equivalence check experiment.
The inline logic in prove_atom_result's deferred closure does the same work.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/src/checker/Pulse.Checker.Prover.fst | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst
index 28a3e6305c6..8f1440224ed 100644
--- a/pulse/src/checker/Pulse.Checker.Prover.fst
+++ b/pulse/src/checker/Pulse.Checker.Prover.fst
@@ -935,15 +935,6 @@ let is_unamb g (cands: list (int & slprop_view)) : T.Tac bool =
 
 let dup_lid = ["Pulse"; "Class"; "Duplicable"; "dup"]
 
-// Check that ctxt_t and goal are equivalent slprops, and (if dup) that the
-// dup token typechecks.
-let check_atom_equiv (g: env) (ctxt_t goal: T.term) (dup: bool) : T.Tac unit =
-  let _ = check_slprop_equiv_ext (RU.range_of_term goal) g ctxt_t goal in
-  if dup then
-    ignore (compute_term_type g
-      (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
-        [ctxt_t, R.Q_Explicit; unit_const, R.Q_Explicit]))
-
 let prove_atom_result (g: env)
     (ctxt: slprop_view { Atom? ctxt }) (rest_ctxt: list slprop_view)
     (#ctxt0: list slprop_view) // ctxt0 == ctxt ** rest_ctxt

From ad4d24ce05183228e2818ba9029191dec60d2062 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Thu, 14 May 2026 17:06:29 -0700
Subject: [PATCH 12/13] Fix CI: update expected outputs, sort namespace list
 for determinism

- RewriteNopWarning.fst: (12,1-13,21) -> (13,2-13,21) due to parser fix
- Test.RewriteBy.fst: (31,1-37,8) -> (32,2-37,8) due to parser fix
- FStarC.Parser.Dep: sort valid_namespaces list for deterministic output
- OpenScopeError.fst: regenerated with sorted namespace list

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 .../error_messages/OpenScopeError.fst.output.expected     | 8 +++++++-
 pulse/test/nolib/RewriteNopWarning.fst.output.expected    | 4 ++--
 pulse/test/nolib/Test.RewriteBy.fst.output.expected       | 2 +-
 src/parser/FStarC.Parser.Dep.fst                          | 2 +-
 4 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/pulse/test/error_messages/OpenScopeError.fst.output.expected b/pulse/test/error_messages/OpenScopeError.fst.output.expected
index 985b7e0f047..cbb7efd920d 100644
--- a/pulse/test/error_messages/OpenScopeError.fst.output.expected
+++ b/pulse/test/error_messages/OpenScopeError.fst.output.expected
@@ -1,6 +1,12 @@
+* Warning 285 at OpenScopeError.fst(11,19-11,25):
+  - Module not found: NonExistent.Module
+
 Could not resolve namespace NonExistent.Module
- valid namespaces are ["fstar.class.ord", "fstar.finiteset", "fstar.stubs.tactics.v2", "fstar.tactics.bv", "fstar.algebra.commmonoid", "fstar.stubs.typechecker", "fstar.stubs", "fstar.finitemap", "fstar.tactics.canon", "fstar.seq", "fstar.reflection.termeq", "pulse.lib.sort", "fstar.tactics.v2", "fstar.tactics.canoncommmonoidsimple", "fstar.sealed", "fstar.class.eq", "fstar.stubs.syntax", "fstar.algebra", "fstar.stubs.tactics.types", "pulse.lib.reference", "fstar.class", "fstar.list", "fstar.vector", "fstar.list.tot", "fstar.reflection.typing", "pulse.lib.seqmatch", "pulse.lib.trade", "pulse.class", "fstar.stubs.errors", "pulse.lib.hashtable", "fstar.reflection", "fstar.int.cast", "pulse.lib", "fstar.tactics.logic", "pulse.lib.core", "pulse.lib.forall", "fstar.int", "fstar", "fstar.tactics", "fstar.stubs.reflection.v2", "pulsecore", "pulse.lib.spec", "fstar.reflection.v2", "fstar.wellfounded", "fstar.stubs.reflection", "fstar.stubs.tactics", "pulse.c", "fstar.sequence", "fstar.classical", "pulse", "fstar.math", "fstar.list.pure", "fstar.reflection.v2.derived", "pulse.lib.pcm", "fstar.universe", "pulse.lib.slice", "fstar.algebra.commmonoid.fold", "pulse.c.types.struct", "pulse.c.types.array", "pulse.lib.array", "pulse.lib.linkedlist", "fstar.cardinality", "fstar.constanttime", "pulse.c.types", "pulse.lib.swap", "fstar.monotonic", "fstar.pure", "fstar.class.totalorder", "fstar.immutablearray", "fstar.pervasives", "pulse.lib.sort.merge"]
+ valid namespaces are ["fstar", "fstar.algebra", "fstar.algebra.commmonoid", "fstar.algebra.commmonoid.fold", "fstar.cardinality", "fstar.class", "fstar.class.eq", "fstar.class.ord", "fstar.class.totalorder", "fstar.classical", "fstar.constanttime", "fstar.finitemap", "fstar.finiteset", "fstar.immutablearray", "fstar.int", "fstar.int.cast", "fstar.list", "fstar.list.pure", "fstar.list.tot", "fstar.math", "fstar.monotonic", "fstar.pervasives", "fstar.pure", "fstar.reflection", "fstar.reflection.termeq", "fstar.reflection.typing", "fstar.reflection.v2", "fstar.reflection.v2.derived", "fstar.sealed", "fstar.seq", "fstar.sequence", "fstar.stubs", "fstar.stubs.errors", "fstar.stubs.reflection", "fstar.stubs.reflection.v2", "fstar.stubs.syntax", "fstar.stubs.tactics", "fstar.stubs.tactics.types", "fstar.stubs.tactics.v2", "fstar.stubs.typechecker", "fstar.tactics", "fstar.tactics.bv", "fstar.tactics.canon", "fstar.tactics.canoncommmonoidsimple", "fstar.tactics.logic", "fstar.tactics.v2", "fstar.universe", "fstar.vector", "fstar.wellfounded", "pulse", "pulse.c", "pulse.c.types", "pulse.c.types.array", "pulse.c.types.struct", "pulse.class", "pulse.lib", "pulse.lib.array", "pulse.lib.core", "pulse.lib.forall", "pulse.lib.hashtable", "pulse.lib.linkedlist", "pulse.lib.pcm", "pulse.lib.reference", "pulse.lib.seqmatch", "pulse.lib.slice", "pulse.lib.sort", "pulse.lib.sort.merge", "pulse.lib.spec", "pulse.lib.swap", "pulse.lib.trade", "pulsecore"]
 * Info at OpenScopeError.fst(11,2-11,25):
   - Expected failure:
   - Failed to open namespace NonExistent.Module; You may need to bind this namespace outside Pulse for the F* dependency scanner to pick it up, e.g., write ``module _X = NonExistent.Module`` in F*
 
+* Warning 285 at OpenScopeError.fst(11,19-11,25):
+  - Module not found: NonExistent.Module
+
diff --git a/pulse/test/nolib/RewriteNopWarning.fst.output.expected b/pulse/test/nolib/RewriteNopWarning.fst.output.expected
index 1132fb77c38..68ef378155c 100644
--- a/pulse/test/nolib/RewriteNopWarning.fst.output.expected
+++ b/pulse/test/nolib/RewriteNopWarning.fst.output.expected
@@ -1,9 +1,9 @@
-* Warning <unknown> at RewriteNopWarning.fst(12,1-13,21):
+* Warning <unknown> at RewriteNopWarning.fst(13,2-13,21):
   - No rewrites performed.
   - Rewriting in:
       foo 1
 
-* Warning <unknown> at RewriteNopWarning.fst(21,1-22,22):
+* Warning <unknown> at RewriteNopWarning.fst(22,2-22,22):
   - No rewrites performed.
   - Rewriting in:
       foo y ** foo 1
diff --git a/pulse/test/nolib/Test.RewriteBy.fst.output.expected b/pulse/test/nolib/Test.RewriteBy.fst.output.expected
index c2b9fb61c4c..dc23de5171d 100644
--- a/pulse/test/nolib/Test.RewriteBy.fst.output.expected
+++ b/pulse/test/nolib/Test.RewriteBy.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Test.RewriteBy.fst(31,1-37,8):
+* Info at Test.RewriteBy.fst(32,2-37,8):
   - Expected failure:
   - rewrite: could not prove equality of
   - p
diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst
index 4e4076765fc..15534ed099c 100644
--- a/src/parser/FStarC.Parser.Dep.fst
+++ b/src/parser/FStarC.Parser.Dep.fst
@@ -583,7 +583,7 @@ let is_valid_namespace deps ns =
   let res = Some? (SMap.try_find deps.valid_namespaces (String.lowercase (Ident.string_of_lid ns))) in
   if not res
   then Format.print2 "Could not resolve namespace %s\n valid namespaces are %s\n"
-      (show ns) (show <| SMap.keys deps.valid_namespaces);
+      (show ns) (show <| List.sortWith String.compare (SMap.keys deps.valid_namespaces));
   res
 
 let interface_of deps key = 

From 4f753d2203397e32c23aae69d218d9e515f3d375 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Thu, 14 May 2026 20:42:55 -0700
Subject: [PATCH 13/13] Pulse: fix error localization for deferred atom
 equivalence checks
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The prover's prove_atom_result defers check_slprop_equiv_ext into a
continuation closure that executes after the with_error_bound scope
has exited, causing errors to inherit the wider enclosing range.

Fix: capture the active error_range_bound when the atom match is made,
and restore it (via with_saved_bound) when the deferred closure runs.
This is the same pattern already used for prove_pure/prove_with_pure.

Impact on error localization:
- IfBranchMismatch: (11,2-14,8) -> (14,4-14,8) — points to the exact
  mismatched statement instead of the whole if-else block
- MatchBranchMismatch: (11,2-13,15) -> (13,11-13,15) — points to the
  exact mismatched statement instead of the whole match
- TerminalAction: (11,2-12,6) -> (12,2-12,6) — points to the terminal
  statement instead of the enclosing block

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/src/checker/Pulse.Checker.Prover.fst    | 17 ++++++++-----
 .../test/error_messages/IfBranchMismatch.fst  | 20 +++++++++++++--
 .../IfBranchMismatch.fst.output.expected      | 17 +++++++++++--
 .../MatchBranchMismatch.fst.output.expected   |  4 +--
 .../OpenScopeError.fst.output.expected        |  6 -----
 .../TerminalActionPostConditionMismatch.fst   | 24 ++++++++++++++++++
 ...nPostConditionMismatch.fst.output.expected | 25 +++++++++++++++++++
 7 files changed, 95 insertions(+), 18 deletions(-)
 create mode 100644 pulse/test/error_messages/TerminalActionPostConditionMismatch.fst
 create mode 100644 pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected

diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst
index 8f1440224ed..0f057cb1a2a 100644
--- a/pulse/src/checker/Pulse.Checker.Prover.fst
+++ b/pulse/src/checker/Pulse.Checker.Prover.fst
@@ -942,13 +942,18 @@ let prove_atom_result (g: env)
     T.Tac (prover_result g ctxt0 [goal]) =
   let Atom _ dup _ _ = ctxt in
   let goal = elab_slprop goal in
+  let saved_bound = RU.get_error_bound () in
   (| g, (if dup then rest_ctxt@[ctxt] else rest_ctxt), [], [ctxt], fun g' ->
-    let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
-    (if dup then
-      // Check that we can indeed synthesize a duplicable instance
-      ignore (compute_term_type g
-        (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
-          [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
+    // Restore the error bound that was active when this atom was matched.
+    // This closure is evaluated lazily (via cont_elab_thunk) after the
+    // original with_error_bound scope has exited.
+    with_saved_bound saved_bound (fun () ->
+      let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
+      (if dup then
+        // Check that we can indeed synthesize a duplicable instance
+        ignore (compute_term_type g
+          (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
+            [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit]))));
     cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
 
 // this matches atoms when they're the only unifiable pair
diff --git a/pulse/test/error_messages/IfBranchMismatch.fst b/pulse/test/error_messages/IfBranchMismatch.fst
index 7cfbe86c98b..513441a2e21 100644
--- a/pulse/test/error_messages/IfBranchMismatch.fst
+++ b/pulse/test/error_messages/IfBranchMismatch.fst
@@ -9,8 +9,24 @@ fn if_branch_mismatch (r: ref int) (b: bool)
   ensures pts_to r 1
 {
   if b {
-    r := 1
+    r := 1;
   } else {
-    r := 2  // ERROR: this branch gives pts_to r 2, should be 1
+    r := 2; // ERROR: this branch gives pts_to r 2, should be 1
+  }
+}
+
+
+
+// If branches produce different resources
+[@@expect_failure [19]]
+fn if_branch_mismatch_localized (r: ref int) (b: bool)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  if b {
+    r := 1;
+  } else {
+    r := 2;
+    () // ERROR: this branch gives pts_to r 2, should be 1
   }
 }
diff --git a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
index d51ff01a098..31b0b93dd8d 100644
--- a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
+++ b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at IfBranchMismatch.fst(11,2-14,8):
+* Info at IfBranchMismatch.fst(14,4-14,8):
   - Expected failure:
   - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to r 2
@@ -10,5 +10,18 @@
       (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false))
       (_if_br : Prims.unit)
   - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
-  - See also IfBranchMismatch.fst(11,2-14,10)
+  - See also IfBranchMismatch.fst(14,4-14,10)
+
+* Info at IfBranchMismatch.fst(30,4-30,6):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (b : Prims.bool)
+      (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false))
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
 
diff --git a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
index b2df78cedcc..6398b24e0a4 100644
--- a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
+++ b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at MatchBranchMismatch.fst(11,2-13,15):
+* Info at MatchBranchMismatch.fst(13,11-13,15):
   - Expected failure:
   - Could not prove equality of:
   - Pulse.Lib.Reference.pts_to r 2
@@ -9,5 +9,5 @@
       (r : Pulse.Lib.Reference.ref Prims.int) (x : Prims.int)
       (branch equality : Prims.squash (x == 1)) (_br : Prims.unit)
   - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
-  - See also MatchBranchMismatch.fst(11,2-13,17)
+  - See also MatchBranchMismatch.fst(13,11-13,17)
 
diff --git a/pulse/test/error_messages/OpenScopeError.fst.output.expected b/pulse/test/error_messages/OpenScopeError.fst.output.expected
index cbb7efd920d..fcd9e7f8893 100644
--- a/pulse/test/error_messages/OpenScopeError.fst.output.expected
+++ b/pulse/test/error_messages/OpenScopeError.fst.output.expected
@@ -1,12 +1,6 @@
-* Warning 285 at OpenScopeError.fst(11,19-11,25):
-  - Module not found: NonExistent.Module
-
 Could not resolve namespace NonExistent.Module
  valid namespaces are ["fstar", "fstar.algebra", "fstar.algebra.commmonoid", "fstar.algebra.commmonoid.fold", "fstar.cardinality", "fstar.class", "fstar.class.eq", "fstar.class.ord", "fstar.class.totalorder", "fstar.classical", "fstar.constanttime", "fstar.finitemap", "fstar.finiteset", "fstar.immutablearray", "fstar.int", "fstar.int.cast", "fstar.list", "fstar.list.pure", "fstar.list.tot", "fstar.math", "fstar.monotonic", "fstar.pervasives", "fstar.pure", "fstar.reflection", "fstar.reflection.termeq", "fstar.reflection.typing", "fstar.reflection.v2", "fstar.reflection.v2.derived", "fstar.sealed", "fstar.seq", "fstar.sequence", "fstar.stubs", "fstar.stubs.errors", "fstar.stubs.reflection", "fstar.stubs.reflection.v2", "fstar.stubs.syntax", "fstar.stubs.tactics", "fstar.stubs.tactics.types", "fstar.stubs.tactics.v2", "fstar.stubs.typechecker", "fstar.tactics", "fstar.tactics.bv", "fstar.tactics.canon", "fstar.tactics.canoncommmonoidsimple", "fstar.tactics.logic", "fstar.tactics.v2", "fstar.universe", "fstar.vector", "fstar.wellfounded", "pulse", "pulse.c", "pulse.c.types", "pulse.c.types.array", "pulse.c.types.struct", "pulse.class", "pulse.lib", "pulse.lib.array", "pulse.lib.core", "pulse.lib.forall", "pulse.lib.hashtable", "pulse.lib.linkedlist", "pulse.lib.pcm", "pulse.lib.reference", "pulse.lib.seqmatch", "pulse.lib.slice", "pulse.lib.sort", "pulse.lib.sort.merge", "pulse.lib.spec", "pulse.lib.swap", "pulse.lib.trade", "pulsecore"]
 * Info at OpenScopeError.fst(11,2-11,25):
   - Expected failure:
   - Failed to open namespace NonExistent.Module; You may need to bind this namespace outside Pulse for the F* dependency scanner to pick it up, e.g., write ``module _X = NonExistent.Module`` in F*
 
-* Warning 285 at OpenScopeError.fst(11,19-11,25):
-  - Module not found: NonExistent.Module
-
diff --git a/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst
new file mode 100644
index 00000000000..a52a78f36df
--- /dev/null
+++ b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst
@@ -0,0 +1,24 @@
+module TerminalActionPostConditionMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Terminal action with postcondition that doesn't match the actual state
+[@@expect_failure [19]]
+fn terminal_action_mismatch (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 0;
+  r := 2;
+}
+
+// Same error, with explicit () at end — both should localize to r := 2
+[@@expect_failure [19]]
+fn terminal_action_mismatch_localized (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 0;
+  r := 2;
+  ()
+}
\ No newline at end of file
diff --git a/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected
new file mode 100644
index 00000000000..2baeab648ef
--- /dev/null
+++ b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected
@@ -0,0 +1,25 @@
+* Info at TerminalActionPostConditionMismatch.fst(12,2-12,6):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+  - See also TerminalActionPostConditionMismatch.fst(12,2-12,8)
+
+* Info at TerminalActionPostConditionMismatch.fst(23,2-23,4):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+