Skip to content
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.

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

Spec type and module validation, subtyping, and module instantiation. #382

Merged
merged 13 commits into from
Jul 20, 2023

Conversation

rossberg
Copy link
Member

@rossberg rossberg commented May 30, 2023

Also, moved internal type extensions from syntax to validation chapter.

Baseline: #377

@rossberg rossberg requested a review from conrad-watt May 30, 2023 14:45
@rossberg rossberg mentioned this pull request May 30, 2023
53 tasks

.. |TFUNC| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{func}}
.. |TSTRUCT| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{struct}}
.. |TARRAY| mathdef:: \xref{syntax/types}{syntax-comptype}{\K{array}}
.. |TSUB| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{sub}}
.. |TREC| mathdef:: \xref{syntax/types}{syntax-rectype}{\K{rec}}
.. |TFINAL| mathdef:: \xref{syntax/types}{syntax-subtype}{\K{filan}}
Copy link
Contributor

Choose a reason for hiding this comment

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

Typo: filanfinal

Copy link
Member Author

Choose a reason for hiding this comment

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

Oh dear, thanks, fixed.

@rossberg
Copy link
Member Author

@conrad-watt, ping.

Base automatically changed from spec.valid-instr to main July 12, 2023 18:34
Copy link
Contributor

@conrad-watt conrad-watt left a comment

Choose a reason for hiding this comment

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

Just flagging up that I may fail to catch some semantic errors in matching due to my imperfect understanding - I'm still working to grok.

i.e., all :ref:`type indices <syntax-typeidx>` have been :ref:`substituted <notation-subst>` with their :ref:`defined type <syntax-deftype>` and all free recursive type indices have been :ref:`unrolled <aux-unroll-rectype>`.

.. note::
Recursive type indices are internal to a recursive types.
Copy link
Contributor

Choose a reason for hiding this comment

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

nit: "to a recursive types"

Copy link
Member Author

Choose a reason for hiding this comment

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

Fixed.

