diff --git a/specification/wasm-3.0/4.0-execution.configurations.spectec b/specification/wasm-3.0/4.0-execution.configurations.spectec index f1a7284359..ca4e963a3e 100644 --- a/specification/wasm-3.0/4.0-execution.configurations.spectec +++ b/specification/wasm-3.0/4.0-execution.configurations.spectec @@ -54,7 +54,7 @@ var res : result ;; Instances -syntax hostfunc hint(desc "host function") hint(macro "%" "FI%") = `... +syntax hostfunc hint(desc "host function") hint(macro "%" "FI%") = _HOSTFUNC text syntax funccode hint(show code) hint(macro "funccode") = func | hostfunc syntax taginst hint(desc "tag instance") hint(macro "%" "HI%") = @@ -329,3 +329,18 @@ def $growmem(meminst, n) = meminst' -- if $(i' = |b*| / (64 * $Ki) + n) -- (if i' <= j)? -- if i' <= $(2^($size(at) - 16)) + + +;; Host functions + +syntax hostcallresult = + | RES store result hint(show %, %) + | BOT + +def $hostcall(hostfunc, store, val*) : hostcallresult* hint(show %4 <- %1(%2, %3)) +def $hostcall hint(builtin) + +def $lift_result(result) : instr* hint(show %) +def $lift_result(_VALS val*) = val* +def $lift_result(`(REF.EXN_ADDR a) THROW_REF) = (REF.EXN_ADDR a) THROW_REF +def $lift_result(TRAP) = TRAP diff --git a/specification/wasm-3.0/4.3-execution.instructions.spectec b/specification/wasm-3.0/4.3-execution.instructions.spectec index 04a132b661..65e3de4aeb 100644 --- a/specification/wasm-3.0/4.3-execution.instructions.spectec +++ b/specification/wasm-3.0/4.3-execution.instructions.spectec @@ -170,17 +170,32 @@ rule Step_read/call: z; (CALL x) ~> (REF.FUNC_ADDR a) (CALL_REF $funcinst(z)[a].TYPE) -- if $moduleinst(z).FUNCS[x] = a -rule Step_read/call_ref-null: - z; (REF.NULL_ADDR) (CALL_REF yy) ~> TRAP +rule Step/call_ref-null: + z; (REF.NULL_ADDR) (CALL_REF yy) ~> z; TRAP -rule Step_read/call_ref-func: - z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*)) +rule Step/call_ref-func: + z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> z; (FRAME_ m `{f} (LABEL_ m `{eps} instr*)) ---- -- if $funcinst(z)[a] = fi -- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m -- if fi.CODE = FUNC x (LOCAL t)* (instr*) -- if f = {LOCALS val^n ($default_(t))*, MODULE fi.MODULE} +rule Step/call_ref-hostfunc-res: + s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s'; f; $lift_result(result) + ---- + -- if $funcinst((s; f))[a] = fi + -- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m + -- if fi.CODE = _HOSTFUNC hf + -- if RES s' result <- $hostcall(_HOSTFUNC hf, s, val^n) + +rule Step/call_ref-hostfunc-div: + s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s; f; (REF.FUNC_ADDR a) (CALL_REF yy) + ---- + -- if $funcinst((s; f))[a] = fi + -- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m + -- if fi.CODE = _HOSTFUNC hf + -- if BOT <- $hostcall(_HOSTFUNC hf, s, val^n) rule Step_read/return_call: z; (RETURN_CALL x) ~> (REF.FUNC_ADDR a) (RETURN_CALL_REF $funcinst(z)[a].TYPE) diff --git a/specification/wasm-latest/4.0-execution.configurations.spectec b/specification/wasm-latest/4.0-execution.configurations.spectec index f1a7284359..ca4e963a3e 100644 --- a/specification/wasm-latest/4.0-execution.configurations.spectec +++ b/specification/wasm-latest/4.0-execution.configurations.spectec @@ -54,7 +54,7 @@ var res : result ;; Instances -syntax hostfunc hint(desc "host function") hint(macro "%" "FI%") = `... +syntax hostfunc hint(desc "host function") hint(macro "%" "FI%") = _HOSTFUNC text syntax funccode hint(show code) hint(macro "funccode") = func | hostfunc syntax taginst hint(desc "tag instance") hint(macro "%" "HI%") = @@ -329,3 +329,18 @@ def $growmem(meminst, n) = meminst' -- if $(i' = |b*| / (64 * $Ki) + n) -- (if i' <= j)? -- if i' <= $(2^($size(at) - 16)) + + +;; Host functions + +syntax hostcallresult = + | RES store result hint(show %, %) + | BOT + +def $hostcall(hostfunc, store, val*) : hostcallresult* hint(show %4 <- %1(%2, %3)) +def $hostcall hint(builtin) + +def $lift_result(result) : instr* hint(show %) +def $lift_result(_VALS val*) = val* +def $lift_result(`(REF.EXN_ADDR a) THROW_REF) = (REF.EXN_ADDR a) THROW_REF +def $lift_result(TRAP) = TRAP diff --git a/specification/wasm-latest/4.3-execution.instructions.spectec b/specification/wasm-latest/4.3-execution.instructions.spectec index 04a132b661..65e3de4aeb 100644 --- a/specification/wasm-latest/4.3-execution.instructions.spectec +++ b/specification/wasm-latest/4.3-execution.instructions.spectec @@ -170,17 +170,32 @@ rule Step_read/call: z; (CALL x) ~> (REF.FUNC_ADDR a) (CALL_REF $funcinst(z)[a].TYPE) -- if $moduleinst(z).FUNCS[x] = a -rule Step_read/call_ref-null: - z; (REF.NULL_ADDR) (CALL_REF yy) ~> TRAP +rule Step/call_ref-null: + z; (REF.NULL_ADDR) (CALL_REF yy) ~> z; TRAP -rule Step_read/call_ref-func: - z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> (FRAME_ m `{f} (LABEL_ m `{eps} instr*)) +rule Step/call_ref-func: + z; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> z; (FRAME_ m `{f} (LABEL_ m `{eps} instr*)) ---- -- if $funcinst(z)[a] = fi -- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m -- if fi.CODE = FUNC x (LOCAL t)* (instr*) -- if f = {LOCALS val^n ($default_(t))*, MODULE fi.MODULE} +rule Step/call_ref-hostfunc-res: + s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s'; f; $lift_result(result) + ---- + -- if $funcinst((s; f))[a] = fi + -- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m + -- if fi.CODE = _HOSTFUNC hf + -- if RES s' result <- $hostcall(_HOSTFUNC hf, s, val^n) + +rule Step/call_ref-hostfunc-div: + s; f; val^n (REF.FUNC_ADDR a) (CALL_REF yy) ~> s; f; (REF.FUNC_ADDR a) (CALL_REF yy) + ---- + -- if $funcinst((s; f))[a] = fi + -- Expand: fi.TYPE ~~ FUNC t_1^n -> t_2^m + -- if fi.CODE = _HOSTFUNC hf + -- if BOT <- $hostcall(_HOSTFUNC hf, s, val^n) rule Step_read/return_call: z; (RETURN_CALL x) ~> (REF.FUNC_ADDR a) (RETURN_CALL_REF $funcinst(z)[a].TYPE) diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md index 84c2e20c6c..fc92855151 100644 --- a/spectec/test-frontend/TEST.md +++ b/spectec/test-frontend/TEST.md @@ -5913,12 +5913,12 @@ syntax result = ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax hostfunc = - | `...` + | _HOSTFUNC(text) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax funccode = | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) - | `...` + | _HOSTFUNC(text) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax taginst = @@ -6329,6 +6329,23 @@ def $growmem(meminst : meminst, nat : nat) : meminst -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`} -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat))) +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +syntax hostcallresult = + | RES(store : store, result : result) + | BOT + +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +def $hostcall(hostfunc : hostfunc, store : store, val*) : hostcallresult* + +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +def $lift_result(result : result) : instr* + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result{`val*` : val*}(_VALS_result(val*{val <- `val*`})) = (val : val <: instr)*{val <- `val*`} + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result{a : addr}(`(REF.EXN_ADDR%)THROW_REF`_result(a)) = [`REF.EXN_ADDR`_instr(a) THROW_REF_instr] + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result(TRAP_result) = [TRAP_instr] + ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec relation Num_ok: `%|-%:%`(store, num, numtype) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec @@ -7456,131 +7473,147 @@ relation Step: `%~>%`(config, config) `%~>%`(`%;%`_config(`%;%`_state(s, f), [`FRAME_%{%}%`_instr(n, f', instr*{instr <- `instr*`})]), `%;%`_config(`%;%`_state(s', f), [`FRAME_%{%}%`_instr(n, f'', instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(`%;%`_state(s, f'), instr*{instr <- `instr*`}), `%;%`_config(`%;%`_state(s', f''), instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:227.1-231.49 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:184.1-190.59 + rule `call_ref-hostfunc-res`{s : store, f : frame, n : n, `val*` : val*, a : addr, yy : typeuse, s' : store, result : result, fi : funcinst, `t_1*` : valtype*, m : m, `t_2*` : valtype*, hf : text}: + `%~>%`(`%;%`_config(`%;%`_state(s, f), (val : val <: instr)^n{val <- `val*`} ++ [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)]), `%;%`_config(`%;%`_state(s', f), $lift_result(result))) + -- if ($funcinst(`%;%`_state(s, f))[a] = fi) + -- Expand: `%~~%`(fi.TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1^n{t_1 <- `t_1*`},), `%`_resulttype(t_2^m{t_2 <- `t_2*`},))) + -- if (fi.CODE_funcinst = _HOSTFUNC_funccode(hf)) + -- if (RES_hostcallresult(s', result) <- $hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})) + + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:192.1-198.49 + rule `call_ref-hostfunc-div`{s : store, f : frame, n : n, `val*` : val*, a : addr, yy : typeuse, fi : funcinst, `t_1*` : valtype*, m : m, `t_2*` : valtype*, hf : text}: + `%~>%`(`%;%`_config(`%;%`_state(s, f), (val : val <: instr)^n{val <- `val*`} ++ [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)]), `%;%`_config(`%;%`_state(s, f), [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)])) + -- if ($funcinst(`%;%`_state(s, f))[a] = fi) + -- Expand: `%~~%`(fi.TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1^n{t_1 <- `t_1*`},), `%`_resulttype(t_2^m{t_2 <- `t_2*`},))) + -- if (fi.CODE_funcinst = _HOSTFUNC_funccode(hf)) + -- if (BOT_hostcallresult <- $hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})) + + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:242.1-246.49 rule throw{z : state, n : n, `val*` : val*, x : idx, exn : exninst, a : addr, `t*` : valtype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [THROW_instr(x)]), `%;%`_config($add_exninst(z, [exn]), [`REF.EXN_ADDR`_instr(a) THROW_REF_instr])) -- Expand: `%~~%`($as_deftype($tag(z, x).TYPE_taginst), `FUNC%->%`_comptype(`%`_resulttype(t^n{t <- `t*`},), `%`_resulttype([],))) -- if (a = |$exninst(z)|) -- if (exn = {TAG $tagaddr(z)[x!`%`_idx.0], FIELDS val^n{val <- `val*`}}) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:305.1-306.56 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:320.1-321.56 rule `local.set`{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) `LOCAL.SET`_instr(x)]), `%;%`_config($with_local(z, x, val), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:318.1-319.58 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:333.1-334.58 rule `global.set`{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) `GLOBAL.SET`_instr(x)]), `%;%`_config($with_global(z, x, val), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:332.1-334.33 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:347.1-349.33 rule `table.set-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) `TABLE.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:336.1-338.32 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:351.1-353.32 rule `table.set-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) `TABLE.SET`_instr(x)]), `%;%`_config($with_table(z, x, i!`%`_num_.0, ref), [])) -- if (i!`%`_num_.0 < |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:347.1-350.46 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:362.1-365.46 rule `table.grow-succeed`{z : state, ref : ref, at : addrtype, n : n, x : idx, ti : tableinst}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `TABLE.GROW`_instr(x)]), `%;%`_config($with_tableinst(z, x, ti), [CONST_instr((at : addrtype <: numtype), `%`_num_(|$table(z, x).REFS_tableinst|,))])) -- if (ti = $growtable($table(z, x), n, ref)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:352.1-353.87 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:367.1-368.87 rule `table.grow-fail`{z : state, ref : ref, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `TABLE.GROW`_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int)),))])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:413.1-414.51 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:428.1-429.51 rule `elem.drop`{z : state, x : idx}: `%~>%`(`%;%`_config(z, [`ELEM.DROP`_instr(x)]), `%;%`_config($with_elem(z, x, []), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:497.1-500.60 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:512.1-515.60 rule `store-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:502.1-506.29 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:517.1-521.29 rule `store-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $nbytes_(nt, c)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:508.1-511.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:523.1-526.52 rule `store-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n,),)), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:513.1-517.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:528.1-532.52 rule `store-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n,),)), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $ibytes_(n, $wrap__($size((Inn : Inn <: numtype)), n, c))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:519.1-522.63 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:534.1-537.63 rule `vstore-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:524.1-527.31 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:539.1-542.31 rule `vstore-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $vbytes_(V128_vectype, c)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:530.1-533.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:545.1-548.52 rule `vstore_lane-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N,), x, ao, j)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:535.1-540.49 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:550.1-555.49 rule `vstore_lane-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx, `b*` : byte*, Jnn : Jnn, M : M}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N,), x, ao, j)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (N = $jsize(Jnn)) -- if ((M!`%`_M.0 : nat <:> rat) = ((128 : nat <:> rat) / (N : nat <:> rat))) -- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), M), c)[j!`%`_laneidx.0]!`%`_lane_.0,))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:549.1-552.37 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:564.1-567.37 rule `memory.grow-succeed`{z : state, at : addrtype, n : n, x : idx, mi : meminst}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `MEMORY.GROW`_instr(x)]), `%;%`_config($with_meminst(z, x, mi), [CONST_instr((at : addrtype <: numtype), `%`_num_((((|$mem(z, x).BYTES_meminst| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) : rat <:> nat),))])) -- if (mi = $growmem($mem(z, x), n)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:554.1-555.84 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:569.1-570.84 rule `memory.grow-fail`{z : state, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `MEMORY.GROW`_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int)),))])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:615.1-616.51 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:630.1-631.51 rule `data.drop`{z : state, x : idx}: `%~>%`(`%;%`_config(z, [`DATA.DROP`_instr(x)]), `%;%`_config($with_data(z, x, []), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:692.1-696.65 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:707.1-711.65 rule `struct.new`{z : state, n : n, `val*` : val*, x : idx, si : structinst, a : addr, `mut?*` : mut?*, `zt*` : storagetype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [`STRUCT.NEW`_instr(x)]), `%;%`_config($add_structinst(z, [si]), [`REF.STRUCT_ADDR`_instr(a)])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)^n{`mut?` <- `mut?*`, zt <- `zt*`},))) -- if (a = |$structinst(z)|) -- if (si = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`, zt <- `zt*`}}) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:713.1-714.55 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:728.1-729.55 rule `struct.set-null`{z : state, val : val, x : idx, i : fieldidx}: `%~>%`(`%;%`_config(z, [`REF.NULL_ADDR`_instr (val : val <: instr) `STRUCT.SET`_instr(x, i)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:716.1-719.46 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:731.1-734.46 rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : fieldidx, `zt*` : storagetype*, `mut?*` : mut?*}: `%~>%`(`%;%`_config(z, [`REF.STRUCT_ADDR`_instr(a) (val : val <: instr) `STRUCT.SET`_instr(x, i)]), `%;%`_config($with_struct(z, a, i!`%`_fieldidx.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_fieldidx.0], val)), [])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`},))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:732.1-737.65 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:747.1-752.65 rule `array.new_fixed`{z : state, n : n, `val*` : val*, x : idx, ai : arrayinst, a : addr, `mut?` : mut?, zt : storagetype}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [`ARRAY.NEW_FIXED`_instr(x, `%`_u32(n,))]), `%;%`_config($add_arrayinst(z, [ai]), [`REF.ARRAY_ADDR`_instr(a)])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((a = |$arrayinst(z)|) /\ (ai = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`}})) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:777.1-778.66 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:792.1-793.66 rule `array.set-null`{z : state, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [`REF.NULL_ADDR`_instr CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:780.1-782.39 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:795.1-797.39 rule `array.set-oob`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$arrayinst(z)[a].FIELDS_arrayinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:784.1-787.44 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:799.1-802.44 rule `array.set-array`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx, zt : storagetype, `mut?` : mut?}: `%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config($with_array(z, a, i!`%`_num_.0, $packfield_(zt, val)), [])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index b856ee9989..fda5c5d0b8 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -8963,7 +8963,7 @@ $$ $$ \begin{array}[t]{@{}lrrl@{}l@{}} -\mbox{(host function)} & {\mathit{hostfunc}} & ::= & \ldots \\ +\mbox{(host function)} & {\mathit{hostfunc}} & ::= & \mathbb{T} \\ & {\mathit{code}} & ::= & {\mathit{func}} ~~|~~ {\mathit{hostfunc}} \\ \mbox{(tag instance)} & {\mathit{taginst}} & ::= & \{ \begin{array}[t]{@{}l@{}l@{}} \mathsf{type}~{\mathit{tagtype}} \} \\ @@ -9406,6 +9406,23 @@ $$ \vspace{1ex} +$$ +\begin{array}[t]{@{}lrrl@{}l@{}} +& {\mathit{hostcallresult}} & ::= & {\mathit{store}}, {\mathit{result}} \\ +& & | & \mathsf{bot} \\ +\end{array} +$$ + +$$ +\begin{array}[t]{@{}lcl@{}l@{}} +{{\mathit{val}}^\ast} & = & {{\mathit{val}}^\ast} \\ +( \mathsf{ref{.}exn\_addr}~a )~\mathsf{throw\_ref} & = & (\mathsf{ref{.}exn}~a)~\mathsf{throw\_ref} \\ +\mathsf{trap} & = & \mathsf{trap} \\ +\end{array} +$$ + +\vspace{1ex} + $$ \begin{array}[t]{@{}lcl@{}l@{}} {{\mathrm{default}}}_{{\mathsf{i}}{N}} & = & ({\mathsf{i}}{N}{.}\mathsf{const}~0) \\ @@ -9925,7 +9942,30 @@ $$ \end{array} $$ -\vspace{1ex} +$$ +\begin{array}[t]{@{}lrcl@{}l@{}} +{[\textsc{\scriptsize E{-}call\_ref{-}hostfunc{-}res}]} \quad & s ; f ; {{\mathit{val}}^{n}}~(\mathsf{ref{.}func}~a)~(\mathsf{call\_ref}~y) & \hookrightarrow & {s'} ; f ; {\mathit{result}} & \\ +&&& \multicolumn{2}{@{}l@{}}{\quad +\quad +\begin{array}[t]{@{}l@{}} +\mbox{if}~ (s ; f){.}\mathsf{funcs}{}[a] = {\mathit{fi}} \\ +{\land}~ {\mathit{fi}}{.}\mathsf{type} \approx \mathsf{func}~{t_1^{n}} \rightarrow {t_2^{m}} \\ +{\land}~ {\mathit{fi}}{.}\mathsf{code} = {\mathit{hf}} \\ +{\land}~ {s'}, {\mathit{result}} \in {\mathrm{hostcall}}({\mathit{hf}}, s, {{\mathit{val}}^{n}}) \\ +\end{array} +} \\ +{[\textsc{\scriptsize E{-}call\_ref{-}hostfunc{-}div}]} \quad & s ; f ; {{\mathit{val}}^{n}}~(\mathsf{ref{.}func}~a)~(\mathsf{call\_ref}~y) & \hookrightarrow & s ; f ; (\mathsf{ref{.}func}~a)~(\mathsf{call\_ref}~y) & \\ +&&& \multicolumn{2}{@{}l@{}}{\quad +\quad +\begin{array}[t]{@{}l@{}} +\mbox{if}~ (s ; f){.}\mathsf{funcs}{}[a] = {\mathit{fi}} \\ +{\land}~ {\mathit{fi}}{.}\mathsf{type} \approx \mathsf{func}~{t_1^{n}} \rightarrow {t_2^{m}} \\ +{\land}~ {\mathit{fi}}{.}\mathsf{code} = {\mathit{hf}} \\ +{\land}~ \mathsf{bot} \in {\mathrm{hostcall}}({\mathit{hf}}, s, {{\mathit{val}}^{n}}) \\ +\end{array} +} \\ +\end{array} +$$ $$ \begin{array}[t]{@{}lrcl@{}l@{}} diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md index cbda7bd91c..a01ea239e8 100644 --- a/spectec/test-middlend/TEST.md +++ b/spectec/test-middlend/TEST.md @@ -5436,12 +5436,12 @@ syntax result = ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax hostfunc = - | `...` + | _HOSTFUNC(text) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax funccode = | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) - | `...` + | _HOSTFUNC(text) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax taginst = @@ -5852,6 +5852,23 @@ def $growmem(meminst : meminst, nat : nat) : meminst -- (if (i'!`%`_u64.0 <= j!`%`_u64.0))?{j <- `j?`} -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat))) +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +syntax hostcallresult = + | RES(store : store, result : result) + | BOT + +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +def $hostcall(hostfunc : hostfunc, store : store, val*) : hostcallresult* + +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +def $lift_result(result : result) : instr* + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result{`val*` : val*}(_VALS_result(val*{val <- `val*`})) = (val : val <: instr)*{val <- `val*`} + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result{a : addr}(`(REF.EXN_ADDR%)THROW_REF`_result(a)) = [`REF.EXN_ADDR`_instr(a) THROW_REF_instr] + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result(TRAP_result) = [TRAP_instr] + ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec relation Num_ok: `%|-%:%`(store, num, numtype) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec @@ -6979,131 +6996,147 @@ relation Step: `%~>%`(config, config) `%~>%`(`%;%`_config(`%;%`_state(s, f), [`FRAME_%{%}%`_instr(n, f', instr*{instr <- `instr*`})]), `%;%`_config(`%;%`_state(s', f), [`FRAME_%{%}%`_instr(n, f'', instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(`%;%`_state(s, f'), instr*{instr <- `instr*`}), `%;%`_config(`%;%`_state(s', f''), instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:227.1-231.49 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:184.1-190.59 + rule `call_ref-hostfunc-res`{s : store, f : frame, n : n, `val*` : val*, a : addr, yy : typeuse, s' : store, result : result, fi : funcinst, `t_1*` : valtype*, m : m, `t_2*` : valtype*, hf : text}: + `%~>%`(`%;%`_config(`%;%`_state(s, f), (val : val <: instr)^n{val <- `val*`} ++ [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)]), `%;%`_config(`%;%`_state(s', f), $lift_result(result))) + -- if ($funcinst(`%;%`_state(s, f))[a] = fi) + -- Expand: `%~~%`(fi.TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1^n{t_1 <- `t_1*`},), `%`_resulttype(t_2^m{t_2 <- `t_2*`},))) + -- if (fi.CODE_funcinst = _HOSTFUNC_funccode(hf)) + -- if (RES_hostcallresult(s', result) <- $hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})) + + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:192.1-198.49 + rule `call_ref-hostfunc-div`{s : store, f : frame, n : n, `val*` : val*, a : addr, yy : typeuse, fi : funcinst, `t_1*` : valtype*, m : m, `t_2*` : valtype*, hf : text}: + `%~>%`(`%;%`_config(`%;%`_state(s, f), (val : val <: instr)^n{val <- `val*`} ++ [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)]), `%;%`_config(`%;%`_state(s, f), [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)])) + -- if ($funcinst(`%;%`_state(s, f))[a] = fi) + -- Expand: `%~~%`(fi.TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1^n{t_1 <- `t_1*`},), `%`_resulttype(t_2^m{t_2 <- `t_2*`},))) + -- if (fi.CODE_funcinst = _HOSTFUNC_funccode(hf)) + -- if (BOT_hostcallresult <- $hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})) + + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:242.1-246.49 rule throw{z : state, n : n, `val*` : val*, x : idx, exn : exninst, a : addr, `t*` : valtype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [THROW_instr(x)]), `%;%`_config($add_exninst(z, [exn]), [`REF.EXN_ADDR`_instr(a) THROW_REF_instr])) -- Expand: `%~~%`($as_deftype($tag(z, x).TYPE_taginst), `FUNC%->%`_comptype(`%`_resulttype(t^n{t <- `t*`},), `%`_resulttype([],))) -- if (a = |$exninst(z)|) -- if (exn = {TAG $tagaddr(z)[x!`%`_idx.0], FIELDS val^n{val <- `val*`}}) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:305.1-306.56 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:320.1-321.56 rule `local.set`{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) `LOCAL.SET`_instr(x)]), `%;%`_config($with_local(z, x, val), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:318.1-319.58 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:333.1-334.58 rule `global.set`{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) `GLOBAL.SET`_instr(x)]), `%;%`_config($with_global(z, x, val), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:332.1-334.33 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:347.1-349.33 rule `table.set-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) `TABLE.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:336.1-338.32 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:351.1-353.32 rule `table.set-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) `TABLE.SET`_instr(x)]), `%;%`_config($with_table(z, x, i!`%`_num_.0, ref), [])) -- if (i!`%`_num_.0 < |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:347.1-350.46 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:362.1-365.46 rule `table.grow-succeed`{z : state, ref : ref, at : addrtype, n : n, x : idx, ti : tableinst}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `TABLE.GROW`_instr(x)]), `%;%`_config($with_tableinst(z, x, ti), [CONST_instr((at : addrtype <: numtype), `%`_num_(|$table(z, x).REFS_tableinst|,))])) -- if (ti = $growtable($table(z, x), n, ref)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:352.1-353.87 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:367.1-368.87 rule `table.grow-fail`{z : state, ref : ref, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `TABLE.GROW`_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int)),))])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:413.1-414.51 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:428.1-429.51 rule `elem.drop`{z : state, x : idx}: `%~>%`(`%;%`_config(z, [`ELEM.DROP`_instr(x)]), `%;%`_config($with_elem(z, x, []), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:497.1-500.60 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:512.1-515.60 rule `store-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:502.1-506.29 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:517.1-521.29 rule `store-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $nbytes_(nt, c)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:508.1-511.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:523.1-526.52 rule `store-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n,),)), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:513.1-517.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:528.1-532.52 rule `store-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n,),)), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $ibytes_(n, $wrap__($size((Inn : Inn <: numtype)), n, c))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:519.1-522.63 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:534.1-537.63 rule `vstore-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:524.1-527.31 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:539.1-542.31 rule `vstore-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $vbytes_(V128_vectype, c)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:530.1-533.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:545.1-548.52 rule `vstore_lane-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N,), x, ao, j)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:535.1-540.49 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:550.1-555.49 rule `vstore_lane-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx, `b*` : byte*, Jnn : Jnn, M : M}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N,), x, ao, j)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (N = $jsize(Jnn)) -- if ((M!`%`_M.0 : nat <:> rat) = ((128 : nat <:> rat) / (N : nat <:> rat))) -- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), M), c)[j!`%`_laneidx.0]!`%`_lane_.0,))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:549.1-552.37 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:564.1-567.37 rule `memory.grow-succeed`{z : state, at : addrtype, n : n, x : idx, mi : meminst}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `MEMORY.GROW`_instr(x)]), `%;%`_config($with_meminst(z, x, mi), [CONST_instr((at : addrtype <: numtype), `%`_num_((((|$mem(z, x).BYTES_meminst| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) : rat <:> nat),))])) -- if (mi = $growmem($mem(z, x), n)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:554.1-555.84 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:569.1-570.84 rule `memory.grow-fail`{z : state, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `MEMORY.GROW`_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int)),))])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:615.1-616.51 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:630.1-631.51 rule `data.drop`{z : state, x : idx}: `%~>%`(`%;%`_config(z, [`DATA.DROP`_instr(x)]), `%;%`_config($with_data(z, x, []), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:692.1-696.65 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:707.1-711.65 rule `struct.new`{z : state, n : n, `val*` : val*, x : idx, si : structinst, a : addr, `mut?*` : mut?*, `zt*` : storagetype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [`STRUCT.NEW`_instr(x)]), `%;%`_config($add_structinst(z, [si]), [`REF.STRUCT_ADDR`_instr(a)])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)^n{`mut?` <- `mut?*`, zt <- `zt*`},))) -- if (a = |$structinst(z)|) -- if (si = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`, zt <- `zt*`}}) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:713.1-714.55 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:728.1-729.55 rule `struct.set-null`{z : state, val : val, x : idx, i : fieldidx}: `%~>%`(`%;%`_config(z, [`REF.NULL_ADDR`_instr (val : val <: instr) `STRUCT.SET`_instr(x, i)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:716.1-719.46 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:731.1-734.46 rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : fieldidx, `zt*` : storagetype*, `mut?*` : mut?*}: `%~>%`(`%;%`_config(z, [`REF.STRUCT_ADDR`_instr(a) (val : val <: instr) `STRUCT.SET`_instr(x, i)]), `%;%`_config($with_struct(z, a, i!`%`_fieldidx.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_fieldidx.0], val)), [])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`},))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:732.1-737.65 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:747.1-752.65 rule `array.new_fixed`{z : state, n : n, `val*` : val*, x : idx, ai : arrayinst, a : addr, `mut?` : mut?, zt : storagetype}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [`ARRAY.NEW_FIXED`_instr(x, `%`_u32(n,))]), `%;%`_config($add_arrayinst(z, [ai]), [`REF.ARRAY_ADDR`_instr(a)])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((a = |$arrayinst(z)|) /\ (ai = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`}})) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:777.1-778.66 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:792.1-793.66 rule `array.set-null`{z : state, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [`REF.NULL_ADDR`_instr CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:780.1-782.39 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:795.1-797.39 rule `array.set-oob`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$arrayinst(z)[a].FIELDS_arrayinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:784.1-787.44 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:799.1-802.44 rule `array.set-array`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx, zt : storagetype, `mut?` : mut?}: `%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config($with_array(z, a, i!`%`_num_.0, $packfield_(zt, val)), [])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) @@ -17311,12 +17344,12 @@ syntax result = ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax hostfunc = - | `...` + | _HOSTFUNC(text) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax funccode = | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) - | `...` + | _HOSTFUNC(text) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax taginst = @@ -17729,6 +17762,23 @@ def $growmem(meminst : meminst, nat : nat) : meminst? -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat))) def $growmem{x0 : meminst, x1 : nat}(x0, x1) = ?() +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +syntax hostcallresult = + | RES(store : store, result : result) + | BOT + +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +def $hostcall(hostfunc : hostfunc, store : store, val*) : hostcallresult* + +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +def $lift_result(result : result) : instr* + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result{`val*` : val*}(_VALS_result(val*{val <- `val*`})) = (val : val <: instr)*{val <- `val*`} + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result{a : addr}(`(REF.EXN_ADDR%)THROW_REF`_result(a)) = [`REF.EXN_ADDR`_instr(a) THROW_REF_instr] + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result(TRAP_result) = [TRAP_instr] + ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec relation Num_ok: `%|-%:%`(store, num, numtype) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec @@ -18856,131 +18906,147 @@ relation Step: `%~>%`(config, config) `%~>%`(`%;%`_config(`%;%`_state(s, f), [`FRAME_%{%}%`_instr(n, f', instr*{instr <- `instr*`})]), `%;%`_config(`%;%`_state(s', f), [`FRAME_%{%}%`_instr(n, f'', instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(`%;%`_state(s, f'), instr*{instr <- `instr*`}), `%;%`_config(`%;%`_state(s', f''), instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:227.1-231.49 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:184.1-190.59 + rule `call_ref-hostfunc-res`{s : store, f : frame, n : n, `val*` : val*, a : addr, yy : typeuse, s' : store, result : result, fi : funcinst, `t_1*` : valtype*, m : m, `t_2*` : valtype*, hf : text}: + `%~>%`(`%;%`_config(`%;%`_state(s, f), (val : val <: instr)^n{val <- `val*`} ++ [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)]), `%;%`_config(`%;%`_state(s', f), $lift_result(result))) + -- if ($funcinst(`%;%`_state(s, f))[a] = fi) + -- Expand: `%~~%`(fi.TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1^n{t_1 <- `t_1*`},), `%`_resulttype(t_2^m{t_2 <- `t_2*`},))) + -- if (fi.CODE_funcinst = _HOSTFUNC_funccode(hf)) + -- if (RES_hostcallresult(s', result) <- $hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})) + + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:192.1-198.49 + rule `call_ref-hostfunc-div`{s : store, f : frame, n : n, `val*` : val*, a : addr, yy : typeuse, fi : funcinst, `t_1*` : valtype*, m : m, `t_2*` : valtype*, hf : text}: + `%~>%`(`%;%`_config(`%;%`_state(s, f), (val : val <: instr)^n{val <- `val*`} ++ [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)]), `%;%`_config(`%;%`_state(s, f), [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)])) + -- if ($funcinst(`%;%`_state(s, f))[a] = fi) + -- Expand: `%~~%`(fi.TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1^n{t_1 <- `t_1*`},), `%`_resulttype(t_2^m{t_2 <- `t_2*`},))) + -- if (fi.CODE_funcinst = _HOSTFUNC_funccode(hf)) + -- if (BOT_hostcallresult <- $hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})) + + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:242.1-246.49 rule throw{z : state, n : n, `val*` : val*, x : idx, exn : exninst, a : addr, `t*` : valtype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [THROW_instr(x)]), `%;%`_config($add_exninst(z, [exn]), [`REF.EXN_ADDR`_instr(a) THROW_REF_instr])) -- Expand: `%~~%`($as_deftype($tag(z, x).TYPE_taginst), `FUNC%->%`_comptype(`%`_resulttype(t^n{t <- `t*`},), `%`_resulttype([],))) -- if (a = |$exninst(z)|) -- if (exn = {TAG $tagaddr(z)[x!`%`_idx.0], FIELDS val^n{val <- `val*`}}) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:305.1-306.56 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:320.1-321.56 rule `local.set`{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) `LOCAL.SET`_instr(x)]), `%;%`_config($with_local(z, x, val), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:318.1-319.58 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:333.1-334.58 rule `global.set`{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) `GLOBAL.SET`_instr(x)]), `%;%`_config($with_global(z, x, val), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:332.1-334.33 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:347.1-349.33 rule `table.set-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) `TABLE.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:336.1-338.32 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:351.1-353.32 rule `table.set-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) `TABLE.SET`_instr(x)]), `%;%`_config($with_table(z, x, i!`%`_num_.0, ref), [])) -- if (i!`%`_num_.0 < |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:347.1-350.46 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:362.1-365.46 rule `table.grow-succeed`{z : state, ref : ref, at : addrtype, n : n, x : idx, ti : tableinst}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `TABLE.GROW`_instr(x)]), `%;%`_config($with_tableinst(z, x, ti), [CONST_instr((at : addrtype <: numtype), `%`_num_(|$table(z, x).REFS_tableinst|,))])) -- if (ti = !($growtable($table(z, x), n, ref))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:352.1-353.87 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:367.1-368.87 rule `table.grow-fail`{z : state, ref : ref, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `TABLE.GROW`_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int)),))])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:413.1-414.51 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:428.1-429.51 rule `elem.drop`{z : state, x : idx}: `%~>%`(`%;%`_config(z, [`ELEM.DROP`_instr(x)]), `%;%`_config($with_elem(z, x, []), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:497.1-500.60 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:512.1-515.60 rule `store-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:502.1-506.29 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:517.1-521.29 rule `store-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $nbytes_(nt, c)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:508.1-511.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:523.1-526.52 rule `store-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n,),)), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:513.1-517.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:528.1-532.52 rule `store-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n,),)), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $ibytes_(n, $wrap__($size((Inn : Inn <: numtype)), n, c))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:519.1-522.63 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:534.1-537.63 rule `vstore-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:524.1-527.31 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:539.1-542.31 rule `vstore-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $vbytes_(V128_vectype, c)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:530.1-533.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:545.1-548.52 rule `vstore_lane-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N,), x, ao, j)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:535.1-540.49 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:550.1-555.49 rule `vstore_lane-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx, `b*` : byte*, Jnn : Jnn, M : M}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N,), x, ao, j)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (N = $jsize(Jnn)) -- if ((M!`%`_M.0 : nat <:> rat) = ((128 : nat <:> rat) / (N : nat <:> rat))) -- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), M), c)[j!`%`_laneidx.0]!`%`_lane_.0,))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:549.1-552.37 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:564.1-567.37 rule `memory.grow-succeed`{z : state, at : addrtype, n : n, x : idx, mi : meminst}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `MEMORY.GROW`_instr(x)]), `%;%`_config($with_meminst(z, x, mi), [CONST_instr((at : addrtype <: numtype), `%`_num_((((|$mem(z, x).BYTES_meminst| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) : rat <:> nat),))])) -- if (mi = !($growmem($mem(z, x), n))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:554.1-555.84 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:569.1-570.84 rule `memory.grow-fail`{z : state, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `MEMORY.GROW`_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int)),))])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:615.1-616.51 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:630.1-631.51 rule `data.drop`{z : state, x : idx}: `%~>%`(`%;%`_config(z, [`DATA.DROP`_instr(x)]), `%;%`_config($with_data(z, x, []), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:692.1-696.65 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:707.1-711.65 rule `struct.new`{z : state, n : n, `val*` : val*, x : idx, si : structinst, a : addr, `mut?*` : mut?*, `zt*` : storagetype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [`STRUCT.NEW`_instr(x)]), `%;%`_config($add_structinst(z, [si]), [`REF.STRUCT_ADDR`_instr(a)])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)^n{`mut?` <- `mut?*`, zt <- `zt*`},))) -- if (a = |$structinst(z)|) -- if (si = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`, zt <- `zt*`}}) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:713.1-714.55 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:728.1-729.55 rule `struct.set-null`{z : state, val : val, x : idx, i : fieldidx}: `%~>%`(`%;%`_config(z, [`REF.NULL_ADDR`_instr (val : val <: instr) `STRUCT.SET`_instr(x, i)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:716.1-719.46 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:731.1-734.46 rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : fieldidx, `zt*` : storagetype*, `mut?*` : mut?*}: `%~>%`(`%;%`_config(z, [`REF.STRUCT_ADDR`_instr(a) (val : val <: instr) `STRUCT.SET`_instr(x, i)]), `%;%`_config($with_struct(z, a, i!`%`_fieldidx.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_fieldidx.0], val)), [])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`},))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:732.1-737.65 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:747.1-752.65 rule `array.new_fixed`{z : state, n : n, `val*` : val*, x : idx, ai : arrayinst, a : addr, `mut?` : mut?, zt : storagetype}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [`ARRAY.NEW_FIXED`_instr(x, `%`_u32(n,))]), `%;%`_config($add_arrayinst(z, [ai]), [`REF.ARRAY_ADDR`_instr(a)])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((a = |$arrayinst(z)|) /\ (ai = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`}})) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:777.1-778.66 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:792.1-793.66 rule `array.set-null`{z : state, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [`REF.NULL_ADDR`_instr CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:780.1-782.39 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:795.1-797.39 rule `array.set-oob`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$arrayinst(z)[a].FIELDS_arrayinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:784.1-787.44 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:799.1-802.44 rule `array.set-array`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx, zt : storagetype, `mut?` : mut?}: `%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config($with_array(z, a, i!`%`_num_.0, $packfield_(zt, val)), [])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) @@ -29315,12 +29381,12 @@ syntax result = ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax hostfunc = - | `...` + | _HOSTFUNC(text) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax funccode = | FUNC(typeidx : typeidx, `local*` : local*, expr : expr) - | `...` + | _HOSTFUNC(text) ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec syntax taginst = @@ -29733,6 +29799,23 @@ def $growmem(meminst : meminst, nat : nat) : meminst? -- if (i'!`%`_u64.0 <= (2 ^ ((($size((at : addrtype <: numtype)) : nat <:> int) - (16 : nat <:> int)) : int <:> nat))) def $growmem{x0 : meminst, x1 : nat}(x0, x1) = ?() +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +syntax hostcallresult = + | RES(store : store, result : result) + | BOT + +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +def $hostcall(hostfunc : hostfunc, store : store, val*) : hostcallresult* + +;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec +def $lift_result(result : result) : instr* + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result{`val*` : val*}(_VALS_result(val*{val <- `val*`})) = (val : val <: instr)*{val <- `val*`} + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result{a : addr}(`(REF.EXN_ADDR%)THROW_REF`_result(a)) = [`REF.EXN_ADDR`_instr(a) THROW_REF_instr] + ;; ../../../../specification/wasm-latest/4.0-execution.configurations.spectec + def $lift_result(TRAP_result) = [TRAP_instr] + ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec relation Num_ok: `%|-%:%`(store, num, numtype) ;; ../../../../specification/wasm-latest/4.1-execution.values.spectec @@ -30909,7 +30992,27 @@ relation Step: `%~>%`(config, config) `%~>%`(`%;%`_config(`%;%`_state(s, f), [`FRAME_%{%}%`_instr(n, f', instr*{instr <- `instr*`})]), `%;%`_config(`%;%`_state(s', f), [`FRAME_%{%}%`_instr(n, f'', instr'*{instr' <- `instr'*`})])) -- Step: `%~>%`(`%;%`_config(`%;%`_state(s, f'), instr*{instr <- `instr*`}), `%;%`_config(`%;%`_state(s', f''), instr'*{instr' <- `instr'*`})) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:227.1-231.49 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:184.1-190.59 + rule `call_ref-hostfunc-res`{s : store, f : frame, n : n, `val*` : val*, a : addr, yy : typeuse, s' : store, result : result, fi : funcinst, `t_1*` : valtype*, m : m, `t_2*` : valtype*, hf : text}: + `%~>%`(`%;%`_config(`%;%`_state(s, f), (val : val <: instr)^n{val <- `val*`} ++ [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)]), `%;%`_config(`%;%`_state(s', f), $lift_result(result))) + -- if (a < |$funcinst(`%;%`_state(s, f))|) + -- if ($funcinst(`%;%`_state(s, f))[a] = fi) + -- Expand: `%~~%`(fi.TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1^n{t_1 <- `t_1*`},), `%`_resulttype(t_2^m{t_2 <- `t_2*`},))) + -- if (fi.CODE_funcinst = _HOSTFUNC_funccode(hf)) + -- if (|$hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})| > 0) + -- if (RES_hostcallresult(s', result) <- $hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})) + + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:192.1-198.49 + rule `call_ref-hostfunc-div`{s : store, f : frame, n : n, `val*` : val*, a : addr, yy : typeuse, fi : funcinst, `t_1*` : valtype*, m : m, `t_2*` : valtype*, hf : text}: + `%~>%`(`%;%`_config(`%;%`_state(s, f), (val : val <: instr)^n{val <- `val*`} ++ [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)]), `%;%`_config(`%;%`_state(s, f), [`REF.FUNC_ADDR`_instr(a) CALL_REF_instr(yy)])) + -- if (a < |$funcinst(`%;%`_state(s, f))|) + -- if ($funcinst(`%;%`_state(s, f))[a] = fi) + -- Expand: `%~~%`(fi.TYPE_funcinst, `FUNC%->%`_comptype(`%`_resulttype(t_1^n{t_1 <- `t_1*`},), `%`_resulttype(t_2^m{t_2 <- `t_2*`},))) + -- if (fi.CODE_funcinst = _HOSTFUNC_funccode(hf)) + -- if (|$hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})| > 0) + -- if (BOT_hostcallresult <- $hostcall(_HOSTFUNC_hostfunc(hf), s, val^n{val <- `val*`})) + + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:242.1-246.49 rule throw{z : state, n : n, `val*` : val*, x : idx, exn : exninst, a : addr, `t*` : valtype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [THROW_instr(x)]), `%;%`_config($add_exninst(z, [exn]), [`REF.EXN_ADDR`_instr(a) THROW_REF_instr])) -- Expand: `%~~%`($as_deftype($tag(z, x).TYPE_taginst), `FUNC%->%`_comptype(`%`_resulttype(t^n{t <- `t*`},), `%`_resulttype([],))) @@ -30917,74 +31020,74 @@ relation Step: `%~>%`(config, config) -- if (x!`%`_idx.0 < |$tagaddr(z)|) -- if (exn = {TAG $tagaddr(z)[x!`%`_idx.0], FIELDS val^n{val <- `val*`}}) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:305.1-306.56 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:320.1-321.56 rule `local.set`{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) `LOCAL.SET`_instr(x)]), `%;%`_config($with_local(z, x, val), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:318.1-319.58 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:333.1-334.58 rule `global.set`{z : state, val : val, x : idx}: `%~>%`(`%;%`_config(z, [(val : val <: instr) `GLOBAL.SET`_instr(x)]), `%;%`_config($with_global(z, x, val), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:332.1-334.33 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:347.1-349.33 rule `table.set-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) `TABLE.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (i!`%`_num_.0 >= |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:336.1-338.32 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:351.1-353.32 rule `table.set-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), ref : ref, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) (ref : ref <: instr) `TABLE.SET`_instr(x)]), `%;%`_config($with_table(z, x, i!`%`_num_.0, ref), [])) -- if (i!`%`_num_.0 < |$table(z, x).REFS_tableinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:347.1-350.46 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:362.1-365.46 rule `table.grow-succeed`{z : state, ref : ref, at : addrtype, n : n, x : idx, ti : tableinst}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `TABLE.GROW`_instr(x)]), `%;%`_config($with_tableinst(z, x, ti), [CONST_instr((at : addrtype <: numtype), `%`_num_(|$table(z, x).REFS_tableinst|,))])) -- if ($growtable($table(z, x), n, ref) =/= ?()) -- if (ti = !($growtable($table(z, x), n, ref))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:352.1-353.87 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:367.1-368.87 rule `table.grow-fail`{z : state, ref : ref, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [(ref : ref <: instr) CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `TABLE.GROW`_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int)),))])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:413.1-414.51 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:428.1-429.51 rule `elem.drop`{z : state, x : idx}: `%~>%`(`%;%`_config(z, [`ELEM.DROP`_instr(x)]), `%;%`_config($with_elem(z, x, []), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:497.1-500.60 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:512.1-515.60 rule `store-num-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:502.1-506.29 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:517.1-521.29 rule `store-num-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), nt : numtype, c : num_(nt), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr(nt, c) STORE_instr(nt, ?(), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($size(nt) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $nbytes_(nt, c)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:508.1-511.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:523.1-526.52 rule `store-pack-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n,),)), x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:513.1-517.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:528.1-532.52 rule `store-pack-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), Inn : Inn, c : num_((Inn : Inn <: numtype)), n : n, x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) CONST_instr((Inn : Inn <: numtype), c) STORE_instr((Inn : Inn <: numtype), ?(`%`_storeop_(`%`_sz(n,),)), x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((n : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $ibytes_(n, $wrap__($size((Inn : Inn <: numtype)), n, c))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:519.1-522.63 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:534.1-537.63 rule `vstore-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:524.1-527.31 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:539.1-542.31 rule `vstore-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), x : idx, ao : memarg, `b*` : byte*}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_instr(V128_vectype, x, ao)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), ((($vsize(V128_vectype) : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (b*{b <- `b*`} = $vbytes_(V128_vectype, c)) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:530.1-533.52 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:545.1-548.52 rule `vstore_lane-oob`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N,), x, ao, j)]), `%;%`_config(z, [TRAP_instr])) -- if (((i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0) + (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat)) > |$mem(z, x).BYTES_meminst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:535.1-540.49 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:550.1-555.49 rule `vstore_lane-val`{z : state, at : addrtype, i : num_((at : addrtype <: numtype)), c : vec_(V128_Vnn), N : N, x : idx, ao : memarg, j : laneidx, `b*` : byte*, Jnn : Jnn, M : M}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), i) VCONST_instr(V128_vectype, c) VSTORE_LANE_instr(V128_vectype, `%`_sz(N,), x, ao, j)]), `%;%`_config($with_mem(z, x, (i!`%`_num_.0 + ao.OFFSET_memarg!`%`_u64.0), (((N : nat <:> rat) / (8 : nat <:> rat)) : rat <:> nat), b*{b <- `b*`}), [])) -- if (N = $jsize(Jnn)) @@ -30992,54 +31095,54 @@ relation Step: `%~>%`(config, config) -- if (j!`%`_laneidx.0 < |$lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), M), c)|) -- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), M), c)[j!`%`_laneidx.0]!`%`_lane_.0,))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:549.1-552.37 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:564.1-567.37 rule `memory.grow-succeed`{z : state, at : addrtype, n : n, x : idx, mi : meminst}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `MEMORY.GROW`_instr(x)]), `%;%`_config($with_meminst(z, x, mi), [CONST_instr((at : addrtype <: numtype), `%`_num_((((|$mem(z, x).BYTES_meminst| : nat <:> rat) / ((64 * $Ki) : nat <:> rat)) : rat <:> nat),))])) -- if ($growmem($mem(z, x), n) =/= ?()) -- if (mi = !($growmem($mem(z, x), n))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:554.1-555.84 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:569.1-570.84 rule `memory.grow-fail`{z : state, at : addrtype, n : n, x : idx}: `%~>%`(`%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_(n,)) `MEMORY.GROW`_instr(x)]), `%;%`_config(z, [CONST_instr((at : addrtype <: numtype), `%`_num_($inv_signed_($size((at : addrtype <: numtype)), - (1 : nat <:> int)),))])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:615.1-616.51 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:630.1-631.51 rule `data.drop`{z : state, x : idx}: `%~>%`(`%;%`_config(z, [`DATA.DROP`_instr(x)]), `%;%`_config($with_data(z, x, []), [])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:692.1-696.65 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:707.1-711.65 rule `struct.new`{z : state, n : n, `val*` : val*, x : idx, si : structinst, a : addr, `mut?*` : mut?*, `zt*` : storagetype*}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [`STRUCT.NEW`_instr(x)]), `%;%`_config($add_structinst(z, [si]), [`REF.STRUCT_ADDR`_instr(a)])) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)^n{`mut?` <- `mut?*`, zt <- `zt*`},))) -- if (a = |$structinst(z)|) -- if (si = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`, zt <- `zt*`}}) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:713.1-714.55 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:728.1-729.55 rule `struct.set-null`{z : state, val : val, x : idx, i : fieldidx}: `%~>%`(`%;%`_config(z, [`REF.NULL_ADDR`_instr (val : val <: instr) `STRUCT.SET`_instr(x, i)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:716.1-719.46 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:731.1-734.46 rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : fieldidx, `zt*` : storagetype*, `mut?*` : mut?*}: `%~>%`(`%;%`_config(z, [`REF.STRUCT_ADDR`_instr(a) (val : val <: instr) `STRUCT.SET`_instr(x, i)]), `%;%`_config($with_struct(z, a, i!`%`_fieldidx.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_fieldidx.0], val)), [])) -- if (i!`%`_fieldidx.0 < |zt*{zt <- `zt*`}|) -- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`},))) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:732.1-737.65 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:747.1-752.65 rule `array.new_fixed`{z : state, n : n, `val*` : val*, x : idx, ai : arrayinst, a : addr, `mut?` : mut?, zt : storagetype}: `%~>%`(`%;%`_config(z, (val : val <: instr)^n{val <- `val*`} ++ [`ARRAY.NEW_FIXED`_instr(x, `%`_u32(n,))]), `%;%`_config($add_arrayinst(z, [ai]), [`REF.ARRAY_ADDR`_instr(a)])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt))) -- if ((a = |$arrayinst(z)|) /\ (ai = {TYPE $type(z, x), FIELDS $packfield_(zt, val)^n{val <- `val*`}})) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:777.1-778.66 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:792.1-793.66 rule `array.set-null`{z : state, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [`REF.NULL_ADDR`_instr CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:780.1-782.39 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:795.1-797.39 rule `array.set-oob`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx}: `%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config(z, [TRAP_instr])) -- if (a < |$arrayinst(z)|) -- if (i!`%`_num_.0 >= |$arrayinst(z)[a].FIELDS_arrayinst|) - ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:784.1-787.44 + ;; ../../../../specification/wasm-latest/4.3-execution.instructions.spectec:799.1-802.44 rule `array.set-array`{z : state, a : addr, i : num_(I32_numtype), val : val, x : idx, zt : storagetype, `mut?` : mut?}: `%~>%`(`%;%`_config(z, [`REF.ARRAY_ADDR`_instr(a) CONST_instr(I32_numtype, i) (val : val <: instr) `ARRAY.SET`_instr(x)]), `%;%`_config($with_array(z, a, i!`%`_num_.0, $packfield_(zt, val)), [])) -- Expand: `%~~%`($type(z, x), ARRAY_comptype(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)))