Skip redundant phase1 TC passes when no uvars are left#4183
Open
nikswamy wants to merge 5 commits into
Open
Conversation
Two optimizations in purify_and_check_spec: 1. In purify_spec, skip the final tc_term_phase1_with_type call when the assembled term has no unresolved uvars or universe variables. Profiling shows 98.4% of calls produce fully elaborated terms after per-atom TC. 2. In tc_term_phase1_with_type_twice, guard the second TC call with a no_uvars_in_term check. The second call is only needed when the first leaves unresolved universe variables (e.g., in reveal coercions) — triggered only 2 times across the entire c2pulse library. Combined with the check_slprop_with_core optimization (previous commit), this reduces InsertionSort.fst verification from ~43.4s to ~30.2s (30% speedup). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
… add tc_term_phase1 stats In symb_eval_subterms, the tc_type_phase1 call on Abs/Refine binder types is now skipped when symb_eval_subterms did not modify the binder type (changed1=false). The elaboration will be done later by the per-atom tc_term_phase1_with_type_twice call. Also adds Stats.record wrapping to tc_term_phase1 in Pulse_RuntimeUtils.ml for consistent profiling. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The optimization to skip redundant TC passes when no uvars remain changes universe/uvar numbering in error messages. This updates 8 expected output files to match the new numbering. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Instead of removing check_slprop_with_core calls (which would be unsound), add check_slprop_with_core_structural that walks the Pulse term view and only falls back to core_check_term for opaque Tm_FStar leaves. Pulse's slprop constructors (Star, ExistsSL, ForallSL, WithPure, Pure, Emp, Inv, etc.) are known to produce slprop-typed terms, so the structural walk avoids redundant kernel type-checking for terms built entirely from these constructors. Applied in both purify_and_check_spec (saves ~7s) and bind_res_and_post_typing (saves ~2.5s). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
nikswamy
force-pushed
the
_nik_optimize_purify_and_check_spec
branch
from
d91ca2a to
7c46817
Compare
gebner
reviewed
Apr 10, 2026
| 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. |
Contributor
There was a problem hiding this comment.
The change on the next line is a big hack to work around another big hack. Can we just fix the coercion-inserted reveal calls instead?
(There are a few other places where we run phase1 TC twice to work around this, it would be great if we could just remove all of them.)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.