diff --git a/core/_download/WebAssembly.pdf b/core/_download/WebAssembly.pdf index 391fb57f89..b17100d523 100644 Binary files a/core/_download/WebAssembly.pdf and b/core/_download/WebAssembly.pdf differ diff --git a/core/appendix/index-instructions.html b/core/appendix/index-instructions.html index f650889cd9..b804053361 100644 --- a/core/appendix/index-instructions.html +++ b/core/appendix/index-instructions.html @@ -333,140 +333,140 @@

Quick search

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef316#1{\mathtt{0x#1}}\mathdef316{28}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef317#1{\mathtt{0x#1}}\mathdef317{29}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef318#1{\mathtt{0x#1}}\mathdef318{2A}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle32}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef319#1{\mathtt{0x#1}}\mathdef319{2B}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_s}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef320#1{\mathtt{0x#1}}\mathdef320{2C}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_u}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef321#1{\mathtt{0x#1}}\mathdef321{2D}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{16\_s}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef322#1{\mathtt{0x#1}}\mathdef322{2E}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{16\_u}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef323#1{\mathtt{0x#1}}\mathdef323{2F}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_s}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef324#1{\mathtt{0x#1}}\mathdef324{30}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_u}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef325#1{\mathtt{0x#1}}\mathdef325{31}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{16\_s}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef326#1{\mathtt{0x#1}}\mathdef326{32}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{16\_u}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef327#1{\mathtt{0x#1}}\mathdef327{33}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{32\_s}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef328#1{\mathtt{0x#1}}\mathdef328{34}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{32\_u}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef329#1{\mathtt{0x#1}}\mathdef329{35}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef330#1{\mathtt{0x#1}}\mathdef330{36}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef331#1{\mathtt{0x#1}}\mathdef331{37}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef332#1{\mathtt{0x#1}}\mathdef332{38}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef333#1{\mathtt{0x#1}}\mathdef333{39}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{f\scriptstyle64}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef334#1{\mathtt{0x#1}}\mathdef334{3A}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{16}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef335#1{\mathtt{0x#1}}\mathdef335{3B}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{8}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef336#1{\mathtt{0x#1}}\mathdef336{3C}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{16}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef337#1{\mathtt{0x#1}}\mathdef337{3D}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}\mathsf{32}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef338#1{\mathtt{0x#1}}\mathdef338{3E}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle64}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.size}}~x\)

\(\def\mathdef339#1{\mathtt{0x#1}}\mathdef339{3F}\)

@@ -1905,44 +1905,44 @@

Quick search

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef629#1{\mathtt{0x#1}}\mathdef629{FD}~~\def\mathdef630#1{\mathtt{0x#1}}\mathdef630{00}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8x8\_s}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef631#1{\mathtt{0x#1}}\mathdef631{FD}~~\def\mathdef632#1{\mathtt{0x#1}}\mathdef632{01}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8x8\_u}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef633#1{\mathtt{0x#1}}\mathdef633{FD}~~\def\mathdef634#1{\mathtt{0x#1}}\mathdef634{02}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{16x4\_s}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef635#1{\mathtt{0x#1}}\mathdef635{FD}~~\def\mathdef636#1{\mathtt{0x#1}}\mathdef636{03}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{16x4\_u}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef637#1{\mathtt{0x#1}}\mathdef637{FD}~~\def\mathdef638#1{\mathtt{0x#1}}\mathdef638{04}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{32x2\_s}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef639#1{\mathtt{0x#1}}\mathdef639{FD}~~\def\mathdef640#1{\mathtt{0x#1}}\mathdef640{05}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{32x2\_u}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef641#1{\mathtt{0x#1}}\mathdef641{FD}~~\def\mathdef642#1{\mathtt{0x#1}}\mathdef642{06}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}\mathsf{8\_splat}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef643#1{\mathtt{0x#1}}\mathdef643{FD}~~\def\mathdef644#1{\mathtt{0x#1}}\mathdef644{07}\)

@@ -1971,8 +1971,8 @@

Quick search

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

\(\def\mathdef651#1{\mathtt{0x#1}}\mathdef651{FD}~~\def\mathdef652#1{\mathtt{0x#1}}\mathdef652{0B}\)

\([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\)

-

validation

-

execution

+

validation

+

execution

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-vec}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i\scriptstyle\kern-0.1em128}}\)

