Interesting. Do I have to write specs in Lean against the Wasm semantics or can you annotate Rust directly?