;;
;; Auxiliaries
;;

;; Vectors

grammar Blist(grammar BX : el) : el* =
  | n:Bu32 (el:BX)^n => el^n


;;
;; Values
;;

;; Numbers

grammar Bbyte : byte = 0x00 | ... | 0xFF

grammar BuN(N) : uN(N) hint(show Bu#%) =
  | n:Bbyte                 => n                       -- if $(n < 2^7 /\ n < 2^N)
  | n:Bbyte m:BuN(($(N-7))) => $(2^7 * m + (n - 2^7))  -- if $(n >= 2^7 /\ N > 7)

grammar BsN(N) : sN(N) hint(show Bs#%) =
  | n:Bbyte                 => n                       -- if $(n < 2^6 /\ n < 2^(N-1))
  | n:Bbyte                 => $(n - 2^7)              -- if $(2^6 <= n < 2^7 /\ n >= 2^7 - 2^(N-1))
  | n:Bbyte i:BsN(($(N-7))) => $(2^7 * i + (n - 2^7))  -- if $(n >= 2^7 /\ N > 7)

grammar BiN(N) : iN(N) hint(show Bi#%) =
  | i:BsN(N)                => $inv_signed_(N, i)


grammar BfN(N) : fN(N) hint(show Bf#%) =
  | b*:Bbyte^(N/8)  => $inv_fbytes_(N, b*)


grammar Bu32 : u32 = n:BuN(32) => n
grammar Bu64 : u64 = n:BuN(64) => n
grammar Bs33 : s33 = i:BsN(33) => i

grammar Bf32 : f32 = p:BfN(32) => p
grammar Bf64 : f64 = p:BfN(64) => p


;; Names

var ch : char

;; def $utf8(char*) : byte*
def $utf8(ch) = b  -- if ch < U+0080 /\ ch = b
def $utf8(ch) = b_1 b_2  -- if U+0080 <= ch < U+0800 /\ ch = $(2^6*(b_1 - 0xC0) + (b_2 - 0x80))
def $utf8(ch) = b_1 b_2 b_3  -- if (U+0800 <= ch < U+D800 \/ U+E000 <= ch < U+10000) /\ ch = $(2^12*(b_1 - 0xE0) + 2^6*(b_2 - 0x80) + (b_3 - 0x80))
def $utf8(ch) = b_1 b_2 b_3 b_4  -- if (U+10000 <= ch < U+11000) /\ ch = $(2^18*(b_1 - 0xF0) + 2^12*(b_2 - 0x80) + 2^6*(b_3 - 0x80) + (b_4 - 0x80))
def $utf8(ch*) = $concat_(byte, $utf8(ch)*)

grammar Bname : name =
  | b*:Blist(Bbyte) => name  -- if $utf8(name) = b*


;; Indices

grammar Btypeidx : typeidx = x:Bu32 => x
grammar Bfuncidx : funcidx = x:Bu32 => x
grammar Bglobalidx : globalidx = x:Bu32 => x
grammar Btableidx : tableidx = x:Bu32 => x
grammar Bmemidx : memidx = x:Bu32 => x
grammar Belemidx : elemidx = x:Bu32 => x
grammar Bdataidx : dataidx = x:Bu32 => x
grammar Blocalidx : localidx = x:Bu32 => x
grammar Blabelidx : labelidx = x:Bu32 => x

grammar Bexternidx : externidx =
  | 0x00 x:Bfuncidx => FUNC x
  | 0x01 x:Btableidx => TABLE x
  | 0x02 x:Bmemidx => MEM x
  | 0x03 x:Bglobalidx => GLOBAL x


;;
;; Types
;;

;; Value types

grammar Bnumtype : numtype =
  | 0x7F => I32
  | 0x7E => I64
  | 0x7D => F32
  | 0x7C => F64

grammar Bvectype : vectype =
  | 0x7B => V128

grammar Breftype : reftype =
  | 0x70 => FUNCREF
  | 0x6F => EXTERNREF

grammar Bvaltype : valtype =
  | nt:Bnumtype => nt
  | vt:Bvectype => vt
  | rt:Breftype => rt


grammar Bresulttype : resulttype =
  | t*:Blist(Bvaltype) => t*


;; Type definitions

grammar Bfunctype : functype =
  | 0x60 t_1*:Bresulttype t_2*:Bresulttype => t_1* -> t_2*


;; External types

grammar Bmut : mut =
  | 0x00 => eps
  | 0x01 => MUT

grammar Blimits : limits =
  | 0x00 n:Bu32 => `[n .. eps]
  | 0x01 n:Bu32 m:Bu32 => `[n .. m]

grammar Bglobaltype : globaltype =
  | t:Bvaltype mut:Bmut => mut t

grammar Btabletype : tabletype =
  | rt:Breftype lim:Blimits => lim rt

grammar Bmemtype : memtype =
  | lim:Blimits => lim PAGE


grammar Bexterntype : externtype =
  | 0x00 ft:Bfunctype => FUNC ft  ;; TODO: typeidx
  | 0x01 tt:Btabletype => TABLE tt
  | 0x02 mt:Bmemtype => MEM mt
  | 0x03 gt:Bglobaltype => GLOBAL gt


;;
;; Instructions
;;

;; Block types

grammar Bblocktype : blocktype =
  | 0x40 => _RESULT eps
  | t:Bvaltype => _RESULT t
  | i:Bs33 => _IDX x  -- if i >= 0 /\ i = x


;; Control instructions

grammar Binstr/control : instr =
  | 0x00 => UNREACHABLE
  | 0x01 => NOP
  | 0x02 bt:Bblocktype (in:Binstr)* 0x0B => BLOCK bt in*
  | 0x03 bt:Bblocktype (in:Binstr)* 0x0B => LOOP bt in*
  | 0x04 bt:Bblocktype (in:Binstr)* 0x0B => IF bt in* ELSE eps
  | 0x04 bt:Bblocktype (in_1:Binstr)* 0x05 (in_2:Binstr)* 0x0B => IF bt in_1* ELSE in_2*
  | 0x0C l:Blabelidx => BR l
  | 0x0D l:Blabelidx => BR_IF l
  | 0x0E l*:Blist(Blabelidx) l_N:Blabelidx => BR_TABLE l* l_N
  | 0x0F => RETURN
  | 0x10 x:Bfuncidx => CALL x
  | 0x11 y:Btypeidx x:Btableidx => CALL_INDIRECT x y
  | ...


;; Reference instructions

grammar Binstr/reference : instr = ...
  | 0xD0 rt:Breftype => REF.NULL rt
  | 0xD1 => REF.IS_NULL
  | 0xD2 x:Bfuncidx => REF.FUNC x
  | ...


;; Parametric instructions

grammar Binstr/parametric : instr = ...
  | 0x1A => DROP
  | 0x1B => SELECT eps
  | 0x1C ts:Blist(Bvaltype) => SELECT ts
  | ...


;; Variable instructions

grammar Binstr/variable : instr = ...
  | 0x20 x:Blocalidx => LOCAL.GET x
  | 0x21 x:Blocalidx => LOCAL.SET x
  | 0x22 x:Blocalidx => LOCAL.TEE x
  | 0x23 x:Bglobalidx => GLOBAL.GET x
  | 0x24 x:Bglobalidx => GLOBAL.SET x
  | ...


;; Table instructions

grammar Binstr/table : instr = ...
  | 0x25 x:Btableidx => TABLE.GET x
  | 0x26 x:Btableidx => TABLE.SET x
  | 0xFC 12:Bu32 y:Belemidx x:Btableidx => TABLE.INIT x y
  | 0xFC 13:Bu32 x:Belemidx => ELEM.DROP x
  | 0xFC 14:Bu32 x_1:Btableidx x_2:Btableidx => TABLE.COPY x_1 x_2
  | 0xFC 15:Bu32 x:Btableidx => TABLE.GROW x
  | 0xFC 16:Bu32 x:Btableidx => TABLE.SIZE x
  | 0xFC 17:Bu32 x:Btableidx => TABLE.FILL x
  | ...


;; Memory instructions

grammar Bmemarg : memarg =
  | n:Bu32 m:Bu32 => {ALIGN n, OFFSET m}

grammar Binstr/memory : instr = ...
  | 0x28 ao:Bmemarg => LOAD I32 ao
  | 0x29 ao:Bmemarg => LOAD I64 ao
  | 0x2A ao:Bmemarg => LOAD F32 ao
  | 0x2B ao:Bmemarg => LOAD F64 ao
  | 0x2C ao:Bmemarg => LOAD I32 (8 _ S) ao
  | 0x2D ao:Bmemarg => LOAD I32 (8 _ U) ao
  | 0x2E ao:Bmemarg => LOAD I32 (16 _ S) ao
  | 0x2F ao:Bmemarg => LOAD I32 (16 _ U) ao
  | 0x30 ao:Bmemarg => LOAD I64 (8 _ S) ao
  | 0x31 ao:Bmemarg => LOAD I64 (8 _ U) ao
  | 0x32 ao:Bmemarg => LOAD I64 (16 _ S) ao
  | 0x33 ao:Bmemarg => LOAD I64 (16 _ U) ao
  | 0x34 ao:Bmemarg => LOAD I64 (32 _ S) ao
  | 0x35 ao:Bmemarg => LOAD I64 (32 _ U) ao
  | 0x36 ao:Bmemarg => STORE I32 ao
  | 0x37 ao:Bmemarg => STORE I64 ao
  | 0x38 ao:Bmemarg => STORE F32 ao
  | 0x39 ao:Bmemarg => STORE F64 ao
  | 0x3A ao:Bmemarg => STORE I32 8 ao
  | 0x3B ao:Bmemarg => STORE I32 16 ao
  | 0x3C ao:Bmemarg => STORE I64 8 ao
  | 0x3D ao:Bmemarg => STORE I64 16 ao
  | 0x3E ao:Bmemarg => STORE I64 32 ao
  | 0x3F 0x00 => MEMORY.SIZE
  | 0x40 0x00 => MEMORY.GROW
  | 0xFC 8:Bu32 x:Bdataidx 0x00 => MEMORY.INIT x
  | 0xFC 9:Bu32 x:Bdataidx => DATA.DROP x
  | 0xFC 10:Bu32 0x00 0x00 => MEMORY.COPY
  | 0xFC 11:Bu32 0x00 => MEMORY.FILL
  | ...


;; Numeric instructions

grammar Binstr/numeric-const : instr = ...
  | 0x41 n:Bu32 => CONST I32 n
  | 0x42 n:Bu64 => CONST I64 n
  | 0x43 p:Bf32 => CONST F32 p
  | 0x44 p:Bf64 => CONST F64 p
  | ...

grammar Binstr/numeric-test-i32 : instr = ...
  | 0x45 => TESTOP I32 EQZ
  | ...

grammar Binstr/numeric-rel-i32 : instr = ...
  | 0x46 => RELOP I32 EQ
  | 0x47 => RELOP I32 NE
  | 0x48 => RELOP I32 (LT S)
  | 0x49 => RELOP I32 (LT U)
  | 0x4A => RELOP I32 (GT S)
  | 0x4B => RELOP I32 (GT U)
  | 0x4C => RELOP I32 (LE S)
  | 0x4D => RELOP I32 (LE U)
  | 0x4E => RELOP I32 (GE S)
  | 0x4F => RELOP I32 (GE U)
  | ...

grammar Binstr/numeric-test-i64 : instr = ...
  | 0x50 => TESTOP I64 EQZ
  | ...

grammar Binstr/numeric-rel-i64 : instr = ...
  | 0x51 => RELOP I64 EQ
  | 0x52 => RELOP I64 NE
  | 0x53 => RELOP I64 (LT S)
  | 0x54 => RELOP I64 (LT U)
  | 0x55 => RELOP I64 (GT S)
  | 0x56 => RELOP I64 (GT U)
  | 0x57 => RELOP I64 (LE S)
  | 0x58 => RELOP I64 (LE U)
  | 0x59 => RELOP I64 (GE S)
  | 0x5A => RELOP I64 (GE U)
  | ...

grammar Binstr/numeric-rel-f32 : instr = ...
  | 0x5B => RELOP F32 EQ
  | 0x5C => RELOP F32 NE
  | 0x5D => RELOP F32 LT
  | 0x5E => RELOP F32 GT
  | 0x5F => RELOP F32 LE
  | 0x60 => RELOP F32 GE
  | ...

grammar Binstr/numeric-rel-f64 : instr = ...
  | 0x61 => RELOP F64 EQ
  | 0x62 => RELOP F64 NE
  | 0x63 => RELOP F64 LT
  | 0x64 => RELOP F64 GT
  | 0x65 => RELOP F64 LE
  | 0x66 => RELOP F64 GE
  | ...

grammar Binstr/numeric-un-i32 : instr = ...
  | 0x67 => UNOP I32 CLZ
  | 0x68 => UNOP I32 CTZ
  | 0x69 => UNOP I32 POPCNT
  | ...

grammar Binstr/numeric-bin-i32 : instr = ...
  | 0x6A => BINOP I32 ADD
  | 0x6B => BINOP I32 SUB
  | 0x6C => BINOP I32 MUL
  | 0x6D => BINOP I32 (DIV S)
  | 0x6E => BINOP I32 (DIV U)
  | 0x6F => BINOP I32 (REM S)
  | 0x70 => BINOP I32 (REM U)
  | 0x71 => BINOP I32 AND
  | 0x72 => BINOP I32 OR
  | 0x73 => BINOP I32 XOR
  | 0x74 => BINOP I32 SHL
  | 0x75 => BINOP I32 (SHR S)
  | 0x76 => BINOP I32 (SHR U)
  | 0x77 => BINOP I32 ROTL
  | 0x78 => BINOP I32 ROTR
  | ...

grammar Binstr/numeric-un-i64 : instr = ...
  | 0x79 => UNOP I64 CLZ
  | 0x7A => UNOP I64 CTZ
  | 0x7B => UNOP I64 POPCNT
  | ...

grammar Binstr/numeric-bin-i64 : instr = ...
  | 0x7C => BINOP I64 ADD
  | 0x7D => BINOP I64 SUB
  | 0x7E => BINOP I64 MUL
  | 0x7F => BINOP I64 (DIV S)
  | 0x80 => BINOP I64 (DIV U)
  | 0x81 => BINOP I64 (REM S)
  | 0x82 => BINOP I64 (REM U)
  | 0x83 => BINOP I64 AND
  | 0x84 => BINOP I64 OR
  | 0x85 => BINOP I64 XOR
  | 0x86 => BINOP I64 SHL
  | 0x87 => BINOP I64 (SHR S)
  | 0x88 => BINOP I64 (SHR U)
  | 0x89 => BINOP I64 ROTL
  | 0x8A => BINOP I64 ROTR
  | ...

grammar Binstr/numeric-un-f32 : instr = ...
  | 0x8B => UNOP F32 ABS
  | 0x8C => UNOP F32 NEG
  | 0x8D => UNOP F32 CEIL
  | 0x8E => UNOP F32 FLOOR
  | 0x8F => UNOP F32 TRUNC
  | 0x90 => UNOP F32 NEAREST
  | 0x91 => UNOP F32 SQRT
  | ...

grammar Binstr/numeric-bin-f32 : instr = ...
  | 0x92 => BINOP F32 ADD
  | 0x93 => BINOP F32 SUB
  | 0x94 => BINOP F32 MUL
  | 0x95 => BINOP F32 DIV
  | 0x96 => BINOP F32 MIN
  | 0x97 => BINOP F32 MAX
  | 0x98 => BINOP F32 COPYSIGN
  | ...

grammar Binstr/numeric-un-f64 : instr = ...
  | 0x99 => UNOP F64 ABS
  | 0x9A => UNOP F64 NEG
  | 0x9B => UNOP F64 CEIL
  | 0x9C => UNOP F64 FLOOR
  | 0x9D => UNOP F64 TRUNC
  | 0x9E => UNOP F64 NEAREST
  | 0x9F => UNOP F64 SQRT
  | ...

grammar Binstr/numeric-bin-f64 : instr = ...
  | 0xA0 => BINOP F64 ADD
  | 0xA1 => BINOP F64 SUB
  | 0xA2 => BINOP F64 MUL
  | 0xA3 => BINOP F64 DIV
  | 0xA4 => BINOP F64 MIN
  | 0xA5 => BINOP F64 MAX
  | 0xA6 => BINOP F64 COPYSIGN
  | ...

grammar Binstr/numeric-cvt : instr = ...
  | 0xA7 => CVTOP I32 I64 WRAP
  | 0xA8 => CVTOP I32 F32 (TRUNC S)
  | 0xA9 => CVTOP I32 F32 (TRUNC U)
  | 0xAA => CVTOP I32 F64 (TRUNC S)
  | 0xAB => CVTOP I32 F64 (TRUNC U)
  | 0xAC => CVTOP I64 I32 (EXTEND S)
  | 0xAD => CVTOP I64 I32 (EXTEND U)
  | 0xAE => CVTOP I64 F32 (TRUNC S)
  | 0xAF => CVTOP I64 F32 (TRUNC U)
  | 0xB0 => CVTOP I64 F64 (TRUNC S)
  | 0xB1 => CVTOP I64 F64 (TRUNC U)
  | 0xB2 => CVTOP F32 I32 (CONVERT S)
  | 0xB3 => CVTOP F32 I32 (CONVERT U)
  | 0xB4 => CVTOP F32 I64 (CONVERT S)
  | 0xB5 => CVTOP F32 I64 (CONVERT U)
  | 0xB6 => CVTOP F32 F64 DEMOTE
  | 0xB7 => CVTOP F64 I32 (CONVERT S)
  | 0xB8 => CVTOP F64 I32 (CONVERT U)
  | 0xB9 => CVTOP F64 I64 (CONVERT S)
  | 0xBA => CVTOP F64 I64 (CONVERT U)
  | 0xBB => CVTOP F32 F64 PROMOTE
  | 0xBC => CVTOP I32 F32 REINTERPRET
  | 0xBD => CVTOP I64 F64 REINTERPRET
  | 0xBE => CVTOP F32 I32 REINTERPRET
  | 0xBF => CVTOP F64 I64 REINTERPRET
  | ...

grammar Binstr/numeric-cvt-sat : instr = ...
  | 0xFC 0:Bu32 => CVTOP I32 F32 (TRUNC_SAT S)
  | 0xFC 1:Bu32 => CVTOP I32 F32 (TRUNC_SAT U)
  | 0xFC 2:Bu32 => CVTOP I32 F64 (TRUNC_SAT S)
  | 0xFC 3:Bu32 => CVTOP I32 F64 (TRUNC_SAT U)
  | 0xFC 4:Bu32 => CVTOP I64 F32 (TRUNC_SAT S)
  | 0xFC 5:Bu32 => CVTOP I64 F32 (TRUNC_SAT U)
  | 0xFC 6:Bu32 => CVTOP I64 F64 (TRUNC_SAT S)
  | 0xFC 7:Bu32 => CVTOP I64 F64 (TRUNC_SAT U)
  | ...

grammar Binstr/numeric-extend : instr = ...
  | 0xC0 => UNOP I32 (EXTEND 8)
  | 0xC1 => UNOP I32 (EXTEND 16)
  | 0xC2 => UNOP I64 (EXTEND 8)
  | 0xC3 => UNOP I64 (EXTEND 16)
  | 0xC4 => UNOP I64 (EXTEND 32)
  | ...


;; Vector instructions

grammar Blaneidx : laneidx =
  | l:Bbyte => l

grammar Binstr/vector-memory : instr = ...
  | 0xFD 0:Bu32 ao:Bmemarg => VLOAD V128 ao
  | 0xFD 1:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 8 X 8 _ S) ao
  | 0xFD 2:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 8 X 8 _ U) ao
  | 0xFD 3:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 16 X 4 _ S) ao
  | 0xFD 4:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 16 X 4 _ U) ao
  | 0xFD 5:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 32 X 2 _ S) ao
  | 0xFD 6:Bu32 ao:Bmemarg => VLOAD V128 (SHAPE 32 X 2 _ U) ao
  | 0xFD 7:Bu32 ao:Bmemarg => VLOAD V128 (SPLAT 8) ao
  | 0xFD 8:Bu32 ao:Bmemarg => VLOAD V128 (SPLAT 16) ao
  | 0xFD 9:Bu32 ao:Bmemarg => VLOAD V128 (SPLAT 32) ao
  | 0xFD 10:Bu32 ao:Bmemarg => VLOAD V128 (SPLAT 64) ao
  | 0xFD 92:Bu32 ao:Bmemarg => VLOAD V128 (ZERO 32) ao
  | 0xFD 92:Bu32 ao:Bmemarg => VLOAD V128 (ZERO 64) ao
  | 0xFD 11:Bu32 ao:Bmemarg => VSTORE V128 ao
  | 0xFD 84:Bu32 ao:Bmemarg l:Blaneidx => VLOAD_LANE V128 8 ao l
  | 0xFD 85:Bu32 ao:Bmemarg l:Blaneidx => VLOAD_LANE V128 16 ao l
  | 0xFD 86:Bu32 ao:Bmemarg l:Blaneidx => VLOAD_LANE V128 32 ao l
  | 0xFD 87:Bu32 ao:Bmemarg l:Blaneidx => VLOAD_LANE V128 64 ao l
  | 0xFD 88:Bu32 ao:Bmemarg l:Blaneidx => VSTORE_LANE V128 8 ao l
  | 0xFD 89:Bu32 ao:Bmemarg l:Blaneidx => VSTORE_LANE V128 16 ao l
  | 0xFD 90:Bu32 ao:Bmemarg l:Blaneidx => VSTORE_LANE V128 32 ao l
  | 0xFD 91:Bu32 ao:Bmemarg l:Blaneidx => VSTORE_LANE V128 64 ao l
  | ...

