[spectec] Wasm 1.0: `Limits_sub` missing cases involving an absent maximum

[lzy0505]

The Wasm 1.0 Limits_sub relation only matches limits for which both sides have an explicit maximum.

Current spectec rule

rule Limits_sub:
  |- `[n_11 .. n_12] <: `[n_21 .. n_22]
  -- if n_11 >= n_21
  -- if n_12 <= n_22

The WebAssembly Specification, Release 1.0 PDF Section 4.5.2 allows the maximum to be absent:

n₁ ≥ n₂
────────────────────────────────────────────────────
⊢ {min n₁, max m₁?} ≤ {min n₂, max ε}

The fix should follow Wasm 3.0:

rule Limits_sub/max:
  |- `[n_11 .. n_12] <: `[n_21 .. n_22?]
  -- if n_11 >= n_21
  -- (if n_12 <= n_22)?

rule Limits_sub/eps:
  |- `[n_11 .. eps] <: `[n_21 .. eps]
  -- if n_11 >= n_21