\(\def\mathdef653#1{\mathtt{0x#1}}\mathdef653{FD}~~\def\mathdef654#1{\mathtt{0x#1}}\mathdef654{0C}\)

diff --git a/core/exec/instructions.html b/core/exec/instructions.html index 6f97e01566..0de638ba8b 100644 --- a/core/exec/instructions.html +++ b/core/exec/instructions.html @@ -3182,7 +3182,7 @@

\(t_2\mathsf{x}N\mathsf{.}\href{. However, it may be substantially slower on some hardware.

-

\({{\mathit{numty}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{{\href{../syntax/instructions.html#syntax-sz}{\mathit{sz}}}_{{\mathit{sx}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}}^?}}~x~{\mathit{ao}}\)

+

\({{\mathit{numty}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{{\href{../syntax/instructions.html#syntax-sz}{\mathit{sz}}}_{{\mathit{sx}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}}^?}}~x~{\mathit{ao}}\)

  1. Let \(z\) be the current state.

  2. Assert: Due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

    3. @@ -3243,11 +3243,11 @@

    \(t_2\mathsf{x}N\mathsf{.}\href{.

    1. Let \(F\) be the current frame.

      2. -

    2. Assert: due to validation, \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x]\) exists.

      3. +

    3. Assert: due to validation, \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x]\) exists.

    4. Let \(a\) be the memory address \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x]\).

      5. -

    5. Assert: due to validation, \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) exists.

      6. +

    6. Assert: due to validation, \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) exists.

    7. Let \(\mathit{mem}\) be the memory instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\).

      8. -

    8. Assert: due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

      9. +

    9. Assert: due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

    10. Pop the value \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\) from the stack.

    11. Let \(\mathit{ea}\) be the integer \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\).

    12. If \(N\) is not part of the instruction, then:

      @@ -3287,18 +3287,18 @@

      \(t_2\mathsf{x}N\mathsf{.}\href{. \end{array}\end{split}\]

-

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{M}\mathsf{x}N\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

+

\(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{M}\mathsf{x}N\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

Todo

(*) Rule and prose both not spliced.

  1. Let \(F\) be the current frame.

    2. -

  2. Assert: due to validation, \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x]\) exists.

    3. +

  3. Assert: due to validation, \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x]\) exists.

  4. Let \(a\) be the memory address \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x]\).

    5. -

  5. Assert: due to validation, \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) exists.

    6. +

  6. Assert: due to validation, \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) exists.

  7. Let \(\mathit{mem}\) be the memory instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\).

    8. -

  8. Assert: due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

    9. +

  9. Assert: due to validation, a value of value type \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}\) is on the top of the stack.

  10. Pop the value \(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i\) from the stack.

  11. Let \(\mathit{ea}\) be the integer \(i + \href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{offset}}\).

  12. If \(\mathit{ea} + M \cdot N /8\) is larger than the length of \(\mathit{mem}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\), then:

    @@ -3487,7 +3487,7 @@

    \(t_2\mathsf{x}N\mathsf{.}\href{. \end{array}\end{split}\]

-

\({{\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}}{{{\href{../syntax/instructions.html#syntax-sz}{\mathit{sz}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}}~x~{\mathit{ao}}\)

+

\({{\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}}{{{\href{../syntax/instructions.html#syntax-sz}{\mathit{sz}}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}}~x~{\mathit{ao}}\)

  1. Let \(z\) be the current state.

  2. Assert: Due to validation, a value of value type \({\mathit{numty}}_{\mathit{u{\kern-0.1em\scriptstyle 0}}}\) is on the top of the stack.

    3. @@ -3568,7 +3568,7 @@

    \(t_2\mathsf{x}N\mathsf{.}\href{.

  3. Let \(F\) be the current frame.

  4. Assert: due to validation, \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x]\) exists.

  5. Let \(a\) be the memory address \(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x]\).

    6. -

  6. Assert: due to validation, \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) exists.

    7. +

  7. Assert: due to validation, \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) exists.

  8. Let \(\mathit{mem}\) be the memory instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\).

  9. Assert: due to validation, a value of value type \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}\) is on the top of the stack.

  10. Pop the value \(\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\) from the stack.

    11. diff --git a/core/objects.inv b/core/objects.inv index 104abe0748..80f93323a3 100644 Binary files a/core/objects.inv and b/core/objects.inv differ diff --git a/core/valid/instructions.html b/core/valid/instructions.html index 4c428c8467..5272460a4c 100644 --- a/core/valid/instructions.html +++ b/core/valid/instructions.html @@ -1413,7 +1413,7 @@

    Quick search

    Memory Instructions

    -

    \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    +

    \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

    • The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than the bit width of \(t\) divided by \(8\).

      • @@ -1425,42 +1425,33 @@

      Quick search

      {\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {|{\mathit{nt}}|} / 8 - \qquad -({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq n / 8 < {|{\mathit{nt}}|} / 8)^? - \qquad -{n^?} = \epsilon \lor {\mathit{nt}} = {\mathsf{i}}{{\mathit{{\scriptstyle N}}}} }{ -{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {{\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{({n}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}})^?}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {\mathit{nt}} +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {\mathit{nt}} } \qquad \end{array}\] -
      -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq |t|/8 -}{ - C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.load}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t] -}\]
    -

    \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    +

    \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

    • The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8\).

    • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

    -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq N/8 +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {\mathit{{\scriptstyle M}}} / 8 }{ - C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.load}N\mathsf{\_}\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t] -}\]
    +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {{\mathsf{i}}{{\mathit{{\scriptstyle N}}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{{\mathit{{\scriptstyle M}}}}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow {\mathsf{i}}{{\mathit{{\scriptstyle N}}}} +} +\qquad +\end{array}\]
    -

    \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    +

    \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

    • The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than the bit width of \(t\) divided by \(8\).

      • @@ -1472,55 +1463,68 @@

      \(t\mathsf{.}\href{../syntax/inst {\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} \qquad {2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {|{\mathit{nt}}|} / 8 - \qquad -({2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq n / 8 < {|{\mathit{nt}}|} / 8)^? - \qquad -{n^?} = \epsilon \lor {\mathit{nt}} = {\mathsf{i}}{{\mathit{{\scriptstyle N}}}} }{ -{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {{\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}}{{n^?}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~{\mathit{nt}} \rightarrow \epsilon +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {\mathit{nt}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~{\mathit{nt}} \rightarrow \epsilon } \qquad \end{array}\] -
      -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq |t|/8 -}{ - C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.store}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [] -}\]

    -

    \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    +

    \(t\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

    • The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8\).

    • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

    -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq N/8 +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {\mathit{{\scriptstyle M}}} / 8 }{ - C \href{../valid/instructions.html#valid-instr}{\vdash} t\mathsf{.store}N~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [] -}\]
    +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {{\mathsf{i}}{{\mathit{{\scriptstyle N}}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}}{{\mathit{{\scriptstyle M}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~{\mathsf{i}}{{\mathit{{\scriptstyle N}}}} \rightarrow \epsilon +} +\qquad +\end{array}\] +
    +
    +

    \(\mathsf{v128.}\mathsf{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    +
      +

    • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

      • +

    • The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than the bit width of \(t\) divided by \(8\).

      • +

    • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t]\).

      • +
    +
    +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {|\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}|} / 8 +}{ +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} +} +\qquad +\end{array}\]
    -

    \(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    +

    \(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

    • The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than \(N/8 \cdot M\).

    • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

    -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq N/8 \cdot M +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {\mathit{{\scriptstyle M}}} / 8 \cdot {\mathit{{\scriptstyle N}}} }{ - C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{x}M\_\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] -}\]
    +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{{\mathit{{\scriptstyle M}}}}{\href{../syntax/instructions.html#syntax-shape}{\mathsf{x}}}{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} +} +\qquad +\end{array}\]

    \(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_splat}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    @@ -1530,13 +1534,16 @@

    \(t\mathsf{.}\href{../syntax/inst

  11. Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

    12. -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq N/8 +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {\mathit{{\scriptstyle N}}} / 8 }{ - C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_splat}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] -}\]
    +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{splat}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} +} +\qquad +\end{array}\]

    \(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_zero}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    @@ -1546,13 +1553,16 @@

    \(t\mathsf{.}\href{../syntax/inst

  12. Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

    13. -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} \leq N/8 +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} < {\mathit{{\scriptstyle N}}} / 8 }{ - C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_zero}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] -}\]
    +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{zero}}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} +} +\qquad +\end{array}\]

    \(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_lane}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)

    @@ -1563,15 +1573,37 @@

    \(t\mathsf{.}\href{../syntax/inst

  13. Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

    14. -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} < N/8 - \qquad - \href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} < 128/N +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} < {\mathit{{\scriptstyle N}}} / 8 + \qquad +i < 128 / {\mathit{{\scriptstyle N}}} +}{ +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}}{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{lane}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}~i : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} +} +\qquad +\end{array}\]
    +

    +
    +

    \(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}\)

    +
      +

    • The memory \(C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x]\) must be defined in the context.

      • +

    • The alignment \(2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}\) must not be larger than the bit width of \(t\) divided by \(8\).

      • +

    • Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~t] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} []\).

      • +
    +
    +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} \leq {|\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}|} / 8 }{ - C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{load}}{N}\mathsf{\_lane}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] -}\]
    +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}} : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \epsilon +} +\qquad +\end{array}\]

    \(\mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}\mathsf{\_lane}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}}\)

    @@ -1582,15 +1614,18 @@

    \(t\mathsf{.}\href{../syntax/inst

  14. Then the instruction is valid with type \([\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}]\).

    15. -\[\frac{ - C.\href{../valid/conventions.html#context}{\mathsf{mems}}[x] = \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} - \qquad - 2^{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}.\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}} < N/8 - \qquad - \href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} < 128/N +\[\begin{array}{@{}c@{}}\displaystyle +\frac{ +{\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{mems}}{}[x] = {\mathit{mt}} + \qquad +{2^{{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{align}}}} < {\mathit{{\scriptstyle N}}} / 8 + \qquad +i < 128 / {\mathit{{\scriptstyle N}}} }{ - C \href{../valid/instructions.html#valid-instr}{\vdash} \mathsf{v128.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}{N}\mathsf{\_lane}~x~\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}~\href{../syntax/instructions.html#syntax-laneidx}{\mathit{laneidx}} : [\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [] -}\]
    +{\mathit{{\scriptstyle C}}} \href{../valid/instructions.html#valid-instr}{\vdash} {\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}}{.}\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{store}}}{{\mathit{{\scriptstyle N}}}}{\mathsf{\_}}{\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{lane}}}~x~{\href{../syntax/instructions.html#syntax-memarg}{\mathit{memarg}}}~i : \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}~\href{../syntax/types.html#syntax-vectype}{\mathsf{v\scriptstyle128}} \rightarrow \epsilon +} +\qquad +\end{array}\]

    \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.size}}~x\)

    @@ -2038,7 +2073,7 @@

    \(t\mathsf{.}\href{../syntax/inst

    Note

    The \(\mathsf{return}\) instruction is stack-polymorphic.

    -

    \({\mathit{{\scriptstyle C}}}{.}\mathsf{return}\) is absent (set to \(\epsilon\)) when validating an expression that is not a function body. +

    \({\mathit{{\scriptstyle C}}}{.}\href{../valid/conventions.html#context}{\mathsf{return}}\) is absent (set to \(\epsilon\)) when validating an expression that is not a function body. This differs from it being set to the empty result type \((\epsilon)\), which is the case for functions not returning anything.

    diff --git a/js-api/index.html b/js-api/index.html index 81ff12f142..44b7e8b187 100644 --- a/js-api/index.html +++ b/js-api/index.html @@ -6,7 +6,7 @@ - +