grammar Binstr/vector-const : instr = ...
  | 0xFD 12:Bu32 (b:Bbyte)^16 => VCONST V128 b' -- if $ibytes_(128, b') = b
  | ...

grammar Binstr/vector-shuffle : instr = ...
  | 0xFD 13:Bu32 (l:Blaneidx)^16 => VSHUFFLE (I8 X 16) l
  | ...

grammar Binstr/vector-lanes : instr = ...
  | 0xFD 21:Bu32 l:Blaneidx => VEXTRACT_LANE (I8 X 16) S l
  | 0xFD 22:Bu32 l:Blaneidx => VEXTRACT_LANE (I8 X 16) U l
  | 0xFD 23:Bu32 l:Blaneidx => VREPLACE_LANE (I8 X 16) l
  | 0xFD 24:Bu32 l:Blaneidx => VEXTRACT_LANE (I16 X 8) S l
  | 0xFD 25:Bu32 l:Blaneidx => VEXTRACT_LANE (I16 X 8) U l
  | 0xFD 26:Bu32 l:Blaneidx => VREPLACE_LANE (I16 X 8) l
  | 0xFD 27:Bu32 l:Blaneidx => VEXTRACT_LANE (I32 X 4) l
  | 0xFD 28:Bu32 l:Blaneidx => VREPLACE_LANE (I32 X 4) l
  | 0xFD 29:Bu32 l:Blaneidx => VEXTRACT_LANE (I64 X 2) l
  | 0xFD 30:Bu32 l:Blaneidx => VREPLACE_LANE (I64 X 2) l
  | 0xFD 31:Bu32 l:Blaneidx => VEXTRACT_LANE (F32 X 4) l
  | 0xFD 32:Bu32 l:Blaneidx => VREPLACE_LANE (F32 X 4) l
  | 0xFD 33:Bu32 l:Blaneidx => VEXTRACT_LANE (F64 X 2) l
  | 0xFD 34:Bu32 l:Blaneidx => VREPLACE_LANE (F64 X 2) l
  | ...

