[spec] Add concrete ref types by rossberg · Pull Request #49 · WebAssembly/function-references

rossberg · 2021-06-24T18:51:27Z

Starting the spec text for this proposal by adding the new forms of ref types, text & binary format, and surrounding semantics.

(Includes a few minor spec typos that I discovered on the way and that I will upstream in another PR.)

rossberg · 2021-07-13T15:16:29Z

@conrad-watt, friendly ping.

conrad-watt · 2021-07-14T15:55:04Z

sorry for the delay, I'm on this now

conrad-watt

I believe the typing of ref.func also needs to be updated to have a return type that is the type of a specific function, rather than just funcref, but I can't comment directly on that part of the file.

conrad-watt · 2021-07-16T12:25:55Z

document/core/binary/types.rst

-   In future versions of WebAssembly, value types may include types denoted by :ref:`type indices <syntax-typeidx>`.
-   Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future.
+   In some places, possible types include both type constructors or types denoted by :ref:`type indices <syntax-typeidx>`.
+   Thus, the binary format for most type constructors corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, such that they can unambiguously occur in the same place as (positive) type indices.


Will the "most" here be fixed with a rebase?

(ref WebAssembly/spec#1338)

Yes, I merged upstream.

conrad-watt · 2021-07-16T12:27:44Z

document/core/syntax/modules.rst


 .. note::
-   In the current version of WebAssembly, only tables of element type |FUNCREF| can be initialized with an element segment.
+   In the current version of WebAssembly, only tables whose elements are function references can be initialized with an element segment.


should this note contain a ref to <syntax-reftype>?

conrad-watt · 2021-07-16T12:41:00Z

document/core/valid/modules.rst

 .. math::
   \frac{
-     \vdashmemtype \memtype \ok
+     C \vdashmemtype \memtype \ok


Since the memtype is just a limit, the context C isn't used. Could add it trivially to the limit validity judgement to make the shape match, or remove it here.

Uniformly added C to all wf and subtyping judgements. Also updated rules index.

conrad-watt · 2021-07-16T12:44:21Z

document/core/valid/types.rst

+* Or :math:`\heaptype_1` is a :ref:`type index <syntax-typeidx>` that defines a function type and :math:`\heaptype_2` is :math:`FUNC`.
+
+* Or :math:`\heaptype_1` is a :ref:`type index <syntax-typeidx>` that defines a function type :math:`\functype_1`, and :math:`\heaptype_2` is a :ref:`type index <syntax-typeidx>` that defines a function type :math:`\functype_2`, and :math:`\functype_1` :ref:`matches <match-functype>` :math:`\functype_2`.
+


The formatting here is broken for me, with judgments partially clipping into each other.

Tweaked formatting.

conrad-watt · 2021-07-16T12:44:34Z

document/core/valid/types.rst

-* Either both :math:`\reftype_1` and :math:`\reftype_2` are the same.
+* :math:`\NULL_1` is absent or :math:`\NULL_2` is present.

 .. math::


The formatting here is broken for me, with judgments partially clipping into each other.

conrad-watt · 2021-07-16T12:46:31Z

document/core/valid/types.rst

+   ~\\[-1ex]
+   \frac{
+     \begin{array}{@{}c@{}}
+     C \vdashresulttypematch [t_{11}^\ast] \matchesresulttype [t_{21}^ast]


various uses of ^ast instead of ^\ast should be fixed here

conrad-watt · 2021-07-16T12:48:02Z

document/core/appendix/properties.rst

 Soundness
 ---------

+.. todo:: need to ensure wf of nondet types and operate wrt semantic types


Could you give me the cliff-notes version of what's missing here (especially "nondet types")?

Backmerged refinements of these notes from follow-up PR.

rossberg

Comments addressed. Also moved the subtyping rules to a new section and updated the rule index.

rossberg · 2021-07-24T10:35:24Z

document/core/appendix/properties.rst

 Soundness
 ---------

+.. todo:: need to ensure wf of nondet types and operate wrt semantic types


Backmerged refinements of these notes from follow-up PR.

rossberg · 2021-07-24T10:43:38Z

document/core/binary/types.rst

-   In future versions of WebAssembly, value types may include types denoted by :ref:`type indices <syntax-typeidx>`.
-   Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future.
+   In some places, possible types include both type constructors or types denoted by :ref:`type indices <syntax-typeidx>`.
+   Thus, the binary format for most type constructors corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, such that they can unambiguously occur in the same place as (positive) type indices.


Yes, I merged upstream.

rossberg · 2021-07-24T10:46:30Z

document/core/syntax/modules.rst


 .. note::
-   In the current version of WebAssembly, only tables of element type |FUNCREF| can be initialized with an element segment.
+   In the current version of WebAssembly, only tables whose elements are function references can be initialized with an element segment.


rossberg · 2021-07-24T10:50:59Z

document/core/valid/modules.rst

 .. math::
   \frac{
-     \vdashmemtype \memtype \ok
+     C \vdashmemtype \memtype \ok


Uniformly added C to all wf and subtyping judgements. Also updated rules index.

rossberg · 2021-07-24T11:50:14Z

document/core/valid/types.rst

+* Or :math:`\heaptype_1` is a :ref:`type index <syntax-typeidx>` that defines a function type and :math:`\heaptype_2` is :math:`FUNC`.
+
+* Or :math:`\heaptype_1` is a :ref:`type index <syntax-typeidx>` that defines a function type :math:`\functype_1`, and :math:`\heaptype_2` is a :ref:`type index <syntax-typeidx>` that defines a function type :math:`\functype_2`, and :math:`\functype_1` :ref:`matches <match-functype>` :math:`\functype_2`.
+


Tweaked formatting.

rossberg · 2021-07-24T11:50:34Z

document/core/valid/types.rst

-* Either both :math:`\reftype_1` and :math:`\reftype_2` are the same.
+* :math:`\NULL_1` is absent or :math:`\NULL_2` is present.

 .. math::


rossberg · 2021-07-24T11:50:56Z

document/core/valid/types.rst

+   ~\\[-1ex]
+   \frac{
+     \begin{array}{@{}c@{}}
+     C \vdashresulttypematch [t_{11}^\ast] \matchesresulttype [t_{21}^ast]


conrad-watt

minor nit

conrad-watt · 2021-08-05T17:56:08Z

document/core/appendix/index-rules.rst

 ===============================================  ===============================================================================
-:ref:`External type <match-externtype>`          :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2`
-:ref:`Limits <match-limits>`                     :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2`
+:ref:`Number type <match-numtype>`               :math:`C \vdashnumtypematch \numtype_1 \matchesnumtype \numtype_2`


The various \matches* symbols don't appear to correctly link to the "Matching" section when clicked

Should be fixed now.

conrad-watt

LGTM

Just to check, when this is fully merged into the main spec, there will be a second round of reviews (hopefully with another fresh pair of eyes)? The changes are involved enough that I could definitely have missed something.

rossberg · 2021-08-06T16:31:34Z

Yes, that's the idea. Though how thorough that final review will be is hard to predict.

conrad-watt · 2021-08-06T16:47:41Z

document/core/util/macros.def

+.. |matchestabletype| mathdef:: \xref{valid/matching}{match-tabletype}{\leq}
+.. |matchesmemtype| mathdef:: \xref{valid/matching}{match-memtype}{\leq}
+.. |matchesglobaltype| mathdef:: \xref{valid/matching}{match-globaltype}{\leq}
+.. |matchesexterntype| mathdef:: \xref{exec/matching}{match-externtype}{\leq}


Oops, missed this - a few exec/matching should be valid/matching

Fix included in #52.

[spec] Add concrete ref types and surrounding semantics

96ae61e

rossberg requested a review from conrad-watt June 24, 2021 18:51

rossberg mentioned this pull request Jun 24, 2021

[spec] Fix a bunch of minor issues WebAssembly/spec#1338

Merged

conrad-watt mentioned this pull request Jun 28, 2021

[spec] New instructions #50

Closed

conrad-watt reviewed Jul 16, 2021

View reviewed changes

rossberg added 5 commits July 24, 2021 12:42

Merge branch 'master' into spec

5d5af81

Comments

bbd4bcb

Merge branch 'master' into spec

d76a4fc

Fix build

2bc77fe

Move subtyping into separate section

8aacfc2

rossberg commented Jul 24, 2021

View reviewed changes

Missing macro

cff9a73

conrad-watt reviewed Aug 5, 2021

View reviewed changes

Fix x-references to new matching file

99b47d5

conrad-watt approved these changes Aug 6, 2021

View reviewed changes

rossberg merged commit e8d2909 into master Aug 6, 2021

conrad-watt reviewed Aug 6, 2021

View reviewed changes

		* Or :math:`\heaptype_1` is a :ref:`type index <syntax-typeidx>` that defines a function type and :math:`\heaptype_2` is :math:`FUNC`.

		* Or :math:`\heaptype_1` is a :ref:`type index <syntax-typeidx>` that defines a function type :math:`\functype_1`, and :math:`\heaptype_2` is a :ref:`type index <syntax-typeidx>` that defines a function type :math:`\functype_2`, and :math:`\functype_1` :ref:`matches <match-functype>` :math:`\functype_2`.

Conversation

rossberg commented Jun 24, 2021

Uh oh!

rossberg commented Jul 13, 2021

Uh oh!

conrad-watt commented Jul 14, 2021

Uh oh!

conrad-watt left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rossberg left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

conrad-watt left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

conrad-watt left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rossberg commented Aug 6, 2021

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

conrad-watt left a comment •

edited

Loading