Convert exec/runtime

document/core/appendix/properties.rst

@@ -400,7 +400,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 .. index:: function type, function instance, host function
 .. _valid-hostfuncinst:
 
-:ref:`Host Function Instances <syntax-funcinst>` :math:`\{\FITYPE~\functype, \FIHOSTCODE~\X{hf}\}`
+:ref:`Host Function Instances <syntax-funcinst>` :math:`\{\FITYPE~\functype, \FIHOSTFUNC~\X{hf}\}`
 ..................................................................................................
 
 * The :ref:`function type <syntax-functype>` :math:`\functype` must be :ref:`valid <valid-functype>` under an empty :ref:`context <context>`.
@@ -441,7 +441,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
        R = (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]
+     S \vdashfuncinst \{\FITYPE~[t_1^\ast] \to [t_2^\ast], \FIHOSTFUNC~\X{hf}\} : [t_1^\ast] \to [t_2^\ast]
    }
 
 .. note::

document/core/exec/conventions.rst

@@ -99,7 +99,8 @@ and a sequence of ${:CONST} instructions can be interpreted as an operand "stack
 
 :ref:`Labels <label>` and :ref:`frames <frame>` are similarly :ref:`defined <syntax-instr-admin>` to be part of an instruction sequence.
 
-The order of reduction is determined by the definition of an appropriate :ref:`evaluation context <syntax-ctxt-eval>`.
+The order of reduction is determined by the details of the reduction rules.
+Usually, the left-most instruction that is not a constant will be the subject of the next reduction *step*.
 
 Reduction *terminates* when no more reduction rules are applicable.
 :ref:`Soundness <soundness>` of the WebAssembly :ref:`type system <type-system>` guarantees that this is only the case when the original instruction sequence has either been reduced to a sequence of ${:CONST} instructions, which can be interpreted as the :ref:`values <syntax-val>` of the resulting operand stack,

document/core/exec/instructions.rst

@@ -2685,7 +2685,7 @@ Furthermore, the resulting store must be :ref:`valid <valid-store>`, i.e., all d
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
-     (\iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTCODE~\X{hf} \} \\
+     (\iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTFUNC~\X{hf} \} \\
      \wedge & \expanddt(\deftype) = \TFUNC~[t_1^n] \toF [t_2^m] \\
      \wedge & (S'; \result) \in \X{hf}(S; \val^n)) \\
      \end{array} \\
@@ -2694,7 +2694,7 @@ Furthermore, the resulting store must be :ref:`valid <valid-store>`, i.e., all d
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
-     (\iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTCODE~\X{hf} \} \\
+     (\iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTFUNC~\X{hf} \} \\
      \wedge & \expanddt(\deftype) = \TFUNC~[t_1^n] \toF [t_2^m] \\
      \wedge & \bot \in \X{hf}(S; \val^n)) \\
      \end{array} \\

document/core/exec/modules.rst

@@ -53,7 +53,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
 
 2. Let :math:`a` be the first free :ref:`function address <syntax-funcaddr>` in :math:`S`.
 
-3. Let :math:`\funcinst` be the :ref:`function instance <syntax-funcinst>` :math:`\{ \FITYPE~\deftype, \FIHOSTCODE~\hostfunc \}`.
+3. Let :math:`\funcinst` be the :ref:`function instance <syntax-funcinst>` :math:`\{ \FITYPE~\deftype, \FIHOSTFUNC~\hostfunc \}`.
 
 4. Append :math:`\funcinst` to the |SFUNCS| of :math:`S`.
 
@@ -65,7 +65,7 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
    \allochostfunc(S, \deftype, \hostfunc) &=& S', \funcaddr \\[1ex]
    \mbox{where:} \hfill \\
    \funcaddr &=& |S.\SFUNCS| \\
-   \funcinst &=& \{ \FITYPE~\deftype, \FIHOSTCODE~\hostfunc \} \\
+   \funcinst &=& \{ \FITYPE~\deftype, \FIHOSTFUNC~\hostfunc \} \\
    S' &=& S \compose \{\SFUNCS~\funcinst\} \\
    \end{array}
 

