Skip to content

[spec] Several scattered spec fixes #2112

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
raoxiaojia wants to merge 3 commits into
base: main
Choose a base branch
from
Open

[spec] Several scattered spec fixes #2112

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
78f3302
3 general spec fixes
raoxiaojia Mar 13, 2026
a8de49f
test expects
raoxiaojia Mar 13, 2026
6515970
prose expects
raoxiaojia Mar 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion specification/wasm-3.0/1.3-syntax.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -515,7 +515,7 @@ def $free_instr(REF.I31) = {}

def $free_instr(I31.GET sx) = {}

def $free_instr(STRUCT.NEW typeidx) = {}
def $free_instr(STRUCT.NEW typeidx) = $free_typeidx(typeidx)
def $free_instr(STRUCT.NEW_DEFAULT typeidx) = $free_typeidx(typeidx)
def $free_instr(STRUCT.GET sx? typeidx u32) = $free_typeidx(typeidx)
def $free_instr(STRUCT.SET typeidx u32) = $free_typeidx(typeidx)
Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-3.0/2.3-validation.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -379,7 +379,7 @@ rule Instr_ok/table.size:
-- if C.TABLES[x] = at lim rt

rule Instr_ok/table.grow:
C |- TABLE.GROW x : rt at -> I32
C |- TABLE.GROW x : rt at -> at
-- if C.TABLES[x] = at lim rt

rule Instr_ok/table.fill:
Expand Down
4 changes: 2 additions & 2 deletions specification/wasm-3.0/6.3-text.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -516,8 +516,8 @@ grammar Tplaininstr_(I)/num-cvt-i32 : instr = ...
| ...

grammar Tplaininstr_(I)/num-cvt-i64 : instr = ...
| "i64.extend_i64_s" => CVTOP I64 I64 EXTEND S
| "i64.extend_i64_u" => CVTOP I64 I64 EXTEND U
| "i64.extend_i32_s" => CVTOP I64 I32 EXTEND S
| "i64.extend_i32_u" => CVTOP I64 I32 EXTEND U
| "i64.trunc_f32_s" => CVTOP I64 F32 TRUNC S
| "i64.trunc_f32_u" => CVTOP I64 F32 TRUNC U
| "i64.trunc_f64_s" => CVTOP I64 F64 TRUNC S
Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-latest/1.3-syntax.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -515,7 +515,7 @@ def $free_instr(REF.I31) = {}

def $free_instr(I31.GET sx) = {}

def $free_instr(STRUCT.NEW typeidx) = {}
def $free_instr(STRUCT.NEW typeidx) = $free_typeidx(typeidx)
def $free_instr(STRUCT.NEW_DEFAULT typeidx) = $free_typeidx(typeidx)
def $free_instr(STRUCT.GET sx? typeidx u32) = $free_typeidx(typeidx)
def $free_instr(STRUCT.SET typeidx u32) = $free_typeidx(typeidx)
Expand Down
2 changes: 1 addition & 1 deletion specification/wasm-latest/2.3-validation.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -379,7 +379,7 @@ rule Instr_ok/table.size:
-- if C.TABLES[x] = at lim rt

rule Instr_ok/table.grow:
C |- TABLE.GROW x : rt at -> I32
C |- TABLE.GROW x : rt at -> at
-- if C.TABLES[x] = at lim rt

rule Instr_ok/table.fill:
Expand Down
4 changes: 2 additions & 2 deletions specification/wasm-latest/6.3-text.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -516,8 +516,8 @@ grammar Tplaininstr_(I)/num-cvt-i32 : instr = ...
| ...

