Tier-S: #45 Frontier 5 — Lean → Rust correspondence mechanization

[hyperpolymath]

Scope (sub-issue of #45 Frontier 5)

Lean → Rust correspondence mechanization — currently testing-based at ~85% confidence per CLAUDE.md, NOT mechanized.

Theorem targets

• rust_mkdir_refines_lean_mkdir — over the Rust AST → state-transition, prove the diagram commutes with Lean's mkdir : Path → FsState → FsState
• extracted_ocaml_observationally_equivalent_to_rust — extraction.v extracts to OCaml; should refine to the same observable behaviour as the Rust impl

Theory frontier

Idris2-via-typed-WASM bridge. Compare hyperpolymath/typed-wasm estate work. Idris2 ABI proofs at src/abi/ are the natural seam — currently unused for refinement.

Resolution

1. Pick the smallest refinement target (mkdir) — methodology PoC.
2. Two seams to explore:
   • Coq extraction to OCaml → observational-equivalence with Rust via Bisimulation
   • Idris2-to-typed-WASM bridge via src/abi/ (echo-types L3 integration)
3. Cross-doc with hyperpolymath/typed-wasm per estate directive.

References

• Parent: Filesystem-theory + practice gap analysis (POSIX 2024, atomicity, crash-consistency) #45 Frontier 5
• docs/LEAN4_RUST_CORRESPONDENCE.md
• docs/VERIFICATION_STRATEGY_ANALYSIS.md
• estate-memory: [Zig=APIs+FFIs, Idris2=ABIs]
• Related: Tier-S: crash-consistency frontier C — Idris2-via-typed-WASM crash boundary #65 (Idris2-via-typed-WASM crash boundary)