Skip to content

[spec] add missing rules for HANDLER #2063

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
zilinc wants to merge 2 commits into
base: main
Choose a base branch
from
+151 −104
Open

[spec] add missing rules for HANDLER #2063

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f3dda39
[spec] add missing context rule for HANDLER
zilinc Jan 30, 2026
cd8b85e
[spec] add missing trap rule for HANDLER
zilinc Jan 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions specification/wasm-3.0/4.3-execution.instructions.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,10 @@ rule Step/ctxt-frame:
s; f; (FRAME_ n `{f'} instr*) ~> s'; f; (FRAME_ n `{f''} instr'*)
-- Step: s; f'; instr* ~> s'; f''; instr'*

rule Step/ctxt-handler:
z; (HANDLER_ n `{catch*} instr*) ~> z'; (HANDLER_ n `{catch*} instr'*)
-- Step: z; instr* ~> z'; instr'*


;; Polymorphic instructions

Expand Down Expand Up @@ -292,6 +296,9 @@ rule Step_pure/trap-label:
rule Step_pure/trap-frame:
(FRAME_ n `{f} TRAP) ~> TRAP

rule Step_pure/trap-handler:
(HANDLER_ n `{catch*} TRAP) ~> TRAP


;; Local instructions

Expand Down
61 changes: 35 additions & 26 deletions spectec/test-frontend/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6083,6 +6083,10 @@ relation Step_pure: `%~>%`(instr*, instr*)
rule `trap-frame`{n : n, f : frame}:
`%~>%`([`FRAME_%{%}%`_instr(n, f, [TRAP_instr])], [TRAP_instr])

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule `trap-handler`{n : n, `catch*` : catch*}:
`%~>%`([`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, [TRAP_instr])], [TRAP_instr])

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec
rule local.tee{val : val, x : idx}:
`%~>%`([(val : val <: instr) LOCAL.TEE_instr(x)], [(val : val <: instr) (val : val <: instr) LOCAL.SET_instr(x)])
Expand Down Expand Up @@ -6909,131 +6913,136 @@ 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-3.0/4.3-execution.instructions.spectec:227.1-231.49
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:45.1-47.36
rule `ctxt-handler`{z : state, n : n, `catch*` : catch*, `instr*` : instr*, z' : state, `instr'*` : instr*}:
`%~>%`(`%;%`_config(z, [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr*{instr <- `instr*`})]), `%;%`_config(z', [`HANDLER_%{%}%`_instr(n, catch*{catch <- `catch*`}, instr'*{instr' <- `instr'*`})]))
-- Step: `%~>%`(`%;%`_config(z, instr*{instr <- `instr*`}), `%;%`_config(z', instr'*{instr' <- `instr'*`}))

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:231.1-235.49
rule throw{z : state, `val*` : val*, n : n, 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-3.0/4.3-execution.instructions.spectec:302.1-303.56
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:309.1-310.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-3.0/4.3-execution.instructions.spectec:315.1-316.58
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:322.1-323.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-3.0/4.3-execution.instructions.spectec:329.1-331.33
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:336.1-338.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-3.0/4.3-execution.instructions.spectec:333.1-335.32
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:340.1-342.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-3.0/4.3-execution.instructions.spectec:344.1-347.46
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:351.1-354.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-3.0/4.3-execution.instructions.spectec:349.1-350.87
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:356.1-357.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-3.0/4.3-execution.instructions.spectec:410.1-411.51
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:417.1-418.51
rule elem.drop{z : state, x : idx}:
`%~>%`(`%;%`_config(z, [ELEM.DROP_instr(x)]), `%;%`_config($with_elem(z, x, []), []))

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:494.1-497.60
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:501.1-504.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-3.0/4.3-execution.instructions.spectec:499.1-503.29
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:506.1-510.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-3.0/4.3-execution.instructions.spectec:505.1-508.52
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:512.1-515.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-3.0/4.3-execution.instructions.spectec:510.1-514.52
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:517.1-521.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-3.0/4.3-execution.instructions.spectec:516.1-519.63
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:523.1-526.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-3.0/4.3-execution.instructions.spectec:521.1-524.31
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:528.1-531.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-3.0/4.3-execution.instructions.spectec:527.1-530.50
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:534.1-537.50
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) > |$mem(z, x).BYTES_meminst|)

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:532.1-537.49
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:539.1-544.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 : nat <:> rat) = ((128 : nat <:> rat) / (N : nat <:> rat)))
-- if (b*{b <- `b*`} = $ibytes_(N, `%`_iN($lanes_(`%X%`_shape((Jnn : Jnn <: lanetype), `%`_dim(M)), c)[j!`%`_laneidx.0]!`%`_lane_.0)))

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:546.1-549.37
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:553.1-556.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-3.0/4.3-execution.instructions.spectec:551.1-552.84
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:558.1-559.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-3.0/4.3-execution.instructions.spectec:612.1-613.51
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:619.1-620.51
rule data.drop{z : state, x : idx}:
`%~>%`(`%;%`_config(z, [DATA.DROP_instr(x)]), `%;%`_config($with_data(z, x, []), []))

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:693.1-697.65
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:700.1-704.65
rule struct.new{z : state, `val*` : val*, n : n, 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-3.0/4.3-execution.instructions.spectec:714.1-715.53
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:721.1-722.53
rule `struct.set-null`{z : state, ht : heaptype, val : val, x : idx, i : u32}:
`%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) (val : val <: instr) STRUCT.SET_instr(x, i)]), `%;%`_config(z, [TRAP_instr]))

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:717.1-720.46
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:724.1-727.46
rule `struct.set-struct`{z : state, a : addr, val : val, x : idx, i : u32, `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!`%`_u32.0, $packfield_(zt*{zt <- `zt*`}[i!`%`_u32.0], val)), []))
-- Expand: `%~~%`($type(z, x), STRUCT_comptype(`%`_list(`%%`_fieldtype(mut?{mut <- `mut?`}, zt)*{`mut?` <- `mut?*`, zt <- `zt*`})))

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:733.1-738.65
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:740.1-745.65
rule array.new_fixed{z : state, `val*` : val*, n : n, 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-3.0/4.3-execution.instructions.spectec:778.1-779.64
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:785.1-786.64
rule `array.set-null`{z : state, ht : heaptype, i : num_(I32_numtype), val : val, x : idx}:
`%~>%`(`%;%`_config(z, [REF.NULL_instr(ht) CONST_instr(I32_numtype, i) (val : val <: instr) ARRAY.SET_instr(x)]), `%;%`_config(z, [TRAP_instr]))

;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:781.1-783.39
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:788.1-790.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-3.0/4.3-execution.instructions.spectec:785.1-788.44
;; ../../../../specification/wasm-3.0/4.3-execution.instructions.spectec:792.1-795.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)))
Expand Down
2 changes: 2 additions & 0 deletions spectec/test-latex/TEST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9644,6 +9644,7 @@ $$
\end{array} \\
{[\textsc{\scriptsize E{-}ctxt{-}label}]} \quad & z ; ({{\mathsf{label}}_{n}}{\{ {{\mathit{instr}}_0^\ast} \}}~{{\mathit{instr}}^\ast}) & \hookrightarrow & {z'} ; ({{\mathsf{label}}_{n}}{\{ {{\mathit{instr}}_0^\ast} \}}~{{\mathit{instr}'}^\ast}) & \quad \mbox{if}~ z ; {{\mathit{instr}}^\ast} \hookrightarrow {z'} ; {{\mathit{instr}'}^\ast} \\
{[\textsc{\scriptsize E{-}ctxt{-}frame}]} \quad & s ; f ; ({{\mathsf{frame}}_{n}}{\{ {f'} \}}~{{\mathit{instr}}^\ast}) & \hookrightarrow & {s'} ; f ; ({{\mathsf{frame}}_{n}}{\{ {f''} \}}~{{\mathit{instr}'}^\ast}) & \quad \mbox{if}~ s ; {f'} ; {{\mathit{instr}}^\ast} \hookrightarrow {s'} ; {f''} ; {{\mathit{instr}'}^\ast} \\
{[\textsc{\scriptsize E{-}ctxt{-}handler}]} \quad & z ; ({{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~{{\mathit{instr}}^\ast}) & \hookrightarrow & {z'} ; ({{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~{{\mathit{instr}'}^\ast}) & \quad \mbox{if}~ z ; {{\mathit{instr}}^\ast} \hookrightarrow {z'} ; {{\mathit{instr}'}^\ast} \\
\end{array}
$$

Expand Down Expand Up @@ -9897,6 +9898,7 @@ $$
{[\textsc{\scriptsize E{-}trap{-}instrs}]} \quad & {{\mathit{val}}^\ast}~\mathsf{trap}~{{\mathit{instr}}^\ast} & \hookrightarrow & \mathsf{trap} & \quad \mbox{if}~ {{\mathit{val}}^\ast} \neq \epsilon \lor {{\mathit{instr}}^\ast} \neq \epsilon \\
{[\textsc{\scriptsize E{-}trap{-}label}]} \quad & ({{\mathsf{label}}_{n}}{\{ {{\mathit{instr}'}^\ast} \}}~\mathsf{trap}) & \hookrightarrow & \mathsf{trap} \\
{[\textsc{\scriptsize E{-}trap{-}frame}]} \quad & ({{\mathsf{frame}}_{n}}{\{ f \}}~\mathsf{trap}) & \hookrightarrow & \mathsf{trap} \\
{[\textsc{\scriptsize E{-}trap{-}handler}]} \quad & ({{\mathsf{handler}}_{n}}{\{ {{\mathit{catch}}^\ast} \}}~\mathsf{trap}) & \hookrightarrow & \mathsf{trap} \\
\end{array}
$$

Expand Down
Loading