parser: exponential backtracking on nested bool(...) — a small legal file hangs parse and the LSP workspace scan

[evdenis]

Summary

rossi::parse takes effectively forever (exponential time, not a crash) on a small, syntactically valid context whose axiom nests bool(...) ~100 deep. pest is a PEG parser without memoization: in

bool_expr            = { kw_bool ~ lparen ~ predicate ~ rparen }
comparison_predicate = { expression ~ (op_eq | …) ~ expression }
atomic_predicate     = { comparison_predicate | predicate_application | … }

(crates/rossi/src/grammar.pest:200,342-357), parsing the predicate inside bool( … ) first tries comparison_predicate, whose leading expression swallows the entire nested subtree — and then fails on the next token (), no comparison operator), discarding all of that work and re-parsing the same subtree under the next alternative. Each level re-parses its subtree a constant factor of times and the factors multiply: T(n) ≈ c·T(n−1).

Measured (debug build), time doubles every ~2 levels:

depth	parse time
10	7 ms
14	26 ms
18	132 ms

Extrapolated to depth 100: thousands of years. Depth ~30 is already seconds, ~40 minutes. Every parse that finishes returns Ok — this is valid input accepted slowly, not invalid input rejected slowly.

Impact: one such file in a workspace hangs rossi lsp at initialize (the scan parses every .eventb file synchronously); rossi fmt on the file spins at 100% CPU forever. Same robustness class as the fixed stack-overflow abort, on the orthogonal resource axis: that was space (recursion depth), this is time (rule-call count). The nesting-depth pre-scan correctly does not catch it — depth ~101 is far under MAX_NESTING_DEPTH = 256, and no depth limit can bound backtracking work (deeper variants at 500 are rejected instantly by the guard, ironically making the shallower file the dangerous one).

Reproduce

python3 -c "n=100; open('/tmp/boolnest.eventb','w').write(
    f\"context c1\naxioms\n  @a1 x = {'bool('*n}true{')'*n}\nend\n\")"
timeout 30 rossi fmt /tmp/boolnest.eventb; echo "exit: $?"   # 124 — still parsing

Note: rossi validate /tmp/boolnest.eventb does not reproduce (it enters parsing differently); the hang is on the rossi::parse / Rule::component path used by the LSP scan and fmt.

Proposed direction

1. Tactical — pest::set_call_limit: bounds total rule calls per parse, which is exactly the exploding quantity; converts the hang into a parse error. Needs calibration: it is one process-wide global, so the limit must clear the call count of the largest legitimate corpus file while tripping early on explosions — workable, since legitimate call counts grow linearly with file size and this grows exponentially with depth. Caveat: open upstream PR Fix set_call_limit to track recursion depth and prevent stack overflow pest-parser/pest#1140 (for Limiting depth during parse to avoid stack overflow pest-parser/pest#1129) would repurpose set_call_limit from total-calls to recursion depth — the wrong axis for this bug — so pin/check pest semantics when implementing.
2. Root fix — left-factor the grammar: the explosion comes from ordered alternatives sharing the expensive expression prefix. Parse one expression, then decide by what follows (=/∈/… → comparison; otherwise fall through) instead of fail-and-re-parse; this makes the parse linear. Higher risk: the grammar is load-bearing (EB-rule oracle parity, type-inference parity, tree-sitter mirror), so it needs the full corpus + parity gates as a safety net. Language-preserving, hence testable.
3. Defense in depth — LSP scan watchdog: time-bound per-file parses during the workspace scan. Weak alone (a pest parse cannot be cancelled mid-flight, so a timed-out parse leaks a busy thread), but cheap insurance alongside (1).

Notes

• Found while verifying the nesting-depth guard (fix(parser): reject over-deep nesting instead of overflowing the stack); previously masked because the scan crashed on a deep-paren file before ever reaching a bool nest.
• Memoization (packrat) is the textbook PEG cure but pest doesn't offer it; that option only exists via a parser migration.
• pest's released set_call_limit counter never decrements (verified in pest 2.8.6 source, parser_state.rs — the method is named increment_depth but tracks a running total), which is exactly why it fits this bug and not the depth one.