Create specification/wasm-latest

To give proposal repos a consistent location to make changes to the
SpecTec source and to simplify merging those proposals back into the
spec repo once they are completed. The new directory is a copy of the
wasm-3.0 directory in its current state, created via a sequence of git
mv and merge operations to preserve the blame history in both
directories.

Also add a new CI script ensuring that the contents of wasm-latest match
the contents of the highest versioned wasm-X.Y directory. This will
ensure that bug fixes are applied in both directories.

As a drive-by fix, rename 6.3-text.modules.spectec to
6.4-text.modules.spectec.

Author: tlively

.github/workflows/ci-spec.yml

@@ -3,16 +3,25 @@ name: CI for specs
 on:
   push:
     branches: [ main, wasm-3.0 ]
-    paths: [ .github/**, document/**, spectec/** ]
+    paths: [ .github/**, document/**, spectec/**, specification/** ]
 
   pull_request:
     branches: [ main, wasm-3.0 ]
-    paths: [ .github/**, document/**, spectec/** ]
+    paths: [ .github/**, document/**, spectec/**, specification/** ]
 
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
 
 jobs:
+  ensure-wasm-latest:
+    if: ${{ github.repository == 'WebAssembly/spec' }}
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repo
+        uses: actions/checkout@v4
+      - name: Diff wasm-latest
+        run: bash .github/workflows/diff-wasm-latest.sh
+
   build-core-spec:
     runs-on: ubuntu-latest
     steps:
@@ -145,6 +154,7 @@ jobs:
   publish-spec:
     runs-on: ubuntu-latest
     needs:
+      - ensure-wasm-latest
       - build-core-spec
       - build-js-api-spec
       - build-web-api-spec

.github/workflows/diff-wasm-latest.sh

@@ -0,0 +1,30 @@
+#!/bin/bash
+
+# Identify the highest versioned directory
+HIGHEST_VER=$(ls -d specification/wasm-[0-9]* 2>/dev/null | sort -V | tail -n 1)
+
+if [ -z "$HIGHEST_VER" ]; then
+    echo "❌ Error: No wasm-X.Y versioned directories found in specification/"
+    exit 1
+fi
+
+LATEST="specification/wasm-latest"
+
+# Check that wasm-latest exists
+if [ ! -d "$LATEST" ]; then
+    echo "❌ Error: $LATEST does not exist."
+    exit 1
+fi
+
+# Diff the highest version with wasm-latest and check that the diff is empty
+echo "Checking for differences between $HIGHEST_VER and $LATEST..."
+
+if diff -qr "$HIGHEST_VER" "$LATEST" > /dev/null; then
+    echo "✅ Success: Contents match. No changes needed."
+else
+    echo "🔍 Differences detected:"
+    echo "--------------------------------"
+    diff -r "$HIGHEST_VER" "$LATEST"
+    echo "--------------------------------"
+    exit 1
+fi

.github/workflows/w3c-publish.yml

@@ -4,9 +4,9 @@ on:
   push:
     # Disable on forks!
     branches: [ main ]
-    paths: [ .github/**, document/** ]
+    paths: [ .github/**, document/**, specification/** ]
   pull_request:
-    paths: [ .github/**, document/** ]
+    paths: [ .github/**, document/**, specification/** ]
 
   # Allows you to run this workflow manually from the Actions tab, gh CLI tool,
   # or REST API. THe w3c-status options correspond to the valid options for

specification/wasm-3.0/0.1-aux.vars.spectec

@@ -0,0 +1,9 @@
+;;
+;; General Variable Conventions
+;;
+
+syntax N hint(macro none) = nat
+syntax M hint(macro none) = nat
+syntax K hint(macro none) = nat
+syntax n hint(macro none) = nat  ;; hack
+syntax m hint(macro none) = nat  ;; hack

specification/wasm-3.0/0.2-aux.num.spectec

@@ -0,0 +1,15 @@
+;;
+;; General Numeric Functions
+;;
+
+def $min(nat, nat) : nat
+def $min(i, j) = i  -- if $(i <= j)
+def $min(i, j) = j  -- otherwise
+
+def $sum(nat*) : nat  hint(show (+) %) hint(macro none)
+def $sum(eps) = 0
+def $sum(n n'*) = $(n + $sum(n'*))
+
+def $prod(nat*) : nat  hint(show (*) %) hint(macro none)
+def $prod(eps) = 1
+def $prod(n n'*) = $(n * $prod(n'*))

specification/wasm-3.0/0.3-aux.seq.spectec

@@ -0,0 +1,58 @@
+;;
+;; General Functions on Sequences
+;;
+
+;; Type casting
+
+def $opt_(syntax X, X*) : X?  hint(show %2)
+def $opt_(syntax X, eps) = eps
+def $opt_(syntax X, w) = w
+
+
+;; Concatenation
+
+def $concat_(syntax X, (X*)*) : X*  hint(show (++) %2) hint(inverse $inv_concat_)
+def $concat_(syntax X, eps) = eps
+def $concat_(syntax X, (w*) (w'*)*) = w* ++ $concat_(X, (w'*)*)
+
+def $concatn_(syntax X, (X*)*, nat) : X*  hint(show (++) %2) hint(inverse $inv_concatn_)
+def $concatn_(syntax X, eps, n) = eps
+def $concatn_(syntax X, (w^n) (w'^n)*, n) = w^n $concatn_(X, (w'^n)*, n)
+
+def $concatopt_(syntax X, (X?)*) : X*  hint(show (++) %2)
+def $concatopt_(syntax X, eps) = eps
+def $concatopt_(syntax X, (w?) (w'?)*) = w? ++ $concat_(X, (w'?)*)
+
+def $inv_concat_(syntax X, X*) : (X*)*
+def $inv_concat_ hint(builtin)
+
+def $inv_concatn_(syntax X, nat, X*) : (X*)*
+def $inv_concatn_ hint(builtin)
+
+
+;; Set functions
+
+def $disjoint_(syntax X, X*) : bool  hint(show %2 $disjoint) hint(macro none)
+def $disjoint_(syntax X, eps) = true
+def $disjoint_(syntax X, w w'*) = ~(w <- w'*) /\ $disjoint_(X, w'*)
+
+def $setminus_(syntax X, X*, X*) : X*  hint(show %2\%3)
+def $setminus1_(syntax X, X, X*) : X*
+
+def $setminus_(syntax X, eps, w*) = eps
+def $setminus_(syntax X, w_1 w'*, w*) = $setminus1_(X, w_1, w*) ++ $setminus_(X, w'*, w*)
+def $setminus1_(syntax X, w, eps) = w
+def $setminus1_(syntax X, w, w_1 w'*) = eps                     -- if w = w_1
+def $setminus1_(syntax X, w, w_1 w'*) = $setminus1_(X, w, w'*)  -- otherwise
+
+;; [{1, 2}, {a, b, c}] -> {[1, a], [1, b], [1, c], [2, a], [2, b], [2, c]}
+def $setproduct_(syntax X, (X*)*) : (X*)*  hint(show %latex("{\\Large\\times}") %2)
+def $setproduct1_(syntax X, X*, (X*)*) : (X*)*
+def $setproduct2_(syntax X, X, (X*)*) : (X*)*
+
+def $setproduct_(syntax X, eps) = (eps)
+def $setproduct_(syntax X, (w_1*) (w*)*) = $setproduct1_(X, w_1*, $setproduct_(X, (w*)*))
+def $setproduct1_(syntax X, eps, (w*)*) = eps
+def $setproduct1_(syntax X, w_1 w'*, (w*)*) = $setproduct2_(X, w_1, (w*)*) ++ $setproduct1_(X, w'*, (w*)*)
+def $setproduct2_(syntax X, w_1, eps) = eps
+def $setproduct2_(syntax X, w_1, (w'*) (w*)*) = (w_1 w'*) ++ $setproduct2_(X, w_1, (w*)*)

specification/wasm-3.0/1.0-syntax.profiles.spectec

@@ -0,0 +1,5 @@
+;;
+;; Profiles
+;;
+
+def $ND : bool hint(builtin)  ;; non-determinism

specification/wasm-3.0/1.1-syntax.values.spectec

@@ -0,0 +1,205 @@
+;;
+;; Syntax of Values
+;;
+
+;; Integers
+
+syntax bit  hint(desc "bit") = 0 | 1
+syntax byte hint(desc "byte") = 0x00 | ... | 0xFF
+
+syntax uN(N) hint(desc "unsigned integer") hint(show u#%) hint(macro "uNX") =
+  0 | ... | $nat$(2^N-1)
+syntax sN(N) hint(desc "signed integer") hint(show s#%) hint(macro "sNX") =
+  -2^(N-1) | ... | -1 | 0 | +1 | ... | +2^(N-1)-1
+syntax iN(N) hint(desc "integer") hint(show i#%) hint(macro "iNX") =
+  uN(N)
+
+syntax u8  = uN(`8)
+syntax u16 = uN(`16)
+syntax u31 = uN(`31)
+syntax u32 = uN(`32)
+syntax u64 = uN(`64)
+syntax s33 = sN(`33)
+syntax i32 = iN(`32)
+syntax i64 = iN(`64)
+syntax i128 = iN(`128)
+
+var b : byte
+
+
+;; Floating-point
+
+def $signif(N) : nat
+def $signif(32) = 23
+def $signif(64) = 52
+
+def $expon(N) : nat
+def $expon(32) = 8
+def $expon(64) = 11
+
+def $M(N) : nat hint(show `M) hint(macro none)
+def $M(N) = $signif(N)
+
+def $E(N) : nat hint(show `E) hint(macro none)
+def $E(N) = $expon(N)
+
+syntax fN(N) hint(desc "floating-point number") hint(show f#%) hint(macro "fNX") =
+  | POS fNmag(N)  hint(show $(+%)) \
+  | NEG fNmag(N)  hint(show $(-%))
+
+syntax exp hint(show e) hint(macro none) = int
+syntax fNmag(N) hint(desc "floating-point magnitude") hint(show fNmag) =
+  | NORM m exp   hint(show $((1 + %*2^(-$M(N))) * 2^%))   -- if $(m < 2^$M(N) /\ 2-2^($E(N)-1) <= exp <= 2^($E(N)-1)-1)
+  | SUBNORM m    hint(show $((0 + %*2^(-$M(N))) * 2^exp)) -- if $(m < 2^$M(N) /\ 2-2^($E(N)-1) = exp)
+  | INF          hint(show infinity)
+  | NAN (m)      hint(show NAN#(%))                       -- if $(1 <= m < 2^$M(N))
+
+syntax f32 = fN(`32)
+syntax f64 = fN(`64)
+
+def $fzero(N) : fN(N) hint(show $(+0))
+def $fzero(N) = POS (SUBNORM 0)
+
+def $fnat(N, nat) : fN(N)  hint(show $(+%))
+def $fnat(N, n) = POS (NORM n 0)
+
+def $fone(N) : fN(N)  hint(show $(+1))
+def $fone(N) = POS (NORM 1 0)
+
+def $canon_(N) : nat
+def $canon_(N) = $(2^($signif(N)-1))
+
+
+;; Vectors
+
+syntax vN(N) hint(desc "vector") hint(show v#%) hint(macro "vNX") =
+  uN(N)
+
+syntax v128 = vN(`128)
+
+
+;; Lists
+
+;; TODO(3, rossberg): enable writing X^n
+syntax list(syntax X) = X*  -- if |X*| < $(2^32)
+
+
+;; Names
+
+syntax char hint(desc "character") = U+0000 | ... | U+D7FF | U+E000 | ... | U+10FFFF
+
+def $utf8(char*) : byte*
+
+syntax name hint(desc "name") = char*  -- if |$utf8(char*)| < $(2^32)
+
+var nm : name
+
+
+;; Indices
+
+syntax idx hint(desc "index") = u32
+syntax laneidx hint(desc "lane index") = u8
+
+syntax typeidx hint(desc "type index") = idx
+syntax funcidx hint(desc "function index") = idx
+syntax globalidx hint(desc "global index") = idx
+syntax tableidx hint(desc "table index") = idx
+syntax memidx hint(desc "memory index") = idx
+syntax tagidx hint(desc "tag index") = idx
+syntax elemidx hint(desc "elem index") = idx
+syntax dataidx hint(desc "data index") = idx
+syntax labelidx hint(desc "label index") = idx
+syntax localidx hint(desc "local index") = idx
+syntax fieldidx hint(desc "field index") = idx
+
+syntax externidx hint(desc "external index") hint(macro "%" "XX%") =
+  | FUNC funcidx | GLOBAL globalidx | TABLE tableidx | MEM memidx | TAG tagidx
+
+var x : idx
+var y : idx
+var l : labelidx
+var xx : externidx
+var x33 : s33 hint(show x)
+
+
+;; Sort projection
+
+;; TODO(3, rossberg): add built-in notation for comprehensions?
+
+def $funcsxx(externidx*) : typeidx*      hint(show $funcs(%))   hint(macro "funcsxx")
+def $globalsxx(externidx*) : globalidx*  hint(show $globals(%)) hint(macro "globalsxx")
+def $tablesxx(externidx*) : tableidx*    hint(show $tables(%))  hint(macro "tablesxx")
+def $memsxx(externidx*) : memidx*        hint(show $mems(%))    hint(macro "memsxx")
+def $tagsxx(externidx*) : tagidx*        hint(show $tags(%))    hint(macro "tagsxx")
+
+def $funcsxx(eps) = eps
+def $funcsxx((FUNC x) xx*) = x $funcsxx(xx*)
+def $funcsxx(externidx xx*) = $funcsxx(xx*)  -- otherwise
+
+def $globalsxx(eps) = eps
+def $globalsxx((GLOBAL x) xx*) = x $globalsxx(xx*)
+def $globalsxx(externidx xx*) = $globalsxx(xx*)  -- otherwise
+
+def $tablesxx(eps) = eps
+def $tablesxx((TABLE x) xx*) = x $tablesxx(xx*)
+def $tablesxx(externidx xx*) = $tablesxx(xx*)  -- otherwise
+
+def $memsxx(eps) = eps
+def $memsxx((MEM x) xx*) = x $memsxx(xx*)
+def $memsxx(externidx xx*) = $memsxx(xx*)  -- otherwise
+
+def $tagsxx(eps) = eps
+def $tagsxx((TAG x) xx*) = x $tagsxx(xx*)
+def $tagsxx(externidx xx*) = $tagsxx(xx*)  -- otherwise
+
+
+;; Free indices
+
+syntax free =
+  { TYPES typeidx*,
+    FUNCS funcidx*,
+    GLOBALS globalidx*,
+    TABLES tableidx*,
+    MEMS memidx*,
+    ELEMS elemidx*,
+    DATAS dataidx*,
+    LOCALS localidx*,
+    LABELS labelidx*
+  }
+
+
+def $free_opt(free?) : free
+def $free_list(free*) : free
+
+def $free_opt(eps) = {}
+def $free_opt(free) = free
+
+def $free_list(eps) = {}
+def $free_list(free free'*) = free ++ $free_list(free'*)
+
+
+def $free_typeidx(typeidx) : free
+def $free_funcidx(funcidx) : free
+def $free_globalidx(globalidx) : free
+def $free_tableidx(tableidx) : free
+def $free_memidx(memidx) : free
+def $free_elemidx(elemidx) : free
+def $free_dataidx(dataidx) : free
+def $free_localidx(localidx) : free
+def $free_labelidx(labelidx) : free
+def $free_externidx(externidx) : free
+
+def $free_typeidx(typeidx) = {TYPES typeidx}
+def $free_funcidx(funcidx) = {FUNCS funcidx}
+def $free_globalidx(globalidx) = {GLOBALS globalidx}
+def $free_tableidx(tableidx) = {TABLES tableidx}
+def $free_memidx(memidx) = {MEMS memidx}
+def $free_elemidx(elemidx) = {ELEMS elemidx}
+def $free_dataidx(dataidx) = {DATAS dataidx}
+def $free_localidx(localidx) = {LOCALS localidx}
+def $free_labelidx(labelidx) = {LABELS labelidx}
+
+def $free_externidx(FUNC funcidx) = $free_funcidx(funcidx)
+def $free_externidx(GLOBAL globalidx) = $free_globalidx(globalidx)
+def $free_externidx(TABLE tableidx) = $free_tableidx(tableidx)
+def $free_externidx(MEM memidx) = $free_memidx(memidx)