The article mentions also other instructions that trap than just memory accesses, so proving statically when those can't trap could still help. BTW. The trick

The article mentions also other instructions that trap than just memory accesses, so proving statically when those can't trap could still help. BTW. The trick that many WASM runtimes use is to allocate 8GB of address space for each linear memory, which a 32-bit pointer + 32-bit offset won't exceed. While fast, that can be limiting: On x86-64, you may only get 47 bits for user-space addresses (one bit reserved for kernel space). On 64-bit RISC-V, the address space bits could be as low as 39. 39-1-33 = 5 bits, limiting you to at most 31 instances in a runtime.