grammar Binstr/vector-swizzle : instr = ...
  | 0xFD 14:Bu32 => VSWIZZLE (I8 X 16)
  | ...

grammar Binstr/vector-splat : instr = ...
  | 0xFD 15:Bu32 => VSPLAT (I8 X 16)
  | 0xFD 16:Bu32 => VSPLAT (I16 X 8)
  | 0xFD 17:Bu32 => VSPLAT (I32 X 4)
  | 0xFD 18:Bu32 => VSPLAT (I64 X 2)
  | 0xFD 19:Bu32 => VSPLAT (F32 X 4)
  | 0xFD 20:Bu32 => VSPLAT (F64 X 2)
  | ...

grammar Binstr/vector-rel-i8x16 : instr = ...
  | 0xFD 35:Bu32 => VRELOP (I8 X 16) EQ
  | 0xFD 36:Bu32 => VRELOP (I8 X 16) NE
  | 0xFD 37:Bu32 => VRELOP (I8 X 16) (LT S)
  | 0xFD 38:Bu32 => VRELOP (I8 X 16) (LT U)
  | 0xFD 39:Bu32 => VRELOP (I8 X 16) (GT S)
  | 0xFD 40:Bu32 => VRELOP (I8 X 16) (GT U)
  | 0xFD 41:Bu32 => VRELOP (I8 X 16) (LE S)
  | 0xFD 42:Bu32 => VRELOP (I8 X 16) (LE U)
  | 0xFD 43:Bu32 => VRELOP (I8 X 16) (GE S)
  | 0xFD 44:Bu32 => VRELOP (I8 X 16) (GE U)
  | ...

