perf/safety: convert parseStr from recursive to iterative to prevent stack overflow

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

Lck/Json/Tokenizer.lean の parseStr の再帰的な CPS 実装から始め、呼び出し側がその CPS インターフェースにどのように依存しているかを確認します。そのインターフェースを維持したまま、文字列の解析を反復的なアキュムレーターとして書き直し、帰納的なループ不変条件を中心に証明を適用し直し、大きな文字列リテラルでスタックオーバーフローが発生するリスクがなくなったことを検証します。