Merge pull request Wasm-DSL#7 from dhil/funcref-merge

Merge with function-references

Author: dhil

.github/workflows/ci-interpreter.yml

@@ -1,4 +1,4 @@
-2name: CI for interpreter & tests
+name: CI for interpreter & tests
 
 on:
   push:
@@ -21,7 +21,7 @@ jobs:
       - name: Setup OCaml
         uses: ocaml/setup-ocaml@v2
         with:
-          ocaml-compiler: 4.12.x
+          ocaml-compiler: 4.14.x
       - name: Setup OCaml tools
         run: opam install --yes ocamlbuild.0.14.0 ocamlfind.1.9.5 js_of_ocaml.4.0.0 js_of_ocaml-ppx.4.0.0
       - name: Setup Node.js
@@ -31,5 +31,6 @@ jobs:
       - name: Build interpreter
         run: cd interpreter && opam exec make
       - name: Run tests
+        # TODO: disable node.js run until it fully implements proposal
+        # run: cd interpreter && opam exec make JS=node ci
         run: cd interpreter && opam exec make test
-        #run: cd interpreter && opam exec make JS=node ci

README.md

@@ -1,5 +1,5 @@
-[![CI for specs](https://github.com/WebAssembly/spec/actions/workflows/ci-spec.yml/badge.svg)](https://github.com/WebAssembly/spec/actions/workflows/ci-spec.yml)
-[![CI for interpreter & tests](https://github.com/WebAssembly/spec/actions/workflows/ci-interpreter.yml/badge.svg)](https://github.com/WebAssembly/spec/actions/workflows/ci-interpreter.yml)
+[![CI for specs](https://github.com/wasmfx/specfx/actions/workflows/ci-spec.yml/badge.svg)](https://github.com/wasmfx/specfx/actions/workflows/ci-spec.yml)
+[![CI for interpreter & tests](https://github.com/wasmfx/specfx/actions/workflows/ci-interpreter.yml/badge.svg)](https://github.com/wasmfx/specfx/actions/workflows/ci-interpreter.yml)
 
 # Typed Continuations Proposal for WebAssembly
 

document/core/appendix/embedding.rst

@@ -167,7 +167,7 @@ Modules
 :math:`\F{module\_imports}(\module) : (\name, \name, \externtype)^\ast`
 .......................................................................
 
-1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with the :ref:`dynamic <syntax-type-dyn>` external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`.
+1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with the external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`.
 
 2. Let :math:`\import^\ast` be the :ref:`imports <syntax-import>` :math:`\module.\MIMPORTS`.
 
@@ -179,7 +179,7 @@ Modules
 
 5. Return the concatenation of all :math:`\X{result}_i`, in index order.
 
-6. Post-condition: each :ref:`dynamic <syntax-type-dyn>` :math:`\externtype_i` is :ref:`valid <valid-externtype>`.
+6. Post-condition: each :math:`\externtype_i` is :ref:`valid <valid-externtype>` under the empty :ref:`context <context>`.
 
 .. math::
    ~ \\
@@ -195,7 +195,7 @@ Modules
 :math:`\F{module\_exports}(\module) : (\name, \externtype)^\ast`
 ................................................................
 
-1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with the :ref:`dynamic <syntax-type-dyn>` external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`.
+1. Pre-condition: :math:`\module` is :ref:`valid <valid-module>` with the external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`.
 
 2. Let :math:`\export^\ast` be the :ref:`exports <syntax-export>` :math:`\module.\MEXPORTS`.
 
@@ -207,7 +207,7 @@ Modules
 
 5. Return the concatenation of all :math:`\X{result}_i`, in index order.
 
-6. Post-condition: each :ref:`dynamic <syntax-type-dyn>` :math:`\externtype'_i` is :ref:`valid <valid-externtype>`.
+6. Post-condition: each :math:`\externtype'_i` is :ref:`valid <valid-externtype>` under the empty :ref:`context <context>`.
 
 .. math::
    ~ \\
@@ -246,29 +246,6 @@ Module Instances
    \end{array}
 
 
-.. index:: type, type instance, function type
-.. _embed-type:
-
-Types
-~~~~~
-
-.. _embed-type-alloc:
-
-:math:`\F{type\_alloc}(\store, \functype) : (\store, \typeaddr)`
-...........................................................................
-
-1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\functype` is :ref:`valid <valid-functype>`.
-
-2. Let :math:`\typeaddr` be the result of :ref:`allocating a type <alloc-type>` in :math:`\store` for :ref:`function type <syntax-functype>` :math:`\functype`.
-
-3. Return the new store paired with :math:`\typeaddr`.
-
-.. math::
-   \begin{array}{lclll}
-   \F{type\_alloc}(S, \X{ft}) &=& (S', \X{a}) && (\iff \alloctype(S, \X{ft}) = S', \X{a}) \\
-   \end{array}
-
-
 .. index:: function, host function, function address, function instance, function type, store
 .. _embed-func:
 
@@ -277,12 +254,12 @@ Functions
 
 .. _embed-func-alloc:
 
-:math:`\F{func\_alloc}(\store, \typeaddr, \hostfunc) : (\store, \funcaddr)`
+:math:`\F{func\_alloc}(\store, \functype, \hostfunc) : (\store, \funcaddr)`
 ...........................................................................
 
-1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\functype` is :ref:`valid <valid-functype>`.
+1. Pre-condition: the :math:`\functype` is :ref:`valid <valid-functype>` under the empty :ref:`context <context>`.
 
-2. Let :math:`\funcaddr` be the result of :ref:`allocating a host function <alloc-func>` in :math:`\store` with :ref:`type address <syntax-typeaddr>` :math:`\typeaddr` and host function code :math:`\hostfunc`.
+2. Let :math:`\funcaddr` be the result of :ref:`allocating a host function <alloc-func>` in :math:`\store` with :ref:`function type <syntax-functype>` :math:`\functype` and host function code :math:`\hostfunc`.
 
 3. Return the new store paired with :math:`\funcaddr`.
 
@@ -302,15 +279,15 @@ Functions
 :math:`\F{func\_type}(\store, \funcaddr) : \functype`
 .....................................................
 
-1. Let :math:`\typeaddr` be the :ref:`type address <syntax-typeaddr>` :math:`S.\SFUNCS[a].\FITYPE`.
+1. Let :math:`\functype` be the :ref:`function type <syntax-functype>` :math:`S.\SFUNCS[a].\FITYPE`.
 
-2. Return :math:`S.\STYPES[\typeaddr]`.
+2. Return :math:`\functype`.
 
-3. Post-condition: the returned :ref:`dynamic <syntax-type-dyn>` :ref:`function type <syntax-functype>` is :ref:`valid <valid-functype>`.
+3. Post-condition: the returned :ref:`function type <syntax-functype>` is :ref:`valid <valid-functype>`.
 
 .. math::
    \begin{array}{lclll}
-   \F{func\_type}(S, a) &=& S.\STYPES[S.\SFUNCS[a].\FITYPE] \\
+   \F{func\_type}(S, a) &=& S.\SFUNCS[a].\FITYPE \\
    \end{array}
 
 
@@ -350,7 +327,7 @@ Tables
 :math:`\F{table\_alloc}(\store, \tabletype, \reff) : (\store, \tableaddr)`
 ..........................................................................
 
-1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\tabletype` is :ref:`valid <valid-tabletype>`.
+1. Pre-condition: the :math:`\tabletype` is :ref:`valid <valid-tabletype>` under the empty :ref:`context <context>`.
 
 2. Let :math:`\tableaddr` be the result of :ref:`allocating a table <alloc-table>` in :math:`\store` with :ref:`table type <syntax-tabletype>` :math:`\tabletype` and initialization value :math:`\reff`.
 
@@ -369,7 +346,7 @@ Tables
 
 1. Return :math:`S.\STABLES[a].\TITYPE`.
 
-2. Post-condition: the returned :ref:`dynamic <syntax-type-dyn>` :ref:`table type <syntax-tabletype>` is :ref:`valid <valid-tabletype>`.
+2. Post-condition: the returned :ref:`table type <syntax-tabletype>` is :ref:`valid <valid-tabletype>` under the empty :ref:`context <context>`.
 
 .. math::
    \begin{array}{lclll}
@@ -462,7 +439,7 @@ Memories
 :math:`\F{mem\_alloc}(\store, \memtype) : (\store, \memaddr)`
 ................................................................
 
-1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\memtype` is :ref:`valid <valid-memtype>`.
+1. Pre-condition: the :math:`\memtype` is :ref:`valid <valid-memtype>` under the empty :ref:`context <context>`.
 
 2. Let :math:`\memaddr` be the result of :ref:`allocating a memory <alloc-mem>` in :math:`\store` with :ref:`memory type <syntax-memtype>` :math:`\memtype`.
 
@@ -481,7 +458,7 @@ Memories
 
 1. Return :math:`S.\SMEMS[a].\MITYPE`.
 
-2. Post-condition: the returned :ref:`dynamic <syntax-type-dyn>` :ref:`memory type <syntax-memtype>` is :ref:`valid <valid-memtype>`.
+2. Post-condition: the returned :ref:`memory type <syntax-memtype>` is :ref:`valid <valid-memtype>` under the empty :ref:`context <context>`.
 
 .. math::
    \begin{array}{lclll}
@@ -575,7 +552,7 @@ Globals
 :math:`\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)`
 ............................................................................
 
-1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\globaltype` is :ref:`valid <valid-globaltype>`.
+1. Pre-condition: the :math:`\globaltype` is :ref:`valid <valid-globaltype>` under the empty :ref:`context <context>`.
 
 2. Let :math:`\globaladdr` be the result of :ref:`allocating a global <alloc-global>` in :math:`\store` with :ref:`global type <syntax-globaltype>` :math:`\globaltype` and initialization value :math:`\val`.
 
@@ -594,7 +571,7 @@ Globals
 
 1. Return :math:`S.\SGLOBALS[a].\GITYPE`.
 
-2. Post-condition: the returned :ref:`dynamic <syntax-type-dyn>` :ref:`global type <syntax-globaltype>` is :ref:`valid <valid-globaltype>`.
+2. Post-condition: the returned :ref:`global type <syntax-globaltype>` is :ref:`valid <valid-globaltype>` under the empty :ref:`context <context>`.
 
 .. math::
    \begin{array}{lclll}
@@ -638,3 +615,29 @@ Globals
    \F{global\_write}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GITYPE = \MVAR~t \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\
    \F{global\_write}(S, a, v) &=& \ERROR && (\otherwise) \\
    \end{array}
+
+
+.. index:: reference, reference type
+.. _embed-ref:
+
+References
+~~~~~~~~~~
+
+:math:`\F{ref\_type}(\store, \reff) : \reftype`
+...............................................
+
+1. Pre-condition: the :ref:`reference <syntax-ref>` :math:`\reff` is :ref:`valid <valid-val>` under store :math:`S`.
+
+2. Return the :ref:`reference type <syntax-reftype>` :math:`t` with which :math:`\reff` is valid.
+
+3. Post-condition: the returned :ref:`reference type <syntax-reftype>` is :ref:`valid <valid-reftype>` under the empty :ref:`context <context>`.
+
+.. math::
+   \begin{array}{lclll}
+   \F{ref\_type}(S, r) &=& t && (\iff S \vdashval r : t) \\
+   \end{array}
+
+.. note::
+   In future versions of WebAssembly,
+   not all references may carry precise type information at run time.
+   In such cases, this function may return a less precise supertype.

document/core/appendix/index-instructions.py

@@ -280,9 +280,9 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\REFNULL~\X{ht}', r'\hex{D0}', r'[] \to [(\REF~\NULL~\X{ht})]', r'valid-ref.null', r'exec-ref.null'),
     Instruction(r'\REFISNULL', r'\hex{D1}', r'[(\REF~\NULL~\X{ht})] \to [\I32]', r'valid-ref.is_null', r'exec-ref.is_null'),
     Instruction(r'\REFFUNC~x', r'\hex{D2}', r'[] \to [\FUNCREF]', r'valid-ref.func', r'exec-ref.func'),
-    Instruction(r'\REFASNONNULL', r'\hex{D3}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'),
-    Instruction(r'\BRONNULL~l', r'\hex{D4}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'),
-    Instruction(None, r'\hex{D5}'),
+    Instruction(None, r'\hex{D3}'),
+    Instruction(r'\REFASNONNULL', r'\hex{D4}', r'[(\REF~\NULL~\X{ht})] \to [(\REF~\X{ht})]', r'valid-ref.as_non_null', r'exec-ref.as_non_null'),
+    Instruction(r'\BRONNULL~l', r'\hex{D5}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast~(\REF~\X{ht})]', r'valid-br_on_null', r'exec-br_on_null'),
     Instruction(r'\BRONNONNULL~l', r'\hex{D6}', r'[t^\ast~(\REF~\NULL~\X{ht})] \to [t^\ast]', r'valid-br_on_non_null', r'exec-br_on_non_null'),
     Instruction(None, r'\hex{D7}'),
     Instruction(None, r'\hex{D8}'),

document/core/appendix/index-rules.rst

@@ -29,7 +29,7 @@ Construct                                        Judgement
 :ref:`Instruction <valid-instr>`                 :math:`S;C \vdashinstr \instr : \functype`
 :ref:`Instruction sequence <valid-instr-seq>`    :math:`S;C \vdashinstrseq \instr^\ast : \functype`
 :ref:`Expression <valid-expr>`                   :math:`C \vdashexpr \expr : \resulttype`
-:ref:`Function <valid-func>`                     :math:`C \vdashfunc \func : \typeid`
+:ref:`Function <valid-func>`                     :math:`C \vdashfunc \func : \functype`
 :ref:`Local <valid-local>`                       :math:`C \vdashlocal \local : \localtype`
 :ref:`Table <valid-table>`                       :math:`C \vdashtable \table : \tabletype`
 :ref:`Memory <valid-mem>`                        :math:`C \vdashmem \mem : \memtype`
@@ -58,7 +58,6 @@ Construct                                        Judgement
 :ref:`Value <valid-val>`                         :math:`S \vdashval \val : \valtype`
 :ref:`Result <valid-result>`                     :math:`S \vdashresult \result : \resulttype`
 :ref:`External value <valid-externval>`          :math:`S \vdashexternval \externval : \externtype`
-:ref:`Type instance <valid-typeinst>`            :math:`S \vdashtypeinst \typeinst \ok`
 :ref:`Function instance <valid-funcinst>`        :math:`S \vdashfuncinst \funcinst : \functype`
 :ref:`Table instance <valid-tableinst>`          :math:`S \vdashtableinst \tableinst : \tabletype`
 :ref:`Memory instance <valid-meminst>`           :math:`S \vdashmeminst \meminst : \memtype`
@@ -122,7 +121,6 @@ Store Extension
 ===============================================  ===============================================================================
 Construct                                        Judgement
 ===============================================  ===============================================================================
-:ref:`Type instance <extend-typeinst>`           :math:`\vdashtypeinstextends \typeinst_1 \extendsto \typeinst_2`
 :ref:`Function instance <extend-funcinst>`       :math:`\vdashfuncinstextends \funcinst_1 \extendsto \funcinst_2`
 :ref:`Table instance <extend-tableinst>`         :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2`
 :ref:`Memory instance <extend-meminst>`          :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2`

document/core/appendix/index-types.rst

@@ -16,10 +16,10 @@ Category                                  Constructor
 (reserved)                                                                             :math:`\hex{7A}` .. :math:`\hex{71}`
 :ref:`Heap type <syntax-heaptype>`        |FUNC|                                       :math:`\hex{70}` (-16 as |Bs7|)
 :ref:`Heap type <syntax-heaptype>`        |EXTERN|                                     :math:`\hex{6F}` (-17 as |Bs7|)
-(reserved)                                                                             :math:`\hex{6E}` .. :math:`\hex{6D}`
-:ref:`Reference type <syntax-reftype>`    |REF| |NULL|                                 :math:`\hex{6C}` (-20 as |Bs7|)
-:ref:`Reference type <syntax-reftype>`    |REF|                                        :math:`\hex{6B}` (-21 as |Bs7|)
-(reserved)                                                                             :math:`\hex{6A}` .. :math:`\hex{61}`
+(reserved)                                                                             :math:`\hex{6E}` .. :math:`\hex{65}`
+:ref:`Reference type <syntax-reftype>`    |REF|                                        :math:`\hex{64}` (-28 as |Bs7|)
+:ref:`Reference type <syntax-reftype>`    |REF| |NULL|                                 :math:`\hex{63}` (-29 as |Bs7|)
+(reserved)                                                                             :math:`\hex{62}` .. :math:`\hex{61}`
 :ref:`Function type <syntax-functype>`    :math:`[\valtype^\ast] \toF[\valtype^\ast]`  :math:`\hex{60}` (-32 as |Bs7|)
 (reserved)                                                                             :math:`\hex{5F}` .. :math:`\hex{41}`
 :ref:`Result type <syntax-resulttype>`    :math:`[\epsilon]`                           :math:`\hex{40}` (-64 as |Bs7|)