Conversation
Since #4515, application arguments are bound without restating their result-type refinement, on the premise that the solver recovers it from the callee's typing axiom. For nonlinear arithmetic that premise fails: `distributivity_add_right base (eval s) (pow2 n * eval t)` lost the sign facts `eval _ >= 0` and `pow2 _ > 0`, pushing a goal from ~5 rlimit to exhausting 60 (and making it sensitive to unrelated declarations above). When the callee's result is a refined unit (a lemma call), bind the arguments with the new `TcUtil.bind_capture_quantifier_free`, which restates only the quantifier-free conjuncts of the argument's refinement. The lemma's result type is dissolved into a hypothesis, so this does not pollute any value's type; quantified conjuncts (e.g. `Seq.init`'s `forall i. index s i == f i`) are dropped since they add instantiation work to every later goal (they destabilized FStar.Matrix). Also: - FStar.UInt128.eq_mask: call v_inj explicitly; the proof was brittle (1.08/5 rlimit) and flipped under the context perturbation. - tests/tactics/Postprocess: accept gensym renumbering. - tests/bug-reports/closed/Bug4591.fst: regression test. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Contributor
Author
|
!bench |
Contributor
🔬 F* Performance ComparisonBaseline: Summary
Totals: Memory: 787.3 MiB | Time: +53.1s Change Distribution
Heavy Tests (baseline > 100 MiB, n=776)
📉 Top 20 Memory Improvements
📈 Top 20 Memory Regressions
⬇️ Top 20 Time Improvements
⬆️ Top 20 Time Regressions
|
This branch has not been deployed
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
1 participant
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.
Fixes #4591.
Root cause
The regression window (2026.09.20 → nightly-2026-09-23) contains only #4556 and #4515; the release already includes the prop encoding (#4519). The cause is in #4515:
check_application_argsbinds non-constructor arguments withbind_no_capture, assuming the solver recovers an argument's result refinement from the callee's typing axiom. For nonlinear arithmetic that fails. In the reproducer,distributivity_add_right base (eval …) (pow2 … * eval …)lost the sign factseval _ >= 0andpow2 _ > 0, which the release VC had next to the lemma's postcondition.Evidence: in a faithful replay of the incremental Z3 session, adding just those three facts before the failing goal takes it from >40M rlimit (canceled) to 3.9M.
eval_emptycontributes nothing to the query; it only reorders prelude declarations, so its effect (like the module-name sensitivity) is Z3 luck on a goal that had become hard.Fix
When the callee's result type is a refined
unit(a lemma call), bind the arguments with a newTcUtil.bind_capture_quantifier_free. It restates only the quantifier-free conjuncts of each argument's refinement. The lemma's result type becomes a hypothesis once the call is sequenced, so no value's type is polluted. Quantified conjuncts (e.g.Seq.init'sforall i. index s i == f i) are dropped: an earlier version that kept them destabilizedFStar.Matrix.Also:
FStar.UInt128.eq_mask: callsv_injexplicitly. The query text is unchanged, but the goal was brittle (1.08 of 5 rlimit) and flipped under context changes from dependency checked files. With the hint it uses ≤0.36 both before and after this change.tests/tactics/Postprocess.fst.output.expected: gensym renumbering only.tests/bug-reports/closed/Bug4591.fst: regression test (max 8.7 of 60 rlimit over 8 seeds).Results
Reproducer, max rlimit over
--z3seed 0..7(rlimit 60):Spec.Bignum4BugBefore this PR the nightly exhausts 60 on the default seed.
Testing
ADMIT(stage2/ulib.checkeddeleted), plus Pulse core/libmake testwith all_cache/_outputdirs cleared, plus examples,doc/book/codeand Pulse teststests/custardRelocApp ("did not say where it found the source" / Error 369), fails identically on unmodified master.I have not re-run hacl-pulse.