### Define Start from Declarations

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Defines how to extract start function declarations.

```wast
def $startsd(decl*) : start*
  ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24
  def $startsd([]) = []
  ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52

```

--------------------------------

### Install Sphinx and Six

Source: https://github.com/webassembly/spec/blob/main/document/README.md

Installs the necessary Python packages for building Sphinx documentation.

```shell
pip install sphinx six
```

--------------------------------

### Start Option Syntax

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Defines the syntax for the start option in WebAssembly modules.

```spectec
;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec
syntax startopt = start*
```

--------------------------------

### Setup Function for Pre-Test Code

Source: https://github.com/webassembly/spec/blob/main/test/js-api/README.md

Encapsulate non-trivial code that runs before subtests using the 'setup' function. This ensures that any exceptions thrown are handled gracefully.

```javascript
setup(function)
```

--------------------------------

### Install TeX Live Full

Source: https://github.com/webassembly/spec/blob/main/document/README.md

Installs the complete TeX Live distribution, which is required for building the PDF version of the WebAssembly specification.

```shell
apt install texlive-full
```

--------------------------------

### WebAssembly Binary Format: Start Section Option Syntax

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Defines the syntax for the optional start section in WebAssembly modules.

```spectec
syntax startopt = start*
```

--------------------------------

### Install Sphinx

Source: https://github.com/webassembly/spec/blob/main/document/core/README.md

Installs the Sphinx documentation generator using pip. This is a prerequisite for building the documentation.

```shell
pip install sphinx
```

--------------------------------

### WebAssembly Start Section Syntax

Source: https://github.com/webassembly/spec/blob/main/spectec/test-latex/TEST.md

Defines the syntax for the start section in WebAssembly, which specifies the function to be executed when the module is instantiated.

```text
start ::= x:funcidx  => (start x)
```

```text
start section ::= start* : section_8(start)  => start*
```

--------------------------------

### Example Instruction Sequence

Source: https://github.com/webassembly/spec/blob/main/document/core/valid/instructions.md

This example demonstrates a sequence of instructions: pushing two i32 constants and then adding them. Subsumption is used to handle type compatibility between the constant instruction and the binary operation.

```wasm
(CONST I32 1) (CONST I32 2) (BINOP I32 ADD)
```

--------------------------------

### Start Function Definition

Source: https://github.com/webassembly/spec/blob/main/interpreter/README.md

Syntax for specifying the start function of a module.

```wast
start:   ( start <var> )
```

--------------------------------

### WebAssembly Start Section Grammar

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Defines the grammar for the start section, which optionally specifies a start function.

```wast
grammar Bstartsec : start?
  ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec
  prod{startopt : startopt} startopt:Bsection_(8, syntax start, grammar Bstart) => $opt_(syntax start, startopt)
```

--------------------------------

### WebAssembly Start Function Grammar

Source: https://github.com/webassembly/spec/blob/main/document/metadata/code/text/modules.md

Defines the syntax for specifying a start function within a module.

```webassembly
Tstart_
  = "start" Tfuncidx
```

--------------------------------

### Parse Start Section

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Parses the start section of a WebAssembly binary module.

```wast
grammar Bstart : start*
  ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec
  prod{x : idx} x:Bfuncidx => [START_start(x)]
```

```wast
grammar Bstartsec : start?
  ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec
  prod{startopt : startopt} startopt:Bsection_(8, syntax start, grammar Bstart) => $opt_(syntax start, startopt)
```

--------------------------------

### Constant Expression Example

Source: https://github.com/webassembly/spec/blob/main/document/metadata/code/valid/instructions.md

This example shows a valid constant expression. It includes instructions like CONST, BINOP, and REF.NULL, which are permitted within constant expressions.

```wasm
(CONST I32 1)
```

--------------------------------

### Install OCaml Dependencies

Source: https://github.com/webassembly/spec/blob/main/spectec/README.md

Installs necessary OCaml libraries including dune, menhir, mdx, and zarith using Opam.

```bash
$ opam install dune menhir mdx zarith
```

--------------------------------

### Loop Label Example

Source: https://github.com/webassembly/spec/blob/main/document/metadata/code/exec/runtime.md

An example of a loop label, which includes a placeholder for instructions and an arity. Branching to this label restarts the loop.

```text
[LABEL]() n 

```
`
```

{(LOOP bt $instrdots)}

