[Lorenzobattistela]

Each step of a conversion asks the rigid pass first, so a copy met past an unfold is not evaluated

Addresses the problem in #1232 with a different, stateless change. Thanks to @Giulio2002 for the report and to @Tor-Saxberg for the minimal case.

Problem

compare_go runs term_wnf on 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:

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

The rigid pass fails at the root (Ctr against Ref). The full pass then unfolds boxed() and meets big() against big(): the same def, but two different nodes, so === misses. It unfolds both and walks 2^30 Succ cells: stack overflow.

The same happens in types, where it costs time instead of stack:

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

Here Same(Unit) is not rigidly Unit, so the full pass normalizes Heavy() on both sides. The time doubles with each step of slow.

Solution

compare_go asks the rigid pass at every step of the full pass, before it unfolds anything:

if (book !== RIGID && compare_go(mode, RIGID, lhs, rhs, dep)) {
  return true;
}

term_compare now just calls compare_go: the old rigid pass at the root is the first of these steps.

• Sound: rigid equality implies definitional equality, since the rigid book knows no def and so only equates what the full book also equates.
• Complete: a rigid "no" falls through to the unchanged path.
• No new state: no memo, no new field, no side table.

It catches more than the exact repro. Both sides evaluate in step, so once they reach the same text the walk stops there. tests/check/conversion_call_after_unfold_near.bend has five such cases, and each one overflows on main:

• a def that names another (mid2() = mid());
• another def with the same body;
• equal arguments written differently (pow2(Nat.add(8n, 8n)) against pow2(16n));
• a call as the argument;
• a constructor as the argument.

An earlier version of this PR (b0e4476) caught only calls of one def whose arguments are the same atoms. It cost nothing (compute_1600 1.03x), but every one of these five cases still overflowed.

Cost

The rigid try walks the two sides until their first difference, and it does so again at every step. Where the two sides are long, nearly equal concrete data that differ deep down, that walk repeats down the chain, which is quadratic. This happens in proofs by computation over large data:

def t() -> {add(a(), b()) == add(b(), a()) : N}: {==}  # a, b: unary numerals

Proofs that move the computation into a lemma do not pay it. add_comm by induction with rewrites, then used as add_comm(a(), b()), checks at 1.00x for n = 3000.

compute_1600 is 1.35x its pin, so gates/perf.ts fails (slack 1.15). Merging this needs the pin re-recorded.

Measurements

Whole runs of bend <file> (startup, parse and check), median of 5 to 11 interleaved rounds on one M-series laptop, main aee1b1f2 against this change:

case	main	this
boxed_eq (2^30)	stack overflow	ALL PROOFS CHECK, 0.06 s
cast with slow(22n)	3.7 s	0.06 s
cast with slow(26n)	> 60 s	0.06 s
the 5 cases in _near.bend (2^16)	stack overflow	ALL PROOFS CHECK
--check-only over the 1,707 test files	122.0 s	122.4 s (1.003x)
compute_1600	0.524 s	0.684 s (1.31x)
trees_400	0.839 s	0.856 s (1.02x)
defs_12800, generics_3200, proofs_3200		1.00–1.02x
add(a, b) == add(b, a) by {==}, n = 1500	0.039 s	4.6x
add(a, b) == add(b, a) by {==}, n = 3000	0.044 s	14.1x
len(append(xs, ys)) == len(append(ys, xs)), n = 3000	0.067 s	11.4x

bend.ts goes from 43,767 to 43,798 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: the cast case with slow(26n), through the LE conversion (check-any). Does not finish in 60 s on main.
• tests/check/conversion_call_after_unfold_near.bend: the five cases above, at 2^16. At 2^30, BendTT runs out of fuel on four of them.
• tests/check/conversion_call_after_unfold_differ.bend: calls of one def on different arguments must still fail (Box{8n} against Box{16n}). Same output on main; this test guards against a false accept.

Gates

On main aee1b1f2 plus this branch:

• repo 54/54, test 1711/1711, ping 73/73.
• gates/safe.ts tests: agree 1113, false reject 0, timeout 0.
• perf 123/124: compute_1600 fails at 1.35x. A rerun also showed bfs PAR-GPU at 1.18x, a runtime cell the checker does not touch.