Conversation
The result refinement of a pure application `f a1 .. an` was reachable by the solver only through f's typing axiom: instantiate it, prove the argument typings (f's preconditions), then unfold the result refinement. Since #4515 stopped restating argument refinements, that chain is often not found under nonlinear arithmetic, e.g. `eval (slice s k n) : nat` (#4591). split_goals now states `HasType e t` for each such application, not under a binder, at implication hypotheses, `if` guards and before goals. Facts are only taken from unguarded positions (the later operands of ==>, \/, /\, &&, || and ite are typechecked under the earlier ones), and not for `e` in a hypothesis `x == e` where x already has e's type (let-bindings). Controlled by `--ext typing_facts=off|hastype|refinement` (default hastype). Proof fixes: FStar.OrdSet.lemma_as_set_disjoint_left (see #4601), PulseCore.IndirectionTheorySep.read_inv_age, and a fragile proof in tests/micro-benchmarks/SquashSubtypingDivergence. TestErrorLocations now reports one error instead of two. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Contributor
Author
|
!bench |
Contributor
🔬 F* Performance ComparisonBaseline: Summary
Totals: Memory: 62.4 MiB | Time: +7.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 (alternative to #4597).
Problem
The result refinement of a pure application
f a1 .. anreached the solver only throughf's typing axiom. To use it, the solver has to instantiate the axiom, prove the argument typings (i.e.f's preconditions), and then unfold the result refinement. Since #4515 stopped restating argument refinements, Z3 often fails to find that chain under nonlinear arithmetic. For example, it may not learn thateval (slice s k n) : natholds, so sign facts disappear (#4591).Change
split_goals(FStarC.SMTEncoding.ErrorReporting) now statesHasType e tfor each application whose result type is refined and that is not under a binder. The fact is placed next to the formula the application occurs in: at an implication's hypothesis, at anifguard, and before a goal. It is valid there because the typechecker established that the application is well typed at that position, much like the typing hypothesis we already emit for alet-bound variable.==>,\/,/\,&&,||anditeare typechecked assuming the earlier ones, so facts are only taken from unguarded positions. In a hypothesis known to hold, both sides of/\and&&count. Without this,x >= 0 ==> p (g x)withg : x:int{x >= 0} -> r:nat{r <= x}would provex >= 0. Seetests/micro-benchmarks/TypingFactsGuards.fst.x == ewherex's type already ise's result type, the fact oneis skipped because it duplicatesx's typing. The duplicates caused the blowup that Bug4405 guards against.--ext typing_facts=off|hastype|refinement, defaulthastype.refinementasserts the refinement formulas instead ofHasType.Proof and test changes
FStar.OrdSet.lemma_as_set_disjoint_left: addedeq_lemma (intersect s1 s2) empty. Mentioning the ground termsorted f (intersect s1 s2)makes Z3 give up immediately with "incomplete quantifiers", independent of rlimit. This is pre-existing: it fails the same way on master when the term is written explicitly (Adding a true ground hypothesis makes Z3 give up instantly with 'incomplete quantifiers' (rlimit-independent) #4601).PulseCore.IndirectionTheorySep.read_inv_age: addedset_loc__age1 w l; assert on l (later p') (age1_ w).tests/micro-benchmarks/SquashSubtypingDivergence: addedUI.one_to_vec_lemma #32 31. The proof was seed-fragile on master too (3–16 rlimit); it now needs 0.15 on every seed.TestErrorLocations:eliminate exists (n:nat). n = 0 with assert (n = 0)now reports one error instead of two. Once the precondition obligation (the existential) is assumed, the assertion follows from the witness's typing.Testing
make _test _test_pulsepasses, except CustardRelocApp, which also fails on master.Spec.Bignum4): passes on 4/4 seeds (max 25.7 of rlimit 60). Withtyping_facts=off(≈ master) it fails on 2/4.