grammar Binstr/vector-rel-i16x8 : instr = ...
  | 0xFD 45:Bu32 => VRELOP (I16 X 8) EQ
  | 0xFD 46:Bu32 => VRELOP (I16 X 8) NE
  | 0xFD 47:Bu32 => VRELOP (I16 X 8) (LT S)
  | 0xFD 48:Bu32 => VRELOP (I16 X 8) (LT U)
  | 0xFD 49:Bu32 => VRELOP (I16 X 8) (GT S)
  | 0xFD 50:Bu32 => VRELOP (I16 X 8) (GT U)
  | 0xFD 51:Bu32 => VRELOP (I16 X 8) (LE S)
  | 0xFD 52:Bu32 => VRELOP (I16 X 8) (LE U)
  | 0xFD 53:Bu32 => VRELOP (I16 X 8) (GE S)
  | 0xFD 54:Bu32 => VRELOP (I16 X 8) (GE U)
  | ...

grammar Binstr/vector-rel-i32x4 : instr = ...
  | 0xFD 55:Bu32 => VRELOP (I32 X 4) EQ
  | 0xFD 56:Bu32 => VRELOP (I32 X 4) NE
  | 0xFD 57:Bu32 => VRELOP (I32 X 4) (LT S)
  | 0xFD 58:Bu32 => VRELOP (I32 X 4) (LT U)
  | 0xFD 59:Bu32 => VRELOP (I32 X 4) (GT S)
  | 0xFD 60:Bu32 => VRELOP (I32 X 4) (GT U)
  | 0xFD 61:Bu32 => VRELOP (I32 X 4) (LE S)
  | 0xFD 62:Bu32 => VRELOP (I32 X 4) (LE U)
  | 0xFD 63:Bu32 => VRELOP (I32 X 4) (GE S)
  | 0xFD 64:Bu32 => VRELOP (I32 X 4) (GE U)
  | ...

