From a2c2861a04ca13a4ea7f976c7bad24c226baffd1 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 27 Jan 2026 17:09:55 +0100 Subject: [PATCH] [spec] Fix limit validation for memory and table types --- .../wasm-3.0/2.1-validation.types.spectec | 4 ++-- spectec/doc/example/output/NanoWasm.pdf | Bin 245621 -> 245627 bytes spectec/test-frontend/TEST.md | 4 ++-- spectec/test-latex/TEST.md | 4 ++-- spectec/test-middlend/TEST.md | 12 ++++++------ spectec/test-prose/TEST.md | 8 ++++---- 6 files changed, 16 insertions(+), 16 deletions(-) diff --git a/specification/wasm-3.0/2.1-validation.types.spectec b/specification/wasm-3.0/2.1-validation.types.spectec index 0d74d8109e..eac31a1408 100644 --- a/specification/wasm-3.0/2.1-validation.types.spectec +++ b/specification/wasm-3.0/2.1-validation.types.spectec @@ -222,11 +222,11 @@ rule Globaltype_ok: rule Memtype_ok: C |- addrtype limits PAGE : OK - -- Limits_ok: C |- limits : $(2^16) + -- Limits_ok: C |- limits : $(2^($size(addrtype) - 16)) rule Tabletype_ok: C |- addrtype limits reftype : OK - -- Limits_ok: C |- limits : $(2^32 - 1) + -- Limits_ok: C |- limits : $(2^$size(addrtype) - 1) -- Reftype_ok: C |- reftype : OK diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index 50850e9bd53b8abcb8de415070284fcbcf327db0..270dac88bda2add7033b7a4c96b48ff378bc2cb6 100644 GIT binary patch delta 1080 zcmezRkMH+Cz71wVjFyuVg*EF_&)a4ncHm)q@VBnjP5w&PlHU{ZdAG3gw@zy2%WOMb zINRavmMs_d$6NEU%<^2{@}+^}UgLv{7xw>3tysmvqqSh-1@DGDgWIwP>t=0tm=V-+ z|MN8lJAS8}@d#ogWtou7Z6-TwXNAI6NcK3>fh!tEBqj6lq^ z-9nhzXAy^yxuLm%g^|Vdo~_K%aNhRyTbT>l0u4=F4V>J}3>{rv9L>y~4UAolOhkPW-dC4?S@nHa$kq)1Xj7w4>@G<;UOXyC*2KFg2?`q;3JKXe9O6&NN>E6&Uw?9P z`TpwlTd!Naw!D4j&HCA)QO9%)x39bJC2ss|DZ2-sQ9^H?y(S}T!rVOhl>#Y_^VZD^ zVd*-^7Aw1wWlB@M@2;pI$s4TOUVNK$%F(q;W5Mmisj4d$X)n2bHq~^+!qb-~3f)a` znR4l+pzo>Mi+cJZg>*Znx>?R$c0KJzYRJWnO)mB>%(23Ar(NTi^@8tG=GU_d?$`a6 z=WcCiE{QFS3-Y*pjKgM~ZI0ajD}I+XyIwQv_P>#(-9Gy{ z*EN?;V3&Tt)*q8(XIUv4Q<(j$e&I%M2k&Uc)eVtCZLM-US*P7C65Vwr?b-pZ$x8JZ z({;?B{MZ)#n_I5$$mDeYDHF82?y?;#J*jwH%wg(;n;hadB!wh$oo^{+dt8ePcyDI1 zC~|{win?FhoFhjZ_D-nc5SI`$;#s;#*ke}Sg~!w6)H%%;ozG1Pp6(%>V;^=?tG@pE zfjJ-;!S+HJ9m+U72mnC^-<~GJ?JK8ORc4*Mo3)g4d%LsOhHz{0OvXAYybcN delta 1102 zcmezUkMHY0z71wVj24p*Fl*MQp7-@W;=sf9;P;;{ne+q4R6b8U7aFjT-LdSz;a%+u zqe~B#iL(CR_ckn|z`s&>61&p}E|%|Y|E~HUE>=wlVDxQqRQj^`<~xpWpZ72ynj`#Y z&NerWiGe0(f6AIY`*>)#=CfbtswXtu(sHh36g+x@>r|5u=P9{u-wv9}Np?Hjf-7qSJKn>jm~IGHDOg^Or8|sXQ4tshQ`-g4N2Z3j8^jWEGz_Gi`7U_ts)@O_;r|EriGG zfb6cU`XEgUhO!r{JR%DWT%TN&eYS~b%H^k*LyIaoLN172m?(5N!EMTg%nq@qnSox% zwK~m?_$hlYe_ATxC;7DGjlxC#K>zC=%h#GVxa|_Ndb^MF$%|VrOV*@aaJufheDd}t zvt5r%etF(bt~22R2lVQcNlUW zySwUs_6L?3jNx~(+>c)ecv!UK{%%|x1d|` z^cr>b^-ZDMkIB#4%~ro<>+1(>2~%4#7b=z?+!d|2+FLe_IVL^u3IE(lZ`)+G47*fLId6~KDZd>f@hi+eX$KJc9dWq$DzqHKM{ly7>^$C6neruS& zaH7LFhX(;5sNmbvWVn6h^s0)ilYfhra&AA~>@_)0|J#(H_bzB~U~E;f04?@M6j zvD%Wj%xkr;=Utlf`>?;)=Xd^}r-d9sE=p9KlfTa z@67-ES7#-t` int) - (16 : nat <:> int)) : int <:> nat))) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec relation Tabletype_ok: `%|-%:OK`(context, tabletype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec rule _{C : context, addrtype : addrtype, limits : limits, reftype : reftype}: `%|-%:OK`(C, `%%%`_tabletype(addrtype, limits, reftype)) - -- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ 32) : nat <:> int) - (1 : nat <:> int)) : int <:> nat)) + -- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ $size((addrtype : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)) : int <:> nat)) -- Reftype_ok: `%|-%:OK`(C, reftype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 6e7984d6fb..6b6193a24b 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -5072,7 +5072,7 @@ $$ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ -C \vdash {\mathit{limits}} : {2^{16}} +C \vdash {\mathit{limits}} : {2^{{|{\mathit{addrtype}}|} - 16}} }{ C \vdash {\mathit{addrtype}}~{\mathit{limits}}~\mathsf{page} : \mathsf{ok} } \, {[\textsc{\scriptsize K{-}mem}]} @@ -5083,7 +5083,7 @@ $$ $$ \begin{array}{@{}c@{}}\displaystyle \frac{ -C \vdash {\mathit{limits}} : {2^{32}} - 1 +C \vdash {\mathit{limits}} : {2^{{|{\mathit{addrtype}}|}}} - 1 \qquad C \vdash {\mathit{reftype}} : \mathsf{ok} }{ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index cd32d52dbf..018c3d0c8a 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -3138,14 +3138,14 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec rule _{C : context, addrtype : addrtype, limits : limits}: `%|-%:OK`(C, `%%PAGE`_memtype(addrtype, limits)) - -- Limits_ok: `%|-%:%`(C, limits, (2 ^ 16)) + -- Limits_ok: `%|-%:%`(C, limits, (2 ^ ((($size((addrtype : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat))) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec relation Tabletype_ok: `%|-%:OK`(context, tabletype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec rule _{C : context, addrtype : addrtype, limits : limits, reftype : reftype}: `%|-%:OK`(C, `%%%`_tabletype(addrtype, limits, reftype)) - -- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ 32) : nat <:> int) - (1 : nat <:> int)) : int <:> nat)) + -- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ $size((addrtype : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)) : int <:> nat)) -- Reftype_ok: `%|-%:OK`(C, reftype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec @@ -14492,14 +14492,14 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec rule _{C : context, addrtype : addrtype, limits : limits}: `%|-%:OK`(C, `%%PAGE`_memtype(addrtype, limits)) - -- Limits_ok: `%|-%:%`(C, limits, (2 ^ 16)) + -- Limits_ok: `%|-%:%`(C, limits, (2 ^ ((($size((addrtype : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat))) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec relation Tabletype_ok: `%|-%:OK`(context, tabletype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec rule _{C : context, addrtype : addrtype, limits : limits, reftype : reftype}: `%|-%:OK`(C, `%%%`_tabletype(addrtype, limits, reftype)) - -- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ 32) : nat <:> int) - (1 : nat <:> int)) : int <:> nat)) + -- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ $size((addrtype : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)) : int <:> nat)) -- Reftype_ok: `%|-%:OK`(C, reftype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec @@ -25865,14 +25865,14 @@ relation Memtype_ok: `%|-%:OK`(context, memtype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec rule _{C : context, addrtype : addrtype, limits : limits}: `%|-%:OK`(C, `%%PAGE`_memtype(addrtype, limits)) - -- Limits_ok: `%|-%:%`(C, limits, (2 ^ 16)) + -- Limits_ok: `%|-%:%`(C, limits, (2 ^ ((($size((addrtype : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat))) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec relation Tabletype_ok: `%|-%:OK`(context, tabletype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec rule _{C : context, addrtype : addrtype, limits : limits, reftype : reftype}: `%|-%:OK`(C, `%%%`_tabletype(addrtype, limits, reftype)) - -- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ 32) : nat <:> int) - (1 : nat <:> int)) : int <:> nat)) + -- Limits_ok: `%|-%:%`(C, limits, ((((2 ^ $size((addrtype : addrtype <: numtype))) : nat <:> int) - (1 : nat <:> int)) : int <:> nat)) -- Reftype_ok: `%|-%:OK`(C, reftype) ;; ../../../../specification/wasm-3.0/2.1-validation.types.spectec diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index e8b5858aed..e6750e02b2 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -14776,7 +14776,7 @@ The global type :math:`({\mathsf{mut}^?}~t)` is :ref:`valid ` if: The memory type :math:`({\mathit{addrtype}}~{\mathit{limits}}~\mathsf{page})` is :ref:`valid ` if: - * The limits range :math:`{\mathit{limits}}` is :ref:`valid ` within :math:`{2^{16}}`. + * The limits range :math:`{\mathit{limits}}` is :ref:`valid ` within :math:`{2^{{|{\mathit{addrtype}}|} - 16}}`. @@ -14784,7 +14784,7 @@ The memory type :math:`({\mathit{addrtype}}~{\mathit{limits}}~\mathsf{page})` is The table type :math:`({\mathit{addrtype}}~{\mathit{limits}}~{\mathit{reftype}})` is :ref:`valid ` if: - * The limits range :math:`{\mathit{limits}}` is :ref:`valid ` within :math:`{2^{32}} - 1`. + * The limits range :math:`{\mathit{limits}}` is :ref:`valid ` within :math:`{2^{{|{\mathit{addrtype}}|}}} - 1`. * The reference type :math:`{\mathit{reftype}}` is :ref:`valid `. @@ -27294,11 +27294,11 @@ Globaltype_ok Memtype_ok - the memory type addrtype limits PAGE is valid if: - - the limits range limits is valid within (2 ^ 16). + - the limits range limits is valid within (2 ^ ($size(addrtype) - 16)). Tabletype_ok - the table type (addrtype limits reftype) is valid if: - - the limits range limits is valid within ((2 ^ 32) - 1). + - the limits range limits is valid within ((2 ^ $size(addrtype)) - 1). - the reference type reftype is valid. Externtype_ok