Skip redundant check_slprop_with_core in purify_and_check_spec and bind_res_and_post_typing

In purify_and_check_spec: purify_spec already elaborates each atom via
tc_term_phase1_with_type (which includes core_check_term). The star-composition
of slprop-typed atoms is trivially slprop-typed, so the full-term
core_check_term recheck was redundant. For InsertionSort's inner while
invariant, this single call took 7.3s.

In bind_res_and_post_typing: each bind in a sequential composition called
check_slprop_with_core on the accumulated postcondition. With N statements,
the same growing post was kernel-checked N times (O(n^2) behavior). The
postcondition type was already verified when the sub-computation was checked.
For InsertionSort, 18 expensive calls totaled ~4.1s.

Combined savings: ~11.2s (core_check_term: 11.6s -> 0.44s, 96% reduction)
Total InsertionSort verification time: 43.4s -> 19.5s (55% speedup)

Also adds PULSE_PROFILE_CORE env var for optional per-call timing profiling
of core_check_term in Pulse_RuntimeUtils.ml.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: nikswamy

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

@@ -423,8 +423,8 @@ let purify_spec (g: env) (ctxt: ctxt) (t0: slprop) : T.Tac slprop =
   t
 
 let purify_and_check_spec (g: env) (ctxt: ctxt) (t: slprop) =
-  // purify_spec already elaborates the term via tc_term_phase1_with_type,
-  // so we only need the core checker for validation (skip instantiate_term_implicits)
+  // purify_spec already elaborates each atom via tc_term_phase1_with_type (which
+  // includes a core_check_term). The star-composition of slprop-typed atoms is
+  // trivially slprop-typed, so a redundant full-term core_check_term is skipped.
   let t = purify_spec g ctxt t in
-  check_slprop_with_core g t;
   t

pulse/src/checker/Pulse.Typing.Combinators.fst

@@ -299,20 +299,16 @@ let bind_res_and_post_typing g c2 x post_hint
   = let s2 = st_comp_of_comp c2 in
     match post_hint with
     | NoHint | TypeHint _ -> 
-      (* We're inferring a post, so these checks are unavoidable *)
-      (* since we need to type the result in a smaller env g *)          
+      (* We're inferring a post, so check that the result universe matches *)
+      (* and the bound variable doesn't escape scope *)
+      (* The postcondition's slprop typing was already checked when the *)
+      (* sub-computation was checked, so skip redundant core_check_term *)
       let u = check_universe g s2.res in 
       if not (eq_univ u s2.u)
       then fail g None "Unexpected universe for result type"
       else if x `Set.mem` freevars (RU.deep_compress_safe s2.post)
       then fail g None (Printf.sprintf "Bound variable %d escapes scope in postcondition %s" x (P.term_to_string s2.post))
-      else (
-        let y = x in //fresh g in
-        let s2_post_opened = open_term_nv s2.post (v_as_nv y) in
-        let _ =
-          check_slprop_with_core (push_binding g y ppname_default s2.res) s2_post_opened in
-        ()
-      )
+      else ()
     | PostHint post -> 
       CU.debug g "pulse.main" (fun _ -> "bind_res_and_post_typing (with post_hint)\n");
       ()

pulse/src/ml/Pulse_RuntimeUtils.ml

@@ -272,6 +272,58 @@ let record_stats (key:string) (f: unit -> 'a utac)
 = fun ps ->
     FStarC_Stats.record key (fun () -> f () ps)
 
+(* Per-call timing distribution for core_check_term profiling *)
+let core_check_term_timings : (int * float * string * string) list ref = ref []
+let core_check_term_call_count = ref 0
+let core_check_caller_label = ref ""
+let profiling_enabled = try ignore (Sys.getenv "PULSE_PROFILE_CORE"); true with Not_found -> false
+
+let record_core_check_term_call (label:string) (f: unit -> 'a) : 'a =
+  if not profiling_enabled then f ()
+  else begin
+    let idx = !core_check_term_call_count in
+    incr core_check_term_call_count;
+    let caller = !core_check_caller_label in
+    core_check_caller_label := "";
+    let t0 = Unix.gettimeofday () in
+    let result = f () in
+    let elapsed = Unix.gettimeofday () -. t0 in
+    core_check_term_timings := (idx, elapsed, label, caller) :: !core_check_term_timings;
+    result
+  end
+
+let () = Stdlib.at_exit (fun () ->
+  if not profiling_enabled then ()
+  else
+  let timings = List.rev !core_check_term_timings in
+  if timings <> [] then begin
+    let total = List.fold_left (fun acc (_, t, _, _) -> acc +. t) 0.0 timings in
+    Printf.eprintf "\n=== core_check_term per-call distribution (%d calls, %.1fms total) ===\n"
+      (List.length timings) (total *. 1000.0);
+    (* Print histogram buckets *)
+    let buckets = [0.0; 0.001; 0.01; 0.05; 0.1; 0.5; 1.0; 5.0] in
+    let counts = List.map (fun lo ->
+      let hi = match List.find_opt (fun x -> x > lo) buckets with Some x -> x | None -> infinity in
+      let n = List.length (List.filter (fun (_, t, _, _) -> t >= lo && t < hi) timings) in
+      let sum = List.fold_left (fun acc (_, t, _, _) -> if t >= lo && t < hi then acc +. t else acc) 0.0 timings in
+      (lo, hi, n, sum)
+    ) buckets in
+    List.iter (fun (lo, hi, n, sum) ->
+      if n > 0 then
+        Printf.eprintf "  [%.0fms-%.0fms): %d calls, %.1fms total\n"
+          (lo *. 1000.0) (hi *. 1000.0) n (sum *. 1000.0)
+    ) counts;
+    (* Print the top 20 slowest calls *)
+    let sorted = List.sort (fun (_, t1, _, _) (_, t2, _, _) -> compare t2 t1) timings in
+    Printf.eprintf "\nTop 20 slowest core_check_term calls:\n";
+    List.iteri (fun i (idx, t, label, caller) ->
+      if i < 20 then
+        Printf.eprintf "  #%d: %.1fms [%s] caller=%s\n" idx (t *. 1000.0) label caller
+    ) sorted;
+    Printf.eprintf "===\n%!"
+  end
+)
+
 let stack_dump () = FStarC_Util.stack_dump()
 
 let push_options () : unit = FStarC_Options.push ()

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

@@ -3,8 +3,8 @@
   - Current context:
       some_pred x v
   - In typing environment:
-      __#403 : squash (_v_5 == v)
-      _v_5#402 : erased int
+      __#402 : squash (_v_5 == v)
+      _v_5#401 : erased int
       __#281 : squash (v == v)
       v#156 : erased int
       x#150 : R.ref int