From 0aa9dbaee32de702fd80ffb452ea9e889ea0e76c Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 6 Jul 2026 20:33:22 -0700 Subject: [PATCH 1/9] Syntax and validation for struct.new_desc And struct.new_default_desc. Also update the valiation for struct.new and struct.new_default to require empty descriptors. Add an explanation of expansion to desctype to the validation conventions section and teach SpecTec about the new ExpandDesc relation to avoid errors during rendering. --- document/core/syntax/instructions.rst | 5 ++++- document/core/util/macros.def | 4 ++++ document/core/valid/conventions.rst | 5 +++++ document/core/valid/instructions.rst | 20 +++++++++++++++++++ .../wasm-latest/1.2-syntax.types.spectec | 2 +- .../1.3-syntax.instructions.spectec | 2 ++ .../wasm-latest/2.1-validation.types.spectec | 5 +++++ .../2.3-validation.instructions.spectec | 13 ++++++++++-- spectec/src/backend-prose/gen.ml | 2 +- 9 files changed, 53 insertions(+), 5 deletions(-) diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 74bbcc634..7a93f1d59 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -265,6 +265,8 @@ while the latter performs a downcast and :ref:`traps ` if the operand's ty .. _syntax-struct.new: .. _syntax-struct.new_default: +.. _syntax-struct.new_desc: +.. _syntax-struct.new_default_desc: .. _syntax-struct.get: .. _syntax-struct.get_s: .. _syntax-struct.get_u: @@ -301,7 +303,8 @@ Instructions in this group are concerned with creating and accessing :ref:`refer $${syntax: {instr/struct instr/array instr/i31 instr/extern}} -The instructions ${:STRUCT.NEW} and ${:STRUCT.NEW_DEFAULT} allocate a new :ref:`structure `, initializing them either with operands or with default values. +The instructions ${:STRUCT.NEW}, ${:STRUCT.NEW_DEFAULT} allocate a new :ref:`structure `, initializing them either with operands or with default values. +The instructions ${:STRUCT.NEW_DESC} and ${:STRUCT.NEW_DEFAULT_DESC} do the same, but additionally take the :ref:`descriptor ` operand necessary to allocate types with descriptors. The remaining instructions on structs access individual fields, allowing for different sign extension modes in the case of :ref:`packed ` storage types. diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 1a81d68af..35413fb95 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -342,8 +342,10 @@ .. |rolldt| mathdef:: \xref{valid/conventions}{aux-roll-deftype}{\F{roll}} .. |unrolldt| mathdef:: \xref{valid/conventions}{aux-unroll-deftype}{\F{unroll}} .. |expanddt| mathdef:: \xref{valid/conventions}{aux-expand-deftype}{\F{expand}} +.. |expanddttodesctype| mathdef:: \xref{valid/conventions}{aux-expand-deftype-to-desctype}{\F{expand}} .. |approxexpanddt| mathdef:: \mathrel{\xref{valid/conventions}{aux-expand-deftype}{\approx}} .. |approxexpandyy| mathdef:: \mathrel{\xref{valid/conventions}{aux-expand-typeuse}{\approx}} +.. |approxexpanddttodesctype| mathdef:: \mathrel{\xref{valid/conventions}{aux-expand-deftype-to-desctype}{\approx}} .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}} .. |unpack| mathdef:: \xref{syntax/types}{aux-unpack}{\F{unpack}} @@ -551,6 +553,8 @@ .. |STRUCTNEW| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new}} .. |STRUCTNEWDEFAULT| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_default}} +.. |STRUCTNEWDESC| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_desc}} +.. |STRUCTNEWDEFAULTDESC| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}new\_default\_desc}} .. |STRUCTGET| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get}} .. |STRUCTGETS| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get\_s}} .. |STRUCTGETU| mathdef:: \xref{syntax/instructions}{syntax-instr-struct}{\K{struct{.}get\_u}} diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 7164062ed..8ec31b468 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -138,6 +138,7 @@ Conventions .. _aux-roll-deftype: .. _aux-unroll-deftype: .. _aux-expand-deftype: +.. _aux-expand-deftype-to-desctype: .. _aux-expand-typeuse: Rolling and Unrolling @@ -169,6 +170,10 @@ $${rule: Expand {Expand_use/*}} $${relation-ignore: Expand Expand_use} $${definition-ignore: expanddt} +We use the same notation to denote the expansion of a :ref:`defined type ` or :ref:`type use ` to a :ref:`desctype ` as well. + +$${rule: ExpandDesc} + .. index:: ! instruction type, value type, result type, instruction, local, local index pair: abstract syntax; instruction type diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 6013d4de2..8ddb6465a 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -854,6 +854,26 @@ $${rule-prose: Instr_ok/struct.new_default} $${rule: Instr_ok/struct.new_default} +.. _valid-struct.new_desc: + +:math:`\STRUCTNEWDESC~x` +........................ + +$${rule-prose: Instr_ok/struct.new_desc} + +$${rule: Instr_ok/struct.new_desc} + + +.. _valid-struct.new_default_desc: + +:math:`\STRUCTNEWDEFAULTDESC~x` +............................... + +$${rule-prose: Instr_ok/struct.new_default_desc} + +$${rule: Instr_ok/struct.new_default_desc} + + .. _valid-struct.get: .. _valid-struct.get_u: .. _valid-struct.get_s: diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index a4b2249e7..25990998e 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/specification/wasm-latest/1.2-syntax.types.spectec @@ -474,7 +474,7 @@ def $rollrt(typeidx, rectype) : rectype hint(show $roll_(%, %)) hint(macro "r def $unrollrt(rectype) : rectype hint(show $unroll(%)) hint(macro "unrollrt") def $rolldt(typeidx, rectype) : deftype* hint(show $roll_(%)*#((%))) hint(macro "rolldt") def $unrolldt(deftype) : subtype hint(show $unroll(%)) hint(macro "unrolldt") -def $expanddt_to_desctype(deftype) : desctype hint(show $expand_desc(%)) +def $expanddt_to_desctype(deftype) : desctype hint(show $expand_desc(%)) hint(macro "expanddttodesctype") def $expanddt(deftype) : comptype hint(show $expand(%)) hint(macro "expanddt") def $rollrt(x, rectype) = REC ($subst_subtype(subtype, ((_IDX $(x + i)))^(i` of %1 is %2") ;; TODO(3, ?): avoid hardcoding reST + +rule ExpandDesc: deftype ~~ desctype -- if $expanddt_to_desctype(deftype) = desctype + ;; Type definitions diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index aa012b18f..99829b6ae 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -251,11 +251,20 @@ rule Instr_ok/i31.get: rule Instr_ok/struct.new: C |- STRUCT.NEW x : $unpack(zt)* -> (REF (_IDX x)) - -- Expand: C.TYPES[x] ~~ STRUCT (mut? zt)* + -- ExpandDesc: C.TYPES[x] ~~ describestype? eps STRUCT (mut? zt)* rule Instr_ok/struct.new_default: C |- STRUCT.NEW_DEFAULT x : eps -> (REF (_IDX x)) - -- Expand: C.TYPES[x] ~~ STRUCT (mut? zt)* + -- ExpandDesc: C.TYPES[x] ~~ describestype? eps STRUCT (mut? zt)* + -- (Defaultable: |- $unpack(zt) DEFAULTABLE)* + +rule Instr_ok/struct.new_desc: + C |- STRUCT.NEW_DESC x : $unpack(zt)* (REF NULL (EXACT (_IDX y))) -> (REF (EXACT (_IDX x))) + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) (STRUCT (mut? zt)*) + +rule Instr_ok/struct.new_default_desc: + C |- STRUCT.NEW_DEFAULT_DESC x : (REF NULL (EXACT (_IDX y))) -> (REF (EXACT (_IDX x))) + -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) (STRUCT (mut? zt)*) -- (Defaultable: |- $unpack(zt) DEFAULTABLE)* def $is_packtype(storagetype) : bool hint(show %1 = $unpack(%1)) hint(prose "%1 is a packed type") diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml index 4c88ce6b0..9b966ce22 100644 --- a/spectec/src/backend-prose/gen.ml +++ b/spectec/src/backend-prose/gen.ml @@ -32,7 +32,7 @@ let flatten_rec def = let is_validation_helper_relation def = match def.it with - | Ast.RelD (id, _, _, _) -> id.it = "Expand" || id.it = "Expand_use" + | Ast.RelD (id, _, _, _) -> id.it = "Expand" || id.it = "Expand_use" || id.it = "ExpandDesc" | _ -> false (* NOTE: Assume validation relation is `|-` *) let is_validation_relation def = From 47b07b73918d2c2e023c89c94824b895ed432cc5 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 7 Jul 2026 10:10:57 -0700 Subject: [PATCH 2/9] const expr --- document/core/valid/instructions.rst | 1 + .../wasm-latest/2.3-validation.instructions.spectec | 6 ++++++ 2 files changed, 7 insertions(+) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 8ddb6465a..c49fc727a 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -1441,6 +1441,7 @@ $${rule: {Instr_const/const Instr_const/vconst Instr_const/binop} {Instr_const/ref.null Instr_const/ref.i31 Instr_const/ref.func} {Instr_const/struct.new Instr_const/struct.new_default} + {Instr_const/struct.new_desc Instr_const/struct.new_default_desc} {Instr_const/array.new Instr_const/array.new_default Instr_const/array.new_fixed} {Instr_const/any.convert_extern Instr_const/extern.convert_any} {Instr_const/global.get} diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index 99829b6ae..2e042e76f 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -682,6 +682,12 @@ rule Instr_const/struct.new: rule Instr_const/struct.new_default: C |- (STRUCT.NEW_DEFAULT x) CONST +rule Instr_const/struct.new_desc: + C |- (STRUCT.NEW_DESC x) CONST + +rule Instr_const/struct.new_default_desc: + C |- (STRUCT.NEW_DEFAULT_DESC x) CONST + rule Instr_const/array.new: C |- (ARRAY.NEW x) CONST From 3b16166dd7ef318d1d07fec65593815c1f894e07 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 13 Jul 2026 03:27:10 -0700 Subject: [PATCH 3/9] Make exact and non-exact heap types the same case Previously the definition of `heaptype` was `... | EXACT typeuse | typeuse`, but this made it impossible to treat the exactness as a variable. Refactor the definition to `... | _HT exact? typeuse` instead. This is similar to how nullability is treated in reference types, except that the `_HT` tag will not be displayed in the rendered spec. --- document/core/syntax/types.rst | 1 + document/core/util/macros.def | 1 + document/core/valid/types.rst | 4 +-- .../wasm-latest/1.2-syntax.types.spectec | 10 +++--- .../wasm-latest/2.1-validation.types.spectec | 14 +++----- .../2.2-validation.subtyping.spectec | 28 +++++++-------- .../2.3-validation.instructions.spectec | 36 +++++++++---------- .../wasm-latest/4.1-execution.values.spectec | 6 ++-- .../4.3-execution.instructions.spectec | 6 ++-- .../wasm-latest/5.2-binary.types.spectec | 2 +- .../wasm-latest/6.2-text.types.spectec | 2 +- 11 files changed, 55 insertions(+), 55 deletions(-) diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 43b06d776..fec815899 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -92,6 +92,7 @@ The syntax of type uses is :ref:`extended ` with additional .. _syntax-i31: .. _syntax-heaptype: .. _syntax-absheaptype: +.. _syntax-exact: Heap Types ~~~~~~~~~~ diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 1a81d68af..35f85ec4b 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -321,6 +321,7 @@ .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}} .. |null| mathdef:: \xref{syntax/types}{syntax-null}{\X{null}} +.. |exact| mathdef:: \xref{syntax/types}{syntax-exact}{\X{exact}} .. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}} .. |final| mathdef:: \xref{syntax/types}{syntax-final}{\X{final}} .. |init| mathdef:: \xref{valid/conventions}{syntax-init}{\X{init}} diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 3c36dba8e..a20422a57 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -58,9 +58,9 @@ $${rule-prose: Heaptype_ok/abs} $${rule: Heaptype_ok/abs} -$${rule-prose: Heaptype_ok/exact} +$${rule-prose: Heaptype_ok/typeuse} -$${rule: Heaptype_ok/exact} +$${rule: Heaptype_ok/typeuse} .. index:: reference type, heap type diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index a4b2249e7..c0e9f8a9d 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/specification/wasm-latest/1.2-syntax.types.spectec @@ -7,6 +7,8 @@ ;; TODO(3, rossberg): add ability to do this inline syntax null hint(show NULL) hint(macro "%" "%") = NULL +syntax exact hint(desc "exactness") = EXACT + syntax addrtype hint(desc "address type") = | I32 | I64 @@ -41,7 +43,7 @@ syntax typevar hint(desc "type variable") = | _IDX typeidx | REC n hint(show REC.%) syntax heaptype hint(desc "heap type") = - | absheaptype | typeuse | EXACT typeuse + | absheaptype | _HT exact? typeuse syntax reftype hint(desc "reference type") = | REF null? heaptype @@ -382,8 +384,8 @@ def $subst_addrtype(at, tv*, tu*) = at def $subst_numtype(nt, tv*, tu*) = nt def $subst_vectype(vt, tv*, tu*) = vt -def $subst_heaptype(tv', tv*, tu*) = $subst_typevar(tv', tv*, tu*) -def $subst_heaptype(dt, tv*, tu*) = $subst_deftype(dt, tv*, tu*) +def $subst_heaptype(_HT exact? tv', tv*, tu*) = _HT exact? $subst_typevar(tv', tv*, tu*) +def $subst_heaptype(_HT exact? dt, tv*, tu*) = _HT exact? $subst_deftype(dt, tv*, tu*) def $subst_heaptype(ht, tv*, tu*) = ht -- otherwise def $subst_reftype((REF null? ht), tv*, tu*) = REF null? $subst_heaptype(ht, tv*, tu*) @@ -550,7 +552,7 @@ def $free_typeuse(typevar) = $free_typevar(typevar) def $free_typeuse(deftype) = $free_deftype(deftype) def $free_heaptype(absheaptype) = $free_absheaptype(absheaptype) -def $free_heaptype(typeuse) = $free_typeuse(typeuse) +def $free_heaptype(_HT exact? typeuse) = $free_typeuse(typeuse) def $free_reftype(REF null? heaptype) = $free_heaptype(heaptype) diff --git a/specification/wasm-latest/2.1-validation.types.spectec b/specification/wasm-latest/2.1-validation.types.spectec index cb788a75f..60ae2a819 100644 --- a/specification/wasm-latest/2.1-validation.types.spectec +++ b/specification/wasm-latest/2.1-validation.types.spectec @@ -21,11 +21,7 @@ rule Heaptype_ok/abs: C |- absheaptype : OK rule Heaptype_ok/typeuse: - C |- typeuse : OK - -- Typeuse_ok: C |- typeuse : OK - -rule Heaptype_ok/exact: - C |- EXACT typeuse : OK + C |- _HT exact? typeuse : OK -- Typeuse_ok: C |- typeuse : OK rule Reftype_ok: @@ -167,15 +163,15 @@ def $before(_IDX typeidx, x, i) = typeidx < x def $before(REC j, x, i) = j < i def $unrollht(context, heaptype) : subtype hint(show $unroll_(%,%)) -def $unrollht(C, deftype) = $unrolldt(deftype) -def $unrollht(C, _IDX typeidx) = $unrolldt(C.TYPES[typeidx]) -def $unrollht(C, REC i) = C.RECS[i] +def $unrollht(C, _HT exact? deftype) = $unrolldt(deftype) +def $unrollht(C, _HT exact? _IDX typeidx) = $unrolldt(C.TYPES[typeidx]) +def $unrollht(C, _HT exact? REC i) = C.RECS[i] rule Subtype_ok2: C |- SUB FINAL? typeuse* desctype : OK x i -- if |typeuse*| <= 1 -- (if $before(typeuse, x, i))* - -- (if $unrollht(C, typeuse) = SUB typeuse'* desctype')* + -- (if $unrollht(C, _HT typeuse) = SUB typeuse'* desctype')* ---- -- Desctype_ok: C |- desctype : OK -- (Desctype_sub: C |- desctype <: desctype')* diff --git a/specification/wasm-latest/2.2-validation.subtyping.spectec b/specification/wasm-latest/2.2-validation.subtyping.spectec index 9bd60602f..53277147b 100644 --- a/specification/wasm-latest/2.2-validation.subtyping.spectec +++ b/specification/wasm-latest/2.2-validation.subtyping.spectec @@ -21,8 +21,8 @@ rule Heaptype_sub/refl: C |- heaptype <: heaptype rule Heaptype_sub/exact-l: - C |- EXACT typeuse <: heaptype - -- Heaptype_sub: C |- typeuse <: heaptype + C |- _HT exact typeuse <: heaptype + -- Heaptype_sub: C |- _HT typeuse <: heaptype rule Heaptype_sub/trans: C |- heaptype_1 <: heaptype_2 @@ -43,31 +43,31 @@ rule Heaptype_sub/array-eq: C |- ARRAY <: EQ rule Heaptype_sub/struct: - C |- deftype <: STRUCT + C |- _HT deftype <: STRUCT -- Expand: deftype ~~ STRUCT fieldtype* rule Heaptype_sub/array: - C |- deftype <: ARRAY + C |- _HT deftype <: ARRAY -- Expand: deftype ~~ ARRAY fieldtype rule Heaptype_sub/func: - C |- deftype <: FUNC + C |- _HT deftype <: FUNC -- Expand: deftype ~~ FUNC t_1* -> t_2* rule Heaptype_sub/def: - C |- deftype_1 <: deftype_2 + C |- _HT deftype_1 <: _HT deftype_2 -- Deftype_sub: C |- deftype_1 <: deftype_2 rule Heaptype_sub/typeidx-l: - C |- _IDX typeidx <: heaptype - -- Heaptype_sub: C |- C.TYPES[typeidx] <: heaptype + C |- _HT _IDX typeidx <: heaptype + -- Heaptype_sub: C |- _HT C.TYPES[typeidx] <: heaptype rule Heaptype_sub/typeidx-r: - C |- heaptype <: _IDX typeidx - -- Heaptype_sub: C |- heaptype <: C.TYPES[typeidx] + C |- heaptype <: _HT _IDX typeidx + -- Heaptype_sub: C |- heaptype <: _HT C.TYPES[typeidx] rule Heaptype_sub/rec: - C |- REC i <: typeuse*[j] + C |- _HT REC i <: _HT typeuse*[j] -- if C.RECS[i] = SUB final? typeuse* desctype rule Heaptype_sub/none: @@ -183,8 +183,8 @@ rule Comptype_sub/func: ;; TODO: Check descriptor square rules rule Desctype_sub: C |- (DESCRIBES tu_11) (DESCRIPTOR tu_12) ct_1 <: (DESCRIBES tu_21) (DESCRIPTOR tu_22) ct_2 - -- Heaptype_sub: C |- tu_11 <: tu_21 - -- Heaptype_sub: C |- tu_12 <: tu_22 + -- Heaptype_sub: C |- _HT tu_11 <: _HT tu_21 + -- Heaptype_sub: C |- _HT tu_12 <: _HT tu_22 -- Comptype_sub: C |- ct_1 <: ct_2 @@ -195,7 +195,7 @@ rule Deftype_sub/refl: rule Deftype_sub/super: C |- deftype_1 <: deftype_2 -- if $unrolldt(deftype_1) = SUB final? typeuse* desctype - -- Heaptype_sub: C |- typeuse*[i] <: deftype_2 + -- Heaptype_sub: C |- _HT typeuse*[i] <: _HT deftype_2 ;; External types diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index aa012b18f..6a2337166 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -123,7 +123,7 @@ rule Instr_ok/call: -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2* rule Instr_ok/call_ref: - C |- CALL_REF (_IDX x) : t_1* (REF NULL (_IDX x)) -> t_2* + C |- CALL_REF (_IDX x) : t_1* (REF NULL (_HT _IDX x)) -> t_2* -- Expand: C.TYPES[x] ~~ FUNC t_1* -> t_2* rule Instr_ok/call_indirect: @@ -147,7 +147,7 @@ rule Instr_ok/return_call: ;; TODO(3, rossberg): enable t_2* <: C.RETURN rule Instr_ok/return_call_ref: - C |- RETURN_CALL_REF (_IDX x) : t_3* t_1* (REF NULL (_IDX x)) -> t_4* + C |- RETURN_CALL_REF (_IDX x) : t_3* t_1* (REF NULL (_HT _IDX x)) -> t_4* -- Expand: C.TYPES[x] ~~ FUNC t_1* -> t_2* -- if C.RETURN = (t'_2*) -- Resulttype_sub: C |- t_2* <: t'_2* @@ -210,7 +210,7 @@ rule Instr_ok/ref.null: -- Heaptype_ok: C |- ht : OK rule Instr_ok/ref.func: - C |- REF.FUNC x : eps -> (REF dt) + C |- REF.FUNC x : eps -> (REF (_HT dt)) -- if C.FUNCS[x] = dt -- if x <- C.REFS @@ -250,11 +250,11 @@ rule Instr_ok/i31.get: ;; Structure instructions rule Instr_ok/struct.new: - C |- STRUCT.NEW x : $unpack(zt)* -> (REF (_IDX x)) + C |- STRUCT.NEW x : $unpack(zt)* -> (REF (_HT _IDX x)) -- Expand: C.TYPES[x] ~~ STRUCT (mut? zt)* rule Instr_ok/struct.new_default: - C |- STRUCT.NEW_DEFAULT x : eps -> (REF (_IDX x)) + C |- STRUCT.NEW_DEFAULT x : eps -> (REF (_HT _IDX x)) -- Expand: C.TYPES[x] ~~ STRUCT (mut? zt)* -- (Defaultable: |- $unpack(zt) DEFAULTABLE)* @@ -262,13 +262,13 @@ def $is_packtype(storagetype) : bool hint(show %1 = $unpack(%1)) hin def $is_packtype(zt) = zt =/= $unpack(zt) rule Instr_ok/struct.get: - C |- STRUCT.GET sx? x i : (REF NULL (_IDX x)) -> $unpack(zt) + C |- STRUCT.GET sx? x i : (REF NULL (_HT _IDX x)) -> $unpack(zt) -- Expand: C.TYPES[x] ~~ STRUCT ft* -- if ft*[i] = mut? zt -- if sx? =/= eps <=> $is_packtype(zt) rule Instr_ok/struct.set: - C |- STRUCT.SET x i : (REF NULL (_IDX x)) $unpack(zt) -> eps + C |- STRUCT.SET x i : (REF NULL (_HT _IDX x)) $unpack(zt) -> eps -- Expand: C.TYPES[x] ~~ STRUCT ft* -- if ft*[i] = MUT zt @@ -276,58 +276,58 @@ rule Instr_ok/struct.set: ;; Array instructions rule Instr_ok/array.new: - C |- ARRAY.NEW x : $unpack(zt) I32 -> (REF (_IDX x)) + C |- ARRAY.NEW x : $unpack(zt) I32 -> (REF (_HT _IDX x)) -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt) rule Instr_ok/array.new_default: - C |- ARRAY.NEW_DEFAULT x : I32 -> (REF (_IDX x)) + C |- ARRAY.NEW_DEFAULT x : I32 -> (REF (_HT _IDX x)) -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt) -- Defaultable: |- $unpack(zt) DEFAULTABLE rule Instr_ok/array.new_fixed: - C |- ARRAY.NEW_FIXED x n : $unpack(zt)^n -> (REF (_IDX x)) + C |- ARRAY.NEW_FIXED x n : $unpack(zt)^n -> (REF (_HT _IDX x)) -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt) rule Instr_ok/array.new_elem: - C |- ARRAY.NEW_ELEM x y : I32 I32 -> (REF (_IDX x)) + C |- ARRAY.NEW_ELEM x y : I32 I32 -> (REF (_HT _IDX x)) -- Expand: C.TYPES[x] ~~ ARRAY (mut? rt) -- Reftype_sub: C |- C.ELEMS[y] <: rt rule Instr_ok/array.new_data: - C |- ARRAY.NEW_DATA x y : I32 I32 -> (REF (_IDX x)) + C |- ARRAY.NEW_DATA x y : I32 I32 -> (REF (_HT _IDX x)) -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt) -- if $unpack(zt) = numtype \/ $unpack(zt) = vectype -- if C.DATAS[y] = OK rule Instr_ok/array.get: - C |- ARRAY.GET sx? x : (REF NULL (_IDX x)) I32 -> $unpack(zt) + C |- ARRAY.GET sx? x : (REF NULL (_HT _IDX x)) I32 -> $unpack(zt) -- Expand: C.TYPES[x] ~~ ARRAY (mut? zt) -- if sx? = eps <=> $is_packtype(zt) rule Instr_ok/array.set: - C |- ARRAY.SET x : (REF NULL (_IDX x)) I32 $unpack(zt) -> eps + C |- ARRAY.SET x : (REF NULL (_HT _IDX x)) I32 $unpack(zt) -> eps -- Expand: C.TYPES[x] ~~ ARRAY (MUT zt) rule Instr_ok/array.len: C |- ARRAY.LEN : (REF NULL ARRAY) -> I32 rule Instr_ok/array.fill: - C |- ARRAY.FILL x : (REF NULL (_IDX x)) I32 $unpack(zt) I32 -> eps + C |- ARRAY.FILL x : (REF NULL (_HT _IDX x)) I32 $unpack(zt) I32 -> eps -- Expand: C.TYPES[x] ~~ ARRAY (MUT zt) rule Instr_ok/array.copy: - C |- ARRAY.COPY x_1 x_2 : (REF NULL (_IDX x_1)) I32 (REF NULL (_IDX x_2)) I32 I32 -> eps + C |- ARRAY.COPY x_1 x_2 : (REF NULL (_HT _IDX x_1)) I32 (REF NULL (_HT _IDX x_2)) I32 I32 -> eps -- Expand: C.TYPES[x_1] ~~ ARRAY (MUT zt_1) -- Expand: C.TYPES[x_2] ~~ ARRAY (mut? zt_2) -- Storagetype_sub: C |- zt_2 <: zt_1 rule Instr_ok/array.init_elem: - C |- ARRAY.INIT_ELEM x y : (REF NULL (_IDX x)) I32 I32 I32 -> eps + C |- ARRAY.INIT_ELEM x y : (REF NULL (_HT _IDX x)) I32 I32 I32 -> eps -- Expand: C.TYPES[x] ~~ ARRAY (MUT zt) -- Storagetype_sub: C |- C.ELEMS[y] <: zt rule Instr_ok/array.init_data: - C |- ARRAY.INIT_DATA x y : (REF NULL (_IDX x)) I32 I32 I32 -> eps + C |- ARRAY.INIT_DATA x y : (REF NULL (_HT _IDX x)) I32 I32 I32 -> eps -- Expand: C.TYPES[x] ~~ ARRAY (MUT zt) -- if $unpack(zt) = numtype \/ $unpack(zt) = vectype -- if C.DATAS[y] = OK diff --git a/specification/wasm-latest/4.1-execution.values.spectec b/specification/wasm-latest/4.1-execution.values.spectec index 1b38a0623..31df2deeb 100644 --- a/specification/wasm-latest/4.1-execution.values.spectec +++ b/specification/wasm-latest/4.1-execution.values.spectec @@ -40,15 +40,15 @@ rule Ref_ok/i31: s |- REF.I31_NUM i : (REF I31) rule Ref_ok/struct: - s |- REF.STRUCT_ADDR a : (REF dt) + s |- REF.STRUCT_ADDR a : (REF (_HT dt)) -- if s.STRUCTS[a].TYPE = dt rule Ref_ok/array: - s |- REF.ARRAY_ADDR a : (REF dt) + s |- REF.ARRAY_ADDR a : (REF (_HT dt)) -- if s.ARRAYS[a].TYPE = dt rule Ref_ok/func: - s |- REF.FUNC_ADDR a : (REF dt) + s |- REF.FUNC_ADDR a : (REF (_HT dt)) -- if s.FUNCS[a].TYPE = dt rule Ref_ok/exn: diff --git a/specification/wasm-latest/4.3-execution.instructions.spectec b/specification/wasm-latest/4.3-execution.instructions.spectec index bde165a66..3aefa08e7 100644 --- a/specification/wasm-latest/4.3-execution.instructions.spectec +++ b/specification/wasm-latest/4.3-execution.instructions.spectec @@ -203,10 +203,10 @@ rule Step_read/return_call_ref-frame-addr: rule Step_pure/call_indirect: - (CALL_INDIRECT x yy) ~> (TABLE.GET x) (REF.CAST (REF NULL yy)) (CALL_REF yy) + (CALL_INDIRECT x yy) ~> (TABLE.GET x) (REF.CAST (REF NULL (_HT yy))) (CALL_REF yy) rule Step_pure/return_call_indirect: - (RETURN_CALL_INDIRECT x yy) ~> (TABLE.GET x) (REF.CAST (REF NULL yy)) (RETURN_CALL_REF yy) + (RETURN_CALL_INDIRECT x yy) ~> (TABLE.GET x) (REF.CAST (REF NULL (_HT yy))) (RETURN_CALL_REF yy) rule Step_pure/frame-vals: @@ -616,7 +616,7 @@ rule Step/data.drop: ;; Reference instructions rule Step_read/ref.null-idx: - z; (REF.NULL (_IDX x)) ~> (REF.NULL $type(z, x)) + z; (REF.NULL (_HT _IDX x)) ~> (REF.NULL (_HT $type(z, x))) rule Step_read/ref.func: z; (REF.FUNC x) ~> (REF.FUNC_ADDR $moduleinst(z).FUNCS[x]) diff --git a/specification/wasm-latest/5.2-binary.types.spectec b/specification/wasm-latest/5.2-binary.types.spectec index 743ff8785..d6c1d7093 100644 --- a/specification/wasm-latest/5.2-binary.types.spectec +++ b/specification/wasm-latest/5.2-binary.types.spectec @@ -29,7 +29,7 @@ grammar Babsheaptype : heaptype = grammar Bheaptype : heaptype = | ht:Babsheaptype => ht - | x33:Bs33 => _IDX $s33_to_u32(x33) -- if x33 >= 0 + | x33:Bs33 => _HT (_IDX $s33_to_u32(x33)) -- if x33 >= 0 grammar Breftype : reftype = | 0x63 ht:Bheaptype => REF NULL ht diff --git a/specification/wasm-latest/6.2-text.types.spectec b/specification/wasm-latest/6.2-text.types.spectec index 2afedafc9..fd437be11 100644 --- a/specification/wasm-latest/6.2-text.types.spectec +++ b/specification/wasm-latest/6.2-text.types.spectec @@ -30,7 +30,7 @@ grammar Tabsheaptype : heaptype = grammar Theaptype_(I) : heaptype = | ht:Tabsheaptype => ht - | x:Ttypeidx_(I) => _IDX x + | x:Ttypeidx_(I) => _HT (_IDX x) grammar Tnull : null = | "null" => NULL From e7acc8d388eb2609f4d8668ab3e4e97c1f68fab2 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Mon, 13 Jul 2026 05:24:52 -0700 Subject: [PATCH 4/9] show EXACT --- specification/wasm-latest/1.2-syntax.types.spectec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index c0e9f8a9d..6bf936730 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/specification/wasm-latest/1.2-syntax.types.spectec @@ -7,7 +7,7 @@ ;; TODO(3, rossberg): add ability to do this inline syntax null hint(show NULL) hint(macro "%" "%") = NULL -syntax exact hint(desc "exactness") = EXACT +syntax exact hint(show EXACT) = EXACT syntax addrtype hint(desc "address type") = | I32 | I64 From 34f1e6525787f49e1298b211a39d8d63c3f8293d Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 14 Jul 2026 03:07:38 -0700 Subject: [PATCH 5/9] update tests --- spectec/test-frontend/TEST.md | 424 +++++++++++++++++----------------- 1 file changed, 210 insertions(+), 214 deletions(-) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 9fbf91e57..3f47dc1b8 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -555,6 +555,10 @@ def $free_externidx(externidx : externidx) : free syntax null = | NULL +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec +syntax exact = + | EXACT + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec syntax addrtype = | I32 @@ -606,13 +610,13 @@ syntax final = ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:37.1-38.43 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:39.1-40.43 syntax typeuse = | _IDX{typeidx : typeidx}(typeidx : typeidx) | _DEF{rectype : rectype, n : n}(rectype : rectype, n : n) | REC{n : n}(n : n) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:43.1-44.42 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:45.1-46.37 syntax heaptype = | ANY | EQ @@ -627,12 +631,9 @@ syntax heaptype = | EXTERN | NOEXTERN | BOT - | _IDX{typeidx : typeidx}(typeidx : typeidx) - | REC{n : n}(n : n) - | _DEF{rectype : rectype, n : n}(rectype : rectype, n : n) - | EXACT{typeuse : typeuse}(typeuse : typeuse) + | _HT{`exact?` : exact?, typeuse : typeuse}(exact?{exact <- `exact?`} : exact?, typeuse : typeuse) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:51.1-52.14 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:53.1-54.14 syntax valtype = | I32 | I64 @@ -642,7 +643,7 @@ syntax valtype = | REF{`null?` : null?, heaptype : heaptype}(null?{null <- `null?`} : null?, heaptype : heaptype) | BOT -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:92.1-92.66 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:94.1-94.66 syntax storagetype = | BOT | I32 @@ -654,36 +655,36 @@ syntax storagetype = | I8 | I16 -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:102.1-103.16 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:104.1-105.16 syntax resulttype = list(syntax valtype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:112.1-112.61 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:114.1-114.61 syntax fieldtype = | `%%`{`mut?` : mut?, storagetype : storagetype}(mut?{mut <- `mut?`} : mut?, storagetype : storagetype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:114.1-117.34 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:116.1-119.34 syntax comptype = | STRUCT{list : list(syntax fieldtype)}(list : list(syntax fieldtype)) | ARRAY{fieldtype : fieldtype}(fieldtype : fieldtype) | `FUNC%->%`{resulttype : resulttype}(resulttype : resulttype, resulttype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:119.1-119.90 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:121.1-121.90 syntax describestype = | DESCRIBES{typeuse : typeuse}(typeuse : typeuse) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:120.1-120.93 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:122.1-122.93 syntax descriptortype = | DESCRIPTOR{typeuse : typeuse}(typeuse : typeuse) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:122.1-123.44 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:124.1-125.44 syntax desctype = | `%%%`{`describestype?` : describestype?, `descriptortype?` : descriptortype?, comptype : comptype}(describestype?{describestype <- `describestype?`} : describestype?, descriptortype?{descriptortype <- `descriptortype?`} : descriptortype?, comptype : comptype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:125.1-126.33 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:127.1-128.33 syntax subtype = | SUB{`final?` : final?, `typeuse*` : typeuse*, desctype : desctype}(final?{final <- `final?`} : final?, typeuse*{typeuse <- `typeuse*`} : typeuse*, desctype : desctype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:128.1-129.22 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:130.1-131.22 syntax rectype = | REC{list : list(syntax subtype)}(list : list(syntax subtype)) } @@ -1065,13 +1066,13 @@ def $as_deftype(typeuse : typeuse) : deftype ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:314.1-314.87 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:316.1-316.87 def $tagsxt(externtype*) : tagtype* - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:320.1-320.23 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:322.1-322.23 def $tagsxt([]) = [] - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:321.1-321.44 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:323.1-323.44 def $tagsxt{jt : tagtype, `xt*` : externtype*}([TAG_externtype(jt)] ++ xt*{xt <- `xt*`}) = [jt] ++ $tagsxt(xt*{xt <- `xt*`}) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:322.1-322.57 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:324.1-324.57 def $tagsxt{externtype : externtype, `xt*` : externtype*}([externtype] ++ xt*{xt <- `xt*`}) = $tagsxt(xt*{xt <- `xt*`}) -- otherwise } @@ -1079,13 +1080,13 @@ def $tagsxt(externtype*) : tagtype* ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:315.1-315.90 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:317.1-317.90 def $globalsxt(externtype*) : globaltype* - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:324.1-324.26 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:326.1-326.26 def $globalsxt([]) = [] - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:325.1-325.53 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:327.1-327.53 def $globalsxt{gt : globaltype, `xt*` : externtype*}([GLOBAL_externtype(gt)] ++ xt*{xt <- `xt*`}) = [gt] ++ $globalsxt(xt*{xt <- `xt*`}) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:326.1-326.63 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:328.1-328.63 def $globalsxt{externtype : externtype, `xt*` : externtype*}([externtype] ++ xt*{xt <- `xt*`}) = $globalsxt(xt*{xt <- `xt*`}) -- otherwise } @@ -1093,13 +1094,13 @@ def $globalsxt(externtype*) : globaltype* ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:316.1-316.87 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:318.1-318.87 def $memsxt(externtype*) : memtype* - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:328.1-328.23 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:330.1-330.23 def $memsxt([]) = [] - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:329.1-329.44 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:331.1-331.44 def $memsxt{mt : memtype, `xt*` : externtype*}([MEM_externtype(mt)] ++ xt*{xt <- `xt*`}) = [mt] ++ $memsxt(xt*{xt <- `xt*`}) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:330.1-330.57 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:332.1-332.57 def $memsxt{externtype : externtype, `xt*` : externtype*}([externtype] ++ xt*{xt <- `xt*`}) = $memsxt(xt*{xt <- `xt*`}) -- otherwise } @@ -1107,13 +1108,13 @@ def $memsxt(externtype*) : memtype* ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:317.1-317.89 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:319.1-319.89 def $tablesxt(externtype*) : tabletype* - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:332.1-332.25 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:334.1-334.25 def $tablesxt([]) = [] - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:333.1-333.50 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:335.1-335.50 def $tablesxt{tt : tabletype, `xt*` : externtype*}([TABLE_externtype(tt)] ++ xt*{xt <- `xt*`}) = [tt] ++ $tablesxt(xt*{xt <- `xt*`}) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:334.1-334.61 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:336.1-336.61 def $tablesxt{externtype : externtype, `xt*` : externtype*}([externtype] ++ xt*{xt <- `xt*`}) = $tablesxt(xt*{xt <- `xt*`}) -- otherwise } @@ -1121,13 +1122,13 @@ def $tablesxt(externtype*) : tabletype* ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:318.1-318.88 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:320.1-320.88 def $funcsxt(externtype*) : deftype* - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:336.1-336.24 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:338.1-338.24 def $funcsxt([]) = [] - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:337.1-337.47 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:339.1-339.47 def $funcsxt{dt : deftype, `xt*` : externtype*}([FUNC_externtype((dt : deftype <: typeuse))] ++ xt*{xt <- `xt*`}) = [dt] ++ $funcsxt(xt*{xt <- `xt*`}) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:338.1-338.59 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:340.1-340.59 def $funcsxt{externtype : externtype, `xt*` : externtype*}([externtype] ++ xt*{xt <- `xt*`}) = $funcsxt(xt*{xt <- `xt*`}) -- otherwise } @@ -1135,14 +1136,14 @@ def $funcsxt(externtype*) : deftype* ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:343.1-343.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:345.1-345.112 def $subst_typevar(typevar : typevar, typevar*, typeuse*) : typeuse - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:374.1-374.38 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:376.1-376.38 def $subst_typevar{tv : typevar}(tv, [], []) = (tv : typevar <: typeuse) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:375.1-375.95 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:377.1-377.95 def $subst_typevar{tv : typevar, tv_1 : typevar, `tv'*` : typevar*, tu_1 : typeuse, `tu'*` : typeuse*}(tv, [tv_1] ++ tv'*{tv' <- `tv'*`}, [tu_1] ++ tu'*{tu' <- `tu'*`}) = tu_1 -- if (tv = tv_1) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:376.1-376.92 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:378.1-378.92 def $subst_typevar{tv : typevar, tv_1 : typevar, `tv'*` : typevar*, tu_1 : typeuse, `tu'*` : typeuse*}(tv, [tv_1] ++ tv'*{tv' <- `tv'*`}, [tu_1] ++ tu'*{tu' <- `tu'*`}) = $subst_typevar(tv, tv'*{tv' <- `tv'*`}, tu'*{tu' <- `tu'*`}) -- otherwise } @@ -1150,13 +1151,13 @@ def $subst_typevar(typevar : typevar, typevar*, typeuse*) : typeuse ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:416.1-416.59 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:418.1-418.59 def $minus_recs(typevar*, typeuse*) : (typevar*, typeuse*) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:417.1-417.39 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:419.1-419.39 def $minus_recs([], []) = ([], []) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:418.1-418.63 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:420.1-420.63 def $minus_recs{n : n, `tv*` : typevar*, tu_1 : typeuse, `tu*` : typeuse*}([REC_typevar(n)] ++ tv*{tv <- `tv*`}, [tu_1] ++ tu*{tu <- `tu*`}) = $minus_recs(tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:419.1-420.45 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:421.1-422.45 def $minus_recs{x : idx, `tv*` : typevar*, tu_1 : typeuse, `tu*` : typeuse*, `tv'*` : typevar*, `tu'*` : typeuse*}([_IDX_typevar(x)] ++ tv*{tv <- `tv*`}, [tu_1] ++ tu*{tu <- `tu*`}) = ([_IDX_typevar(x)] ++ tv'*{tv' <- `tv'*`}, [tu_1] ++ tu'*{tu' <- `tu'*`}) -- if ((tv'*{tv' <- `tv'*`}, tu'*{tu' <- `tu'*`}) = $minus_recs(tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) } @@ -1179,89 +1180,89 @@ def $subst_vectype(vectype : vectype, typevar*, typeuse*) : vectype ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:344.1-344.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:346.1-346.112 def $subst_typeuse(typeuse : typeuse, typevar*, typeuse*) : typeuse - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:378.1-378.66 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:380.1-380.66 def $subst_typeuse{tv' : typevar, `tv*` : typevar*, `tu*` : typeuse*}((tv' : typevar <: typeuse), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = $subst_typevar(tv', tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:379.1-379.64 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:381.1-381.64 def $subst_typeuse{dt : deftype, `tv*` : typevar*, `tu*` : typeuse*}((dt : deftype <: typeuse), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ($subst_deftype(dt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : deftype <: typeuse) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:349.1-349.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:351.1-351.112 def $subst_heaptype(heaptype : heaptype, typevar*, typeuse*) : heaptype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:385.1-385.67 - def $subst_heaptype{tv' : typevar, `tv*` : typevar*, `tu*` : typeuse*}((tv' : typevar <: heaptype), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ($subst_typevar(tv', tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : typeuse <: heaptype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:386.1-386.65 - def $subst_heaptype{dt : deftype, `tv*` : typevar*, `tu*` : typeuse*}((dt : deftype <: heaptype), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ($subst_deftype(dt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : deftype <: heaptype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:387.1-387.53 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:387.1-387.89 + def $subst_heaptype{`exact?` : exact?, tv' : typevar, `tv*` : typevar*, `tu*` : typeuse*}(_HT_heaptype(exact?{exact <- `exact?`}, (tv' : typevar <: typeuse)), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = _HT_heaptype(exact?{exact <- `exact?`}, $subst_typevar(tv', tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:388.1-388.87 + def $subst_heaptype{`exact?` : exact?, dt : deftype, `tv*` : typevar*, `tu*` : typeuse*}(_HT_heaptype(exact?{exact <- `exact?`}, (dt : deftype <: typeuse)), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = _HT_heaptype(exact?{exact <- `exact?`}, ($subst_deftype(dt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : deftype <: typeuse)) + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:389.1-389.53 def $subst_heaptype{ht : heaptype, `tv*` : typevar*, `tu*` : typeuse*}(ht, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ht -- otherwise -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:350.1-350.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:352.1-352.112 def $subst_reftype(reftype : reftype, typevar*, typeuse*) : reftype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:389.1-389.87 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:391.1-391.87 def $subst_reftype{`null?` : null?, ht : heaptype, `tv*` : typevar*, `tu*` : typeuse*}(REF_reftype(null?{null <- `null?`}, ht), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = REF_reftype(null?{null <- `null?`}, $subst_heaptype(ht, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:351.1-351.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:353.1-353.112 def $subst_valtype(valtype : valtype, typevar*, typeuse*) : valtype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:391.1-391.64 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:393.1-393.64 def $subst_valtype{nt : numtype, `tv*` : typevar*, `tu*` : typeuse*}((nt : numtype <: valtype), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ($subst_numtype(nt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : numtype <: valtype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:392.1-392.64 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:394.1-394.64 def $subst_valtype{vt : vectype, `tv*` : typevar*, `tu*` : typeuse*}((vt : vectype <: valtype), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ($subst_vectype(vt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : vectype <: valtype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:393.1-393.64 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:395.1-395.64 def $subst_valtype{rt : reftype, `tv*` : typevar*, `tu*` : typeuse*}((rt : reftype <: valtype), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ($subst_reftype(rt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : reftype <: valtype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:394.1-394.40 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:396.1-396.40 def $subst_valtype{`tv*` : typevar*, `tu*` : typeuse*}(BOT_valtype, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = BOT_valtype -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:354.1-354.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:356.1-356.112 def $subst_storagetype(storagetype : storagetype, typevar*, typeuse*) : storagetype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:398.1-398.66 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:400.1-400.66 def $subst_storagetype{t : valtype, `tv*` : typevar*, `tu*` : typeuse*}((t : valtype <: storagetype), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ($subst_valtype(t, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : valtype <: storagetype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:399.1-399.69 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:401.1-401.69 def $subst_storagetype{pt : packtype, `tv*` : typevar*, `tu*` : typeuse*}((pt : packtype <: storagetype), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ($subst_packtype(pt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) : packtype <: storagetype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:355.1-355.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:357.1-357.112 def $subst_fieldtype(fieldtype : fieldtype, typevar*, typeuse*) : fieldtype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:401.1-401.82 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:403.1-403.82 def $subst_fieldtype{`mut?` : mut?, zt : storagetype, `tv*` : typevar*, `tu*` : typeuse*}(`%%`_fieldtype(mut?{mut <- `mut?`}, zt), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = `%%`_fieldtype(mut?{mut <- `mut?`}, $subst_storagetype(zt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:356.1-356.122 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:358.1-358.122 def $subst_describestype(describestype : describestype, typevar*, typeuse*) : describestype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:407.1-407.92 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:409.1-409.92 def $subst_describestype{tu' : typeuse, `tv*` : typevar*, `tu*` : typeuse*}(DESCRIBES_describestype(tu'), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = DESCRIBES_describestype($subst_typeuse(tu', tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:357.1-357.122 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:359.1-359.122 def $subst_descriptortype(descriptortype : descriptortype, typevar*, typeuse*) : descriptortype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:408.1-408.95 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:410.1-410.95 def $subst_descriptortype{tu' : typeuse, `tv*` : typevar*, `tu*` : typeuse*}(DESCRIPTOR_descriptortype(tu'), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = DESCRIPTOR_descriptortype($subst_typeuse(tu', tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:359.1-359.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:361.1-361.112 def $subst_comptype(comptype : comptype, typevar*, typeuse*) : comptype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:403.1-403.85 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:405.1-405.85 def $subst_comptype{`ft*` : fieldtype*, `tv*` : typevar*, `tu*` : typeuse*}(STRUCT_comptype(`%`_list(ft*{ft <- `ft*`})), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = STRUCT_comptype(`%`_list($subst_fieldtype(ft, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})*{ft <- `ft*`})) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:404.1-404.81 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:406.1-406.81 def $subst_comptype{ft : fieldtype, `tv*` : typevar*, `tu*` : typeuse*}(ARRAY_comptype(ft), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = ARRAY_comptype($subst_fieldtype(ft, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:405.1-405.123 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:407.1-407.123 def $subst_comptype{`t_1*` : valtype*, `t_2*` : valtype*, `tv*` : typevar*, `tu*` : typeuse*}(`FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`})), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = `FUNC%->%`_comptype(`%`_resulttype($subst_valtype(t_1, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})*{t_1 <- `t_1*`}), `%`_resulttype($subst_valtype(t_2, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})*{t_2 <- `t_2*`})) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:360.1-360.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:362.1-362.112 def $subst_desctype(desctype : desctype, typevar*, typeuse*) : desctype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:410.1-411.107 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:412.1-413.107 def $subst_desctype{`dc1?` : describestype?, `dc2?` : descriptortype?, ct : comptype, `tv*` : typevar*, `tu*` : typeuse*}(`%%%`_desctype(dc1?{dc1 <- `dc1?`}, dc2?{dc2 <- `dc2?`}, ct), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = `%%%`_desctype($subst_describestype(dc1, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})?{dc1 <- `dc1?`}, $subst_descriptortype(dc2, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})?{dc2 <- `dc2?`}, $subst_comptype(ct, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:361.1-361.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:363.1-363.112 def $subst_subtype(subtype : subtype, typevar*, typeuse*) : subtype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:413.1-414.80 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:415.1-416.80 def $subst_subtype{`final?` : final?, `tu'*` : typeuse*, desctype : desctype, `tv*` : typevar*, `tu*` : typeuse*}(SUB_subtype(final?{final <- `final?`}, tu'*{tu' <- `tu'*`}, desctype), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = SUB_subtype(final?{final <- `final?`}, $subst_typeuse(tu', tv*{tv <- `tv*`}, tu*{tu <- `tu*`})*{tu' <- `tu'*`}, $subst_desctype(desctype, tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:362.1-362.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:364.1-364.112 def $subst_rectype(rectype : rectype, typevar*, typeuse*) : rectype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:422.1-423.45 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:424.1-425.45 def $subst_rectype{`st*` : subtype*, `tv*` : typevar*, `tu*` : typeuse*, `tv'*` : typevar*, `tu'*` : typeuse*}(REC_rectype(`%`_list(st*{st <- `st*`})), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = REC_rectype(`%`_list($subst_subtype(st, tv'*{tv' <- `tv'*`}, tu'*{tu' <- `tu'*`})*{st <- `st*`})) -- if ((tv'*{tv' <- `tv'*`}, tu'*{tu' <- `tu'*`}) = $minus_recs(tv*{tv <- `tv*`}, tu*{tu <- `tu*`})) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:363.1-363.112 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:365.1-365.112 def $subst_deftype(deftype : deftype, typevar*, typeuse*) : deftype - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:428.1-428.80 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:430.1-430.80 def $subst_deftype{qt : rectype, i : n, `tv*` : typevar*, `tu*` : typeuse*}(_DEF_deftype(qt, i), tv*{tv <- `tv*`}, tu*{tu <- `tu*`}) = _DEF_deftype($subst_rectype(qt, tv*{tv <- `tv*`}, tu*{tu <- `tu*`}), i) } @@ -1356,11 +1357,11 @@ def $subst_all_moduletype(moduletype : moduletype, typeuse*) : moduletype ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:466.1-466.97 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:468.1-468.97 def $subst_all_deftypes(deftype*, typeuse*) : deftype* - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:467.1-467.40 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:469.1-469.40 def $subst_all_deftypes{`tu*` : typeuse*}([], tu*{tu <- `tu*`}) = [] - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:468.1-468.101 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:470.1-470.101 def $subst_all_deftypes{dt_1 : deftype, `dt*` : deftype*, `tu*` : typeuse*}([dt_1] ++ dt*{dt <- `dt*`}, tu*{tu <- `tu*`}) = [$subst_all_deftype(dt_1, tu*{tu <- `tu*`})] ++ $subst_all_deftypes(dt*{dt <- `dt*`}, tu*{tu <- `tu*`}) } @@ -1449,90 +1450,90 @@ def $free_typevar(typevar : typevar) : free ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec rec { -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:501.1-501.36 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:503.1-503.36 def $free_heaptype(heaptype : heaptype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:552.1-552.65 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:554.1-554.65 def $free_heaptype{absheaptype : absheaptype}((absheaptype : absheaptype <: heaptype)) = $free_absheaptype(absheaptype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:553.1-553.53 - def $free_heaptype{typeuse : typeuse}((typeuse : typeuse <: heaptype)) = $free_typeuse(typeuse) + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:555.1-555.64 + def $free_heaptype{`exact?` : exact?, typeuse : typeuse}(_HT_heaptype(exact?{exact <- `exact?`}, typeuse)) = $free_typeuse(typeuse) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:502.1-502.34 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:504.1-504.34 def $free_reftype(reftype : reftype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:555.1-555.65 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:557.1-557.65 def $free_reftype{`null?` : null?, heaptype : heaptype}(REF_reftype(null?{null <- `null?`}, heaptype)) = $free_heaptype(heaptype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:504.1-504.34 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:506.1-506.34 def $free_typeuse(typeuse : typeuse) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:549.1-549.52 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:551.1-551.52 def $free_typeuse{typevar : typevar}((typevar : typevar <: typeuse)) = $free_typevar(typevar) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:550.1-550.52 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:552.1-552.52 def $free_typeuse{deftype : deftype}((deftype : deftype <: typeuse)) = $free_deftype(deftype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:505.1-505.34 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:507.1-507.34 def $free_valtype(valtype : valtype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:557.1-557.52 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:559.1-559.52 def $free_valtype{numtype : numtype}((numtype : numtype <: valtype)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:558.1-558.52 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:560.1-560.52 def $free_valtype{vectype : vectype}((vectype : vectype <: valtype)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:559.1-559.52 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:561.1-561.52 def $free_valtype{reftype : reftype}((reftype : reftype <: valtype)) = $free_reftype(reftype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:560.1-560.28 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:562.1-562.28 def $free_valtype(BOT_valtype) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:507.1-507.40 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:509.1-509.40 def $free_resulttype(resulttype : resulttype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:562.1-562.69 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:564.1-564.69 def $free_resulttype{`valtype*` : valtype*}(`%`_resulttype(valtype*{valtype <- `valtype*`})) = $free_list($free_valtype(valtype)*{valtype <- `valtype*`}) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:508.1-508.42 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:510.1-510.42 def $free_storagetype(storagetype : storagetype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:564.1-564.56 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:566.1-566.56 def $free_storagetype{valtype : valtype}((valtype : valtype <: storagetype)) = $free_valtype(valtype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:565.1-565.59 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:567.1-567.59 def $free_storagetype{packtype : packtype}((packtype : packtype <: storagetype)) = $free_packtype(packtype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:509.1-509.38 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:511.1-511.38 def $free_fieldtype(fieldtype : fieldtype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:567.1-567.71 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:569.1-569.71 def $free_fieldtype{`mut?` : mut?, storagetype : storagetype}(`%%`_fieldtype(mut?{mut <- `mut?`}, storagetype)) = $free_storagetype(storagetype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:510.1-510.36 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:512.1-512.36 def $free_comptype(comptype : comptype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:569.1-569.80 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:571.1-571.80 def $free_comptype{`fieldtype*` : fieldtype*}(STRUCT_comptype(`%`_list(fieldtype*{fieldtype <- `fieldtype*`}))) = $free_list($free_fieldtype(fieldtype)*{fieldtype <- `fieldtype*`}) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:570.1-570.65 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:572.1-572.65 def $free_comptype{fieldtype : fieldtype}(ARRAY_comptype(fieldtype)) = $free_fieldtype(fieldtype) - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:571.1-571.121 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:573.1-573.121 def $free_comptype{resulttype_1 : resulttype, resulttype_2 : resulttype}(`FUNC%->%`_comptype(resulttype_1, resulttype_2)) = $free_resulttype(resulttype_1) +++ $free_resulttype(resulttype_2) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:511.1-511.46 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:513.1-513.46 def $free_describestype(describestype : describestype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:573.1-573.58 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:575.1-575.58 def $free_describestype{tu : typeuse}(DESCRIBES_describestype(tu)) = $free_typeuse(tu) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:512.1-512.48 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:514.1-514.48 def $free_descriptortype(descriptortype : descriptortype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:574.1-574.60 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:576.1-576.60 def $free_descriptortype{tu : typeuse}(DESCRIPTOR_descriptortype(tu)) = $free_typeuse(tu) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:513.1-513.36 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:515.1-515.36 def $free_desctype(desctype : desctype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:576.1-577.102 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:578.1-579.102 def $free_desctype{`dc1?` : describestype?, `dc2?` : descriptortype?, ct : comptype}(`%%%`_desctype(dc1?{dc1 <- `dc1?`}, dc2?{dc2 <- `dc2?`}, ct)) = $free_opt($free_describestype(dc1)?{dc1 <- `dc1?`}) +++ $free_opt($free_descriptortype(dc2)?{dc2 <- `dc2?`}) +++ $free_comptype(ct) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:514.1-514.34 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:516.1-516.34 def $free_subtype(subtype : subtype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:579.1-580.66 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:581.1-582.66 def $free_subtype{`final?` : final?, `typeuse*` : typeuse*, desctype : desctype}(SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, desctype)) = $free_list($free_typeuse(typeuse)*{typeuse <- `typeuse*`}) +++ $free_desctype(desctype) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:515.1-515.34 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:517.1-517.34 def $free_rectype(rectype : rectype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:582.1-582.70 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:584.1-584.70 def $free_rectype{`subtype*` : subtype*}(REC_rectype(`%`_list(subtype*{subtype <- `subtype*`}))) = $free_list($free_subtype(subtype)*{subtype <- `subtype*`}) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:543.1-543.34 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:545.1-545.34 def $free_deftype(deftype : deftype) : free - ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:544.1-544.59 + ;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:546.1-546.59 def $free_deftype{rectype : rectype, n : n}(_DEF_deftype(rectype, n)) = $free_rectype(rectype) } @@ -2794,11 +2795,11 @@ def $before(typeuse : typeuse, typeidx : typeidx, nat : nat) : bool ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec def $unrollht(context : context, heaptype : heaptype) : subtype ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec - def $unrollht{C : context, deftype : deftype}(C, (deftype : deftype <: heaptype)) = $unrolldt(deftype) + def $unrollht{C : context, `exact?` : exact?, deftype : deftype}(C, _HT_heaptype(exact?{exact <- `exact?`}, (deftype : deftype <: typeuse))) = $unrolldt(deftype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec - def $unrollht{C : context, typeidx : typeidx}(C, _IDX_heaptype(typeidx)) = $unrolldt(C.TYPES_context[typeidx!`%`_typeidx.0]) + def $unrollht{C : context, `exact?` : exact?, typeidx : typeidx}(C, _HT_heaptype(exact?{exact <- `exact?`}, _IDX_typeuse(typeidx))) = $unrolldt(C.TYPES_context[typeidx!`%`_typeidx.0]) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec - def $unrollht{C : context, i : n}(C, REC_heaptype(i)) = C.RECS_context[i] + def $unrollht{C : context, `exact?` : exact?, i : n}(C, _HT_heaptype(exact?{exact <- `exact?`}, REC_typeuse(i))) = C.RECS_context[i] ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec rec { @@ -2810,116 +2811,111 @@ relation Heaptype_ok: `%|-%:OK`(context, heaptype) `%|-%:OK`(C, (absheaptype : absheaptype <: heaptype)) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:23.1-25.35 - rule typeuse{C : context, typeuse : typeuse}: - `%|-%:OK`(C, (typeuse : typeuse <: heaptype)) - -- Typeuse_ok: `%|-%:OK`(C, typeuse) - - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:27.1-29.35 - rule exact{C : context, typeuse : typeuse}: - `%|-%:OK`(C, EXACT_heaptype(typeuse)) + rule typeuse{C : context, `exact?` : exact?, typeuse : typeuse}: + `%|-%:OK`(C, _HT_heaptype(exact?{exact <- `exact?`}, typeuse)) -- Typeuse_ok: `%|-%:OK`(C, typeuse) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:10.1-10.91 relation Reftype_ok: `%|-%:OK`(context, reftype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:31.1-33.37 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:27.1-29.37 rule _{C : context, heaptype : heaptype}: `%|-%:OK`(C, REF_reftype(NULL_null?{}, heaptype)) -- Heaptype_ok: `%|-%:OK`(C, heaptype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:11.1-11.91 relation Valtype_ok: `%|-%:OK`(context, valtype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:35.1-37.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:31.1-33.35 rule num{C : context, numtype : numtype}: `%|-%:OK`(C, (numtype : numtype <: valtype)) -- Numtype_ok: `%|-%:OK`(C, numtype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:39.1-41.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:35.1-37.35 rule vec{C : context, vectype : vectype}: `%|-%:OK`(C, (vectype : vectype <: valtype)) -- Vectype_ok: `%|-%:OK`(C, vectype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:43.1-45.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:39.1-41.35 rule ref{C : context, reftype : reftype}: `%|-%:OK`(C, (reftype : reftype <: valtype)) -- Reftype_ok: `%|-%:OK`(C, reftype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:47.1-48.16 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:43.1-44.16 rule bot{C : context}: `%|-%:OK`(C, BOT_valtype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:12.1-12.94 relation Typeuse_ok: `%|-%:OK`(context, typeuse) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:105.1-107.30 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:101.1-103.30 rule typeidx{C : context, typeidx : typeidx, dt : deftype}: `%|-%:OK`(C, _IDX_typeuse(typeidx)) -- if (C.TYPES_context[typeidx!`%`_typeidx.0] = dt) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:109.1-111.23 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:105.1-107.23 rule rec{C : context, i : n, st : subtype}: `%|-%:OK`(C, REC_typeuse(i)) -- if (C.RECS_context[i] = st) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:113.1-115.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:109.1-111.35 rule deftype{C : context, deftype : deftype}: `%|-%:OK`(C, (deftype : deftype <: typeuse)) -- Deftype_ok: `%|-%:OK`(C, deftype) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:53.1-53.100 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:49.1-49.100 relation Resulttype_ok: `%|-%:OK`(context, resulttype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:56.1-58.32 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:52.1-54.32 rule _{C : context, `t*` : valtype*}: `%|-%:OK`(C, `%`_resulttype(t*{t <- `t*`})) -- (Valtype_ok: `%|-%:OK`(C, t))*{t <- `t*`} -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:89.1-89.104 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:85.1-85.104 relation Fieldtype_ok: `%|-%:OK`(context, fieldtype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:129.1-131.43 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:125.1-127.43 rule _{C : context, storagetype : storagetype}: `%|-%:OK`(C, `%%`_fieldtype(MUT_mut?{}, storagetype)) -- Storagetype_ok: `%|-%:OK`(C, storagetype) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:90.1-90.106 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:86.1-86.106 relation Storagetype_ok: `%|-%:OK`(context, storagetype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:121.1-123.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:117.1-119.35 rule val{C : context, valtype : valtype}: `%|-%:OK`(C, (valtype : valtype <: storagetype)) -- Valtype_ok: `%|-%:OK`(C, valtype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:125.1-127.37 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:121.1-123.37 rule pack{C : context, packtype : packtype}: `%|-%:OK`(C, (packtype : packtype <: storagetype)) -- Packtype_ok: `%|-%:OK`(C, packtype) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:91.1-91.103 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:87.1-87.103 relation Comptype_ok: `%|-%:OK`(context, comptype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:134.1-136.42 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:130.1-132.42 rule struct{C : context, `fieldtype*` : fieldtype*}: `%|-%:OK`(C, STRUCT_comptype(`%`_list(fieldtype*{fieldtype <- `fieldtype*`}))) -- (Fieldtype_ok: `%|-%:OK`(C, fieldtype))*{fieldtype <- `fieldtype*`} - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:138.1-140.39 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:134.1-136.39 rule array{C : context, fieldtype : fieldtype}: `%|-%:OK`(C, ARRAY_comptype(fieldtype)) -- Fieldtype_ok: `%|-%:OK`(C, fieldtype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:142.1-145.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:138.1-141.35 rule func{C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%|-%:OK`(C, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_1*{t_1 <- `t_1*`})) -- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`})) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:92.1-92.103 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:88.1-88.103 relation Desctype_ok: `%|-%:OK`(context, desctype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:148.1-152.31 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:144.1-148.31 rule _{C : context, `tu_1?` : typeuse?, `tu_2?` : typeuse?, ct : comptype}: `%|-%:OK`(C, `%%%`_desctype(DESCRIBES_describestype(tu_1)?{tu_1 <- `tu_1?`}, DESCRIPTOR_descriptortype(tu_2)?{tu_2 <- `tu_2?`}, ct)) -- (Typeuse_ok: `%|-%:OK`(C, tu_1))?{tu_1 <- `tu_1?`} -- (Typeuse_ok: `%|-%:OK`(C, tu_2))?{tu_2 <- `tu_2?`} -- Comptype_ok: `%|-%:OK`(C, ct) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:93.1-93.126 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:89.1-89.126 relation Subtype_ok: `%|-%:%`(context, subtype, oktypeidx) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:155.1-162.49 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:151.1-158.49 rule _{C : context, `x*` : idx*, desctype : desctype, x_0 : idx, `x'**` : idx**, `desctype'*` : desctype*}: `%|-%:%`(C, SUB_subtype(FINAL_final?{}, _IDX_typeuse(x)*{x <- `x*`}, desctype), OK_oktypeidx(x_0)) -- if (|x*{x <- `x*`}| <= 1) @@ -2928,56 +2924,56 @@ relation Subtype_ok: `%|-%:%`(context, subtype, oktypeidx) -- Desctype_ok: `%|-%:OK`(C, desctype) -- (Desctype_sub: `%|-%<:%`(C, desctype, desctype'))*{desctype' <- `desctype'*`} -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:94.1-94.126 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:90.1-90.126 relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:184.1-185.23 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:180.1-181.23 rule empty{C : context, x : idx}: `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidx(x)) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:187.1-190.48 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:183.1-186.48 rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx}: `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidx(x)) -- Subtype_ok: `%|-%:%`(C, subtype_1, OK_oktypeidx(x)) -- Rectype_ok: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidx(`%`_typeidx((x!`%`_idx.0 + 1)))) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:192.1-194.60 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:188.1-190.60 rule _rec2{C : context, `subtype*` : subtype*, x : idx}: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidx(x)) -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype*{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, 0)) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:95.1-95.126 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:91.1-91.126 relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:174.1-181.49 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:170.1-177.49 rule _{C : context, `typeuse*` : typeuse*, desctype : desctype, x : idx, i : nat, `typeuse'**` : typeuse**, `desctype'*` : desctype*}: `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, desctype), OK_oktypeidxnat(x, i)) -- if (|typeuse*{typeuse <- `typeuse*`}| <= 1) -- (if $before(typeuse, x, i))*{typeuse <- `typeuse*`} - -- (if ($unrollht(C, (typeuse : typeuse <: heaptype)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, desctype')))*{desctype' <- `desctype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`} + -- (if ($unrollht(C, _HT_heaptype(?(), typeuse)) = SUB_subtype(?(), typeuse'*{typeuse' <- `typeuse'*`}, desctype')))*{desctype' <- `desctype'*`, typeuse <- `typeuse*`, `typeuse'*` <- `typeuse'**`} -- Desctype_ok: `%|-%:OK`(C, desctype) -- (Desctype_sub: `%|-%<:%`(C, desctype, desctype'))*{desctype' <- `desctype'*`} -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.126 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:92.1-92.126 relation Rectype_ok2: `%|-%:%`(context, rectype, oktypeidxnat) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:196.1-197.24 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:192.1-193.24 rule empty{C : context, x : idx, i : nat}: `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidxnat(x, i)) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:199.1-202.55 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:195.1-198.55 rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx, i : nat}: `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, i)) -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypeidxnat(x, i)) -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(`%`_typeidx((x!`%`_idx.0 + 1)), (i + 1))) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.102 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:93.1-93.102 relation Deftype_ok: `%|-%:OK`(context, deftype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:205.1-209.14 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:201.1-205.14 rule _{C : context, rectype : rectype, i : n, x : idx, `subtype*` : subtype*, n : n}: `%|-%:OK`(C, _DEF_deftype(rectype, i)) -- Rectype_ok: `%|-%:%`(C, rectype, OK_oktypeidx(x)) -- if (rectype = REC_rectype(`%`_list(subtype^n{subtype <- `subtype*`}))) -- if (i < n) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:100.1-100.108 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.108 relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:170.1-172.41 rule struct{C : context, `ft_1*` : fieldtype*, `ft'_1*` : fieldtype*, `ft_2*` : fieldtype*}: @@ -2995,27 +2991,27 @@ relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_11*{t_11 <- `t_11*`})) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_12*{t_12 <- `t_12*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`})) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:101.1-101.108 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.108 relation Desctype_sub: `%|-%<:%`(context, desctype, desctype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:184.1-188.37 rule _{C : context, tu_11 : typeuse, tu_12 : typeuse, ct_1 : comptype, tu_21 : typeuse, tu_22 : typeuse, ct_2 : comptype}: `%|-%<:%`(C, `%%%`_desctype(?(DESCRIBES_describestype(tu_11)), ?(DESCRIPTOR_descriptortype(tu_12)), ct_1), `%%%`_desctype(?(DESCRIBES_describestype(tu_21)), ?(DESCRIPTOR_descriptortype(tu_22)), ct_2)) - -- Heaptype_sub: `%|-%<:%`(C, (tu_11 : typeuse <: heaptype), (tu_21 : typeuse <: heaptype)) - -- Heaptype_sub: `%|-%<:%`(C, (tu_12 : typeuse <: heaptype), (tu_22 : typeuse <: heaptype)) + -- Heaptype_sub: `%|-%<:%`(C, _HT_heaptype(?(), tu_11), _HT_heaptype(?(), tu_21)) + -- Heaptype_sub: `%|-%<:%`(C, _HT_heaptype(?(), tu_12), _HT_heaptype(?(), tu_22)) -- Comptype_sub: `%|-%<:%`(C, ct_1, ct_2) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:102.1-102.107 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:98.1-98.107 relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:191.1-193.66 rule refl{C : context, deftype_1 : deftype, deftype_2 : deftype}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($clos_deftype(C, deftype_1) = $clos_deftype(C, deftype_2)) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:195.1-198.49 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:195.1-198.57 rule super{C : context, deftype_1 : deftype, deftype_2 : deftype, `final?` : final?, `typeuse*` : typeuse*, desctype : desctype, i : nat}: `%|-%<:%`(C, deftype_1, deftype_2) -- if ($unrolldt(deftype_1) = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, desctype)) - -- Heaptype_sub: `%|-%<:%`(C, (typeuse*{typeuse <- `typeuse*`}[i] : typeuse <: heaptype), (deftype_2 : deftype <: heaptype)) + -- Heaptype_sub: `%|-%<:%`(C, _HT_heaptype(?(), typeuse*{typeuse <- `typeuse*`}[i]), _HT_heaptype(?(), (deftype_2 : deftype <: typeuse))) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:9.1-9.104 relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) @@ -3023,10 +3019,10 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) rule refl{C : context, heaptype : heaptype}: `%|-%<:%`(C, heaptype, heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:23.1-25.44 - rule `exact-l`{C : context, typeuse : typeuse, heaptype : heaptype}: - `%|-%<:%`(C, EXACT_heaptype(typeuse), heaptype) - -- Heaptype_sub: `%|-%<:%`(C, (typeuse : typeuse <: heaptype), heaptype) + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:23.1-25.48 + rule `exact-l`{C : context, exact : exact, typeuse : typeuse, heaptype : heaptype}: + `%|-%<:%`(C, _HT_heaptype(?(exact), typeuse), heaptype) + -- Heaptype_sub: `%|-%<:%`(C, _HT_heaptype(?(), typeuse), heaptype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:27.1-31.48 rule trans{C : context, heaptype_1 : heaptype, heaptype_2 : heaptype, heaptype' : heaptype}: @@ -3053,37 +3049,37 @@ relation Heaptype_sub: `%|-%<:%`(context, heaptype, heaptype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:45.1-47.42 rule struct{C : context, deftype : deftype, `fieldtype*` : fieldtype*}: - `%|-%<:%`(C, (deftype : deftype <: heaptype), STRUCT_heaptype) + `%|-%<:%`(C, _HT_heaptype(?(), (deftype : deftype <: typeuse)), STRUCT_heaptype) -- Expand: `%~~%`(deftype, STRUCT_comptype(`%`_list(fieldtype*{fieldtype <- `fieldtype*`}))) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:49.1-51.40 rule array{C : context, deftype : deftype, fieldtype : fieldtype}: - `%|-%<:%`(C, (deftype : deftype <: heaptype), ARRAY_heaptype) + `%|-%<:%`(C, _HT_heaptype(?(), (deftype : deftype <: typeuse)), ARRAY_heaptype) -- Expand: `%~~%`(deftype, ARRAY_comptype(fieldtype)) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:53.1-55.42 rule func{C : context, deftype : deftype, `t_1*` : valtype*, `t_2*` : valtype*}: - `%|-%<:%`(C, (deftype : deftype <: heaptype), FUNC_heaptype) + `%|-%<:%`(C, _HT_heaptype(?(), (deftype : deftype <: typeuse)), FUNC_heaptype) -- Expand: `%~~%`(deftype, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:57.1-59.46 rule def{C : context, deftype_1 : deftype, deftype_2 : deftype}: - `%|-%<:%`(C, (deftype_1 : deftype <: heaptype), (deftype_2 : deftype <: heaptype)) + `%|-%<:%`(C, _HT_heaptype(?(), (deftype_1 : deftype <: typeuse)), _HT_heaptype(?(), (deftype_2 : deftype <: typeuse))) -- Deftype_sub: `%|-%<:%`(C, deftype_1, deftype_2) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:61.1-63.53 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:61.1-63.57 rule `typeidx-l`{C : context, typeidx : typeidx, heaptype : heaptype}: - `%|-%<:%`(C, _IDX_heaptype(typeidx), heaptype) - -- Heaptype_sub: `%|-%<:%`(C, (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: heaptype), heaptype) + `%|-%<:%`(C, _HT_heaptype(?(), _IDX_typeuse(typeidx)), heaptype) + -- Heaptype_sub: `%|-%<:%`(C, _HT_heaptype(?(), (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: typeuse)), heaptype) - ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:65.1-67.53 + ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:65.1-67.57 rule `typeidx-r`{C : context, heaptype : heaptype, typeidx : typeidx}: - `%|-%<:%`(C, heaptype, _IDX_heaptype(typeidx)) - -- Heaptype_sub: `%|-%<:%`(C, heaptype, (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: heaptype)) + `%|-%<:%`(C, heaptype, _HT_heaptype(?(), _IDX_typeuse(typeidx))) + -- Heaptype_sub: `%|-%<:%`(C, heaptype, _HT_heaptype(?(), (C.TYPES_context[typeidx!`%`_typeidx.0] : deftype <: typeuse))) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:69.1-71.49 rule rec{C : context, i : n, `typeuse*` : typeuse*, j : nat, `final?` : final?, desctype : desctype}: - `%|-%<:%`(C, REC_heaptype(i), (typeuse*{typeuse <- `typeuse*`}[j] : typeuse <: heaptype)) + `%|-%<:%`(C, _HT_heaptype(?(), REC_typeuse(i)), _HT_heaptype(?(), typeuse*{typeuse <- `typeuse*`}[j])) -- if (C.RECS_context[i] = SUB_subtype(final?{final <- `final?`}, typeuse*{typeuse <- `typeuse*`}, desctype)) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:73.1-75.40 @@ -3527,7 +3523,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:125.1-127.45 rule call_ref{C : context, x : idx, `t_1*` : valtype*, `t_2*` : valtype*}: - `%|-%:%`(C, CALL_REF_instr(_IDX_typeuse(x)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`} ++ [REF_valtype(?(NULL_null), _IDX_heaptype(x))]), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) + `%|-%:%`(C, CALL_REF_instr(_IDX_typeuse(x)), `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`} ++ [REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x)))]), [], `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:129.1-133.45 @@ -3553,7 +3549,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:149.1-154.42 rule return_call_ref{C : context, x : idx, `t_3*` : valtype*, `t_1*` : valtype*, `t_4*` : valtype*, `t_2*` : valtype*, `t'_2*` : valtype*}: - `%|-%:%`(C, RETURN_CALL_REF_instr(_IDX_typeuse(x)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 <- `t_3*`} ++ t_1*{t_1 <- `t_1*`} ++ [REF_valtype(?(NULL_null), _IDX_heaptype(x))]), [], `%`_resulttype(t_4*{t_4 <- `t_4*`}))) + `%|-%:%`(C, RETURN_CALL_REF_instr(_IDX_typeuse(x)), `%->_%%`_instrtype(`%`_resulttype(t_3*{t_3 <- `t_3*`} ++ t_1*{t_1 <- `t_1*`} ++ [REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x)))]), [], `%`_resulttype(t_4*{t_4 <- `t_4*`}))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- if (C.RETURN_context = ?(`%`_resulttype(t'_2*{t'_2 <- `t'_2*`}))) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`}), `%`_resulttype(t'_2*{t'_2 <- `t'_2*`})) @@ -3594,7 +3590,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:212.1-215.20 rule ref.func{C : context, x : idx, dt : deftype}: - `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), (dt : deftype <: heaptype))]))) + `%|-%:%`(C, REF.FUNC_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), (dt : deftype <: typeuse)))]))) -- if (C.FUNCS_context[x!`%`_idx.0] = dt) -- if (x <- C.REFS_context) @@ -3636,66 +3632,66 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:252.1-254.45 rule struct.new{C : context, x : idx, `zt*` : storagetype*, `mut?*` : mut?*}: - `%|-%:%`(C, STRUCT.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)*{zt <- `zt*`}), [], `%`_resulttype([REF_valtype(?(), _IDX_heaptype(x))]))) + `%|-%:%`(C, STRUCT.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)*{zt <- `zt*`}), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:256.1-259.48 rule struct.new_default{C : context, x : idx, `mut?*` : mut?*, `zt*` : storagetype*}: - `%|-%:%`(C, STRUCT.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), _IDX_heaptype(x))]))) + `%|-%:%`(C, STRUCT.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:264.1-268.41 rule struct.get{C : context, `sx?` : sx?, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*, `mut?` : mut?}: - `%|-%:%`(C, STRUCT.GET_instr(sx?{sx <- `sx?`}, x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x))]), [], `%`_resulttype([$unpack(zt)]))) + `%|-%:%`(C, STRUCT.GET_instr(sx?{sx <- `sx?`}, x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x)))]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(mut?{mut <- `mut?`}, zt)) -- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt)) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:270.1-273.24 rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}: - `%|-%:%`(C, STRUCT.SET_instr(x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x)) $unpack(zt)]), [], `%`_resulttype([]))) + `%|-%:%`(C, STRUCT.SET_instr(x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) $unpack(zt)]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(?(MUT_mut), zt)) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:278.1-280.43 rule array.new{C : context, x : idx, zt : storagetype, `mut?` : mut?}: - `%|-%:%`(C, ARRAY.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype([$unpack(zt) I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _IDX_heaptype(x))]))) + `%|-%:%`(C, ARRAY.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype([$unpack(zt) I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:282.1-285.45 rule array.new_default{C : context, x : idx, `mut?` : mut?, zt : storagetype}: - `%|-%:%`(C, ARRAY.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _IDX_heaptype(x))]))) + `%|-%:%`(C, ARRAY.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- Defaultable: `|-%DEFAULTABLE`($unpack(zt)) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:287.1-289.43 rule array.new_fixed{C : context, x : idx, n : n, zt : storagetype, `mut?` : mut?}: - `%|-%:%`(C, ARRAY.NEW_FIXED_instr(x, `%`_u32(n)), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)^n{}), [], `%`_resulttype([REF_valtype(?(), _IDX_heaptype(x))]))) + `%|-%:%`(C, ARRAY.NEW_FIXED_instr(x, `%`_u32(n)), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)^n{}), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:291.1-294.40 rule array.new_elem{C : context, x : idx, y : idx, `mut?` : mut?, rt : reftype}: - `%|-%:%`(C, ARRAY.NEW_ELEM_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _IDX_heaptype(x))]))) + `%|-%:%`(C, ARRAY.NEW_ELEM_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, (rt : reftype <: storagetype)))) -- Reftype_sub: `%|-%<:%`(C, C.ELEMS_context[y!`%`_idx.0], rt) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:296.1-300.24 rule array.new_data{C : context, x : idx, y : idx, `mut?` : mut?, zt : storagetype, numtype : numtype, vectype : vectype}: - `%|-%:%`(C, ARRAY.NEW_DATA_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _IDX_heaptype(x))]))) + `%|-%:%`(C, ARRAY.NEW_DATA_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if (($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype))) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:302.1-305.39 rule array.get{C : context, `sx?` : sx?, x : idx, zt : storagetype, `mut?` : mut?}: - `%|-%:%`(C, ARRAY.GET_instr(sx?{sx <- `sx?`}, x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x)) I32_valtype]), [], `%`_resulttype([$unpack(zt)]))) + `%|-%:%`(C, ARRAY.GET_instr(sx?{sx <- `sx?`}, x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((sx?{sx <- `sx?`} = ?()) <=> $is_packtype(zt)) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:307.1-309.42 rule array.set{C : context, x : idx, zt : storagetype}: - `%|-%:%`(C, ARRAY.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x)) I32_valtype $unpack(zt)]), [], `%`_resulttype([]))) + `%|-%:%`(C, ARRAY.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype $unpack(zt)]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:311.1-312.43 @@ -3704,25 +3700,25 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:314.1-316.42 rule array.fill{C : context, x : idx, zt : storagetype}: - `%|-%:%`(C, ARRAY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x)) I32_valtype $unpack(zt) I32_valtype]), [], `%`_resulttype([]))) + `%|-%:%`(C, ARRAY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype $unpack(zt) I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:318.1-322.40 rule array.copy{C : context, x_1 : idx, x_2 : idx, zt_1 : storagetype, `mut?` : mut?, zt_2 : storagetype}: - `%|-%:%`(C, ARRAY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x_1)) I32_valtype REF_valtype(?(NULL_null), _IDX_heaptype(x_2)) I32_valtype I32_valtype]), [], `%`_resulttype([]))) + `%|-%:%`(C, ARRAY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x_1))) I32_valtype REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x_2))) I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x_1!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt_1))) -- Expand: `%~~%`(C.TYPES_context[x_2!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt_2))) -- Storagetype_sub: `%|-%<:%`(C, zt_2, zt_1) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:324.1-327.44 rule array.init_elem{C : context, x : idx, y : idx, zt : storagetype}: - `%|-%:%`(C, ARRAY.INIT_ELEM_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x)) I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) + `%|-%:%`(C, ARRAY.INIT_ELEM_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) -- Storagetype_sub: `%|-%<:%`(C, (C.ELEMS_context[y!`%`_idx.0] : reftype <: storagetype), zt) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:329.1-333.24 rule array.init_data{C : context, x : idx, y : idx, zt : storagetype, numtype : numtype, vectype : vectype}: - `%|-%:%`(C, ARRAY.INIT_DATA_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _IDX_heaptype(x)) I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) + `%|-%:%`(C, ARRAY.INIT_DATA_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) -- if (($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype))) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) @@ -5913,17 +5909,17 @@ relation Ref_ok: `%|-%:%`(store, ref, reftype) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec:42.1-44.31 rule struct{s : store, a : addr, dt : deftype}: - `%|-%:%`(s, REF.STRUCT_ADDR_ref(a), REF_reftype(?(), (dt : deftype <: heaptype))) + `%|-%:%`(s, REF.STRUCT_ADDR_ref(a), REF_reftype(?(), _HT_heaptype(?(), (dt : deftype <: typeuse)))) -- if (s.STRUCTS_store[a].TYPE_structinst = dt) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec:46.1-48.30 rule array{s : store, a : addr, dt : deftype}: - `%|-%:%`(s, REF.ARRAY_ADDR_ref(a), REF_reftype(?(), (dt : deftype <: heaptype))) + `%|-%:%`(s, REF.ARRAY_ADDR_ref(a), REF_reftype(?(), _HT_heaptype(?(), (dt : deftype <: typeuse)))) -- if (s.ARRAYS_store[a].TYPE_arrayinst = dt) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec:50.1-52.29 rule func{s : store, a : addr, dt : deftype}: - `%|-%:%`(s, REF.FUNC_ADDR_ref(a), REF_reftype(?(), (dt : deftype <: heaptype))) + `%|-%:%`(s, REF.FUNC_ADDR_ref(a), REF_reftype(?(), _HT_heaptype(?(), (dt : deftype <: typeuse)))) -- if (s.FUNCS_store[a].TYPE_funcinst = dt) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec:54.1-56.24 @@ -6125,11 +6121,11 @@ relation Step_pure: `%~>%`(instr*, instr*) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec rule call_indirect{x : idx, yy : typeuse}: - `%~>%`([CALL_INDIRECT_instr(x, yy)], [TABLE.GET_instr(x) REF.CAST_instr(REF_reftype(?(NULL_null), (yy : typeuse <: heaptype))) CALL_REF_instr(yy)]) + `%~>%`([CALL_INDIRECT_instr(x, yy)], [TABLE.GET_instr(x) REF.CAST_instr(REF_reftype(?(NULL_null), _HT_heaptype(?(), yy))) CALL_REF_instr(yy)]) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec rule return_call_indirect{x : idx, yy : typeuse}: - `%~>%`([RETURN_CALL_INDIRECT_instr(x, yy)], [TABLE.GET_instr(x) REF.CAST_instr(REF_reftype(?(NULL_null), (yy : typeuse <: heaptype))) RETURN_CALL_REF_instr(yy)]) + `%~>%`([RETURN_CALL_INDIRECT_instr(x, yy)], [TABLE.GET_instr(x) REF.CAST_instr(REF_reftype(?(NULL_null), _HT_heaptype(?(), yy))) RETURN_CALL_REF_instr(yy)]) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec rule `frame-vals`{n : n, f : frame, `val*` : val*}: @@ -6754,7 +6750,7 @@ relation Step_read: `%~>%`(config, instr*) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec rule `ref.null-idx`{z : state, x : idx}: - `%~>%`(`%;%`_config(z, [REF.NULL_instr(_IDX_heaptype(x))]), [REF.NULL_instr(($type(z, x) : deftype <: heaptype))]) + `%~>%`(`%;%`_config(z, [REF.NULL_instr(_HT_heaptype(?(), _IDX_typeuse(x)))]), [REF.NULL_instr(_HT_heaptype(?(), ($type(z, x) : deftype <: typeuse)))]) ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec rule ref.func{z : state, x : idx}: @@ -7599,7 +7595,7 @@ grammar Bheaptype : heaptype ;; ../../../../specification/wasm-latest/5.2-binary.types.spectec prod{ht : heaptype} ht:Babsheaptype => ht ;; ../../../../specification/wasm-latest/5.2-binary.types.spectec - prod{x33 : s33} x33:Bs33 => _IDX_heaptype($s33_to_u32(x33)) + prod{x33 : s33} x33:Bs33 => _HT_heaptype(?(), _IDX_typeuse($s33_to_u32(x33))) -- if (x33!`%`_s33.0 >= (0 : nat <:> int)) ;; ../../../../specification/wasm-latest/5.2-binary.types.spectec @@ -9633,7 +9629,7 @@ grammar Theaptype_(I : I) : heaptype ;; ../../../../specification/wasm-latest/6.2-text.types.spectec prod{ht : heaptype} ht:Tabsheaptype => ht ;; ../../../../specification/wasm-latest/6.2-text.types.spectec - prod{x : idx} x:Ttypeidx_(I) => _IDX_heaptype(x) + prod{x : idx} x:Ttypeidx_(I) => _HT_heaptype(?(), _IDX_typeuse(x)) ;; ../../../../specification/wasm-latest/6.2-text.types.spectec grammar Tnull : null From c3b35c63962ef8d029782a525b35459d07389d70 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 14 Jul 2026 03:18:45 -0700 Subject: [PATCH 6/9] update tests --- spectec/test-frontend/TEST.md | 470 ++++++++++++++++++---------------- 1 file changed, 249 insertions(+), 221 deletions(-) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 3f47dc1b8..24fe9b19c 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -2174,6 +2174,8 @@ syntax instr = | I31.GET{sx : sx}(sx : sx) | STRUCT.NEW{typeidx : typeidx}(typeidx : typeidx) | STRUCT.NEW_DEFAULT{typeidx : typeidx}(typeidx : typeidx) + | STRUCT.NEW_DESC{typeidx : typeidx}(typeidx : typeidx) + | STRUCT.NEW_DEFAULT_DESC{typeidx : typeidx}(typeidx : typeidx) | STRUCT.GET{`sx?` : sx?, typeidx : typeidx, u32 : u32}(sx?{sx <- `sx?`} : sx?, typeidx : typeidx, u32 : u32) | STRUCT.SET{typeidx : typeidx, u32 : u32}(typeidx : typeidx, u32 : u32) | ARRAY.NEW{typeidx : typeidx}(typeidx : typeidx) @@ -2264,227 +2266,227 @@ def $free_blocktype(blocktype : blocktype) : free ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec rec { -;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:572.1-572.44 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:574.1-574.44 def $shift_labelidxs(labelidx*) : labelidx* - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:573.1-573.32 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:575.1-575.32 def $shift_labelidxs([]) = [] - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:574.1-574.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:576.1-576.66 def $shift_labelidxs{`labelidx'*` : labelidx*}([`%`_labelidx(0)] ++ labelidx'*{labelidx' <- `labelidx'*`}) = $shift_labelidxs(labelidx'*{labelidx' <- `labelidx'*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:575.1-575.91 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:577.1-577.91 def $shift_labelidxs{labelidx : labelidx, `labelidx'*` : labelidx*}([labelidx] ++ labelidx'*{labelidx' <- `labelidx'*`}) = [`%`_labelidx((((labelidx!`%`_labelidx.0 : nat <:> int) - (1 : nat <:> int)) : int <:> nat))] ++ $shift_labelidxs(labelidx'*{labelidx' <- `labelidx'*`}) } ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec rec { -;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:417.1-417.30 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:419.1-419.30 def $free_instr(instr : instr) : free - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:428.1-428.26 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:430.1-430.26 def $free_instr(NOP_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:429.1-429.34 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:431.1-431.34 def $free_instr(UNREACHABLE_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:430.1-430.27 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:432.1-432.27 def $free_instr(DROP_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:431.1-431.86 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:433.1-433.86 def $free_instr{`valtype*?` : valtype*?}(SELECT_instr(valtype*{valtype <- `valtype*`}?{`valtype*` <- `valtype*?`})) = $free_opt($free_list($free_valtype(valtype)*{valtype <- `valtype*`})?{`valtype*` <- `valtype*?`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:433.1-433.92 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:435.1-435.92 def $free_instr{blocktype : blocktype, `instr*` : instr*}(BLOCK_instr(blocktype, instr*{instr <- `instr*`})) = $free_blocktype(blocktype) +++ $free_block(instr*{instr <- `instr*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:434.1-434.91 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:436.1-436.91 def $free_instr{blocktype : blocktype, `instr*` : instr*}(LOOP_instr(blocktype, instr*{instr <- `instr*`})) = $free_blocktype(blocktype) +++ $free_block(instr*{instr <- `instr*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:435.1-436.79 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:437.1-438.79 def $free_instr{blocktype : blocktype, `instr_1*` : instr*, `instr_2*` : instr*}(`IF%%ELSE%`_instr(blocktype, instr_1*{instr_1 <- `instr_1*`}, instr_2*{instr_2 <- `instr_2*`})) = $free_blocktype(blocktype) +++ $free_block(instr_1*{instr_1 <- `instr_1*`}) +++ $free_block(instr_2*{instr_2 <- `instr_2*`}) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:438.1-438.56 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:440.1-440.56 def $free_instr{labelidx : labelidx}(BR_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:439.1-439.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:441.1-441.59 def $free_instr{labelidx : labelidx}(BR_IF_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:440.1-441.69 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:442.1-443.69 def $free_instr{`labelidx*` : labelidx*, labelidx' : labelidx}(BR_TABLE_instr(labelidx*{labelidx <- `labelidx*`}, labelidx')) = $free_list($free_labelidx(labelidx)*{labelidx <- `labelidx*`}) +++ $free_labelidx(labelidx') - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:442.1-442.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:444.1-444.64 def $free_instr{labelidx : labelidx}(BR_ON_NULL_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:443.1-443.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:445.1-445.68 def $free_instr{labelidx : labelidx}(BR_ON_NON_NULL_instr(labelidx)) = $free_labelidx(labelidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:444.1-445.83 - def $free_instr{labelidx : labelidx, reftype_1 : reftype, reftype_2 : reftype}(BR_ON_CAST_instr(labelidx, reftype_1, reftype_2)) = $free_labelidx(labelidx) +++ $free_reftype(reftype_1) +++ $free_reftype(reftype_2) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:446.1-447.83 + def $free_instr{labelidx : labelidx, reftype_1 : reftype, reftype_2 : reftype}(BR_ON_CAST_instr(labelidx, reftype_1, reftype_2)) = $free_labelidx(labelidx) +++ $free_reftype(reftype_1) +++ $free_reftype(reftype_2) + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:448.1-449.83 def $free_instr{labelidx : labelidx, reftype_1 : reftype, reftype_2 : reftype}(BR_ON_CAST_FAIL_instr(labelidx, reftype_1, reftype_2)) = $free_labelidx(labelidx) +++ $free_reftype(reftype_1) +++ $free_reftype(reftype_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:449.1-449.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:451.1-451.55 def $free_instr{funcidx : funcidx}(CALL_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:450.1-450.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:452.1-452.59 def $free_instr{typeuse : typeuse}(CALL_REF_instr(typeuse)) = $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:451.1-452.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:453.1-454.53 def $free_instr{tableidx : tableidx, typeuse : typeuse}(CALL_INDIRECT_instr(tableidx, typeuse)) = $free_tableidx(tableidx) +++ $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:453.1-453.29 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:455.1-455.29 def $free_instr(RETURN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:454.1-454.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:456.1-456.62 def $free_instr{funcidx : funcidx}(RETURN_CALL_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:455.1-455.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:457.1-457.66 def $free_instr{typeuse : typeuse}(RETURN_CALL_REF_instr(typeuse)) = $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:456.1-457.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:458.1-459.53 def $free_instr{tableidx : tableidx, typeuse : typeuse}(RETURN_CALL_INDIRECT_instr(tableidx, typeuse)) = $free_tableidx(tableidx) +++ $free_typeuse(typeuse) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:459.1-459.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:461.1-461.63 def $free_instr{numtype : numtype, numlit : num_(numtype)}(CONST_instr(numtype, numlit)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:460.1-460.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:462.1-462.60 def $free_instr{numtype : numtype, unop : unop_(numtype)}(UNOP_instr(numtype, unop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:461.1-461.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:463.1-463.62 def $free_instr{numtype : numtype, binop : binop_(numtype)}(BINOP_instr(numtype, binop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:462.1-462.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:464.1-464.64 def $free_instr{numtype : numtype, testop : testop_(numtype)}(TESTOP_instr(numtype, testop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:463.1-463.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:465.1-465.62 def $free_instr{numtype : numtype, relop : relop_(numtype)}(RELOP_instr(numtype, relop)) = $free_numtype(numtype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:464.1-465.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:466.1-467.55 def $free_instr{numtype_1 : numtype, numtype_2 : numtype, cvtop : cvtop__(numtype_2, numtype_1)}(CVTOP_instr(numtype_1, numtype_2, cvtop)) = $free_numtype(numtype_1) +++ $free_numtype(numtype_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:467.1-467.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:469.1-469.64 def $free_instr{vectype : vectype, veclit : vec_(vectype)}(VCONST_instr(vectype, veclit)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:468.1-468.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:470.1-470.64 def $free_instr{vectype : vectype, vvunop : vvunop}(VVUNOP_instr(vectype, vvunop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:469.1-469.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:471.1-471.66 def $free_instr{vectype : vectype, vvbinop : vvbinop}(VVBINOP_instr(vectype, vvbinop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:470.1-470.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:472.1-472.68 def $free_instr{vectype : vectype, vvternop : vvternop}(VVTERNOP_instr(vectype, vvternop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:471.1-471.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:473.1-473.68 def $free_instr{vectype : vectype, vvtestop : vvtestop}(VVTESTOP_instr(vectype, vvtestop)) = $free_vectype(vectype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:472.1-472.56 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:474.1-474.56 def $free_instr{shape : shape, vunop : vunop_(shape)}(VUNOP_instr(shape, vunop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:473.1-473.58 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:475.1-475.58 def $free_instr{shape : shape, vbinop : vbinop_(shape)}(VBINOP_instr(shape, vbinop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:474.1-474.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:476.1-476.60 def $free_instr{shape : shape, vternop : vternop_(shape)}(VTERNOP_instr(shape, vternop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:475.1-475.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:477.1-477.60 def $free_instr{shape : shape, vtestop : vtestop_(shape)}(VTESTOP_instr(shape, vtestop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:476.1-476.58 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:478.1-478.58 def $free_instr{shape : shape, vrelop : vrelop_(shape)}(VRELOP_instr(shape, vrelop)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:477.1-477.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:479.1-479.64 def $free_instr{ishape : ishape, vshiftop : vshiftop_(ishape)}(VSHIFTOP_instr(ishape, vshiftop)) = $free_shape(ishape!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:478.1-478.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:480.1-480.55 def $free_instr{ishape : ishape}(VBITMASK_instr(ishape)) = $free_shape(ishape!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:479.1-479.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:481.1-481.66 def $free_instr{bshape : bshape, vswizzlop : vswizzlop_(bshape)}(VSWIZZLOP_instr(bshape, vswizzlop)) = $free_shape(bshape!`%`_bshape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:480.1-480.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:482.1-482.64 def $free_instr{bshape : bshape, `laneidx*` : laneidx*}(VSHUFFLE_instr(bshape, laneidx*{laneidx <- `laneidx*`})) = $free_shape(bshape!`%`_bshape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:481.1-482.49 - def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextunop : vextunop__(ishape_2, ishape_1)}(VEXTUNOP_instr(ishape_1, ishape_2, vextunop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:483.1-484.49 - def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextbinop : vextbinop__(ishape_2, ishape_1)}(VEXTBINOP_instr(ishape_1, ishape_2, vextbinop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) + def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextunop : vextunop__(ishape_2, ishape_1)}(VEXTUNOP_instr(ishape_1, ishape_2, vextunop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:485.1-486.49 - def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextternop : vextternop__(ishape_2, ishape_1)}(VEXTTERNOP_instr(ishape_1, ishape_2, vextternop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) + def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextbinop : vextbinop__(ishape_2, ishape_1)}(VEXTBINOP_instr(ishape_1, ishape_2, vextbinop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:487.1-488.49 + def $free_instr{ishape_1 : ishape, ishape_2 : ishape, vextternop : vextternop__(ishape_2, ishape_1)}(VEXTTERNOP_instr(ishape_1, ishape_2, vextternop)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:489.1-490.49 def $free_instr{ishape_1 : ishape, ishape_2 : ishape, sx : sx}(VNARROW_instr(ishape_1, ishape_2, sx)) = $free_shape(ishape_1!`%`_ishape.0) +++ $free_shape(ishape_2!`%`_ishape.0) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:489.1-490.47 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:491.1-492.47 def $free_instr{shape_1 : shape, shape_2 : shape, vcvtop : vcvtop__(shape_2, shape_1)}(VCVTOP_instr(shape_1, shape_2, vcvtop)) = $free_shape(shape_1) +++ $free_shape(shape_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:491.1-491.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:493.1-493.51 def $free_instr{shape : shape}(VSPLAT_instr(shape)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:492.1-492.70 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:494.1-494.70 def $free_instr{shape : shape, `sx?` : sx?, laneidx : laneidx}(VEXTRACT_LANE_instr(shape, sx?{sx <- `sx?`}, laneidx)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:493.1-493.66 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:495.1-495.66 def $free_instr{shape : shape, laneidx : laneidx}(VREPLACE_LANE_instr(shape, laneidx)) = $free_shape(shape) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:495.1-495.62 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:497.1-497.62 def $free_instr{heaptype : heaptype}(REF.NULL_instr(heaptype)) = $free_heaptype(heaptype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:496.1-496.34 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:498.1-498.34 def $free_instr(REF.IS_NULL_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:497.1-497.38 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:499.1-499.38 def $free_instr(REF.AS_NON_NULL_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:498.1-498.29 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:500.1-500.29 def $free_instr(REF.EQ_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:499.1-499.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:501.1-501.59 def $free_instr{reftype : reftype}(REF.TEST_instr(reftype)) = $free_reftype(reftype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:500.1-500.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:502.1-502.59 def $free_instr{reftype : reftype}(REF.CAST_instr(reftype)) = $free_reftype(reftype) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:501.1-501.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:503.1-503.59 def $free_instr{funcidx : funcidx}(REF.FUNC_instr(funcidx)) = $free_funcidx(funcidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:502.1-502.30 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:504.1-504.30 def $free_instr(REF.I31_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:504.1-504.33 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:506.1-506.33 def $free_instr{sx : sx}(I31.GET_instr(sx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:506.1-506.41 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:508.1-508.41 def $free_instr{typeidx : typeidx}(STRUCT.NEW_instr(typeidx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:507.1-507.69 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:509.1-509.69 def $free_instr{typeidx : typeidx}(STRUCT.NEW_DEFAULT_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:508.1-508.69 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:510.1-510.69 def $free_instr{`sx?` : sx?, typeidx : typeidx, u32 : u32}(STRUCT.GET_instr(sx?{sx <- `sx?`}, typeidx, u32)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:509.1-509.65 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:511.1-511.65 def $free_instr{typeidx : typeidx, u32 : u32}(STRUCT.SET_instr(typeidx, u32)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:511.1-511.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:513.1-513.60 def $free_instr{typeidx : typeidx}(ARRAY.NEW_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:512.1-512.68 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:514.1-514.68 def $free_instr{typeidx : typeidx}(ARRAY.NEW_DEFAULT_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:513.1-513.70 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:515.1-515.70 def $free_instr{typeidx : typeidx, u32 : u32}(ARRAY.NEW_FIXED_instr(typeidx, u32)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:514.1-515.51 - def $free_instr{typeidx : typeidx, dataidx : dataidx}(ARRAY.NEW_DATA_instr(typeidx, dataidx)) = $free_typeidx(typeidx) +++ $free_dataidx(dataidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:516.1-517.51 + def $free_instr{typeidx : typeidx, dataidx : dataidx}(ARRAY.NEW_DATA_instr(typeidx, dataidx)) = $free_typeidx(typeidx) +++ $free_dataidx(dataidx) + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-519.51 def $free_instr{typeidx : typeidx, elemidx : elemidx}(ARRAY.NEW_ELEM_instr(typeidx, elemidx)) = $free_typeidx(typeidx) +++ $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:520.1-520.64 def $free_instr{`sx?` : sx?, typeidx : typeidx}(ARRAY.GET_instr(sx?{sx <- `sx?`}, typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:519.1-519.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:521.1-521.60 def $free_instr{typeidx : typeidx}(ARRAY.SET_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:520.1-520.32 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:522.1-522.32 def $free_instr(ARRAY.LEN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:521.1-521.61 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:523.1-523.61 def $free_instr{typeidx : typeidx}(ARRAY.FILL_instr(typeidx)) = $free_typeidx(typeidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:522.1-523.55 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:524.1-525.55 def $free_instr{typeidx_1 : typeidx, typeidx_2 : typeidx}(ARRAY.COPY_instr(typeidx_1, typeidx_2)) = $free_typeidx(typeidx_1) +++ $free_typeidx(typeidx_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:524.1-525.51 - def $free_instr{typeidx : typeidx, dataidx : dataidx}(ARRAY.INIT_DATA_instr(typeidx, dataidx)) = $free_typeidx(typeidx) +++ $free_dataidx(dataidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:526.1-527.51 + def $free_instr{typeidx : typeidx, dataidx : dataidx}(ARRAY.INIT_DATA_instr(typeidx, dataidx)) = $free_typeidx(typeidx) +++ $free_dataidx(dataidx) + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:528.1-529.51 def $free_instr{typeidx : typeidx, elemidx : elemidx}(ARRAY.INIT_ELEM_instr(typeidx, elemidx)) = $free_typeidx(typeidx) +++ $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:529.1-529.41 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:531.1-531.41 def $free_instr(EXTERN.CONVERT_ANY_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:530.1-530.41 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:532.1-532.41 def $free_instr(ANY.CONVERT_EXTERN_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS []} - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:532.1-532.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:534.1-534.63 def $free_instr{localidx : localidx}(LOCAL.GET_instr(localidx)) = $free_localidx(localidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:533.1-533.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:535.1-535.63 def $free_instr{localidx : localidx}(LOCAL.SET_instr(localidx)) = $free_localidx(localidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:534.1-534.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:536.1-536.63 def $free_instr{localidx : localidx}(LOCAL.TEE_instr(localidx)) = $free_localidx(localidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:536.1-536.67 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:538.1-538.67 def $free_instr{globalidx : globalidx}(GLOBAL.GET_instr(globalidx)) = $free_globalidx(globalidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:537.1-537.67 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:539.1-539.67 def $free_instr{globalidx : globalidx}(GLOBAL.SET_instr(globalidx)) = $free_globalidx(globalidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:539.1-539.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:541.1-541.63 def $free_instr{tableidx : tableidx}(TABLE.GET_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:540.1-540.63 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:542.1-542.63 def $free_instr{tableidx : tableidx}(TABLE.SET_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:541.1-541.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:543.1-543.64 def $free_instr{tableidx : tableidx}(TABLE.SIZE_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:542.1-542.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:544.1-544.64 def $free_instr{tableidx : tableidx}(TABLE.GROW_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:543.1-543.64 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:545.1-545.64 def $free_instr{tableidx : tableidx}(TABLE.FILL_instr(tableidx)) = $free_tableidx(tableidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:544.1-545.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:546.1-547.59 def $free_instr{tableidx_1 : tableidx, tableidx_2 : tableidx}(TABLE.COPY_instr(tableidx_1, tableidx_2)) = $free_tableidx(tableidx_1) +++ $free_tableidx(tableidx_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:546.1-547.53 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:548.1-549.53 def $free_instr{tableidx : tableidx, elemidx : elemidx}(TABLE.INIT_instr(tableidx, elemidx)) = $free_tableidx(tableidx) +++ $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:548.1-548.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:550.1-550.60 def $free_instr{elemidx : elemidx}(ELEM.DROP_instr(elemidx)) = $free_elemidx(elemidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:550.1-551.49 - def $free_instr{numtype : numtype, `loadop?` : loadop_(numtype)?, memidx : memidx, memarg : memarg}(LOAD_instr(numtype, loadop?{loadop <- `loadop?`}, memidx, memarg)) = $free_numtype(numtype) +++ $free_memidx(memidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:552.1-553.49 - def $free_instr{numtype : numtype, `storeop?` : storeop_(numtype)?, memidx : memidx, memarg : memarg}(STORE_instr(numtype, storeop?{storeop <- `storeop?`}, memidx, memarg)) = $free_numtype(numtype) +++ $free_memidx(memidx) + def $free_instr{numtype : numtype, `loadop?` : loadop_(numtype)?, memidx : memidx, memarg : memarg}(LOAD_instr(numtype, loadop?{loadop <- `loadop?`}, memidx, memarg)) = $free_numtype(numtype) +++ $free_memidx(memidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:554.1-555.49 - def $free_instr{vectype : vectype, `vloadop?` : vloadop_(vectype)?, memidx : memidx, memarg : memarg}(VLOAD_instr(vectype, vloadop?{vloadop <- `vloadop?`}, memidx, memarg)) = $free_vectype(vectype) +++ $free_memidx(memidx) + def $free_instr{numtype : numtype, `storeop?` : storeop_(numtype)?, memidx : memidx, memarg : memarg}(STORE_instr(numtype, storeop?{storeop <- `storeop?`}, memidx, memarg)) = $free_numtype(numtype) +++ $free_memidx(memidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:556.1-557.49 - def $free_instr{vectype : vectype, sz : sz, memidx : memidx, memarg : memarg, laneidx : laneidx}(VLOAD_LANE_instr(vectype, sz, memidx, memarg, laneidx)) = $free_vectype(vectype) +++ $free_memidx(memidx) + def $free_instr{vectype : vectype, `vloadop?` : vloadop_(vectype)?, memidx : memidx, memarg : memarg}(VLOAD_instr(vectype, vloadop?{vloadop <- `vloadop?`}, memidx, memarg)) = $free_vectype(vectype) +++ $free_memidx(memidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:558.1-559.49 - def $free_instr{vectype : vectype, memidx : memidx, memarg : memarg}(VSTORE_instr(vectype, memidx, memarg)) = $free_vectype(vectype) +++ $free_memidx(memidx) + def $free_instr{vectype : vectype, sz : sz, memidx : memidx, memarg : memarg, laneidx : laneidx}(VLOAD_LANE_instr(vectype, sz, memidx, memarg, laneidx)) = $free_vectype(vectype) +++ $free_memidx(memidx) ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:560.1-561.49 + def $free_instr{vectype : vectype, memidx : memidx, memarg : memarg}(VSTORE_instr(vectype, memidx, memarg)) = $free_vectype(vectype) +++ $free_memidx(memidx) + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:562.1-563.49 def $free_instr{vectype : vectype, sz : sz, memidx : memidx, memarg : memarg, laneidx : laneidx}(VSTORE_LANE_instr(vectype, sz, memidx, memarg, laneidx)) = $free_vectype(vectype) +++ $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:562.1-562.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:564.1-564.59 def $free_instr{memidx : memidx}(MEMORY.SIZE_instr(memidx)) = $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:563.1-563.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:565.1-565.59 def $free_instr{memidx : memidx}(MEMORY.GROW_instr(memidx)) = $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:564.1-564.59 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:566.1-566.59 def $free_instr{memidx : memidx}(MEMORY.FILL_instr(memidx)) = $free_memidx(memidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:565.1-566.51 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:567.1-568.51 def $free_instr{memidx_1 : memidx, memidx_2 : memidx}(MEMORY.COPY_instr(memidx_1, memidx_2)) = $free_memidx(memidx_1) +++ $free_memidx(memidx_2) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:567.1-568.49 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:569.1-570.49 def $free_instr{memidx : memidx, dataidx : dataidx}(MEMORY.INIT_instr(memidx, dataidx)) = $free_memidx(memidx) +++ $free_dataidx(dataidx) - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:569.1-569.60 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:571.1-571.60 def $free_instr{dataidx : dataidx}(DATA.DROP_instr(dataidx)) = $free_dataidx(dataidx) -;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:418.1-418.31 +;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:420.1-420.31 def $free_block(instr*) : free - ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:577.1-578.47 + ;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:579.1-580.47 def $free_block{`instr*` : instr*, free : free}(instr*{instr <- `instr*`}) = free[LABELS_free = $shift_labelidxs(free.LABELS_free)] -- if (free = $free_list($free_instr(instr)*{instr <- `instr*`})) } @@ -2845,17 +2847,17 @@ relation Valtype_ok: `%|-%:OK`(context, valtype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:12.1-12.94 relation Typeuse_ok: `%|-%:OK`(context, typeuse) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:101.1-103.30 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:106.1-108.30 rule typeidx{C : context, typeidx : typeidx, dt : deftype}: `%|-%:OK`(C, _IDX_typeuse(typeidx)) -- if (C.TYPES_context[typeidx!`%`_typeidx.0] = dt) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:105.1-107.23 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:110.1-112.23 rule rec{C : context, i : n, st : subtype}: `%|-%:OK`(C, REC_typeuse(i)) -- if (C.RECS_context[i] = st) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:109.1-111.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:114.1-116.35 rule deftype{C : context, deftype : deftype}: `%|-%:OK`(C, (deftype : deftype <: typeuse)) -- Deftype_ok: `%|-%:OK`(C, deftype) @@ -2867,55 +2869,55 @@ relation Resulttype_ok: `%|-%:OK`(context, resulttype) `%|-%:OK`(C, `%`_resulttype(t*{t <- `t*`})) -- (Valtype_ok: `%|-%:OK`(C, t))*{t <- `t*`} -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:85.1-85.104 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:90.1-90.104 relation Fieldtype_ok: `%|-%:OK`(context, fieldtype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:125.1-127.43 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:130.1-132.43 rule _{C : context, storagetype : storagetype}: `%|-%:OK`(C, `%%`_fieldtype(MUT_mut?{}, storagetype)) -- Storagetype_ok: `%|-%:OK`(C, storagetype) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:86.1-86.106 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:91.1-91.106 relation Storagetype_ok: `%|-%:OK`(context, storagetype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:117.1-119.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:122.1-124.35 rule val{C : context, valtype : valtype}: `%|-%:OK`(C, (valtype : valtype <: storagetype)) -- Valtype_ok: `%|-%:OK`(C, valtype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:121.1-123.37 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:126.1-128.37 rule pack{C : context, packtype : packtype}: `%|-%:OK`(C, (packtype : packtype <: storagetype)) -- Packtype_ok: `%|-%:OK`(C, packtype) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:87.1-87.103 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:92.1-92.103 relation Comptype_ok: `%|-%:OK`(context, comptype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:130.1-132.42 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:135.1-137.42 rule struct{C : context, `fieldtype*` : fieldtype*}: `%|-%:OK`(C, STRUCT_comptype(`%`_list(fieldtype*{fieldtype <- `fieldtype*`}))) -- (Fieldtype_ok: `%|-%:OK`(C, fieldtype))*{fieldtype <- `fieldtype*`} - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:134.1-136.39 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:139.1-141.39 rule array{C : context, fieldtype : fieldtype}: `%|-%:OK`(C, ARRAY_comptype(fieldtype)) -- Fieldtype_ok: `%|-%:OK`(C, fieldtype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:138.1-141.35 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:143.1-146.35 rule func{C : context, `t_1*` : valtype*, `t_2*` : valtype*}: `%|-%:OK`(C, `FUNC%->%`_comptype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_1*{t_1 <- `t_1*`})) -- Resulttype_ok: `%|-%:OK`(C, `%`_resulttype(t_2*{t_2 <- `t_2*`})) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:88.1-88.103 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:93.1-93.103 relation Desctype_ok: `%|-%:OK`(context, desctype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:144.1-148.31 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:149.1-153.31 rule _{C : context, `tu_1?` : typeuse?, `tu_2?` : typeuse?, ct : comptype}: `%|-%:OK`(C, `%%%`_desctype(DESCRIBES_describestype(tu_1)?{tu_1 <- `tu_1?`}, DESCRIPTOR_descriptortype(tu_2)?{tu_2 <- `tu_2?`}, ct)) -- (Typeuse_ok: `%|-%:OK`(C, tu_1))?{tu_1 <- `tu_1?`} -- (Typeuse_ok: `%|-%:OK`(C, tu_2))?{tu_2 <- `tu_2?`} -- Comptype_ok: `%|-%:OK`(C, ct) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:89.1-89.126 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:94.1-94.126 relation Subtype_ok: `%|-%:%`(context, subtype, oktypeidx) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:151.1-158.49 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:156.1-163.49 rule _{C : context, `x*` : idx*, desctype : desctype, x_0 : idx, `x'**` : idx**, `desctype'*` : desctype*}: `%|-%:%`(C, SUB_subtype(FINAL_final?{}, _IDX_typeuse(x)*{x <- `x*`}, desctype), OK_oktypeidx(x_0)) -- if (|x*{x <- `x*`}| <= 1) @@ -2924,26 +2926,26 @@ relation Subtype_ok: `%|-%:%`(context, subtype, oktypeidx) -- Desctype_ok: `%|-%:OK`(C, desctype) -- (Desctype_sub: `%|-%<:%`(C, desctype, desctype'))*{desctype' <- `desctype'*`} -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:90.1-90.126 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:95.1-95.126 relation Rectype_ok: `%|-%:%`(context, rectype, oktypeidx) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:180.1-181.23 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:185.1-186.23 rule empty{C : context, x : idx}: `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidx(x)) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:183.1-186.48 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:188.1-191.48 rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx}: `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidx(x)) -- Subtype_ok: `%|-%:%`(C, subtype_1, OK_oktypeidx(x)) -- Rectype_ok: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidx(`%`_typeidx((x!`%`_idx.0 + 1)))) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:188.1-190.60 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:193.1-195.60 rule _rec2{C : context, `subtype*` : subtype*, x : idx}: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidx(x)) -- Rectype_ok2: `%|-%:%`({TYPES [], RECS subtype*{subtype <- `subtype*`}, TAGS [], GLOBALS [], MEMS [], TABLES [], FUNCS [], DATAS [], ELEMS [], LOCALS [], LABELS [], RETURN ?(), REFS []} +++ C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, 0)) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:91.1-91.126 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.126 relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:170.1-177.49 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:175.1-182.49 rule _{C : context, `typeuse*` : typeuse*, desctype : desctype, x : idx, i : nat, `typeuse'**` : typeuse**, `desctype'*` : desctype*}: `%|-%:%`(C, SUB_subtype(FINAL_final?{}, typeuse*{typeuse <- `typeuse*`}, desctype), OK_oktypeidxnat(x, i)) -- if (|typeuse*{typeuse <- `typeuse*`}| <= 1) @@ -2952,28 +2954,28 @@ relation Subtype_ok2: `%|-%:%`(context, subtype, oktypeidxnat) -- Desctype_ok: `%|-%:OK`(C, desctype) -- (Desctype_sub: `%|-%<:%`(C, desctype, desctype'))*{desctype' <- `desctype'*`} -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:92.1-92.126 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.126 relation Rectype_ok2: `%|-%:%`(context, rectype, oktypeidxnat) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:192.1-193.24 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:197.1-198.24 rule empty{C : context, x : idx, i : nat}: `%|-%:%`(C, REC_rectype(`%`_list([])), OK_oktypeidxnat(x, i)) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:195.1-198.55 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:200.1-203.55 rule cons{C : context, subtype_1 : subtype, `subtype*` : subtype*, x : idx, i : nat}: `%|-%:%`(C, REC_rectype(`%`_list([subtype_1] ++ subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(x, i)) -- Subtype_ok2: `%|-%:%`(C, subtype_1, OK_oktypeidxnat(x, i)) -- Rectype_ok2: `%|-%:%`(C, REC_rectype(`%`_list(subtype*{subtype <- `subtype*`})), OK_oktypeidxnat(`%`_typeidx((x!`%`_idx.0 + 1)), (i + 1))) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:93.1-93.102 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:98.1-98.102 relation Deftype_ok: `%|-%:OK`(context, deftype) - ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:201.1-205.14 + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:206.1-210.14 rule _{C : context, rectype : rectype, i : n, x : idx, `subtype*` : subtype*, n : n}: `%|-%:OK`(C, _DEF_deftype(rectype, i)) -- Rectype_ok: `%|-%:%`(C, rectype, OK_oktypeidx(x)) -- if (rectype = REC_rectype(`%`_list(subtype^n{subtype <- `subtype*`}))) -- if (i < n) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:96.1-96.108 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:101.1-101.108 relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:170.1-172.41 rule struct{C : context, `ft_1*` : fieldtype*, `ft'_1*` : fieldtype*, `ft_2*` : fieldtype*}: @@ -2991,7 +2993,7 @@ relation Comptype_sub: `%|-%<:%`(context, comptype, comptype) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_21*{t_21 <- `t_21*`}), `%`_resulttype(t_11*{t_11 <- `t_11*`})) -- Resulttype_sub: `%|-%<:%`(C, `%`_resulttype(t_12*{t_12 <- `t_12*`}), `%`_resulttype(t_22*{t_22 <- `t_22*`})) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:97.1-97.108 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:102.1-102.108 relation Desctype_sub: `%|-%<:%`(context, desctype, desctype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:184.1-188.37 rule _{C : context, tu_11 : typeuse, tu_12 : typeuse, ct_1 : comptype, tu_21 : typeuse, tu_22 : typeuse, ct_2 : comptype}: @@ -3000,7 +3002,7 @@ relation Desctype_sub: `%|-%<:%`(context, desctype, desctype) -- Heaptype_sub: `%|-%<:%`(C, _HT_heaptype(?(), tu_12), _HT_heaptype(?(), tu_22)) -- Comptype_sub: `%|-%<:%`(C, ct_1, ct_2) -;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:98.1-98.107 +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec:103.1-103.107 relation Deftype_sub: `%|-%<:%`(context, deftype, deftype) ;; ../../../../specification/wasm-latest/2.2-validation.subtyping.spectec:191.1-193.66 rule refl{C : context, deftype_1 : deftype, deftype_2 : deftype}: @@ -3193,6 +3195,13 @@ relation Expand_use: `%~~_%%`(typeuse, context, comptype) `%~~_%%`(_IDX_typeuse(typeidx), C, comptype) -- Expand: `%~~%`(C.TYPES_context[typeidx!`%`_typeidx.0], comptype) +;; ../../../../specification/wasm-latest/2.1-validation.types.spectec +relation ExpandDesc: `%~~%`(deftype, desctype) + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec + rule _{deftype : deftype, desctype : desctype}: + `%~~%`(deftype, desctype) + -- if ($expanddt_to_desctype(deftype) = desctype) + ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec relation Limits_ok: `%|-%:%`(context, limits, nat) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec @@ -3630,414 +3639,425 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) rule i31.get{C : context, sx : sx}: `%|-%:%`(C, I31.GET_instr(sx), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), I31_heaptype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:252.1-254.45 - rule struct.new{C : context, x : idx, `zt*` : storagetype*, `mut?*` : mut?*}: + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:252.1-254.68 + rule struct.new{C : context, x : idx, `zt*` : storagetype*, `describestype?` : describestype?, `mut?*` : mut?*}: `%|-%:%`(C, STRUCT.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)*{zt <- `zt*`}), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) - -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) + -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:256.1-259.48 - rule struct.new_default{C : context, x : idx, `mut?*` : mut?*, `zt*` : storagetype*}: + rule struct.new_default{C : context, x : idx, `describestype?` : describestype?, `mut?*` : mut?*, `zt*` : storagetype*}: `%|-%:%`(C, STRUCT.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) - -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`}))) + -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:264.1-268.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:261.1-263.88 + rule struct.new_desc{C : context, x : idx, `zt*` : storagetype*, y : idx, `describestype?` : describestype?, `mut?*` : mut?*}: + `%|-%:%`(C, STRUCT.NEW_DESC_instr(x), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)*{zt <- `zt*`} ++ [REF_valtype(?(NULL_null), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(y)))]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(x)))]))) + -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) + + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:265.1-268.48 + rule struct.new_default_desc{C : context, x : idx, y : idx, `describestype?` : describestype?, `mut?*` : mut?*, `zt*` : storagetype*}: + `%|-%:%`(C, STRUCT.NEW_DEFAULT_DESC_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(y)))]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(x)))]))) + -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) + -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} + + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:273.1-277.41 rule struct.get{C : context, `sx?` : sx?, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*, `mut?` : mut?}: `%|-%:%`(C, STRUCT.GET_instr(sx?{sx <- `sx?`}, x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x)))]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(mut?{mut <- `mut?`}, zt)) -- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:270.1-273.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:279.1-282.24 rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}: `%|-%:%`(C, STRUCT.SET_instr(x, i), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) $unpack(zt)]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`}))) -- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(?(MUT_mut), zt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:278.1-280.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:287.1-289.43 rule array.new{C : context, x : idx, zt : storagetype, `mut?` : mut?}: `%|-%:%`(C, ARRAY.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype([$unpack(zt) I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:282.1-285.45 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:291.1-294.45 rule array.new_default{C : context, x : idx, `mut?` : mut?, zt : storagetype}: `%|-%:%`(C, ARRAY.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- Defaultable: `|-%DEFAULTABLE`($unpack(zt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:287.1-289.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:296.1-298.43 rule array.new_fixed{C : context, x : idx, n : n, zt : storagetype, `mut?` : mut?}: `%|-%:%`(C, ARRAY.NEW_FIXED_instr(x, `%`_u32(n)), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)^n{}), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:291.1-294.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:300.1-303.40 rule array.new_elem{C : context, x : idx, y : idx, `mut?` : mut?, rt : reftype}: `%|-%:%`(C, ARRAY.NEW_ELEM_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, (rt : reftype <: storagetype)))) -- Reftype_sub: `%|-%<:%`(C, C.ELEMS_context[y!`%`_idx.0], rt) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:296.1-300.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:305.1-309.24 rule array.new_data{C : context, x : idx, y : idx, `mut?` : mut?, zt : storagetype, numtype : numtype, vectype : vectype}: `%|-%:%`(C, ARRAY.NEW_DATA_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([I32_valtype I32_valtype]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if (($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype))) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:302.1-305.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:311.1-314.39 rule array.get{C : context, `sx?` : sx?, x : idx, zt : storagetype, `mut?` : mut?}: `%|-%:%`(C, ARRAY.GET_instr(sx?{sx <- `sx?`}, x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype]), [], `%`_resulttype([$unpack(zt)]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((sx?{sx <- `sx?`} = ?()) <=> $is_packtype(zt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:307.1-309.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:316.1-318.42 rule array.set{C : context, x : idx, zt : storagetype}: `%|-%:%`(C, ARRAY.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype $unpack(zt)]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:311.1-312.43 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:320.1-321.43 rule array.len{C : context}: `%|-%:%`(C, ARRAY.LEN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), ARRAY_heaptype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:314.1-316.42 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:323.1-325.42 rule array.fill{C : context, x : idx, zt : storagetype}: `%|-%:%`(C, ARRAY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype $unpack(zt) I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:318.1-322.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:327.1-331.40 rule array.copy{C : context, x_1 : idx, x_2 : idx, zt_1 : storagetype, `mut?` : mut?, zt_2 : storagetype}: `%|-%:%`(C, ARRAY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x_1))) I32_valtype REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x_2))) I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x_1!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt_1))) -- Expand: `%~~%`(C.TYPES_context[x_2!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt_2))) -- Storagetype_sub: `%|-%<:%`(C, zt_2, zt_1) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:324.1-327.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:333.1-336.44 rule array.init_elem{C : context, x : idx, y : idx, zt : storagetype}: `%|-%:%`(C, ARRAY.INIT_ELEM_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) -- Storagetype_sub: `%|-%<:%`(C, (C.ELEMS_context[y!`%`_idx.0] : reftype <: storagetype), zt) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:329.1-333.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:338.1-342.24 rule array.init_data{C : context, x : idx, y : idx, zt : storagetype, numtype : numtype, vectype : vectype}: `%|-%:%`(C, ARRAY.INIT_DATA_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(), _IDX_typeuse(x))) I32_valtype I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], ARRAY_comptype(`%%`_fieldtype(?(MUT_mut), zt))) -- if (($unpack(zt) = (numtype : numtype <: valtype)) \/ ($unpack(zt) = (vectype : vectype <: valtype))) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:338.1-340.26 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:347.1-349.26 rule extern.convert_any{C : context, `null_1?` : null?, `null_2?` : null?}: `%|-%:%`(C, EXTERN.CONVERT_ANY_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(null_1?{null_1 <- `null_1?`}, ANY_heaptype)]), [], `%`_resulttype([REF_valtype(null_2?{null_2 <- `null_2?`}, EXTERN_heaptype)]))) -- if (null_1?{null_1 <- `null_1?`} = null_2?{null_2 <- `null_2?`}) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:342.1-344.26 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:351.1-353.26 rule any.convert_extern{C : context, `null_1?` : null?, `null_2?` : null?}: `%|-%:%`(C, ANY.CONVERT_EXTERN_instr, `%->_%%`_instrtype(`%`_resulttype([REF_valtype(null_1?{null_1 <- `null_1?`}, EXTERN_heaptype)]), [], `%`_resulttype([REF_valtype(null_2?{null_2 <- `null_2?`}, ANY_heaptype)]))) -- if (null_1?{null_1 <- `null_1?`} = null_2?{null_2 <- `null_2?`}) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:349.1-351.28 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:358.1-360.28 rule local.get{C : context, x : idx, t : valtype}: `%|-%:%`(C, LOCAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(SET_init, t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:353.1-355.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:362.1-364.29 rule local.set{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:357.1-359.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:366.1-368.29 rule local.tee{C : context, x : idx, t : valtype, init : init}: `%|-%:%`(C, LOCAL.TEE_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [x], `%`_resulttype([t]))) -- if (C.LOCALS_context[x!`%`_idx.0] = `%%`_localtype(init, t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:364.1-366.30 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:373.1-375.30 rule global.get{C : context, x : idx, t : valtype, `mut?` : mut?}: `%|-%:%`(C, GLOBAL.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([t]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(mut?{mut <- `mut?`}, t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:368.1-370.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:377.1-379.29 rule global.set{C : context, x : idx, t : valtype}: `%|-%:%`(C, GLOBAL.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([t]), [], `%`_resulttype([]))) -- if (C.GLOBALS_context[x!`%`_idx.0] = `%%`_globaltype(?(MUT_mut), t)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:375.1-377.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:384.1-386.32 rule table.get{C : context, x : idx, at : addrtype, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.GET_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(rt : reftype <: valtype)]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:379.1-381.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:388.1-390.32 rule table.set{C : context, x : idx, at : addrtype, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.SET_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (rt : reftype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:383.1-385.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:392.1-394.32 rule table.size{C : context, x : idx, at : addrtype, lim : limits, rt : reftype}: `%|-%:%`(C, TABLE.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([(at : addrtype <: valtype)]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:387.1-389.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:396.1-398.32 rule table.grow{C : context, x : idx, rt : reftype, at : addrtype, lim : limits}: `%|-%:%`(C, TABLE.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) (at : addrtype <: valtype)]), [], `%`_resulttype([I32_valtype]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:391.1-393.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:400.1-402.32 rule table.fill{C : context, x : idx, at : addrtype, rt : reftype, lim : limits}: `%|-%:%`(C, TABLE.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (rt : reftype <: valtype) (at : addrtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:395.1-399.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:404.1-408.36 rule table.copy{C : context, x_1 : idx, x_2 : idx, at_1 : addrtype, at_2 : addrtype, lim_1 : limits, rt_1 : reftype, lim_2 : limits, rt_2 : reftype}: `%|-%:%`(C, TABLE.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([(at_1 : addrtype <: valtype) (at_2 : addrtype <: valtype) ($minat(at_1, at_2) : addrtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x_1!`%`_idx.0] = `%%%`_tabletype(at_1, lim_1, rt_1)) -- if (C.TABLES_context[x_2!`%`_idx.0] = `%%%`_tabletype(at_2, lim_2, rt_2)) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:401.1-405.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:410.1-414.36 rule table.init{C : context, x : idx, y : idx, at : addrtype, lim : limits, rt_1 : reftype, rt_2 : reftype}: `%|-%:%`(C, TABLE.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt_1)) -- if (C.ELEMS_context[y!`%`_idx.0] = rt_2) -- Reftype_sub: `%|-%<:%`(C, rt_2, rt_1) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:407.1-409.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:416.1-418.24 rule elem.drop{C : context, x : idx, rt : reftype}: `%|-%:%`(C, ELEM.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.ELEMS_context[x!`%`_idx.0] = rt) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:422.1-424.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:431.1-433.32 rule memory.size{C : context, x : idx, at : addrtype, lim : limits}: `%|-%:%`(C, MEMORY.SIZE_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([(at : addrtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:426.1-428.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:435.1-437.32 rule memory.grow{C : context, x : idx, at : addrtype, lim : limits}: `%|-%:%`(C, MEMORY.GROW_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(at : addrtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:430.1-432.32 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:439.1-441.32 rule memory.fill{C : context, x : idx, at : addrtype, lim : limits}: `%|-%:%`(C, MEMORY.FILL_instr(x), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) I32_valtype (at : addrtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:434.1-437.38 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:443.1-446.38 rule memory.copy{C : context, x_1 : idx, x_2 : idx, at_1 : addrtype, at_2 : addrtype, lim_1 : limits, lim_2 : limits}: `%|-%:%`(C, MEMORY.COPY_instr(x_1, x_2), `%->_%%`_instrtype(`%`_resulttype([(at_1 : addrtype <: valtype) (at_2 : addrtype <: valtype) ($minat(at_1, at_2) : addrtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x_1!`%`_idx.0] = `%%PAGE`_memtype(at_1, lim_1)) -- if (C.MEMS_context[x_2!`%`_idx.0] = `%%PAGE`_memtype(at_2, lim_2)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:439.1-442.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:448.1-451.24 rule memory.init{C : context, x : idx, y : idx, at : addrtype, lim : limits}: `%|-%:%`(C, MEMORY.INIT_instr(x, y), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) I32_valtype I32_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (C.DATAS_context[y!`%`_idx.0] = OK_datatype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:444.1-446.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:453.1-455.24 rule data.drop{C : context, x : idx}: `%|-%:%`(C, DATA.DROP_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) -- if (C.DATAS_context[x!`%`_idx.0] = OK_datatype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:457.1-460.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:466.1-469.44 rule `load-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, LOAD_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(nt : numtype <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:462.1-465.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:471.1-474.36 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, M) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:476.1-479.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:485.1-488.44 rule `store-val`{C : context, nt : numtype, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, STORE_instr(nt, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (nt : numtype <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $size(nt)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:481.1-484.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:490.1-493.36 rule `store-pack`{C : context, Inn : Inn, M : M, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(M))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) (Inn : Inn <: valtype)]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, M) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:486.1-489.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:495.1-498.47 rule `vload-val`{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $vsize(V128_vectype)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:491.1-494.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:500.1-503.41 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, (M * N)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:496.1-499.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:505.1-508.36 rule `vload-splat`{C : context, N : N, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, N) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:501.1-504.36 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:510.1-513.36 rule `vload-zero`{C : context, N : N, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(ZERO_vloadop_(`%`_sz(N))), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, N) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:506.1-510.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:515.1-519.21 rule vload_lane{C : context, N : N, x : idx, memarg : memarg, i : laneidx, at : addrtype, lim : limits}: `%|-%:%`(C, VLOAD_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, i), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, N) -- if ((i!`%`_laneidx.0 : nat <:> rat) < ((128 : nat <:> rat) / (N : nat <:> rat))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:512.1-515.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:521.1-524.47 rule vstore{C : context, x : idx, memarg : memarg, at : addrtype, lim : limits}: `%|-%:%`(C, VSTORE_instr(V128_vectype, x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, $vsize(V128_vectype)) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:517.1-521.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:526.1-530.21 rule vstore_lane{C : context, N : N, x : idx, memarg : memarg, i : laneidx, at : addrtype, lim : limits}: `%|-%:%`(C, VSTORE_LANE_instr(V128_vectype, `%`_sz(N), x, memarg, i), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype) V128_valtype]), [], `%`_resulttype([]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- Memarg_ok: `|-%:%->%`(memarg, at, N) -- if ((i!`%`_laneidx.0 : nat <:> rat) < ((128 : nat <:> rat) / (N : nat <:> rat))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:526.1-527.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:535.1-536.33 rule const{C : context, nt : numtype, c_nt : num_(nt)}: `%|-%:%`(C, CONST_instr(nt, c_nt), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([(nt : numtype <: valtype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:529.1-530.34 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:538.1-539.34 rule unop{C : context, nt : numtype, unop_nt : unop_(nt)}: `%|-%:%`(C, UNOP_instr(nt, unop_nt), `%->_%%`_instrtype(`%`_resulttype([(nt : numtype <: valtype)]), [], `%`_resulttype([(nt : numtype <: valtype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:532.1-533.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:541.1-542.39 rule binop{C : context, nt : numtype, binop_nt : binop_(nt)}: `%|-%:%`(C, BINOP_instr(nt, binop_nt), `%->_%%`_instrtype(`%`_resulttype([(nt : numtype <: valtype) (nt : numtype <: valtype)]), [], `%`_resulttype([(nt : numtype <: valtype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:535.1-536.39 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:544.1-545.39 rule testop{C : context, nt : numtype, testop_nt : testop_(nt)}: `%|-%:%`(C, TESTOP_instr(nt, testop_nt), `%->_%%`_instrtype(`%`_resulttype([(nt : numtype <: valtype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:538.1-539.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:547.1-548.40 rule relop{C : context, nt : numtype, relop_nt : relop_(nt)}: `%|-%:%`(C, RELOP_instr(nt, relop_nt), `%->_%%`_instrtype(`%`_resulttype([(nt : numtype <: valtype) (nt : numtype <: valtype)]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:541.1-542.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:550.1-551.44 rule cvtop{C : context, nt_1 : numtype, nt_2 : numtype, cvtop : cvtop__(nt_2, nt_1)}: `%|-%:%`(C, CVTOP_instr(nt_1, nt_2, cvtop), `%->_%%`_instrtype(`%`_resulttype([(nt_2 : numtype <: valtype)]), [], `%`_resulttype([(nt_1 : numtype <: valtype)]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:547.1-548.35 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:556.1-557.35 rule vconst{C : context, c : vec_(V128_Vnn)}: `%|-%:%`(C, VCONST_instr(V128_vectype, c), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:550.1-551.41 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:559.1-560.41 rule vvunop{C : context, vvunop : vvunop}: `%|-%:%`(C, VVUNOP_instr(V128_vectype, vvunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:553.1-554.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:562.1-563.48 rule vvbinop{C : context, vvbinop : vvbinop}: `%|-%:%`(C, VVBINOP_instr(V128_vectype, vvbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:556.1-557.55 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:565.1-566.55 rule vvternop{C : context, vvternop : vvternop}: `%|-%:%`(C, VVTERNOP_instr(V128_vectype, vvternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:559.1-560.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:568.1-569.44 rule vvtestop{C : context, vvtestop : vvtestop}: `%|-%:%`(C, VVTESTOP_instr(V128_vectype, vvtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:562.1-563.37 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:571.1-572.37 rule vunop{C : context, sh : shape, vunop : vunop_(sh)}: `%|-%:%`(C, VUNOP_instr(sh, vunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:565.1-566.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:574.1-575.44 rule vbinop{C : context, sh : shape, vbinop : vbinop_(sh)}: `%|-%:%`(C, VBINOP_instr(sh, vbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:568.1-569.51 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:577.1-578.51 rule vternop{C : context, sh : shape, vternop : vternop_(sh)}: `%|-%:%`(C, VTERNOP_instr(sh, vternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:571.1-572.40 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:580.1-581.40 rule vtestop{C : context, sh : shape, vtestop : vtestop_(sh)}: `%|-%:%`(C, VTESTOP_instr(sh, vtestop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:574.1-575.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:583.1-584.44 rule vrelop{C : context, sh : shape, vrelop : vrelop_(sh)}: `%|-%:%`(C, VRELOP_instr(sh, vrelop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:577.1-578.47 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:586.1-587.47 rule vshiftop{C : context, sh : ishape, vshiftop : vshiftop_(sh)}: `%|-%:%`(C, VSHIFTOP_instr(sh, vshiftop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype I32_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:580.1-581.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:589.1-590.33 rule vbitmask{C : context, sh : ishape}: `%|-%:%`(C, VBITMASK_instr(sh), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([I32_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:583.1-584.50 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:592.1-593.50 rule vswizzlop{C : context, sh : bshape, vswizzlop : vswizzlop_(sh)}: `%|-%:%`(C, VSWIZZLOP_instr(sh, vswizzlop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:586.1-588.29 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:595.1-597.29 rule vshuffle{C : context, sh : bshape, `i*` : laneidx*}: `%|-%:%`(C, VSHUFFLE_instr(sh, i*{i <- `i*`}), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) -- (if (i!`%`_laneidx.0 < (2 * $dim(sh!`%`_bshape.0)!`%`_dim.0)))*{i <- `i*`} - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:590.1-591.44 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:599.1-600.44 rule vsplat{C : context, sh : shape}: `%|-%:%`(C, VSPLAT_instr(sh), `%->_%%`_instrtype(`%`_resulttype([($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:593.1-595.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:602.1-604.21 rule vextract_lane{C : context, sh : shape, `sx?` : sx?, i : laneidx}: `%|-%:%`(C, VEXTRACT_LANE_instr(sh, sx?{sx <- `sx?`}, i), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([($unpackshape(sh) : numtype <: valtype)]))) -- if (i!`%`_laneidx.0 < $dim(sh)!`%`_dim.0) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:597.1-599.21 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:606.1-608.21 rule vreplace_lane{C : context, sh : shape, i : laneidx}: `%|-%:%`(C, VREPLACE_LANE_instr(sh, i), `%->_%%`_instrtype(`%`_resulttype([V128_valtype ($unpackshape(sh) : numtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (i!`%`_laneidx.0 < $dim(sh)!`%`_dim.0) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:601.1-602.50 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:610.1-611.50 rule vextunop{C : context, sh_1 : ishape, sh_2 : ishape, vextunop : vextunop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTUNOP_instr(sh_1, sh_2, vextunop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:604.1-605.57 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:613.1-614.57 rule vextbinop{C : context, sh_1 : ishape, sh_2 : ishape, vextbinop : vextbinop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTBINOP_instr(sh_1, sh_2, vextbinop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:607.1-608.64 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:616.1-617.64 rule vextternop{C : context, sh_1 : ishape, sh_2 : ishape, vextternop : vextternop__(sh_2, sh_1)}: `%|-%:%`(C, VEXTTERNOP_instr(sh_1, sh_2, vextternop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:610.1-611.48 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:619.1-620.48 rule vnarrow{C : context, sh_1 : ishape, sh_2 : ishape, sx : sx}: `%|-%:%`(C, VNARROW_instr(sh_1, sh_2, sx), `%->_%%`_instrtype(`%`_resulttype([V128_valtype V128_valtype]), [], `%`_resulttype([V128_valtype]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:613.1-614.46 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:622.1-623.46 rule vcvtop{C : context, sh_1 : shape, sh_2 : shape, vcvtop : vcvtop__(sh_2, sh_1)}: `%|-%:%`(C, VCVTOP_instr(sh_1, sh_2, vcvtop), `%->_%%`_instrtype(`%`_resulttype([V128_valtype]), [], `%`_resulttype([V128_valtype]))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:6.1-6.96 relation Instrs_ok: `%|-%:%`(context, instr*, instrtype) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:619.1-620.24 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:628.1-629.24 rule empty{C : context}: `%|-%:%`(C, [], `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([]))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:623.1-627.82 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:632.1-636.82 rule seq{C : context, instr_1 : instr, `instr_2*` : instr*, `t_1*` : valtype*, `x_1*` : idx*, `x_2*` : idx*, `t_3*` : valtype*, `t_2*` : valtype*, `init*` : init*, `t*` : valtype*}: `%|-%:%`(C, [instr_1] ++ instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x_1*{x_1 <- `x_1*`} ++ x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`}))) -- Instr_ok: `%|-%:%`(C, instr_1, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x_1*{x_1 <- `x_1*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`}))) -- (if (C.LOCALS_context[x_1!`%`_idx.0] = `%%`_localtype(init, t)))*{init <- `init*`, t <- `t*`, x_1 <- `x_1*`} -- Instrs_ok: `%|-%:%`($with_locals(C, x_1*{x_1 <- `x_1*`}, `%%`_localtype(SET_init, t)*{t <- `t*`}), instr_2*{instr_2 <- `instr_2*`}, `%->_%%`_instrtype(`%`_resulttype(t_2*{t_2 <- `t_2*`}), x_2*{x_2 <- `x_2*`}, `%`_resulttype(t_3*{t_3 <- `t_3*`}))) - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:629.1-633.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:638.1-642.33 rule sub{C : context, `instr*` : instr*, it' : instrtype, it : instrtype}: `%|-%:%`(C, instr*{instr <- `instr*`}, it') -- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, it) -- Instrtype_sub: `%|-%<:%`(C, it, it') -- Instrtype_ok: `%|-%:OK`(C, it') - ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:636.1-639.33 + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:645.1-648.33 rule frame{C : context, `instr*` : instr*, `t*` : valtype*, `t_1*` : valtype*, `x*` : idx*, `t_2*` : valtype*}: `%|-%:%`(C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t*{t <- `t*`} ++ t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t*{t <- `t*`} ++ t_2*{t_2 <- `t_2*`}))) -- Instrs_ok: `%|-%:%`(C, instr*{instr <- `instr*`}, `%->_%%`_instrtype(`%`_resulttype(t_1*{t_1 <- `t_1*`}), x*{x <- `x*`}, `%`_resulttype(t_2*{t_2 <- `t_2*`}))) @@ -4088,6 +4108,14 @@ relation Instr_const: `%|-%CONST`(context, instr) rule struct.new_default{C : context, x : idx}: `%|-%CONST`(C, STRUCT.NEW_DEFAULT_instr(x)) + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec + rule struct.new_desc{C : context, x : idx}: + `%|-%CONST`(C, STRUCT.NEW_DESC_instr(x)) + + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec + rule struct.new_default_desc{C : context, x : idx}: + `%|-%CONST`(C, STRUCT.NEW_DEFAULT_DESC_instr(x)) + ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec rule array.new{C : context, x : idx}: `%|-%CONST`(C, ARRAY.NEW_instr(x)) From f1b94b8bcb92ae2cdf96890a58a2cec06a329cb0 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 14 Jul 2026 05:39:27 -0700 Subject: [PATCH 7/9] fix parens --- specification/wasm-latest/1.2-syntax.types.spectec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec index 6bf936730..cdf6c2ef1 100644 --- a/specification/wasm-latest/1.2-syntax.types.spectec +++ b/specification/wasm-latest/1.2-syntax.types.spectec @@ -43,7 +43,7 @@ syntax typevar hint(desc "type variable") = | _IDX typeidx | REC n hint(show REC.%) syntax heaptype hint(desc "heap type") = - | absheaptype | _HT exact? typeuse + | absheaptype | _HT exact? typeuse hint(show % %) syntax reftype hint(desc "reference type") = | REF null? heaptype From de6816fa1db460e5ee669f19d21f4e51e9c51e13 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Tue, 14 Jul 2026 05:44:22 -0700 Subject: [PATCH 8/9] update tests --- 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 3f47dc1b8..8dcc6cc80 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -616,7 +616,7 @@ syntax typeuse = | _DEF{rectype : rectype, n : n}(rectype : rectype, n : n) | REC{n : n}(n : n) -;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:45.1-46.37 +;; ../../../../specification/wasm-latest/1.2-syntax.types.spectec:45.1-46.52 syntax heaptype = | ANY | EQ From 29dcc39efa829c2e41ee8eb2d567dfd85e4babe8 Mon Sep 17 00:00:00 2001 From: Thomas Lively Date: Fri, 24 Jul 2026 11:59:54 -0700 Subject: [PATCH 9/9] Update prose and ExpandDesc => Expand_desc --- document/core/valid/conventions.rst | 4 ++-- specification/wasm-latest/2.1-validation.types.spectec | 4 ++-- .../wasm-latest/2.3-validation.instructions.spectec | 8 ++++---- spectec/src/backend-prose/gen.ml | 2 +- spectec/test-frontend/TEST.md | 10 +++++----- 5 files changed, 14 insertions(+), 14 deletions(-) diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 8ec31b468..8d009021a 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -170,9 +170,9 @@ $${rule: Expand {Expand_use/*}} $${relation-ignore: Expand Expand_use} $${definition-ignore: expanddt} -We use the same notation to denote the expansion of a :ref:`defined type ` or :ref:`type use ` to a :ref:`desctype ` as well. +The same notation also denotes the expansion of a :ref:`defined type ` or :ref:`type use ` to a :ref:`desctype `. -$${rule: ExpandDesc} +$${rule: Expand_desc} .. index:: ! instruction type, value type, result type, instruction, local, local index diff --git a/specification/wasm-latest/2.1-validation.types.spectec b/specification/wasm-latest/2.1-validation.types.spectec index 8cf635aa5..a8d40c64e 100644 --- a/specification/wasm-latest/2.1-validation.types.spectec +++ b/specification/wasm-latest/2.1-validation.types.spectec @@ -73,10 +73,10 @@ rule Expand: deftype ~~ comptype -- if $expanddt(deftype) = comptype rule Expand_use/deftype: deftype ~~_C comptype -- Expand: deftype ~~ comptype rule Expand_use/typeidx: _IDX typeidx ~~_C comptype -- Expand: C.TYPES[typeidx] ~~ comptype -relation ExpandDesc: deftype ~~ desctype hint(macro "%expanddt_to_desctype") hint(tabular) +relation Expand_desc: deftype ~~ desctype hint(macro "%expanddt_to_desctype") hint(tabular) hint(prose "The :ref:`expansion ` of %1 is %2") ;; TODO(3, ?): avoid hardcoding reST -rule ExpandDesc: deftype ~~ desctype -- if $expanddt_to_desctype(deftype) = desctype +rule Expand_desc: deftype ~~ desctype -- if $expanddt_to_desctype(deftype) = desctype ;; Type definitions diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec index 28487693e..ff3dd90b7 100644 --- a/specification/wasm-latest/2.3-validation.instructions.spectec +++ b/specification/wasm-latest/2.3-validation.instructions.spectec @@ -251,20 +251,20 @@ rule Instr_ok/i31.get: rule Instr_ok/struct.new: C |- STRUCT.NEW x : $unpack(zt)* -> (REF (_HT _IDX x)) - -- ExpandDesc: C.TYPES[x] ~~ describestype? eps STRUCT (mut? zt)* + -- Expand_desc: C.TYPES[x] ~~ describestype? eps STRUCT (mut? zt)* rule Instr_ok/struct.new_default: C |- STRUCT.NEW_DEFAULT x : eps -> (REF (_HT _IDX x)) - -- ExpandDesc: C.TYPES[x] ~~ describestype? eps STRUCT (mut? zt)* + -- Expand_desc: C.TYPES[x] ~~ describestype? eps STRUCT (mut? zt)* -- (Defaultable: |- $unpack(zt) DEFAULTABLE)* rule Instr_ok/struct.new_desc: C |- STRUCT.NEW_DESC x : $unpack(zt)* (REF NULL (_HT EXACT _IDX y)) -> (REF (_HT EXACT _IDX x)) - -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) (STRUCT (mut? zt)*) + -- Expand_desc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) (STRUCT (mut? zt)*) rule Instr_ok/struct.new_default_desc: C |- STRUCT.NEW_DEFAULT_DESC x : (REF NULL (_HT EXACT (_IDX y))) -> (REF (_HT EXACT _IDX x)) - -- ExpandDesc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) (STRUCT (mut? zt)*) + -- Expand_desc: C.TYPES[x] ~~ describestype? (DESCRIPTOR (_IDX y)) (STRUCT (mut? zt)*) -- (Defaultable: |- $unpack(zt) DEFAULTABLE)* def $is_packtype(storagetype) : bool hint(show %1 = $unpack(%1)) hint(prose "%1 is a packed type") diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml index 9b966ce22..4c4ffb3a3 100644 --- a/spectec/src/backend-prose/gen.ml +++ b/spectec/src/backend-prose/gen.ml @@ -32,7 +32,7 @@ let flatten_rec def = let is_validation_helper_relation def = match def.it with - | Ast.RelD (id, _, _, _) -> id.it = "Expand" || id.it = "Expand_use" || id.it = "ExpandDesc" + | Ast.RelD (id, _, _, _) -> id.it = "Expand" || id.it = "Expand_use" || id.it = "Expand_desc" | _ -> false (* NOTE: Assume validation relation is `|-` *) let is_validation_relation def = diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 82c65d700..bfb0edfd1 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -3196,7 +3196,7 @@ relation Expand_use: `%~~_%%`(typeuse, context, comptype) -- Expand: `%~~%`(C.TYPES_context[typeidx!`%`_typeidx.0], comptype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec -relation ExpandDesc: `%~~%`(deftype, desctype) +relation Expand_desc: `%~~%`(deftype, desctype) ;; ../../../../specification/wasm-latest/2.1-validation.types.spectec rule _{deftype : deftype, desctype : desctype}: `%~~%`(deftype, desctype) @@ -3642,23 +3642,23 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:252.1-254.68 rule struct.new{C : context, x : idx, `zt*` : storagetype*, `describestype?` : describestype?, `mut?*` : mut?*}: `%|-%:%`(C, STRUCT.NEW_instr(x), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)*{zt <- `zt*`}), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) - -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) + -- Expand_desc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:256.1-259.48 rule struct.new_default{C : context, x : idx, `describestype?` : describestype?, `mut?*` : mut?*, `zt*` : storagetype*}: `%|-%:%`(C, STRUCT.NEW_DEFAULT_instr(x), `%->_%%`_instrtype(`%`_resulttype([]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(), _IDX_typeuse(x)))]))) - -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) + -- Expand_desc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:261.1-263.88 rule struct.new_desc{C : context, x : idx, `zt*` : storagetype*, y : idx, `describestype?` : describestype?, `mut?*` : mut?*}: `%|-%:%`(C, STRUCT.NEW_DESC_instr(x), `%->_%%`_instrtype(`%`_resulttype($unpack(zt)*{zt <- `zt*`} ++ [REF_valtype(?(NULL_null), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(y)))]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(x)))]))) - -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) + -- Expand_desc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:265.1-268.48 rule struct.new_default_desc{C : context, x : idx, y : idx, `describestype?` : describestype?, `mut?*` : mut?*, `zt*` : storagetype*}: `%|-%:%`(C, STRUCT.NEW_DEFAULT_DESC_instr(x), `%->_%%`_instrtype(`%`_resulttype([REF_valtype(?(NULL_null), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(y)))]), [], `%`_resulttype([REF_valtype(?(), _HT_heaptype(?(EXACT_exact), _IDX_typeuse(x)))]))) - -- ExpandDesc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) + -- Expand_desc: `%~~%`(C.TYPES_context[x!`%`_idx.0], `%%%`_desctype(describestype?{describestype <- `describestype?`}, ?(DESCRIPTOR_descriptortype(_IDX_typeuse(y))), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))) -- (Defaultable: `|-%DEFAULTABLE`($unpack(zt)))*{zt <- `zt*`} ;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:273.1-277.41