Repository navigation
Make expand_defs linear in the size of the context - #303
Merged
Merged
Conversation
lemmy
force-pushed
the
expand-defs-single-pass
branch
from
October 12, 2026 19:01
5afd17d to
1be05cf
Compare
lemmy
changed the title
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Pin substitution chains, de Bruijn index shifts, binder handling, definition visibility and selection, pragma expansion, and preservation of untouched hypotheses, definition bodies, and obligation metadata. Include an allocation-scaling regression test, disabled until the repeated traversal of the context is removed. Part of Github issue tlaplus#299 tlaplus#299 [Tests] Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
force-pushed
the
expand-defs-single-pass
branch
from
October 14, 2026 01:35
1be05cf to
356d9e3
Compare
lemmy
marked this pull request as ready for review
October 14, 2026 01:42
Member
Author
|
/cc @Calvin-L @letFunny @qdelamea-aneo - The more reviewers, the better! :-) |
|
Hey Markus, thank you for the work here. As for my review, I am afraid I don't have enough knowledge about tlapm internals to say confidently whether this is a safe change or not. At best I would be regurgitating some AI review. However, I am happy to test the changes and report the speed up in my specs. |
Member
Author
|
@kape1395 Does your verbal approval count as formal approval as well? :-) |
Calvin-L
approved these changes
Nov 10, 2026
Backend.Prep.expand_defs substituted each expanded definition into the whole remaining sequent separately, which is quadratic in the size of the context. Instead, accumulate the substitution in a single pass and apply it to each hypothesis and the goal once. Use None for the identity substitution, so that hypotheses before the first expanded definition are left unchanged, as before. Apply the same change to the copy in Backend.Toolbox.expand_defs. Enable the allocation-scaling regression test. Doubling the context must allocate less than three times as much; the old traversal allocates approximately four times as much. Addresses Github issue tlaplus#299 tlaplus#299 [Refactor] Co-authored-by: qdelamea <qdelamea@aneo.fr> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
force-pushed
the
expand-defs-single-pass
branch
from
November 10, 2026 19:07
356d9e3 to
369884f
Compare
|
A feedback from this PR: on my laptop on a rather big proof (~10K LOC in multiple files) we got:
Thanks you for this, it is amazing! :-) |
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
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 #299. Part of #286.
Backend.Prep.expand_defssubstituted each expanded definition into the whole remaining sequent separately: O(#expanded-defs × sequent size), quadratic on INSTANCE-heavy contexts. This PR accumulates the substitution in one pass and applies it to each hypothesis and the goal once.Nonestands for the identity, so hypotheses before the first expanded definition stay unchanged, as onmain. The duplicate inBackend.Toolbox.expand_defsgets the same change.Correctness
The single substitution is the composition of the per-definition ones. Outputs can differ only in how often
app_exprbeta-normalizes copies of inlined bodies, so they are identical when bodies are in normal form and otherwise equal up to beta-reduction.expand_defsis pure: immutable data and persistent deques, no mutation of its input or of global state (apart fromErrors.setright beforefailwithon arity mismatch). Comparingmain's and this PR's outputs on the same input is therefore a complete check: equal outputs mean everything downstream, provers included, sees the same input. Fingerprints are computed beforeexpand_defsand are unaffected.Testing
main's and this PR'sexpand_defsran on every obligation tlapm prepared (--noproving --nofp, no timeout), compared by strict structural equality of the whole obligation (names, visibility,Parens, locations, ...). A deliberately broken variant served as a control.source/, flash-proof, CCF (516 modules)results/(6,787 modules)Contexts reached 2,031 hypotheses and 939 expanded definitions. A randomized test (1.2M sequents) of this PR's
Prep.expand_defsandToolbox.expand_defsgave byte-identical results for normal-form bodies and differences only up to beta-normalization for injected redexes.dune runtest srcandtest/fast(48/48) pass.Performance
expand_defstime over the corpora above: 352,682 s onmainvs. 5,368 s (66×). On the CCF RaftLogInvproof, backend preparation is 7.7× faster (see #286).