From 073be711bf8f7412a0f33a81e727111e7907ca2d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 10 Jan 2025 11:25:02 +0100 Subject: [PATCH 1/2] Pass on instruciton syntax --- document/core/syntax/instructions.rst | 19 ++--- document/core/util/macros.def | 5 ++ spectec/spec/wasm-3.0/1-syntax.watsup | 33 ++++---- spectec/spec/wasm-3.0/3-typing.watsup | 6 +- spectec/spec/wasm-3.0/8-reduction.watsup | 12 +-- spectec/spec/wasm-3.0/A-binary.watsup | 32 +++---- spectec/src/al/al_util.ml | 2 +- spectec/src/backend-interpreter/construct.ml | 5 +- spectec/src/backend-latex/render.ml | 2 +- spectec/src/il2al/translate.ml | 2 +- spectec/test-frontend/TEST.md | 88 ++++++++++---------- 11 files changed, 105 insertions(+), 101 deletions(-) diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 7c6ccec841..f9c1ba3ff7 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -38,7 +38,7 @@ The ${:UNREACHABLE} instruction causes an unconditional :ref:`trap `. The ${:DROP} instruction simply throws away a single operand. The ${:SELECT} instruction selects one of its first two operands based on whether its third operand is zero or not. -It may include a :ref:`value type ` determining the type of these operands. If missing, the operands must be of :ref:`numeric type `. +It may include a :ref:`value type ` determining the type of these operands. If the type immediate is absent, the operands must be of :ref:`numeric type `. .. note:: In future versions of WebAssembly, the type annotation on ${:SELECT} may allow for more than a single value being selected at the same time. @@ -119,22 +119,22 @@ Vector instructions (also known as *SIMD* instructions, *single instruction mult $${syntax: {lanetype dim shape ishape bshape} half__ zero__ laneidx instr/vec} -$${syntax: - vvunop vvbinop vvternop vvtestop - vunop_ vbinop_ vternop_ vtestop_ vrelop_ vswizzlop_ vshiftop_ vextunop__ vextbinop__ vextternop__ vcvtop__ -} - Vector instructions have a naming convention involving a *shape* prefix that determines how their operands will be interpreted, written ${:t#X#N}, and consisting of a *lane type* ${:t}, a possibly *packed* :ref:`numeric type `, and the number of *lanes* ${:N} of that type. Operations are performed point-wise on the values of each lane. +Instructions prefixed with ${:V128} do not involve a specific interpretation, and treat the ${:V128} as either an ${:i128} value or a vector of ${:128} individual bits. + .. note:: For example, the shape ${shape: I32 X `4} interprets the operand as four ${:i32} values, packed into an ${:i128}. The bit width of the lane type ${:t} times ${:N} always is ${:128}. -Instructions prefixed with ${:V128} do not involve a specific interpretation, and treat the ${:V128} as either an ${:i128} value or a vector of ${:128} individual bits. +$${syntax: + vvunop vvbinop vvternop vvtestop + vunop_ vbinop_ vternop_ vtestop_ vrelop_ vswizzlop_ vshiftop_ vextunop__ vextbinop__ vextternop__ vcvtop__ +} Vector instructions can be grouped into several subcategories: @@ -352,11 +352,6 @@ The ${:MEMORY.INIT} instruction copies data from a :ref:`passive data segment ` :ref:`index ` ${:0}. - This restriction may be lifted in future versions. - .. index:: ! control instruction, ! structured control, ! exception, ! label, ! block, ! block type, ! branch, ! unwinding, stack type, label index, function index, type index, list, trap, function, table, tag, function type, value type, tag type, try block, type index pair: abstract syntax; instruction diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 2ed2712ca7..9e2a02e7ea 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -219,6 +219,11 @@ .. |VNX| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v}} .. |VN| mathdef:: \xref{syntax/types}{syntax-vectype}{\K{v}\scriptstyle\kern-0.1emN} +.. |ntI| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{i}} +.. |ntF| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{f}} +.. |ntV| mathdef:: \xref{syntax/types}{syntax-numtype}{\K{v}} +.. |ntN| mathdef:: \xref{syntax/types}{syntax-numtype}{\scriptstyle\kern-0.1emN} + .. |ANYREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{anyref}} .. |EQREF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{eqref}} .. |I31REF| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{i{\scriptstyle31}ref}} diff --git a/spectec/spec/wasm-3.0/1-syntax.watsup b/spectec/spec/wasm-3.0/1-syntax.watsup index bd942ec320..9f1dc8d325 100644 --- a/spectec/spec/wasm-3.0/1-syntax.watsup +++ b/spectec/spec/wasm-3.0/1-syntax.watsup @@ -185,9 +185,9 @@ syntax valtype/syn hint(desc "value type") = syntax valtype/sem = | ... | BOT -syntax Inn hint(show I#N) hint(macro none) = I32 | I64 -syntax Fnn hint(show F#N) hint(macro none) = F32 | F64 -syntax Vnn hint(show V#N) hint(macro none) = V128 +syntax Inn hint(show I#N) hint(macro "nt%") = I32 | I64 +syntax Fnn hint(show F#N) hint(macro "nt%") = F32 | F64 +syntax Vnn hint(show V#N) hint(macro "nt%") = V128 syntax Cnn hint(show t) = Inn | Fnn | Vnn @@ -224,9 +224,9 @@ syntax packtype hint(desc "packed type") = I8 | I16 syntax lanetype hint(desc "lane type") = numtype | packtype syntax storagetype hint(desc "storage type") = valtype | packtype -syntax Pnn hint(show I#N) hint(macro none) = I8 | I16 -syntax Jnn hint(show I#N) hint(macro none) = Inn | Pnn -syntax Lnn hint(show I#N) hint(macro none) = Inn | Fnn | Pnn +syntax Pnn hint(show I#N) hint(macro "nt%") = I8 | I16 +syntax Jnn hint(show I#N) hint(macro "nt%") = Inn | Pnn +syntax Lnn hint(show I#N) hint(macro "nt%") = Inn | Fnn | Pnn ;; Result types @@ -439,6 +439,7 @@ syntax relop_(Inn) = syntax relop_(Fnn) = | EQ | NE | LT | GT | LE | GE +;; TODO(3, rossberg): change order of parameters? syntax cvtop__(numtype_1, numtype_2) syntax cvtop__(Inn_1, Inn_2) = | EXTEND sx hint(show %0#_#%1) -- if $sizenn1(Inn_1) < $sizenn2(Inn_2) @@ -479,11 +480,11 @@ syntax bshape hint(desc "byte shape") = shape -- if $lanetype(shape) = I8 ;; Vector operators syntax half__(shape_1, shape_2) -syntax half__(Jnn_1 X M_1, Jnn_2 X M_2) = LOW | HIGH -- if $(2 * $lsizenn1(Jnn_1)) = $lsizenn1(Jnn_2) -syntax half__(Lnn_1 X M_1, Fnn_2 X M_2) = LOW -- if $(2 * $lsizenn1(Lnn_1)) = $sizenn1(Fnn_2) = `64 +syntax half__(Jnn_1 X M_1, Jnn_2 X M_2) = LOW | HIGH -- if $(2 * $lsizenn1(Jnn_1)) = $lsizenn2(Jnn_2) +syntax half__(Lnn_1 X M_1, Fnn_2 X M_2) = LOW -- if $(2 * $lsizenn1(Lnn_1)) = $sizenn2(Fnn_2) = 64 syntax zero__(shape_1, shape_2) -syntax zero__(Fnn_1 X M_1, Lnn_2 X M_2) = ZERO -- if $(2 * $lsizenn2(Lnn_2)) = $sizenn1(Fnn_1) = `64 +syntax zero__(Fnn_1 X M_1, Lnn_2 X M_2) = ZERO -- if $(2 * $lsizenn2(Lnn_2)) = $sizenn1(Fnn_1) = 64 syntax vvunop hint(macro "%" "V%") = NOT syntax vvbinop hint(macro "%" "V%") = AND | ANDNOT | OR | XOR @@ -507,7 +508,8 @@ syntax vbinop_(Jnn X M) = | RELAXED_Q15MULR S hint(show RELAXED_Q15MULR#_#%) -- if $lsizenn(Jnn) = `16 | MIN sx hint(show MIN#_#%) -- if $lsizenn(Jnn) <= `32 | MAX sx hint(show MAX#_#%) -- if $lsizenn(Jnn) <= `32 -syntax vbinop_(Fnn X M) = ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX | RELAXED_MIN | RELAXED_MAX +syntax vbinop_(Fnn X M) = ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX + | RELAXED_MIN | RELAXED_MAX syntax vternop_(shape) hint(macro "%" "V%") syntax vternop_(Jnn X M) = RELAXED_LANESELECT @@ -575,15 +577,15 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32} var ao : memarg syntax loadop_(numtype) -syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $sizenn(Inn) +syntax loadop_(Inn) = sz _ sx hint(show %0#_#%2) -- if sz < $sizenn(Inn) syntax storeop_(numtype) -syntax storeop_(Inn) = sz -- if sz < $sizenn(Inn) +syntax storeop_(Inn) = sz -- if sz < $sizenn(Inn) syntax vloadop_(vectype) hint(macro "%" "L%") = - | SHAPE sz X M sx hint(show %1#X#%3#_#%4) hint(macro "%shape") -- if $(sz * M = $vsize(vectype)/2) - | SPLAT sz hint(show %#_#SPLAT) - | ZERO sz hint(show %#_#ZERO) -- if sz >= `32 + | SHAPE sz X M _ sx hint(show %1#X#%3#_#%5) hint(macro "%shape") -- if $(sz * M = $vsize(vectype)/2) + | SPLAT sz hint(show %#_#SPLAT) + | ZERO sz hint(show %#_#ZERO) -- if sz >= `32 ;; Block types @@ -681,6 +683,7 @@ syntax instr/vec hint(desc "vector instruction") = ... | VNARROW ishape_1 ishape_2 sx hint(show ##%.NARROW#_# ##%#_#%) hint(macro "VNARROW") -- if $($lsize($lanetype(ishape_2)) = 2*$lsize($lanetype(ishape_1)) <= `32) | VCVTOP shape_1 shape_2 vcvtop__(shape_2, shape_1) half__(shape_2, shape_1)? zero__(shape_2, shape_1)? + ;; TODO(1, rossberg): fix overlong line hint(show ##%1.%3#_# ##%2) hint(show ##%1.%3#_# ##%2#_#%4) ;; TODO(2, rossberg): this is wrong when half is absent hint(show ##%1.%3#_#%5#_# ##%2#_#%4) ;; TODO(2, rossberg): this is wrong when half is present diff --git a/spectec/spec/wasm-3.0/3-typing.watsup b/spectec/spec/wasm-3.0/3-typing.watsup index 3170c421cc..87f34c261a 100644 --- a/spectec/spec/wasm-3.0/3-typing.watsup +++ b/spectec/spec/wasm-3.0/3-typing.watsup @@ -1074,7 +1074,7 @@ rule Instr_ok/data.drop: (; rule Instr_ok/load: - C |- LOAD nt (N sx)? x memarg : at -> nt + C |- LOAD nt (N _ sx)? x memarg : at -> nt -- if C.MEMS[x] = at lim PAGE -- if $(2^(memarg.ALIGN) <= $size(nt)/8) -- if $(2^(memarg.ALIGN) <= N/8 < $size(nt)/8)? @@ -1087,7 +1087,7 @@ rule Instr_ok/load-val: -- if $(2^(memarg.ALIGN) <= $size(nt)/8) rule Instr_ok/load-pack: - C |- LOAD Inn (M sx) x memarg : at -> Inn + C |- LOAD Inn (M _ sx) x memarg : at -> Inn -- if C.MEMS[x] = at lim PAGE -- if $(2^(memarg.ALIGN) <= M/8) @@ -1116,7 +1116,7 @@ rule Instr_ok/vload-val: -- if $(2^(memarg.ALIGN) <= $vsize(V128)/8) rule Instr_ok/vload-pack: - C |- VLOAD V128 (SHAPE M X N sx) x memarg : at -> V128 + C |- VLOAD V128 (SHAPE M X N _ sx) x memarg : at -> V128 -- if C.MEMS[x] = at lim PAGE -- if $(2^(memarg.ALIGN) <= M/8 * N) diff --git a/spectec/spec/wasm-3.0/8-reduction.watsup b/spectec/spec/wasm-3.0/8-reduction.watsup index dfc06ae7b7..2114d5223c 100644 --- a/spectec/spec/wasm-3.0/8-reduction.watsup +++ b/spectec/spec/wasm-3.0/8-reduction.watsup @@ -900,12 +900,12 @@ rule Step_read/load-num-val: -- if $nbytes_(nt, c) = $mem(z, x).BYTES[i + ao.OFFSET : $size(nt)/8] rule Step_read/load-pack-oob: - z; (CONST at i) (LOAD Inn (n sx) x ao) ~> TRAP + z; (CONST at i) (LOAD Inn (n _ sx) x ao) ~> TRAP ---- -- if $(i + ao.OFFSET + n/8 > |$mem(z, x).BYTES|) rule Step_read/load-pack-val: - z; (CONST at i) (LOAD Inn (n sx) x ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c)) + z; (CONST at i) (LOAD Inn (n _ sx) x ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c)) ---- -- if $ibytes_(n, c) = $mem(z, x).BYTES[i + ao.OFFSET : n/8] @@ -919,11 +919,11 @@ rule Step_read/vload-val: rule Step_read/vload-pack-oob: - z; (CONST at i) (VLOAD V128 (SHAPE M X K sx) x ao) ~> TRAP + z; (CONST at i) (VLOAD V128 (SHAPE M X K _ sx) x ao) ~> TRAP -- if $(i + ao.OFFSET + M * K/8) > |$mem(z, x).BYTES| rule Step_read/vload-pack-val: - z; (CONST at i) (VLOAD V128 (SHAPE M X K sx) x ao) ~> (VCONST V128 c) + z; (CONST at i) (VLOAD V128 (SHAPE M X K _ sx) x ao) ~> (VCONST V128 c) ---- ---- -- (if $ibytes_(M, j) = $mem(z, x).BYTES[i + ao.OFFSET + k * M/8 : M/8])^(k - (CONST at_1 i_1) (CONST at_2 i_2) (LOAD I32 (8 U) x_2 $memarg0) (STORE I32 8 x_1 $memarg0) + (CONST at_1 i_1) (CONST at_2 i_2) (LOAD I32 (8 _ U) x_2 $memarg0) (STORE I32 8 x_1 $memarg0) (CONST at_1 $(i_1 + 1)) (CONST at_2 $(i_2 + 1)) (CONST at' $(n - 1)) (MEMORY.COPY x_1 x_2) -- otherwise -- if i_1 <= i_2 rule Step_read/memory.copy-gt: z; (CONST at_1 i_1) (CONST at_2 i_2) (CONST at' n) (MEMORY.COPY x_1 x_2) ~> - (CONST at_1 $(i_1+n-1)) (CONST at_2 $(i_2+n-1)) (LOAD I32 (8 U) x_2 $memarg0) (STORE I32 8 x_1 $memarg0) + (CONST at_1 $(i_1+n-1)) (CONST at_2 $(i_2+n-1)) (LOAD I32 (8 _ U) x_2 $memarg0) (STORE I32 8 x_1 $memarg0) (CONST at_1 i_1) (CONST at_2 i_2) (CONST at' $(n-1)) (MEMORY.COPY x_1 x_2) -- otherwise diff --git a/spectec/spec/wasm-3.0/A-binary.watsup b/spectec/spec/wasm-3.0/A-binary.watsup index 527de36102..19f2183e65 100644 --- a/spectec/spec/wasm-3.0/A-binary.watsup +++ b/spectec/spec/wasm-3.0/A-binary.watsup @@ -359,16 +359,16 @@ grammar Binstr/memory : instr = ... | 0x29 (x,ao):Bmemarg => LOAD I64 x ao | 0x2A (x,ao):Bmemarg => LOAD F32 x ao | 0x2B (x,ao):Bmemarg => LOAD F64 x ao - | 0x2C (x,ao):Bmemarg => LOAD I32 (`8 S) x ao - | 0x2D (x,ao):Bmemarg => LOAD I32 (`8 U) x ao - | 0x2E (x,ao):Bmemarg => LOAD I32 (`16 S) x ao - | 0x2F (x,ao):Bmemarg => LOAD I32 (`16 U) x ao - | 0x30 (x,ao):Bmemarg => LOAD I64 (`8 S) x ao - | 0x31 (x,ao):Bmemarg => LOAD I64 (`8 U) x ao - | 0x32 (x,ao):Bmemarg => LOAD I64 (`16 S) x ao - | 0x33 (x,ao):Bmemarg => LOAD I64 (`16 U) x ao - | 0x34 (x,ao):Bmemarg => LOAD I64 (`32 S) x ao - | 0x35 (x,ao):Bmemarg => LOAD I64 (`32 U) x ao + | 0x2C (x,ao):Bmemarg => LOAD I32 (`8 _ S) x ao + | 0x2D (x,ao):Bmemarg => LOAD I32 (`8 _ U) x ao + | 0x2E (x,ao):Bmemarg => LOAD I32 (`16 _ S) x ao + | 0x2F (x,ao):Bmemarg => LOAD I32 (`16 _ U) x ao + | 0x30 (x,ao):Bmemarg => LOAD I64 (`8 _ S) x ao + | 0x31 (x,ao):Bmemarg => LOAD I64 (`8 _ U) x ao + | 0x32 (x,ao):Bmemarg => LOAD I64 (`16 _ S) x ao + | 0x33 (x,ao):Bmemarg => LOAD I64 (`16 _ U) x ao + | 0x34 (x,ao):Bmemarg => LOAD I64 (`32 _ S) x ao + | 0x35 (x,ao):Bmemarg => LOAD I64 (`32 _ U) x ao | 0x36 (x,ao):Bmemarg => STORE I32 x ao | 0x37 (x,ao):Bmemarg => STORE I64 x ao | 0x38 (x,ao):Bmemarg => STORE F32 x ao @@ -596,12 +596,12 @@ grammar Blaneidx : laneidx = grammar Binstr/vec-memory : instr = ... | 0xFD 0:Bu32 (x,ao):Bmemarg => VLOAD V128 x ao - | 0xFD 1:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `8 X `8 S) x ao - | 0xFD 2:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `8 X `8 U) x ao - | 0xFD 3:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `16 X `4 S) x ao - | 0xFD 4:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `16 X `4 U) x ao - | 0xFD 5:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `32 X `2 S) x ao - | 0xFD 6:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `32 X `2 U) x ao + | 0xFD 1:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `8 X `8 _ S) x ao + | 0xFD 2:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `8 X `8 _ U) x ao + | 0xFD 3:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `16 X `4 _ S) x ao + | 0xFD 4:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `16 X `4 _ U) x ao + | 0xFD 5:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `32 X `2 _ S) x ao + | 0xFD 6:Bu32 (x,ao):Bmemarg => VLOAD V128 (SHAPE `32 X `2 _ U) x ao | 0xFD 7:Bu32 (x,ao):Bmemarg => VLOAD V128 (SPLAT `8) x ao | 0xFD 8:Bu32 (x,ao):Bmemarg => VLOAD V128 (SPLAT `16) x ao | 0xFD 9:Bu32 (x,ao):Bmemarg => VLOAD V128 (SPLAT `32) x ao diff --git a/spectec/src/al/al_util.ml b/spectec/src/al/al_util.ml index 6401016632..fb24f581f4 100644 --- a/spectec/src/al/al_util.ml +++ b/spectec/src/al/al_util.ml @@ -289,7 +289,7 @@ let frameE ?(at = no) ~note (arity, e) = let get_atom op = - match List.find_opt (fun al -> List.length al <> 0) op with + match List.find_opt (fun al -> al <> []) op with | Some al -> Some (List.hd al) | None -> None diff --git a/spectec/src/backend-interpreter/construct.ml b/spectec/src/backend-interpreter/construct.ml index 3100953fc8..4f3219dd5b 100644 --- a/spectec/src/backend-interpreter/construct.ml +++ b/spectec/src/backend-interpreter/construct.ml @@ -694,7 +694,7 @@ let al_to_memop (f: value -> 'p) : value list -> idx * (num_type, 'p) memop = fu | v -> error_values "memop" v let al_to_pack_size_extension: value -> Pack.pack_size * Pack.extension = function - | TupV [ p; ext ] -> al_to_pack_size p, al_to_extension ext + | CaseV ("_", [ p; ext ]) -> al_to_pack_size p, al_to_extension ext | v -> error_value "pack size, extension" v let al_to_loadop: value list -> idx * loadop = al_to_opt al_to_pack_size_extension |> al_to_memop @@ -1876,7 +1876,8 @@ let al_of_memop f idx memop = in [ al_of_num_type memop.ty; f memop.pack ] @ al_of_memidx idx @ [ StrV str ] -let al_of_pack_size_extension (p, s) = tupV [ al_of_pack_size p; al_of_extension s ] +let al_of_pack_size_extension (p, s) = + CaseV ("_", [ al_of_pack_size p; al_of_extension s ]) let al_of_loadop = al_of_opt al_of_pack_size_extension |> al_of_memop diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml index 4cec55b1a5..d0b3c87369 100644 --- a/spectec/src/backend-latex/render.ml +++ b/spectec/src/backend-latex/render.ml @@ -1128,7 +1128,7 @@ and render_nottyp env t : table = [Row [Col ( "\\{ " ^ render_table env "@{}" ["l"; "l"] 0 0 - (concat_table "" (render_nl_list env (`H, " ") render_typfield tfs) [Row [Col " \\}"]]) + (concat_table "" (render_nl_list env (`H, ", ") render_typfield tfs) [Row [Col " \\}"]]) )]] | CaseT (dots1, ts, tcs, dots2) -> let render env = function diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 963627b0eb..e7ae7d0a96 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -777,7 +777,7 @@ and handle_special_lhs lhs rhs free_ids = (match tag_opt with | Some ({ it = Atom.Atom _; _} as tag) -> [ ifI ( - inject_isCaseOf tag rhs, + inject_isCaseOf tag rhs, letI (caseE (op, es') ~at:lhs.at ~note:lhs.note, rhs) ~at:at :: translate_bindings free_ids bindings, [] diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 01598062b7..4c01f83384 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -1011,13 +1011,13 @@ syntax half__(shape_1 : shape, shape_2 : shape) syntax half__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M}(`%X%`_shape((Jnn_1 : Jnn <: lanetype), `%`_dim(M_1)), `%X%`_shape((Jnn_2 : Jnn <: lanetype), `%`_dim(M_2))) = | LOW | HIGH - -- if ((2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))) = $lsizenn1((Jnn_2 : Jnn <: lanetype))) + -- if ((2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))) = $lsizenn2((Jnn_2 : Jnn <: lanetype))) ;; 1-syntax.watsup syntax half__{Lnn_1 : Lnn, M_1 : M, Fnn_2 : Fnn, M_2 : M}(`%X%`_shape(Lnn_1, `%`_dim(M_1)), `%X%`_shape((Fnn_2 : Fnn <: lanetype), `%`_dim(M_2))) = | LOW - -- if (((2 * $lsizenn1(Lnn_1)) = $sizenn1((Fnn_2 : Fnn <: numtype))) /\ ($sizenn1((Fnn_2 : Fnn <: numtype)) = 64)) + -- if (((2 * $lsizenn1(Lnn_1)) = $sizenn2((Fnn_2 : Fnn <: numtype))) /\ ($sizenn2((Fnn_2 : Fnn <: numtype)) = 64)) ;; 1-syntax.watsup @@ -1214,7 +1214,7 @@ syntax memarg = ;; 1-syntax.watsup syntax loadop_{Inn : Inn}((Inn : Inn <: numtype)) = - | `%%`{sz : sz, sx : sx}(sz : sz, sx : sx) + | `%_%`{sz : sz, sx : sx}(sz : sz, sx : sx) -- if (sz!`%`_sz.0 < $sizenn((Inn : Inn <: numtype))) ;; 1-syntax.watsup @@ -1224,7 +1224,7 @@ syntax storeop_{Inn : Inn}((Inn : Inn <: numtype)) = ;; 1-syntax.watsup syntax vloadop_{vectype : vectype}(vectype) = - | `SHAPE%X%%`{sz : sz, M : M, sx : sx}(sz : sz, M : M, sx : sx) + | `SHAPE%X%_%`{sz : sz, M : M, sx : sx}(sz : sz, M : M, sx : sx) -- if (((sz!`%`_sz.0 * M) : nat <:> rat) = (($vsize(vectype) : nat <:> rat) / (2 : nat <:> rat))) | SPLAT{sz : sz}(sz : sz) | ZERO{sz : sz}(sz : sz) @@ -3802,7 +3802,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 3-typing.watsup:1089.1-1092.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: - `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) + `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) : nat <:> rat) <= ((M : nat <:> rat) / (8 : nat <:> rat))) @@ -3826,7 +3826,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 3-typing.watsup:1118.1-1121.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: - `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) + `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) : nat <:> rat) <= (((M : nat <:> rat) / (8 : nat <:> rat)) * (N : nat <:> rat))) @@ -6595,12 +6595,12 @@ relation Step_read: `%~>%`(config, instr*) ;; 8-reduction.watsup rule `load-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, n : n, sx : sx, x : idx, ao : memarg}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(n), sx)), x, ao)]), [TRAP_instr]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(n), sx)), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; 8-reduction.watsup rule `load-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, n : n, sx : sx, x : idx, ao : memarg, c : iN(n)}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(n), sx)), x, ao)]), [CONST_instr((Inn : Inn <: numtype), $extend__(n, $size((Inn : Inn <: numtype)), sx, c))]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(n), sx)), x, ao)]), [CONST_instr((Inn : Inn <: numtype), $extend__(n, $size((Inn : Inn <: numtype)), sx, c))]) -- if ($ibytes_(n, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) : (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) ;; 8-reduction.watsup @@ -6615,12 +6615,12 @@ relation Step_read: `%~>%`(config, instr*) ;; 8-reduction.watsup rule `vload-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), M : M, K : K, sx : sx, x : idx, ao : memarg}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [TRAP_instr]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + ((((M * K) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; 8-reduction.watsup rule `vload-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), M : M, K : K, sx : sx, x : idx, ao : memarg, c : vec_(V128_Vnn), `j*` : iN(M)*, `k*` : nat*, Jnn : Jnn}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [VCONST_instr(V128_vectype, c)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [VCONST_instr(V128_vectype, c)]) -- (if ($ibytes_(M, j) = $mem(z, x).BYTES_meminst[((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + ((((k * M) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) : (((M : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]))^(k%`(config, instr*) ;; 8-reduction.watsup rule `memory.copy-le`{z : state, at_1 : addrtype, i_1 : num_((at_1 : addrtype <: numtype)), at_2 : addrtype, i_2 : num_((at_2 : addrtype <: numtype)), at' : addrtype, n : n, x_1 : idx, x_2 : idx}: - `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), `%`_num_((i_1!`%`_num_.0 + 1))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_((i_2!`%`_num_.0 + 1))) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), `%`_num_((i_1!`%`_num_.0 + 1))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_((i_2!`%`_num_.0 + 1))) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) -- otherwise -- if (i_1!`%`_num_.0 <= i_2!`%`_num_.0) ;; 8-reduction.watsup rule `memory.copy-gt`{z : state, at_1 : addrtype, i_1 : num_((at_1 : addrtype <: numtype)), at_2 : addrtype, i_2 : num_((at_2 : addrtype <: numtype)), at' : addrtype, n : n, x_1 : idx, x_2 : idx}: - `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), `%`_num_(((((i_1!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_(((((i_2!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), `%`_num_(((((i_1!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_(((((i_2!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) -- otherwise ;; 8-reduction.watsup @@ -7683,26 +7683,26 @@ grammar Binstr : instr prod{x : idx, ao : memarg} {0x2A (x, ao):Bmemarg} => LOAD_instr(F32_numtype, ?(), x, ao) ;; A-binary.watsup:361.5-361.41 prod{x : idx, ao : memarg} {0x2B (x, ao):Bmemarg} => LOAD_instr(F64_numtype, ?(), x, ao) - ;; A-binary.watsup:362.5-362.48 - prod{x : idx, ao : memarg} {0x2C (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), S_sx)), x, ao) - ;; A-binary.watsup:363.5-363.48 - prod{x : idx, ao : memarg} {0x2D (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x, ao) - ;; A-binary.watsup:364.5-364.49 - prod{x : idx, ao : memarg} {0x2E (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(16), S_sx)), x, ao) - ;; A-binary.watsup:365.5-365.49 - prod{x : idx, ao : memarg} {0x2F (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(16), U_sx)), x, ao) - ;; A-binary.watsup:366.5-366.48 - prod{x : idx, ao : memarg} {0x30 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(8), S_sx)), x, ao) - ;; A-binary.watsup:367.5-367.48 - prod{x : idx, ao : memarg} {0x31 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x, ao) - ;; A-binary.watsup:368.5-368.49 - prod{x : idx, ao : memarg} {0x32 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(16), S_sx)), x, ao) - ;; A-binary.watsup:369.5-369.49 - prod{x : idx, ao : memarg} {0x33 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(16), U_sx)), x, ao) - ;; A-binary.watsup:370.5-370.49 - prod{x : idx, ao : memarg} {0x34 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(32), S_sx)), x, ao) - ;; A-binary.watsup:371.5-371.49 - prod{x : idx, ao : memarg} {0x35 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(32), U_sx)), x, ao) + ;; A-binary.watsup:362.5-362.50 + prod{x : idx, ao : memarg} {0x2C (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), S_sx)), x, ao) + ;; A-binary.watsup:363.5-363.50 + prod{x : idx, ao : memarg} {0x2D (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x, ao) + ;; A-binary.watsup:364.5-364.51 + prod{x : idx, ao : memarg} {0x2E (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(16), S_sx)), x, ao) + ;; A-binary.watsup:365.5-365.51 + prod{x : idx, ao : memarg} {0x2F (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(16), U_sx)), x, ao) + ;; A-binary.watsup:366.5-366.50 + prod{x : idx, ao : memarg} {0x30 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(8), S_sx)), x, ao) + ;; A-binary.watsup:367.5-367.50 + prod{x : idx, ao : memarg} {0x31 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x, ao) + ;; A-binary.watsup:368.5-368.51 + prod{x : idx, ao : memarg} {0x32 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(16), S_sx)), x, ao) + ;; A-binary.watsup:369.5-369.51 + prod{x : idx, ao : memarg} {0x33 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(16), U_sx)), x, ao) + ;; A-binary.watsup:370.5-370.51 + prod{x : idx, ao : memarg} {0x34 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(32), S_sx)), x, ao) + ;; A-binary.watsup:371.5-371.51 + prod{x : idx, ao : memarg} {0x35 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(32), U_sx)), x, ao) ;; A-binary.watsup:372.5-372.42 prod{x : idx, ao : memarg} {0x36 (x, ao):Bmemarg} => STORE_instr(I32_numtype, ?(), x, ao) ;; A-binary.watsup:373.5-373.42 @@ -8015,18 +8015,18 @@ grammar Binstr : instr prod {0xFC `%`_u32(7):Bu32} => CVTOP_instr(I64_numtype, F64_numtype, TRUNC_SAT_cvtop__(U_sx)) ;; A-binary.watsup:598.5-598.50 prod{x : idx, ao : memarg} {0xFD `%`_u32(0):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(), x, ao) - ;; A-binary.watsup:599.5-599.68 - prod{x : idx, ao : memarg} {0xFD `%`_u32(1):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(8), 8, S_sx)), x, ao) - ;; A-binary.watsup:600.5-600.68 - prod{x : idx, ao : memarg} {0xFD `%`_u32(2):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(8), 8, U_sx)), x, ao) - ;; A-binary.watsup:601.5-601.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(3):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(16), 4, S_sx)), x, ao) - ;; A-binary.watsup:602.5-602.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(4):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(16), 4, U_sx)), x, ao) - ;; A-binary.watsup:603.5-603.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(5):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(32), 2, S_sx)), x, ao) - ;; A-binary.watsup:604.5-604.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(6):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(32), 2, U_sx)), x, ao) + ;; A-binary.watsup:599.5-599.70 + prod{x : idx, ao : memarg} {0xFD `%`_u32(1):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(8), 8, S_sx)), x, ao) + ;; A-binary.watsup:600.5-600.70 + prod{x : idx, ao : memarg} {0xFD `%`_u32(2):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(8), 8, U_sx)), x, ao) + ;; A-binary.watsup:601.5-601.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(3):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(16), 4, S_sx)), x, ao) + ;; A-binary.watsup:602.5-602.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(4):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(16), 4, U_sx)), x, ao) + ;; A-binary.watsup:603.5-603.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(5):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(32), 2, S_sx)), x, ao) + ;; A-binary.watsup:604.5-604.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(6):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(32), 2, U_sx)), x, ao) ;; A-binary.watsup:605.5-605.61 prod{x : idx, ao : memarg} {0xFD `%`_u32(7):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(8))), x, ao) ;; A-binary.watsup:606.5-606.62 From 31aa55418a4d4fcc4caec1d071f9463bc102abcf Mon Sep 17 00:00:00 2001 From: DJ Date: Mon, 13 Jan 2025 14:54:10 +0900 Subject: [PATCH 2/2] Modify loadop for wasm 1 and 2 --- spectec/spec/wasm-1.0/1-syntax.watsup | 2 +- spectec/spec/wasm-1.0/6-typing.watsup | 4 +- spectec/spec/wasm-1.0/8-reduction.watsup | 4 +- spectec/spec/wasm-1.0/A-binary.watsup | 20 +- spectec/spec/wasm-2.0/1-syntax.watsup | 8 +- spectec/spec/wasm-2.0/6-typing.watsup | 6 +- spectec/spec/wasm-2.0/8-reduction.watsup | 12 +- spectec/spec/wasm-2.0/A-binary.watsup | 32 +-- spectec/test-latex/TEST.md | 65 +++--- spectec/test-middlend/TEST.md | 264 +++++++++++------------ spectec/test-prose/TEST.md | 118 +++++----- 11 files changed, 277 insertions(+), 258 deletions(-) diff --git a/spectec/spec/wasm-1.0/1-syntax.watsup b/spectec/spec/wasm-1.0/1-syntax.watsup index a52288d09b..f9bfe43ee7 100644 --- a/spectec/spec/wasm-1.0/1-syntax.watsup +++ b/spectec/spec/wasm-1.0/1-syntax.watsup @@ -184,7 +184,7 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32} var ao : memarg syntax loadop_(valtype) -syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $size(Inn) +syntax loadop_(Inn) = sz _ sx hint(show %0#_#%2) -- if sz < $size(Inn) ;; Instructions diff --git a/spectec/spec/wasm-1.0/6-typing.watsup b/spectec/spec/wasm-1.0/6-typing.watsup index 190b8142a8..2eec420acc 100644 --- a/spectec/spec/wasm-1.0/6-typing.watsup +++ b/spectec/spec/wasm-1.0/6-typing.watsup @@ -270,7 +270,7 @@ rule Instr_ok/memory.grow: (; rule Instr_ok/load: - C |- LOAD t (n sx)? memarg : I32 -> t + C |- LOAD t (n _ sx)? memarg : I32 -> t -- if C.MEMS[0] = mt -- if $(2^(memarg.ALIGN) <= $size(t)/8) -- if $(2^(memarg.ALIGN) <= n/8 < $size(t)/8)? @@ -283,7 +283,7 @@ rule Instr_ok/load-val: -- if $(2^(memarg.ALIGN) <= $size(t)/8) rule Instr_ok/load-pack: - C |- LOAD Inn (M sx) memarg : I32 -> Inn + C |- LOAD Inn (M _ sx) memarg : I32 -> Inn -- if C.MEMS[0] = mt -- if $(2^(memarg.ALIGN) <= M/8) diff --git a/spectec/spec/wasm-1.0/8-reduction.watsup b/spectec/spec/wasm-1.0/8-reduction.watsup index 407810159a..3bd8f5e7a1 100644 --- a/spectec/spec/wasm-1.0/8-reduction.watsup +++ b/spectec/spec/wasm-1.0/8-reduction.watsup @@ -233,11 +233,11 @@ rule Step_read/load-num-val: -- if $bytes_(t, c) = $mem(z, 0).BYTES[i + ao.OFFSET : $size(t)/8] rule Step_read/load-pack-trap: - z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> TRAP + z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> TRAP -- if $(i + ao.OFFSET + n/8 > |$mem(z, 0).BYTES|) rule Step_read/load-pack-val: - z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c)) + z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c)) -- if $ibytes_(n, c) = $mem(z, 0).BYTES[i + ao.OFFSET : n/8] diff --git a/spectec/spec/wasm-1.0/A-binary.watsup b/spectec/spec/wasm-1.0/A-binary.watsup index 803f46c6c5..0bfee6ab36 100644 --- a/spectec/spec/wasm-1.0/A-binary.watsup +++ b/spectec/spec/wasm-1.0/A-binary.watsup @@ -181,16 +181,16 @@ grammar Binstr/memory : instr = ... | 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 + | 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 diff --git a/spectec/spec/wasm-2.0/1-syntax.watsup b/spectec/spec/wasm-2.0/1-syntax.watsup index 6907f63143..ab4ec216bf 100644 --- a/spectec/spec/wasm-2.0/1-syntax.watsup +++ b/spectec/spec/wasm-2.0/1-syntax.watsup @@ -345,12 +345,12 @@ syntax memarg hint(desc "memory argument") = {ALIGN u32, OFFSET u32} var ao : memarg syntax loadop_(numtype) -syntax loadop_(Inn) = sz sx hint(show %0#_#%1) -- if sz < $sizenn(Inn) +syntax loadop_(Inn) = sz _ sx hint(show %0#_#%2) -- if sz < $sizenn(Inn) syntax vloadop = - | SHAPE nat X nat sx hint(show %#X#%#_#%) - | SPLAT nat hint(show %#_#SPLAT) - | ZERO nat hint(show %#_#ZERO) + | SHAPE nat X nat _ sx hint(show %1#X#%3#_#%5) + | SPLAT nat hint(show %#_#SPLAT) + | ZERO nat hint(show %#_#ZERO) ;; diff --git a/spectec/spec/wasm-2.0/6-typing.watsup b/spectec/spec/wasm-2.0/6-typing.watsup index b7a9fa6455..7806dd5a03 100644 --- a/spectec/spec/wasm-2.0/6-typing.watsup +++ b/spectec/spec/wasm-2.0/6-typing.watsup @@ -448,7 +448,7 @@ rule Instr_ok/data.drop: (; rule Instr_ok/load: - C |- LOAD nt (n sx)? memarg : I32 -> nt + C |- LOAD nt (n _ sx)? memarg : I32 -> nt -- if C.MEMS[0] = mt -- if $(2^(memarg.ALIGN) <= $size(nt)/8) -- if $(2^(memarg.ALIGN) <= n/8 < $size(nt)/8)? @@ -461,7 +461,7 @@ rule Instr_ok/load-val: -- if $(2^(memarg.ALIGN) <= $size(nt)/8) rule Instr_ok/load-pack: - C |- LOAD Inn (M sx) memarg : I32 -> Inn + C |- LOAD Inn (M _ sx) memarg : I32 -> Inn -- if C.MEMS[0] = mt -- if $(2^(memarg.ALIGN) <= M/8) @@ -485,7 +485,7 @@ rule Instr_ok/store-pack: -- if $(2^(memarg.ALIGN) <= M/8) rule Instr_ok/vload: - C |- VLOAD V128 (SHAPE M X N sx) memarg : I32 -> V128 + C |- VLOAD V128 (SHAPE M X N _ sx) memarg : I32 -> V128 -- if C.MEMS[0] = mt -- if $(2^(memarg.ALIGN) <= M/8 * N) diff --git a/spectec/spec/wasm-2.0/8-reduction.watsup b/spectec/spec/wasm-2.0/8-reduction.watsup index 01cfb44ea7..4e3b4d70d1 100644 --- a/spectec/spec/wasm-2.0/8-reduction.watsup +++ b/spectec/spec/wasm-2.0/8-reduction.watsup @@ -492,11 +492,11 @@ rule Step_read/load-num-val: -- if $nbytes_(nt, c) = $mem(z, 0).BYTES[i + ao.OFFSET : $size(nt)/8] rule Step_read/load-pack-trap: - z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> TRAP + z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> TRAP -- if $(i + ao.OFFSET + n/8 > |$mem(z, 0).BYTES|) rule Step_read/load-pack-val: - z; (CONST I32 i) (LOAD Inn (n sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c)) + z; (CONST I32 i) (LOAD Inn (n _ sx) ao) ~> (CONST Inn $extend__(n, $size(Inn), sx, c)) -- if $ibytes_(n, c) = $mem(z, 0).BYTES[i + ao.OFFSET : n/8] rule Step_read/vload-oob: @@ -509,11 +509,11 @@ rule Step_read/vload-val: rule Step_read/vload-shape-oob: - z; (CONST I32 i) (VLOAD V128 (SHAPE M X N sx) ao) ~> TRAP + z; (CONST I32 i) (VLOAD V128 (SHAPE M X N _ sx) ao) ~> TRAP -- if $(i + ao.OFFSET + M * N/8) > |$mem(z, 0).BYTES| rule Step_read/vload-shape-val: - z; (CONST I32 i) (VLOAD V128 (SHAPE M X N sx) ao) ~> (VCONST V128 c) + z; (CONST I32 i) (VLOAD V128 (SHAPE M X N _ sx) ao) ~> (VCONST V128 c) -- (if $ibytes_(M, j) = $mem(z, 0).BYTES[i + ao.OFFSET + k * M/8 : M/8])^(k - (CONST I32 j) (CONST I32 i) (LOAD I32 (8 U) $memarg0) (STORE I32 8 $memarg0) + (CONST I32 j) (CONST I32 i) (LOAD I32 (8 _ U) $memarg0) (STORE I32 8 $memarg0) (CONST I32 $(j+1)) (CONST I32 $(i+1)) (CONST I32 $(n-1)) (MEMORY.COPY) -- otherwise -- if j <= i rule Step_read/memory.copy-gt: z; (CONST I32 j) (CONST I32 i) (CONST I32 n) (MEMORY.COPY) ~> - (CONST I32 $(j+n-1)) (CONST I32 $(i+n-1)) (LOAD I32 (8 U) $memarg0) (STORE I32 8 $memarg0) + (CONST I32 $(j+n-1)) (CONST I32 $(i+n-1)) (LOAD I32 (8 _ U) $memarg0) (STORE I32 8 $memarg0) (CONST I32 j) (CONST I32 i) (CONST I32 $(n-1)) (MEMORY.COPY) -- otherwise diff --git a/spectec/spec/wasm-2.0/A-binary.watsup b/spectec/spec/wasm-2.0/A-binary.watsup index d3686843c2..012178babe 100644 --- a/spectec/spec/wasm-2.0/A-binary.watsup +++ b/spectec/spec/wasm-2.0/A-binary.watsup @@ -221,16 +221,16 @@ grammar Binstr/memory : instr = ... | 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 + | 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 @@ -454,12 +454,12 @@ grammar Blaneidx : laneidx = 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 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 diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index 8c7679a14d..9859a21a10 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -3027,14 +3027,14 @@ $$ $$ \begin{array}[t]{@{}lrrl@{}l@{}} -& {{\mathit{half}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}} & ::= & \mathsf{low} ~|~ \mathsf{high} & \quad \mbox{if}~ 2 \cdot N_1 = N_1 \\ -& {{\mathit{half}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{f}}{N}}_2}{\mathsf{x}}{M_2}} & ::= & \mathsf{low} & \quad \mbox{if}~ 2 \cdot N_1 = N_1 = \mathsf{{\scriptstyle 64}} \\ +& {{\mathit{half}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}} & ::= & \mathsf{low} ~|~ \mathsf{high} & \quad \mbox{if}~ 2 \cdot N_1 = N_2 \\ +& {{\mathit{half}}}_{{{{\mathsf{i}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{f}}{N}}_2}{\mathsf{x}}{M_2}} & ::= & \mathsf{low} & \quad \mbox{if}~ 2 \cdot N_1 = N_2 = 64 \\ \end{array} $$ $$ \begin{array}[t]{@{}lrrl@{}l@{}} -& {{\mathit{zero}}}_{{{{\mathsf{f}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}} & ::= & \mathsf{zero} & \quad \mbox{if}~ 2 \cdot N_2 = N_1 = \mathsf{{\scriptstyle 64}} \\ +& {{\mathit{zero}}}_{{{{\mathsf{f}}{N}}_1}{\mathsf{x}}{M_1}, {{{\mathsf{i}}{N}}_2}{\mathsf{x}}{M_2}} & ::= & \mathsf{zero} & \quad \mbox{if}~ 2 \cdot N_2 = N_1 = 64 \\ & {\mathit{vvunop}} & ::= & \mathsf{not} \\ & {\mathit{vvbinop}} & ::= & \mathsf{and} ~|~ \mathsf{andnot} ~|~ \mathsf{or} ~|~ \mathsf{xor} \\ & {\mathit{vvternop}} & ::= & \mathsf{bitselect} \\ @@ -3062,7 +3062,8 @@ $$ & & | & {\mathsf{relaxed\_q{\scriptstyle 15}mulr}}{\mathsf{\_}}{\mathsf{s}} & \quad \mbox{if}~ N = \mathsf{{\scriptstyle 16}} \\ & & | & {\mathsf{min}}{\mathsf{\_}}{{\mathit{sx}}} & \quad \mbox{if}~ N \leq \mathsf{{\scriptstyle 32}} \\ & & | & {\mathsf{max}}{\mathsf{\_}}{{\mathit{sx}}} & \quad \mbox{if}~ N \leq \mathsf{{\scriptstyle 32}} \\ -& {{\mathit{vbinop}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}} & ::= & \mathsf{add} ~|~ \mathsf{sub} ~|~ \mathsf{mul} ~|~ \mathsf{div} ~|~ \mathsf{min} ~|~ \mathsf{max} ~|~ \mathsf{pmin} ~|~ \mathsf{pmax} ~|~ \mathsf{relaxed\_min} ~|~ \mathsf{relaxed\_max} \\ +& {{\mathit{vbinop}}}_{{{\mathsf{f}}{N}}{\mathsf{x}}{M}} & ::= & \mathsf{add} ~|~ \mathsf{sub} ~|~ \mathsf{mul} ~|~ \mathsf{div} ~|~ \mathsf{min} ~|~ \mathsf{max} ~|~ \mathsf{pmin} ~|~ \mathsf{pmax} \\ +& & | & \mathsf{relaxed\_min} ~|~ \mathsf{relaxed\_max} \\ \end{array} $$ @@ -3138,14 +3139,14 @@ $$ $$ \begin{array}[t]{@{}lrrl@{}l@{}} \mbox{(memory argument)} & {\mathit{memarg}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{align}~{\mathit{u{\kern-0.1em\scriptstyle 32}}} \mathsf{offset}~{\mathit{u{\kern-0.1em\scriptstyle 32}}} \} \\ +\mathsf{align}~{\mathit{u{\kern-0.1em\scriptstyle 32}}} , \mathsf{offset}~{\mathit{u{\kern-0.1em\scriptstyle 32}}} \} \\ \end{array} \\ \end{array} $$ $$ \begin{array}[t]{@{}lrrl@{}l@{}} -& {{\mathit{loadop}}}_{{\mathsf{i}}{N}} & ::= & {\mathit{sz}}~{\mathit{sx}} & \quad \mbox{if}~ {\mathit{sz}} < N \\ +& {{\mathit{loadop}}}_{{\mathsf{i}}{N}} & ::= & {{\mathit{sz}}}{\mathsf{\_}}{{\mathit{sx}}} & \quad \mbox{if}~ {\mathit{sz}} < N \\ \end{array} $$ @@ -7052,7 +7053,7 @@ C{.}\mathsf{mems}{}[x] = {\mathit{at}}~{\mathit{lim}}~\mathsf{page} \qquad {2^{{\mathit{memarg}}{.}\mathsf{align}}} \leq M / 8 }{ -C \vdash {{\mathsf{i}}{N}{.}\mathsf{load}}{M~{\mathit{sx}}}~x~{\mathit{memarg}} : {\mathit{at}} \rightarrow {\mathsf{i}}{N} +C \vdash {{\mathsf{i}}{N}{.}\mathsf{load}}{{M}{\mathsf{\_}}{{\mathit{sx}}}}~x~{\mathit{memarg}} : {\mathit{at}} \rightarrow {\mathsf{i}}{N} } \, {[\textsc{\scriptsize T{-}load{-}pack}]} \qquad \end{array} @@ -8815,28 +8816,28 @@ $$ \mbox{(host function)} & {\mathit{hostfunc}} & ::= & \ldots \\ & {\mathit{code}} & ::= & {\mathit{func}} ~|~ {\mathit{hostfunc}} \\ \mbox{(function instance)} & {\mathit{funcinst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{type}~{\mathit{deftype}} \mathsf{module}~{\mathit{moduleinst}} \mathsf{code}~{\mathit{code}} \} \\ +\mathsf{type}~{\mathit{deftype}} , \mathsf{module}~{\mathit{moduleinst}} , \mathsf{code}~{\mathit{code}} \} \\ \end{array} \\ \mbox{(global instance)} & {\mathit{globalinst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{type}~{\mathit{globaltype}} \mathsf{value}~{\mathit{val}} \} \\ +\mathsf{type}~{\mathit{globaltype}} , \mathsf{value}~{\mathit{val}} \} \\ \end{array} \\ \mbox{(table instance)} & {\mathit{tableinst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{type}~{\mathit{tabletype}} \mathsf{refs}~{{\mathit{ref}}^\ast} \} \\ +\mathsf{type}~{\mathit{tabletype}} , \mathsf{refs}~{{\mathit{ref}}^\ast} \} \\ \end{array} \\ \mbox{(memory instance)} & {\mathit{meminst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{type}~{\mathit{memtype}} \mathsf{bytes}~{{\mathit{byte}}^\ast} \} \\ +\mathsf{type}~{\mathit{memtype}} , \mathsf{bytes}~{{\mathit{byte}}^\ast} \} \\ \end{array} \\ \mbox{(tag instance)} & {\mathit{taginst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} \mathsf{type}~{\mathit{tagtype}} \} \\ \end{array} \\ \mbox{(element instance)} & {\mathit{eleminst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{type}~{\mathit{elemtype}} \mathsf{refs}~{{\mathit{ref}}^\ast} \} \\ +\mathsf{type}~{\mathit{elemtype}} , \mathsf{refs}~{{\mathit{ref}}^\ast} \} \\ \end{array} \\ \mbox{(data instance)} & {\mathit{datainst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} \mathsf{bytes}~{{\mathit{byte}}^\ast} \} \\ \end{array} \\ \mbox{(export instance)} & {\mathit{exportinst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{name}~{\mathit{name}} \mathsf{addr}~{\mathit{externaddr}} \} \\ +\mathsf{name}~{\mathit{name}} , \mathsf{addr}~{\mathit{externaddr}} \} \\ \end{array} \\ \end{array} $$ @@ -8848,13 +8849,13 @@ $$ \mbox{(packed value)} & {\mathit{packval}} & ::= & {\mathit{packtype}}{.}\mathsf{pack}~{i}{N} \\ \mbox{(field value)} & {\mathit{fieldval}} & ::= & {\mathit{val}} ~|~ {\mathit{packval}} \\ \mbox{(structure instance)} & {\mathit{structinst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{type}~{\mathit{deftype}} \mathsf{fields}~{{\mathit{fieldval}}^\ast} \} \\ +\mathsf{type}~{\mathit{deftype}} , \mathsf{fields}~{{\mathit{fieldval}}^\ast} \} \\ \end{array} \\ \mbox{(array instance)} & {\mathit{arrayinst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{type}~{\mathit{deftype}} \mathsf{fields}~{{\mathit{fieldval}}^\ast} \} \\ +\mathsf{type}~{\mathit{deftype}} , \mathsf{fields}~{{\mathit{fieldval}}^\ast} \} \\ \end{array} \\ \mbox{(exception instance)} & {\mathit{exninst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{tag}~{\mathit{tagaddr}} \mathsf{fields}~{{\mathit{val}}^\ast} \} \\ +\mathsf{tag}~{\mathit{tagaddr}} , \mathsf{fields}~{{\mathit{val}}^\ast} \} \\ \end{array} \\ \end{array} $$ @@ -8894,7 +8895,7 @@ $$ \mathsf{exns}~{{\mathit{exninst}}^\ast} \} \\ \end{array} \\ \mbox{(frame)} & {\mathit{frame}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -\mathsf{locals}~{({{\mathit{val}}^?})^\ast} \mathsf{module}~{\mathit{moduleinst}} \} \\ +\mathsf{locals}~{({{\mathit{val}}^?})^\ast} , \mathsf{module}~{\mathit{moduleinst}} \} \\ \end{array} \\ \end{array} $$ @@ -10573,11 +10574,11 @@ $$ &&& \multicolumn{2}{@{}l@{}}{\quad \quad \mbox{if}~ {{\mathrm{bytes}}}_{{\mathit{nt}}}(c) = z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : {|{\mathit{nt}}|} / 8] } \\ -{[\textsc{\scriptsize E{-}load{-}pack{-}oob}]} \quad & z ; ({\mathit{at}}{.}\mathsf{const}~i)~({{\mathsf{i}}{N}{.}\mathsf{load}}{n~{\mathit{sx}}}~x~{\mathit{ao}}) & \hookrightarrow & \mathsf{trap} & \\ +{[\textsc{\scriptsize E{-}load{-}pack{-}oob}]} \quad & z ; ({\mathit{at}}{.}\mathsf{const}~i)~({{\mathsf{i}}{N}{.}\mathsf{load}}{{n}{\mathsf{\_}}{{\mathit{sx}}}}~x~{\mathit{ao}}) & \hookrightarrow & \mathsf{trap} & \\ &&& \multicolumn{2}{@{}l@{}}{\quad \quad \mbox{if}~ i + {\mathit{ao}}{.}\mathsf{offset} + n / 8 > {|z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}|} } \\ -{[\textsc{\scriptsize E{-}load{-}pack{-}val}]} \quad & z ; ({\mathit{at}}{.}\mathsf{const}~i)~({{\mathsf{i}}{N}{.}\mathsf{load}}{n~{\mathit{sx}}}~x~{\mathit{ao}}) & \hookrightarrow & ({\mathsf{i}}{N}{.}\mathsf{const}~{{{{\mathrm{extend}}}_{n, {|{\mathsf{i}}{N}|}}^{{\mathit{sx}}}}}{(c)}) & \\ +{[\textsc{\scriptsize E{-}load{-}pack{-}val}]} \quad & z ; ({\mathit{at}}{.}\mathsf{const}~i)~({{\mathsf{i}}{N}{.}\mathsf{load}}{{n}{\mathsf{\_}}{{\mathit{sx}}}}~x~{\mathit{ao}}) & \hookrightarrow & ({\mathsf{i}}{N}{.}\mathsf{const}~{{{{\mathrm{extend}}}_{n, {|{\mathsf{i}}{N}|}}^{{\mathit{sx}}}}}{(c)}) & \\ &&& \multicolumn{2}{@{}l@{}}{\quad \quad \mbox{if}~ {{\mathrm{bytes}}}_{{\mathsf{i}}{n}}(c) = z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : n / 8] } \\ @@ -10745,14 +10746,14 @@ $$ {[\textsc{\scriptsize E{-}memory.copy{-}le}]} \quad & z ; ({\mathit{at}}_1{.}\mathsf{const}~i_1)~({\mathit{at}}_2{.}\mathsf{const}~i_2)~({\mathit{at}'}{.}\mathsf{const}~n)~(\mathsf{memory{.}copy}~x_1~x_2) & \hookrightarrow & & \\ & \multicolumn{4}{@{}l@{}}{\quad \begin{array}[t]{@{}l@{}l@{}} -\begin{array}[t]{@{}l@{}} ({\mathit{at}}_1{.}\mathsf{const}~i_1)~({\mathit{at}}_2{.}\mathsf{const}~i_2)~({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{8~\mathsf{u}}~x_2)~({\mathsf{i{\scriptstyle 32}}{.}\mathsf{store}}{8}~x_1) \\ +\begin{array}[t]{@{}l@{}} ({\mathit{at}}_1{.}\mathsf{const}~i_1)~({\mathit{at}}_2{.}\mathsf{const}~i_2)~({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{8}{\mathsf{\_}}{\mathsf{u}}}~x_2)~({\mathsf{i{\scriptstyle 32}}{.}\mathsf{store}}{8}~x_1) \\ ({\mathit{at}}_1{.}\mathsf{const}~i_1 + 1)~({\mathit{at}}_2{.}\mathsf{const}~i_2 + 1)~({\mathit{at}'}{.}\mathsf{const}~n - 1)~(\mathsf{memory{.}copy}~x_1~x_2) \end{array} & \quad \mbox{otherwise, if}~ i_1 \leq i_2 \\ \end{array} } \\ {[\textsc{\scriptsize E{-}memory.copy{-}gt}]} \quad & z ; ({\mathit{at}}_1{.}\mathsf{const}~i_1)~({\mathit{at}}_2{.}\mathsf{const}~i_2)~({\mathit{at}'}{.}\mathsf{const}~n)~(\mathsf{memory{.}copy}~x_1~x_2) & \hookrightarrow & & \\ & \multicolumn{4}{@{}l@{}}{\quad \begin{array}[t]{@{}l@{}l@{}} -\begin{array}[t]{@{}l@{}} ({\mathit{at}}_1{.}\mathsf{const}~i_1 + n - 1)~({\mathit{at}}_2{.}\mathsf{const}~i_2 + n - 1)~({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{8~\mathsf{u}}~x_2)~({\mathsf{i{\scriptstyle 32}}{.}\mathsf{store}}{8}~x_1) \\ +\begin{array}[t]{@{}l@{}} ({\mathit{at}}_1{.}\mathsf{const}~i_1 + n - 1)~({\mathit{at}}_2{.}\mathsf{const}~i_2 + n - 1)~({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{8}{\mathsf{\_}}{\mathsf{u}}}~x_2)~({\mathsf{i{\scriptstyle 32}}{.}\mathsf{store}}{8}~x_1) \\ ({\mathit{at}}_1{.}\mathsf{const}~i_1)~({\mathit{at}}_2{.}\mathsf{const}~i_2)~({\mathit{at}'}{.}\mathsf{const}~n - 1)~(\mathsf{memory{.}copy}~x_1~x_2) \end{array} & \quad \mbox{otherwise} \\ \end{array} } \\ @@ -11491,16 +11492,16 @@ $$ & & | & \mathtt{0x29}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}}{.}\mathsf{load}~x~{\mathit{ao}} \\ & & | & \mathtt{0x2A}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & \mathsf{f{\scriptstyle 32}}{.}\mathsf{load}~x~{\mathit{ao}} \\ & & | & \mathtt{0x2B}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & \mathsf{f{\scriptstyle 64}}{.}\mathsf{load}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x2C}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 8}}~\mathsf{s}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x2D}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 8}}~\mathsf{u}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x2E}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 16}}~\mathsf{s}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x2F}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 16}}~\mathsf{u}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x30}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 8}}~\mathsf{s}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x31}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 8}}~\mathsf{u}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x32}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 16}}~\mathsf{s}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x33}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 16}}~\mathsf{u}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x34}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 32}}~\mathsf{s}}~x~{\mathit{ao}} \\ -& & | & \mathtt{0x35}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{\mathsf{{\scriptstyle 32}}~\mathsf{u}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x2C}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 8}}}{\mathsf{\_}}{\mathsf{s}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x2D}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 8}}}{\mathsf{\_}}{\mathsf{u}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x2E}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 16}}}{\mathsf{\_}}{\mathsf{s}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x2F}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 16}}}{\mathsf{\_}}{\mathsf{u}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x30}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 8}}}{\mathsf{\_}}{\mathsf{s}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x31}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 8}}}{\mathsf{\_}}{\mathsf{u}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x32}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 16}}}{\mathsf{\_}}{\mathsf{s}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x33}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 16}}}{\mathsf{\_}}{\mathsf{u}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x34}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 32}}}{\mathsf{\_}}{\mathsf{s}}}~x~{\mathit{ao}} \\ +& & | & \mathtt{0x35}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & {\mathsf{i{\scriptstyle 64}}{.}\mathsf{load}}{{\mathsf{{\scriptstyle 32}}}{\mathsf{\_}}{\mathsf{u}}}~x~{\mathit{ao}} \\ & & | & \mathtt{0x36}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 32}}{.}\mathsf{store}~x~{\mathit{ao}} \\ & & | & \mathtt{0x37}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & \mathsf{i{\scriptstyle 64}}{.}\mathsf{store}~x~{\mathit{ao}} \\ & & | & \mathtt{0x38}~~(x, {\mathit{ao}}){:}{\mathtt{memarg}} & \quad\Rightarrow\quad{} & \mathsf{f{\scriptstyle 32}}{.}\mathsf{store}~x~{\mathit{ao}} \\ @@ -12213,7 +12214,7 @@ $$ & {\mathit{sym}} & ::= & A_1 ~|~ A_2 \\ & & ::= & () \\ & r & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} -{\mathsf{field}}_{1}~A_1 {\mathsf{field}}_{2}~A_2 \ldots~ \} \\ +{\mathsf{field}}_{1}~A_1 , {\mathsf{field}}_{2}~A_2 , \ldots~ \} \\ \end{array} \\ & {\mathit{pth}} & ::= & {({}[ i ]~\mid~{.}\mathsf{field})^{+}} \\ \end{array} diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index 577ce1e187..3ad497e229 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -1001,13 +1001,13 @@ syntax half__(shape_1 : shape, shape_2 : shape) syntax half__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M}(`%X%`_shape((Jnn_1 : Jnn <: lanetype), `%`_dim(M_1)), `%X%`_shape((Jnn_2 : Jnn <: lanetype), `%`_dim(M_2))) = | LOW | HIGH - -- if ((2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))) = $lsizenn1((Jnn_2 : Jnn <: lanetype))) + -- if ((2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))) = $lsizenn2((Jnn_2 : Jnn <: lanetype))) ;; 1-syntax.watsup syntax half__{Lnn_1 : Lnn, M_1 : M, Fnn_2 : Fnn, M_2 : M}(`%X%`_shape(Lnn_1, `%`_dim(M_1)), `%X%`_shape((Fnn_2 : Fnn <: lanetype), `%`_dim(M_2))) = | LOW - -- if (((2 * $lsizenn1(Lnn_1)) = $sizenn1((Fnn_2 : Fnn <: numtype))) /\ ($sizenn1((Fnn_2 : Fnn <: numtype)) = 64)) + -- if (((2 * $lsizenn1(Lnn_1)) = $sizenn2((Fnn_2 : Fnn <: numtype))) /\ ($sizenn2((Fnn_2 : Fnn <: numtype)) = 64)) ;; 1-syntax.watsup @@ -1204,7 +1204,7 @@ syntax memarg = ;; 1-syntax.watsup syntax loadop_{Inn : Inn}((Inn : Inn <: numtype)) = - | `%%`{sz : sz, sx : sx}(sz : sz, sx : sx) + | `%_%`{sz : sz, sx : sx}(sz : sz, sx : sx) -- if (sz!`%`_sz.0 < $sizenn((Inn : Inn <: numtype))) ;; 1-syntax.watsup @@ -1214,7 +1214,7 @@ syntax storeop_{Inn : Inn}((Inn : Inn <: numtype)) = ;; 1-syntax.watsup syntax vloadop_{vectype : vectype}(vectype) = - | `SHAPE%X%%`{sz : sz, M : M, sx : sx}(sz : sz, M : M, sx : sx) + | `SHAPE%X%_%`{sz : sz, M : M, sx : sx}(sz : sz, M : M, sx : sx) -- if (((sz!`%`_sz.0 * M) : nat <:> rat) = (($vsize(vectype) : nat <:> rat) / (2 : nat <:> rat))) | SPLAT{sz : sz}(sz : sz) | ZERO{sz : sz}(sz : sz) @@ -3792,7 +3792,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 3-typing.watsup:1089.1-1092.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: - `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) + `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) : nat <:> rat) <= ((M : nat <:> rat) / (8 : nat <:> rat))) @@ -3816,7 +3816,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 3-typing.watsup:1118.1-1121.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: - `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) + `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) : nat <:> rat) <= (((M : nat <:> rat) / (8 : nat <:> rat)) * (N : nat <:> rat))) @@ -6585,12 +6585,12 @@ relation Step_read: `%~>%`(config, instr*) ;; 8-reduction.watsup rule `load-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, n : n, sx : sx, x : idx, ao : memarg}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(n), sx)), x, ao)]), [TRAP_instr]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(n), sx)), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; 8-reduction.watsup rule `load-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, n : n, sx : sx, x : idx, ao : memarg, c : iN(n)}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(n), sx)), x, ao)]), [CONST_instr((Inn : Inn <: numtype), $extend__(n, $size((Inn : Inn <: numtype)), sx, c))]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(n), sx)), x, ao)]), [CONST_instr((Inn : Inn <: numtype), $extend__(n, $size((Inn : Inn <: numtype)), sx, c))]) -- if ($ibytes_(n, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) : (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) ;; 8-reduction.watsup @@ -6605,12 +6605,12 @@ relation Step_read: `%~>%`(config, instr*) ;; 8-reduction.watsup rule `vload-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), M : M, K : K, sx : sx, x : idx, ao : memarg}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [TRAP_instr]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + ((((M * K) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; 8-reduction.watsup rule `vload-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), M : M, K : K, sx : sx, x : idx, ao : memarg, c : vec_(V128_Vnn), `j*` : iN(M)*, `k*` : nat*, Jnn : Jnn}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [VCONST_instr(V128_vectype, c)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [VCONST_instr(V128_vectype, c)]) -- (if ($ibytes_(M, j) = $mem(z, x).BYTES_meminst[((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + ((((k * M) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) : (((M : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]))^(k%`(config, instr*) ;; 8-reduction.watsup rule `memory.copy-le`{z : state, at_1 : addrtype, i_1 : num_((at_1 : addrtype <: numtype)), at_2 : addrtype, i_2 : num_((at_2 : addrtype <: numtype)), at' : addrtype, n : n, x_1 : idx, x_2 : idx}: - `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), `%`_num_((i_1!`%`_num_.0 + 1))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_((i_2!`%`_num_.0 + 1))) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), `%`_num_((i_1!`%`_num_.0 + 1))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_((i_2!`%`_num_.0 + 1))) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) -- otherwise -- if (i_1!`%`_num_.0 <= i_2!`%`_num_.0) ;; 8-reduction.watsup rule `memory.copy-gt`{z : state, at_1 : addrtype, i_1 : num_((at_1 : addrtype <: numtype)), at_2 : addrtype, i_2 : num_((at_2 : addrtype <: numtype)), at' : addrtype, n : n, x_1 : idx, x_2 : idx}: - `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), `%`_num_(((((i_1!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_(((((i_2!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), `%`_num_(((((i_1!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_(((((i_2!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) -- otherwise ;; 8-reduction.watsup @@ -7673,26 +7673,26 @@ grammar Binstr : instr prod{x : idx, ao : memarg} {0x2A (x, ao):Bmemarg} => LOAD_instr(F32_numtype, ?(), x, ao) ;; A-binary.watsup:361.5-361.41 prod{x : idx, ao : memarg} {0x2B (x, ao):Bmemarg} => LOAD_instr(F64_numtype, ?(), x, ao) - ;; A-binary.watsup:362.5-362.48 - prod{x : idx, ao : memarg} {0x2C (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), S_sx)), x, ao) - ;; A-binary.watsup:363.5-363.48 - prod{x : idx, ao : memarg} {0x2D (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x, ao) - ;; A-binary.watsup:364.5-364.49 - prod{x : idx, ao : memarg} {0x2E (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(16), S_sx)), x, ao) - ;; A-binary.watsup:365.5-365.49 - prod{x : idx, ao : memarg} {0x2F (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(16), U_sx)), x, ao) - ;; A-binary.watsup:366.5-366.48 - prod{x : idx, ao : memarg} {0x30 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(8), S_sx)), x, ao) - ;; A-binary.watsup:367.5-367.48 - prod{x : idx, ao : memarg} {0x31 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x, ao) - ;; A-binary.watsup:368.5-368.49 - prod{x : idx, ao : memarg} {0x32 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(16), S_sx)), x, ao) - ;; A-binary.watsup:369.5-369.49 - prod{x : idx, ao : memarg} {0x33 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(16), U_sx)), x, ao) - ;; A-binary.watsup:370.5-370.49 - prod{x : idx, ao : memarg} {0x34 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(32), S_sx)), x, ao) - ;; A-binary.watsup:371.5-371.49 - prod{x : idx, ao : memarg} {0x35 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(32), U_sx)), x, ao) + ;; A-binary.watsup:362.5-362.50 + prod{x : idx, ao : memarg} {0x2C (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), S_sx)), x, ao) + ;; A-binary.watsup:363.5-363.50 + prod{x : idx, ao : memarg} {0x2D (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x, ao) + ;; A-binary.watsup:364.5-364.51 + prod{x : idx, ao : memarg} {0x2E (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(16), S_sx)), x, ao) + ;; A-binary.watsup:365.5-365.51 + prod{x : idx, ao : memarg} {0x2F (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(16), U_sx)), x, ao) + ;; A-binary.watsup:366.5-366.50 + prod{x : idx, ao : memarg} {0x30 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(8), S_sx)), x, ao) + ;; A-binary.watsup:367.5-367.50 + prod{x : idx, ao : memarg} {0x31 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x, ao) + ;; A-binary.watsup:368.5-368.51 + prod{x : idx, ao : memarg} {0x32 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(16), S_sx)), x, ao) + ;; A-binary.watsup:369.5-369.51 + prod{x : idx, ao : memarg} {0x33 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(16), U_sx)), x, ao) + ;; A-binary.watsup:370.5-370.51 + prod{x : idx, ao : memarg} {0x34 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(32), S_sx)), x, ao) + ;; A-binary.watsup:371.5-371.51 + prod{x : idx, ao : memarg} {0x35 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(32), U_sx)), x, ao) ;; A-binary.watsup:372.5-372.42 prod{x : idx, ao : memarg} {0x36 (x, ao):Bmemarg} => STORE_instr(I32_numtype, ?(), x, ao) ;; A-binary.watsup:373.5-373.42 @@ -8005,18 +8005,18 @@ grammar Binstr : instr prod {0xFC `%`_u32(7):Bu32} => CVTOP_instr(I64_numtype, F64_numtype, TRUNC_SAT_cvtop__(U_sx)) ;; A-binary.watsup:598.5-598.50 prod{x : idx, ao : memarg} {0xFD `%`_u32(0):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(), x, ao) - ;; A-binary.watsup:599.5-599.68 - prod{x : idx, ao : memarg} {0xFD `%`_u32(1):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(8), 8, S_sx)), x, ao) - ;; A-binary.watsup:600.5-600.68 - prod{x : idx, ao : memarg} {0xFD `%`_u32(2):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(8), 8, U_sx)), x, ao) - ;; A-binary.watsup:601.5-601.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(3):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(16), 4, S_sx)), x, ao) - ;; A-binary.watsup:602.5-602.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(4):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(16), 4, U_sx)), x, ao) - ;; A-binary.watsup:603.5-603.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(5):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(32), 2, S_sx)), x, ao) - ;; A-binary.watsup:604.5-604.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(6):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(32), 2, U_sx)), x, ao) + ;; A-binary.watsup:599.5-599.70 + prod{x : idx, ao : memarg} {0xFD `%`_u32(1):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(8), 8, S_sx)), x, ao) + ;; A-binary.watsup:600.5-600.70 + prod{x : idx, ao : memarg} {0xFD `%`_u32(2):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(8), 8, U_sx)), x, ao) + ;; A-binary.watsup:601.5-601.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(3):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(16), 4, S_sx)), x, ao) + ;; A-binary.watsup:602.5-602.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(4):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(16), 4, U_sx)), x, ao) + ;; A-binary.watsup:603.5-603.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(5):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(32), 2, S_sx)), x, ao) + ;; A-binary.watsup:604.5-604.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(6):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(32), 2, U_sx)), x, ao) ;; A-binary.watsup:605.5-605.61 prod{x : idx, ao : memarg} {0xFD `%`_u32(7):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(8))), x, ao) ;; A-binary.watsup:606.5-606.62 @@ -9864,13 +9864,13 @@ syntax half__(shape_1 : shape, shape_2 : shape) syntax half__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M}(`%X%`_shape((Jnn_1 : Jnn <: lanetype), `%`_dim(M_1)), `%X%`_shape((Jnn_2 : Jnn <: lanetype), `%`_dim(M_2))) = | LOW | HIGH - -- if ((2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))) = $lsizenn1((Jnn_2 : Jnn <: lanetype))) + -- if ((2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))) = $lsizenn2((Jnn_2 : Jnn <: lanetype))) ;; 1-syntax.watsup syntax half__{Lnn_1 : Lnn, M_1 : M, Fnn_2 : Fnn, M_2 : M}(`%X%`_shape(Lnn_1, `%`_dim(M_1)), `%X%`_shape((Fnn_2 : Fnn <: lanetype), `%`_dim(M_2))) = | LOW - -- if (((2 * $lsizenn1(Lnn_1)) = $sizenn1((Fnn_2 : Fnn <: numtype))) /\ ($sizenn1((Fnn_2 : Fnn <: numtype)) = 64)) + -- if (((2 * $lsizenn1(Lnn_1)) = $sizenn2((Fnn_2 : Fnn <: numtype))) /\ ($sizenn2((Fnn_2 : Fnn <: numtype)) = 64)) ;; 1-syntax.watsup @@ -10067,7 +10067,7 @@ syntax memarg = ;; 1-syntax.watsup syntax loadop_{Inn : Inn}((Inn : Inn <: numtype)) = - | `%%`{sz : sz, sx : sx}(sz : sz, sx : sx) + | `%_%`{sz : sz, sx : sx}(sz : sz, sx : sx) -- if (sz!`%`_sz.0 < $sizenn((Inn : Inn <: numtype))) ;; 1-syntax.watsup @@ -10077,7 +10077,7 @@ syntax storeop_{Inn : Inn}((Inn : Inn <: numtype)) = ;; 1-syntax.watsup syntax vloadop_{vectype : vectype}(vectype) = - | `SHAPE%X%%`{sz : sz, M : M, sx : sx}(sz : sz, M : M, sx : sx) + | `SHAPE%X%_%`{sz : sz, M : M, sx : sx}(sz : sz, M : M, sx : sx) -- if (((sz!`%`_sz.0 * M) : nat <:> rat) = (($vsize(vectype) : nat <:> rat) / (2 : nat <:> rat))) | SPLAT{sz : sz}(sz : sz) | ZERO{sz : sz}(sz : sz) @@ -12655,7 +12655,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 3-typing.watsup:1089.1-1092.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: - `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) + `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) : nat <:> rat) <= ((M : nat <:> rat) / (8 : nat <:> rat))) @@ -12679,7 +12679,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 3-typing.watsup:1118.1-1121.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: - `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) + `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) : nat <:> rat) <= (((M : nat <:> rat) / (8 : nat <:> rat)) * (N : nat <:> rat))) @@ -15450,12 +15450,12 @@ relation Step_read: `%~>%`(config, instr*) ;; 8-reduction.watsup rule `load-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, n : n, sx : sx, x : idx, ao : memarg}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(n), sx)), x, ao)]), [TRAP_instr]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(n), sx)), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; 8-reduction.watsup rule `load-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, n : n, sx : sx, x : idx, ao : memarg, c : iN(n)}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(n), sx)), x, ao)]), [CONST_instr((Inn : Inn <: numtype), $extend__(n, $size((Inn : Inn <: numtype)), sx, c))]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(n), sx)), x, ao)]), [CONST_instr((Inn : Inn <: numtype), $extend__(n, $size((Inn : Inn <: numtype)), sx, c))]) -- if ($ibytes_(n, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) : (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) ;; 8-reduction.watsup @@ -15470,12 +15470,12 @@ relation Step_read: `%~>%`(config, instr*) ;; 8-reduction.watsup rule `vload-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), M : M, K : K, sx : sx, x : idx, ao : memarg}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [TRAP_instr]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + ((((M * K) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; 8-reduction.watsup rule `vload-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), M : M, K : K, sx : sx, x : idx, ao : memarg, c : vec_(V128_Vnn), `j*` : iN(M)*, `k*` : nat*, Jnn : Jnn}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [VCONST_instr(V128_vectype, c)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [VCONST_instr(V128_vectype, c)]) -- (if ($ibytes_(M, j) = $mem(z, x).BYTES_meminst[((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + ((((k * M) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) : (((M : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]))^(k%`(config, instr*) ;; 8-reduction.watsup rule `memory.copy-le`{z : state, at_1 : addrtype, i_1 : num_((at_1 : addrtype <: numtype)), at_2 : addrtype, i_2 : num_((at_2 : addrtype <: numtype)), at' : addrtype, n : n, x_1 : idx, x_2 : idx}: - `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), `%`_num_((i_1!`%`_num_.0 + 1))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_((i_2!`%`_num_.0 + 1))) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), `%`_num_((i_1!`%`_num_.0 + 1))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_((i_2!`%`_num_.0 + 1))) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) -- otherwise -- if (i_1!`%`_num_.0 <= i_2!`%`_num_.0) ;; 8-reduction.watsup rule `memory.copy-gt`{z : state, at_1 : addrtype, i_1 : num_((at_1 : addrtype <: numtype)), at_2 : addrtype, i_2 : num_((at_2 : addrtype <: numtype)), at' : addrtype, n : n, x_1 : idx, x_2 : idx}: - `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), `%`_num_(((((i_1!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_(((((i_2!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), `%`_num_(((((i_1!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_(((((i_2!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) -- otherwise ;; 8-reduction.watsup @@ -16538,26 +16538,26 @@ grammar Binstr : instr prod{x : idx, ao : memarg} {0x2A (x, ao):Bmemarg} => LOAD_instr(F32_numtype, ?(), x, ao) ;; A-binary.watsup:361.5-361.41 prod{x : idx, ao : memarg} {0x2B (x, ao):Bmemarg} => LOAD_instr(F64_numtype, ?(), x, ao) - ;; A-binary.watsup:362.5-362.48 - prod{x : idx, ao : memarg} {0x2C (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), S_sx)), x, ao) - ;; A-binary.watsup:363.5-363.48 - prod{x : idx, ao : memarg} {0x2D (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x, ao) - ;; A-binary.watsup:364.5-364.49 - prod{x : idx, ao : memarg} {0x2E (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(16), S_sx)), x, ao) - ;; A-binary.watsup:365.5-365.49 - prod{x : idx, ao : memarg} {0x2F (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(16), U_sx)), x, ao) - ;; A-binary.watsup:366.5-366.48 - prod{x : idx, ao : memarg} {0x30 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(8), S_sx)), x, ao) - ;; A-binary.watsup:367.5-367.48 - prod{x : idx, ao : memarg} {0x31 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x, ao) - ;; A-binary.watsup:368.5-368.49 - prod{x : idx, ao : memarg} {0x32 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(16), S_sx)), x, ao) - ;; A-binary.watsup:369.5-369.49 - prod{x : idx, ao : memarg} {0x33 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(16), U_sx)), x, ao) - ;; A-binary.watsup:370.5-370.49 - prod{x : idx, ao : memarg} {0x34 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(32), S_sx)), x, ao) - ;; A-binary.watsup:371.5-371.49 - prod{x : idx, ao : memarg} {0x35 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(32), U_sx)), x, ao) + ;; A-binary.watsup:362.5-362.50 + prod{x : idx, ao : memarg} {0x2C (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), S_sx)), x, ao) + ;; A-binary.watsup:363.5-363.50 + prod{x : idx, ao : memarg} {0x2D (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x, ao) + ;; A-binary.watsup:364.5-364.51 + prod{x : idx, ao : memarg} {0x2E (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(16), S_sx)), x, ao) + ;; A-binary.watsup:365.5-365.51 + prod{x : idx, ao : memarg} {0x2F (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(16), U_sx)), x, ao) + ;; A-binary.watsup:366.5-366.50 + prod{x : idx, ao : memarg} {0x30 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(8), S_sx)), x, ao) + ;; A-binary.watsup:367.5-367.50 + prod{x : idx, ao : memarg} {0x31 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x, ao) + ;; A-binary.watsup:368.5-368.51 + prod{x : idx, ao : memarg} {0x32 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(16), S_sx)), x, ao) + ;; A-binary.watsup:369.5-369.51 + prod{x : idx, ao : memarg} {0x33 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(16), U_sx)), x, ao) + ;; A-binary.watsup:370.5-370.51 + prod{x : idx, ao : memarg} {0x34 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(32), S_sx)), x, ao) + ;; A-binary.watsup:371.5-371.51 + prod{x : idx, ao : memarg} {0x35 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(32), U_sx)), x, ao) ;; A-binary.watsup:372.5-372.42 prod{x : idx, ao : memarg} {0x36 (x, ao):Bmemarg} => STORE_instr(I32_numtype, ?(), x, ao) ;; A-binary.watsup:373.5-373.42 @@ -16870,18 +16870,18 @@ grammar Binstr : instr prod {0xFC `%`_u32(7):Bu32} => CVTOP_instr(I64_numtype, F64_numtype, TRUNC_SAT_cvtop__(U_sx)) ;; A-binary.watsup:598.5-598.50 prod{x : idx, ao : memarg} {0xFD `%`_u32(0):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(), x, ao) - ;; A-binary.watsup:599.5-599.68 - prod{x : idx, ao : memarg} {0xFD `%`_u32(1):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(8), 8, S_sx)), x, ao) - ;; A-binary.watsup:600.5-600.68 - prod{x : idx, ao : memarg} {0xFD `%`_u32(2):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(8), 8, U_sx)), x, ao) - ;; A-binary.watsup:601.5-601.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(3):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(16), 4, S_sx)), x, ao) - ;; A-binary.watsup:602.5-602.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(4):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(16), 4, U_sx)), x, ao) - ;; A-binary.watsup:603.5-603.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(5):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(32), 2, S_sx)), x, ao) - ;; A-binary.watsup:604.5-604.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(6):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(32), 2, U_sx)), x, ao) + ;; A-binary.watsup:599.5-599.70 + prod{x : idx, ao : memarg} {0xFD `%`_u32(1):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(8), 8, S_sx)), x, ao) + ;; A-binary.watsup:600.5-600.70 + prod{x : idx, ao : memarg} {0xFD `%`_u32(2):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(8), 8, U_sx)), x, ao) + ;; A-binary.watsup:601.5-601.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(3):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(16), 4, S_sx)), x, ao) + ;; A-binary.watsup:602.5-602.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(4):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(16), 4, U_sx)), x, ao) + ;; A-binary.watsup:603.5-603.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(5):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(32), 2, S_sx)), x, ao) + ;; A-binary.watsup:604.5-604.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(6):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(32), 2, U_sx)), x, ao) ;; A-binary.watsup:605.5-605.61 prod{x : idx, ao : memarg} {0xFD `%`_u32(7):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(8))), x, ao) ;; A-binary.watsup:606.5-606.62 @@ -18729,13 +18729,13 @@ syntax half__(shape_1 : shape, shape_2 : shape) syntax half__{Jnn_1 : Jnn, M_1 : M, Jnn_2 : Jnn, M_2 : M}(`%X%`_shape((Jnn_1 : Jnn <: lanetype), `%`_dim(M_1)), `%X%`_shape((Jnn_2 : Jnn <: lanetype), `%`_dim(M_2))) = | LOW | HIGH - -- if ((2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))) = $lsizenn1((Jnn_2 : Jnn <: lanetype))) + -- if ((2 * $lsizenn1((Jnn_1 : Jnn <: lanetype))) = $lsizenn2((Jnn_2 : Jnn <: lanetype))) ;; 1-syntax.watsup syntax half__{Lnn_1 : Lnn, M_1 : M, Fnn_2 : Fnn, M_2 : M}(`%X%`_shape(Lnn_1, `%`_dim(M_1)), `%X%`_shape((Fnn_2 : Fnn <: lanetype), `%`_dim(M_2))) = | LOW - -- if (((2 * $lsizenn1(Lnn_1)) = $sizenn1((Fnn_2 : Fnn <: numtype))) /\ ($sizenn1((Fnn_2 : Fnn <: numtype)) = 64)) + -- if (((2 * $lsizenn1(Lnn_1)) = $sizenn2((Fnn_2 : Fnn <: numtype))) /\ ($sizenn2((Fnn_2 : Fnn <: numtype)) = 64)) ;; 1-syntax.watsup @@ -18932,7 +18932,7 @@ syntax memarg = ;; 1-syntax.watsup syntax loadop_{Inn : Inn}((Inn : Inn <: numtype)) = - | `%%`{sz : sz, sx : sx}(sz : sz, sx : sx) + | `%_%`{sz : sz, sx : sx}(sz : sz, sx : sx) -- if (sz!`%`_sz.0 < $sizenn((Inn : Inn <: numtype))) ;; 1-syntax.watsup @@ -18942,7 +18942,7 @@ syntax storeop_{Inn : Inn}((Inn : Inn <: numtype)) = ;; 1-syntax.watsup syntax vloadop_{vectype : vectype}(vectype) = - | `SHAPE%X%%`{sz : sz, M : M, sx : sx}(sz : sz, M : M, sx : sx) + | `SHAPE%X%_%`{sz : sz, M : M, sx : sx}(sz : sz, M : M, sx : sx) -- if (((sz!`%`_sz.0 * M) : nat <:> rat) = (($vsize(vectype) : nat <:> rat) / (2 : nat <:> rat))) | SPLAT{sz : sz}(sz : sz) | ZERO{sz : sz}(sz : sz) @@ -21610,7 +21610,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 3-typing.watsup:1089.1-1092.35 rule `load-pack`{C : context, Inn : Inn, M : M, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: - `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) + `%|-%:%`(C, LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(M), sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([(Inn : Inn <: valtype)]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) : nat <:> rat) <= ((M : nat <:> rat) / (8 : nat <:> rat))) @@ -21638,7 +21638,7 @@ relation Instr_ok: `%|-%:%`(context, instr, instrtype) ;; 3-typing.watsup:1118.1-1121.39 rule `vload-pack`{C : context, M : M, N : N, sx : sx, x : idx, memarg : memarg, at : addrtype, lim : limits}: - `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) + `%|-%:%`(C, VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), N, sx)), x, memarg), `%->_%%`_instrtype(`%`_resulttype([(at : addrtype <: valtype)]), [], `%`_resulttype([V128_valtype]))) -- if (x!`%`_idx.0 < |C.MEMS_context|) -- if (C.MEMS_context[x!`%`_idx.0] = `%%PAGE`_memtype(at, lim)) -- if (((2 ^ memarg.ALIGN_memarg!`%`_u32.0) : nat <:> rat) <= (((M : nat <:> rat) / (8 : nat <:> rat)) * (N : nat <:> rat))) @@ -24486,12 +24486,12 @@ relation Step_read: `%~>%`(config, instr*) ;; 8-reduction.watsup rule `load-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, n : n, sx : sx, x : idx, ao : memarg}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(n), sx)), x, ao)]), [TRAP_instr]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(n), sx)), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; 8-reduction.watsup rule `load-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, n : n, sx : sx, x : idx, ao : memarg, c : iN(n)}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%%`_loadop_(`%`_sz(n), sx)), x, ao)]), [CONST_instr((Inn : Inn <: numtype), $extend__(n, $size((Inn : Inn <: numtype)), sx, c))]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) LOAD_instr((Inn : Inn <: numtype), ?(`%_%`_loadop_(`%`_sz(n), sx)), x, ao)]), [CONST_instr((Inn : Inn <: numtype), $extend__(n, $size((Inn : Inn <: numtype)), sx, c))]) -- if ($ibytes_(n, c) = $mem(z, x).BYTES_meminst[(i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) : (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]) ;; 8-reduction.watsup @@ -24506,12 +24506,12 @@ relation Step_read: `%~>%`(config, instr*) ;; 8-reduction.watsup rule `vload-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), M : M, K : K, sx : sx, x : idx, ao : memarg}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [TRAP_instr]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [TRAP_instr]) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + ((((M * K) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) ;; 8-reduction.watsup rule `vload-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), M : M, K : K, sx : sx, x : idx, ao : memarg, c : vec_(V128_Vnn), `j*` : iN(M)*, `k*` : nat*, Jnn : Jnn}: - `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [VCONST_instr(V128_vectype, c)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(M), K, sx)), x, ao)]), [VCONST_instr(V128_vectype, c)]) -- (if ($ibytes_(M, j) = $mem(z, x).BYTES_meminst[((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u32.0) + ((((k * M) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) : (((M : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)]))^(k%`(config, instr*) ;; 8-reduction.watsup rule `memory.copy-le`{z : state, at_1 : addrtype, i_1 : num_((at_1 : addrtype <: numtype)), at_2 : addrtype, i_2 : num_((at_2 : addrtype <: numtype)), at' : addrtype, n : n, x_1 : idx, x_2 : idx}: - `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), `%`_num_((i_1!`%`_num_.0 + 1))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_((i_2!`%`_num_.0 + 1))) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), `%`_num_((i_1!`%`_num_.0 + 1))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_((i_2!`%`_num_.0 + 1))) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) -- otherwise -- if (i_1!`%`_num_.0 <= i_2!`%`_num_.0) ;; 8-reduction.watsup rule `memory.copy-gt`{z : state, at_1 : addrtype, i_1 : num_((at_1 : addrtype <: numtype)), at_2 : addrtype, i_2 : num_((at_2 : addrtype <: numtype)), at' : addrtype, n : n, x_1 : idx, x_2 : idx}: - `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), `%`_num_(((((i_1!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_(((((i_2!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) + `%~>%`(`%;%`_config(z, [CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_(n)) MEMORY.COPY_instr(x_1, x_2)]), [CONST_instr((at_1 : addrtype <: numtype), `%`_num_(((((i_1!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) CONST_instr((at_2 : addrtype <: numtype), `%`_num_(((((i_2!`%`_num_.0 + n) : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x_2, $memarg0) STORE_instr(I32_numtype, ?(`%`_storeop_(`%`_sz(8))), x_1, $memarg0) CONST_instr((at_1 : addrtype <: numtype), i_1) CONST_instr((at_2 : addrtype <: numtype), i_2) CONST_instr((at' : addrtype <: numtype), `%`_num_((((n : nat <:> int) - (1 : nat <:> int)) : int <:> nat))) MEMORY.COPY_instr(x_1, x_2)]) -- otherwise ;; 8-reduction.watsup @@ -25581,26 +25581,26 @@ grammar Binstr : instr prod{x : idx, ao : memarg} {0x2A (x, ao):Bmemarg} => LOAD_instr(F32_numtype, ?(), x, ao) ;; A-binary.watsup:361.5-361.41 prod{x : idx, ao : memarg} {0x2B (x, ao):Bmemarg} => LOAD_instr(F64_numtype, ?(), x, ao) - ;; A-binary.watsup:362.5-362.48 - prod{x : idx, ao : memarg} {0x2C (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), S_sx)), x, ao) - ;; A-binary.watsup:363.5-363.48 - prod{x : idx, ao : memarg} {0x2D (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x, ao) - ;; A-binary.watsup:364.5-364.49 - prod{x : idx, ao : memarg} {0x2E (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(16), S_sx)), x, ao) - ;; A-binary.watsup:365.5-365.49 - prod{x : idx, ao : memarg} {0x2F (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%%`_loadop_(`%`_sz(16), U_sx)), x, ao) - ;; A-binary.watsup:366.5-366.48 - prod{x : idx, ao : memarg} {0x30 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(8), S_sx)), x, ao) - ;; A-binary.watsup:367.5-367.48 - prod{x : idx, ao : memarg} {0x31 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(8), U_sx)), x, ao) - ;; A-binary.watsup:368.5-368.49 - prod{x : idx, ao : memarg} {0x32 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(16), S_sx)), x, ao) - ;; A-binary.watsup:369.5-369.49 - prod{x : idx, ao : memarg} {0x33 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(16), U_sx)), x, ao) - ;; A-binary.watsup:370.5-370.49 - prod{x : idx, ao : memarg} {0x34 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(32), S_sx)), x, ao) - ;; A-binary.watsup:371.5-371.49 - prod{x : idx, ao : memarg} {0x35 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%%`_loadop_(`%`_sz(32), U_sx)), x, ao) + ;; A-binary.watsup:362.5-362.50 + prod{x : idx, ao : memarg} {0x2C (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), S_sx)), x, ao) + ;; A-binary.watsup:363.5-363.50 + prod{x : idx, ao : memarg} {0x2D (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x, ao) + ;; A-binary.watsup:364.5-364.51 + prod{x : idx, ao : memarg} {0x2E (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(16), S_sx)), x, ao) + ;; A-binary.watsup:365.5-365.51 + prod{x : idx, ao : memarg} {0x2F (x, ao):Bmemarg} => LOAD_instr(I32_numtype, ?(`%_%`_loadop_(`%`_sz(16), U_sx)), x, ao) + ;; A-binary.watsup:366.5-366.50 + prod{x : idx, ao : memarg} {0x30 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(8), S_sx)), x, ao) + ;; A-binary.watsup:367.5-367.50 + prod{x : idx, ao : memarg} {0x31 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(8), U_sx)), x, ao) + ;; A-binary.watsup:368.5-368.51 + prod{x : idx, ao : memarg} {0x32 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(16), S_sx)), x, ao) + ;; A-binary.watsup:369.5-369.51 + prod{x : idx, ao : memarg} {0x33 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(16), U_sx)), x, ao) + ;; A-binary.watsup:370.5-370.51 + prod{x : idx, ao : memarg} {0x34 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(32), S_sx)), x, ao) + ;; A-binary.watsup:371.5-371.51 + prod{x : idx, ao : memarg} {0x35 (x, ao):Bmemarg} => LOAD_instr(I64_numtype, ?(`%_%`_loadop_(`%`_sz(32), U_sx)), x, ao) ;; A-binary.watsup:372.5-372.42 prod{x : idx, ao : memarg} {0x36 (x, ao):Bmemarg} => STORE_instr(I32_numtype, ?(), x, ao) ;; A-binary.watsup:373.5-373.42 @@ -25913,18 +25913,18 @@ grammar Binstr : instr prod {0xFC `%`_u32(7):Bu32} => CVTOP_instr(I64_numtype, F64_numtype, TRUNC_SAT_cvtop__(U_sx)) ;; A-binary.watsup:598.5-598.50 prod{x : idx, ao : memarg} {0xFD `%`_u32(0):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(), x, ao) - ;; A-binary.watsup:599.5-599.68 - prod{x : idx, ao : memarg} {0xFD `%`_u32(1):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(8), 8, S_sx)), x, ao) - ;; A-binary.watsup:600.5-600.68 - prod{x : idx, ao : memarg} {0xFD `%`_u32(2):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(8), 8, U_sx)), x, ao) - ;; A-binary.watsup:601.5-601.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(3):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(16), 4, S_sx)), x, ao) - ;; A-binary.watsup:602.5-602.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(4):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(16), 4, U_sx)), x, ao) - ;; A-binary.watsup:603.5-603.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(5):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(32), 2, S_sx)), x, ao) - ;; A-binary.watsup:604.5-604.69 - prod{x : idx, ao : memarg} {0xFD `%`_u32(6):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%%`_vloadop_(`%`_sz(32), 2, U_sx)), x, ao) + ;; A-binary.watsup:599.5-599.70 + prod{x : idx, ao : memarg} {0xFD `%`_u32(1):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(8), 8, S_sx)), x, ao) + ;; A-binary.watsup:600.5-600.70 + prod{x : idx, ao : memarg} {0xFD `%`_u32(2):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(8), 8, U_sx)), x, ao) + ;; A-binary.watsup:601.5-601.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(3):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(16), 4, S_sx)), x, ao) + ;; A-binary.watsup:602.5-602.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(4):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(16), 4, U_sx)), x, ao) + ;; A-binary.watsup:603.5-603.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(5):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(32), 2, S_sx)), x, ao) + ;; A-binary.watsup:604.5-604.71 + prod{x : idx, ao : memarg} {0xFD `%`_u32(6):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(`SHAPE%X%_%`_vloadop_(`%`_sz(32), 2, U_sx)), x, ao) ;; A-binary.watsup:605.5-605.61 prod{x : idx, ao : memarg} {0xFD `%`_u32(7):Bu32 (x, ao):Bmemarg} => VLOAD_instr(V128_vectype, ?(SPLAT_vloadop_(`%`_sz(8))), x, ao) ;; A-binary.watsup:606.5-606.62 diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 6530f6c444..a8e863d51f 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -467,7 +467,7 @@ The instruction :math:`({t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}{.}\mathsf{loa * The number type :math:`t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is equal to :math:`{\mathsf{i}}{n}`. - * :math:`{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 1}}}^?}` is equal to :math:`(M, {\mathit{sx}})`. + * :math:`{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 1}}}^?}` is equal to :math:`{M}{\mathsf{\_}}{{\mathit{sx}}}`. * The number type :math:`t_{\mathit{u{\kern-0.1em\scriptstyle 3}}}` is equal to :math:`{\mathsf{i}}{n}`. @@ -531,7 +531,7 @@ The instruction :math:`({t{.}\mathsf{load}}{\epsilon}~{\mathit{memarg}})` is val -The instruction :math:`({{\mathsf{i}}{n}{.}\mathsf{load}}{(M, {\mathit{sx}})}~{\mathit{memarg}})` is valid with the function type :math:`\mathsf{i{\scriptstyle 32}}~\rightarrow~{\mathsf{i}}{n}` if: +The instruction :math:`({{\mathsf{i}}{n}{.}\mathsf{load}}{{M}{\mathsf{\_}}{{\mathit{sx}}}}~{\mathit{memarg}})` is valid with the function type :math:`\mathsf{i{\scriptstyle 32}}~\rightarrow~{\mathsf{i}}{n}` if: * The memory type :math:`C{.}\mathsf{mems}{}[0]` exists. @@ -1388,7 +1388,9 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as 1) Let :math:`{\mathit{loadop\_{\scriptstyle 0}}}` be :math:`{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 1}}}^?}`. - #) Let :math:`(n, {\mathit{sx}})` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. + #) Assert: Due to validation, :math:`{\mathit{loadop\_{\scriptstyle 0}}}` is of the case :math:`\mathsf{\_}`. + + #) Let :math:`{n}{\mathsf{\_}}{{\mathit{sx}}}` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. #) If :math:`i + {\mathit{ao}}{.}\mathsf{offset} + n / 8 > {|z{.}\mathsf{mems}{}[0]{.}\mathsf{bytes}|}`, then: @@ -1400,7 +1402,9 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as 1) Let :math:`{\mathit{loadop\_{\scriptstyle 0}}}` be :math:`{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 1}}}^?}`. - #) Let :math:`(n, {\mathit{sx}})` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. + #) Assert: Due to validation, :math:`{\mathit{loadop\_{\scriptstyle 0}}}` is of the case :math:`\mathsf{\_}`. + + #) Let :math:`{n}{\mathsf{\_}}{{\mathit{sx}}}` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. #) Let :math:`c` be the result for which :math:`{{\mathrm{bytes}}}_{{\mathsf{i}}{n}}(c)` :math:`=` :math:`z{.}\mathsf{mems}{}[0]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : n / 8]`. @@ -3134,7 +3138,7 @@ Instr_ok/load - (2 ^ memarg.ALIGN) is less than or equal to ($size(t) / 8). - Or: - t_u1 is Inn. - - loadop__u1? is ?((M, sx)). + - loadop__u1? is ?(M _ sx). - t_u3 is Inn. - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). @@ -3167,7 +3171,7 @@ Instr_ok/load-val - (2 ^ memarg.ALIGN) is less than or equal to ($size(t) / 8). Instr_ok/load-pack -- the instruction (LOAD Inn ?((M, sx)) memarg) is valid with the function type [I32] -> [Inn] if: +- the instruction (LOAD Inn ?(M _ sx) memarg) is valid with the function type [I32] -> [Inn] if: - the memory type C.MEMS[0] exists. - C.MEMS[0] is mt. - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). @@ -3585,15 +3589,17 @@ Step_read/load t_u1 loadop__u1? ao 5. If the type of t_u1 is Inn, then: a. If loadop__u1? is defined, then: 1) Let ?(loadop__0) be loadop__u1?. - 2) Let (n, sx) be loadop__0. - 3) If (((i + ao.OFFSET) + (n / 8)) > |$mem(z, 0).BYTES|), then: + 2) Assert: Due to validation, loadop__0 is of the case _. + 3) Let n _ sx be loadop__0. + 4) If (((i + ao.OFFSET) + (n / 8)) > |$mem(z, 0).BYTES|), then: a) Trap. b. Let Inn be t_u1. c. If loadop__u1? is defined, then: 1) Let ?(loadop__0) be loadop__u1?. - 2) Let (n, sx) be loadop__0. - 3) Let c be $ibytes__1^-1(n, $mem(z, 0).BYTES[(i + ao.OFFSET) : (n / 8)]). - 4) Push the value (Inn.CONST $extend__(n, $size(Inn), sx, c)) to the stack. + 2) Assert: Due to validation, loadop__0 is of the case _. + 3) Let n _ sx be loadop__0. + 4) Let c be $ibytes__1^-1(n, $mem(z, 0).BYTES[(i + ao.OFFSET) : (n / 8)]). + 5) Push the value (Inn.CONST $extend__(n, $size(Inn), sx, c)) to the stack. Step_read/memory.size 1. Let z be the current state. @@ -5131,7 +5137,7 @@ The instruction :math:`({{\mathit{nt}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}{. * The number type :math:`{\mathit{nt}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is equal to :math:`{\mathsf{i}}{n}`. - * :math:`{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 1}}}^?}` is equal to :math:`(M, {\mathit{sx}})`. + * :math:`{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 1}}}^?}` is equal to :math:`{M}{\mathsf{\_}}{{\mathit{sx}}}`. * The value type :math:`t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is equal to :math:`{\mathsf{i}}{n}`. @@ -5179,7 +5185,7 @@ The instruction :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~{\mathit{vl * Either: - * :math:`{\mathit{vloadop}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is equal to :math:`({M}{\mathsf{x}}{\mathsf{x}}{\mathsf{\_}}{N})`. + * :math:`{\mathit{vloadop}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}` is equal to :math:`({M}{\mathsf{x}}{N}{\mathsf{\_}}{{\mathit{sx}}})`. * :math:`{2^{{\mathit{memarg}}{.}\mathsf{align}}}` is less than or equal to :math:`M / 8 \cdot N`. @@ -5277,7 +5283,7 @@ The instruction :math:`({{\mathit{nt}}{.}\mathsf{load}}{\epsilon}~{\mathit{memar -The instruction :math:`({{\mathsf{i}}{n}{.}\mathsf{load}}{(M, {\mathit{sx}})}~{\mathit{memarg}})` is valid with the function type :math:`\mathsf{i{\scriptstyle 32}}~\rightarrow~{\mathsf{i}}{n}` if: +The instruction :math:`({{\mathsf{i}}{n}{.}\mathsf{load}}{{M}{\mathsf{\_}}{{\mathit{sx}}}}~{\mathit{memarg}})` is valid with the function type :math:`\mathsf{i{\scriptstyle 32}}~\rightarrow~{\mathsf{i}}{n}` if: * The memory type :math:`C{.}\mathsf{mems}{}[0]` exists. @@ -5313,7 +5319,7 @@ The instruction :math:`({{\mathsf{i}}{n}{.}\mathsf{store}}{M}~{\mathit{memarg}}) -The instruction :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~({M}{\mathsf{x}}{\mathsf{x}}{\mathsf{\_}}{N})~{\mathit{memarg}})` is valid with the function type :math:`\mathsf{i{\scriptstyle 32}}~\rightarrow~\mathsf{v{\scriptstyle 128}}` if: +The instruction :math:`(\mathsf{v{\scriptstyle 128}}{.}\mathsf{load}~({M}{\mathsf{x}}{N}{\mathsf{\_}}{{\mathit{sx}}})~{\mathit{memarg}})` is valid with the function type :math:`\mathsf{i{\scriptstyle 32}}~\rightarrow~\mathsf{v{\scriptstyle 128}}` if: * The memory type :math:`C{.}\mathsf{mems}{}[0]` exists. @@ -6931,7 +6937,9 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as 1) Let :math:`{\mathit{loadop\_{\scriptstyle 0}}}` be :math:`{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 1}}}^?}`. - #) Let :math:`(n, {\mathit{sx}})` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. + #) Assert: Due to validation, :math:`{\mathit{loadop\_{\scriptstyle 0}}}` is of the case :math:`\mathsf{\_}`. + + #) Let :math:`{n}{\mathsf{\_}}{{\mathit{sx}}}` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. #) If :math:`i + {\mathit{ao}}{.}\mathsf{offset} + n / 8 > {|z{.}\mathsf{mems}{}[0]{.}\mathsf{bytes}|}`, then: @@ -6943,7 +6951,9 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as 1) Let :math:`{\mathit{loadop\_{\scriptstyle 0}}}` be :math:`{{\mathit{loadop\_u{\kern-0.1em\scriptstyle 1}}}^?}`. - #) Let :math:`(n, {\mathit{sx}})` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. + #) Assert: Due to validation, :math:`{\mathit{loadop\_{\scriptstyle 0}}}` is of the case :math:`\mathsf{\_}`. + + #) Let :math:`{n}{\mathsf{\_}}{{\mathit{sx}}}` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. #) Let :math:`c` be the result for which :math:`{{\mathrm{bytes}}}_{{\mathsf{i}}{n}}(c)` :math:`=` :math:`z{.}\mathsf{mems}{}[0]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : n / 8]`. @@ -6976,7 +6986,7 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as #. If :math:`{\mathit{vloadop}}_0` is of the case :math:`\mathsf{shape}`, then: - 1) Let :math:`({M}{\mathsf{x}}{\mathsf{x}}{\mathsf{\_}}{N})` be :math:`{\mathit{vloadop}}_0`. + 1) Let :math:`({M}{\mathsf{x}}{N}{\mathsf{\_}}{{\mathit{sx}}})` be :math:`{\mathit{vloadop}}_0`. #) If :math:`i + {\mathit{ao}}{.}\mathsf{offset} + M \cdot N / 8 > {|z{.}\mathsf{mems}{}[0]{.}\mathsf{bytes}|}`, then: @@ -7150,7 +7160,7 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as #) Push the value :math:`(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~i)` to the stack. - #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{(8, \mathsf{u})})`. + #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{8}{\mathsf{\_}}{\mathsf{u}}})`. #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{store}}{8})`. @@ -7164,7 +7174,7 @@ The module :math:`(\mathsf{module}~{{\mathit{type}}^\ast}~{{\mathit{import}}^\as #) Push the value :math:`(\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~i + n - 1)` to the stack. - #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{(8, \mathsf{u})})`. + #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{8}{\mathsf{\_}}{\mathsf{u}}})`. #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{store}}{8})`. @@ -10423,7 +10433,7 @@ Instr_ok/load - (2 ^ memarg.ALIGN) is less than or equal to ($size(nt) / 8). - Or: - nt_u1 is Inn. - - loadop__u1? is ?((M, sx)). + - loadop__u1? is ?(M _ sx). - t_u1 is Inn. - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). @@ -10447,7 +10457,7 @@ Instr_ok/vload - the memory type C.MEMS[0] exists. - C.MEMS[0] is mt. - Either: - - vloadop_u1 is (SHAPE M X N sx). + - vloadop_u1 is (SHAPE M X N _ sx). - (2 ^ memarg.ALIGN) is less than or equal to ((M / 8) * N). - Or: - vloadop_u1 is (SPLAT n). @@ -10498,7 +10508,7 @@ Instr_ok/load-val - (2 ^ memarg.ALIGN) is less than or equal to ($size(nt) / 8). Instr_ok/load-pack -- the instruction (LOAD Inn ?((M, sx)) memarg) is valid with the function type [I32] -> [Inn] if: +- the instruction (LOAD Inn ?(M _ sx) memarg) is valid with the function type [I32] -> [Inn] if: - the memory type C.MEMS[0] exists. - C.MEMS[0] is mt. - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). @@ -10516,7 +10526,7 @@ Instr_ok/store-pack - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). Instr_ok/vload -- the instruction (VLOAD V128 ?((SHAPE M X N sx)) memarg) is valid with the function type [I32] -> [V128] if: +- the instruction (VLOAD V128 ?((SHAPE M X N _ sx)) memarg) is valid with the function type [I32] -> [V128] if: - the memory type C.MEMS[0] exists. - C.MEMS[0] is mt. - (2 ^ memarg.ALIGN) is less than or equal to ((M / 8) * N). @@ -11307,15 +11317,17 @@ Step_read/load nt_u1 loadop__u1? ao 5. If the type of nt_u1 is Inn, then: a. If loadop__u1? is defined, then: 1) Let ?(loadop__0) be loadop__u1?. - 2) Let (n, sx) be loadop__0. - 3) If (((i + ao.OFFSET) + (n / 8)) > |$mem(z, 0).BYTES|), then: + 2) Assert: Due to validation, loadop__0 is of the case _. + 3) Let n _ sx be loadop__0. + 4) If (((i + ao.OFFSET) + (n / 8)) > |$mem(z, 0).BYTES|), then: a) Trap. b. Let Inn be nt_u1. c. If loadop__u1? is defined, then: 1) Let ?(loadop__0) be loadop__u1?. - 2) Let (n, sx) be loadop__0. - 3) Let c be $ibytes__1^-1(n, $mem(z, 0).BYTES[(i + ao.OFFSET) : (n / 8)]). - 4) Push the value (Inn.CONST $extend__(n, $size(Inn), sx, c)) to the stack. + 2) Assert: Due to validation, loadop__0 is of the case _. + 3) Let n _ sx be loadop__0. + 4) Let c be $ibytes__1^-1(n, $mem(z, 0).BYTES[(i + ao.OFFSET) : (n / 8)]). + 5) Push the value (Inn.CONST $extend__(n, $size(Inn), sx, c)) to the stack. Step_read/vload V128 vloadop_u1? ao 1. Let z be the current state. @@ -11329,7 +11341,7 @@ Step_read/vload V128 vloadop_u1? ao 6. Else: a. Let ?(vloadop_0) be vloadop_u1?. b. If vloadop_0 is of the case SHAPE, then: - 1) Let (SHAPE M X N sx) be vloadop_0. + 1) Let (SHAPE M X N _ sx) be vloadop_0. 2) If (((i + ao.OFFSET) + ((M * N) / 8)) > |$mem(z, 0).BYTES|), then: a) Trap. 3) Let j^N be $ibytes__1^-1(M, $mem(z, 0).BYTES[((i + ao.OFFSET) + ((k * M) / 8)) : (M / 8)])^(k {|z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}|}`, then: @@ -18524,7 +18538,9 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i 1) Let :math:`{\mathit{loadop\_{\scriptstyle 0}}}` be :math:`{{\mathit{loadop}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^?}`. - #) Let :math:`(n, {\mathit{sx}})` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. + #) Assert: Due to validation, :math:`{\mathit{loadop\_{\scriptstyle 0}}}` is of the case :math:`\mathsf{\_}`. + + #) Let :math:`{n}{\mathsf{\_}}{{\mathit{sx}}}` be :math:`{\mathit{loadop\_{\scriptstyle 0}}}`. #) Let :math:`c` be the result for which :math:`{{\mathrm{bytes}}}_{{\mathsf{i}}{n}}(c)` :math:`=` :math:`z{.}\mathsf{mems}{}[x]{.}\mathsf{bytes}{}[i + {\mathit{ao}}{.}\mathsf{offset} : n / 8]`. @@ -18735,7 +18751,7 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #) Push the value :math:`({\mathit{at}}_2{.}\mathsf{const}~i_2)` to the stack. - #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{(8, \mathsf{u})}~x_2)`. + #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{8}{\mathsf{\_}}{\mathsf{u}}}~x_2)`. #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{store}}{8}~x_1)`. @@ -18749,7 +18765,7 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i #) Push the value :math:`({\mathit{at}}_2{.}\mathsf{const}~i_2 + n - 1)` to the stack. - #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{(8, \mathsf{u})}~x_2)`. + #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{load}}{{8}{\mathsf{\_}}{\mathsf{u}}}~x_2)`. #) Execute the instruction :math:`({\mathsf{i{\scriptstyle 32}}{.}\mathsf{store}}{8}~x_1)`. @@ -25839,7 +25855,7 @@ Instr_ok/load - (2 ^ memarg.ALIGN) is less than or equal to ($size(nt) / 8). - Or: - nt_u1 is Inn. - - loadop_u1? is ?((M, sx)). + - loadop_u1? is ?(M _ sx). - t_u1 is Inn. - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). @@ -25866,7 +25882,7 @@ Instr_ok/vload - vloadop_u1? is ?(). - (2 ^ memarg.ALIGN) is less than or equal to ($vsize(V128) / 8). - Or: - - vloadop_u1? is ?((SHAPE M X N sx)). + - vloadop_u1? is ?((SHAPE M X N _ sx)). - (2 ^ memarg.ALIGN) is less than or equal to ((M / 8) * N). - Or: - vloadop_u1? is ?((SPLAT N)). @@ -25912,7 +25928,7 @@ Instr_ok/load-val - (2 ^ memarg.ALIGN) is less than or equal to ($size(nt) / 8). Instr_ok/load-pack -- the instruction (LOAD Inn ?((M, sx)) x memarg) is valid with the instruction type [at] -> [Inn] if: +- the instruction (LOAD Inn ?(M _ sx) x memarg) is valid with the instruction type [at] -> [Inn] if: - the memory type C.MEMS[x] exists. - C.MEMS[x] is at lim PAGE. - (2 ^ memarg.ALIGN) is less than or equal to (M / 8). @@ -25936,7 +25952,7 @@ Instr_ok/vload-val - (2 ^ memarg.ALIGN) is less than or equal to ($vsize(V128) / 8). Instr_ok/vload-pack -- the instruction (VLOAD V128 ?((SHAPE M X N sx)) x memarg) is valid with the instruction type [at] -> [V128] if: +- the instruction (VLOAD V128 ?((SHAPE M X N _ sx)) x memarg) is valid with the instruction type [at] -> [V128] if: - the memory type C.MEMS[x] exists. - C.MEMS[x] is at lim PAGE. - (2 ^ memarg.ALIGN) is less than or equal to ((M / 8) * N). @@ -27444,15 +27460,17 @@ Step_read/load nt_u1 loadop_u1? x ao 5. If the type of nt_u1 is Inn, then: a. If loadop_u1? is defined, then: 1) Let ?(loadop__0) be loadop_u1?. - 2) Let (n, sx) be loadop__0. - 3) If (((i + ao.OFFSET) + (n / 8)) > |$mem(z, x).BYTES|), then: + 2) Assert: Due to validation, loadop__0 is of the case _. + 3) Let n _ sx be loadop__0. + 4) If (((i + ao.OFFSET) + (n / 8)) > |$mem(z, x).BYTES|), then: a) Trap. b. Let Inn be nt_u1. c. If loadop_u1? is defined, then: 1) Let ?(loadop__0) be loadop_u1?. - 2) Let (n, sx) be loadop__0. - 3) Let c be $ibytes__1^-1(n, $mem(z, x).BYTES[(i + ao.OFFSET) : (n / 8)]). - 4) Push the value (Inn.CONST $extend__(n, $size(Inn), sx, c)) to the stack. + 2) Assert: Due to validation, loadop__0 is of the case _. + 3) Let n _ sx be loadop__0. + 4) Let c be $ibytes__1^-1(n, $mem(z, x).BYTES[(i + ao.OFFSET) : (n / 8)]). + 5) Push the value (Inn.CONST $extend__(n, $size(Inn), sx, c)) to the stack. Step_read/vload V128 vloadop_u1? x ao 1. Let z be the current state. @@ -27466,7 +27484,7 @@ Step_read/vload V128 vloadop_u1? x ao 6. Else: a. Let ?(vloadop__0) be vloadop_u1?. b. If vloadop__0 is of the case SHAPE, then: - 1) Let (SHAPE M X K sx) be vloadop__0. + 1) Let (SHAPE M X K _ sx) be vloadop__0. 2) If (((i + ao.OFFSET) + ((M * K) / 8)) > |$mem(z, x).BYTES|), then: a) Trap. 3) Let j^K be $ibytes__1^-1(M, $mem(z, x).BYTES[((i + ao.OFFSET) + ((k * M) / 8)) : (M / 8)])^(k