[Spec] Soundness: Make Limit max be unconstrained in Store and Store Extension Relations

[DCupello1]

Previously, some of the store relations had been constrained to only having defined max for memory and table types, i.e.

rule Extend_meminst:
  {TYPE at `[n..m] PAGE, BYTES b*} `<= {TYPE at `[n'..m] PAGE, BYTES b'*}
  -- if n <= n'
  -- if |b*| <= |b'*|

Here, m can only be defined. This PR is made to fix this issue.

[rossberg]

Thanks, looks good to me. Is there a reason why you didn't include the fixes for 1.0 and 2.0?

[DCupello1]

Thanks, looks good to me. Is there a reason why you didn't include the fixes for 1.0 and 2.0?

It would require adding the soundness files for Wasm 1.0 and 2.0, which could be done, though I feel like this isn't the right place to do it. Perhaps in another PR?

[rossberg]

Ah, right. Yes, can't harm to add those in another PR.