refactor: separate proof/spec files into a dedicated LckSpec lake target

Problem

Spec and proof files (RegexSpec.lean, DesugarSpec.lean, ParserSpec.lean, etc.) are included in the main Lck library target. This means every downstream user of the library also compiles the proof infrastructure, which is heavyweight (imports Mathlib, long compile times).

Expected fix

Move spec/proof files into a separate LckSpec Lake target (or library) that is only built when explicitly requested (e.g., for verification or CI). The main Lck target should contain only the runtime-relevant code.

References

• Suggested by AI code review on PR #9

現在の Lake ターゲット定義と、一覧にある spec/proof ファイル（RegexSpec.lean、DesugarSpec.lean、ParserSpec.lean を含む）を調査します。どのファイルがメインの Lck ターゲットに取り込まれているかを確認し、それらを明示的にビルドされる LckSpec ターゲットに分離します。その際、ランタイムに関係するコードは Lck に残します。Lck の下流ビルドで proof インフラストラクチャがコンパイルされなくなり、LckSpec が引き続き検証または CI に利用できれば完了です。