\rollrt_x(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(x + i)^\ast \subst (\REC~i)^\ast])^\ast \\
&&& (\iff i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\
\unrollrt(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(\REC~i)^\ast \subst ((\TREC~\subtype^\ast).i)^\ast])^\ast \\[2ex]
&&& (\iff i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\
Copy link
Contributor

Choose a reason for hiding this comment

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

indenting here seems messy - it makes sense to put the side-condition on its own line if the previous line is too long to fit it alongside, but the the &&& then indents the side-condition past the end of the previous line, creating a scroll bar anyway.

Copy link
Member Author

Choose a reason for hiding this comment

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

Fixed.

\unrollrt(\TREC~\subtype^\ast) &=& \TREC~(\subtype[(\REC~i)^\ast \subst ((\TREC~\subtype^\ast).i)^\ast])^\ast \\[2ex]
&&& (\iff i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\
\rolldt_x(\rectype) &=& (\rectype'.i)^\ast & (\iff \rollrt_x(\rectype) = \rectype' = \TREC~\subtype^\ast \\
&&& \land i^\ast = 0 \cdots (|\subtype^\ast| - 1)) \\
Copy link
Contributor

Choose a reason for hiding this comment

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

nit: add whitespace after \land

Copy link
Member Author

Choose a reason for hiding this comment

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

Fixed.


* Then the type sequence is valid.

.. math::
Copy link
Contributor

Choose a reason for hiding this comment

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

probably should move each judgement to a separate line, and separate the premises of the first judgement across multiple lines

Copy link
Member Author

Choose a reason for hiding this comment

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

Moved rules to separate lines.

C \vdashcomptype \TSTRUCT~\X{ft}^\ast \ok
}

:math:`TARRAY~\fieldtype`
Copy link
Contributor

Choose a reason for hiding this comment

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

nit: TARRAY should be \TARRAY

Copy link
Member Author

Choose a reason for hiding this comment

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

Fixed.

Recursive Types
~~~~~~~~~~~~~~~

:ref:`Recursive types <syntax-rectype>` are validated for a specific :ref:`type index <syntax-typeidx>` that denotes the index of the type defined by the recursive group.
Copy link
Contributor

Choose a reason for hiding this comment

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

Do we want the additional index to be notated like this? It seems hard to read. I'd expect a judgement of either the form C |- rec subtype* : x or C, x |- rec subtype* ok instead of C |- rec subtype* ok (x)

Copy link
Member Author

Choose a reason for hiding this comment

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

It's essentially the former, but I wanted to keep the "ok" for consistency with the other type wf judgements. Moving it to the left doesn't look right to me, since it is not really a context.

Copy link
Contributor

Choose a reason for hiding this comment

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

What about C |-_{x} rec subtype* ok (i.e. a subscript)?

I'm personally quite negative about ok (x) because it looks unstructured/like a typo, and we don't normally use brackets this way.

Copy link
Member Author

Choose a reason for hiding this comment

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

Subscripts on turnstiles are usually used for distinguishing different relations or modes of relations. So I wouldn't want to put it there.

Not sure I follow what's so bad about ok(x) as a classifier, it's like an indexed ok. Note that I deliberately didn't put a space where you put it. :)

Copy link
Member Author

Choose a reason for hiding this comment

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

Oh, I get it, I just noticed that the macros mess up the spacing in the rendered version. That should be fixed now.

Copy link
Contributor

Choose a reason for hiding this comment

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

I think you pushed this on the other PR's branch

Copy link
Member Author

Choose a reason for hiding this comment

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

Oops, yes, pushed here now.

.. |vdashpackedtype| mathdef:: \xref{valid/types}{valid-packedtype}{\vdash}
.. |vdashstoragetype| mathdef:: \xref{valid/types}{valid-storagetype}{\vdash}
.. |vdashsubtype| mathdef:: \xref{valid/types}{valid-subtype}{\vdash}
.. |vdashrectype| mathdef:: \xref{valid/types}{valid-retype}{\vdash}
Copy link
Contributor

Choose a reason for hiding this comment

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

should this be valid-rectype instead of valid-retype?

Copy link
Member Author

Choose a reason for hiding this comment

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

Fixed.


* Or :math:`\heaptype_2` is a :ref:`type index <syntax-typeidx>` :math:`x_2`, and :math:`\heaptype_1` :ref:`matches <match-heaptype>` :math:`C.\CTYPES[x_2]`.
* Or :math:`\heaptype_1` is a :ref:`defined type <syntax-deftype>` which :ref:`expands <aux-expand-deftype>` to a :ref:`structure type <syntax-structtype>` and :math:`\heaptype_2` is :math:`STRUCT`.
Copy link
Contributor

Choose a reason for hiding this comment

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

should STRUCT, ARRAY and FUNC here be macros?

Copy link
Member Author

Choose a reason for hiding this comment

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

Fixed.


* The :ref:`result type <syntax-resulttype>` :math:`[t_{11}^\ast]` :ref:`matches <match-resulttype>` :math:`[t_{21}^\ast]`, and vice versa.
* The :ref:`result type <syntax-resulttype>` :math:`[t_{21}^\ast]` :ref:`matches <match-resulttype>` :math:`[t_{11}^\ast]`.
Copy link
Contributor

Choose a reason for hiding this comment

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

Just double checking, this change to allow function subtyping is part of the MVP?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, that's why we introduced final types.

}

.. note::
In future versions of WebAssembly, subtyping on function types may be relaxed to support co- and contra-variance.
A :ref:`storage type <syntax-storagetype>` :math:`\storagetype_1` matches a type :math:`\storagetype_2` if and only if:
Copy link
Contributor

Choose a reason for hiding this comment

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

This prose doesn't seem to have an accompanying math block

Copy link
Member Author

Choose a reason for hiding this comment

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

Because it's just injection. We could write out rules like

C ⊢ valtype_1 ≤ valtype_2
--------------------------
C ⊢ valtype_1 ≤ valtype_2

but that seems odd, and I omitted them elsewhere in similar situations.

@rossberg rossberg mentioned this pull request Jul 19, 2023
Copy link
Contributor

@conrad-watt conrad-watt left a comment

Choose a reason for hiding this comment

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

lgtm

@rossberg rossberg merged commit f58ae60 into main Jul 20, 2023
4 checks passed
@rossberg rossberg deleted the spec.valid-types branch July 20, 2023 06:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants