From ae5e6677bfeb7438c288a74032ea0d24a09a1804 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Wed, 11 Mar 2026 19:08:35 +0100
Subject: [PATCH 1/3] [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)

From 2cb08fa81a1ff7c5303b1a6af0635e634adc3919 Mon Sep 17 00:00:00 2001
From: DJ <f52985@gmail.com>
Date: Tue, 24 Mar 2026 18:13:27 +0900
Subject: [PATCH 2/3] Handle optionally itered (?) boolean premise

---
 spectec/src/backend-interpreter/interpreter.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index 16878b2572..d9c5108d98 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -212,6 +212,8 @@ and eval_expr env expr =
   let rec to_bool source = function
     | BoolV b -> b
     | ListV _ as v -> List.for_all (to_bool source) (unwrap_listv_to_list v)
+    | OptV None -> true
+    | OptV Some v -> to_bool source v
     | _ -> fail_expr source "type mismatch for boolean value"
   in
 

From 39e7c721374d314015dab6a826fb82c4fb3dfb58 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Tue, 24 Mar 2026 11:47:14 +0100
Subject: [PATCH 3/3] expects

---
 spectec/doc/example/output/NanoWasm.pdf | Bin 245508 -> 245508 bytes
 spectec/test-latex/TEST.md              |   2 ++
 spectec/test-middlend/TEST.md           |   6 ++++++
 spectec/test-prose/TEST.md              |  24 ++++++++++++++++++------
 4 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 55a94fd237f660644f89ec93da49f7332b312d84..e68ccc1d9c36f44322ea2f0feb7ff260902d8839 100644
GIT binary patch
delta 1101
zcmZqq$Jg?YZ-c22laayX1I(KBspoyO4;%2XJ=k4;w0cWoq3X@PNv{*6Ma(2j-(2{b
za4APy=k30P`g+e`jWz0fg)T8G?P)4Ve-Z!J#3qc%nKf#1|D+4NX?qoOj{g*Ta(mmc
z_l4OGK5txK8}3g|mDAtzI!A1~qQj!=ZjwJ)m0k&JPdRFQ^+fcVx6P|9Zf>%-*%|Gy
zt%iS{Q0|*oi{F=>7fA}QD{J3-`^nRZ$zKm?`pLLU7P}msRg>WtSNHn7Q<>Mc_s<UA
znes4aV}9_YlUYZOPY7r|IlXMzyVKWeG(Wx)@p$#}&!gM3bN(@8M*H|STMD;Z3Nr#R
z({@W?=4%VJjZ6#;O-xOUwG9l_4Gh#Zx%7SWQ(O{DQWZ2@tc(nd%nXcSO14{VWiDb1
za5OYCbulwEb1^eAb8&TcHnK1_HF7a@adt8>G;%etQ?Rilq$HM0-zPOMy(B}y%+eGb
z=BiV?^L+y)+V;PHb8mH&Ztlg?FaNH46;`V09=$g{HtNeNXW@DW9v|PM41$KARGpN3
zRE{m_v{(4k=;y<uBJ}O^ESt*jyRS!8uiZR<^Vu{1c17+?JtI{7`qx^M`G)$IK1CB4
zSC_PVaGqe!E@AilxqxBK<*Spp90hMISgk19EVQBCGu&5;wfcbAUB)2E8?%)@z4%rf
z$*1+=)5}#m?yzgU<a*)JnP;Hv^}@uZ`_mSUrO8uWq?48hx-EZND&Z$7TJlEWB7dO!
zb%*6^uQs#oO0#;qPcY@>trsP0)Gqj3cU?Ytdqdc+I;+1bxeH`VcBrnu6dq_WY0;0s
zu1)K!G-LCoM%FL&dzNP$p1+X2WOwM<7kTm)Our5W8Zh)VK7PPr!RgoNSRlpIX#7CO
zg8f``VgX|e)83bt@4d(rckJ6MabWrm)^)|nJUu%?>n}YBG~m?RebpwwoKJ0r_Sv)p
zQ=;GM-<`|Wop9}Kz`|XY)9$mFACQV*mwuq;EEeJK7su+I$Gf|JRyAuz_UQ!H4PJ+~
zT$phC!K~<S|Mxq!N3x#Q>H4!Uc+=epk8kJY>PyOWs-KUZIzhYZ4x3x)N$)=01}(+S
zf_fW_RSa&mZE?LeVa?tJ*WQ-+txiZk;WvlJva_?XO7W|Jo`Ft^gqJJ(1e3c9j^|oj
ztlA-1n<u`#q|@Z!$K=+<pX$r`&Ts-@XEsAE6B=w17qAckK@VZef|I#_w#v<mD%u{D
zdFAcH372NvUVYqarT%^OsmJdA<I(cnVO|$FtK|GyP2ZjC?+4B*+rNLY$>V=p95S!f
zx~m<V^ZQ-fr9J7J?oSc3DPA9*dC}P3PfNGb=&zN}%Pw{Qx>@S)?Uz^lcG@Q1q!hsZ
zs&SuSuLAe1hJAv%3q)UhzQAYYpnl=`!rPO}<u5(8KX=RidH*zn>9_YWD{`1~sj9mA
HyKw;ktP|)}

