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

Commencez dans Lck/Json/Tokenizer.lean, au niveau de l’implémentation CPS récursive de parseStr, puis examinez comment les appelants dépendent de son interface CPS. Réécrivez l’analyse des chaînes sous la forme d’un accumulateur itératif tout en préservant cette interface, adaptez la preuve autour d’un invariant de boucle inductif et vérifiez que les littéraux de chaîne volumineux ne risquent plus de provoquer un dépassement de pile.