document/core/syntax/instructions.rst

@@ -13,10 +13,12 @@ In addition to dynamic operands from the stack, some instructions also have stat
 typically :ref:`indices <syntax-index>` or type annotations,
 which are part of the instruction itself.
 
-Some instructions are :ref:`structured <syntax-instr-control>` in that they bracket nested sequences of instructions.
+Some instructions are :ref:`structured <syntax-instr-control>` in that they contain nested sequences of instructions.
 
 The following sections group instructions into a number of different categories.
 
+The syntax of instruction is further :ref:`extended <syntax-instr-admin>` with additional forms for the purpose of specifying :ref:`execution <exec>`.
+
 
 .. index:: ! parametric instruction, value type
    pair: abstract syntax; instruction

document/core/syntax/types.rst

@@ -367,6 +367,33 @@ Global Types
 $${syntax: globaltype}
 
 
+.. index:: ! element type, reference type, table, element
+   pair: abstract syntax; element type
+   pair: element; type
+.. _syntax-elemtype:
+
+Element Types
+~~~~~~~~~~~~~
+
+*Element types* classify :ref:`element segments <syntax-elem>` by a :ref:`reference type <syntax-reftype>` of its elements.
+
+$${syntax: elemtype}
+
+
+.. index:: ! data type, memory
+   pair: abstract syntax; data type
+   pair: data; type
+.. _syntax-datatype:
+
+Data Types
+~~~~~~~~~~
+
+*Data types* classify :ref:`data segments <syntax-elem>`.
+Since the contents of a data segment requires no further classification, they merely consist of a universal marker ${:OK} indicating well-formedness.
+
+$${syntax: datatype}
+
+
 .. index:: ! external type, defined type, function type, table type, memory type, global type, import, external value
    pair: abstract syntax; external type
    pair: external; type

document/core/util/macros.def

@@ -289,7 +289,8 @@
 .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}}
 .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
 .. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}}
-.. |datatype| mathdef:: \xref{valid/modules}{syntax-datatype}{\X{datatype}}
+.. |elemtype| mathdef:: \xref{syntax/types}{syntax-elemtype}{\X{elemtype}}
+.. |datatype| mathdef:: \xref{syntax/types}{syntax-datatype}{\X{datatype}}
 .. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}}
 
 .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
@@ -1307,7 +1308,8 @@
 .. |FITYPE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{type}}
 .. |FIMODULE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{module}}
 .. |FICODE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{code}}
-.. |FIHOSTCODE| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{hostcode}}
+.. |FIHOSTFUNC| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\K{hostfunc}}
+.. |FIdots| mathdef:: \dots
 
 .. |TITYPE| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{type}}
 .. |TIREFS| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\K{elem}}
@@ -1384,10 +1386,12 @@
 
 .. |fieldval| mathdef:: \xref{exec/runtime}{syntax-fieldval}{\X{fieldval}}
 .. |packval| mathdef:: \xref{exec/runtime}{syntax-packval}{\X{packval}}
+.. |pack| mathdef:: \xref{exec/runtime}{syntax-pack}{\X{pack}}
 
 .. |externval| mathdef:: \xref{exec/runtime}{syntax-externval}{\X{externval}}
 
 .. |moduleinst| mathdef:: \xref{exec/runtime}{syntax-moduleinst}{\X{moduleinst}}
+.. |funccode| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\X{code}}
 .. |funcinst| mathdef:: \xref{exec/runtime}{syntax-funcinst}{\X{funcinst}}
 .. |tableinst| mathdef:: \xref{exec/runtime}{syntax-tableinst}{\X{tableinst}}
 .. |meminst| mathdef:: \xref{exec/runtime}{syntax-meminst}{\X{meminst}}
@@ -1423,6 +1427,7 @@
 .. Store, non-terminals
 
 .. |store| mathdef:: \xref{exec/runtime}{syntax-store}{\X{store}}
+.. |state| mathdef:: \xref{exec/runtime}{syntax-state}{\X{state}}
 
 
 .. Stack, terminals
