Skip to content

[spec] Fix definition of is_packtype #2061

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

Merged
rossberg merged 1 commit into from
Jan 28, 2026
Merged

[spec] Fix definition of is_packtype #2061

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 2 additions & 2 deletions 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 @@ -253,13 +253,13 @@ rule Instr_ok/struct.new_default:
-- (Defaultable: |- $unpack(zt) DEFAULTABLE)*

def $is_packtype(storagetype) : bool hint(show %1 = $unpack(%1)) hint(prose "%1 is a packed type")
def $is_packtype(zt) = zt = $unpack(zt)
def $is_packtype(zt) = zt =/= $unpack(zt)

rule Instr_ok/struct.get:
C |- STRUCT.GET sx? x i : (REF NULL (_IDX x)) -> $unpack(zt)
-- Expand: C.TYPES[x] ~~ STRUCT ft*
-- if ft*[i] = mut? zt
-- if sx? = eps <=> $is_packtype(zt)
-- if sx? =/= eps <=> $is_packtype(zt)

rule Instr_ok/struct.set:
C |- STRUCT.SET x i : (REF NULL (_IDX x)) $unpack(zt) -> eps
Expand Down
Binary file modified spectec/doc/example/output/NanoWasm.pdf
View file
Open in desktop
Binary file not shown.
6 changes: 5 additions & 1 deletion spectec/src/backend-prose/render.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -941,7 +941,11 @@ let rec render_single_stmt ?(with_type=true) env stmt =
| CmpS (e1, cmpop, e2) ->
let cmpop, rhs =
match e2.it with
| OptE None -> render_prose_cmpop_eps cmpop, "absent"
| OptE None ->
if cmpop = `NeOp then
render_prose_cmpop_eps `EqOp, "present"
else
render_prose_cmpop_eps cmpop, "absent"
| ListE [] -> render_prose_cmpop_eps cmpop, "empty"
| BoolE _ -> render_prose_cmpop_eps cmpop, render_expr env e2
| _ -> render_prose_cmpop cmpop, render_expr env e2
Expand Down
6 changes: 3 additions & 3 deletions spectec/test-frontend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3340,7 +3340,7 @@ relation Memarg_ok: `|-%:%->%`(memarg, addrtype, N)
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
def $is_packtype(storagetype : storagetype) : bool
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
def $is_packtype{zt : storagetype}(zt) = (zt = ($unpack(zt) : valtype <: storagetype))
def $is_packtype{zt : storagetype}(zt) = (zt =/= ($unpack(zt) : valtype <: storagetype))

;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
rec {
Expand Down Expand Up @@ -3564,12 +3564,12 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
-- 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-3.0/2.3-validation.instructions.spectec:258.1-262.39
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.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)])))
-- 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))
-- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt))

;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:264.1-267.24
rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}:
Expand Down
4 changes: 2 additions & 2 deletions spectec/test-latex/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6360,7 +6360,7 @@ $$

$$
\begin{array}[t]{@{}lcl@{}l@{}}
{\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}}) & = & {\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}}) \\
{\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}}) & = & {\mathit{zt}} \neq {\mathrm{unpack}}({\mathit{zt}}) \\
\end{array}
$$

Expand All @@ -6371,7 +6371,7 @@ C{.}\mathsf{types}{}[x] \approx \mathsf{struct}~{{\mathit{ft}}^\ast}
\qquad
{{\mathit{ft}}^\ast}{}[i] = {\mathsf{mut}^?}~{\mathit{zt}}
\qquad
{{\mathit{sx}}^?} = \epsilon \Leftrightarrow {\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}})
{{\mathit{sx}}^?} \neq \epsilon \Leftrightarrow {\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}})
}{
C \vdash {\mathsf{struct{.}get}}{\mathsf{\_}}{{{\mathit{sx}}^?}}~x~i : (\mathsf{ref}~\mathsf{null}~x) \rightarrow {\mathrm{unpack}}({\mathit{zt}})
} \, {[\textsc{\scriptsize T{-}instr{-}struct.get}]}
Expand Down
18 changes: 9 additions & 9 deletions spectec/test-middlend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3330,7 +3330,7 @@ relation Memarg_ok: `|-%:%->%`(memarg, addrtype, N)
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
def $is_packtype(storagetype : storagetype) : bool
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
def $is_packtype{zt : storagetype}(zt) = (zt = ($unpack(zt) : valtype <: storagetype))
def $is_packtype{zt : storagetype}(zt) = (zt =/= ($unpack(zt) : valtype <: storagetype))

;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
rec {
Expand Down Expand Up @@ -3554,12 +3554,12 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
-- 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-3.0/2.3-validation.instructions.spectec:258.1-262.39
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.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)])))
-- 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))
-- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt))

