SIMD execution

Makefile

@@ -1,7 +1,13 @@
 default:
 	opam install .
 
+SHELL := bash
+
+SCRIPT := ./run_wast.sh
+
+FOLDER ?=
+FILTER ?=
+
+.PHONY: run_wast
 run_wast:
-	@FOLDER=$$(if [ "$(filter-out run_wast,$(MAKECMDGOALS))" ]; then echo "$(word 2, $(MAKECMDGOALS))"; else echo "./wast_testsuite"; fi);\
-	chmod +x run_wast.sh; \
-	./run_wast.sh "$$FOLDER"
+	$(SCRIPT) "$(FOLDER)" "$(FILTER)"

README.md

@@ -6,10 +6,11 @@ A WebAssembly (aka Wasm) formalisation in Coq(Rocq), based on the [official spec
 The quotes from the WebAssembly standard (starting with `std-doc`) are (C) their respective authors. 
 The files located in `src/Parray` are adapted from the Rocq kernel and therefore licensed under GNU LPGL 2.1 - see `src/Parray/LICENSE.LGPL`.
 
-The current project formalises Wasm version 2.0 with the following deltas:
+The current project formalises Wasm version 2.0 with the following additions:
 - [+] Subtyping systems (from the future funcref/GC extension proposals);
-- [+] Tail-call;
-- [-] SIMD.
+- [+] Tail-call.
+
+SIMD execution is implemented via the corresponding evaluation functions in the reference implementations. The Rocq mechanisation uses opauqe opcodes (from the binary format) for parsing the SIMD instructions and handling their execution.
 
 A large part of the old Wasm 1.0 formalisation has been published at [FM'21](https://link.springer.com/chapter/10.1007/978-3-030-90870-6_4), with many additions to the repository since then.
 
@@ -27,7 +28,7 @@ A large part of the old Wasm 1.0 formalisation has been published at [FM'21](htt
 - [x] Interpreter with optimised context representations.
 
 ## Merged
-- [x] Updates for Wasm 2.0 (except SIMD) + subtyping systems + tail-call.
+- [x] Updates for Wasm 2.0 + subtyping systems + tail-call.
 - [x] Validate WasmRef-Coq (conformance tests).
 
 # Program Logic
@@ -70,12 +71,22 @@ Then, run:
 ```bash
 make run_wast
 ```
-All SIMD tests are skipped since the project does not implement SIMD yet. The interpreter is expected to pass all the other core tests (last tested on 30th May 2025):
+The interpreter is expected to pass all the other core tests (last tested on 17th Aug 2025):
 ```bash
-Total passed: 28018/28018 (100.00%)
+Total passed: 54004/54004 (100.00%)
 ```
 
-Running the test suite takes around 1-2 minutes.
+Running the test suite takes around 2-3 minutes.
+
+It is also possible to run a selected subset of the test by filtering the file names. For example,
+```bash
+make run_wast FILTER="simd"
+```
+runs only the SIMD tests, while
+```bash
+make run_wast FILTER="load"
+```
+runs only the test files whose names include `load` (i.e. various memory load instructions both for the Wasm 1.0 values and the v128 values).
 
 Note that tail-call is not part of the standard yet and is therefore not tested.
 

changelogs/v2.2.0.md

@@ -0,0 +1,9 @@
+# Release 2.2.0
+
+## New Features
+- Implemented SIMD execution via eval functions in the reference implementation. The extracted runtime now pass the full Wasm 2.0 test suite.
+
+## Refactorings and Infrastructural Changes
+- Extraction now extracts Coq's `String.string` to OCaml native `string` instead of `char list`. The signature of various interfaces are updated accordingly.
+- Extraction now extracts Coq's binary integers (N/Z/positive) to ZArith's BigInt instead. The original conversion functions are therefore deprecated. New conversion functions between ZArith's BigInt and OCaml's native int are added. This is to avoid cyclic dependencies in the parametric SIMD implementations.
+- The testing script `run_wast.sh` and the makefile now support testing a subset of the test suite by passing in a filter argument. For example: `make run_wast FILTER="simd"` runs only the simd tests.

run_wast.sh

@@ -1,33 +1,52 @@
 #!/bin/bash
-set -e
+set -euo pipefail
 
-folder="${1:-./wast_testsuite}"  # Use argument, or fallback to default
+folder="${1:-./wast_testsuite}"  
+filter="${2:-}" 
+
+shopt -s nullglob
+
+if [[ -n "$filter" ]]; then
+  files=( "$folder"/*"$filter"*.wast )
+else
+  files=( "$folder"/*.wast )
+fi
+
+if (( ${#files[@]} == 0 )); then
+  echo "No matching .wast files in '$folder'${filter:+ containing '$filter'}."
+  exit 0
+fi
 
 total_passed=0
 total_tests=0
 
-for wastfile in "$folder"/*.wast; do
-	if [[ "$wastfile" == *simd* ]]; then
-		echo "Skipping SIMD test: $wastfile"
-		continue
-	fi
-	echo "Running: $wastfile"
-	tmpfile=$(mktemp)
-	cleaned=$(mktemp)
-	dune exec -- wasm_coq_interpreter --wast "$wastfile" | tee "$tmpfile"
-	cat "$tmpfile" | tr -d '\r' | sed 's/\x1b\[[0-9;]*m//g' > "$cleaned"
-	result_line=$(grep "Result: " "$cleaned")
-	if [[ "$result_line" =~ Result:\ ([0-9]+)/([0-9]+) ]]; then
-		passed="${BASH_REMATCH[1]}"
-		total="${BASH_REMATCH[2]}"
-		total_passed=$((total_passed + passed))
-		total_tests=$((total_tests + total))
-	else
-		echo "Regex match failed for $$wastfile"
-	fi
-	rm -f "$tmpfile" "$cleaned"
+for wastfile in "${files[@]}"; do
+  echo "Running: $wastfile"
+  tmpfile=$(mktemp)
+  cleaned=$(mktemp)
+
+  dune exec -- wasm_coq_interpreter --wast "$wastfile" | tee "$tmpfile"
+  tr -d '\r' < "$tmpfile" | sed 's/\x1b\[[0-9;]*m//g' > "$cleaned"
+
+  if result_line=$(grep -m1 "Result: " "$cleaned"); then
+    if [[ "$result_line" =~ Result:\ ([0-9]+)/([0-9]+) ]]; then
+      passed="${BASH_REMATCH[1]}"
+      total="${BASH_REMATCH[2]}"
+      total_passed=$((total_passed + passed))
+      total_tests=$((total_tests + total))
+    else
+      echo "Regex match failed for $wastfile"
+    fi
+  else
+    echo "No 'Result:' line found for $wastfile"
+  fi
+  rm -f "$tmpfile" "$cleaned"
 done
 
 echo "================"
-percentage=$(awk "BEGIN { printf \"%.2f\", ($total_passed / $total_tests) * 100}")
-echo "Total Passed: $total_passed/$total_tests ($percentage%)"
+if (( total_tests > 0 )); then
+  percentage=$(awk "BEGIN { printf \"%.2f\", ($total_passed / $total_tests) * 100 }")
+  echo "Total Passed: $total_passed/$total_tests ($percentage%)"
+else
+  echo "No tests run."
+fi