@@ -1438,12 +1443,12 @@
 
 .. |label| mathdef:: \xref{exec/runtime}{syntax-label}{\X{label}}
 .. |frame| mathdef:: \xref{exec/runtime}{syntax-frame}{\X{frame}}
-.. |framestate| mathdef:: \xref{exec/runtime}{syntax-framestate}{\X{framestate}}
+.. |callframe| mathdef:: \xref{exec/runtime}{syntax-callframe}{\X{callframe}}
 
 
 .. Stack, meta functions
 
-.. |fblocktype| mathdef:: \xref{exec/runtime}{aux-fblocktype}{\F{instrtype}}
+.. |fblocktype| mathdef:: \xref{exec/runtime}{aux-blocktype}{\F{instrtype}}
 
 
 .. Administrative Instructions, terminals
@@ -1455,8 +1460,10 @@
 .. |REFHOSTADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}host}}
 .. |REFEXTERN| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}extern}}
 .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}}
-.. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}}
-.. |RETURNINVOKE| mathdef:: \xref{exec/runtime}{syntax-return_invoke}{\K{return\_invoke}}
+
+.. TODO remove these
+.. |INVOKE| mathdef:: \xref{exec/instructions}{exec-invoke}{\K{invoke}}
+.. |RETURNINVOKE| mathdef:: \xref{exec/instructions}{exec-invoke}{\K{return\_invoke}}
 
 
 .. Values & Results, non-terminals
@@ -1483,11 +1490,6 @@
 .. |unpackfield| mathdef:: \xref{exec/runtime}{aux-unpackfield}{\F{unpack}}
 
 
-.. Administrative Instructions, non-terminals
-
-.. |XB| mathdef:: \xref{exec/runtime}{syntax-ctxt-block}{B}
-
-
 .. Configurations, non-terminals
 
 .. |config| mathdef:: \xref{exec/runtime}{syntax-config}{\X{config}}

document/core/valid/modules.rst

@@ -283,7 +283,6 @@ $${rule: Elemmode_ok/declare}
    single: memory; data
    single: data; segment
 .. _valid-data:
-.. _syntax-datatype:
 
 Data Segments
 ~~~~~~~~~~~~~

spectec/spec/wasm-3.0/1-syntax.watsup

@@ -246,7 +246,7 @@ syntax memtype hint(desc "memory type") =
   limits PAGE
 syntax elemtype hint(desc "element type") =
   reftype
-syntax datatype hint(desc "data type") hint(show OK) hint(macro "%data" "%data") =
+syntax datatype hint(desc "data type") hint(macro "%" "%data") =
   OK
 syntax externtype hint(desc "external type") hint(macro "%" "ET%") =
   | FUNC typeuse | GLOBAL globaltype | TABLE tabletype | MEM memtype
@@ -301,6 +301,9 @@ def $sizenn(nt) = $size(nt)
 def $sizenn1(nt) = $size(nt)
 def $sizenn2(nt) = $size(nt)
 
+def $psizenn(packtype) : nat   hint(show N)   hint(macro none)  ;; HACK!
+def $psizenn(pt) = $psize(pt)
+
 def $lsizenn(lanetype) : nat   hint(show N)   hint(macro none)  ;; HACK!
 def $lsizenn1(lanetype) : nat  hint(show N_1) hint(macro none)  ;; HACK!
 def $lsizenn2(lanetype) : nat  hint(show N_2) hint(macro none)  ;; HACK!
@@ -312,7 +315,7 @@ syntax num_(numtype)
 syntax num_(Inn) = iN($sizenn(Inn))
 syntax num_(Fnn) = fN($sizenn(Fnn))
 
-syntax pack_(Pnn) = iN($psize(Pnn))
+syntax pack_(Pnn) = iN($psizenn(Pnn))
 
 syntax lane_(lanetype)
 syntax lane_(numtype) = num_(numtype)
@@ -644,6 +647,7 @@ syntax instr/memory hint(desc "memory instruction") = ...
 
 syntax instr/data hint(desc "data instruction") = ...
   | DATA.DROP dataidx
+  | ...
 
 
 syntax expr hint(desc "expression") =

spectec/spec/wasm-3.0/4-runtime.watsup