;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:264.1-267.24
rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}:
Expand Down Expand Up @@ -14684,7 +14684,7 @@ relation Memarg_ok: `|-%:%->%`(memarg, addrtype, N)
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
def $is_packtype(storagetype : storagetype) : bool
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
def $is_packtype{zt : storagetype}(zt) = (zt = ($unpack(zt) : valtype <: storagetype))
def $is_packtype{zt : storagetype}(zt) = (zt =/= ($unpack(zt) : valtype <: storagetype))

;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
rec {
Expand Down Expand Up @@ -14908,12 +14908,12 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
-- 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-3.0/2.3-validation.instructions.spectec:258.1-262.39
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.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)])))
-- 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))
-- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt))

;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:264.1-267.24
rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}:
Expand Down Expand Up @@ -26066,7 +26066,7 @@ relation Memarg_ok: `|-%:%->%`(memarg, addrtype, N)
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
def $is_packtype(storagetype : storagetype) : bool
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
def $is_packtype{zt : storagetype}(zt) = (zt = ($unpack(zt) : valtype <: storagetype))
def $is_packtype{zt : storagetype}(zt) = (zt =/= ($unpack(zt) : valtype <: storagetype))

;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec
rec {
Expand Down Expand Up @@ -26311,14 +26311,14 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype)
-- 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-3.0/2.3-validation.instructions.spectec:258.1-262.39
;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:258.1-262.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)])))
-- if (x!`%`_idx.0 < |C.TYPES_context|)
-- Expand: `%~~%`(C.TYPES_context[x!`%`_idx.0], STRUCT_comptype(`%`_list(ft*{ft <- `ft*`})))
-- if (i!`%`_u32.0 < |ft*{ft <- `ft*`}|)
-- if (ft*{ft <- `ft*`}[i!`%`_u32.0] = `%%`_fieldtype(mut?{mut <- `mut?`}, zt))
-- if ((sx?{sx <- `sx?`} = ?()) <=> $is_packtype(zt))
-- if ((sx?{sx <- `sx?`} =/= ?()) <=> $is_packtype(zt))

;; ../../../../specification/wasm-3.0/2.3-validation.instructions.spectec:264.1-267.24
rule struct.set{C : context, x : idx, i : u32, zt : storagetype, `ft*` : fieldtype*}:
Expand Down
10 changes: 5 additions & 5 deletions spectec/test-prose/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15216,7 +15216,7 @@ The catch clause :math:`(\mathsf{catch\_all\_ref}~l)` is :ref:`valid <valid-val>
The value type :math:`t` is defaultable if:


* The value :math:`{{\mathrm{default}}}_{t}` is not absent.
* The value :math:`{{\mathrm{default}}}_{t}` is present.



Expand Down Expand Up @@ -15658,7 +15658,7 @@ The instruction :math:`({\mathsf{struct{.}get}}{\mathsf{\_}}{{{\mathit{sx}}^?}}~

* The field type :math:`{{\mathit{ft}}^\ast}{}[i]` is of the form :math:`({\mathsf{mut}^?}~{\mathit{zt}})`.

* The signedness :math:`{{\mathit{sx}}^?}` is absent if and only if :math:`{\mathit{zt}}` is a packed type.
* The signedness :math:`{{\mathit{sx}}^?}` is present if and only if :math:`{\mathit{zt}}` is a packed type.

* The value type :math:`t` is :math:`{\mathrm{unpack}}({\mathit{zt}})`.

Expand Down Expand Up @@ -23690,7 +23690,7 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
......................................


1. Return :math:`{\mathit{zt}} = {\mathrm{unpack}}({\mathit{zt}})`.
1. Return :math:`{\mathit{zt}} \neq {\mathrm{unpack}}({\mathit{zt}})`.


:math:`{\mathrm{funcidx}}({{\mathit{global}}^\ast}~{{\mathit{mem}}^\ast}~{{\mathit{table}}^\ast}~{{\mathit{elem}}^\ast})`
Expand Down Expand Up @@ -27741,7 +27741,7 @@ Instr_ok/struct.get
- The :ref:`expansion <aux-expand-deftype>` of C.TYPES[x] is (STRUCT ft*).
- |ft*| is greater than i.
- the field type ft*[i] is (mut? zt).
- the signedness sx? is ?() if and only if $is_packtype(zt).
- the signedness sx? is not ?() if and only if $is_packtype(zt).
Copy link
Member

@tlively tlively Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not related to this change, but it's not clear what ?() means.

Copy link
Member Author

@rossberg rossberg Jan 28, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's internal notation for an empty option (this is essentially just debug output).

- the value type t is $unpack(zt).

Instr_ok/struct.set
Expand Down Expand Up @@ -31617,7 +31617,7 @@ default_ valtype
8. Return ?().

is_packtype zt
1. Return (zt = $unpack(zt)).
1. Return (zt =/= $unpack(zt)).

funcidx_nonfuncs (global* mem* table* elem*)
1. Return $funcidx_module((MODULE [] [] [] global* mem* table* [] [] elem* ?() [])).
Expand Down