Skip redundant phase1 TC passes when no uvars are left

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

@@ -111,7 +111,10 @@ let rec symb_eval_subterms (g:env) (ctxt: ctxt') (t:R.term) : T.Tac (bool & R.te
     let x = fresh g in
     let ppname = mk_ppname_no_range (T.unseal b.ppname) in
     let changed1, b_ty = symb_eval_subterms g ctxt b.sort in
-    let b_ty, b_u = tc_type_phase1 g b_ty in
+    let b_ty =
+      if changed1 then fst (tc_type_phase1 g b_ty)
+      else b_ty
+    in
     debug g (fun _ -> [text "symb eval subterms abs 1"; pp changed1; pp b_ty]);
     let b = { b with sort = b_ty } in
     let g' = push_binding g x ppname b.sort in
@@ -129,7 +132,10 @@ let rec symb_eval_subterms (g:env) (ctxt: ctxt') (t:R.term) : T.Tac (bool & R.te
     let x = fresh g in
     let ppname = mk_ppname_no_range (T.unseal b.ppname) in
     let changed1, b_ty = symb_eval_subterms g ctxt b.sort in
-    let b_ty, b_u = tc_type_phase1 g b_ty in
+    let b_ty =
+      if changed1 then fst (tc_type_phase1 g b_ty)
+      else b_ty
+    in
     debug g (fun _ -> [text "symb eval subterms refine 1"; pp changed1; pp b_ty]);
     let b = { b with sort = b_ty } in
     let g' = push_binding g x ppname b.sort in
@@ -280,11 +286,12 @@ let is_literally (t: term) : option term =
   | _ -> None
 
 let tc_term_phase1_with_type_twice g t ty =
-  // If we call phase1 TC only once, then the universe instantiation in
-  // coercion-inserted reveal calls remains a uvar.
   let t, eff = tc_term_phase1_with_type g t ty in
-  let t, eff = tc_term_phase1_with_type g t ty in
-  t, eff
+  // If the first TC left unresolved uvars/univars (e.g., universe instantiation
+  // in coercion-inserted reveal calls), run TC again to resolve them.
+  if RU.no_uvars_in_term t
+  then t, eff
+  else let t, eff = tc_term_phase1_with_type g t ty in t, eff
 
 let or_emp (t: option slprop) : slprop =
   match t with Some t -> t | None -> tm_emp
@@ -403,15 +410,24 @@ let purify_spec (g: env) (ctxt: ctxt) (t0: slprop) : T.Tac slprop =
   let ctxt = { ctxt; in_old = false } in
   let t = purify_spec_core g' ctxt [t] |> or_emp in
   // TODO: check that xs is not free in t
-  // If we call phase1 TC only once, then the universe instantiation in
-  // op_Exists_Star can remain unresolved.
-  let t, _ = tc_term_phase1_with_type g t tm_slprop in
+  // Only run the final tc_term_phase1_with_type if there are unresolved
+  // uvars or universe variables (e.g., in op_Exists_Star when universe
+  // annotations are missing). In most cases, per-atom TC in purify_spec_core
+  // has already fully elaborated the term.
+  let t =
+    if RU.no_uvars_in_term t
+    then t
+    else let t, _ = tc_term_phase1_with_type g t tm_slprop in t
+  in
   debug g (fun _ -> [ text "purified" ^/^ pp t0; text "to" ^/^ pp t ]);
   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)
   let t = purify_spec g ctxt t in
-  check_slprop_with_core g t;
+  // Use structural check: purify_spec already core-checked each atom via
+  // tc_term_phase1_with_type. The structural check avoids re-walking the
+  // full term tree through the kernel for slprop-typed AST nodes
+  // (Star, ExistsSL, ForallSL, etc.), only calling core_check_term on
+  // opaque Tm_FStar leaves.
+  check_slprop_with_core_structural g t;
   t

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

@@ -519,6 +519,31 @@ let check_slprop_with_core (g:env)
   core_check_term
     (push_context_no_range g "check_slprop_with_core") t T.E_Total tm_slprop
 
+// Structural slprop check: walk the Pulse term view and only fall back to
+// core_check_term for Tm_FStar (opaque) leaves. Sound because Pulse's
+// slprop constructors (Star, ExistsSL, ForallSL, WithPure, Pure, Emp, etc.)
+// are known to produce slprop-typed terms when their sub-components are slprops.
+let rec check_slprop_with_core_structural (g:env) (t:term)
+: T.Tac unit
+= match inspect_term t with
+  | Tm_Star l r ->
+    check_slprop_with_core_structural g l;
+    check_slprop_with_core_structural g r
+  | Tm_ExistsSL _ _ _
+  | Tm_ForallSL _ _ _
+  | Tm_WithPure _ _ _
+  | Tm_Pure _
+  | Tm_Emp
+  | Tm_Inv _ _
+  | Tm_SLProp
+  | Tm_IsUnreachable
+  | Tm_EmpInames
+  | Tm_Inames -> ()
+  | _ ->
+    // Opaque term: fall back to full core check
+    core_check_term
+      (push_context_no_range g "check_slprop_with_core") t T.E_Total tm_slprop
+
 
 
 let non_informative_class_typing

pulse/src/checker/Pulse.Checker.Pure.fsti

@@ -83,6 +83,10 @@ val check_slprop_with_core (g:env)
                           (t:term)
   : T.Tac unit
 
+val check_slprop_with_core_structural (g:env)
+                                      (t:term)
+  : T.Tac unit
+
 val try_get_non_informative_witness (g:env) (u:universe) (t:term)
   : T.Tac (option (non_informative_t g u t))
 

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

@@ -299,18 +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 *)          
       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 y = x 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
