I don’t think the OP is starting from WASM code; they’re starting from a language with SIMD primitives that map closely to those of WASM. There, you often have information to prove function arguments do not alias.