[spec] Fix and clean up invariants for host functions (#563)

document/core/appendix/index-rules.rst

@@ -44,6 +44,9 @@ Typing of Runtime Constructs
 ===============================================  ===============================================================================
 Construct                                        Judgement
 ===============================================  ===============================================================================
+:ref:`Value <valid-val>`                         :math:`\vdashval \val : \valtype`
+:ref:`Result <valid-result>`                     :math:`\vdashresult \result : \resulttype`
+:ref:`External value <valid-externval>`          :math:`S \vdashexternval \externval : \externtype`
 :ref:`Module instruction <valid-moduleinstr>`    :math:`S \vdashmoduleinstr \moduleinstr \ok`
 :ref:`Function instance <valid-funcinst>`        :math:`S \vdashfuncinst \funcinst : \resulttype`
 :ref:`Table instance <valid-tableinst>`          :math:`S \vdashtableinst \tableinst : \tabletype`
@@ -55,8 +58,6 @@ Construct                                        Judgement
 :ref:`Configuration <valid-config>`              :math:`\vdashconfig \config \ok`
 :ref:`Thread <valid-thread>`                     :math:`S;\resulttype^? \vdashthread \thread : \resulttype^?`
 :ref:`Frame <valid-frame>`                       :math:`S \vdashframe \frame : C`
-:ref:`Value <valid-val>`                         :math:`\vdashval \val : \valtype`
-:ref:`External value <valid-externval>`          :math:`S \vdashexternval \externval : \externtype`
 ===============================================  ===============================================================================
 
 

document/core/appendix/properties.rst

@@ -20,6 +20,58 @@ The typing rules defining WebAssembly :ref:`validation <valid>` only cover the *
 In order to state and prove soundness precisely, the typing rules must be extended to the *dynamic* components of the abstract :ref:`runtime <syntax-runtime>`, that is, the :ref:`store <syntax-store>`, :ref:`configurations <syntax-config>`, and :ref:`administrative instructions <syntax-instr-admin>` as well as :ref:`module instructions <valid-moduleinstr>`. [#pldi2017]_
 
 
+.. index:: value, value type, result, result type, trap
+.. _valid-val:
+.. _valid-result:
+
+Values and Results
+~~~~~~~~~~~~~~~~~~
+
+:ref:`Values <syntax-val>` and :ref:`results <syntax-result>` can be classified by :ref:`value types <syntax-valtype>` and :ref:`result types <syntax-resulttype>` as follows.
+
+:ref:`Values <syntax-val>` :math:`t.\CONST~c`
+.............................................
+
+* The value is valid with :ref:`value type <syntax-valtype>` :math:`t`.
+
+.. math::
+   \frac{
+   }{
+     \vdashval t.\CONST~c : t
+   }
+
+
+:ref:`Results <syntax-result>` :math:`\val^\ast`
+................................................
+
+* For each :ref:`value <syntax-val>` :math:`\val_i` in :math:`\val^\ast`:
+
+  * The value :math:`\val_i` is :ref:`valid <valid-val>` with some :ref:`value type <syntax-valtype>` :math:`t_i`.
+
+* Let :math:`t^\ast` be the concatenation of all :math:`t_i`.
+
+* Then the result is valid with :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`.
+
+.. math::
+   \frac{
+     (\vdashval \val : t)^\ast
+   }{
+     \vdashresult \val^\ast : [t^\ast]
+   }
+
+
+:ref:`Results <syntax-result>` :math:`\TRAP`
+............................................
+
+* The result is valid with :ref:`result type <syntax-resulttype>` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`value types <syntax-valtype>`.
+
+.. math::
+   \frac{
+   }{
+     \vdashresult \TRAP : [t^\ast]
+   }
+
+
 .. _module-context:
 .. _valid-store:
 
@@ -76,8 +128,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 .. index:: function type, function instance
 .. _valid-funcinst:
 
-:ref:`Function Instance <syntax-funcinst>` :math:`\{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\}`
-......................................................................................................................
+:ref:`Function Instances <syntax-funcinst>` :math:`\{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\}`
+.......................................................................................................................
 
 * The :ref:`function type <syntax-functype>` :math:`\functype` must be :ref:`valid <valid-functype>`.
 
@@ -99,11 +151,59 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
    }
 
 
+.. index:: function type, function instance, host function
+.. _valid-hostfuncinst:
+
+:ref:`Host Function Instances <syntax-funcinst>` :math:`\{\FITYPE~\functype, \FIHOSTCODE~\X{hf}\}`
+..................................................................................................
+
+* The :ref:`function type <syntax-functype>` :math:`\functype` must be :ref:`valid <valid-functype>`.
+
+* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type <syntax-functype>` :math:`\functype`.
+
+* For every possible :ref:`valid <valid-store>` :ref:`store <syntax-store>` :math:`S_1` :ref:`extending <extend-store>` :math:`S` and every sequence :math:`\val^\ast` of :ref:`values <syntax-val>` whose :ref:`types <valid-val>` coincide with :math:`t_1^\ast`:
+
+  * There must exist a :ref:`valid <valid-store>` :ref:`store <syntax-store>` :math:`S_2` :ref:`extending <extend-store>` :math:`S_1` and a :ref:`result <syntax-result>` :math:`\result` whose :ref:`type <valid-result>` coincides with :math:`[t_2^\ast]` such that:
+
+    * :ref:`Executing <exec-invoke-host>` :math:`\X{hf}` in store :math:`S_1` with arguments :math:`\val^\ast` produces :math:`\result` and store :math:`S_2`.
+
+* Then the function instance is valid with :ref:`function type <syntax-functype>` :math:`\functype`.
+
+.. math::
+   \frac{
+     \begin{array}[b]{@{}l@{}}
+     \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok \\
+     \end{array}
+     \quad
+     \begin{array}[b]{@{}l@{}}
+     \forall S_1, \val^\ast,~
+       {\vdashstore S_1 \ok} \wedge
+       {\vdashstoreextends S \extendsto S_1} \wedge
+       {\vdashresult \val^\ast : [t_1^\ast]}
+       \Longrightarrow {} \\ \qquad
+     \exists S_2, \result,~
+       {\vdashstore S_2 \ok} \wedge
+       {\vdashstoreextends S_1 \extendsto S_2} \wedge
+       {\vdashresult \result : [t_2^\ast]} \wedge
+       \X{hf}(S_1; \val^\ast) = S_2; \result
+     \end{array}
+   }{
+     S \vdashfuncinst \{\FITYPE~[t_1^\ast] \to [t_2^\ast], \FIHOSTCODE~\X{hf}\} : [t_1^\ast] \to [t_2^\ast]
+   }
+
+.. note::
+   This rule states that, if appropriate pre-conditions about store and arguments are satisfied, then executing the host function must satisfy appropriate post-conditions about store and results.
+   The post-conditions match the ones in the :ref:`execution rule <exec-invoke-host>` for invoking host functions.
+
+   Any store under which the function is invoked is assumed to be an extension of the current store.
+   That way, the function itself is able to make sufficient assumptions about future stores.
+
+
 .. index:: table type, table instance, limits, function address
 .. _valid-tableinst:
 
-:ref:`Table Instance <syntax-tableinst>` :math:`\{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \}`
-.............................................................................................
+:ref:`Table Instances <syntax-tableinst>` :math:`\{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \}`
+..............................................................................................
 
 * For each optional :ref:`function address <syntax-funcaddr>` :math:`\X{fa}^?_i` in the table elements :math:`(\X{fa}^?)^n`:
 
@@ -128,8 +228,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 .. index:: memory type, memory instance, limits, byte
 .. _valid-meminst:
 
-:ref:`Memory Instance <syntax-meminst>` :math:`\{ \MIDATA~b^n, \MIMAX~m^? \}`
-.............................................................................
+:ref:`Memory Instances <syntax-meminst>` :math:`\{ \MIDATA~b^n, \MIMAX~m^? \}`
+..............................................................................
 
 * The :ref:`limits <syntax-limits>` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid <valid-limits>`.
 
@@ -146,8 +246,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 .. index:: global type, global instance, value, mutability
 .. _valid-globalinst:
 
-:ref:`Global Instance <syntax-globalinst>` :math:`\{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \}`
-...........................................................................................
+:ref:`Global Instances <syntax-globalinst>` :math:`\{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \}`
+............................................................................................
 
 * The global instance is valid with :ref:`global type <syntax-globaltype>` :math:`\mut~t`.
 
@@ -161,8 +261,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 .. index:: external type, export instance, name, external value
 .. _valid-exportinst:
 
-:ref:`Export Instance <syntax-exportinst>` :math:`\{ \EINAME~\name, \EIVALUE~\externval \}`
-......................................................................................................
+:ref:`Export Instances <syntax-exportinst>` :math:`\{ \EINAME~\name, \EIVALUE~\externval \}`
+.......................................................................................................
 
 * The :ref:`external value <syntax-externval>` :math:`\externval` must be :ref:`valid <valid-externval>` with some :ref:`external type <syntax-externtype>` :math:`\externtype`.
 
@@ -179,8 +279,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 .. index:: module instance, context
 .. _valid-moduleinst:
 
-:ref:`Module Instance <syntax-moduleinst>` :math:`\moduleinst`
-..............................................................
+:ref:`Module Instances <syntax-moduleinst>` :math:`\moduleinst`
+...............................................................
 
 * Each :ref:`function type <syntax-functype>` :math:`\functype_i` in :math:`\moduleinst.\MITYPES` must be :ref:`valid <valid-functype>`.
 
@@ -254,7 +354,7 @@ Configuration Validity
 To relate the WebAssembly :ref:`type system <valid>` to its :ref:`execution semantics <exec>`, the :ref:`typing rules for instructions <valid-instr>` must be extended to :ref:`configurations <syntax-config>` :math:`S;T`,
 which relates the :ref:`store <syntax-store>` to execution :ref:`threads <syntax-thread>`.
 
-Threads may either be regular threads executing sequences of :ref:`instructions <syntax-instr>`, or module threads executing :ref:`module instructions <synax-moduleinstr>` that represent an ongoing module instantiation.
+Threads may either be regular threads executing sequences of :ref:`instructions <syntax-instr>`, or module threads executing :ref:`module instructions <syntax-moduleinstr>` that represent an ongoing module instantiation.
 Regular threads are classified by their :ref:`result type <syntax-resulttype>`.
 Module threads on the other hand have no result, not even an empty one.
 Consequently, threads and configurations are cumutavily classified by an *optional* result type, where :math:`\epsilon` classifies the thread as a module computation.
@@ -339,7 +439,7 @@ Finally, :ref:`frames <syntax-frame>` are classified with *frame contexts*, whic
 :ref:`Frames <syntax-frame>` :math:`\{\ALOCALS~\val^\ast, \AMODULE~\moduleinst\}`
 .................................................................................
 
-* The :ref:`module instance <syntax-moduleinst>` :math:`\moduleinst` must be :ref:`valid <valid-moduleinst>` with some :ref:`module context <module context>` :math:`C`.
+* The :ref:`module instance <syntax-moduleinst>` :math:`\moduleinst` must be :ref:`valid <valid-moduleinst>` with some :ref:`module context <module-context>` :math:`C`.
 
 * Each :ref:`value <syntax-val>` :math:`\val_i` in :math:`\val^\ast` must be :ref:`valid <valid-val>` with some :ref:`value type <syntax-valtype>` :math:`t_i`.
 
@@ -359,29 +459,14 @@ Finally, :ref:`frames <syntax-frame>` are classified with *frame contexts*, whic
    }
 
 
-.. index:: value, value type
-.. _valid-val:
-
-:ref:`Values <syntax-val>` :math:`t.\CONST~c`
-.............................................
-
-* The value is valid with :ref:`value type <syntax-valtype>` :math:`t`.
-
-.. math::
-   \frac{
-   }{
-     \vdashval t.\CONST~c : t
-   }
-
-
 .. index:: administrative instruction, value type, context, store
 .. _valid-instr-admin:
 
 Administrative Instructions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Typing rules for :ref:`administrative instructions <syntax-instr-admin>` are specified as follows.
-In addition to the :ref:`context <contxt>` :math:`C`, typing of these instructions is defined under a given :ref:`store <syntax-store>` :math:`S`.
+In addition to the :ref:`context <context>` :math:`C`, typing of these instructions is defined under a given :ref:`store <syntax-store>` :math:`S`.
 To that end, all previous typing judgements :math:`C \vdash \X{prop}` are generalized to include the store, as in :math:`S; C \vdash \X{prop}`, by implicitly adding :math:`S` to all rules -- :math:`S` is never modified by the pre-existing rules, but it is accessed in the new rules for :ref:`administrative instructions <valid-instr-admin>` and  :ref:`module instructions <valid-moduleinstr>` given below.
 
 

document/core/exec/instructions.rst

@@ -1101,31 +1101,24 @@ Furthermore, the resulting store must be :ref:`valid <valid-store>`, i.e., all d
    ~\\[-1ex]
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; \val_1^n~(\INVOKE~a) &\stepto& S'; \val_2^m
+   S; \val^n~(\INVOKE~a) &\stepto& S'; \result
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
-     (\mbox{if} & S.\SFUNCS[a] = \{ \FITYPE~[t_1^n] \to [t_2^m], \FIHOSTCODE~\dots \} \\
-     \wedge & \val_1^n = (t_1.\CONST~c_1)^n \\
-     \wedge & \val_2^m = (t_2.\CONST~c_2)^m \\
-     \wedge & \vdashstoreextends S \extendsto S' \\
-     \wedge & \vdashstore S' \ok) \\
-     \end{array}
-   \\[1ex]
-   \begin{array}{lcl@{\qquad}l}
-   S; \val^n~(\INVOKE~a) &\stepto& S'; \TRAP
-   \end{array}
-   \\ \qquad
-     \begin{array}[t]{@{}r@{~}l@{}}
-     (\mbox{if} & S.\SFUNCS[a] = \{ \FITYPE~\X{ft}, \FIHOSTCODE~\dots \} \\ 
-     \wedge & \vdashstoreextends S \extendsto S' \\
-     \wedge & \vdashstore S' \ok) \\
+     (\mbox{if} & S.\SFUNCS[a] = \{ \FITYPE~[t_1^n] \to [t_2^m], \FIHOSTCODE~\X{hf} \} \\
+     \wedge & \X{hf}(S; \val^n) = S'; \result) \\
      \end{array} \\
    \end{array}
 
-Here, :math:`S \extendsto S'` expresses that the new store :math:`S'` is an :ref:`extension <extend>` of :math:`S`.
-Moreover, :math:`\vdashstore S' \ok` restricts :math:`S'` to be a :ref:`valid <valid-store>` store.
-Both notions are defined in the :ref:`Appendix <properties>`.
+Here, :math:`\X{hf}(S; \val^n)` denotes the implementation-defined execution of host function :math:`\X{hf}` in current store :math:`S` with arguments :math:`\val^n`.
+The outcome is a pair of a modified store :math:`S'` and a :ref:`result <syntax-result>`.
+
+For a WebAssembly implementation to be :ref:`sound <soundness>` in the presence of host functions,
+every :ref:`host function instance <syntax-funcinst>` must be :ref:`valid <valid-hostfuncinst>`,
+which means that it adheres to suitable pre- and post-conditions:
+under a :ref:`valid store <valid-store>` :math:`S`, and given arguments :math:`\val^n` matching the ascribed parameter types :math:`t_1^n`,
+executing the host function must produce a valid store :math:`S'` that is an :ref:`extension <extend-store>` of :math:`S` and a result matching the ascribed return types :math:`t_2^m`.
+All these notions are made precise in the :ref:`Appendix <soundness>`.
 
 .. note::
    A host function can call back into WebAssembly by :ref:`invoking <exec-invocation>` a function :ref:`exported <syntax-export>` from a :ref:`module <syntax-module>`.

document/core/exec/modules.rst

@@ -729,8 +729,8 @@ The values :math:`\val_{\F{res}}^m` are returned as the results of the invocatio
 .. math::
    ~\\[-1ex]
    \begin{array}{@{}lcl}
-   \invoke(S, \funcaddr, \val^n) &=& \val_{\F{res}}^m / \TRAP \\
+   \invoke(S, \funcaddr, \val^n) &=& \result \\
      &(\iff & S.\SFUNCS[\funcaddr].\FITYPE = [t_1^n] \to [t_2^m] \\
      &\wedge& \val^n = (t_1.\CONST~c)^n \\
-     &\wedge& S; \val^n~(\INVOKE~\funcaddr) \stepto^\ast S'; \val_{\F{res}}^m / \TRAP) \\
+     &\wedge& S; \val^n~(\INVOKE~\funcaddr) \stepto^\ast S'; \result) \\
    \end{array}

document/core/exec/runtime.rst

@@ -30,6 +30,27 @@ It is convenient to reuse the same notation as for the |CONST| :ref:`instruction
    \end{array}
 
 
+.. index:: ! result, value, trap
+   pair: abstract syntax; result
+.. _syntax-result:
+
+Results
+~~~~~~~
+
+A *result* is the outcome of a computation.
+It is either a sequence of :ref:`values <syntax-val>` or a :ref:`trap <syntax-trap>`.
+
+.. math::
+   \begin{array}{llcl}
+   \production{(result)} & \result &::=&
+     \val^\ast \\&&|&
+     \TRAP
+   \end{array}
+
+.. note::
+   In the current version of WebAssembly, a result can consist of at most one value.
+
+
 .. index:: ! store, function instance, table instance, memory instance, global instance, module, allocation
    pair: abstract syntax; store
 .. _syntax-store:
@@ -171,7 +192,8 @@ The module instance is used to resolve references to other definitions during ex
 A *host function* is a function expressed outside WebAssembly but passed to a :ref:`module <syntax-module>` as an :ref:`import <syntax-import>`.
 The definition and behavior of host functions are outside the scope of this specification.
 For the purpose of this specification, it is assumed that when :ref:`invoked <exec-invoke-host>`,
-a host function behaves non-deterministically.
+a host function behaves non-deterministically,
+but within certain :ref:`constraints <exec-invoke-host>` that ensure the integrity of the runtime.
 
 .. note::
    Function instances are immutable, and their identity is not observable by WebAssembly code.

document/core/util/math.def

@@ -819,9 +819,13 @@
 .. |DO| mathdef:: \xref{exec/runtime}{syntax-do}{\K{do}}
 
 
-.. Values & Administrative Instructions, non-terminals
+.. Values & Results, non-terminals
 
 .. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}}
+.. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}}
+
+
+.. Administrative Instructions, non-terminals
 
 .. |moduleinstr| mathdef:: \xref{exec/runtime}{syntax-moduleinstr}{\X{moduleinstr}}
 
@@ -938,6 +942,9 @@
 .. |vdashadmininstr| mathdef:: \xref{appendix/properties}{valid-instr-admin}{\vdash}
 .. |vdashmoduleinstr| mathdef:: \xref{appendix/properties}{valid-moduleinstr}{\vdash}
 
+.. |vdashval| mathdef:: \xref{appendix/properties}{valid-val}{\vdash}
+.. |vdashresult| mathdef:: \xref{appendix/properties}{valid-result}{\vdash}
+
 .. |vdashfuncinst| mathdef:: \xref{appendix/properties}{valid-funcinst}{\vdash}
 .. |vdashtableinst| mathdef:: \xref{appendix/properties}{valid-tableinst}{\vdash}
 .. |vdashmeminst| mathdef:: \xref{appendix/properties}{valid-meminst}{\vdash}
@@ -949,7 +956,6 @@
 .. |vdashconfig| mathdef:: \xref{appendix/properties}{valid-config}{\vdash}
 .. |vdashthread| mathdef:: \xref{appendix/properties}{valid-thread}{\vdash}
 .. |vdashframe| mathdef:: \xref{appendix/properties}{valid-frame}{\vdash}
-.. |vdashval| mathdef:: \xref{appendix/properties}{valid-val}{\vdash}
 
 .. |vdashfuncinstextends| mathdef:: \xref{appendix/properties}{extend-funcinst}{\vdash}
 .. |vdashtableinstextends| mathdef:: \xref{appendix/properties}{extend-tableinst}{\vdash}