+          check_slprop_with_core_structural (push_binding g y ppname_default s2.res) s2_post_opened in
         ()
       )
     | PostHint post -> 

pulse/src/ml/Pulse_RuntimeUtils.ml

@@ -189,6 +189,7 @@ let lax_check_term_with_unknown_universes (g:TcEnv.env) (e:S.term)
     | Some (Some x) -> Some x
 
 let tc_term_phase1 (g:TcEnv.env) (e:S.term) (instantiate_imp:bool) =
+  FStarC_Stats.record "Pulse.tc_term_phase1" (fun () ->
   let issues, res = FStarC_Errors.catch_errors (fun _ ->
     let g = TcEnv.set_range g e.pos in
     let g = {g with phase1=true; admit=true; instantiate_imp} in
@@ -199,7 +200,7 @@ let tc_term_phase1 (g:TcEnv.env) (e:S.term) (instantiate_imp:bool) =
     let guard = FStarC_TypeChecker_Rel.solve_deferred_constraints g guard in
     let guard = FStarC_TypeChecker_Rel.resolve_implicits g guard in
     e, t, eff) in
-  res, issues
+  res, issues)
 
 let teq_nosmt_force (g:TcEnv.env) (ty1:S.term) (ty2:S.term) =
   let issues, res = FStarC_Errors.catch_errors (fun _ ->
@@ -271,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/Bug174.fst.output.expected

@@ -2,7 +2,7 @@
   - Expected failure:
   - Tactic failed
   - Cannot prove:
-      Pulse.Lib.Reference.pts_to r (*?u173*)_
+      Pulse.Lib.Reference.pts_to r (*?u133*)_
   - In the context:
       Pulse.Lib.Reference.pts_to r v
 

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

@@ -11,12 +11,12 @@
   - Current context:
       emp
   - In typing environment:
-      __#66 : squash (__ == my_intro l_False)
-      __#65 :
+      __#58 : squash (__ == my_intro l_False)
+      __#57 :
         ghost fn
           requires pure l_False
           ensures post ()
-      uu___0#50 : unit
+      uu___0#42 : unit
 
-      goto _return#54 requires emp
+      goto _return#46 requires emp
 

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

@@ -2,8 +2,8 @@
   - Expected failure:
   - Tactic failed
   - Cannot prove any of:
-      trade (*?u96*)_ (*?u97*)_
-      trade (*?u97*)_ (*?u98*)_
+      trade (*?u72*)_ (*?u73*)_
+      trade (*?u73*)_ (*?u74*)_
   - In the context:
       trade p q
       trade q r
@@ -12,8 +12,8 @@
   - Expected failure:
   - Tactic failed
   - Cannot prove any of:
-      trade (*?u96*)_ (*?u97*)_
-      trade (*?u97*)_ (*?u98*)_
+      trade (*?u72*)_ (*?u73*)_
+      trade (*?u73*)_ (*?u74*)_
   - In the context:
       trade p q
       trade q r
@@ -22,8 +22,8 @@
   - Expected failure:
   - Tactic failed
   - Cannot prove any of:
-      trade (*?u116*)_ (*?u117*)_
-      (*?u116*)_
+      trade (*?u84*)_ (*?u85*)_
+      (*?u84*)_
   - In the context:
       p
       trade p q

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

@@ -1,5 +1,5 @@
 * Info at Bug278.fst(29,5-31,5):
   - Expected failure:
   - Tactic failed
-  - Internal error: unexpected unresolved (universe) uvar in deep_compress: 321
+  - Internal error: unexpected unresolved (universe) uvar in deep_compress: 317
 

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

@@ -1,5 +1,5 @@
 * Info at Bug45.fst(57,10-62,5):
   - Expected failure:
   - Tactic failed
-  - Internal error: unexpected unresolved (universe) uvar in deep_compress: 547
+  - Internal error: unexpected unresolved (universe) uvar in deep_compress: 543
 

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

@@ -3,17 +3,17 @@
   - Current context:
       some_pred x v
   - In typing environment:
-      __#492 : squash (_v_5 == v)
-      _v_5#491 : erased int
-      __#370 : squash (v == v)
-      v#245 : erased int
-      x#239 : R.ref int
+      __#402 : squash (_v_5 == v)
+      _v_5#401 : erased int
+      __#281 : squash (v == v)
+      v#156 : erased int
+      x#150 : R.ref int
 
-      goto _return#289 requires emp
+      goto _return#200 requires emp
 
 * Info at ExistsErasedAndPureEqualities.fst(66,32-68,5):
   - Expected failure:
-  - Ill-typed term: pure (v == (*?u102*)_)
+  - Ill-typed term: pure (v == (*?u82*)_)
   - Expected a term of type slprop
   - Cannot check relation with uvars.
 

pulse/test/nolib/AdmitDoesNotSimpl.fst.output.expected

@@ -3,36 +3,36 @@
   - Current context:
       foo x
   - In typing environment:
-      y#289 : int
-      x#287 : int
+      y#175 : int
+      x#173 : int
 
-      goto _return#342 requires foo x
+      goto _return#228 requires foo x
 
 * Info at AdmitDoesNotSimpl.fst(20,2-20,9):
   - Admitting continuation.
   - Current context:
       foo x
   - In typing environment:
-      y#289 : int
-      x#287 : int
+      y#175 : int
+      x#173 : int
 
-      goto _return#342 requires foo x
+      goto _return#228 requires foo x
 
 * Info at AdmitDoesNotSimpl.fst(27,2-27,9):
   - Admitting continuation.
   - Current context:
       foo 2
   - In typing environment:
-      uu___0#85 : unit
+      uu___0#64 : unit
 
-      goto _return#93 requires foo 2
+      goto _return#72 requires foo 2
 
 * Info at AdmitDoesNotSimpl.fst(35,2-35,9):
   - Admitting continuation.
   - Current context:
       foo 2
   - In typing environment:
-      uu___0#85 : unit
+      uu___0#64 : unit
 
-      goto _return#93 requires foo 2
+      goto _return#72 requires foo 2
 

pulse/test/nolib/ErrCantFindWitness.fst.output.expected

@@ -1,7 +1,7 @@
 * Info at ErrCantFindWitness.fst(8,1-8,1):
   - Expected failure:
   - Cannot find witness for (exists* (x:nat). emp)
-  - Ill-typed term: (*?u54*)_
+  - Ill-typed term: (*?u42*)_
   - Expected a term of type nat
   - Cannot check relation with uvars.