perf/safety: convert parseStr from recursive to iterative to prevent stack overflow
还没有人认领这个 Issue。
评估
- 难度
- 4/5
- 预计耗时
- 3-5 天
- 新手友好度
- 45/100
- Issue 类型
- 重构
- 描述清晰度
- 描述清楚
- 活跃度
- 停滞
- 领域
- compilers, performance
调研方向
从 Lck/Json/Tokenizer.lean 中 parseStr 的递归 CPS 实现开始，然后检查调用方如何依赖其 CPS 接口。在保留该接口的同时，将字符串解析重写为迭代式累加器，围绕归纳循环不变量调整证明，并验证大型字符串字面量不再有导致栈溢出的风险。
由索引模型根据 Issue 内容生成。
描述
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
- 主要语言
- Lean
- 星标
- 2
- 派生
- 1
- PR 合并指标
- 30 天内没有已合并 PR
贡献指南
这个仓库没有索引到贡献指南
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
lambdaclass/lambda_compiler_kit 的其他 Issue
-
难度 1/5 1 小时以内 新手友好度 72/100
-
难度 1/5 1 小时以内 新手友好度 68/100
-
难度 2/5 1-3 小时 新手友好度 68/100
-
enhancement
难度 4/5 3-5 天 新手友好度 48/100
-
难度 2/5 1-3 小时 新手友好度 50/100
查看 lambdaclass/lambda_compiler_kit 的全部 Issue
相似的 Issue
-
flang:fir-hlfir
难度 2/5 1-3 小时 新手友好度 70/100
llvm/llvm-project#225935 ·
-
难度 2/5 1-3 小时 新手友好度 75/100
objectionary/eo#8923 ·
-
难度 2/5 1-3 小时 新手友好度 75/100
-
难度 2/5 1-3 小时 新手友好度 75/100
-
Coarray integration tests carry no LABELS, so run_tests.py silently skips them under every backend 未关闭coarray
难度 2/5 1-3 小时 新手友好度 70/100