@@ -2,7 +2,7 @@
 ;; Addresses
 ;;
 
-syntax addr hint(desc "address") = nat
+syntax addr hint(desc "address") = nat  ;; TODO: 0 | 1 | 2 | ...
 syntax funcaddr hint(desc "function address") = addr
 syntax globaladdr hint(desc "global address") = addr
 syntax tableaddr hint(desc "table address") = addr
@@ -69,38 +69,32 @@ var xv : externval
 
 ;; Instances
 
+syntax funccode hint(show code) hint(macro "funccode") =
+  func | HOSTFUNC `... hint(macro "FI%")
+
 syntax funcinst hint(desc "function instance") hint(macro "%" "FI%") =
-  { TYPE deftype,
-    MODULE moduleinst,
-    CODE func }
+  { TYPE deftype, MODULE moduleinst, CODE funccode }
 syntax globalinst hint(desc "global instance") hint(macro "%" "GI%") =
-  { TYPE globaltype,
-    VALUE val }
+  { TYPE globaltype, VALUE val }
 syntax tableinst hint(desc "table instance") hint(macro "%" "TI%") =
-  { TYPE tabletype,
-    REFS ref* }
+  { TYPE tabletype, REFS ref* }
 syntax meminst hint(desc "memory instance") hint(macro "%" "MI%") =
-  { TYPE memtype,
-    BYTES byte* }
+  { TYPE memtype, BYTES byte* }
 syntax eleminst hint(desc "element instance") hint(macro "%" "EI%") =
-  { TYPE elemtype,
-    REFS ref* }
+  { TYPE elemtype, REFS ref* }
 syntax datainst hint(desc "data instance") hint(macro "%" "DI%") =
   { BYTES byte* }
 syntax exportinst hint(desc "export instance") hint(macro "%" "EI%") =
-  { NAME name,
-    VALUE externval }
+  { NAME name, VALUE externval }
 
 syntax packval hint(desc "packed value") =
-  | PACK packtype pack_(packtype)    hint(show %.PACK %)
+  | PACK packtype iN($psizenn(packtype))    hint(show %.PACK %)
 syntax fieldval hint(desc "field value") =
   | val | packval
 syntax structinst hint(desc "structure instance") hint(macro "%" "SI%") =
-  { TYPE deftype,
-    FIELDS fieldval* }
+  { TYPE deftype, FIELDS fieldval* }
 syntax arrayinst hint(desc "array instance") hint(macro "%" "AI%") =
-  { TYPE deftype,
-    FIELDS fieldval* }
+  { TYPE deftype, FIELDS fieldval* }
 
 syntax moduleinst hint(desc "module instance") hint(macro "%" "MI%") =
   { TYPES deftype*,
@@ -140,11 +134,10 @@ syntax store hint(desc "store") hint(macro "%" "S%") =
     ARRAYS arrayinst* }
 
 syntax frame hint(desc "frame") hint(macro "%" "A%") =
-  { LOCALS (val?)*,
-    MODULE moduleinst }
+  { LOCALS (val?)*, MODULE moduleinst }
 
 syntax state hint(desc "state") = store; frame
-syntax config hint(desc "configuration") = state; admininstr*
+syntax config hint(desc "configuration") = state; instr*
 
 var s : store
 var f : frame
@@ -155,9 +148,9 @@ var z : state
 ;; Administrative Instructions
 ;;
 
-syntax admininstr hint(show instr) hint(desc "administrative instruction") =
-  | instr
+syntax instr/admin hint(desc "administrative instruction") =
+  | ...
   | addrref
-  | LABEL_ n `{instr*} admininstr* hint(show LABEL_%#% %%)
-  | FRAME_ n `{frame} admininstr*  hint(show FRAME_%#% %%)
+  | LABEL_ n `{instr*} instr*  hint(show LABEL_%#% %%)
+  | FRAME_ n `{frame} instr*   hint(show FRAME_%#% %%)
   | TRAP

spectec/spec/wasm-3.0/5-runtime-aux.watsup

@@ -18,25 +18,23 @@ def $inst_reftype(mm, rt) = $subst_all_reftype(rt, dt*)
 
 def $default_(valtype) : val?
 
-def $default_(I32) = (CONST I32 0)
-def $default_(I64) = (CONST I64 0)
-def $default_(F32) = (CONST F32 $fzero(32))
-def $default_(F64) = (CONST F64 $fzero(64))
-def $default_(V128) = (VCONST V128 0)
+def $default_(Inn) = (CONST Inn 0)
+def $default_(Fnn) = (CONST Fnn $fzero($size(Fnn)))
+def $default_(Vnn) = (VCONST Vnn 0)
 def $default_(REF NULL ht) = (REF.NULL ht)
-def $default_(REF eps ht) = eps
+def $default_(REF ht) = eps
 
 
 ;; Packed fields
 
 def $packfield(storagetype, val) : fieldval         hint(show $pack_(%,%)) hint(macro "packfield")
 def $unpackfield(storagetype, sx?, fieldval) : val  hint(show $unpack_(%)^(%)#((%))) hint(macro "unpackfield")
 
-def $packfield(t, val) = val
-def $packfield(pt, CONST I32 i) = PACK pt $wrap(32, $psize(pt), i)
+def $packfield(valtype, val) = val
+def $packfield(packtype, CONST I32 i) = PACK packtype $wrap(32, $psize(packtype), i)
 
-def $unpackfield(t, eps, val) = val
-def $unpackfield(pt, sx, PACK pt i) = CONST I32 $ext($psize(pt), 32, sx, i)
+def $unpackfield(valtype, eps, val) = val
+def $unpackfield(packtype, sx, PACK packtype i) = CONST I32 $ext($psize(packtype), 32, sx, i)
 
 
 ;; Projections

spectec/spec/wasm-3.0/6-typing.watsup

@@ -20,7 +20,7 @@ syntax context hint(desc "context") hint(macro "%" "C%") =
     GLOBALS globaltype*,
     TABLES tabletype*,
     MEMS memtype*,
-    ELEMS reftype*,
+    ELEMS elemtype*,
     DATAS datatype*,
     LOCALS localtype*,
     LABELS resulttype*,
@@ -1186,10 +1186,10 @@ relation Local_ok: context |- local : localtype      hint(show "T-local")    hin
 relation Global_ok: context |- global : globaltype   hint(show "T-global")   hint(macro "%global")
 relation Table_ok: context |- table : tabletype      hint(show "T-table")    hint(macro "%table")
 relation Mem_ok: context |- mem : memtype            hint(show "T-mem")      hint(macro "%mem")
-relation Elem_ok: context |- elem : reftype          hint(show "T-elem")     hint(macro "%elem")
+relation Elem_ok: context |- elem : elemtype         hint(show "T-elem")     hint(macro "%elem")
 relation Data_ok: context |- data : datatype         hint(show "T-data")     hint(macro "%data")
-relation Elemmode_ok: context |- elemmode : reftype  hint(show "T-elemmode") hint(macro "%elemmode")
-relation Datamode_ok: context |- datamode : OK       hint(show "T-datamode") hint(macro "%datamode")
+relation Elemmode_ok: context |- elemmode : elemtype hint(show "T-elemmode") hint(macro "%elemmode")
+relation Datamode_ok: context |- datamode : datatype hint(show "T-datamode") hint(macro "%datamode")
 relation Start_ok: context |- start : OK             hint(show "T-start")    hint(macro "%start")
 
 rule Type_ok:
@@ -1229,10 +1229,10 @@ rule Mem_ok:
   -- Memtype_ok: C |- memtype : OK
 
 rule Elem_ok:
-  C |- ELEM reftype expr* elemmode : reftype
-  -- Reftype_ok: C |- reftype : OK
-  -- (Expr_ok_const: C |- expr : reftype CONST)*
-  -- Elemmode_ok: C |- elemmode : reftype
+  C |- ELEM elemtype expr* elemmode : elemtype
+  -- Reftype_ok: C |- elemtype : OK
+  -- (Expr_ok_const: C |- expr : elemtype CONST)*
+  -- Elemmode_ok: C |- elemmode : elemtype
 
 rule Data_ok:
   C |- DATA b* datamode : OK