```

--------------------------------

### Install Yarn and Build Bikeshed Core

Source: https://github.com/webassembly/spec/blob/main/document/README.md

Installs Yarn globally and then builds the Bikeshed version of the core WebAssembly specification. This is a prerequisite for generating the single-page HTML W3C version.

```shell
npm install -g yarn
cd document
make -C core bikeshed
```

--------------------------------

### Getting a Global Export

Source: https://github.com/webassembly/spec/blob/main/interpreter/README.md

Example of retrieving the value of a global export named 'my_global'.

```S-expression
(get "my_global")
```

--------------------------------

### Constant Expression with Global Get

Source: https://github.com/webassembly/spec/blob/main/document/metadata/code/valid/instructions.md

This example shows a constant expression that uses global.get. Note that in certain contexts (like modules), this instruction may have additional constraints regarding the globals it can refer to.

```wasm
(GLOBAL.GET 0)
```

--------------------------------

### Run the Test Suite

Source: https://github.com/webassembly/spec/blob/main/interpreter/README.md

Execute the test suite for the WebAssembly interpreter using the 'make test' command.

```bash
make test
```

--------------------------------

### Serve WebAssembly Test Repository Locally

Source: https://github.com/webassembly/spec/blob/main/test/README.md

Use this command to start a local HTTP server for the WebAssembly test repository. Access the tests via your browser at http://localhost:8000/test/out.

```python
python -m SimpleHTTPServer 8000
```

--------------------------------

### Struct Instructions

Source: https://github.com/webassembly/spec/blob/main/interpreter/README.md

Syntax for creating, getting, and setting struct fields.

```wast
struct.new(_<default>)? <var>
struct.get(_<sign>)? <var> <var>
struct.set <var> <var>
```

--------------------------------

### Start Function Validation

Source: https://github.com/webassembly/spec/blob/main/document/core/valid/modules.md

This rule validates the start function declaration within a WebAssembly module. It ensures that the start function is correctly specified.

```WebAssembly
Start_ok
```

--------------------------------

### WebAssembly Instruction Step: MEMORY.INIT

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/TEST.md

Describes the steps for executing the MEMORY.INIT instruction, including stack operations, bounds checking, and memory initialization.

```text
11. Else:
  a. Assert: Due to validation, (i < |$data(z, x).BYTES|).
  b. Push the value (I32.CONST j) to the stack.
  c. Push the value (I32.CONST $data(z, x).BYTES[i]) to the stack.
  d. Execute the instruction (STORE I32 ?(8) $memarg0()).
  e. Push the value (I32.CONST (j + 1)) to the stack.
  f. Push the value (I32.CONST (i + 1)) to the stack.
  g. Push the value (I32.CONST (n - 1)) to the stack.
  h. Execute the instruction (MEMORY.INIT x).
