From a664a86bb556d9beb6d0a3f05a7123915a2cc359 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 2 Apr 2026 10:30:41 +0200 Subject: [PATCH 1/3] [interpreter] Remove redundant substitution in Invoke reduction --- interpreter/exec/eval.ml | 3 +- .../wasm-3.0/4.2-execution.types.spectec | 16 +++----- spectec/doc/example/output/NanoWasm.pdf | Bin 245508 -> 245512 bytes spectec/test-prose/TEST.md | 35 +++++------------- 4 files changed, 16 insertions(+), 38 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 33ffa9a029..ab78027fed 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -1122,8 +1122,7 @@ let rec step (c : config) : config = | Func.AstFunc (_, inst', func) -> let Func (_x, ls, es) = func.it in let m = Lib.Promise.value inst' in - let s = subst_of m in - let ts = List.map (fun {it = Local t; _} -> subst_valtype s t) ls in + let ts = List.map (fun {it = Local t; _} -> t) ls in let lvs = List.(rev (map Option.some args) @ map default_value ts) in let frame' = {inst = m; locals = List.map ref lvs} in let instr' = [Label (n2, [], ([], List.map plain es)) @@ func.at] in diff --git a/specification/wasm-3.0/4.2-execution.types.spectec b/specification/wasm-3.0/4.2-execution.types.spectec index 5f9f9c881e..2b29f46613 100644 --- a/specification/wasm-3.0/4.2-execution.types.spectec +++ b/specification/wasm-3.0/4.2-execution.types.spectec @@ -8,14 +8,8 @@ def $inst_globaltype(moduleinst, globaltype) : globaltype hint(show $inst_(%,%) def $inst_memtype(moduleinst, memtype) : memtype hint(show $inst_(%,%)) hint(macro "insttype") def $inst_tabletype(moduleinst, tabletype) : tabletype hint(show $inst_(%,%)) hint(macro "insttype") -;; TODO(3, rossberg): make inlining moduleinst.TYPES work -def $inst_valtype(moduleinst, t) = $subst_all_valtype(t, dt*) - -- if dt* = moduleinst.TYPES -def $inst_reftype(moduleinst, rt) = $subst_all_reftype(rt, dt*) - -- if dt* = moduleinst.TYPES -def $inst_globaltype(moduleinst, gt) = $subst_all_globaltype(gt, dt*) - -- if dt* = moduleinst.TYPES -def $inst_memtype(moduleinst, mt) = $subst_all_memtype(mt, dt*) - -- if dt* = moduleinst.TYPES -def $inst_tabletype(moduleinst, tt) = $subst_all_tabletype(tt, dt*) - -- if dt* = moduleinst.TYPES +def $inst_valtype(moduleinst, t) = $subst_all_valtype(t, moduleinst.TYPES) +def $inst_reftype(moduleinst, rt) = $subst_all_reftype(rt, moduleinst.TYPES) +def $inst_globaltype(moduleinst, gt) = $subst_all_globaltype(gt, moduleinst.TYPES) +def $inst_memtype(moduleinst, mt) = $subst_all_memtype(mt, moduleinst.TYPES) +def $inst_tabletype(moduleinst, tt) = $subst_all_tabletype(tt, moduleinst.TYPES) diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index e68ccc1d9c36f44322ea2f0feb7ff260902d8839..a06cbe5ef5e286b835bfe782ec841562ff1210a1 100644 GIT binary patch delta 1109 zcmZqq$JgRIJ&GuvYiX>)vU`*)T9aI&gF$by+QQ(E#2Uh^hepPR05-$c@W z`C3N9jpApM>yDqYiK{R_s`JjN!Dancqf^{2SJcBay3V( z(;Z%0wyjRS|8}0{k#&FX$$rZVo~GV+m3z5Gp-k!-LDB3_3;%sS6hsQ)l_G$vFg$HT5;%!w{h_G(g?)&$|K67Vq`nWe+3AbAbGXgQw zb}M1#s|)o_42%p7j4X{TwGE8a4Gh#Zx%7SWQ(O{DQWZ2@tc(nd%nXo~Y`5FWoW~Yu z;cRSTZ0KxmVQ6gWX5eV*Y+z|_U})juY;J5}WMpA!r(i=+Ni3JXPikIzNrr-%r3E^t0x9gQf-yIux&Jq8+_=Tm@M1<%&JQl< zq@LE+t=@lFU&&uMcI?oM7dH8ypUf>kXIXr1?(@ExH|@<=Z|I3k%6nTs<(bj5rR<)3 zMi0zlWi=UD6I$OftP~Jw4BZtKWO$;yoQWj5cuRTzIQKwfU~*qJ}*A z>7olJt(&l}>$GixeypIZ=0)B#7tOhC8G-Y}QcKoM%5Z*Ta_Z%lJ$#2X7f1$dyBsU4GJNqRiEr|25ZQKzKySVLm#1z{gw;t1puSC<*5Jw delta 1105 zcmeD9$Jg?YZ-bc-qrv0@%$oJ7=Y6ve8}P6_*j<0LdP`!V>dn4MuM?z2%p^?TT=<%B zDMwr9?Y@Nide2~uHR^kXE-@?ZX(~v65&zf3CXC6MHEMGIqzk-hdlhqz{}g(1d)u-1 zh1m{1Z(Ls+?oUpY)8F$tM{K*I!=meMl0R9MUI}YYIcj|MMD&`s&8sbLZnC%88SSvG zhJT$iNeZtkYu|hO$e$+$}vyBwWWli?Rv_xik3nb)@W&ko+1 z@-Sy(e(XL)7NV>KfV(2c=htnquaA{{xM`m`}j6n3%6SfGXgQw zc57kgs|)pwjZ6#;O-xOUwG9l_4Gh#Zx%7SWQ(O{DQWZ2@tc(nd%nXo~Y`5RaoW~Yu z>1b$X>SAVS=3-`K=Hlw?Y-C|57Q{$2MftW?uIdT)Ge)R$Gx!u1Y3KE6j81Pwo_Iw|?6 z99z<9ukfeQ&xc1v=-cO6HkIFZUyrI@yLtZRvuFP8irkrcMyUApueB!g4fQR3iY73w zE@}7RJi(k@!tVKV0mGWhS0`~f3f@?-T2ZuFXhXecxUUv#^#QTFj6sq&W-EPq@vS(L zPwT~}m#cQ%Vb^-e^}?ew&p_Ghg^5e|r!5*wlc%~!CoK zo7Pup#^z0ptY7N)EYCPRe<6Fx?$EO@^5iX;ejN-nVCZXn{D8%R)34F7K#Hf)_<@cE z`?==C0>&7oy)Q4{dyy&b*tb{W!1Nug>xz?kdUk}?UwRN|z^S+Us!f17pV|!VvuOvW zM8DO)JD06H;o94Pg}W@L-DfdBAQizb{XorGEW+O}j@3JlcX$1)YSxVG(+R8_ybf)- zFyZ!tS<&DA?{{jCWIe6Z^=D!5rn?g!-_Fa`mz3#LKOa4Hf_B#(Hn-A~-hH|aT8f(m z^)?u*7~E>x;(Beun!O9Iy)E%uosfRQZw`-TXJ=!T;#UDZ1DzBJFIV;nCU+Mc&$YN% zwL`ErPkehxr^&&O$*qe&)tB>~;RM3YY=&AUG}t6AU?Bp69>SIdCv*R7m75n;v^^;E z%G-w%F3q^T`ncCh{rl=ukKO&pqvgB9ye@E7$@#OIzB||751duDfB#~W$N#oCWL~Rv zS35T6_q(=Bd(t=EpCV>cygoehqOrZ7mTsldUn`%NUF!aIv((?)FR%FRv`xH8DS-V| z<37P&1@2i5`vi3th`#uIfzQf8{lfEwwzv(al diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 1671b3b180..b7183fb062 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -25884,45 +25884,35 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i .................................................... -1. Let :math:`{{\mathit{dt}}^\ast}` be :math:`{\mathit{moduleinst}}{.}\mathsf{types}`. - -#. Return :math:`{t}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. +1. Return :math:`{t}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]}`. :math:`{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{rt}})` ................................................................ -1. Let :math:`{{\mathit{dt}}^\ast}` be :math:`{\mathit{moduleinst}}{.}\mathsf{types}`. - -#. Return :math:`{{\mathit{rt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. +1. Return :math:`{{\mathit{rt}}}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]}`. :math:`{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{gt}})` ................................................................ -1. Let :math:`{{\mathit{dt}}^\ast}` be :math:`{\mathit{moduleinst}}{.}\mathsf{types}`. - -#. Return :math:`{{\mathit{gt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. +1. Return :math:`{{\mathit{gt}}}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]}`. :math:`{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{mt}})` ................................................................ -1. Let :math:`{{\mathit{dt}}^\ast}` be :math:`{\mathit{moduleinst}}{.}\mathsf{types}`. - -#. Return :math:`{{\mathit{mt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. +1. Return :math:`{{\mathit{mt}}}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]}`. :math:`{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{tt}})` ................................................................ -1. Let :math:`{{\mathit{dt}}^\ast}` be :math:`{\mathit{moduleinst}}{.}\mathsf{types}`. - -#. Return :math:`{{\mathit{tt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]}`. +1. Return :math:`{{\mathit{tt}}}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]}`. :math:`{{\mathrm{blocktype}}}_{z}({\mathit{blocktype}})` @@ -32762,24 +32752,19 @@ growmem meminst n 5. Fail. inst_valtype moduleinst t -1. Let dt* be moduleinst.TYPES. -2. Return $subst_all_valtype(t, dt*). +1. Return $subst_all_valtype(t, moduleinst.TYPES). inst_reftype moduleinst rt -1. Let dt* be moduleinst.TYPES. -2. Return $subst_all_reftype(rt, dt*). +1. Return $subst_all_reftype(rt, moduleinst.TYPES). inst_globaltype moduleinst gt -1. Let dt* be moduleinst.TYPES. -2. Return $subst_all_globaltype(gt, dt*). +1. Return $subst_all_globaltype(gt, moduleinst.TYPES). inst_memtype moduleinst mt -1. Let dt* be moduleinst.TYPES. -2. Return $subst_all_memtype(mt, dt*). +1. Return $subst_all_memtype(mt, moduleinst.TYPES). inst_tabletype moduleinst tt -1. Let dt* be moduleinst.TYPES. -2. Return $subst_all_tabletype(tt, dt*). +1. Return $subst_all_tabletype(tt, moduleinst.TYPES). blocktype_ z blocktype 1. If blocktype is some _IDX, then: From 47b039a0ef947dc3834163438a76815a1572c827 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 2 Apr 2026 11:04:33 +0200 Subject: [PATCH 2/3] CI --- .../wasm-latest/4.2-execution.types.spectec | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/specification/wasm-latest/4.2-execution.types.spectec b/specification/wasm-latest/4.2-execution.types.spectec index 5f9f9c881e..2b29f46613 100644 --- a/specification/wasm-latest/4.2-execution.types.spectec +++ b/specification/wasm-latest/4.2-execution.types.spectec @@ -8,14 +8,8 @@ def $inst_globaltype(moduleinst, globaltype) : globaltype hint(show $inst_(%,%) def $inst_memtype(moduleinst, memtype) : memtype hint(show $inst_(%,%)) hint(macro "insttype") def $inst_tabletype(moduleinst, tabletype) : tabletype hint(show $inst_(%,%)) hint(macro "insttype") -;; TODO(3, rossberg): make inlining moduleinst.TYPES work -def $inst_valtype(moduleinst, t) = $subst_all_valtype(t, dt*) - -- if dt* = moduleinst.TYPES -def $inst_reftype(moduleinst, rt) = $subst_all_reftype(rt, dt*) - -- if dt* = moduleinst.TYPES -def $inst_globaltype(moduleinst, gt) = $subst_all_globaltype(gt, dt*) - -- if dt* = moduleinst.TYPES -def $inst_memtype(moduleinst, mt) = $subst_all_memtype(mt, dt*) - -- if dt* = moduleinst.TYPES -def $inst_tabletype(moduleinst, tt) = $subst_all_tabletype(tt, dt*) - -- if dt* = moduleinst.TYPES +def $inst_valtype(moduleinst, t) = $subst_all_valtype(t, moduleinst.TYPES) +def $inst_reftype(moduleinst, rt) = $subst_all_reftype(rt, moduleinst.TYPES) +def $inst_globaltype(moduleinst, gt) = $subst_all_globaltype(gt, moduleinst.TYPES) +def $inst_memtype(moduleinst, mt) = $subst_all_memtype(mt, moduleinst.TYPES) +def $inst_tabletype(moduleinst, tt) = $subst_all_tabletype(tt, moduleinst.TYPES) From 70a4e37cb44b615a5d7301a6de2603fcced74f4d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 2 Apr 2026 14:48:48 +0200 Subject: [PATCH 3/3] CI --- spectec/doc/example/output/NanoWasm.pdf | Bin 245512 -> 245512 bytes spectec/test-frontend/TEST.md | 15 +++----- spectec/test-latex/TEST.md | 10 +++--- spectec/test-middlend/TEST.md | 45 ++++++++---------------- 4 files changed, 25 insertions(+), 45 deletions(-) diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index a06cbe5ef5e286b835bfe782ec841562ff1210a1..6f82a5bffae705bd121d75b9fdcb2a07e308bc70 100644 GIT binary patch delta 112 zcmeD9$Jg5^NS1Tz5jE*;kZ delta 112 zcmeD9$Jg5^NS1Tz5O=^aG? diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 5aae8c8475..c801a47769 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -5955,32 +5955,27 @@ relation Externaddr_ok: `%|-%:%`(store, externaddr, externtype) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_valtype{moduleinst : moduleinst, t : valtype, `dt*` : deftype*}(moduleinst, t) = $subst_all_valtype(t, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_valtype{moduleinst : moduleinst, t : valtype}(moduleinst, t) = $subst_all_valtype(t, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_reftype{moduleinst : moduleinst, rt : reftype}(moduleinst, rt) = $subst_all_reftype(rt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype}(moduleinst, gt) = $subst_all_globaltype(gt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_memtype{moduleinst : moduleinst, mt : memtype}(moduleinst, mt) = $subst_all_memtype(mt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype}(moduleinst, tt) = $subst_all_tabletype(tt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec relation Step_pure: `%~>%`(instr*, instr*) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 07faa4f442..d6d5e0903b 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -9608,31 +9608,31 @@ $$ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{{\mathrm{inst}}}_{{\mathit{moduleinst}}}(t) & = & {t}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]} & \quad \mbox{if}~ {{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\ +{{\mathrm{inst}}}_{{\mathit{moduleinst}}}(t) & = & {t}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]} \\ \end{array} $$ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{rt}}) & = & {{\mathit{rt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]} & \quad \mbox{if}~ {{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\ +{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{rt}}) & = & {{\mathit{rt}}}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]} \\ \end{array} $$ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{gt}}) & = & {{\mathit{gt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]} & \quad \mbox{if}~ {{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\ +{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{gt}}) & = & {{\mathit{gt}}}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]} \\ \end{array} $$ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{mt}}) & = & {{\mathit{mt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]} & \quad \mbox{if}~ {{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\ +{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{mt}}) & = & {{\mathit{mt}}}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]} \\ \end{array} $$ $$ \begin{array}[t]{@{}lcl@{}l@{}} -{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{tt}}) & = & {{\mathit{tt}}}{{}[ {:=}\, {{\mathit{dt}}^\ast} ]} & \quad \mbox{if}~ {{\mathit{dt}}^\ast} = {\mathit{moduleinst}}{.}\mathsf{types} \\ +{{\mathrm{inst}}}_{{\mathit{moduleinst}}}({\mathit{tt}}) & = & {{\mathit{tt}}}{{}[ {:=}\, {\mathit{moduleinst}}{.}\mathsf{types} ]} \\ \end{array} $$ diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 52de5c986f..bb0a518af2 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -5945,32 +5945,27 @@ relation Externaddr_ok: `%|-%:%`(store, externaddr, externtype) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_valtype{moduleinst : moduleinst, t : valtype, `dt*` : deftype*}(moduleinst, t) = $subst_all_valtype(t, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_valtype{moduleinst : moduleinst, t : valtype}(moduleinst, t) = $subst_all_valtype(t, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_reftype{moduleinst : moduleinst, rt : reftype}(moduleinst, rt) = $subst_all_reftype(rt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype}(moduleinst, gt) = $subst_all_globaltype(gt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_memtype{moduleinst : moduleinst, mt : memtype}(moduleinst, mt) = $subst_all_memtype(mt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype}(moduleinst, tt) = $subst_all_tabletype(tt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec relation Step_pure: `%~>%`(instr*, instr*) @@ -17371,32 +17366,27 @@ relation Externaddr_ok: `%|-%:%`(store, externaddr, externtype) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_valtype{moduleinst : moduleinst, t : valtype, `dt*` : deftype*}(moduleinst, t) = $subst_all_valtype(t, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_valtype{moduleinst : moduleinst, t : valtype}(moduleinst, t) = $subst_all_valtype(t, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_reftype{moduleinst : moduleinst, rt : reftype}(moduleinst, rt) = $subst_all_reftype(rt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype}(moduleinst, gt) = $subst_all_globaltype(gt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_memtype{moduleinst : moduleinst, mt : memtype}(moduleinst, mt) = $subst_all_memtype(mt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype}(moduleinst, tt) = $subst_all_tabletype(tt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec relation Step_pure: `%~>%`(instr*, instr*) @@ -28930,32 +28920,27 @@ relation Externaddr_ok: `%|-%:%`(store, externaddr, externtype) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_valtype(moduleinst : moduleinst, valtype : valtype) : valtype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_valtype{moduleinst : moduleinst, t : valtype, `dt*` : deftype*}(moduleinst, t) = $subst_all_valtype(t, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_valtype{moduleinst : moduleinst, t : valtype}(moduleinst, t) = $subst_all_valtype(t, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_reftype(moduleinst : moduleinst, reftype : reftype) : reftype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_reftype{moduleinst : moduleinst, rt : reftype, `dt*` : deftype*}(moduleinst, rt) = $subst_all_reftype(rt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_reftype{moduleinst : moduleinst, rt : reftype}(moduleinst, rt) = $subst_all_reftype(rt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_globaltype(moduleinst : moduleinst, globaltype : globaltype) : globaltype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_globaltype{moduleinst : moduleinst, gt : globaltype, `dt*` : deftype*}(moduleinst, gt) = $subst_all_globaltype(gt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_globaltype{moduleinst : moduleinst, gt : globaltype}(moduleinst, gt) = $subst_all_globaltype(gt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_memtype(moduleinst : moduleinst, memtype : memtype) : memtype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_memtype{moduleinst : moduleinst, mt : memtype, `dt*` : deftype*}(moduleinst, mt) = $subst_all_memtype(mt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_memtype{moduleinst : moduleinst, mt : memtype}(moduleinst, mt) = $subst_all_memtype(mt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec def $inst_tabletype(moduleinst : moduleinst, tabletype : tabletype) : tabletype ;; ../../../../specification/wasm-latest/4.2-execution.types.spectec - def $inst_tabletype{moduleinst : moduleinst, tt : tabletype, `dt*` : deftype*}(moduleinst, tt) = $subst_all_tabletype(tt, (dt : deftype <: typeuse)*{dt <- `dt*`}) - -- if (dt*{dt <- `dt*`} = moduleinst.TYPES_moduleinst) + def $inst_tabletype{moduleinst : moduleinst, tt : tabletype}(moduleinst, tt) = $subst_all_tabletype(tt, (moduleinst.TYPES_moduleinst : deftype* <: typeuse*)) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec relation Step_pure: `%~>%`(instr*, instr*)