diff --git a/specification/wasm-3.0/7.1-soundness.configurations.spectec b/specification/wasm-3.0/7.1-soundness.configurations.spectec index 63bbd7d97b..6b8f56cbb4 100644 --- a/specification/wasm-3.0/7.1-soundness.configurations.spectec +++ b/specification/wasm-3.0/7.1-soundness.configurations.spectec @@ -87,13 +87,13 @@ rule Globalinst_ok: -- Val_ok: s |- val : t rule Meminst_ok: - s |- {TYPE at `[n..m] PAGE, BYTES b*} : at `[n..m] PAGE - -- Memtype_ok: {} |- at `[n..m] PAGE : OK + s |- {TYPE at `[n..m?] PAGE, BYTES b*} : at `[n..m?] PAGE + -- Memtype_ok: {} |- at `[n..m?] PAGE : OK -- if |b*| = $(n * $($(64 * $Ki))) rule Tableinst_ok: - s |- {TYPE at `[n..m] rt, REFS ref*} : at `[n..m] rt - -- Tabletype_ok: {} |- at `[n..m] rt : OK + s |- {TYPE at `[n..m?] rt, REFS ref*} : at `[n..m?] rt + -- Tabletype_ok: {} |- at `[n..m?] rt : OK -- if |ref*| = n -- (Ref_ok: s |- ref : rt)* @@ -263,12 +263,12 @@ rule Extend_globalinst: -- if mut? = MUT \/ val = val' rule Extend_meminst: - {TYPE at `[n..m] PAGE, BYTES b*} `<= {TYPE at `[n'..m] PAGE, BYTES b'*} + {TYPE at `[n..m?] PAGE, BYTES b*} `<= {TYPE at `[n'..m?] PAGE, BYTES b'*} -- if n <= n' -- if |b*| <= |b'*| rule Extend_tableinst: - {TYPE at `[n..m] rt, REFS ref*} `<= {TYPE at `[n'..m] rt, REFS ref'*} + {TYPE at `[n..m?] rt, REFS ref*} `<= {TYPE at `[n'..m?] rt, REFS ref'*} -- if n <= n' -- if |ref*| <= |ref'*| diff --git a/specification/wasm-latest/7.1-soundness.configurations.spectec b/specification/wasm-latest/7.1-soundness.configurations.spectec index 63bbd7d97b..6b8f56cbb4 100644 --- a/specification/wasm-latest/7.1-soundness.configurations.spectec +++ b/specification/wasm-latest/7.1-soundness.configurations.spectec @@ -87,13 +87,13 @@ rule Globalinst_ok: -- Val_ok: s |- val : t rule Meminst_ok: - s |- {TYPE at `[n..m] PAGE, BYTES b*} : at `[n..m] PAGE - -- Memtype_ok: {} |- at `[n..m] PAGE : OK + s |- {TYPE at `[n..m?] PAGE, BYTES b*} : at `[n..m?] PAGE + -- Memtype_ok: {} |- at `[n..m?] PAGE : OK -- if |b*| = $(n * $($(64 * $Ki))) rule Tableinst_ok: - s |- {TYPE at `[n..m] rt, REFS ref*} : at `[n..m] rt - -- Tabletype_ok: {} |- at `[n..m] rt : OK + s |- {TYPE at `[n..m?] rt, REFS ref*} : at `[n..m?] rt + -- Tabletype_ok: {} |- at `[n..m?] rt : OK -- if |ref*| = n -- (Ref_ok: s |- ref : rt)* @@ -263,12 +263,12 @@ rule Extend_globalinst: -- if mut? = MUT \/ val = val' rule Extend_meminst: - {TYPE at `[n..m] PAGE, BYTES b*} `<= {TYPE at `[n'..m] PAGE, BYTES b'*} + {TYPE at `[n..m?] PAGE, BYTES b*} `<= {TYPE at `[n'..m?] PAGE, BYTES b'*} -- if n <= n' -- if |b*| <= |b'*| rule Extend_tableinst: - {TYPE at `[n..m] rt, REFS ref*} `<= {TYPE at `[n'..m] rt, REFS ref'*} + {TYPE at `[n..m?] rt, REFS ref*} `<= {TYPE at `[n'..m?] rt, REFS ref'*} -- if n <= n' -- if |ref*| <= |ref'*|