Add algorithmic backend

spectec/spec/wasm-3.0/1-syntax.watsup

@@ -253,30 +253,10 @@ var testop : testop_numtype
 var relop : relop_numtype
 
 
-syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32}
+syntax memop hint(desc "memory operator") = {ALIGN u32, OFFSET u32}
 
-var marg : memarg
+var mo : memop
 
-syntax lanetype hint(desc "lane type") =
-  | packedtype | numtype
-syntax lanesize hint(desc "lane size") = nat
-
-var lnt : lanetype
-var lns : lanesize
-syntax shape hint(desc "shape") = lanetype X lanesize
-
-var psl : nat
-var psr : nat
-
-syntax packshape =
-  | PACKSHAPE nat nat
-
-var psh : packshape
-
-syntax half = | LOW | HIGH
-var hf : half
-
-var sh : shape
 
 syntax unopVVXX = | NOT
 syntax binopVVXX = | AND | ANDNOT | OR | XOR
@@ -370,30 +350,41 @@ syntax instr/numeric hint(desc "numeric instruction") = ...
   | CVTOP numtype cvtop numtype sx?  hint(show %.%#_#%#_#%)
   | ...
 
+syntax lanetype hint(desc "lane type") = | packedtype | numtype
+syntax lanesize hint(desc "lane size") = nat
+syntax shape hint(desc "shape") = lanetype X lanesize
+syntax half = | LOW | HIGH
+
+var lnt : lanetype
+var lns : lanesize
+var sh : shape
+var hf : half
+
 syntax instr/vector hint(desc "vector instruction") = ...
-  | VVCONST vectype c_vectype                                        hint(show %.CONST %)
-  | VVUNOP vectype unop_vvectype                                     hint(show %.%)
-  | VVBINOP vectype binop_vvectype                                   hint(show %.%)
-  | VVTERNOP vectype ternop_vvectype                                 hint(show %.%)
-  | VVTESTOP vectype testop_vvectype                                 hint(show %.%)
-  | SWIZZLE shape
-  | SHUFFLE shape laneidx*
-  | SPLAT shape                                                     hint(show %.SPLAT)
-  | EXTRACT_LANE shape sx? laneidx                                  hint(show %.EXTRACT#_#LANE#_#% %)
-  | REPLACE_LANE shape laneidx                                      hint(show %.REPLACE#_#LANE %)
-  | VUNOP shape unop_vectype
-  | VBINOP shape binop_vectype
-  | VRELOP shape relop_vectype
-  | VISHIFTOP shape shiftop_vectype
-  | ALL_TRUE shape                                                  hint(show %.ALL_TRUE)
-  | BITMASK shape
-  | NARROW shape shape sx
-  | VCVTOP shape cvtop_vectype half? shape sx? zero
-  | EXTMUL_HALF shape half shape sx
-  | DOT shape shape sx
-  | EXTADD_PAIRWISE shape shape sx
+  | VVCONST vectype c_vectype                                 hint(show %.CONST %)
+  | VVUNOP vectype unop_vvectype                              hint(show %.%)
+  | VVBINOP vectype binop_vvectype                            hint(show %.%)
+  | VVTERNOP vectype ternop_vvectype                          hint(show %.%)
+  | VVTESTOP vectype testop_vvectype                          hint(show %.%)
+  | VSWIZZLE shape                                            hint(show %.VSWIZZLE)
+  | VSHUFFLE shape laneidx*                                   hint(show %.VSHUFFLE %)
+  | VSPLAT shape                                              hint(show %.VSPLAT)
+  | VEXTRACT_LANE shape sx? laneidx                           hint(show %.VEXTRACT#_#LANE#_#% %)
+  | VREPLACE_LANE shape laneidx                               hint(show %.VREPLACE#_#LANE %)
+  | VUNOP shape unop_vectype                                  hint(show %.%)
+  | VBINOP shape binop_vectype                                hint(show %.%)
+  | VRELOP shape relop_vectype                                hint(show %.%)
+  | VISHIFTOP shape shiftop_vectype                           hint(show %.%)
+  | VALL_TRUE shape                                           hint(show %.VALL_TRUE)
+  | VBITMASK shape                                            hint(show %.VBITMASK)
+  | VNARROW shape shape sx                                    hint(show %.VNARROW#_#%#_#%)
+  | VCVTOP shape cvtop_vectype half? shape sx? zero           hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%) hint(show %.%#_#%#_#%#_#%#_#%)
+  | VEXTMUL shape half shape sx                               hint(show %.VEXTMUL#_#%#_#%#_#%)
+  | VDOT shape shape sx                                       hint(show %.VDOT#_#%#_#%)
+  | VEXTADD_PAIRWISE shape shape sx                           hint(show %.VEXTADD_PAIRWISE#_#%#_#%)
   | ...
 
+
 syntax instr/reference hint(desc "reference instruction") = ...
   | REF.NULL heaptype
   | REF.I31
@@ -449,8 +440,12 @@ syntax instr/table hint(desc "table instruction") = ...
   | ELEM.DROP elemidx
   | ...
 
+
+syntax packshape = nat X nat
 syntax vloadop =
-  | LOAD memarg | SHAPE packshape sx memarg | SPLAT nat memarg | ZERO nat memarg
+  | SHAPE packshape sx  hint(show %#_#%)
+  | SPLAT nat           hint(show %#_#SPLAT)
+  | ZERO nat            hint(show %#_#ZERO)
 
 syntax instr/memory hint(desc "memory instruction") = ...
   | MEMORY.SIZE memidx
@@ -459,12 +454,12 @@ syntax instr/memory hint(desc "memory instruction") = ...
   | MEMORY.COPY memidx memidx
   | MEMORY.INIT memidx dataidx
   | DATA.DROP dataidx
-  | LOAD numtype (n _ sx)? memidx memarg  hint(show %.LOAD % %)  hint(show %.LOAD#% % %)
-  | STORE numtype n? memidx memarg        hint(show %.STORE % %) hint(show %.STORE#% % %)
-  | VLOAD vloadop memidx
-  | VLOAD_LANE n memidx memarg laneidx
-  | VSTORE memidx memarg
-  | VSTORE_LANE n memidx memarg laneidx
+  | LOAD numtype (n _ sx)? memidx memop  hint(show %.LOAD % %)    hint(show %.LOAD#% % %)
+  | STORE numtype n? memidx memop        hint(show %.STORE % %)   hint(show %.STORE#% % %)
+  | VLOAD vloadop? memidx memop          hint(show V128.LOAD % %) hint(show V128.LOAD#% % %)
+  | VLOAD_LANE n memidx memop laneidx    hint(show V128.LOAD#%#_#LANE % % %)
+  | VSTORE memidx memop                  hint(show V128.STORE % %)
+  | VSTORE_LANE n memidx memop laneidx   hint(show V128.STORE#%#_#LANE % % %)
 
 syntax expr hint(desc "expression") =
   instr*

spectec/spec/wasm-3.0/2-syntax-aux.watsup

@@ -246,5 +246,5 @@ def $memsxt(externtype et*) = $memsxt(et*)  -- otherwise
 
 ;; Shorthands for Instructions
 
-def $memarg0 : memarg  hint(show )
-def $memarg0 = {ALIGN 0, OFFSET 0}
+def $memop0 : memop  hint(show )
+def $memop0 = {ALIGN 0, OFFSET 0}

spectec/spec/wasm-3.0/6-typing.watsup

@@ -772,22 +772,22 @@ rule Instr_ok/vvternop:
 rule Instr_ok/vvtestop:
   C |- VVTESTOP vt vvtestop : V128 -> I32
 
-rule Instr_ok/swizzle:
-  C |- SWIZZLE sh : V128 V128 -> V128
+rule Instr_ok/vswizzle:
+  C |- VSWIZZLE sh : V128 V128 -> V128
 
-rule Instr_ok/shuffle:
-  C |- SHUFFLE sh laneidx* : V128 V128 -> V128
+rule Instr_ok/vshuffle:
+  C |- VSHUFFLE sh laneidx* : V128 V128 -> V128
   -- (if $(laneidx<$dim(sh) * 2))*
 
-rule Instr_ok/splat:
-  C |- SPLAT sh : $unpacked(sh) -> V128
+rule Instr_ok/vsplat:
+  C |- VSPLAT sh : $unpacked(sh) -> V128
 
-rule Instr_ok/extract_lane:
-  C |- EXTRACT_LANE sh sx? laneidx : V128 -> $unpacked(sh)
+rule Instr_ok/vextract_lane:
+  C |- VEXTRACT_LANE sh sx? laneidx : V128 -> $unpacked(sh)
   -- if laneidx < $dim(sh)
 
-rule Instr_ok/replace_lane:
-  C |- REPLACE_LANE sh laneidx : V128 $unpacked(sh) -> V128
+rule Instr_ok/vreplace_lane:
+  C |- VREPLACE_LANE sh laneidx : V128 $unpacked(sh) -> V128
   -- if laneidx < $dim(sh)
 
 rule Instr_ok/vunop:
@@ -803,25 +803,25 @@ rule Instr_ok/vishiftop:
   C |- VISHIFTOP sh vishiftop : V128 V128 -> V128
 
 rule Instr_ok/vtestop:
-  C |- ALL_TRUE sh : V128 -> I32
+  C |- VALL_TRUE sh : V128 -> I32
 
 rule Instr_ok/vcvtop:
   C |- VCVTOP sh vcvtop hf? sh sx? zero : V128 -> V128
 
-rule Instr_ok/narrow:
-  C |- NARROW sh sh sx : V128 V128 -> V128
+rule Instr_ok/vnarrow:
+  C |- VNARROW sh sh sx : V128 V128 -> V128
 
-rule Instr_ok/bitmask:
-  C |- BITMASK sh : V128 -> I32
+rule Instr_ok/vbitmask:
+  C |- VBITMASK sh : V128 -> I32
 
-rule Instr_ok/dot:
-  C |- DOT sh sh sx : V128 V128 -> V128
+rule Instr_ok/vdot:
+  C |- VDOT sh sh sx : V128 V128 -> V128
 
-rule Instr_ok/extmul_half:
-  C |- EXTMUL_HALF sh half sh sx : V128 V128 -> V128
+rule Instr_ok/vextmul:
+  C |- VEXTMUL sh half sh sx : V128 V128 -> V128
 
-rule Instr_ok/extadd_pairwise:
-  C |- EXTADD_PAIRWISE sh sh sx : V128 -> V128
+rule Instr_ok/vextadd_pairwise:
+  C |- VEXTADD_PAIRWISE sh sh sx : V128 -> V128
 
 
 ;; Structure instructions
@@ -1025,17 +1025,17 @@ rule Instr_ok/store:
   -- if n? = eps \/ nt = inn
 
 rule Instr_ok/vload:
-  C |- VLOAD (SHAPE (PACKSHAPE psl psr) sx {ALIGN n_A, OFFSET n_O}) x : I32 -> V128
+  C |- VLOAD (SHAPE (M X N) sx) x {ALIGN n_A, OFFSET n_O} : I32 -> V128
   -- if C.MEM[x] = mt
-  -- if $(2^(n_A) <= psl/8 * psr)
+  -- if $(2^(n_A) <= M/8 * N)
 
 rule Instr_ok/vload-splat:
-  C |- VLOAD (SPLAT n {ALIGN n_A, OFFSET n_O}) x : I32 -> V128
+  C |- VLOAD (SPLAT n) x {ALIGN n_A, OFFSET n_O} : I32 -> V128
   -- if C.MEM[x] = mt
   -- if $(2^(n_A) <= n/8)
 
 rule Instr_ok/vload-zero:
-  C |- VLOAD (ZERO n {ALIGN n_A, OFFSET n_O}) x : I32 -> V128
+  C |- VLOAD (ZERO n) x {ALIGN n_A, OFFSET n_O} : I32 -> V128
   -- if C.MEM[x] = mt
   -- if $(2^(n_A) < n/8)