grammar Binstr/vector-rel-i64x2 : instr = ...
  | 0xFD 214:Bu32 => VRELOP (I64 X 2) EQ
  | 0xFD 215:Bu32 => VRELOP (I64 X 2) NE
  | 0xFD 216:Bu32 => VRELOP (I64 X 2) (LT S)
  | 0xFD 217:Bu32 => VRELOP (I64 X 2) (GT S)
  | 0xFD 218:Bu32 => VRELOP (I64 X 2) (LE S)
  | 0xFD 219:Bu32 => VRELOP (I64 X 2) (GE S)
  | ...

grammar Binstr/vector-rel-f32x4 : instr = ...
  | 0xFD 65:Bu32 => VRELOP (F32 X 4) EQ
  | 0xFD 66:Bu32 => VRELOP (F32 X 4) NE
  | 0xFD 67:Bu32 => VRELOP (F32 X 4) LT
  | 0xFD 68:Bu32 => VRELOP (F32 X 4) GT
  | 0xFD 69:Bu32 => VRELOP (F32 X 4) LE
  | 0xFD 70:Bu32 => VRELOP (F32 X 4) GE
  | ...

grammar Binstr/vector-rel-f64x2 : instr = ...
  | 0xFD 71:Bu32 => VRELOP (F64 X 2) EQ
  | 0xFD 72:Bu32 => VRELOP (F64 X 2) NE
  | 0xFD 73:Bu32 => VRELOP (F64 X 2) LT
  | 0xFD 74:Bu32 => VRELOP (F64 X 2) GT
  | 0xFD 75:Bu32 => VRELOP (F64 X 2) LE
  | 0xFD 76:Bu32 => VRELOP (F64 X 2) GE
  | ...

grammar Binstr/vector-vv : instr = ...
  | 0xFD 77:Bu32 => VVUNOP V128 NOT
  | 0xFD 78:Bu32 => VVBINOP V128 AND
  | 0xFD 79:Bu32 => VVBINOP V128 ANDNOT
  | 0xFD 80:Bu32 => VVBINOP V128 OR
  | 0xFD 81:Bu32 => VVBINOP V128 XOR
  | 0xFD 82:Bu32 => VVTERNOP V128 BITSELECT
  | 0xFD 83:Bu32 => VVTESTOP V128 ANY_TRUE
  | ...

