Repository navigation
Two calls of one def compare their arguments before either unfolds - #1832
Lorenzobattistela wants to merge 8 commits into
Conversation
compare_go unfolded both sides before comparing them, and the rigid pass
(no def unfolds) ran only once, at the root of the goal. A copy that
lines up only after an outer def unfolds was evaluated on both sides:
{Box{big()} == boxed()} with big() = 2^30 overflowed the stack, and a
type holding a slow closed call next to a part that needs one unfold
re-ran the slow call on both sides.
Before compare_go unfolds anything, compare_call walks both spines. If
both are the same Ref and each pair of arguments is one atom (the same
cell, def, literal or bound variable, seen through cells and
annotations, nothing reduced), the calls are equal by congruence. If
not,
nothing is decided and the comparison goes on as before. A failed try
costs one step per argument. Comparing the arguments recursively instead
made compute_1600 1.4x slower, because the walk down unary chains was
repeated at every level. A non-atomic argument is still caught one
unfold lower, where its own call meets its copy.
The atom shortcut caught only calls of one def on the same atoms, so a
copy that agrees only after a few steps (a def naming another, another
def with the same body, equal arguments written differently, a call or
a constructor as the argument) still overflowed. compare_go now asks
the rigid pass (no def unfolds) at every step of the full pass before
it unfolds anything, and the rigid pass at the root of term_compare is
that first step. Both sides evaluate in step, so once they reach the
same text the walk stops there.
The cost is in proofs by computation over large data: compute_1600 is
1.35x its pin, and {add(a, b) == add(b, a)} on unary numbers grows
quadratically, as each rigid try walks the long common prefix again.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Lorenzobattistela
changed the title
|
Tested this on the proof workload in Giulio2002/bend-collections. Mixed results: useful frontend speedups, but large regressions in two secp256k1 files. Setup
Frontend results: base → PR
Regressions:
The two timeouts are censored measurements, not completed runtimes: they imply >10× and >20× slowdowns respectively relative to the base medians. The intended Separate kernel checkThese timings are frontend checks, not BendTT acceptance. In the separate end-to-end So this fixes the intended conversion cases and helps several real frontend workloads, but it is not an across-the-board improvement for this library. The repeated |
As in Lean's lazy delta reduction: when both sides of a conversion are calls of the same def, their arguments are compared rigidly (the empty book unfolds no def and fills no cell) before either side unfolds. The rigid answer on a pair of shared cells is kept for the whole conversion, so a DAG whose tree is exponential is walked once. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Lorenzobattistela
changed the title
…ir is kept Review (xhigh) of the previous commit found three regressions against main. Each fix follows Lean's lazy delta reduction more closely: - Identical copies headed by a redex (a local lambda, an applied lambda-match) were evaluated on both sides: main's root rigid pass beta-reduced them to one stuck call, and same_call looked only at raw heads. Lean runs its same-head step after whnfCore, so same_call now reduces a side whose head is a redex (Let, Rwt, an applied Lam or Mat) with the rigid book first. A call, a value or a neutral is already reduced and is not walked again, which keeps compute_1600 where it was (always reducing cost 1.30x). - len(xs) == len(ys) on literal lists that differ at the end was quadratic: each level's same_call walked the rest of the raw tails, and the memo saw only cells. Lean's caches key on any pair of terms; the memo now keeps every rigid pair, under a pair key (one partner per lhs lost an answer when a cell met two partners in turn). - The rigid pass decides two calls without a whnf again (same_call is tri-state in both modes), since a whnf of a stuck call rebuilds its spine. Not changed, by design: the rigid walk of a call's arguments runs nested in the full pass, so a proof whose full walk is deep and whose call arguments are deep needs the sum of both stacks (Lean nests the same way). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…pares whole Review (high) of 8d0a4d7 found a soundness break and a regression: - same_call found each side's head on its own, then compared arguments until the shorter spine ran out, so g(1n)(0n) and g(0n) were rigidly equal when their shared argument was, and {7n == 5n} checked through one conversion. Both spines are now walked together, as before 8d0a4d7: two calls match only on as many arguments. The test conversion_call_after_unfold_arity.bend fails on 8d0a4d7. - A lambda-match stuck on a call, on both sides, was evaluated on both sides (main's root rigid pass compared it whole). Lean's same-head step reaches such terms because its matchers are defs; here a term whose head is still a redex after rigid reduction is stuck on a def, so the full pass compares the two whole and rigidly before it unfolds. - The memo now keeps only EQ answers, instead of trusting that the rigid pass is entered only in EQ, and it is allocated on the first rigid pair and dropped when the conversion ends. Not changed, by design: same_call's rigid reduct is not reused by the full whnf (only a redex head is reduced twice, and on compute_1600 those are under 100 of the 450k pairs), and the rigid pass stays the RIGID book sentinel that compare_go already used. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…is safe Review (medium) of eda032e: - In the rigid pass, same_call reduced a redex head with the rigid book and compare_one then reduced the same term again. The rigid pass's own whnf and its App case already compare stuck calls, so same_call now reduces only in the full pass. - The memo comment claimed a pair holds no free var; it does (the fresh vars of a binder). What holds is that vars are levels and a pair met at one depth holds only levels below it. Checked and not changed: - A let chain of matches with no def is exponential on main too; the PR is a steady 1.8x on it (n = 22, 24, 26), and filling cells with values in the rigid pass did not change that. - BendTT agrees with every new test (safe: 0 false rejects). - The full pass does not continue from same_call's rigid reduct, since that would lose the share cell it fills; only redex heads pay it. - A rigid answer is final only in the rigid pass; in the full pass two calls of different defs return after the head walk, before any argument. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
/simplify on the PR: the reset on exit was redundant. The reset on entry already covers a conversion that threw and was caught, and the table of the last conversion lives only until the next one. Tried and not kept: a boolean same_call used only by the full pass, comparing both kinds of rigid try (two calls, two stuck terms) whole through compare_go. It is 164 ttok shorter but costs 1.49x on compute_1600, because the rigid pass then rebuilds every call's spine through term_wnf instead of comparing its arguments in place. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Retested the updated head This supersedes the earlier revision's performance observations above. These are frontend Fails only on this PRThese four roots pass on BASE but stack-overflow on PR:
All four report: Source-link caveat: these permalinks identify the corresponding original files. As in the earlier comment, the actual tested snapshot contains unpublished compatibility/proof-decomposition changes; the links are navigation references, not exact standalone reproducers. The A/B used the same modified snapshot on both sides. No source/proof changes were made between variants. What works versus BASE
Suggested fix directionI also reran This points toward deep structural comparison consuming the JS stack, though it is not yet a reduced root-cause proof. In particular, the recursive Proposal, not yet implemented or validated: keep the same-head optimization, but make the deep structural equality traversal stack-safe using an explicit worklist/trampoline rather than recursively nesting comparator callbacks. Preserve comparison mode, binder depth, short-circuit behavior, and sharing semantics; finalize memoized answers only after their child comparisons are resolved. Also inspect the recursive That seems a better direction than increasing the host stack or weakening the proof obligations. The full matched sweep shows real improvements, but these four new frontend crashes still block treating the update as an unconditional improvement for this workload. |
Two calls of one def compare their arguments before either unfolds, as in Lean's lazy delta reduction
Addresses the problem in #1232 with a different change. Thanks to @Giulio2002 for the report and to @Tor-Saxberg for the minimal case.
Problem
compare_gorunsterm_wnfon both sides before it compares them. The rigid pass (RIGID, the empty book, where no def unfolds) runs only once, at the root of the goal. When two copies of a call line up only after an outer def unfolds, the full pass evaluates both copies:The rigid pass fails at the root (
CtragainstRef). The full pass then unfoldsboxed()and meetsbig()againstbig(): the same def, but two different nodes, so===misses. It unfolds both and walks 2^30Succcells: stack overflow.The same happens in types, where it costs time instead of stack:
Here
Same(Unit)is not rigidlyUnit, so the full pass normalizesHeavy()on both sides. The time doubles with each step ofslow.Solution
This is the same-head step of Lean's
lazy_delta_reduction_step: before either side unfolds, both sides are reduced with no def unfolded (Lean'swhnfCore). Two calls of the same def then compare their arguments, and the checker unfolds only when that fails.same_callreduces a side whose head is a redex (aLet, aRwt, an appliedLamorMat) withRIGID, the empty book, which unfolds no def. A call, a value or a neutral is already reduced and is not walked again.RIGID. Both spines are walked together, sog(1n)(0n)never matchesg(0n). A rigid "yes" is a definitional "yes".term_wnfas before. In the rigid pass, two calls that differ are rigidly different. Every other term goes through the rigid pass's own whnf and structural compare.tm.i === -1 && book !== RIGID). Without this, a rigid walk would fill a cell with a value stuck on a def it may not unfold. The full pass would then inherit that value, and its-2unification would make the walk exponential.SEENkeeps every rigid EQ answer for oneterm_compare, under a pair key, like Lean's equiv manager and failure cache. A DAG whose tree is exponential is then walked once, and so is nearly equal data walked again from each level below. It is allocated on the first rigid pair and reset when the next conversion starts.term_compareno longer runs a rigid pass at the root, since the same-head step covers that case.An earlier version of this PR asked the whole rigid pass at every step of the full pass. That fixed the repro, but it was quadratic on long, nearly equal data (14x on
add(a, b) == add(b, a)at n = 3000) and exponential on shared DAGs (34x on a 22-deep chain off(n) = z(n) + z(n)). Both are gone here.What this costs, by design: the rigid walk of a call's arguments runs nested inside the full pass, as in Lean. A proof whose full walk is deep and whose call arguments are deep needs both depths of stack. A 20,000-deep box chain over 4,500-element list arguments passes on main and overflows here. The deepest single walk, a unary numeral against its copy, is the same as on main (about 31,900).
Review
Rounds of code review (xhigh, high, medium, low) on this PR found these, now fixed:
len(xs) == len(ys)on literal lists that differ only at the end was quadratic, because the memo only kept cell pairs. Fixed by keeping every rigid pair.{7n == 5n}checked. Fixed by walking both spines together, and covered by_arity.bend.Checked and not changed: a let chain of matches with no def is exponential on main too, and is a steady 1.8x here.
Measurements
Whole runs of
bend <file>(startup, parse and check), median of 7 interleaved rounds on one M-series laptop, main9d514f3bagainst this change:boxed_eq(2^30)castwithslow(22n)_near.bend(2^16)gates/perf.ts)add(a, b) == add(b, a)by{==}, n = 3000len(append(xs, ys)) == len(append(ys, xs)), n = 3000len(xs) == len(ys), literal lists of 4000root_loop(24n, 3) == root_rec(24n, 3)(_shared.bend)--check-onlyover 1,892 repo files (tests, bench, demos, guide, evals) and 576 BendHub files: every output is identical to main's, with no timeouts. Total time is 0.98x on the repo and 0.99x on the hub.bend.tsgoes from 44,493 to 45,260 ttok (cap 48k).Tests
tests/check/conversion_call_after_unfold.bend: the repro, its mirror, and a literal argument (boxed_at(30n)). Stack overflow on main.tests/check/conversion_call_after_unfold_type.bend: thecastcase withslow(26n), through theLEconversion (check-any).tests/check/conversion_call_after_unfold_near.bend: five calls whose arguments are equal only after a few steps, at 2^16. Each one overflows on main.tests/check/conversion_call_after_unfold_differ.bend: calls of one def on different arguments must still fail (Box{8n}againstBox{16n}). This guards against a false accept.tests/check/conversion_call_after_unfold_redex.bend: copies of a local lambda, of an applied lambda-match and of a match stuck onslow(26n). Each takes 2^26 steps on both sides without the reduction before the same-head step.tests/check/conversion_call_after_unfold_arity.bend:g(1n)(0n) == g(0n)must fail (7n against 5n). It guards against a false accept.tests/check/conversion_call_after_unfold_shared.bend: theSEENcache.root_recis a chain ofmix(h, h)on one cell; without the cache the check does not finish in 60 s.The 22-deep
fchain is not a test: BendTT runs out of fuel on it from depth 22, and at depth 20 the old version of this PR still took only 0.75 s, so it would not have caught the regression.Gates
On main
9d514f3bplus this branch (0e1fbd8):gates/safe.ts tests: agree 1149, false reject 0, timeout 0.🤖 Generated with Claude Code