[spectec] Require explicit declaration of builtins

specification/wasm-1.0/3-numerics.spectec

@@ -40,10 +40,23 @@ def $promote__(M, N, fN(M)) : fN(N)*
 def $convert__(M, N, sx, iN(M)) : fN(N)              hint(show $convert__(%,%)^(%)#((%)))
 def $reinterpret__(valtype_1, valtype_2, val_(valtype_1)) : val_(valtype_2)
 
+;; TODO(3, rossberg): implement numerics internally
+def $wrap__        hint(builtin)
+def $extend__      hint(builtin)
+def $trunc__       hint(builtin)
+def $demote__      hint(builtin)
+def $promote__     hint(builtin)
+def $convert__     hint(builtin)
+def $reinterpret__ hint(builtin)
+
 def $ibytes_(N, iN(N)) : byte*                       hint(show $bytes_(I#%,%))
 def $fbytes_(N, fN(N)) : byte*                       hint(show $bytes_(F#%,%))
 def $bytes_(valtype, val_(valtype)) : byte*
 
+def $ibytes_ hint(builtin)
+def $fbytes_ hint(builtin)
+def $bytes_ hint(builtin)
+
 def $invibytes_(N, byte*) : iN(N)
 def $invfbytes_(N, byte*) : fN(N)
 
@@ -79,16 +92,36 @@ def $ige_(N, sx, iN(N), iN(N)) : u32     hint(show $ige_(%)^(%)#((%,%)))
 def $iadd_(N, i_1, i_2) = $((i_1 + i_2) \ 2^N)
 def $isub_(N, i_1, i_2) = $((2^N + i_1 - i_2) \ 2^N)
 def $imul_(N, i_1, i_2) = $((i_1 * i_2) \ 2^N)
+
+def $idiv_ hint(builtin)
+def $irem_ hint(builtin)
+def $inot_ hint(builtin)
+def $iand_ hint(builtin)
+def $ior_  hint(builtin)
+def $ixor_ hint(builtin)
+def $ishl_ hint(builtin)
+def $ishr_ hint(builtin)
+def $irotl_ hint(builtin)
+def $irotr_ hint(builtin)
+def $iclz_  hint(builtin)
+def $ictz_  hint(builtin)
+def $ipopcnt_ hint(builtin)
+
 def $ieqz_(N, i_1) = $bool(i_1 = 0)
 def $inez_(N, i_1) = $bool(i_1 =/= 0)
+
 def $ieq_(N, i_1, i_2) = $bool(i_1 = i_2)
 def $ine_(N, i_1, i_2) = $bool(i_1 =/= i_2)
+
 def $ilt_(N, U, i_1, i_2) = $bool(i_1 < i_2)
 def $ilt_(N, S, i_1, i_2) = $bool($signed_(N, i_1) < $signed_(N, i_2))
+
 def $igt_(N, U, i_1, i_2) = $bool(i_1 > i_2)
 def $igt_(N, S, i_1, i_2) = $bool($signed_(N, i_1) > $signed_(N, i_2))
+
 def $ile_(N, U, i_1, i_2) = $bool(i_1 <= i_2)
 def $ile_(N, S, i_1, i_2) = $bool($signed_(N, i_1) <= $signed_(N, i_2))
+
 def $ige_(N, U, i_1, i_2) = $bool(i_1 >= i_2)
 def $ige_(N, S, i_1, i_2) = $bool($signed_(N, i_1) >= $signed_(N, i_2))
 
@@ -113,6 +146,29 @@ def $fgt_(N, fN(N), fN(N)) : u32
 def $fle_(N, fN(N), fN(N)) : u32
 def $fge_(N, fN(N), fN(N)) : u32
 
+def $fadd_  hint(builtin)
+def $fsub_  hint(builtin)
+def $fmul_  hint(builtin)
+def $fdiv_  hint(builtin)
+def $fmin_  hint(builtin)
+def $fmax_  hint(builtin)
+
+def $fcopysign_ hint(builtin)
+def $fabs_      hint(builtin)
+def $fneg_      hint(builtin)
+def $fsqrt_     hint(builtin)
+def $fceil_     hint(builtin)
+def $ffloor_    hint(builtin)
+def $ftrunc_    hint(builtin)
+def $fnearest_  hint(builtin)
+
+def $feq_ hint(builtin)
+def $fne_ hint(builtin)
+def $flt_ hint(builtin)
+def $fgt_ hint(builtin)
+def $fle_ hint(builtin)
+def $fge_ hint(builtin)
+
 
 def $binop_(Inn, ADD, iN_1, iN_2) = $iadd_($size(Inn), iN_1, iN_2)
 def $binop_(Inn, SUB, iN_1, iN_2) = $isub_($size(Inn), iN_1, iN_2)

specification/wasm-2.0/3-numerics.spectec

@@ -64,6 +64,24 @@ def $fbytes_(N, fN(N)) : byte*                       hint(show $bytes_(F#%,%))
 def $nbytes_(numtype, num_(numtype)) : byte*         hint(show $bytes_(%,%))
 def $vbytes_(vectype, vec_(vectype)) : byte*         hint(show $bytes_(%,%))
 
+;; TODO(3, rossberg): implement numerics internally
+def $wrap__        hint(builtin)
+def $extend__      hint(builtin)
+def $trunc__       hint(builtin)
+def $trunc_sat__   hint(builtin)
+def $demote__      hint(builtin)
+def $promote__     hint(builtin)
+def $convert__     hint(builtin)
+def $narrow__      hint(builtin)
+def $reinterpret__ hint(builtin)
+
+def $ibits_  hint(builtin)
+def $fbits_  hint(builtin)
+def $ibytes_ hint(builtin)
+def $fbytes_ hint(builtin)
+def $nbytes_ hint(builtin)
+def $vbytes_ hint(builtin)
+
 
 def $invibytes_(N, byte*) : iN(N)
 def $invfbytes_(N, byte*) : fN(N)
@@ -108,30 +126,63 @@ def $isub_sat_(N, sx, iN(N), iN(N)) : iN(N)     hint(show $isub__sat_(%)^(%)#((%
 def $iavgr_(N, sx, iN(N), iN(N)) : iN(N)        hint(show $iavgr_(%)^(%)#((%,%)))
 def $iq15mulr_sat_(N, sx, iN(N), iN(N)) : iN(N) hint(show $iq15mulr__sat_(%)^(%)#((%,%)))
 
-;; TODO(3, rossberg): implement numerics internally
 def $iadd_(N, i_1, i_2) = $((i_1 + i_2) \ 2^N)
 def $isub_(N, i_1, i_2) = $((2^N + i_1 - i_2) \ 2^N)
 def $imul_(N, i_1, i_2) = $((i_1 * i_2) \ 2^N)
+
+def $idiv_ hint(builtin)
+def $irem_ hint(builtin)
+def $inot_ hint(builtin)
+def $irev_ hint(builtin)
+def $iand_ hint(builtin)
+def $iandnot_ hint(builtin)
+def $ior_  hint(builtin)
+def $ixor_ hint(builtin)
+def $ishl_ hint(builtin)
+def $ishr_ hint(builtin)
+def $irotl_ hint(builtin)
+def $irotr_ hint(builtin)
+def $iclz_  hint(builtin)
+def $ictz_  hint(builtin)
+def $ipopcnt_ hint(builtin)
+
 def $ieqz_(N, i_1) = $bool(i_1 = 0)
 def $inez_(N, i_1) = $bool(i_1 =/= 0)
+
 def $ieq_(N, i_1, i_2) = $bool(i_1 = i_2)
 def $ine_(N, i_1, i_2) = $bool(i_1 =/= i_2)
+
 def $ilt_(N, U, i_1, i_2) = $bool(i_1 < i_2)
 def $ilt_(N, S, i_1, i_2) = $bool($signed_(N, i_1) < $signed_(N, i_2))
+
 def $igt_(N, U, i_1, i_2) = $bool(i_1 > i_2)
 def $igt_(N, S, i_1, i_2) = $bool($signed_(N, i_1) > $signed_(N, i_2))
+
 def $ile_(N, U, i_1, i_2) = $bool(i_1 <= i_2)
 def $ile_(N, S, i_1, i_2) = $bool($signed_(N, i_1) <= $signed_(N, i_2))
+
 def $ige_(N, U, i_1, i_2) = $bool(i_1 >= i_2)
 def $ige_(N, S, i_1, i_2) = $bool($signed_(N, i_1) >= $signed_(N, i_2))
+
+def $ibitselect_ hint(builtin)
+
 def $iabs_(N, i_1) = i_1             -- if $signed_(N, i_1) >= 0
 def $iabs_(N, i_1) = $ineg_(N, i_1)  -- otherwise
+
+def $imin_ hint(builtin)
+def $imax_ hint(builtin)
+
 def $ineg_(N, i_1) = $invsigned_(N, $(- $signed_(N, i_1)))
+
 def $iadd_sat_(N, U, i_1, i_2) = $sat_u_(N, $(i_1 + i_2))
 def $iadd_sat_(N, S, i_1, i_2) = $invsigned_(N, $sat_s_(N, $($signed_(N, i_1) + $signed_(N, i_2))))
+
 def $isub_sat_(N, U, i_1, i_2) = $sat_u_(N, $(i_1 - i_2))
 def $isub_sat_(N, S, i_1, i_2) = $invsigned_(N, $sat_s_(N, $($signed_(N, i_1) - $signed_(N, i_2))))
 
+def $iavgr_ hint(builtin)
+def $iq15mulr_sat_ hint(builtin)
+
 def $fadd_(N, fN(N), fN(N)) : fN(N)*
 def $fsub_(N, fN(N), fN(N)) : fN(N)*
 def $fmul_(N, fN(N), fN(N)) : fN(N)*
@@ -155,6 +206,31 @@ def $fgt_(N, fN(N), fN(N)) : u32
 def $fle_(N, fN(N), fN(N)) : u32
 def $fge_(N, fN(N), fN(N)) : u32
 
+def $fadd_  hint(builtin)
+def $fsub_  hint(builtin)
+def $fmul_  hint(builtin)
+def $fdiv_  hint(builtin)
+def $fmin_  hint(builtin)
+def $fmax_  hint(builtin)
+def $fpmin_ hint(builtin)
+def $fpmax_ hint(builtin)
+
+def $fcopysign_ hint(builtin)
+def $fabs_      hint(builtin)
+def $fneg_      hint(builtin)
+def $fsqrt_     hint(builtin)
+def $fceil_     hint(builtin)
+def $ffloor_    hint(builtin)
+def $ftrunc_    hint(builtin)
+def $fnearest_  hint(builtin)
+
+def $feq_ hint(builtin)
+def $fne_ hint(builtin)
+def $flt_ hint(builtin)
+def $fgt_ hint(builtin)
+def $fle_ hint(builtin)
+def $fge_ hint(builtin)
+
 def $binop_(Inn, ADD, iN_1, iN_2) = $iadd_($sizenn(Inn), iN_1, iN_2)
 def $binop_(Inn, SUB, iN_1, iN_2) = $isub_($sizenn(Inn), iN_1, iN_2)
 def $binop_(Inn, MUL, iN_1, iN_2) = $imul_($sizenn(Inn), iN_1, iN_2)
@@ -229,6 +305,7 @@ def $unpacknum_(packtype, c) = $extend__($psize(packtype), $size($unpack(packtyp
 ;; Vectors
 
 def $lanes_(shape, vec_(V128)) : lane_($lanetype(shape))*
+def $lanes_ hint(builtin)
 
 def $invlanes_(shape, lane_($lanetype(shape))*) : vec_(V128)
     hint(show $lanes^(-1)#_%#(%,%))

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

@@ -2,4 +2,4 @@
 ;; Profiles
 ;;
 
-def $ND : bool  ;; non-determinism
+def $ND : bool hint(builtin)  ;; non-determinism

specification/wasm-3.0/3.0-numerics.relaxed.spectec

@@ -15,12 +15,12 @@ def $relaxed4(i, syntax X, X_1, X_2, X_3, X_4) = (X_1 X_2 X_3 X_4)[i]  -- if $ND
 def $relaxed4(i, syntax X, X_1, X_2, X_3, X_4) = (X_1 X_2 X_3 X_4)[0]  -- otherwise
 
 
-def $R_fmadd : relaxed2
-def $R_fmin : relaxed4
-def $R_fmax : relaxed4
-def $R_idot : relaxed2
-def $R_iq15mulr : relaxed2
-def $R_trunc_u : relaxed4
-def $R_trunc_s : relaxed2
-def $R_swizzle : relaxed2
-def $R_laneselect : relaxed2
+def $R_fmadd : relaxed2      hint(builtin)
+def $R_fmin : relaxed4       hint(builtin)
+def $R_fmax : relaxed4       hint(builtin)
+def $R_idot : relaxed2       hint(builtin)
+def $R_iq15mulr : relaxed2   hint(builtin)
+def $R_trunc_u : relaxed4    hint(builtin)
+def $R_trunc_s : relaxed2    hint(builtin)
+def $R_swizzle : relaxed2    hint(builtin)
+def $R_laneselect : relaxed2 hint(builtin)

specification/wasm-3.0/3.1-numerics.scalar.spectec

@@ -18,6 +18,16 @@ def $vbytes_(vectype, vec_(vectype)) : byte*         hint(show $bytes_(%,%))
 def $zbytes_(storagetype, lit_(storagetype)) : byte* hint(show $bytes_(%,%))
 def $cbytes_(Cnn, lit_(Cnn)) : byte*                 hint(show $bytes_(%,%))
 
+;; TODO(3, rossberg): implement numerics internally
+def $ibits_  hint(builtin)
+def $fbits_  hint(builtin)
+def $ibytes_ hint(builtin)
+def $fbytes_ hint(builtin)
+def $nbytes_ hint(builtin)
+def $vbytes_ hint(builtin)
+def $zbytes_ hint(builtin)
+def $cbytes_ hint(builtin)
+
 
 def $invibytes_(N, byte*) : iN(N) hint(show $bytes_($IN(%))^(-1)#((%)))
 def $invfbytes_(N, byte*) : fN(N) hint(show $bytes_($FN(%))^(-1)#((%)))
@@ -122,10 +132,13 @@ def $ineg_(N, i_1) = $invsigned_(N, $(- $signed_(N, i_1)))
 def $iabs_(N, i_1) = i_1             -- if $signed_(N, i_1) >= 0
 def $iabs_(N, i_1) = $ineg_(N, i_1)  -- otherwise
 
+def $iclz_ hint(builtin)
 ;;def $iclz_(N, i_1) = k               -- if $ibits_(N, i_1) = (0)^k 1 d*
 
+def $ictz_ hint(builtin)
 ;;def $ictz_(N, i_1) = k               -- if $ibits_(N, i_1) = d* 1 (0)^k
 
+def $ipopcnt_ hint(builtin)
 ;;def $ipopcnt_(N, i_1) = k            -- if $ibits_(N, i_1) = (0* 1)^k 0*
 
 def $iextend_(N, M, U, i) = $(i \ 2^M)
@@ -138,23 +151,27 @@ def $isub_(N, i_1, i_2) = $((2^N + i_1 - i_2) \ 2^N)
 
 def $imul_(N, i_1, i_2) = $((i_1 * i_2) \ 2^N)
 
+def $idiv_ hint(builtin)
 ;;def $idiv_(N, U, i_1, 0)   = eps
 ;;def $idiv_(N, U, i_1, i_2) = $($int(i_1 / i_2))
 ;;def $idiv_(N, S, i_1, 0)   = eps
 ;;def $idiv_(N, S, i_1, i_2) = eps  -- if $($signed_(N, i_1) / $signed_(N, i_2)) = 2^(N-1)
 ;;def $idiv_(N, S, i_1, i_2) = $($invsigned_(N, $int($signed_(N, i_1) / $signed_(N, i_2))))
 
+def $irem_ hint(builtin)
 ;;def $irem_(N, U, i_1, 0)   = eps
 ;;def $irem_(N, U, i_1, i_2) = $(i_1 - i_2 * $int(i_1 / i_2))
 ;;def $irem_(N, S, i_1, 0)   = eps
 ;;def $irem_(N, S, i_1, i_2) = $($invsigned_(N, j_1 - j_2 * $int(j_1 / f_2)))
 ;;                             -- if j_1 = $signed_(N, i_1) /\ j_2 = $signed_(N, i_2)
 
+def $imin_ hint(builtin)
 ;;def $imin_(N, U, i_1, i_2) = i_1  -- if i_1 <= i_2
 ;;def $imin_(N, U, i_1, i_2) = i_2  -- otherwise
 ;;def $imin_(N, S, i_1, i_2) = i_1  -- if $signed_(N, i_1) <= $signed_(N, i_2)
 ;;def $imin_(N, S, i_1, i_2) = i_2  -- otherwise
 
+def $imax_ hint(builtin)
 ;;def $imax_(N, U, i_1, i_2) = i_1  -- if i_1 >= i_2
 ;;def $imax_(N, U, i_1, i_2) = i_2  -- otherwise
 ;;def $imax_(N, S, i_1, i_2) = i_1  -- if $signed_(N, i_1) >= $signed_(N, i_2)
@@ -166,6 +183,24 @@ def $iadd_sat_(N, S, i_1, i_2) = $invsigned_(N, $sat_s_(N, $($signed_(N, i_1) +
 def $isub_sat_(N, U, i_1, i_2) = $sat_u_(N, $(i_1 - i_2))
 def $isub_sat_(N, S, i_1, i_2) = $invsigned_(N, $sat_s_(N, $($signed_(N, i_1) - $signed_(N, i_2))))
 
+def $iq15mulr_sat_     hint(builtin)
+def $irelaxed_q15mulr_ hint(builtin)
+def $iavgr_            hint(builtin)
+
+def $inot_             hint(builtin)
+def $irev_             hint(builtin)
+def $iand_             hint(builtin)
+def $iandnot_          hint(builtin)
+def $ior_              hint(builtin)
+def $ixor_             hint(builtin)
+def $ishl_             hint(builtin)
+def $ishr_             hint(builtin)
+def $irotl_            hint(builtin)
+def $irotr_            hint(builtin)
+
+def $ibitselect_          hint(builtin)
+def $irelaxed_laneselect_ hint(builtin)
+
 
 def $ieqz_(N, i_1) = $bool(i_1 = 0)
 
@@ -224,6 +259,36 @@ def $frelaxed_nmadd_(N, fN(N), fN(N), fN(N)) : fN(N)*   hint(show $frelaxed__nma
 
 ;; TODO(3, rossberg): implement numerics internally
 
+def $fabs_     hint(builtin)
+def $fneg_     hint(builtin)
+def $fsqrt_    hint(builtin)
+def $fceil_    hint(builtin)
+def $ffloor_   hint(builtin)
+def $ftrunc_   hint(builtin)
+def $fnearest_ hint(builtin)
+
+def $fadd_     hint(builtin)
+def $fsub_     hint(builtin)
+def $fmul_     hint(builtin)
+def $fdiv_     hint(builtin)
+def $fmin_     hint(builtin)
+def $fmax_     hint(builtin)
+def $fpmin_    hint(builtin)
+def $fpmax_    hint(builtin)
+def $frelaxed_min_ hint(builtin)
+def $frelaxed_max_ hint(builtin)
+def $fcopysign_    hint(builtin)
+
+def $feq_ hint(builtin)
+def $fne_ hint(builtin)
+def $flt_ hint(builtin)
+def $fgt_ hint(builtin)
+def $fle_ hint(builtin)
+def $fge_ hint(builtin)
+
+def $frelaxed_madd_  hint(builtin)
+def $frelaxed_nmadd_ hint(builtin)
+
 
 ;; Conversions
 
@@ -242,6 +307,18 @@ def $reinterpret__(numtype_1, numtype_2, num_(numtype_1)) : num_(numtype_2)
 
 ;; TODO(3, rossberg): implement numerics internally
 
+def $wrap__          hint(builtin)
+def $extend__        hint(builtin)
+def $trunc__         hint(builtin)
+def $trunc_sat__     hint(builtin)
+def $relaxed_trunc__ hint(builtin)
+def $demote__        hint(builtin)
+def $promote__       hint(builtin)
+def $convert__       hint(builtin)
+def $narrow__        hint(builtin)
+
+def $reinterpret__   hint(builtin)
+
 
 ;; Packed numbers
 

specification/wasm-3.0/3.2-numerics.vector.spectec

@@ -9,6 +9,9 @@
 
 def $lanes_(shape, vec_(V128)) : lane_($lanetype(shape))*
 
+;; TODO(3, rossberg): implement numerics internally
+def $lanes_ hint(builtin)
+
 def $invlanes_(shape, lane_($lanetype(shape))*) : vec_(V128)
     hint(show $lanes_(%)^(-1)#((%)))
 def $invlanes_(sh, c*) = vc  -- if c* = $lanes_(sh, vc)