From f2f9d35ed8fbb08640839ea61b06b693134c8fe3 Mon Sep 17 00:00:00 2001 From: raoxiaojia Date: Mon, 23 Mar 2026 08:39:44 -0700 Subject: [PATCH 1/4] fix subst_externtype matching incorrect argtypes --- specification/wasm-3.0/1.2-syntax.types.spectec | 2 +- spectec/test-prose/TEST.md | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/specification/wasm-3.0/1.2-syntax.types.spectec b/specification/wasm-3.0/1.2-syntax.types.spectec index b354619610..ba57c57a2b 100644 --- a/specification/wasm-3.0/1.2-syntax.types.spectec +++ b/specification/wasm-3.0/1.2-syntax.types.spectec @@ -421,7 +421,7 @@ def $subst_externtype((TAG jt), tv*, tu*) = TAG $subst_tagtype(jt, tv*, tu*) def $subst_externtype((GLOBAL gt), tv*, tu*) = GLOBAL $subst_globaltype(gt, tv*, tu*) def $subst_externtype((TABLE tt), tv*, tu*) = TABLE $subst_tabletype(tt, tv*, tu*) def $subst_externtype((MEM mt), tv*, tu*) = MEM $subst_memtype(mt, tv*, tu*) -def $subst_externtype((FUNC dt), tv*, tu*) = FUNC $subst_deftype(dt, tv*, tu*) +def $subst_externtype((FUNC tu_1), tv*, tu*) = FUNC $subst_typeuse(tu_1, tv*, tu*) def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)* diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 34fdf8a1df..2a0cbe78cf 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -22321,9 +22321,9 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Assert: Due to validation, :math:`{\mathit{externtype}}` is some :math:`\mathsf{func}~{\mathit{typeuse}}`. -#. Let :math:`(\mathsf{func}~{\mathit{dt}})` be the destructuring of :math:`{\mathit{externtype}}`. +#. Let :math:`(\mathsf{func}~{\mathit{tu}}_1)` be the destructuring of :math:`{\mathit{externtype}}`. -#. Return :math:`(\mathsf{func}~{{\mathit{dt}}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]})`. +#. Return :math:`(\mathsf{func}~{{\mathit{tu}}_1}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]})`. :math:`{{{\mathit{xt}}_1^\ast}~\rightarrow~{{\mathit{xt}}_2^\ast}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]}` @@ -31066,8 +31066,8 @@ subst_externtype externtype tv* tu* a. Let (MEM mt) be externtype. b. Return (MEM $subst_memtype(mt, tv*, tu*)). 5. Assert: Due to validation, externtype is some FUNC. -6. Let (FUNC dt) be externtype. -7. Return (FUNC $subst_deftype(dt, tv*, tu*)). +6. Let (FUNC tu_1) be externtype. +7. Return (FUNC $subst_typeuse(tu_1, tv*, tu*)). subst_moduletype xt_1* -> xt_2* tv* tu* 1. Return $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)*. From fbd873f118beaf6a032d306909dc18d4743ff899 Mon Sep 17 00:00:00 2001 From: raoxiaojia Date: Mon, 23 Mar 2026 09:13:59 -0700 Subject: [PATCH 2/4] slight change to arg names from review, sync to latest, and test expects --- specification/wasm-3.0/1.2-syntax.types.spectec | 2 +- specification/wasm-latest/1.2-syntax.types.spectec | 2 +- spectec/test-prose/TEST.md | 8 ++++---- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/specification/wasm-3.0/1.2-syntax.types.spectec b/specification/wasm-3.0/1.2-syntax.types.spectec index ba57c57a2b..96acf96d84 100644 --- a/specification/wasm-3.0/1.2-syntax.types.spectec +++ b/specification/wasm-3.0/1.2-syntax.types.spectec @@ -421,7 +421,7 @@ def $subst_externtype((TAG jt), tv*, tu*) = TAG $subst_tagtype(jt, tv*, tu*) def $subst_externtype((GLOBAL gt), tv*, tu*) = GLOBAL $subst_globaltype(gt, tv*, tu*) def $subst_externtype((TABLE tt), tv*, tu*) = TABLE $subst_tabletype(tt, tv*, tu*) def $subst_externtype((MEM mt), tv*, tu*) = MEM $subst_memtype(mt, tv*, tu*) -def $subst_externtype((FUNC tu_1), tv*, tu*) = FUNC $subst_typeuse(tu_1, tv*, tu*) +def $subst_externtype((FUNC tu'), tv*, tu*) = FUNC $subst_typeuse(tu', tv*, tu*) def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)* diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index b354619610..96acf96d84 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/specification/wasm-latest/1.2-syntax.types.spectec @@ -421,7 +421,7 @@ def $subst_externtype((TAG jt), tv*, tu*) = TAG $subst_tagtype(jt, tv*, tu*) def $subst_externtype((GLOBAL gt), tv*, tu*) = GLOBAL $subst_globaltype(gt, tv*, tu*) def $subst_externtype((TABLE tt), tv*, tu*) = TABLE $subst_tabletype(tt, tv*, tu*) def $subst_externtype((MEM mt), tv*, tu*) = MEM $subst_memtype(mt, tv*, tu*) -def $subst_externtype((FUNC dt), tv*, tu*) = FUNC $subst_deftype(dt, tv*, tu*) +def $subst_externtype((FUNC tu'), tv*, tu*) = FUNC $subst_typeuse(tu', tv*, tu*) def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)* diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 2a0cbe78cf..52adee8fcc 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -22321,9 +22321,9 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #. Assert: Due to validation, :math:`{\mathit{externtype}}` is some :math:`\mathsf{func}~{\mathit{typeuse}}`. -#. Let :math:`(\mathsf{func}~{\mathit{tu}}_1)` be the destructuring of :math:`{\mathit{externtype}}`. +#. Let :math:`(\mathsf{func}~{\mathit{tu}'})` be the destructuring of :math:`{\mathit{externtype}}`. -#. Return :math:`(\mathsf{func}~{{\mathit{tu}}_1}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]})`. +#. Return :math:`(\mathsf{func}~{{\mathit{tu}'}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]})`. :math:`{{{\mathit{xt}}_1^\ast}~\rightarrow~{{\mathit{xt}}_2^\ast}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]}` @@ -31066,8 +31066,8 @@ subst_externtype externtype tv* tu* a. Let (MEM mt) be externtype. b. Return (MEM $subst_memtype(mt, tv*, tu*)). 5. Assert: Due to validation, externtype is some FUNC. -6. Let (FUNC tu_1) be externtype. -7. Return (FUNC $subst_typeuse(tu_1, tv*, tu*)). +6. Let (FUNC tu') be externtype. +7. Return (FUNC $subst_typeuse(tu', tv*, tu*)). subst_moduletype xt_1* -> xt_2* tv* tu* 1. Return $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)*. From d03dfd2e26c4a57b441bc6878450974fc0fbaa16 Mon Sep 17 00:00:00 2001 From: raoxiaojia Date: Mon, 23 Mar 2026 09:22:18 -0700 Subject: [PATCH 3/4] test promote for frontend --- spectec/test-frontend/TEST.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 2dcddd8853..23ae1351f3 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -1281,7 +1281,7 @@ def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_externtype{mt : memtype, `tv*` : typevar*, `tu*` : typeuse*}(MEM_externtype(mt), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = MEM_externtype($subst_memtype(mt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec - def $subst_externtype{dt : deftype, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype(($subst_deftype(dt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : deftype <: typeuse)) + def $subst_externtype{tu' : typeuse, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype(tu'), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype($subst_typeuse(tu', tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_moduletype(moduletype : moduletype, typevar*, typeuse*) : moduletype From 51afe2a0fa2c9a7a8ab28502046e9441120d2da2 Mon Sep 17 00:00:00 2001 From: raoxiaojia Date: Mon, 23 Mar 2026 09:28:15 -0700 Subject: [PATCH 4/4] should be all test expects --- spectec/test-latex/TEST.md | 2 +- spectec/test-middlend/TEST.md | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 763ae1162f..03f0af71ad 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -3341,7 +3341,7 @@ $$ {(\mathsf{global}~{\mathit{gt}})}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} & = & \mathsf{global}~{{\mathit{gt}}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} \\ {(\mathsf{table}~{\mathit{tt}})}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} & = & \mathsf{table}~{{\mathit{tt}}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} \\ {(\mathsf{mem}~{\mathit{mt}})}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} & = & \mathsf{mem}~{{\mathit{mt}}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} \\ -{(\mathsf{func}~{\mathit{dt}})}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} & = & \mathsf{func}~{{\mathit{dt}}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} \\ +{(\mathsf{func}~{\mathit{tu}'})}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} & = & \mathsf{func}~{{\mathit{tu}'}}{{}[ {{\mathit{tv}}^\ast} := {{\mathit{tu}}^\ast} ]} \\ \end{array} $$ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 261da39e2c..dc5dd9de35 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -1271,7 +1271,7 @@ def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_externtype{mt : memtype, `tv*` : typevar*, `tu*` : typeuse*}(MEM_externtype(mt), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = MEM_externtype($subst_memtype(mt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec - def $subst_externtype{dt : deftype, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype(($subst_deftype(dt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : deftype <: typeuse)) + def $subst_externtype{tu' : typeuse, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype(tu'), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype($subst_typeuse(tu', tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_moduletype(moduletype : moduletype, typevar*, typeuse*) : moduletype @@ -12683,7 +12683,7 @@ def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_externtype{mt : memtype, `tv*` : typevar*, `tu*` : typeuse*}(MEM_externtype(mt), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = MEM_externtype($subst_memtype(mt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec - def $subst_externtype{dt : deftype, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype(($subst_deftype(dt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : deftype <: typeuse)) + def $subst_externtype{tu' : typeuse, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype(tu'), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype($subst_typeuse(tu', tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_moduletype(moduletype : moduletype, typevar*, typeuse*) : moduletype @@ -24097,7 +24097,7 @@ def $subst_externtype(externtype : externtype, typevar*, typeuse*) : externtype ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_externtype{mt : memtype, `tv*` : typevar*, `tu*` : typeuse*}(MEM_externtype(mt), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = MEM_externtype($subst_memtype(mt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec - def $subst_externtype{dt : deftype, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype((dt : deftype <: typeuse)), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype(($subst_deftype(dt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : deftype <: typeuse)) + def $subst_externtype{tu' : typeuse, `tv*` : typevar*, `tu*` : typeuse*}(FUNC_externtype(tu'), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = FUNC_externtype($subst_typeuse(tu', tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec def $subst_moduletype(moduletype : moduletype, typevar*, typeuse*) : moduletype