[Giulio2002]

Disclosure: I wrote this change with Claude Code (an AI coding agent), like #1142 and #1209. bend2/bend.ts is touched (+45/−3), which AGENTS.md reserves for humans: if you would rather write the idea yourself, please close this and take it. It replaces #1210 (closed) with a smaller change: no side table, no wrapper frames.

The problem

A conversion whose two sides become identical only after a def unfolds evaluates both closed sub-terms. A big numeral is then a unary chain, and the checker overflows its stack.

def big() -> Nat: Nat.pow(2n, 30n)
def boxed() -> Box: Box{big()}
def boxed_eq() -> {Box{big()} == boxed() : Box}: {==}

Stock term_compare runs the rigid pass (the empty book: no def unfolds, calls compare by head and arguments) once, on the whole goal. boxed() against Box{big()} is not rigidly equal, so the full pass unfolds boxed() to Box{big()}. It then evaluates big() on both sides (2^30 Succ cells each). It never asks the cheap question again. In a real project (a verified SSZ library whose schemas carry list limits of 2^30 and above) this blocks every proof that unfolds a spec definition next to its limit.

The change

Before the full pass unfolds two calls of one filled def, compare their arguments with the rigid pass (compare_call, first to last, stopping at the first unequal argument). If they are equal the calls are equal and neither unfolds.

• Soundness. Rigid equality implies definitional equality: the rigid book knows no def, so it only equates what the full book also equates. A "not equal" falls through to the unchanged comparison. The share-cell unification of Conversion without blowups on numerals, same calls and shared graphs, at no cost to ordinary checks (#1071, #1075) #1151 (rhs.v = lhs.v) runs on success, as it does today.
• The memo is stock's. Successes are already memoized by that unification. The retry would otherwise repeat failing walks (a call and its sibling with different first arguments), so a failure is remembered by one optional field on the cell, u?: object: the right-hand side the rigid pass found it unequal to. It is read only in rigid EQ mode and written in the block that does the unification. No table, no wrapper function, no extra stack frame, so conversions recurse exactly as deep as on stock.
• A rigid whnf no longer fills a -1 cell (book !== RIGID): otherwise the rigid retry would stop the full pass's own evaluation of that cell.

A step budget on the retry did not help. compute_1600 makes about 475k retries and all of them fail, and even 4 steps per retry cost about as much as the unbounded walk. The failure marker brings rigid steps from 6.6M to 1.46M.

Measurements

All on a shared Linux server, so times are noisy. Stock is 01875127.

	stock	this PR
the repro (tests/check/conversion_copy_after_unfold.bend)	stack overflow	ALL PROOFS CHECK, 0.3 s
depth probe: largest n with {U32.to_nat(n) == n'n} by {==}	28,984	28,984
tests/ (1,526 files, one run each)		output identical to stock except the new tests
bench/checker compute_1600 (median CPU of 10, interleaved)	2.36 s	2.69 s (+14%)
defs_12800, generics_3200, proofs_3200, trees_400		within ±2%

I also ran a verified SSZ proof tree of about 6,100 files (48 import-only umbrella checks) on this change: all 48 pass at the pinned stack (423 s wall on the shared box).

Soundness probes, same verdict as stock on each: equal arguments to different defs; different arguments under a box; partial application and arity; 2^30 literals (also inside a box); different lambdas; an unfilled hole; an unfilled law; a non-terminating def with equal and with different arguments; an @unsafe def through an import. Every rejection stays a rejection. The controls stock overflows on (copy after unfold, nested, twice(big())) are accepted.

Tests

tests/check/conversion_copy_after_unfold.bend (the repro, its mirror, twice(big()), and a call nested in an unfolded def) and tests/check/conversion_copy_after_unfold_mismatch.bend (arguments that differ must still fail to convert, including under a box).

🤖 Generated with Claude Code

[Tor-Saxberg]

An independent measurement, with a minimal case that has no large numerals. The cost comes from a slow closed computation inside a type, compared after an unrelated part of the type needed one unfolding step:

import Base

# Slow to evaluate: about 2^n steps.
def slow(+n: Nat) -> Nat:
  match n:
    case 0n: 0n
    case 1n+p: Nat.add(slow(p), slow(p))

# A type whose normal form needs slow(22n).
def Heavy() -> Data:
  {slow(22n) == 0n : Nat}

# One unfolding step away from its argument.
def Same(x: Data) -> Data:
  x

def Both(x: Data, y: Data) -> Data:
  Sigma<&2, &2, x, _ => y>

def cast(w: Both(Heavy(), Same(Unit))) -> Both(Heavy(), Unit):
  w

The control is the same file with Same(Unit) replaced by Unit.

	2.0.34 (7d8a3eb)	this PR (c55a7f0)
the file above	6.19 s	0.13 s
control	0.13 s	0.12 s

Both checkers print ALL PROOFS CHECK for both files. On 2.0.34, each increase of n by one roughly doubles the first time. Here the rigid pass fails on Same(Unit) against Unit, so the full pass reduces both Heavy() calls; with this PR, Heavy() against Heavy() converts without unfolding.

macOS arm64, bun 1.2.9.

[nicolas-abril]

Sorry for not answering this earlier. While I'm not in favour of the approach here, adding an extra field to Var, i think we could do a similar optimization in the same spirit. I've tried it a couple times but didn't get to a design I liked.
So, I've kept this issue open to remember the problem and direction of the solution.

[Giulio2002]

you can close it and do the optimization. whatever you need

[Lorenzobattistela]

Closed in favor of #1832