perf/safety: convert parseStr from recursive to iterative to prevent stack overflow
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 45/100
- Issue type
- Refactor
- Clarity
- Clearly specified
- Activity status
- Stale
- Domain
- compilers, performance
Research direction
Start in Lck/Json/Tokenizer.lean at the recursive CPS implementation of parseStr, then inspect how callers depend on its CPS interface. Rewrite the string parsing as an iterative accumulator while preserving that interface, adapt the proof around an inductive loop invariant, and verify that large string literals no longer risk stack overflow.
Written by the indexing model from the issue text.
Description
Problem
parseStr in Lck/Json/Tokenizer.lean is written as a recursive CPS function. While the continuation wrapping is proven zero-cost at runtime (proofs are erased), the recursion itself is structural on the input — meaning for a string literal of length n, the Lean runtime creates n stack frames.
For pathologically large string values this can overflow the stack.
Expected fix
Rewrite parseStr as an iterative (tail-recursive or explicit loop) accumulator, maintaining the same CPS interface for callers. The proof structure can be adapted to use an inductive invariant on the loop state.
References
- Flagged by AI code review on PR #8
- Dominant language
- Lean
- Stars
- 2
- Forks
- 1
- PR merge metrics
- No merged PRs in 30d
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from lambdaclass/lambda_compiler_kit
-
Difficulty 1/5 Under an hour Newbie friendliness 72/100
-
Difficulty 1/5 Under an hour Newbie friendliness 68/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
-
enhancement
Difficulty 4/5 3-5 days Newbie friendliness 48/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 50/100
All issues in lambdaclass/lambda_compiler_kit
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
-
internal.h中，漏掉了1个定义。 Open
Difficulty 1/5 Under an hour Newbie friendliness 95/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
oxc-project/oxc#26944 ·