Add Lean 4 showcase proofs for issue 452 constructor lowering

[peter941221]

Summary

• add a small standalone Lean 4 showcase project under lean/
• model the core enum and witness semantics behind issue_452
• prove constructor-only lowering preservation and witness preservation
• document the current proof boundary for unsupported pure enum match lowering
• add a Rust-to-Lean proof mapping note

Scope

This PR is intentionally a showcase and documentation layer. It does not replace the main Boogie + Z3 verification pipeline and it does not claim full correctness of the entire prover.

Included modules

• Core for the tiny enum model and base theorems
• PureLowering for constructor-lowering preservation
• QuantifierView for the existential witness / exists!-style view
• MatchBoundary for the currently unsupported pure enum match boundary
• ProofToCode.md for Rust-to-Lean concept mapping

Validation

• lake build

Notes for reviewers

• The proof scope is deliberately limited to the constructor-only subset fixed by issue_452.
• The MatchBoundary module explicitly states that pure enum match lowering remains unsupported.
• This PR is designed to be reviewed independently from the Rust bugfix PR for easier focus.
• This PR has no runtime impact on the existing prover pipeline.

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

^{Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

[cursor]

Windows backslash in snapshot breaks cross-platform CI

High Severity

The snapshot file contains a Windows-style backslash path separator (tests/inputs\pure_functions\issue_452_match.move) whereas every other snapshot in the same directory uses forward slashes (tests/inputs/pure_functions/...). This snapshot was generated on Windows and will cause insta snapshot assertion failures on Linux/macOS CI, since the post_process_output function only replaces the sources_dir prefix but does not normalize remaining path separators in the output.

 

[cursor]

Personal filesystem path committed in README

Low Severity

The README contains a developer's personal Windows filesystem path (C:\Users\peter\.elan\bin\lake.exe). This is a local development artifact that leaks a developer's username and is not useful guidance for other contributors. A generic or environment-variable-based path reference would be more appropriate.