diff --git a/document/core/.gitignore b/document/.gitignore similarity index 50% rename from document/core/.gitignore rename to document/.gitignore index b932ec28..09f98591 100644 --- a/document/core/.gitignore +++ b/document/.gitignore @@ -1,3 +1,2 @@ _build _static -document/*.pyc diff --git a/document/Makefile b/document/Makefile index 875efc72..5df0df13 100644 --- a/document/Makefile +++ b/document/Makefile @@ -1,76 +1,270 @@ -DIRS = core js-api web-api -FILES = index.html -BUILDDIR = _build +# Makefile for Sphinx documentation +# -# Global targets. +# You can set these variables from the command line. +SPHINXOPTS = +SPHINXBUILD = sphinx-build +PAPER = a4 +BUILDDIR = _build +STATICDIR = _static +DOWNLOADDIR = _download +GHPAGESDIR = ../docs +NAME = WebAssembly -.PHONY: all -all: $(BUILDDIR) root $(DIRS) +# Internal variables. +PAPEROPT_a4 = -D latex_paper_size=a4 +PAPEROPT_letter = -D latex_paper_size=letter +ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) . +# the i18n builder cannot share the environment and doctrees with the others +I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) . -$(BUILDDIR): - mkdir -p $@ +.PHONY: usage +usage: + @echo "Please use \`make ' where is one of" + @echo " html to make standalone HTML files" + @echo " pdf to make standalone PDF file" + @echo " all to make both" + @echo " publish to make all and push to gh-pages" + @echo " help to see more options" -.PHONY: deploy -deploy: - GIT_DEPLOY_DIR=$(BUILDDIR) bash deploy.sh +.PHONY: help +help: + @echo "Usage: \`make ' where is one of" + @echo " html to make standalone HTML files" + @echo " pdf to make standalone PDF file" + @echo " all to make both" + @echo " publish to make all and push to gh-pages" + @echo " dirhtml to make HTML files named index.html in directories" + @echo " singlehtml to make a single large HTML file" + @echo " pickle to make pickle files" + @echo " json to make JSON files" + @echo " htmlhelp to make HTML files and a HTML help project" + @echo " qthelp to make HTML files and a qthelp project" + @echo " applehelp to make an Apple Help Book" + @echo " devhelp to make HTML files and a Devhelp project" + @echo " epub to make an epub" + @echo " epub3 to make an epub3" + @echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter" + @echo " latexpdf to make LaTeX files and run them through pdflatex" + @echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx" + @echo " text to make text files" + @echo " man to make manual pages" + @echo " texinfo to make Texinfo files" + @echo " info to make Texinfo files and run them through makeinfo" + @echo " gettext to make PO message catalogs" + @echo " changes to make an overview of all changed/added/deprecated items" + @echo " xml to make Docutils-native XML files" + @echo " pseudoxml to make pseudoxml-XML files for display purposes" + @echo " linkcheck to check all external links for integrity" + @echo " doctest to run all doctests embedded in the documentation (if enabled)" + @echo " coverage to run coverage check of the documentation (if enabled)" + @echo " dummy to check syntax errors of document sources" .PHONY: publish publish: all deploy +.PHONY: deploy +deploy: + GIT_DEPLOY_DIR=$(BUILDDIR)/html sh deploy.sh + +.PHONY: all +all: pdf html + +.PHONY: pdf +pdf: latexpdf + mkdir -p $(BUILDDIR)/html/$(DOWNLOADDIR) + ln -f $(BUILDDIR)/latex/$(NAME).pdf $(BUILDDIR)/html/$(DOWNLOADDIR)/$(NAME).pdf + + .PHONY: clean -clean: $(DIRS:%=clean-%) +clean: rm -rf $(BUILDDIR) + rm -rf $(STATICDIR) -.PHONY: diff -diff: $(DIRS:%=diff-%) +.PHONY: html +html: + $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html + for file in `ls $(BUILDDIR)/html/*.html`; \ + do \ + sed s:BASEDIR:.:g <$$file >$$file.out; \ + mv -f $$file.out $$file; \ + done + for file in `ls $(BUILDDIR)/html/*/*.html`; \ + do \ + sed s:BASEDIR:..:g <$$file >$$file.out; \ + sed 's;MathJax.Hub.Config({TeX: {MAXBUFFER: 10*1024}})$$file; \ + rm -f $$file.out; \ + done + @echo + @echo "Build finished. The HTML pages are in `pwd`/$(BUILDDIR)/html." +.PHONY: dirhtml +dirhtml: + $(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml + @echo + @echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml." -# Directory-specific targets. +.PHONY: singlehtml +singlehtml: + $(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml + @echo + @echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml." -.PHONY: root -root: $(BUILDDIR) - touch $(BUILDDIR)/.nojekyll - cp -f $(FILES) $(BUILDDIR)/ +.PHONY: pickle +pickle: + $(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle + @echo + @echo "Build finished; now you can process the pickle files." -.PHONY: $(DIRS) -$(DIRS): %: $(BUILDDIR) $(DIRS:%=build-%) $(DIRS:%=dir-%) +.PHONY: json +json: + $(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json + @echo + @echo "Build finished; now you can process the JSON files." -.PHONY: $(DIRS:%=build-%) -$(DIRS:%=build-%): build-%: - (cd $(@:build-%=%); make BUILDDIR=$(BUILDDIR) all) +.PHONY: htmlhelp +htmlhelp: + $(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp + @echo + @echo "Build finished; now you can run HTML Help Workshop with the" \ + ".hhp project file in $(BUILDDIR)/htmlhelp." -.PHONY: $(DIRS:%=dir-%) -$(DIRS:%=dir-%): dir-%: - mkdir -p $(BUILDDIR)/$(@:dir-%=%) - rm -rf $(BUILDDIR)/$(@:dir-%=%)/* - cp -R $(@:dir-%=%)/$(BUILDDIR)/html/* $(BUILDDIR)/$(@:dir-%=%)/ +.PHONY: qthelp +qthelp: + $(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp + @echo + @echo "Build finished; now you can run "qcollectiongenerator" with the" \ + ".qhcp project file in $(BUILDDIR)/qthelp, like this:" + @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/WebAssembly.qhcp" + @echo "To view the help file:" + @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/WebAssembly.qhc" -.PHONY: $(DIRS:%=deploy-%) -$(DIRS:%=deploy-%): deploy-%: - GIT_DEPLOY_DIR=$(BUILDDIR) GIT_DEPLOY_SUBDIR=$(@:deploy-%=%) bash deploy.sh +.PHONY: applehelp +applehelp: + $(SPHINXBUILD) -b applehelp $(ALLSPHINXOPTS) $(BUILDDIR)/applehelp + @echo + @echo "Build finished. The help book is in $(BUILDDIR)/applehelp." + @echo "N.B. You won't be able to view it unless you put it in" \ + "~/Library/Documentation/Help or install it in your application" \ + "bundle." -.PHONY: $(DIRS:%=publish-%) -$(DIRS:%=publish-%): publish-%: % deploy-% +.PHONY: devhelp +devhelp: + $(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp + @echo + @echo "Build finished." + @echo "To view the help file:" + @echo "# mkdir -p $$HOME/.local/share/devhelp/WebAssembly" + @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/WebAssembly" + @echo "# devhelp" -.PHONY: $(DIRS:%=clean-%) -$(DIRS:%=clean-%): clean-%: - (cd $(@:clean-%=%); make BUILDDIR=$(BUILDDIR) clean) - rm -rf $(BUILDDIR)/$(@:clean-%=%) +.PHONY: epub +epub: + $(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub + @echo + @echo "Build finished. The epub file is in $(BUILDDIR)/epub." -.PHONY: $(DIRS:%=diff-%) -$(DIRS:%=diff-%): diff-%: - (cd $(@:diff-%=%); make BUILDDIR=$(BUILDDIR) diff) +.PHONY: epub3 +epub3: + $(SPHINXBUILD) -b epub3 $(ALLSPHINXOPTS) $(BUILDDIR)/epub3 + @echo + @echo "Build finished. The epub3 file is in $(BUILDDIR)/epub3." +.PHONY: latex +latex: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo + @echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex." + @echo "Run \`make' in that directory to run these through (pdf)latex" \ + "(use \`make latexpdf' here to do that automatically)." -# Help. +.PHONY: latexpdf +latexpdf: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo "Running LaTeX files through pdflatex..." + $(MAKE) -C $(BUILDDIR)/latex all-pdf + @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." -.PHONY: help -help: - @echo "Please use \`make ' where is one of" - @echo " all to build all documents" - @echo " publish to make all and push to gh-pages" - @echo " to build a specific subdirectory" - @echo " publish- to build and push a specific subdirectory" +.PHONY: latexpdfja +latexpdfja: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo "Running LaTeX files through platex and dvipdfmx..." + $(MAKE) -C $(BUILDDIR)/latex all-pdf-ja + @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." -.PHONY: usage -usage: help +.PHONY: text +text: + $(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text + @echo + @echo "Build finished. The text files are in $(BUILDDIR)/text." + +.PHONY: man +man: + $(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man + @echo + @echo "Build finished. The manual pages are in $(BUILDDIR)/man." + +.PHONY: texinfo +texinfo: + $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo + @echo + @echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo." + @echo "Run \`make' in that directory to run these through makeinfo" \ + "(use \`make info' here to do that automatically)." + +.PHONY: info +info: + $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo + @echo "Running Texinfo files through makeinfo..." + make -C $(BUILDDIR)/texinfo info + @echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo." + +.PHONY: gettext +gettext: + $(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale + @echo + @echo "Build finished. The message catalogs are in $(BUILDDIR)/locale." + +.PHONY: changes +changes: + $(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes + @echo + @echo "The overview file is in $(BUILDDIR)/changes." + +.PHONY: linkcheck +linkcheck: + $(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck + @echo + @echo "Link check complete; look for any errors in the above output " \ + "or in $(BUILDDIR)/linkcheck/output.txt." + +.PHONY: doctest +doctest: + $(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest + @echo "Testing of doctests in the sources finished, look at the " \ + "results in $(BUILDDIR)/doctest/output.txt." + +.PHONY: coverage +coverage: + $(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage + @echo "Testing of coverage in the sources finished, look at the " \ + "results in $(BUILDDIR)/coverage/python.txt." + +.PHONY: xml +xml: + $(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml + @echo + @echo "Build finished. The XML files are in $(BUILDDIR)/xml." + +.PHONY: pseudoxml +pseudoxml: + $(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml + @echo + @echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml." + +.PHONY: dummy +dummy: + $(SPHINXBUILD) -b dummy $(ALLSPHINXOPTS) $(BUILDDIR)/dummy + @echo + @echo "Build finished. Dummy builder generates no files." diff --git a/document/README.md b/document/README.md index e8312f42..310e5d3e 100644 --- a/document/README.md +++ b/document/README.md @@ -1,23 +1,20 @@ -# WebAssembly Specifications +# WebAssembly Specification -This directory contains the source code for the WebAssembly spec documents, as served from the [webassembly.github.io/spec](https://webassembly.github.io/spec) pages. -It uses [Sphinx](http://www.sphinx-doc.org/) and [Bikeshed](https://github.com/tabatkins/bikeshed). +This is (meant to become) the official WebAssembly "language" specification. -To install Sphinx: +It uses [Sphinx](http://www.sphinx-doc.org/). To install that: ``` pip install sphinx ``` - -To install Bikeshed, see the instructions [here](https://tabatkins.github.io/bikeshed/#installing). - - -To build everything locally (result appears in `_build/`): +To make HTML (result in `_build/html`): ``` -make all +make html ``` - -To build everything and update [webassembly.github.io/spec](https://webassembly.github.io/spec) with it: +To make PDF (result in `_build/latex`, requires LaTeX): +``` +make pdf ``` -make publish +To make all: +``` +make all ``` -Please make sure to only use that once a change has approval. diff --git a/document/appendix-algorithm/index.rst b/document/appendix-algorithm/index.rst new file mode 100644 index 00000000..883daeb7 --- /dev/null +++ b/document/appendix-algorithm/index.rst @@ -0,0 +1,6 @@ +Appendix: Validation Algorithm +------------------------------ + +.. todo:: + + Describe algorithm, state correctness properties (soundness, completeness) diff --git a/document/appendix-names/index.rst b/document/appendix-names/index.rst new file mode 100644 index 00000000..6c8fe7a2 --- /dev/null +++ b/document/appendix-names/index.rst @@ -0,0 +1,6 @@ +Appendix: Name Section +---------------------- + +.. todo:: + + Describe diff --git a/document/appendix-properties/index.rst b/document/appendix-properties/index.rst new file mode 100644 index 00000000..d43f7ccf --- /dev/null +++ b/document/appendix-properties/index.rst @@ -0,0 +1,6 @@ +Appendix: Formal Properties +--------------------------- + +.. todo:: + + Describe and sketch proof (progress, preservation, uniqueness) diff --git a/document/appendix-textual/index.rst b/document/appendix-textual/index.rst new file mode 100644 index 00000000..e7ea647e --- /dev/null +++ b/document/appendix-textual/index.rst @@ -0,0 +1,8 @@ +.. text-format: + +Appendix: Text Format +--------------------- + +.. todo:: + + Describe diff --git a/document/core/binary/index.rst b/document/binary/index.rst similarity index 86% rename from document/core/binary/index.rst rename to document/binary/index.rst index b47e6647..ce1879dd 100644 --- a/document/core/binary/index.rst +++ b/document/binary/index.rst @@ -1,4 +1,4 @@ -.. _binary: +.. _binary-format: Binary Format ============= @@ -9,5 +9,5 @@ Binary Format conventions values types - instructions modules + instructions diff --git a/document/core/conf.py b/document/conf.py similarity index 97% rename from document/core/conf.py rename to document/conf.py index d410ee04..5971bb4a 100644 --- a/document/core/conf.py +++ b/document/conf.py @@ -18,7 +18,7 @@ import os import sys pwd = os.path.abspath('.') -sys.path.insert(0, pwd + '/util') +sys.path.insert(0, pwd) # -- General configuration ------------------------------------------------ @@ -36,7 +36,6 @@ 'sphinx.ext.ifconfig', 'sphinx.ext.githubpages', 'mathdef', - 'pseudo-lexer' ] # Add any paths that contain templates here, relative to this directory. @@ -60,8 +59,7 @@ title = u'WebAssembly Specification' copyright = u'2017, WebAssembly Community Group' author = u'WebAssembly Community Group' -editor = u'Andreas Rossberg (editor)' -logo = 'static/webassembly.png' +logo = 'placeholder.jpg' # The version info for the project you're documenting, acts as replacement for # |version| and |release|, also used in various other places throughout the @@ -138,8 +136,7 @@ # html_theme_options = { 'logo': logo, - 'logo_name': 'WebAssembly', - 'description': 'WebAssembly Specification', + 'description': ' ', 'fixed_sidebar': True, 'sidebar_width': '260px', 'sidebar_collapse': True, @@ -159,7 +156,6 @@ ] } - # Add any paths that contain custom themes here, relative to this directory. # html_theme_path = [] @@ -186,7 +182,7 @@ # Add any paths that contain custom static files (such as style sheets) here, # relative to this directory. They are copied after the builtin static files, # so a file named "default.css" will overwrite the builtin "default.css". -html_static_path = ['_static', 'static/custom.css'] +html_static_path = ['_static', 'custom.css'] # Add any extra paths that contain custom files (such as robots.txt or # .htaccess) here, relative to this directory. These files are copied @@ -302,7 +298,7 @@ ( master_doc, name + '.tex', title, - author + '\\\\ \\hfill\\large ' + editor, + author, 'manual' ), ] @@ -476,5 +472,5 @@ # Macros rst_prolog = """ -.. include:: /""" + pwd + """/util/macros.def +.. include:: /""" + pwd + """/math.def """ diff --git a/document/core/LICENSE b/document/core/LICENSE deleted file mode 100644 index 795b406e..00000000 --- a/document/core/LICENSE +++ /dev/null @@ -1,50 +0,0 @@ -W3C SOFTWARE AND DOCUMENT NOTICE AND LICENSE - -This work is being provided by the copyright holders under the following -license. - - -LICENSE - -By obtaining and/or copying this work, you (the licensee) agree that you have -read, understood, and will comply with the following terms and conditions. - -Permission to copy, modify, and distribute this work, with or without -modification, for any purpose and without fee or royalty is hereby granted, -provided that you include the following on ALL copies of the work or portions -thereof, including modifications: - -* The full text of this NOTICE in a location viewable to users of the - redistributed or derivative work. - -* Any pre-existing intellectual property disclaimers, notices, or terms and - conditions. If none exist, the W3C Software and Document Short Notice - (https://www.w3.org/Consortium/Legal/copyright-software-short-notice) should - be included. - -* Notice of any changes or modifications, through a copyright statement on the - new code or document such as "This software or document includes material - copied from or derived from [title and URI of the W3C document]. Copyright © [YEAR] W3C® (MIT, ERCIM, Keio, Beihang)." - - -DISCLAIMERS - -THIS WORK IS PROVIDED "AS IS," AND COPYRIGHT HOLDERS MAKE NO REPRESENTATIONS -OR WARRANTIES, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO, WARRANTIES OF -MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE OR THAT THE USE OF THE -SOFTWARE OR DOCUMENT WILL NOT INFRINGE ANY THIRD PARTY PATENTS, COPYRIGHTS, -TRADEMARKS OR OTHER RIGHTS. - -COPYRIGHT HOLDERS WILL NOT BE LIABLE FOR ANY DIRECT, INDIRECT, SPECIAL OR -CONSEQUENTIAL DAMAGES ARISING OUT OF ANY USE OF THE SOFTWARE OR DOCUMENT. - -The name and trademarks of copyright holders may NOT be used in advertising or -publicity pertaining to the work without specific, written prior permission. -Title to copyright in this work will at all times remain with copyright -holders. - - -NOTES - -This version: -http://www.w3.org/Consortium/Legal/2015/copyright-software-and-document diff --git a/document/core/Makefile b/document/core/Makefile deleted file mode 100644 index 6a06fed0..00000000 --- a/document/core/Makefile +++ /dev/null @@ -1,355 +0,0 @@ -# Makefile for Sphinx documentation -# - -# You can set these variables from the command line. -SPHINXOPTS = -SPHINXBUILD = sphinx-build -PAPER = a4 -BUILDDIR = _build -STATICDIR = _static -DOWNLOADDIR = _download -NAME = WebAssembly - -# Hack until we have moved to more recent Sphinx. -OLDMATHJAX = https://cdn.mathjax.org/mathjax/latest/MathJax.js -NEWMATHJAX = https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js - -# Internal variables. -PAPEROPT_a4 = -D latex_paper_size=a4 -PAPEROPT_letter = -D latex_paper_size=letter -ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) . -# the i18n builder cannot share the environment and doctrees with the others -I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) . - -.PHONY: usage -usage: - @echo "Please use \`make ' where is one of" - @echo " html to make standalone HTML files" - @echo " pdf to make standalone PDF file" - @echo " bikeshed to make a bikeshed wrapped single large HTML file" - @echo " diff to make a diff of the bikeshed HTML file with the latest TR" - @echo " WD-tar generate tar file for updating the Working Draft" - @echo " WD-echidna publish the Working Draft tar file via Echidna" - @echo " all to make all 3" - @echo " publish to make all and push to gh-pages" - @echo " help to see more options" - -.PHONY: help -help: - @echo "Usage: \`make ' where is one of" - @echo " html to make standalone HTML files" - @echo " pdf to make standalone PDF file" - @echo " bikeshed to make a bikeshed wrapped single large HTML file" - @echo " all to make all 3" - @echo " publish to make all and push to gh-pages" - @echo " dirhtml to make HTML files named index.html in directories" - @echo " singlehtml to make a single large HTML file" - @echo " pickle to make pickle files" - @echo " json to make JSON files" - @echo " htmlhelp to make HTML files and a HTML help project" - @echo " qthelp to make HTML files and a qthelp project" - @echo " applehelp to make an Apple Help Book" - @echo " devhelp to make HTML files and a Devhelp project" - @echo " epub to make an epub" - @echo " epub3 to make an epub3" - @echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter" - @echo " latexpdf to make LaTeX files and run them through pdflatex" - @echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx" - @echo " text to make text files" - @echo " man to make manual pages" - @echo " texinfo to make Texinfo files" - @echo " info to make Texinfo files and run them through makeinfo" - @echo " gettext to make PO message catalogs" - @echo " changes to make an overview of all changed/added/deprecated items" - @echo " xml to make Docutils-native XML files" - @echo " pseudoxml to make pseudoxml-XML files for display purposes" - @echo " linkcheck to check all external links for integrity" - @echo " doctest to run all doctests embedded in the documentation (if enabled)" - @echo " coverage to run coverage check of the documentation (if enabled)" - @echo " dummy to check syntax errors of document sources" - -.PHONY: deploy -deploy: - (cd ..; make dir-core deploy-core) - -.PHONY: publish -publish: clean all deploy - -.PHONY: publish-main -publish-main: clean main bikeshed-keep deploy - -.PHONY: all -all: pdf html bikeshed - -.PHONY: main -main: pdf html - -# Dirty hack to avoid rebuilding the Bikeshed version for every push. -.PHONY: bikeshed-keep -bikeshed-keep: - test -e $(BUILDDIR)/html/bikeshed || \ - wget -r -nH --cut-dirs=2 -P $(BUILDDIR)/html --no-check-certificate \ - https://webassembly.github.io/spec/core/bikeshed || \ - echo Downloaded Bikeshed. - - -.PHONY: pdf -pdf: latexpdf - mkdir -p $(BUILDDIR)/html/$(DOWNLOADDIR) - ln -f $(BUILDDIR)/latex/$(NAME).pdf $(BUILDDIR)/html/$(DOWNLOADDIR)/$(NAME).pdf - - -.PHONY: clean -clean: - rm -rf $(BUILDDIR) - rm -rf $(STATICDIR) - -.PHONY: html -html: - $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html - for file in `ls $(BUILDDIR)/html/*.html`; \ - do \ - sed s:BASEDIR:.:g <$$file >$$file.out; \ - mv -f $$file.out $$file; \ - sed s~$(OLDMATHJAX)~$(NEWMATHJAX)~g <$$file >$$file.out; \ - mv -f $$file.out $$file; \ - done - for file in `ls $(BUILDDIR)/html/*/*.html`; \ - do \ - sed s:BASEDIR:..:g <$$file >$$file.out; \ - sed 's;MathJax.Hub.Config({TeX: {MAXBUFFER: 30*1024}})$$file; \ - rm -f $$file.out; \ - sed s~$(OLDMATHJAX)~$(NEWMATHJAX)~g <$$file >$$file.out; \ - mv -f $$file.out $$file; \ - done - @echo - @echo "Build finished. The HTML pages are in `pwd`/$(BUILDDIR)/html/." - -.PHONY: dirhtml -dirhtml: - $(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml - @echo - @echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml." - -.PHONY: singlehtml -singlehtml: - $(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml - @echo - @echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml." - -.PHONY: bikeshed -bikeshed: - $(SPHINXBUILD) -b singlehtml -c util/bikeshed \ - $(ALLSPHINXOPTS) $(BUILDDIR)/bikeshed_singlehtml - python util/bikeshed_fixup.py $(BUILDDIR)/bikeshed_singlehtml/index.html \ - >$(BUILDDIR)/bikeshed_singlehtml/index_fixed.html - mkdir -p $(BUILDDIR)/bikeshed_mathjax/ - bikeshed spec index.bs $(BUILDDIR)/bikeshed_mathjax/index.html - mkdir -p $(BUILDDIR)/html/bikeshed/ - (cd util/katex/ && yarn && yarn build && npm install --only=prod) - python util/mathjax2katex.py $(BUILDDIR)/bikeshed_mathjax/index.html \ - >$(BUILDDIR)/html/bikeshed/index.html - mkdir -p $(BUILDDIR)/html/bikeshed/katex/dist/ - cp -r util/katex/dist/* $(BUILDDIR)/html/bikeshed/katex/dist/ - patch -p0 $(BUILDDIR)/html/bikeshed/katex/dist/katex.css \ - < util/katex_fix.patch - cp $(BUILDDIR)/bikeshed_singlehtml/_static/pygments.css \ - $(BUILDDIR)/html/bikeshed/ - @echo - @echo "Build finished. The HTML page is in $(BUILDDIR)/html/bikeshed/." - -.PHONY: WD-tar -WD-tar: bikeshed - @echo "Building tar file..." - tar cvf \ - $(BUILDDIR)/WD.tar \ - --transform='s|$(BUILDDIR)/html/bikeshed/||' \ - --transform='s|index.html|Overview.html|' \ - $(BUILDDIR)/html/bikeshed/index.html \ - $(BUILDDIR)/html/bikeshed/pygments.css \ - $(BUILDDIR)/html/bikeshed/katex/dist/katex.css \ - $(BUILDDIR)/html/bikeshed/katex/dist/fonts - @echo "Built $(BUILDDIR)/WD.tar." - -.PHONY: WD-echidna -WD-echidna: WD-tar - @if [ -z $(W3C_USERNAME) ] || \ - [ -z $(W3C_PASSWORD) ] || \ - [ -z $(DECISION_URL) ] ; then \ - echo "Must provide W3C_USERNAME, W3C_PASSWORD, and DECISION_URL environment variables"; \ - exit 1; \ - fi - curl 'https://labs.w3.org/echidna/api/request' \ - --user '$(W3C_USERNAME):$(W3C_PASSWORD)' \ - -F "tar=@$(BUILDDIR)/WD.tar" \ - -F "decision=$(DECISION_URL)" | tee $(BUILDDIR)/WD-echidna-id.txt - @echo - @echo "Published working draft. Check its status at https://labs.w3.org/echidna/api/status?id=`cat $(BUILDDIR)/WD-echidna-id.txt`" - -.PHONY: diff -diff: bikeshed - @echo "Downloading the old single-file html spec..." - curl `grep "^TR" index.bs | cut -d' ' -f2` -o $(BUILDDIR)/html/bikeshed/old.html - @echo "Done." - @echo "Diffing new against old (go get a coffee)..." - perl ../util/htmldiff.pl $(BUILDDIR)/html/bikeshed/old.html $(BUILDDIR)/html/bikeshed/index.html $(BUILDDIR)/html/bikeshed/diff.html - @echo "Done. The diff is at $(BUILDDIR)/html/bikeshed/diff.html" - -.PHONY: pickle -pickle: - $(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle - @echo - @echo "Build finished; now you can process the pickle files." - -.PHONY: json -json: - $(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json - @echo - @echo "Build finished; now you can process the JSON files." - -.PHONY: htmlhelp -htmlhelp: - $(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp - @echo - @echo "Build finished; now you can run HTML Help Workshop with the" \ - ".hhp project file in $(BUILDDIR)/htmlhelp." - -.PHONY: qthelp -qthelp: - $(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp - @echo - @echo "Build finished; now you can run "qcollectiongenerator" with the" \ - ".qhcp project file in $(BUILDDIR)/qthelp, like this:" - @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/WebAssembly.qhcp" - @echo "To view the help file:" - @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/WebAssembly.qhc" - -.PHONY: applehelp -applehelp: - $(SPHINXBUILD) -b applehelp $(ALLSPHINXOPTS) $(BUILDDIR)/applehelp - @echo - @echo "Build finished. The help book is in $(BUILDDIR)/applehelp." - @echo "N.B. You won't be able to view it unless you put it in" \ - "~/Library/Documentation/Help or install it in your application" \ - "bundle." - -.PHONY: devhelp -devhelp: - $(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp - @echo - @echo "Build finished." - @echo "To view the help file:" - @echo "# mkdir -p $$HOME/.local/share/devhelp/WebAssembly" - @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/WebAssembly" - @echo "# devhelp" - -.PHONY: epub -epub: - $(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub - @echo - @echo "Build finished. The epub file is in $(BUILDDIR)/epub." - -.PHONY: epub3 -epub3: - $(SPHINXBUILD) -b epub3 $(ALLSPHINXOPTS) $(BUILDDIR)/epub3 - @echo - @echo "Build finished. The epub3 file is in $(BUILDDIR)/epub3." - -.PHONY: latex -latex: - $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex - @echo - @echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex." - @echo "Run \`make' in that directory to run these through (pdf)latex" \ - "(use \`make latexpdf' here to do that automatically)." - -.PHONY: latexpdf -latexpdf: - $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex - @echo "Running LaTeX files through pdflatex..." - $(MAKE) -C $(BUILDDIR)/latex LATEXMKOPTS=" $(BUILDDIR)/latex/LOG 2>&1 || cat $(BUILDDIR)/latex/LOG - @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." - -.PHONY: latexpdfja -latexpdfja: - $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex - @echo "Running LaTeX files through platex and dvipdfmx..." - $(MAKE) -C $(BUILDDIR)/latex all-pdf-ja - @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." - -.PHONY: text -text: - $(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text - @echo - @echo "Build finished. The text files are in $(BUILDDIR)/text." - -.PHONY: man -man: - $(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man - @echo - @echo "Build finished. The manual pages are in $(BUILDDIR)/man." - -.PHONY: texinfo -texinfo: - $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo - @echo - @echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo." - @echo "Run \`make' in that directory to run these through makeinfo" \ - "(use \`make info' here to do that automatically)." - -.PHONY: info -info: - $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo - @echo "Running Texinfo files through makeinfo..." - make -C $(BUILDDIR)/texinfo info - @echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo." - -.PHONY: gettext -gettext: - $(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale - @echo - @echo "Build finished. The message catalogs are in $(BUILDDIR)/locale." - -.PHONY: changes -changes: - $(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes - @echo - @echo "The overview file is in $(BUILDDIR)/changes." - -.PHONY: linkcheck -linkcheck: - $(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck - @echo - @echo "Link check complete; look for any errors in the above output " \ - "or in $(BUILDDIR)/linkcheck/output.txt." - -.PHONY: doctest -doctest: - $(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest - @echo "Testing of doctests in the sources finished, look at the " \ - "results in $(BUILDDIR)/doctest/output.txt." - -.PHONY: coverage -coverage: - $(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage - @echo "Testing of coverage in the sources finished, look at the " \ - "results in $(BUILDDIR)/coverage/python.txt." - -.PHONY: xml -xml: - $(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml - @echo - @echo "Build finished. The XML files are in $(BUILDDIR)/xml." - -.PHONY: pseudoxml -pseudoxml: - $(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml - @echo - @echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml." - -.PHONY: dummy -dummy: - $(SPHINXBUILD) -b dummy $(ALLSPHINXOPTS) $(BUILDDIR)/dummy - @echo - @echo "Build finished. Dummy builder generates no files." diff --git a/document/core/README.md b/document/core/README.md deleted file mode 100644 index 299b7a3a..00000000 --- a/document/core/README.md +++ /dev/null @@ -1,25 +0,0 @@ -# WebAssembly Core Specification - -This is the official WebAssembly "language" specification. - -It uses [Sphinx](http://www.sphinx-doc.org/). To install that: -``` -pip install sphinx -``` -To make HTML (result in `_build/html`): -``` -make html -``` -To make PDF (result in `_build/latex`, requires LaTeX): -``` -make pdf -``` -To make all: -``` -make all -``` -Finally, to make all and update webassembly.github.io/spec with it: -``` -make publish -``` -Please make sure to only use that once a change has approval. diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst deleted file mode 100644 index 19ec29a0..00000000 --- a/document/core/appendix/algorithm.rst +++ /dev/null @@ -1,233 +0,0 @@ -.. index:: validation, algorithm, instruction, module, binary format, opcode -.. _algo-valid: - -Validation Algorithm --------------------- - -The specification of WebAssembly :ref:`validation ` is purely *declarative*. -It describes the constraints that must be met by a :ref:`module ` or :ref:`instruction ` sequence to be valid. - -This section sketches the skeleton of a sound and complete *algorithm* for effectively validating code, i.e., sequences of :ref:`instructions `. -(Other aspects of validation are straightforward to implement.) - -In fact, the algorithm is expressed over the flat sequence of opcodes as occurring in the :ref:`binary format `, and performs only a single pass over it. -Consequently, it can be integrated directly into a decoder. - -The algorithm is expressed in typed pseudo code whose semantics is intended to be self-explanatory. - - -.. index:: value type, stack, label, frame, instruction - -Data Structures -~~~~~~~~~~~~~~~ - -Types are representable as an enumeration. -A simple subtyping check can be defined on these types. - -.. code-block:: pseudo - - type val_type = I32 | I64 | F32 | F64 | Anyref | Funcref | Nullref | Bot - - func is_num(t : val_type) : bool = - return t = I32 || t = I64 || t = F32 || t = F64 || t = Bot - - func is_ref(t : val_type) : bool = - return t = Anyref || t = Funcref || t = Nullref || t = Bot - - func matches(t1 : val_type, t2 : val_type) : bool = - return t1 = t2 || t1 = Bot || - (t1 = Nullref && is_ref(t2)) || (is_ref(t1) && t2 = Anyref) - -The algorithm uses two separate stacks: the *value stack* and the *control stack*. -The former tracks the :ref:`types ` of operand values on the :ref:`stack `, -the latter surrounding :ref:`structured control instructions ` and their associated :ref:`blocks `. - -.. code-block:: pseudo - - type val_stack = stack(val_type) - - type ctrl_stack = stack(ctrl_frame) - type ctrl_frame = { - label_types : list(val_type) - end_types : list(val_type) - height : nat - unreachable : bool - } - -For each value, the value stack records its :ref:`value type `. - -For each entered block, the control stack records a *control frame* with the type of the associated :ref:`label ` (used to type-check branches), the result type of the block (used to check its result), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic ` typing after branches). - -.. note:: - In the presentation of this algorithm, multiple values are supported for the :ref:`result types ` classifying blocks and labels. - With the current version of WebAssembly, the :code:`list` could be simplified to an optional value. - -For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global variables: - -.. code-block:: pseudo - - var vals : val_stack - var ctrls : ctrl_stack - -However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary functions: - -.. code-block:: pseudo - - func push_val(type : val_type) = - vals.push(type) - - func pop_val() : val_type = - if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Bot - error_if(vals.size() = ctrls[0].height) - return vals.pop() - - func pop_val(expect : val_type) : val_type = - let actual = pop_val() - error_if(not matches(actual, expect)) - return actual - - func push_vals(types : list(val_type)) = foreach (t in types) push_val(t) - func pop_vals(types : list(val_type)) : list(val_type) = - var popped := [] - foreach (t in reverse(types)) popped.append(pop_val(t)) - return popped - -Pushing an operand value simply pushes the respective type to the value stack. - -Popping an operand value checks that the value stack does not underflow the current block and then removes one type. -But first, a special case is handled where the block contains no known values, but has been marked as unreachable. -That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically `. -In that case, the :code:`Bot` type is returned, because that is a *principal* choice trivially satisfying all use constraints. - -A second function for popping an operand value takes an expected type, which the actual operand type is checked against. -The types may differ by subtyping, including the case where the actual type is :code:`Bot`, and thereby matches unconditionally. -The function returns the actual type popped from the stack. - -Finally, there are accumulative functions for pushing or popping multiple operand types. - -.. note:: - The notation :code:`stack[i]` is meant to index the stack from the top, - so that, e.g., :code:`ctrls[0]` accesses the element pushed last. - - -The control stack is likewise manipulated through auxiliary functions: - -.. code-block:: pseudo - - func push_ctrl(label : list(val_type), out : list(val_type)) = -  let frame = ctrl_frame(label, out, vals.size(), false) -   ctrls.push(frame) - - func pop_ctrl() : list(val_type) = -  error_if(ctrls.is_empty()) -  let frame = ctrls[0] -   pop_vals(frame.end_types) -   error_if(vals.size() =/= frame.height) - ctrls.pop() -   return frame.end_types - - func unreachable() = -   vals.resize(ctrls[0].height) -   ctrls[0].unreachable := true - -Pushing a control frame takes the types of the label and result values. -It allocates a new frame record recording them along with the current height of the operand stack and marks the block as reachable. - -Popping a frame first checks that the control stack is not empty. -It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack. -Afterwards, it checks that the stack has shrunk back to its initial height. - -Finally, the current frame can be marked as unreachable. -In that case, all existing operand types are purged from the value stack, in order to allow for the :ref:`stack-polymorphism ` logic in :code:`pop_val` to take effect. - -.. note:: - Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack. - That is necessary to detect invalid :ref:`examples ` like :math:`(\UNREACHABLE~(\I32.\CONST)~\I64.\ADD)`. - However, a polymorphic stack cannot underflow, but instead generates :code:`Bot` types as needed. - - -.. index:: opcode - -Validation of Instruction Sequences -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The following function shows the validation of a number of representative instructions that manipulate the stack. -Other instructions are checked in a similar manner. - -.. note:: - Various instructions not shown here will additionally require the presence of a validation :ref:`context ` for checking uses of :ref:`indices `. - That is an easy addition and therefore omitted from this presentation. - -.. code-block:: pseudo - - func validate(opcode) = - switch (opcode) - case (i32.add) - pop_val(I32) - pop_val(I32) - push_val(I32) - - case (drop) - pop_val() - - case (select) - pop_val(I32) - let t1 = pop_val() - let t2 = pop_val() - error_if(not (is_num(t1) && is_num(t2))) - error_if(t1 =/= t2 && t1 =/= Bot && t2 =/= Bot) - push_val(if (t1 = Bot) t2 else t1) - - case (select t) - pop_val(I32) - pop_val(t) - pop_val(t) - push_val(t) - -    case (unreachable) -       unreachable() - - case (block t*) - push_ctrl([t*], [t*]) - - case (loop t*) - push_ctrl([], [t*]) - - case (if t*) - pop_val(I32) - push_ctrl([t*], [t*]) - - case (end) - let results = pop_ctrl() - push_vals(results) - - case (else) - let results = pop_ctrl() - push_ctrl(results, results) - - case (br n) -      error_if(ctrls.size() < n) -       pop_vals(ctrls[n].label_types) -       unreachable() - - case (br_if n) -      error_if(ctrls.size() < n) - pop_val(I32) -       pop_vals(ctrls[n].label_types) -       push_vals(ctrls[n].label_types) - -    case (br_table n* m) - pop_val(I32) -       error_if(ctrls.size() < m) - let arity = ctrls[m].label_types.size() -       foreach (n in n*) -         error_if(ctrls.size() < n) -         error_if(ctrls[n].label_types.size() =/= arity) - push_vals(pop_vals(ctrls[n].label_types)) - pop_vals(ctrls[m].label_types) -       unreachable() - -.. note:: - It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack. - This would change if the language were extended with stack instructions like :code:`dup`. - Under such an extension, the above algorithm would need to be refined by replacing the :code:`Unknown` type with proper *type variables* to ensure that all uses are consistent. diff --git a/document/core/appendix/custom.rst b/document/core/appendix/custom.rst deleted file mode 100644 index bea81d61..00000000 --- a/document/core/appendix/custom.rst +++ /dev/null @@ -1,145 +0,0 @@ -.. index:: custom section, section, binary format - -Custom Sections ---------------- - -This appendix defines dedicated :ref:`custom sections ` for WebAssembly's :ref:`binary format `. -Such sections do not contribute to, or otherwise affect, the WebAssembly semantics, and like any custom section they may be ignored by an implementation. -However, they provide useful meta data that implementations can make use of to improve user experience or take compilation hints. - -Currently, only one dedicated custom section is defined, the :ref:`name section`. - - -.. index:: ! name section, name, Unicode UTF-8 -.. _binary-namesec: - -Name Section -~~~~~~~~~~~~ - -The *name section* is a :ref:`custom section ` whose name string is itself :math:`\text{name}`. -The name section should appear only once in a module, and only after the :ref:`data section `. - -The purpose of this section is to attach printable names to definitions in a module, which e.g. can be used by a debugger or when parts of the module are to be rendered in :ref:`text form `. - -.. note:: - All :ref:`names ` are represented in |Unicode|_ encoded in UTF-8. - Names need not be unique. - - -.. _binary-namesubsection: - -Subsections -........... - -The :ref:`data ` of a name section consists of a sequence of *subsections*. -Each subsection consists of a - -* a one-byte subsection *id*, -* the |U32| *size* of the contents, in bytes, -* the actual *contents*, whose structure is depended on the subsection id. - -.. math:: - \begin{array}{llcll} - \production{name section} & \Bnamesec &::=& - \Bsection_0(\Bnamedata) \\ - \production{name data} & \Bnamedata &::=& - n{:}\Bname & (\iff n = \text{name}) \\ &&& - \Bmodulenamesubsec^? \\ &&& - \Bfuncnamesubsec^? \\ &&& - \Blocalnamesubsec^? \\ - \production{name subsection} & \Bnamesubsection_N(\B{B}) &::=& - N{:}\Bbyte~~\X{size}{:}\Bu32~~\B{B} - & (\iff \X{size} = ||\B{B}||) \\ - \end{array} - -The following subsection ids are used: - -== =========================================== -Id Subsection -== =========================================== - 0 :ref:`module name ` - 1 :ref:`function names ` - 2 :ref:`local names ` -== =========================================== - -Each subsection may occur at most once, and in order of increasing id. - - -.. index:: ! name map, index, index space -.. _binary-indirectnamemap: -.. _binary-namemap: - -Name Maps -......... - -A *name map* assigns :ref:`names ` to :ref:`indices ` in a given :ref:`index space `. -It consists of a :ref:`vector ` of index/name pairs in order of increasing index value. -Each index must be unique, but the assigned names need not be. - -.. math:: - \begin{array}{llclll} - \production{name map} & \Bnamemap &::=& - \Bvec(\Bnameassoc) \\ - \production{name association} & \Bnameassoc &::=& - \Bidx~\Bname \\ - \end{array} - -An *indirect name map* assigns :ref:`names ` to a two-dimensional :ref:`index space `, where secondary indices are *grouped* by primary indices. -It consists of a vector of primary index/name map pairs in order of increasing index value, where each name map in turn maps secondary indices to names. -Each primary index must be unique, and likewise each secondary index per individual name map. - -.. math:: - \begin{array}{llclll} - \production{indirect name map} & \Bindirectnamemap &::=& - \Bvec(\Bindirectnameassoc) \\ - \production{indirect name association} & \Bindirectnameassoc &::=& - \Bidx~\Bnamemap \\ - \end{array} - - -.. index:: module -.. _binary-modulenamesec: - -Module Names -............ - -The *module name subsection* has the id 0. -It simply consists of a single :ref:`name ` that is assigned to the module itself. - -.. math:: - \begin{array}{llclll} - \production{module name subsection} & \Bmodulenamesubsec &::=& - \Bnamesubsection_0(\Bname) \\ - \end{array} - - -.. index:: function, function index -.. _binary-funcnamesec: - -Function Names -.............. - -The *function name subsection* has the id 1. -It consists of a :ref:`name map ` assigning function names to :ref:`function indices `. - -.. math:: - \begin{array}{llclll} - \production{function name subsection} & \Bfuncnamesubsec &::=& - \Bnamesubsection_1(\Bnamemap) \\ - \end{array} - - -.. index:: function, local, function index, local index -.. _binary-localnamesec: - -Local Names -........... - -The *local name subsection* has the id 2. -It consists of an :ref:`indirect name map ` assigning local names to :ref:`local indices ` grouped by :ref:`function indices `. - -.. math:: - \begin{array}{llclll} - \production{local name subsection} & \Blocalnamesubsec &::=& - \Bnamesubsection_2(\Bindirectnamemap) \\ - \end{array} diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst deleted file mode 100644 index db83ae26..00000000 --- a/document/core/appendix/embedding.rst +++ /dev/null @@ -1,616 +0,0 @@ -.. index:: ! embedding, embedder, implementation, host -.. _embed: - -Embedding ---------- - -A WebAssembly implementation will typically be *embedded* into a *host* environment. -An *embedder* implements the connection between such a host environment and the WebAssembly semantics as defined in the main body of this specification. -An embedder is expected to interact with the semantics in well-defined ways. - -This section defines a suitable interface to the WebAssembly semantics in the form of entry points through which an embedder can access it. -The interface is intended to be complete, in the sense that an embedder does not need to reference other functional parts of the WebAssembly specification directly. - -.. note:: - On the other hand, an embedder does not need to provide the host environment with access to all functionality defined in this interface. - For example, an implementation may not support :ref:`parsing ` of the :ref:`text format `. - -Types -~~~~~ - -In the description of the embedder interface, syntactic classes from the :ref:`abstract syntax ` and the :ref:`runtime's abstract machine ` are used as names for variables that range over the possible objects from that class. -Hence, these syntactic classes can also be interpreted as types. - -For numeric parameters, notation like :math:`n:\u32` is used to specify a symbolic name in addition to the respective value range. - - -.. _embed-error: - -Errors -~~~~~~ - -Failure of an interface operation is indicated by an auxiliary syntactic class: - -.. math:: - \begin{array}{llll} - \production{(error)} & \error &::=& \ERROR \\ - \end{array} - -In addition to the error conditions specified explicitly in this section, implementations may also return errors when specific :ref:`implementation limitations ` are reached. - -.. note:: - Errors are abstract and unspecific with this definition. - Implementations can refine it to carry suitable classifications and diagnostic messages. - - -Pre- and Post-Conditions -~~~~~~~~~~~~~~~~~~~~~~~~ - -Some operations state *pre-conditions* about their arguments or *post-conditions* about their results. -It is the embedder's responsibility to meet the pre-conditions. -If it does, the post conditions are guaranteed by the semantics. - -In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for :ref:`runtime objects ` (:math:`store`, :math:`\moduleinst`, :math:`\externval`, :ref:`addresses `): - -* Every runtime object passed as a parameter must be :ref:`valid ` per an implicit pre-condition. - -* Every runtime object returned as a result is :ref:`valid ` per an implicit post-condition. - -.. note:: - As long as an embedder treats runtime objects as abstract and only creates and manipulates them through the interface defined here, all implicit pre-conditions are automatically met. - - - -.. index:: allocation, store -.. _embed-store: - -Store -~~~~~ - -.. _embed-store-init: - -:math:`\F{store\_init}() : \store` -.................................. - -1. Return the empty :ref:`store `. - -.. math:: - \begin{array}{lclll} - \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\ - \end{array} - - - -.. index:: module -.. _embed-module: - -Modules -~~~~~~~ - -.. index:: binary format -.. _embed-module-decode: - -:math:`\F{module\_decode}(\byte^\ast) : \module ~|~ \error` -........................................................... - -1. If there exists a derivation for the :ref:`byte ` sequence :math:`\byte^\ast` as a :math:`\Bmodule` according to the :ref:`binary grammar for modules `, yielding a :ref:`module ` :math:`m`, then return :math:`m`. - -2. Else, return :math:`\ERROR`. - -.. math:: - \begin{array}{lclll} - \F{module\_decode}(b^\ast) &=& m && (\iff \Bmodule \stackrel\ast\Longrightarrow m{:}b^\ast) \\ - \F{module\_decode}(b^\ast) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. index:: text format -.. _embed-module-parse: - -:math:`\F{module\_parse}(\char^\ast) : \module ~|~ \error` -.......................................................... - -1. If there exists a derivation for the :ref:`source ` :math:`\char^\ast` as a :math:`\Tmodule` according to the :ref:`text grammar for modules `, yielding a :ref:`module ` :math:`m`, then return :math:`m`. - -2. Else, return :math:`\ERROR`. - -.. math:: - \begin{array}{lclll} - \F{module\_parse}(c^\ast) &=& m && (\iff \Tmodule \stackrel\ast\Longrightarrow m{:}c^\ast) \\ - \F{module\_parse}(c^\ast) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. index:: validation -.. _embed-module-validate: - -:math:`\F{module\_validate}(\module) : \error^?` -................................................ - -1. If :math:`\module` is :ref:`valid `, then return nothing. - -2. Else, return :math:`\ERROR`. - -.. math:: - \begin{array}{lclll} - \F{module\_validate}(m) &=& \epsilon && (\iff {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\ - \F{module\_validate}(m) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. index:: instantiation, module instance -.. _embed-module-instantiate: - -:math:`\F{module\_instantiate}(\store, \module, \externval^\ast) : (\store, \moduleinst ~|~ \error)` -.................................................................................................... - -1. Try :ref:`instantiating ` :math:`\module` in :math:`\store` with :ref:`external values ` :math:`\externval^\ast` as imports: - - a. If it succeeds with a :ref:`module instance ` :math:`\moduleinst`, then let :math:`\X{result}` be :math:`\moduleinst`. - - b. Else, let :math:`\X{result}` be :math:`\ERROR`. - -2. Return the new store paired with :math:`\X{result}`. - -.. math:: - \begin{array}{lclll} - \F{module\_instantiate}(S, m, \X{ev}^\ast) &=& (S', F.\AMODULE) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \epsilon) \\ - \F{module\_instantiate}(S, m, \X{ev}^\ast) &=& (S', \ERROR) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \TRAP) \\ - \end{array} - -.. note:: - The store may be modified even in case of an error. - - -.. index:: import -.. _embed-module-imports: - -:math:`\F{module\_imports}(\module) : (\name, \name, \externtype)^\ast` -....................................................................... - -1. Pre-condition: :math:`\module` is :ref:`valid ` with external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`. - -2. Let :math:`\import^\ast` be the :ref:`imports ` :math:`\module.\MIMPORTS`. - -3. Assert: the length of :math:`\import^\ast` equals the length of :math:`\externtype^\ast`. - -4. For each :math:`\import_i` in :math:`\import^\ast` and corresponding :math:`\externtype_i` in :math:`\externtype^\ast`, do: - - a. Let :math:`\X{result}_i` be the triple :math:`(\import_i.\IMODULE, \import_i.\INAME, \externtype_i)`. - -5. Return the concatenation of all :math:`\X{result}_i`, in index order. - -6. Post-condition: each :math:`\externtype_i` is :ref:`valid `. - -.. math:: - ~ \\ - \begin{array}{lclll} - \F{module\_imports}(m) &=& (\X{im}.\IMODULE, \X{im}.\INAME, \externtype)^\ast \\ - && \qquad (\iff \X{im}^\ast = m.\MIMPORTS \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\ - \end{array} - - -.. index:: export -.. _embed-module-exports: - -:math:`\F{module\_exports}(\module) : (\name, \externtype)^\ast` -................................................................ - -1. Pre-condition: :math:`\module` is :ref:`valid ` with external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`. - -2. Let :math:`\export^\ast` be the :ref:`exports ` :math:`\module.\MEXPORTS`. - -3. Assert: the length of :math:`\export^\ast` equals the length of :math:`{\externtype'}^\ast`. - -4. For each :math:`\export_i` in :math:`\export^\ast` and corresponding :math:`\externtype'_i` in :math:`{\externtype'}^\ast`, do: - - a. Let :math:`\X{result}_i` be the pair :math:`(\export_i.\ENAME, \externtype'_i)`. - -5. Return the concatenation of all :math:`\X{result}_i`, in index order. - -6. Post-condition: each :math:`\externtype'_i` is :ref:`valid `. - -.. math:: - ~ \\ - \begin{array}{lclll} - \F{module\_exports}(m) &=& (\X{ex}.\ENAME, \externtype')^\ast \\ - && \qquad (\iff \X{ex}^\ast = m.\MEXPORTS \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\ - \end{array} - - -.. index:: module, module instance -.. _embed-instance: - -Module Instances -~~~~~~~~~~~~~~~~ - -.. index:: export, export instance - -.. _embed-instance-export: - -:math:`\F{instance\_export}(\moduleinst, \name) : \externval ~|~ \error` -........................................................................ - -1. Assert: due to :ref:`validity ` of the :ref:`module instance ` :math:`\moduleinst`, all its :ref:`export names ` are different. - -2. If there exists an :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS` such that :ref:`name ` :math:`\exportinst_i.\EINAME` equals :math:`\name`, then: - - a. Return the :ref:`external value ` :math:`\exportinst_i.\EIVALUE`. - -3. Else, return :math:`\ERROR`. - -.. math:: - ~ \\ - \begin{array}{lclll} - \F{instance\_export}(m, \name) &=& m.\MIEXPORTS[i].\EIVALUE && (\iff m.\MEXPORTS[i].\EINAME = \name) \\ - \F{instance\_export}(m, \name) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. index:: function, host function, function address, function instance, function type, store -.. _embed-func: - -Functions -~~~~~~~~~ - -.. _embed-func-alloc: - -:math:`\F{func\_alloc}(\store, \functype, \hostfunc) : (\store, \funcaddr)` -........................................................................... - -1. Pre-condition: :math:`\functype` is :math:`valid `. - -2. Let :math:`\funcaddr` be the result of :ref:`allocating a host function ` in :math:`\store` with :ref:`function type ` :math:`\functype` 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}) \\ - \end{array} - -.. note:: - This operation assumes that :math:`\hostfunc` satisfies the :ref:`pre- and post-conditions ` required for a function instance with type :math:`\functype`. - - Regular (non-host) function instances can only be created indirectly through :ref:`module instantiation `. - - -.. _embed-func-type: - -:math:`\F{func\_type}(\store, \funcaddr) : \functype` -..................................................... - -1. Return :math:`S.\SFUNCS[a].\FITYPE`. - -2. Post-condition: the returned :ref:`function type ` is :ref:`valid `. - -.. math:: - \begin{array}{lclll} - \F{func\_type}(S, a) &=& S.\SFUNCS[a].\FITYPE \\ - \end{array} - - -.. index:: invocation, value, result -.. _embed-func-invoke: - -:math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error)` -........................................................................................ - -1. Try :ref:`invoking ` the function :math:`\funcaddr` in :math:`\store` with :ref:`values ` :math:`\val^\ast` as arguments: - - a. If it succeeds with :ref:`values ` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`. - - b. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`. - -2. Return the new store paired with :math:`\X{result}`. - -.. math:: - ~ \\ - \begin{array}{lclll} - \F{func\_invoke}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; {v'}^\ast) \\ - \F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\ - \end{array} - -.. note:: - The store may be modified even in case of an error. - - -.. index:: table, table address, store, table instance, table type, element, function address -.. _embed-table: - -Tables -~~~~~~ - -.. _embed-table-alloc: - -:math:`\F{table\_alloc}(\store, \tabletype) : (\store, \tableaddr, \reff)` -.......................................................................... - -1. Pre-condition: :math:`\tabletype` is :math:`valid `. - -2. Let :math:`\tableaddr` be the result of :ref:`allocating a table ` in :math:`\store` with :ref:`table type ` :math:`\tabletype` and initialization value :math:`\reff`. - -3. Return the new store paired with :math:`\tableaddr`. - -.. math:: - \begin{array}{lclll} - \F{table\_alloc}(S, \X{tt}, r) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}, r) = S', \X{a}) \\ - \end{array} - - -.. _embed-table-type: - -:math:`\F{table\_type}(\store, \tableaddr) : \tabletype` -........................................................ - -1. Return :math:`S.\STABLES[a].\TITYPE`. - -2. Post-condition: the returned :ref:`table type ` is :math:`valid `. - -.. math:: - \begin{array}{lclll} - \F{table\_type}(S, a) &=& S.\STABLES[a].\TITYPE \\ - \end{array} - - -.. _embed-table-read: - -:math:`\F{table\_read}(\store, \tableaddr, i:\u32) : \reff ~|~ \error` -...................................................................... - -1. Let :math:`\X{ti}` be the :ref:`table instance ` :math:`\store.\STABLES[\tableaddr]`. - -2. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`. - -3. Else, return the :ref:`reference value ` :math:`\X{ti}.\TIELEM[i]`. - -.. math:: - \begin{array}{lclll} - \F{table\_read}(S, a, i) &=& r && (\iff S.\STABLES[a].\TIELEM[i] = r) \\ - \F{table\_read}(S, a, i) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. _embed-table-write: - -:math:`\F{table\_write}(\store, \tableaddr, i:\u32, \reff) : \store ~|~ \error` -............................................................................... - -1. Let :math:`\X{ti}` be the :ref:`table instance ` :math:`\store.\STABLES[\tableaddr]`. - -2. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`. - -3. Replace :math:`\X{ti}.\TIELEM[i]` with the :ref:`reference value ` :math:`\reff`. - -4. Return the updated store. - -.. math:: - \begin{array}{lclll} - \F{table\_write}(S, a, i, r) &=& S' && (\iff S' = S \with \STABLES[a].\TIELEM[i] = r) \\ - \F{table\_write}(S, a, i, r) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. _embed-table-size: - -:math:`\F{table\_size}(\store, \tableaddr) : \u32` -.................................................. - -1. Return the length of :math:`\store.\STABLES[\tableaddr].\TIELEM`. - -.. math:: - ~ \\ - \begin{array}{lclll} - \F{table\_size}(S, a) &=& n && - (\iff |S.\STABLES[a].\TIELEM| = n) \\ - \end{array} - - - -.. _embed-table-grow: - -:math:`\F{table\_grow}(\store, \tableaddr, n:\u32, \reff) : \store ~|~ \error` -.............................................................................. - -1. Try :ref:`growing ` the :ref:`table instance ` :math:`\store.\STABLES[\tableaddr]` by :math:`n` elements with initialization value :math:`\reff`: - - a. If it succeeds, return the updated store. - - b. Else, return :math:`\ERROR`. - -.. math:: - ~ \\ - \begin{array}{lclll} - \F{table\_grow}(S, a, n, r) &=& S' && - (\iff S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n, r)) \\ - \F{table\_grow}(S, a, n, r) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. index:: memory, memory address, store, memory instance, memory type, byte -.. _embed-mem: - -Memories -~~~~~~~~ - -.. _embed-mem-alloc: - -:math:`\F{mem\_alloc}(\store, \memtype) : (\store, \memaddr)` -................................................................ - -1. Pre-condition: :math:`\memtype` is :math:`valid `. - -2. Let :math:`\memaddr` be the result of :ref:`allocating a memory ` in :math:`\store` with :ref:`memory type ` :math:`\memtype`. - -3. Return the new store paired with :math:`\memaddr`. - -.. math:: - \begin{array}{lclll} - \F{mem\_alloc}(S, \X{mt}) &=& (S', \X{a}) && (\iff \allocmem(S, \X{mt}) = S', \X{a}) \\ - \end{array} - - -.. _embed-mem-type: - -:math:`\F{mem\_type}(\store, \memaddr) : \memtype` -.................................................. - -1. Return :math:`S.\SMEMS[a].\MITYPE`. - -2. Post-condition: the returned :ref:`memory type ` is :math:`valid `. - -.. math:: - \begin{array}{lclll} - \F{mem\_type}(S, a) &=& S.\SMEMS[a].\MITYPE \\ - \end{array} - - -.. _embed-mem-read: - -:math:`\F{mem\_read}(\store, \memaddr, i:\u32) : \byte ~|~ \error` -.................................................................. - -1. Let :math:`\X{mi}` be the :ref:`memory instance ` :math:`\store.\SMEMS[\memaddr]`. - -2. If :math:`i` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`. - -3. Else, return the :ref:`byte ` :math:`\X{mi}.\MIDATA[i]`. - -.. math:: - \begin{array}{lclll} - \F{mem\_read}(S, a, i) &=& b && (\iff S.\SMEMS[a].\MIDATA[i] = b) \\ - \F{mem\_read}(S, a, i) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. _embed-mem-write: - -:math:`\F{mem\_write}(\store, \memaddr, i:\u32, \byte) : \store ~|~ \error` -........................................................................... - -1. Let :math:`\X{mi}` be the :ref:`memory instance ` :math:`\store.\SMEMS[\memaddr]`. - -2. If :math:`\u32` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`. - -3. Replace :math:`\X{mi}.\MIDATA[i]` with :math:`\byte`. - -4. Return the updated store. - -.. math:: - \begin{array}{lclll} - \F{mem\_write}(S, a, i, b) &=& S' && (\iff S' = S \with \SMEMS[a].\MIDATA[i] = b) \\ - \F{mem\_write}(S, a, i, b) &=& \ERROR && (\otherwise) \\ - \end{array} - - -.. _embed-mem-size: - -:math:`\F{mem\_size}(\store, \memaddr) : \u32` -.............................................. - -1. Return the length of :math:`\store.\SMEMS[\memaddr].\MIDATA` divided by the :ref:`page size `. - -.. math:: - ~ \\ - \begin{array}{lclll} - \F{mem\_size}(S, a) &=& n && - (\iff |S.\SMEMS[a].\MIDATA| = n \cdot 64\,\F{Ki}) \\ - \end{array} - - - -.. _embed-mem-grow: - -:math:`\F{mem\_grow}(\store, \memaddr, n:\u32) : \store ~|~ \error` -................................................................... - -1. Try :ref:`growing ` the :ref:`memory instance ` :math:`\store.\SMEMS[\memaddr]` by :math:`n` :ref:`pages `: - - a. If it succeeds, return the updated store. - - b. Else, return :math:`\ERROR`. - -.. math:: - ~ \\ - \begin{array}{lclll} - \F{mem\_grow}(S, a, n) &=& S' && - (\iff S' = S \with \SMEMS[a] = \growmem(S.\SMEMS[a], n)) \\ - \F{mem\_grow}(S, a, n) &=& \ERROR && (\otherwise) \\ - \end{array} - - - -.. index:: global, global address, store, global instance, global type, value -.. _embed-global: - -Globals -~~~~~~~ - -.. _embed-global-alloc: - -:math:`\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)` -............................................................................ - -1. Pre-condition: :math:`\globaltype` is :math:`valid `. - -2. Let :math:`\globaladdr` be the result of :ref:`allocating a global ` in :math:`\store` with :ref:`global type ` :math:`\globaltype` and initialization value :math:`\val`. - -3. Return the new store paired with :math:`\globaladdr`. - -.. math:: - \begin{array}{lclll} - \F{global\_alloc}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\ - \end{array} - - -.. _embed-global-type: - -:math:`\F{global\_type}(\store, \globaladdr) : \globaltype` -........................................................... - -1. Return :math:`S.\SGLOBALS[a].\GITYPE`. - -2. Post-condition: the returned :ref:`global type ` is :math:`valid `. - -.. math:: - \begin{array}{lclll} - \F{global\_type}(S, a) &=& S.\SGLOBALS[a].\GITYPE \\ - \end{array} - - -.. _embed-global-read: - -:math:`\F{global\_read}(\store, \globaladdr) : \val` -.................................................... - -1. Let :math:`\X{gi}` be the :ref:`global instance ` :math:`\store.\SGLOBALS[\globaladdr]`. - -2. Return the :ref:`value ` :math:`\X{gi}.\GIVALUE`. - -.. math:: - \begin{array}{lclll} - \F{global\_read}(S, a) &=& v && (\iff S.\SGLOBALS[a].\GIVALUE = v) \\ - \end{array} - - -.. _embed-global-write: - -:math:`\F{global\_write}(\store, \globaladdr, \val) : \store ~|~ \error` -........................................................................ - -1. Let :math:`\X{gi}` be the :ref:`global instance ` :math:`\store.\SGLOBALS[\globaladdr]`. - -2. Let :math:`\mut~t` be the structure of the :ref:`global type ` :math:`\X{gi}.\GITYPE`. - -3. If :math:`\mut` is not :math:`\MVAR`, then return :math:`\ERROR`. - -4. Replace :math:`\X{gi}.\GIVALUE` with the :ref:`value ` :math:`\val`. - -5. Return the updated store. - -.. math:: - ~ \\ - \begin{array}{lclll} - \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} diff --git a/document/core/appendix/implementation.rst b/document/core/appendix/implementation.rst deleted file mode 100644 index df2885cc..00000000 --- a/document/core/appendix/implementation.rst +++ /dev/null @@ -1,137 +0,0 @@ -.. index:: ! implementation limitations, implementation -.. _impl: - -Implementation Limitations --------------------------- - -Implementations typically impose additional restrictions on a number of aspects of a WebAssembly module or execution. -These may stem from: - -* physical resource limits, -* constraints imposed by the embedder or its environment, -* limitations of selected implementation strategies. - -This section lists allowed limitations. -Where restrictions take the form of numeric limits, no minimum requirements are given, -nor are the limits assumed to be concrete, fixed numbers. -However, it is expected that all implementations have "reasonably" large limits to enable common applications. - -.. note:: - A conforming implementation is not allowed to leave out individual *features*. - However, designated subsets of WebAssembly may be specified in the future. - - -Syntactic Limits -~~~~~~~~~~~~~~~~ - -.. index:: abstract syntax, module, type, function, table, memory, global, element, data, import, export, parameter, result, local, structured control instruction, instruction, name, Unicode, character -.. _impl-syntax: - -Structure -......... - -An implementation may impose restrictions on the following dimensions of a module: - -* the number of :ref:`types ` in a :ref:`module ` -* the number of :ref:`functions ` in a :ref:`module `, including imports -* the number of :ref:`tables ` in a :ref:`module `, including imports -* the number of :ref:`memories ` in a :ref:`module `, including imports -* the number of :ref:`globals ` in a :ref:`module `, including imports -* the number of :ref:`element segments ` in a :ref:`module ` -* the number of :ref:`data segments ` in a :ref:`module ` -* the number of :ref:`imports ` to a :ref:`module ` -* the number of :ref:`exports ` from a :ref:`module ` -* the number of parameters in a :ref:`function type ` -* the number of results in a :ref:`function type ` -* the number of :ref:`locals ` in a :ref:`function ` -* the size of a :ref:`function ` body -* the size of a :ref:`structured control instruction ` -* the number of :ref:`structured control instructions ` in a :ref:`function ` -* the nesting depth of :ref:`structured control instructions ` -* the number of :ref:`label indices ` in a |brtable| instruction -* the length of an :ref:`element segment ` -* the length of a :ref:`data segment ` -* the length of a :ref:`name ` -* the range of :ref:`characters ` in a :ref:`name ` - -If the limits of an implementation are exceeded for a given module, -then the implementation may reject the :ref:`validation `, compilation, or :ref:`instantiation ` of that module with an embedder-specific error. - -.. note:: - The last item allows :ref:`embedders ` that operate in limited environments without support for - |Unicode|_ to limit the - names of :ref:`imports ` and :ref:`exports ` - to common subsets like |ASCII|_. - - -.. index:: binary format, module, section, function, code -.. _impl-binary: - -Binary Format -............. - -For a module given in :ref:`binary format `, additional limitations may be imposed on the following dimensions: - -* the size of a :ref:`module ` -* the size of any :ref:`section ` -* the size of an individual function's :ref:`code ` -* the number of :ref:`sections ` - - -.. index:: text format, source text, token, identifier, character, unicode -.. _impl-text: - -Text Format -........... - -For a module given in :ref:`text format `, additional limitations may be imposed on the following dimensions: - -* the size of the :ref:`source text ` -* the size of any syntactic element -* the size of an individual :ref:`token ` -* the nesting depth of :ref:`folded instructions ` -* the length of symbolic :ref:`identifiers ` -* the range of literal :ref:`characters ` allowed in the :ref:`source text ` - - -.. index:: validation, function -.. _impl-valid: - -Validation -~~~~~~~~~~ - -An implementation may defer :ref:`validation ` of individual :ref:`functions ` until they are first :ref:`invoked `. - -If a function turns out to be invalid, then the invocation, and every consecutive call to the same function, results in a :ref:`trap `. - -.. note:: - This is to allow implementations to use interpretation or just-in-time compilation for functions. - The function must still be fully validated before execution of its body begins. - - -.. index:: execution, module instance, function instance, table instance, memory instance, global instance, allocation, frame, label, value -.. _impl-exec: - -Execution -~~~~~~~~~ - -Restrictions on the following dimensions may be imposed during :ref:`execution ` of a WebAssembly program: - -* the number of allocated :ref:`module instances ` -* the number of allocated :ref:`function instances ` -* the number of allocated :ref:`table instances ` -* the number of allocated :ref:`memory instances ` -* the number of allocated :ref:`global instances ` -* the size of a :ref:`table instance ` -* the size of a :ref:`memory instance ` -* the number of :ref:`frames ` on the :ref:`stack ` -* the number of :ref:`labels ` on the :ref:`stack ` -* the number of :ref:`values ` on the :ref:`stack ` - -If the runtime limits of an implementation are exceeded during execution of a computation, -then it may terminate that computation and report an embedder-specific error to the invoking code. - -Some of the above limits may already be verified during instantiation, in which case an implementation may report exceedance in the same manner as for :ref:`syntactic limits `. - -.. note:: - Concrete limits are usually not fixed but may be dependent on specifics, interdependent, vary over time, or depend on other implementation- or embedder-specific situations or events. diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst deleted file mode 100644 index 394a98e5..00000000 --- a/document/core/appendix/index-instructions.rst +++ /dev/null @@ -1,221 +0,0 @@ -.. index:: instruction -.. _index-instr: - -Index of Instructions ---------------------- - -====================================== ================ ========================================== ======================================== =============================================================== -Instruction Binary Opcode Type Validation Execution -====================================== ================ ========================================== ======================================== =============================================================== -:math:`\UNREACHABLE` :math:`\hex{00}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\NOP` :math:`\hex{01}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` -:math:`\BLOCK~[t^?]` :math:`\hex{02}` :math:`[] \to [t^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\LOOP~[t^?]` :math:`\hex{03}` :math:`[] \to [t^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\IF~[t^?]` :math:`\hex{04}` :math:`[\I32] \to [t^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\ELSE` :math:`\hex{05}` -(reserved) :math:`\hex{06}` -(reserved) :math:`\hex{07}` -(reserved) :math:`\hex{08}` -(reserved) :math:`\hex{09}` -(reserved) :math:`\hex{0A}` -:math:`\END` :math:`\hex{0B}` -:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^?~\I32] \to [t^?]` :ref:`validation ` :ref:`execution ` -:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^?~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -:math:`\CALLINDIRECT~x` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{12}` -(reserved) :math:`\hex{13}` -(reserved) :math:`\hex{14}` -(reserved) :math:`\hex{15}` -(reserved) :math:`\hex{16}` -(reserved) :math:`\hex{17}` -(reserved) :math:`\hex{18}` -(reserved) :math:`\hex{19}` -:math:`\DROP` :math:`\hex{1A}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\SELECT` :math:`\hex{1B}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\SELECT~t` :math:`\hex{1C}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{1D}` -(reserved) :math:`\hex{1E}` -(reserved) :math:`\hex{1F}` -:math:`\LOCALGET~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\LOCALSET~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\LOCALTEE~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\GLOBALGET~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\GLOBALSET~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` -:math:`\TABLEGET~x` :math:`\hex{25}` :math:`[\I32] \to [t]` :ref:`validation ` :ref:`execution ` -:math:`\TABLESET~x` :math:`\hex{26}` :math:`[\I32~t] \to []` :ref:`validation ` :ref:`execution ` -(reserved) :math:`\hex{27}` -:math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\F32.\LOAD~\memarg` :math:`\hex{2A}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution ` -:math:`\F64.\LOAD~\memarg` :math:`\hex{2B}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{8\_s}~\memarg` :math:`\hex{2C}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{8\_u}~\memarg` :math:`\hex{2D}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{16\_s}~\memarg` :math:`\hex{2E}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\LOAD\K{16\_u}~\memarg` :math:`\hex{2F}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{8\_s}~\memarg` :math:`\hex{30}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{8\_u}~\memarg` :math:`\hex{31}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{16\_s}~\memarg` :math:`\hex{32}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{16\_u}~\memarg` :math:`\hex{33}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{32\_s}~\memarg` :math:`\hex{34}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\LOAD\K{32\_u}~\memarg` :math:`\hex{35}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE~\memarg` :math:`\hex{36}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE~\memarg` :math:`\hex{37}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\F32.\STORE~\memarg` :math:`\hex{38}` :math:`[\I32~\F32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\F64.\STORE~\memarg` :math:`\hex{39}` :math:`[\I32~\F64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE\K{8}~\memarg` :math:`\hex{3A}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I32.\STORE\K{16}~\memarg` :math:`\hex{3B}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{8}~\memarg` :math:`\hex{3C}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{16}~\memarg` :math:`\hex{3D}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\I64.\STORE\K{32}~\memarg` :math:`\hex{3E}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYSIZE` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\MEMORYGROW` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\CONST~\i32` :math:`\hex{41}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\I64.\CONST~\i64` :math:`\hex{42}` :math:`[] \to [\I64]` :ref:`validation ` :ref:`execution ` -:math:`\F32.\CONST~\f32` :math:`\hex{43}` :math:`[] \to [\F32]` :ref:`validation ` :ref:`execution ` -:math:`\F64.\CONST~\f64` :math:`\hex{44}` :math:`[] \to [\F64]` :ref:`validation ` :ref:`execution ` -:math:`\I32.\EQZ` :math:`\hex{45}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\EQ` :math:`\hex{46}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\NE` :math:`\hex{47}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LT\K{\_s}` :math:`\hex{48}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LT\K{\_u}` :math:`\hex{49}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GT\K{\_s}` :math:`\hex{4A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GT\K{\_u}` :math:`\hex{4B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LE\K{\_s}` :math:`\hex{4C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\LE\K{\_u}` :math:`\hex{4D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GE\K{\_s}` :math:`\hex{4E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\GE\K{\_u}` :math:`\hex{4F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EQZ` :math:`\hex{50}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EQ` :math:`\hex{51}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\NE` :math:`\hex{52}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LT\K{\_s}` :math:`\hex{53}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LT\K{\_u}` :math:`\hex{54}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GT\K{\_s}` :math:`\hex{55}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GT\K{\_u}` :math:`\hex{56}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LE\K{\_s}` :math:`\hex{57}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\LE\K{\_u}` :math:`\hex{58}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GE\K{\_s}` :math:`\hex{59}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\GE\K{\_u}` :math:`\hex{5A}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\EQ` :math:`\hex{5B}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NE` :math:`\hex{5C}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\LT` :math:`\hex{5D}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\GT` :math:`\hex{5E}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\LE` :math:`\hex{5F}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\GE` :math:`\hex{60}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\EQ` :math:`\hex{61}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NE` :math:`\hex{62}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\LT` :math:`\hex{63}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\GT` :math:`\hex{64}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\LE` :math:`\hex{65}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\GE` :math:`\hex{66}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\CLZ` :math:`\hex{67}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\CTZ` :math:`\hex{68}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\POPCNT` :math:`\hex{69}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ADD` :math:`\hex{6A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SUB` :math:`\hex{6B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\MUL` :math:`\hex{6C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\DIV\K{\_s}` :math:`\hex{6D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\DIV\K{\_u}` :math:`\hex{6E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REM\K{\_s}` :math:`\hex{6F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REM\K{\_u}` :math:`\hex{70}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\AND` :math:`\hex{71}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\OR` :math:`\hex{72}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\XOR` :math:`\hex{73}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHL` :math:`\hex{74}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHR\K{\_s}` :math:`\hex{75}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\SHR\K{\_u}` :math:`\hex{76}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ROTL` :math:`\hex{77}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\ROTR` :math:`\hex{78}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\CLZ` :math:`\hex{79}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\CTZ` :math:`\hex{7A}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\POPCNT` :math:`\hex{7B}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ADD` :math:`\hex{7C}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SUB` :math:`\hex{7D}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\MUL` :math:`\hex{7E}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\DIV\K{\_s}` :math:`\hex{7F}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\DIV\K{\_u}` :math:`\hex{80}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REM\K{\_s}` :math:`\hex{81}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REM\K{\_u}` :math:`\hex{82}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\AND` :math:`\hex{83}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\OR` :math:`\hex{84}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\XOR` :math:`\hex{85}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHL` :math:`\hex{86}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHR\K{\_s}` :math:`\hex{87}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\SHR\K{\_u}` :math:`\hex{88}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ROTL` :math:`\hex{89}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\ROTR` :math:`\hex{8A}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\ABS` :math:`\hex{8B}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NEG` :math:`\hex{8C}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CEIL` :math:`\hex{8D}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FLOOR` :math:`\hex{8E}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\TRUNC` :math:`\hex{8F}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\NEAREST` :math:`\hex{90}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\SQRT` :math:`\hex{91}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\ADD` :math:`\hex{92}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\SUB` :math:`\hex{93}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\MUL` :math:`\hex{94}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\DIV` :math:`\hex{95}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FMIN` :math:`\hex{96}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\FMAX` :math:`\hex{97}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\COPYSIGN` :math:`\hex{98}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\ABS` :math:`\hex{99}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NEG` :math:`\hex{9A}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CEIL` :math:`\hex{9B}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FLOOR` :math:`\hex{9C}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\TRUNC` :math:`\hex{9D}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\NEAREST` :math:`\hex{9E}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\SQRT` :math:`\hex{9F}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\ADD` :math:`\hex{A0}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\SUB` :math:`\hex{A1}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\MUL` :math:`\hex{A2}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\DIV` :math:`\hex{A3}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FMIN` :math:`\hex{A4}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\FMAX` :math:`\hex{A5}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\COPYSIGN` :math:`\hex{A6}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\WRAP\K{\_}\I64` :math:`\hex{A7}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{\_}\I32\K{\_s}` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\EXTEND\K{\_}\I32\K{\_u}` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{B5}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\DEMOTE\K{\_}\F64` :math:`\hex{B6}` :math:`[\F64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{BA}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\PROMOTE\K{\_}\F32` :math:`\hex{BB}` :math:`[\F32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I32.\REINTERPRET\K{\_}\F32` :math:`\hex{BC}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\I64.\REINTERPRET\K{\_}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F32.\REINTERPRET\K{\_}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -:math:`\F64.\REINTERPRET\K{\_}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` -(reserved) :math:`\hex{C0}` -(reserved) :math:`\hex{C1}` -(reserved) :math:`\hex{C2}` -(reserved) :math:`\hex{C3}` -(reserved) :math:`\hex{C4}` -(reserved) :math:`\hex{C5}` -(reserved) :math:`\hex{C6}` -(reserved) :math:`\hex{C7}` -(reserved) :math:`\hex{C8}` -(reserved) :math:`\hex{C9}` -(reserved) :math:`\hex{CA}` -(reserved) :math:`\hex{CB}` -(reserved) :math:`\hex{CC}` -(reserved) :math:`\hex{CD}` -(reserved) :math:`\hex{CE}` -(reserved) :math:`\hex{CF}` -:math:`\REFNULL` :math:`\hex{D0}` :math:`[] \to [\NULLREF]` :ref:`validation ` :ref:`execution ` -:math:`\REFISNULL` :math:`\hex{D1}` :math:`[\ANYREF] \to [\I32]` :ref:`validation ` :ref:`execution ` -:math:`\REFFUNC~x` :math:`\hex{D2}` :math:`[] \to [\FUNCREF]` :ref:`validation ` :ref:`execution ` -====================================== ================ ========================================== ======================================== =============================================================== diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst deleted file mode 100644 index fe1fb3f2..00000000 --- a/document/core/appendix/index-rules.rst +++ /dev/null @@ -1,112 +0,0 @@ -.. _index-rules: - -Index of Semantic Rules ------------------------ - - -.. index:: validation -.. _index-valid: - -Typing of Static Constructs -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -=============================================== =============================================================================== -Construct Judgement -=============================================== =============================================================================== -:ref:`Limits ` :math:`\vdashlimits \limits : k` -:ref:`Function type ` :math:`\vdashfunctype \functype \ok` -:ref:`Table type ` :math:`\vdashtabletype \tabletype \ok` -:ref:`Memory type ` :math:`\vdashmemtype \memtype \ok` -:ref:`Global type ` :math:`\vdashglobaltype \globaltype \ok` -:ref:`External type ` :math:`\vdashexterntype \externtype \ok` -:ref:`Instruction ` :math:`S;C \vdashinstr \instr : \functype` -:ref:`Instruction sequence ` :math:`S;C \vdashinstrseq \instr^\ast : \functype` -:ref:`Expression ` :math:`C \vdashexpr \expr : \resulttype` -:ref:`Function ` :math:`C \vdashfunc \func : \functype` -:ref:`Table ` :math:`C \vdashtable \table : \tabletype` -:ref:`Memory ` :math:`C \vdashmem \mem : \memtype` -:ref:`Global ` :math:`C \vdashglobal \global : \globaltype` -:ref:`Element segment ` :math:`C \vdashelem \elem \ok` -:ref:`Data segment ` :math:`C \vdashdata \data \ok` -:ref:`Start function ` :math:`C \vdashstart \start \ok` -:ref:`Export ` :math:`C \vdashexport \export : \externtype` -:ref:`Export description ` :math:`C \vdashexportdesc \exportdesc : \externtype` -:ref:`Import ` :math:`C \vdashimport \import : \externtype` -:ref:`Import description ` :math:`C \vdashimportdesc \importdesc : \externtype` -:ref:`Module ` :math:`\vdashmodule \module : \externtype^\ast \to \externtype^\ast` -=============================================== =============================================================================== - - -.. index:: runtime - -Typing of Runtime Constructs -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -=============================================== =============================================================================== -Construct Judgement -=============================================== =============================================================================== -:ref:`Value ` :math:`S \vdashval \val : \valtype` -:ref:`Result ` :math:`S \vdashresult \result : \resulttype` -:ref:`External value ` :math:`S \vdashexternval \externval : \externtype` -:ref:`Function instance ` :math:`S \vdashfuncinst \funcinst : \functype` -:ref:`Table instance ` :math:`S \vdashtableinst \tableinst : \tabletype` -:ref:`Memory instance ` :math:`S \vdashmeminst \meminst : \memtype` -:ref:`Global instance ` :math:`S \vdashglobalinst \globalinst : \globaltype` -:ref:`Export instance ` :math:`S \vdashexportinst \exportinst \ok` -:ref:`Module instance ` :math:`S \vdashmoduleinst \moduleinst : C` -:ref:`Store ` :math:`\vdashstore \store \ok` -:ref:`Configuration ` :math:`\vdashconfig \config \ok` -:ref:`Thread ` :math:`S;\resulttype^? \vdashthread \thread : \resulttype` -:ref:`Frame ` :math:`S \vdashframe \frame : C` -=============================================== =============================================================================== - - -Constantness -~~~~~~~~~~~~ - -=============================================== =============================================================================== -Construct Judgement -=============================================== =============================================================================== -:ref:`Constant expression ` :math:`C \vdashexprconst \expr \const` -:ref:`Constant instruction ` :math:`C \vdashinstrconst \instr \const` -=============================================== =============================================================================== - - -Matching -~~~~~~~~ - -=============================================== =============================================================================== -Construct Judgement -=============================================== =============================================================================== -:ref:`Number type ` :math:`\vdashnumtypematch \numtype_1 \matchesvaltype \numtype_2` -:ref:`Reference type ` :math:`\vdashreftypematch \reftype_1 \matchesvaltype \reftype_2` -:ref:`Value type ` :math:`\vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2` -:ref:`Result type ` :math:`\vdashresulttypematch [t_1^?] \matchesresulttype [t_2^?]` -:ref:`External type ` :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2` -:ref:`Limits ` :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2` -=============================================== =============================================================================== - - -Store Extension -~~~~~~~~~~~~~~~ - -=============================================== =============================================================================== -Construct Judgement -=============================================== =============================================================================== -:ref:`Function instance ` :math:`\vdashfuncinstextends \funcinst_1 \extendsto \funcinst_2` -:ref:`Table instance ` :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2` -:ref:`Memory instance ` :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2` -:ref:`Global instance ` :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2` -:ref:`Store ` :math:`\vdashstoreextends \store_1 \extendsto \store_2` -=============================================== =============================================================================== - - -Execution -~~~~~~~~~ - -=============================================== =============================================================================== -Construct Judgement -=============================================== =============================================================================== -:ref:`Instruction ` :math:`S;F;\instr^\ast \stepto S';F';{\instr'}^\ast` -:ref:`Expression ` :math:`S;F;\expr \stepto S';F';\expr'` -=============================================== =============================================================================== diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst deleted file mode 100644 index 37f33c7b..00000000 --- a/document/core/appendix/index-types.rst +++ /dev/null @@ -1,26 +0,0 @@ -.. index:: type -.. _index-type: - -Index of Types --------------- - -======================================== =========================================== =============================================================================== -Category Constructor Binary Opcode -======================================== =========================================== =============================================================================== -:ref:`Type index ` :math:`x` (positive number as |Bs32| or |Bu32|) -:ref:`Number type ` |I32| :math:`\hex{7F}` (-1 as |Bs7|) -:ref:`Number type ` |I64| :math:`\hex{7E}` (-2 as |Bs7|) -:ref:`Number type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) -:ref:`Number type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) -(reserved) :math:`\hex{7B}` .. :math:`\hex{71}` -:ref:`Reference type ` |FUNCREF| :math:`\hex{70}` (-16 as |Bs7|) -:ref:`Reference type ` |ANYREF| :math:`\hex{6F}` (-17 as |Bs7|) -:ref:`Reference type ` |NULLREF| :math:`\hex{6E}` (-18 as |Bs7|) -(reserved) :math:`\hex{6D}` .. :math:`\hex{61}` -:ref:`Function type ` :math:`[\valtype^\ast] \to [\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) -(reserved) :math:`\hex{5F}` .. :math:`\hex{41}` -:ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) -:ref:`Table type ` :math:`\limits~\reftype` (none) -:ref:`Memory type ` :math:`\limits` (none) -:ref:`Global type ` :math:`\mut~\valtype` (none) -======================================== =========================================== =============================================================================== diff --git a/document/core/appendix/index.rst b/document/core/appendix/index.rst deleted file mode 100644 index 789d2140..00000000 --- a/document/core/appendix/index.rst +++ /dev/null @@ -1,22 +0,0 @@ -.. _appendix: - -Appendix -======== - -.. toctree:: - :maxdepth: 2 - - embedding - implementation - algorithm - custom - properties - -.. only:: singlehtml - - .. toctree:: - - index-types - index-instructions - index-rules - diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst deleted file mode 100644 index 490e2c55..00000000 --- a/document/core/appendix/properties.rst +++ /dev/null @@ -1,791 +0,0 @@ -.. index:: ! soundness, type system -.. _soundness: - -Soundness ---------- - -The :ref:`type system ` of WebAssembly is *sound*, implying both *type safety* and *memory safety* with respect to the WebAssembly semantics. For example: - -* All types declared and derived during validation are respected at run time; - e.g., every :ref:`local ` or :ref:`global ` variable will only contain type-correct values, every :ref:`instruction ` will only be applied to operands of the expected type, and every :ref:`function ` :ref:`invocation ` always evaluates to a result of the right type (if it does not :ref:`trap ` or diverge). - -* No memory location will be read or written except those explicitly defined by the program, i.e., as a :ref:`local `, a :ref:`global `, an element in a :ref:`table `, or a location within a linear :ref:`memory `. - -* There is no undefined behavior, - i.e., the :ref:`execution rules ` cover all possible cases that can occur in a :ref:`valid ` program, and the rules are mutually consistent. - -Soundness also is instrumental in ensuring additional properties, most notably, *encapsulation* of function and module scopes: no :ref:`locals ` can be accessed outside their own function and no :ref:`module ` components can be accessed outside their own module unless they are explicitly :ref:`exported ` or :ref:`imported `. - -The typing rules defining WebAssembly :ref:`validation ` only cover the *static* components of a WebAssembly program. -In order to state and prove soundness precisely, the typing rules must be extended to the *dynamic* components of the abstract :ref:`runtime `, that is, the :ref:`store `, :ref:`configurations `, and :ref:`administrative instructions `. [#cite-pldi2017]_ - - -.. index:: value, value type, result, result type, trap -.. _valid-result: - -Results -~~~~~~~ - -:ref:`Results ` can be classified by :ref:`result types ` as follows. - -:ref:`Results ` :math:`\val^\ast` -................................................ - -* For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast`: - - * The value :math:`\val_i` is :ref:`valid ` with some :ref:`value type ` :math:`t_i`. - -* Let :math:`t^\ast` be the concatenation of all :math:`t_i`. - -* Then the result is valid with :ref:`result type ` :math:`[t^\ast]`. - -.. math:: - \frac{ - (S \vdashval \val : t)^\ast - }{ - S \vdashresult \val^\ast : [t^\ast] - } - - -:ref:`Results ` :math:`\TRAP` -............................................ - -* The result is valid with :ref:`result type ` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`value types `. - -.. math:: - \frac{ - }{ - S \vdashresult \TRAP : [t^\ast] - } - - -.. _module-context: -.. _valid-store: - -Store Validity -~~~~~~~~~~~~~~ - -The following typing rules specify when a runtime :ref:`store ` :math:`S` is *valid*. -A valid store must consist of -:ref:`function `, :ref:`table `, :ref:`memory `, :ref:`global `, and :ref:`module ` instances that are themselves valid, relative to :math:`S`. - -To that end, each kind of instance is classified by a respective :ref:`function `, :ref:`table `, :ref:`memory `, or :ref:`global ` type. -Module instances are classified by *module contexts*, which are regular :ref:`contexts ` repurposed as module types describing the :ref:`index spaces ` defined by a module. - - - -.. index:: store, function instance, table instance, memory instance, global instance, function type, table type, memory type, global type - -:ref:`Store ` :math:`S` -..................................... - -* Each :ref:`function instance ` :math:`\funcinst_i` in :math:`S.\SFUNCS` must be :ref:`valid ` with some :ref:`function type ` :math:`\functype_i`. - -* Each :ref:`table instance ` :math:`\tableinst_i` in :math:`S.\STABLES` must be :ref:`valid ` with some :ref:`table type ` :math:`\tabletype_i`. - -* Each :ref:`memory instance ` :math:`\meminst_i` in :math:`S.\SMEMS` must be :ref:`valid ` with some :ref:`memory type ` :math:`\memtype_i`. - -* Each :ref:`global instance ` :math:`\globalinst_i` in :math:`S.\SGLOBALS` must be :ref:`valid ` with some :ref:`global type ` :math:`\globaltype_i`. - -* Then the store is valid. - -.. math:: - ~\\[-1ex] - \frac{ - \begin{array}{@{}c@{}} - (S \vdashfuncinst \funcinst : \functype)^\ast - \qquad - (S \vdashtableinst \tableinst : \tabletype)^\ast - \\ - (S \vdashmeminst \meminst : \memtype)^\ast - \qquad - (S \vdashglobalinst \globalinst : \globaltype)^\ast - \\ - S = \{ - \SFUNCS~\funcinst^\ast, - \STABLES~\tableinst^\ast, - \SMEMS~\meminst^\ast, - \SGLOBALS~\globalinst^\ast \} - \end{array} - }{ - \vdashstore S \ok - } - - -.. index:: function type, function instance -.. _valid-funcinst: - -:ref:`Function Instances ` :math:`\{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\}` -....................................................................................................................... - -* The :ref:`function type ` :math:`\functype` must be :ref:`valid `. - -* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`context ` :math:`C`. - -* Under :ref:`context ` :math:`C`, the :ref:`function ` :math:`\func` must be :ref:`valid ` with :ref:`function type ` :math:`\functype`. - -* Then the function instance is valid with :ref:`function type ` :math:`\functype`. - -.. math:: - \frac{ - \vdashfunctype \functype \ok - \qquad - S \vdashmoduleinst \moduleinst : C - \qquad - C \vdashfunc \func : \functype - }{ - S \vdashfuncinst \{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\} : \functype - } - - -.. index:: function type, function instance, host function -.. _valid-hostfuncinst: - -:ref:`Host Function Instances ` :math:`\{\FITYPE~\functype, \FIHOSTCODE~\X{hf}\}` -.................................................................................................. - -* The :ref:`function type ` :math:`\functype` must be :ref:`valid `. - -* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`\functype`. - -* For every :ref:`valid ` :ref:`store ` :math:`S_1` :ref:`extending ` :math:`S` and every sequence :math:`\val^\ast` of :ref:`values ` whose :ref:`types ` coincide with :math:`t_1^\ast`: - - * :ref:`Executing ` :math:`\X{hf}` in store :math:`S_1` with arguments :math:`\val^\ast` has a non-empty set of possible outcomes. - - * For every element :math:`R` of this set: - - * Either :math:`R` must be :math:`\bot` (i.e., divergence). - - * Or :math:`R` consists of a :ref:`valid ` :ref:`store ` :math:`S_2` :ref:`extending ` :math:`S_1` and a :ref:`result ` :math:`\result` whose :ref:`type ` coincides with :math:`[t_2^\ast]`. - -* Then the function instance is valid with :ref:`function type ` :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 - {S_1 \vdashresult \val^\ast : [t_1^\ast]} - \Longrightarrow {} \\ \qquad - \X{hf}(S_1; \val^\ast) \supset \emptyset \wedge {} \\ \qquad - \forall R \in \X{hf}(S_1; \val^\ast),~ - R = \bot \vee {} \\ \qquad\qquad - \exists S_2, \result,~ - {\vdashstore S_2 \ok} \wedge - {\vdashstoreextends S_1 \extendsto S_2} \wedge - {S_2 \vdashresult \result : [t_2^\ast]} \wedge - 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] - } - -.. 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 ` 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 Instances ` :math:`\{ \TITYPE~(\limits~t), \TIELEM~\reff^\ast \}` -............................................................................................... - -* The :ref:`table type ` :math:`\limits~t` must be :ref:`valid `. - -* The length of :math:`\reff^\ast` must equal :math:`\limits.\LMIN`. - -* For each :ref:`reference ` :math:`\reff_i` in the table elements :math:`\reff^n`: - - * The :ref:`reference ` :math:`\reff_i` must be :ref:`valid ` with some :ref:`reference type ` :math:`t'_i`. - - * The :ref:`reference type ` :math:`t'_i` must :ref:`match ` the :ref:`reference type ` :math:`t`. - -* Then the table instance is valid with :ref:`table type ` :math:`\limits~t`. - -.. math:: - \frac{ - \vdashtabletype \limits~t \ok - \qquad - n = \limits.\LMIN - \qquad - (S \vdash \reff : t')^n - \qquad - (\vdashreftypematch t' \matchesvaltype t)^n - }{ - S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t - } - - -.. index:: memory type, memory instance, limits, byte -.. _valid-meminst: - -:ref:`Memory Instances ` :math:`\{ \MITYPE~\limits, \MIDATA~b^\ast \}` -...................................................................................... - -* The :ref:`memory type ` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid `. - -* The length of :math:`b^\ast` must equal :math:`\limits.\LMIN` multiplied by the :ref:`page size ` :math:`64\,\F{Ki}`. - -* Then the memory instance is valid with :ref:`memory type ` :math:`\limits`. - -.. math:: - \frac{ - \vdashmemtype \limits \ok - \qquad - n = \limits.\LMIN \cdot 64\,\F{Ki} - }{ - S \vdashmeminst \{ \MITYPE~\limits, \MIDATA~b^n \} : \limits - } - - -.. index:: global type, global instance, value, mutability -.. _valid-globalinst: - -:ref:`Global Instances ` :math:`\{ \GITYPE~(\mut~t), \GIVALUE~\val \}` -......................................................................................... - -* The :ref:`global type ` :math:`\mut~t` must be :ref:`valid `. - -* The :ref:`value ` :math:`\val` must be :ref:`valid ` with some :ref:`value type ` :math:`t'`. - -* The :ref:`value type ` :math:`t'` must :ref:`match ` the :ref:`value type ` :math:`t`. - -* Then the global instance is valid with :ref:`global type ` :math:`\mut~t`. - -.. math:: - \frac{ - \vdashglobaltype \mut~t \ok - \qquad - S \vdashval \val : t' - \qquad - \vdashvaltypematch t' \matchesvaltype t - }{ - S \vdashglobalinst \{ \GITYPE~(\mut~t), \GIVALUE~\val \} : \mut~t - } - - -.. index:: external type, export instance, name, external value -.. _valid-exportinst: - -:ref:`Export Instances ` :math:`\{ \EINAME~\name, \EIVALUE~\externval \}` -....................................................................................................... - -* The :ref:`external value ` :math:`\externval` must be :ref:`valid ` with some :ref:`external type ` :math:`\externtype`. - -* Then the export instance is valid. - -.. math:: - \frac{ - S \vdashexternval \externval : \externtype - }{ - S \vdashexportinst \{ \EINAME~\name, \EIVALUE~\externval \} \ok - } - - -.. index:: module instance, context -.. _valid-moduleinst: - -:ref:`Module Instances ` :math:`\moduleinst` -............................................................... - -* Each :ref:`function type ` :math:`\functype_i` in :math:`\moduleinst.\MITYPES` must be :ref:`valid `. - -* For each :ref:`function address ` :math:`\funcaddr_i` in :math:`\moduleinst.\MIFUNCS`, the :ref:`external value ` :math:`\EVFUNC~\funcaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETFUNC~\functype'_i`. - -* For each :ref:`table address ` :math:`\tableaddr_i` in :math:`\moduleinst.\MITABLES`, the :ref:`external value ` :math:`\EVTABLE~\tableaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETTABLE~\tabletype_i`. - -* For each :ref:`memory address ` :math:`\memaddr_i` in :math:`\moduleinst.\MIMEMS`, the :ref:`external value ` :math:`\EVMEM~\memaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETMEM~\memtype_i`. - -* For each :ref:`global address ` :math:`\globaladdr_i` in :math:`\moduleinst.\MIGLOBALS`, the :ref:`external value ` :math:`\EVGLOBAL~\globaladdr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETGLOBAL~\globaltype_i`. - -* Each :ref:`export instance ` :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS` must be :ref:`valid `. - -* For each :ref:`export instance ` :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS`, the :ref:`name ` :math:`\exportinst_i.\EINAME` must be different from any other name occurring in :math:`\moduleinst.\MIEXPORTS`. - -* Let :math:`{\functype'}^\ast` be the concatenation of all :math:`\functype'_i` in order. - -* Let :math:`\tabletype^\ast` be the concatenation of all :math:`\tabletype_i` in order. - -* Let :math:`\memtype^\ast` be the concatenation of all :math:`\memtype_i` in order. - -* Let :math:`\globaltype^\ast` be the concatenation of all :math:`\globaltype_i` in order. - -* Then the module instance is valid with :ref:`context ` :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CGLOBALS~\globaltype^\ast\}`. - -.. math:: - ~\\[-1ex] - \frac{ - \begin{array}{@{}c@{}} - (\vdashfunctype \functype \ok)^\ast - \\ - (S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype')^\ast - \qquad - (S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\tabletype)^\ast - \\ - (S \vdashexternval \EVMEM~\memaddr : \ETMEM~\memtype)^\ast - \qquad - (S \vdashexternval \EVGLOBAL~\globaladdr : \ETGLOBAL~\globaltype)^\ast - \\ - (S \vdashexportinst \exportinst \ok)^\ast - \qquad - (\exportinst.\EINAME)^\ast ~\mbox{disjoint} - \end{array} - }{ - S \vdashmoduleinst \{ - \begin{array}[t]{@{}l@{~}l@{}} - \MITYPES & \functype^\ast, \\ - \MIFUNCS & \funcaddr^\ast, \\ - \MITABLES & \tableaddr^\ast, \\ - \MIMEMS & \memaddr^\ast, \\ - \MIGLOBALS & \globaladdr^\ast \\ - \MIEXPORTS & \exportinst^\ast ~\} : \{ - \begin{array}[t]{@{}l@{~}l@{}} - \CTYPES & \functype^\ast, \\ - \CFUNCS & {\functype'}^\ast, \\ - \CTABLES & \tabletype^\ast, \\ - \CMEMS & \memtype^\ast, \\ - \CGLOBALS & \globaltype^\ast ~\} - \end{array} - \end{array} - } - - -.. index:: configuration, administrative instruction, store, frame -.. _frame-context: -.. _valid-config: - -Configuration Validity -~~~~~~~~~~~~~~~~~~~~~~ - -To relate the WebAssembly :ref:`type system ` to its :ref:`execution semantics `, the :ref:`typing rules for instructions ` must be extended to :ref:`configurations ` :math:`S;T`, -which relates the :ref:`store ` to execution :ref:`threads `. - -Configurations and threads are classified by their :ref:`result type `. -In addition to the store :math:`S`, threads are typed under a *return type* :math:`\resulttype^?`, which controls whether and with which type a |return| instruction is allowed. -This type is absent (:math:`\epsilon`) except for instruction sequences inside an administrative |FRAME| instruction. - -Finally, :ref:`frames ` are classified with *frame contexts*, which extend the :ref:`module contexts ` of a frame's associated :ref:`module instance ` with the :ref:`locals ` that the frame contains. - - -.. index:: result type, thread - -:ref:`Configurations ` :math:`S;T` -................................................. - -* The :ref:`store ` :math:`S` must be :ref:`valid `. - -* Under no allowed return type, - the :ref:`thread ` :math:`T` must be :ref:`valid ` with some :ref:`result type ` :math:`[t^?]`. - -* Then the configuration is valid with the :ref:`result type ` :math:`[t^?]`. - -.. math:: - \frac{ - \vdashstore S \ok - \qquad - S; \epsilon \vdashthread T : [t^?] - }{ - \vdashconfig S; T : [t^?] - } - - -.. index:: thread, frame, instruction, result type, context -.. _valid-thread: - -:ref:`Threads ` :math:`F;\instr^\ast` -.................................................... - -* Let :math:`\resulttype^?` be the current allowed return type. - -* The :ref:`frame ` :math:`F` must be :ref:`valid ` with a :ref:`context ` :math:`C`. - -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with |CRETURN| set to :math:`\resulttype^?`. - -* Under context :math:`C'`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with some type :math:`[] \to [t^?]`. - -* Then the thread is valid with the :ref:`result type ` :math:`[t^?]`. - -.. math:: - \frac{ - S \vdashframe F : C - \qquad - S; C,\CRETURN~\resulttype^? \vdashinstrseq \instr^\ast : [] \to [t^?] - }{ - S; \resulttype^? \vdashthread F; \instr^\ast : [t^?] - } - - -.. index:: frame, local, module instance, value, value type, context -.. _valid-frame: - -:ref:`Frames ` :math:`\{\ALOCALS~\val^\ast, \AMODULE~\moduleinst\}` -................................................................................. - -* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`module context ` :math:`C`. - -* Each :ref:`value ` :math:`\val_i` in :math:`\val^\ast` must be :ref:`valid ` with some :ref:`value type ` :math:`t_i`. - -* Let :math:`t^\ast` the concatenation of all :math:`t_i` in order. - -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`value types ` :math:`t^\ast` prepended to the |CLOCALS| vector. - -* Then the frame is valid with :ref:`frame context ` :math:`C'`. - -.. math:: - \frac{ - S \vdashmoduleinst \moduleinst : C - \qquad - (S \vdashval \val : t)^\ast - }{ - S \vdashframe \{\ALOCALS~\val^\ast, \AMODULE~\moduleinst\} : (C, \CLOCALS~t^\ast) - } - - -.. index:: administrative instruction, value type, context, store -.. _valid-instr-admin: - -Administrative Instructions -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Typing rules for :ref:`administrative instructions ` are specified as follows. -In addition to the :ref:`context ` :math:`C`, typing of these instructions is defined under a given :ref:`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 extra rules for :ref:`administrative instructions ` given below. - - -.. index:: trap - -:math:`\TRAP` -............. - -* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. - -.. math:: - \frac{ - }{ - S; C \vdashadmininstr \TRAP : [t_1^\ast] \to [t_2^\ast] - } - - -.. index:: host address - -:math:`\REFHOST~\hostaddr` -.......................... - -* The instruction is valid with type :math:`[] \to [\ANYREF]`. - -.. math:: - \frac{ - }{ - S; C \vdashadmininstr \REFHOST~\hostaddr : [] \to [\ANYREF] - } - - -.. index:: function address, extern value, extern type, function type - -:math:`\REFFUNCADDR~\funcaddr` -.............................. - -* The :ref:`external function value ` :math:`\EVFUNC~\funcaddr` must be :ref:`valid ` with :ref:`external function type ` :math:`\ETFUNC \functype`. - -* Then the instruction is valid with type :math:`[] \to [\FUNCREF]`. - -.. math:: - \frac{ - S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype - }{ - S; C \vdashadmininstr \REFFUNCADDR~\funcaddr : [] \to [\FUNCREF] - } - - -.. index:: function address, extern value, extern type, function type - -:math:`\INVOKE~\funcaddr` -......................... - -* The :ref:`external function value ` :math:`\EVFUNC~\funcaddr` must be :ref:`valid ` with :ref:`external function type ` :math:`\ETFUNC ([t_1^\ast] \to [t_2^\ast])`. - -* Then the instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. - -.. math:: - \frac{ - S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~[t_1^\ast] \to [t_2^\ast] - }{ - S; C \vdashadmininstr \INVOKE~\funcaddr : [t_1^\ast] \to [t_2^\ast] - } - - -.. index:: element, table, table address, module instance, function index - -:math:`\INITELEM~\tableaddr~o~x^n` -.................................. - -* The :ref:`external table value ` :math:`\EVTABLE~\tableaddr` must be :ref:`valid ` with some :ref:`external table type ` :math:`\ETTABLE~(\limits~\FUNCREF)`. - -* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN`. - -* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`context ` :math:`C`. - -* Each :ref:`function index ` :math:`x_i` in :math:`x^n` must be defined in the context :math:`C`. - -* Then the instruction is valid. - -.. math:: - \frac{ - S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\limits~\FUNCREF - \qquad - o + n \leq \limits.\LMIN - \qquad - (C.\CFUNCS[x] = \functype)^n - }{ - S; C \vdashadmininstr \INITELEM~\tableaddr~o~x^n \ok - } - - -.. index:: data, memory, memory address, byte - -:math:`\INITDATA~\memaddr~o~b^n` -................................ - -* The :ref:`external memory value ` :math:`\EVMEM~\memaddr` must be :ref:`valid ` with some :ref:`external memory type ` :math:`\ETMEM~\limits`. - -* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN` divided by the :ref:`page size ` :math:`64\,\F{Ki}`. - -* Then the instruction is valid. - -.. math:: - \frac{ - S \vdashexternval \EVMEM~\memaddr : \ETMEM~\limits - \qquad - o + n \leq \limits.\LMIN \cdot 64\,\F{Ki} - }{ - S; C \vdashadmininstr \INITDATA~\memaddr~o~b^n \ok - } - - -.. index:: label, instruction, result type - -:math:`\LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END` -.................................................. - -* The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid ` with some type :math:`[t_1^n] \to [t_2^?]`. - -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_1^n]` prepended to the |CLABELS| vector. - -* Under context :math:`C'`, - the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^?]`. - -* Then the compound instruction is valid with type :math:`[] \to [t_2^?]`. - -.. math:: - \frac{ - S; C \vdashinstrseq \instr_0^\ast : [t_1^n] \to [t_2^?] - \qquad - S; C,\CLABELS\,[t_1^n] \vdashinstrseq \instr^\ast : [] \to [t_2^?] - }{ - S; C \vdashadmininstr \LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END : [] \to [t_2^?] - } - - -.. index:: frame, instruction, result type - -:math:`\FRAME_n\{F\}~\instr^\ast~\END` -........................................... - -* Under the return type :math:`[t^n]`, - the :ref:`thread ` :math:`F; \instr^\ast` must be :ref:`valid ` with :ref:`result type ` :math:`[t^n]`. - -* Then the compound instruction is valid with type :math:`[] \to [t^n]`. - -.. math:: - \frac{ - S; [t^n] \vdashinstrseq F; \instr^\ast : [t^n] - }{ - S; C \vdashadmininstr \FRAME_n\{F\}~\instr^\ast~\END : [] \to [t^n] - } - - -.. index:: ! store extension, store -.. _extend: - -Store Extension -~~~~~~~~~~~~~~~ - -Programs can mutate the :ref:`store ` and its contained instances. -Any such modification must respect certain invariants, such as not removing allocated instances or changing immutable definitions. -While these invariants are inherent to the execution semantics of WebAssembly :ref:`instructions ` and :ref:`modules `, -:ref:`host functions ` do not automatically adhere to them. Consequently, the required invariants must be stated as explicit constraints on the :ref:`invocation ` of host functions. -Soundness only holds when the :ref:`embedder ` ensures these constraints. - -The necessary constraints are codified by the notion of store *extension*: -a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'`, when the following rules hold. - -.. note:: - Extension does not imply that the new store is valid, which is defined separately :ref:`above `. - - -.. index:: store, function instance, table instance, memory instance, global instance -.. _extend-store: - -:ref:`Store ` :math:`S` -..................................... - -* The length of :math:`S.\SFUNCS` must not shrink. - -* The length of :math:`S.\STABLES` must not shrink. - -* The length of :math:`S.\SMEMS` must not shrink. - -* The length of :math:`S.\SGLOBALS` must not shrink. - -* For each :ref:`function instance ` :math:`\funcinst_i` in the original :math:`S.\SFUNCS`, the new function instance must be an :ref:`extension ` of the old. - -* For each :ref:`table instance ` :math:`\tableinst_i` in the original :math:`S.\STABLES`, the new table instance must be an :ref:`extension ` of the old. - -* For each :ref:`memory instance ` :math:`\meminst_i` in the original :math:`S.\SMEMS`, the new memory instance must be an :ref:`extension ` of the old. - -* For each :ref:`global instance ` :math:`\globalinst_i` in the original :math:`S.\SGLOBALS`, the new global instance must be an :ref:`extension ` of the old. - -.. math:: - \frac{ - \begin{array}{@{}ccc@{}} - S_1.\SFUNCS = \funcinst_1^\ast & - S_2.\SFUNCS = {\funcinst'_1}^\ast~\funcinst_2^\ast & - (\funcinst_1 \extendsto \funcinst'_1)^\ast \\ - S_1.\STABLES = \tableinst_1^\ast & - S_2.\STABLES = {\tableinst'_1}^\ast~\tableinst_2^\ast & - (\tableinst_1 \extendsto \tableinst'_1)^\ast \\ - S_1.\SMEMS = \meminst_1^\ast & - S_2.\SMEMS = {\meminst'_1}^\ast~\meminst_2^\ast & - (\meminst_1 \extendsto \meminst'_1)^\ast \\ - S_1.\SGLOBALS = \globalinst_1^\ast & - S_2.\SGLOBALS = {\globalinst'_1}^\ast~\globalinst_2^\ast & - (\globalinst_1 \extendsto \globalinst'_1)^\ast \\ - \end{array} - }{ - \vdashstoreextends S_1 \extendsto S_2 - } - - -.. index:: function instance -.. _extend-funcinst: - -:ref:`Function Instance ` :math:`\funcinst` -............................................................ - -* A function instance must remain unchanged. - -.. math:: - \frac{ - }{ - \vdashfuncinstextends \funcinst \extendsto \funcinst - } - - -.. index:: table instance -.. _extend-tableinst: - -:ref:`Table Instance ` :math:`\tableinst` -........................................................... - -* The :ref:`table type ` :math:`\tableinst.\TITYPE` must remain unchanged. - -* The length of :math:`\tableinst.\TIELEM` must not shrink. - -.. math:: - \frac{ - n_1 \leq n_2 - }{ - \vdashtableinstextends \{\TITYPE~\X{tt}, \TIELEM~(\X{fa}_1^?)^{n_1}\} \extendsto \{\TITYPE~\X{tt}, \TIELEM~(\X{fa}_2^?)^{n_2}\} - } - - -.. index:: memory instance -.. _extend-meminst: - -:ref:`Memory Instance ` :math:`\meminst` -........................................................ - -* The :ref:`memory type ` :math:`\meminst.\MITYPE` must remain unchanged. - -* The length of :math:`\meminst.\MIDATA` must not shrink. - -.. math:: - \frac{ - n_1 \leq n_2 - }{ - \vdashmeminstextends \{\MITYPE~\X{mt}, \MIDATA~b_1^{n_1}\} \extendsto \{\MITYPE~\X{mt}, \MIDATA~b_2^{n_2}\} - } - - -.. index:: global instance, value, mutability -.. _extend-globalinst: - -:ref:`Global Instance ` :math:`\globalinst` -.............................................................. - -* The :ref:`global type ` :math:`\globalinst.\GITYPE` must remain unchanged. - -* Let :math:`\mut~t` be the structure of :math:`\globalinst.\GITYPE`. - -* If :math:`\mut` is |MCONST|, then the :ref:`value ` :math:`\globalinst.\GIVALUE` must remain unchanged. - -.. math:: - \frac{ - \mut = \MVAR \vee \val_1 = \val_2 - }{ - \vdashglobalinstextends \{\GITYPE~(\mut~t), \GIVALUE~\val_1\} \extendsto \{\GITYPE~(\mut~t), \GIVALUE~\val_2\} - } - - - -.. index:: ! preservation, ! progress, soundness, configuration, thread, terminal configuration, instantiation, invocation, validity, module -.. _soundness-statement: - -Theorems -~~~~~~~~ - -Given the definition of :ref:`valid configurations `, -the standard soundness theorems hold. [#cite-cpp2018]_ - -**Theorem (Preservation).** -If a :ref:`configuration ` :math:`S;T` is :ref:`valid ` with :ref:`result type ` :math:`[t^\ast]` (i.e., :math:`\vdashconfig S;T : [t^\ast]`), -and steps to :math:`S';T'` (i.e., :math:`S;T \stepto S';T'`), -then :math:`S';T'` is a valid configuration with the same result type (i.e., :math:`\vdashconfig S';T' : [t^\ast]`). -Furthermore, :math:`S'` is an :ref:`extension ` of :math:`S` (i.e., :math:`\vdashstoreextends S \extendsto S'`). - -A *terminal* :ref:`thread ` is one whose sequence of :ref:`instructions ` is a :ref:`result `. -A terminal configuration is a configuration whose thread is terminal. - -**Theorem (Progress).** -If a :ref:`configuration ` :math:`S;T` is :ref:`valid ` (i.e., :math:`\vdashconfig S;T : [t^\ast]` for some :ref:`result type ` :math:`[t^\ast]`), -then either it is terminal, -or it can step to some configuration :math:`S';T'` (i.e., :math:`S;T \stepto S';T'`). - -From Preservation and Progress the soundness of the WebAssembly type system follows directly. - -**Corollary (Soundness).** -If a :ref:`configuration ` :math:`S;T` is :ref:`valid ` (i.e., :math:`\vdashconfig S;T : [t^\ast]` for some :ref:`result type ` :math:`[t^\ast]`), -then it either diverges or takes a finite number of steps to reach a terminal configuration :math:`S';T'` (i.e., :math:`S;T \stepto^\ast S';T'`) that is valid with the same result type (i.e., :math:`\vdashconfig S';T' : [t^\ast]`) -and where :math:`S'` is an :ref:`extension ` of :math:`S` (i.e., :math:`\vdashstoreextends S \extendsto S'`). - -In other words, every thread in a valid configuration either runs forever, traps, or terminates with a result that has the expected type. -Consequently, given a :ref:`valid store `, no computation defined by :ref:`instantiation ` or :ref:`invocation ` of a valid module can "crash" or otherwise (mis)behave in ways not covered by the :ref:`execution ` semantics given in this specification. - - -.. [#cite-pldi2017] - The formalization and theorems are derived from the following article: - Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. |PLDI2017|_. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017. - -.. [#cite-cpp2018] - A machine-verified version of the formalization and soundness proof is described in the following article: - Conrad Watt. |CPP2018|_. Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018). ACM 2018. diff --git a/document/core/binary/conventions.rst b/document/core/binary/conventions.rst deleted file mode 100644 index 8d383997..00000000 --- a/document/core/binary/conventions.rst +++ /dev/null @@ -1,118 +0,0 @@ -.. index:: ! binary format, module, byte, file extension, abstract syntax - -Conventions ------------ - -The binary format for WebAssembly :ref:`modules ` is a dense linear *encoding* of their :ref:`abstract syntax `. -[#compression]_ - -The format is defined by an *attribute grammar* whose only terminal symbols are :ref:`bytes `. -A byte sequence is a well-formed encoding of a module if and only if it is generated by the grammar. - -Each production of this grammar has exactly one synthesized attribute: the abstract syntax that the respective byte sequence encodes. -Thus, the attribute grammar implicitly defines a *decoding* function -(i.e., a parsing function for the binary format). - -Except for a few exceptions, the binary grammar closely mirrors the grammar of the abstract syntax. - -.. note:: - Some phrases of abstract syntax have multiple possible encodings in the binary format. - For example, numbers may be encoded as if they had optional leading zeros. - Implementations of decoders must support all possible alternatives; - implementations of encoders can pick any allowed encoding. - -The recommended extension for files containing WebAssembly modules in binary format is ":math:`\T{.wasm}`" -and the recommended |MediaType|_ is ":math:`\T{application/wasm}`". - -.. [#compression] - Additional encoding layers -- for example, introducing compression -- may be defined on top of the basic representation defined here. - However, such layers are outside the scope of the current specification. - - -.. index:: grammar notation, notation, byte - single: binary format; grammar - pair: binary format; notation -.. _binary-grammar: - -Grammar -~~~~~~~ - -The following conventions are adopted in defining grammar rules for the binary format. -They mirror the conventions used for :ref:`abstract syntax `. -In order to distinguish symbols of the binary syntax from symbols of the abstract syntax, :math:`\mathtt{typewriter}` font is adopted for the former. - -* Terminal symbols are :ref:`bytes ` expressed in hexadecimal notation: :math:`\hex{0F}`. - -* Nonterminal symbols are written in typewriter font: :math:`\B{valtype}, \B{instr}`. - -* :math:`B^n` is a sequence of :math:`n\geq 0` iterations of :math:`B`. - -* :math:`B^\ast` is a possibly empty sequence of iterations of :math:`B`. - (This is a shorthand for :math:`B^n` used where :math:`n` is not relevant.) - -* :math:`B^?` is an optional occurrence of :math:`B`. - (This is a shorthand for :math:`B^n` where :math:`n \leq 1`.) - -* :math:`x{:}B` denotes the same language as the nonterminal :math:`B`, but also binds the variable :math:`x` to the attribute synthesized for :math:`B`. - -* Productions are written :math:`\B{sym} ::= B_1 \Rightarrow A_1 ~|~ \dots ~|~ B_n \Rightarrow A_n`, where each :math:`A_i` is the attribute that is synthesized for :math:`\B{sym}` in the given case, usually from attribute variables bound in :math:`B_i`. - -* Some productions are augmented by side conditions in parentheses, which restrict the applicability of the production. They provide a shorthand for a combinatorial expansion of the production into many separate cases. - -.. note:: - For example, the :ref:`binary grammar ` for :ref:`value types ` is given as follows: - - .. math:: - \begin{array}{llcll@{\qquad\qquad}l} - \production{value types} & \Bvaltype &::=& - \hex{7F} &\Rightarrow& \I32 \\ &&|& - \hex{7E} &\Rightarrow& \I64 \\ &&|& - \hex{7D} &\Rightarrow& \F32 \\ &&|& - \hex{7C} &\Rightarrow& \F64 \\ - \end{array} - - Consequently, the byte :math:`\hex{7F}` encodes the type |I32|, - :math:`\hex{7E}` encodes the type |I64|, and so forth. - No other byte value is allowed as the encoding of a value type. - - The :ref:`binary grammar ` for :ref:`limits ` is defined as follows: - - .. math:: - \begin{array}{llclll} - \production{limits} & \Blimits &::=& - \hex{00}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \} \\ &&|& - \hex{01}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \} \\ - \end{array} - - That is, a limits pair is encoded as either the byte :math:`\hex{00}` followed by the encoding of a |U32| value, - or the byte :math:`\hex{01}` followed by two such encodings. - The variables :math:`n` and :math:`m` name the attributes of the respective |Bu32| nonterminals, which in this case are the actual :ref:`unsigned integers ` those decode into. - The attribute of the complete production then is the abstract syntax for the limit, expressed in terms of the former values. - - -.. _binary-notation: - -Auxiliary Notation -~~~~~~~~~~~~~~~~~~ - -When dealing with binary encodings the following notation is also used: - -* :math:`\epsilon` denotes the empty byte sequence. - -* :math:`||B||` is the length of the byte sequence generated from the production :math:`B` in a derivation. - - -.. index:: vector - pair: binary format; vector -.. _binary-vec: - -Vectors -~~~~~~~ - -:ref:`Vectors ` are encoded with their |Bu32| length followed by the encoding of their element sequence. - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{vector} & \Bvec(\B{B}) &::=& - n{:}\Bu32~~(x{:}\B{B})^n &\Rightarrow& x^n \\ - \end{array} diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst deleted file mode 100644 index 27deed05..00000000 --- a/document/core/binary/instructions.rst +++ /dev/null @@ -1,429 +0,0 @@ -.. index:: instruction, ! opcode -.. _binary-instr: - -Instructions ------------- - -:ref:`Instructions ` are encoded by *opcodes*. -Each opcode is represented by a single byte, -and is followed by the instruction's immediate arguments, where present. -The only exception are :ref:`structured control instructions `, which consist of several opcodes bracketing their nested instruction sequences. - -.. note:: - Gaps in the byte code ranges for encoding instructions are reserved for future extensions. - - -.. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, polymorphism - pair: binary format; instruction -.. _binary-instr-control: - -Control Instructions -~~~~~~~~~~~~~~~~~~~~ - -:ref:`Control instructions ` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are terminated with explicit opcodes for |END| and |ELSE|. - -.. _binary-nop: -.. _binary-unreachable: -.. _binary-block: -.. _binary-loop: -.. _binary-if: -.. _binary-br: -.. _binary-br_if: -.. _binary-br_table: -.. _binary-return: -.. _binary-call: -.. _binary-call_indirect: - -.. math:: - \begin{array}{llclll} - \production{instruction} & \Binstr &::=& - \hex{00} &\Rightarrow& \UNREACHABLE \\ &&|& - \hex{01} &\Rightarrow& \NOP \\ &&|& - \hex{02}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \BLOCK~\X{rt}~\X{in}^\ast~\END \\ &&|& - \hex{03}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \LOOP~\X{rt}~\X{in}^\ast~\END \\ &&|& - \hex{04}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \IF~\X{rt}~\X{in}^\ast~\ELSE~\epsilon~\END \\ &&|& - \hex{04}~~\X{rt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~ - \hex{05}~~(\X{in}_2{:}\Binstr)^\ast~~\hex{0B} - &\Rightarrow& \IF~\X{rt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \\ &&|& - \hex{0C}~~l{:}\Blabelidx &\Rightarrow& \BR~l \\ &&|& - \hex{0D}~~l{:}\Blabelidx &\Rightarrow& \BRIF~l \\ &&|& - \hex{0E}~~l^\ast{:}\Bvec(\Blabelidx)~~l_N{:}\Blabelidx - &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|& - \hex{0F} &\Rightarrow& \RETURN \\ &&|& - \hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|& - \hex{11}~~y{:}\Btypeidx~~x{:}\Btableidx &\Rightarrow& \CALLINDIRECT~x~y \\ - \end{array} - -.. note:: - The |ELSE| opcode :math:`\hex{05}` in the encoding of an |IF| instruction can be omitted if the following instruction sequence is empty. - - -.. index:: reference instruction - pair: binary format; instruction -.. _binary-instr-ref: - -Reference Instructions -~~~~~~~~~~~~~~~~~~~~~~ - -:ref:`Reference instructions ` are represented by single byte codes. - -.. _binary-ref.null: -.. _binary-ref.isnull: - -.. math:: - \begin{array}{llclll} - \production{instruction} & \Binstr &::=& \dots \\ &&|& - \hex{D0} &\Rightarrow& \REFNULL \\ &&|& - \hex{D1} &\Rightarrow& \REFISNULL \\ &&|& - \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\ - \end{array} - -.. note:: - These opcode assignments are preliminary. - - -.. index:: parametric instruction, value type, polymorphism - pair: binary format; instruction -.. _binary-instr-parametric: - -Parametric Instructions -~~~~~~~~~~~~~~~~~~~~~~~ - -:ref:`Parametric instructions ` are represented by single byte codes, possibly followed by a type annotation. - -.. _binary-drop: -.. _binary-select: - -.. math:: - \begin{array}{llclll} - \production{instruction} & \Binstr &::=& \dots \\ &&|& - \hex{1A} &\Rightarrow& \DROP \\ &&|& - \hex{1B} &\Rightarrow& \SELECT \\ &&|& - \hex{1C}~~t^\ast{:}\Bvec(\Bvaltype) &\Rightarrow& \SELECT~t^\ast \\ - \end{array} - - -.. index:: variable instructions, local index, global index - pair: binary format; instruction -.. _binary-instr-variable: - -Variable Instructions -~~~~~~~~~~~~~~~~~~~~~ - -:ref:`Variable instructions ` are represented by byte codes followed by the encoding of the respective :ref:`index `. - -.. _binary-local.get: -.. _binary-local.set: -.. _binary-local.tee: -.. _binary-global.get: -.. _binary-global.set: - -.. math:: - \begin{array}{llclll} - \production{instruction} & \Binstr &::=& \dots \\ &&|& - \hex{20}~~x{:}\Blocalidx &\Rightarrow& \LOCALGET~x \\ &&|& - \hex{21}~~x{:}\Blocalidx &\Rightarrow& \LOCALSET~x \\ &&|& - \hex{22}~~x{:}\Blocalidx &\Rightarrow& \LOCALTEE~x \\ &&|& - \hex{23}~~x{:}\Bglobalidx &\Rightarrow& \GLOBALGET~x \\ &&|& - \hex{24}~~x{:}\Bglobalidx &\Rightarrow& \GLOBALSET~x \\ - \end{array} - - -.. index:: table instruction, table index - pair: binary format; instruction -.. _binary-instr-table: - -Table Instructions -~~~~~~~~~~~~~~~~~~ - -:ref:`Table instructions ` are represented by either single byte or two byte codes. - -.. _binary-table.get: -.. _binary-table.set: -.. _binary-table.size: -.. _binary-table.grow: -.. _binary-table.fill: - -.. math:: - \begin{array}{llclll} - \production{instruction} & \Binstr &::=& \dots \\ &&|& - \hex{25}~~x{:}\Btableidx &\Rightarrow& \TABLEGET~x \\ &&|& - \hex{26}~~x{:}\Btableidx &\Rightarrow& \TABLESET~x \\ &&|& - \hex{FC}~\hex{0F}~~x{:}\Btableidx &\Rightarrow& \TABLEGROW~x \\ &&|& - \hex{FC}~\hex{10}~~x{:}\Btableidx &\Rightarrow& \TABLESIZE~x \\ &&|& - \hex{FC}~\hex{11}~~x{:}\Btableidx &\Rightarrow& \TABLEFILL~x \\ - \end{array} - - -.. index:: memory instruction, memory index - pair: binary format; instruction -.. _binary-instr-memory: - -Memory Instructions -~~~~~~~~~~~~~~~~~~~ - -Each variant of :ref:`memory instruction ` is encoded with a different byte code. Loads and stores are followed by the encoding of their |memarg| immediate. - -.. _binary-memarg: -.. _binary-load: -.. _binary-loadn: -.. _binary-store: -.. _binary-storen: -.. _binary-memory.size: -.. _binary-memory.grow: - -.. math:: - \begin{array}{llclll} - \production{memory argument} & \Bmemarg &::=& - a{:}\Bu32~~o{:}\Bu32 &\Rightarrow& \{ \ALIGN~a,~\OFFSET~o \} \\ - \production{instruction} & \Binstr &::=& \dots \\ &&|& - \hex{28}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD~m \\ &&|& - \hex{29}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD~m \\ &&|& - \hex{2A}~~m{:}\Bmemarg &\Rightarrow& \F32.\LOAD~m \\ &&|& - \hex{2B}~~m{:}\Bmemarg &\Rightarrow& \F64.\LOAD~m \\ &&|& - \hex{2C}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD\K{8\_s}~m \\ &&|& - \hex{2D}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD\K{8\_u}~m \\ &&|& - \hex{2E}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD\K{16\_s}~m \\ &&|& - \hex{2F}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD\K{16\_u}~m \\ &&|& - \hex{30}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{8\_s}~m \\ &&|& - \hex{31}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{8\_u}~m \\ &&|& - \hex{32}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{16\_s}~m \\ &&|& - \hex{33}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{16\_u}~m \\ &&|& - \hex{34}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{32\_s}~m \\ &&|& - \hex{35}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{32\_u}~m \\ &&|& - \hex{36}~~m{:}\Bmemarg &\Rightarrow& \I32.\STORE~m \\ &&|& - \hex{37}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE~m \\ &&|& - \hex{38}~~m{:}\Bmemarg &\Rightarrow& \F32.\STORE~m \\ &&|& - \hex{39}~~m{:}\Bmemarg &\Rightarrow& \F64.\STORE~m \\ &&|& - \hex{3A}~~m{:}\Bmemarg &\Rightarrow& \I32.\STORE\K{8}~m \\ &&|& - \hex{3B}~~m{:}\Bmemarg &\Rightarrow& \I32.\STORE\K{16}~m \\ &&|& - \hex{3C}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{8}~m \\ &&|& - \hex{3D}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{16}~m \\ &&|& - \hex{3E}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{32}~m \\ &&|& - \hex{3F}~~\hex{00} &\Rightarrow& \MEMORYSIZE \\ &&|& - \hex{40}~~\hex{00} &\Rightarrow& \MEMORYGROW \\ - \end{array} - -.. note:: - In future versions of WebAssembly, the additional zero bytes occurring in the encoding of the |MEMORYSIZE| and |MEMORYGROW| instructions may be used to index additional memories. - - -.. index:: numeric instruction - pair: binary format; instruction -.. _binary-instr-numeric: - -Numeric Instructions -~~~~~~~~~~~~~~~~~~~~ - -All variants of :ref:`numeric instructions ` are represented by separate byte codes. - -The |CONST| instructions are followed by the respective literal. - -.. _binary-const: - -.. math:: - \begin{array}{llclll} - \production{instruction} & \Binstr &::=& \dots \\&&|& - \hex{41}~~n{:}\Bi32 &\Rightarrow& \I32.\CONST~n \\ &&|& - \hex{42}~~n{:}\Bi64 &\Rightarrow& \I64.\CONST~n \\ &&|& - \hex{43}~~z{:}\Bf32 &\Rightarrow& \F32.\CONST~z \\ &&|& - \hex{44}~~z{:}\Bf64 &\Rightarrow& \F64.\CONST~z \\ - \end{array} - -All other numeric instructions are plain opcodes without any immediates. - -.. _binary-testop: -.. _binary-relop: - -.. math:: - \begin{array}{llclll} - \production{instruction} & \Binstr &::=& \dots && \phantom{thisshouldbeenough} \\&&|& - \hex{45} &\Rightarrow& \I32.\EQZ \\ &&|& - \hex{46} &\Rightarrow& \I32.\EQ \\ &&|& - \hex{47} &\Rightarrow& \I32.\NE \\ &&|& - \hex{48} &\Rightarrow& \I32.\LT\K{\_s} \\ &&|& - \hex{49} &\Rightarrow& \I32.\LT\K{\_u} \\ &&|& - \hex{4A} &\Rightarrow& \I32.\GT\K{\_s} \\ &&|& - \hex{4B} &\Rightarrow& \I32.\GT\K{\_u} \\ &&|& - \hex{4C} &\Rightarrow& \I32.\LE\K{\_s} \\ &&|& - \hex{4D} &\Rightarrow& \I32.\LE\K{\_u} \\ &&|& - \hex{4E} &\Rightarrow& \I32.\GE\K{\_s} \\ &&|& - \hex{4F} &\Rightarrow& \I32.\GE\K{\_u} \\ - \end{array} - -.. math:: - \begin{array}{llclll} - \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& - \hex{50} &\Rightarrow& \I64.\EQZ \\ &&|& - \hex{51} &\Rightarrow& \I64.\EQ \\ &&|& - \hex{52} &\Rightarrow& \I64.\NE \\ &&|& - \hex{53} &\Rightarrow& \I64.\LT\K{\_s} \\ &&|& - \hex{54} &\Rightarrow& \I64.\LT\K{\_u} \\ &&|& - \hex{55} &\Rightarrow& \I64.\GT\K{\_s} \\ &&|& - \hex{56} &\Rightarrow& \I64.\GT\K{\_u} \\ &&|& - \hex{57} &\Rightarrow& \I64.\LE\K{\_s} \\ &&|& - \hex{58} &\Rightarrow& \I64.\LE\K{\_u} \\ &&|& - \hex{59} &\Rightarrow& \I64.\GE\K{\_s} \\ &&|& - \hex{5A} &\Rightarrow& \I64.\GE\K{\_u} \\ - \end{array} - -.. math:: - \begin{array}{llclll} - \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& - \hex{5B} &\Rightarrow& \F32.\EQ \\ &&|& - \hex{5C} &\Rightarrow& \F32.\NE \\ &&|& - \hex{5D} &\Rightarrow& \F32.\LT \\ &&|& - \hex{5E} &\Rightarrow& \F32.\GT \\ &&|& - \hex{5F} &\Rightarrow& \F32.\LE \\ &&|& - \hex{60} &\Rightarrow& \F32.\GE \\ - \end{array} - -.. math:: - \begin{array}{llclll} - \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& - \hex{61} &\Rightarrow& \F64.\EQ \\ &&|& - \hex{62} &\Rightarrow& \F64.\NE \\ &&|& - \hex{63} &\Rightarrow& \F64.\LT \\ &&|& - \hex{64} &\Rightarrow& \F64.\GT \\ &&|& - \hex{65} &\Rightarrow& \F64.\LE \\ &&|& - \hex{66} &\Rightarrow& \F64.\GE \\ - \end{array} - -.. _binary-unop: -.. _binary-binop: - -.. math:: - \begin{array}{llclll} - \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& - \hex{67} &\Rightarrow& \I32.\CLZ \\ &&|& - \hex{68} &\Rightarrow& \I32.\CTZ \\ &&|& - \hex{69} &\Rightarrow& \I32.\POPCNT \\ &&|& - \hex{6A} &\Rightarrow& \I32.\ADD \\ &&|& - \hex{6B} &\Rightarrow& \I32.\SUB \\ &&|& - \hex{6C} &\Rightarrow& \I32.\MUL \\ &&|& - \hex{6D} &\Rightarrow& \I32.\DIV\K{\_s} \\ &&|& - \hex{6E} &\Rightarrow& \I32.\DIV\K{\_u} \\ &&|& - \hex{6F} &\Rightarrow& \I32.\REM\K{\_s} \\ &&|& - \hex{70} &\Rightarrow& \I32.\REM\K{\_u} \\ &&|& - \hex{71} &\Rightarrow& \I32.\AND \\ &&|& - \hex{72} &\Rightarrow& \I32.\OR \\ &&|& - \hex{73} &\Rightarrow& \I32.\XOR \\ &&|& - \hex{74} &\Rightarrow& \I32.\SHL \\ &&|& - \hex{75} &\Rightarrow& \I32.\SHR\K{\_s} \\ &&|& - \hex{76} &\Rightarrow& \I32.\SHR\K{\_u} \\ &&|& - \hex{77} &\Rightarrow& \I32.\ROTL \\ &&|& - \hex{78} &\Rightarrow& \I32.\ROTR \\ - \end{array} - -.. math:: - \begin{array}{llclll} - \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& - \hex{79} &\Rightarrow& \I64.\CLZ \\ &&|& - \hex{7A} &\Rightarrow& \I64.\CTZ \\ &&|& - \hex{7B} &\Rightarrow& \I64.\POPCNT \\ &&|& - \hex{7C} &\Rightarrow& \I64.\ADD \\ &&|& - \hex{7D} &\Rightarrow& \I64.\SUB \\ &&|& - \hex{7E} &\Rightarrow& \I64.\MUL \\ &&|& - \hex{7F} &\Rightarrow& \I64.\DIV\K{\_s} \\ &&|& - \hex{80} &\Rightarrow& \I64.\DIV\K{\_u} \\ &&|& - \hex{81} &\Rightarrow& \I64.\REM\K{\_s} \\ &&|& - \hex{82} &\Rightarrow& \I64.\REM\K{\_u} \\ &&|& - \hex{83} &\Rightarrow& \I64.\AND \\ &&|& - \hex{84} &\Rightarrow& \I64.\OR \\ &&|& - \hex{85} &\Rightarrow& \I64.\XOR \\ &&|& - \hex{86} &\Rightarrow& \I64.\SHL \\ &&|& - \hex{87} &\Rightarrow& \I64.\SHR\K{\_s} \\ &&|& - \hex{88} &\Rightarrow& \I64.\SHR\K{\_u} \\ &&|& - \hex{89} &\Rightarrow& \I64.\ROTL \\ &&|& - \hex{8A} &\Rightarrow& \I64.\ROTR \\ - \end{array} - -.. math:: - \begin{array}{llclll} - \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& - \hex{8B} &\Rightarrow& \F32.\ABS \\ &&|& - \hex{8C} &\Rightarrow& \F32.\NEG \\ &&|& - \hex{8D} &\Rightarrow& \F32.\CEIL \\ &&|& - \hex{8E} &\Rightarrow& \F32.\FLOOR \\ &&|& - \hex{8F} &\Rightarrow& \F32.\TRUNC \\ &&|& - \hex{90} &\Rightarrow& \F32.\NEAREST \\ &&|& - \hex{91} &\Rightarrow& \F32.\SQRT \\ &&|& - \hex{92} &\Rightarrow& \F32.\ADD \\ &&|& - \hex{93} &\Rightarrow& \F32.\SUB \\ &&|& - \hex{94} &\Rightarrow& \F32.\MUL \\ &&|& - \hex{95} &\Rightarrow& \F32.\DIV \\ &&|& - \hex{96} &\Rightarrow& \F32.\FMIN \\ &&|& - \hex{97} &\Rightarrow& \F32.\FMAX \\ &&|& - \hex{98} &\Rightarrow& \F32.\COPYSIGN \\ - \end{array} - -.. math:: - \begin{array}{llclll} - \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& - \hex{99} &\Rightarrow& \F64.\ABS \\ &&|& - \hex{9A} &\Rightarrow& \F64.\NEG \\ &&|& - \hex{9B} &\Rightarrow& \F64.\CEIL \\ &&|& - \hex{9C} &\Rightarrow& \F64.\FLOOR \\ &&|& - \hex{9D} &\Rightarrow& \F64.\TRUNC \\ &&|& - \hex{9E} &\Rightarrow& \F64.\NEAREST \\ &&|& - \hex{9F} &\Rightarrow& \F64.\SQRT \\ &&|& - \hex{A0} &\Rightarrow& \F64.\ADD \\ &&|& - \hex{A1} &\Rightarrow& \F64.\SUB \\ &&|& - \hex{A2} &\Rightarrow& \F64.\MUL \\ &&|& - \hex{A3} &\Rightarrow& \F64.\DIV \\ &&|& - \hex{A4} &\Rightarrow& \F64.\FMIN \\ &&|& - \hex{A5} &\Rightarrow& \F64.\FMAX \\ &&|& - \hex{A6} &\Rightarrow& \F64.\COPYSIGN \\ - \end{array} - -.. _binary-cvtop: - -.. math:: - \begin{array}{llclll} - \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& - \hex{A7} &\Rightarrow& \I32.\WRAP\K{\_}\I64 \\ &&|& - \hex{A8} &\Rightarrow& \I32.\TRUNC\K{\_}\F32\K{\_s} \\ &&|& - \hex{A9} &\Rightarrow& \I32.\TRUNC\K{\_}\F32\K{\_u} \\ &&|& - \hex{AA} &\Rightarrow& \I32.\TRUNC\K{\_}\F64\K{\_s} \\ &&|& - \hex{AB} &\Rightarrow& \I32.\TRUNC\K{\_}\F64\K{\_u} \\ &&|& - \hex{AC} &\Rightarrow& \I64.\EXTEND\K{\_}\I32\K{\_s} \\ &&|& - \hex{AD} &\Rightarrow& \I64.\EXTEND\K{\_}\I32\K{\_u} \\ &&|& - \hex{AE} &\Rightarrow& \I64.\TRUNC\K{\_}\F32\K{\_s} \\ &&|& - \hex{AF} &\Rightarrow& \I64.\TRUNC\K{\_}\F32\K{\_u} \\ &&|& - \hex{B0} &\Rightarrow& \I64.\TRUNC\K{\_}\F64\K{\_s} \\ &&|& - \hex{B1} &\Rightarrow& \I64.\TRUNC\K{\_}\F64\K{\_u} \\ &&|& - \hex{B2} &\Rightarrow& \F32.\CONVERT\K{\_}\I32\K{\_s} \\ &&|& - \hex{B3} &\Rightarrow& \F32.\CONVERT\K{\_}\I32\K{\_u} \\ &&|& - \hex{B4} &\Rightarrow& \F32.\CONVERT\K{\_}\I64\K{\_s} \\ &&|& - \hex{B5} &\Rightarrow& \F32.\CONVERT\K{\_}\I64\K{\_u} \\ &&|& - \hex{B6} &\Rightarrow& \F32.\DEMOTE\K{\_}\F64 \\ &&|& - \hex{B7} &\Rightarrow& \F64.\CONVERT\K{\_}\I32\K{\_s} \\ &&|& - \hex{B8} &\Rightarrow& \F64.\CONVERT\K{\_}\I32\K{\_u} \\ &&|& - \hex{B9} &\Rightarrow& \F64.\CONVERT\K{\_}\I64\K{\_s} \\ &&|& - \hex{BA} &\Rightarrow& \F64.\CONVERT\K{\_}\I64\K{\_u} \\ &&|& - \hex{BB} &\Rightarrow& \F64.\PROMOTE\K{\_}\F32 \\ &&|& - \hex{BC} &\Rightarrow& \I32.\REINTERPRET\K{\_}\F32 \\ &&|& - \hex{BD} &\Rightarrow& \I64.\REINTERPRET\K{\_}\F64 \\ &&|& - \hex{BE} &\Rightarrow& \F32.\REINTERPRET\K{\_}\I32 \\ &&|& - \hex{BF} &\Rightarrow& \F64.\REINTERPRET\K{\_}\I64 \\ - \end{array} - - -.. index:: expression - pair: binary format; expression - single: expression; constant -.. _binary-expr: - -Expressions -~~~~~~~~~~~ - -:ref:`Expressions ` are encoded by their instruction sequence terminated with an explicit :math:`\hex{0B}` opcode for |END|. - -.. math:: - \begin{array}{llclll} - \production{expression} & \Bexpr &::=& - (\X{in}{:}\Binstr)^\ast~~\hex{0B} &\Rightarrow& \X{in}^\ast~\END \\ - \end{array} diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst deleted file mode 100644 index f7c36c9f..00000000 --- a/document/core/binary/modules.rst +++ /dev/null @@ -1,486 +0,0 @@ -Modules -------- - -The binary encoding of modules is organized into *sections*. -Most sections correspond to one component of a :ref:`module ` record, -except that :ref:`function definitions ` are split into two sections, separating their type declarations in the :ref:`function section ` from their bodies in the :ref:`code section `. - -.. note:: - This separation enables *parallel* and *streaming* compilation of the functions in a module. - - -.. index:: index, type index, function index, table index, memory index, global index, local index, label index - pair: binary format; type index - pair: binary format; function index - pair: binary format; table index - pair: binary format; memory index - pair: binary format; global index - pair: binary format; local index - pair: binary format; label index -.. _binary-typeidx: -.. _binary-funcidx: -.. _binary-tableidx: -.. _binary-memidx: -.. _binary-globalidx: -.. _binary-localidx: -.. _binary-labelidx: -.. _binary-index: - -Indices -~~~~~~~ - -All :ref:`indices ` are encoded with their respective value. - -.. math:: - \begin{array}{llclll} - \production{type index} & \Btypeidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{function index} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{table index} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{memory index} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{global index} & \Bglobalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{local index} & \Blocalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{label index} & \Blabelidx &::=& l{:}\Bu32 &\Rightarrow& l \\ - \end{array} - - -.. index:: ! section - pair: binary format; section -.. _binary-section: - -Sections -~~~~~~~~ - -Each section consists of - -* a one-byte section *id*, -* the |U32| *size* of the contents, in bytes, -* the actual *contents*, whose structure is depended on the section id. - -Every section is optional; an omitted section is equivalent to the section being present with empty contents. - -The following parameterized grammar rule defines the generic structure of a section with id :math:`N` and contents described by the grammar :math:`\B{B}`. - -.. math:: - \begin{array}{llclll@{\qquad}l} - \production{section} & \Bsection_N(\B{B}) &::=& - N{:}\Bbyte~~\X{size}{:}\Bu32~~\X{cont}{:}\B{B} - &\Rightarrow& \X{cont} & (\iff \X{size} = ||\B{B}||) \\ &&|& - \epsilon &\Rightarrow& \epsilon - \end{array} - -For most sections, the contents :math:`\B{B}` encodes a :ref:`vector `. -In these cases, the empty result :math:`\epsilon` is interpreted as the empty vector. - -.. note:: - Other than for unknown :ref:`custom sections `, - the :math:`\X{size}` is not required for decoding, but can be used to skip sections when navigating through a binary. - The module is malformed if the size does not match the length of the binary contents :math:`\B{B}`. - -The following section ids are used: - -== ======================================== -Id Section -== ======================================== - 0 :ref:`custom section ` - 1 :ref:`type section ` - 2 :ref:`import section ` - 3 :ref:`function section ` - 4 :ref:`table section ` - 5 :ref:`memory section ` - 6 :ref:`global section ` - 7 :ref:`export section ` - 8 :ref:`start section ` - 9 :ref:`element section ` -10 :ref:`code section ` -11 :ref:`data section ` -== ======================================== - - -.. index:: ! custom section - pair: binary format; custom section - single: section; custom -.. _binary-customsec: - -Custom Section -~~~~~~~~~~~~~~ - -*Custom sections* have the id 0. -They are intended to be used for debugging information or third-party extensions, and are ignored by the WebAssembly semantics. -Their contents consist of a :ref:`name ` further identifying the custom section, followed by an uninterpreted sequence of bytes for custom use. - -.. math:: - \begin{array}{llclll} - \production{custom section} & \Bcustomsec &::=& - \Bsection_0(\Bcustom) \\ - \production{custom data} & \Bcustom &::=& - \Bname~~\Bbyte^\ast \\ - \end{array} - -.. note:: - If an implementation interprets the contents of a custom section, then errors in that contents, or the placement of the section, must not invalidate the module. - - -.. index:: ! type section, type definition - pair: binary format; type section - pair: section; type -.. _binary-typedef: -.. _binary-typesec: - -Type Section -~~~~~~~~~~~~ - -The *type section* has the id 1. -It decodes into a vector of :ref:`function types ` that represent the |MTYPES| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{type section} & \Btypesec &::=& - \X{ft}^\ast{:\,}\Bsection_1(\Bvec(\Bfunctype)) &\Rightarrow& \X{ft}^\ast \\ - \end{array} - - -.. index:: ! import section, import, name, function type, table type, memory type, global type - pair: binary format; import - pair: section; import -.. _binary-import: -.. _binary-importdesc: -.. _binary-importsec: - -Import Section -~~~~~~~~~~~~~~ - -The *import section* has the id 2. -It decodes into a vector of :ref:`imports ` that represent the |MIMPORTS| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{import section} & \Bimportsec &::=& - \X{im}^\ast{:}\Bsection_2(\Bvec(\Bimport)) &\Rightarrow& \X{im}^\ast \\ - \production{import} & \Bimport &::=& - \X{mod}{:}\Bname~~\X{nm}{:}\Bname~~d{:}\Bimportdesc - &\Rightarrow& \{ \IMODULE~\X{mod}, \INAME~\X{nm}, \IDESC~d \} \\ - \production{import description} & \Bimportdesc &::=& - \hex{00}~~x{:}\Btypeidx &\Rightarrow& \IDFUNC~x \\ &&|& - \hex{01}~~\X{tt}{:}\Btabletype &\Rightarrow& \IDTABLE~\X{tt} \\ &&|& - \hex{02}~~\X{mt}{:}\Bmemtype &\Rightarrow& \IDMEM~\X{mt} \\ &&|& - \hex{03}~~\X{gt}{:}\Bglobaltype &\Rightarrow& \IDGLOBAL~\X{gt} \\ - \end{array} - - -.. index:: ! function section, function, type index, function type - pair: binary format; function - pair: section; function -.. _binary-funcsec: - -Function Section -~~~~~~~~~~~~~~~~ - -The *function section* has the id 3. -It decodes into a vector of :ref:`type indices ` that represent the |FTYPE| fields of the :ref:`functions ` in the |MFUNCS| component of a :ref:`module `. -The |FLOCALS| and |FBODY| fields of the respective functions are encoded separately in the :ref:`code section `. - -.. math:: - \begin{array}{llclll} - \production{function section} & \Bfuncsec &::=& - x^\ast{:}\Bsection_3(\Bvec(\Btypeidx)) &\Rightarrow& x^\ast \\ - \end{array} - - -.. index:: ! table section, table, table type - pair: binary format; table - pair: section; table -.. _binary-table: -.. _binary-tablesec: - -Table Section -~~~~~~~~~~~~~ - -The *table section* has the id 4. -It decodes into a vector of :ref:`tables ` that represent the |MTABLES| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{table section} & \Btablesec &::=& - \X{tab}^\ast{:}\Bsection_4(\Bvec(\Btable)) &\Rightarrow& \X{tab}^\ast \\ - \production{table} & \Btable &::=& - \X{tt}{:}\Btabletype &\Rightarrow& \{ \TTYPE~\X{tt} \} \\ - \end{array} - - -.. index:: ! memory section, memory, memory type - pair: binary format; memory - pair: section; memory -.. _binary-mem: -.. _binary-memsec: - -Memory Section -~~~~~~~~~~~~~~ - -The *memory section* has the id 5. -It decodes into a vector of :ref:`memories ` that represent the |MMEMS| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{memory section} & \Bmemsec &::=& - \X{mem}^\ast{:}\Bsection_5(\Bvec(\Bmem)) &\Rightarrow& \X{mem}^\ast \\ - \production{memory} & \Bmem &::=& - \X{mt}{:}\Bmemtype &\Rightarrow& \{ \MTYPE~\X{mt} \} \\ - \end{array} - - -.. index:: ! global section, global, global type, expression - pair: binary format; global - pair: section; global -.. _binary-global: -.. _binary-globalsec: - -Global Section -~~~~~~~~~~~~~~ - -The *global section* has the id 6. -It decodes into a vector of :ref:`globals ` that represent the |MGLOBALS| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{global section} & \Bglobalsec &::=& - \X{glob}^\ast{:}\Bsection_6(\Bvec(\Bglobal)) &\Rightarrow& \X{glob}^\ast \\ - \production{global} & \Bglobal &::=& - \X{gt}{:}\Bglobaltype~~e{:}\Bexpr - &\Rightarrow& \{ \GTYPE~\X{gt}, \GINIT~e \} \\ - \end{array} - - -.. index:: ! export section, export, name, index, function index, table index, memory index, global index - pair: binary format; export - pair: section; export -.. _binary-export: -.. _binary-exportdesc: -.. _binary-exportsec: - -Export Section -~~~~~~~~~~~~~~ - -The *export section* has the id 7. -It decodes into a vector of :ref:`exports ` that represent the |MEXPORTS| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{export section} & \Bexportsec &::=& - \X{ex}^\ast{:}\Bsection_7(\Bvec(\Bexport)) &\Rightarrow& \X{ex}^\ast \\ - \production{export} & \Bexport &::=& - \X{nm}{:}\Bname~~d{:}\Bexportdesc - &\Rightarrow& \{ \ENAME~\X{nm}, \EDESC~d \} \\ - \production{export description} & \Bexportdesc &::=& - \hex{00}~~x{:}\Bfuncidx &\Rightarrow& \EDFUNC~x \\ &&|& - \hex{01}~~x{:}\Btableidx &\Rightarrow& \EDTABLE~x \\ &&|& - \hex{02}~~x{:}\Bmemidx &\Rightarrow& \EDMEM~x \\ &&|& - \hex{03}~~x{:}\Bglobalidx &\Rightarrow& \EDGLOBAL~x \\ - \end{array} - - -.. index:: ! start section, start function, function index - pair: binary format; start function - single: section; start - single: start function; section -.. _binary-start: -.. _binary-startsec: - -Start Section -~~~~~~~~~~~~~ - -The *start section* has the id 8. -It decodes into an optional :ref:`start function ` that represents the |MSTART| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{start section} & \Bstartsec &::=& - \X{st}^?{:}\Bsection_8(\Bstart) &\Rightarrow& \X{st}^? \\ - \production{start function} & \Bstart &::=& - x{:}\Bfuncidx &\Rightarrow& \{ \SFUNC~x \} \\ - \end{array} - - -.. index:: ! element section, element, table index, expression, function index - pair: binary format; element - pair: section; element - single: table; element - single: element; segment -.. _binary-elem: -.. _binary-elemsec: - -Element Section -~~~~~~~~~~~~~~~ - -The *element section* has the id 9. -It decodes into a vector of :ref:`element segments ` that represent the |MELEM| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{element section} & \Belemsec &::=& - \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\ - \production{element segment} & \Belem &::=& - \hex{00}~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx) - &\Rightarrow& \{ \ETABLE~0, \EOFFSET~e, \EINIT~y^\ast \} \\ &&|& - \hex{02}~~x{:}\Btableidx~~e{:}\Bexpr~~\hex{00}~~y^\ast{:}\Bvec(\Bfuncidx) - &\Rightarrow& \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\ - \end{array} - - -.. index:: ! code section, function, local, type index, function type - pair: binary format; function - pair: binary format; local - pair: section; code -.. _binary-code: -.. _binary-func: -.. _binary-local: -.. _binary-codesec: - -Code Section -~~~~~~~~~~~~ - -The *code section* has the id 10. -It decodes into a vector of *code* entries that are pairs of :ref:`value type ` vectors and :ref:`expressions `. -They represent the |FLOCALS| and |FBODY| field of the :ref:`functions ` in the |MFUNCS| component of a :ref:`module `. -The |FTYPE| fields of the respective functions are encoded separately in the :ref:`function section `. - -The encoding of each code entry consists of - -* the |U32| *size* of the function code in bytes, -* the actual *function code*, which in turn consists of - - * the declaration of *locals*, - * the function *body* as an :ref:`expression `. - -Local declarations are compressed into a vector whose entries consist of - -* a |U32| *count*, -* a :ref:`value type `, - -denoting *count* locals of the same value type. - -.. math:: - \begin{array}{llclll@{\qquad}l} - \production{code section} & \Bcodesec &::=& - \X{code}^\ast{:}\Bsection_{10}(\Bvec(\Bcode)) - &\Rightarrow& \X{code}^\ast \\ - \production{code} & \Bcode &::=& - \X{size}{:}\Bu32~~\X{code}{:}\Bfunc - &\Rightarrow& \X{code} & (\iff \X{size} = ||\Bfunc||) \\ - \production{function} & \Bfunc &::=& - (t^\ast)^\ast{:}\Bvec(\Blocals)~~e{:}\Bexpr - &\Rightarrow& \concat((t^\ast)^\ast), e^\ast - & (\iff |\concat((t^\ast)^\ast)| < 2^{32}) \\ - \production{locals} & \Blocals &::=& - n{:}\Bu32~~t{:}\Bvaltype &\Rightarrow& t^n \\ - \end{array} - -Here, :math:`\X{code}` ranges over pairs :math:`(\valtype^\ast, \expr)`. -The meta function :math:`\concat((t^\ast)^\ast)` concatenates all sequences :math:`t_i^\ast` in :math:`(t^\ast)^\ast`. -Any code for which the length of the resulting sequence is out of bounds of the maximum size of a :ref:`vector ` is malformed. - -.. note:: - Like with :ref:`sections `, the code :math:`\X{size}` is not needed for decoding, but can be used to skip functions when navigating through a binary. - The module is malformed if a size does not match the length of the respective function code. - - -.. index:: ! data section, data, memory, memory index, expression, byte - pair: binary format; data - pair: section; data - single: memory; data - single: data; segment -.. _binary-data: -.. _binary-datasec: - -Data Section -~~~~~~~~~~~~ - -The *data section* has the id 11. -It decodes into a vector of :ref:`data segments ` that represent the |MDATA| component of a :ref:`module `. - -.. math:: - \begin{array}{llclll} - \production{data section} & \Bdatasec &::=& - \X{seg}^\ast{:}\Bsection_{11}(\Bvec(\Bdata)) &\Rightarrow& \X{seg} \\ - \production{data segment} & \Bdata &::=& - x{:}\Bmemidx~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte) - &\Rightarrow& \{ \DMEM~x, \DOFFSET~e, \DINIT~b^\ast \} \\ - \end{array} - - -.. index:: module, section, type definition, function type, function, table, memory, global, element, data, start function, import, export, context, version - pair: binary format; module -.. _binary-magic: -.. _binary-version: -.. _binary-module: - -Modules -~~~~~~~ - -The encoding of a :ref:`module ` starts with a preamble containing a 4-byte magic number (the string :math:`\text{\backslash0asm}`) and a version field. -The current version of the WebAssembly binary format is 1. - -The preamble is followed by a sequence of :ref:`sections `. -:ref:`Custom sections ` may be inserted at any place in this sequence, -while other sections must occur at most once and in the prescribed order. -All sections can be empty. - -The lengths of vectors produced by the (possibly empty) :ref:`function ` and :ref:`code ` section must match up. - -.. math:: - \begin{array}{llcllll} - \production{magic} & \Bmagic &::=& - \hex{00}~\hex{61}~\hex{73}~\hex{6D} \\ - \production{version} & \Bversion &::=& - \hex{01}~\hex{00}~\hex{00}~\hex{00} \\ - \production{module} & \Bmodule &::=& - \Bmagic \\ &&& - \Bversion \\ &&& - \Bcustomsec^\ast \\ &&& - \functype^\ast{:\,}\Btypesec \\ &&& - \Bcustomsec^\ast \\ &&& - \import^\ast{:\,}\Bimportsec \\ &&& - \Bcustomsec^\ast \\ &&& - \typeidx^n{:\,}\Bfuncsec \\ &&& - \Bcustomsec^\ast \\ &&& - \table^\ast{:\,}\Btablesec \\ &&& - \Bcustomsec^\ast \\ &&& - \mem^\ast{:\,}\Bmemsec \\ &&& - \Bcustomsec^\ast \\ &&& - \global^\ast{:\,}\Bglobalsec \\ &&& - \Bcustomsec^\ast \\ &&& - \export^\ast{:\,}\Bexportsec \\ &&& - \Bcustomsec^\ast \\ &&& - \start^?{:\,}\Bstartsec \\ &&& - \Bcustomsec^\ast \\ &&& - \elem^\ast{:\,}\Belemsec \\ &&& - \Bcustomsec^\ast \\ &&& - \X{code}^n{:\,}\Bcodesec \\ &&& - \Bcustomsec^\ast \\ &&& - \data^\ast{:\,}\Bdatasec \\ &&& - \Bcustomsec^\ast - \quad\Rightarrow\quad \{~ - \begin{array}[t]{@{}l@{}} - \MTYPES~\functype^\ast, \\ - \MFUNCS~\func^n, \\ - \MTABLES~\table^\ast, \\ - \MMEMS~\mem^\ast, \\ - \MGLOBALS~\global^\ast, \\ - \MELEM~\elem^\ast, \\ - \MDATA~\data^\ast, \\ - \MSTART~\start^?, \\ - \MIMPORTS~\import^\ast, \\ - \MEXPORTS~\export^\ast ~\} \\ - \end{array} \\ - \end{array} - -where for each :math:`t_i^\ast, e_i` in :math:`\X{code}^n`, - -.. math:: - \func^n[i] = \{ \FTYPE~\typeidx^n[i], \FLOCALS~t_i^\ast, \FBODY~e_i \} ) \\ - -.. note:: - The version of the WebAssembly binary format may increase in the future - if backward-incompatible changes have to be made to the format. - However, such changes are expected to occur very infrequently, if ever. - The binary format is intended to be forward-compatible, - such that future extensions can be made without incrementing its version. diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst deleted file mode 100644 index e7a7f8ed..00000000 --- a/document/core/binary/types.rst +++ /dev/null @@ -1,175 +0,0 @@ -.. index:: type - pair: binary format; type -.. _binary-type: - -Types ------ - -.. note:: - In future versions of WebAssembly, value types may include types denoted by :ref:`type indices `. - 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. - - -.. index:: number type - pair: binary format; number type -.. _binary-numtype: - -Number Types -~~~~~~~~~~~~ - -:ref:`Number types ` are encoded by a single byte. - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{number type} & \Bnumtype &::=& - \hex{7F} &\Rightarrow& \I32 \\ &&|& - \hex{7E} &\Rightarrow& \I64 \\ &&|& - \hex{7D} &\Rightarrow& \F32 \\ &&|& - \hex{7C} &\Rightarrow& \F64 \\ - \end{array} - - -.. index:: reference type - pair: binary format; reference type -.. _binary-reftype: - -Reference Types -~~~~~~~~~~~~~~~ - -:ref:`Reference types ` are also encoded by a single byte. - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{reference type} & \Breftype &::=& - \hex{70} &\Rightarrow& \FUNCREF \\ &&|& - \hex{6F} &\Rightarrow& \ANYREF \\ &&|& - \hex{6E} &\Rightarrow& \NULLREF \\ - \end{array} - - -.. index:: value type, number type, reference type - pair: binary format; value type -.. _binary-valtype: - -Value Types -~~~~~~~~~~~ - -:ref:`Value types ` are encoded with their respective encoding as a :ref:`number type ` or :ref:`reference type `. - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{value type} & \Bvaltype &::=& - t{:}\Bnumtype &\Rightarrow& t \\ &&|& - t{:}\Breftype &\Rightarrow& t \\ - \end{array} - -.. note:: - The type :math:`\BOT` cannot occur in a module. - - -.. index:: result type, value type - pair: binary format; result type -.. _binary-blocktype: -.. _binary-resulttype: - -Result Types -~~~~~~~~~~~~ - -The only :ref:`result types ` occurring in the binary format are the types of blocks. These are encoded in special compressed form, by either the byte :math:`\hex{40}` indicating the empty type or as a single :ref:`value type `. - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{result type} & \Bblocktype &::=& - \hex{40} &\Rightarrow& [] \\ &&|& - t{:}\Bvaltype &\Rightarrow& [t] \\ - \end{array} - -.. note:: - In future versions of WebAssembly, this scheme may be extended to support multiple results or more general block types. - - -.. index:: function type, value type, result type - pair: binary format; function type -.. _binary-functype: - -Function Types -~~~~~~~~~~~~~~ - -:ref:`Function types ` are encoded by the byte :math:`\hex{60}` followed by the respective :ref:`vectors ` of parameter and result types. - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{function type} & \Bfunctype &::=& - \hex{60}~~t_1^\ast{:\,}\Bvec(\Bvaltype)~~t_2^\ast{:\,}\Bvec(\Bvaltype) - &\Rightarrow& [t_1^\ast] \to [t_2^\ast] \\ - \end{array} - - -.. index:: limits - pair: binary format; limits -.. _binary-limits: - -Limits -~~~~~~ - -:ref:`Limits ` are encoded with a preceding flag indicating whether a maximum is present. - -.. math:: - \begin{array}{llclll} - \production{limits} & \Blimits &::=& - \hex{00}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \} \\ &&|& - \hex{01}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \} \\ - \end{array} - - -.. index:: memory type, limits, page size - pair: binary format; memory type -.. _binary-memtype: - -Memory Types -~~~~~~~~~~~~ - -:ref:`Memory types ` are encoded with their :ref:`limits `. - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{memory type} & \Bmemtype &::=& - \X{lim}{:}\Blimits &\Rightarrow& \X{lim} \\ - \end{array} - - -.. index:: table type, reference type, limits - pair: binary format; table type -.. _binary-tabletype: - -Table Types -~~~~~~~~~~~ - -:ref:`Table types ` are encoded with their :ref:`limits ` and the encoding of their element :ref:`reference type `. - -.. math:: - \begin{array}{llclll} - \production{table type} & \Btabletype &::=& - \X{et}{:}\Breftype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\ - \end{array} - - -.. index:: global type, mutability, value type - pair: binary format; global type - pair: binary format; mutability -.. _binary-mut: -.. _binary-globaltype: - -Global Types -~~~~~~~~~~~~ - -:ref:`Global types ` are encoded by their :ref:`value type ` and a flag for their :ref:`mutability `. - -.. math:: - \begin{array}{llclll} - \production{global type} & \Bglobaltype &::=& - t{:}\Bvaltype~~m{:}\Bmut &\Rightarrow& m~t \\ - \production{mutability} & \Bmut &::=& - \hex{00} &\Rightarrow& \MCONST \\ &&|& - \hex{01} &\Rightarrow& \MVAR \\ - \end{array} diff --git a/document/core/binary/values.rst b/document/core/binary/values.rst deleted file mode 100644 index c6268624..00000000 --- a/document/core/binary/values.rst +++ /dev/null @@ -1,148 +0,0 @@ -.. index:: value - pair: binary format; value -.. _binary-value: - -Values ------- - - -.. index:: byte - pair: binary format; byte -.. _binary-byte: - -Bytes -~~~~~ - -:ref:`Bytes ` encode themselves. - -.. math:: - \begin{array}{llcll@{\qquad}l} - \production{byte} & \Bbyte &::=& - \hex{00} &\Rightarrow& \hex{00} \\ &&|&& - \dots \\ &&|& - \hex{FF} &\Rightarrow& \hex{FF} \\ - \end{array} - - -.. index:: integer, unsigned integer, signed integer, uninterpreted integer, LEB128, two's complement - pair: binary format; integer - pair: binary format; unsigned integer - pair: binary format; signed integer - pair: binary format; uninterpreted integer -.. _binary-sint: -.. _binary-uint: -.. _binary-int: - -Integers -~~~~~~~~ - -All :ref:`integers ` are encoded using the |LEB128|_ variable-length integer encoding, in either unsigned or signed variant. - -:ref:`Unsigned integers ` are encoded in |UnsignedLEB128|_ format. -As an additional constraint, the total number of bytes encoding a value of type :math:`\uN` must not exceed :math:`\F{ceil}(N/7)` bytes. - -.. math:: - \begin{array}{llclll@{\qquad}l} - \production{unsigned integer} & \BuN &::=& - n{:}\Bbyte &\Rightarrow& n & (\iff n < 2^7 \wedge n < 2^N) \\ &&|& - n{:}\Bbyte~~m{:}\BuX{(N\B{-7})} &\Rightarrow& - 2^7\cdot m + (n-2^7) & (\iff n \geq 2^7 \wedge N > 7) \\ - \end{array} - -:ref:`Signed integers ` are encoded in |SignedLEB128|_ format, which uses a two's complement representation. -As an additional constraint, the total number of bytes encoding a value of type :math:`\sN` must not exceed :math:`\F{ceil}(N/7)` bytes. - -.. math:: - \begin{array}{llclll@{\qquad}l} - \production{signed integer} & \BsN &::=& - n{:}\Bbyte &\Rightarrow& n & (\iff n < 2^6 \wedge n < 2^{N-1}) \\ &&|& - n{:}\Bbyte &\Rightarrow& n-2^7 & (\iff 2^6 \leq n < 2^7 \wedge n \geq 2^7-2^{N-1}) \\ &&|& - n{:}\Bbyte~~m{:}\BsX{(N\B{-7})} &\Rightarrow& - 2^7\cdot m + (n-2^7) & (\iff n \geq 2^7 \wedge N > 7) \\ - \end{array} - -:ref:`Uninterpreted integers ` are encoded as signed integers. - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{uninterpreted integer} & \BiN &::=& - n{:}\BsN &\Rightarrow& i & (\iff n = \signed_{\iN}(i)) - \end{array} - -.. note:: - The side conditions :math:`N > 7` in the productions for non-terminal bytes of the :math:`\uX{}` and :math:`\sX{}` encodings restrict the encoding's length. - However, "trailing zeros" are still allowed within these bounds. - For example, :math:`\hex{03}` and :math:`\hex{83}~\hex{00}` are both well-formed encodings for the value :math:`3` as a |u8|. - Similarly, either of :math:`\hex{7e}` and :math:`\hex{FE}~\hex{7F}` and :math:`\hex{FE}~\hex{FF}~\hex{7F}` are well-formed encodings of the value :math:`-2` as a |s16|. - - The side conditions on the value :math:`n` of terminal bytes further enforce that - any unused bits in these bytes must be :math:`0` for positive values and :math:`1` for negative ones. - For example, :math:`\hex{83}~\hex{10}` is malformed as a |u8| encoding. - Similarly, both :math:`\hex{83}~\hex{3E}` and :math:`\hex{FF}~\hex{7B}` are malformed as |s8| encodings. - - -.. index:: floating-point number, little endian - pair: binary format; floating-point number -.. _binary-float: - -Floating-Point -~~~~~~~~~~~~~~ - -:ref:`Floating-point ` values are encoded directly by their |IEEE754|_ (Section 3.4) bit pattern in |LittleEndian|_ byte order: - -.. math:: - \begin{array}{llclll@{\qquad\qquad}l} - \production{floating-point value} & \BfN &::=& - b^\ast{:\,}\Bbyte^{N/8} &\Rightarrow& \bytes_{\fN}^{-1}(b^\ast) \\ - \end{array} - - -.. index:: name, byte, Unicode, ! UTF-8 - pair: binary format; name -.. _binary-utf8: -.. _binary-name: - -Names -~~~~~ - -:ref:`Names ` are encoded as a :ref:`vector ` of bytes containing the |Unicode|_ (Section 3.9) UTF-8 encoding of the name's character sequence. - -.. math:: - \begin{array}{llclllll} - \production{name} & \Bname &::=& - b^\ast{:}\Bvec(\Bbyte) &\Rightarrow& \name - && (\iff \utf8(\name) = b^\ast) \\ - \end{array} - -The auxiliary |utf8| function expressing this encoding is defined as follows: - -.. math:: - \begin{array}{@{}l@{}} - \begin{array}{@{}lcl@{\qquad}l@{}} - \utf8(c^\ast) &=& (\utf8(c))^\ast \\[1ex] - \utf8(c) &=& b & - (\begin{array}[t]{@{}c@{~}l@{}} - \iff & c < \unicode{80} \\ - \wedge & c = b) \\ - \end{array} \\ - \utf8(c) &=& b_1~b_2 & - (\begin{array}[t]{@{}c@{~}l@{}} - \iff & \unicode{80} \leq c < \unicode{800} \\ - \wedge & c = 2^6(b_1-\hex{C0})+(b_2-\hex{80})) \\ - \end{array} \\ - \utf8(c) &=& b_1~b_2~b_3 & - (\begin{array}[t]{@{}c@{~}l@{}} - \iff & \unicode{800} \leq c < \unicode{D800} \vee \unicode{E000} \leq c < \unicode{10000} \\ - \wedge & c = 2^{12}(b_1-\hex{E0})+2^6(b_2-\hex{80})+(b_3-\hex{80})) \\ - \end{array} \\ - \utf8(c) &=& b_1~b_2~b_3~b_4 & - (\begin{array}[t]{@{}c@{~}l@{}} - \iff & \unicode{10000} \leq c < \unicode{110000} \\ - \wedge & c = 2^{18}(b_1-\hex{F0})+2^{12}(b_2-\hex{80})+2^6(b_3-\hex{80})+(b_4-\hex{80})) \\ - \end{array} \\ - \end{array} \\ - \where b_2, b_3, b_4 < \hex{C0} \\ - \end{array} - -.. note:: - Unlike in some other formats, name strings are not 0-terminated. diff --git a/document/core/exec/conventions.rst b/document/core/exec/conventions.rst deleted file mode 100644 index 807239b0..00000000 --- a/document/core/exec/conventions.rst +++ /dev/null @@ -1,134 +0,0 @@ -.. index:: ! execution, stack, store - -Conventions ------------ - -WebAssembly code is *executed* when :ref:`instantiating ` a module or :ref:`invoking ` an :ref:`exported ` function on the resulting module :ref:`instance `. - -Execution behavior is defined in terms of an *abstract machine* that models the *program state*. -It includes a *stack*, which records operand values and control constructs, and an abstract *store* containing global state. - -For each instruction, there is a rule that specifies the effect of its execution on the program state. -Furthermore, there are rules describing the instantiation of a module. -As with :ref:`validation `, all rules are given in two *equivalent* forms: - -1. In *prose*, describing the execution in intuitive form. -2. In *formal notation*, describing the rule in mathematical form. [#cite-pldi2017]_ - -.. note:: - As with validation, the prose and formal rules are equivalent, - so that understanding of the formal notation is *not* required to read this specification. - The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof. - - -.. _exec-notation-textual: - -Prose Notation -~~~~~~~~~~~~~~ - -Execution is specified by stylised, step-wise rules for each :ref:`instruction ` of the :ref:`abstract syntax `. -The following conventions are adopted in stating these rules. - -* The execution rules implicitly assume a given :ref:`store ` :math:`S`. - -* The execution rules also assume the presence of an implicit :ref:`stack ` - that is modified by *pushing* or *popping* - :ref:`values `, :ref:`labels `, and :ref:`frames `. - -* Certain rules require the stack to contain at least one frame. - The most recent frame is referred to as the *current* frame. - -* Both the store and the current frame are mutated by *replacing* some of their components. - Such replacement is assumed to apply globally. - -* The execution of an instruction may *trap*, - in which case the entire computation is aborted and no further modifications to the store are performed by it. (Other computations can still be initiated afterwards.) - -* The execution of an instruction may also end in a *jump* to a designated target, - which defines the next instruction to execute. - -* Execution can *enter* and *exit* :ref:`instruction sequences ` that form :ref:`blocks `. - -* :ref:`Instruction sequences ` are implicitly executed in order, unless a trap or jump occurs. - -* In various places the rules contain *assertions* expressing crucial invariants about the program state. - - -.. index:: ! reduction rules, configuration, evaluation context -.. _exec-notation: - -Formal Notation -~~~~~~~~~~~~~~~ - -.. note:: - This section gives a brief explanation of the notation for specifying execution formally. - For the interested reader, a more thorough introduction can be found in respective text books. [#cite-tapl]_ - -The formal execution rules use a standard approach for specifying operational semantics, rendering them into *reduction rules*. -Every rule has the following general form: - -.. math:: - \X{configuration} \quad\stepto\quad \X{configuration} - -A *configuration* is a syntactic description of a program state. -Each rule specifies one *step* of execution. -As long as there is at most one reduction rule applicable to a given configuration, reduction -- and thereby execution -- is *deterministic*. -WebAssembly has only very few exceptions to this, which are noted explicitly in this specification. - -For WebAssembly, a configuration typically is a tuple :math:`(S; F; \instr^\ast)` consisting of the current :ref:`store ` :math:`S`, the :ref:`call frame ` :math:`F` of the current function, and the sequence of :ref:`instructions ` that is to be executed. -(A more precise definition is given :ref:`later `.) - -To avoid unnecessary clutter, the store :math:`S` and the frame :math:`F` are omitted from reduction rules that do not touch them. - -There is no separate representation of the :ref:`stack `. -Instead, it is conveniently represented as part of the configuration's instruction sequence. -In particular, :ref:`values ` are defined to coincide with |CONST| instructions, -and a sequence of |CONST| instructions can be interpreted as an operand "stack" that grows to the right. - -.. note:: - For example, the :ref:`reduction rule ` for the :math:`\I32.\ADD` instruction can be given as follows: - - .. math:: - (\I32.\CONST~n_1)~(\I32.\CONST~n_2)~\I32.\ADD \quad\stepto\quad (\I32.\CONST~(n_1 + n_2) \mod 2^{32}) - - Per this rule, two |CONST| instructions and the |ADD| instruction itself are removed from the instruction stream and replaced with one new |CONST| instruction. - This can be interpreted as popping two value off the stack and pushing the result. - - When no result is produced, an instruction reduces to the empty sequence: - - .. math:: - \NOP \quad\stepto\quad \epsilon - -:ref:`Labels