grammar Binstr/vector-v-i8x16 : instr = ...
  | 0xFD 96:Bu32 => VUNOP (I8 X 16) ABS
  | 0xFD 97:Bu32 => VUNOP (I8 X 16) NEG
  | 0xFD 98:Bu32 => VUNOP (I8 X 16) POPCNT
  | 0xFD 99:Bu32 => VTESTOP (I8 X 16) ALL_TRUE
  | 0xFD 100:Bu32 => VBITMASK (I8 X 16)
  | 0xFD 101:Bu32 => VNARROW (I8 X 16) (I16 X 8) S
  | 0xFD 102:Bu32 => VNARROW (I8 X 16) (I16 X 8) U
  | 0xFD 107:Bu32 => VSHIFTOP (I8 X 16) SHL
  | 0xFD 108:Bu32 => VSHIFTOP (I8 X 16) (SHR S)
  | 0xFD 109:Bu32 => VSHIFTOP (I8 X 16) (SHR U)
  | 0xFD 110:Bu32 => VBINOP (I8 X 16) ADD
  | 0xFD 111:Bu32 => VBINOP (I8 X 16) (ADD_SAT S)
  | 0xFD 112:Bu32 => VBINOP (I8 X 16) (ADD_SAT U)
  | 0xFD 113:Bu32 => VBINOP (I8 X 16) SUB
  | 0xFD 114:Bu32 => VBINOP (I8 X 16) (SUB_SAT S)
  | 0xFD 115:Bu32 => VBINOP (I8 X 16) (SUB_SAT U)
  | 0xFD 118:Bu32 => VBINOP (I8 X 16) (MIN S)
  | 0xFD 119:Bu32 => VBINOP (I8 X 16) (MIN U)
  | 0xFD 120:Bu32 => VBINOP (I8 X 16) (MAX S)
  | 0xFD 121:Bu32 => VBINOP (I8 X 16) (MAX U)
  | 0xFD 123:Bu32 => VBINOP (I8 X 16) (AVGR U)
  | ...

grammar Binstr/vector-v-i16x8 : instr = ...
  | 0xFD 124:Bu32 => VEXTUNOP (I16 X 8) (I8 X 16) (EXTADD_PAIRWISE S)
  | 0xFD 125:Bu32 => VEXTUNOP (I16 X 8) (I8 X 16) (EXTADD_PAIRWISE U)
  | 0xFD 128:Bu32 => VUNOP (I16 X 8) ABS
  | 0xFD 129:Bu32 => VUNOP (I16 X 8) NEG
  | 0xFD 130:Bu32 => VBINOP (I16 X 8) (Q15MULR_SAT S)
  | 0xFD 131:Bu32 => VTESTOP (I16 X 8) ALL_TRUE
  | 0xFD 132:Bu32 => VBITMASK (I16 X 8)
  | 0xFD 133:Bu32 => VNARROW (I16 X 8) (I32 X 4) S
  | 0xFD 134:Bu32 => VNARROW (I16 X 8) (I32 X 4) U
  | 0xFD 135:Bu32 => VCVTOP (I16 X 8) (I8 X 16) (EXTEND LOW S)
  | 0xFD 136:Bu32 => VCVTOP (I16 X 8) (I8 X 16) (EXTEND HIGH S)
  | 0xFD 137:Bu32 => VCVTOP (I16 X 8) (I8 X 16) (EXTEND LOW U)
  | 0xFD 138:Bu32 => VCVTOP (I16 X 8) (I8 X 16) (EXTEND HIGH U)
  | 0xFD 139:Bu32 => VSHIFTOP (I16 X 8) SHL
  | 0xFD 140:Bu32 => VSHIFTOP (I16 X 8) (SHR S)
  | 0xFD 141:Bu32 => VSHIFTOP (I16 X 8) (SHR U)
  | 0xFD 142:Bu32 => VBINOP (I16 X 8) ADD
  | 0xFD 143:Bu32 => VBINOP (I16 X 8) (ADD_SAT S)
  | 0xFD 144:Bu32 => VBINOP (I16 X 8) (ADD_SAT U)
  | 0xFD 145:Bu32 => VBINOP (I16 X 8) SUB
  | 0xFD 146:Bu32 => VBINOP (I16 X 8) (SUB_SAT S)
  | 0xFD 147:Bu32 => VBINOP (I16 X 8) (SUB_SAT U)
  | 0xFD 149:Bu32 => VBINOP (I16 X 8) MUL
  | 0xFD 150:Bu32 => VBINOP (I16 X 8) (MIN S)
  | 0xFD 151:Bu32 => VBINOP (I16 X 8) (MIN U)
  | 0xFD 152:Bu32 => VBINOP (I16 X 8) (MAX S)
  | 0xFD 153:Bu32 => VBINOP (I16 X 8) (MAX U)
  | 0xFD 155:Bu32 => VBINOP (I16 X 8) (AVGR U)
  | 0xFD 156:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL LOW S)
  | 0xFD 157:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL HIGH S)
  | 0xFD 158:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL LOW U)
  | 0xFD 159:Bu32 => VEXTBINOP (I16 X 8) (I8 X 16) (EXTMUL HIGH U)
  | ...

grammar Binstr/vector-v-i32x4 : instr = ...
  | 0xFD 126:Bu32 => VEXTUNOP (I32 X 4) (I16 X 8) (EXTADD_PAIRWISE S)
  | 0xFD 127:Bu32 => VEXTUNOP (I32 X 4) (I16 X 8) (EXTADD_PAIRWISE U)
  | 0xFD 160:Bu32 => VUNOP (I32 X 4) ABS
  | 0xFD 161:Bu32 => VUNOP (I32 X 4) NEG
  | 0xFD 163:Bu32 => VTESTOP (I32 X 4) ALL_TRUE
  | 0xFD 164:Bu32 => VBITMASK (I32 X 4)
  | 0xFD 167:Bu32 => VCVTOP (I32 X 4) (I16 X 8) (EXTEND LOW S)
  | 0xFD 168:Bu32 => VCVTOP (I32 X 4) (I16 X 8) (EXTEND HIGH S)
  | 0xFD 169:Bu32 => VCVTOP (I32 X 4) (I16 X 8) (EXTEND LOW U)
  | 0xFD 170:Bu32 => VCVTOP (I32 X 4) (I16 X 8) (EXTEND HIGH U)
  | 0xFD 171:Bu32 => VSHIFTOP (I32 X 4) SHL
  | 0xFD 172:Bu32 => VSHIFTOP (I32 X 4) (SHR S)
  | 0xFD 173:Bu32 => VSHIFTOP (I32 X 4) (SHR U)
  | 0xFD 174:Bu32 => VBINOP (I32 X 4) ADD
  | 0xFD 177:Bu32 => VBINOP (I32 X 4) SUB
  | 0xFD 181:Bu32 => VBINOP (I32 X 4) MUL
  | 0xFD 182:Bu32 => VBINOP (I32 X 4) (MIN S)
  | 0xFD 183:Bu32 => VBINOP (I32 X 4) (MIN U)
  | 0xFD 184:Bu32 => VBINOP (I32 X 4) (MAX S)
  | 0xFD 185:Bu32 => VBINOP (I32 X 4) (MAX U)
  | 0xFD 186:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (DOT S)
  | 0xFD 188:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL LOW S)
  | 0xFD 189:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL HIGH S)
  | 0xFD 190:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL LOW U)
  | 0xFD 191:Bu32 => VEXTBINOP (I32 X 4) (I16 X 8) (EXTMUL HIGH U)
  | ...

