Skip to content

Commit

Permalink
Update Soundness appendix (WebAssembly#72)
Browse files Browse the repository at this point in the history
@rossberg
rossberg authored Oct 8, 2022
1 parent c4eef9a commit c86b2fb
Showing 16 changed files with 571 additions and 383 deletions.
38 changes: 20 additions & 18 deletions document/core/appendix/embedding.rst
View file
Original file line number Diff line number Diff line change
@@ -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:`semantic <syntax-type-sem>` 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 :ref:`dynamic <syntax-type-dyn>` 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:`semantic <syntax-type-sem>` :math:`\externtype_i` is :ref:`valid <valid-externtype>`.
6. Post-condition: each :ref:`dynamic <syntax-type-dyn>` :math:`\externtype_i` is :ref:`valid <valid-externtype>`.

.. 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:`semantic <syntax-type-sem>` 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 :ref:`dynamic <syntax-type-dyn>` 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:`semantic <syntax-type-sem>` :math:`\externtype'_i` is :ref:`valid <valid-externtype>`.
6. Post-condition: each :ref:`dynamic <syntax-type-dyn>` :math:`\externtype'_i` is :ref:`valid <valid-externtype>`.

.. math::
~ \\
@@ -257,7 +257,7 @@ Types
:math:`\F{type\_alloc}(\store, \functype) : (\store, \typeaddr)`
...........................................................................

1. Pre-condition: the :ref:`semantic <syntax-type-sem>` :math:`\functype` is :ref:`valid <valid-functype>`.
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`.

@@ -277,18 +277,18 @@ Functions

.. _embed-func-alloc:

:math:`\F{func\_alloc}(\store, \functype, \hostfunc) : (\store, \funcaddr)`
:math:`\F{func\_alloc}(\store, \typeaddr, \hostfunc) : (\store, \funcaddr)`
...........................................................................

1. Pre-condition: the :ref:`semantic <syntax-type-sem>` :math:`\functype` is :ref:`valid <valid-functype>`.
1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\functype` is :ref:`valid <valid-functype>`.

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`.
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`.

3. Return the new store paired with :math:`\funcaddr`.

.. math::
\begin{array}{lclll}
\F{func\_alloc}(S, \X{ft}, \X{code}) &=& (S', \X{a}) && (\iff \allochostfunc(S, \X{ft}, \X{code}) = S', \X{a}) \\
\F{func\_alloc}(S, \X{ta}, \X{code}) &=& (S', \X{a}) && (\iff \allochostfunc(S, \X{ta}, \X{code}) = S', \X{a}) \\
\end{array}
.. note::
@@ -302,13 +302,15 @@ Functions
:math:`\F{func\_type}(\store, \funcaddr) : \functype`
.....................................................

1. Return :math:`S.\SFUNCS[a].\FITYPE`.
1. Let :math:`\typeaddr` be the :ref:`type address <syntax-typeaddr>` :math:`S.\SFUNCS[a].\FITYPE`.

2. Post-condition: the returned :ref:`semantic <syntax-type-sem>` :ref:`function type <syntax-functype>` is :ref:`valid <valid-functype>`.
2. Return :math:`S.\STYPES[\typeaddr]`.

3. Post-condition: the returned :ref:`dynamic <syntax-type-dyn>` :ref:`function type <syntax-functype>` is :ref:`valid <valid-functype>`.

.. math::
\begin{array}{lclll}
\F{func\_type}(S, a) &=& S.\SFUNCS[a].\FITYPE \\
\F{func\_type}(S, a) &=& S.\STYPES[S.\SFUNCS[a].\FITYPE] \\
\end{array}
@@ -348,7 +350,7 @@ Tables
:math:`\F{table\_alloc}(\store, \tabletype) : (\store, \tableaddr, \reff)`
..........................................................................

1. Pre-condition: the :ref:`semantic <syntax-type-sem>` :math:`\tabletype` is :ref:`valid <valid-tabletype>`.
1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\tabletype` is :ref:`valid <valid-tabletype>`.

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`.

@@ -367,7 +369,7 @@ Tables

1. Return :math:`S.\STABLES[a].\TITYPE`.

2. Post-condition: the returned :ref:`semantic <syntax-type-sem>` :ref:`table type <syntax-tabletype>` is :ref:`valid <valid-tabletype>`.
2. Post-condition: the returned :ref:`dynamic <syntax-type-dyn>` :ref:`table type <syntax-tabletype>` is :ref:`valid <valid-tabletype>`.

.. math::
\begin{array}{lclll}
@@ -460,7 +462,7 @@ Memories
:math:`\F{mem\_alloc}(\store, \memtype) : (\store, \memaddr)`
................................................................

1. Pre-condition: the :ref:`semantic <syntax-type-sem>` :math:`\memtype` is :ref:`valid <valid-memtype>`.
1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\memtype` is :ref:`valid <valid-memtype>`.

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`.

@@ -479,7 +481,7 @@ Memories

1. Return :math:`S.\SMEMS[a].\MITYPE`.

2. Post-condition: the returned :ref:`semantic <syntax-type-sem>` :ref:`memory type <syntax-memtype>` is :ref:`valid <valid-memtype>`.
2. Post-condition: the returned :ref:`dynamic <syntax-type-dyn>` :ref:`memory type <syntax-memtype>` is :ref:`valid <valid-memtype>`.

.. math::
\begin{array}{lclll}
@@ -573,7 +575,7 @@ Globals
:math:`\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)`
............................................................................

1. Pre-condition: the :ref:`semantic <syntax-type-sem>` :math:`\globaltype` is :ref:`valid <valid-globaltype>`.
1. Pre-condition: the :ref:`dynamic <syntax-type-dyn>` :math:`\globaltype` is :ref:`valid <valid-globaltype>`.

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`.

@@ -592,7 +594,7 @@ Globals

1. Return :math:`S.\SGLOBALS[a].\GITYPE`.

2. Post-condition: the returned :ref:`semantic <syntax-type-sem>` :ref:`global type <syntax-globaltype>` is :ref:`valid <valid-globaltype>`.
2. Post-condition: the returned :ref:`dynamic <syntax-type-dyn>` :ref:`global type <syntax-globaltype>` is :ref:`valid <valid-globaltype>`.

.. math::
\begin{array}{lclll}
4 changes: 3 additions & 1 deletion document/core/appendix/index-rules.rst
View file
Original file line number Diff line number Diff line change
@@ -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 : \functype`
:ref:`Function <valid-func>` :math:`C \vdashfunc \func : \typeid`
: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,6 +58,7 @@ 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`
@@ -120,6 +121,7 @@ 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`
Loading

0 comments on commit c86b2fb

Please sign in to comment.