```

--------------------------------

### Build Core Spec Document

Source: https://github.com/webassembly/spec/blob/main/spectec/README.md

Navigates to the core document directory and invokes make to build the main specification using SpecTec.

```bash
cd ../document/core
make main
```

--------------------------------

### Install Bikeshed and Update

Source: https://github.com/webassembly/spec/blob/main/document/README.md

Installs the Bikeshed tool, which is required for generating single-page HTML and other formats. It clones the Bikeshed repository and installs it as an editable package within the pipenv environment.

```shell
git clone https://github.com/tabatkins/bikeshed.git
pipenv install -e bikeshed
bikeshed update
```

--------------------------------

### Instruction Type Example

Source: https://github.com/webassembly/spec/blob/main/document/metadata/code/valid/instructions.md

Illustrates the type of an instruction, showing consumed and produced values.

```text
For example, the instruction $(BINOP I32 ADD) has type I32 I32 -> I32,
consuming two I32 values and producing one.
The instruction (LOCAL.SET x) has type t ->_(x) eps, provided t is the type declared for the local x.
```

--------------------------------

### Array Initialization and Setting Instructions

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Demonstrates the use of ARRAY.INIT_DATA and ARRAY.SET instructions for initializing and modifying array elements. This snippet involves complex indexing and size calculations.

```spectre
`%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, I32_numtype, i) CONST_instr(I32_numtype, I32_numtype, j) CONST_instr(I32_numtype, I32_numtype, `%`_num_(n)) `ARRAY.INIT_DATA`_instr(x, y)]), [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, I32_numtype, i) $const($cunpack(zt), $cunpacknum_(zt, c)) `ARRAY.SET`_instr(x) `REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, I32_numtype, `%`_num_((i!`%`_num_.0 + 1))) CONST_instr(I32_numtype, I32_numtype, `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) `ARRAY.INIT_DATA`_instr(x, y)])
```

--------------------------------

### Parse Start Declarations

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Recursively parses start declarations from a list of declarations.

```spectec
def $startsd(decl*) : start*
  def $startsd([]) = []
  def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
  def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
    -- otherwise
```

--------------------------------

### Start Function Grammar

Source: https://github.com/webassembly/spec/blob/main/document/core/text/modules.md

Defines the structure for specifying a start function by its index.

```grammar
Tstart_
  = funcidx
```

--------------------------------

### Ignored Integer Syntax Examples

Source: https://github.com/webassembly/spec/blob/main/document/core/syntax/values.md

These integer syntax examples are ignored in the specification.

```WebAssembly
${syntax-ignore: u8 u16 u31 u32 u64 s33 i32 i64 i128}
```

--------------------------------

### Free Instruction for I31.GET

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Defines the free function for I31.GET_instr, handling sx and returning an empty set of resources.

```spectre
def $free_instr{sx : sx}(`I31.GET`_instr(sx)) = {TYPES [], FUNCS [], GLOBALS [], TABLES [], MEMS [], ELEMS [], DATAS [], LOCALS [], LABELS [], TAGS []}
```

--------------------------------

### Validate Start Function

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Checks the validity of the start function, ensuring it has no parameters or results.

```wast
relation Start_ok: `%|-%:OK`(context, start)
  rule _{C : context, x : idx}:
    `%|-%:OK`(C, START_start(x))
    -- Expand: `%~~%`(C.FUNCS_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype([]), `%`_resulttype([])))
```

--------------------------------

### Value Polymorphism Example (SELECT)

Source: https://github.com/webassembly/spec/blob/main/document/metadata/code/valid/instructions.md

Demonstrates value polymorphism with the SELECT instruction, showing valid instantiations for different types.

```text
For example, the SELECT instruction is valid with type t t I32 -> t, for any possible number type t.
Consequently, both instruction sequences
(CONST I32 1) (CONST I32 2) (CONST I32 3) (SELECT)
and
(CONST F64 $fnat(64, 1)) (CONST F64 $fnat(64, 2)) (CONST I32 3) (SELECT)
are valid, with t in the typing of SELECT being instantiated to I32 or F64, respectively.
```

--------------------------------

### Example Reduction Rule for BINOP I32 ADD

Source: https://github.com/webassembly/spec/blob/main/document/core/exec/conventions.md

Illustrates the reduction of the BINOP I32 ADD instruction, showing how two constant values are popped and their sum is pushed as a new constant value. This is a pure step that does not involve state changes.

```text
${Step_pure: (CONST I32 n_1) (CONST I32 n_2) (BINOP I32 ADD) ~> (CONST I32 $((n_1 + n_2) 2^32))}
```

--------------------------------

### Free Start Definition

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Defines how to free a start structure, which references a function index.

```wast
;; ../../../../specification/wasm-latest/1.4-syntax.modules.spectec
def $free_start(start : start) : free
  ;; ../../../../specification/wasm-latest/1.4-syntax.modules.spectec
  def $free_start{funcidx : funcidx}(START_start(funcidx)) = $free_funcidx(funcidx)
```

--------------------------------

### Free Instruction for LOCAL.GET

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Frees resources associated with the LOCAL.GET instruction by freeing the local index.

```spectre
def $free_instr{localidx : localidx}(`LOCAL.GET`_instr(localidx)) = $free_localidx(localidx)
```

--------------------------------

### Install Opam

Source: https://github.com/webassembly/spec/blob/main/spectec/README.md

Installs the Opam package manager, a prerequisite for managing OCaml packages.

```bash
$ apt-get install opam
$ opam init
```

--------------------------------

### ARRAY.INIT_ELEM Instruction Steps

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/TEST.md

Details the process of initializing elements in an array using existing elements from another array. Includes checks for bounds and type compatibility.

```WebAssembly
Step_read/array.init_elem x y
1. Let z be the current state.
2. Assert: Due to validation, a value of value type I32 is on the top of the stack.
3. Pop the value (I32.CONST n) from the stack.
4. Assert: Due to validation, a value of value type I32 is on the top of the stack.
5. Pop the value (I32.CONST j) from the stack.
6. Assert: Due to validation, a value of value type I32 is on the top of the stack.
7. Pop the value (I32.CONST i) from the stack.
8. Assert: Due to validation, a value is on the top of the stack.
9. Pop the value val from the stack.
10. If (val = REF.NULL_ADDR), then:
  a. Trap.
11. Assert: Due to validation, val is some REF.ARRAY_ADDR.
12. Let (REF.ARRAY_ADDR a) be val.
13. If ((a < |$arrayinst(z)|) /\ ((i + n) > |$arrayinst(z)[a].FIELDS|)), then:
  a. Trap.
14. If ((j + n) > |$elem(z, y).REFS|), then:
  a. Trap.
15. If (n = 0), then:
  a. Do nothing.
16. Else if (j < |$elem(z, y).REFS|), then:
  a. Let ref be $elem(z, y).REFS[j].
  b. Push the value (REF.ARRAY_ADDR a) to the stack.
  c. Push the value (I32.CONST i) to the stack.
  d. Push the value ref to the stack.
  e. Execute the instruction (ARRAY.SET x).
  f. Push the value (REF.ARRAY_ADDR a) to the stack.
  g. Push the value (I32.CONST (i + 1)) to the stack.
  h. Push the value (I32.CONST (j + 1)) to the stack.
  i. Push the value (I32.CONST (n - 1)) to the stack.
  j. Execute the instruction (ARRAY.INIT_ELEM x y).
```

--------------------------------

### Vector Shape Example

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/doc/syntax/instructions.md

Example of a vector shape interpretation: I32 X 4.

```text
I32 X 
4
```

--------------------------------

### vcvtop syntax with DEMOTE and PROMOTELOW

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Defines the syntax for vcvtop instructions, supporting DEMOTE and PROMOTELOW with conditions based on type size relationships.

```spectec
syntax vcvtop__{Fnn_1 : Fnn, M_1 : M, Fnn_2 : Fnn, M_2 : M}(`%X%`_shape((Fnn_1 : Fnn <: lanetype), `%`_dim(M_1)), `%X%`_shape((Fnn_2 : Fnn <: lanetype), `%`_dim(M_2))) =
  | DEMOTE(zero : zero)
    -- if ($sizenn1((Fnn_1 : Fnn <: numtype)) = (2 * $sizenn2((Fnn_2 : Fnn <: numtype))))
  | PROMOTELOW
    -- if ((2 * $sizenn1((Fnn_1 : Fnn <: numtype))) = $sizenn2((Fnn_2 : Fnn <: numtype)))
```

--------------------------------

### Parse Start Section Declarations

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Parses a list of declarations to extract start section declarations.

```spectec
def $startsd(decl*) : start*
  rec {
    ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:268.1-268.76
    def $startsd(decl*) : start*
      ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:306.1-306.24
      def $startsd([]) = []
      ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:307.1-307.52
      def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
      ;; ../../../../specification/wasm-latest/6.4-text.modules.spectec:308.1-308.59
      def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
        -- otherwise
  }
```

--------------------------------

### WebAssembly Start Function Definition

Source: https://github.com/webassembly/spec/blob/main/spectec/test-latex/TEST.md

Defines the start function for a WebAssembly module, which is an index to a function.

```WebAssembly
start ::= start funcidx
```

--------------------------------

### TABLE.GROW Instruction Steps

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/TEST.md

Outlines the steps for growing a table. This involves checking the current state and potentially performing actions based on the table's current size and growth parameters.

```WebAssembly
Step/table.grow x
1. Let z be the current state.
```

--------------------------------

### WebAssembly Instruction Step: table.grow

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/TEST.md

Details the table.grow instruction, including stack operations for size and element, and potential table resizing.

```text
1. Let z be the current state.
2. Assert: Due to validation, a value of value type I32 is on the top of the stack.
3. Pop the value (I32.CONST n) from the stack.
4. Assert: Due to validation, a value of value type ref is on the top of the stack.
5. Pop the value ref from the stack.
6. Either:
  a. Let ti be $growtable($table(z, x), n, ref).
  b. Push the value (I32.CONST |$table(z, x).REFS|) to the stack.
  c. Perform $with_tableinst(z, x, ti).
7. Or:
  a. Push the value (I32.CONST $inv_signed_(32, (- 1))) to the stack.
```

--------------------------------

### SpecTec Relation Declaration Example

Source: https://github.com/webassembly/spec/blob/main/spectec/doc/Language.md

An example of declaring a typing relation in SpecTec, specifying its notation.

```spec
relation Type_exp: ctxt |- exp : typ
```

--------------------------------

### Array Initialization and Setting Instructions

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Demonstrates array initialization and setting operations using specific instruction sequences. This is used in scenarios involving data initialization and modification within arrays.

```spectre
%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) CONST_instr(I32_numtype, j) CONST_instr(I32_numtype, `%`_num_(n)) `ARRAY.INIT_DATA`_instr(x, y)]), [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) $const($cunpack(zt), $cunpacknum_(zt, c)) `ARRAY.SET`_instr(x) `REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, `%`_num_((i!`%`_num_.0 + 1))) CONST_instr(I32_numtype, `%`_num_((((zsize(zt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)))) CONST_instr(I32_numtype, `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) `ARRAY.INIT_DATA`_instr(x, y)])
```

--------------------------------

### Build PDF Document

Source: https://github.com/webassembly/spec/blob/main/document/README.md

Compiles the core WebAssembly specification into a PDF document. This requires TeX Live to be installed.

```shell
make -C core pdf
```

--------------------------------

### WebAssembly Typing Rule Example

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/doc/exec/runtime-in.md

An example of a typing rule in WebAssembly, specifically for reference validity.

```wast
Ref_ok/*

```

--------------------------------

### Numeric Instructions Examples

Source: https://github.com/webassembly/spec/blob/main/document/metadata/code/syntax/instructions-in.md

Demonstrates various numeric operations including unary, binary, test, relational, and conversion operations.

```WebAssembly
unop_
```

```WebAssembly
binop_
```

```WebAssembly
testop_
```

```WebAssembly
relop_
```

```WebAssembly
cvtop__
```

--------------------------------

### Generated Prose from Otherwise Example

Source: https://github.com/webassembly/spec/blob/main/spectec/doc/Assumptions.md

Shows the prose generated from the 'otherwise' rule ordering example.

```text
1. If P then:
  a. Return output1
2. Else if Q then:
  a. Return output2
3. Else:
  a. Return output3
```

--------------------------------

### ARRAY.INIT_DATA Instruction Steps

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/TEST.md

Details the process of initializing array elements from raw data bytes. Includes checks for data bounds and type conversions.

```WebAssembly
Step_read/array.init_data x y
1. Let z be the current state.
2. Assert: Due to validation, a value of value type I32 is on the top of the stack.
3. Pop the value (I32.CONST n) from the stack.
4. Assert: Due to validation, a value of value type I32 is on the top of the stack.
5. Pop the value (I32.CONST j) from the stack.
6. Assert: Due to validation, a value of value type I32 is on the top of the stack.
7. Pop the value (I32.CONST i) from the stack.
8. Assert: Due to validation, a value is on the top of the stack.
9. Pop the value val from the stack.
10. If (val = REF.NULL_ADDR), then:
  a. Trap.
11. Assert: Due to validation, val is some REF.ARRAY_ADDR.
12. Let (REF.ARRAY_ADDR a) be val.
13. If ((a < |$arrayinst(z)|) /\ ((i + n) > |$arrayinst(z)[a].FIELDS|)), then:
  a. Trap.
14. If $Expand($type(z, x)) is some ARRAY, then:
  a. Let (ARRAY fieldtype_0) be $Expand($type(z, x)).
  b. Let (mut? zt) be fieldtype_0.
  c. If ((j + ((n * $zsize(zt)) / 8)) > |$data(z, y).BYTES|), then:
    1) Trap.
  d. If (n = 0), then:
    1) Do nothing.
  e. Else:
    1) Let c be $zbytes__1^-1(zt, $data(z, y).BYTES[j : ($zsize(zt) / 8)]).
    2) Push the value (REF.ARRAY_ADDR a) to the stack.
    3) Push the value (I32.CONST i) to the stack.
    4) Push the value $const($cunpack(zt), $cunpacknum_(zt, c)) to the stack.
    5) Execute the instruction (ARRAY.SET x).
    6) Push the value (REF.ARRAY_ADDR a) to the stack.
    7) Push the value (I32.CONST (i + 1)) to the stack.
    8) Push the value (I32.CONST (j + ($zsize(zt) / 8))) to the stack.
    9) Push the value (I32.CONST (n - 1)) to the stack.
    10) Execute the instruction (ARRAY.INIT_DATA x y).
15. Else if (n = 0), then:
  a. Do nothing.
```

--------------------------------

### WebAssembly Start Function Definition Grammar

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Defines the grammar for the start function, specifying a function index.

```wast
grammar Bstart : start*
  ;; ../../../../specification/wasm-latest/5.4-binary.modules.spectec
  prod{x : idx} x:Bfuncidx => [START_start(x)]
```

--------------------------------

### Free Type for Start Section

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Defines the free type for the start section, which specifies the entry point function.

```wast
def $free_start(start : start) : free
  def $free_start{funcidx : funcidx}(START_start(funcidx)) = $free_funcidx(funcidx)
```

--------------------------------

### Freeing Start Section in WebAssembly

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Defines the function to free the start section of a WebAssembly module, which includes a funcidx.

```wast
def $free_start(start : start) : free
  ;; ../../../../specification/wasm-latest/1.4-syntax.modules.spectec
  def $free_start{funcidx : funcidx}(START_start(funcidx)) = $free_funcidx(funcidx)
```

--------------------------------

### Navigate to Document Directory

Source: https://github.com/webassembly/spec/blob/main/document/README.md

Changes the current directory to the `document` folder, where the README and build configurations are located.

```shell
cd spec/document
```

--------------------------------

### Freeing Start Section in WebAssembly

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/TEST.md

Frees resources associated with the start section, which references a function index.

```text
free_start (START funcidx)
1. Return $free_funcidx(funcidx).
```

--------------------------------

### Install Menhir Parser Generator

Source: https://github.com/webassembly/spec/blob/main/interpreter/README.md

Install the Menhir parser generator using OPAM, a prerequisite for building the interpreter.

```bash
opam install menhir
```

--------------------------------

### Generate All Documentation Formats

Source: https://github.com/webassembly/spec/blob/main/document/core/README.md

Compiles all available documentation formats.

```shell
make all
```

--------------------------------

### Install Python Dependencies with Pipenv

Source: https://github.com/webassembly/spec/blob/main/document/README.md

Installs the required Python packages, Sphinx and six, within the pipenv environment.

```shell
pipenv install Sphinx==8.1.3 six
```

--------------------------------

### JavaScript Library: Instantiate and Export Function

Source: https://github.com/webassembly/spec/blob/main/interpreter/README.md

Example of instantiating a WebAssembly module from a binary and calling an exported function using the JavaScript library.

```javascript
(new WebAssembly.Instance(new WebAssembly.Module(binary))).exports.f(3, 4)
```

--------------------------------

### Example Mixfix Operator Construction

Source: https://github.com/webassembly/spec/blob/main/spectec/doc/IL.md

Illustrates how mixfix operators are constructed from notation, using a relation definition as an example.

```text
relation Expr_ok: context |- exp : typ
will be represented by the mixfix operator "%|-%:%", applied to a triple of arguments.
```

--------------------------------

### List Update Examples

Source: https://github.com/webassembly/spec/blob/main/spectec/doc/Language.md

Demonstrates updating a list element or a slice of a list with new values.

```Text
If `l` was the list `a b c d e f`,
then `l[[2] = x]` would be the list `a b x d e f`,
and `l[2 : 3] = x y z]` would be `a b x y z e f`.
```

```Text
More interestingly, if `ll` was the list `a b (c d) e f`,
then `ll[[2][0] = x]` would b `a b (x d) e f`
and `ll[[2] =++ x y]` would be `a b (c d x y) e f`.
```

--------------------------------

### Start Function Validation Rule

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Defines the validation rule for a start function, ensuring it is an exported function with no parameters and no results.

```wast
relation Start_ok: `%|-%:OK`(context, start)
  ;; ../../../../specification/wasm-latest/2.4-validation.modules.spectec
  rule _{C : context, x : idx}:
    `%|-%:OK`(C, START_start(x))
    -- Expand: `%~~%`(C.FUNCS_context[x!`%`_idx.0], `FUNC%->%`_comptype(`%`_resulttype([]), `%`_resulttype([])))
```

--------------------------------

### WebAssembly Instruction Step: global.set

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/TEST.md

Outlines the steps for the global.set instruction, including stack value retrieval and global variable modification.

```text
1. Let z be the current state.
2. Assert: Due to validation, a value is on the top of the stack.
3. Pop the value val from the stack.
4. Perform $with_global(z, x, val).
```

--------------------------------

### WebAssembly CVTOP Instructions

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Demonstrates various CVTOP (Convert Operation) instructions for type conversions between integer and floating-point types. These snippets show the opcode and the specific conversion details.

```wast
prod 0xBB => CVTOP_instr(F64_numtype, F32_numtype, PROMOTE_cvtop__)
;;
```

```wast
prod 0xBC => CVTOP_instr(I32_numtype, F32_numtype, REINTERPRET_cvtop__)
;;
```

```wast
prod 0xBD => CVTOP_instr(I64_numtype, F64_numtype, REINTERPRET_cvtop__)
;;
```

```wast
prod 0xBE => CVTOP_instr(F32_numtype, I32_numtype, REINTERPRET_cvtop__)
;;
```

```wast
prod 0xBF => CVTOP_instr(F64_numtype, I64_numtype, REINTERPRET_cvtop__)
;;
```

--------------------------------

### WebAssembly Start Function Free Type

Source: https://github.com/webassembly/spec/blob/main/spectec/test-latex/TEST.md

Defines the 'free' type calculation for a start function, which is based on the function index.

```WebAssembly
free_start(start funcidx) = free_funcidx(funcidx)
```

--------------------------------

### Free Instruction for STORE

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Frees resources for a generic STORE instruction, including numeric type and memory index.

```spectre
def $free_instr{numtype : numtype, `storeop?` : storeop_(numtype)?, memidx : memidx, memarg : memarg}(STORE_instr(numtype, storeop?{storeop <- `storeop?`}, memidx, memarg)) = $free_numtype(numtype) +++ $free_memidx(memidx)
```

--------------------------------

### Parse Start Declarations

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/TEST.md

Parses start declarations from a given list. Returns an empty list if the input is empty.

```text
startsd decl'*
1. If (decl'* = []), then:
  a. Return [].
2. Let [start] :: decl'* be decl'*.
3. Return [start] :: $startsd(decl'*).
```

--------------------------------

### Free Instruction for GLOBAL.GET

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

Frees resources associated with the GLOBAL.GET instruction by freeing the global index.

```spectre
def $free_instr{globalidx : globalidx}(`GLOBAL.GET`_instr(globalidx)) = $free_globalidx(globalidx)
```

--------------------------------

### Instantiate WebAssembly Module

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

Instantiates a WebAssembly module given a store and external addresses. This process involves type checking, allocating instances, evaluating initializers, and setting up the execution state.

```spectre
def $instantiate(store : store, module : module, externaddr*) : config
  ;; ../../../../specification/wasm-latest/4.4-execution.modules.spectec
  def $instantiate{s : store, module : module, `externaddr*` : externaddr*, s'''' : store, moduleinst : moduleinst, `instr_E*` : instr*, `instr_D*` : instr*, `instr_S?` : instr?, `xt_I*` : externtype*, `xt_E*` : externtype*, `type*` : type*, `import*` : import*, `tag*` : tag*, `global*` : global*, `mem*` : mem*, `table*` : table*, `func*` : func*, `data*` : data*, `elem*` : elem*, `start?` : start?, `export*` : export*, `expr_G*` : expr*, `globaltype*` : globaltype*, `expr_T*` : expr*, `tabletype*` : tabletype*, `byte**` : byte**, `datamode*` : datamode*, `elemmode*` : elemmode*, `expr_E**` : expr**, `reftype*` : reftype*, `x?` : idx?, moduleinst_0 : moduleinst, z : state, z' : state, `val_G*` : val*, z'' : state, `ref_T*` : ref*, z''' : state, `ref_E**` : ref**, s''' : store, f : frame, i_D : nat, i_E : nat}(s, module, externaddr*{externaddr <- `externaddr*`}) = `%;%`_config(`%;%`_state(s'''', {LOCALS [], MODULE moduleinst}), instr_E*{instr_E <- `instr_E*`} ++ instr_D*{instr_D <- `instr_D*`} ++ lift(instr_S?{instr_S <- `instr_S?`}))
    -- Module_ok: `|-%:%`(module, `%->%`_moduletype(xt_I*{xt_I <- `xt_I*`}, xt_E*{xt_E <- `xt_E*`}))
    -- (Externaddr_ok: `%|-%:%`(s, externaddr, xt_I))*{externaddr <- `externaddr*`, xt_I <- `xt_I*`}
    -- if (module = MODULE_module(`%`_list(type*{type <- `type*`}), `%`_list(import*{import <- `import*`}), `%`_list(tag*{tag <- `tag*`}), `%`_list(global*{global <- `global*`}), `%`_list(mem*{mem <- `mem*`}), `%`_list(table*{table <- `table*`}), `%`_list(func*{func <- `func*`}), `%`_list(data*{data <- `data*`}), `%`_list(elem*{elem <- `elem*`}), start?{start <- `start?`}, `%`_list(export*{export <- `export*`})))
    -- if (global*{global <- `global*`} = GLOBAL_global(globaltype, expr_G)*{expr_G <- `expr_G*`, globaltype <- `globaltype*`})
    -- if (table*{table <- `table*`} = TABLE_table(tabletype, expr_T)*{expr_T <- `expr_T*`, tabletype <- `tabletype*`})
    -- if (data*{data <- `data*`} = DATA_data(byte*{byte <- `byte*`}, datamode)*{`byte*` <- `byte**`, datamode <- `datamode*`})
    -- if (elem*{elem <- `elem*`} = ELEM_elem(reftype, expr_E*{expr_E <- `expr_E*`}, elemmode)*{elemmode <- `elemmode*`, `expr_E*` <- `expr_E**`, reftype <- `reftype*`})
    -- if (start?{start <- `start?`} = START_start(x)?{x <- `x?`})
    -- if (moduleinst_0 = {TYPES $alloctypes(type*{type <- `type*`}), TAGS [], GLOBALS $globalsxa(externaddr*{externaddr <- `externaddr*`}), MEMS [], TABLES [], FUNCS $funcsxa(externaddr*{externaddr <- `externaddr*`}) ++ (|s.FUNCS_store| + i_F)^(i_F<|func*{func <- `func*`}|){}, DATAS [], ELEMS [], EXPORTS []})
    -- if (z = `%;%`_state(s, {LOCALS [], MODULE moduleinst_0}))
    -- if ((z', val_G*{val_G <- `val_G*`}) = $evalglobals(z, globaltype*{globaltype <- `globaltype*`}, expr_G*{expr_G <- `expr_G*`}))
    -- if ((z'', ref_T*{ref_T <- `ref_T*`}) = $evalexprs(z', expr_T*{expr_T <- `expr_T*`}))
    -- if ((z''', ref_E*{ref_E <- `ref_E*`}*{`ref_E*` <- `ref_E**`}) = $evalexprss(z'', expr_E*{expr_E <- `expr_E*`}*{`expr_E*` <- `expr_E**`}))
    -- if (z''' = `%;%`_state(s''', f))
```

--------------------------------

### WebAssembly Instruction Syntax Overview

Source: https://github.com/webassembly/spec/blob/main/spectec/test-middlend/TEST.md

This section lists various WebAssembly instructions and their associated parameters and types. It serves as a reference for the available operations.

```text
syntax expr = instr*

def $memarg0 : memarg
  def $memarg0 = {ALIGN `%`_u32(0), OFFSET `%`_u64(0)}

def $const(consttype : consttype, lit_ : lit_((consttype : consttype <: storagetype))) : instr
```

--------------------------------

### Install js_of_ocaml for JavaScript Compilation

Source: https://github.com/webassembly/spec/blob/main/interpreter/README.md

Install the necessary js_of_ocaml packages using OPAM, required for cross-compiling the interpreter to JavaScript.

```bash
opam install js_of_ocaml js_of_ocaml-ppx
```

--------------------------------

### Constant Definition Example

Source: https://github.com/webassembly/spec/blob/main/spectec/doc/Overview.md

Demonstrates how to define constants, such as a 32-bit zero value, using SpecTec.

```SpecTec
def $zero32 : val
def $zero32 = CONST I32 0
```

--------------------------------

### Define $fof to get frame from state

Source: https://github.com/webassembly/spec/blob/main/spectec/test-frontend/TEST.md

A shorthand definition to get the frame from a state. It directly calls the $frame definition.

```wast
def $fof(state : state) : frame
  def $fof{z : state}(z) = $frame(z)
```

--------------------------------

### Generate PDF Documentation

Source: https://github.com/webassembly/spec/blob/main/document/core/README.md

Builds the PDF version of the documentation. This requires a LaTeX installation and the output will be in `_build/latex`.

```shell
make pdf
```

--------------------------------

### Syntax for Value and Heap Types

Source: https://github.com/webassembly/spec/blob/main/spectec/test-prose/doc/valid/conventions.md

Illustrates the syntax for value types and heap types, including special bottom types.

```text
$${syntax: {valtype/sem absheaptype/sem typeuse/sem}}
```