grammar Binstr/vector-v-i64x2 : instr = ...
  | 0xFD 192:Bu32 => VUNOP (I64 X 2) ABS
  | 0xFD 193:Bu32 => VUNOP (I64 X 2) NEG
  | 0xFD 195:Bu32 => VTESTOP (I64 X 2) ALL_TRUE
  | 0xFD 196:Bu32 => VBITMASK (I64 X 2)
  | 0xFD 199:Bu32 => VCVTOP (I64 X 2) (I32 X 4) (EXTEND LOW S)
  | 0xFD 200:Bu32 => VCVTOP (I64 X 2) (I32 X 4) (EXTEND HIGH S)
  | 0xFD 201:Bu32 => VCVTOP (I64 X 2) (I32 X 4) (EXTEND LOW U)
  | 0xFD 202:Bu32 => VCVTOP (I64 X 2) (I32 X 4) (EXTEND HIGH U)
  | 0xFD 203:Bu32 => VSHIFTOP (I64 X 2) SHL
  | 0xFD 204:Bu32 => VSHIFTOP (I64 X 2) (SHR S)
  | 0xFD 205:Bu32 => VSHIFTOP (I64 X 2) (SHR U)
  | 0xFD 206:Bu32 => VBINOP (I64 X 2) ADD
  | 0xFD 209:Bu32 => VBINOP (I64 X 2) SUB
  | 0xFD 213:Bu32 => VBINOP (I64 X 2) MUL
  | 0xFD 220:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL LOW S)
  | 0xFD 221:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL HIGH S)
  | 0xFD 222:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL LOW U)
  | 0xFD 223:Bu32 => VEXTBINOP (I64 X 2) (I32 X 4) (EXTMUL HIGH U)
  | ...

grammar Binstr/vector-v-f32x4 : instr = ...
  | 0xFD 103:Bu32 => VUNOP (F32 X 4) CEIL
  | 0xFD 104:Bu32 => VUNOP (F32 X 4) FLOOR
  | 0xFD 105:Bu32 => VUNOP (F32 X 4) TRUNC
  | 0xFD 106:Bu32 => VUNOP (F32 X 4) NEAREST
  | 0xFD 224:Bu32 => VUNOP (F32 X 4) ABS
  | 0xFD 225:Bu32 => VUNOP (F32 X 4) NEG
  | 0xFD 227:Bu32 => VUNOP (F32 X 4) SQRT
  | 0xFD 228:Bu32 => VBINOP (F32 X 4) ADD
  | 0xFD 229:Bu32 => VBINOP (F32 X 4) SUB
  | 0xFD 230:Bu32 => VBINOP (F32 X 4) MUL
  | 0xFD 231:Bu32 => VBINOP (F32 X 4) DIV
  | 0xFD 232:Bu32 => VBINOP (F32 X 4) MIN
  | 0xFD 233:Bu32 => VBINOP (F32 X 4) MAX
  | 0xFD 234:Bu32 => VBINOP (F32 X 4) PMIN
  | 0xFD 235:Bu32 => VBINOP (F32 X 4) PMAX
  | ...

grammar Binstr/vector-v-f64x2 : instr = ...
  | 0xFD 116:Bu32 => VUNOP (F64 X 2) CEIL
  | 0xFD 117:Bu32 => VUNOP (F64 X 2) FLOOR
  | 0xFD 122:Bu32 => VUNOP (F64 X 2) TRUNC
  | 0xFD 148:Bu32 => VUNOP (F64 X 2) NEAREST
  | 0xFD 236:Bu32 => VUNOP (F64 X 2) ABS
  | 0xFD 237:Bu32 => VUNOP (F64 X 2) NEG
  | 0xFD 239:Bu32 => VUNOP (F64 X 2) SQRT
  | 0xFD 240:Bu32 => VBINOP (F64 X 2) ADD
  | 0xFD 241:Bu32 => VBINOP (F64 X 2) SUB
  | 0xFD 242:Bu32 => VBINOP (F64 X 2) MUL
  | 0xFD 243:Bu32 => VBINOP (F64 X 2) DIV
  | 0xFD 244:Bu32 => VBINOP (F64 X 2) MIN
  | 0xFD 245:Bu32 => VBINOP (F64 X 2) MAX
  | 0xFD 246:Bu32 => VBINOP (F64 X 2) PMIN
  | 0xFD 247:Bu32 => VBINOP (F64 X 2) PMAX
  | ...

grammar Binstr/vector-cvt : instr = ...
  | 0xFD 248:Bu32 => VCVTOP (I32 X 4) (F32 X 4) (TRUNC_SAT S)
  | 0xFD 249:Bu32 => VCVTOP (I32 X 4) (F32 X 4) (TRUNC_SAT U)
  | 0xFD 250:Bu32 => VCVTOP (F32 X 4) (I32 X 4) (CONVERT S)
  | 0xFD 251:Bu32 => VCVTOP (F32 X 4) (I32 X 4) (CONVERT U)
  | 0xFD 252:Bu32 => VCVTOP (I32 X 4) (F64 X 2) (TRUNC_SAT S ZERO)
  | 0xFD 253:Bu32 => VCVTOP (I32 X 4) (F64 X 2) (TRUNC_SAT U ZERO)
  | 0xFD 254:Bu32 => VCVTOP (F64 X 2) (I32 X 4) (CONVERT LOW S)
  | 0xFD 255:Bu32 => VCVTOP (F64 X 2) (I32 X 4) (CONVERT LOW U)
  | 0xFD 94:Bu32 => VCVTOP (F32 X 4) (F64 X 2) DEMOTE ZERO
  | 0xFD 95:Bu32 => VCVTOP (F64 X 2) (F32 X 4) PROMOTE LOW


;; Expressions

grammar Bexpr : expr =
  | (in:Binstr)* 0x0B => in*


;;
;; Modules
;;