delta 1100
zcmZqq$Jg?YZ-c22lcDA01I(KBspoyYnH_o99{m2(C6j)j*Ylb3?r_J}rlyhu&TkWM
ztjj%^`<LnezTL756Z|WMC$T$iU~Q^){{O1|;YuNc6%A^K6a;@=Tyu?OcIG~YL+iXh
z6yK6kbaA_A^3*(H)^hImYO`NkzjtKHTFvuQ)I~&DTZ7w3^@Mc9P50{sTb>rwlts<U
z`6(5veCyWJ-xuD;pJ?A#^S+;b`?+r6<6Vag&&aUPENW;oU6lWS&mQS>PGw$YFJ3P&
zOSOsaiS03pUYqbiP|E)IrO;OkYp!`eTP@Y1a`w6S{d;Mjxie1rcs5%Jw_6D_0x{Ee
zD`Dnq3$+am4b4rAO-!{74Al(`)HS*Eee+XX5=&AQG+eBV42;YSjA2T)TW@79V)HjJ
zFmpC?ax<{BurM+=F)?<ra5Qo<G<S3{c6Bj!GO<&zu_UA<mP_9!H7~s+L&3~)@_uHm
zdf6$K{-S{rZTsKz%~ohy&~Tz?Vy$qX%blB3o;GoHEIP!xWb-F}3E}MMT$PJAJ|2}2
zc1~SmI_n3s&lmQL#N@=pMW6Saom_rzX7RH*)$^>=(*ECBbI2&Ib7$%Qz+JNp^=*BM
zCNQop`MQKfq``ET^Ae{3mQN+6OOgVZuD#6itahl^ys==l;?%~y36tL`tdx1<Ey!BJ
zzGDr;)RNYct1<7`LrYvsmbjQp2rezDa+&;To5tegX)fGJO9TCuzuYQWCONfajlxC#
ziw@UamM=AJQro3m5>;z_;?ma3nbEorIAYD`mfhpJ^@8oim&se2`7XSi_GXEDpvlCf
z^OHrM#+PW^&8rWMT&j00&oFHH1@5XltBQBs=I?7_Ea2g3di;Pzf=T_Lfd#AEfy@H7
zIjqkQR2DGCusmL%Uwb=yZ>~tsMlt3eLgfc|^J18U^Gx4={h%^~ar)gX`IWPoF854L
zD^9q!_TBb(&kiunC||7~RNng1{DAHTwoeJNcb-kmKBKO_zS(tq{W5u}-7H(S%uZl6
z@IJKRf^zx6P0?lZ^|sCoEtu>%(SD2fH0h$6(`)~#^1DAe`8iDWNte*}gPgHNCpK~h
zsHT`5Vl8W9al1WX+X<;jTluf-?Cr@Cd&6_HbF!kkp<#gj61hXHZLK`cD_^ioTE_lm
z*V5yjhk9R>OW(bqdWq$Bzv#C5Q}-<m)Io3><1ZF;$Sz<Z0)igG$q9FIUrmjh7gbch
z|I(7%j|G={=UMwt4T|6AtL?k<uWZ<?viyH5Odi{rtv7i+Z~yWs#q~ctGtbrT4#>Rs
zce78A_B;E}Ug5Tr|E?-IYs_CYRm|pdtw-j?$<}waU7DnRzHX-aZuy`+m5R5!9XT@?
zdL8a}q)lMe1yW%b*uGT0V3@mr`^D!Ak5AsdTk@;C_?!HC^J(1EZ|`GP<S^q>Rdw}u
G;{pJl_UL2)

diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index aa7136b61d..807228791c 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -9296,6 +9296,7 @@ $$
 {\land}~ {\mathit{tableinst}'} = \{ \mathsf{type}~({\mathit{at}}~{}[ {i'} .. {j^?} ]~{\mathit{rt}}),\; \mathsf{refs}~{{r'}^\ast}~{r^{n}} \} \\
 {\land}~ {i'} = {|{{r'}^\ast}|} + n \\
 {\land}~ ({i'} \leq j)^? \\
+{\land}~ {i'} \leq {2^{{|{\mathit{at}}|}}} - 1 \\
 \end{array} \\
 \end{array}
 $$
@@ -9308,6 +9309,7 @@ $$
 {\land}~ {\mathit{meminst}'} = \{ \mathsf{type}~({\mathit{at}}~{}[ {i'} .. {j^?} ]~\mathsf{page}),\; \mathsf{bytes}~{b^\ast}~{(\mathtt{0x00})^{n \cdot 64 \, {\mathrm{Ki}}}} \} \\
 {\land}~ {i'} = {|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n \\
 {\land}~ ({i'} \leq j)^? \\
+{\land}~ {i'} \leq {2^{{|{\mathit{at}}|} - 16}} \\
 \end{array} \\
 \end{array}
 $$
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 0a4552419a..3b0a7c6934 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -5809,6 +5809,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
@@ -5818,6 +5819,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)
@@ -17224,6 +17226,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)))
   def $growtable{x0 : tableinst, x1 : nat, x2 : ref}(x0, x1, x2) = ?()
 
 ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec
@@ -17234,6 +17237,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)))
   def $growmem{x0 : meminst, x1 : nat}(x0, x1) = ?()
 
 ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec
@@ -28765,6 +28769,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)))
   def $growtable{x0 : tableinst, x1 : nat, x2 : ref}(x0, x1, x2) = ?()
 
 ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec
@@ -28775,6 +28780,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)))
   def $growmem{x0 : meminst, x1 : nat}(x0, x1) = ?()
 
 ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index 7f19a5e8f6..48f3fa6335 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -25817,7 +25817,11 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
 
 #. Let :math:`{i'}` be :math:`{|{{r'}^\ast}|} + n`.
 
-#. If :math:`{({i'} \leq j)^?}`, then:
+#. If not :math:`{({i'} \leq j)^?}`, then:
+
+   a. Fail.
+
+#. If :math:`{i'} \leq {2^{{|{\mathit{at}}|}}} - 1`, then:
 
    a. Let :math:`{\mathit{tableinst}'}` be the table instance :math:`\{ \mathsf{type}~({\mathit{at}}~{}[ {i'} .. {j^?} ]~{\mathit{rt}}),\;\allowbreak \mathsf{refs}~{{r'}^\ast}~{r^{n}} \}`.
 
@@ -25834,7 +25838,11 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
 
 #. Let :math:`{i'}` be :math:`{|{b^\ast}|} / (64 \, {\mathrm{Ki}}) + n`.
 
-#. If :math:`{({i'} \leq j)^?}`, then:
+#. If not :math:`{({i'} \leq j)^?}`, then:
+
+   a. Fail.
+
+#. If :math:`{i'} \leq {2^{{|{\mathit{at}}|} - 16}}`, then:
 
    a. Let :math:`{\mathit{meminst}'}` be the memory instance :math:`\{ \mathsf{type}~({\mathit{at}}~{}[ {i'} .. {j^?} ]~\mathsf{page}),\;\allowbreak \mathsf{bytes}~{b^\ast}~{\mathtt{0x00}^{n \cdot 64 \, {\mathrm{Ki}}}} \}`.
 
@@ -32693,18 +32701,22 @@ add_exninst (s, f) exn*
 growtable tableinst n r
 1. Let { TYPE: (at ([ i .. j? ]) rt); REFS: r'* } be tableinst.
 2. Let i' be (|r'*| + n).
-3. If (i' <= j)?, then:
+3. If not (i' <= j)?, then:
+  a. Fail.
+4. If (i' <= ((2 ^ $size(at)) - 1)), then:
   a. Let tableinst' be { TYPE: (at ([ i' .. j? ]) rt); REFS: r'* :: r^n }.
   b. Return tableinst'.
-4. Fail.
+5. Fail.
 
 growmem meminst n
 1. Let { TYPE: at ([ i .. j? ]) PAGE; BYTES: b* } be meminst.
 2. Let i' be ((|b*| / (64 * $Ki())) + n).
-3. If (i' <= j)?, then:
+3. If not (i' <= j)?, then:
+  a. Fail.
+4. If (i' <= (2 ^ ($size(at) - 16))), then:
   a. Let meminst' be { TYPE: at ([ i' .. j? ]) PAGE; BYTES: b* :: 0^(n * (64 * $Ki())) }.
   b. Return meminst'.
-4. Fail.
+5. Fail.
 
 inst_valtype moduleinst t
 1. Let dt* be moduleinst.TYPES.