grammar Tplaininstr_(I)/num-cvt-i64 : instr = ...
| "i64.extend_i64_s" => CVTOP I64 I64 EXTEND S
| "i64.extend_i64_u" => CVTOP I64 I64 EXTEND U
| "i64.extend_i32_s" => CVTOP I64 I32 EXTEND S
| "i64.extend_i32_u" => CVTOP I64 I32 EXTEND U
| "i64.trunc_f32_s" => CVTOP I64 F32 TRUNC S
| "i64.trunc_f32_u" => CVTOP I64 F32 TRUNC U
| "i64.trunc_f64_s" => CVTOP I64 F64 TRUNC S
Expand Down
10 changes: 5 additions & 5 deletions spectec/test-frontend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2370,8 +2370,8 @@ def $free_instr(instr : instr) : free
def $free_instr(`REF.I31`_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:516.1-516.33
def $free_instr{sx : sx}(`I31.GET`_instr(sx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.41
def $free_instr{typeidx : typeidx}(`STRUCT.NEW`_instr(typeidx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.61
def $free_instr{typeidx : typeidx}(`STRUCT.NEW`_instr(typeidx)) = $free_typeidx(typeidx)
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:519.1-519.69
def $free_instr{typeidx : typeidx}(`STRUCT.NEW_DEFAULT`_instr(typeidx)) = $free_typeidx(typeidx)
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:520.1-520.69
Expand Down Expand Up @@ -3723,7 +3723,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:381.1-383.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])))
`%|-%:%`(C, `TABLE.GROW`_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) (at : addrtype <: valtype)]), [], `%`_resulttype([(at : addrtype <: valtype)])))
-- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:385.1-387.32
Expand Down Expand Up @@ -10600,9 +10600,9 @@ grammar Tplaininstr_(I : I) : instr
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i32.trunc_sat_f64_u" => CVTOP_instr(I32_numtype, F64_numtype, TRUNC_SAT_cvtop__(U_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.extend_i64_s" => CVTOP_instr(I64_numtype, I64_numtype, EXTEND_cvtop__(S_sx))
prod "i64.extend_i32_s" => CVTOP_instr(I64_numtype, I32_numtype, EXTEND_cvtop__(S_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.extend_i64_u" => CVTOP_instr(I64_numtype, I64_numtype, EXTEND_cvtop__(U_sx))
prod "i64.extend_i32_u" => CVTOP_instr(I64_numtype, I32_numtype, EXTEND_cvtop__(U_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.trunc_f32_s" => CVTOP_instr(I64_numtype, F32_numtype, TRUNC_cvtop__(S_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
Expand Down
8 changes: 4 additions & 4 deletions spectec/test-latex/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4196,7 +4196,7 @@ $$
{\mathrm{free}}_{\mathit{instr}}(\mathsf{ref{.}func}~{\mathit{funcidx}}) & = & {\mathrm{free}}_{\mathit{funcidx}}({\mathit{funcidx}}) \\
{\mathrm{free}}_{\mathit{instr}}(\mathsf{ref{.}i{\scriptstyle 31}}) & = & \{ \} \\
{\mathrm{free}}_{\mathit{instr}}({\mathsf{i{\scriptstyle 31}{.}get}}{\mathsf{\_}}{{\mathit{sx}}}) & = & \{ \} \\
{\mathrm{free}}_{\mathit{instr}}(\mathsf{struct{.}new}~{\mathit{typeidx}}) & = & \{ \} \\
{\mathrm{free}}_{\mathit{instr}}(\mathsf{struct{.}new}~{\mathit{typeidx}}) & = & {\mathrm{free}}_{\mathit{typeidx}}({\mathit{typeidx}}) \\
{\mathrm{free}}_{\mathit{instr}}(\mathsf{struct{.}new\_default}~{\mathit{typeidx}}) & = & {\mathrm{free}}_{\mathit{typeidx}}({\mathit{typeidx}}) \\
{\mathrm{free}}_{\mathit{instr}}({\mathsf{struct{.}get}}{\mathsf{\_}}{{{\mathit{sx}}^?}}~{\mathit{typeidx}}~{\mathit{u{\kern-0.1em\scriptstyle 32}}}) & = & {\mathrm{free}}_{\mathit{typeidx}}({\mathit{typeidx}}) \\
{\mathrm{free}}_{\mathit{instr}}(\mathsf{struct{.}set}~{\mathit{typeidx}}~{\mathit{u{\kern-0.1em\scriptstyle 32}}}) & = & {\mathrm{free}}_{\mathit{typeidx}}({\mathit{typeidx}}) \\
Expand Down Expand Up @@ -6677,7 +6677,7 @@ $$
\frac{
C{.}\mathsf{tables}{}[x] = {\mathit{at}}~{\mathit{lim}}~{\mathit{rt}}
}{
C \vdash \mathsf{table{.}grow}~x : {\mathit{rt}}~{\mathit{at}} \rightarrow \mathsf{i{\scriptstyle 32}}
C \vdash \mathsf{table{.}grow}~x : {\mathit{rt}}~{\mathit{at}} \rightarrow {\mathit{at}}
} \, {[\textsc{\scriptsize T{-}instr{-}table.grow}]}
\qquad
\end{array}
Expand Down Expand Up @@ -13186,8 +13186,8 @@ $$
& & | & \mbox{‘\texttt{i32.trunc\_sat\_f32\_u}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 32}} {.} {{\mathsf{trunc\_sat}}{\mathsf{\_}}{\mathsf{u}}}{\mathsf{\_}}{\mathsf{f{\scriptstyle 32}}} \\
& & | & \mbox{‘\texttt{i32.trunc\_sat\_f64\_s}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 32}} {.} {{\mathsf{trunc\_sat}}{\mathsf{\_}}{\mathsf{s}}}{\mathsf{\_}}{\mathsf{f{\scriptstyle 64}}} \\
& & | & \mbox{‘\texttt{i32.trunc\_sat\_f64\_u}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 32}} {.} {{\mathsf{trunc\_sat}}{\mathsf{\_}}{\mathsf{u}}}{\mathsf{\_}}{\mathsf{f{\scriptstyle 64}}} \\
& & | & \mbox{‘\texttt{i64.extend\_i64\_s}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}} {.} {{\mathsf{extend}}{\mathsf{\_}}{\mathsf{s}}}{\mathsf{\_}}{\mathsf{i{\scriptstyle 64}}} \\
& & | & \mbox{‘\texttt{i64.extend\_i64\_u}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}} {.} {{\mathsf{extend}}{\mathsf{\_}}{\mathsf{u}}}{\mathsf{\_}}{\mathsf{i{\scriptstyle 64}}} \\
& & | & \mbox{‘\texttt{i64.extend\_i32\_s}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}} {.} {{\mathsf{extend}}{\mathsf{\_}}{\mathsf{s}}}{\mathsf{\_}}{\mathsf{i{\scriptstyle 32}}} \\
& & | & \mbox{‘\texttt{i64.extend\_i32\_u}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}} {.} {{\mathsf{extend}}{\mathsf{\_}}{\mathsf{u}}}{\mathsf{\_}}{\mathsf{i{\scriptstyle 32}}} \\
& & | & \mbox{‘\texttt{i64.trunc\_f32\_s}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}} {.} {{\mathsf{trunc}}{\mathsf{\_}}{\mathsf{s}}}{\mathsf{\_}}{\mathsf{f{\scriptstyle 32}}} \\
& & | & \mbox{‘\texttt{i64.trunc\_f32\_u}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}} {.} {{\mathsf{trunc}}{\mathsf{\_}}{\mathsf{u}}}{\mathsf{\_}}{\mathsf{f{\scriptstyle 32}}} \\
& & | & \mbox{‘\texttt{i64.trunc\_f64\_s}’} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}} {.} {{\mathsf{trunc}}{\mathsf{\_}}{\mathsf{s}}}{\mathsf{\_}}{\mathsf{f{\scriptstyle 64}}} \\
Expand Down
30 changes: 15 additions & 15 deletions spectec/test-middlend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2360,8 +2360,8 @@ def $free_instr(instr : instr) : free
def $free_instr(`REF.I31`_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:516.1-516.33
def $free_instr{sx : sx}(`I31.GET`_instr(sx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.41
def $free_instr{typeidx : typeidx}(`STRUCT.NEW`_instr(typeidx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.61
def $free_instr{typeidx : typeidx}(`STRUCT.NEW`_instr(typeidx)) = $free_typeidx(typeidx)
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:519.1-519.69
def $free_instr{typeidx : typeidx}(`STRUCT.NEW_DEFAULT`_instr(typeidx)) = $free_typeidx(typeidx)
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:520.1-520.69
Expand Down Expand Up @@ -3713,7 +3713,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:381.1-383.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])))
`%|-%:%`(C, `TABLE.GROW`_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) (at : addrtype <: valtype)]), [], `%`_resulttype([(at : addrtype <: valtype)])))
-- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:385.1-387.32
Expand Down Expand Up @@ -10590,9 +10590,9 @@ grammar Tplaininstr_(I : I) : instr
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i32.trunc_sat_f64_u" => CVTOP_instr(I32_numtype, F64_numtype, TRUNC_SAT_cvtop__(U_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.extend_i64_s" => CVTOP_instr(I64_numtype, I64_numtype, EXTEND_cvtop__(S_sx))
prod "i64.extend_i32_s" => CVTOP_instr(I64_numtype, I32_numtype, EXTEND_cvtop__(S_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.extend_i64_u" => CVTOP_instr(I64_numtype, I64_numtype, EXTEND_cvtop__(U_sx))
prod "i64.extend_i32_u" => CVTOP_instr(I64_numtype, I32_numtype, EXTEND_cvtop__(U_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.trunc_f32_s" => CVTOP_instr(I64_numtype, F32_numtype, TRUNC_cvtop__(S_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
Expand Down Expand Up @@ -13775,8 +13775,8 @@ def $free_instr(instr : instr) : free
def $free_instr(`REF.I31`_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:516.1-516.33
def $free_instr{sx : sx}(`I31.GET`_instr(sx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.41
def $free_instr{typeidx : typeidx}(`STRUCT.NEW`_instr(typeidx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.61
def $free_instr{typeidx : typeidx}(`STRUCT.NEW`_instr(typeidx)) = $free_typeidx(typeidx)
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:519.1-519.69
def $free_instr{typeidx : typeidx}(`STRUCT.NEW_DEFAULT`_instr(typeidx)) = $free_typeidx(typeidx)
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:520.1-520.69
Expand Down Expand Up @@ -15128,7 +15128,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:381.1-383.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])))
`%|-%:%`(C, `TABLE.GROW`_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) (at : addrtype <: valtype)]), [], `%`_resulttype([(at : addrtype <: valtype)])))
-- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt))

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:385.1-387.32
Expand Down Expand Up @@ -22007,9 +22007,9 @@ grammar Tplaininstr_(I : I) : instr
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i32.trunc_sat_f64_u" => CVTOP_instr(I32_numtype, F64_numtype, TRUNC_SAT_cvtop__(U_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.extend_i64_s" => CVTOP_instr(I64_numtype, I64_numtype, EXTEND_cvtop__(S_sx))
prod "i64.extend_i32_s" => CVTOP_instr(I64_numtype, I32_numtype, EXTEND_cvtop__(S_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.extend_i64_u" => CVTOP_instr(I64_numtype, I64_numtype, EXTEND_cvtop__(U_sx))
prod "i64.extend_i32_u" => CVTOP_instr(I64_numtype, I32_numtype, EXTEND_cvtop__(U_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.trunc_f32_s" => CVTOP_instr(I64_numtype, F32_numtype, TRUNC_cvtop__(S_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
Expand Down Expand Up @@ -25192,8 +25192,8 @@ def $free_instr(instr : instr) : free
def $free_instr(`REF.I31`_instr) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:516.1-516.33
def $free_instr{sx : sx}(`I31.GET`_instr(sx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.41
def $free_instr{typeidx : typeidx}(`STRUCT.NEW`_instr(typeidx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:518.1-518.61
def $free_instr{typeidx : typeidx}(`STRUCT.NEW`_instr(typeidx)) = $free_typeidx(typeidx)
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:519.1-519.69
def $free_instr{typeidx : typeidx}(`STRUCT.NEW_DEFAULT`_instr(typeidx)) = $free_typeidx(typeidx)
;; ../../../../specification/wasm-latest/1.3-syntax.instructions.spectec:520.1-520.69
Expand Down Expand Up @@ -26620,7 +26620,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)

;; ../../../../specification/wasm-latest/2.3-validation.instructions.spectec:381.1-383.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])))
`%|-%:%`(C, `TABLE.GROW`_instr(x), `%->_%%`_instrtype(`%`_resulttype([(rt : reftype <: valtype) (at : addrtype <: valtype)]), [], `%`_resulttype([(at : addrtype <: valtype)])))
-- if (x!`%`_idx.0 < |C.TABLES_context|)
-- if (C.TABLES_context[x!`%`_idx.0] = `%%%`_tabletype(at, lim, rt))

Expand Down Expand Up @@ -33604,9 +33604,9 @@ grammar Tplaininstr_(I : I) : instr
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i32.trunc_sat_f64_u" => CVTOP_instr(I32_numtype, F64_numtype, TRUNC_SAT_cvtop__(U_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.extend_i64_s" => CVTOP_instr(I64_numtype, I64_numtype, EXTEND_cvtop__(S_sx))
prod "i64.extend_i32_s" => CVTOP_instr(I64_numtype, I32_numtype, EXTEND_cvtop__(S_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.extend_i64_u" => CVTOP_instr(I64_numtype, I64_numtype, EXTEND_cvtop__(U_sx))
prod "i64.extend_i32_u" => CVTOP_instr(I64_numtype, I32_numtype, EXTEND_cvtop__(U_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
prod "i64.trunc_f32_s" => CVTOP_instr(I64_numtype, F32_numtype, TRUNC_cvtop__(S_sx))
;; ../../../../specification/wasm-latest/6.3-text.instructions.spectec
Expand Down
11 changes: 7 additions & 4 deletions spectec/test-prose/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15935,7 +15935,7 @@ The instruction :math:`(\mathsf{table{.}size}~x)` is :ref:`valid <valid-val>` wi



The instruction :math:`(\mathsf{table{.}grow}~x)` is :ref:`valid <valid-val>` with the instruction type :math:`{\mathit{rt}}~{\mathit{at}}~\rightarrow~\mathsf{i{\scriptstyle 32}}` if:
The instruction :math:`(\mathsf{table{.}grow}~x)` is :ref:`valid <valid-val>` with the instruction type :math:`{\mathit{rt}}~{\mathit{at}}~\rightarrow~{\mathit{at}}` if:


* The table :math:`C{.}\mathsf{tables}{}[x]` exists.
Expand Down Expand Up @@ -23191,7 +23191,9 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i

#. If :math:`{\mathit{instr}'}` is some :math:`\mathsf{struct{.}new}~{\mathit{typeidx}}`, then:

a. Return :math:`\{ \}`.
a. Let :math:`(\mathsf{struct{.}new}~{\mathit{typeidx}})` be the destructuring of :math:`{\mathit{instr}'}`.

#. Return :math:`{\mathrm{free}}_{\mathit{typeidx}}({\mathit{typeidx}})`.

#. If :math:`{\mathit{instr}'}` is some :math:`\mathsf{struct{.}new\_default}~{\mathit{typeidx}}`, then:

Expand Down Expand Up @@ -27958,7 +27960,7 @@ Instr_ok/table.size
- C.TABLES[x] is (at lim rt).

Instr_ok/table.grow
- the instruction (TABLE.GROW x) is valid with the instruction type [rt, at] -> [I32] if:
- the instruction (TABLE.GROW x) is valid with the instruction type [rt, at] -> [at] if:
- the table C.TABLES[x] exists.
- C.TABLES[x] is (at lim rt).

Expand Down Expand Up @@ -31459,7 +31461,8 @@ free_instr instr'
61. If instr' is some I31.GET, then:
a. Return {}.
62. If instr' is some STRUCT.NEW, then:
a. Return {}.
a. Let (STRUCT.NEW typeidx) be instr'.
b. Return $free_typeidx(typeidx).
63. If instr' is some STRUCT.NEW_DEFAULT, then:
a. Let (STRUCT.NEW_DEFAULT typeidx) be instr'.
b. Return $free_typeidx(typeidx).
Expand Down
Loading