;; Sections

var len : nat

grammar Bsection_(N, grammar BX : en*) : en*  hint(desc "section") =
  | N:Bbyte len:Bu32 en*:BX => en*  -- if len = ||BX||
  | eps => eps


;; Custom sections

grammar Bcustom : ()* hint(desc "custom data") =
  | Bname Bbyte* => ()

grammar Bcustomsec : () hint(desc "custom section") =
  | Bsection_(0, Bcustom) => ()


;; Type section

grammar Btype : type =
  | ft:Bfunctype => TYPE ft

grammar Btypesec : type* hint(desc "type section") =
  | ty*:Bsection_(1, Blist(Btype)) => ty*


;; Import section

grammar Bimport : import =
  | nm_1:Bname nm_2:Bname xt:Bexterntype => IMPORT nm_1 nm_2 xt

grammar Bimportsec : import* hint(desc "import section") =
  | im*:Bsection_(2, Blist(Bimport)) => im*


;; Function section

grammar Bfuncsec : typeidx* hint(desc "function section") =
  | x*:Bsection_(3, Blist(Btypeidx)) => x*


;; Table section

grammar Btable : table =
  | tt:Btabletype => TABLE tt

grammar Btablesec : table* hint(desc "table section") =
  | tab*:Bsection_(4, Blist(Btable)) => tab*


;; Memory section

grammar Bmem : mem =
  | mt:Bmemtype => MEMORY mt

grammar Bmemsec : mem* hint(desc "memory section") =
  | mem*:Bsection_(5, Blist(Bmem)) => mem*


;; Global section

grammar Bglobal : global =
  | gt:Bglobaltype e:Bexpr => GLOBAL gt e

grammar Bglobalsec : global* hint(desc "global section") =
  | glob*:Bsection_(6, Blist(Bglobal)) => glob*


;; Export section

grammar Bexport : export =
  | nm:Bname xx:Bexternidx => EXPORT nm xx

grammar Bexportsec : export* hint(desc "export section") =
  | ex*:Bsection_(7, Blist(Bexport)) => ex*


;; Start section

grammar Bstart : start* =
  | x:Bfuncidx => (START x)

syntax startopt hint(show start?) = start*  ;; HACK

grammar Bstartsec : start? hint(desc "start section") =
  | startopt:Bsection_(8, Bstart) => $opt_(start, startopt)


;; Element section

grammar Belemkind : reftype hint(desc "element kind") =
  | 0x00 => FUNCREF

grammar Belem : elem =
  | 0:Bu32 e_o:Bexpr y*:Blist(Bfuncidx) =>
      ELEM FUNCREF (REF.FUNC y)* (ACTIVE 0 e_o)
  | 1:Bu32 rt:Belemkind y*:Blist(Bfuncidx) =>
      ELEM rt (REF.FUNC y)* PASSIVE
  | 2:Bu32 x:Btableidx expr:Bexpr rt:Belemkind y*:Blist(Bfuncidx) =>
      ELEM rt (REF.FUNC y)* (ACTIVE x expr)
  | 3:Bu32 rt:Belemkind y*:Blist(Bfuncidx) =>
      ELEM rt (REF.FUNC y)* DECLARE
  | 4:Bu32 e_o:Bexpr e*:Blist(Bexpr) =>
      ELEM FUNCREF e* (ACTIVE 0 e_o)
  | 5:Bu32 rt:Breftype e*:Blist(Bexpr) =>
      ELEM rt e* PASSIVE
  | 6:Bu32 x:Btableidx expr:Bexpr e*:Blist(Bexpr) =>
      ELEM FUNCREF e* (ACTIVE x expr)
  | 7:Bu32 rt:Breftype e*:Blist(Bexpr) =>
      ELEM rt e* DECLARE

grammar Belemsec : elem* hint(desc "element section") =
  | elem*:Bsection_(9, Blist(Belem)) => elem*


;; Code section

syntax code = (local*, expr)

grammar Blocals : local* hint(desc "local") =
  | n:Bu32 t:Bvaltype => (LOCAL t)^n

grammar Bfunc : code =
  | local**:Blist(Blocals) expr:Bexpr => ($concat_(local, local**), expr)

grammar Bcode : code =
  | len:Bu32 code:Bfunc => code  -- if len = ||Bfunc||

grammar Bcodesec : code* hint(desc "code section") =
  | code*:Bsection_(10, Blist(Bcode)) => code*


;; Data section

grammar Bdata : data =
  | 0:Bu32 e:Bexpr b*:Blist(Bbyte) => DATA b* (ACTIVE 0 e)
  | 1:Bu32 b*:Blist(Bbyte) => DATA b* PASSIVE
  | 2:Bu32 x:Bmemidx e:Bexpr b*:Blist(Bbyte) => DATA b* (ACTIVE x e)

grammar Bdatasec : data* hint(desc "data section") =
  | data*:Bsection_(11, Blist(Bdata)) => data*


;; Data count section

grammar Bdatacnt : u32* hint(desc "data count") =
  | n:Bu32 => n

syntax nopt hint(show n?) = u32*  ;; HACK

grammar Bdatacntsec : u32? hint(desc "data count section") =
  | nopt:Bsection_(12, Bdatacnt) => $opt_(u32, nopt)


;; Modules

grammar Bmodule : module =
  | 0x00 0x61 0x73 0x6D 1:Bu32
    Bcustomsec* type*:Btypesec
    Bcustomsec* import*:Bimportsec
    Bcustomsec* typeidx*:Bfuncsec
    Bcustomsec* table*:Btablesec
    Bcustomsec* mem*:Bmemsec
    Bcustomsec* global*:Bglobalsec
    Bcustomsec* export*:Bexportsec
    Bcustomsec* start?:Bstartsec
    Bcustomsec* elem*:Belemsec
    Bcustomsec* n?:Bdatacntsec
    Bcustomsec* (local*, expr)*:Bcodesec
    Bcustomsec* data*:Bdatasec
    Bcustomsec* =>
      MODULE type* import* func* global* table* mem* elem* data* start? export*
    ----
    -- (if n = |data*|)?
    -- if n? =/= eps \/ $dataidx_funcs(func*) = eps
    -- (if func = FUNC typeidx local* expr)*