diff --git a/.github/workflows/ci-interpreter.yml b/.github/workflows/ci-interpreter.yml index 89550968..76f44418 100644 --- a/.github/workflows/ci-interpreter.yml +++ b/.github/workflows/ci-interpreter.yml @@ -3,11 +3,11 @@ name: CI for interpreter & tests on: push: branches: [ main ] - paths: [ interpreter/**, test/** ] + paths: [ .github/**, interpreter/**, test/** ] pull_request: branches: [ main ] - paths: [ interpreter/**, test/** ] + paths: [ .github/**, interpreter/**, test/** ] # Allows you to run this workflow manually from the Actions tab workflow_dispatch: diff --git a/.github/workflows/ci-spec.yml b/.github/workflows/ci-spec.yml index 7610b33b..e88a224d 100644 --- a/.github/workflows/ci-spec.yml +++ b/.github/workflows/ci-spec.yml @@ -3,11 +3,11 @@ name: CI for specs on: push: branches: [ main ] - paths: [ document/** ] + paths: [ .github/**, document/** ] pull_request: branches: [ main ] - paths: [ document/** ] + paths: [ .github/**, document/** ] # Allows you to run this workflow manually from the Actions tab workflow_dispatch: diff --git a/.github/workflows/w3c-publish.yml b/.github/workflows/w3c-publish.yml new file mode 100644 index 00000000..eeade04e --- /dev/null +++ b/.github/workflows/w3c-publish.yml @@ -0,0 +1,36 @@ +name: Publish to W3C TR space + +on: + push: + branches: [ main ] + paths: [ .github/**, document/** ] + + # Allows you to run this workflow manually from the Actions tab + workflow_dispatch: + +jobs: + publish-to-w3c-TR: + runs-on: ubuntu-latest + steps: + - name: Checkout repo + uses: actions/checkout@v2 + with: + submodules: "recursive" + - name: Setup Node.js + uses: actions/setup-node@v3 + with: + node-version: 16 + - name: Setup Bikeshed + run: pip install bikeshed && bikeshed update + - name: Setup TexLive + run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended + - name: Setup Sphinx + run: pip install six && pip install sphinx==5.1.0 + - name: Publish all specs to their https://www.w3.org/TR/ URLs + run: cd document && make -e WD-echidna-CI + env: + STATUS: --md-status=WD + W3C_ECHIDNA_TOKEN_CORE: ${{ secrets.W3C_ECHIDNA_TOKEN_CORE }} + W3C_ECHIDNA_TOKEN_JSAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_JSAPI }} + W3C_ECHIDNA_TOKEN_WEBAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_WEBAPI }} + YARN_ENABLE_IMMUTABLE_INSTALLS: false diff --git a/document/Makefile b/document/Makefile index 875efc72..01a6d934 100644 --- a/document/Makefile +++ b/document/Makefile @@ -1,6 +1,7 @@ -DIRS = core js-api web-api +DIRS = js-api web-api core FILES = index.html BUILDDIR = _build +TAR = tar # Global targets. @@ -24,6 +25,25 @@ clean: $(DIRS:%=clean-%) .PHONY: diff diff: $(DIRS:%=diff-%) +# macOS: do “brew install tar” & run “make” as: TAR=gtar make -e WD-tar +.PHONY: WD-tar +WD-tar: + for dir in $(DIRS); \ + do STATUS=--md-status=WD TAR=$(TAR) $(MAKE) -e -C $$dir $@;\ + done + +# macOS: do “brew install tar” & run “make” as: TAR=gtar make -e WD-echidna +.PHONY: WD-echidna +WD-echidna: + for dir in $(DIRS); \ + do $(MAKE) -e -C $$dir $@;\ + done + +.PHONY: WD-echidna-CI +WD-echidna-CI: + for dir in $(DIRS); \ + do $(MAKE) -e -C $$dir $@;\ + done # Directory-specific targets. diff --git a/document/core/Makefile b/document/core/Makefile index 8a3650ec..74c9daee 100644 --- a/document/core/Makefile +++ b/document/core/Makefile @@ -9,6 +9,8 @@ BUILDDIR = _build STATICDIR = _static DOWNLOADDIR = _download NAME = WebAssembly +DECISION_URL = https://github.com/WebAssembly/meetings/blob/main/main/2017/WG-12-06.md +TAR = tar # Internal variables. PAPEROPT_a4 = -D latex_paper_size=a4 @@ -148,7 +150,7 @@ bikeshed: $(GENERATED) @echo @echo ========================================================================= mkdir -p $(BUILDDIR)/bikeshed_mathjax/ - bikeshed spec index.bs $(BUILDDIR)/bikeshed_mathjax/index.html + bikeshed spec $(STATUS) index.bs $(BUILDDIR)/bikeshed_mathjax/index.html mkdir -p $(BUILDDIR)/html/bikeshed/ (cd util/katex/ && yarn && yarn build && npm install --only=prod) python3 util/mathjax2katex.py $(BUILDDIR)/bikeshed_mathjax/index.html \ @@ -163,9 +165,11 @@ bikeshed: $(GENERATED) @echo "Build finished. The HTML page is in $(BUILDDIR)/html/bikeshed/." .PHONY: WD-tar +# macOS tar has no “--transform” option (only GNU tar does), so on macOS, +# do “brew install tar” & run “make” like this: “TAR=gtar make -e WD-tar” WD-tar: bikeshed @echo "Building tar file..." - tar cvf \ + $(TAR) cvf \ $(BUILDDIR)/WD.tar \ --transform='s|$(BUILDDIR)/html/bikeshed/||' \ --transform='s|index.html|Overview.html|' \ @@ -190,6 +194,20 @@ WD-echidna: WD-tar @echo @echo "Published working draft. Check its status at https://labs.w3.org/echidna/api/status?id=`cat $(BUILDDIR)/WD-echidna-id.txt`" +.PHONY: WD-echidna-CI +WD-echidna-CI: WD-tar + @if [ -z $(W3C_ECHIDNA_TOKEN_CORE) ] || \ + [ -z $(DECISION_URL) ] ; then \ + echo "Must provide W3C_ECHIDNA_TOKEN_CORE and DECISION_URL environment variables"; \ + exit 1; \ + fi + curl 'https://labs.w3.org/echidna/api/request' \ + -F "tar=@$(BUILDDIR)/WD.tar" \ + -F "token=$(W3C_ECHIDNA_TOKEN_CORE)" \ + -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..." diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst index 27aac4b3..96fa6b2f 100644 --- a/document/core/appendix/embedding.rst +++ b/document/core/appendix/embedding.rst @@ -323,7 +323,7 @@ Tables .. _embed-table-alloc: -:math:`\F{table\_alloc}(\store, \tabletype) : (\store, \tableaddr, \reff)` +:math:`\F{table\_alloc}(\store, \tabletype, \reff) : (\store, \tableaddr)` .......................................................................... 1. Pre-condition: :math:`\tabletype` is :ref:`valid `. diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index 2503a7ab..ac94dd1a 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -54,8 +54,7 @@ def RefWrap(s, kind): def Instruction(name, opcode, type=None, validation=None, execution=None, operator=None): if operator: - execution_str = ', '.join([RefWrap(execution, 'execution'), - RefWrap(operator, 'operator')]) + execution_str = RefWrap(execution, 'execution') + ' (' + RefWrap(operator, 'operator') + ')' else: execution_str = RefWrap(execution, 'execution') @@ -374,48 +373,48 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\F32X4.\REPLACELANE~\laneidx', r'\hex{FD}~~\hex{20}', r'[\V128~\F32] \to [\V128]', r'valid-vec-replace_lane', r'exec-vec-replace_lane'), Instruction(r'\F64X2.\EXTRACTLANE~\laneidx', r'\hex{FD}~~\hex{21}', r'[\V128] \to [\F64]', r'valid-vec-extract_lane', r'exec-vec-extract_lane'), Instruction(r'\F64X2.\REPLACELANE~\laneidx', r'\hex{FD}~~\hex{22}', r'[\V128~\F64] \to [\V128]', r'valid-vec-replace_lane', r'exec-vec-replace_lane'), - Instruction(r'\I8X16.\VEQ', r'\hex{FD}~~\hex{23}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ieq'), - Instruction(r'\I8X16.\VNE', r'\hex{FD}~~\hex{24}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ine'), - Instruction(r'\I8X16.\VLT\K{\_s}', r'\hex{FD}~~\hex{25}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_s'), - Instruction(r'\I8X16.\VLT\K{\_u}', r'\hex{FD}~~\hex{26}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_u'), - Instruction(r'\I8X16.\VGT\K{\_s}', r'\hex{FD}~~\hex{27}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_s'), - Instruction(r'\I8X16.\VGT\K{\_u}', r'\hex{FD}~~\hex{28}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_u'), - Instruction(r'\I8X16.\VLE\K{\_s}', r'\hex{FD}~~\hex{29}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_s'), - Instruction(r'\I8X16.\VLE\K{\_u}', r'\hex{FD}~~\hex{2A}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_u'), - Instruction(r'\I8X16.\VGE\K{\_s}', r'\hex{FD}~~\hex{2B}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_s'), - Instruction(r'\I8X16.\VGE\K{\_u}', r'\hex{FD}~~\hex{2C}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_u'), - Instruction(r'\I16X8.\VEQ', r'\hex{FD}~~\hex{2D}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ieq'), - Instruction(r'\I16X8.\VNE', r'\hex{FD}~~\hex{2E}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ine'), - Instruction(r'\I16X8.\VLT\K{\_s}', r'\hex{FD}~~\hex{2F}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_s'), - Instruction(r'\I16X8.\VLT\K{\_u}', r'\hex{FD}~~\hex{30}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_u'), - Instruction(r'\I16X8.\VGT\K{\_s}', r'\hex{FD}~~\hex{31}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_s'), - Instruction(r'\I16X8.\VGT\K{\_u}', r'\hex{FD}~~\hex{32}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_u'), - Instruction(r'\I16X8.\VLE\K{\_s}', r'\hex{FD}~~\hex{33}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_s'), - Instruction(r'\I16X8.\VLE\K{\_u}', r'\hex{FD}~~\hex{34}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_u'), - Instruction(r'\I16X8.\VGE\K{\_s}', r'\hex{FD}~~\hex{35}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_s'), - Instruction(r'\I16X8.\VGE\K{\_u}', r'\hex{FD}~~\hex{36}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_u'), - Instruction(r'\I32X4.\VEQ', r'\hex{FD}~~\hex{37}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ieq'), - Instruction(r'\I32X4.\VNE', r'\hex{FD}~~\hex{38}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ine'), - Instruction(r'\I32X4.\VLT\K{\_s}', r'\hex{FD}~~\hex{39}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_s'), - Instruction(r'\I32X4.\VLT\K{\_u}', r'\hex{FD}~~\hex{3A}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_u'), - Instruction(r'\I32X4.\VGT\K{\_s}', r'\hex{FD}~~\hex{3B}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_s'), - Instruction(r'\I32X4.\VGT\K{\_u}', r'\hex{FD}~~\hex{3C}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_u'), - Instruction(r'\I32X4.\VLE\K{\_s}', r'\hex{FD}~~\hex{3D}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_s'), - Instruction(r'\I32X4.\VLE\K{\_u}', r'\hex{FD}~~\hex{3E}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_u'), - Instruction(r'\I32X4.\VGE\K{\_s}', r'\hex{FD}~~\hex{3F}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_s'), - Instruction(r'\I32X4.\VGE\K{\_u}', r'\hex{FD}~~\hex{40}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_u'), - Instruction(r'\F32X4.\VEQ', r'\hex{FD}~~\hex{41}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-feq'), - Instruction(r'\F32X4.\VNE', r'\hex{FD}~~\hex{42}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fne'), - Instruction(r'\F32X4.\VLT', r'\hex{FD}~~\hex{43}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-flt'), - Instruction(r'\F32X4.\VGT', r'\hex{FD}~~\hex{44}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fgt'), - Instruction(r'\F32X4.\VLE', r'\hex{FD}~~\hex{45}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fle'), - Instruction(r'\F32X4.\VGE', r'\hex{FD}~~\hex{46}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fge'), - Instruction(r'\F64X2.\VEQ', r'\hex{FD}~~\hex{47}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-feq'), - Instruction(r'\F64X2.\VNE', r'\hex{FD}~~\hex{48}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fne'), - Instruction(r'\F64X2.\VLT', r'\hex{FD}~~\hex{49}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-flt'), - Instruction(r'\F64X2.\VGT', r'\hex{FD}~~\hex{4A}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fgt'), - Instruction(r'\F64X2.\VLE', r'\hex{FD}~~\hex{4B}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fle'), - Instruction(r'\F64X2.\VGE', r'\hex{FD}~~\hex{4C}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fge'), + Instruction(r'\I8X16.\VEQ', r'\hex{FD}~~\hex{23}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ieq'), + Instruction(r'\I8X16.\VNE', r'\hex{FD}~~\hex{24}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ine'), + Instruction(r'\I8X16.\VLT\K{\_s}', r'\hex{FD}~~\hex{25}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_s'), + Instruction(r'\I8X16.\VLT\K{\_u}', r'\hex{FD}~~\hex{26}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_u'), + Instruction(r'\I8X16.\VGT\K{\_s}', r'\hex{FD}~~\hex{27}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_s'), + Instruction(r'\I8X16.\VGT\K{\_u}', r'\hex{FD}~~\hex{28}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_u'), + Instruction(r'\I8X16.\VLE\K{\_s}', r'\hex{FD}~~\hex{29}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_s'), + Instruction(r'\I8X16.\VLE\K{\_u}', r'\hex{FD}~~\hex{2A}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_u'), + Instruction(r'\I8X16.\VGE\K{\_s}', r'\hex{FD}~~\hex{2B}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_s'), + Instruction(r'\I8X16.\VGE\K{\_u}', r'\hex{FD}~~\hex{2C}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_u'), + Instruction(r'\I16X8.\VEQ', r'\hex{FD}~~\hex{2D}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ieq'), + Instruction(r'\I16X8.\VNE', r'\hex{FD}~~\hex{2E}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ine'), + Instruction(r'\I16X8.\VLT\K{\_s}', r'\hex{FD}~~\hex{2F}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_s'), + Instruction(r'\I16X8.\VLT\K{\_u}', r'\hex{FD}~~\hex{30}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_u'), + Instruction(r'\I16X8.\VGT\K{\_s}', r'\hex{FD}~~\hex{31}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_s'), + Instruction(r'\I16X8.\VGT\K{\_u}', r'\hex{FD}~~\hex{32}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_u'), + Instruction(r'\I16X8.\VLE\K{\_s}', r'\hex{FD}~~\hex{33}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_s'), + Instruction(r'\I16X8.\VLE\K{\_u}', r'\hex{FD}~~\hex{34}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_u'), + Instruction(r'\I16X8.\VGE\K{\_s}', r'\hex{FD}~~\hex{35}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_s'), + Instruction(r'\I16X8.\VGE\K{\_u}', r'\hex{FD}~~\hex{36}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_u'), + Instruction(r'\I32X4.\VEQ', r'\hex{FD}~~\hex{37}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ieq'), + Instruction(r'\I32X4.\VNE', r'\hex{FD}~~\hex{38}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ine'), + Instruction(r'\I32X4.\VLT\K{\_s}', r'\hex{FD}~~\hex{39}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_s'), + Instruction(r'\I32X4.\VLT\K{\_u}', r'\hex{FD}~~\hex{3A}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_u'), + Instruction(r'\I32X4.\VGT\K{\_s}', r'\hex{FD}~~\hex{3B}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_s'), + Instruction(r'\I32X4.\VGT\K{\_u}', r'\hex{FD}~~\hex{3C}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_u'), + Instruction(r'\I32X4.\VLE\K{\_s}', r'\hex{FD}~~\hex{3D}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_s'), + Instruction(r'\I32X4.\VLE\K{\_u}', r'\hex{FD}~~\hex{3E}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_u'), + Instruction(r'\I32X4.\VGE\K{\_s}', r'\hex{FD}~~\hex{3F}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_s'), + Instruction(r'\I32X4.\VGE\K{\_u}', r'\hex{FD}~~\hex{40}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_u'), + Instruction(r'\F32X4.\VEQ', r'\hex{FD}~~\hex{41}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-feq'), + Instruction(r'\F32X4.\VNE', r'\hex{FD}~~\hex{42}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fne'), + Instruction(r'\F32X4.\VLT', r'\hex{FD}~~\hex{43}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-flt'), + Instruction(r'\F32X4.\VGT', r'\hex{FD}~~\hex{44}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fgt'), + Instruction(r'\F32X4.\VLE', r'\hex{FD}~~\hex{45}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fle'), + Instruction(r'\F32X4.\VGE', r'\hex{FD}~~\hex{46}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fge'), + Instruction(r'\F64X2.\VEQ', r'\hex{FD}~~\hex{47}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-feq'), + Instruction(r'\F64X2.\VNE', r'\hex{FD}~~\hex{48}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fne'), + Instruction(r'\F64X2.\VLT', r'\hex{FD}~~\hex{49}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-flt'), + Instruction(r'\F64X2.\VGT', r'\hex{FD}~~\hex{4A}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fgt'), + Instruction(r'\F64X2.\VLE', r'\hex{FD}~~\hex{4B}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fle'), + Instruction(r'\F64X2.\VGE', r'\hex{FD}~~\hex{4C}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fge'), Instruction(r'\V128.\VNOT', r'\hex{FD}~~\hex{4D}', r'[\V128] \to [\V128]', r'valid-vvunop', r'exec-vvunop', r'op-inot'), Instruction(r'\V128.\VAND', r'\hex{FD}~~\hex{4E}', r'[\V128~\V128] \to [\V128]', r'valid-vvbinop', r'exec-vvbinop', r'op-iand'), Instruction(r'\V128.\VANDNOT', r'\hex{FD}~~\hex{4F}', r'[\V128~\V128] \to [\V128]', r'valid-vvbinop', r'exec-vvbinop', r'op-iandnot'), @@ -431,8 +430,8 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat Instruction(r'\V128.\STORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'), Instruction(r'\V128.\STORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'), Instruction(r'\V128.\STORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'), - Instruction(r'\V128.\LOAD\K{32\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5C}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'), - Instruction(r'\V128.\LOAD\K{64\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5D}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'), + Instruction(r'\V128.\LOAD\K{32\_zero}~\memarg', r'\hex{FD}~~\hex{5C}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'), + Instruction(r'\V128.\LOAD\K{64\_zero}~\memarg', r'\hex{FD}~~\hex{5D}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'), Instruction(r'\F32X4.\VDEMOTE\K{\_f64x2\_zero}', r'\hex{FD}~~\hex{5E}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-demote'), Instruction(r'\F64X2.\VPROMOTE\K{\_low\_f32x4}', r'\hex{FD}~~\hex{5F}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-promote'), Instruction(r'\I8X16.\VABS', r'\hex{FD}~~\hex{60}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-iabs'), diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index d9b6a354..36bc6f80 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -278,8 +278,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co .. index:: element instance, reference .. _valid-eleminst: -:ref:`Element Instances ` :math:`\{ \EIELEM~\X{fa}^\ast \}` -............................................................................ +:ref:`Element Instances ` :math:`\{ \EITYPE~t, \EIELEM~\reff^\ast \}` +...................................................................................... * For each :ref:`reference ` :math:`\reff_i` in the elements :math:`\reff^n`: @@ -362,10 +362,14 @@ Module instances are classified by *module contexts*, which are regular :ref:`co * Let :math:`\reftype^\ast` be the concatenation of all :math:`\reftype_i` in order. +* Let :math:`m` be the length of :math:`\moduleinst.\MIFUNCS`. + * Let :math:`n` be the length of :math:`\moduleinst.\MIDATAS`. +* Let :math:`x^\ast` be the sequence of :ref:`function indices ` from :math:`0` to :math:`m-1`. + * Then the module instance is valid with :ref:`context ` - :math:`\{\CTYPES~\functype^\ast,` :math:`\CFUNCS~{\functype'}^\ast,` :math:`\CTABLES~\tabletype^\ast,` :math:`\CMEMS~\memtype^\ast,` :math:`\CGLOBALS~\globaltype^\ast,` :math:`\CELEMS~\reftype^\ast,` :math:`\CDATAS~{\ok}^n\}`. + :math:`\{\CTYPES~\functype^\ast,` :math:`\CFUNCS~{\functype'}^\ast,` :math:`\CTABLES~\tabletype^\ast,` :math:`\CMEMS~\memtype^\ast,` :math:`\CGLOBALS~\globaltype^\ast,` :math:`\CELEMS~\reftype^\ast,` :math:`\CDATAS~{\ok}^n,` :math:`\CREFS~x^\ast\}`. .. math:: ~\\[-1ex] @@ -407,7 +411,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co \CMEMS & \memtype^\ast, \\ \CGLOBALS & \globaltype^\ast, \\ \CELEMS & \reftype^\ast, \\ - \CDATAS & {\ok}^n ~\} + \CDATAS & {\ok}^n, \\ + \CREFS & 0 \dots (|\funcaddr^\ast|-1) ~\} \end{array} \end{array} } @@ -665,9 +670,9 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S' * 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. -* For each :ref:`element instance ` :math:`\eleminst_i` in the original :math:`S.\SELEMS`, the new global instance must be an :ref:`extension ` of the old. +* For each :ref:`element instance ` :math:`\eleminst_i` in the original :math:`S.\SELEMS`, the new element instance must be an :ref:`extension ` of the old. -* For each :ref:`data instance ` :math:`\datainst_i` in the original :math:`S.\SDATAS`, the new global instance must be an :ref:`extension ` of the old. +* For each :ref:`data instance ` :math:`\datainst_i` in the original :math:`S.\SDATAS`, the new data instance must be an :ref:`extension ` of the old. .. math:: \frac{ diff --git a/document/core/binary/conventions.rst b/document/core/binary/conventions.rst index 83c80399..7b606e1e 100644 --- a/document/core/binary/conventions.rst +++ b/document/core/binary/conventions.rst @@ -54,6 +54,7 @@ In order to distinguish symbols of the binary syntax from symbols of the abstrac (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`. + A pattern may also be used instead of a variable, e.g., :math:`7{:}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`. diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index e9c72b61..95ae7689 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -60,7 +60,7 @@ 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. +* the actual *contents*, whose structure is dependent on the section id. Every section is optional; an omitted section is equivalent to the section being present with empty contents. @@ -102,6 +102,9 @@ Id Section 12 :ref:`data count section ` == =============================================== +.. note:: + Section ids do not always correspond to the :ref:`order of sections ` in the encoding of a module. + .. index:: ! custom section pair: binary format; custom section diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 4f040d0e..b03b600b 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -20,15 +20,15 @@ The mapping of numeric instructions to their underlying operators is expressed b .. math:: \begin{array}{lll@{\qquad}l} - \X{op}_{\K{i}N}(n_1,\dots,n_k) &=& \F{i}\X{op}_N(n_1,\dots,n_k) \\ - \X{op}_{\K{f}N}(z_1,\dots,z_k) &=& \F{f}\X{op}_N(z_1,\dots,z_k) \\ + \X{op}_{\IN}(i_1,\dots,i_k) &=& \xref{exec/numerics}{int-ops}{\F{i}\X{op}}_N(i_1,\dots,i_k) \\ + \X{op}_{\FN}(z_1,\dots,z_k) &=& \xref{exec/numerics}{float-ops}{\F{f}\X{op}}_N(z_1,\dots,z_k) \\ \end{array} And for :ref:`conversion operators `: .. math:: \begin{array}{lll@{\qquad}l} - \X{cvtop}^{\sx^?}_{t_1,t_2}(c) &=& \X{cvtop}^{\sx^?}_{|t_1|,|t_2|}(c) \\ + \cvtop^{\sx^?}_{t_1,t_2}(c) &=& \xref{exec/numerics}{convert-ops}{\X{cvtop}}^{\sx^?}_{|t_1|,|t_2|}(c) \\ \end{array} Where the underlying operators are partial, the corresponding instruction will :ref:`trap ` when the result is not defined. @@ -63,9 +63,9 @@ Where the underlying operators are non-deterministic, because they may return on 2. Pop the value :math:`t.\CONST~c_1` from the stack. -3. If :math:`\unop_t(c_1)` is defined, then: +3. If :math:`\unopF_t(c_1)` is defined, then: - a. Let :math:`c` be a possible result of computing :math:`\unop_t(c_1)`. + a. Let :math:`c` be a possible result of computing :math:`\unopF_t(c_1)`. b. Push the value :math:`t.\CONST~c` to the stack. @@ -76,9 +76,9 @@ Where the underlying operators are non-deterministic, because they may return on .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~t\K{.}\unop &\stepto& (t\K{.}\CONST~c) - & (\iff c \in \unop_t(c_1)) \\ + & (\iff c \in \unopF_t(c_1)) \\ (t\K{.}\CONST~c_1)~t\K{.}\unop &\stepto& \TRAP - & (\iff \unop_{t}(c_1) = \{\}) + & (\iff \unopF_{t}(c_1) = \{\}) \end{array} @@ -93,9 +93,9 @@ Where the underlying operators are non-deterministic, because they may return on 3. Pop the value :math:`t.\CONST~c_1` from the stack. -4. If :math:`\binop_t(c_1, c_2)` is defined, then: +4. If :math:`\binopF_t(c_1, c_2)` is defined, then: - a. Let :math:`c` be a possible result of computing :math:`\binop_t(c_1, c_2)`. + a. Let :math:`c` be a possible result of computing :math:`\binopF_t(c_1, c_2)`. b. Push the value :math:`t.\CONST~c` to the stack. @@ -106,9 +106,9 @@ Where the underlying operators are non-deterministic, because they may return on .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\binop &\stepto& (t\K{.}\CONST~c) - & (\iff c \in \binop_t(c_1,c_2)) \\ + & (\iff c \in \binopF_t(c_1,c_2)) \\ (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\binop &\stepto& \TRAP - & (\iff \binop_{t}(c_1,c_2) = \{\}) + & (\iff \binopF_{t}(c_1,c_2) = \{\}) \end{array} @@ -121,14 +121,14 @@ Where the underlying operators are non-deterministic, because they may return on 2. Pop the value :math:`t.\CONST~c_1` from the stack. -3. Let :math:`c` be the result of computing :math:`\testop_t(c_1)`. +3. Let :math:`c` be the result of computing :math:`\testopF_t(c_1)`. 4. Push the value :math:`\I32.\CONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~t\K{.}\testop &\stepto& (\I32\K{.}\CONST~c) - & (\iff c = \testop_t(c_1)) \\ + & (\iff c = \testopF_t(c_1)) \\ \end{array} @@ -143,14 +143,14 @@ Where the underlying operators are non-deterministic, because they may return on 3. Pop the value :math:`t.\CONST~c_1` from the stack. -4. Let :math:`c` be the result of computing :math:`\relop_t(c_1, c_2)`. +4. Let :math:`c` be the result of computing :math:`\relopF_t(c_1, c_2)`. 5. Push the value :math:`\I32.\CONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\relop &\stepto& (\I32\K{.}\CONST~c) - & (\iff c = \relop_t(c_1,c_2)) \\ + & (\iff c = \relopF_t(c_1,c_2)) \\ \end{array} @@ -255,20 +255,27 @@ Reference Instructions Vector Instructions ~~~~~~~~~~~~~~~~~~~ -Most vector instructions are defined in terms of generic numeric operators applied lane-wise based on the :ref:`shape `. +Vector instructions that operate bitwise are handled as integer operations of respective width. .. math:: \begin{array}{lll@{\qquad}l} + \X{op}_{\VN}(i_1,\dots,i_k) &=& \xref{exec/numerics}{int-ops}{\F{i}\X{op}}_N(i_1,\dots,i_k) \\ + \end{array} + +Most other vector instructions are defined in terms of numeric operators that are applied lane-wise according to the given :ref:`shape `. + +.. math:: + \begin{array}{llll} \X{op}_{t\K{x}N}(n_1,\dots,n_k) &=& - \lanes^{-1}_{t\K{x}N}(op_t(\lanes_{t\K{x}N}(n_1) ~\dots~ \lanes_{t\K{x}N}(n_k)) + \lanes^{-1}_{t\K{x}N}(\xref{exec/instructions}{exec-instr-numeric}{\X{op}}_t(i_1,\dots,i_k)^\ast) & \qquad(\iff i_1^\ast = \lanes_{t\K{x}N}(n_1) \land \dots \land i_k^\ast = \lanes_{t\K{x}N}(n_k) \\ \end{array} .. note:: - For example, the result of instruction :math:`\K{i32x4}.\ADD` applied to operands :math:`i_1, i_2` - invokes :math:`\ADD_{\K{i32x4}}(i_1, i_2)`, which maps to - :math:`\lanes^{-1}_{\K{i32x4}}(\ADD_{\I32}(i_1^+, i_2^+))`, - where :math:`i_1^+` and :math:`i_2^+` are sequences resulting from invoking - :math:`\lanes_{\K{i32x4}}(i_1)` and :math:`\lanes_{\K{i32x4}}(i_2)` + For example, the result of instruction :math:`\K{i32x4}.\ADD` applied to operands :math:`v_1, v_2` + invokes :math:`\ADD_{\K{i32x4}}(v_1, v_2)`, which maps to + :math:`\lanes^{-1}_{\K{i32x4}}(\ADD_{\I32}(i_1, i_2)^\ast)`, + where :math:`i_1^\ast` and :math:`i_2^\ast` are sequences resulting from invoking + :math:`\lanes_{\K{i32x4}}(v_1)` and :math:`\lanes_{\K{i32x4}}(v_2)` respectively. @@ -292,14 +299,14 @@ Most vector instructions are defined in terms of generic numeric operators appli 2. Pop the value :math:`\V128.\VCONST~c_1` from the stack. -3. Let :math:`c` be the result of computing :math:`\vvunop_{\I128}(c_1)`. +3. Let :math:`c` be the result of computing :math:`\vvunop_{\V128}(c_1)`. 4. Push the value :math:`\V128.\VCONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (\V128\K{.}\VCONST~c_1)~\V128\K{.}\vvunop &\stepto& (\V128\K{.}\VCONST~c) - & (\iff c = \vvunop_{\I128}(c_1)) \\ + & (\iff c = \vvunop_{\V128}(c_1)) \\ \end{array} @@ -314,14 +321,14 @@ Most vector instructions are defined in terms of generic numeric operators appli 3. Pop the value :math:`\V128.\VCONST~c_1` from the stack. -4. Let :math:`c` be the result of computing :math:`\vvbinop_{\I128}(c_1, c_2)`. +4. Let :math:`c` be the result of computing :math:`\vvbinop_{\V128}(c_1, c_2)`. 5. Push the value :math:`\V128.\VCONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~\V128\K{.}\vvbinop &\stepto& (\V128\K{.}\VCONST~c) - & (\iff c = \vvbinop_{\I128}(c_1, c_2)) \\ + & (\iff c = \vvbinop_{\V128}(c_1, c_2)) \\ \end{array} @@ -338,14 +345,14 @@ Most vector instructions are defined in terms of generic numeric operators appli 4. Pop the value :math:`\V128.\VCONST~c_1` from the stack. -5. Let :math:`c` be the result of computing :math:`\vvternop_{\I128}(c_1, c_2, c_3)`. +5. Let :math:`c` be the result of computing :math:`\vvternop_{\V128}(c_1, c_2, c_3)`. 6. Push the value :math:`\V128.\VCONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (\V128\K{.}\VCONST~c_1)~(\V128\K{.}\VCONST~c_2)~(\V128\K{.}\VCONST~c_3)~\V128\K{.}\vvternop &\stepto& (\V128\K{.}\VCONST~c) - & (\iff c = \vvternop_{\I128}(c_1, c_2, c_3)) \\ + & (\iff c = \vvternop_{\V128}(c_1, c_2, c_3)) \\ \end{array} @@ -379,15 +386,15 @@ Most vector instructions are defined in terms of generic numeric operators appli 2. Pop the value :math:`\V128.\VCONST~c_2` from the stack. -3. Let :math:`i^\ast` be the result of computing :math:`\lanes_{i8x16}(c_2)`. +3. Let :math:`i^\ast` be the result of computing :math:`\lanes_{\I8X16}(c_2)`. 4. Pop the value :math:`\V128.\VCONST~c_1` from the stack. -5. Let :math:`j^\ast` be the result of computing :math:`\lanes_{i8x16}(c_1)`. +5. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\I8X16}(c_1)`. 6. Let :math:`c^\ast` be the concatenation of the two sequences :math:`j^\ast` and :math:`0^{240}`. -7. Let :math:`c'` be the result of computing :math:`\lanes^{-1}_{i8x16}(c^\ast[ i^\ast[0] ] \dots c^\ast[ i^\ast[15] ])`. +7. Let :math:`c'` be the result of computing :math:`\lanes^{-1}_{\I8X16}(c^\ast[ i^\ast[0] ] \dots c^\ast[ i^\ast[15] ])`. 8. Push the value :math:`\V128.\VCONST~c'` onto the stack. @@ -398,9 +405,9 @@ Most vector instructions are defined in terms of generic numeric operators appli \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & i^\ast = \lanes_{i8x16}(c_2) \\ - \wedge & c^\ast = \lanes_{i8x16}(c_1)~0^{240} \\ - \wedge & c' = \lanes^{-1}_{i8x16}(c^\ast[ i^\ast[0] ] \dots c^\ast[ i^\ast[15] ])) + (\iff & i^\ast = \lanes_{\I8X16}(c_2) \\ + \wedge & c^\ast = \lanes_{\I8X16}(c_1)~0^{240} \\ + \wedge & c' = \lanes^{-1}_{\I8X16}(c^\ast[ i^\ast[0] ] \dots c^\ast[ i^\ast[15] ])) \end{array} \end{array} @@ -416,15 +423,15 @@ Most vector instructions are defined in terms of generic numeric operators appli 3. Pop the value :math:`\V128.\VCONST~c_2` from the stack. -4. Let :math:`i_2^\ast` be the result of computing :math:`\lanes_{i8x16}(c_2)`. +4. Let :math:`i_2^\ast` be the result of computing :math:`\lanes_{\I8X16}(c_2)`. 5. Pop the value :math:`\V128.\VCONST~c_1` from the stack. -6. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{i8x16}(c_1)`. +6. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\I8X16}(c_1)`. 7. Let :math:`i^\ast` be the concatenation of the two sequences :math:`i_1^\ast` and :math:`i_2^\ast`. -8. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{i8x16}(i^\ast[x^\ast[0]] \dots i^\ast[x^\ast[15]])`. +8. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\I8X16}(i^\ast[x^\ast[0]] \dots i^\ast[x^\ast[15]])`. 9. Push the value :math:`\V128.\VCONST~c` onto the stack. @@ -435,8 +442,8 @@ Most vector instructions are defined in terms of generic numeric operators appli \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & i^\ast = \lanes_{i8x16}(c_1)~\lanes_{i8x16}(c_2) \\ - \wedge & c = \lanes^{-1}_{i8x16}(i^\ast[x^\ast[0]] \dots i^\ast[x^\ast[15]])) + (\iff & i^\ast = \lanes_{\I8X16}(c_1)~\lanes_{\I8X16}(c_2) \\ + \wedge & c = \lanes^{-1}_{\I8X16}(i^\ast[x^\ast[0]] \dots i^\ast[x^\ast[15]])) \end{array} \end{array} @@ -506,31 +513,31 @@ Most vector instructions are defined in terms of generic numeric operators appli 1. Assert: due to :ref:`validation `, :math:`x < \dim(\shape)`. -2. Let :math:`t_1` be the type :math:`\unpacked(\shape)`. +2. Let :math:`t_2` be the type :math:`\unpacked(\shape)`. 3. Assert: due to :ref:`validation `, a value of :ref:`value type ` :math:`t_1` is on the top of the stack. -4. Pop the value :math:`t_1.\CONST~c_1` from the stack. +4. Pop the value :math:`t_2.\CONST~c_2` from the stack. 5. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. -6. Pop the value :math:`\V128.\VCONST~c_2` from the stack. +6. Pop the value :math:`\V128.\VCONST~c_1` from the stack. -7. Let :math:`i^\ast` be the result of computing :math:`\lanes_{\shape}(c_2)`. +7. Let :math:`i^\ast` be the result of computing :math:`\lanes_{\shape}(c_1)`. -8. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\shape}(i^\ast \with [x] = c_1)`. +8. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\shape}(i^\ast \with [x] = c_2)`. 9. Push :math:`\V128.\VCONST~c` on the stack. .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - (t_1\K{.}\CONST~c_1)~(\V128\K{.}\VCONST~c_2)~(\shape\K{.}\REPLACELANE~x) &\stepto& (\V128\K{.}\VCONST~c) + (\V128\K{.}\VCONST~c_1)~(t_2\K{.}\CONST~c_2)~(\shape\K{.}\REPLACELANE~x) &\stepto& (\V128\K{.}\VCONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & i^\ast = \lanes_{\shape}(c_2) \\ - \wedge & c = \lanes^{-1}_{\shape}(i^\ast \with [x] = c_1)) + (\iff & i^\ast = \lanes_{\shape}(c_1) \\ + \wedge & c = \lanes^{-1}_{\shape}(i^\ast \with [x] = c_2)) \end{array} \end{array} @@ -550,7 +557,7 @@ Most vector instructions are defined in terms of generic numeric operators appli .. math:: \begin{array}{lcl@{\qquad}l} - (\V128\K{.}\VCONST~c_1)~\V128\K{.}\vunop &\stepto& (\V128\K{.}\VCONST~c) + (\V128\K{.}\VCONST~c_1)~\shape\K{.}\vunop &\stepto& (\V128\K{.}\VCONST~c) & (\iff c = \vunop_{\shape}(c_1)) \end{array} @@ -662,9 +669,9 @@ Most vector instructions are defined in terms of generic numeric operators appli 1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. -2. Pop the value :math:`\V128.\VCONST~c_1` from the stack. +2. Pop the value :math:`\V128.\VCONST~c` from the stack. -3. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\shape}(c_1)`. +3. Let :math:`i_1^\ast` be the result of computing :math:`\lanes_{\shape}(c)`. 4. Let :math:`i` be the result of computing :math:`\bool(\bigwedge(i_1 \neq 0)^\ast)`. @@ -674,7 +681,7 @@ Most vector instructions are defined in terms of generic numeric operators appli .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - (\V128\K{.}\VCONST~c_1)~\shape\K{.}\ALLTRUE &\stepto& (\I32\K{.}\CONST~i) + (\V128\K{.}\VCONST~c)~\shape\K{.}\ALLTRUE &\stepto& (\I32\K{.}\CONST~i) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -691,7 +698,7 @@ Most vector instructions are defined in terms of generic numeric operators appli 1. Assert: due to :ref:`validation `, a value of :ref:`value type ` |V128| is on the top of the stack. -2. Pop the value :math:`\V128.\VCONST~c_1` from the stack. +2. Pop the value :math:`\V128.\VCONST~c` from the stack. 3. Let :math:`i_1^N` be the result of computing :math:`\lanes_{t\K{x}N}(c)`. @@ -701,14 +708,14 @@ Most vector instructions are defined in terms of generic numeric operators appli 6. Let :math:`j^\ast` be the concatenation of the two sequences :math:`i_2^N` and :math:`0^{32-N}`. -7. Let :math:`c` be the result of computing :math:`\ibits_{32}^{-1}(j^\ast)`. +7. Let :math:`i` be the result of computing :math:`\ibits_{32}^{-1}(j^\ast)`. -8. Push the value :math:`\I32.\CONST~c` onto the stack. +8. Push the value :math:`\I32.\CONST~i` onto the stack. .. math:: \begin{array}{lcl@{\qquad}l} - (\V128\K{.}\VCONST~c_1)~t\K{x}N\K{.}\BITMASK &\stepto& (\I32\K{.}\CONST~c) - & (\iff c = \ibits_{32}^{-1}(\ilts_{|t|}(\lanes_{t\K{x}N}(c), 0^N))) + (\V128\K{.}\VCONST~c)~t\K{x}N\K{.}\BITMASK &\stepto& (\I32\K{.}\CONST~i) + & (\iff i = \ibits_{32}^{-1}(\ilts_{|t|}(\lanes_{t\K{x}N}(c), 0^N))) \\ \end{array} @@ -830,8 +837,8 @@ where: \end{array} -:math:`t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx\K{\_zero}` -............................................................... +:math:`t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx^?\K{\_zero}` +................................................................. 1. Assert: due to :ref:`syntax `, :math:`N = 2 \cdot M`. @@ -841,7 +848,7 @@ where: 4. Let :math:`i^\ast` be the result of computing :math:`\lanes_{t_1\K{x}M}(c_1)`. -5. Let :math:`j^\ast` be the result of computing :math:`\vcvtop^{\sx}_{|t_1|,|t_2|}(i^\ast)`. +5. Let :math:`j^\ast` be the result of computing :math:`\vcvtop^{\sx^?}_{|t_1|,|t_2|}(i^\ast)`. 6. Let :math:`k^\ast` be the concatenation of the two sequences :math:`j^\ast` and :math:`0^M`. @@ -852,11 +859,11 @@ where: .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - (\V128\K{.}\VCONST~c_1)~t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx\K{\_zero} &\stepto& (\V128\K{.}\VCONST~c) \\ + (\V128\K{.}\VCONST~c_1)~t_2\K{x}N\K{.}\vcvtop\K{\_}t_1\K{x}M\K{\_}\sx^?\K{\_zero} &\stepto& (\V128\K{.}\VCONST~c) \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))~0^M)) + (\iff & c = \lanes^{-1}_{t_2\K{x}N}(\vcvtop^{\sx^?}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1))~0^M)) \end{array} \end{array} @@ -935,7 +942,7 @@ where: 10. Let :math:`k_2^\ast` be the result of computing :math:`\extend^{\sx}_{|t_1|,|t_2|}(j_2^\ast)`. -11. Let :math:`k^\ast` be the result of computing :math:`\imul_{t_2\K{x}N}(k_1^\ast, k_2^\ast)`. +11. Let :math:`k^\ast` be the result of computing :math:`\imul_{|t_2|}(k_1^\ast, k_2^\ast)`. 12. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{t_2\K{x}N}(k^\ast)`. @@ -949,7 +956,7 @@ where: \begin{array}[t]{@{}r@{~}l@{}} (\iff & i^\ast = \lanes_{t_1\K{x}M}(c_1)[\half(0, N) \slice N] \\ \wedge & j^\ast = \lanes_{t_1\K{x}M}(c_2)[\half(0, N) \slice N] \\ - \wedge & c = \lanes^{-1}_{t_2\K{x}N}(\imul_{t_2\K{x}N}(\extend^{\sx}_{|t_1|,|t_2|}(i^\ast), \extend^{\sx}_{|t_1|,|t_2|}(j^\ast)))) + \wedge & c = \lanes^{-1}_{t_2\K{x}N}(\imul_{|t_2|}(\extend^{\sx}_{|t_1|,|t_2|}(i^\ast), \extend^{\sx}_{|t_1|,|t_2|}(j^\ast)))) \end{array} where: @@ -976,7 +983,7 @@ where: 5. Let :math:`(j_1~j_2)^\ast` be the result of computing :math:`\extend^{\sx}_{|t_1|,|t_2|}(i^\ast)`. -6. Let :math:`k^\ast` be the result of computing :math:`\iadd_{N}(j_1, j_2)^\ast`. +6. Let :math:`k^\ast` be the result of computing :math:`\iadd_{|t_2|}(j_1, j_2)^\ast`. 7. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{t_2\K{x}N}(k^\ast)`. @@ -990,7 +997,7 @@ where: \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & (i_1~i_2)^\ast = \extend^{\sx}_{|t_1|,|t_2|}(\lanes_{t_1\K{x}M}(c_1)) \\ - \wedge & j^\ast = \iadd_{N}(i_1, i_2)^\ast \\ + \wedge & j^\ast = \iadd_{|t_2|}(i_1, i_2)^\ast \\ \wedge & c = \lanes^{-1}_{t_2\K{x}N}(j^\ast)) \end{array} \end{array} @@ -1681,7 +1688,7 @@ Table Instructions 4. Assert: due to :ref:`validation `, :math:`S.\SELEMS[a]` exists. -5. Replace :math:`S.\SELEMS[a]` with the :ref:`element instance ` :math:`\{\EIELEM~\epsilon\}`. +5. Replace :math:`S.\SELEMS[a].\EIELEM` with :math:`\epsilon`. .. math:: ~\\[-1ex] @@ -1690,7 +1697,7 @@ Table Instructions S; F; (\ELEMDROP~x) &\stepto& S'; F; \epsilon \end{array} \\ \qquad - (\iff S' = S \with \SELEMS[F.\AMODULE.\MIELEMS[x]] = \{ \EIELEM~\epsilon \}) \\ + (\iff S' = S \with \SELEMS[F.\AMODULE.\MIELEMS[x]].\EIELEM = \epsilon) \\ \end{array} @@ -1820,7 +1827,7 @@ Memory Instructions 13. Let :math:`n_k` be the result of computing :math:`\extend^{\sx}_{M,W}(m_k)`. -14. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\X{i}W\K{x}N}(n_0 \dots n_{N-1})`. +14. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\K{i}W\K{x}N}(n_0 \dots n_{N-1})`. 15. Push the value :math:`\V128.\CONST~c` to the stack. @@ -1837,7 +1844,7 @@ Memory Instructions \wedge & \X{ea} + M \cdot N / 8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ \wedge & \bytes_{\iM}(m_k) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} + k \cdot M/8 \slice M/8] \\ \wedge & W = M \cdot 2 \\ - \wedge & c = \lanes^{-1}_{\X{i}W\K{x}N}(\extend^{\sx}_{M,W}(m_0) \dots \extend^{\sx}_{M,W}(m_{N-1}))) + \wedge & c = \lanes^{-1}_{\K{i}W\K{x}N}(\extend^{\sx}_{M,W}(m_0) \dots \extend^{\sx}_{M,W}(m_{N-1}))) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -1879,7 +1886,7 @@ Memory Instructions 12. Let :math:`L` be the integer :math:`128 / N`. -13. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\iN\K{x}L}(n^L)`. +13. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(n^L)`. 14. Push the value :math:`\V128.\CONST~c` to the stack. @@ -1894,7 +1901,7 @@ Memory Instructions (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + N/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ \wedge & \bytes_{\iN}(n) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] \\ - \wedge & c = \lanes^{-1}_{\iN\K{x}L}(n^L)) + \wedge & c = \lanes^{-1}_{\IN\K{x}L}(n^L)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -1995,9 +2002,9 @@ Memory Instructions 14. Let :math:`L` be :math:`128 / N`. -15. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\K{i}N\K{x}L}(v)`. +15. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(v)`. -16. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\K{i}N\K{x}L}(j^\ast \with [x] = r)`. +16. Let :math:`c` be the result of computing :math:`\lanes^{-1}_{\IN\K{x}L}(j^\ast \with [x] = r)`. 17. Push the value :math:`\V128.\CONST~c` to the stack. @@ -2013,7 +2020,7 @@ Memory Instructions \wedge & \X{ea} + N/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ \wedge & \bytes_{\iN}(r) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] \\ \wedge & L = 128/N \\ - \wedge & c = \lanes^{-1}_{\K{i}N\K{x}L}(\lanes_{\K{i}N\K{x}L}(v) \with [x] = r)) + \wedge & c = \lanes^{-1}_{\IN\K{x}L}(\lanes_{\IN\K{x}L}(v) \with [x] = r)) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -2132,7 +2139,7 @@ Memory Instructions 12. Let :math:`L` be :math:`128/N`. -13. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\K{i}N\K{x}L}(c)`. +13. Let :math:`j^\ast` be the result of computing :math:`\lanes_{\IN\K{x}L}(c)`. 14. Let :math:`b^\ast` be the result of computing :math:`\bytes_{\iN}(j^\ast[x])`. @@ -2149,7 +2156,7 @@ Memory Instructions (\iff & \X{ea} = i + \memarg.\OFFSET \\ \wedge & \X{ea} + N \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\ \wedge & L = 128/N \\ - \wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] = \bytes_{\iN}(\lanes_{\K{i}N\K{x}L}(c)[x])) + \wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] = \bytes_{\iN}(\lanes_{\IN\K{x}L}(c)[x])) \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index ad485c36..cdb20d03 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -798,6 +798,10 @@ Once the function has returned, the following steps are executed: 2. Pop :math:`\val_{\F{res}}^m` from the stack. +3. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. + +4. Pop the frame :math:`F` from the stack. + The values :math:`\val_{\F{res}}^m` are returned as the results of the invocation. .. math:: diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index 71dfef6a..b76190f6 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -104,18 +104,19 @@ Conventions: -.. index:: bit, integer, floating-point +.. index:: bit, integer, floating-point, numeric vector .. _aux-bits: Representations ~~~~~~~~~~~~~~~ -Numbers have an underlying binary representation as a sequence of bits: +Numbers and numeric vectors have an underlying binary representation as a sequence of bits: .. math:: \begin{array}{lll@{\qquad}l} - \bits_{\K{i}N}(i) &=& \ibits_N(i) \\ - \bits_{\K{f}N}(z) &=& \fbits_N(z) \\ + \bits_{\IN}(i) &=& \ibits_N(i) \\ + \bits_{\FN}(z) &=& \fbits_N(z) \\ + \bits_{\VN}(i) &=& \ibits_N(i) \\ \end{array} Each of these functions is a bijection, hence they are invertible. @@ -161,48 +162,51 @@ Floating-Point where :math:`M = \significand(N)` and :math:`E = \exponent(N)`. -.. index:: byte, little endian, memory -.. _aux-littleendian: -.. _aux-bytes: +.. index:: numeric vector, shape, lane +.. _aux-lanes: +.. _syntax-i128: -Storage +Vectors ....... -When a number is stored into :ref:`memory `, it is converted into a sequence of :ref:`bytes ` in |LittleEndian|_ byte order: +Numeric vectors of type |VN| have the same underlying representation as an |IN|. +They can also be interpreted as a sequence of numeric values packed into a |VN| with a particular |shape| :math:`t\K{x}M`, +provided that :math:`N = |t|\cdot M`. .. math:: + \begin{array}{l} \begin{array}{lll@{\qquad}l} - \bytes_t(i) &=& \littleendian(\bits_t(i)) \\[1ex] - \littleendian(\epsilon) &=& \epsilon \\ - \littleendian(d^8~{d'}^\ast~) &=& \littleendian({d'}^\ast)~\ibits_8^{-1}(d^8) \\ + \lanes_{t\K{x}M}(c) &=& + c_0~\dots~c_{M-1} \\ + \end{array} + \\ \qquad + \begin{array}[t]{@{}r@{~}l@{}l@{~}l@{~}l} + (\where & w &=& |t| / 8 \\ + \wedge & b^\ast &=& \bytes_{\IN}(c) \\ + \wedge & c_i &=& \bytes_{t}^{-1}(b^\ast[i \cdot w \slice w])) + \end{array} \end{array} -Again these functions are invertible bijections. +This function is a bijection on |IN|, hence it is invertible. -.. index:: numeric vectors, shape -.. _aux-lanes: +.. index:: byte, little endian, memory +.. _aux-littleendian: +.. _aux-bytes: -Vectors +Storage ....... -Numeric vectors have the same underlying representation as an |i128|. They can also be interpreted as a sequence of numeric values packed into a |V128| with a particular |shape|. +When a number is stored into :ref:`memory `, it is converted into a sequence of :ref:`bytes ` in |LittleEndian|_ byte order: .. math:: - \begin{array}{l} \begin{array}{lll@{\qquad}l} - \lanes_{t\K{x}N}(c) &=& - c_0~\dots~c_{N-1} \\ - \end{array} - \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - (\where & B = |t| / 8 \\ - \wedge & b^{16} = \bytes_{\i128}(c) \\ - \wedge & c_i = \bytes_{t}^{-1}(b^{16}[i \cdot B \slice B])) - \end{array} + \bytes_t(i) &=& \littleendian(\bits_t(i)) \\[1ex] + \littleendian(\epsilon) &=& \epsilon \\ + \littleendian(d^8~{d'}^\ast~) &=& \littleendian({d'}^\ast)~\ibits_8^{-1}(d^8) \\ \end{array} -These functions are bijections, so they are invertible. +Again these functions are invertible bijections. .. index:: integer @@ -712,11 +716,13 @@ The integer result of predicates -- i.e., :ref:`tests ` and :ref: :math:`\iextendMs_N(i)` ....................... -* Return :math:`\extends_{M,N}(i)`. +* Let :math:`j` be the result of computing :math:`\wrap_{N,M}(i)`. + +* Return :math:`\extends_{M,N}(j)`. .. math:: \begin{array}{lll@{\qquad}l} - \iextendMs_{N}(i) &=& \extends_{M,N}(i) \\ + \iextendMs_{N}(i) &=& \extends_{M,N}(\wrap_{N,M}(i)) \\ \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 6c53a4e9..c7a6b981 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -419,6 +419,7 @@ It filters out entries of a specific kind in an order-preserving fashion: pair: abstract syntax; frame pair: abstract syntax; label .. _syntax-frame: +.. _syntax-framestate: .. _syntax-label: .. _frame: .. _label: @@ -486,6 +487,8 @@ and a reference to the function's own :ref:`module instance ` .. math:: \begin{array}{llll} \production{frame} & \frame &::=& + \FRAME_n\{ \framestate \} \\ + \production{frame state} & \framestate &::=& \{ \ALOCALS~\val^\ast, \AMODULE~\moduleinst \} \\ \end{array} @@ -499,7 +502,7 @@ Conventions * The meta variable :math:`L` ranges over labels where clear from context. -* The meta variable :math:`F` ranges over frames where clear from context. +* The meta variable :math:`F` ranges over frame states where clear from context. * The following auxiliary definition takes a :ref:`block type ` and looks up the :ref:`function type ` that it denotes in the current frame: @@ -534,7 +537,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls ` and an executing *thread*. A thread is a computation over :ref:`instructions ` -that operates relative to a current :ref:`frame ` referring to the :ref:`module instance ` in which the computation runs, i.e., where the current function originates from. +that operates relative to the state of a current :ref:`frame ` referring to the :ref:`module instance ` in which the computation runs, i.e., where the current function originates from. .. math:: \begin{array}{llcl} \production{configuration} & \config &::=& \store; \thread \\ \production{thread} & \thread &::=& - \frame; \instr^\ast \\ + \framestate; \instr^\ast \\ \end{array} .. note:: diff --git a/document/core/index.bs b/document/core/index.bs index d27a9699..830c0595 100644 --- a/document/core/index.bs +++ b/document/core/index.bs @@ -3,14 +3,16 @@ Title: WebAssembly Core Specification Shortname: wasm-core Group: wasm Status: ED +Issue Tracking: GitHub https://github.com/WebAssembly/spec/issues Level: 2 TR: https://www.w3.org/TR/wasm-core-2/ ED: https://webassembly.github.io/spec/core/bikeshed/ -Editor: Andreas Rossberg (Dfinity Stiftung) +Editor: Andreas Rossberg, w3cid 82328 Repository: WebAssembly/spec Markup Shorthands: css no, markdown no, algorithm no, idl no Abstract: This document describes release 2.0 of the core WebAssembly standard, a safe, portable, low-level code format designed for efficient execution and compact representation. Prepare For TR: true +Date: now 
diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst
index 9c48736b..ddb51d7e 100644
--- a/document/core/syntax/instructions.rst
+++ b/document/core/syntax/instructions.rst
@@ -171,7 +171,7 @@ Occasionally, it is convenient to group operators together according to the foll
    \end{array}
 
 
-.. index:: ! vector instruction, numeric vectors, number, value, value type, SIMD
+.. index:: ! vector instruction, numeric vector, number, value, value type, SIMD
    pair: abstract syntax; instruction
 .. _syntax-laneidx:
 .. _syntax-shape:
@@ -707,7 +707,7 @@ the callee is dynamically checked against the :ref:`function type ` bodies, initialization values for :ref:`globals `, and offsets of :ref:`element ` or :ref:`data ` segments are given as expressions, which are sequences of :ref:`instructions ` terminated by an |END| marker.
+:ref:`Function ` bodies, initialization values for :ref:`globals `, elements and offsets of :ref:`element ` segments, and offsets of :ref:`data ` segments are given as expressions, which are sequences of :ref:`instructions ` terminated by an |END| marker.
 
 .. math::
    \begin{array}{llll}
diff --git a/document/core/syntax/values.rst b/document/core/syntax/values.rst
index 1b155df4..72ff7d3a 100644
--- a/document/core/syntax/values.rst
+++ b/document/core/syntax/values.rst
@@ -148,7 +148,7 @@ Conventions
 * The meta variable :math:`z` ranges over floating-point values where clear from context.
 
 
-.. index:: ! numeric vectors, integer, floating-point, lane, SIMD
+.. index:: ! numeric vector, integer, floating-point, lane, SIMD
    pair: abstract syntax; vector
 .. _syntax-vecnum:
 
diff --git a/document/core/text/conventions.rst b/document/core/text/conventions.rst
index c2ba92fc..493d7921 100644
--- a/document/core/text/conventions.rst
+++ b/document/core/text/conventions.rst
@@ -49,6 +49,7 @@ In order to distinguish symbols of the textual syntax from symbols of the abstra
   (This is a shorthand for :math:`T^n` where :math:`n \leq 1`.)
 
 * :math:`x{:}T` denotes the same language as the nonterminal :math:`T`, but also binds the variable :math:`x` to the attribute synthesized for :math:`T`.
+  A pattern may also be used instead of a variable, e.g., :math:`(x,y){:}T`.
 
 * Productions are written :math:`\T{sym} ::= T_1 \Rightarrow A_1 ~|~ \dots ~|~ T_n \Rightarrow A_n`, where each :math:`A_i` is the attribute that is synthesized for :math:`\T{sym}` in the given case, usually from attribute variables bound in :math:`T_i`.
 
diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst
index e491d691..c284326f 100644
--- a/document/core/text/instructions.rst
+++ b/document/core/text/instructions.rst
@@ -853,6 +853,10 @@ Vector constant instructions have a mandatory :ref:`shape ` de
      \text{f32x4.abs} &\Rightarrow& \F32X4.\VABS\\ &&|&
      \text{f32x4.neg} &\Rightarrow& \F32X4.\VNEG\\ &&|&
      \text{f32x4.sqrt} &\Rightarrow& \F32X4.\VSQRT\\ &&|&
+     \text{f32x4.ceil} &\Rightarrow& \F32X4.\VCEIL\\ &&|&
+     \text{f32x4.floor} &\Rightarrow& \F32X4.\VFLOOR\\ &&|&
+     \text{f32x4.trunc} &\Rightarrow& \F32X4.\VTRUNC\\ &&|&
+     \text{f32x4.nearest} &\Rightarrow& \F32X4.\VNEAREST\\ &&|&
      \text{f32x4.add} &\Rightarrow& \F32X4.\VADD\\ &&|&
      \text{f32x4.sub} &\Rightarrow& \F32X4.\VSUB\\ &&|&
      \text{f32x4.mul} &\Rightarrow& \F32X4.\VMUL\\ &&|&
@@ -869,6 +873,10 @@ Vector constant instructions have a mandatory :ref:`shape ` de
      \text{f64x2.abs} &\Rightarrow& \F64X2.\VABS\\ &&|&
      \text{f64x2.neg} &\Rightarrow& \F64X2.\VNEG\\ &&|&
      \text{f64x2.sqrt} &\Rightarrow& \F64X2.\VSQRT\\ &&|&
+     \text{f64x2.ceil} &\Rightarrow& \F64X2.\VCEIL\\ &&|&
+     \text{f64x2.floor} &\Rightarrow& \F64X2.\VFLOOR\\ &&|&
+     \text{f64x2.trunc} &\Rightarrow& \F64X2.\VTRUNC\\ &&|&
+     \text{f64x2.nearest} &\Rightarrow& \F64X2.\VNEAREST\\ &&|&
      \text{f64x2.add} &\Rightarrow& \F64X2.\VADD\\ &&|&
      \text{f64x2.sub} &\Rightarrow& \F64X2.\VSUB\\ &&|&
      \text{f64x2.mul} &\Rightarrow& \F64X2.\VMUL\\ &&|&
@@ -913,7 +921,7 @@ Such a folded instruction can appear anywhere a regular instruction can.
 
 .. math::
    \begin{array}{lllll}
-   \production{instruction} & 
+   \production{instruction} &
      \text{(}~\Tplaininstr~~\Tfoldedinstr^\ast~\text{)}
        &\equiv\quad \Tfoldedinstr^\ast~~\Tplaininstr \\ &
      \text{(}~\text{block}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast~\text{)}
diff --git a/document/core/text/lexical.rst b/document/core/text/lexical.rst
index af99974b..077dae17 100644
--- a/document/core/text/lexical.rst
+++ b/document/core/text/lexical.rst
@@ -85,7 +85,9 @@ The allowed formatting characters correspond to a subset of the |ASCII|_ *format
    \production{white space} & \Tspace &::=&
      (\text{~~} ~|~ \Tformat ~|~ \Tcomment)^\ast \\
    \production{format} & \Tformat &::=&
-     \unicode{09} ~|~ \unicode{0A} ~|~ \unicode{0D} \\
+     \Tnewline ~|~ \unicode{09} \\
+   \production{newline} & \Tnewline &::=&
+     \unicode{0A} ~|~ \unicode{0D} ~|~ \unicode{0D}~\unicode{0A} \\
    \end{array}
 
 The only relevance of white space is to separate :ref:`tokens `. It is otherwise ignored.
@@ -107,13 +109,13 @@ Block comments can be nested.
    \production{comment} & \Tcomment &::=&
      \Tlinecomment ~|~ \Tblockcomment \\
    \production{line comment} & \Tlinecomment &::=&
-     \Tcommentd~~\Tlinechar^\ast~~(\unicode{0A} ~|~ \T{eof}) \\
+     \Tcommentd~~\Tlinechar^\ast~~(\Tnewline ~|~ \T{eof}) \\
    \production{line character} & \Tlinechar &::=&
-     c{:}\Tchar & (\iff c \neq \unicode{0A}) \\
+     c{:}\Tchar & (\iff c \neq \unicode{0A} \land c \neq \unicode{0D}) \\
    \production{block comment} & \Tblockcomment &::=&
      \Tcommentl~~\Tblockchar^\ast~~\Tcommentr \\
    \production{block character} & \Tblockchar &::=&
-     c{:}\Tchar & (\iff c \neq \text{;} \wedge c \neq \text{(}) \\ &&|&
+     c{:}\Tchar & (\iff c \neq \text{;} \land c \neq \text{(}) \\ &&|&
      \text{;} & (\iff~\mbox{the next character is not}~\text{)}) \\ &&|&
      \text{(} & (\iff~\mbox{the next character is not}~\text{;}) \\ &&|&
      \Tblockcomment \\
diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst
index 0a5a3348..69d5f90a 100644
--- a/document/core/text/modules.rst
+++ b/document/core/text/modules.rst
@@ -292,7 +292,7 @@ An :ref:`element segment ` can be given inline with a table definitio
    \production{module field} &
      \text{(}~\text{table}~~\Tid^?~~\Treftype~~\text{(}~\text{elem}~~\expr^n{:}\Tvec(\Telemexpr)~\text{)}~\text{)} \quad\equiv \\ & \qquad
        \text{(}~\text{table}~~\Tid'~~n~~n~~\Treftype~\text{)} \\ & \qquad
-       \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Tvec(\Telemexpr)~\text{)}
+       \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\Telemexpr)~\text{)}
        \\ & \qquad\qquad
        (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh) \\
    \end{array}
@@ -302,7 +302,7 @@ An :ref:`element segment ` can be given inline with a table definitio
    \production{module field} &
      \text{(}~\text{table}~~\Tid^?~~\Treftype~~\text{(}~\text{elem}~~x^n{:}\Tvec(\Tfuncidx)~\text{)}~\text{)} \quad\equiv \\ & \qquad
        \text{(}~\text{table}~~\Tid'~~n~~n~~\Treftype~\text{)} \\ & \qquad
-       \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\Tvec(\Tfuncidx)~\text{)}
+       \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\text{i32.const}~~\text{0}~\text{)}~~\text{func}~~\Tvec(\Tfuncidx)~\text{)}
        \\ & \qquad\qquad
        (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh) \\
    \end{array}
diff --git a/document/core/util/bikeshed_fixup.py b/document/core/util/bikeshed_fixup.py
index 05439207..7041d875 100755
--- a/document/core/util/bikeshed_fixup.py
+++ b/document/core/util/bikeshed_fixup.py
@@ -3,6 +3,7 @@
 
 import os
 import sys
+import re
 
 
 SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__))
@@ -59,10 +60,32 @@ def Main():
   )
 
   data = data.replace(
-      """IEEE 754-2019""",
+      """IEEE 754""",
       "[[!IEEE-754-2019]]"
   )
 
+  # Fix this problem that causes an  element to be generated in the output
+  # as a child of another  element, and for which the HTML validator reports
+  # an error — which in turn causes the W3C pubrules checker to refuse to
+  # autopublish the resulting bikeshed output.
+  data = data.replace(
+      """\href{#binary-sint}{\href{#syntax-int}""",
+      """{\href{#syntax-int}""")
+
+  # Strip the entire  element from the the sphinx output — because it
+  # contains several ,