proof: add parseRaw_iff end-to-end correctness theorem

Problem

There is no end-to-end iff theorem connecting parseRaw / parse directly to the ValidJson spec predicate at the string level. The existing theorems operate at the token level (parseValue_iff etc.), requiring callers to reason about tokenization separately.

Expected fix

Add parseRaw_iff (and/or parse_iff):

theorem parseRaw_iff (input : String) :
    parseRaw input = .ok v ↔ ... -- ValidJson characterization over input

This requires composing tokenizer correctness with parser correctness.

References

• Suggested by AI code review on PR #8

parseRaw と parse のエントリポイントから始め、既存の parseValue_iff 定理と tokenizer の正しさに関する結果を読んでください。tokenizer と parser の保証を、ValidJson を特徴付ける文字列レベルの iff 定理としてまとめてください。parseRaw_iff および／または parse_iff がその関係を直接述べていれば完了です。