From ae5e6677bfeb7438c288a74032ea0d24a09a1804 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 11 Mar 2026 19:08:35 +0100 Subject: [PATCH] [spec] Add missing side condition on growtable/memory --- specification/wasm-3.0/4.0-execution.configurations.spectec | 2 ++ specification/wasm-latest/4.0-execution.configurations.spectec | 2 ++ spectec/test-frontend/TEST.md | 2 ++ 3 files changed, 6 insertions(+) diff --git a/specification/wasm-3.0/4.0-execution.configurations.spectec b/specification/wasm-3.0/4.0-execution.configurations.spectec index d7c2ce8f93..58e494ad70 100644 --- a/specification/wasm-3.0/4.0-execution.configurations.spectec +++ b/specification/wasm-3.0/4.0-execution.configurations.spectec @@ -318,9 +318,11 @@ def $growtable(tableinst, n, r) = tableinst' -- if tableinst' = { TYPE (at `[i' .. j?] rt), REFS r'* r^n } -- if $(i' = |r'*| + n) -- (if i' <= j)? + -- if i' <= $(2^$size(at) - 1) def $growmem(meminst, n) = meminst' -- if meminst = { TYPE (at `[i .. j?] PAGE), BYTES b* } -- if meminst' = { TYPE (at `[i' .. j?] PAGE), BYTES b* (0x00)^(n * $($(64 * $Ki))) } -- if $(i' = |b*| / (64 * $Ki) + n) -- (if i' <= j)? + -- if i' <= $(2^($size(at) - 16)) diff --git a/specification/wasm-latest/4.0-execution.configurations.spectec b/specification/wasm-latest/4.0-execution.configurations.spectec index d7c2ce8f93..58e494ad70 100644 --- a/specification/wasm-latest/4.0-execution.configurations.spectec +++ b/specification/wasm-latest/4.0-execution.configurations.spectec @@ -318,9 +318,11 @@ def $growtable(tableinst, n, r) = tableinst' -- if tableinst' = { TYPE (at `[i' .. j?] rt), REFS r'* r^n } -- if $(i' = |r'*| + n) -- (if i' <= j)? + -- if i' <= $(2^$size(at) - 1) def $growmem(meminst, n) = meminst' -- if meminst = { TYPE (at `[i .. j?] PAGE), BYTES b* } -- if meminst' = { TYPE (at `[i' .. j?] PAGE), BYTES b* (0x00)^(n * $($(64 * $Ki))) } -- if $(i' = |b*| / (64 * $Ki) + n) -- (if i' <= j)? + -- if i' <= $(2^($size(at) - 16)) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index fd20528ef7..e2b04ba40f 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -5819,6 +5819,7 @@ def $growtable(tableinst : tableinst, nat : nat, ref : ref) : tableinst -- if (tableinst' = {TYPE `%%%`_tabletype(at, `[%..%]`_limits(i', j?{j <- `j?`}), rt), REFS r'*{r' <- `r'*`} ++ r^n{}}) -- if (i'!`%`_u64.0 = (|r'*{r' <- `r'*`}| + n)) -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`} + -- if ((i'!`%`_u64.0 : nat <:> int) <= (((2 ^ $size((at : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int))) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec def $growmem(meminst : meminst, nat : nat) : meminst @@ -5828,6 +5829,7 @@ def $growmem(meminst : meminst, nat : nat) : meminst -- if (meminst' = {TYPE `%%PAGE`_memtype(at, `[%..%]`_limits(i', j?{j <- `j?`})), BYTES b*{b <- `b*`} ++ `%`_byte(0)^(n * (64 * $Ki)){}}) -- if ((i'!`%`_u64.0 : nat <:> rat) = (((|b*{b <- `b*`}| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) + (n : nat <:> rat))) -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`} + -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat))) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec relation Num_ok: `%|-%:%`(store, num, numtype)