Prove parser/encoder round-trip identity

[avrabe]

Overview

Prove that parse_wasm(encode_wasm(module)) == Ok(module) for well-formed modules.

Property

∀ m: Module. parse_wasm(encode_wasm(m)?) == Ok(m)

Implementation

1. Translate parse_wasm to Rocq (or subset)
2. Translate encode_wasm to Rocq (or subset)
3. Prove round-trip identity

Depends on

• Add Rocq formal verification support using rules_rocq_rust #45 (Rocq foundation)

Files

• loom-core/src/lib.rs (parse_wasm, encode_wasm)
• proofs/codec/roundtrip.v (new)